# HG changeset patch # User haftmann # Date 1190715375 -7200 # Node ID 0041117b756c9172d6ce49da7a31c4349fff48cc # Parent f875049a13a140f9868092f2a9b2d462c66186f4 dropped diff -r f875049a13a1 -r 0041117b756c src/Pure/Tools/nbe.ML --- 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; diff -r f875049a13a1 -r 0041117b756c src/Pure/Tools/nbe_codegen.ML --- 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; diff -r f875049a13a1 -r 0041117b756c src/Pure/Tools/nbe_eval.ML --- 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;