(* 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/ *)

(* SML/NJ 0.93 version *)

(* 7/13/98-8/19/98. Copyright 1998 Peter Selinger. Version 1.3. *)

(* Usage: From SML/NJ, type
 *   use "compiler.sml";
 * 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 *)
fun len [] = 0
  | len (h::t) = 1+len(t);

(* reverse a list *)
fun revapp l [] = l
  | revapp l (h::t) = revapp (h::l) t;

fun reverse l = revapp [] l;

(* integer to string conversion *)
val int2str = Integer.makestring;

(* increment an integer counter and return its previous value *)
fun plusplus(ctr) = (ctr:= !ctr+1; !ctr-1);

(* ensure !ctr is at least v *)
fun atleast(ctr,v) = if ((v:int)> !ctr) then (ctr:=v) else ();

(* add an element to a set. Subtract an element from a set. *)
fun setplus x [] = [x]
  | setplus x (h::t) = if x=h then h::t else h::(setplus x t);
fun setminus x [] = []
  | setminus x (h::t) = if x=h then t else h::(setminus x t);

(* set union *)
fun setunion s [] = s
  | setunion s (h::t) = setunion (setplus h s) t;

(* coordinatewise union of two pairs of sets *)
fun 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 *)
fun indent [] = []
  | indent (h::t) = ("  "^h)::indent(t);

(* print a list of strings, each in a line by itself, to prnt: string->unit *)
fun spool prnt [] = ()
  | spool prnt (h::t) = (prnt h; prnt "\n"; spool prnt t);

(* ---------------------------------------------------------------------- *)
(* The datatype of lambda-mu-nu terms *)

type var = string;
type fnconst = string;
datatype 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;
fun lookup key [] = raise (Lookupexn key)
  | lookup key ((x,y)::rest) = if (x=key) then y else lookup key rest;

(* reorder a context to match a given variable domain *)
fun coord_transform context [] = []
  | coord_transform context (x::t) = 
	(x,lookup x context)::(coord_transform context t);

(* ---------------------------------------------------------------------- *)
(* Free variables and names of a term *)

fun free(Var x     )= ([x],[])
  | free(Unit      )= ([],[])
  | free(Pair(m,n) )= unionpairs(free m,free n)
  | free(Proj1 m   )= free m
  | free(Proj2 m   )= free m
  | free(App(m,n)  )= unionpairs(free m,free n)
  | free(Lam(x,m)  )= let val (fv,frn)=free(m) in (setminus x fv,frn) end
  | free(Pass(x,m) )= let val (fv,frn)=free(m) in (fv,setplus x frn) end
  | free(Mu(x,m)   )= let val (fv,frn)=free(m) in (fv,setminus x frn) end
  | free(Ang(x,m)  )= let val (fv,frn)=free(m) in (fv,setplus x frn) end
  | free(Nu(x,m)   )= let val (fv,frn)=free(m) in (fv,setminus x frn) end
  | free(Intconst c)= ([],[])
  | free(True      )= ([],[])
  | free(False     )= ([],[])
  | free(Fnconst f )= ([],[])
;

(* ---------------------------------------------------------------------- *)
(* Generic to-string routines for terms and contexts *)

(* term to string conversion: pretty-printing. p is precedence *)
fun t2s p (Var x) = x
  | t2s p (Unit) = "()"
  | t2s p (Pair(m,n)) = "("^(t2s 0 m)^","^(t2s 0 n)^")"
  | t2s p (Proj1 m) = if (p>=2) then "(Proj1 "^(t2s 2 m)^")"
                              else "Proj1 "^(t2s 2 m)
  | t2s p (Proj2 m) = if (p>=2) then "(Proj2 "^(t2s 2 m)^")"
                              else "Proj2 "^(t2s 2 m)
  | t2s p (App(m,n)) = if (p>=2) then "("^(t2s 1 m)^" "^(t2s 2 n)^")"
                              else (t2s 1 m)^" "^(t2s 2 n)
  | t2s p (Lam(x,m)) = if (p>=1) then "(lam "^x^"."^(t2s 0 m)^")"
                              else "lam "^x^"."^(t2s 0 m)
  | t2s p (Pass(x,m)) = if (p>=1) then "(["^x^"]"^(t2s 0 m)^")"
                              else "["^x^"]"^(t2s 0 m)
  | t2s p (Mu(x,m)) = if (p>=1) then "(mu "^x^"."^(t2s 0 m)^")"
                              else "mu "^x^"."^(t2s 0 m)
  | t2s p (Ang(x,m)) = if (p>=1) then "(<"^x^">"^(t2s 0 m)^")"
                              else "<"^x^">"^(t2s 0 m)
  | t2s p (Nu(x,m)) = if (p>=1) then "(nu "^x^"."^(t2s 0 m)^")"
                              else "nu "^x^"."^(t2s 0 m)
  | t2s p (Intconst c) = int2str c
  | t2s p (True) = "true"
  | t2s p (False) = "false"
  | t2s p (Fnconst f) = f
;

val term2str = t2s 0;

(* context to string conversion: as a comma-separated list or 0 *)
fun context2str []       = "0"
  | context2str ((x,acc)::[])    = x
  | context2str ((x,acc)::h2::t) = x^","^context2str(h2::t);

(* judgment to string conversion *)
fun judg2str(gamma,m,delta) = context2str(gamma)^" |- "^term2str(m)
                                ^" | "^context2str(delta);

(* from a context, make code that prints the current environment *)
fun contextprinter char []     =[]
  | contextprinter char [(x,acc)]  =["printf(\""^x^"->%d"^char^"\","^acc^");"]
  | contextprinter char ((x,acc)::h::t)=("printf(\""^x^"->%d,\","^acc^");")
                         ::(contextprinter char (h::t));

fun envprinter gamma delta =
  (contextprinter ";" gamma) @ (contextprinter "" delta);

(* from a judgment, make code that prints the current state of the abstract
   machine in verbose mode *)
fun 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 *)
fun intverbose () =
        ["if (verbose) {"]
        @ indent(["printf(\"Value: %d\\n\", value);",
                  "printf(\"Stack: \");",
                  "printstack();"]
          )
        @ ["}"];

fun 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 *)
fun verbose_closure (gamma,m,delta) =
        ["if (verbose) {"]
        @ indent(["printf(\"New term closure: %d={"^term2str(m)^
                 (if (gamma=[] andalso delta=[]) then "" else ", ")^"\",tmp);"]
                @ envprinter gamma delta
                @ ["printf(\"}\\n\\n\");"]
          )
        @ ["}"];

(* ---------------------------------------------------------------------- *)
(* definition of the basic functions *)

datatype denottype = Unop of (string->string)
        | Binop of (string->string->string)
        | Sideeff of (string->(judgment->int->code)->code);
datatype resulttype = Int | Bool | Void;

val fnconstdef = [
(* triple: name, denotation, resulttype *)
  ("+",          Binop (fn x => fn y => x^"+"^y), Int),
  ("-",          Binop (fn x => fn y => x^"-"^y), Int),
  ("*",          Binop (fn x => fn y => x^"*"^y), Int),
  ("/",          Binop (fn x => fn y =>
   "("^y^"==0) ? runtimeerr(\"Division by zero\") : ("^x^" div "^y^")"), Int),
  ("succ",       Unop (fn x => x^"+1"), Int),
  ("~",          Unop (fn x => "-"^x), Int),
  ("and",        Binop (fn x => fn y => x^"&&"^y), Bool),
  ("or",         Binop (fn x => fn y => x^"||"^y), Bool),
  ("not",        Unop (fn x => "!"^x), Bool),
  ("iszero",     Unop (fn x => x^"==0"), Bool),
  ("<",          Binop (fn x => fn y => x^"<"^y), Bool),
  (">",          Binop (fn x => fn y => x^">"^y), Bool),
  ("=",          Binop (fn x => fn y => x^"=="^y), Bool),
  (">=",         Binop (fn x => fn y => x^">="^y), Bool),
  ("=<",         Binop (fn x => fn y => x^"=<"^y), Bool),
  ("if",         Sideeff (fn x => fn sem =>
                          ["if ("^x^") {"]
                          @ indent(
                            sem ([],Lam("x",Lam("y",Var "x")),[]) 0
                          )
                          @ ["}"]
                          @ sem ([],Lam("x",Lam("y",Var "y")),[]) 0
                        ), Void),
  ("print",      Sideeff (fn x => fn sem =>
                          ["output(int2str("^x^"));"]
                          @ sem ([],Lam("x",Var "x"),[]) 0
                        ), Void),
  ("printbool",  Sideeff (fn x => fn 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 *)
fun lookup13 key [] = raise (Lookupexn key)
  | lookup13 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 *)
fun denot_of f =
  let val (_,y,_) = lookup13 f fnconstdef in y end
  handle Lookupexn key => raise (Fnconstexn key);

fun resulttype_of f =
  let val (_,_,z) = lookup13 f fnconstdef in z end
  handle Lookupexn key => raise (Fnconstexn key);

fun arity_of f =
  let fun arity_from_denot (Unop _) = 1
    | arity_from_denot (Binop _) = 2
    | arity_from_denot (Sideeff _) = 1
  in
    arity_from_denot (denot_of f)
  end;

fun ftag_of f =
  let fun position key [] = raise (Fnconstexn key)
        | position key ((x,_,_)::t) = if x=key then 0 else 1+position key t
  in 
    position f fnconstdef
  end;

(* ---------------------------------------------------------------------- *)
(* The actual compiler. See the documentation. *)

(* global counters for registers and labels, respectively *)
val regctr=ref 0;
val labelctr=ref 0;
val usedfunctions=ref ([]:fnconst list);

(* returns the name of the v'th register, the n'th label, the n'th switch *)
fun regname(v) = (atleast(regctr,v); "reg"^int2str(v));
fun labelname(n) = "label"^int2str(n);
fun switchname(n) = int2str(n);

fun sem1 (gamma,Unit,delta) v =	 
			   ["return \"()\";"]
  | sem1 (gamma,Var x,delta) v = 
			   ["clos = "^lookup x gamma^";",
                                 "goto jump;"]
  | sem1 (gamma,Pair(m,n),delta) v =
			   ["if (stackempty()) return \"pair\";",
                                 "if (pop()==(void*)1) {"]
                                @ indent(sem (gamma,m,delta) v)
                                @ ["}"]
                                @ (sem (gamma,n,delta) v)
  | sem1 (gamma,Proj1 m,delta) v =
			   ["push((void*)1);"]
                                @ (sem (gamma,m,delta) v)
  | sem1 (gamma,Proj2 m,delta) v =
			   ["push((void*)2);"]
                                @ (sem (gamma,m,delta) v)
  | sem1 (gamma,App(m,n),delta) v =
        let val (fvn,fnn) = free(n)
        in
          let val 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 fun closure_loop ([],i)   = []
            |   closure_loop ((x,acc)::t,i) = ("tmp["^int2str(i)^"]="^acc^";")
                                 :: closure_loop(t,i+1)
        and new_context i []     = []
            |   new_context i (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
	end end end
  | sem1 (gamma,Lam(x,m),delta) v =
        let val regv=regname(v)
        in
                      ["if (stackempty()) return \"fn\";",
                      regv^" = pop();"]
                      @ sem ((x,regv)::gamma,m,delta) (v+1)
	end
  | sem1 (gamma,Pass(a,m),delta) v =
                      ["if (stackempty()) return \"pass\";",
                       "loadstack("^lookup a delta^");"]
                      @ sem (gamma,m,delta) v
  | sem1 (gamma,Mu(a,m),delta) v =
        let val regv=regname(v)
        in
                      [regv^" = savestack();",
                       "push((void*)0);"]
                      @ sem (gamma,m,(a,regv)::delta) (v+1)
	end
  | sem1 (gamma,Ang(a,m),delta) v =
                      ["push("^lookup a delta^");"]
                      @ sem (gamma,m,delta) v
  | sem1 (gamma,Nu(a,m),delta) v =
        let val regv=regname(v)
        in
                      ["if (stackempty()) return \"nu\";",
                       regv^" = pop();"]
                      @ sem (gamma,m,(a,regv)::delta) (v+1)
	end
  | sem1 (gamma,Intconst c,delta) v =
			    ["value = "^int2str(c)^";",
                       "goto intvalue;"]
  | sem1 (gamma,True,delta) v =
			          ["value = 1;",
                       "goto boolvalue;"]
  | sem1 (gamma,False,delta) v =
			         ["value = 0;",
                       "goto boolvalue;"]
  | sem1 (gamma,Fnconst f,delta) v =
       let val 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;"]
	end
and sem (gamma,m,delta) v =     ["","/* "^judg2str(gamma,m,delta)^" */"]
                                @ verbose (gamma,m,delta)
                                @ sem1 (gamma,m,delta) v
;

fun valuehandler () =
  let fun argumentpopper (i,n) =
        if (i<n) then
                (regname(i)^" = pop();") :: argumentpopper (i+1,n)
        else    []
  and fnhandler [] = ["default:"]
        @ indent(["runtimeerr(\"unknown function tag\");"])
    | fnhandler (f::t) = ["case "^int2str(ftag_of f)^": /* "^f^" */"]
        @ indent(argumentpopper (0,(arity_of f)-1)
          @ (fn 
               Unop denot =>
                     ["value = "^(denot "value")^";"]
             | Binop denot =>
                     ["value = "^(denot ("((int)"^regname 0^")") "value")^";"]
             | Sideeff denot =>
                     denot "value" sem
            ) (denot_of f)
          @ (fn
               Int => ["goto intvalue;"]
             | Bool => ["goto boolvalue;"]
             | Void => []
            ) (resulttype_of f)
          )
          @ 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<arity) {"]
                @ indent(["clos = getstack(2+j);",
                  "modifystack(2+j,(void *)value);",
                  "modifystack(2,(void *)j+1);",
                  "goto jump;",
                  "}"])
                @ ["ftag = (int)pop();",
                "pop();",
                "pop();",
                "switch (ftag) {"]
                @ fnhandler(!usedfunctions)
                @ ["}"]
  end
;

fun compile m file =
        let fun decreg(n) =     (* declare registers 0..n *)
                if (n<0) then []
                          else ("void *"^regname(n)^";")::decreg(n-1)
            and declabels(n) =  (* declare labels 0..n-1 *)
                if (n<=0) then []
                         else ("case "^switchname(n-1)^
                                ": goto "^labelname(n-1)^";")
                              :: declabels(n-1)
        in let val rawcode =
            (
                regctr:= ~1;
                labelctr:=0;
                usedfunctions:=[];
                sem ([],m,[]) 0
            )
        in let val vhandlercode = valuehandler()
        in let val code = ["#include \"runtime.c\"","","char *compiled() {"]
                        @ indent("void **clos, **tmp;" ::
                            "int value, arity, j, ftag;" ::
                            (reverse(decreg(!regctr)))
                            @ rawcode
                            @ ["","jump: switch((int)(clos[0])) {"]
                            @ indent(reverse(declabels(!labelctr))
                                @ ["default: runtimeerr(\"unknown label\");"])
                            @ ["}"]
                            @ vhandlercode)
                        @ ["}"]
        in let val outstream = open_out(file)
        in
        (spool (IO.outputc outstream) code;
        flush_out outstream)
	end end end end end
      handle Lookupexn key =>
                print("Error: unbound variable or name: "^key^"\n")
         | Fnconstexn key =>
                print("Error: unknown function constant: "^key^"\n")
;

(* a few tests *)

val term1 = Lam("z",Var"z");
val term2 = Proj1(App(Lam("x",Pair(Var "x", Unit)),term1));
val term2a = Proj2(App(Lam("x",Pair(Var "x", Unit)),term1));
val term3 = Mu("a",Pass("a",Lam("x",Lam("y",App(Var "x", Var "y")))));
val term4 = Lam("y",Lam("x",Pair(Var "y", Var "x")));
val term5 = Lam("x",Mu("a",Pass("a",Var "x")));
val 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);
val term7 = App(Mu("a",Pass("a",Lam("x",Pass("a",term1)))),term1);
val term8 = App(Lam("x",Mu("a",Pass("a",Ang("a",Var"x")))),Nu("b",Lam("y",Pass
                ("b",Var"y"))));
val term8a = App(term8,term1);
val term9 = (App (term8a,Lam("x",Mu("x",Ang("x",Var "x")))));
val term10 = (App (term8a,Lam("x",Mu("x",Ang("x",App(Var "x",Var "x"))))));
val 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"))))))));

val term12 = App(App(App(Fnconst "print", Intconst 5),App(App(Fnconst "if",
App(App(Fnconst ">",Intconst 5),Intconst 3)),Intconst 13)),
Intconst 15);

val term13 = App(App(Fnconst "+", Intconst 13),Intconst 11);