-
Notifications
You must be signed in to change notification settings - Fork 0
/
simplebool.pl
87 lines (70 loc) · 2.79 KB
/
simplebool.pl
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
:- style_check(-singleton).
% ------------------------ SYNTAX ------------------------
t(T) :- T = bool
; T = nat
; T = var(X) , atom(X)
; T = arr(T1,T2) , t(T1),t(T2)
.
m(M) :- M = true
; M = false
; M = if(M1,M2,M3) , m(M1),m(M2),m(M3)
; M = zero
; M = succ(M1) , m(M1)
; M = pred(M1) , m(M1)
; M = iszero(M1) , m(M1)
; M = var(X) , atom(X)
; M = fn(X,T1,M1) , atom(X),t(T1),m(M1)
; M = app(M1,M2) , m(M1),m(M2)
.
% ------------------------ SUBSTITUTION ------------------------
%subst(J,M,A,B):-writeln(subst(J,M,A,B)),fail.
subst(J,M,if(M1, M2, M3), if(M1_,M2_,M3_)) :- subst(J,M,M1,M1_), subst(J,M,M2,M2_), subst(J,M,M3,M3_).
subst(J,M,var(J), M).
subst(J,M,var(X), var(X)).
subst(J,M,fn(X,T1,M2),fn(X,T1,M2_)) :-subst2(X,J,M,M2,M2_).
subst(J,M,app(M1, M2), app(M1_,M2_)) :- subst(J,M,M1,M1_), subst(J,M,M2,M2_).
%subst(J,M,A,B):-writeln(error:subst(J,M,A,B)),fail.
subst2(J,J,M,S,S).
subst2(X,J,M,S,M_) :- subst(J,M,S,M_).
getb(Γ,X,B) :- member(X-B,Γ).
gett(Γ,X,T) :- getb(Γ,X,bVar(T)).
%gett(Γ,X,_) :- writeln(error:gett(Γ,X)),fail.
% ------------------------ EVALUATION ------------------------
v(true).
v(false).
v(fn(_,_,_)).
%eval1(_,M,_) :- writeln(eval1:M),fail.
eval1(Γ,app(fn(X,T11,M12),V2),R) :- v(V2), subst(X, V2, M12, R).
eval1(Γ,app(V1,M2),app(V1, M2_)) :- v(V1), eval1(Γ,M2,M2_).
eval1(Γ,app(M1,M2),app(M1_, M2)) :- eval1(Γ,M1,M1_).
eval1(Γ,if(true,M2,_), M2).
eval1(Γ,if(false,_,M3), M3).
eval1(Γ,if(M1,M2,M3), if(M1_, M2, M3)) :- eval1(Γ,M1,M1_).
eval(Γ,M,M_) :- eval1(Γ,M,M1), eval(Γ,M1,M_).
eval(Γ,M,M).
% ------------------------ TYPING ------------------------
typeof(Γ,true,bool).
typeof(Γ,false,bool).
typeof(Γ,if(M1,M2,M3), T2) :- typeof(Γ, M1,bool), typeof(Γ, M2, T2), typeof(Γ, M3, T2).
typeof(Γ,var(X),T) :- gett(Γ, X, T).
typeof(Γ,fn(X,T1,M2), arr(T1, T2_)) :- typeof([X-bVar(T1)|Γ],M2,T2_).
typeof(Γ,app(M1,M2),T12) :- typeof(Γ,M1,arr(T11,T12)), typeof(Γ,M2,T11).
% ------------------------ MAIN ------------------------
run(eval(M),Γ,Γ) :- !,m(M),!,typeof(Γ,M,T),!,eval(Γ,M,M_),!,writeln(M_:T).
run(bind(X,T),Γ,[X-bVar(T)|Γ]) :- !,writeln(X : T).
run(Ls) :- foldl(run,Ls,[],_).
% ------------------------ TEST ------------------------
:- run([
eval(fn(x,bool,var(x))),
eval(fn(x,bool,fn(x,bool, var(x)))),
eval(app(
fn(x,arr(bool,bool), if(app(var(x), false), true,false)),
fn(x,bool, if(var(x),false,true)))),
bind(a,bool),
eval(var(a)),
eval(app(fn(x,bool, var(x)), var(a))),
eval(app(fn(x,bool, app(fn(x,bool, var(x)), var(x))), var(a))),
eval(app(fn(x,bool, var(x)), true)),
eval(app(fn(x,bool, app(fn(x,bool, var(x)), var(x))), true))
]).
:- halt.