--- a/src/Pure/Tools/class_package.ML Tue Jun 27 10:09:48 2006 +0200
+++ b/src/Pure/Tools/class_package.ML Tue Jun 27 10:10:20 2006 +0200
@@ -48,10 +48,9 @@
type sortcontext = (string * sort) list
datatype classlookup = Instance of (class * string) * classlookup list list
| Lookup of class list * (string * (int * int))
- val extract_sortctxt: theory -> typ -> sortcontext
- val extract_classlookup: theory -> string * typ -> classlookup list list
- val extract_classlookup_inst: theory -> class * string -> class -> classlookup list list
- val extract_classlookup_member: theory -> typ * typ -> classlookup list list
+ val sortcontext_of_typ: theory -> typ -> sortcontext
+ val sortlookup: theory -> sort * typ -> classlookup list
+ val sortlookups_const: theory -> string * typ -> classlookup list list
end;
structure ClassPackage: CLASS_PACKAGE =
@@ -129,17 +128,13 @@
|> Option.map (not o null o #consts)
|> the_default false;
-fun operational_sort_of thy sort =
+fun operational_sort_of thy =
let
fun get_sort class =
if is_operational_class thy class
then [class]
else operational_sort_of thy (Sign.super_classes thy class);
- in
- map get_sort sort
- |> flat
- |> Sign.certify_sort thy
- end;
+ in Sign.certify_sort thy o maps get_sort end;
fun the_superclasses thy class =
if is_class thy class
@@ -193,7 +188,7 @@
|> fold (fn (_, ty) => curry (gen_union (op =))
((map (fst o fst) o typ_tvars) ty @ (map fst o typ_tfrees) ty)) const_sign
|> fold_map add_var arity;
- val ty_inst = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vsorts);
+ val ty_inst = Type (tyco, map TFree vsorts);
val inst_signs = map (apsnd (subst_clsvar clsvar ty_inst)) const_sign;
in (vsorts, inst_signs) end;
@@ -599,7 +594,7 @@
type sortcontext = (string * sort) list;
-fun extract_sortctxt thy ty =
+fun sortcontext_of_typ thy ty =
(typ_tfrees o fst o Type.freeze_thaw_type) ty
|> map (apsnd (operational_sort_of thy))
|> filter (not o null o snd);
@@ -613,75 +608,52 @@
:: map pretty_lookup lss
)
| pretty_lookup' (Lookup (classes, (v, (i, j)))) =
- Pretty.enum " <" "[" "]" (map Pretty.str classes @ [Pretty.str (v ^ "!" ^ string_of_int i ^ "/" ^ string_of_int j)])
+ Pretty.enum " <" "[" "]" (map Pretty.str classes @
+ [Pretty.str (v ^ "!" ^ string_of_int i ^ "/" ^ string_of_int j)])
and pretty_lookup ls = (Pretty.enum "," "(" ")" o map pretty_lookup') ls;
-fun extract_lookup thy sortctxt raw_typ_def raw_typ_use =
+fun sortlookup thy (sort_decl, typ_ctxt) =
let
- val typ_def = Logic.legacy_varifyT raw_typ_def;
- val typ_use = Logic.legacy_varifyT raw_typ_use;
- val match_tab = Sign.typ_match thy (typ_def, typ_use) Vartab.empty;
- fun tab_lookup vname = (the o Vartab.lookup match_tab) (vname, 0);
- fun mk_class_deriv thy subclasses superclass =
- let
- val (i, (subclass::deriv)) = (the oo get_index) (fn subclass =>
- get_superclass_derivation thy (subclass, superclass)
- ) subclasses;
- in (rev deriv, (i, length subclasses)) end;
- fun mk_lookup (sort_def, (Type (tyco, tys))) =
- map (fn class => Instance ((class, tyco),
- map2 (curry mk_lookup)
- (map (operational_sort_of thy) (Sign.arity_sorts thy tyco [class]))
- tys)
- ) sort_def
- | mk_lookup (sort_def, TVar ((vname, _), sort_use)) =
- let
- fun mk_look class =
- let val (deriv, classindex) = mk_class_deriv thy (operational_sort_of thy sort_use) class
- in Lookup (deriv, (vname, classindex)) end;
- in map mk_look sort_def end;
+ val pp = Sign.pp thy;
+ val algebra = Sorts.project_algebra pp (is_operational_class thy)
+ (Sign.classes_of thy);
+ fun classrel (l as Lookup (classes, p), _) class =
+ Lookup (class :: classes, p)
+ | classrel (Instance ((_, tyco), lss), _) class =
+ Instance ((class, tyco), lss);
+ fun constructor tyco lss class =
+ Instance ((class, tyco), (map o map) fst lss)
+ fun variable (TFree (v, sort)) =
+ map_index (fn (n, class) => (Lookup ([], (v, (n, length sort))), class))
+ (operational_sort_of thy sort)
+ | variable (TVar _) = error "TVar encountered while deriving sortlookup";
in
- sortctxt
- |> map (tab_lookup o fst)
- |> map (apfst (operational_sort_of thy))
- |> filter (not o null o fst)
- |> map mk_lookup
+ Sorts.of_sort_derivation pp algebra
+ {classrel = classrel, constructor = constructor, variable = variable}
+ (typ_ctxt, operational_sort_of thy sort_decl)
end;
-fun extract_classlookup thy (c, raw_typ_use) =
+fun sortlookups_const thy (c, typ_ctxt) =
let
- val raw_typ_def = Sign.the_const_constraint thy c;
- val typ_def = Logic.legacy_varifyT raw_typ_def;
- fun reorder_sortctxt ctxt =
- case lookup_const_class thy c
- of NONE => ctxt
- | SOME class =>
- let
- val data = the_class_data thy class;
- val sign = (Logic.legacy_varifyT o the o AList.lookup (op =) ((map snd o #consts) data)) c;
- val match_tab = Sign.typ_match thy (sign, typ_def) Vartab.empty;
- val v : string = case Vartab.lookup match_tab (#var data, 0)
- of SOME (_, TVar ((v, _), _)) => v;
- in
- (v, (the o AList.lookup (op =) ctxt) v) :: AList.delete (op =) v ctxt
- end;
+ val typ_decl = case lookup_const_class thy c
+ of NONE => Sign.the_const_type thy c
+ | SOME class => case the_consts_sign thy class of (v, cs) =>
+ (Logic.legacy_varifyT o subst_clsvar v (TFree (v, [class])))
+ ((the o AList.lookup (op =) cs) c)
+ val vartab = typ_tvars typ_decl;
+ fun prep_vartab (v, (_, ty)) =
+ case (the o AList.lookup (op =) vartab) v
+ of [] => NONE
+ | sort => SOME (sort, ty);
in
- extract_lookup thy
- (reorder_sortctxt (extract_sortctxt thy ((fst o Type.freeze_thaw_type) raw_typ_def)))
- raw_typ_def raw_typ_use
+ Vartab.empty
+ |> Sign.typ_match thy (typ_decl, typ_ctxt)
+ |> Vartab.dest
+ |> map_filter prep_vartab
+ |> map (sortlookup thy)
+ |> filter_out null
end;
-fun extract_classlookup_inst thy (class, tyco) supclass =
- let
- fun mk_typ class = Type (tyco, (map TFree o fst o the_inst_sign thy) (class, tyco))
- val typ_def = mk_typ supclass;
- val typ_use = mk_typ class;
- in
- extract_lookup thy (extract_sortctxt thy typ_def) typ_def typ_use
- end;
-
-fun extract_classlookup_member thy (ty_decl, ty_use) =
- extract_lookup thy (extract_sortctxt thy ty_decl) ty_decl ty_use;
(* toplevel interface *)
--- a/src/Pure/Tools/codegen_package.ML Tue Jun 27 10:09:48 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML Tue Jun 27 10:10:20 2006 +0200
@@ -219,7 +219,7 @@
|> Symtab.update (
#haskell CodegenSerializer.serializers
|> apsnd (fn seri => seri
- [nsp_module, nsp_class, nsp_tyco, nsp_dtcon]
+ (nsp_dtcon, [nsp_module, nsp_class, nsp_tyco, nsp_dtcon])
[[nsp_module], [nsp_class], [nsp_tyco], [nsp_const, nsp_overl, nsp_mem], [nsp_dtcon], [nsp_inst], [nsp_instmem]]
)
)
@@ -307,7 +307,7 @@
structure CodegenData = TheoryDataFun
(struct
- val name = "Pure/CodegenPackage";
+ val name = "Pure/codegen_package";
type T = {
modl: module,
gens: gens,
@@ -541,7 +541,7 @@
of SOME cls =>
let
val (v, cs) = (ClassPackage.the_consts_sign thy) cls;
- val sortctxts = map (ClassPackage.extract_sortctxt thy o snd) cs;
+ val sortctxts = map (ClassPackage.sortcontext_of_typ thy o snd) cs;
val idfs = map (idf_of_name thy nsp_mem o fst) cs;
in
trns
@@ -623,14 +623,15 @@
|-> (fn clss => pair (Lookup (clss, (v |> unprefix "'", if j = 1 then ~1 else i))))
and mk_fun thy tabs (c, ty) trns =
case CodegenTheorems.get_funs thy (c, Logic.legacy_varifyT ty) (* FIXME *)
- of SOME (ty, eq_thms) =>
+ of eq_thms as eq_thm :: _ =>
let
val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms);
- val sortctxt = ClassPackage.extract_sortctxt thy ty;
+ val ty = (Logic.legacy_unvarifyT o CodegenTheorems.extr_typ thy) eq_thm
+ val sortcontext = ClassPackage.sortcontext_of_typ thy ty;
fun dest_eqthm eq_thm =
let
val ((t, args), rhs) =
- (apfst strip_comb o Logic.dest_equals o prop_of) eq_thm;
+ (apfst strip_comb o Logic.dest_equals o Logic.legacy_unvarify o prop_of) eq_thm;
in case t
of Const (c', _) => if c' = c then (args, rhs)
else error ("illegal function equation for " ^ quote c
@@ -645,11 +646,11 @@
trns
|> message msg (fn trns => trns
|> fold_map (exprgen_eq o dest_eqthm) eq_thms
+ ||>> fold_map (exprgen_tyvar_sort thy tabs) sortcontext
||>> exprgen_type thy tabs ty
- ||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt
- |-> (fn ((eqs, ity), sortctxt) => (pair o SOME) ((eqs, (sortctxt, ity)), ty)))
+ |-> (fn ((eqs, sortctxt), ty) => (pair o SOME) ((eqs, (sortctxt, ty)), map snd sortcontext)))
end
- | NONE => (NONE, trns)
+ | [] => (NONE, trns)
and ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns =
let
fun defgen_inst thy (tabs as (_, (insttab, _, _))) inst trns =
@@ -657,20 +658,24 @@
of SOME (_, (class, tyco)) =>
let
val (arity, memdefs) = ClassPackage.the_inst_sign thy (class, tyco);
+ val arity_typ = Type (tyco, (map TFree arity));
+ val operational_arity = map_filter (fn (v, sort) => case ClassPackage.operational_sort_of thy sort
+ of [] => NONE
+ | sort => SOME (v, sort)) arity;
fun gen_suparity supclass trns =
trns
|> ensure_def_class thy tabs supclass
- ||>> ensure_def_inst thy tabs (supclass, tyco)
- ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
- (ClassPackage.extract_classlookup_inst thy (class, tyco) supclass)
- |-> (fn ((supclass, inst), lss) => pair (supclass, (inst, lss)));
+ ||>> fold_map (exprgen_classlookup thy tabs)
+ (ClassPackage.sortlookup thy ([supclass], arity_typ));
fun gen_membr (m, ty) trns =
trns
|> mk_fun thy tabs (m, ty)
|-> (fn NONE => error ("could not derive definition for member "
^ quote m ^ " :: " ^ Sign.string_of_typ thy ty)
- | SOME (funn, ty_decl) => (fold_map o fold_map) (exprgen_classlookup thy tabs)
- (ClassPackage.extract_classlookup_member thy (ty_decl, ty))
+ | SOME (funn, sorts) => fold_map (fn (sort, sort_ctxt) =>
+ fold_map (exprgen_classlookup thy tabs)
+ (ClassPackage.sortlookup thy (sort, TFree sort_ctxt)))
+ (sorts ~~ operational_arity)
#-> (fn lss =>
pair (idf_of_name thy nsp_mem m, ((idf_of_name thy nsp_instmem m, funn), lss))));
in
@@ -783,7 +788,7 @@
|> ensure_def_const thy tabs (c, ty)
||>> exprgen_type thy tabs ty
||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
- (ClassPackage.extract_classlookup thy (c, ty))
+ (ClassPackage.sortlookups_const thy (c, ty))
||>> fold_map (exprgen_term thy tabs) ts
|-> (fn (((c, ty), ls), es) =>
pair (IConst (c, (ls, ty)) `$$ es))
@@ -878,7 +883,7 @@
|> ensure_def ((K o fail) "no extraction of wfrec") false ("generating wfrec") idf
|> exprgen_type thy tabs ty'
||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
- (ClassPackage.extract_classlookup thy (c, ty))
+ (ClassPackage.sortlookups_const thy (c, ty))
||>> exprgen_type thy tabs ty_def
||>> exprgen_term thy tabs tf
||>> exprgen_term thy tabs tx
@@ -1006,7 +1011,6 @@
let
val tabs = mk_tabs thy NONE;
val idfs = map (idf_of_const' thy tabs) cs;
- val _ = writeln ("purging " ^ commas idfs);
fun purge idfs modl =
CodegenThingol.purge_module (filter (can (get_def modl)) idfs) modl
in
--- a/src/Pure/Tools/codegen_serializer.ML Tue Jun 27 10:09:48 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML Tue Jun 27 10:10:20 2006 +0200
@@ -23,7 +23,7 @@
val pretty_list: string -> string -> int * string -> CodegenThingol.iexpr pretty_syntax;
val serializers: {
ml: string * (string * string * (string -> bool) -> serializer),
- haskell: string * (string list -> serializer)
+ haskell: string * (string * string list -> serializer)
};
val mk_flat_ml_resolver: string list -> string -> string;
val ml_fun_datatype: string * string * (string -> bool)
@@ -259,10 +259,10 @@
|> postprocess_module name
end;
-fun constructive_fun (name, (eqs, ty)) =
+fun constructive_fun is_cons (name, (eqs, ty)) =
let
fun check_eq (eq as (lhs, rhs)) =
- if forall CodegenThingol.is_pat lhs
+ if forall (CodegenThingol.is_pat is_cons) lhs
then SOME eq
else (warning ("in function " ^ quote name ^ ", throwing away one "
^ "non-executable function clause"); NONE)
@@ -342,22 +342,24 @@
val ml_from_label =
str o translate_string (fn "_" => "__" | "." => "_" | c => c)
o NameSpace.base o resolv;
- fun ml_from_tyvar (v, sort) =
- let
- fun mk_class v class =
- str (prefix "'" v ^ " " ^ resolv class);
- in
- Pretty.block [
- str "(",
- str v,
- str ":",
- case sort
- of [] => str "unit"
- | [class] => mk_class v class
- | _ => Pretty.enum " *" "" "" (map (mk_class v) sort),
- str ")"
- ]
- end;
+ fun ml_from_tyvar (v, []) =
+ str "()"
+ | ml_from_tyvar (v, sort) =
+ let
+ val w = (Char.toString o Char.toUpper o the o Char.fromString) v;
+ fun mk_class class =
+ str (prefix "'" v ^ " " ^ resolv class);
+ in
+ Pretty.block [
+ str "(",
+ str w,
+ str ":",
+ case sort
+ of [class] => mk_class class
+ | _ => Pretty.enum " *" "" "" (map mk_class sort),
+ str ")"
+ ]
+ end;
fun ml_from_sortlookup fxy lss =
let
fun from_label l =
@@ -365,16 +367,17 @@
if (is_some o Int.fromString) l then str l
else ml_from_label l
];
- fun from_lookup fxy [] p = p
- | from_lookup fxy [l] p =
+ fun from_lookup fxy [] v =
+ v
+ | from_lookup fxy [l] v =
brackify fxy [
from_label l,
- p
+ v
]
- | from_lookup fxy ls p =
+ | from_lookup fxy ls v =
brackify fxy [
Pretty.enum " o" "(" ")" (map from_label ls),
- p
+ v
];
fun from_classlookup fxy (Instance (inst, lss)) =
brackify fxy (
@@ -382,9 +385,11 @@
:: map (ml_from_sortlookup BR) lss
)
| from_classlookup fxy (Lookup (classes, (v, ~1))) =
- from_lookup BR classes (str v)
+ from_lookup BR classes
+ ((str o Char.toString o Char.toUpper o the o Char.fromString) v)
| from_classlookup fxy (Lookup (classes, (v, i))) =
- from_lookup BR (string_of_int (i+1) :: classes) (str v)
+ from_lookup BR (string_of_int (i+1) :: classes)
+ ((str o Char.toString o Char.toUpper o the o Char.fromString) v)
in case lss
of [] => str "()"
| [ls] => from_classlookup fxy ls
@@ -596,7 +601,7 @@
:: map (mk_eq "|") eq_tl
)
end;
- val def' :: defs' = map (apsnd eta_expand_poly_fun o constructive_fun) defs
+ val def' :: defs' = map (apsnd eta_expand_poly_fun o constructive_fun is_cons) defs
in
chunk_defs (
(mk_fun (the (fold check_args defs NONE))) def'
@@ -653,6 +658,7 @@
| _ => error ("class block without class: " ^ (commas o map (quote o fst)) defs)
fun ml_from_class (name, (supclasses, (v, membrs))) =
let
+ val w = (Char.toString o Char.toUpper o the o Char.fromString) v;
fun from_supclass class =
Pretty.block [
ml_from_label class,
@@ -673,10 +679,10 @@
(Pretty.block o Pretty.breaks) [
str "fun",
(str o resolv) m,
- Pretty.enclose "(" ")" [str (v ^ ":'" ^ v ^ " " ^ resolv name)],
+ Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ resolv name)],
str "=",
Pretty.block [str "#", ml_from_label m],
- str (v ^ ";")
+ str (w ^ ";")
];
in
Pretty.chunks (
@@ -706,15 +712,12 @@
| 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)) =
- (Pretty.block o Pretty.breaks) (
- ml_from_label supclass
- :: str "="
- :: (str o resolv) supinst
- :: (if null lss andalso (not o null) arity
- then [str "()"]
- else map (ml_from_sortlookup NOBR) lss)
- );
+ fun from_supclass (supclass, ls) =
+ (Pretty.block o Pretty.breaks) [
+ ml_from_label supclass,
+ str "=",
+ ml_from_sortlookup NOBR ls
+ ];
fun from_memdef (m, ((m', def), lss)) =
(ml_from_funs [(m', def)], (Pretty.block o Pretty.breaks) (
ml_from_label m
@@ -831,7 +834,7 @@
local
-fun hs_from_defs with_typs (class_syntax, tyco_syntax, const_syntax)
+fun hs_from_defs (is_cons, with_typs) (class_syntax, tyco_syntax, const_syntax)
resolver prefix defs =
let
val resolv = resolver "";
@@ -965,7 +968,7 @@
Pretty.brk 1,
hs_from_expr NOBR rhs
]
- in Pretty.chunks ((map from_eq o fst o snd o constructive_fun) def) end;
+ in Pretty.chunks ((map from_eq o fst o snd o constructive_fun is_cons) def) end;
fun hs_from_def (name, CodegenThingol.Fun (def as (_, (sctxt, ty)))) =
let
val body = hs_from_funeqs (name, def);
@@ -1044,7 +1047,7 @@
in
-fun hs_from_thingol target nsps_upper nspgrp =
+fun hs_from_thingol target (nsp_dtcon, nsps_upper) nspgrp =
let
val reserved_hs = [
"hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
@@ -1053,6 +1056,7 @@
] @ [
"Bool", "Integer", "Maybe", "True", "False", "Nothing", "Just", "not", "negate"
];
+ fun is_cons c = CodegenThingol.has_nsp c nsp_dtcon;
fun hs_from_module resolv imps ((_, name), ps) =
(Pretty.chunks) (
str ("module " ^ name ^ " where")
@@ -1068,7 +1072,7 @@
else ch_first Char.toLower n
end;
fun serializer with_typs = abstract_serializer (target, nspgrp)
- "Main" (hs_from_defs with_typs, hs_from_module, abstract_validator reserved_hs, postproc);
+ "Main" (hs_from_defs (is_cons, with_typs), hs_from_module, abstract_validator reserved_hs, postproc);
fun eta_expander const_syntax c =
const_syntax c
|> Option.map (fst o fst)
--- a/src/Pure/Tools/codegen_theorems.ML Tue Jun 27 10:09:48 2006 +0200
+++ b/src/Pure/Tools/codegen_theorems.ML Tue Jun 27 10:10:20 2006 +0200
@@ -21,10 +21,11 @@
val notify_dirty: theory -> theory;
val proper_name: string -> string;
+ val extr_typ: theory -> thm -> typ;
val common_typ: theory -> (thm -> typ) -> thm list -> thm list;
- val preprocess: theory -> thm list -> (typ * thm list) option;
+ val preprocess: theory -> thm list -> thm list;
- val get_funs: theory -> string * typ -> (typ * thm list) option;
+ val get_funs: theory -> string * typ -> thm list;
val get_datatypes: theory -> string
-> (((string * sort) list * (string * typ list) list) * thm list) option;
@@ -95,7 +96,7 @@
structure CodegenTheoremsSetup = TheoryDataFun
(struct
- val name = "Pure/CodegenTheoremsSetup";
+ val name = "Pure/codegen_theorems_setup";
type T = ((string * thm) * ((string * string) * (string * string))) option;
val empty = NONE;
val copy = I;
@@ -409,7 +410,7 @@
structure CodegenTheoremsData = TheoryDataFun
(struct
- val name = "Pure/CodegenTheoremsData";
+ val name = "Pure/codegen_theorems_data";
type T = T;
val empty = mk_T ((false, mk_notify []), (mk_preproc ([], []),
(mk_extrs ([], []), mk_funthms ([], Symtab.empty))));
@@ -566,6 +567,9 @@
(* preprocessing *)
+fun extr_typ thy thm = case dest_fun thy thm
+ of (_, (ty, _)) => ty;
+
fun common_typ thy _ [] = []
| common_typ thy _ [thm] = [thm]
| common_typ thy extract_typ thms =
@@ -591,12 +595,8 @@
|> Conjunction.intr_list
|> f
|> Conjunction.elim_list;
- fun extr_typ thm = case dest_fun thy thm
- of (_, (ty, _)) => ty;
- fun tap_typ [] = NONE
- | tap_typ (thms as (thm::_)) = SOME (extr_typ thm, thms);
fun cmp_thms (thm1, thm2) =
- not (Sign.typ_instance thy (extr_typ thm1, extr_typ thm2));
+ not (Sign.typ_instance thy (extr_typ thy thm1, extr_typ thy thm2));
fun rewrite_rhs conv thm = (case (Drule.strip_comb o cprop_of) thm
of (ct', [ct1, ct2]) => (case term_of ct'
of Const ("==", _) =>
@@ -617,7 +617,7 @@
|> sort (make_ord cmp_thms)
|> debug_msg (fn _ => "[cg_thm] common_typ")
|> debug_msg (commas o map string_of_thm)
- |> common_typ thy extr_typ
+ |> common_typ thy (extr_typ thy)
|> debug_msg (fn _ => "[cg_thm] abs_norm")
|> debug_msg (commas o map string_of_thm)
|> map (abs_norm thy)
@@ -633,8 +633,6 @@
#> Drule.zero_var_indexes
)
|> drop_redundant thy
- |> unvarify
- |> tap_typ
end;
--- a/src/Pure/Tools/codegen_thingol.ML Tue Jun 27 10:09:48 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML Tue Jun 27 10:10:20 2006 +0200
@@ -57,7 +57,7 @@
((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 is_pat: (string -> bool) -> iexpr -> bool;
val map_pure: (iexpr -> 'a) -> iexpr -> 'a;
val resolve_tycos: (string -> string) -> itype * iexpr list -> itype * iexpr list;
val resolve_consts: (string -> string) -> iexpr -> iexpr;
@@ -74,7 +74,7 @@
| Class of class list * (vname * (string * (sortcontext * itype)) list)
| Classmember of class
| Classinst of ((class * (string * (vname * sort) list))
- * (class * (string * iclasslookup list list)) list)
+ * (class * iclasslookup list) list)
* (string * ((string * funn) * iclasslookup list list)) list
| Classinstmember;
type module;
@@ -304,13 +304,13 @@
| instant y = map_itype instant y;
in instant end;
-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 as IChar _) = true
- | is_pat e = false;
+fun is_pat is_cons (e as IConst (c, ([], _))) = is_cons c
+ | is_pat _ (e as IVar _) = true
+ | is_pat is_cons (e as (e1 `$ e2)) =
+ is_pat is_cons e1 andalso is_pat is_cons e2
+ | is_pat _ (e as INum _) = true
+ | is_pat _ (e as IChar _) = true
+ | is_pat _ _ = false;
fun map_pure f (e as IConst _) =
f e
@@ -397,7 +397,7 @@
| Class of class list * (vname * (string * (sortcontext * itype)) list)
| Classmember of class
| Classinst of ((class * (string * (vname * sort) list))
- * (class * (string * iclasslookup list list)) list)
+ * (class * iclasslookup list) list)
* (string * ((string * funn) * iclasslookup list list)) list
| Classinstmember;
@@ -668,7 +668,7 @@
|> (pair defs #> PN);
fun select (PN (defs, modls)) (Module module) =
module
- |> Graph.subgraph (Graph.all_succs module (defs @ map fst modls))
+ |> Graph.project (member (op =) (Graph.all_succs module (defs @ map fst modls)))
|> fold (fn (name, modls) => Graph.map_node name (select modls)) modls
|> Module;
in
@@ -1003,7 +1003,6 @@
(map (fn (name, Def def) => (fst (mk_name prfx name), def)) ds)
in
seri_module (resolver []) (map (resolver []) ((the o Symtab.lookup imptab) ""))
- (*map (resolver []) (Graph.strong_conn module |> flat |> rev)*)
(("", name_root), (mk_contents [] module))
end;