lisp.twelf

%use equality/integers.
%use equality/strings.

sexp : type.
env : type.

num : integer -> sexp.
sym : string -> sexp.
nil : sexp.
cons : sexp -> sexp -> sexp.
func : env -> sexp -> sexp -> sexp. % env, params, body
prim : string -> sexp.

empty : env.
bind : sexp -> sexp -> env -> env.


parse-sym-char : string -> type.
parse-sym-char/a : parse-sym-char "a".
parse-sym-char/b : parse-sym-char "b".
parse-sym-char/c : parse-sym-char "c".
parse-sym-char/d : parse-sym-char "d".
parse-sym-char/e : parse-sym-char "e".
parse-sym-char/f : parse-sym-char "f".
parse-sym-char/g : parse-sym-char "g".
parse-sym-char/h : parse-sym-char "h".
parse-sym-char/i : parse-sym-char "i".
parse-sym-char/j : parse-sym-char "j".
parse-sym-char/k : parse-sym-char "k".
parse-sym-char/l : parse-sym-char "l".
parse-sym-char/m : parse-sym-char "m".
parse-sym-char/n : parse-sym-char "n".
parse-sym-char/o : parse-sym-char "o".
parse-sym-char/p : parse-sym-char "p".
parse-sym-char/q : parse-sym-char "q".
parse-sym-char/r : parse-sym-char "r".
parse-sym-char/s : parse-sym-char "s".
parse-sym-char/t : parse-sym-char "t".
parse-sym-char/u : parse-sym-char "u".
parse-sym-char/v : parse-sym-char "v".
parse-sym-char/w : parse-sym-char "w".
parse-sym-char/x : parse-sym-char "x".
parse-sym-char/y : parse-sym-char "y".
parse-sym-char/z : parse-sym-char "z".
parse-sym-char/z : parse-sym-char "z".
parse-sym-char/A : parse-sym-char "A".
parse-sym-char/B : parse-sym-char "B".
parse-sym-char/C : parse-sym-char "C".
parse-sym-char/D : parse-sym-char "D".
parse-sym-char/E : parse-sym-char "E".
parse-sym-char/F : parse-sym-char "F".
parse-sym-char/G : parse-sym-char "G".
parse-sym-char/H : parse-sym-char "H".
parse-sym-char/I : parse-sym-char "I".
parse-sym-char/J : parse-sym-char "J".
parse-sym-char/K : parse-sym-char "K".
parse-sym-char/L : parse-sym-char "L".
parse-sym-char/M : parse-sym-char "M".
parse-sym-char/N : parse-sym-char "N".
parse-sym-char/O : parse-sym-char "O".
parse-sym-char/P : parse-sym-char "P".
parse-sym-char/Q : parse-sym-char "Q".
parse-sym-char/R : parse-sym-char "R".
parse-sym-char/S : parse-sym-char "S".
parse-sym-char/T : parse-sym-char "T".
parse-sym-char/U : parse-sym-char "U".
parse-sym-char/V : parse-sym-char "V".
parse-sym-char/W : parse-sym-char "W".
parse-sym-char/X : parse-sym-char "X".
parse-sym-char/Y : parse-sym-char "Y".
parse-sym-char/Z : parse-sym-char "Z".
parse-sym-char/_ : parse-sym-char "_".
parse-sym-char/- : parse-sym-char "-".
parse-sym-char/+ : parse-sym-char "+".
parse-sym-char/* : parse-sym-char "*".

parse-digit : string -> integer -> type.
parse-digit/0 : parse-digit "0" 0.
parse-digit/1 : parse-digit "1" 1.
parse-digit/2 : parse-digit "2" 2.
parse-digit/3 : parse-digit "3" 3.
parse-digit/4 : parse-digit "4" 4.
parse-digit/5 : parse-digit "5" 5.
parse-digit/6 : parse-digit "6" 6.
parse-digit/7 : parse-digit "7" 7.
parse-digit/8 : parse-digit "8" 8.
parse-digit/9 : parse-digit "9" 9.

parse-white : string -> type.
parse-white/none : parse-white "".
parse-white/++ : parse-white (" " ++ Y)
                 <- parse-white Y.

parse-real-white : string -> type.
parse-real-white/spc : parse-real-white " ".
parse-real-white/++ : parse-real-white (" " ++ Y)
                      <- parse-real-white Y.

parse-char : string -> type.
parse-char/SYM : parse-char S
                 <- parse-sym-char S.
parse-char/LPAR : parse-char "(".
parse-char/RPAR : parse-char ")".
parse-char/SP : parse-char " ".
parse-char/DIGIT : parse-char D
                   <- parse-digit D _.

% First integer is an accumulator initialized to 0.
parse-int : string -> integer -> integer -> type.
% Putting more before dig makes the parser greedy. Doing it the other way fails
%   miserably, turning every digit into its own number.
parse-int/more : parse-int (X ++ Rest) Acc Ntot
                 <- parse-digit X NX
                 <- parse-int Rest (10 * Acc + NX) Ntot.
% Require at least one digit to parse as an integer.
parse-int/dig : parse-int X Acc (10 * Acc + NX)
                <- parse-digit X NX.

parse-sym : string -> type.
% Putting ++ before c makes the parser greedy. Doing it the other way fails
%   miserably, turning every char into its own symbol.
parse-sym/++ : parse-sym (X ++ Y)
               <- parse-sym-char Y
               <- parse-sym X.
parse-sym/c : parse-sym X
              <- parse-sym-char X.

parse : string -> sexp -> type.
parse-list : string -> sexp -> type.

parse-list/nil : parse-list X nil
                 <- parse-white X.
parse-list/single : parse-list X (cons A nil)
                    <- parse X A.
parse-list/cons : parse-list (X ++ Y ++ Z) (cons A B)
                  <- parse X A
                  <- parse-real-white Y
                  <- parse-list Z B.
 
parse/number : parse X (num NX)
               <- parse-int X 0 NX.
parse/sym : parse X (sym X)
            <- parse-sym X.
parse/list : parse ("(" ++ L ++ ")") List
             <- parse-list L List.

env-lookup : env -> sexp -> sexp -> type.
env-lookup/found : env-lookup (bind K V _) K V.
env-lookup/rest : env-lookup (bind K1 _ C) K V
                  <- env-lookup C K V.

not-env-has : env -> sexp -> type.
not-env-has/nil : not-env-has empty _.
not-env-has/nope : not-env-has (bind K1 _ Rest) K
                   <- not-env-has Rest K.

ctx-lookup : env -> env -> sexp -> sexp -> type.
ctx-lookup/g : ctx-lookup G L K V
               <- env-lookup G K V.
ctx-lookup/l : ctx-lookup G L K V
               <- not-env-has G K
               <- env-lookup L K V.

% NB: binds in reverse order. That should never matter...
bind-params : env -> sexp -> sexp -> env -> type.
bind-params/nil : bind-params E nil nil E.
bind-params/cons : bind-params E (cons K Params) (cons V Args) (bind K V E')
                   <- bind-params E Params Args E'.

% Global env, local env, exp, new global env, value
eval : env -> env -> sexp -> env -> sexp -> type.
do-progn : env -> env -> sexp -> env -> sexp -> type.
do-cond : env -> env -> sexp -> env -> sexp -> type.
eval-list : env -> env -> sexp -> env -> sexp -> type.
apply-prim : env -> env -> string -> sexp -> env -> sexp -> type.

eval/num : eval G _ (num N) G (num N).
eval/nil : eval G _ nil G nil.
eval/sym : eval G L (sym S) G V
           <- ctx-lookup G L (sym S) V.
eval/progn : eval G L (cons (sym "progn") Rest) G' Result
             <- do-progn G L Rest G' Result.
eval/lambda : eval G L (cons (sym "lambda") (cons Params Body)) G (func L Params (cons (sym "progn") Body)).
eval/define : eval G L (cons (sym "define") (cons (sym K) (cons Exp nil))) (bind (sym K) V G') V
              <- eval G L Exp G' V.
eval/define-func : eval G L (cons (sym "define") (cons (cons K Params) Body)) (bind K (func L Params (cons (sym "progn") Body)) G) nil.
eval/quote : eval G L (cons (sym "quote") (cons E nil)) G E.
eval/cond : eval G L (cons (sym "cond") Clauses) G' V
            <- do-cond G L Clauses G' V.
eval/apply : eval G L (cons F Args) G''' V
             <- eval G L F G' (func Env Params Body)
             <- eval-list G' L Args G'' Args'
             <- bind-params Env Params Args' Env'
             <- eval G'' Env' Body G''' V.
eval/apply-primitive : eval G L (cons F Args) G''' V
                       <- eval G L F G' (prim Prim)
                       <- eval-list G' L Args G'' Args'
                       <- apply-prim G'' L Prim Args' G''' V.

do-progn/nil : do-progn G _ nil G nil.
do-progn/one : do-progn G L (cons E nil) G' V
               <- eval G L E G' V.
do-progn/rest : do-progn G L (cons E (cons X XS)) G'' V
                <- eval G L E G' _
                <- do-progn G' L (cons X XS) G'' V.

eval-list/nil : eval-list G _ nil G nil.
eval-list/cons : eval-list G L (cons E Rest) G'' (cons V Rest')
                 <- eval G L E G' V
                 <- eval-list G' L Rest G'' Rest'.

apply-prim/car : apply-prim G _ "car" (cons (cons Car _) nil) G Car.
apply-prim/cdr : apply-prim G _ "cdr" (cons (cons _ Cdr) nil) G Cdr.
apply-prim/cons : apply-prim G _ "cons" (cons A (cons B nil)) G (cons A B).
apply-prim/eq-t : apply-prim G _ "eq" (cons X (cons X nil)) G (sym "true").
apply-prim/eq-nil : apply-prim G _ "eq" (cons X (cons Y nil)) G nil.
apply-prim/+ : apply-prim G _ "+" (cons (num X) (cons (num Y) nil)) G (num (X + Y)).
apply-prim/- : apply-prim G _ "-" (cons (num X) (cons (num Y) nil)) G (num (X - Y)).
apply-prim/* : apply-prim G _ "*" (cons (num X) (cons (num Y) nil)) G (num (X * Y)).
%deterministic apply-prim.

% XXX Can probably extend this to catch anything that's not nil, and
%   reintroduce the one-element special case in cond.
is-true : sexp -> type.
is-true/t : is-true (sym "true").

is-nil : sexp -> type.
is-nil/nil : is-nil nil.

do-cond/nil : do-cond G _ nil G nil.
do-cond/false : do-cond G L (cons (cons Cond _) Clauses) G'' V
                <- eval G L Cond G' X
                <- is-nil X
                <- do-cond G' L Clauses G'' V.
do-cond/progn : do-cond G L (cons (cons Cond Rest) _) G' V
                <- eval G L Cond G' X
                <- is-true X
                <- eval G L (cons (sym "progn") Rest) G' V.
%deterministic do-cond.

%define env = (bind (sym "nil") nil 
              (bind (sym "true") (sym "true")
              (bind (sym "car") (prim "car")
              (bind (sym "cdr") (prim "cdr")
              (bind (sym "cons") (prim "cons")
              (bind (sym "eq") (prim "eq")
              (bind (sym "+") (prim "+")
              (bind (sym "-") (prim "-")
              (bind (sym "*") (prim "*")
              empty)))))))))
%define program = Program
%solve _ : parse "(progn (define (fact n) (cond ((eq n 0) 1) (true (* n (fact (- n 1)))))) (fact 5))" Program.
%%solve _ : parse "(progn (define (fact n) (cond ((eq n 0) 1) (true (* n (- n 1))))) (fact 0))" Program.
%%solve _ : parse "(cond ((eq 0 0) 1) (true 2))" Program.
%%solve _ : parse "(eq 0 0)" Program.
%%solve _ : parse "(progn (define (timesfive n) (* n 5)) (timesfive 5))" Program.
%%solve _ : parse "(progn (define (id x y) (cons x (cons y ()))) (id car 1))" Program.
%%solve _ : parse "(* 5 5)" Program.
%%solve _ : parse "(progn (define (fact n) 1) 1 2 3)" Program.
%solve _ : eval env empty program _ Result.