hsk

% Dervation System EvalContML4
:- module('EvalContML4',[
  op(640,xfy,[$,$>]),
  op(700,xfy,=>),
  op(750,xfx,⇓),
  op(780,xfx,⊦),
  op(1200,xfx,--),
  v/1,k/1,e/1,'⊦'/2,'⇓'/2
]).

hsk

% Dervation System EvalContML1
:- use_module(rtg).
:- op(650,xfy, ≫ ).
:- op(700,xfy, ⇒).
:- op(750,xfx, ⇓).
:- op(1200,xfx, --).
term_expansion(A--B,B:-A).

% Syntax
syntax(integer). int ::= integer. bool ::= true | false.

hsk

import Control.Monad.IO.Class
type X = String
type Env = X->E
newtype Clo = Clo Env
instance Show Clo where show _ = "_"
data E = I Int | Abs X E | Cls Clo X E | E :$ E | E :+ E | V X deriving Show

extends :: X -> E -> Env -> X -> E
extends x e env y | x == y = e 
extends _ _ env y          = env y

hsk

module Main where
import Control.Monad.State
import Control.Monad.Coroutine
import Control.Monad.Coroutine.SuspensionFunctors

crst :: Coroutine (Yield Int) (StateT Int IO) Int
crst = do v<-lift get;yield v;lift(modify(+1));liftIO(putStr "動く">>print(v*10)); return (v*10)

runT :: MonadIO m=>Coroutine (Yield Int) m Int -> m Int
runT c = resume c>>=g where

hsk

:- op(500,yfx,[$]).
type(bool=[true,false]).
type(list=[nil,cons$[_,list]]).
ty(K) :- type(K=_).
ty(U->V) :- ty(U),ty(V).
tm(X) :- atom(X).
tm(λ(X:U,V)) :- atom(X),ty(U),tm(V).
tm(T$U) :- tm(T),tm(U).
tm(C) :- type(_=Ts),member(C,Ts).
tm(C$Ls) :- type(_=Ts),member(C$Cs,Ts),length(Ls,L),length(Cs,L),maplist(tm,Ls).

hsk

/*
e ::= 式
| i 整数
| x 変数
| e+e 足し算
| [e1,...,ei] リスト(0<=i<=n)
| {e:[e1,...,ei]} 関数呼び出し(0<=i<=n)
| e;e 文
| x=e 変数代入
d ::= 宣言

hsk

  :- tpp(
      type Colour = 'MkColour'!(int,int,int);
      type Point = 'MkPoint'!(float,float);
      type CPoint = 'MkCPoint'!(float,float,Colour);
      val 'MkColour' : (int->int->int->Colour);
      val c1 : (Colour->int);
      val c2 : (Colour->int);
      val c3 : (Colour->int);
      val 'MkPoint' : (float->float->Point);
      val pt1 : (Point->float);

hsk

$ swipl test.pl
7

hsk

test: test1 test2
test1:
	swipl funtest.pl
test2:
	swipl funtest.pl fun2

hsk

% An algorithm for type-checking dependent types

:- op(650,xfy,$).
:- op(900,xfy,[=>,->,⇓]).
:- op(920,xfx,[⊢]).
failwith(A,L) :- format(A,L),halt.

% Syntax

id(Id)               :- atom(Id).                      % Identify