# HG changeset patch # User haftmann # Date 1160751167 -7200 # Node ID f08574148b7a0180e78eb03af27f34e92e6dbd2a # Parent 19d7f07b0fa397b22ff8f011fa053bbbe11282d4 tuned diff -r 19d7f07b0fa3 -r f08574148b7a src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Fri Oct 13 16:52:46 2006 +0200 +++ b/src/HOL/Tools/datatype_codegen.ML Fri Oct 13 16:52:47 2006 +0200 @@ -336,8 +336,6 @@ val abs = Name.names Name.context "a" (Library.drop (length ts, tys)); val (ts', t) = split_last (ts @ map Free abs); val (tys', sty) = split_last tys; - fun freenames_of t = fold_aterms - (fn Free (v, _) => insert (op =) v | _ => I) t []; fun dest_case ((c, tys_decl), ty) t = let val (vs, t') = Term.strip_abs_eta (length tys_decl) t; diff -r 19d7f07b0fa3 -r f08574148b7a src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Fri Oct 13 16:52:46 2006 +0200 +++ b/src/Pure/Tools/codegen_package.ML Fri Oct 13 16:52:47 2006 +0200 @@ -21,6 +21,8 @@ -> ((string * typ) list * ((term * typ) * (term * term) list)) option) -> appgen; val appgen_let: appgen; + + val timing: bool ref; end; structure CodegenPackage : CODEGEN_PACKAGE = @@ -173,6 +175,7 @@ |-> (fn (tyco, tys) => pair (tyco `%% tys)); exception CONSTRAIN of (string * typ) * typ; +val timing = ref false; fun exprgen_typinst thy (algbr as ((proj_sort, algebra), consts)) funcgr strct (ty_ctxt, sort_decl) trns = let @@ -271,6 +274,8 @@ (perhaps (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy)) (c, tys)) of eq_thms as eq_thm :: _ => let + 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 eq_thms); val ty = (Logic.unvarifyT o CodegenData.typ_func thy) eq_thm; val vs = (map dest_TFree o Consts.typargs consts) (c', ty); @@ -283,7 +288,7 @@ in trns |> CodegenThingol.message msg (fn trns => trns - |> fold_map (exprgen_eq o dest_eqthm) eq_thms + |> timeap (fold_map (exprgen_eq o dest_eqthm) eq_thms) ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs ||>> exprgen_type thy algbr funcgr strct ty |-> (fn ((eqs, vs), ty) => succeed (CodegenThingol.Fun (eqs, (vs, ty))))) @@ -397,8 +402,7 @@ case try (int_of_numeral thy) (list_comb (Const c, ts)) of SOME i => trns - |> appgen_default thy algbr funcgr strct app - |-> (fn t => pair (CodegenThingol.INum (i, t))) + |> pair (CodegenThingol.INum i) | NONE => trns |> appgen_default thy algbr funcgr strct app; @@ -408,14 +412,16 @@ of SOME i => trns |> exprgen_type thy algbr funcgr strct ty - ||>> appgen_default thy algbr funcgr strct app - |-> (fn (_, t0) => pair (IChar (chr i, t0))) + |-> (fn _ => pair (IChar (chr i))) | NONE => trns |> appgen_default thy algbr funcgr strct app; +val debug_term = ref (Bound 0); + fun appgen_case dest_case_expr thy algbr funcgr strct (app as (c_ty, ts)) trns = let + val _ = debug_term := list_comb (Const c_ty, ts); val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts)); fun fold_map_aterms f (t $ u) s = s @@ -427,16 +433,23 @@ |> fold_map_aterms f t |-> (fn t' => pair (Abs (v, ty, t'))) | fold_map_aterms f a s = f a s; - fun purify_term_frees (Free (v, ty)) ctxt = + fun purify_term_frees (Free (v, ty)) (renaming, ctxt) = let val ([v'], ctxt') = Name.variants [CodegenNames.purify_var v] ctxt; - in (Free (v, ty), ctxt') end + val renaming' = if v <> v' then Symtab.update (v, v') renaming else renaming; + in (Free (v', ty), (renaming', ctxt')) end | purify_term_frees t ctxt = (t, ctxt); fun clausegen (raw_dt, raw_bt) trns = let - val ((dt, bt), _) = Name.context - |> fold_map_aterms purify_term_frees raw_dt - ||>> fold_map_aterms purify_term_frees raw_bt; + val d_vs = map fst (Term.add_frees raw_dt []); + val b_vs = map fst (Term.add_frees raw_bt []); + val (dt, (renaming, ctxt)) = + Name.context + |> fold Name.declare (subtract (op =) d_vs b_vs) + |> pair Symtab.empty + |> fold_map_aterms purify_term_frees raw_dt; + val bt = map_aterms (fn t as Free (v, ty) => Free (perhaps (Symtab.lookup renaming) v, ty) + | t => t) raw_bt; in trns |> exprgen_term thy algbr funcgr strct dt @@ -447,21 +460,19 @@ |> exprgen_term thy algbr funcgr strct st ||>> exprgen_type thy algbr funcgr strct sty ||>> fold_map clausegen ds - ||>> appgen_default thy algbr funcgr strct app - |-> (fn (((se, sty), ds), e0) => pair (ICase (((se, sty), ds), e0))) + |-> (fn ((se, sty), ds) => pair (ICase ((se, sty), ds))) end; fun appgen_let thy algbr funcgr strct (app as (_, [st, ct])) trns = trns |> exprgen_term thy algbr funcgr strct ct ||>> exprgen_term thy algbr funcgr strct st - ||>> appgen_default thy algbr funcgr strct app - |-> (fn (((v, ty) `|-> be, se), e0) => - pair (ICase (((se, ty), case be - of ICase (((IVar w, _), ds), _) => if v = w then ds else [(IVar v, be)] + |-> (fn ((v, ty) `|-> be, se) => + pair (ICase ((se, ty), case be + of ICase ((IVar w, _), ds) => if v = w then ds else [(IVar v, be)] | _ => [(IVar v, be)] - ), e0)) - | (_, e0) => pair e0); + )) + | _ => appgen_default thy algbr funcgr strct app); fun add_appconst (c, appgen) thy = let @@ -630,7 +641,7 @@ of [] => NONE | xs => SOME xs; val seris' = map_filter (fn (target, args as _ :: _) => - SOME (CodegenSerializer.get_serializer thy (target, args)) | _ => NONE) seris; + SOME (CodegenSerializer.get_serializer thy target args) | _ => NONE) seris; fun generate' thy = case cs of [] => [] | _ => diff -r 19d7f07b0fa3 -r f08574148b7a src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Fri Oct 13 16:52:46 2006 +0200 +++ b/src/Pure/Tools/codegen_thingol.ML Fri Oct 13 16:52:47 2006 +0200 @@ -28,12 +28,11 @@ | IVar of vname | `$ of iterm * iterm | `|-> of (vname * itype) * iterm - | INum of IntInf.int * iterm - | IChar of string (*length one!*) * iterm - | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm; - (*((discriminendum term (td), discriminendum type (ty)), - [(selector pattern (p), body term (t))] (bs)), - pure term (t0))*) + | INum of IntInf.int + | IChar of string (*length one!*) + | ICase of (iterm * itype) * (iterm * iterm) list; + (*(discriminendum term (td), discriminendum type (ty)), + [(selector pattern (p), body term (t))] (bs))*) val `--> : itype list * itype -> itype; val `$$ : iterm * iterm list -> iterm; val `|--> : (vname * itype) list * iterm -> iterm; @@ -47,11 +46,10 @@ val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a; val unfold_fun: itype -> itype list * itype; val unfold_app: iterm -> iterm * iterm list; - val unfold_abs: iterm -> (iterm * itype) list * iterm; + val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm; val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm; val unfold_const_app: iterm -> ((string * (inst list list * itype)) * iterm list) option; - val map_pure: (iterm -> 'a) -> iterm -> 'a; val eta_expand: (string * (inst list list * itype)) * iterm list -> int -> iterm; val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; @@ -72,9 +70,10 @@ val empty_code: code; val get_def: code -> string -> def; val merge_code: code * code -> code; - val project_code: string list -> code -> code; + val project_code: string list (*hidden*) -> string list option (*selected*) + -> code -> code; val add_eval_def: string (*shallow name space*) * iterm -> code -> string * code; - val delete_garbage: string list (*hidden definitions*) -> code -> code; + val ensure_def: (transact -> def * code) -> bool -> string -> string -> transact -> transact; @@ -85,7 +84,6 @@ val trace: bool ref; val tracing: ('a -> string) -> 'a -> 'a; - val soft_exc: bool ref; end; structure CodegenThingol: CODEGEN_THINGOL = @@ -95,7 +93,6 @@ val trace = ref false; fun tracing f x = (if !trace then Output.tracing (f x) else (); x); -val soft_exc = ref true; fun unfoldl dest x = case dest x @@ -131,9 +128,9 @@ | IVar of vname | `$ of iterm * iterm | `|-> of (vname * itype) * iterm - | INum of IntInf.int * iterm - | IChar of string * iterm - | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm; + | INum of IntInf.int + | IChar of string + | ICase of (iterm * itype) * (iterm * iterm) list; (*see also signature*) (* @@ -174,13 +171,13 @@ | _ => NONE); val unfold_abs = unfoldr - (fn (v, ty) `|-> (t as ICase (((IVar w, _), [(p, t')]), _)) => - if v = w then SOME ((p, ty), t') else SOME ((IVar v, ty), t) - | (v, ty) `|-> t => SOME ((IVar v, ty), t) + (fn (v, ty) `|-> (t as ICase ((IVar w, _), [(p, t')])) => + if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t) + | (v, ty) `|-> t => SOME (((v, NONE), ty), t) | _ => NONE) val unfold_let = unfoldr - (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t) + (fn ICase ((td, ty), [(p, t)]) => SOME (((p, ty), td), t) | _ => NONE); fun unfold_const_app t = @@ -188,21 +185,6 @@ of (IConst c, ts) => SOME (c, ts) | _ => NONE; -fun map_pure f (t as IConst _) = - f t - | map_pure f (t as IVar _) = - f t - | map_pure f (t as _ `$ _) = - f t - | map_pure f (t as _ `|-> _) = - f t - | map_pure f (INum (_, t0)) = - f t0 - | map_pure f (IChar (_, t0)) = - f t0 - | map_pure f (ICase (_, t0)) = - f t0; - fun fold_aiterms f (t as IConst _) = f t | fold_aiterms f (t as IVar _) = @@ -211,12 +193,12 @@ fold_aiterms f t1 #> fold_aiterms f t2 | fold_aiterms f (t as _ `|-> t') = f t #> fold_aiterms f t' - | fold_aiterms f (INum (_, t0)) = - fold_aiterms f t0 - | fold_aiterms f (IChar (_, t0)) = - fold_aiterms f t0 - | fold_aiterms f (ICase (_, t0)) = - fold_aiterms f t0; + | fold_aiterms f (t as INum _) = + f t + | fold_aiterms f (t as IChar _) = + f t + | fold_aiterms f (ICase ((td, _), bs)) = + fold_aiterms f td #> fold (fn (p, t) => fold_aiterms f p #> fold_aiterms f t) bs; fun fold_constnames f = let @@ -241,12 +223,12 @@ add vs t1 #> add vs t2 | add vs ((v, _) `|-> t) = add (insert (op =) v vs) t - | add vs (INum (_, t)) = - add vs t - | add vs (IChar (_, t)) = - add vs t - | add vs (ICase (_, t0)) = - add vs t0 + | add vs (INum _) = + I + | add vs (IChar _) = + I + | add vs (ICase ((td, _), bs)) = + add vs td #> fold (fn (p, t) => add vs p #> add vs t) bs; in add [] end; fun eta_expand (c as (_, (_, ty)), ts) k = @@ -278,7 +260,7 @@ type code = def Graph.T; type transact = Graph.key option * code; -exception FAIL of string list * exn option; +exception FAIL of string list; (* abstract code *) @@ -307,19 +289,24 @@ val merge_code = Graph.join (fn _ => fn def12 => if eq_def def12 then fst def12 else Bot); -fun project_code names code = - Graph.project (member (op =) (Graph.all_succs code names)) code; - -fun delete_garbage hidden code = +fun project_code hidden raw_selected code = let fun is_bot name = case get_def code name of Bot => true | _ => false; val names = subtract (op =) hidden (Graph.keys code); - val names' = subtract (op =) - (Graph.all_preds code (filter is_bot names)) names; + val deleted = Graph.all_preds code (filter is_bot names); + val selected = case raw_selected + of NONE => names |> subtract (op =) deleted + | SOME sel => sel + |> subtract (op =) deleted + |> subtract (op =) hidden + |> Graph.all_succs code + |> subtract (op =) deleted + |> subtract (op =) hidden; in - Graph.project (member (op =) names') code + code + |> Graph.project (member (op =) selected) end; fun check_samemodule names = @@ -406,17 +393,10 @@ fun prep_def def modl = (check_prep_def modl def, modl); fun invoke_generator name defgen modl = - if ! soft_exc (*that "!" isn't a "not"...*) - then defgen (SOME name, modl) - handle FAIL (msgs, exc) => - if strict then raise FAIL (msg' :: msgs, exc) - else (Bot, modl) - | e => raise - FAIL (["definition generator for " ^ quote name, msg'], SOME e) - else defgen (SOME name, modl) - handle FAIL (msgs, exc) => - if strict then raise FAIL (msg' :: msgs, exc) - else (Bot, modl); + defgen (SOME name, modl) + handle FAIL msgs => + if strict then raise FAIL (msg' :: msgs) + else (Bot, modl); in modl |> (if can (get_def modl) name @@ -442,20 +422,18 @@ fun succeed some (_, modl) = (some, modl); -fun fail msg (_, modl) = raise FAIL ([msg], NONE); +fun fail msg (_, modl) = raise FAIL [msg]; fun message msg f trns = - f trns handle FAIL (msgs, exc) => - raise FAIL (msg :: msgs, exc); + f trns handle FAIL msgs => + raise FAIL (msg :: msgs); fun start_transact init f modl = let fun handle_fail f x = (f x - handle FAIL (msgs, NONE) => + handle FAIL msgs => (error o cat_lines) ("Code generation failed, while:" :: msgs)) - handle FAIL (msgs, SOME e) => - ((Output.error_msg o cat_lines) ("Code generation failed, while:" :: msgs); raise e); in modl |> (if is_some init then ensure_bot (the init) else I)