# HG changeset patch # User haftmann # Date 1151661857 -7200 # Node ID 2180f0f443af8d0f74ac4aaadb9a1e57be762179 # Parent 33da452f0abe8f0fa81c12423006b9b9d75c78b4 fixed stale theory bug diff -r 33da452f0abe -r 2180f0f443af src/Pure/Tools/nbe.ML --- a/src/Pure/Tools/nbe.ML Fri Jun 30 12:04:03 2006 +0200 +++ b/src/Pure/Tools/nbe.ML Fri Jun 30 12:04:17 2006 +0200 @@ -16,6 +16,9 @@ structure NBE: NBE = struct + +(* theory data setup *) + structure NBE_Data = TheoryDataFun (struct val name = "Pure/NBE" @@ -27,25 +30,18 @@ fun print _ _ = () end); -val trace_nbe = ref false; +val _ = Context.add_setup NBE_Data.init; -fun nbe_trace fs = if !trace_nbe then tracing(fs()) else (); -val _ = Context.add_setup NBE_Data.init; +(* 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)); fun defined s = Symtab.defined (!tab) s; -fun use_show "" = () - | use_show s = - (if !trace_nbe then tracing ("\n---generated code:\n"^ s) else (); - use_text(tracing o enclose "\n---compiler echo:\n" "\n---\n", - tracing o enclose "\n--- compiler echo (with error!):\n" "\n---\n") - (!trace_nbe) s); -(* FIXME move to term.ML *) +(* FIXME replace by Term.map_aterms *) fun subst_Frees [] tm = tm | subst_Frees inst tm = let @@ -57,49 +53,86 @@ fun var_tab t = (Term.add_frees t [], Term.add_vars t []); -fun anno_vars (Ftab,Vtab) = - subst_Vars (map (fn (ixn,T) => (ixn, Var(ixn,T))) Vtab) o - subst_Frees (map (fn (s,T) => (s, Free(s,T))) Ftab) +fun anno_vars (Ftab, Vtab) = + subst_Vars (map (fn (ixn, T) => (ixn, Var(ixn,T))) Vtab) o + subst_Frees (map (fn (s, T) => (s, Free(s,T))) Ftab) + + +(* debugging *) + +val trace_nbe = ref false; + +fun trace f = if !trace_nbe then tracing (f ()) else (); + +(* FIXME better turn this into a function + NBE_Eval.Univ Symtab.table -> NBE_Eval.Univ Symtab.table + with implicit side effect *) +fun use_code "" = () + | use_code s = + (if !trace_nbe then tracing ("\n---generated code:\n"^ s) else (); + use_text(tracing o enclose "\n---compiler echo:\n" "\n---\n", + tracing o enclose "\n--- compiler echo (with error!):\n" "\n---\n") + (!trace_nbe) s); + + +(* norm by eval *) (* FIXME try to use isar_cmd/print_term to take care of context *) -fun norm_print_i thy t = +fun norm_print t thy = let - val _ = nbe_trace (fn() => "Input:\n" ^ Display.raw_string_of_term t) - val nbe_tab = NBE_Data.get thy; - val modl_old = CodegenThingol.project_module (Symtab.keys nbe_tab) - (CodegenPackage.get_root_module 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 _ = nbe_trace (fn() => "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 _ = nbe_trace (fn()=> "Normalized:\n" ^ NBE_Eval.string_of_nterm nt'); - val t' = NBE_Codegen.nterm_to_term thy'' nt'; - val _ = nbe_trace (fn()=>"Converted back:\n" ^ Display.raw_string_of_term t'); - val t'' = anno_vars (var_tab t) t'; - val _ = nbe_trace (fn()=>"Vars typed:\n" ^ Display.raw_string_of_term t''); - val ty = type_of t; - val (t''', _) = - Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy) (K NONE) (K NONE) - [] false ([t''], ty); - val s = Pretty.string_of - (Pretty.block [Pretty.quote (Sign.pretty_term thy'' t'''), Pretty.fbrk, - Pretty.str "::", Pretty.brk 1, Pretty.quote (Sign.pretty_typ thy'' ty)]) - val _ = writeln s - in (t''', thy'') end; + val _ = trace (fn () => "Input:\n" ^ Display.raw_string_of_term t); + fun compile_term t thy = + let + val (modl_this, thy') = CodegenPackage.get_root_module thy; + val nbe_tab = NBE_Data.get thy'; + val modl_old = CodegenThingol.project_module (Symtab.keys nbe_tab) modl_this; + val (t', thy'') = CodegenPackage.codegen_term t thy'; + val (modl_new, thy''') = CodegenPackage.get_root_module thy''; + val diff = CodegenThingol.diff_module (modl_new, modl_old); + val _ = trace (fn () => "new definitions: " ^ (commas o map fst) diff); + val _ = (tab := nbe_tab; + Library.seq (use_code o NBE_Codegen.generate defined) diff); + val thy'''' = NBE_Data.put (!tab) thy'''; + val nt' = NBE_Eval.nbe (!tab) t'; + in (nt', thy'''') end; + fun eval_term t nt thy = + let + val vtab = var_tab t; + val ty = type_of t; + fun restrain ty t = Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy) + (K NONE) (K NONE) + [] false ([t], ty) |> fst; + val _ = trace (fn () => "Normalized:\n" ^ NBE_Eval.string_of_nterm nt); + val t' = NBE_Codegen.nterm_to_term thy nt; + val _ = trace (fn () =>"Converted back:\n" ^ Display.raw_string_of_term t'); + val t'' = anno_vars vtab t'; + val _ = trace (fn () =>"Vars typed:\n" ^ Display.raw_string_of_term t''); + val t''' = restrain ty t'' + val s = Pretty.string_of + (Pretty.block [Pretty.quote (Sign.pretty_term thy t'''), Pretty.fbrk, + Pretty.str "::", Pretty.brk 1, Pretty.quote (Sign.pretty_typ thy ty)]) + val _ = writeln s + in (t''', thy) end; + in + thy + |> compile_term t + |-> (fn nt => eval_term t nt) + end; -fun norm_print s thy = norm_print_i thy (Sign.read_term thy s); +fun norm_print' s thy = norm_print (Sign.read_term thy s) thy; + +fun norm_term thy t = fst (norm_print t (Theory.copy thy)); -fun norm_term thy t = fst (norm_print_i (Theory.copy thy) t); -structure P = OuterParse and K = OuterKeyword; +(* Isar setup *) + +local structure P = OuterParse and K = OuterKeyword in val nbeP = OuterSyntax.command "normal_form" "normalization by evaluation" K.thy_decl - (P.term >> (fn s => Toplevel.theory (snd o norm_print s))); + (P.term >> (fn s => Toplevel.theory (snd o norm_print' s))); + +end; val _ = OuterSyntax.add_parsers [nbeP];