--- a/src/HOL/ex/nbe.thy Thu Mar 02 18:51:11 2006 +0100
+++ b/src/HOL/ex/nbe.thy Fri Mar 03 08:52:39 2006 +0100
@@ -19,5 +19,6 @@
norm_by_eval "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f])"
norm_by_eval "%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True"
norm_by_eval "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()]"
+norm_by_eval "rev [a, b, c]"
end
--- a/src/Pure/Tools/codegen_package.ML Thu Mar 02 18:51:11 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML Fri Mar 03 08:52:39 2006 +0100
@@ -420,7 +420,7 @@
| NONE => idf_of_name thy nsp_const c
end;
-fun recconst_of_idf thy ((deftab, _), (_, (_, overltab2), _)) idf =
+fun recconst_of_idf thy (_, (_, (_, overltab2), _)) idf =
case name_of_idf thy nsp_const idf
of SOME c => SOME (c, Sign.the_const_type thy c)
| NONE => (
@@ -432,6 +432,16 @@
| NONE => NONE
);
+fun const_of_idf thy (tabs as (_, (_, _, dtcontab))) idf =
+ case recconst_of_idf thy tabs idf
+ of SOME c_ty => SOME c_ty
+ | NONE => case dest_nsp nsp_mem idf
+ of SOME c => SOME (c, Sign.the_const_constraint thy c)
+ | NONE => case name_of_idf thy nsp_dtcon idf
+ of SOME idf' => let
+ val c = (fst o DatatypeconsNameMangler.rev thy dtcontab) idf'
+ in SOME (c, Sign.the_const_type thy c) end
+ | NONE => NONE;
(* further theory data accessors *)
@@ -1163,13 +1173,13 @@
fun codegen_term t thy =
thy
- |> expand_module NONE exprsgen_term [t]
+ |> expand_module NONE exprsgen_term [Codegen.preprocess_term thy t]
|-> (fn [t] => pair t);
val is_dtcon = has_nsp nsp_dtcon;
fun consts_of_idfs thy =
- map (the o recconst_of_idf thy (mk_tabs thy));
+ map (the o const_of_idf thy (mk_tabs thy));
fun idfs_of_consts thy =
map (idf_of_const thy (mk_tabs thy));
--- a/src/Pure/Tools/nbe.ML Thu Mar 02 18:51:11 2006 +0100
+++ b/src/Pure/Tools/nbe.ML Fri Mar 03 08:52:39 2006 +0100
@@ -1,81 +1,71 @@
(* ID: $Id$
Author: Tobias Nipkow, Florian Haftmann, TU Muenchen
-Installing "normalization by evaluation"
+Toplevel theory interface for "normalization by evaluation"
*)
-signature NORMBYEVAL =
+signature NBE =
sig
- val lookup: string -> NBE_Eval.Univ
- val update: string * NBE_Eval.Univ -> unit
+ val norm_by_eval_i: term -> theory -> term * theory;
+ val lookup: string -> NBE_Eval.Univ;
+ val update: string * NBE_Eval.Univ -> unit;
end;
-structure NormByEval:NORMBYEVAL =
+structure NBE: NBE =
struct
structure NBE_Data = TheoryDataFun
(struct
- val name = "Pure/NormByEval";
- type T = NBE_Eval.Univ Symtab.table
- val empty = Symtab.empty
+ val name = "Pure/NBE";
+ type T = NBE_Eval.Univ Symtab.table;
+ val empty = Symtab.empty;
val copy = I;
val extend = I;
- fun merge _ = Symtab.merge (K true)
+ fun merge _ = Symtab.merge (K true);
fun print _ _ = ();
end);
val _ = Context.add_setup NBE_Data.init;
+val tab : NBE_Eval.Univ Symtab.table ref = ref Symtab.empty;
+fun lookup s = (the o Symtab.lookup (!tab)) s;
+fun update sx = (tab := Symtab.update sx (!tab));
+fun defined s = Symtab.defined (!tab) s;
+
fun use_show 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 tab : NBE_Eval.Univ Symtab.table ref = ref Symtab.empty;
-fun lookup s = the(Symtab.lookup (!tab) s);
-fun update sx = (tab := Symtab.update sx (!tab));
-fun defined s = Symtab.defined (!tab) s;
-
-fun top_nbe st thy =
+fun norm_by_eval_i t thy =
let
- val t = Sign.read_term thy st;
val nbe_tab = NBE_Data.get thy;
val modl_old = CodegenThingol.partof (Symtab.keys nbe_tab)
(CodegenPackage.get_root_module thy);
- val (t', thy') = CodegenPackage.codegen_term t thy
+ val (t', thy') = CodegenPackage.codegen_term t thy;
val modl_new = CodegenPackage.get_root_module thy';
val diff = CodegenThingol.diff_module (modl_new, modl_old);
val _ = writeln ("new definitions: " ^ (commas o map fst) diff);
val _ = (tab := nbe_tab;
- Library.seq (use_show o NBE_Codegen.generate defined) diff)
- val thy'' = NBE_Data.put (!tab) thy'
- val nt' = NBE_Eval.nbe (!tab) t'
- val _ = print nt'
+ Library.seq (use_show o NBE_Codegen.generate defined) diff);
+ val thy'' = NBE_Data.put (!tab) thy';
+ val nt' = NBE_Eval.nbe (!tab) t';
+ val t' = NBE_Codegen.nterm_to_term thy'' nt';
+ val _ = print nt';
+ val _ = (Pretty.writeln o Sign.pretty_term thy'') t';
in
- thy''
+ (t', thy'')
end;
+fun norm_by_eval raw_t thy = norm_by_eval_i (Sign.read_term thy raw_t) thy;
+
structure P = OuterParse and K = OuterKeyword;
val nbeP =
- OuterSyntax.command "norm_by_eval" "norm by eval" K.thy_decl
- (P.term >> (Toplevel.theory o top_nbe));
+ OuterSyntax.command "norm_by_eval" "normalization by evaluation" K.thy_decl
+ (P.term >> (fn t => Toplevel.theory (snd o norm_by_eval t)));
val _ = OuterSyntax.add_parsers [nbeP];
-(*
-ProofGeneral.write_keywords "nbe";
-*)
-(* isar-keywords-nbe.el -> isabelle/etc/
- Isabelle -k nbe *)
-end
-
-
-(*
-fun to_term xs (C s) = Const(s,dummyT)
- | to_term xs (V s) = Free(s,dummyT)
- | to_term xs (B i) = Bound (find_index_eq i xs)
- | to_term xs (A(t1,t2)) = to_term xs t1 $ to_term xs t2
- | to_term xs (AbsN(i,t)) = Abs("u",dummyT,to_term (i::xs) t);
-*)
+end;
--- a/src/Pure/Tools/nbe_codegen.ML Thu Mar 02 18:51:11 2006 +0100
+++ b/src/Pure/Tools/nbe_codegen.ML Fri Mar 03 08:52:39 2006 +0100
@@ -1,5 +1,7 @@
(* ID: $Id$
- Author: Klaus Aehlig, Tobias Nipkow
+ Author: Klaus Aehlig, LMU Muenchen; Tobias Nipkow, TU Muenchen
+
+Code generator for "normalization by evaluation".
*)
(* Global asssumptions:
@@ -14,7 +16,8 @@
signature NBE_CODEGEN =
sig
- val generate: (string -> bool) -> string * CodegenThingol.def -> string
+ val generate: (string -> bool) -> string * CodegenThingol.def -> string;
+ val nterm_to_term: theory -> NBE_Eval.nterm -> term;
end
@@ -63,8 +66,8 @@
end
-val tab_lookup = S.app "NormByEval.lookup";
-val tab_update = S.app "NormByEval.update";
+val tab_lookup = S.app "NBE.lookup";
+val tab_update = S.app "NBE.update";
fun mk_nbeFUN(nm,e) =
S.app Eval_Fun (S.tup [S.abs(S.list [MLvname nm])e,S.list [],"1",
@@ -117,31 +120,52 @@
fun mk_eqn defined nm ar (lhs,e) =
([S.list(map mk_lexpr (rev lhs))], mk_rexpr defined nm ar e);
-fun funs_of_expr (IConst ((s, _), _)) = insert (op =) s
- | funs_of_expr (e1 `$ e2) =
- funs_of_expr e1 #> funs_of_expr e2
- | funs_of_expr (_ `|-> e) = funs_of_expr e
- | funs_of_expr (IAbs (_, e)) = funs_of_expr e
- | funs_of_expr (ICase (_, e)) = funs_of_expr e
- | funs_of_expr _ = I;
+fun consts_of (IConst ((s, _), _)) = insert (op =) s
+ | consts_of (e1 `$ e2) =
+ consts_of e1 #> consts_of e2
+ | consts_of (_ `|-> e) = consts_of e
+ | consts_of (IAbs (_, e)) = consts_of e
+ | consts_of (ICase (_, e)) = consts_of e
+ | consts_of _ = I;
fun lookup nm = S.Val (MLname nm) (tab_lookup (S.quote nm));
fun generate defined (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) => consts_of e []) eqns) \ nm;
+ val globals = map lookup (filter defined funs);
+ val default_eqn = ([params], S.app Eval_Constr (S.tup[S.quote nm,params]));
+ val code = S.eqns (MLname nm)
+ (map (mk_eqn defined nm ar) eqns @ [default_eqn])
+ val register = tab_update
+ (S.app Eval_mk_Fun (S.tup[S.quote nm, MLname nm, string_of_int ar]))
+ in
+ S.Let (globals @ [code]) register
+ end
+ | generate _ _ = "";
+
+open NBE_Eval;
+
+fun nterm_to_term thy t =
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 defined funs);
- val default_eqn = ([params], S.app Eval_Constr (S.tup[S.quote nm,params]));
- val code = S.eqns (MLname nm)
- (map (mk_eqn defined nm ar) eqns @ [default_eqn])
- val register = tab_update
- (S.app Eval_mk_Fun (S.tup[S.quote nm, MLname nm, string_of_int ar]))
- in
- S.Let (globals @ [code]) register
- end
- | generate _ _ = "";
+ fun consts_of (C s) = insert (op =) s
+ | consts_of (V _) = I
+ | consts_of (B _) = I
+ | consts_of (A (t1, t2)) = consts_of t1 #> consts_of t2
+ | consts_of (AbsN (_, t)) = consts_of t;
+ val consts = consts_of t [];
+ val the_const = AList.lookup (op =)
+ (consts ~~ CodegenPackage.consts_of_idfs thy consts)
+ #> the_default ("", dummyT);
+ fun to_term bounds (C s) = Const (the_const s)
+ | to_term bounds (V s) = Free (s, dummyT)
+ | to_term bounds (B i) = Bound (find_index (fn j => i = j) bounds)
+ | to_term bounds (A (t1, t2)) = to_term bounds t1 $ to_term bounds t2
+ | to_term bounds (AbsN (i, t)) =
+ Abs("u", dummyT, to_term (i::bounds) t);
+ in to_term [] t end;
end;
--- a/src/Pure/Tools/nbe_eval.ML Thu Mar 02 18:51:11 2006 +0100
+++ b/src/Pure/Tools/nbe_eval.ML Fri Mar 03 08:52:39 2006 +0100
@@ -1,9 +1,9 @@
(* ID: $Id$
- Author: Klaus Aehlig, Tobias Nipkow
+ Author: Klaus Aehlig, LMU Muenchen; Tobias Nipkow, TU Muenchen
+
+Evaluator infrastructure for "normalization by evaluation".
*)
-(* ------------------------------ Evaluator ------------------------------ *)
-
(* Optimizations:
int instead of string in Constr
treat int via ML ints
@@ -11,50 +11,42 @@
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 *)
+ (*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*);
+ 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*);
-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 nbe: Univ Symtab.table -> CodegenThingol.iexpr -> nterm
+ val nbe: Univ Symtab.table -> CodegenThingol.iexpr -> nterm;
+ val apply: Univ -> Univ -> Univ;
+
+ val to_term: Univ -> nterm;
-val apply: Univ -> Univ -> Univ;
-val to_term: Univ -> nterm;
+ val mk_Fun: string * (Univ list -> Univ) * int -> string * Univ;
+ val new_name: unit -> int;
-val mk_Fun: string * (Univ list -> Univ) * int -> string * Univ
-val new_name: unit -> int;
-
-(* For testing
-val eval: term -> (Univ list) -> Univ
-*)
-
+ (* For testing
+ val eval: (Univ list) -> term -> 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 =
+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 *);
+ C of string
+ | V of string
+ | B of int
+ | A of nterm * nterm
+ | AbsN of int * nterm;
fun apps t args = foldr (fn (y,x) => A(x,y)) t args;
@@ -100,11 +92,11 @@
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);
+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);
fun mk_Fun(name,v,0) = (name,v [])
| mk_Fun(name,v,n) = (name,Fun(v,[],n, fn () => C name));
@@ -123,7 +115,7 @@
val counter = ref 0;
-fun new_name() = (counter := !counter +1; !counter);
+fun new_name () = (counter := !counter +1; !counter);
(* greetings to Tarski *)
@@ -142,7 +134,6 @@
| eval xs (IAbs (_, t)) = eval xs t
| eval xs (ICase (_, t)) = eval xs t;
-
(* finally... *)
fun nbe tab t = (counter :=0; xfun_tab := tab; to_term(eval [] t));