--- a/src/HOL/ex/nbe.thy Wed Mar 01 10:37:00 2006 +0100
+++ b/src/HOL/ex/nbe.thy Wed Mar 01 13:47:42 2006 +0100
@@ -7,28 +7,17 @@
imports Main
begin
-datatype n = Z | S n
-consts
- add :: "n \<Rightarrow> n \<Rightarrow> n"
- mul :: "n \<Rightarrow> n \<Rightarrow> n"
- exp :: "n \<Rightarrow> n \<Rightarrow> n"
-primrec
-"add Z = id"
-"add (S m) = S o add m"
-primrec
-"mul Z = (%n. Z)"
-"mul (S m) = (%n. add (mul m n) n)"
-primrec
-"exp m Z = S Z"
-"exp m (S n) = mul (exp m n) m"
-
(*ML"set Toplevel.timing"*)
-;norm_by_eval "exp (S(S(S(S(S(S(S Z))))))) (S(S(S(S(S Z)))))";
-norm_by_eval "0 + (n::nat)";
-norm_by_eval "0 + Suc(n)";
-norm_by_eval "Suc(n) + Suc m";
-norm_by_eval "[] @ xs";
-norm_by_eval "(x#xs) @ ys";
-norm_by_eval "[x,y,z] @ [a,b,c]";
+norm_by_eval "exp (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) (Suc (Suc (Suc (Suc (Suc 0)))))"
+norm_by_eval "0 + (n::nat)"
+norm_by_eval "0 + Suc(n)"
+norm_by_eval "Suc(n) + Suc m"
+norm_by_eval "[] @ xs"
+norm_by_eval "(x#xs) @ ys"
+norm_by_eval "[x,y,z] @ [a,b,c]"
+norm_by_eval "%(xs, ys). xs @ ys"
+norm_by_eval "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f])"
+norm_by_eval "%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True"
+norm_by_eval "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()]"
end
--- a/src/Pure/Tools/codegen_package.ML Wed Mar 01 10:37:00 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML Wed Mar 01 13:47:42 2006 +0100
@@ -83,13 +83,6 @@
struct
open CodegenThingol;
-infix 8 `%%;
-infixr 6 `->;
-infixr 6 `-->;
-infix 4 `$;
-infix 4 `$$;
-infixr 3 `|->;
-infixr 3 `|-->;
(* shallow name spaces *)
@@ -661,7 +654,7 @@
| exprgen_type thy tabs (TFree v_s) trns =
trns
|> exprgen_tyvar_sort thy tabs v_s
- |-> (fn (v, sort) => pair (IVarT v))
+ |-> (fn (v, sort) => pair (ITyVar v))
| exprgen_type thy tabs (Type ("fun", [t1, t2])) trns =
trns
|> exprgen_type thy tabs t1
@@ -815,7 +808,7 @@
| exprgen_term thy tabs (Free (v, ty)) trns =
trns
|> exprgen_type thy tabs ty
- |-> (fn ty => pair (IVarE (v, ty)))
+ |-> (fn ty => pair (IVar v))
| exprgen_term thy tabs (Abs (abs as (_, ty, _))) trns =
let
val (v, t) = Term.variant_abs abs
@@ -823,7 +816,7 @@
trns
|> exprgen_type thy tabs ty
||>> exprgen_term thy tabs t
- |-> (fn (ty, e) => pair (IVarE (v, ty) `|-> e))
+ |-> (fn (ty, e) => pair ((v, ty) `|-> e))
end
| exprgen_term thy tabs (t as t1 $ t2) trns =
let
@@ -867,7 +860,7 @@
|> debug 10 (fn _ => "eta-expanding")
|> fold_map (exprgen_type thy tabs) tys
||>> ag thy tabs ((f, ty), ts @ map2 (curry Free) vs tys)
- |-> (fn (tys, e) => pair (map2 (curry IVarE) vs tys `|--> e))
+ |-> (fn (tys, e) => pair (vs ~~ tys `|--> e))
end
else if length ts > imax then
trns
@@ -875,7 +868,7 @@
^ string_of_int (length ts) ^ ")")
|> ag thy tabs ((f, ty), Library.take (imax, ts))
||>> fold_map (exprgen_term thy tabs) (Library.drop (imax, ts))
- |-> (fn es => pair (mk_apps es))
+ |-> (fn (e, es) => pair (e `$$ es))
else
trns
|> debug 10 (fn _ => "keeping arguments")
@@ -896,27 +889,32 @@
(* parametrized generators, for instantiation in HOL *)
-fun appgen_let strip_abs thy tabs ((c, ty), [t_val, t_cont]) trns =
+fun appgen_let strip_abs thy tabs (app as ((c, ty), [dt, ct])) trns =
let
- val ([t_abs], t_body) = strip_abs 1 t_cont;
+ val ([st], bt) = strip_abs 1 ct;
+ val dtyp = (hd o fst o strip_type) ty
in
trns
- |> exprgen_term thy tabs t_val
- ||>> exprgen_term thy tabs t_abs
- ||>> exprgen_term thy tabs t_body
- |-> (fn ((e, abs), body) => pair (ICase (e, [(abs, body)])))
+ |> 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 (c, [t2]) trns =
- case strip_abs 1 (Const c $ t2)
- of ([p], body) =>
+fun appgen_split strip_abs thy tabs (app as (c as (_, ty), [t])) trns =
+ case strip_abs 1 (Const c $ t)
+ of ([vt], tb) =>
trns
- |> exprgen_term thy tabs p
- ||>> exprgen_term thy tabs body
- |-> (fn (e, body) => pair (e `|-> body))
+ |> exprgen_term thy tabs vt
+ ||>> exprgen_type thy tabs (((fn [_, ty] => ty) o fst o strip_type) ty)
+ ||>> exprgen_term thy tabs tb
+ ||>> appgen_default thy tabs app
+ |-> (fn (((ve, vty), be), e0) => pair (IAbs (((ve, vty), be), e0)))
| _ =>
trns
- |> appgen_default thy tabs (c, [t2]);
+ |> 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 =
@@ -975,7 +973,7 @@
| eqextr_eq f fals thy tabs _ =
NONE;
-fun appgen_datatype_case cos thy tabs ((_, ty), ts) trns =
+fun appgen_datatype_case cos thy tabs (app as ((_, ty), ts)) trns =
let
val (ts', t) = split_last ts;
val (tys, dty) = (split_last o fst o strip_type) ty;
@@ -997,8 +995,10 @@
in
trns
|> exprgen_term thy tabs t
+ ||>> exprgen_type thy tabs dty
||>> fold_map cg_case_d ((cos ~~ tys) ~~ ts')
- |-> (fn (t, ds) => pair (ICase (t, ds)))
+ ||>> appgen_default thy tabs app
+ |-> (fn (((de, dty), bses), e0) => pair (ICase (((de, dty), bses), e0)))
end;
fun gen_add_case_const prep_c get_case_const_data raw_c thy =
--- a/src/Pure/Tools/codegen_serializer.ML Wed Mar 01 10:37:00 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Wed Mar 01 13:47:42 2006 +0100
@@ -38,15 +38,8 @@
structure CodegenSerializer: CODEGEN_SERIALIZER =
struct
-open CodegenThingol;
-infix 8 `%%;
-infixr 6 `->;
-infixr 6 `-->;
-infix 4 `$;
-infix 4 `$$;
-infixr 3 `|->;
-infixr 3 `|-->;
-
+open BasicCodegenThingol;
+val debug = CodegenThingol.debug;
(** generic serialization **)
@@ -217,7 +210,7 @@
case Scan.finite Symbol.stopper (Scan.repeat (
($$ "`" |-- $$ "`" >> (CodegenThingol.Pretty o str))
|| ($$ "`" |-- Scan.repeat1 (Scan.unless ($$ "`") (Scan.one Symbol.not_eof))
- --| $$ "`" >> (fn ["_"] => Name | s => error ("malformed antiquote: " ^ implode s)))
+ --| $$ "`" >> (fn ["_"] => CodegenThingol.Name | s => error ("malformed antiquote: " ^ implode s)))
|| Scan.repeat1
(Scan.unless ($$ "`") (Scan.one Symbol.not_eof)) >> (CodegenThingol.Pretty o str o implode)
)) ((Symbol.explode o Symbol.strip_blanks) s)
@@ -234,7 +227,7 @@
* (string -> itype pretty_syntax option)
* (string -> iexpr pretty_syntax option)
-> string list option
- -> module -> unit)
+ -> CodegenThingol.module -> unit)
* OuterParse.token list;
fun abstract_serializer (target, nspgrp) name_root (from_defs, from_module, validator, postproc)
@@ -244,7 +237,7 @@
fun pretty_of_prim resolv (name, primdef) =
let
fun pr (CodegenThingol.Pretty p) = p
- | pr Name = (str o resolv) name;
+ | pr CodegenThingol.Name = (str o resolv) name;
in case AList.lookup (op = : string * string -> bool) primdef target
of NONE => error ("no primitive definition for " ^ quote name)
| SOME ps => (case map pr ps
@@ -256,11 +249,11 @@
in
module
|> debug 3 (fn _ => "selecting submodule...")
- |> (if is_some select then (partof o the) select else I)
+ |> (if is_some select then (CodegenThingol.partof o the) select else I)
|> debug 3 (fn _ => "preprocessing...")
|> preprocess
|> debug 3 (fn _ => "serializing...")
- |> serialize (from_defs (pretty_of_prim, (class_syntax : string -> string option, tyco_syntax, const_syntax)))
+ |> CodegenThingol.serialize (from_defs (pretty_of_prim, (class_syntax : string -> string option, tyco_syntax, const_syntax)))
from_module' validator postproc nspgrp name_root
|> K ()
end;
@@ -343,7 +336,7 @@
fun pretty_list thingol_nil thingol_cons (target_pred, target_cons) =
let
- fun dest_cons (IApp (IApp (IConst ((c, _), _), e1), e2)) =
+ fun dest_cons (IConst ((c, _), _) `$ e1 `$ e2) =
if c = thingol_cons
then SOME (e1, e2)
else NONE
@@ -355,7 +348,7 @@
pr (INFX (target_pred, R)) e2
];
fun pretty_compact fxy pr [e1, e2] =
- case unfoldr dest_cons e2
+ case CodegenThingol.unfoldr dest_cons e2
of (es, IConst ((c, _), _)) =>
if c = thingol_nil
then Pretty.enum "," "[" "]" (map (pr NOBR) (e1::es))
@@ -427,7 +420,7 @@
| [p] => Pretty.block [p, Pretty.brk 1, tyco']
| (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
end
- and ml_from_type fxy (IType (tycoexpr as (tyco, tys))) =
+ and ml_from_type fxy (tycoexpr as tyco `%% tys) =
(case tyco_syntax tyco
of NONE => ml_from_tycoexpr fxy (tyco, tys)
| SOME ((i, k), pr) =>
@@ -437,7 +430,7 @@
^ string_of_int i ^ " to " ^ string_of_int k
^ " expected")
else pr fxy ml_from_type tys)
- | ml_from_type fxy (IFun (t1, t2)) =
+ | ml_from_type fxy (t1 `-> t2) =
let
val brackify = gen_brackify
(case fxy
@@ -450,102 +443,109 @@
ml_from_type (INFX (1, R)) t2
]
end
- | ml_from_type fxy (IVarT v) =
+ | ml_from_type fxy (ITyVar v) =
str ("'" ^ v);
- fun ml_from_expr fxy (e as IApp (e1, e2)) =
- (case unfold_const_app e
+ fun typify trans ty p =
+ let
+ fun needs_type_t (tyco `%% tys) =
+ needs_type tyco
+ orelse trans
+ andalso 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);
+ in if needs_type_t ty
+ then
+ Pretty.enclose "(" ")" [
+ p,
+ str ":",
+ ml_from_type NOBR ty
+ ]
+ else p
+ end;
+ fun ml_from_expr fxy (e as IConst x) =
+ ml_from_app fxy (x, [])
+ | ml_from_expr fxy (IVar v) =
+ str v
+ | ml_from_expr fxy (e as e1 `$ e2) =
+ (case CodegenThingol.unfold_const_app e
of SOME x => ml_from_app fxy x
| NONE =>
brackify fxy [
ml_from_expr NOBR e1,
ml_from_expr BR e2
])
- | ml_from_expr fxy (e as IConst x) =
- ml_from_app fxy (x, [])
- | ml_from_expr fxy (IVarE (v, ty)) =
- if needs_type ty
- then
- Pretty.enclose "(" ")" [
- str v,
- str ":",
- ml_from_type NOBR ty
- ]
- else
- str v
- | ml_from_expr fxy (IAbs (e1, e2)) =
+ | ml_from_expr fxy ((v, ty) `|-> e) =
+ brackify BR [
+ str "fn",
+ typify true ty (str v),
+ str "=>",
+ ml_from_expr NOBR e
+ ]
+ | ml_from_expr fxy (IAbs (((ve, vty), be), _)) =
brackify BR [
str "fn",
- ml_from_expr NOBR e1,
+ typify true vty (ml_from_expr NOBR ve),
str "=>",
- ml_from_expr NOBR e2
+ ml_from_expr NOBR be
]
- | ml_from_expr fxy (e as ICase (_, [_])) =
+ | ml_from_expr fxy (e as ICase ((_, [_]), _)) =
let
- val (ps, e) = unfold_let e;
- fun mk_val (p, e) = Pretty.block [
- str "val ",
- ml_from_expr fxy p,
- str " =",
- Pretty.brk 1,
- ml_from_expr NOBR e,
+ val (ves, be) = CodegenThingol.unfold_let e;
+ fun mk_val ((ve, vty), se) = Pretty.block [
+ (Pretty.block o Pretty.breaks) [
+ str "val",
+ typify true vty (ml_from_expr NOBR ve),
+ str "=",
+ ml_from_expr NOBR se
+ ],
str ";"
- ]
+ ];
in Pretty.chunks [
- [str ("let"), Pretty.fbrk, map mk_val ps |> Pretty.chunks] |> Pretty.block,
- [str ("in"), Pretty.fbrk, ml_from_expr NOBR e] |> Pretty.block,
+ [str ("let"), Pretty.fbrk, map mk_val ves |> Pretty.chunks] |> Pretty.block,
+ [str ("in"), Pretty.fbrk, ml_from_expr NOBR be] |> Pretty.block,
str ("end")
] end
- | ml_from_expr fxy (ICase (e, c::cs)) =
+ | ml_from_expr fxy (ICase (((de, dty), bse::bses), _)) =
let
- fun mk_clause definer (p, e) =
- Pretty.block [
+ fun mk_clause definer (se, be) =
+ (Pretty.block o Pretty.breaks) [
str definer,
- ml_from_expr NOBR p,
- str " =>",
- Pretty.brk 1,
- ml_from_expr NOBR e
+ ml_from_expr NOBR se,
+ str "=>",
+ ml_from_expr NOBR be
]
in brackify fxy (
str "case"
- :: ml_from_expr NOBR e
- :: mk_clause "of " c
- :: map (mk_clause "| ") cs
+ :: typify true dty (ml_from_expr NOBR de)
+ :: mk_clause "of" bse
+ :: map (mk_clause "|") bses
) end
| ml_from_expr _ e =
- error ("dubious expression: " ^ (Pretty.output o pretty_iexpr) e)
+ error ("dubious expression: " ^ (Pretty.output o CodegenThingol.pretty_iexpr) e)
and ml_mk_app f es =
if is_cons f andalso length es > 1 then
[(str o resolv) f, Pretty.enum "," "(" ")" (map (ml_from_expr BR) es)]
- else if has_nsp f "mem" then
- Pretty.block [str "#", ml_from_label f] :: 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) =
case map (ml_from_sortlookup BR) lss
of [] =>
- let
- val p = from_app ml_mk_app ml_from_expr const_syntax fxy ((c, ty), es)
- in if needs_type ty
- then
- Pretty.enclose "(" ")" [
- p,
- str ":",
- ml_from_type NOBR ty
- ]
- else
- p
- end
+ from_app ml_mk_app ml_from_expr const_syntax fxy ((c, ty), es)
+ |> typify false ty
| lss =>
brackify fxy (
(str o resolv) c
:: (lss
@ map (ml_from_expr BR) es)
);
- in (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) end;
+ in (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, typify, ml_from_expr) end;
fun ml_fun_datatyp (is_cons, needs_type) (tyco_syntax, const_syntax) resolv =
let
- val (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) =
+ val (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, typify, ml_from_expr) =
ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv;
fun chunk_defs ps =
let
@@ -579,12 +579,18 @@
let
val shift = if null eq_tl then I else
map (Pretty.block o single o Pretty.block o single);
+ fun mk_arg e ty =
+ ml_from_expr BR e
+ |> typify true ty
fun mk_eq definer (pats, expr) =
(Pretty.block o Pretty.breaks) (
[str definer, (str o resolv) name]
@ (if null pats
then [str ":", ml_from_type NOBR ty]
- else map from_tyvar sortctxt @ map (ml_from_expr BR) pats)
+ else
+ map from_tyvar sortctxt
+ @ map2 mk_arg pats
+ ((curry Library.take (length pats) o fst o CodegenThingol.unfold_fun) ty))
@ [str "=", ml_from_expr NOBR expr]
)
in
@@ -613,7 +619,7 @@
fun mk_datatype definer (t, (vs, cs)) =
(Pretty.block o Pretty.breaks) (
str definer
- :: ml_from_tycoexpr NOBR (t, map (IVarT o fst) vs)
+ :: ml_from_tycoexpr NOBR (t, map (ITyVar o fst) vs)
:: str "="
:: separate (str "|") (map mk_cons cs)
)
@@ -629,22 +635,22 @@
(from_prim, (_, tyco_syntax, const_syntax)) resolver prefix defs =
let
val resolv = resolver prefix;
- val (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) =
+ val (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, typify, ml_from_expr) =
ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv;
val (ml_from_funs, ml_from_datatypes) =
ml_fun_datatyp (is_cons, needs_type) (tyco_syntax, const_syntax) resolv;
val filter_datatype =
List.mapPartial
- (fn (name, Datatype info) => SOME (name, info)
- | (name, Datatypecons _) => NONE
+ (fn (name, CodegenThingol.Datatype info) => SOME (name, info)
+ | (name, CodegenThingol.Datatypecons _) => NONE
| (name, def) => error ("datatype block containing illegal def: "
- ^ (Pretty.output o pretty_def) def));
+ ^ (Pretty.output o CodegenThingol.pretty_def) def));
fun filter_class defs =
case List.mapPartial
- (fn (name, Class info) => SOME (name, info)
- | (name, Classmember _) => NONE
+ (fn (name, CodegenThingol.Class info) => SOME (name, info)
+ | (name, CodegenThingol.Classmember _) => NONE
| (name, def) => error ("class block containing illegal def: "
- ^ (Pretty.output o pretty_def) def)) defs
+ ^ (Pretty.output o CodegenThingol.pretty_def) def)) defs
of [class] => class
| _ => error ("class block without class: " ^ (commas o map (quote o fst)) defs)
fun ml_from_class (name, (supclasses, (v, membrs))) =
@@ -687,23 +693,23 @@
]
:: map from_membr_fun membrs)
end
- fun ml_from_def (name, Undef) =
+ fun ml_from_def (name, CodegenThingol.Undef) =
error ("empty definition during serialization: " ^ quote name)
- | ml_from_def (name, Prim prim) =
+ | ml_from_def (name, CodegenThingol.Prim prim) =
from_prim resolv (name, prim)
- | ml_from_def (name, Typesyn (vs, ty)) =
+ | ml_from_def (name, CodegenThingol.Typesyn (vs, ty)) =
(map (fn (vname, []) => () | _ =>
error "can't serialize sort constrained type declaration to ML") vs;
Pretty.block [
str "type ",
- ml_from_tycoexpr NOBR (name, map (IVarT o fst) vs),
+ ml_from_tycoexpr NOBR (name, map (ITyVar o fst) vs),
str " =",
Pretty.brk 1,
ml_from_type NOBR ty,
str ";"
]
) |> SOME
- | ml_from_def (name, Classinst (((class, (tyco, arity)), suparities), memdefs)) =
+ | ml_from_def (name, CodegenThingol.Classinst (((class, (tyco, arity)), suparities), memdefs)) =
let
val definer = if null arity then "val" else "fun"
fun from_supclass (supclass, (supinst, lss)) =
@@ -749,23 +755,21 @@
] |> SOME
end;
in case defs
- of (_, Fun _)::_ => (SOME o ml_from_funs o map (fn (name, Fun info) => (name, info))) defs
- | (_, Datatypecons _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs
- | (_, Datatype _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs
- | (_, Class _)::_ => (SOME o ml_from_class o filter_class) defs
- | (_, Classmember _)::_ => (SOME o ml_from_class o filter_class) defs
+ of (_, CodegenThingol.Fun _)::_ => (SOME o ml_from_funs o map (fn (name, CodegenThingol.Fun info) => (name, info))) defs
+ | (_, CodegenThingol.Datatypecons _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs
+ | (_, CodegenThingol.Datatype _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs
+ | (_, CodegenThingol.Class _)::_ => (SOME o ml_from_class o filter_class) defs
+ | (_, CodegenThingol.Classmember _)::_ => (SOME o ml_from_class o filter_class) defs
| [def] => ml_from_def def
| defs => error ("illegal mutual dependencies: " ^ (commas o map fst) defs)
end;
fun ml_annotators (nsp_dtcon, nsp_class, is_int_tyco) =
let
- fun needs_type (IType (tyco, _)) =
- has_nsp tyco nsp_class
- orelse is_int_tyco tyco
- | needs_type _ =
- false;
- fun is_cons c = has_nsp c nsp_dtcon;
+ fun needs_type tyco =
+ CodegenThingol.has_nsp tyco nsp_class
+ orelse is_int_tyco tyco;
+ fun is_cons c = CodegenThingol.has_nsp c nsp_dtcon;
in (is_cons, needs_type) end;
in
@@ -788,21 +792,22 @@
fun eta_expander module const_syntax s =
case const_syntax s
of SOME ((i, _), _) => i
- | _ => if has_nsp s nsp_dtcon
- then case get_def module s
- of Datatypecons dtname => case get_def module dtname
- of Datatype (_, cs) =>
+ | _ => if CodegenThingol.has_nsp s nsp_dtcon
+ then case CodegenThingol.get_def module s
+ of CodegenThingol.Datatypecons dtname =>
+ case CodegenThingol.get_def module dtname
+ of CodegenThingol.Datatype (_, cs) =>
let val l = AList.lookup (op =) cs s |> the |> length
in if l >= 2 then l else 0 end
else 0;
fun preprocess const_syntax module =
module
|> debug 3 (fn _ => "eta-expanding...")
- |> eta_expand (eta_expander module const_syntax)
+ |> CodegenThingol.eta_expand (eta_expander module const_syntax)
|> debug 3 (fn _ => "eta-expanding polydefs...")
- |> eta_expand_poly
+ |> CodegenThingol.eta_expand_poly
|> debug 3 (fn _ => "unclashing expression/type variables...")
- |> unclash_vars_tvars;
+ |> CodegenThingol.unclash_vars_tvars;
val parse_multi =
OuterParse.name
#-> (fn "dir" =>
@@ -861,10 +866,10 @@
end;
fun hs_from_tycoexpr fxy (tyco, tys) =
brackify fxy ((str o resolv) tyco :: map (hs_from_type BR) tys)
- and hs_from_type fxy (IType (tycoexpr as (tyco, tys))) =
+ and hs_from_type fxy (tycoexpr as tyco `%% tys) =
(case tyco_syntax tyco
of NONE =>
- hs_from_tycoexpr fxy tycoexpr
+ hs_from_tycoexpr fxy (tyco, tys)
| SOME ((i, k), pr) =>
if not (i <= length tys andalso length tys <= k)
then error ("number of argument mismatch in customary serialization: "
@@ -872,71 +877,80 @@
^ string_of_int i ^ " to " ^ string_of_int k
^ " expected")
else pr fxy hs_from_type tys)
- | hs_from_type fxy (IFun (t1, t2)) =
+ | hs_from_type fxy (t1 `-> t2) =
brackify_infix (1, R) fxy [
hs_from_type (INFX (1, X)) t1,
str "->",
hs_from_type (INFX (1, R)) t2
]
- | hs_from_type fxy (IVarT v) =
+ | hs_from_type fxy (ITyVar v) =
str v;
fun hs_from_sctxt_tycoexpr (sctxt, tycoexpr) =
Pretty.block [hs_from_sctxt sctxt, hs_from_tycoexpr NOBR tycoexpr]
fun hs_from_sctxt_type (sctxt, ty) =
Pretty.block [hs_from_sctxt sctxt, hs_from_type NOBR ty]
- fun hs_from_expr fxy (e as IApp (e1, e2)) =
- (case unfold_const_app e
+ fun hs_from_expr fxy (e as IConst x) =
+ hs_from_app fxy (x, [])
+ | hs_from_expr fxy (e as (e1 `$ e2)) =
+ (case CodegenThingol.unfold_const_app e
of SOME x => hs_from_app fxy x
| _ =>
brackify fxy [
hs_from_expr NOBR e1,
hs_from_expr BR e2
])
- | hs_from_expr fxy (e as IConst x) =
- hs_from_app fxy (x, [])
- | hs_from_expr fxy (IVarE (v, _)) =
- str v
- | hs_from_expr fxy (e as IAbs _) =
+ | hs_from_expr fxy (IVar v) =
+ (str o String.implode o nth_map 0 Char.toLower o String.explode) v
+ | hs_from_expr fxy (e as _ `|-> _) =
let
- val (es, e) = unfold_abs e
+ val (es, e) = CodegenThingol.unfold_abs e
in
brackify BR (
str "\\"
- :: map (hs_from_expr BR) es @ [
+ :: map (hs_from_expr BR o fst) es @ [
str "->",
hs_from_expr NOBR e
])
end
- | hs_from_expr fxy (e as ICase (_, [_])) =
+ | hs_from_expr fxy (e as IAbs _) =
let
- val (ps, body) = unfold_let e;
- fun mk_bind (p, e) = Pretty.block [
+ val (es, e) = CodegenThingol.unfold_abs e
+ in
+ brackify BR (
+ str "\\"
+ :: map (hs_from_expr BR o fst) es @ [
+ str "->",
+ hs_from_expr NOBR e
+ ])
+ end
+ | hs_from_expr fxy (e as ICase ((_, [_]), _)) =
+ let
+ val (ps, body) = CodegenThingol.unfold_let e;
+ fun mk_bind ((p, _), e) = (Pretty.block o Pretty.breaks) [
hs_from_expr BR p,
- str " =",
- Pretty.brk 1,
+ str "=",
hs_from_expr NOBR e
];
in Pretty.chunks [
[str ("let"), Pretty.fbrk, map mk_bind ps |> Pretty.chunks] |> Pretty.block,
[str ("in "), hs_from_expr NOBR body] |> Pretty.block
] end
- | hs_from_expr fxy (ICase (e, cs)) =
+ | hs_from_expr fxy (ICase (((de, _), bses), _)) =
let
- fun mk_clause (p, e) =
- Pretty.block [
- hs_from_expr NOBR p,
- str " ->",
- Pretty.brk 1,
- hs_from_expr NOBR e
+ fun mk_clause (se, be) =
+ (Pretty.block o Pretty.breaks) [
+ hs_from_expr NOBR se,
+ str "->",
+ hs_from_expr NOBR be
]
in Pretty.block [
str "case",
Pretty.brk 1,
- hs_from_expr NOBR e,
+ hs_from_expr NOBR de,
Pretty.brk 1,
str "of",
Pretty.fbrk,
- (Pretty.chunks o map mk_clause) cs
+ (Pretty.chunks o map mk_clause) bses
] end
and hs_mk_app c es =
(str o resolv) c :: map (hs_from_expr BR) es
@@ -954,11 +968,11 @@
hs_from_expr NOBR rhs
]
in Pretty.chunks (map (from_eq name) eqs) end;
- fun hs_from_def (name, Undef) =
+ fun hs_from_def (name, CodegenThingol.Undef) =
error ("empty statement during serialization: " ^ quote name)
- | hs_from_def (name, Prim prim) =
+ | hs_from_def (name, CodegenThingol.Prim prim) =
from_prim resolv_here (name, prim)
- | hs_from_def (name, Fun (eqs, (sctxt, ty))) =
+ | hs_from_def (name, CodegenThingol.Fun (eqs, (sctxt, ty))) =
let
val body = hs_from_funeqs (name, eqs);
in if with_typs then
@@ -971,15 +985,15 @@
body
] |> SOME
else SOME body end
- | hs_from_def (name, Typesyn (vs, ty)) =
+ | hs_from_def (name, CodegenThingol.Typesyn (sctxt, ty)) =
Pretty.block [
str "type ",
- hs_from_sctxt_tycoexpr (vs, (resolv_here name, map (IVarT o fst) vs)),
+ hs_from_sctxt_tycoexpr (sctxt, (resolv_here name, map (ITyVar o fst) sctxt)),
str " =",
Pretty.brk 1,
hs_from_sctxt_type ([], ty)
] |> SOME
- | hs_from_def (name, Datatype (vs, constrs)) =
+ | hs_from_def (name, CodegenThingol.Datatype (sctxt, constrs)) =
let
fun mk_cons (co, tys) =
(Pretty.block o Pretty.breaks) (
@@ -989,7 +1003,7 @@
in
Pretty.block ((
str "data "
- :: hs_from_sctxt_type (vs, IType (resolv_here name, map (IVarT o fst) vs))
+ :: hs_from_sctxt_tycoexpr (sctxt, (resolv_here name, map (ITyVar o fst) sctxt))
:: str " ="
:: Pretty.brk 1
:: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs)
@@ -998,9 +1012,9 @@
str "deriving Show"
])
end |> SOME
- | hs_from_def (_, Datatypecons _) =
+ | hs_from_def (_, CodegenThingol.Datatypecons _) =
NONE
- | hs_from_def (name, Class (supclasss, (v, membrs))) =
+ | hs_from_def (name, CodegenThingol.Class (supclasss, (v, membrs))) =
let
fun mk_member (m, (sctxt, ty)) =
Pretty.block [
@@ -1018,14 +1032,14 @@
Pretty.chunks (map mk_member membrs)
] |> SOME
end
- | hs_from_def (name, Classmember _) =
+ | hs_from_def (name, CodegenThingol.Classmember _) =
NONE
- | hs_from_def (_, Classinst (((clsname, (tyco, arity)), _), memdefs)) =
+ | hs_from_def (_, CodegenThingol.Classinst (((clsname, (tyco, arity)), _), memdefs)) =
Pretty.block [
str "instance ",
- hs_from_sctxt_tycoexpr (arity, (clsname, map (IVarT o fst) arity)),
+ hs_from_sctxt_tycoexpr (arity, (clsname, map (ITyVar o fst) arity)),
str " ",
- hs_from_sctxt_tycoexpr (arity, (tyco, map (IVarT o fst) arity)),
+ 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)
@@ -1045,7 +1059,7 @@
"import", "default", "forall", "let", "in", "class", "qualified", "data",
"newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
] @ [
- "Bool", "Integer", "Maybe", "True", "False", "Nothing", "Just", "negate"
+ "Bool", "Integer", "Maybe", "True", "False", "Nothing", "Just", "not", "negate"
];
fun hs_from_module imps ((_, name), ps) =
(Pretty.chunks) (
@@ -1070,7 +1084,7 @@
fun preprocess const_syntax module =
module
|> debug 3 (fn _ => "eta-expanding...")
- |> eta_expand (eta_expander const_syntax)
+ |> CodegenThingol.eta_expand (eta_expander const_syntax)
in
(Scan.optional (OuterParse.name >> (fn "no_typs" => false | s => Scan.fail_with (fn _ => "illegal flag: " ^ quote s) true)) true
#-> (fn with_typs => parse_multi_file ((K o K) NONE) "hs" (serializer with_typs)))
--- a/src/Pure/Tools/codegen_thingol.ML Wed Mar 01 10:37:00 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Wed Mar 01 13:47:42 2006 +0100
@@ -5,53 +5,58 @@
Intermediate language ("Thin-gol") for code extraction.
*)
+infix 8 `%%;
+infixr 6 `->;
+infixr 6 `-->;
+infix 4 `$;
+infix 4 `$$;
+infixr 3 `|->;
+infixr 3 `|-->;
+
signature BASIC_CODEGEN_THINGOL =
sig
type vname = string;
- datatype classlookup = Instance of string * classlookup list list
- | Lookup of class list * (string * int);
+ type sortcontext = ClassPackage.sortcontext;
+ datatype iclasslookup = Instance of string * iclasslookup list list
+ | Lookup of class list * (string * int);
datatype itype =
- IType of string * itype list
- | IFun of itype * itype
- | IVarT of vname;
- type ityp = ClassPackage.sortcontext * itype;
+ `%% of string * itype list
+ | `-> of itype * itype
+ | ITyVar of vname;
datatype iexpr =
- IConst of (string * itype) * classlookup list list
- | IVarE of vname * itype
- | IApp of iexpr * iexpr
- | IAbs of iexpr * iexpr
- | ICase of iexpr * (iexpr * iexpr) list;
+ IConst of (string * itype) * iclasslookup list list
+ | IVar of vname
+ | `$ of iexpr * iexpr
+ | `|-> of (vname * itype) * iexpr
+ | IAbs of ((iexpr * itype) * iexpr) * iexpr
+ (* (((binding expression (ve), binding type (vty)),
+ body expression (be)), native expression (e0)) *)
+ | ICase of ((iexpr * itype) * (iexpr * iexpr) list) * iexpr;
+ (* ((discrimendum expression (de), discrimendum type (dty)),
+ [(selector expression (se), body expression (be))]),
+ native expression (e0)) *)
end;
signature CODEGEN_THINGOL =
sig
include BASIC_CODEGEN_THINGOL;
- val mk_funs: itype list * itype -> itype;
- val mk_apps: iexpr * iexpr list -> iexpr;
- val mk_abss: iexpr list * iexpr -> iexpr;
+ val `--> : itype list * itype -> itype;
+ val `$$ : iexpr * iexpr list -> iexpr;
+ val `|--> : (vname * itype) list * iexpr -> iexpr;
val pretty_itype: itype -> Pretty.T;
val pretty_iexpr: iexpr -> Pretty.T;
val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list;
val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a;
val unfold_fun: itype -> itype list * itype;
val unfold_app: iexpr -> iexpr * iexpr list;
- val unfold_abs: iexpr -> iexpr list * iexpr;
- val unfold_let: iexpr -> (iexpr * iexpr) list * iexpr;
+ val unfold_abs: iexpr -> (iexpr * itype) list * iexpr;
+ val unfold_let: iexpr -> ((iexpr * itype) * iexpr) list * iexpr;
val unfold_const_app: iexpr ->
- (((string * itype) * classlookup list list) * iexpr list) option;
+ (((string * itype) * iclasslookup list list) * iexpr list) option;
val ensure_pat: iexpr -> iexpr;
- val itype_of_iexpr: iexpr -> itype;
- val `%% : string * itype list -> itype;
- val `-> : itype * itype -> itype;
- val `--> : itype list * itype -> itype;
- val `$ : iexpr * iexpr -> iexpr;
- val `$$ : iexpr * iexpr list -> iexpr;
- val `|-> : iexpr * iexpr -> iexpr;
- val `|--> : iexpr list * iexpr -> iexpr;
-
- type funn = (iexpr list * iexpr) list * ityp;
- type datatyp = ClassPackage.sortcontext * (string * itype list) list;
+ type funn = (iexpr list * iexpr) list * (sortcontext * itype);
+ type datatyp = sortcontext * (string * itype list) list;
datatype prim =
Pretty of Pretty.T
| Name;
@@ -62,10 +67,10 @@
| Typesyn of (vname * sort) list * itype
| Datatype of datatyp
| Datatypecons of string
- | Class of class list * (vname * (string * ityp) list)
+ | Class of class list * (vname * (string * (sortcontext * itype)) list)
| Classmember of class
| Classinst of ((class * (string * (vname * sort) list))
- * (class * (string * classlookup list list)) list)
+ * (class * (string * iclasslookup list list)) list)
* (string * (string * funn)) list;
type module;
type transact;
@@ -144,31 +149,25 @@
(* language representation *)
-infix 8 `%%;
-infixr 6 `->;
-infixr 6 `-->;
-infix 4 `$;
-infix 4 `$$;
-infixr 3 `|->;
-infixr 3 `|-->;
-
type vname = string;
-datatype classlookup = Instance of string * classlookup list list
- | Lookup of class list * (string * int);
+type sortcontext = ClassPackage.sortcontext;
+datatype iclasslookup = Instance of string * iclasslookup list list
+ | Lookup of class list * (string * int);
datatype itype =
- IType of string * itype list
- | IFun of itype * itype
- | IVarT of vname;
-type ityp = ClassPackage.sortcontext * itype;
+ `%% of string * itype list
+ | `-> of itype * itype
+ | ITyVar of vname;
datatype iexpr =
- IConst of (string * itype) * classlookup list list
- | IVarE of vname * itype
- | IApp of iexpr * iexpr
- | IAbs of iexpr * iexpr
- | ICase of iexpr * (iexpr * iexpr) list;
+ IConst of (string * itype) * iclasslookup list list
+ | IVar of vname
+ | `$ of iexpr * iexpr
+ | `|-> of (vname * itype) * iexpr
+ | IAbs of ((iexpr * itype) * iexpr) * iexpr
+ | ICase of ((iexpr * itype) * (iexpr * iexpr) list) * iexpr;
+ (*see also signature*)
(*
variable naming conventions
@@ -194,64 +193,62 @@
constructors (co, tys) constr
*)
-val mk_funs = Library.foldr IFun;
-val mk_apps = Library.foldl IApp;
-val mk_abss = Library.foldr IAbs;
-
-val op `%% = IType;
-val op `-> = IFun;
-val op `$ = IApp;
-val op `|-> = IAbs;
-val op `--> = mk_funs;
-val op `$$ = mk_apps;
-val op `|--> = mk_abss;
+val op `--> = Library.foldr (op `->);
+val op `$$ = Library.foldl (op `$);
+val op `|--> = Library.foldr (op `|->);
val pretty_sortcontext =
Pretty.commas o map (fn (v, sort) => (Pretty.block o Pretty.breaks)
[Pretty.str v, Pretty.str "::", Pretty.enum "&" "" "" (map Pretty.str sort)]);
-fun pretty_itype (IType (tyco, tys)) =
- Pretty.enum "" "(" ")" (Pretty.str tyco :: map pretty_itype tys)
- | pretty_itype (IFun (ty1, ty2)) =
+fun pretty_itype (tyco `%% tys) =
+ Pretty.block (Pretty.str tyco :: map pretty_itype tys)
+ | pretty_itype (ty1 `-> ty2) =
Pretty.enum "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
- | pretty_itype (IVarT v) =
+ | pretty_itype (ITyVar v) =
Pretty.str v;
-fun pretty_iexpr (IConst ((c, ty), _)) =
- Pretty.block [Pretty.str (c ^ "::"), pretty_itype ty]
- | pretty_iexpr (IVarE (v, ty)) =
- Pretty.block [Pretty.str ("?" ^ v ^ "::"), pretty_itype ty]
- | pretty_iexpr (IApp (e1, e2)) =
- Pretty.enclose "(" ")" [pretty_iexpr e1, Pretty.brk 1, pretty_iexpr e2]
- | pretty_iexpr (IAbs (e1, e2)) =
- Pretty.enclose "(" ")" [pretty_iexpr e1, Pretty.brk 1, Pretty.str "|->", Pretty.brk 1, pretty_iexpr e2]
- | pretty_iexpr (ICase (e, cs)) =
- Pretty.enclose "(" ")" [
- Pretty.str "case ",
+fun pretty_iexpr (IConst ((c, _), _)) =
+ Pretty.str c
+ | pretty_iexpr (IVar v) =
+ Pretty.str ("?" ^ v)
+ | pretty_iexpr (e1 `$ e2) =
+ (Pretty.enclose "(" ")" o Pretty.breaks)
+ [pretty_iexpr e1, pretty_iexpr e2]
+ | 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 (IAbs (((e1, _), e2), _)) =
+ (Pretty.enclose "(" ")" o Pretty.breaks)
+ [pretty_iexpr e1, Pretty.str "|->", pretty_iexpr e2]
+ | pretty_iexpr (ICase (((e, _), cs), _)) =
+ (Pretty.enclose "(" ")" o Pretty.breaks) [
+ Pretty.str "case",
pretty_iexpr e,
Pretty.enclose "(" ")" (map (fn (p, e) =>
- Pretty.block [
+ (Pretty.block o Pretty.breaks) [
pretty_iexpr p,
- Pretty.str " => ",
+ Pretty.str "=>",
pretty_iexpr e
]
) cs)
];
val unfold_fun = unfoldr
- (fn IFun t => SOME t
+ (fn op `-> t => SOME t
| _ => NONE);
val unfold_app = unfoldl
- (fn IApp e => SOME e
+ (fn op `$ e => SOME e
| _ => NONE);
val unfold_abs = unfoldr
- (fn IAbs b => SOME b
+ (fn (v, ty) `|-> e => SOME ((IVar v, ty), e)
+ | IAbs (((e1, ty), e2), _) => SOME ((e1, ty), e2)
| _ => NONE)
val unfold_let = unfoldr
- (fn ICase (e, [(p, e')]) => SOME ((p, e), e')
+ (fn ICase (((de, dty), [(se, be)]), _) => SOME (((se, dty), de), be)
| _ => NONE);
fun unfold_const_app e =
@@ -259,59 +256,36 @@
of (IConst x, es) => SOME (x, es)
| _ => NONE;
-fun map_itype f_itype (IType (tyco, tys)) =
- tyco `%% map f_itype tys
- | map_itype f_itype (IFun (t1, t2)) =
- f_itype t1 `-> f_itype t2
- | map_itype _ (ty as IVarT _) =
- ty;
+fun map_itype _ (ty as ITyVar _) =
+ ty
+ | map_itype f (tyco `%% tys) =
+ tyco `%% map f tys
+ | map_itype f (t1 `-> t2) =
+ f t1 `-> f t2;
-fun map_iexpr f (IApp (e1, e2)) =
- f e1 `$ f e2
- | map_iexpr f (IAbs (v, e)) =
- v `|-> f e
- | map_iexpr f (ICase (e, ps)) =
- ICase (f e, map (fn (p, e) => (f p, f e)) ps)
- | map_iexpr _ (e as IConst _) =
+fun map_iexpr _ (e as IConst _) =
e
- | map_iexpr _ (e as IVarE _) =
- e;
-
-fun map_atype f (ty as IVarT _) =
- f ty
- | map_atype f ty =
- map_itype (map_atype f) ty;
-
-fun map_aexpr f (e as IConst _) =
- f e
- | map_aexpr f (e as IVarE _) =
- f e
- | map_aexpr f e =
- map_iexpr (map_aexpr f) e;
+ | map_iexpr _ (e as IVar _) =
+ e
+ | map_iexpr f (e1 `$ e2) =
+ f e1 `$ f e2
+ | map_iexpr f ((v, ty) `|-> e) =
+ (v, ty) `|-> f e
+ | map_iexpr f (IAbs (((ve, vty), be), e0)) =
+ IAbs (((f ve, vty), f be), e0)
+ | map_iexpr f (ICase (((de, dty), bses), e0)) =
+ ICase (((f de, dty), map (fn (se, be) => (f se, f be)) bses), e0);
fun map_iexpr_itype f =
let
- fun mapp (IConst ((c, ty), ctxt)) = IConst ((c, f ty), ctxt)
- | mapp (IVarE (v, ty)) = IVarE (v, f ty)
- in map_aexpr mapp end;
-
-fun fold_atype f (IFun (ty1, ty2)) =
- fold_atype f ty1 #> fold_atype f ty2
- | fold_atype f (ty as IType _) =
- f ty
- | fold_atype f (ty as IVarT _) =
- f ty;
-
-fun fold_aexpr f (IApp (e1, e2)) =
- fold_aexpr f e1 #> fold_aexpr f e2
- | fold_aexpr f (IAbs (v, e)) =
- fold_aexpr f e
- | fold_aexpr f (ICase (e, ps)) =
- fold_aexpr f e #> fold (fn (p, e) => fold_aexpr f p #> fold_aexpr f e) ps
- | fold_aexpr f (e as IConst _) =
- f e
- | fold_aexpr f (e as IVarE _) =
- f e;
+ fun mapp (IConst ((c, ty), sctxt)) = IConst ((c, f ty), sctxt)
+ | mapp ((v, ty) `|-> e) = (v, f ty) `|-> mapp e
+ | mapp (IAbs (((ve, vty), be), e0)) =
+ IAbs (((mapp ve, f vty), mapp be), e0)
+ | mapp (ICase (((de, dty), bses), e0)) =
+ ICase (((mapp de, f dty), map (fn (se, be) => (mapp se, mapp be)) bses), e0)
+ | mapp e = map_iexpr mapp e;
+ in mapp end;
fun eq_ityp ((sctxt1, ty1), (sctxt2, ty2)) =
let
@@ -322,18 +296,18 @@
| SOME v' => case AList.lookup (op =) sctxt2 v'
of NONE => raise NO_MATCH
| SOME sort' => if sort <> sort' then raise NO_MATCH else ()) sctxt1
- fun eq (IVarT v1) (IVarT v2) subs =
+ fun eq (ITyVar v1) (ITyVar v2) subs =
(case AList.lookup (op =) subs v1
of NONE => subs |> AList.update (op =) (v1, v2)
| SOME v1' =>
if v1' <> v2
then raise NO_MATCH
else subs)
- | eq (IType (tyco1, tys1)) (IType (tyco2, tys2)) subs =
+ | eq (tyco1 `%% tys1) (tyco2 `%% tys2) subs =
if tyco1 <> tyco2
then raise NO_MATCH
else subs |> fold2 eq tys1 tys2
- | eq (IFun (ty11, ty12)) (IFun (ty21, ty22)) subs =
+ | eq (ty11 `-> ty12) (ty21 `-> ty22) subs =
subs |> eq ty11 ty21 |> eq ty12 ty22
| eq _ _ _ = raise NO_MATCH;
in
@@ -343,44 +317,36 @@
fun instant_itype f =
let
- fun instant (IVarT x) = f x
+ fun instant (ITyVar x) = f x
| instant y = map_itype instant y;
in map_itype instant end;
-fun itype_of_iexpr (IConst ((_, ty), s)) = ty
- | itype_of_iexpr (IVarE (_, ty)) = ty
- | itype_of_iexpr (e as IApp (e1, e2)) = (case itype_of_iexpr e1
- of (IFun (ty2, ty')) =>
- if ty2 = itype_of_iexpr e2
- then ty'
- else error ("inconsistent application: in " ^ Pretty.output (pretty_iexpr e)
- ^ ", " ^ (Pretty.output o pretty_itype) ty2
- ^ " vs. " ^ (Pretty.output o pretty_itype o itype_of_iexpr) e2)
- | _ => error ("expression is not a function: " ^ Pretty.output (pretty_iexpr e1)))
- | itype_of_iexpr (IAbs (e1, e2)) = itype_of_iexpr e1 `-> itype_of_iexpr e2
- | itype_of_iexpr (ICase ((_, [(_, e)]))) = itype_of_iexpr e;
-
fun ensure_pat (e as IConst (_, [])) = e
- | ensure_pat (e as IVarE _) = e
- | ensure_pat (e as IApp (e1, e2)) =
- (ensure_pat e1 `$ ensure_pat e2; 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 type_vnames ty =
- let
- fun extr (IVarT v) =
- insert (op =) v
- | extr _ = I;
- in fold_atype extr ty end;
+fun has_tyvars (_ `%% tys) =
+ exists has_tyvars tys
+ | has_tyvars (ITyVar _) =
+ true
+ | has_tyvars (ty1 `-> ty2) =
+ has_tyvars ty1 orelse has_tyvars ty2;
-fun expr_names e =
- let
- fun extr (IConst ((c, _), _)) =
- insert (op =) c
- | extr (IVarE (v, _)) =
- insert (op =) v
- in fold_aexpr extr e end;
+fun varnames_of (IConst ((c, _), _)) =
+ I
+ | varnames_of (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;
fun invent seed used =
let
@@ -393,8 +359,8 @@
(* type definitions *)
-type funn = (iexpr list * iexpr) list * ityp;
-type datatyp = ClassPackage.sortcontext * (string * itype list) list;
+type funn = (iexpr list * iexpr) list * (sortcontext * itype);
+type datatyp = sortcontext * (string * itype list) list;
datatype prim =
Pretty of Pretty.T
@@ -407,10 +373,10 @@
| Typesyn of (vname * sort) list * itype
| Datatype of datatyp
| Datatypecons of string
- | Class of class list * (vname * (string * ityp) list)
+ | Class of class list * (vname * (string * (sortcontext * itype)) list)
| Classmember of class
| Classinst of ((class * (string * (vname * sort) list))
- * (class * (string * classlookup list list)) list)
+ * (class * (string * iclasslookup list list)) list)
* (string * (string * funn)) list;
datatype node = Def of def | Module of node Graph.T;
@@ -784,14 +750,14 @@
then error "too many member definitions given"
else ();
fun instant (w, ty) v =
- if v = w then ty else IVarT v;
+ if v = w then ty else ITyVar v;
fun mk_memdef (m, (sortctxt, ty)) =
case AList.lookup (op =) memdefs m
of NONE => error ("missing definition for member " ^ quote m)
| SOME (m', (eqs, (sortctxt', ty'))) =>
if eq_ityp
((sortctxt |> fold (fn v_sort => AList.update (op =) v_sort) arity,
- instant_itype (instant (v, tyco `%% map (IVarT o fst) arity)) ty),
+ instant_itype (instant (v, tyco `%% map (ITyVar o fst) arity)) ty),
(sortctxt', ty'))
then (m, (m', (check_funeqs eqs, (sortctxt', ty'))))
else error ("inconsistent type for member definition " ^ quote m)
@@ -926,28 +892,25 @@
(fst o unfold_fun) ty
|> curry Library.drop (length es)
|> curry Library.take add_n
- val add_vars =
- map2 (curry IVarE) (Term.invent_names (fold expr_names es []) "x" add_n) tys;
+ val vs = (Term.invent_names (fold varnames_of es []) "x" add_n)
in
- add_vars `|--> IConst ((f, ty), ls) `$$ map eta es `$$ add_vars
+ vs ~~ tys `|--> IConst ((f, ty), ls) `$$ 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;
val eta_expand_poly =
let
- fun eta (funn as ([([], e)], cty as (sortctxt, (ty as IFun (ty1, ty2))))) =
- if (not o null) sortctxt
- orelse null (type_vnames ty [])
+ fun eta (funn as ([([], e)], cty as (sctxt, (ty as (ty1 `-> ty2))))) =
+ if (not o null) sctxt
+ orelse (not o has_tyvars) ty
then funn
- else
- (case unfold_abs e
- of ([], e) =>
- let
- val add_var = IVarE (hd (Term.invent_names (expr_names e []) "x" 1), ty1)
- in (([([add_var], e `$ add_var)], cty)) end
- | eq =>
- (([eq], cty)))
+ else (case unfold_abs e
+ of ([], e) =>
+ let
+ val add_var = IVar (hd (Term.invent_names (varnames_of e []) "x" 1))
+ in (([([add_var], e `$ add_var)], cty)) end
+ | _ => funn)
| eta funn = funn;
in (map_defs o map_def_fun) eta end;
@@ -956,13 +919,13 @@
fun unclash (eqs, (sortctxt, ty)) =
let
val used_expr =
- fold (fn (pats, rhs) => fold expr_names pats #> expr_names rhs) eqs [];
+ fold (fn (pats, rhs) => fold varnames_of pats #> varnames_of 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;
val rename =
perhaps (AList.lookup (op =) rename_map);
- val rename_typ = instant_itype (IVarT o rename);
+ val rename_typ = instant_itype (ITyVar o rename);
val rename_expr = map_iexpr_itype rename_typ;
fun rename_eq (args, rhs) = (map rename_expr args, rename_expr rhs)
in
--- a/src/Pure/Tools/nbe.ML Wed Mar 01 10:37:00 2006 +0100
+++ b/src/Pure/Tools/nbe.ML Wed Mar 01 13:47:42 2006 +0100
@@ -44,8 +44,9 @@
val modl_old = CodegenThingol.partof (Symtab.keys nbe_tab)
(CodegenPackage.get_root_module thy);
val (t', thy') = CodegenPackage.codegen_term t thy
- val modl_new = CodegenPackage.get_root_module thy;
- val diff = CodegenThingol.diff_module (modl_old, modl_new);
+ val modl_new = CodegenPackage.get_root_module thy';
+ val diff = CodegenThingol.diff_module (modl_new, modl_old);
+ val _ = writeln ("new definitions: " ^ (commas o map fst) diff);
val _ = (tab := nbe_tab;
Library.seq (use_show o NBE_Codegen.generate defined) diff)
val thy'' = NBE_Data.put (!tab) thy'
--- a/src/Pure/Tools/nbe_codegen.ML Wed Mar 01 10:37:00 2006 +0100
+++ b/src/Pure/Tools/nbe_codegen.ML Wed Mar 01 13:47:42 2006 +0100
@@ -10,7 +10,6 @@
fun MLname
val quote = quote;
-FIXME CodegenThingol names!
*)
signature NBE_CODEGEN =
@@ -86,46 +85,53 @@
S.abs (S.tup []) (S.app Eval_C
(S.quote nm))]);
+open BasicCodegenThingol;
fun mk_rexpr defined nm ar =
let fun mk args t = case t of
- CodegenThingol.IConst((s,_),_) =>
+ 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 ])
- | CodegenThingol.IVarE(s,_) => S.nbe_apps (MLvname s) args
- | CodegenThingol.IApp(e1,e2) => mk (args @ [mk [] e2]) e1
- | CodegenThingol.IAbs(CodegenThingol.IVarE(nm,_), e) =>
+ | 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
| _ => sys_error "NBE mkexpr"
in mk [] end;
val mk_lexpr =
let fun mk args t = case t of
- CodegenThingol.IConst((s,_),_) =>
+ IConst((s,_),_) =>
S.app Eval_Constr (S.tup [S.quote s, S.list args])
- | CodegenThingol.IVarE(s,_) => if args = [] then MLvname s else
+ | IVar s => if args = [] then MLvname s else
sys_error "NBE mk_lexpr illegal higher order pattern"
- | CodegenThingol.IApp(e1,e2) => mk (args @ [mk [] e2]) e1
+ | e1 `$ e2 => mk (args @ [mk [] e2]) e1
+ | IAbs (_, e) => mk args e
+ | ICase (_, e) => mk args e
| _ => sys_error "NBE mk_lexpr illegal pattern"
in mk [] end;
fun mk_eqn defined nm ar (lhs,e) =
([S.list(map mk_lexpr (rev lhs))], mk_rexpr defined nm ar e);
-fun funs_of_expr(CodegenThingol.IConst((s,_),_),fs) = s::fs
- | funs_of_expr(CodegenThingol.IApp(e1,e2),fs) =
- funs_of_expr(e1, funs_of_expr(e2, fs))
- | funs_of_expr(CodegenThingol.IAbs(_, e),fs) = funs_of_expr(e,fs)
- | funs_of_expr(_,fs) = fs;
+fun funs_of_expr (IConst ((s, _), _)) = insert (op =) s
+ | funs_of_expr (e1 `$ e2) =
+ funs_of_expr e1 #> funs_of_expr e2
+ | funs_of_expr (_ `|-> e) = funs_of_expr e
+ | funs_of_expr (IAbs (_, e)) = funs_of_expr e
+ | funs_of_expr (ICase (_, e)) = funs_of_expr e
+ | funs_of_expr _ = I;
fun lookup nm = S.Val (MLname nm) (tab_lookup (S.quote nm));
-fun generate defined (nm,CodegenThingol.Fun(eqns,_)) =
+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) => funs_of_expr(e,[])) eqns) \ nm;
+ val funs = Library.flat(map (fn (_,e) => funs_of_expr e []) eqns) \ 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 Wed Mar 01 10:37:00 2006 +0100
+++ b/src/Pure/Tools/nbe_eval.ML Wed Mar 01 13:47:42 2006 +0100
@@ -127,21 +127,24 @@
(* greetings to Tarski *)
-structure IL = CodegenThingol
+open BasicCodegenThingol;
-fun eval(IL.IConst((f,_),_)) xs = lookup f
- | eval(IL.IVarE(n,_)) xs =
- (case AList.lookup (op =) xs n of NONE => Var(n,[])
- | SOME v => v)
- | eval(IL.IApp(s,t)) xs = apply (eval s xs) (eval t xs)
- | eval(IL.IAbs(IL.IVarE(n,_), t)) xs =
- Fun (fn [x] => eval t ((n,x)::xs), [], 1,
- fn () => let val var = new_name() in
- AbsN(var, to_term (eval t ((n,BVar(var,[])) :: xs))) end);
+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,
+ [], 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;
(* finally... *)
-fun nbe tab t = (counter :=0; xfun_tab := tab; to_term(eval t []));
+fun nbe tab t = (counter :=0; xfun_tab := tab; to_term(eval [] t));
end;