--- a/src/Pure/Tools/nbe.ML Tue Sep 25 12:16:14 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,222 +0,0 @@
-(* Title: Pure/nbe.ML
- ID: $Id$
- Author: Tobias Nipkow, Florian Haftmann, TU Muenchen
-
-Toplevel theory interface for "normalization by evaluation"
-*)
-
-signature NBE =
-sig
- (*preconditions: no Vars/TVars in term*)
- val normalization_conv: cterm -> thm
- val lookup: string -> NBE_Eval.Univ
- val update: string * NBE_Eval.Univ -> unit
- val trace: bool ref
-end;
-
-structure NBE: NBE =
-struct
-
-val trace = ref false;
-fun tracing f x = if !trace then (Output.tracing (f x); x) else x;
-
-
-(** data setup **)
-
-(* preproc and postproc attributes *)
-
-structure NBE_Rewrite = TheoryDataFun
-(
- type T = thm list * thm list
- val empty = ([], []);
- val copy = I;
- val extend = I;
- fun merge _ ((pres1,posts1), (pres2,posts2)) =
- (Library.merge Thm.eq_thm (pres1,pres2), Library.merge Thm.eq_thm (posts1,posts2))
-);
-
-val _ =
- let
- fun map_data f = Context.mapping (NBE_Rewrite.map f) I;
- fun attr_pre (thy, thm) =
- ((map_data o apfst) (insert Thm.eq_thm thm) thy, thm)
- fun attr_post (thy, thm) =
- ((map_data o apsnd) (insert Thm.eq_thm thm) thy, thm)
- val attr = Attrib.syntax (Scan.lift (Args.$$$ "pre" >> K attr_pre
- || Args.$$$ "post" >> K attr_post));
- in
- Context.add_setup (
- Attrib.add_attributes
- [("normal", attr, "declare rewrite theorems for normalization")]
- )
- end;
-
-fun the_pres thy =
- let
- val ctxt = ProofContext.init thy;
- val pres = (map (LocalDefs.meta_rewrite_rule ctxt) o fst) (NBE_Rewrite.get thy)
- in pres end
-
-fun apply_posts thy =
- let
- val ctxt = ProofContext.init thy;
- val posts = (map (LocalDefs.meta_rewrite_rule ctxt) o snd) (NBE_Rewrite.get thy)
- in MetaSimplifier.rewrite false posts end
-
-(* theorem store *)
-
-structure Funcgr = CodeFuncgrRetrieval (val rewrites = the_pres);
-
-(* code store *)
-
-structure NBE_Data = CodeDataFun
-(struct
- type T = NBE_Eval.Univ Symtab.table;
- val empty = Symtab.empty;
- fun merge _ = Symtab.merge (K true);
- fun purge _ _ _ = Symtab.empty;
-end);
-
-
-(** norm by eval **)
-
-(* sandbox communication *)
-
-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));
-
-local
-
-(* function generation *)
-
-fun generate thy funs =
- let
- (* FIXME better turn this into a function
- NBE_Eval.Univ Symtab.table -> NBE_Eval.Univ Symtab.table
- with implicit side effect *)
- fun use_code NONE = ()
- | use_code (SOME s) =
- (tracing (fn () => "\n---generated code:\n" ^ s) ();
- use_text "" (Output.tracing o enclose "\n---compiler echo:\n" "\n---\n",
- Output.tracing o enclose "\n--- compiler echo (with error!):\n" "\n---\n")
- (!trace) s);
- val _ = tracing (fn () => "new definitions: " ^ (commas o maps (map fst)) funs) ();
- val _ = tab := NBE_Data.get thy;;
- val _ = List.app (use_code o NBE_Codegen.generate thy
- (fn s => Symtab.defined (!tab) s)) funs;
- in NBE_Data.change thy (K (!tab)) end;
-
-fun ensure_funs thy funcgr t =
- let
- fun consts_of thy t =
- fold_aterms (fn Const c => cons (CodeUnit.const_of_cexpr thy c) | _ => I) t []
- val consts = consts_of thy t;
- val nbe_tab = NBE_Data.get thy;
- in
- CodeFuncgr.deps funcgr consts
- |> (map o filter_out) (Symtab.defined nbe_tab o CodeNames.const thy)
- |> filter_out null
- |> (map o map) (fn c => (CodeNames.const thy c, CodeFuncgr.funcs funcgr c))
- |> generate thy
- end;
-
-(* term evaluation *)
-
-fun eval_term thy funcgr t =
- let
- fun subst_Frees [] = I
- | subst_Frees inst =
- Term.map_aterms (fn (t as Free (s, _)) => the_default t (AList.lookup (op =) inst s)
- | t => t);
- val anno_vars =
- subst_Frees (map (fn (s, T) => (s, Free (s, T))) (Term.add_frees t []))
- #> subst_Vars (map (fn (ixn, T) => (ixn, Var (ixn, T))) (Term.add_vars t []))
- fun check_tvars t = if null (Term.term_tvars t) then t else
- error ("Illegal schematic type variables in normalized term: "
- ^ setmp show_types true (Sign.string_of_term thy) t);
- val ty = type_of t;
- fun constrain t =
- singleton (Syntax.check_terms (ProofContext.init thy)) (TypeInfer.constrain ty t);
- val _ = ensure_funs thy funcgr t;
- in
- t
- |> tracing (fn t => "Input:\n" ^ Display.raw_string_of_term t)
- |> NBE_Eval.eval thy (!tab)
- |> tracing (fn nt => "Normalized:\n" ^ NBE_Eval.string_of_nterm nt)
- |> NBE_Codegen.nterm_to_term thy
- |> tracing (fn t => "Converted back:\n" ^ setmp show_types true Display.raw_string_of_term t)
- |> tracing (fn _ => "Term type:\n" ^ Display.raw_string_of_typ ty)
- |> anno_vars
- |> tracing (fn t => "Vars typed:\n" ^ setmp show_types true Display.raw_string_of_term t)
- |> constrain
- |> tracing (fn t => "Types inferred:\n" ^ setmp show_types true Display.raw_string_of_term t)
- |> check_tvars
- end;
-
-(* evaluation oracle *)
-
-exception Normalization of CodeFuncgr.T * term;
-
-fun normalization_oracle (thy, Normalization (funcgr, t)) =
- Logic.mk_equals (t, eval_term thy funcgr t);
-
-fun normalization_invoke thy funcgr t =
- Thm.invoke_oracle_i thy "Pure.normalization" (thy, Normalization (funcgr, t));
-
-in
-
-(* interface *)
-
-fun normalization_conv ct =
- let
- val thy = Thm.theory_of_cterm ct;
- fun mk funcgr drop_classes ct thm1 =
- let
- val t = Thm.term_of ct;
- val thm2 = normalization_invoke thy funcgr t;
- val thm3 = apply_posts thy (Thm.rhs_of thm2);
- val thm23 = drop_classes (Thm.transitive thm2 thm3);
- in
- Thm.transitive thm1 thm23 handle THM _ =>
- error ("normalization_conv - could not construct proof:\n"
- ^ (cat_lines o map string_of_thm) [thm1, thm2, thm3])
- end;
- in fst (Funcgr.make_term thy mk ct) end;
-
-fun norm_print_term ctxt modes t =
- let
- val thy = ProofContext.theory_of ctxt;
- val ct = Thm.cterm_of thy t;
- val (_, t') = (Logic.dest_equals o Thm.prop_of o normalization_conv) ct;
- val ty = Term.type_of t';
- val p = PrintMode.with_modes modes (fn () =>
- Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
- Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)]) ();
- in Pretty.writeln p end;
-
-fun norm_print_term_e (modes, s) state =
- let val ctxt = Toplevel.context_of state
- in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
-
-val _ = Context.add_setup
- (Theory.add_oracle ("normalization", normalization_oracle));
-
-end; (*local*)
-
-
-(* Isar setup *)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
-
-val nbeP =
- OuterSyntax.improper_command "normal_form" "normalize term by evaluation" K.diag
- (opt_modes -- P.typ >> (Toplevel.keep o norm_print_term_e));
-
-end;
-
-val _ = OuterSyntax.add_parsers [nbeP];
-
-end;
--- a/src/Pure/Tools/nbe_codegen.ML Tue Sep 25 12:16:14 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,170 +0,0 @@
-(* Title: Pure/nbe_codegen.ML
- ID: $Id$
- Author: Klaus Aehlig, LMU Muenchen; Tobias Nipkow, TU Muenchen
-
-Code generator for "normalization by evaluation".
-*)
-
-(* Global asssumptions:
- For each function: there is at least one defining eqns and
- all defining equations have same number of arguments.
-
-FIXME
-fun MLname
-val quote = quote;
-
-*)
-
-signature NBE_CODEGEN =
-sig
- val generate: theory -> (string -> bool) -> (string * thm list) list -> string option;
- val nterm_to_term: theory -> NBE_Eval.nterm -> term;
-end
-
-
-structure NBE_Codegen: NBE_CODEGEN =
-struct
-
-val Eval = "NBE_Eval";
-val Eval_mk_Fun = Eval ^ ".mk_Fun";
-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_" ^ translate_string (fn "." => "_" | c => c) 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 space_implode "\n | " (map eqn ees) end;
-
-fun eqnss (es :: ess) = prefix "fun " es :: map (prefix "and ") ess
- |> space_implode "\n"
- |> suffix "\n";
-
-fun Val v s = "val " ^ v ^ " = " ^ s;
-fun Let ds e = "let\n" ^ (space_implode "\n" ds) ^ " in " ^ e ^ " end"
-
-end
-
-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" (*,
- 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 defined names ar =
- let
- fun mk args (Const (c, _)) =
- if member (op =) names c then selfcall c ar args
- else if defined c then S.nbe_apps (MLname c) args
- else S.app Eval_Constr (S.tup [S.quote c, S.list args])
- | mk args (Free (v, _)) = S.nbe_apps (MLvname v) args
- | mk args (t1 $ t2) = mk (args @ [mk [] t2]) t1
- | mk args (Abs (v, _, t)) = S.nbe_apps (mk_nbeFUN (v, mk [] t)) args;
- in mk [] end;
-
-val mk_lexpr =
- let
- fun mk args (Const (c, _)) =
- S.app Eval_Constr (S.tup [S.quote c, S.list args])
- | mk args (Free (v, _)) = if null args then MLvname v else
- sys_error "NBE mk_lexpr illegal higher order pattern"
- | mk args (t1 $ t2) = mk (args @ [mk [] t2]) t1
- | mk args (Abs _) =
- sys_error "NBE mk_lexpr illegal pattern";
- in mk [] end;
-
-fun lookup nm = S.Val (MLname nm) (tab_lookup (S.quote nm));
-
-fun generate thy defined [(_, [])] = NONE
- | generate thy defined raw_eqnss =
- let
- val eqnss0 = map (fn (name, thms as thm :: _) =>
- (name, ((length o snd o strip_comb o fst o Logic.dest_equals o prop_of) thm,
- map (apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify
- o prop_of) thms)))
- raw_eqnss;
- val eqnss = (map o apsnd o apsnd o map) (fn (args, t) =>
- (map (NBE_Eval.prep_term thy) args, NBE_Eval.prep_term thy t)) eqnss0
- val names = map fst eqnss;
- val used_funs =
- []
- |> fold (fold (fold_aterms (fn Const (c, _) => insert (op =) c
- | _ => I)) o map snd o snd o snd) eqnss
- |> subtract (op =) names;
- fun mk_def (name, (ar, eqns)) =
- let
- fun mk_eqn (args, t) = ([S.list (map mk_lexpr (rev args))],
- mk_rexpr defined names ar t);
- val default_params = (S.list o rev o MLparams) ar;
- val default_eqn = ([default_params], S.app Eval_Constr (S.tup [S.quote name, default_params]));
- in S.eqns (MLname name) (map mk_eqn eqns @ [default_eqn]) end;
- val globals = map lookup (filter defined used_funs);
- fun register (name, (ar, _)) = tab_update
- (S.app Eval_mk_Fun (S.tup [S.quote name, MLname name, string_of_int ar]))
- in SOME (S.Let (globals @ [S.eqnss (map mk_def eqnss)]) (space_implode "; " (map register eqnss))) end;
-
-open NBE_Eval;
-
-fun nterm_to_term thy t =
- let
- fun to_term bounds (C s) tcount =
- let
- val SOME (const as (c, _)) = CodeNames.const_rev thy s;
- val ty = CodegenData.default_typ thy const;
- val ty' = map_type_tvar (fn ((s,i),S) => TypeInfer.param (tcount + i) (s,S)) ty;
- val tcount' = tcount + maxidx_of_typ ty + 1;
- in (Const (c, ty'), tcount') end
- | to_term bounds (V s) tcount = (Free (s, dummyT), tcount)
- | to_term bounds (B i) tcount = (Bound (find_index (fn j => i = j) bounds), tcount)
- | to_term bounds (A (t1, t2)) tcount =
- tcount
- |> to_term bounds t1
- ||>> to_term bounds t2
- |-> (fn (t1', t2') => pair (t1' $ t2'))
- | to_term bounds (AbsN (i, t)) tcount =
- tcount
- |> to_term (i :: bounds) t
- |-> (fn t' => pair (Abs ("u", dummyT, t')));
- in fst (to_term [] t 0) end;
-
-end;
--- a/src/Pure/Tools/nbe_eval.ML Tue Sep 25 12:16:14 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,146 +0,0 @@
-(* Title: Pure/nbe_eval.ML
- ID: $Id$
- Author: Klaus Aehlig, LMU Muenchen; Tobias Nipkow, TU Muenchen
-
-Evaluator infrastructure for "normalization by evaluation".
-*)
-
-(* Optimizations:
- int instead of string in Constr
- 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*);
- 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
- (*functions*);
-
- val eval: theory -> Univ Symtab.table -> term -> nterm
- val apply: Univ -> Univ -> Univ
- val prep_term: theory -> term -> term
-
- val to_term: Univ -> nterm
-
- val mk_Fun: string * (Univ list -> Univ) * int -> string * Univ
- val new_name: unit -> int
-
- val string_of_nterm: nterm -> string
-end;
-
-structure NBE_Eval: NBE_EVAL =
-struct
-
-datatype nterm =
- C of string
- | V of string
- | B of int
- | A of nterm * nterm
- | AbsN of int * nterm;
-
-fun string_of_nterm(C s) = "(C \"" ^ s ^ "\")"
- | string_of_nterm(V s) = "(V \"" ^ s ^ "\")"
- | string_of_nterm(B n) = "(B " ^ string_of_int n ^ ")"
- | string_of_nterm(A(s,t)) =
- "(A " ^ string_of_nterm s ^ string_of_nterm t ^ ")"
- | string_of_nterm(AbsN(n,t)) =
- "(Abs " ^ string_of_int n ^ " " ^ string_of_nterm t ^ ")";
-
-fun apps t args = fold_rev (fn y => fn x => A(x,y)) args t;
-
-(* ------------------------------ 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;
-
-(*
- 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)) x = f (x::xs)
- | apply (Fun(f,xs,n)) x = Fun(f,x::xs,n-1)
- | 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));
-
-
-(* ------------------ evaluation with greetings to Tarski ------------------ *)
-
-fun prep_term thy (Const c) = Const (CodeNames.const thy
- (CodeUnit.const_of_cexpr thy c), dummyT)
- | prep_term thy (Free v_ty) = Free v_ty
- | prep_term thy (s $ t) = prep_term thy s $ prep_term thy t
- | prep_term thy (Abs (raw_v, ty, raw_t)) =
- let val (v,t) = Syntax.variant_abs (raw_v, ty, raw_t);
- in Abs (v, ty, prep_term thy t) end;
-
-
-(* generation of fresh names *)
-
-val counter = ref 0;
-fun new_name () = (counter := !counter +1; !counter);
-
-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 (F as Fun _) =
- let val var = new_name()
- in AbsN(var, to_term (apply F (BVar(var,[])))) end;
-
-
-(* greetings to Tarski *)
-
-fun eval thy tab t =
- let
- fun evl vars (Const (s, _)) =
- the_default (Constr (s, [])) (Symtab.lookup tab s)
- | evl vars (Free (v, _)) =
- the_default (Var (v, [])) (AList.lookup (op =) vars v)
- | evl vars (s $ t) =
- apply (evl vars s) (evl vars t)
- | evl vars (Abs (v, _, t)) =
- Fun (fn [x] => evl (AList.update (op =) (v, x) vars) t, [], 1)
- in (counter := 0; to_term (evl [] (prep_term thy t))) end;
-
-end;