# HG changeset patch # User haftmann # Date 1151395820 -7200 # Node ID 2f54a51f18015c3381f7951a0afc9b0924f0ca87 # Parent eaf2c25654d3cd9cf80fb8d99731c272aa704596 class package refinements, slight code generation refinements diff -r eaf2c25654d3 -r 2f54a51f1801 src/Pure/Tools/class_package.ML --- 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 *) diff -r eaf2c25654d3 -r 2f54a51f1801 src/Pure/Tools/codegen_package.ML --- 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 diff -r eaf2c25654d3 -r 2f54a51f1801 src/Pure/Tools/codegen_serializer.ML --- 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) diff -r eaf2c25654d3 -r 2f54a51f1801 src/Pure/Tools/codegen_theorems.ML --- 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; diff -r eaf2c25654d3 -r 2f54a51f1801 src/Pure/Tools/codegen_thingol.ML --- 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;