ADDED   .fossil-settings/clean-glob
Index: .fossil-settings/clean-glob
==================================================================
--- .fossil-settings/clean-glob
+++ .fossil-settings/clean-glob
@@ -0,0 +1,2 @@
+*.o
+*.exe

ADDED   .fossil-settings/ignore-glob
Index: .fossil-settings/ignore-glob
==================================================================
--- .fossil-settings/ignore-glob
+++ .fossil-settings/ignore-glob
@@ -0,0 +1,4 @@
+x-*/*
+*.*~
+*build/*
+*.test

ADDED   gaunilo/readme.md
Index: gaunilo/readme.md
==================================================================
--- gaunilo/readme.md
+++ gaunilo/readme.md
@@ -0,0 +1,4 @@
+# Gaunilo
+
+This directory contains the code for *Gaunilo*, the core dependently
+typed CBPV calculus that Anselm is formalized in terms of.

ADDED   gaunilo/src/eval.pro
Index: gaunilo/src/eval.pro
==================================================================
--- gaunilo/src/eval.pro
+++ gaunilo/src/eval.pro
@@ -0,0 +1,32 @@
+:- module(eval, [eval/3]).
+:- use_module(library(clpfd)).
+
+eval([X-V|_],var(X),V).
+eval([_|T],var(X),V) :- eval(T,var(X),V).
+eval([],var(X),_) :- throw(lookup_failure(X)).
+
+eval(_,int(K),vint(K)).
+eval(_,bool(B),vbool(B)).
+eval(E,thunk(T),vthunk(E,T)).
+eval(E,fun(X,_,B),vfun(E,X,B)).
+eval(E,plus(X0,Y0),vint(Z)) :-
+    eval(E,X0,vint(X1)), eval(E,Y0,vint(Y1)), Z #= X1 + Y1.
+eval(E,minus(X0,Y0),vint(Z)) :-
+    eval(E,X0,vint(X1)), eval(E,Y0,vint(Y1)), Z #= X1 - Y1.
+eval(E,times(X0,Y0),vint(Z)) :-
+    eval(E,X0,vint(X1)), eval(E,Y0,vint(Y1)), Z #= X1 * Y1.
+eval(E,equal(X0,Y0),vbool(true)) :- eval(E,X0,vint(Z)), eval(E,Y0,vint(Z)).
+eval(E,equal(X0,Y0),vbool(false)) :-
+    eval(E,X0,vint(X1)), eval(E,Y0,vint(Y1)), X1 #\= Y1.
+eval(E,less(X0,Y0),vbool(true)) :-
+    eval(E,X0,vint(X1)), eval(E,Y0,vint(Y1)), X1 #< Y1.
+eval(E,equal(X0,Y0),vbool(false)) :-
+    eval(E,X0,vint(X1)), eval(E,Y0,vint(Y1)), X1 #>= Y1.
+eval(E,if(X,C,_),Z) :- eval(E,X,vbool(true)), eval(E,C,Z).
+eval(E,if(X,_,C),Z) :- eval(E,X,vbool(false)), eval(E,C,Z).
+eval(E,apply(F0,A0),Z) :-
+    eval(E,F0,vfun(E1,X,B)), eval(E,A0,A1), eval([X-A1|E1],B,Z).
+eval(E,let(X,V,B),Z) :- eval(E,V,W), eval([X-W|E],B,Z).
+eval(E,seq(X,V,B),Z) :- eval(E,V,vreturn(W)), eval([X-W|E],B,Z).
+eval(E,return(V),vreturn(Z)) :- eval(E,V,Z).
+eval(E,force(C),Z) :- eval(E,C,vthunk(E1,B)), eval(E1,B,Z).

ADDED   gaunilo/src/gaunilo.pro
Index: gaunilo/src/gaunilo.pro
==================================================================
--- gaunilo/src/gaunilo.pro
+++ gaunilo/src/gaunilo.pro
@@ -0,0 +1,7 @@
+:- use_module('lexer.pro').
+:- use_module('parser.pro').
+:- use_module('type.pro').
+:- use_module('eval.pro').
+
+do(S,L,E,T,Z) :-
+    parse(lexer(L),S), phrase(expr(E),L), type([],T,E), eval([],E,Z).

ADDED   gaunilo/src/lexer.pro
Index: gaunilo/src/lexer.pro
==================================================================
--- gaunilo/src/lexer.pro
+++ gaunilo/src/lexer.pro
@@ -0,0 +1,60 @@
+:- module(lexer, [lexer//1, token//1]).
+:- use_module(library(dcg/basics)).
+
+lexer([]) --> [].
+lexer([token(H)|T]) --> token(H), sp, lexer(T).
+
+token(A) --> {key(K)}, K, {atom_string(A,K)}.
+token(id(S)) --> ident(S), !, {\+ key(S)}.
+token(int(I)) --> integer(I).
+token(arrow) --> "->".
+token(ascript) --> "::".
+token(thick) --> "=>".
+token(assign) --> ":=".
+token(eq) --> "=".
+token(less) --> "<".
+token(plus) --> "+".
+token(minus) --> "-".
+token(times) --> "*".
+token(brk(curly,left)) --> "{".
+token(brk(curly,right)) --> "}".
+token(brk(paren,left)) --> "(".
+token(brk(paren,right)) --> ")".
+
+int(I) --> integer(I).
+
+ident(S) --> alt([range("AZ"), range("az")], H),
+             star(alt([range("__"), range("AZ"), range("az"), range("09")]),T),
+             {string_codes(S,[H|T])}.
+
+key("int").
+key("bool").
+
+key("force").
+key("return").
+key("let").
+key("seq").
+key("if").
+key("then").
+key("else").
+key("exec").
+key("end").
+key("fun").
+key("rec").
+
+key("true").
+key("false").
+
+key("F").
+key("U").
+
+alt([H|T],C) --> call(H,C); alt(T,C).
+
+range(R,C) --> [C], {string_codes(R,[L,H]), between(L,H,C)}.
+
+star(G,[H|T]) --> call(G,H), star(G,T).
+star(_,[]) --> [].
+
+nil([]) --> [].
+
+sp --> []; (" "; "\t"; "\r"; "\n"), sp.

ADDED   gaunilo/src/parser.pro
Index: gaunilo/src/parser.pro
==================================================================
--- gaunilo/src/parser.pro
+++ gaunilo/src/parser.pro
@@ -0,0 +1,37 @@
+:- module(parser, [parse/2, file/2, expr//1]).
+
+parse(G,S) :-
+    split_string(S,"","\s\t\n",[N]), string_codes(N,C), phrase(G,C).
+file(G,F) :- read_file_to_string(F,S,[]), parse(G,S).
+
+:- op(900,fy,#).
+:- table (expr//1, type//1) as incremental.
+
+expr(E) --> #brk(paren,left), expr(E), #brk(paren,right).
+expr(int(I)) --> #int(I).
+expr(bool(true)) --> #true.
+expr(bool(false)) --> #false.
+expr(var(V)) --> #id(V).
+expr(force(A)) --> #force, expr(A).
+expr(thunk(A)) --> #brk(curly,left), expr(A), #brk(curly,right).
+expr(return(A)) --> #return, expr(A).
+expr(apply(A,N)) --> expr(A), expr(N).
+expr(plus(X,Y)) --> expr(X), #plus, expr(Y).
+expr(minus(X,Y)) --> expr(X), #minus, expr(Y).
+expr(times(X,Y)) --> expr(X), #times, expr(Y).
+expr(equal(X,Y)) --> expr(X), #eq, expr(Y).
+expr(less(X,Y)) --> expr(X), #less, expr(Y).
+expr(let(V,E,B)) --> #let, #id(V), #assign, expr(E), #exec, expr(B), #end.
+expr(seq(V,E,B)) --> #seq, #id(V), #assign, expr(E), #exec, expr(B), #end.
+expr(if(X,T,E)) --> #if, expr(X), #then, expr(T), #else, expr(E), #end.
+expr(fun(X,T,B)) --> #fun, #id(X), #ascript, type(T), #thick, expr(B), #end.
+expr(rec(X,T,B)) --> #rec, #id(X), #ascript, type(T), #thick, expr(B), #end.
+
+type(T) --> #brk(paren,left), type(T), #brk(paren,right).
+type(carrow(I,O)) --> type(I), #arrow, type(O).
+type(vforget(T)) --> #'U', type(T).
+type(cfree(T)) --> #'F', type(T).
+type(vint) --> #int.
+type(vbool) --> #bool.
+
+#(T) --> [token(T)].

ADDED   gaunilo/src/type.pro
Index: gaunilo/src/type.pro
==================================================================
--- gaunilo/src/type.pro
+++ gaunilo/src/type.pro
@@ -0,0 +1,35 @@
+:- module(type, [polarity/2, type/3]).
+
+lookup([K-V|_],K,V). % fix backtracking over this
+lookup([_|T],K,V) :- lookup(T,K,V).
+lookup([],K,_) :- throw(lookup_failure(K)).
+
+polarity(comp,cfree(T)) :- polarity(val,T).
+polarity(comp,carrow(T0,T1)) :- polarity(val,T0), polarity(comp,T1).
+polarity(val,vint).
+polarity(val,vbool).
+polarity(val,vforget(T)) :- polarity(comp,T).
+
+type(C,T,var(X)) :- lookup(C,X,T).
+type(_,vint,int(_)).
+type(_,vbool,bool(_)).
+type(C,vint,plus(X,Y)) :- type(C,vint,X), type(C,vint,Y).
+type(C,vint,minus(X,Y)) :- type(C,vint,X), type(C,vint,Y).
+type(C,vint,times(X,Y)) :- type(C,vint,X), type(C,vint,Y).
+type(C,vbool,equal(X,Y)) :- type(C,vint,X), type(C,vint,Y).
+type(C,vbool,less(X,Y)) :- type(C,vint,X), type(C,vint,Y).
+
+type(C,T,if(X,Y,Z)) :-
+    type(C,vbool,X), type(C,T,Y), polarity(comp,T), type(C,T,Z).
+type(C,carrow(P,T),fun(X,P,B)) :-
+    polarity(comp,carrow(P,T)), type([X-P|C],T,B).
+type(C,T1,apply(X,Y)) :- type(C,carrow(T0,T1),X), type(C,T0,Y).
+type(C,T1,seq(V,E,B)) :-
+    type(C,cfree(T0),E), polarity(val,T0), type([V-T0],T1,B), polarity(comp,T1).
+type(C,T1,let(V,E,B)) :-
+    type(C,T0,E), polarity(val,T0), type([V-T0|C],T1,B), polarity(comp,T1).
+type(C,cfree(T),return(E)) :- type(C,T,E), polarity(val,T).
+
+type(C,T,force(E)) :- type(C,vforget(T),E), polarity(comp,T).
+type(C,vforget(T),thunk(E)) :- type(C,T,E), polarity(comp,T).
+type(C,vforget(T),rec(X,T,B)) :- polarity(comp,T), type([X-vforget(T)|C],T,B).