(* This is an experimental compiler for the call-by-name lambda-mu-nu calculus, based on a Krivine-style abstract machine. The input is abstract syntax - we do no typechecking, but the correctness of the implementation depends on the typability of the source. Parser and typechecker can be added later. The execution of the underlying abstract machine can be observed step by step by starting the compiled program with the -v option. The target language is C, with a set of runtime primitives defined in runtime.c. For a detailed description of the compiler and the underlying abstract machine, and how it relates to a CPS translation of the lambda-mu-nu calculus, see the accompanying documentation. Enjoy. *) (* see http://www.math.lsa.umich.edu/~selinger/lammunu/ *) (* Caml Light version *) (* 7/13/98-8/19/98. Copyright 1998 Peter Selinger. Version 1.3. *) (* Usage: From Caml Light, type * include "compiler.ml";; * to load this file. Then, type * compile term "myfile.c";; * to generate a C-program from a term. Compile this with * gcc myfile.c -o myfile * from a shell. Make sure that the file runtime.c is in the same * directory, because it is included. Finally, execute the code via * myfile -v * The -v tag causes the program to print information on each step of the * computation. *) (* ---------------------------------------------------------------------- *) (* General-purpose auxiliary functions *) (* length of a list *) let rec len = function [] -> 0 | h::t -> 1+len(t);; (* reverse a list *) let rec revapp l = function [] -> l | h::t -> revapp (h::l) t;; let reverse l = revapp [] l;; (* integer to string conversion *) let int2str = string_of_int;; (* increment an integer counter and return its previous value *) let plusplus(ctr) = (ctr:= !ctr+1; !ctr-1);; (* ensure !ctr is at least v *) let atleast(ctr,v) = if (v> !ctr) then (ctr:=v) else ();; (* add an element to a set. Subtract an element from a set. *) let rec setplus x = function [] -> [x] | h::t -> if x=h then h::t else h::(setplus x t);; let rec setminus x = function [] -> [] | h::t -> if x=h then t else h::(setminus x t);; (* set union *) let rec setunion s = function [] -> s | h::t -> setunion (setplus h s) t;; (* coordinatewise union of two pairs of sets *) let unionpairs ((a,b),(c,d)) = (setunion a c,setunion b d);; (* The compiler assembles its output in a list of strings. Each string * represents one line of code. *) (* indent a list of strings *) let rec indent = function [] -> [] | h::t -> (" "^h)::indent(t);; (* print a list of strings, each in a line by itself, to prnt: string->unit *) let rec spool prnt = function [] -> () | h::t -> (prnt h; prnt "\n"; spool prnt t);; (* ---------------------------------------------------------------------- *) (* The datatype of lambda-mu-nu terms *) type var == string;; type fnconst == string;; type term = Var of var | Unit | Pair of term*term | Proj1 of term | Proj2 of term | App of term*term | Lam of var*term | Pass of var*term | Mu of var*term | Ang of var*term | Nu of var*term | Intconst of int | True | False | Fnconst of fnconst;; (* ---------------------------------------------------------------------- *) (* handling of l-value contexts *) type context == (var*string) list;; (* called gamma and delta *) type judgment == context*term*context;; type code == string list;; (* look up a value in a list of key-value pairs (such as, a context) *) exception Lookupexn of string;; let rec lookup key = function [] -> raise (Lookupexn key) | (x,y)::rest -> if (x=key) then y else lookup key rest;; (* reorder a context to match a given variable domain *) let rec coord_transform context = function [] -> [] | x::t -> (x,lookup x context)::(coord_transform context t);; (* ---------------------------------------------------------------------- *) (* Free variables and names of a term *) let rec free = function Var x -> ([x],[]) | Unit -> ([],[]) | Pair(m,n) -> unionpairs(free m,free n) | Proj1 m -> free m | Proj2 m -> free m | App(m,n) -> unionpairs(free m,free n) | Lam(x,m) -> let (fv,fn)=free(m) in (setminus x fv,fn) | Pass(x,m) -> let (fv,fn)=free(m) in (fv,setplus x fn) | Mu(x,m) -> let (fv,fn)=free(m) in (fv,setminus x fn) | Ang(x,m) -> let (fv,fn)=free(m) in (fv,setplus x fn) | Nu(x,m) -> let (fv,fn)=free(m) in (fv,setminus x fn) | Intconst c-> ([],[]) | True -> ([],[]) | False -> ([],[]) | Fnconst f -> ([],[]) ;; (* ---------------------------------------------------------------------- *) (* Generic to-string routines for terms and contexts *) (* term to string conversion: pretty-printing. p is precedence *) let rec t2s p = function Var x -> x | Unit -> "()" | Pair(m,n) -> "("^(t2s 0 m)^","^(t2s 0 n)^")" | Proj1 m -> if (p>=2) then "(Proj1 "^(t2s 2 m)^")" else "Proj1 "^(t2s 2 m) | Proj2 m -> if (p>=2) then "(Proj2 "^(t2s 2 m)^")" else "Proj2 "^(t2s 2 m) | App(m,n) -> if (p>=2) then "("^(t2s 1 m)^" "^(t2s 2 n)^")" else (t2s 1 m)^" "^(t2s 2 n) | Lam(x,m) -> if (p>=1) then "(lam "^x^"."^(t2s 0 m)^")" else "lam "^x^"."^(t2s 0 m) | Pass(x,m) -> if (p>=1) then "(["^x^"]"^(t2s 0 m)^")" else "["^x^"]"^(t2s 0 m) | Mu(x,m) -> if (p>=1) then "(mu "^x^"."^(t2s 0 m)^")" else "mu "^x^"."^(t2s 0 m) | Ang(x,m) -> if (p>=1) then "(<"^x^">"^(t2s 0 m)^")" else "<"^x^">"^(t2s 0 m) | Nu(x,m) -> if (p>=1) then "(nu "^x^"."^(t2s 0 m)^")" else "nu "^x^"."^(t2s 0 m) | Intconst c -> int2str c | True -> "true" | False -> "false" | Fnconst f -> f ;; let term2str = t2s 0;; (* context to string conversion: as a comma-separated list or 0 *) let rec context2str = function [] -> "0" | (x,acc)::[] -> x | (x,acc)::h2::t -> x^","^context2str(h2::t);; (* judgment to string conversion *) let judg2str(gamma,m,delta) = context2str(gamma)^" |- "^term2str(m) ^" | "^context2str(delta);; (* from a context, make code that prints the current environment *) let rec contextprinter char = function [] ->[] | [(x,acc)] ->["printf(\""^x^"->%d"^char^"\","^acc^");"] | (x,acc)::h::t->("printf(\""^x^"->%d,\","^acc^");") ::(contextprinter char (h::t));; let envprinter gamma delta = (contextprinter ";" gamma) @ (contextprinter "" delta);; (* from a judgment, make code that prints the current state of the abstract machine in verbose mode *) let verbose (gamma,m,delta) = ["if (verbose) {"] @ indent(["printf(\"Term: "^term2str(m)^"\\n\");"; "printf(\"Environment: \");"] @ envprinter gamma delta @ ["printf(\"\\nStack: \");"; "printstack();"] ) @ ["}"];; (* make code that prints a value state of the abstract machine *) let intverbose () = ["if (verbose) {"] @ indent(["printf(\"Value: %d\\n\", value);"; "printf(\"Stack: \");"; "printstack();"] ) @ ["}"];; let boolverbose () = ["if (verbose) {"] @ indent(["printf(\"Value: %s\\n\", value ? \"true\" : \"false\");"; "printf(\"Stack: \");"; "printstack();"] ) @ ["}"];; (* from a judgment, make code that prints information about a closure in verbose mode *) let verbose_closure (gamma,m,delta) = ["if (verbose) {"] @ indent(["printf(\"New term closure: %d={"^term2str(m)^ (if (gamma=[] & delta=[]) then "" else ", ")^"\",tmp);"] @ envprinter gamma delta @ ["printf(\"}\\n\\n\");"] ) @ ["}"];; (* ---------------------------------------------------------------------- *) (* definition of the basic functions *) type denottype = Unop of (string->string) | Binop of (string->string->string) | Sideeff of (string->(judgment->int->code)->code);; type resulttype = Int | Bool | Void;; let fnconstdef = [ (* triple: name, denotation, resulttype *) "+", Binop (fun x y -> x^"+"^y), Int; "-", Binop (fun x y -> x^"-"^y), Int; "*", Binop (fun x y -> x^"*"^y), Int; "/", Binop (fun x y -> "("^y^"==0) ? runtimeerr(\"Division by zero\") : ("^x^" div "^y^")"), Int; "succ", Unop (fun x -> x^"+1"), Int; "~", Unop (fun x -> "-"^x), Int; "and", Binop (fun x y -> x^"&&"^y), Bool; "or", Binop (fun x y -> x^"||"^y), Bool; "not", Unop (fun x -> "!"^x), Bool; "iszero", Unop (fun x -> x^"==0"), Bool; "<", Binop (fun x y -> x^"<"^y), Bool; ">", Binop (fun x y -> x^">"^y), Bool; "=", Binop (fun x y -> x^"=="^y), Bool; ">=", Binop (fun x y -> x^">="^y), Bool; "=<", Binop (fun x y -> x^"=<"^y), Bool; "if", Sideeff (fun x sem -> ["if ("^x^") {"] @ indent( sem ([],Lam("x",Lam("y",Var "x")),[]) 0 ) @ ["}"] @ sem ([],Lam("x",Lam("y",Var "y")),[]) 0 ), Void; "print", Sideeff (fun x sem -> ["output(int2str("^x^"));"] @ sem ([],Lam("x",Var "x"),[]) 0 ), Void; "printbool", Sideeff (fun x sem -> ["output("^x^" ? \"true\" : \"false\");"] @ sem ([],Lam("x",Var "x"),[]) 0 ), Void; ];; exception Fnconstexn of string;; (* look up a triple by its first component in a list *) let rec lookup13 key = function [] -> raise (Lookupexn key) | (x,y,z)::t -> if (key=x) then (x,y,z) else lookup13 key t;; (* return the denotation, resulttype, arity, or function tag of a function constant f *) let rec denot_of f = try match lookup13 f fnconstdef with (_,y,_) -> y with Lookupexn key -> raise (Fnconstexn key) and resulttype_of f = try match lookup13 f fnconstdef with (_,_,z) -> z with Lookupexn key -> raise (Fnconstexn key) and arity_of f = match denot_of f with Unop _ -> 1 | Binop _ -> 2 | Sideeff _ -> 1 and ftag_of f = let rec position key = function [] -> raise (Fnconstexn key) | (x,_,_)::t -> if x=key then 0 else 1+position key t in position f fnconstdef ;; (* ---------------------------------------------------------------------- *) (* The actual compiler. See the documentation. *) (* global counters for registers and labels, respectively *) let regctr=ref 0;; let labelctr=ref 0;; let usedfunctions=ref ([]:fnconst list);; (* returns the name of the v'th register, the n'th label, the n'th switch *) let regname(v) = atleast(regctr,v); "reg"^int2str(v);; let labelname(n) = "label"^int2str(n);; let switchname(n) = int2str(n);; let rec sem1 (gamma,term,delta) v = match term with Unit -> ["return \"()\";"] | Var x -> ["clos = "^lookup x gamma^";"; "goto jump;"] | Pair(m,n) -> ["if (stackempty()) return \"pair\";"; "if (pop()==(void*)1) {"] @ indent(sem (gamma,m,delta) v) @ ["}"] @ (sem (gamma,n,delta) v) | Proj1 m -> ["push((void*)1);"] @ (sem (gamma,m,delta) v) | Proj2 m -> ["push((void*)2);"] @ (sem (gamma,m,delta) v) | App(m,n) -> let (fvn,fnn) = free(n) in let gamma2 = coord_transform gamma fvn and delta2 = coord_transform delta fnn and fvns = len(fvn) and fnns = len(fnn) and label = plusplus(labelctr) in let rec closure_loop = function ([],i) -> [] | ((x,acc)::t,i) -> ("tmp["^int2str(i)^"]="^acc^";") :: closure_loop(t,i+1) and new_context i = function [] -> [] | (h::t) -> (h,"clos["^int2str(i)^"]")::(new_context (i+1) t) in ["/* build closure for "^judg2str(gamma2,n,delta2)^" */"; "tmp=alloc("^int2str(fvns+fnns+1)^");"; "tmp[0]=(void*)"^switchname(label)^";"] @ closure_loop(gamma2,1) @ closure_loop(delta2,fvns+1) @ verbose_closure (gamma2,n,delta2) @ ["push(tmp);"] @ sem (gamma,m,delta) v @ ["";labelname(label)^":"] @ sem (new_context 1 fvn,n,new_context (fvns+1) fnn) 0 | Lam(x,m) -> let regv=regname(v) in ["if (stackempty()) return \"fn\";"; regv^" = pop();"] @ sem ((x,regv)::gamma,m,delta) (v+1) | Pass(a,m) -> ["if (stackempty()) return \"pass\";"; "loadstack("^lookup a delta^");"] @ sem (gamma,m,delta) v | Mu(a,m) -> let regv=regname(v) in [regv^" = savestack();"; "push((void*)0);"] @ sem (gamma,m,(a,regv)::delta) (v+1) | Ang(a,m) -> ["push("^lookup a delta^");"] @ sem (gamma,m,delta) v | Nu(a,m) -> let regv=regname(v) in ["if (stackempty()) return \"nu\";"; regv^" = pop();"] @ sem (gamma,m,(a,regv)::delta) (v+1) | Intconst c -> ["value = "^int2str(c)^";"; "goto intvalue;"] | True -> ["value = 1;"; "goto boolvalue;"] | False -> ["value = 0;"; "goto boolvalue;"] | Fnconst f -> let ar=arity_of f and ftag=ftag_of f in usedfunctions:=setplus f !usedfunctions; ["if (stackheight()<"^int2str(ar)^") return \"fn\";"; "clos = pop();"; "push((void*)1); /* argument currently evaluated */"; "push((void*)"^int2str(ar)^"); /* arity */"; "push((void*)"^int2str(ftag)^"); /* tag for "^f^" */"; "goto jump;"] and sem (gamma,m,delta) v = ["";"/* "^judg2str(gamma,m,delta)^" */"] @ verbose (gamma,m,delta) @ sem1 (gamma,m,delta) v ;; let valuehandler () = let rec argumentpopper (i,n) = if (i ["default:"] @ indent(["runtimeerr(\"unknown function tag\");"]) | f::t -> ["case "^int2str(ftag_of f)^": /* "^f^" */"] @ indent(argumentpopper (0,(arity_of f)-1) @ begin match denot_of f with Unop denot -> ["value = "^(denot "value")^";"] | Binop denot -> ["value = "^(denot ("((int)"^regname 0^")") "value")^";"] | Sideeff denot -> denot "value" sem end @ begin match resulttype_of f with Int -> ["goto intvalue;"] | Bool -> ["goto boolvalue;"] | Void -> [] end ) @ fnhandler t in ["";"boolvalue:"] @ boolverbose() @ ["if (stackempty()) return value ? \"true\" : \"false\";"; "goto applyfunction;"] @ ["";"intvalue:"] @ intverbose() @ ["if (stackempty()) return int2str(value);"] @ ["";"applyfunction:"; "arity = (int)(getstack(1));"; "j = (int)(getstack(2));"; "if (j print_string("Error: unbound variable or name: "^key^"\n") | Fnconstexn key -> print_string("Error: unknown function constant: "^key^"\n") ;; (* a few tests *) let term1 = Lam("z",Var"z");; let term2 = Proj1(App(Lam("x",Pair(Var "x", Unit)),term1));; let term2a = Proj2(App(Lam("x",Pair(Var "x", Unit)),term1));; let term3 = Mu("a",Pass("a",Lam("x",Lam("y",App(Var "x", Var "y")))));; let term4 = Lam("y",Lam("x",Pair(Var "y", Var "x")));; let term5 = Lam("x",Mu("a",Pass("a",Var "x")));; let term6 = App(App(Lam("x",Lam("y",App(Var"x",App(Var"x",Var"y")))), Lam("x",Lam("y",App(Var"x",App(Var"x",Var"y"))))),term1);; let term7 = App(Mu("a",Pass("a",Lam("x",Pass("a",term1)))),term1);; let term8 = App(Lam("x",Mu("a",Pass("a",Ang("a",Var"x")))),Nu("b",Lam("y",Pass ("b",Var"y"))));; let term8a = App(term8,term1);; let term9 = (App (term8a,Lam("x",Mu("x",Ang("x",Var "x")))));; let term10 = (App (term8a,Lam("x",Mu("x",Ang("x",App(Var "x",Var "x"))))));; let term11 = Lam("x",Lam("y",Nu("a",Nu("b",Mu("c",App(App(Var"x",Ang("a",Ang("b" ,Var"y"))),Ang("b",Ang("a",Var"x"))))))));; let term12 = App(App(App(Fnconst "print", Intconst 5),App(App(Fnconst "if", App(App(Fnconst ">",Intconst 5),Intconst 3)),Intconst 13)), Intconst 15);; let term13 = App(App(Fnconst "+", Intconst 13),Intconst 11);;