# HG changeset patch # User haftmann # Date 1187161062 -7200 # Node ID 8ca96f4e49cd6ddcc05f359744e8fde1055d6831 # Parent 9b64aa2975249fb4be2391baf20c72299a38d4d2 tuned diff -r 9b64aa297524 -r 8ca96f4e49cd src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Wed Aug 15 08:57:41 2007 +0200 +++ b/src/Pure/Isar/code.ML Wed Aug 15 08:57:42 2007 +0200 @@ -638,10 +638,8 @@ | NONE => check_typ_fun (const, thm); in check_typ (fst (CodeUnit.head_func thm), thm) end; -val mk_func = CodeUnit.error_thm - (assert_func_typ o CodeUnit.mk_func); -val mk_func_liberal = CodeUnit.warning_thm - (assert_func_typ o CodeUnit.mk_func); +val mk_func = CodeUnit.error_thm (assert_func_typ o CodeUnit.mk_func); +val mk_func_liberal = CodeUnit.warning_thm (assert_func_typ o CodeUnit.mk_func); end; diff -r 9b64aa297524 -r 8ca96f4e49cd src/Tools/code/code_funcgr.ML --- a/src/Tools/code/code_funcgr.ML Wed Aug 15 08:57:41 2007 +0200 +++ b/src/Tools/code/code_funcgr.ML Wed Aug 15 08:57:42 2007 +0200 @@ -12,25 +12,18 @@ val timing: bool ref val funcs: T -> CodeUnit.const -> thm list val typ: T -> CodeUnit.const -> typ - val deps: T -> CodeUnit.const list -> CodeUnit.const list list val all: T -> CodeUnit.const list val pretty: theory -> T -> Pretty.T + val make: theory -> CodeUnit.const list -> T + val make_consts: theory -> CodeUnit.const list -> CodeUnit.const list * T + val eval_conv: theory -> (T -> cterm -> thm) -> cterm -> thm + val eval_term: theory -> (T -> cterm -> 'a) -> cterm -> 'a + val intervene: theory -> T -> T + (*FIXME drop intervene as soon as possible*) structure Constgraph : GRAPH end -signature CODE_FUNCGR_RETRIEVAL = -sig - type T (* = CODE_FUNCGR.T *) - val make: theory -> CodeUnit.const list -> T - val make_consts: theory -> CodeUnit.const list -> CodeUnit.const list * T - val make_term: theory -> (T -> (thm -> thm) -> cterm -> thm -> 'a) -> cterm -> 'a * T - (*FIXME drop make_term as soon as possible*) - val eval_conv: theory -> (T -> cterm -> thm) -> cterm -> thm - val intervene: theory -> T -> T - (*FIXME drop intervene as soon as possible*) -end; - -structure CodeFuncgr = (*signature is added later*) +structure CodeFuncgr : CODE_FUNCGR = struct (** the graph type **) @@ -48,15 +41,6 @@ fun typ funcgr = fst o Constgraph.get_node funcgr; -fun deps funcgr cs = - let - val conn = Constgraph.strong_conn funcgr; - val order = rev conn; - in - (map o filter) (member (op =) (Constgraph.all_succs funcgr cs)) order - |> filter_out null - end; - fun all funcgr = Constgraph.keys funcgr; fun pretty thy funcgr = @@ -208,7 +192,7 @@ |> instances_of thy algebra end; -fun ensure_const' rewrites thy algebra funcgr const auxgr = +fun ensure_const' thy algebra funcgr const auxgr = if can (Constgraph.get_node funcgr) const then (NONE, auxgr) else if can (Constgraph.get_node auxgr) const @@ -219,26 +203,25 @@ |> pair (SOME const) else let val thms = Code.these_funcs thy const - |> map (CodeUnit.rewrite_func (rewrites thy)) |> CodeUnit.norm_args |> CodeUnit.norm_varnames CodeName.purify_tvar CodeName.purify_var; val rhs = consts_of (const, thms); in auxgr |> Constgraph.new_node (const, thms) - |> fold_map (ensure_const rewrites thy algebra funcgr) rhs + |> fold_map (ensure_const thy algebra funcgr) rhs |-> (fn rhs' => fold (fn SOME const' => Constgraph.add_edge (const, const') | NONE => I) rhs') |> pair (SOME const) end -and ensure_const rewrites thy algebra funcgr const = +and ensure_const thy algebra funcgr const = let val timeap = if !timing then Output.timeap_msg ("time for " ^ CodeUnit.string_of_const thy const) else I; - in timeap (ensure_const' rewrites thy algebra funcgr const) end; + in timeap (ensure_const' thy algebra funcgr const) end; -fun merge_funcss rewrites thy algebra raw_funcss funcgr = +fun merge_funcss thy algebra raw_funcss funcgr = let val funcss = raw_funcss |> resort_funcss thy algebra funcgr @@ -267,7 +250,7 @@ (fold_consts (insert (op =)) thms []); in funcgr - |> ensure_consts' rewrites thy algebra insts + |> ensure_consts' thy algebra insts |> fold (curry Constgraph.add_edge const) deps |> fold (curry Constgraph.add_edge const) insts end; @@ -276,22 +259,22 @@ |> fold add_funcs funcss |> fold add_deps funcss end -and ensure_consts' rewrites thy algebra cs funcgr = +and ensure_consts' thy algebra cs funcgr = let val auxgr = Constgraph.empty - |> fold (snd oo ensure_const rewrites thy algebra funcgr) cs; + |> fold (snd oo ensure_const thy algebra funcgr) cs; in funcgr - |> fold (merge_funcss rewrites thy algebra) + |> fold (merge_funcss thy algebra) (map (AList.make (Constgraph.get_node auxgr)) (rev (Constgraph.strong_conn auxgr))) end handle INVALID (cs', msg) => raise INVALID (fold (insert CodeUnit.eq_const) cs' cs, msg); -fun ensure_consts rewrites thy consts funcgr = +fun ensure_consts thy consts funcgr = let val algebra = Code.coregular_algebra thy - in ensure_consts' rewrites thy algebra consts funcgr + in ensure_consts' thy algebra consts funcgr handle INVALID (cs', msg) => error (msg ^ ",\nwhile preprocessing equations for constant(s) " ^ commas (map (CodeUnit.string_of_const thy) cs')) end; @@ -302,16 +285,16 @@ val ensure_consts = ensure_consts; -fun check_consts rewrites thy consts funcgr = +fun check_consts thy consts funcgr = let val algebra = Code.coregular_algebra thy; fun try_const const funcgr = - (SOME const, ensure_consts' rewrites thy algebra [const] funcgr) + (SOME const, ensure_consts' thy algebra [const] funcgr) handle INVALID (cs', msg) => (NONE, funcgr); val (consts', funcgr') = fold_map try_const consts funcgr; in (map_filter I consts', funcgr') end; -fun ensure_consts_term rewrites thy f ct funcgr = +fun ensure_consts_term_proto thy f ct funcgr = let fun consts_of thy t = fold_aterms (fn Const c => cons (CodeUnit.const_of_cexpr thy c) | _ => I) t [] @@ -321,11 +304,10 @@ in Thm.transitive thm thm' end val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct); val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) (); - val thm1 = Code.preprocess_conv ct - |> fold (rhs_conv o MetaSimplifier.rewrite false o single) (rewrites thy); + val thm1 = Code.preprocess_conv ct; val ct' = Thm.rhs_of thm1; val consts = consts_of thy (Thm.term_of ct'); - val funcgr' = ensure_consts rewrites thy consts funcgr; + val funcgr' = ensure_consts thy consts funcgr; val algebra = Code.coregular_algebra thy; val (_, thm2) = Thm.varifyT' [] thm1; val thm3 = Thm.reflexive (Thm.rhs_of thm2); @@ -344,10 +326,10 @@ val cs = fold_aterms (fn Const c => cons c | _ => I) (Thm.term_of ct'') []; val drop = drop_classes thy tfrees; val instdefs = instances_of_consts thy algebra funcgr' cs; - val funcgr'' = ensure_consts rewrites thy instdefs funcgr'; + val funcgr'' = ensure_consts thy instdefs funcgr'; in (f funcgr'' drop ct'' thm5, funcgr'') end; -fun ensure_consts_eval rewrites thy conv = +fun ensure_consts_eval thy conv = let fun conv' funcgr drop_classes ct thm1 = let @@ -359,49 +341,38 @@ error ("eval_conv - could not construct proof:\n" ^ (cat_lines o map string_of_thm) [thm1, thm2, thm3]) end; - in ensure_consts_term rewrites thy conv' end; + in ensure_consts_term_proto thy conv' end; + +fun ensure_consts_term thy f = + let + fun f' funcgr drop_classes ct thm1 = f funcgr ct; + in ensure_consts_term_proto thy f' end; end; (*local*) -end; (*struct*) - -functor CodeFuncgrRetrieval (val rewrites: theory -> thm list) : CODE_FUNCGR_RETRIEVAL = -struct - -(** code data **) - -type T = CodeFuncgr.T; - structure Funcgr = CodeDataFun (struct type T = T; - val empty = CodeFuncgr.Constgraph.empty; - fun merge _ _ = CodeFuncgr.Constgraph.empty; - fun purge _ NONE _ = CodeFuncgr.Constgraph.empty + val empty = Constgraph.empty; + fun merge _ _ = Constgraph.empty; + fun purge _ NONE _ = Constgraph.empty | purge _ (SOME cs) funcgr = - CodeFuncgr.Constgraph.del_nodes ((CodeFuncgr.Constgraph.all_preds funcgr - o filter (can (CodeFuncgr.Constgraph.get_node funcgr))) cs) funcgr; + Constgraph.del_nodes ((Constgraph.all_preds funcgr + o filter (can (Constgraph.get_node funcgr))) cs) funcgr; end); fun make thy = - Funcgr.change thy o CodeFuncgr.ensure_consts rewrites thy; + Funcgr.change thy o ensure_consts thy; fun make_consts thy = - Funcgr.change_yield thy o CodeFuncgr.check_consts rewrites thy; - -fun make_term thy f = - Funcgr.change_yield thy o CodeFuncgr.ensure_consts_term rewrites thy f; + Funcgr.change_yield thy o check_consts thy; fun eval_conv thy f = - fst o Funcgr.change_yield thy o CodeFuncgr.ensure_consts_eval rewrites thy f; + fst o Funcgr.change_yield thy o ensure_consts_eval thy f; + +fun eval_term thy f = + fst o Funcgr.change_yield thy o ensure_consts_term thy f; fun intervene thy funcgr = Funcgr.change thy (K funcgr); -end; (*functor*) - -structure CodeFuncgr : CODE_FUNCGR = -struct - -open CodeFuncgr; - end; (*struct*) diff -r 9b64aa297524 -r 8ca96f4e49cd src/Tools/code/code_package.ML --- a/src/Tools/code/code_package.ML Wed Aug 15 08:57:41 2007 +0200 +++ b/src/Tools/code/code_package.ML Wed Aug 15 08:57:42 2007 +0200 @@ -9,14 +9,15 @@ sig (* interfaces *) val eval_conv: theory - -> (CodeThingol.code -> CodeThingol.iterm -> cterm -> thm) -> cterm -> thm; + -> (CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> cterm -> thm) + -> cterm -> thm; + val eval_term: theory + -> (CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> cterm -> 'a) + -> cterm -> 'a; + val satisfies_ref: bool option ref; + val satisfies: theory -> cterm -> string list -> bool; val codegen_command: theory -> string -> unit; - (* primitive interfaces *) - val eval_term: theory -> (string (*reference name!*) * 'a option ref) * term -> 'a; - val satisfies_ref: bool option ref; - val satisfies: theory -> term -> string list -> bool; - (* axiomatic interfaces *) type appgen; val add_appconst: string * appgen -> theory -> theory; @@ -63,12 +64,10 @@ (merge_appgens (appgens1, appgens2), merge_abstypes (abstypes1, abstypes2)); ); -structure Funcgr = CodeFuncgrRetrieval (fun rewrites thy = []); - -fun code_depgr thy [] = Funcgr.make thy [] +fun code_depgr thy [] = CodeFuncgr.make thy [] | code_depgr thy consts = let - val gr = Funcgr.make thy consts; + val gr = CodeFuncgr.make thy consts; val select = CodeFuncgr.Constgraph.all_succs gr consts; in CodeFuncgr.Constgraph.subgraph @@ -116,7 +115,10 @@ of SOME ty => SOME ((map_atyps (fn TFree (n, _) => nth tys (the (Int.fromString n)))) ty) | NONE => NONE; -fun ensure_def thy = CodeThingol.ensure_def (CodeName.labelled_name thy); +val value_name = "Isabelle_Eval.EVAL.EVAL"; + +fun ensure_def thy = CodeThingol.ensure_def + (fn s => if s = value_name then "" else CodeName.labelled_name thy s); fun ensure_def_class thy (algbr as ((_, algebra), _)) funcgr class = let @@ -442,7 +444,7 @@ orelse is_some (Code.get_datatype_of_constr thy c2) then error ("Not a function: " ^ CodeUnit.string_of_const thy c2) else (); - val funcgr = Funcgr.make thy [c1, c2]; + val funcgr = CodeFuncgr.make thy [c1, c2]; val ty1 = (f o CodeFuncgr.typ funcgr) c1; val ty2 = CodeFuncgr.typ funcgr c2; val _ = if Sign.typ_equiv thy (ty1, ty2) then () else @@ -513,75 +515,23 @@ fun generate thy funcgr gen it = let (*FIXME*) - val _ = Funcgr.intervene thy funcgr; + val _ = CodeFuncgr.intervene thy funcgr; val cs = map_filter (Consttab.lookup ((snd o snd o Translation.get) thy)) (CodeFuncgr.all funcgr); - val funcgr' = Funcgr.make thy cs; + val CodeFuncgr' = CodeFuncgr.make thy cs; val naming = NameSpace.qualified_names NameSpace.default_naming; val consttab = Consts.empty |> fold (fn c => Consts.declare naming - ((CodeName.const thy c, CodeFuncgr.typ funcgr' c), true)) - (CodeFuncgr.all funcgr'); + ((CodeName.const thy c, CodeFuncgr.typ CodeFuncgr' c), true)) + (CodeFuncgr.all CodeFuncgr'); val algbr = (Code.operational_algebra thy, consttab); in Program.change_yield thy - (CodeThingol.start_transact (gen thy algbr funcgr' it)) + (CodeThingol.start_transact (gen thy algbr CodeFuncgr' it)) + |> fst end; - (*val val_name = "Isabelle_Eval.EVAL.EVAL"; - val val_name' = "Isabelle_Eval.EVAL"; - val val_name'_args = space_implode " " (val_name' :: map (enclose "(" ")") args); - val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [] labelled_name; - fun eval code = ( - reff := NONE; - seri (SOME [val_name]) code; - use_text "generated code for evaluation" Output.ml_output (!eval_verbose) - ("val _ = (" ^ ref_name ^ " := SOME (" ^ val_name'_args ^ "))"); - case !reff - of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name - ^ " (reference probably has been shadowed)") - | SOME value => value - ); - - fun defgen_fun trns = - let - val const' = perhaps (Consttab.lookup ((snd o snd o Translation.get) thy)) const; - val raw_thms = CodeFuncgr.funcs funcgr const'; - val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) const'; - val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty - then raw_thms - else map (CodeUnit.expand_eta 1) raw_thms; - val timeap = if !timing then Output.timeap_msg ("time for " ^ c') - else I; - val msg = cat_lines ("generating code for theorems " :: map string_of_thm thms); - val vs = (map dest_TFree o Consts.typargs consts) (c', ty); - val dest_eqthm = - apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify o prop_of; - fun exprgen_eq (args, rhs) trns = - trns - |> fold_map (exprgen_term thy algbr funcgr) args - ||>> exprgen_term thy algbr funcgr rhs; - in - trns - |> CodeThingol.message msg (fn trns => trns - |> timeap (fold_map (exprgen_eq o dest_eqthm) thms) - ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs - ||>> exprgen_typ thy algbr funcgr ty - |-> (fn ((eqs, vs), ty) => succeed (CodeThingol.Fun (eqs, (vs, ty))))) - end; - val defgen = if (is_some o Code.get_datatype_of_constr thy) const - then defgen_datatypecons - else if is_some opt_tyco - orelse (not o is_some o AxClass.class_of_param thy) c - then defgen_fun - else defgen_classop - in - trns - |> ensure_def thy defgen ("generating constant " ^ CodeUnit.string_of_const thy const) c' - -*) - -(*fun eval_conv thy conv = +fun raw_eval f thy g = let val value_name = "Isabelle_Eval.EVAL.EVAL"; fun ensure_eval thy algbr funcgr t = @@ -590,58 +540,46 @@ exprgen_term' thy algbr funcgr t ##>> exprgen_typ thy algbr funcgr (fastype_of t) #>> (fn (t, ty) => CodeThingol.Fun ([([], t)], ([], ty))); + fun result (dep, code) = + let + val CodeThingol.Fun ([([], t)], ([], ty)) = Graph.get_node code value_name; + val deps = Graph.imm_succs code value_name; + val code' = Graph.del_nodes [value_name] code; + val code'' = CodeThingol.project_code false [] (SOME deps) code'; + in ((code'', (t, ty), deps), (dep, code')) end; in ensure_def thy defgen_eval "evaluation" value_name - #> pair value_name + #> result end; - fun conv' funcgr ct = - let - val (_, code) = generate thy funcgr ensure_eval (Thm.term_of ct); - val consts = CodeThingol.fold_constnames (insert (op =)) t []; - val code = Program.get thy - |> CodeThingol.project_code true [] (SOME consts) - in conv code t ct end; - in Funcgr.eval_conv thy conv' end;*) - -fun eval_conv thy conv = - let - fun conv' funcgr ct = + fun h funcgr ct = let - val (t, _) = generate thy funcgr exprgen_term' (Thm.term_of ct); - val consts = CodeThingol.fold_constnames (insert (op =)) t []; - val code = Program.get thy - |> CodeThingol.project_code true [] (SOME consts) - in conv code t ct end; - in Funcgr.eval_conv thy conv' end; + val (code, (t, ty), deps) = generate thy funcgr ensure_eval (Thm.term_of ct); + in g code (t, ty) deps ct end; + in f thy h end; -fun codegen_term thy t = - let - val ct = Thm.cterm_of thy t; - val (ct', funcgr) = Funcgr.make_term thy (K (K K)) ct; - val t' = Thm.term_of ct'; - in generate thy funcgr exprgen_term' t' |> fst end; - -fun raw_eval_term thy (ref_spec, t) args = - let - val _ = (Term.map_types o Term.map_atyps) (fn _ => - error ("Term " ^ Sign.string_of_term thy t ^ " contains polymorphic type")) - t; - val t' = codegen_term thy t; - in - CodeTarget.eval_term thy CodeName.labelled_name - (Program.get thy) (ref_spec, t') args - end; +fun eval_conv thy = raw_eval CodeFuncgr.eval_conv thy; +fun eval_term thy = raw_eval CodeFuncgr.eval_term thy; val satisfies_ref : bool option ref = ref NONE; -fun eval_term thy t = raw_eval_term thy t []; -fun satisfies thy t witnesses = raw_eval_term thy - (("CodePackage.satisfies_ref", satisfies_ref), t) witnesses; +fun satisfies thy ct witnesses = + let + fun evl code (t, ty) deps ct = + let + val t0 = Thm.term_of ct + val _ = (Term.map_types o Term.map_atyps) (fn _ => + error ("Term " ^ Sign.string_of_term thy t0 ^ " contains polymorphic type")) + t0; + in + CodeTarget.eval_term thy ("CodePackage.satisfies_ref", satisfies_ref) + code (t, ty) witnesses + end; + in eval_term thy evl ct end; fun filter_generatable thy consts = let - val (consts', funcgr) = Funcgr.make_consts thy consts; - val (consts'', _) = generate thy funcgr (fold_map ooo perhaps_def_const) consts'; + val (consts', funcgr) = CodeFuncgr.make_consts thy consts; + val consts'' = generate thy funcgr (fold_map ooo perhaps_def_const) consts'; val consts''' = map_filter (fn (const, SOME _) => SOME const | (_, NONE) => NONE) (consts' ~~ consts''); in consts''' end; @@ -658,9 +596,9 @@ let val (perm1, cs) = CodeUnit.read_const_exprs thy (filter_generatable thy) raw_cs; - val (perm2, cs') = case generate thy (Funcgr.make thy cs) (fold_map ooo ensure_def_const') cs - of ([], _) => (true, NONE) - | (cs, _) => (false, SOME cs); + val (perm2, cs') = case generate thy (CodeFuncgr.make thy cs) (fold_map ooo ensure_def_const') cs + of [] => (true, NONE) + | cs => (false, SOME cs); val code = Program.get thy; val seris' = map (fn (((target, module), file), args) => CodeTarget.get_serializer thy target (perm1 orelse perm2) module file args @@ -670,10 +608,10 @@ end; fun code_thms_cmd thy = - code_thms thy o snd o CodeUnit.read_const_exprs thy (fst o Funcgr.make_consts thy); + code_thms thy o snd o CodeUnit.read_const_exprs thy (fst o CodeFuncgr.make_consts thy); fun code_deps_cmd thy = - code_deps thy o snd o CodeUnit.read_const_exprs thy (fst o Funcgr.make_consts thy); + code_deps thy o snd o CodeUnit.read_const_exprs thy (fst o CodeFuncgr.make_consts thy); val (inK, module_nameK, fileK) = ("in", "module_name", "file"); diff -r 9b64aa297524 -r 8ca96f4e49cd src/Tools/code/code_thingol.ML --- a/src/Tools/code/code_thingol.ML Wed Aug 15 08:57:41 2007 +0200 +++ b/src/Tools/code/code_thingol.ML Wed Aug 15 08:57:42 2007 +0200 @@ -76,7 +76,7 @@ -> code -> code; val empty_funs: code -> string list; val is_cons: code -> string -> bool; - val add_eval_def: string (*bind name*) * iterm -> code -> code; + val add_eval_def: string (*bind name*) * (iterm * itype) -> code -> code; val ensure_def: (string -> string) -> (transact -> def * transact) -> string -> string -> transact -> transact; @@ -247,7 +247,6 @@ * (string * iterm) list); type code = def Graph.T; -type transact = Graph.key option * code; (* abstract code *) @@ -372,6 +371,8 @@ (* transaction protocol *) +type transact = Graph.key option * code; + fun ensure_def labelled_name defgen msg name (dep, code) = let val msg' = (case dep @@ -402,9 +403,9 @@ |> f |-> (fn x => fn (_, code) => (x, code)); -fun add_eval_def (name, t) code = +fun add_eval_def (name, (t, ty)) code = code - |> Graph.new_node (name, Fun ([([], t)], ([("_", [])], ITyVar "_"))) + |> Graph.new_node (name, Fun ([([], t)], ([], ty))) |> fold (curry Graph.add_edge name) (Graph.keys code); end; (*struct*) diff -r 9b64aa297524 -r 8ca96f4e49cd src/Tools/nbe.ML --- a/src/Tools/nbe.ML Wed Aug 15 08:57:41 2007 +0200 +++ b/src/Tools/nbe.ML Wed Aug 15 08:57:42 2007 +0200 @@ -60,11 +60,6 @@ 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 = @@ -233,7 +228,7 @@ val result = ml_list (map (fn (c, n) => nbe_abss n (nbe_fun c)) num_args); in (cs, ml_Let (bind_funs @ [bind_locals]) result) end; -fun assemble_eval thy is_fun t = +fun assemble_eval thy is_fun (t, deps) = let val funs = CodeThingol.fold_constnames (insert (op =)) t []; val frees = CodeThingol.fold_unbound_varnames (insert (op =)) t []; @@ -314,7 +309,7 @@ (* evaluation with type reconstruction *) -fun eval thy code t t' = +fun eval thy code t t' deps = let fun subst_Frees [] = I | subst_Frees inst = @@ -330,7 +325,7 @@ fun constrain t = singleton (ProofContext.infer_types_pats (ProofContext.init thy)) (TypeInfer.constrain t ty); in - t' + (t', deps) |> eval_term thy (Symtab.defined (ensure_funs thy code)) |> term_of_univ thy |> tracing (fn t => "Normalized:\n" ^ setmp show_types true Display.raw_string_of_term t) @@ -345,22 +340,22 @@ (* evaluation oracle *) -exception Normalization of CodeThingol.code * term * CodeThingol.iterm; +exception Normalization of CodeThingol.code * term * CodeThingol.iterm * string list; -fun normalization_oracle (thy, Normalization (code, t, t')) = - Logic.mk_equals (t, eval thy code t t'); +fun normalization_oracle (thy, Normalization (code, t, t', deps)) = + Logic.mk_equals (t, eval thy code t t' deps); -fun normalization_invoke thy code t t' = - Thm.invoke_oracle_i thy "HOL.normalization" (thy, Normalization (code, t, t')); - (*FIXME get rid of hardwired theory name "HOL"*) +fun normalization_invoke thy code t t' deps = + Thm.invoke_oracle_i thy "Code_Setup.normalization" (thy, Normalization (code, t, t', deps)); + (*FIXME get rid of hardwired theory name*) fun normalization_conv ct = let val thy = Thm.theory_of_cterm ct; - fun conv code t' ct = + fun conv code (t', ty') deps ct = let val t = Thm.term_of ct; - in normalization_invoke thy code t t' end; + in normalization_invoke thy code t t' deps end; in CodePackage.eval_conv thy conv ct end; (* evaluation command *)