# HG changeset patch # User haftmann # Date 1208894431 -7200 # Node ID 6c8cd101f8753186844a698fc9b36c104bb5c229 # Parent 947b6013e8637c85ba7e5f9ea9941edc48ed70c6 more general evaluation combinators diff -r 947b6013e863 -r 6c8cd101f875 src/Tools/code/code_funcgr.ML --- a/src/Tools/code/code_funcgr.ML Tue Apr 22 22:00:25 2008 +0200 +++ b/src/Tools/code/code_funcgr.ML Tue Apr 22 22:00:31 2008 +0200 @@ -16,8 +16,8 @@ val pretty: theory -> T -> Pretty.T val make: theory -> string list -> T val make_consts: theory -> string list -> string list * T - val eval_conv: theory -> (T -> cterm -> thm) -> cterm -> thm - val eval_term: theory -> (T -> term -> 'a) -> term -> 'a + val eval_conv: theory -> (term -> term * (T -> term -> thm)) -> cterm -> thm + val eval_term: theory -> (term -> term * (T -> term -> 'a)) -> term -> 'a end structure CodeFuncgr : CODE_FUNCGR = @@ -276,55 +276,42 @@ val (consts', funcgr') = fold_map try_const consts funcgr; in (map_filter I consts', funcgr') end; -fun raw_eval thy f ct funcgr = +fun proto_eval thy cterm_of evaluator_fr evaluator proto_ct funcgr = let - val algebra = Code.coregular_algebra thy; - fun consts_of ct = fold_aterms (fn Const c_ty => cons c_ty | _ => I) - (Thm.term_of ct) []; + val ct = cterm_of proto_ct; 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; - val ct' = Thm.rhs_of thm1; - val cs = map fst (consts_of ct'); - val funcgr' = ensure_consts thy algebra cs funcgr; - val (_, thm2) = Thm.varifyT' [] thm1; - val thm3 = Thm.reflexive (Thm.rhs_of thm2); - val [thm4] = resort_thms algebra (try (fst o Graph.get_node funcgr')) [thm3] - handle CLASS_ERROR (_, msg) => error msg; - val tfrees = Term.add_tfrees (Thm.prop_of thm1) []; - fun inst thm = + fun consts_of t = fold_aterms (fn Const c_ty => cons c_ty | _ => I) + t []; + val algebra = Code.coregular_algebra thy; + val thm = Code.preprocess_conv ct; + val ct' = Thm.rhs_of thm; + val t' = Thm.term_of ct'; + val consts = map fst (consts_of t'); + val funcgr' = ensure_consts thy algebra consts funcgr; + val (t'', evaluator') = apsnd evaluator_fr (evaluator t'); + val consts' = consts_of t''; + val dicts = instances_of_consts thy algebra funcgr' consts'; + val funcgr'' = ensure_consts thy algebra dicts funcgr'; + in (evaluator' thm funcgr'' t'', funcgr'') end; + +fun proto_eval_conv thy = + let + fun evaluator evaluator' thm1 funcgr t = let - val tvars = Term.add_tvars (Thm.prop_of thm) []; - val instmap = map2 (fn (v_i, sort) => fn (v, _) => pairself (Thm.ctyp_of thy) - (TVar (v_i, sort), TFree (v, sort))) tvars tfrees; - in Thm.instantiate (instmap, []) thm end; - val thm5 = inst thm2; - val thm6 = inst thm4; - val ct'' = Thm.rhs_of thm6; - val c_exprs = consts_of ct''; - val drop = drop_classes thy tfrees; - val instdefs = instances_of_consts thy algebra funcgr' c_exprs; - val funcgr'' = ensure_consts thy algebra instdefs funcgr'; - in (f drop thm5 funcgr'' ct'', funcgr'') end; - -fun raw_eval_conv thy conv = - let - fun conv' drop_classes thm1 funcgr ct = - let - val thm2 = conv funcgr ct; + val thm2 = evaluator' funcgr t; val thm3 = Code.postprocess_conv (Thm.rhs_of thm2); - val thm23 = drop_classes (Thm.transitive thm2 thm3); in - Thm.transitive thm1 thm23 handle THM _ => - error ("could not construct proof:\n" + Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ => + error ("could not construct evaluation proof (probably due to wellsortedness problem):\n" ^ (cat_lines o map string_of_thm) [thm1, thm2, thm3]) end; - in raw_eval thy conv' end; + in proto_eval thy I evaluator end; -fun raw_eval_term thy f t = +fun proto_eval_term thy = let - fun f' _ _ funcgr ct = f funcgr (Thm.term_of ct); - in raw_eval thy f' (Thm.cterm_of thy t) end; + fun evaluator evaluator' _ funcgr t = evaluator' funcgr t; + in proto_eval thy (Thm.cterm_of thy) evaluator end; end; (*local*) @@ -346,9 +333,9 @@ Funcgr.change_yield thy o check_consts thy; fun eval_conv thy f = - fst o Funcgr.change_yield thy o raw_eval_conv thy f; + fst o Funcgr.change_yield thy o proto_eval_conv thy f; fun eval_term thy f = - fst o Funcgr.change_yield thy o raw_eval_term thy f; + fst o Funcgr.change_yield thy o proto_eval_term thy f; end; (*struct*) diff -r 947b6013e863 -r 6c8cd101f875 src/Tools/code/code_package.ML --- a/src/Tools/code/code_package.ML Tue Apr 22 22:00:25 2008 +0200 +++ b/src/Tools/code/code_package.ML Tue Apr 22 22:00:31 2008 +0200 @@ -8,12 +8,12 @@ signature CODE_PACKAGE = sig val evaluate_conv: theory - -> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm - -> string list -> cterm -> thm) + -> (term -> term * (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm + -> string list -> thm)) -> cterm -> thm; val evaluate_term: theory - -> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm - -> string list -> term -> 'a) + -> (term -> term * (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm + -> string list -> 'a)) -> term -> 'a; val eval_conv: string * (unit -> thm) option ref -> theory -> cterm -> string list -> thm; @@ -103,24 +103,31 @@ (* evaluation machinery *) -fun evaluate eval_kind term_of thy eval = eval_kind thy (fn funcgr => fn ct => +fun evaluate eval_kind thy evaluator = let - val ((code, (vs_ty_t, deps)), _) = generate thy funcgr - CodeThingol.ensure_value (term_of ct) - in eval code vs_ty_t deps ct end); + fun evaluator'' evaluator''' funcgr t = + let + val ((code, (vs_ty_t, deps)), _) = + generate thy funcgr CodeThingol.ensure_value t; + in evaluator''' code vs_ty_t deps end; + fun evaluator' t = + let + val (t', evaluator''') = evaluator t; + in (t', evaluator'' evaluator''') end; + in eval_kind thy evaluator' end -fun evaluate_conv thy = evaluate CodeFuncgr.eval_conv Thm.term_of thy; -fun evaluate_term thy = evaluate CodeFuncgr.eval_term I thy; +fun evaluate_conv thy = evaluate CodeFuncgr.eval_conv thy; +fun evaluate_term thy = evaluate CodeFuncgr.eval_term thy; -fun eval_ml reff args thy code ((vs, ty), t) deps _ = +fun eval_ml reff args thy code ((vs, ty), t) deps = CodeTarget.eval thy reff code (t, ty) args; fun eval evaluate term_of reff thy ct args = let val _ = if null (term_frees (term_of ct)) then () else error ("Term " ^ quote (Sign.string_of_term thy (term_of ct)) - ^ " to be evaluated containts free variables"); - in evaluate thy (eval_ml reff args thy) ct end; + ^ " to be evaluated contains free variables"); + in evaluate thy (fn t => (t, eval_ml reff args thy)) ct end; fun eval_conv reff = eval evaluate_conv Thm.term_of reff; fun eval_term reff = eval evaluate_term I reff;