tuned
authorhaftmann
Fri Oct 13 16:52:47 2006 +0200 (2006-10-13)
changeset 21012f08574148b7a
parent 21011 19d7f07b0fa3
child 21013 b9321724c2cc
tuned
src/HOL/Tools/datatype_codegen.ML
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_thingol.ML
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Oct 13 16:52:46 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Oct 13 16:52:47 2006 +0200
     1.3 @@ -336,8 +336,6 @@
     1.4      val abs = Name.names Name.context "a" (Library.drop (length ts, tys));
     1.5      val (ts', t) = split_last (ts @ map Free abs);
     1.6      val (tys', sty) = split_last tys;
     1.7 -    fun freenames_of t = fold_aterms
     1.8 -      (fn Free (v, _) => insert (op =) v | _ => I) t [];
     1.9      fun dest_case ((c, tys_decl), ty) t =
    1.10        let
    1.11          val (vs, t') = Term.strip_abs_eta (length tys_decl) t;
     2.1 --- a/src/Pure/Tools/codegen_package.ML	Fri Oct 13 16:52:46 2006 +0200
     2.2 +++ b/src/Pure/Tools/codegen_package.ML	Fri Oct 13 16:52:47 2006 +0200
     2.3 @@ -21,6 +21,8 @@
     2.4      -> ((string * typ) list * ((term * typ) * (term * term) list)) option)
     2.5      -> appgen;
     2.6    val appgen_let: appgen;
     2.7 +
     2.8 +  val timing: bool ref;
     2.9  end;
    2.10  
    2.11  structure CodegenPackage : CODEGEN_PACKAGE =
    2.12 @@ -173,6 +175,7 @@
    2.13              |-> (fn (tyco, tys) => pair (tyco `%% tys));
    2.14  
    2.15  exception CONSTRAIN of (string * typ) * typ;
    2.16 +val timing = ref false;
    2.17  
    2.18  fun exprgen_typinst thy (algbr as ((proj_sort, algebra), consts)) funcgr strct (ty_ctxt, sort_decl) trns =
    2.19    let
    2.20 @@ -271,6 +274,8 @@
    2.21          (perhaps (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy)) (c, tys))
    2.22         of eq_thms as eq_thm :: _ =>
    2.23              let
    2.24 +              val timeap = if !timing then Output.timeap_msg ("time for " ^ c')
    2.25 +                else I;
    2.26                val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms);
    2.27                val ty = (Logic.unvarifyT o CodegenData.typ_func thy) eq_thm;
    2.28                val vs = (map dest_TFree o Consts.typargs consts) (c', ty);
    2.29 @@ -283,7 +288,7 @@
    2.30              in
    2.31                trns
    2.32                |> CodegenThingol.message msg (fn trns => trns
    2.33 -              |> fold_map (exprgen_eq o dest_eqthm) eq_thms
    2.34 +              |> timeap (fold_map (exprgen_eq o dest_eqthm) eq_thms)
    2.35                ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
    2.36                ||>> exprgen_type thy algbr funcgr strct ty
    2.37                |-> (fn ((eqs, vs), ty) => succeed (CodegenThingol.Fun (eqs, (vs, ty)))))
    2.38 @@ -397,8 +402,7 @@
    2.39    case try (int_of_numeral thy) (list_comb (Const c, ts))
    2.40     of SOME i =>
    2.41          trns
    2.42 -        |> appgen_default thy algbr funcgr strct app
    2.43 -        |-> (fn t => pair (CodegenThingol.INum (i, t)))
    2.44 +        |> pair (CodegenThingol.INum i)
    2.45      | NONE =>
    2.46          trns
    2.47          |> appgen_default thy algbr funcgr strct app;
    2.48 @@ -408,14 +412,16 @@
    2.49     of SOME i =>
    2.50          trns
    2.51          |> exprgen_type thy algbr funcgr strct ty
    2.52 -        ||>> appgen_default thy algbr funcgr strct app
    2.53 -        |-> (fn (_, t0) => pair (IChar (chr i, t0)))
    2.54 +        |-> (fn _ => pair (IChar (chr i)))
    2.55      | NONE =>
    2.56          trns
    2.57          |> appgen_default thy algbr funcgr strct app;
    2.58  
    2.59 +val debug_term = ref (Bound 0);
    2.60 +
    2.61  fun appgen_case dest_case_expr thy algbr funcgr strct (app as (c_ty, ts)) trns =
    2.62    let
    2.63 +    val _ = debug_term := list_comb (Const c_ty, ts);
    2.64      val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
    2.65      fun fold_map_aterms f (t $ u) s =
    2.66            s
    2.67 @@ -427,16 +433,23 @@
    2.68            |> fold_map_aterms f t
    2.69            |-> (fn t' => pair (Abs (v, ty, t')))
    2.70        | fold_map_aterms f a s = f a s;
    2.71 -    fun purify_term_frees (Free (v, ty)) ctxt = 
    2.72 +    fun purify_term_frees (Free (v, ty)) (renaming, ctxt) = 
    2.73            let
    2.74              val ([v'], ctxt') = Name.variants [CodegenNames.purify_var v] ctxt;
    2.75 -          in (Free (v, ty), ctxt') end
    2.76 +            val renaming' = if v <> v' then Symtab.update (v, v') renaming else renaming;
    2.77 +          in (Free (v', ty), (renaming', ctxt')) end
    2.78        | purify_term_frees t ctxt = (t, ctxt);
    2.79      fun clausegen (raw_dt, raw_bt) trns =
    2.80        let
    2.81 -        val ((dt, bt), _) = Name.context
    2.82 -          |> fold_map_aterms purify_term_frees raw_dt
    2.83 -          ||>> fold_map_aterms purify_term_frees raw_bt;
    2.84 +        val d_vs = map fst (Term.add_frees raw_dt []);
    2.85 +        val b_vs = map fst (Term.add_frees raw_bt []);
    2.86 +        val (dt, (renaming, ctxt)) =
    2.87 +          Name.context
    2.88 +          |> fold Name.declare (subtract (op =) d_vs b_vs)
    2.89 +          |> pair Symtab.empty
    2.90 +          |> fold_map_aterms purify_term_frees raw_dt;
    2.91 +        val bt = map_aterms (fn t as Free (v, ty) => Free (perhaps (Symtab.lookup renaming) v, ty)
    2.92 +                              | t => t) raw_bt;
    2.93        in
    2.94          trns
    2.95          |> exprgen_term thy algbr funcgr strct dt
    2.96 @@ -447,21 +460,19 @@
    2.97      |> exprgen_term thy algbr funcgr strct st
    2.98      ||>> exprgen_type thy algbr funcgr strct sty
    2.99      ||>> fold_map clausegen ds
   2.100 -    ||>> appgen_default thy algbr funcgr strct app
   2.101 -    |-> (fn (((se, sty), ds), e0) => pair (ICase (((se, sty), ds), e0)))
   2.102 +    |-> (fn ((se, sty), ds) => pair (ICase ((se, sty), ds)))
   2.103    end;
   2.104  
   2.105  fun appgen_let thy algbr funcgr strct (app as (_, [st, ct])) trns =
   2.106    trns
   2.107    |> exprgen_term thy algbr funcgr strct ct
   2.108    ||>> exprgen_term thy algbr funcgr strct st
   2.109 -  ||>> appgen_default thy algbr funcgr strct app
   2.110 -  |-> (fn (((v, ty) `|-> be, se), e0) =>
   2.111 -            pair (ICase (((se, ty), case be
   2.112 -              of ICase (((IVar w, _), ds), _) => if v = w then ds else [(IVar v, be)]
   2.113 +  |-> (fn ((v, ty) `|-> be, se) =>
   2.114 +            pair (ICase ((se, ty), case be
   2.115 +              of ICase ((IVar w, _), ds) => if v = w then ds else [(IVar v, be)]
   2.116                 | _ => [(IVar v, be)]
   2.117 -            ), e0))
   2.118 -        | (_, e0) => pair e0);
   2.119 +            ))
   2.120 +        | _ => appgen_default thy algbr funcgr strct app);
   2.121  
   2.122  fun add_appconst (c, appgen) thy =
   2.123    let
   2.124 @@ -630,7 +641,7 @@
   2.125       of [] => NONE
   2.126        | xs => SOME xs;
   2.127      val seris' = map_filter (fn (target, args as _ :: _) =>
   2.128 -      SOME (CodegenSerializer.get_serializer thy (target, args)) | _ => NONE) seris;
   2.129 +      SOME (CodegenSerializer.get_serializer thy target args) | _ => NONE) seris;
   2.130      fun generate' thy = case cs
   2.131       of [] => []
   2.132        | _ =>
     3.1 --- a/src/Pure/Tools/codegen_thingol.ML	Fri Oct 13 16:52:46 2006 +0200
     3.2 +++ b/src/Pure/Tools/codegen_thingol.ML	Fri Oct 13 16:52:47 2006 +0200
     3.3 @@ -28,12 +28,11 @@
     3.4      | IVar of vname
     3.5      | `$ of iterm * iterm
     3.6      | `|-> of (vname * itype) * iterm
     3.7 -    | INum of IntInf.int * iterm
     3.8 -    | IChar of string (*length one!*) * iterm
     3.9 -    | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
    3.10 -        (*((discriminendum term (td), discriminendum type (ty)),
    3.11 -                [(selector pattern (p), body term (t))] (bs)),
    3.12 -                pure term (t0))*)
    3.13 +    | INum of IntInf.int
    3.14 +    | IChar of string (*length one!*)
    3.15 +    | ICase of (iterm * itype) * (iterm * iterm) list;
    3.16 +        (*(discriminendum term (td), discriminendum type (ty)),
    3.17 +                [(selector pattern (p), body term (t))] (bs))*)
    3.18    val `--> : itype list * itype -> itype;
    3.19    val `$$ : iterm * iterm list -> iterm;
    3.20    val `|--> : (vname * itype) list * iterm -> iterm;
    3.21 @@ -47,11 +46,10 @@
    3.22    val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a;
    3.23    val unfold_fun: itype -> itype list * itype;
    3.24    val unfold_app: iterm -> iterm * iterm list;
    3.25 -  val unfold_abs: iterm -> (iterm * itype) list * iterm;
    3.26 +  val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm;
    3.27    val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
    3.28    val unfold_const_app: iterm ->
    3.29      ((string * (inst list list * itype)) * iterm list) option;
    3.30 -  val map_pure: (iterm -> 'a) -> iterm -> 'a;
    3.31    val eta_expand: (string * (inst list list * itype)) * iterm list -> int -> iterm;
    3.32    val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
    3.33    val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
    3.34 @@ -72,9 +70,10 @@
    3.35    val empty_code: code;
    3.36    val get_def: code -> string -> def;
    3.37    val merge_code: code * code -> code;
    3.38 -  val project_code: string list -> code -> code;
    3.39 +  val project_code: string list (*hidden*) -> string list option (*selected*)
    3.40 +    -> code -> code;
    3.41    val add_eval_def: string (*shallow name space*) * iterm -> code -> string * code;
    3.42 -  val delete_garbage: string list (*hidden definitions*) -> code -> code;
    3.43 +
    3.44  
    3.45    val ensure_def: (transact -> def * code) -> bool -> string
    3.46      -> string -> transact -> transact;
    3.47 @@ -85,7 +84,6 @@
    3.48  
    3.49    val trace: bool ref;
    3.50    val tracing: ('a -> string) -> 'a -> 'a;
    3.51 -  val soft_exc: bool ref;
    3.52  end;
    3.53  
    3.54  structure CodegenThingol: CODEGEN_THINGOL =
    3.55 @@ -95,7 +93,6 @@
    3.56  
    3.57  val trace = ref false;
    3.58  fun tracing f x = (if !trace then Output.tracing (f x) else (); x);
    3.59 -val soft_exc = ref true;
    3.60  
    3.61  fun unfoldl dest x =
    3.62    case dest x
    3.63 @@ -131,9 +128,9 @@
    3.64    | IVar of vname
    3.65    | `$ of iterm * iterm
    3.66    | `|-> of (vname * itype) * iterm
    3.67 -  | INum of IntInf.int * iterm
    3.68 -  | IChar of string * iterm
    3.69 -  | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
    3.70 +  | INum of IntInf.int
    3.71 +  | IChar of string
    3.72 +  | ICase of (iterm * itype) * (iterm * iterm) list;
    3.73      (*see also signature*)
    3.74  
    3.75  (*
    3.76 @@ -174,13 +171,13 @@
    3.77      | _ => NONE);
    3.78  
    3.79  val unfold_abs = unfoldr
    3.80 -  (fn (v, ty) `|-> (t as ICase (((IVar w, _), [(p, t')]), _)) =>
    3.81 -        if v = w then SOME ((p, ty), t') else SOME ((IVar v, ty), t)
    3.82 -    | (v, ty) `|-> t => SOME ((IVar v, ty), t)
    3.83 +  (fn (v, ty) `|-> (t as ICase ((IVar w, _), [(p, t')])) =>
    3.84 +        if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t)
    3.85 +    | (v, ty) `|-> t => SOME (((v, NONE), ty), t)
    3.86      | _ => NONE)
    3.87  
    3.88  val unfold_let = unfoldr
    3.89 -  (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
    3.90 +  (fn ICase ((td, ty), [(p, t)]) => SOME (((p, ty), td), t)
    3.91      | _ => NONE);
    3.92  
    3.93  fun unfold_const_app t =
    3.94 @@ -188,21 +185,6 @@
    3.95    of (IConst c, ts) => SOME (c, ts)
    3.96     | _ => NONE;
    3.97  
    3.98 -fun map_pure f (t as IConst _) =
    3.99 -      f t
   3.100 -  | map_pure f (t as IVar _) =
   3.101 -      f t
   3.102 -  | map_pure f (t as _ `$ _) =
   3.103 -      f t
   3.104 -  | map_pure f (t as _ `|-> _) =
   3.105 -      f t
   3.106 -  | map_pure f (INum (_, t0)) =
   3.107 -      f t0
   3.108 -  | map_pure f (IChar (_, t0)) =
   3.109 -      f t0
   3.110 -  | map_pure f (ICase (_, t0)) =
   3.111 -      f t0;
   3.112 -
   3.113  fun fold_aiterms f (t as IConst _) =
   3.114        f t
   3.115    | fold_aiterms f (t as IVar _) =
   3.116 @@ -211,12 +193,12 @@
   3.117        fold_aiterms f t1 #> fold_aiterms f t2
   3.118    | fold_aiterms f (t as _ `|-> t') =
   3.119        f t #> fold_aiterms f t'
   3.120 -  | fold_aiterms f (INum (_, t0)) =
   3.121 -      fold_aiterms f t0
   3.122 -  | fold_aiterms f (IChar (_, t0)) =
   3.123 -      fold_aiterms f t0
   3.124 -  | fold_aiterms f (ICase (_, t0)) =
   3.125 -      fold_aiterms f t0;
   3.126 +  | fold_aiterms f (t as INum _) =
   3.127 +      f t
   3.128 +  | fold_aiterms f (t as IChar _) =
   3.129 +      f t
   3.130 +  | fold_aiterms f (ICase ((td, _), bs)) =
   3.131 +      fold_aiterms f td #> fold (fn (p, t) => fold_aiterms f p #> fold_aiterms f t) bs;
   3.132  
   3.133  fun fold_constnames f =
   3.134    let
   3.135 @@ -241,12 +223,12 @@
   3.136            add vs t1 #> add vs t2
   3.137        | add vs ((v, _) `|-> t) =
   3.138            add (insert (op =) v vs) t
   3.139 -      | add vs (INum (_, t)) =
   3.140 -          add vs t
   3.141 -      | add vs (IChar (_, t)) =
   3.142 -          add vs t
   3.143 -      | add vs (ICase (_, t0)) =
   3.144 -          add vs t0
   3.145 +      | add vs (INum _) =
   3.146 +          I
   3.147 +      | add vs (IChar _) =
   3.148 +          I
   3.149 +      | add vs (ICase ((td, _), bs)) =
   3.150 +          add vs td #> fold (fn (p, t) => add vs p #> add vs t) bs;
   3.151    in add [] end;
   3.152  
   3.153  fun eta_expand (c as (_, (_, ty)), ts) k =
   3.154 @@ -278,7 +260,7 @@
   3.155  
   3.156  type code = def Graph.T;
   3.157  type transact = Graph.key option * code;
   3.158 -exception FAIL of string list * exn option;
   3.159 +exception FAIL of string list;
   3.160  
   3.161  
   3.162  (* abstract code *)
   3.163 @@ -307,19 +289,24 @@
   3.164  
   3.165  val merge_code = Graph.join (fn _ => fn def12 => if eq_def def12 then fst def12 else Bot);
   3.166  
   3.167 -fun project_code names code =
   3.168 -  Graph.project (member (op =) (Graph.all_succs code names)) code;
   3.169 -
   3.170 -fun delete_garbage hidden code =
   3.171 +fun project_code hidden raw_selected code =
   3.172    let
   3.173      fun is_bot name = case get_def code name
   3.174       of Bot => true
   3.175        | _ => false;
   3.176      val names = subtract (op =) hidden (Graph.keys code);
   3.177 -    val names' = subtract (op =)
   3.178 -      (Graph.all_preds code (filter is_bot names)) names;
   3.179 +    val deleted = Graph.all_preds code (filter is_bot names);
   3.180 +    val selected = case raw_selected
   3.181 +     of NONE => names |> subtract (op =) deleted 
   3.182 +      | SOME sel => sel
   3.183 +          |> subtract (op =) deleted
   3.184 +          |> subtract (op =) hidden
   3.185 +          |> Graph.all_succs code
   3.186 +          |> subtract (op =) deleted
   3.187 +          |> subtract (op =) hidden;
   3.188    in
   3.189 -    Graph.project (member (op =) names') code
   3.190 +    code
   3.191 +    |> Graph.project (member (op =) selected)
   3.192    end;
   3.193  
   3.194  fun check_samemodule names =
   3.195 @@ -406,17 +393,10 @@
   3.196      fun prep_def def modl =
   3.197        (check_prep_def modl def, modl);
   3.198      fun invoke_generator name defgen modl =
   3.199 -      if ! soft_exc (*that "!" isn't a "not"...*)
   3.200 -      then defgen (SOME name, modl)
   3.201 -        handle FAIL (msgs, exc) =>
   3.202 -                if strict then raise FAIL (msg' :: msgs, exc)
   3.203 -                else (Bot, modl)
   3.204 -             | e => raise
   3.205 -                FAIL (["definition generator for " ^ quote name, msg'], SOME e)
   3.206 -      else defgen (SOME name, modl)
   3.207 -        handle FAIL (msgs, exc) =>
   3.208 -              if strict then raise FAIL (msg' :: msgs, exc)
   3.209 -              else (Bot, modl);
   3.210 +      defgen (SOME name, modl)
   3.211 +        handle FAIL msgs =>
   3.212 +          if strict then raise FAIL (msg' :: msgs)
   3.213 +          else (Bot, modl);
   3.214    in
   3.215      modl
   3.216      |> (if can (get_def modl) name
   3.217 @@ -442,20 +422,18 @@
   3.218  
   3.219  fun succeed some (_, modl) = (some, modl);
   3.220  
   3.221 -fun fail msg (_, modl) = raise FAIL ([msg], NONE);
   3.222 +fun fail msg (_, modl) = raise FAIL [msg];
   3.223  
   3.224  fun message msg f trns =
   3.225 -  f trns handle FAIL (msgs, exc) =>
   3.226 -    raise FAIL (msg :: msgs, exc);
   3.227 +  f trns handle FAIL msgs =>
   3.228 +    raise FAIL (msg :: msgs);
   3.229  
   3.230  fun start_transact init f modl =
   3.231    let
   3.232      fun handle_fail f x =
   3.233        (f x
   3.234 -      handle FAIL (msgs, NONE) =>
   3.235 +      handle FAIL msgs =>
   3.236          (error o cat_lines) ("Code generation failed, while:" :: msgs))
   3.237 -      handle FAIL (msgs, SOME e) =>
   3.238 -        ((Output.error_msg o cat_lines) ("Code generation failed, while:" :: msgs); raise e);
   3.239    in
   3.240      modl
   3.241      |> (if is_some init then ensure_bot (the init) else I)