substantial improvement in codegen iml
authorhaftmann
Tue Mar 07 14:09:48 2006 +0100 (2006-03-07)
changeset 192020b9eb4b0ad98
parent 19201 294448903a66
child 19203 778507520684
substantial improvement in codegen iml
src/HOL/Datatype.thy
src/HOL/Tools/recfun_codegen.ML
src/HOL/ex/nbe.thy
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/Tools/codegen_thingol.ML
src/Pure/Tools/nbe_codegen.ML
src/Pure/Tools/nbe_eval.ML
     1.1 --- a/src/HOL/Datatype.thy	Tue Mar 07 04:06:02 2006 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Tue Mar 07 14:09:48 2006 +0100
     1.3 @@ -246,6 +246,9 @@
     1.4    fst_conv [code]
     1.5    snd_conv [code]
     1.6  
     1.7 +lemma [code unfold]:
     1.8 +  "1 == Suc 0" by simp
     1.9 +
    1.10  code_generate True False Not "op &" "op |" If
    1.11  
    1.12  code_syntax_tyco bool
    1.13 @@ -311,9 +314,4 @@
    1.14      ml (target_atom "SOME")
    1.15      haskell (target_atom "Just")
    1.16  
    1.17 -code_syntax_const
    1.18 -  "1 :: nat"
    1.19 -    ml ("{*Suc 0*}")
    1.20 -    haskell ("{*Suc 0*}")
    1.21 -
    1.22  end
     2.1 --- a/src/HOL/Tools/recfun_codegen.ML	Tue Mar 07 04:06:02 2006 +0100
     2.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue Mar 07 14:09:48 2006 +0100
     2.3 @@ -9,7 +9,6 @@
     2.4  sig
     2.5    val add: string option -> attribute
     2.6    val del: attribute
     2.7 -  val get_rec_equations: theory -> string * typ -> (term list * term) list * typ
     2.8    val get_thm_equations: theory -> string * typ -> (thm list * typ) option
     2.9    val setup: theory -> theory
    2.10  end;
    2.11 @@ -81,19 +80,6 @@
    2.12               | SOME thyname => thyname)
    2.13         end);
    2.14  
    2.15 -fun get_rec_equations thy (s, T) =
    2.16 -  Symtab.lookup (CodegenData.get thy) s
    2.17 -  |> Option.map (fn thms => 
    2.18 -       List.filter (fn (thm, _) => is_instance thy T ((snd o const_of o prop_of) thm)) thms
    2.19 -       |> del_redundant thy [])
    2.20 -  |> Option.mapPartial (fn thms => if null thms then NONE else SOME thms)
    2.21 -  |> Option.map (fn thms =>
    2.22 -       (preprocess thy (map fst thms),
    2.23 -          (snd o const_of o prop_of o fst o hd) thms))
    2.24 -  |> the_default ([], dummyT)
    2.25 -  |> apfst (map prop_of)
    2.26 -  |> apfst (map (Codegen.rename_term #> HOLogic.dest_Trueprop #> HOLogic.dest_eq #> apfst (strip_comb #> snd)))
    2.27 -
    2.28  fun get_thm_equations thy (c, ty) =
    2.29    Symtab.lookup (CodegenData.get thy) c
    2.30    |> Option.map (fn thms => 
     3.1 --- a/src/HOL/ex/nbe.thy	Tue Mar 07 04:06:02 2006 +0100
     3.2 +++ b/src/HOL/ex/nbe.thy	Tue Mar 07 14:09:48 2006 +0100
     3.3 @@ -6,15 +6,16 @@
     3.4  theory nbe
     3.5  imports Main
     3.6  begin
     3.7 +
     3.8  ML"reset quick_and_dirty"
     3.9  
    3.10  declare disj_assoc[code]
    3.11  
    3.12  norm_by_eval "(P | Q) | R"
    3.13  
    3.14 -lemma[code]: "(P \<longrightarrow> P)=True" by blast
    3.15 +(*lemma[code]: "(P \<longrightarrow> P) = True" by blast
    3.16  norm_by_eval "P \<longrightarrow> P"
    3.17 -norm_by_eval "True \<longrightarrow> P"
    3.18 +norm_by_eval "True \<longrightarrow> P"*)
    3.19  
    3.20  
    3.21  datatype n = Z | S n
    3.22 @@ -52,7 +53,6 @@
    3.23  "exp m Z = S Z"
    3.24  "exp m (S n) = mul (exp m n) m"
    3.25  
    3.26 -
    3.27  norm_by_eval "mul2 (S(S(S(S(S(S(S Z))))))) (S(S(S(S(S Z)))))"
    3.28  norm_by_eval "mul (S(S(S(S(S(S(S Z))))))) (S(S(S(S(S Z)))))"
    3.29  norm_by_eval "exp (S(S(S(S(S(S(S Z))))))) (S(S(S(S(S Z)))))"
    3.30 @@ -94,16 +94,21 @@
    3.31  norm_by_eval "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()]"
    3.32  norm_by_eval "rev [a, b, c]"
    3.33  
    3.34 -end
    3.35 -
    3.36 -(*
    3.37 -ML"set Toplevel.debug"
    3.38  norm_by_eval "case n of None \<Rightarrow> True | Some((x,y),(u,v)) \<Rightarrow> False"
    3.39  norm_by_eval "let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)"
    3.40  norm_by_eval "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z))"
    3.41 -*)
    3.42 -(* to be done
    3.43 -norm_by_eval "max 0 (0::nat)"
    3.44  norm_by_eval "last[a,b,c]"
    3.45 - Numerals! *)
    3.46 +
    3.47 +text {*
    3.48 +  won't work since it relies on 
    3.49 +  polymorphically used ad-hoc overloaded function:
    3.50 +  norm_by_eval "max 0 (0::nat)"
    3.51 +*}
    3.52  
    3.53 +text {*
    3.54 +  Numerals still take their time\<dots>
    3.55 +*}
    3.56 +
    3.57 +end
    3.58 +
    3.59 +
     4.1 --- a/src/Pure/Tools/codegen_package.ML	Tue Mar 07 04:06:02 2006 +0100
     4.2 +++ b/src/Pure/Tools/codegen_package.ML	Tue Mar 07 14:09:48 2006 +0100
     4.3 @@ -138,7 +138,7 @@
     4.4    andalso Sign.typ_instance thy (ty2, ty1);
     4.5  
     4.6  fun is_overloaded thy c = case Defs.specifications_of (Theory.defs_of thy) c
     4.7 - of [] => false
     4.8 + of [] => true
     4.9    | [(ty, _)] => not (eq_typ thy (ty, Sign.the_const_type thy c))
    4.10    | _ => true;
    4.11  
    4.12 @@ -161,10 +161,17 @@
    4.13    fun mk thy ((c, ty), i) =
    4.14      let
    4.15        val c' = idf_of_name thy nsp_overl c;
    4.16 -      val prefix = case (AList.lookup (eq_typ thy)
    4.17 -          (Defs.specifications_of (Theory.defs_of thy) c)) ty
    4.18 -       of SOME thyname => NameSpace.append thyname nsp_overl
    4.19 -        | NONE => NameSpace.drop_base c';
    4.20 +      val prefix = 
    4.21 +        case (AList.lookup (eq_typ thy)
    4.22 +            (Defs.specifications_of (Theory.defs_of thy) c)) ty
    4.23 +         of SOME thyname => NameSpace.append thyname nsp_overl
    4.24 +          | NONE => if c = "op ="
    4.25 +              then
    4.26 +                NameSpace.append
    4.27 +                  (((fn s => Codegen.thyname_of_type s thy) o fst o dest_Type o hd o fst o strip_type) ty)
    4.28 +                  nsp_overl
    4.29 +              else
    4.30 +                NameSpace.drop_base c';
    4.31        val c'' = NameSpace.append prefix (NameSpace.base c');
    4.32        fun mangle (Type (tyco, tys)) =
    4.33              (NameSpace.base o alias_get thy) tyco :: Library.flat (List.mapPartial mangle tys) |> SOME
    4.34 @@ -399,13 +406,13 @@
    4.35        (c, ty) =
    4.36    let
    4.37      fun get_overloaded (c, ty) =
    4.38 -      case Symtab.lookup overltab1 c
    4.39 +      (case Symtab.lookup overltab1 c
    4.40         of SOME tys =>
    4.41              (case find_first (curry (Sign.typ_instance thy) ty) tys
    4.42               of SOME ty' => ConstNameMangler.get thy overltab2
    4.43                    (c, ty') |> SOME
    4.44                | _ => NONE)
    4.45 -        | _ => NONE
    4.46 +        | _ => NONE)
    4.47      fun get_datatypecons (c, ty) =
    4.48        case (snd o strip_type) ty
    4.49         of Type (tyco, _) =>
    4.50 @@ -851,12 +858,12 @@
    4.51  and appgen_default thy tabs ((c, ty), ts) trns =
    4.52    trns
    4.53    |> ensure_def_const thy tabs (c, ty)
    4.54 +  ||>> exprsgen_type thy tabs [ty]
    4.55    ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
    4.56           (ClassPackage.extract_classlookup thy (c, ty))
    4.57 -  ||>> exprsgen_type thy tabs [ty]
    4.58    ||>> fold_map (exprgen_term thy tabs) ts
    4.59 -  |-> (fn (((c, ls), [ty]), es) =>
    4.60 -         pair (IConst ((c, ty), ls) `$$ es))
    4.61 +  |-> (fn (((c, [ty]), ls), es) =>
    4.62 +         pair (IConst (c, (ls, ty)) `$$ es))
    4.63  and appgen thy tabs ((f, ty), ts) trns =
    4.64    case Symtab.lookup ((#appconst o #gens o CodegenData.get) thy) f
    4.65     of SOME ((imin, imax), (ag, _)) =>
    4.66 @@ -899,43 +906,48 @@
    4.67  
    4.68  (* parametrized generators, for instantiation in HOL *)
    4.69  
    4.70 -fun appgen_let strip_abs thy tabs (app as ((c, ty), [dt, ct])) trns =
    4.71 -  let
    4.72 -    val ([st], bt) = strip_abs 1 ct;
    4.73 -    val dtyp = (hd o fst o strip_type) ty
    4.74 -  in
    4.75 -    trns
    4.76 -    |> exprgen_term thy tabs dt
    4.77 -    ||>> exprgen_type thy tabs dtyp
    4.78 -    ||>> exprgen_term thy tabs st
    4.79 -    ||>> exprgen_term thy tabs bt
    4.80 -    ||>> appgen_default thy tabs app
    4.81 -    |-> (fn ((((de, dty), se), be), e0) => pair (ICase (((de, dty), [(se, be)]), e0)))
    4.82 -  end;
    4.83 -
    4.84 -fun appgen_split strip_abs thy tabs (app as (c as (_, ty), [t])) trns =
    4.85 +fun appgen_split strip_abs thy tabs (app as (c, [t])) trns =
    4.86    case strip_abs 1 (Const c $ t)
    4.87 -   of ([vt], tb) =>
    4.88 +   of ([vt], bt) =>
    4.89          trns
    4.90          |> exprgen_term thy tabs vt
    4.91 -        ||>> exprgen_type thy tabs (((fn [_, ty] => ty) o fst o strip_type) ty)
    4.92 -        ||>> exprgen_term thy tabs tb
    4.93 +        ||>> exprgen_type thy tabs (type_of vt)
    4.94 +        ||>> exprgen_term thy tabs bt
    4.95          ||>> appgen_default thy tabs app
    4.96          |-> (fn (((ve, vty), be), e0) => pair (IAbs (((ve, vty), be), e0)))
    4.97      | _ =>
    4.98          trns
    4.99          |> appgen_default thy tabs app;
   4.100  
   4.101 +fun appgen_let strip_abs thy tabs (app as ((c, ty), [dt, ct])) trns =
   4.102 +  case strip_abs 1 ct
   4.103 +   of ([st], bt) =>
   4.104 +        trns
   4.105 +        |> exprgen_term thy tabs dt
   4.106 +        ||>> exprgen_type thy tabs (type_of dt)
   4.107 +        ||>> exprgen_term thy tabs st
   4.108 +        ||>> exprgen_term thy tabs bt
   4.109 +        ||>> appgen_default thy tabs app
   4.110 +        |-> (fn ((((de, dty), se), be), e0) => pair (ICase (((de, dty), [(se, be)]), e0)))
   4.111 +    | _ =>
   4.112 +        trns
   4.113 +        |> appgen_default thy tabs app;
   4.114 +
   4.115  fun appgen_number_of mk_int_to_nat bin_to_int tyco_int tyco_nat thy tabs ((_,
   4.116    Type (_, [_, ty as Type (tyco, [])])), [bin]) trns =
   4.117 -    if tyco = tyco_int then
   4.118 +    if tyco = tyco_nat then
   4.119        trns
   4.120 -      |> exprgen_type thy tabs ty
   4.121 -      |-> (fn ty => pair (CodegenThingol.IConst (((IntInf.toString o bin_to_int thy) bin, ty), [])))
   4.122 -    else if tyco = tyco_nat then
   4.123 -      trns
   4.124 -      |> exprgen_term thy tabs (mk_int_to_nat bin)
   4.125 -    else error ("invalid type constructor for numeral: " ^ quote tyco);
   4.126 +      |> exprgen_term thy tabs (mk_int_to_nat bin) (*should be a preprocessor's work*)
   4.127 +    else
   4.128 +      let
   4.129 +        val i = bin_to_int thy bin;
   4.130 +        val _ = if i < 0 then error ("negative numeral: " ^ IntInf.toString i) else ();
   4.131 +          (*should be a preprocessor's work*)
   4.132 +      in
   4.133 +        trns
   4.134 +        |> exprgen_type thy tabs ty
   4.135 +        |-> (fn ty => pair (CodegenThingol.INum ((i, ty), ())))
   4.136 +      end;
   4.137  
   4.138  fun appgen_wfrec thy tabs ((c, ty), [_, tf, tx]) trns =
   4.139    let
   4.140 @@ -951,25 +963,7 @@
   4.141      ||>> exprsgen_type thy tabs [ty_def]
   4.142      ||>> exprgen_term thy tabs tf
   4.143      ||>> exprgen_term thy tabs tx
   4.144 -    |-> (fn ((((_, ls), [ty]), tf), tx) => pair (IConst ((idf, ty), ls) `$ tf `$ tx))
   4.145 -  end;
   4.146 -
   4.147 -
   4.148 -fun appgen_wfrec thy tabs ((c, ty), [_, tf, tx]) trns =
   4.149 -  let
   4.150 -    val ty_def = (op ---> o apfst tl o strip_type o Sign.the_const_type thy) c;
   4.151 -    val ty' = (op ---> o apfst tl o strip_type) ty;
   4.152 -    val idf = idf_of_const thy tabs (c, ty);
   4.153 -  in
   4.154 -    trns
   4.155 -    |> ensure_def [("wfrec", (K o succeed) Undef)] ("generating wfrec") idf
   4.156 -    |> exprgen_type thy tabs ty'
   4.157 -    ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
   4.158 -           (ClassPackage.extract_classlookup thy (c, ty))
   4.159 -    ||>> exprsgen_type thy tabs [ty_def]
   4.160 -    ||>> exprgen_term thy tabs tf
   4.161 -    ||>> exprgen_term thy tabs tx
   4.162 -    |-> (fn ((((_, ls), [ty]), tf), tx) => pair (IConst ((idf, ty), ls) `$ tf `$ tx))
   4.163 +    |-> (fn ((((_, ls), [ty]), tf), tx) => pair (IConst (idf, (ls, ty)) `$ tf `$ tx))
   4.164    end;
   4.165  
   4.166  fun eqextr_eq f fals thy tabs ("op =", ty) =
     5.1 --- a/src/Pure/Tools/codegen_serializer.ML	Tue Mar 07 04:06:02 2006 +0100
     5.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Tue Mar 07 14:09:48 2006 +0100
     5.3 @@ -314,6 +314,19 @@
     5.4      |> postprocess_module name
     5.5    end;
     5.6  
     5.7 +fun constructive_fun (name, (eqs, ty)) =
     5.8 +  let
     5.9 +    fun check_eq (eq as (lhs, rhs)) =
    5.10 +      if forall CodegenThingol.is_pat lhs
    5.11 +      then SOME eq
    5.12 +      else (warning ("in function " ^ quote name ^ ", throwing away one "
    5.13 +        ^ "non-executable function clause"); NONE)
    5.14 +  in case List.mapPartial check_eq eqs
    5.15 +   of [] => error ("in function " ^ quote name ^ ", no"
    5.16 +        ^ "executable function clauses found")
    5.17 +    | eqs => (name, (eqs, ty))
    5.18 +  end;
    5.19 +
    5.20  fun parse_single_file serializer =
    5.21    OuterParse.path
    5.22    >> (fn path => serializer
    5.23 @@ -336,7 +349,7 @@
    5.24  
    5.25  fun pretty_list thingol_nil thingol_cons (target_pred, target_cons) =
    5.26    let
    5.27 -    fun dest_cons (IConst ((c, _), _) `$ e1 `$ e2) =
    5.28 +    fun dest_cons (IConst (c, _) `$ e1 `$ e2) =
    5.29            if c = thingol_cons
    5.30            then SOME (e1, e2)
    5.31            else NONE
    5.32 @@ -349,7 +362,7 @@
    5.33        ];
    5.34      fun pretty_compact fxy pr [e1, e2] =
    5.35        case CodegenThingol.unfoldr dest_cons e2
    5.36 -       of (es, IConst ((c, _), _)) =>
    5.37 +       of (es, IConst (c, _)) =>
    5.38              if c = thingol_nil
    5.39              then Pretty.enum "," "[" "]" (map (pr NOBR) (e1::es))
    5.40              else pretty_default fxy pr e1 e2
    5.41 @@ -445,17 +458,15 @@
    5.42            end
    5.43        | ml_from_type fxy (ITyVar v) =
    5.44            str ("'" ^ v);
    5.45 -    fun typify trans ty p =
    5.46 +    fun typify ty p =
    5.47        let
    5.48          fun needs_type_t (tyco `%% tys) =
    5.49              needs_type tyco
    5.50 -            orelse trans
    5.51 -              andalso exists needs_type_t tys
    5.52 +            orelse exists needs_type_t tys
    5.53          | needs_type_t (ITyVar _) =
    5.54              false
    5.55          | needs_type_t (ty1 `-> ty2) =
    5.56 -            trans
    5.57 -            andalso (needs_type_t ty1 orelse needs_type_t ty2);
    5.58 +            needs_type_t ty1 orelse needs_type_t ty2;
    5.59        in if needs_type_t ty
    5.60          then
    5.61            Pretty.enclose "(" ")" [
    5.62 @@ -480,14 +491,20 @@
    5.63        | ml_from_expr fxy ((v, ty) `|-> e) =
    5.64            brackify BR [
    5.65              str "fn",
    5.66 -            typify true ty (str v),
    5.67 +            typify ty (str v),
    5.68              str "=>",
    5.69              ml_from_expr NOBR e
    5.70            ]
    5.71 +      | ml_from_expr fxy (INum ((n, ty), _)) =
    5.72 +          Pretty.enclose "(" ")" [
    5.73 +            (str o IntInf.toString) n,
    5.74 +            str ":",
    5.75 +            ml_from_type NOBR ty
    5.76 +          ]
    5.77        | ml_from_expr fxy (IAbs (((ve, vty), be), _)) =
    5.78            brackify BR [
    5.79              str "fn",
    5.80 -            typify true vty (ml_from_expr NOBR ve),
    5.81 +            typify vty (ml_from_expr NOBR ve),
    5.82              str "=>",
    5.83              ml_from_expr NOBR be
    5.84            ]
    5.85 @@ -497,7 +514,7 @@
    5.86              fun mk_val ((ve, vty), se) = Pretty.block [
    5.87                  (Pretty.block o Pretty.breaks) [
    5.88                    str "val",
    5.89 -                  typify true vty (ml_from_expr NOBR ve),
    5.90 +                  typify vty (ml_from_expr NOBR ve),
    5.91                    str "=",
    5.92                    ml_from_expr NOBR se
    5.93                  ],
    5.94 @@ -519,7 +536,7 @@
    5.95                ]
    5.96            in brackify fxy (
    5.97              str "case"
    5.98 -            :: typify true dty (ml_from_expr NOBR de)
    5.99 +            :: typify dty (ml_from_expr NOBR de)
   5.100              :: mk_clause "of" bse
   5.101              :: map (mk_clause "|") bses
   5.102            ) end
   5.103 @@ -530,11 +547,10 @@
   5.104          [(str o resolv) f, Pretty.enum "," "(" ")" (map (ml_from_expr BR) es)]
   5.105        else
   5.106          (str o resolv) f :: map (ml_from_expr BR) es
   5.107 -    and ml_from_app fxy (((c, ty), lss), es) =
   5.108 +    and ml_from_app fxy ((c, (lss, ty)), es) =
   5.109        case map (ml_from_sortlookup BR) lss
   5.110         of [] =>
   5.111              from_app ml_mk_app ml_from_expr const_syntax fxy ((c, ty), es)
   5.112 -            |> typify false ty
   5.113          | lss =>
   5.114              brackify fxy (
   5.115                (str o resolv) c
   5.116 @@ -581,7 +597,7 @@
   5.117                map (Pretty.block o single o Pretty.block o single);
   5.118              fun mk_arg e ty =
   5.119                ml_from_expr BR e
   5.120 -              |> typify true ty
   5.121 +              |> typify ty
   5.122              fun mk_eq definer (pats, expr) =
   5.123                (Pretty.block o Pretty.breaks) (
   5.124                  [str definer, (str o resolv) name]
   5.125 @@ -601,8 +617,8 @@
   5.126            end;
   5.127        in
   5.128          chunk_defs (
   5.129 -          mk_fun (the (fold check_args defs NONE)) def
   5.130 -          :: map (mk_fun "and") defs_tl
   5.131 +          (mk_fun (the (fold check_args defs NONE)) o constructive_fun) def
   5.132 +          :: map (mk_fun "and" o constructive_fun) defs_tl
   5.133          )
   5.134        end;
   5.135      fun ml_from_datatypes (defs as (def::defs_tl)) =
   5.136 @@ -912,6 +928,8 @@
   5.137                hs_from_expr NOBR e
   5.138              ])
   5.139            end
   5.140 +      | hs_from_expr fxy (INum ((n, _), _)) =
   5.141 +          (str o IntInf.toString) n
   5.142        | hs_from_expr fxy (e as IAbs _) =
   5.143            let
   5.144              val (es, e) = CodegenThingol.unfold_abs e
   5.145 @@ -954,11 +972,11 @@
   5.146            ] end
   5.147      and hs_mk_app c es =
   5.148        (str o resolv) c :: map (hs_from_expr BR) es
   5.149 -    and hs_from_app fxy (((c, ty), ls), es) =
   5.150 +    and hs_from_app fxy ((c, (ty, ls)), es) =
   5.151        from_app hs_mk_app hs_from_expr const_syntax fxy ((c, ty), es);
   5.152 -    fun hs_from_funeqs (name, eqs) =
   5.153 +    fun hs_from_funeqs (def as (name, _)) =
   5.154        let
   5.155 -        fun from_eq name (args, rhs) =
   5.156 +        fun from_eq (args, rhs) =
   5.157            Pretty.block [
   5.158              (str o resolv_here) name,
   5.159              Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, hs_from_expr BR p]) args),
   5.160 @@ -967,14 +985,14 @@
   5.161              Pretty.brk 1,
   5.162              hs_from_expr NOBR rhs
   5.163            ]
   5.164 -      in Pretty.chunks (map (from_eq name) eqs) end;
   5.165 +      in Pretty.chunks ((map from_eq o fst o snd o constructive_fun) def) end;
   5.166      fun hs_from_def (name, CodegenThingol.Undef) =
   5.167            error ("empty statement during serialization: " ^ quote name)
   5.168        | hs_from_def (name, CodegenThingol.Prim prim) =
   5.169            from_prim resolv_here (name, prim)
   5.170 -      | hs_from_def (name, CodegenThingol.Fun (eqs, (sctxt, ty))) =
   5.171 +      | hs_from_def (name, CodegenThingol.Fun (def as (_, (sctxt, ty)))) =
   5.172            let
   5.173 -            val body = hs_from_funeqs (name, eqs);
   5.174 +            val body = hs_from_funeqs (name, def);
   5.175            in if with_typs then
   5.176              Pretty.chunks [
   5.177                Pretty.block [
   5.178 @@ -1042,7 +1060,7 @@
   5.179              hs_from_sctxt_tycoexpr (arity, (tyco, map (ITyVar o fst) arity)),
   5.180              str " where",
   5.181              Pretty.fbrk,
   5.182 -            Pretty.chunks (map (fn (m, (_, (eqs, _))) => hs_from_funeqs (m, eqs)) memdefs)
   5.183 +            Pretty.chunks (map (fn (m, (_, (eqs, ty))) => hs_from_funeqs (m, (eqs, ty))) memdefs)
   5.184            ] |> SOME
   5.185    in
   5.186      case List.mapPartial (fn (name, def) => hs_from_def (name, def)) defs
     6.1 --- a/src/Pure/Tools/codegen_thingol.ML	Tue Mar 07 04:06:02 2006 +0100
     6.2 +++ b/src/Pure/Tools/codegen_thingol.ML	Tue Mar 07 14:09:48 2006 +0100
     6.3 @@ -24,10 +24,11 @@
     6.4      | `-> of itype * itype
     6.5      | ITyVar of vname;
     6.6    datatype iexpr =
     6.7 -      IConst of (string * itype) * iclasslookup list list
     6.8 +      IConst of string * (iclasslookup list list * itype)
     6.9      | IVar of vname
    6.10      | `$ of iexpr * iexpr
    6.11      | `|-> of (vname * itype) * iexpr
    6.12 +    | INum of (IntInf.int (*positive!*) * itype) * unit
    6.13      | IAbs of ((iexpr * itype) * iexpr) * iexpr
    6.14          (* (((binding expression (ve), binding type (vty)),
    6.15                  body expression (be)), native expression (e0)) *)
    6.16 @@ -52,8 +53,11 @@
    6.17    val unfold_abs: iexpr -> (iexpr * itype) list * iexpr;
    6.18    val unfold_let: iexpr -> ((iexpr * itype) * iexpr) list * iexpr;
    6.19    val unfold_const_app: iexpr ->
    6.20 -    (((string * itype) * iclasslookup list list) * iexpr list) option;
    6.21 -  val ensure_pat: iexpr -> iexpr;
    6.22 +    ((string * (iclasslookup list list * itype)) * iexpr list) option;
    6.23 +  val add_constnames: iexpr -> string list -> string list;
    6.24 +  val add_varnames: iexpr -> string list -> string list;
    6.25 +  val is_pat: iexpr -> bool;
    6.26 +  val map_pure: (iexpr -> 'a) -> iexpr -> 'a;
    6.27  
    6.28    type funn = (iexpr list * iexpr) list * (sortcontext * itype);
    6.29    type datatyp = sortcontext * (string * itype list) list;
    6.30 @@ -161,10 +165,11 @@
    6.31    | ITyVar of vname;
    6.32  
    6.33  datatype iexpr =
    6.34 -    IConst of (string * itype) * iclasslookup list list
    6.35 +    IConst of string * (iclasslookup list list * itype)
    6.36    | IVar of vname
    6.37    | `$ of iexpr * iexpr
    6.38    | `|-> of (vname * itype) * iexpr
    6.39 +  | INum of (IntInf.int (*positive!*) * itype) * unit
    6.40    | IAbs of ((iexpr * itype) * iexpr) * iexpr
    6.41    | ICase of ((iexpr * itype) * (iexpr * iexpr) list) * iexpr;
    6.42      (*see also signature*)
    6.43 @@ -208,7 +213,7 @@
    6.44    | pretty_itype (ITyVar v) =
    6.45        Pretty.str v;
    6.46  
    6.47 -fun pretty_iexpr (IConst ((c, _), _)) =
    6.48 +fun pretty_iexpr (IConst (c, _)) =
    6.49        Pretty.str c
    6.50    | pretty_iexpr (IVar v) =
    6.51        Pretty.str ("?" ^ v)
    6.52 @@ -218,6 +223,8 @@
    6.53    | pretty_iexpr ((v, ty) `|-> e) =
    6.54        (Pretty.enclose "(" ")" o Pretty.breaks)
    6.55          [Pretty.str v, Pretty.str "::", pretty_itype ty, Pretty.str "|->", pretty_iexpr e]
    6.56 +  | pretty_iexpr (INum ((n, _), _)) =
    6.57 +      (Pretty.str o IntInf.toString) n
    6.58    | pretty_iexpr (IAbs (((e1, _), e2), _)) =
    6.59        (Pretty.enclose "(" ")" o Pretty.breaks)
    6.60          [pretty_iexpr e1, Pretty.str "|->", pretty_iexpr e2]
    6.61 @@ -271,6 +278,8 @@
    6.62        f e1 `$ f e2
    6.63    | map_iexpr f ((v, ty) `|-> e) =
    6.64        (v, ty) `|-> f e
    6.65 +  | map_iexpr _ (e as INum _) =
    6.66 +      e
    6.67    | map_iexpr f (IAbs (((ve, vty), be), e0)) =
    6.68        IAbs (((f ve, vty), f be), e0)
    6.69    | map_iexpr f (ICase (((de, dty), bses), e0)) =
    6.70 @@ -278,8 +287,8 @@
    6.71  
    6.72  fun map_iexpr_itype f =
    6.73    let
    6.74 -    fun mapp (IConst ((c, ty), sctxt)) = IConst ((c, f ty), sctxt)
    6.75 -      | mapp ((v, ty) `|-> e) = (v, f ty) `|-> mapp e
    6.76 +    fun mapp ((v, ty) `|-> e) = (v, f ty) `|-> mapp e
    6.77 +      | mapp (INum ((n, ty), e)) = INum ((n, f ty), e)
    6.78        | mapp (IAbs (((ve, vty), be), e0)) =
    6.79            IAbs (((mapp ve, f vty), mapp be), e0)
    6.80        | mapp (ICase (((de, dty), bses), e0)) =
    6.81 @@ -321,12 +330,27 @@
    6.82        | instant y = map_itype instant y;
    6.83    in map_itype instant end;
    6.84  
    6.85 -fun ensure_pat (e as IConst (_, [])) = e
    6.86 -  | ensure_pat (e as IVar _) = e
    6.87 -  | ensure_pat (e as (e1 `$ e2)) =
    6.88 -      (ensure_pat e1; ensure_pat e2; e)
    6.89 -  | ensure_pat e =
    6.90 -      error ("illegal expression for pattern: " ^ (Pretty.output o pretty_iexpr) e);
    6.91 +fun is_pat (e as IConst (_, ([], _))) = true
    6.92 +  | is_pat (e as IVar _) = true
    6.93 +  | is_pat (e as (e1 `$ e2)) =
    6.94 +      is_pat e1 andalso is_pat e2
    6.95 +  | is_pat (e as INum _) = true
    6.96 +  | is_pat e = false;
    6.97 +
    6.98 +fun map_pure f (e as IConst _) =
    6.99 +      f e
   6.100 +  | map_pure f (e as IVar _) =
   6.101 +      f e
   6.102 +  | map_pure f (e as _ `$ _) =
   6.103 +      f e
   6.104 +  | map_pure f (e as _ `|-> _) =
   6.105 +      f e
   6.106 +  | map_pure _ (INum _) =
   6.107 +      error ("sorry, no pure representation of numerals so far")
   6.108 +  | map_pure f (IAbs (_, e0)) =
   6.109 +      f e0
   6.110 +  | map_pure f (ICase (_, e0)) =
   6.111 +      f e0;
   6.112  
   6.113  fun has_tyvars (_ `%% tys) =
   6.114        exists has_tyvars tys
   6.115 @@ -335,18 +359,35 @@
   6.116    | has_tyvars (ty1 `-> ty2) =
   6.117        has_tyvars ty1 orelse has_tyvars ty2;
   6.118  
   6.119 -fun varnames_of (IConst ((c, _), _)) =
   6.120 +fun add_constnames (IConst (c, _)) =
   6.121 +      insert (op =) c
   6.122 +  | add_constnames (IVar _) =
   6.123        I
   6.124 -  | varnames_of (IVar v) =
   6.125 +  | add_constnames (e1 `$ e2) =
   6.126 +      add_constnames e1 #> add_constnames e2
   6.127 +  | add_constnames (_ `|-> e) =
   6.128 +      add_constnames e
   6.129 +  | add_constnames (INum _) =
   6.130 +      I
   6.131 +  | add_constnames (IAbs (_, e)) =
   6.132 +      add_constnames e
   6.133 +  | add_constnames (ICase (_, e)) =
   6.134 +      add_constnames e;
   6.135 +
   6.136 +fun add_varnames (IConst _) =
   6.137 +      I
   6.138 +  | add_varnames (IVar v) =
   6.139        insert (op =) v
   6.140 -  | varnames_of (e1 `$ e2) =
   6.141 -      varnames_of e1 #> varnames_of e2
   6.142 -  | varnames_of ((v, _) `|-> e) =
   6.143 -      insert (op =) v #> varnames_of e
   6.144 -  | varnames_of (IAbs (((ve, _), be), _)) =
   6.145 -      varnames_of ve #> varnames_of be
   6.146 -  | varnames_of (ICase (((de, _), bses), _)) =
   6.147 -      varnames_of de #> fold (fn (be, se) => varnames_of be #> varnames_of se) bses;
   6.148 +  | add_varnames (e1 `$ e2) =
   6.149 +      add_varnames e1 #> add_varnames e2
   6.150 +  | add_varnames ((v, _) `|-> e) =
   6.151 +      insert (op =) v #> add_varnames e
   6.152 +  | add_varnames (INum _) =
   6.153 +      I
   6.154 +  | add_varnames (IAbs (((ve, _), be), _)) =
   6.155 +      add_varnames ve #> add_varnames be
   6.156 +  | add_varnames (ICase (((de, _), bses), _)) =
   6.157 +      add_varnames de #> fold (fn (be, se) => add_varnames be #> add_varnames se) bses;
   6.158  
   6.159  fun invent seed used =
   6.160    let
   6.161 @@ -884,17 +925,17 @@
   6.162    let
   6.163      fun eta e =
   6.164       case unfold_const_app e
   6.165 -      of SOME (((f, ty), ls), es) =>
   6.166 +      of SOME (const as (c, (_, ty)), es) =>
   6.167            let
   6.168 -            val delta = query f - length es;
   6.169 +            val delta = query c - length es;
   6.170              val add_n = if delta < 0 then 0 else delta;
   6.171              val tys =
   6.172                (fst o unfold_fun) ty
   6.173                |> curry Library.drop (length es)
   6.174                |> curry Library.take add_n
   6.175 -            val vs = (Term.invent_names (fold varnames_of es []) "x" add_n)
   6.176 +            val vs = (Term.invent_names (fold add_varnames es []) "x" add_n)
   6.177            in
   6.178 -            vs ~~ tys `|--> IConst ((f, ty), ls) `$$ map eta es `$$ map IVar vs
   6.179 +            vs ~~ tys `|--> IConst const `$$ map eta es `$$ map IVar vs
   6.180            end
   6.181         | NONE => map_iexpr eta e;
   6.182    in (map_defs o map_def_fun o map_def_fun_expr) eta end;
   6.183 @@ -908,7 +949,7 @@
   6.184            else (case unfold_abs e
   6.185             of ([], e) =>
   6.186                let
   6.187 -                val add_var = IVar (hd (Term.invent_names (varnames_of e []) "x" 1))
   6.188 +                val add_var = IVar (hd (Term.invent_names (add_varnames e []) "x" 1))
   6.189                in (([([add_var], e `$ add_var)], cty)) end
   6.190              | _ =>  funn)
   6.191        | eta funn = funn;
   6.192 @@ -919,7 +960,7 @@
   6.193      fun unclash (eqs, (sortctxt, ty)) =
   6.194        let
   6.195          val used_expr =
   6.196 -          fold (fn (pats, rhs) => fold varnames_of pats #> varnames_of rhs) eqs [];
   6.197 +          fold (fn (pats, rhs) => fold add_varnames pats #> add_varnames rhs) eqs [];
   6.198          val used_type = map fst sortctxt;
   6.199          val clash = gen_union (op =) (used_expr, used_type);
   6.200          val rename_map = fold_map (fn c => invent c #-> (fn c' => pair (c, c'))) clash [] |> fst;
     7.1 --- a/src/Pure/Tools/nbe_codegen.ML	Tue Mar 07 04:06:02 2006 +0100
     7.2 +++ b/src/Pure/Tools/nbe_codegen.ML	Tue Mar 07 14:09:48 2006 +0100
     7.3 @@ -91,55 +91,43 @@
     7.4  open BasicCodegenThingol;
     7.5  
     7.6  fun mk_rexpr defined nm ar =
     7.7 -  let fun mk args t = case t of
     7.8 -    IConst((s,_),_) => 
     7.9 -    if s=nm then selfcall nm ar args
    7.10 -    else if defined s then S.nbe_apps (MLname s) args
    7.11 -    else S.app Eval_Constr (S.tup [S.quote s,S.list args ])
    7.12 -  | IVar s => S.nbe_apps (MLvname s) args
    7.13 -  | e1 `$ e2 => mk (args @ [mk [] e2]) e1
    7.14 -  | (nm, _) `|-> e => S.nbe_apps (mk_nbeFUN(nm, mk [] e)) args
    7.15 -  | IAbs (_, e) => mk args e
    7.16 -  | ICase (_, e) => mk args e
    7.17 +  let
    7.18 +    fun mk args = CodegenThingol.map_pure (mk' args)
    7.19 +    and mk' args (IConst (c, _)) =
    7.20 +          if c = nm then selfcall nm ar args
    7.21 +          else if defined c then S.nbe_apps (MLname c) args
    7.22 +          else S.app Eval_Constr (S.tup [S.quote c, S.list args])
    7.23 +      | mk' args (IVar s) = S.nbe_apps (MLvname s) args
    7.24 +      | mk' args (e1 `$ e2) = mk (args @ [mk [] e2]) e1
    7.25 +      | mk' args ((nm, _) `|-> e) = S.nbe_apps (mk_nbeFUN (nm, mk [] e)) args;
    7.26    in mk [] end;
    7.27  
    7.28  val mk_lexpr =
    7.29 -  let fun mk args t = case t of
    7.30 -    IConst((s,_),_) =>
    7.31 -      S.app Eval_Constr (S.tup [S.quote s, S.list args])
    7.32 -  | IVar s => if args = [] then MLvname s else 
    7.33 -      sys_error "NBE mk_lexpr illegal higher order pattern"
    7.34 -  | e1 `$ e2 => mk (args @ [mk [] e2]) e1
    7.35 -  | IAbs (_, e) => mk args e
    7.36 -  | ICase (_, e) => mk args e
    7.37 -  | _ => sys_error "NBE mk_lexpr illegal pattern"
    7.38 +  let
    7.39 +    fun mk args = CodegenThingol.map_pure (mk' args)
    7.40 +    and mk' args (IConst (c, _)) =
    7.41 +          S.app Eval_Constr (S.tup [S.quote c, S.list args])
    7.42 +      | mk' args (IVar s) = if args = [] then MLvname s else 
    7.43 +          sys_error "NBE mk_lexpr illegal higher order pattern"
    7.44 +      | mk' args (e1 `$ e2) = mk (args @ [mk [] e2]) e1
    7.45 +      | mk' args (_ `|-> _) =
    7.46 +          sys_error "NBE mk_lexpr illegal pattern";
    7.47    in mk [] end;
    7.48  
    7.49 -fun vars (IVar s) = [s]
    7.50 -  | vars (e1 `$ e2) = (vars e1) @ (vars e2)
    7.51 -  | vars (IAbs(_,e)) = vars e
    7.52 -  | vars (ICase(_,e)) = vars e
    7.53 -  | vars _ = [] (* note that a lambda won't occur here anyway *)
    7.54 -
    7.55  fun mk_eqn defined nm ar (lhs,e) =
    7.56 -  if has_duplicates (op =) (Library.flat (map vars lhs)) then [] else
    7.57 +  if has_duplicates (op =) (fold CodegenThingol.add_varnames lhs []) then [] else
    7.58    [([S.list(map mk_lexpr (rev lhs))], mk_rexpr defined nm ar e)];
    7.59  
    7.60 -fun consts_of (IConst ((s, _), _)) = insert (op =) s
    7.61 -  | consts_of (e1 `$ e2) =
    7.62 -      consts_of e1 #> consts_of e2
    7.63 -  | consts_of (_ `|-> e) = consts_of e
    7.64 -  | consts_of (IAbs (_, e)) = consts_of e
    7.65 -  | consts_of (ICase (_, e)) = consts_of e
    7.66 -  | consts_of _ = I;
    7.67 -
    7.68  fun lookup nm = S.Val (MLname nm) (tab_lookup (S.quote nm));
    7.69  
    7.70  fun generate defined (nm, CodegenThingol.Fun (eqns, _)) =
    7.71        let
    7.72 -        val ar = length(fst(hd eqns));
    7.73 -        val params = S.list (rev (MLparams ar));
    7.74 -        val funs = Library.flat(map (fn (_,e) => consts_of e []) eqns) \ nm;
    7.75 +        val ar = (length o fst o hd) eqns;
    7.76 +        val params = (S.list o rev o MLparams) ar;
    7.77 +        val funs =
    7.78 +          []
    7.79 +          |> fold (fn (_, e) => CodegenThingol.add_constnames e) eqns
    7.80 +          |> remove (op =) nm;
    7.81          val globals = map lookup (filter defined funs);
    7.82          val default_eqn = ([params], S.app Eval_Constr (S.tup[S.quote nm,params]));
    7.83          val code = S.eqns (MLname nm)
     8.1 --- a/src/Pure/Tools/nbe_eval.ML	Tue Mar 07 04:06:02 2006 +0100
     8.2 +++ b/src/Pure/Tools/nbe_eval.ML	Tue Mar 07 14:09:48 2006 +0100
     8.3 @@ -121,18 +121,19 @@
     8.4  
     8.5  open BasicCodegenThingol;
     8.6  
     8.7 -fun eval xs (IConst ((f, _), _)) = lookup f
     8.8 -  | eval xs (IVar n) =
     8.9 -      AList.lookup (op =) xs n
    8.10 -      |> the_default (Var (n, []))
    8.11 -  | eval xs (s `$ t) = apply (eval xs s) (eval xs t)
    8.12 -  | eval xs ((n, _) `|-> t) =
    8.13 -      Fun (fn [x] => eval (AList.update (op =) (n, x) xs) t,
    8.14 +fun eval xs =
    8.15 +  let
    8.16 +    fun evl (IConst (c, _)) = lookup c
    8.17 +      | evl (IVar n) =
    8.18 +          AList.lookup (op =) xs n
    8.19 +          |> the_default (Var (n, []))
    8.20 +      | evl (s `$ t) = apply (eval xs s) (eval xs t)
    8.21 +      | evl ((n, _) `|-> t) =
    8.22 +          Fun (fn [x] => eval (AList.update (op =) (n, x) xs) t,
    8.23               [], 1,
    8.24               fn () => let val var = new_name() in
    8.25                   AbsN (var, to_term (eval (AList.update (op =) (n, BVar (var, [])) xs) t)) end)
    8.26 -  | eval xs (IAbs (_, t)) = eval xs t
    8.27 -  | eval xs (ICase (_, t)) = eval xs t;
    8.28 +  in CodegenThingol.map_pure evl end;
    8.29  
    8.30  (* finally... *)
    8.31