# HG changeset patch
# User nipkow
# Date 1140535130 -3600
# Node ID d065ec5580928ddb27796ac4a93565eb7d3ae46b
# Parent  bc8da9b4a81c5120f8725b9d15a4694fd87a85d4
New normalization-by-evaluation package

diff -r bc8da9b4a81c -r d065ec558092 src/Pure/Tools/nbe_codegen.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/nbe_codegen.ML	Tue Feb 21 16:18:50 2006 +0100
@@ -0,0 +1,372 @@
+(*  ID:         $Id$
+    Author:     Klaus Aehlig, Tobias Nipkow
+*)
+
+(* Global asssumptions:
+   For each function: there is at least one defining eqns and
+   all defining equations have same number of arguments.
+
+FIXME
+fun MLname s = "nbe_" ^ s;
+val quote = quote;
+
+FIXME xtab in theory
+*)
+(*
+structure NBE_Codegen =
+struct
+
+FIXME CodegenThingol names! which "error"?
+*)
+
+val is_constr = NBE_Eval.is_constr;
+val Eval = "NBE_Eval";
+val Eval_register= Eval ^ ".register";
+val Eval_lookup  = Eval ^ ".lookup";
+val Eval_apply   = Eval ^ ".apply";
+val Eval_Constr  = Eval ^ ".Constr";
+val Eval_C       = Eval ^ ".C";
+val Eval_AbsN    = Eval ^ ".AbsN";
+val Eval_Fun     = Eval ^ ".Fun";
+val Eval_BVar    = Eval ^ ".BVar";
+val Eval_new_name = Eval ^ ".new_name";
+val Eval_to_term = Eval ^ ".to_term";
+
+fun MLname s = "nbe_" ^ s;
+fun MLvname s  = "v_" ^ MLname s;
+fun MLparam n  = "p_" ^ string_of_int n;
+fun MLintern s = "i_" ^ MLname s;
+
+fun MLparams n = map MLparam (1 upto n);
+
+structure S =
+struct
+
+val quote = quote; (* FIXME *)
+
+fun app e1 e2 = "(" ^ e1 ^ " " ^ e2 ^ ")";
+fun abs v e = "(fn" ^ v ^ " => " ^ e ^ ")";
+fun tup es = "(" ^ commas es ^ ")";
+fun list es = "[" ^ commas es ^ "]";
+
+fun apps s ss = Library.foldl (uncurry app) (s, ss);
+fun nbe_apps s ss =
+  Library.foldr (fn (s,e) => app (app Eval_apply e) s) (ss,s);
+
+fun eqns name ees =
+  let fun eqn (es,e) = name ^ " " ^ space_implode " " es ^ " = " ^ e
+  in "fun " ^ space_implode "\n  | " (map eqn ees) ^ ";\n" end;
+
+
+fun Val v s = "val " ^ v ^ " = " ^ s;
+fun Let ds e = "let\n" ^ (space_implode "\n" ds) ^ " in " ^ e ^ " end"
+
+end
+
+fun mk_nbeFUN(nm,e) =
+  S.app Eval_Fun (S.tup [S.abs(S.list [MLvname nm])e,S.list [],"1",
+      S.abs(S.tup [])(S.Let 
+        [S.Val (MLintern "var") (S.app Eval_new_name (S.tup [])),
+         S.Val (MLvname nm) (S.app Eval_BVar (S.tup [(MLintern "var"), S.list []]))]
+	(S.app Eval_AbsN(S.tup[MLintern "var",(S.app Eval_to_term e)])))]);
+
+fun take_last n xs = rev (Library.take(n, rev xs));
+fun drop_last n xs = rev (Library.drop(n, rev xs));
+
+fun selfcall nm ar args =
+	if (ar <= length args) then 
+	  S.nbe_apps (S.app (MLname nm) (S.list (take_last ar args)))
+	             (drop_last ar args)
+        else S.app Eval_Fun (S.tup [MLname nm,S.list args,
+	           string_of_int(ar - (length args)),
+		   S.abs (S.tup []) (S.app Eval_C
+	(S.quote nm))]);
+
+
+fun mk_rexpr nm ar =
+  let fun mk args t = case t of
+    CodegenThingol.IConst((s,_),_) => 
+    if s=nm then selfcall nm ar args
+    else if is_constr s then S.app Eval_Constr 
+                                   (S.tup [S.quote s,S.list args ])
+    else S.nbe_apps (MLname s) args
+  | CodegenThingol.IVarE(s,_) => S.nbe_apps (MLvname s) args
+  | CodegenThingol.IApp(e1,e2) => mk (args @ [mk [] e2]) e1
+  | CodegenThingol.IAbs(CodegenThingol.IVarE(nm,_), e) =>
+      S.nbe_apps (mk_nbeFUN(nm, mk [] e)) args
+  | _ => sys_error "NBE mkexpr"
+  in mk [] end;
+
+val mk_lexpr =
+  let fun mk args t = case t of
+    CodegenThingol.IConst((s,_),_) =>
+      S.app Eval_Constr (S.tup [S.quote s, S.list args])
+  | CodegenThingol.IVarE(s,_) => if args = [] then MLvname s else 
+      sys_error "NBE mk_lexpr illegal higher order pattern"
+  | CodegenThingol.IApp(e1,e2) => mk (args @ [mk [] e2]) e1
+  | _ => sys_error "NBE mk_lexpr illegal pattern"
+  in mk [] end;
+
+fun mk_eqn nm ar (lhs,e) = ([S.list(map mk_lexpr (rev lhs))], mk_rexpr nm ar e);
+
+fun funs_of_expr(CodegenThingol.IConst((s,_),_),fs) = s::fs
+  | funs_of_expr(CodegenThingol.IApp(e1,e2),fs) =
+      funs_of_expr(e1, funs_of_expr(e2, fs))
+  | funs_of_expr(CodegenThingol.IAbs(_, e),fs) = funs_of_expr(e,fs)
+  | funs_of_expr(_,fs) = fs;
+
+fun lookup nm =
+  S.Val (MLname nm) (S.app Eval_lookup (S.quote nm));
+
+fun export thy (nm,CodegenThingol.Fun(eqns,_)) =
+  let
+    val ar = length(fst(hd eqns));
+    val params = S.list (rev (MLparams ar));
+    val funs = Library.flat(map (fn (_,e) => funs_of_expr(e,[])) eqns) \ nm;
+    val globals = map lookup (filter_out is_constr funs);
+    val default_eqn = ([params], S.app Eval_Constr (S.tup[S.quote nm,params]));
+    val code = S.eqns (MLname nm) (map (mk_eqn nm ar) eqns @ [default_eqn])
+    val register = S.app Eval_register
+                     (S.tup[S.quote nm, MLname nm, string_of_int ar])
+  in
+    S.Let (globals @ [code]) register
+  end
+  | export _ _ = "\"NBE no op\"";
+
+val use_show = fn s => (writeln ("\n---generated code:\n"^ s);
+     use_text(writeln o enclose "\n---compiler echo:\n" "\n---\n",
+              writeln o enclose "\n--- compiler echo (with error!):\n" 
+                                "\n---\n")
+      true s);
+
+val dummyIT = CodegenThingol.IType("DUMMY",[]);
+
+use_show(export "" ("append",CodegenThingol.Fun(
+  [([CodegenThingol.IConst(("Nil",dummyIT),[]),
+     CodegenThingol.IVarE("ys",dummyIT)],
+    CodegenThingol.IVarE("ys",dummyIT)),
+   ([CodegenThingol.IApp(
+       CodegenThingol.IApp(
+         CodegenThingol.IConst(("Cons",dummyIT),[]),
+         CodegenThingol.IVarE("x",dummyIT)),
+       CodegenThingol.IVarE("xs",dummyIT)),
+     CodegenThingol.IVarE("ys",dummyIT)],
+    CodegenThingol.IApp(
+       CodegenThingol.IApp(
+         CodegenThingol.IConst(("Cons",dummyIT),[]),
+         CodegenThingol.IVarE("x",dummyIT)),
+       CodegenThingol.IApp(
+         CodegenThingol.IApp(
+           CodegenThingol.IConst(("append",dummyIT),[]),
+           CodegenThingol.IVarE("xs",dummyIT)),
+         CodegenThingol.IVarE("ys",dummyIT))))]
+  ,([],dummyIT))));
+
+
+let
+fun test a b = if a=b then () else error "oops!";
+
+val CNil = Const("Nil",dummyT);
+val CCons = Const("Cons",dummyT);
+val Cappend = Const("append",dummyT);
+val Fx = Free("x",dummyT);
+val Fy = Free("y",dummyT);
+val Fxs = Free("xs",dummyT);
+val Fys = Free("ys",dummyT);
+open NBE_Eval
+in
+test (nbe(CNil)) (C "Nil");
+test (nbe(CCons)) (C "Cons");
+test (nbe(Cappend)) (C "append");
+test (nbe(Cappend $ CNil $ CNil)) (C "Nil");
+test (nbe(Cappend $ Fxs)) (A (C "append", V "xs"));
+test (nbe(Cappend $ Fxs $ Fys)) (A (A (C "append", V "xs"), V "ys"));
+test (nbe(Cappend $ CNil $ Fxs)) (V "xs");
+test (nbe(Cappend $ (CCons $ Fx $ Fxs) $ Fys))
+     (A (A (C "Cons", V "x"), A (A (C "append", V "xs"), V "ys")));
+test (nbe(Cappend $ (CCons $ Fx $ Fxs) $ (CCons $ Fy $ Fys)))
+     (A (A (C "Cons", V "x"), A (A (C "append", V "xs"), A (A (C "Cons", V "y"), V "ys"))));
+test (nbe(Cappend $ (CCons $ Fx $ (CCons $ Fy $ Fxs)) $ (CCons$Fy$Fys)))
+ (A
+      (A (C "Cons", V "x"),
+         A
+            (A (C "Cons", V "y"),
+               A (A (C "append", V "xs"), A (A (C "Cons", V "y"), V "ys")))))
+
+end;
+
+
+use_show(export "" ("app",CodegenThingol.Fun(
+  [
+  ([CodegenThingol.IConst(("Nil",dummyIT),[])],
+    CodegenThingol.IAbs(CodegenThingol.IVarE("ys",dummyIT),
+                        CodegenThingol.IVarE("ys",dummyIT))),
+
+   ([CodegenThingol.IApp(
+       CodegenThingol.IApp(
+         CodegenThingol.IConst(("Cons",dummyIT),[]),
+         CodegenThingol.IVarE("x",dummyIT)),
+       CodegenThingol.IVarE("xs",dummyIT))],
+    CodegenThingol.IAbs(CodegenThingol.IVarE("ys",dummyIT),
+    CodegenThingol.IApp(
+       CodegenThingol.IApp(
+         CodegenThingol.IConst(("Cons",dummyIT),[]),
+         CodegenThingol.IVarE("x",dummyIT)),
+       CodegenThingol.IApp(
+         CodegenThingol.IApp(
+           CodegenThingol.IConst(("app",dummyIT),[]),
+           CodegenThingol.IVarE("xs",dummyIT)),
+         CodegenThingol.IVarE("ys",dummyIT)))))]
+  ,([],dummyIT))));
+
+
+let
+fun test a b = if a=b then () else error "oops!";
+
+val CNil = Const("Nil",dummyT);
+val CCons = Const("Cons",dummyT);
+val Cappend = Const("app",dummyT);
+val Fx = Free("x",dummyT);
+val Fy = Free("y",dummyT);
+val Fxs = Free("xs",dummyT);
+val Fys = Free("ys",dummyT);
+open NBE_Eval
+in
+test (nbe(CNil)) (C "Nil");
+test (nbe(CCons)) (C "Cons");
+test (nbe(Cappend)) (C "app");
+test (nbe(Cappend $ CNil)) (AbsN (1, B 1));
+test (nbe(Cappend $ CNil $ CNil)) (C "Nil");
+test (nbe(Cappend $ Fxs)) (A (C "app", V "xs"));
+test (nbe(Cappend $ Fxs $ Fys)) (A (A (C "app", V "xs"), V "ys"));
+test (nbe(Cappend $ CNil $ Fxs)) (V "xs");
+test (nbe(Cappend $ (CCons $ Fx $ Fxs) $ Fys))
+     (A (A (C "Cons", V "x"), A (A (C "app", V "xs"), V "ys")));
+test (nbe(Cappend $ (CCons $ Fx $ Fxs))) 
+   (AbsN (1, A (A (C "Cons", V "x"), A (A (C "app", V "xs"), B 1))));
+test (nbe(Cappend $ (CCons $ Fx $ Fxs) $ (CCons $ Fy $ Fys)))
+     (A (A (C "Cons", V "x"), A (A (C "app", V "xs"), A (A (C "Cons", V "y"), V "ys"))));
+test (nbe(Cappend $ (CCons $ Fx $ (CCons $ Fy $ Fxs)) $ (CCons$Fy$Fys)))
+ (A
+      (A (C "Cons", V "x"),
+         A
+            (A (C "Cons", V "y"),
+               A (A (C "app", V "xs"), A (A (C "Cons", V "y"), V "ys")))));
+()
+end;
+
+
+use_show(export "" ("add",CodegenThingol.Fun(
+  [
+  ([CodegenThingol.IConst(("0",dummyIT),[])],
+    CodegenThingol.IAbs(CodegenThingol.IVarE("n",dummyIT),
+                        CodegenThingol.IVarE("n",dummyIT))),
+   ([CodegenThingol.IApp(
+       CodegenThingol.IConst(("S",dummyIT),[]),
+       CodegenThingol.IVarE("n",dummyIT))],
+    CodegenThingol.IAbs(CodegenThingol.IVarE("m",dummyIT),
+      CodegenThingol.IApp(
+         CodegenThingol.IConst(("S",dummyIT),[]),
+           CodegenThingol.IApp(
+             CodegenThingol.IApp(
+               CodegenThingol.IConst(("add",dummyIT),[]),
+               CodegenThingol.IVarE("n",dummyIT)),
+             CodegenThingol.IVarE("m",dummyIT)))))]
+  ,([],dummyIT))));
+
+
+let
+fun test a b = if a=b then () else error "oops!";
+
+val C0 = Const("0",dummyT);
+val CS = Const("S",dummyT);
+val Cadd = Const("add",dummyT);
+val Fx = Free("x",dummyT);
+val Fy = Free("y",dummyT);
+open NBE_Eval
+in
+test (nbe(Cadd $ C0)) (AbsN (1, B 1));
+test (nbe(Cadd $ C0 $ C0)) (C "0");
+test (nbe(Cadd $ (CS $ (CS $ (CS $ Fx))) $ (CS $ (CS $ (CS $ Fy)))))
+(A (C "S", A (C "S", A (C "S", A (A (C "add", V "x"), A (C "S", A (C "S", A (C "S", V "y")))))))
+)
+end;
+
+
+
+use_show(export "" ("mul",CodegenThingol.Fun(
+  [
+  ([CodegenThingol.IConst(("0",dummyIT),[])],
+    CodegenThingol.IAbs(CodegenThingol.IVarE("n",dummyIT),
+                        CodegenThingol.IConst(("0",dummyIT),[]))),
+   ([CodegenThingol.IApp(
+       CodegenThingol.IConst(("S",dummyIT),[]),
+       CodegenThingol.IVarE("n",dummyIT))],
+    CodegenThingol.IAbs(CodegenThingol.IVarE("m",dummyIT),
+      CodegenThingol.IApp(
+       CodegenThingol.IApp(
+         CodegenThingol.IConst(("add",dummyIT),[]),
+        CodegenThingol.IVarE("m",dummyIT)),
+           CodegenThingol.IApp(
+             CodegenThingol.IApp(
+               CodegenThingol.IConst(("mul",dummyIT),[]),
+               CodegenThingol.IVarE("n",dummyIT)),
+             CodegenThingol.IVarE("m",dummyIT)))))]
+  ,([],dummyIT))));
+
+
+let
+fun test a b = if a=b then () else error "oops!";
+
+val C0 = Const("0",dummyT);
+val CS = Const("S",dummyT);
+val Cmul = Const("mul",dummyT);
+val Fx = Free("x",dummyT);
+val Fy = Free("y",dummyT);
+open NBE_Eval
+in
+test (nbe(Cmul $ C0)) (AbsN (1, C "0"));
+test (nbe(Cmul $ C0 $ Fx)) (C "0");
+test (nbe(Cmul $ (CS $ (CS $ (CS $ C0)))))
+(AbsN (1, A (A (C "add", B 1), A (A (C "add", B 1), A (A (C "add", B 1), C "0")))));
+test (nbe(Cmul $ (CS $ (CS $ (CS $ Fx)))))
+ (AbsN (1, A (A (C "add", B 1), A (A (C "add", B 1),
+                     A (A (C "add", B 1), A (A (C "mul", V "x"), B 1))))));
+test (nbe(Cmul $ (CS $ (CS $ Fx)) $ (CS $ (CS $ (CS $ Fy)))))
+(A (C "S", A(C "S",A(C "S",A(A (C "add", V "y"),A(C "S",A(C "S",A(C "S",A
+ (A (C "add", V "y"),A(A (C "mul", V "x"),A(C "S",A(C "S",A(C "S", V"y")))))))))))));
+()
+end;
+
+
+
+
+
+(*
+  | export(nm,Fun(cls,(_,ty)))
+  | export _ = ""
+
+fun top_eval st thy =
+let val t = Sign.read_term thy st
+    val tabs = CodegenPackage.mk_tabs thy;
+    val thy') =
+      CodegenPackage.expand_module NONE (CodegenPackage.codegen_term
+         thy tabs [t]) thy
+    val s = map export diff
+in use s; (* FIXME val thy'' = thy' |> *)
+   Pretty.writeln (Sign.pretty_term thy t');
+   thy'
+end
+
+structure P = OuterParse;
+
+val nbeP =
+  OuterSyntax.command "norm_by_eval" "norm by eval" K.thy_decl
+    (P.term >> (Toplevel.theory o top_eval));
+
+val _ = OuterSyntax.add_parsers [nbeP];
+
+ProofGeneral.write_keywords "nbe";
+(* isar-keywords-nbe.el -> isabelle/etc/
+   Isabelle -k nbe *)
+*)
diff -r bc8da9b4a81c -r d065ec558092 src/Pure/Tools/nbe_eval.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/nbe_eval.ML	Tue Feb 21 16:18:50 2006 +0100
@@ -0,0 +1,151 @@
+(*  ID:         $Id$
+    Author:     Klaus Aehlig, Tobias Nipkow
+*)
+
+(* ------------------------------ Evaluator  ------------------------------ *)
+
+(* Optimizations:
+ int instead of string in Constr
+ xtab as real table
+ treat int via ML ints
+*)
+
+signature NBE_EVAL =
+sig
+(* named terms used for output only *)
+datatype nterm =
+    C of string (* Named Constants *)
+  | V of string (* Free Variable *)
+  | B of int (* Named(!!) Bound Variables *)
+  | A of nterm*nterm (* Application *)
+  | AbsN of int*nterm ; (* Binding of named Variables *)
+
+val nbe: term -> nterm
+
+datatype Univ = 
+    Constr of string*(Univ list)       (* Named Constructors *)
+  | Var of string*(Univ list)          (* Free variables *)
+  | BVar of int*(Univ list)            (* Bound named variables *)
+  | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm);
+                                            (* Functions *)
+val apply: Univ -> Univ -> Univ;
+val to_term: Univ -> nterm;
+
+val lookup: string -> Univ;
+val is_constr: string -> bool;
+val register: string * (Univ list -> Univ) * int -> unit
+val new_name: unit -> int;
+
+(* For testing
+val eval: term -> (Univ list) -> Univ
+*)
+
+end;
+
+(* FIXME add_funs and relatives should NOT be exported. Eventually it
+should work like for quickcheck: Eval generates code which leaves the
+function values in a public reference variable, the code is executed,
+and the value of the reference variable is added to the internal
+tables, all in one go, w/o interruption. *)
+
+
+structure NBE_Eval:NBE_EVAL =
+struct
+
+datatype nterm =
+    C of string (* Named Constants *)
+  | V of string (* Free Variable *)
+  | B of int (* Named(!!) Variables *)
+  | A of nterm * nterm (* Application *)
+  | AbsN of int * nterm (* Binding of named Variables *);
+
+fun apps t args = foldr (fn (y,x) => A(x,y)) t args;
+
+(* ------------------------------ The semantical universe --------------------- *)
+
+(*
+   Functions are given by their semantical function value. To avoid
+   trouble with the ML-type system, these functions have the most
+   generic type, that is "Univ list -> Univ". The calling convention is
+   that the arguments come as a list, the last argument first. In
+   other words, a function call that usually would look like
+
+   f x_1 x_2 ... x_n   or   f(x_1,x_2, ..., x_n)
+
+   would be in our convention called as
+
+              f [x_n,..,x_2,x_1]
+
+   Moreover, to handle functions that are still waiting for some
+   arguments we have additionally a list of arguments collected to far
+   and the number of arguments we're still waiting for.
+
+   Finally, it might happen, that a function does not get all the
+   arguments it needs. In this case the function must provide means to
+   present itself as a string. As this might be a heavy-wight
+   operation, we delay it.
+*)
+
+datatype Univ = 
+    Constr of string*(Univ list)       (* Named Constructors *)
+  | Var of string*(Univ list)          (* Free variables *)
+  | BVar of int*(Univ list)         (* Bound named variables *)
+  | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm);
+
+fun to_term (Constr(name, args))    = apps (C name) (map to_term args)
+  |	to_term (Var   (name, args))    = apps (V name) (map to_term args)
+  |	to_term (BVar  (name, args))    = apps (B name) (map to_term args)
+  |	to_term (Fun(_,args,_,name_thunk)) = apps (name_thunk ()) (map to_term args);
+
+(*
+   A typical operation, why functions might be good for, is
+   application. Moreover, functions are the only values that can
+   reasonably we applied in a semantical way.
+*)
+
+fun  apply (Fun(f,xs,1,name))  x = f (x::xs)
+   | apply (Fun(f,xs,n,name))  x = Fun(f,x::xs,n-1,name)
+   | apply (Constr(name,args)) x = Constr(name,x::args)
+   | apply (Var(name,args))    x = Var(name,x::args)
+   | apply (BVar(name,args))   x = BVar(name,x::args);
+
+(* ---------------- table with the meaning of constants -------------------- *)
+
+val xfun_tab: (string * Univ)list ref = ref [];
+fun do_register sx = (xfun_tab := sx :: !xfun_tab);
+fun register(name,v,0) = do_register(name,v [])
+  | register(name,v,n) = do_register(name,Fun(v,[],n, fn () => C name));
+
+fun do_lookup [] s          = NONE
+  |	do_lookup ((n,v)::xs) s = if (s=n) then SOME v else do_lookup xs s;
+
+fun lookup s = case do_lookup (!xfun_tab) s of
+    SOME x => x
+  | NONE   => Constr(s,[]);
+
+fun is_constr s = is_none (do_lookup (!xfun_tab) s);
+
+(* ------------------ evaluation with greetings to Tarski ------------------ *)
+
+(* generation of fresh names *)
+
+val counter = ref 0;
+
+fun new_name() = (counter := !counter +1; !counter);
+
+(* greetings to Tarski *)
+
+fun eval(Const(f,_)) xs = lookup f
+  | eval(Free(x,_)) xs = Var(x,[])
+  | eval(Bound n) xs = List.nth(xs,n)
+  | eval(s $ t) xs = apply (eval s xs) (eval t xs)
+  | eval(Abs(_,_, t)) xs = Fun ((fn [x] => eval t (x::xs)),[],1,
+                           fn () => let val var = new_name() in
+                         AbsN(var, to_term (eval t ((BVar(var,[]) :: xs)))) end);
+
+
+(* finally... *)
+
+fun nbe t = (counter :=0; to_term(eval t []));
+
+end;