--- 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
--- 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 =>
--- 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 \<longrightarrow> P)=True" by blast
+(*lemma[code]: "(P \<longrightarrow> P) = True" by blast
norm_by_eval "P \<longrightarrow> P"
-norm_by_eval "True \<longrightarrow> P"
+norm_by_eval "True \<longrightarrow> 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 \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()]"
norm_by_eval "rev [a, b, c]"
-end
-
-(*
-ML"set Toplevel.debug"
norm_by_eval "case n of None \<Rightarrow> True | Some((x,y),(u,v)) \<Rightarrow> 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\<dots>
+*}
+
+end
+
+
--- 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) =
--- 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
--- 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;
--- 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)
--- 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... *)