# HG changeset patch # User haftmann # Date 1248183871 -7200 # Node ID 8bac9ee4b28d79133b8f44164ccc6cdc0a9dd423 # Parent 4ee1c1aebbcc62e9b090ecbdc470af519bdd69c9 integrated add_triv_classes into evaluation stack diff -r 4ee1c1aebbcc -r 8bac9ee4b28d src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Tue Jul 21 15:44:31 2009 +0200 +++ b/src/Tools/Code/code_ml.ML Tue Jul 21 15:44:31 2009 +0200 @@ -966,7 +966,7 @@ val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name' ^ space_implode " " (map (enclose "(" ")") args) ^ " end"; in ML_Context.evaluate ctxt false reff sml_code end; - in Code_Thingol.eval thy I postproc evaluator t end; + in Code_Thingol.eval thy postproc evaluator t end; (* instrumentalization by antiquotation *) diff -r 4ee1c1aebbcc -r 8bac9ee4b28d src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Tue Jul 21 15:44:31 2009 +0200 +++ b/src/Tools/Code/code_preproc.ML Tue Jul 21 15:44:31 2009 +0200 @@ -23,9 +23,10 @@ val all: code_graph -> string list val pretty: theory -> code_graph -> Pretty.T val obtain: theory -> string list -> term list -> code_algebra * code_graph - val eval_conv: theory -> (sort -> sort) + val resubst_triv_consts: theory -> term -> term + val eval_conv: theory -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm - val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a) + val eval: theory -> ((term -> term) -> 'a -> 'a) -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a val setup: theory -> theory @@ -161,7 +162,10 @@ |> rhs_conv (Simplifier.rewrite post) end; -fun postprocess_term thy = term_of_conv thy (postprocess_conv thy); +fun resubst_triv_consts thy = map_aterms (fn t as Const (c, ty) => Const (Code.resubst_alias thy c, ty) + | t => t); + +fun postprocess_term thy = term_of_conv thy (postprocess_conv thy) #> resubst_triv_consts thy; fun print_codeproc thy = let @@ -495,7 +499,7 @@ Abs (v, prepare_sorts_typ prep_sort ty, prepare_sorts prep_sort t) | prepare_sorts _ (t as Bound _) = t; -fun gen_eval thy cterm_of conclude_evaluation prep_sort evaluator proto_ct = +fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct = let val pp = Syntax.pp_global thy; val ct = cterm_of proto_ct; @@ -507,8 +511,10 @@ val vs = Term.add_tfrees t' []; val consts = fold_aterms (fn Const (c, _) => insert (op =) c | _ => I) t' []; - - val t'' = prepare_sorts prep_sort t'; + + val add_triv_classes = curry (Sorts.inter_sort (Sign.classes_of thy)) + (Code.triv_classes thy); + val t'' = prepare_sorts add_triv_classes t'; val (algebra', eqngr') = obtain thy consts [t'']; in conclude_evaluation (evaluator algebra' eqngr' vs t'' ct') thm end; @@ -527,8 +533,8 @@ end; in gen_eval thy I conclude_evaluation end; -fun eval thy prep_sort postproc evaluator = gen_eval thy (Thm.cterm_of thy) - (K o postproc (postprocess_term thy)) prep_sort (simple_evaluator evaluator); +fun eval thy postproc evaluator = gen_eval thy (Thm.cterm_of thy) + (K o postproc (postprocess_term thy)) (simple_evaluator evaluator); (** setup **) diff -r 4ee1c1aebbcc -r 8bac9ee4b28d src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Tue Jul 21 15:44:31 2009 +0200 +++ b/src/Tools/Code/code_thingol.ML Tue Jul 21 15:44:31 2009 +0200 @@ -82,10 +82,10 @@ val read_const_exprs: theory -> string list -> string list * string list val consts_program: theory -> string list -> string list * (naming * program) val cached_program: theory -> naming * program - val eval_conv: theory -> (sort -> sort) + val eval_conv: theory -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> cterm -> thm) -> cterm -> thm - val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a) + val eval: theory -> ((term -> term) -> 'a -> 'a) -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a) -> term -> 'a end; @@ -803,8 +803,8 @@ val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs'; in evaluator naming program ((vs'', (vs', ty')), t') deps end; -fun eval_conv thy prep_sort = Code_Preproc.eval_conv thy prep_sort o base_evaluator thy; -fun eval thy prep_sort postproc = Code_Preproc.eval thy prep_sort postproc o base_evaluator thy; +fun eval_conv thy = Code_Preproc.eval_conv thy o base_evaluator thy; +fun eval thy postproc = Code_Preproc.eval thy postproc o base_evaluator thy; (** diagnostic commands **) diff -r 4ee1c1aebbcc -r 8bac9ee4b28d src/Tools/nbe.ML --- a/src/Tools/nbe.ML Tue Jul 21 15:44:31 2009 +0200 +++ b/src/Tools/nbe.ML Tue Jul 21 15:44:31 2009 +0200 @@ -439,9 +439,6 @@ fun normalize thy naming program ((vs0, (vs, ty)), t) deps = let - fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty) - | t => t); - val resubst_triv_consts = subst_const (Code.resubst_alias thy); val ty' = typ_of_itype program vs0 ty; fun type_infer t = singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I @@ -453,8 +450,8 @@ val string_of_term = setmp show_types true (Syntax.string_of_term_global thy); in compile_eval thy naming program (vs, t) deps + |> Code_Preproc.resubst_triv_consts thy |> tracing (fn t => "Normalized:\n" ^ string_of_term t) - |> resubst_triv_consts |> type_infer |> tracing (fn t => "Types inferred:\n" ^ string_of_term t) |> check_tvars @@ -463,9 +460,6 @@ (* evaluation oracle *) -fun add_triv_classes thy = curry (Sorts.inter_sort (Sign.classes_of thy)) - (Code.triv_classes thy); - fun mk_equals thy lhs raw_rhs = let val ty = Thm.typ_of (Thm.ctyp_of_term lhs); @@ -506,9 +500,9 @@ val norm_conv = no_frees_conv (fn ct => let val thy = Thm.theory_of_cterm ct; - in Code_Thingol.eval_conv thy (add_triv_classes thy) (norm_oracle thy) ct end); + in Code_Thingol.eval_conv thy (norm_oracle thy) ct end); -fun norm thy = no_frees_rew (Code_Thingol.eval thy (add_triv_classes thy) I (normalize thy)); +fun norm thy = no_frees_rew (Code_Thingol.eval thy I (normalize thy)); (* evaluation command *)