# HG changeset patch # User haftmann # Date 1241706155 -7200 # Node ID 88aaab83b6fcd93e95bb900288f918dafa08161f # Parent 878e00798148f5ee6fe61e4106d25f5637d07f75 dropped explicit suppport for frees in evaluation conversion stack diff -r 878e00798148 -r 88aaab83b6fc src/Tools/code/code_ml.ML --- a/src/Tools/code/code_ml.ML Thu May 07 16:22:34 2009 +0200 +++ b/src/Tools/code/code_ml.ML Thu May 07 16:22:35 2009 +0200 @@ -958,10 +958,7 @@ fun eval some_target reff postproc thy t args = let val ctxt = ProofContext.init thy; - val _ = if null (Term.add_frees t []) then () else error ("Term " - ^ quote (Syntax.string_of_term_global thy t) - ^ " to be evaluated contains free variables"); - fun evaluator naming program (((_, (_, ty)), _), t) deps = + fun evaluator naming program ((_, (_, ty)), t) deps = let val _ = if Code_Thingol.contains_dictvar t then error "Term to be evaluated contains free dictionaries" else (); diff -r 878e00798148 -r 88aaab83b6fc src/Tools/code/code_thingol.ML --- a/src/Tools/code/code_thingol.ML Thu May 07 16:22:34 2009 +0200 +++ b/src/Tools/code/code_thingol.ML Thu May 07 16:22:35 2009 +0200 @@ -85,10 +85,10 @@ val consts_program: theory -> string list -> string list * (naming * program) val cached_program: theory -> naming * program val eval_conv: theory -> (sort -> sort) - -> (naming -> program -> (((string * sort) list * typscheme) * (string * itype) list) * iterm -> string list -> cterm -> thm) + -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> cterm -> thm) -> cterm -> thm val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a) - -> (naming -> program -> (((string * sort) list * typscheme) * (string * itype) list) * iterm -> string list -> 'a) + -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a) -> term -> 'a end; @@ -755,7 +755,7 @@ (* value evaluation *) -fun ensure_value thy algbr funcgr (fs, t) = +fun ensure_value thy algbr funcgr t = let val ty = fastype_of t; val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =) @@ -766,7 +766,7 @@ ##>> translate_term thy algbr funcgr NONE t #>> (fn ((vs, ty), t) => Fun (Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))]))); - fun term_value fs (dep, (naming, program1)) = + fun term_value (dep, (naming, program1)) = let val Fun (_, (vs_ty, [(([], t), _)])) = Graph.get_node program1 Term.dummy_patternN; @@ -774,22 +774,19 @@ val program2 = Graph.del_nodes [Term.dummy_patternN] program1; val deps_all = Graph.all_succs program2 deps; val program3 = Graph.subgraph (member (op =) deps_all) program2; - in (((naming, program3), (((vs_ty, fs), t), deps)), (dep, (naming, program2))) end; + in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end; in ensure_stmt ((K o K) NONE) pair stmt_value Term.dummy_patternN #> snd - #> fold_map (fn (v, ty) => translate_typ thy algbr funcgr ty - #-> (fn ty' => pair (v, ty'))) fs - #-> (fn fs' => term_value fs') + #> term_value end; fun base_evaluator thy evaluator algebra funcgr vs t = let - val fs = Term.add_frees t []; - val (((naming, program), ((((vs', ty'), fs'), t'), deps)), _) = - invoke_generation thy (algebra, funcgr) ensure_value (fs, t); + val (((naming, program), (((vs', ty'), t'), deps)), _) = + invoke_generation thy (algebra, funcgr) ensure_value t; val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs'; - in evaluator naming program (((vs'', (vs', ty')), fs'), t') deps end; + in evaluator naming program ((vs'', (vs', ty')), t') deps end; fun eval_conv thy prep_sort = Code_Wellsorted.eval_conv thy prep_sort o base_evaluator thy; fun eval thy prep_sort postproc = Code_Wellsorted.eval thy prep_sort postproc o base_evaluator thy; diff -r 878e00798148 -r 88aaab83b6fc src/Tools/code/code_wellsorted.ML --- a/src/Tools/code/code_wellsorted.ML Thu May 07 16:22:34 2009 +0200 +++ b/src/Tools/code/code_wellsorted.ML Thu May 07 16:22:35 2009 +0200 @@ -293,19 +293,22 @@ fun obtain thy cs ts = apsnd snd (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts)); -fun prepare_sorts prep_sort (Const (c, ty)) = Const (c, map_type_tfree - (fn (v, sort) => TFree (v, prep_sort sort)) ty) +fun prepare_sorts_typ prep_sort + = map_type_tfree (fn (v, sort) => TFree (v, prep_sort sort)); + +fun prepare_sorts prep_sort (Const (c, ty)) = + Const (c, prepare_sorts_typ prep_sort ty) | prepare_sorts prep_sort (t1 $ t2) = prepare_sorts prep_sort t1 $ prepare_sorts prep_sort t2 | prepare_sorts prep_sort (Abs (v, ty, t)) = - Abs (v, Type.strip_sorts ty, prepare_sorts prep_sort t) - | prepare_sorts _ (Term.Free (v, ty)) = Term.Free (v, Type.strip_sorts ty) + 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 = let + val pp = Syntax.pp_global thy; val ct = cterm_of proto_ct; - val _ = (Term.map_types Type.no_tvars o Sign.no_vars (Syntax.pp_global thy)) + val _ = (Sign.no_frees pp o map_types (K dummyT) o Sign.no_vars pp) (Thm.term_of ct); val thm = Code.preprocess_conv thy ct; val ct' = Thm.rhs_of thm; @@ -313,6 +316,7 @@ 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 (algebra', eqngr') = obtain thy consts [t'']; in conclude_evaluation (evaluator algebra' eqngr' vs t'' ct') thm end;