Anselm: Changes On Branch gaunilo-trunk

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
2

*.o
*.exe

Added .fossil-settings/ignore-glob.

>
>
>
>

x-*/*
*.*~
*build/*
*.test

Added gaunilo/readme.md.

>
>
>
>

# 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.

>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>

:- 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.

>
>
>
>
>
>
>

:- 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.

>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>

:- 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.

>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>

:- 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.

>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>

:- 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).