--- a/src/Pure/Tools/codegen_package.ML Wed Feb 01 12:22:47 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML Wed Feb 01 12:23:14 2006 +0100
@@ -82,8 +82,8 @@
infixr 6 `-->;
infix 4 `$;
infix 4 `$$;
-infixr 5 `|->;
-infixr 5 `|-->;
+infixr 3 `|->;
+infixr 3 `|-->;
(* auxiliary *)
@@ -100,6 +100,7 @@
(* shallow name spaces *)
+val nsp_module = ""; (* a dummy by convention *)
val nsp_class = "class";
val nsp_tyco = "tyco";
val nsp_const = "const";
@@ -189,14 +190,14 @@
#ml CodegenSerializer.serializers
|> apsnd (fn seri => seri
(nsp_dtcon, nsp_class, K false)
- [[nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_class, nsp_mem, nsp_inst]]
+ [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_class, nsp_mem, nsp_inst]]
)
)
|> Symtab.update (
#haskell CodegenSerializer.serializers
|> apsnd (fn seri => seri
nsp_dtcon
- [[nsp_class], [nsp_tyco], [nsp_const, nsp_overl, nsp_mem], [nsp_dtcon], [nsp_inst]]
+ [[nsp_module], [nsp_class], [nsp_tyco], [nsp_const, nsp_overl, nsp_mem], [nsp_dtcon], [nsp_inst]]
)
)
);
@@ -499,7 +500,7 @@
#ml CodegenSerializer.serializers
|> apsnd (fn seri => seri
(nsp_dtcon, nsp_class, fn tyco' => tyco' = idf_of_name thy nsp_tyco tyco )
- [[nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst]]
+ [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst]]
)
)
); thy);
@@ -546,7 +547,7 @@
end
and exprgen_tyvar_sort thy tabs (v, sort) trns =
trns
- |> fold_map (ensure_def_class thy tabs) (ClassPackage.syntactic_sort_of thy sort)
+ |> fold_map (ensure_def_class thy tabs) (ClassPackage.operational_sort_of thy sort)
|-> (fn sort => pair (unprefix "'" v, sort))
and exprgen_type thy tabs (TVar _) trns =
error "TVar encountered during code generation"
@@ -565,16 +566,15 @@
||>> fold_map (exprgen_type thy tabs) tys
|-> (fn (tyco, tys) => pair (tyco `%% tys));
-fun mk_lookup thy tabs (ClassPackage.Instance (inst as (cls, tyco), ls)) trns =
+fun exprgen_classlookup thy tabs (ClassPackage.Instance (inst, ls)) trns =
trns
- |> ensure_def_class thy tabs cls
- ||>> ensure_def_inst thy tabs inst
- ||>> (fold_map o fold_map) (mk_lookup thy tabs) ls
- |-> (fn ((cls, i), ls) => pair (ClassPackage.Instance ((cls, i), ls)))
- | mk_lookup thy tabs (ClassPackage.Lookup (clss, (v, i))) trns =
+ |> ensure_def_inst thy tabs inst
+ ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs) ls
+ |-> (fn (inst, ls) => pair (Instance (inst, ls)))
+ | exprgen_classlookup thy tabs (ClassPackage.Lookup (clss, (v, i))) trns =
trns
|> fold_map (ensure_def_class thy tabs) clss
- |-> (fn clss => pair (ClassPackage.Lookup (clss, (v |> unprefix "'", i))))
+ |-> (fn clss => pair (Lookup (clss, (v |> unprefix "'", i))))
and mk_fun thy tabs (c, ty) trns =
case get_first (fn eqx => eqx (c, ty)) (get_eqextrs thy tabs)
of SOME (eq_thms, ty) =>
@@ -597,14 +597,9 @@
|-> (fn (args, rhs) => pair (args, rhs))
in
trns
- |> debug 6 (fn _ => "(1) retrieved function equations for " ^
- quote (c ^ "::" ^ Sign.string_of_typ thy ty))
|> fold_map (mk_eq o dest_eqthm) eq_thms
- |> debug 6 (fn _ => "(2) building equations")
||>> (exprgen_type thy tabs o devarify_type) ty
- |> debug 6 (fn _ => "(3) building type")
||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt
- |> debug 6 (fn _ => "(4) building sort context")
|-> (fn ((eqs, ty), sortctxt) => (pair o SOME) (eqs, (sortctxt, ty)))
end
| NONE => (NONE, trns)
@@ -612,15 +607,15 @@
let
fun defgen_inst thy (tabs as (_, (insttab, _, _))) inst trns =
case Option.map (InstNameMangler.rev thy insttab) (name_of_idf thy nsp_inst inst)
- of SOME (_, (cls, tyco)) =>
+ of SOME (_, (class, tyco)) =>
let
- val (arity, memdefs) = ClassPackage.the_inst_sign thy (cls, tyco);
+ val (arity, memdefs) = ClassPackage.the_inst_sign thy (class, tyco);
fun gen_suparity supclass trns =
trns
- |> ensure_def_inst thy tabs (supclass, tyco)
- ||>> (fold_map o fold_map) (mk_lookup thy tabs)
- (ClassPackage.extract_sortlookup_inst thy (cls, tyco) supclass)
- |-> (fn (inst, ls) => pair (supclass, (inst, ls)));
+ |> (fold_map o fold_map) (exprgen_classlookup thy tabs)
+ (ClassPackage.extract_classlookup_inst thy (supclass, tyco) supclass)
+ ||>> ensure_def_inst thy tabs (supclass, tyco)
+ |-> (fn (ls, _) => pair (supclass, ls));
fun gen_membr (m, ty) trns =
trns
|> mk_fun thy tabs (m, ty)
@@ -630,18 +625,13 @@
trns
|> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls
^ ", " ^ quote tyco ^ ")")
- |> ensure_def_class thy tabs cls
- |> debug 5 (fn _ => "(1) got class")
+ |> ensure_def_class thy tabs class
||>> ensure_def_tyco thy tabs tyco
- |> debug 5 (fn _ => "(2) got type")
||>> fold_map (exprgen_tyvar_sort thy tabs) arity
- |> debug 5 (fn _ => "(3) got arity")
- ||>> fold_map gen_suparity (ClassPackage.the_superclasses thy cls)
- |> debug 5 (fn _ => "(4) got superarities")
+ ||>> fold_map gen_suparity (ClassPackage.the_superclasses thy class)
||>> fold_map gen_membr memdefs
- |> debug 5 (fn _ => "(5) got members")
- |-> (fn ((((cls, tyco), arity), suparities), memdefs) =>
- succeed (Classinst (((cls, (tyco, arity)), suparities), memdefs)))
+ |-> (fn ((((class, tyco), arity), suparities), memdefs) =>
+ succeed (Classinst (((class, (tyco, arity)), suparities), memdefs)))
end
| _ =>
trns |> fail ("no class instance found for " ^ quote inst);
@@ -732,8 +722,8 @@
and appgen_default thy tabs ((c, ty), ts) trns =
trns
|> ensure_def_const thy tabs (c, ty)
- ||>> (fold_map o fold_map) (mk_lookup thy tabs)
- (ClassPackage.extract_sortlookup thy (c, ty))
+ ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
+ (ClassPackage.extract_classlookup thy (c, ty))
||>> (exprgen_type thy tabs o devarify_type) ty
||>> fold_map (exprgen_term thy tabs o devarify_term) ts
|-> (fn (((c, ls), ty), es) =>
@@ -845,7 +835,7 @@
trns
|> exprgen_term thy tabs p
||>> exprgen_term thy tabs body
- |-> (fn (IVarE v, body) => pair (IAbs (v, body)))
+ |-> (fn (IVarE v, body) => pair (v `|-> body))
end;
fun appgen_number_of mk_int_to_nat bin_to_int tyco_int tyco_nat thy tabs ((_,
--- a/src/Pure/Tools/codegen_serializer.ML Wed Feb 01 12:22:47 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Wed Feb 01 12:23:14 2006 +0100
@@ -37,8 +37,8 @@
infixr 6 `-->;
infix 4 `$;
infix 4 `$$;
-infixr 5 `|->;
-infixr 5 `|-->;
+infixr 3 `|->;
+infixr 3 `|-->;
(** generic serialization **)
@@ -366,6 +366,40 @@
#> NameSpace.base
#> translate_string (fn "_" => "__" | "." => "_" | c => c)
#> str;
+ fun ml_from_label' l =
+ Pretty.block [str "#", ml_from_label l];
+ fun ml_from_lookup fxy [] p =
+ p
+ | ml_from_lookup fxy [l] p =
+ brackify fxy [
+ ml_from_label' l,
+ p
+ ]
+ | ml_from_lookup fxy ls p =
+ brackify fxy [
+ Pretty.enum " o" "(" ")" (map ml_from_label' ls),
+ p
+ ];
+ fun ml_from_sortlookup fxy ls =
+ let
+ fun from_classlookup fxy (Instance (inst, lss)) =
+ brackify fxy (
+ (str o resolv) inst
+ :: map (ml_from_sortlookup BR) lss
+ )
+ | from_classlookup fxy (Lookup (classes, (v, ~1))) =
+ ml_from_lookup BR classes (str v)
+ | from_classlookup fxy (Lookup (classes, (v, i))) =
+ ml_from_lookup BR (string_of_int (i+1) :: classes) (str v)
+ in case ls
+ of [l] => from_classlookup fxy l
+ | ls => (Pretty.list "(" ")" o map (from_classlookup NOBR)) ls
+ end;
+ val ml_from_label =
+ resolv
+ #> NameSpace.base
+ #> translate_string (fn "_" => "__" | "." => "_" | c => c)
+ #> str;
fun ml_from_type fxy (IType (tyco, tys)) =
(case tyco_syntax tyco
of NONE =>
@@ -397,95 +431,74 @@
]
end
| ml_from_type _ (IVarT (v, _)) =
- str ("'" ^ v)
- | ml_from_type _ (IDictT fs) =
- Pretty.enum "," "{" "}" (
- map (fn (f, ty) =>
- Pretty.block [ml_from_label f, str ": ", ml_from_type NOBR ty]) fs
- );
- fun ml_from_expr sortctxt fxy (e as IApp (e1, e2)) =
+ str ("'" ^ v);
+ fun ml_from_expr fxy (e as IApp (e1, e2)) =
(case unfold_const_app e
- of SOME x => ml_from_app sortctxt fxy x
+ of SOME x => ml_from_app fxy x
| NONE =>
brackify fxy [
- ml_from_expr sortctxt NOBR e1,
- ml_from_expr sortctxt BR e2
+ ml_from_expr NOBR e1,
+ ml_from_expr BR e2
])
- | ml_from_expr sortctxt fxy (e as IConst x) =
- ml_from_app sortctxt fxy (x, [])
- | ml_from_expr sortctxt fxy (IVarE (v, _)) =
+ | ml_from_expr fxy (e as IConst x) =
+ ml_from_app fxy (x, [])
+ | ml_from_expr fxy (IVarE (v, _)) =
str v
- | ml_from_expr sortctxt fxy (IAbs ((v, _), e)) =
+ | ml_from_expr fxy (IAbs ((v, _), e)) =
brackify fxy [
str ("fn " ^ v ^ " =>"),
- ml_from_expr sortctxt NOBR e
+ ml_from_expr NOBR e
]
- | ml_from_expr sortctxt 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 sortctxt fxy p,
+ ml_from_expr fxy p,
str " =",
Pretty.brk 1,
- ml_from_expr sortctxt NOBR e,
+ ml_from_expr NOBR e,
str ";"
]
in Pretty.chunks [
[str ("let"), Pretty.fbrk, map mk_val ps |> Pretty.chunks] |> Pretty.block,
- [str ("in"), Pretty.fbrk, ml_from_expr sortctxt NOBR e] |> Pretty.block,
+ [str ("in"), Pretty.fbrk, ml_from_expr NOBR e] |> Pretty.block,
str ("end")
] end
- | ml_from_expr sortctxt fxy (ICase (e, c::cs)) =
+ | ml_from_expr fxy (ICase (e, c::cs)) =
let
fun mk_clause definer (p, e) =
Pretty.block [
str definer,
- ml_from_expr sortctxt NOBR p,
+ ml_from_expr NOBR p,
str " =>",
Pretty.brk 1,
- ml_from_expr sortctxt NOBR e
+ ml_from_expr NOBR e
]
in brackify fxy (
str "case"
- :: ml_from_expr sortctxt NOBR e
+ :: ml_from_expr NOBR e
:: mk_clause "of " c
:: map (mk_clause "| ") cs
) end
- | ml_from_expr sortctxt fxy (IDictE fs) =
- Pretty.enum "," "{" "}" (
- map (fn (f, e) =>
- Pretty.block [ml_from_label f, str " = ", ml_from_expr sortctxt NOBR e]) fs
- )
- | ml_from_expr sortctxt fxy (ILookup ([], v)) =
- str v
- | ml_from_expr sortctxt fxy (ILookup ([l], v)) =
- brackify fxy [
- str "#",
- ml_from_label l,
- str v
- ]
- (*| ml_from_expr sortctxt fxy (ILookup (ls, v)) =
- brackify fxy [
- str ("("
- ^ (ls |> map ((fn s => "#" ^ s) o ml_from_label) |> foldr1 (fn (l, e) => l ^ " o " ^ e))
- ^ ")"),
- str v
- ]*)
- | ml_from_expr _ _ e =
+ | ml_from_expr _ e =
error ("dubious expression: " ^ (Pretty.output o pretty_iexpr) e)
- and ml_mk_app sortctxt f es =
+ 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 sortctxt BR) es)]
+ [(str o resolv) f, Pretty.enum " *" "(" ")" (map (ml_from_expr BR) es)]
else
- (str o resolv) f :: map (ml_from_expr sortctxt BR) es
- and ml_from_app sortctxt fxy (((f, _), ls), es) =
- let
- val _ = ();
- in
- from_app (ml_mk_app sortctxt) (ml_from_expr sortctxt) const_syntax fxy (f, es)
- end;
+ (str o resolv) f :: map (ml_from_expr BR) es
+ and ml_from_app fxy (((c, _), lss), es) =
+ case map (ml_from_sortlookup BR) lss
+ of [] =>
+ from_app ml_mk_app ml_from_expr const_syntax fxy (c, es)
+ | lss =>
+ brackify fxy (
+ (str o resolv) c
+ :: (lss
+ @ map (ml_from_expr BR) es)
+ );
fun ml_from_funs (ds as d::ds_tl) =
let
fun mk_definer [] = "val"
@@ -501,15 +514,16 @@
val definer = the (fold check_args ds NONE);
fun mk_eq definer sortctxt f ty (pats, expr) =
let
+ val args = map (str o fst) sortctxt @ map (ml_from_expr BR) pats;
val lhs = [str (definer ^ " " ^ f)]
- @ (if null pats
+ @ (if null args
then [str ":", ml_from_type NOBR ty]
- else map (ml_from_expr sortctxt BR) pats)
- val rhs = [str "=", ml_from_expr sortctxt NOBR expr]
+ else args)
+ val rhs = [str "=", ml_from_expr NOBR expr]
in
Pretty.block (separate (Pretty.brk 1) (lhs @ rhs))
end
- fun mk_fun definer (f, Fun (eqs as eq::eq_tl, (sortctxt , ty))) =
+ fun mk_fun definer (f, Fun (eqs as eq::eq_tl, (sortctxt, ty))) =
let
val (pats_hd::pats_tl) = (fst o split_list) eqs;
val shift = if null eq_tl then I else map (Pretty.block o single);
@@ -614,15 +628,20 @@
| ml_from_def (name, Classinst (((class, (tyco, arity)), suparities), memdefs)) =
let
val definer = if null arity then "val" else "fun"
- fun from_supclass (supclass, (inst, ls)) = str "<DUMMY>"
+ fun from_supclass (supclass, lss) =
+ (Pretty.block o Pretty.breaks) (
+ ml_from_label supclass
+ :: str "="
+ :: map (ml_from_sortlookup NOBR) lss
+ );
fun from_memdef (m, def) =
((the o ml_from_funs) [(m, Fun def)], Pretty.block [
- (str o resolv) m,
+ ml_from_label m,
Pretty.brk 1,
str "=",
Pretty.brk 1,
(str o resolv) m
- ])
+ ]);
fun mk_memdefs supclassexprs [] =
Pretty.enum "," "{" "};" (
supclassexprs
@@ -677,8 +696,6 @@
fun needs_type (IType (tyco, _)) =
has_nsp tyco nsp_class
orelse is_int_tyco tyco
- | needs_type (IDictT _) =
- true
| needs_type _ =
false;
fun is_cons c = has_nsp c nsp_dtcon;
@@ -700,7 +717,9 @@
|> debug 3 (fn _ => "eta-expanding...")
|> eta_expand (eta_expander module const_syntax)
|> debug 3 (fn _ => "eta-expanding polydefs...")
- |> eta_expand_poly;
+ |> eta_expand_poly
+ |> debug 3 (fn _ => "unclashing expression/type variables...")
+ |> unclash_vars;
val parse_multi =
OuterParse.name
#-> (fn "dir" =>
@@ -783,9 +802,7 @@
hs_from_type (INFX (1, R)) t2
]
| hs_from_type fxy (IVarT (v, _)) =
- (str o lower_first) v
- | hs_from_type fxy (IDictT _) =
- error "can't serialize dictionary type to hs";
+ (str o lower_first) v;
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)) =
@@ -842,10 +859,6 @@
Pretty.fbrk,
(Pretty.chunks o map mk_clause) cs
] end
- | hs_from_expr fxy (IDictE _) =
- error "can't serialize dictionary expression to hs"
- | hs_from_expr fxy (ILookup _) =
- error "can't serialize lookup expression to hs"
and hs_mk_app c es =
(str o resolv_const) c :: map (hs_from_expr BR) es
and hs_from_app fxy (((c, _), ls), es) =
--- a/src/Pure/Tools/codegen_thingol.ML Wed Feb 01 12:22:47 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Wed Feb 01 12:23:14 2006 +0100
@@ -8,19 +8,18 @@
signature CODEGEN_THINGOL =
sig
type vname = string;
+ datatype classlookup = Instance of string * classlookup list list
+ | Lookup of class list * (string * int);
datatype itype =
IType of string * itype list
| IFun of itype * itype
- | IVarT of vname * sort
- | IDictT of (string * itype) list;
+ | IVarT of vname * sort;
datatype iexpr =
- IConst of (string * itype) * ClassPackage.sortlookup list list
+ IConst of (string * itype) * classlookup list list
| IVarE of vname * itype
| IApp of iexpr * iexpr
| IAbs of (vname * itype) * iexpr
- | ICase of iexpr * (iexpr * iexpr) list
- | IDictE of (string * iexpr) list
- | ILookup of (string list * vname);
+ | ICase of iexpr * (iexpr * iexpr) list;
val mk_funs: itype list * itype -> itype;
val mk_apps: iexpr * iexpr list -> iexpr;
val mk_abss: (vname * itype) list * iexpr -> iexpr;
@@ -33,11 +32,8 @@
val unfold_abs: iexpr -> (vname * itype) list * iexpr;
val unfold_let: iexpr -> (iexpr * iexpr) list * iexpr;
val unfold_const_app: iexpr ->
- (((string * itype) * ClassPackage.sortlookup list list) * iexpr list) option;
+ (((string * itype) * classlookup list list) * iexpr list) option;
val itype_of_iexpr: iexpr -> itype;
- val eq_itype: itype * itype -> bool;
- val tvars_of_itypes: itype list -> string list;
- val names_of_iexprs: iexpr list -> string list;
val `%% : string * itype list -> itype;
val `-> : itype * itype -> itype;
@@ -63,7 +59,7 @@
* string list
| Classmember of class
| Classinst of ((class * (string * (vname * sort) list))
- * (class * (string * ClassPackage.sortlookup list list)) list)
+ * (class * classlookup list list) list)
* (string * funn) list;
type module;
type transact;
@@ -87,6 +83,7 @@
val eta_expand: (string -> int) -> module -> module;
val eta_expand_poly: module -> module;
+ val unclash_vars: module -> module;
val debug_level: int ref;
val debug: int -> ('a -> string) -> 'a -> 'a;
@@ -145,27 +142,25 @@
infixr 6 `-->;
infix 4 `$;
infix 4 `$$;
-infixr 5 `|->;
-infixr 5 `|-->;
+infixr 3 `|->;
+infixr 3 `|-->;
type vname = string;
+datatype classlookup = Instance of string * classlookup list list
+ | Lookup of class list * (string * int);
+
datatype itype =
IType of string * itype list
| IFun of itype * itype
- | IVarT of vname * sort
- (*ML auxiliary*)
- | IDictT of (string * itype) list;
+ | IVarT of vname * sort;
datatype iexpr =
- IConst of (string * itype) * ClassPackage.sortlookup list list
+ IConst of (string * itype) * classlookup list list
| IVarE of vname * itype
| IApp of iexpr * iexpr
| IAbs of (vname * itype) * iexpr
- | ICase of iexpr * (iexpr * iexpr) list
- (*ML auxiliary*)
- | IDictE of (string * iexpr) list
- | ILookup of (string list * vname);
+ | ICase of iexpr * (iexpr * iexpr) list;
(*
variable naming conventions
@@ -203,6 +198,34 @@
val op `$$ = mk_apps;
val op `|--> = mk_abss;
+fun pretty_itype (IType (tyco, tys)) =
+ Pretty.enum "" "(" ")" (Pretty.str tyco :: map pretty_itype tys)
+ | pretty_itype (IFun (ty1, ty2)) =
+ Pretty.enum "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
+ | pretty_itype (IVarT (v, sort)) =
+ Pretty.str (v ^ enclose "|" "|" (space_implode "|" sort));
+
+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 ((v, ty), e)) =
+ Pretty.enclose "(" ")" [Pretty.str ("?" ^ v ^ " |->"), Pretty.brk 1, pretty_iexpr e]
+ | pretty_iexpr (ICase (e, cs)) =
+ Pretty.enclose "(" ")" [
+ Pretty.str "case ",
+ pretty_iexpr e,
+ Pretty.enclose "(" ")" (map (fn (p, e) =>
+ Pretty.block [
+ pretty_iexpr p,
+ Pretty.str " => ",
+ pretty_iexpr e
+ ]
+ ) cs)
+ ];
+
val unfold_fun = unfoldr
(fn IFun t => SOME t
| _ => NONE);
@@ -231,41 +254,52 @@
| map_itype _ (ty as IVarT _) =
ty;
-fun map_iexpr f_itype f_iexpr (IApp (e1, e2)) =
- f_iexpr e1 `$ f_iexpr e2
- | map_iexpr f_itype f_iexpr (IAbs (v, e)) =
- IAbs (v, f_iexpr e)
- | map_iexpr f_itype f_iexpr (ICase (e, ps)) =
- ICase (f_iexpr e, map (fn (p, e) => (f_iexpr p, f_iexpr e)) ps)
- | map_iexpr _ _ (e as IConst _) =
+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 _) =
e
- | map_iexpr _ _ (e as IVarE _) =
- e
- | map_iexpr f_itype f_iexpr (IDictE ms) =
- IDictE (map (apsnd f_iexpr) ms)
- | map_iexpr _ _ (e as ILookup _) =
+ | map_iexpr _ (e as IVarE _) =
e;
-fun fold_itype f_itype (IFun (t1, t2)) =
- f_itype t1 #> f_itype t2
- | fold_itype _ (ty as IType _) =
- I
- | fold_itype _ (ty as IVarT _) =
- I;
+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;
+
+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_iexpr f_itype f_iexpr (IApp (e1, e2)) =
- f_iexpr e1 #> f_iexpr e2
- | fold_iexpr f_itype f_iexpr (IAbs (v, e)) =
- f_iexpr e
- | fold_iexpr f_itype f_iexpr (ICase (e, ps)) =
- f_iexpr e #> fold (fn (p, e) => f_iexpr p #> f_iexpr e) ps
- | fold_iexpr _ _ (e as IConst _) =
- I
- | fold_iexpr _ _ (e as IVarE _) =
- I;
+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;
-
-(* simple type matching *)
+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 eq_itype (ty1, ty2) =
let
@@ -292,6 +326,12 @@
handle NO_MATCH => false
end;
+fun instant_itype f =
+ let
+ fun instant (IVarT x) = f x
+ | instant y = map_itype instant y;
+ in map_itype instant end;
+
(* simple diagnosis *)
@@ -300,9 +340,7 @@
| pretty_itype (IFun (ty1, ty2)) =
Pretty.enum "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
| pretty_itype (IVarT (v, sort)) =
- Pretty.str (v ^ enclose "|" "|" (space_implode "|" sort))
- | pretty_itype (IDictT _) =
- Pretty.str "<DictT>";
+ Pretty.str (v ^ enclose "|" "|" (space_implode "|" sort));
fun pretty_iexpr (IConst ((c, ty), _)) =
Pretty.block [Pretty.str (c ^ "::"), pretty_itype ty]
@@ -323,26 +361,11 @@
pretty_iexpr e
]
) cs)
- ]
- | pretty_iexpr (IDictE _) =
- Pretty.str "<DictE>"
- | pretty_iexpr (ILookup (ls, v)) =
- Pretty.str ("<Lookup: " ^ commas ls ^ " in " ^ v ^ ">");
+ ];
(* language auxiliary *)
-
-fun instant_itype (v, sty) ty =
- let
- fun instant (IType (tyco, tys)) =
- tyco `%% map instant tys
- | instant (IFun (ty1, ty2)) =
- instant ty1 `-> instant ty2
- | instant (w as (IVarT (u, _))) =
- if v = u then sty else w
- in instant ty 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
@@ -356,35 +379,25 @@
| itype_of_iexpr (IAbs ((_, ty1), e2)) = ty1 `-> itype_of_iexpr e2
| itype_of_iexpr (ICase ((_, [(_, e)]))) = itype_of_iexpr e;
-fun tvars_of_itypes tys =
+fun type_vnames ty =
let
- fun vars (IType (_, tys)) =
- fold vars tys
- | vars (IFun (ty1, ty2)) =
- vars ty1 #> vars ty2
- | vars (IVarT (v, _)) =
- insert (op =) v
- in fold vars tys [] end;
+ fun extr (IVarT (v, _)) =
+ insert (op =) v
+ in fold_atype extr ty end;
-fun names_of_iexprs es =
+fun expr_names e =
let
- fun vars (IConst ((c, _), _)) =
+ fun extr (IConst ((c, _), _)) =
insert (op =) c
- | vars (IVarE (v, _)) =
- insert (op =) v
- | vars (IApp (e1, e2)) =
- vars e1 #> vars e2
- | vars (IAbs ((v, _), e)) =
+ | extr (IVarE (v, _)) =
insert (op =) v
- #> vars e
- | vars (ICase (e, cs)) =
- vars e
- #> fold (fn (p, e) => vars p #> vars e) cs
- | vars (IDictE ms) =
- fold (vars o snd) ms
- | vars (ILookup (_, v)) =
- cons v
- in fold vars es [] end;
+ in fold_aexpr extr e end;
+
+fun invent seed used =
+ let
+ val x = Term.variant used seed
+ in (x, x :: used) end;
+
(** language module system - definitions, modules, transactions **)
@@ -409,7 +422,7 @@
* string list
| Classmember of class
| Classinst of ((class * (string * (vname * sort) list))
- * (class * (string * ClassPackage.sortlookup list list)) list)
+ * (class * classlookup list list) list)
* (string * funn) list;
datatype node = Def of def | Module of node Graph.T;
@@ -576,28 +589,6 @@
#> Graph.map_node m (Module o add ms o dest_modl)
in add modl end;
-fun map_def name f =
- let
- val (modl, base) = dest_name name;
- fun mapp [] =
- Graph.map_node base (Def o f o dest_def)
- | mapp (m::ms) =
- Graph.map_node m (Module o mapp ms o dest_modl)
- in mapp modl end;
-
-fun ensure_def (name, Undef) module =
- (case try (get_def module) name
- of NONE => (error "attempted to add Undef to module")
- | SOME Undef => (error "attempted to add Undef to module")
- | SOME def' => map_def name (K def') module)
- | ensure_def (name, def) module =
- (case try (get_def module) name
- of NONE => add_def (name, def) module
- | SOME Undef => map_def name (K def) module
- | SOME def' => if eq_def (def, def')
- then module
- else error ("tried to overwrite definition " ^ name));
-
fun add_dep (name1, name2) modl =
if name1 = name2 then modl
else
@@ -618,6 +609,48 @@
|> Graph.map_node m (Module o add ms o dest_modl);
in add ms modl end;
+fun map_def name f =
+ let
+ val (modl, base) = dest_name name;
+ fun mapp [] =
+ Graph.map_node base (Def o f o dest_def)
+ | mapp (m::ms) =
+ Graph.map_node m (Module o mapp ms o dest_modl)
+ in mapp modl end;
+
+fun map_defs f =
+ let
+ fun mapp (Def def) =
+ (Def o f) def
+ | mapp (Module modl) =
+ (Module o Graph.map_nodes mapp) modl
+ in dest_modl o mapp o Module end;
+
+fun fold_defs f =
+ let
+ fun fol prfix (name, Def def) =
+ f (NameSpace.pack (prfix @ [name]), def)
+ | fol prfix (name, Module modl) =
+ Graph.fold_nodes (fol (prfix @ [name])) modl
+ in Graph.fold_nodes (fol []) end;
+
+fun add_deps f modl =
+ modl
+ |> fold add_dep ([] |> fold_defs (append o f) modl);
+
+fun ensure_def (name, Undef) module =
+ (case try (get_def module) name
+ of NONE => (error "attempted to add Undef to module")
+ | SOME Undef => (error "attempted to add Undef to module")
+ | SOME def' => map_def name (K def') module)
+ | ensure_def (name, def) module =
+ (case try (get_def module) name
+ of NONE => add_def (name, def) module
+ | SOME Undef => map_def name (K def) module
+ | SOME def' => if eq_def (def, def')
+ then module
+ else error ("tried to overwrite definition " ^ name));
+
fun add_prim name deps (target, primdef) =
let
val (modl, base) = dest_name name;
@@ -663,46 +696,6 @@
|> Graph.map_node m (Module o ensure ms o dest_modl)
in ensure modl end;
-fun map_defs f =
- let
- fun mapp (Def def) =
- (Def o f) def
- | mapp (Module modl) =
- (Module o Graph.map_nodes mapp) modl
- in dest_modl o mapp o Module end;
-
-fun fold_defs f =
- let
- fun fol prfix (name, Def def) =
- f (NameSpace.pack (prfix @ [name]), def)
- | fol prfix (name, Module modl) =
- Graph.fold_nodes (fol (prfix @ [name])) modl
- in Graph.fold_nodes (fol []) end;
-
-fun add_deps f modl =
- modl
- |> fold add_dep ([] |> fold_defs (append o f) modl);
-
-fun fold_map_defs f =
- let
- fun foldmap prfix (name, Def def) =
- apfst Def o f (NameSpace.pack (prfix @ [name]), def)
- | foldmap prfix (name, Module modl) =
- apfst Module o Graph.fold_map_nodes (foldmap (prfix @ [name])) modl
- in Graph.fold_map_nodes (foldmap []) end;
-
-fun map_def_fun f_iexpr (Fun (eqs, cty)) =
- Fun (map (fn (ps, rhs) => (map f_iexpr ps, f_iexpr rhs)) eqs, cty)
- | map_def_fun _ def = def;
-
-fun transform_defs f_def f_iexpr s modl =
- let
- val (modl', s') = fold_map_defs f_def modl s
- in
- modl'
- |> map_defs (map_def_fun (f_iexpr s'))
- end;
-
fun merge_module modl12 =
let
fun join_module (Module m1, Module m2) =
@@ -799,11 +792,13 @@
val _ = if length memdefs > length memdefs
then error "too many member definitions given"
else ();
+ fun instant (w, ty) (var as (v, _)) =
+ if v = w then ty else IVarT var;
fun mk_memdef (m, (ctxt, ty)) =
case AList.lookup (op =) memdefs m
of NONE => error ("missing definition for member " ^ quote m)
| SOME (eqs, (ctxt', ty')) =>
- if eq_itype (ty |> instant_itype (v, tyco `%% map IVarT arity), ty')
+ if eq_itype (instant_itype (instant (v, tyco `%% map IVarT arity)) ty, ty')
then (m, (check_funeqs eqs, (ctxt', ty')))
else error ("inconsistent type for member definition " ^ quote m)
in Classinst (d, map mk_memdef membrs) end;
@@ -922,40 +917,64 @@
(** generic transformation **)
+fun map_def_fun f (Fun funn) =
+ Fun (f funn)
+ | map_def_fun _ def = def;
+
+fun map_def_fun_expr f (eqs, cty) =
+ (map (fn (ps, rhs) => (map f ps, f rhs)) eqs, cty);
+
fun eta_expand query =
let
- fun eta_app (((f, ty), ls), es) =
- let
- val delta = query f - 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 add_vars =
- Term.invent_names (names_of_iexprs es) "x" add_n ~~ tys;
- in
- Library.foldr IAbs (add_vars,
- IConst ((f, ty), ls) `$$ es `$$ (map IVarE add_vars))
- end;
- fun eta_iexpr e =
+ fun eta e =
case unfold_const_app e
- of SOME x => eta_app x
- | NONE => map_iexpr I eta_iexpr e;
- in map_defs (map_def_fun eta_iexpr) end;
+ of SOME (((f, ty), ls), es) =>
+ let
+ val delta = query f - 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 add_vars =
+ Term.invent_names (fold expr_names es []) "x" add_n ~~ tys;
+ in
+ add_vars `|--> IConst ((f, ty), ls) `$$ es `$$ map IVarE add_vars
+ 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 map_def_fun (def as Fun ([([], e)], cty as (sortctxt, (ty as IFun (ty1, ty2))))) =
+ fun eta (funn as ([([], e)], cty as (sortctxt, (ty as IFun (ty1, ty2))))) =
if (not o null) sortctxt
- orelse (null o tvars_of_itypes) [ty]
- then def
+ orelse null (type_vnames ty [])
+ then funn
else
let
- val add_var = (hd (Term.invent_names (names_of_iexprs [e]) "x" 1), ty1)
- in (Fun ([([IVarE add_var], IAbs (add_var, e))], cty)) end
- | map_def_fun def = def;
- in map_defs map_def_fun end;
+ val add_var = (hd (Term.invent_names (expr_names e []) "x" 1), ty1)
+ in (([([IVarE add_var], add_var `|-> e)], cty)) end
+ | eta funn = funn;
+ in (map_defs o map_def_fun) eta end;
+
+val unclash_vars =
+ let
+ fun unclash (eqs, (sortctxt, ty)) =
+ let
+ val used_expr =
+ fold (fn (pats, rhs) => fold expr_names pats #> expr_names 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;
+ fun rename (v, sort) =
+ (perhaps (AList.lookup (op =) rename_map) v, sort);
+ val rename_typ = instant_itype (IVarT o rename);
+ val rename_expr = map_iexpr_itype rename_typ;
+ fun rename_eq (args, rhs) = (map rename_expr args, rename_expr rhs)
+ in
+ (map rename_eq eqs, (map rename sortctxt, rename_typ ty))
+ end;
+ in (map_defs o map_def_fun) unclash end;
@@ -963,33 +982,101 @@
(* resolving *)
-structure ModlNameMangler = NameManglerFun (
- type ctxt = string -> string option;
- type src = string;
- val ord = string_ord;
- fun mk _ _ = "";
- fun is_valid _ _ = true;
- fun maybe_unique validate name = (SOME oo perhaps) validate name;
- fun re_mangle _ dst = error ("no such module name: " ^ quote dst);
-);
-
-structure DefNameMangler = NameManglerFun (
- type ctxt = string -> string option;
+structure NameMangler = NameManglerFun (
+ type ctxt = (string * string -> string) * (string -> string option);
type src = string * string;
val ord = prod_ord string_ord string_ord;
- fun mk validate ((shallow, name), 0) =
- (case validate name
+ fun mk (preprocess, validate) ((shallow, name), 0) =
+ (case validate (preprocess (shallow, name))
of NONE => name
- | _ => mk validate ((shallow, name), 1))
- | mk validate ((shallow, name), i) =
- shallow ^ "_" ^ name ^ "_" ^ string_of_int (i+1)
+ | _ => mk (preprocess, validate) ((shallow, name), 1))
+ | mk (preprocess, validate) (("", name), i) =
+ preprocess ("", name ^ "_" ^ string_of_int (i+1))
+ |> perhaps validate
+ | mk (preprocess, validate) ((shallow, name), i) =
+ preprocess (shallow, shallow ^ "_" ^ name ^ "_" ^ string_of_int (i+1))
|> perhaps validate;
fun is_valid _ _ = true;
fun maybe_unique _ _ = NONE;
fun re_mangle _ dst = error ("no such definition name: " ^ quote dst);
);
-fun mk_resolvtab nsp_conn validate module =
+fun mk_deresolver module nsp_conn preprocess validate =
+ let
+ datatype tabnode = N of string * tabnode Symtab.table option;
+ fun mk module manglers tab =
+ let
+ fun mk_name name =
+ case NameSpace.unpack name
+ of [n] => ("", n)
+ | [s, n] => (s, n);
+ fun in_conn (shallow, conn) =
+ member (op = : string * string -> bool) conn shallow;
+ fun add_name name =
+ let
+ val n as (shallow, _) = mk_name name;
+ fun diag (nm as (name, n')) = (writeln ("resolving " ^ quote name ^ " to " ^ quote n'); nm);
+ in
+ AList.map_entry_yield in_conn shallow (
+ NameMangler.declare (preprocess, validate) n
+ #-> (fn n' => pair (name, n'))
+ ) #> apfst the #> apfst diag
+ end;
+ val (renamings, manglers') =
+ fold_map add_name (Graph.keys module) manglers;
+ fun extend_tab (n, n') =
+ if (length o NameSpace.unpack) n = 1
+ then
+ Symtab.update_new
+ (n, N (n', SOME (mk ((dest_modl o Graph.get_node module) n) manglers' Symtab.empty)))
+ else
+ Symtab.update_new (n, N (n', NONE));
+ in fold extend_tab renamings tab end;
+ fun get_path_name [] tab =
+ ([], SOME tab)
+ | get_path_name [p] tab =
+ let
+ val _ = writeln ("(1) " ^ p);
+ val SOME (N (p', tab')) = Symtab.lookup tab p
+ in ([p'], tab') end
+ | get_path_name [p1, p2] tab =
+ let
+ val _ = (writeln o prefix "(2) " o NameSpace.pack) [p1, p2];
+ in case Symtab.lookup tab p1
+ of SOME (N (p', SOME tab')) =>
+ let
+ val _ = writeln ("(2) 'twas a module");
+ val (ps', tab'') = get_path_name [p2] tab'
+ in (p' :: ps', tab'') end
+ | NONE =>
+ let
+ val _ = writeln ("(2) 'twas a definition");
+ val SOME (N (p', NONE)) = Symtab.lookup tab (NameSpace.pack [p1, p2])
+ in ([p'], NONE) end
+ end
+ | get_path_name (p::ps) tab =
+ let
+ val _ = (writeln o prefix "(3) " o commas) (p::ps);
+ val SOME (N (p', SOME tab')) = Symtab.lookup tab p
+ val (ps', tab'') = get_path_name ps tab'
+ in (p' :: ps', tab'') end;
+ fun deresolv tab prefix name =
+ if (is_some o Int.fromString) name
+ then name
+ else let
+ val _ = writeln ("(0) prefix: " ^ commas prefix);
+ val _ = writeln ("(0) name: " ^ name)
+ val (common, (_, rem)) = get_prefix (op =) (prefix, NameSpace.unpack name);
+ val _ = writeln ("(0) common: " ^ commas common);
+ val _ = writeln ("(0) rem: " ^ commas rem);
+ val (_, SOME tab') = get_path_name common tab;
+ val (name', _) = get_path_name rem tab';
+ in NameSpace.pack name' end;
+ in deresolv (mk module (AList.make (K NameMangler.empty) nsp_conn) Symtab.empty) end;
+
+val _ : module -> string list list -> (string * string -> string) -> (string -> string option) -> string list -> string -> string = mk_deresolver;
+
+fun mk_resolvtab' nsp_conn validate module =
let
fun validate' n = perhaps validate n;
fun ensure_unique prfix prfix' name name' (locals, tab) =
@@ -1076,8 +1163,8 @@
fun serialize seri_defs seri_module validate nsp_conn name_root module =
let
- val resolvtab = mk_resolvtab nsp_conn validate module;
- val resolver = mk_resolv resolvtab;
+(* val resolver = mk_deresolver module nsp_conn snd validate; *)
+ val resolver = mk_resolv (mk_resolvtab' nsp_conn validate module);
fun mk_name prfx name =
let
val name_qual = NameSpace.pack (prfx @ [name])