# HG changeset patch # User haftmann # Date 1141736988 -3600 # Node ID 0b9eb4b0ad98a65267396ef74fd327a0e6a65f08 # Parent 294448903a66ed9d8412b141ab388a82cc446511 substantial improvement in codegen iml diff -r 294448903a66 -r 0b9eb4b0ad98 src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Tue Mar 07 04:06:02 2006 +0100 +++ b/src/HOL/Datatype.thy Tue Mar 07 14:09:48 2006 +0100 @@ -246,6 +246,9 @@ fst_conv [code] snd_conv [code] +lemma [code unfold]: + "1 == Suc 0" by simp + code_generate True False Not "op &" "op |" If code_syntax_tyco bool @@ -311,9 +314,4 @@ ml (target_atom "SOME") haskell (target_atom "Just") -code_syntax_const - "1 :: nat" - ml ("{*Suc 0*}") - haskell ("{*Suc 0*}") - end diff -r 294448903a66 -r 0b9eb4b0ad98 src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Tue Mar 07 04:06:02 2006 +0100 +++ b/src/HOL/Tools/recfun_codegen.ML Tue Mar 07 14:09:48 2006 +0100 @@ -9,7 +9,6 @@ sig val add: string option -> attribute val del: attribute - val get_rec_equations: theory -> string * typ -> (term list * term) list * typ val get_thm_equations: theory -> string * typ -> (thm list * typ) option val setup: theory -> theory end; @@ -81,19 +80,6 @@ | SOME thyname => thyname) end); -fun get_rec_equations thy (s, T) = - Symtab.lookup (CodegenData.get thy) s - |> Option.map (fn thms => - List.filter (fn (thm, _) => is_instance thy T ((snd o const_of o prop_of) thm)) thms - |> del_redundant thy []) - |> Option.mapPartial (fn thms => if null thms then NONE else SOME thms) - |> Option.map (fn thms => - (preprocess thy (map fst thms), - (snd o const_of o prop_of o fst o hd) thms)) - |> the_default ([], dummyT) - |> apfst (map prop_of) - |> apfst (map (Codegen.rename_term #> HOLogic.dest_Trueprop #> HOLogic.dest_eq #> apfst (strip_comb #> snd))) - fun get_thm_equations thy (c, ty) = Symtab.lookup (CodegenData.get thy) c |> Option.map (fn thms => diff -r 294448903a66 -r 0b9eb4b0ad98 src/HOL/ex/nbe.thy --- a/src/HOL/ex/nbe.thy Tue Mar 07 04:06:02 2006 +0100 +++ b/src/HOL/ex/nbe.thy Tue Mar 07 14:09:48 2006 +0100 @@ -6,15 +6,16 @@ theory nbe imports Main begin + ML"reset quick_and_dirty" declare disj_assoc[code] norm_by_eval "(P | Q) | R" -lemma[code]: "(P \ P)=True" by blast +(*lemma[code]: "(P \ P) = True" by blast norm_by_eval "P \ P" -norm_by_eval "True \ P" +norm_by_eval "True \ P"*) datatype n = Z | S n @@ -52,7 +53,6 @@ "exp m Z = S Z" "exp m (S n) = mul (exp m n) m" - norm_by_eval "mul2 (S(S(S(S(S(S(S Z))))))) (S(S(S(S(S Z)))))" norm_by_eval "mul (S(S(S(S(S(S(S Z))))))) (S(S(S(S(S Z)))))" norm_by_eval "exp (S(S(S(S(S(S(S Z))))))) (S(S(S(S(S Z)))))" @@ -94,16 +94,21 @@ norm_by_eval "map (%x. case x of None \ False | Some y \ True) [None, Some ()]" norm_by_eval "rev [a, b, c]" -end - -(* -ML"set Toplevel.debug" norm_by_eval "case n of None \ True | Some((x,y),(u,v)) \ False" norm_by_eval "let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)" norm_by_eval "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z))" -*) -(* to be done -norm_by_eval "max 0 (0::nat)" norm_by_eval "last[a,b,c]" - Numerals! *) + +text {* + won't work since it relies on + polymorphically used ad-hoc overloaded function: + norm_by_eval "max 0 (0::nat)" +*} +text {* + Numerals still take their time\ +*} + +end + + diff -r 294448903a66 -r 0b9eb4b0ad98 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Tue Mar 07 04:06:02 2006 +0100 +++ b/src/Pure/Tools/codegen_package.ML Tue Mar 07 14:09:48 2006 +0100 @@ -138,7 +138,7 @@ andalso Sign.typ_instance thy (ty2, ty1); fun is_overloaded thy c = case Defs.specifications_of (Theory.defs_of thy) c - of [] => false + of [] => true | [(ty, _)] => not (eq_typ thy (ty, Sign.the_const_type thy c)) | _ => true; @@ -161,10 +161,17 @@ fun mk thy ((c, ty), i) = let val c' = idf_of_name thy nsp_overl c; - val prefix = case (AList.lookup (eq_typ thy) - (Defs.specifications_of (Theory.defs_of thy) c)) ty - of SOME thyname => NameSpace.append thyname nsp_overl - | NONE => NameSpace.drop_base c'; + val prefix = + case (AList.lookup (eq_typ thy) + (Defs.specifications_of (Theory.defs_of thy) c)) ty + of SOME thyname => NameSpace.append thyname nsp_overl + | NONE => if c = "op =" + then + NameSpace.append + (((fn s => Codegen.thyname_of_type s thy) o fst o dest_Type o hd o fst o strip_type) ty) + nsp_overl + else + NameSpace.drop_base c'; val c'' = NameSpace.append prefix (NameSpace.base c'); fun mangle (Type (tyco, tys)) = (NameSpace.base o alias_get thy) tyco :: Library.flat (List.mapPartial mangle tys) |> SOME @@ -399,13 +406,13 @@ (c, ty) = let fun get_overloaded (c, ty) = - case Symtab.lookup overltab1 c + (case Symtab.lookup overltab1 c of SOME tys => (case find_first (curry (Sign.typ_instance thy) ty) tys of SOME ty' => ConstNameMangler.get thy overltab2 (c, ty') |> SOME | _ => NONE) - | _ => NONE + | _ => NONE) fun get_datatypecons (c, ty) = case (snd o strip_type) ty of Type (tyco, _) => @@ -851,12 +858,12 @@ and appgen_default thy tabs ((c, ty), ts) trns = trns |> ensure_def_const thy tabs (c, ty) + ||>> exprsgen_type thy tabs [ty] ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs) (ClassPackage.extract_classlookup thy (c, ty)) - ||>> exprsgen_type thy tabs [ty] ||>> fold_map (exprgen_term thy tabs) ts - |-> (fn (((c, ls), [ty]), es) => - pair (IConst ((c, ty), ls) `$$ es)) + |-> (fn (((c, [ty]), ls), es) => + pair (IConst (c, (ls, ty)) `$$ es)) and appgen thy tabs ((f, ty), ts) trns = case Symtab.lookup ((#appconst o #gens o CodegenData.get) thy) f of SOME ((imin, imax), (ag, _)) => @@ -899,43 +906,48 @@ (* parametrized generators, for instantiation in HOL *) -fun appgen_let strip_abs thy tabs (app as ((c, ty), [dt, ct])) trns = - let - val ([st], bt) = strip_abs 1 ct; - val dtyp = (hd o fst o strip_type) ty - in - trns - |> exprgen_term thy tabs dt - ||>> exprgen_type thy tabs dtyp - ||>> exprgen_term thy tabs st - ||>> exprgen_term thy tabs bt - ||>> appgen_default thy tabs app - |-> (fn ((((de, dty), se), be), e0) => pair (ICase (((de, dty), [(se, be)]), e0))) - end; - -fun appgen_split strip_abs thy tabs (app as (c as (_, ty), [t])) trns = +fun appgen_split strip_abs thy tabs (app as (c, [t])) trns = case strip_abs 1 (Const c $ t) - of ([vt], tb) => + of ([vt], bt) => trns |> exprgen_term thy tabs vt - ||>> exprgen_type thy tabs (((fn [_, ty] => ty) o fst o strip_type) ty) - ||>> exprgen_term thy tabs tb + ||>> exprgen_type thy tabs (type_of vt) + ||>> exprgen_term thy tabs bt ||>> appgen_default thy tabs app |-> (fn (((ve, vty), be), e0) => pair (IAbs (((ve, vty), be), e0))) | _ => trns |> appgen_default thy tabs app; +fun appgen_let strip_abs thy tabs (app as ((c, ty), [dt, ct])) trns = + case strip_abs 1 ct + of ([st], bt) => + trns + |> exprgen_term thy tabs dt + ||>> exprgen_type thy tabs (type_of dt) + ||>> exprgen_term thy tabs st + ||>> exprgen_term thy tabs bt + ||>> appgen_default thy tabs app + |-> (fn ((((de, dty), se), be), e0) => pair (ICase (((de, dty), [(se, be)]), e0))) + | _ => + trns + |> appgen_default thy tabs app; + fun appgen_number_of mk_int_to_nat bin_to_int tyco_int tyco_nat thy tabs ((_, Type (_, [_, ty as Type (tyco, [])])), [bin]) trns = - if tyco = tyco_int then + if tyco = tyco_nat then trns - |> exprgen_type thy tabs ty - |-> (fn ty => pair (CodegenThingol.IConst (((IntInf.toString o bin_to_int thy) bin, ty), []))) - else if tyco = tyco_nat then - trns - |> exprgen_term thy tabs (mk_int_to_nat bin) - else error ("invalid type constructor for numeral: " ^ quote tyco); + |> exprgen_term thy tabs (mk_int_to_nat bin) (*should be a preprocessor's work*) + else + let + val i = bin_to_int thy bin; + val _ = if i < 0 then error ("negative numeral: " ^ IntInf.toString i) else (); + (*should be a preprocessor's work*) + in + trns + |> exprgen_type thy tabs ty + |-> (fn ty => pair (CodegenThingol.INum ((i, ty), ()))) + end; fun appgen_wfrec thy tabs ((c, ty), [_, tf, tx]) trns = let @@ -951,25 +963,7 @@ ||>> exprsgen_type thy tabs [ty_def] ||>> exprgen_term thy tabs tf ||>> exprgen_term thy tabs tx - |-> (fn ((((_, ls), [ty]), tf), tx) => pair (IConst ((idf, ty), ls) `$ tf `$ tx)) - end; - - -fun appgen_wfrec thy tabs ((c, ty), [_, tf, tx]) trns = - let - val ty_def = (op ---> o apfst tl o strip_type o Sign.the_const_type thy) c; - val ty' = (op ---> o apfst tl o strip_type) ty; - val idf = idf_of_const thy tabs (c, ty); - in - trns - |> ensure_def [("wfrec", (K o succeed) Undef)] ("generating wfrec") idf - |> exprgen_type thy tabs ty' - ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs) - (ClassPackage.extract_classlookup thy (c, ty)) - ||>> exprsgen_type thy tabs [ty_def] - ||>> exprgen_term thy tabs tf - ||>> exprgen_term thy tabs tx - |-> (fn ((((_, ls), [ty]), tf), tx) => pair (IConst ((idf, ty), ls) `$ tf `$ tx)) + |-> (fn ((((_, ls), [ty]), tf), tx) => pair (IConst (idf, (ls, ty)) `$ tf `$ tx)) end; fun eqextr_eq f fals thy tabs ("op =", ty) = diff -r 294448903a66 -r 0b9eb4b0ad98 src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Tue Mar 07 04:06:02 2006 +0100 +++ b/src/Pure/Tools/codegen_serializer.ML Tue Mar 07 14:09:48 2006 +0100 @@ -314,6 +314,19 @@ |> postprocess_module name end; +fun constructive_fun (name, (eqs, ty)) = + let + fun check_eq (eq as (lhs, rhs)) = + if forall CodegenThingol.is_pat lhs + then SOME eq + else (warning ("in function " ^ quote name ^ ", throwing away one " + ^ "non-executable function clause"); NONE) + in case List.mapPartial check_eq eqs + of [] => error ("in function " ^ quote name ^ ", no" + ^ "executable function clauses found") + | eqs => (name, (eqs, ty)) + end; + fun parse_single_file serializer = OuterParse.path >> (fn path => serializer @@ -336,7 +349,7 @@ fun pretty_list thingol_nil thingol_cons (target_pred, target_cons) = let - fun dest_cons (IConst ((c, _), _) `$ e1 `$ e2) = + fun dest_cons (IConst (c, _) `$ e1 `$ e2) = if c = thingol_cons then SOME (e1, e2) else NONE @@ -349,7 +362,7 @@ ]; fun pretty_compact fxy pr [e1, e2] = case CodegenThingol.unfoldr dest_cons e2 - of (es, IConst ((c, _), _)) => + of (es, IConst (c, _)) => if c = thingol_nil then Pretty.enum "," "[" "]" (map (pr NOBR) (e1::es)) else pretty_default fxy pr e1 e2 @@ -445,17 +458,15 @@ end | ml_from_type fxy (ITyVar v) = str ("'" ^ v); - fun typify trans ty p = + fun typify ty p = let fun needs_type_t (tyco `%% tys) = needs_type tyco - orelse trans - andalso exists needs_type_t tys + orelse exists needs_type_t tys | needs_type_t (ITyVar _) = false | needs_type_t (ty1 `-> ty2) = - trans - andalso (needs_type_t ty1 orelse needs_type_t ty2); + needs_type_t ty1 orelse needs_type_t ty2; in if needs_type_t ty then Pretty.enclose "(" ")" [ @@ -480,14 +491,20 @@ | ml_from_expr fxy ((v, ty) `|-> e) = brackify BR [ str "fn", - typify true ty (str v), + typify ty (str v), str "=>", ml_from_expr NOBR e ] + | ml_from_expr fxy (INum ((n, ty), _)) = + Pretty.enclose "(" ")" [ + (str o IntInf.toString) n, + str ":", + ml_from_type NOBR ty + ] | ml_from_expr fxy (IAbs (((ve, vty), be), _)) = brackify BR [ str "fn", - typify true vty (ml_from_expr NOBR ve), + typify vty (ml_from_expr NOBR ve), str "=>", ml_from_expr NOBR be ] @@ -497,7 +514,7 @@ fun mk_val ((ve, vty), se) = Pretty.block [ (Pretty.block o Pretty.breaks) [ str "val", - typify true vty (ml_from_expr NOBR ve), + typify vty (ml_from_expr NOBR ve), str "=", ml_from_expr NOBR se ], @@ -519,7 +536,7 @@ ] in brackify fxy ( str "case" - :: typify true dty (ml_from_expr NOBR de) + :: typify dty (ml_from_expr NOBR de) :: mk_clause "of" bse :: map (mk_clause "|") bses ) end @@ -530,11 +547,10 @@ [(str o resolv) f, Pretty.enum "," "(" ")" (map (ml_from_expr BR) es)] else (str o resolv) f :: map (ml_from_expr BR) es - and ml_from_app fxy (((c, ty), lss), es) = + and ml_from_app fxy ((c, (lss, ty)), es) = case map (ml_from_sortlookup BR) lss of [] => from_app ml_mk_app ml_from_expr const_syntax fxy ((c, ty), es) - |> typify false ty | lss => brackify fxy ( (str o resolv) c @@ -581,7 +597,7 @@ map (Pretty.block o single o Pretty.block o single); fun mk_arg e ty = ml_from_expr BR e - |> typify true ty + |> typify ty fun mk_eq definer (pats, expr) = (Pretty.block o Pretty.breaks) ( [str definer, (str o resolv) name] @@ -601,8 +617,8 @@ end; in chunk_defs ( - mk_fun (the (fold check_args defs NONE)) def - :: map (mk_fun "and") defs_tl + (mk_fun (the (fold check_args defs NONE)) o constructive_fun) def + :: map (mk_fun "and" o constructive_fun) defs_tl ) end; fun ml_from_datatypes (defs as (def::defs_tl)) = @@ -912,6 +928,8 @@ hs_from_expr NOBR e ]) end + | hs_from_expr fxy (INum ((n, _), _)) = + (str o IntInf.toString) n | hs_from_expr fxy (e as IAbs _) = let val (es, e) = CodegenThingol.unfold_abs e @@ -954,11 +972,11 @@ ] end and hs_mk_app c es = (str o resolv) c :: map (hs_from_expr BR) es - and hs_from_app fxy (((c, ty), ls), es) = + and hs_from_app fxy ((c, (ty, ls)), es) = from_app hs_mk_app hs_from_expr const_syntax fxy ((c, ty), es); - fun hs_from_funeqs (name, eqs) = + fun hs_from_funeqs (def as (name, _)) = let - fun from_eq name (args, rhs) = + fun from_eq (args, rhs) = Pretty.block [ (str o resolv_here) name, Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, hs_from_expr BR p]) args), @@ -967,14 +985,14 @@ Pretty.brk 1, hs_from_expr NOBR rhs ] - in Pretty.chunks (map (from_eq name) eqs) end; + in Pretty.chunks ((map from_eq o fst o snd o constructive_fun) def) end; fun hs_from_def (name, CodegenThingol.Undef) = error ("empty statement during serialization: " ^ quote name) | hs_from_def (name, CodegenThingol.Prim prim) = from_prim resolv_here (name, prim) - | hs_from_def (name, CodegenThingol.Fun (eqs, (sctxt, ty))) = + | hs_from_def (name, CodegenThingol.Fun (def as (_, (sctxt, ty)))) = let - val body = hs_from_funeqs (name, eqs); + val body = hs_from_funeqs (name, def); in if with_typs then Pretty.chunks [ Pretty.block [ @@ -1042,7 +1060,7 @@ hs_from_sctxt_tycoexpr (arity, (tyco, map (ITyVar o fst) arity)), str " where", Pretty.fbrk, - Pretty.chunks (map (fn (m, (_, (eqs, _))) => hs_from_funeqs (m, eqs)) memdefs) + Pretty.chunks (map (fn (m, (_, (eqs, ty))) => hs_from_funeqs (m, (eqs, ty))) memdefs) ] |> SOME in case List.mapPartial (fn (name, def) => hs_from_def (name, def)) defs diff -r 294448903a66 -r 0b9eb4b0ad98 src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Tue Mar 07 04:06:02 2006 +0100 +++ b/src/Pure/Tools/codegen_thingol.ML Tue Mar 07 14:09:48 2006 +0100 @@ -24,10 +24,11 @@ | `-> of itype * itype | ITyVar of vname; datatype iexpr = - IConst of (string * itype) * iclasslookup list list + IConst of string * (iclasslookup list list * itype) | IVar of vname | `$ of iexpr * iexpr | `|-> of (vname * itype) * iexpr + | INum of (IntInf.int (*positive!*) * itype) * unit | IAbs of ((iexpr * itype) * iexpr) * iexpr (* (((binding expression (ve), binding type (vty)), body expression (be)), native expression (e0)) *) @@ -52,8 +53,11 @@ val unfold_abs: iexpr -> (iexpr * itype) list * iexpr; val unfold_let: iexpr -> ((iexpr * itype) * iexpr) list * iexpr; val unfold_const_app: iexpr -> - (((string * itype) * iclasslookup list list) * iexpr list) option; - val ensure_pat: iexpr -> iexpr; + ((string * (iclasslookup list list * itype)) * iexpr list) option; + val add_constnames: iexpr -> string list -> string list; + val add_varnames: iexpr -> string list -> string list; + val is_pat: iexpr -> bool; + val map_pure: (iexpr -> 'a) -> iexpr -> 'a; type funn = (iexpr list * iexpr) list * (sortcontext * itype); type datatyp = sortcontext * (string * itype list) list; @@ -161,10 +165,11 @@ | ITyVar of vname; datatype iexpr = - IConst of (string * itype) * iclasslookup list list + IConst of string * (iclasslookup list list * itype) | IVar of vname | `$ of iexpr * iexpr | `|-> of (vname * itype) * iexpr + | INum of (IntInf.int (*positive!*) * itype) * unit | IAbs of ((iexpr * itype) * iexpr) * iexpr | ICase of ((iexpr * itype) * (iexpr * iexpr) list) * iexpr; (*see also signature*) @@ -208,7 +213,7 @@ | pretty_itype (ITyVar v) = Pretty.str v; -fun pretty_iexpr (IConst ((c, _), _)) = +fun pretty_iexpr (IConst (c, _)) = Pretty.str c | pretty_iexpr (IVar v) = Pretty.str ("?" ^ v) @@ -218,6 +223,8 @@ | pretty_iexpr ((v, ty) `|-> e) = (Pretty.enclose "(" ")" o Pretty.breaks) [Pretty.str v, Pretty.str "::", pretty_itype ty, Pretty.str "|->", pretty_iexpr e] + | pretty_iexpr (INum ((n, _), _)) = + (Pretty.str o IntInf.toString) n | pretty_iexpr (IAbs (((e1, _), e2), _)) = (Pretty.enclose "(" ")" o Pretty.breaks) [pretty_iexpr e1, Pretty.str "|->", pretty_iexpr e2] @@ -271,6 +278,8 @@ f e1 `$ f e2 | map_iexpr f ((v, ty) `|-> e) = (v, ty) `|-> f e + | map_iexpr _ (e as INum _) = + e | map_iexpr f (IAbs (((ve, vty), be), e0)) = IAbs (((f ve, vty), f be), e0) | map_iexpr f (ICase (((de, dty), bses), e0)) = @@ -278,8 +287,8 @@ fun map_iexpr_itype f = let - fun mapp (IConst ((c, ty), sctxt)) = IConst ((c, f ty), sctxt) - | mapp ((v, ty) `|-> e) = (v, f ty) `|-> mapp e + fun mapp ((v, ty) `|-> e) = (v, f ty) `|-> mapp e + | mapp (INum ((n, ty), e)) = INum ((n, f ty), e) | mapp (IAbs (((ve, vty), be), e0)) = IAbs (((mapp ve, f vty), mapp be), e0) | mapp (ICase (((de, dty), bses), e0)) = @@ -321,12 +330,27 @@ | instant y = map_itype instant y; in map_itype instant end; -fun ensure_pat (e as IConst (_, [])) = e - | ensure_pat (e as IVar _) = e - | ensure_pat (e as (e1 `$ e2)) = - (ensure_pat e1; ensure_pat e2; e) - | ensure_pat e = - error ("illegal expression for pattern: " ^ (Pretty.output o pretty_iexpr) e); +fun is_pat (e as IConst (_, ([], _))) = true + | is_pat (e as IVar _) = true + | is_pat (e as (e1 `$ e2)) = + is_pat e1 andalso is_pat e2 + | is_pat (e as INum _) = true + | is_pat e = false; + +fun map_pure f (e as IConst _) = + f e + | map_pure f (e as IVar _) = + f e + | map_pure f (e as _ `$ _) = + f e + | map_pure f (e as _ `|-> _) = + f e + | map_pure _ (INum _) = + error ("sorry, no pure representation of numerals so far") + | map_pure f (IAbs (_, e0)) = + f e0 + | map_pure f (ICase (_, e0)) = + f e0; fun has_tyvars (_ `%% tys) = exists has_tyvars tys @@ -335,18 +359,35 @@ | has_tyvars (ty1 `-> ty2) = has_tyvars ty1 orelse has_tyvars ty2; -fun varnames_of (IConst ((c, _), _)) = +fun add_constnames (IConst (c, _)) = + insert (op =) c + | add_constnames (IVar _) = I - | varnames_of (IVar v) = + | add_constnames (e1 `$ e2) = + add_constnames e1 #> add_constnames e2 + | add_constnames (_ `|-> e) = + add_constnames e + | add_constnames (INum _) = + I + | add_constnames (IAbs (_, e)) = + add_constnames e + | add_constnames (ICase (_, e)) = + add_constnames e; + +fun add_varnames (IConst _) = + I + | add_varnames (IVar v) = insert (op =) v - | varnames_of (e1 `$ e2) = - varnames_of e1 #> varnames_of e2 - | varnames_of ((v, _) `|-> e) = - insert (op =) v #> varnames_of e - | varnames_of (IAbs (((ve, _), be), _)) = - varnames_of ve #> varnames_of be - | varnames_of (ICase (((de, _), bses), _)) = - varnames_of de #> fold (fn (be, se) => varnames_of be #> varnames_of se) bses; + | add_varnames (e1 `$ e2) = + add_varnames e1 #> add_varnames e2 + | add_varnames ((v, _) `|-> e) = + insert (op =) v #> add_varnames e + | add_varnames (INum _) = + I + | add_varnames (IAbs (((ve, _), be), _)) = + add_varnames ve #> add_varnames be + | add_varnames (ICase (((de, _), bses), _)) = + add_varnames de #> fold (fn (be, se) => add_varnames be #> add_varnames se) bses; fun invent seed used = let @@ -884,17 +925,17 @@ let fun eta e = case unfold_const_app e - of SOME (((f, ty), ls), es) => + of SOME (const as (c, (_, ty)), es) => let - val delta = query f - length es; + val delta = query c - length es; val add_n = if delta < 0 then 0 else delta; val tys = (fst o unfold_fun) ty |> curry Library.drop (length es) |> curry Library.take add_n - val vs = (Term.invent_names (fold varnames_of es []) "x" add_n) + val vs = (Term.invent_names (fold add_varnames es []) "x" add_n) in - vs ~~ tys `|--> IConst ((f, ty), ls) `$$ map eta es `$$ map IVar vs + vs ~~ tys `|--> IConst const `$$ map eta es `$$ map IVar vs end | NONE => map_iexpr eta e; in (map_defs o map_def_fun o map_def_fun_expr) eta end; @@ -908,7 +949,7 @@ else (case unfold_abs e of ([], e) => let - val add_var = IVar (hd (Term.invent_names (varnames_of e []) "x" 1)) + val add_var = IVar (hd (Term.invent_names (add_varnames e []) "x" 1)) in (([([add_var], e `$ add_var)], cty)) end | _ => funn) | eta funn = funn; @@ -919,7 +960,7 @@ fun unclash (eqs, (sortctxt, ty)) = let val used_expr = - fold (fn (pats, rhs) => fold varnames_of pats #> varnames_of rhs) eqs []; + fold (fn (pats, rhs) => fold add_varnames pats #> add_varnames rhs) eqs []; val used_type = map fst sortctxt; val clash = gen_union (op =) (used_expr, used_type); val rename_map = fold_map (fn c => invent c #-> (fn c' => pair (c, c'))) clash [] |> fst; diff -r 294448903a66 -r 0b9eb4b0ad98 src/Pure/Tools/nbe_codegen.ML --- a/src/Pure/Tools/nbe_codegen.ML Tue Mar 07 04:06:02 2006 +0100 +++ b/src/Pure/Tools/nbe_codegen.ML Tue Mar 07 14:09:48 2006 +0100 @@ -91,55 +91,43 @@ open BasicCodegenThingol; fun mk_rexpr defined nm ar = - let fun mk args t = case t of - IConst((s,_),_) => - if s=nm then selfcall nm ar args - else if defined s then S.nbe_apps (MLname s) args - else S.app Eval_Constr (S.tup [S.quote s,S.list args ]) - | IVar s => S.nbe_apps (MLvname s) args - | e1 `$ e2 => mk (args @ [mk [] e2]) e1 - | (nm, _) `|-> e => S.nbe_apps (mk_nbeFUN(nm, mk [] e)) args - | IAbs (_, e) => mk args e - | ICase (_, e) => mk args e + let + fun mk args = CodegenThingol.map_pure (mk' args) + and mk' args (IConst (c, _)) = + if c = nm then selfcall nm ar args + else if defined c then S.nbe_apps (MLname c) args + else S.app Eval_Constr (S.tup [S.quote c, S.list args]) + | mk' args (IVar s) = S.nbe_apps (MLvname s) args + | mk' args (e1 `$ e2) = mk (args @ [mk [] e2]) e1 + | mk' args ((nm, _) `|-> e) = S.nbe_apps (mk_nbeFUN (nm, mk [] e)) args; in mk [] end; val mk_lexpr = - let fun mk args t = case t of - IConst((s,_),_) => - S.app Eval_Constr (S.tup [S.quote s, S.list args]) - | IVar s => if args = [] then MLvname s else - sys_error "NBE mk_lexpr illegal higher order pattern" - | e1 `$ e2 => mk (args @ [mk [] e2]) e1 - | IAbs (_, e) => mk args e - | ICase (_, e) => mk args e - | _ => sys_error "NBE mk_lexpr illegal pattern" + let + fun mk args = CodegenThingol.map_pure (mk' args) + and mk' args (IConst (c, _)) = + S.app Eval_Constr (S.tup [S.quote c, S.list args]) + | mk' args (IVar s) = if args = [] then MLvname s else + sys_error "NBE mk_lexpr illegal higher order pattern" + | mk' args (e1 `$ e2) = mk (args @ [mk [] e2]) e1 + | mk' args (_ `|-> _) = + sys_error "NBE mk_lexpr illegal pattern"; in mk [] end; -fun vars (IVar s) = [s] - | vars (e1 `$ e2) = (vars e1) @ (vars e2) - | vars (IAbs(_,e)) = vars e - | vars (ICase(_,e)) = vars e - | vars _ = [] (* note that a lambda won't occur here anyway *) - fun mk_eqn defined nm ar (lhs,e) = - if has_duplicates (op =) (Library.flat (map vars lhs)) then [] else + if has_duplicates (op =) (fold CodegenThingol.add_varnames lhs []) then [] else [([S.list(map mk_lexpr (rev lhs))], mk_rexpr defined nm ar e)]; -fun consts_of (IConst ((s, _), _)) = insert (op =) s - | consts_of (e1 `$ e2) = - consts_of e1 #> consts_of e2 - | consts_of (_ `|-> e) = consts_of e - | consts_of (IAbs (_, e)) = consts_of e - | consts_of (ICase (_, e)) = consts_of e - | consts_of _ = I; - fun lookup nm = S.Val (MLname nm) (tab_lookup (S.quote nm)); fun generate defined (nm, CodegenThingol.Fun (eqns, _)) = let - val ar = length(fst(hd eqns)); - val params = S.list (rev (MLparams ar)); - val funs = Library.flat(map (fn (_,e) => consts_of e []) eqns) \ nm; + val ar = (length o fst o hd) eqns; + val params = (S.list o rev o MLparams) ar; + val funs = + [] + |> fold (fn (_, e) => CodegenThingol.add_constnames e) eqns + |> remove (op =) nm; val globals = map lookup (filter defined funs); val default_eqn = ([params], S.app Eval_Constr (S.tup[S.quote nm,params])); val code = S.eqns (MLname nm) diff -r 294448903a66 -r 0b9eb4b0ad98 src/Pure/Tools/nbe_eval.ML --- a/src/Pure/Tools/nbe_eval.ML Tue Mar 07 04:06:02 2006 +0100 +++ b/src/Pure/Tools/nbe_eval.ML Tue Mar 07 14:09:48 2006 +0100 @@ -121,18 +121,19 @@ open BasicCodegenThingol; -fun eval xs (IConst ((f, _), _)) = lookup f - | eval xs (IVar n) = - AList.lookup (op =) xs n - |> the_default (Var (n, [])) - | eval xs (s `$ t) = apply (eval xs s) (eval xs t) - | eval xs ((n, _) `|-> t) = - Fun (fn [x] => eval (AList.update (op =) (n, x) xs) t, +fun eval xs = + let + fun evl (IConst (c, _)) = lookup c + | evl (IVar n) = + AList.lookup (op =) xs n + |> the_default (Var (n, [])) + | evl (s `$ t) = apply (eval xs s) (eval xs t) + | evl ((n, _) `|-> t) = + Fun (fn [x] => eval (AList.update (op =) (n, x) xs) t, [], 1, fn () => let val var = new_name() in AbsN (var, to_term (eval (AList.update (op =) (n, BVar (var, [])) xs) t)) end) - | eval xs (IAbs (_, t)) = eval xs t - | eval xs (ICase (_, t)) = eval xs t; + in CodegenThingol.map_pure evl end; (* finally... *)