Many hyperlinks are disabled.
Use anonymous login
to enable hyperlinks.
Changes In Branch gaunilo-trunk Excluding Merge-Ins
This is equivalent to a diff from df2b019c62 to acdfa4bc62
|
2021-02-11
| ||
| 09:53 | created new branch for anselmpro Leaf check-in: bafa31e486 user: kbg tags: anselmpro-trunk | |
|
2021-02-08
| ||
| 16:14 | First development release of Gaunilo. Working simply-typed intepreter. Leaf check-in: a0652b5805 user: kbg tags: trunk, gaunilo-0.0.0 | |
|
2021-02-05
| ||
| 19:50 | merged in config files from trunk check-in: ec18ae98bb user: kbg tags: gaunilo-dev-kbg | |
|
2021-02-03
| ||
| 17:08 | added config files to trunk check-in: 048ee2582b user: kbg tags: trunk | |
| 17:07 | added config files Leaf check-in: acdfa4bc62 user: kbg tags: gaunilo-trunk | |
| 17:05 | created new branch for configuration settings Leaf check-in: 7f78cd7e4b user: kbg tags: config-trunk | |
|
2021-01-28
| ||
| 21:33 | working interpreter for simply-typed CBPV core calculus check-in: abd171e106 user: kbg tags: gaunilo-trunk | |
|
2021-01-27
| ||
| 08:51 | Added new branch for Anselm specification Leaf check-in: ff5a39bb74 user: kbg tags: spec-trunk | |
|
2021-01-26
| ||
| 04:37 | added branch for gaunilo development check-in: 6db864f704 user: kbg tags: gaunilo-trunk | |
| 04:31 | added branch for site development check-in: 1421c0cb5a user: kbg tags: site-trunk | |
| 04:28 | initial commit check-in: df2b019c62 user: kbg tags: trunk, initial_commit | |
|
2021-01-25
| ||
| 16:14 | initial empty check-in check-in: 168a5a3a04 user: anselm_admin tags: trunk | |
Added .fossil-settings/clean-glob.
1 +*.o 2 +*.exe
Added .fossil-settings/ignore-glob.
1 +x-*/* 2 +*.*~ 3 +*build/* 4 +*.test
Added gaunilo/readme.md.
1 +# Gaunilo 2 + 3 +This directory contains the code for *Gaunilo*, the core dependently 4 +typed CBPV calculus that Anselm is formalized in terms of.
Added gaunilo/src/eval.pro.
1 +:- module(eval, [eval/3]). 2 +:- use_module(library(clpfd)). 3 + 4 +eval([X-V|_],var(X),V). 5 +eval([_|T],var(X),V) :- eval(T,var(X),V). 6 +eval([],var(X),_) :- throw(lookup_failure(X)). 7 + 8 +eval(_,int(K),vint(K)). 9 +eval(_,bool(B),vbool(B)). 10 +eval(E,thunk(T),vthunk(E,T)). 11 +eval(E,fun(X,_,B),vfun(E,X,B)). 12 +eval(E,plus(X0,Y0),vint(Z)) :- 13 + eval(E,X0,vint(X1)), eval(E,Y0,vint(Y1)), Z #= X1 + Y1. 14 +eval(E,minus(X0,Y0),vint(Z)) :- 15 + eval(E,X0,vint(X1)), eval(E,Y0,vint(Y1)), Z #= X1 - Y1. 16 +eval(E,times(X0,Y0),vint(Z)) :- 17 + eval(E,X0,vint(X1)), eval(E,Y0,vint(Y1)), Z #= X1 * Y1. 18 +eval(E,equal(X0,Y0),vbool(true)) :- eval(E,X0,vint(Z)), eval(E,Y0,vint(Z)). 19 +eval(E,equal(X0,Y0),vbool(false)) :- 20 + eval(E,X0,vint(X1)), eval(E,Y0,vint(Y1)), X1 #\= Y1. 21 +eval(E,less(X0,Y0),vbool(true)) :- 22 + eval(E,X0,vint(X1)), eval(E,Y0,vint(Y1)), X1 #< Y1. 23 +eval(E,equal(X0,Y0),vbool(false)) :- 24 + eval(E,X0,vint(X1)), eval(E,Y0,vint(Y1)), X1 #>= Y1. 25 +eval(E,if(X,C,_),Z) :- eval(E,X,vbool(true)), eval(E,C,Z). 26 +eval(E,if(X,_,C),Z) :- eval(E,X,vbool(false)), eval(E,C,Z). 27 +eval(E,apply(F0,A0),Z) :- 28 + eval(E,F0,vfun(E1,X,B)), eval(E,A0,A1), eval([X-A1|E1],B,Z). 29 +eval(E,let(X,V,B),Z) :- eval(E,V,W), eval([X-W|E],B,Z). 30 +eval(E,seq(X,V,B),Z) :- eval(E,V,vreturn(W)), eval([X-W|E],B,Z). 31 +eval(E,return(V),vreturn(Z)) :- eval(E,V,Z). 32 +eval(E,force(C),Z) :- eval(E,C,vthunk(E1,B)), eval(E1,B,Z).
Added gaunilo/src/gaunilo.pro.
1 +:- use_module('lexer.pro'). 2 +:- use_module('parser.pro'). 3 +:- use_module('type.pro'). 4 +:- use_module('eval.pro'). 5 + 6 +do(S,L,E,T,Z) :- 7 + parse(lexer(L),S), phrase(expr(E),L), type([],T,E), eval([],E,Z).
Added gaunilo/src/lexer.pro.
1 +:- module(lexer, [lexer//1, token//1]). 2 +:- use_module(library(dcg/basics)). 3 + 4 +lexer([]) --> []. 5 +lexer([token(H)|T]) --> token(H), sp, lexer(T). 6 + 7 +token(A) --> {key(K)}, K, {atom_string(A,K)}. 8 +token(id(S)) --> ident(S), !, {\+ key(S)}. 9 +token(int(I)) --> integer(I). 10 +token(arrow) --> "->". 11 +token(ascript) --> "::". 12 +token(thick) --> "=>". 13 +token(assign) --> ":=". 14 +token(eq) --> "=". 15 +token(less) --> "<". 16 +token(plus) --> "+". 17 +token(minus) --> "-". 18 +token(times) --> "*". 19 +token(brk(curly,left)) --> "{". 20 +token(brk(curly,right)) --> "}". 21 +token(brk(paren,left)) --> "(". 22 +token(brk(paren,right)) --> ")". 23 + 24 +int(I) --> integer(I). 25 + 26 +ident(S) --> alt([range("AZ"), range("az")], H), 27 + star(alt([range("__"), range("AZ"), range("az"), range("09")]),T), 28 + {string_codes(S,[H|T])}. 29 + 30 +key("int"). 31 +key("bool"). 32 + 33 +key("force"). 34 +key("return"). 35 +key("let"). 36 +key("seq"). 37 +key("if"). 38 +key("then"). 39 +key("else"). 40 +key("exec"). 41 +key("end"). 42 +key("fun"). 43 +key("rec"). 44 + 45 +key("true"). 46 +key("false"). 47 + 48 +key("F"). 49 +key("U"). 50 + 51 +alt([H|T],C) --> call(H,C); alt(T,C). 52 + 53 +range(R,C) --> [C], {string_codes(R,[L,H]), between(L,H,C)}. 54 + 55 +star(G,[H|T]) --> call(G,H), star(G,T). 56 +star(_,[]) --> []. 57 + 58 +nil([]) --> []. 59 + 60 +sp --> []; (" "; "\t"; "\r"; "\n"), sp.
Added gaunilo/src/parser.pro.
1 +:- module(parser, [parse/2, file/2, expr//1]). 2 + 3 +parse(G,S) :- 4 + split_string(S,"","\s\t\n",[N]), string_codes(N,C), phrase(G,C). 5 +file(G,F) :- read_file_to_string(F,S,[]), parse(G,S). 6 + 7 +:- op(900,fy,#). 8 +:- table (expr//1, type//1) as incremental. 9 + 10 +expr(E) --> #brk(paren,left), expr(E), #brk(paren,right). 11 +expr(int(I)) --> #int(I). 12 +expr(bool(true)) --> #true. 13 +expr(bool(false)) --> #false. 14 +expr(var(V)) --> #id(V). 15 +expr(force(A)) --> #force, expr(A). 16 +expr(thunk(A)) --> #brk(curly,left), expr(A), #brk(curly,right). 17 +expr(return(A)) --> #return, expr(A). 18 +expr(apply(A,N)) --> expr(A), expr(N). 19 +expr(plus(X,Y)) --> expr(X), #plus, expr(Y). 20 +expr(minus(X,Y)) --> expr(X), #minus, expr(Y). 21 +expr(times(X,Y)) --> expr(X), #times, expr(Y). 22 +expr(equal(X,Y)) --> expr(X), #eq, expr(Y). 23 +expr(less(X,Y)) --> expr(X), #less, expr(Y). 24 +expr(let(V,E,B)) --> #let, #id(V), #assign, expr(E), #exec, expr(B), #end. 25 +expr(seq(V,E,B)) --> #seq, #id(V), #assign, expr(E), #exec, expr(B), #end. 26 +expr(if(X,T,E)) --> #if, expr(X), #then, expr(T), #else, expr(E), #end. 27 +expr(fun(X,T,B)) --> #fun, #id(X), #ascript, type(T), #thick, expr(B), #end. 28 +expr(rec(X,T,B)) --> #rec, #id(X), #ascript, type(T), #thick, expr(B), #end. 29 + 30 +type(T) --> #brk(paren,left), type(T), #brk(paren,right). 31 +type(carrow(I,O)) --> type(I), #arrow, type(O). 32 +type(vforget(T)) --> #'U', type(T). 33 +type(cfree(T)) --> #'F', type(T). 34 +type(vint) --> #int. 35 +type(vbool) --> #bool. 36 + 37 +#(T) --> [token(T)].
Added gaunilo/src/type.pro.
1 +:- module(type, [polarity/2, type/3]). 2 + 3 +lookup([K-V|_],K,V). % fix backtracking over this 4 +lookup([_|T],K,V) :- lookup(T,K,V). 5 +lookup([],K,_) :- throw(lookup_failure(K)). 6 + 7 +polarity(comp,cfree(T)) :- polarity(val,T). 8 +polarity(comp,carrow(T0,T1)) :- polarity(val,T0), polarity(comp,T1). 9 +polarity(val,vint). 10 +polarity(val,vbool). 11 +polarity(val,vforget(T)) :- polarity(comp,T). 12 + 13 +type(C,T,var(X)) :- lookup(C,X,T). 14 +type(_,vint,int(_)). 15 +type(_,vbool,bool(_)). 16 +type(C,vint,plus(X,Y)) :- type(C,vint,X), type(C,vint,Y). 17 +type(C,vint,minus(X,Y)) :- type(C,vint,X), type(C,vint,Y). 18 +type(C,vint,times(X,Y)) :- type(C,vint,X), type(C,vint,Y). 19 +type(C,vbool,equal(X,Y)) :- type(C,vint,X), type(C,vint,Y). 20 +type(C,vbool,less(X,Y)) :- type(C,vint,X), type(C,vint,Y). 21 + 22 +type(C,T,if(X,Y,Z)) :- 23 + type(C,vbool,X), type(C,T,Y), polarity(comp,T), type(C,T,Z). 24 +type(C,carrow(P,T),fun(X,P,B)) :- 25 + polarity(comp,carrow(P,T)), type([X-P|C],T,B). 26 +type(C,T1,apply(X,Y)) :- type(C,carrow(T0,T1),X), type(C,T0,Y). 27 +type(C,T1,seq(V,E,B)) :- 28 + type(C,cfree(T0),E), polarity(val,T0), type([V-T0],T1,B), polarity(comp,T1). 29 +type(C,T1,let(V,E,B)) :- 30 + type(C,T0,E), polarity(val,T0), type([V-T0|C],T1,B), polarity(comp,T1). 31 +type(C,cfree(T),return(E)) :- type(C,T,E), polarity(val,T). 32 + 33 +type(C,T,force(E)) :- type(C,vforget(T),E), polarity(comp,T). 34 +type(C,vforget(T),thunk(E)) :- type(C,T,E), polarity(comp,T). 35 +type(C,vforget(T),rec(X,T,B)) :- polarity(comp,T), type([X-vforget(T)|C],T,B).