--- a/src/Pure/Tools/class_package.ML Tue Feb 14 13:03:00 2006 +0100
+++ b/src/Pure/Tools/class_package.ML Tue Feb 14 17:07:11 2006 +0100
@@ -58,13 +58,13 @@
structure ClassData = TheoryDataFun (
struct
val name = "Pure/classes";
- type T = class_data Symtab.table * class Symtab.table;
- val empty = (Symtab.empty, Symtab.empty);
+ type T = class_data Symtab.table * (class Symtab.table * string Symtab.table);
+ val empty = (Symtab.empty, (Symtab.empty, Symtab.empty));
val copy = I;
val extend = I;
- fun merge _ ((t1, r1), (t2, r2))=
+ fun merge _ ((t1, (c1, l1)), (t2, (c2, l2)))=
(Symtab.merge (op =) (t1, t2),
- Symtab.merge (op =) (r1, r2));
+ (Symtab.merge (op =) (c1, c2), Symtab.merge (op =) (l1, l2)));
fun print thy (tab, _) =
let
fun pretty_class (name, {superclasses, name_locale, name_axclass, var, consts, insts}) =
@@ -95,218 +95,18 @@
val _ = Context.add_setup ClassData.init;
val print_classes = ClassData.print;
+
+(* queries *)
+
val lookup_class_data = Symtab.lookup o fst o ClassData.get;
-val lookup_const_class = Symtab.lookup o snd o ClassData.get;
+val lookup_const_class = Symtab.lookup o fst o snd o ClassData.get;
+val lookup_locale_class = Symtab.lookup o snd o snd o ClassData.get;
-fun get_class_data thy class =
+fun the_class_data thy class =
case lookup_class_data thy class
of NONE => error ("undeclared operational class " ^ quote class)
| SOME data => data;
-fun add_class_data (class, (superclasses, name_locale, name_axclass, classvar, consts)) =
- ClassData.map (fn (classtab, consttab) => (
- classtab
- |> Symtab.update (class, {
- superclasses = superclasses,
- name_locale = name_locale,
- name_axclass = name_axclass,
- var = classvar,
- consts = consts,
- insts = []
- }),
- consttab
- |> fold (fn (c, _) => Symtab.update (c, class)) consts
- ));
-
-fun add_inst_data (class, inst) =
- (ClassData.map o apfst o Symtab.map_entry class)
- (fn {superclasses, name_locale, name_axclass, var, consts, insts}
- => {
- superclasses = superclasses,
- name_locale = name_locale,
- name_axclass = name_axclass,
- var = var,
- consts = consts,
- insts = insts @ [inst]
- });
-
-
-(* name handling *)
-
-fun certify_class thy class =
- (get_class_data thy class; class);
-
-fun intern_class thy raw_class =
- certify_class thy (Sign.intern_class thy raw_class);
-
-fun extern_class thy class =
- Sign.extern_class thy (certify_class thy class);
-
-
-(* classes and instances *)
-
-fun subst_clsvar v ty_subst =
- map_type_tfree (fn u as (w, _) =>
- if w = v then ty_subst else TFree u);
-
-local
-
-fun gen_add_class add_locale prep_class do_proof bname raw_supclasses raw_body thy =
- let
- val supclasses = map (prep_class thy) raw_supclasses;
- fun get_allcs class =
- let
- val data = get_class_data thy class
- in
- Library.flat (map get_allcs (#superclasses data) @ [#consts data])
- end;
- val supcs = Library.flat (map get_allcs supclasses)
- val supsort = case map (#name_axclass o get_class_data thy) supclasses
- of [] => Sign.defaultS thy
- | sort => Sorts.certify_sort (Sign.classes_of thy) sort;
- val locexpr = case supclasses
- of [] => Locale.empty
- | _ => (Locale.Merge o map (Locale.Locale o #name_locale o get_class_data thy))
- supclasses;
- fun mk_c_lookup c_global supcs c_adds =
- map2 (fn ((c, _), _) => pair c) c_global supcs @ c_adds
- fun extract_tyvar_consts thy name_locale =
- let
- fun extract_tyvar_name thy tys =
- fold (curry add_typ_tfrees) tys []
- |> (fn [(v, sort)] =>
- if Sorts.sort_le (Sign.classes_of thy) (swap (sort, supsort))
- then v
- else error ("illegal sort constraint on class type variable: " ^ Sign.string_of_sort thy sort)
- | [] => error ("no class type variable")
- | vs => error ("more than one type variable: " ^ (commas o map (Sign.string_of_typ thy o TFree)) vs))
- val raw_consts =
- Locale.parameters_of thy name_locale
- |> map (apsnd Syntax.unlocalize_mixfix)
- |> ((curry splitAt o length) supcs);
- val v = (extract_tyvar_name thy o map (snd o fst) o op @) raw_consts;
- fun subst_ty cs =
- map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) cs;
- val consts = (subst_ty (fst raw_consts), subst_ty (snd raw_consts));
- val _ = (writeln o commas o map (fst o fst)) (fst consts);
- val _ = (writeln o commas o map (fst o fst)) (snd consts);
- in (v, consts) end;
- fun add_global_const v ((c, ty), syn) thy =
- thy
- |> Sign.add_consts_i [(c, ty |> subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)]
- |> `(fn thy => (c, (Sign.intern_const thy c |> print, ty)))
- fun extract_assumes thy name_locale c_lookup =
- Locale.local_asms_of thy name_locale
- |> map snd
- |> Library.flat
- |> (map o map_aterms) (fn Free (c, ty) => Const ((fst o the o AList.lookup (op =) c_lookup) c, ty)
- | t => t)
- |> tap (fn ts => writeln ("(1) axclass axioms: " ^
- (commas o map (Sign.string_of_term thy)) ts));
- fun add_global_constraint v class (_, (c, ty)) thy =
- thy
- |> Sign.add_const_constraint_i (c, subst_clsvar v (TVar ((v, 0), [class])) ty);
- fun interpret name_locale cs ax_axioms thy =
- thy
- |> Locale.interpretation (NameSpace.base name_locale, [])
- (Locale.Locale name_locale) (map (SOME o fst) cs)
- |> do_proof ax_axioms;
- in
- thy
- |> add_locale bname locexpr raw_body
- |-> (fn ctxt =>
- `(fn thy => Locale.intern thy bname)
- #-> (fn name_locale =>
- `(fn thy => extract_tyvar_consts thy name_locale)
- #-> (fn (v, (c_global, c_defs)) =>
- fold_map (add_global_const v) c_defs
- #-> (fn c_adds =>
- `(fn thy => extract_assumes thy name_locale (mk_c_lookup c_global supcs c_adds))
- #-> (fn assumes =>
- AxClass.add_axclass_i (bname, supsort) (map (Thm.no_attributes o pair "") assumes))
- #-> (fn { axioms = ax_axioms : thm list, ...} =>
- `(fn thy => Sign.intern_class thy bname)
- #-> (fn name_axclass =>
- fold (add_global_constraint v name_axclass) c_adds
- #> add_class_data (name_locale, (supclasses, name_locale, name_axclass, v, map snd c_adds))
- #> interpret name_locale (supcs @ (map (fn ((c, ty), _) => (Sign.intern_const thy c, ty)) c_defs)) ax_axioms
- ))))))
- end;
-
-in
-
-val add_class = gen_add_class (Locale.add_locale true) intern_class
- (fn ax_axioms => Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE));
-val add_class_i = gen_add_class (Locale.add_locale_i true) certify_class
- (fn ax_axioms => Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE));
-val add_class_exp = gen_add_class (Locale.add_locale true) intern_class
- (K I);
-
-end; (* local *)
-
-fun gen_instance_arity prep_arity add_defs tap_def raw_arity raw_defs thy =
- let
- val pp = Sign.pp thy;
- val arity as (tyco, asorts, sort) = prep_arity thy ((fn ((x, y), z) => (x, y, z)) raw_arity);
- val ty_inst = Type (tyco, map2 (curry TVar o rpair 0) (Term.invent_names [] "'a" (length asorts)) asorts)
- fun get_c_req class =
- let
- val data = get_class_data thy class;
- val subst_ty = map_type_tfree (fn (var as (v, _)) =>
- if #var data = v then ty_inst else TFree var)
- in (map (apsnd subst_ty) o #consts) data end;
- val c_req = (Library.flat o map get_c_req) sort;
- fun get_remove_contraint c thy =
- let
- val ty1 = Sign.the_const_constraint thy c;
- val ty2 = Sign.the_const_type thy c;
- in
- thy
- |> Sign.add_const_constraint_i (c, ty2)
- |> pair (c, ty1)
- end;
- fun check_defs raw_defs c_req thy =
- let
- val thy' = thy |> Theory.copy |> Sign.add_arities_i [(tyco, asorts, sort)];
- fun get_c raw_def =
- (fst o Sign.cert_def pp o snd o tap_def thy' o fst) raw_def;
- val c_given = map get_c raw_defs;
-(* spec_opt_name *)
- fun eq_c ((c1, ty1), (c2, ty2)) =
- let
- val ty1' = Type.varifyT ty1;
- val ty2' = Type.varifyT ty2;
- in
- c1 = c2
- andalso Sign.typ_instance thy (ty1', ty2')
- andalso Sign.typ_instance thy (ty2', ty1')
- end;
- val _ = case fold (remove eq_c) c_req c_given
- of [] => ()
- | cs => error ("superfluous definition(s) given for "
- ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);
- val _ = case fold (remove eq_c) c_given c_req
- of [] => ()
- | cs => error ("no definition(s) given for "
- ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);
- in thy end;
- fun after_qed cs =
- fold Sign.add_const_constraint_i cs
- #> fold (fn class => add_inst_data (class, (tyco, Context.theory_name thy))) sort;
- in
- thy
- |> tap (fn thy => check_defs raw_defs c_req thy)
- |> fold_map get_remove_contraint (map fst c_req)
- ||> add_defs (true, raw_defs)
- |-> (fn cs => AxClass.instance_arity_i (after_qed cs) arity)
- end;
-
-val add_instance_arity = gen_instance_arity (AxClass.read_arity) IsarThy.add_defs read_axm;
-val add_instance_arity_i = gen_instance_arity (AxClass.cert_arity) IsarThy.add_defs_i (K I);
-
-
-(* queries *)
-
fun is_class thy cls =
lookup_class_data thy cls
|> Option.map (not o null o #consts)
@@ -333,24 +133,33 @@
else
error ("no syntactic class: " ^ class);
+fun the_ancestry thy classes =
+ let
+ fun ancestry class anc =
+ anc
+ |> cons class
+ |> fold ancestry (the_superclasses thy class);
+ in fold ancestry classes [] end;
+
+fun subst_clsvar v ty_subst =
+ map_type_tfree (fn u as (w, _) =>
+ if w = v then ty_subst else TFree u);
+
fun the_consts_sign thy class =
let
- val data = (the oo Symtab.lookup) ((fst o ClassData.get) thy) class
+ val data = the_class_data thy class
in (#var data, #consts data) end;
-fun lookup_const_class thy =
- Symtab.lookup ((snd o ClassData.get) thy);
-
-fun the_instances thy class =
- (#insts o the o Symtab.lookup ((fst o ClassData.get) thy)) class;
+val the_instances =
+ #insts oo the_class_data;
fun the_inst_sign thy (class, tyco) =
let
val _ = if is_class thy class then () else error ("no syntactic class: " ^ class);
- val arity =
+ val arity =
Sorts.mg_domain (Sign.classes_arities_of thy) tyco [class]
|> map (operational_sort_of thy);
- val clsvar = (#var o the o Symtab.lookup ((fst o ClassData.get) thy)) class;
+ val clsvar = (#var o the_class_data thy) class;
val const_sign = (snd o the_consts_sign thy) class;
fun add_var sort used =
let
@@ -372,6 +181,218 @@
((fst o ClassData.get) thy) Symtab.empty;
+(* updaters *)
+
+fun add_class_data (class, (superclasses, name_locale, name_axclass, classvar, consts)) =
+ ClassData.map (fn (classtab, (consttab, loctab)) => (
+ classtab
+ |> Symtab.update (class, {
+ superclasses = superclasses,
+ name_locale = name_locale,
+ name_axclass = name_axclass,
+ var = classvar,
+ consts = consts,
+ insts = []
+ }),
+ (consttab
+ |> fold (fn (c, _) => Symtab.update (c, class)) consts,
+ loctab
+ |> Symtab.update (name_locale, class))
+ ));
+
+fun add_inst_data (class, inst) =
+ (ClassData.map o apfst o Symtab.map_entry class)
+ (fn {superclasses, name_locale, name_axclass, var, consts, insts}
+ => {
+ superclasses = superclasses,
+ name_locale = name_locale,
+ name_axclass = name_axclass,
+ var = var,
+ consts = consts,
+ insts = insts @ [inst]
+ });
+
+
+(* name handling *)
+
+fun certify_class thy class =
+ (the_class_data thy class; class);
+
+fun intern_class thy raw_class =
+ certify_class thy (Sign.intern_class thy raw_class);
+
+fun extern_class thy class =
+ Sign.extern_class thy (certify_class thy class);
+
+
+(* classes and instances *)
+
+local
+
+fun intern_expr thy (Locale.Locale xname) = Locale.Locale (Locale.intern thy xname)
+ | intern_expr thy (Locale.Merge exprs) = Locale.Merge (map (intern_expr thy) exprs)
+ | intern_expr thy (Locale.Rename (expr, xs)) = Locale.Rename (intern_expr thy expr, xs);
+
+fun gen_add_class add_locale prep_expr eval_expr do_proof bname raw_expr raw_body thy =
+ let
+ val ((import_asms, supclasses), locexpr) = (eval_expr thy o prep_expr thy) raw_expr;
+ val supsort =
+ supclasses
+ |> map (#name_axclass o the_class_data thy)
+ |> Sorts.certify_sort (Sign.classes_of thy)
+ |> null ? K (Sign.defaultS thy);
+ val _ = writeln ("got sort: " ^ Sign.string_of_sort thy supsort);
+ val _ = writeln ("got asms: " ^ (cat_lines o map (Sign.string_of_term thy) o Library.flat o map (snd o fst)) import_asms);
+ val supcs = (Library.flat o map (snd o the_consts_sign thy) o the_ancestry thy) supclasses;
+ fun mk_c_lookup c_global supcs c_adds =
+ map2 (fn ((c, _), _) => pair c) c_global supcs @ c_adds;
+ fun extract_tyvar_consts thy name_locale =
+ let
+ fun extract_tyvar_name thy tys =
+ fold (curry add_typ_tfrees) tys []
+ |> (fn [(v, sort)] =>
+ if Sorts.sort_le (Sign.classes_of thy) (swap (sort, supsort))
+ then v
+ else error ("illegal sort constraint on class type variable: " ^ Sign.string_of_sort thy sort)
+ | [] => error ("no class type variable")
+ | vs => error ("more than one type variable: " ^ (commas o map (Sign.string_of_typ thy o TFree)) vs))
+ val raw_consts =
+ Locale.parameters_of thy name_locale
+ |> map (apsnd Syntax.unlocalize_mixfix)
+ |> Library.chop (length supcs);
+ val v = (extract_tyvar_name thy o map (snd o fst) o op @) raw_consts;
+ fun subst_ty cs =
+ map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) cs;
+ val consts = (subst_ty (fst raw_consts), subst_ty (snd raw_consts));
+ (*val _ = (writeln o commas o map (fst o fst)) (fst consts);
+ val _ = (writeln o commas o map (fst o fst)) (snd consts);*)
+ in (v, consts) end;
+ fun add_global_const v ((c, ty), syn) thy =
+ thy
+ |> Sign.add_consts_i [(c, ty |> subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)]
+ |> `(fn thy => (c, (Sign.intern_const thy c, ty)))
+ fun subst_assume c_lookup renaming =
+ map_aterms (fn Free (c, ty) => Const ((fst o the o AList.lookup (op =) c_lookup o perhaps (AList.lookup (op =) renaming)) c, ty)
+ | t => t)
+ fun extract_assumes thy name_locale c_lookup =
+ map (rpair []) (Locale.local_asms_of thy name_locale) @ import_asms
+ |> map (fn (((name, atts), ts), renaming) => ((name, map (Attrib.attribute thy) atts), (map (subst_assume c_lookup renaming)) ts));
+ fun rearrange_assumes ((name, atts), ts) =
+ map (rpair atts o pair "") ts
+ fun add_global_constraint v class (_, (c, ty)) thy =
+ thy
+ |> Sign.add_const_constraint_i (c, subst_clsvar v (TVar ((v, 0), [class])) ty);
+ fun ad_hoc_const thy class v (c, ty) =
+ let
+ val ty' = subst_clsvar v (TFree (v, [class])) ty;
+ val s_ty = setmp print_mode [] (setmp show_types true (setmp show_sorts true (Sign.string_of_typ thy))) ty';
+ val s = c ^ "::" ^ enclose "(" ")" s_ty;
+ val _ = writeln ("our constant: " ^ s);
+ in SOME s end;
+ fun interpret name_locale name_axclass v cs ax_axioms thy =
+ thy
+ |> Locale.interpretation (NameSpace.base name_locale, [])
+ (Locale.Locale name_locale) (map (ad_hoc_const thy name_axclass v) cs)
+ |> do_proof ax_axioms;
+ in
+ thy
+ |> add_locale bname locexpr raw_body
+ |-> (fn ctxt =>
+ `(fn thy => Locale.intern thy bname)
+ #-> (fn name_locale =>
+ `(fn thy => extract_tyvar_consts thy name_locale)
+ #-> (fn (v, (c_global, c_defs)) =>
+ fold_map (add_global_const v) c_defs
+ #-> (fn c_adds =>
+ `(fn thy => extract_assumes thy name_locale (mk_c_lookup c_global supcs c_adds))
+ #-> (fn assumes =>
+ AxClass.add_axclass_i (bname, supsort) ((Library.flat o map rearrange_assumes) assumes))
+ #-> (fn { axioms = ax_axioms : thm list, ...} =>
+ `(fn thy => Sign.intern_class thy bname)
+ #-> (fn name_axclass =>
+ fold (add_global_constraint v name_axclass) c_adds
+ #> add_class_data (name_locale, (supclasses, name_locale, name_axclass, v, map snd c_adds))
+ #> interpret name_locale name_axclass v (supcs @ map snd c_adds) ax_axioms
+ ))))))
+ end;
+
+fun eval_expr_supclasses thy [] = (([], []), Locale.empty)
+ | eval_expr_supclasses thy supclasses =
+ (([], supclasses),
+ (Locale.Merge o map (Locale.Locale o #name_locale o the_class_data thy)) supclasses);
+
+in
+
+val add_class = gen_add_class (Locale.add_locale true) (map o intern_class)
+ eval_expr_supclasses (fn ax_axioms => Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE));
+val add_class_i = gen_add_class (Locale.add_locale_i true) (map o certify_class)
+ eval_expr_supclasses (fn ax_axioms => Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE));
+val add_class_exp = gen_add_class (Locale.add_locale true) (map o intern_class)
+ eval_expr_supclasses (K I);
+
+end; (* local *)
+
+fun gen_instance_arity prep_arity add_defs tap_def raw_arity raw_defs thy =
+ let
+ val pp = Sign.pp thy;
+ val arity as (tyco, asorts, sort) = prep_arity thy ((fn ((x, y), z) => (x, y, z)) raw_arity);
+ val ty_inst = Type (tyco, map2 (curry TVar o rpair 0) (Term.invent_names [] "'a" (length asorts)) asorts)
+ fun get_c_req class =
+ let
+ val data = the_class_data thy class;
+ val subst_ty = map_type_tfree (fn (var as (v, _)) =>
+ if #var data = v then ty_inst else TFree var)
+ in (map (apsnd subst_ty) o #consts) data end;
+ val c_req = (Library.flat o map get_c_req) sort;
+ fun get_remove_contraint c thy =
+ let
+ val ty1 = Sign.the_const_constraint thy c;
+ val ty2 = Sign.the_const_type thy c;
+ in
+ thy
+ |> Sign.add_const_constraint_i (c, ty2)
+ |> pair (c, ty1)
+ end;
+ fun check_defs raw_defs c_req thy =
+ let
+ val thy' = thy |> Theory.copy |> Sign.add_arities_i [(tyco, asorts, sort)];
+ fun get_c raw_def =
+ (fst o Sign.cert_def pp o snd o tap_def thy' o fst) raw_def;
+ val c_given = map get_c raw_defs;
+(* spec_opt_name *)
+ fun eq_c ((c1, ty1), (c2, ty2)) =
+ let
+ val ty1' = Type.varifyT ty1;
+ val ty2' = Type.varifyT ty2;
+ in
+ c1 = c2
+ andalso Sign.typ_instance thy (ty1', ty2')
+ andalso Sign.typ_instance thy (ty2', ty1')
+ end;
+ val _ = case fold (remove eq_c) c_req c_given
+ of [] => ()
+ | cs => error ("superfluous definition(s) given for "
+ ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);
+ (*val _ = case fold (remove eq_c) c_given c_req
+ of [] => ()
+ | cs => error ("no definition(s) given for "
+ ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);*)
+ in thy end;
+ fun after_qed cs =
+ fold Sign.add_const_constraint_i cs
+ #> fold (fn class => add_inst_data (class, (tyco, Context.theory_name thy))) sort;
+ in
+ thy
+ |> tap (fn thy => check_defs raw_defs c_req thy)
+ |> fold_map get_remove_contraint (map fst c_req)
+ ||> add_defs (true, raw_defs)
+ |-> (fn cs => AxClass.instance_arity_i (after_qed cs) arity)
+ end;
+
+val add_instance_arity = gen_instance_arity (AxClass.read_arity) IsarThy.add_defs read_axm;
+val add_instance_arity_i = gen_instance_arity (AxClass.cert_arity) IsarThy.add_defs_i (K I);
+
+
(* extracting dictionary obligations from types *)
type sortcontext = (string * sort) list;
@@ -434,7 +455,7 @@
of NONE => ctxt
| SOME class =>
let
- val data = (the o Symtab.lookup ((fst o ClassData.get) thy)) class;
+ val data = the_class_data thy class;
val sign = (Type.varifyT o the o AList.lookup (op =) (#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)
@@ -467,7 +488,7 @@
raw_cs
|> map (Sign.intern_const thy)
|> map (fn c => (c, Sign.the_const_constraint thy c));
- val used =
+ val used =
[]
|> fold (fn (_, ty) => curry (gen_union (op =))
((map (fst o fst) o typ_tvars) ty @ (map fst o typ_tfrees) ty)) cs_proto
@@ -511,6 +532,11 @@
)
>> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort))
+val locale_val =
+ (P.locale_expr --
+ Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 P.context_element)) [] ||
+ Scan.repeat1 P.context_element >> pair Locale.empty);
+
val classP =
OuterSyntax.command classK "operational type classes" K.thy_decl (
P.name --| P.$$$ "="
@@ -524,7 +550,7 @@
P.name --| P.$$$ "="
-- Scan.optional (Scan.repeat1 (P.name --| P.$$$ "+")) []
-- Scan.optional (P.!!! (Scan.repeat1 P.context_element)) []
- >> (Toplevel.print oo Toplevel.theory_to_proof
+ >> ((Toplevel.print oo Toplevel.theory_to_proof)
o (fn ((bname, supclasses), elems) => add_class_exp bname supclasses elems)));
val instanceP =
--- a/src/Pure/Tools/codegen_package.ML Tue Feb 14 13:03:00 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML Tue Feb 14 17:07:11 2006 +0100
@@ -46,6 +46,7 @@
-> appgen;
val appgen_number_of: (term -> term) -> (theory -> term -> IntInf.int) -> string -> string
-> appgen;
+ val appgen_wfrec: appgen;
val eqextr_eq: (theory -> string -> thm list) -> term
-> eqextr_default;
val add_case_const: (theory -> string -> (string * int) list option) -> xstring
@@ -84,6 +85,10 @@
(* shallow name spaces *)
+val alias_ref = ref (fn thy : theory => fn s : string => s, fn thy : theory => fn s : string => s);
+fun alias_get name = (fst o !) alias_ref name;
+fun alias_rev name = (snd o !) alias_ref name;
+
val nsp_module = ""; (* a dummy by convention *)
val nsp_class = "class";
val nsp_tyco = "tyco";
@@ -93,11 +98,43 @@
val nsp_mem = "mem";
val nsp_inst = "inst";
+fun add_nsp shallow name =
+ name
+ |> NameSpace.unpack
+ |> split_last
+ |> apsnd (single #> cons shallow)
+ |> (op @)
+ |> NameSpace.pack;
+
+fun dest_nsp nsp idf =
+ let
+ val idf' = NameSpace.unpack idf;
+ val (idf'', idf_base) = split_last idf';
+ val (modl, shallow) = split_last idf'';
+ in
+ if nsp = shallow
+ then (SOME o NameSpace.pack) (modl @ [idf_base])
+ else NONE
+ end;
+
+fun idf_of_name thy shallow name =
+ name
+ |> alias_get thy
+ |> add_nsp shallow;
+
+fun name_of_idf thy shallow idf =
+ idf
+ |> dest_nsp shallow
+ |> Option.map (alias_rev thy);
+
(* code generator basics *)
-val alias_ref = ref (fn thy : theory => fn s : string => s);
-fun alias_get name = ! alias_ref name;
+type deftab = (typ * (thm * string)) list Symtab.table;
+
+fun eq_typ thy (ty1, ty2) =
+ Sign.typ_instance thy (ty1, ty2)
+ andalso Sign.typ_instance thy (ty2, ty1);
structure InstNameMangler = NameManglerFun (
type ctxt = theory;
@@ -112,11 +149,19 @@
);
structure ConstNameMangler = NameManglerFun (
- type ctxt = theory;
+ type ctxt = theory * deftab;
type src = string * (typ * typ);
val ord = prod_ord string_ord (prod_ord Term.typ_ord Term.typ_ord);
- fun mk thy ((c, (ty_decl, ty)), i) =
+ fun mk (thy, deftab) ((c, (ty_decl, ty)), i) =
let
+ val thyname = if c = "op ="
+ then
+ (NameSpace.drop_base o alias_get thy o fst o dest_Type o hd o fst o strip_type) ty
+ else (the o get_first
+ (fn (ty', (_, thyname)) => if eq_typ thy (ty, ty') then SOME thyname else NONE)
+ o the o Symtab.lookup deftab) c;
+ val c' = idf_of_name thy nsp_overl c;
+ val c'' = NameSpace.append thyname (NameSpace.append nsp_overl (NameSpace.base c'));
fun mangle (Type (tyco, tys)) =
(NameSpace.base o alias_get thy) tyco :: Library.flat (List.mapPartial mangle tys) |> SOME
| mangle _ =
@@ -128,7 +173,7 @@
|> List.mapPartial mangle
|> Library.flat
|> null ? K ["x"]
- |> cons c
+ |> cons c''
|> space_implode "_"
|> curry (op ^ o swap) ((implode oo replicate) i "'")
end;
@@ -162,7 +207,7 @@
fun re_mangle _ dst = error ("no such datatype constructor: " ^ quote dst);
);
-type auxtab = ((typ * thm) list Symtab.table * string Symtab.table)
+type auxtab = (deftab * string Symtab.table)
* (InstNameMangler.T * ((typ * typ list) Symtab.table * ConstNameMangler.T)
* DatatypeconsNameMangler.T);
type eqextr = theory -> auxtab
@@ -327,7 +372,7 @@
end;
-(* name handling *)
+(* advanced name handling *)
fun add_alias (src, dst) =
map_codegen_data
@@ -338,47 +383,18 @@
(tab |> Symtab.update (src, dst),
tab_rev |> Symtab.update (dst, src))))));
-val _ = alias_ref := (perhaps o Symtab.lookup o fst o #alias o #logic_data o CodegenData.get);
-val alias_rev = perhaps o Symtab.lookup o snd o #alias o #logic_data o CodegenData.get;
-
-fun add_nsp shallow name =
- name
- |> NameSpace.unpack
- |> split_last
- |> apsnd (single #> cons shallow)
- |> (op @)
- |> NameSpace.pack;
+val _ = alias_ref := (perhaps o Symtab.lookup o fst o #alias o #logic_data o CodegenData.get,
+ perhaps o Symtab.lookup o snd o #alias o #logic_data o CodegenData.get);
-fun dest_nsp nsp idf =
- let
- val idf' = NameSpace.unpack idf;
- val (idf'', idf_base) = split_last idf';
- val (modl, shallow) = split_last idf'';
- in
- if nsp = shallow
- then (SOME o NameSpace.pack) (modl @ [idf_base])
- else NONE
- end;
-
-fun idf_of_name thy shallow name =
- name
- |> alias_get thy
- |> add_nsp shallow;
-
-fun name_of_idf thy shallow idf =
- idf
- |> dest_nsp shallow
- |> Option.map (alias_rev thy);
-
-fun idf_of_const thy (tabs as ((_, clsmemtab), (_, (overltab1, overltab2), dtcontab)))
+fun idf_of_const thy (tabs as ((deftab, clsmemtab), (_, (overltab1, overltab2), dtcontab)))
(c, ty) =
let
fun get_overloaded (c, ty) =
case Symtab.lookup overltab1 c
of SOME (ty_decl, tys) =>
(case find_first (curry (Sign.typ_instance thy) ty) tys
- of SOME ty' => ConstNameMangler.get thy overltab2
- (idf_of_name thy nsp_overl c, (ty_decl, ty')) |> SOME
+ of SOME ty' => ConstNameMangler.get (thy, deftab) overltab2
+ (c, (ty_decl, ty')) |> SOME
| _ => NONE)
| _ => NONE
fun get_datatypecons (c, ty) =
@@ -395,15 +411,14 @@
| NONE => idf_of_name thy nsp_const c
end;
-fun recconst_of_idf thy (_, (_, (_, overltab2), _)) idf =
+fun recconst_of_idf thy ((deftab, _), (_, (_, overltab2), _)) idf =
case name_of_idf thy nsp_const idf
of SOME c => SOME (c, Sign.the_const_type thy c)
| NONE => (
case dest_nsp nsp_overl idf
of SOME _ =>
idf
- |> ConstNameMangler.rev thy overltab2
- |> apfst (the o name_of_idf thy nsp_overl)
+ |> ConstNameMangler.rev (thy, deftab) overltab2
|> apsnd snd
|> SOME
| NONE => NONE
@@ -494,10 +509,6 @@
(* sophisticated devarification *)
-fun eq_typ thy (ty1, ty2) =
- Sign.typ_instance thy (ty1, ty2)
- andalso Sign.typ_instance thy (ty2, ty1);
-
fun devarify_typs tys =
let
fun add_rename (vi as (v, _), sorts) used =
@@ -583,7 +594,7 @@
||>> (codegen_type thy tabs o map snd) cs
||>> (fold_map o fold_map) (exprgen_tyvar_sort thy tabs) sortctxts
|-> (fn ((supcls, memtypes), sortctxts) => succeed
- (Class ((supcls, ("a", idfs ~~ (sortctxts ~~ memtypes))), [])))
+ (Class (supcls, ("a", idfs ~~ (sortctxts ~~ memtypes)))))
end
| _ =>
trns
@@ -611,7 +622,7 @@
|> fold_map (exprgen_tyvar_sort thy tabs) vars
||>> fold_map (fn (c, ty) => codegen_type thy tabs ty #-> (fn ty' => pair (c, ty'))) cos'
|-> (fn (sorts, cos'') => succeed (Datatype
- ((sorts, cos''), [])))
+ (sorts, cos'')))
end
| NONE =>
trns
@@ -799,7 +810,7 @@
trns
|> exprgen_type thy tabs ty
||>> exprgen_term thy tabs (subst_bound (Free (v, ty), t))
- |-> (fn (ty, e) => pair ((v, ty) `|-> e))
+ |-> (fn (ty, e) => pair (IVarE (v, ty) `|-> e))
| exprgen_term thy tabs (t as t1 $ t2) trns =
let
val (t', ts) = strip_comb t
@@ -842,7 +853,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 ((vs ~~ tys) `|--> e))
+ |-> (fn (tys, e) => pair (map2 (curry IVarE) vs tys `|--> e))
end
else if length ts > imax then
trns
@@ -863,7 +874,7 @@
(* function extractors *)
fun eqextr_defs thy ((deftab, _), _) (c, ty) =
- Option.mapPartial (get_first (fn (ty', thm) => if eq_typ thy (ty, ty')
+ Option.mapPartial (get_first (fn (ty', (thm, _)) => if eq_typ thy (ty, ty')
then SOME ([thm], ty')
else NONE
)) (Symtab.lookup deftab c);
@@ -871,28 +882,16 @@
(* parametrized generators, for instantiation in HOL *)
-fun appgen_let strip_abs thy tabs ((c, ty), [t2, t3]) trns =
+fun appgen_let strip_abs thy tabs ((c, ty), [t_val, t_cont]) trns =
let
- fun dest_let (l as Const (c', _) $ t $ u) =
- if c = c' then
- case strip_abs 1 u
- of ([p], u') => apfst (cons (p, t)) (dest_let u')
- | _ => ([], l)
- else ([], t)
- | dest_let t = ([], t);
- fun mk_let (l, r) trns =
- trns
- |> exprgen_term thy tabs l
- ||>> exprgen_term thy tabs r
- |-> (fn (l, r) => pair (r, l));
- val (lets, body) = dest_let (Const (c, ty) $ t2 $ t3)
+ val ([t_abs], t_body) = strip_abs 1 t_cont;
in
trns
- |> fold_map mk_let lets
- ||>> exprgen_term thy tabs body
- |-> (fn (lets, body) =>
- pair (Library.foldr (fn ((e, p), body) => ICase (e, [(p, body)])) (lets, body)))
- end
+ |> 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)])))
+ end;
fun appgen_split strip_abs thy tabs (c, [t2]) trns =
let
@@ -901,7 +900,7 @@
trns
|> exprgen_term thy tabs p
||>> exprgen_term thy tabs body
- |-> (fn (IVarE v, body) => pair (v `|-> body))
+ |-> (fn (e, body) => pair (e `|-> body))
end;
fun appgen_number_of mk_int_to_nat bin_to_int tyco_int tyco_nat thy tabs ((_,
@@ -915,6 +914,23 @@
|> exprgen_term thy tabs (mk_int_to_nat bin)
else error ("invalid type constructor for numeral: " ^ quote tyco);
+fun appgen_wfrec thy tabs ((c, ty), [_, tf, tx]) trns =
+ let
+ val ty_def = (op ---> o apfst tl o strip_type o Sign.the_const_type thy) c;
+ val ty' = (op ---> o apfst tl o strip_type) ty;
+ val idf = idf_of_const thy tabs (c, ty);
+ in
+ trns
+ |> gen_ensure_def [("wfrec", (K o succeed) Undef)] ("generating wfrec") idf
+ |> exprgen_type thy tabs ty'
+ ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
+ (ClassPackage.extract_classlookup thy (c, ty))
+ ||>> codegen_type thy tabs [ty_def]
+ ||>> exprgen_term thy tabs tf
+ ||>> exprgen_term thy tabs tx
+ |-> (fn ((((_, ls), [ty]), tf), tx) => pair (IConst ((idf, ty), ls) `$ tf `$ tx))
+ end;
+
fun eqextr_eq f fals thy tabs ("op =", ty) =
(case ty
of Type ("fun", [Type (dtco, _), _]) =>
@@ -974,24 +990,29 @@
let
fun extract_defs thy =
let
- fun dest tm =
+ fun dest thm =
let
- val (lhs, rhs) = Logic.dest_equals (prop_of tm);
+ val (lhs, rhs) = Logic.dest_equals (prop_of thm);
val (t, args) = strip_comb lhs;
val (c, ty) = dest_Const t
- in if forall is_Var args then SOME ((c, ty), tm) else NONE
+ in if forall is_Var args then SOME ((c, ty), thm) else NONE
end handle TERM _ => NONE;
fun prep_def def = (case Codegen.preprocess thy [def] of
[def'] => def' | _ => error "mk_tabs: bad preprocessor");
- fun add_def (name, _) =
+ fun add_def thyname (name, _) =
case (dest o prep_def o Thm.get_axiom thy) name
- of SOME ((c, ty), tm) =>
- Symtab.default (c, []) #> Symtab.map_entry c (cons (ty, tm))
+ of SOME ((c, ty), thm) =>
+ Symtab.default (c, [])
+ #> Symtab.map_entry c (cons (ty, (thm, thyname)))
| NONE => I
+ fun get_defs thy =
+ let
+ val thyname = Context.theory_name thy;
+ val defs = (snd o #axioms o Theory.rep_theory) thy;
+ in Symtab.fold (add_def thyname) defs end;
in
Symtab.empty
- |> fold (Symtab.fold add_def o snd o #axioms o Theory.rep_theory)
- (thy :: Theory.ancestors_of thy)
+ |> fold get_defs (thy :: Theory.ancestors_of thy)
end;
fun mk_insttab thy =
InstNameMangler.empty
@@ -1000,7 +1021,7 @@
(fn (tyco, thyname) => InstNameMangler.declare thy (thyname, (cls, tyco))) clsinsts)
(ClassPackage.get_classtab thy)
|-> (fn _ => I);
- fun add_monoeq thy (overltab1, overltab2) =
+ fun add_monoeq thy deftab (overltab1, overltab2) =
let
val c = "op =";
val ty = Sign.the_const_type thy c;
@@ -1013,8 +1034,8 @@
(overltab1
|> Symtab.update_new (c, (ty, tys)),
overltab2
- |> fold (fn ty' => ConstNameMangler.declare thy
- (idf_of_name thy nsp_overl c, (ty, ty')) #> snd) tys)
+ |> fold (fn ty' => ConstNameMangler.declare (thy, deftab)
+ (c, (ty, ty')) #> snd) tys)
end;
fun mk_overltabs thy deftab =
(Symtab.empty, ConstNameMangler.empty)
@@ -1026,11 +1047,11 @@
overltab1
|> Symtab.update_new (c, (Sign.the_const_type thy c, map fst tytab)),
overltab2
- |> fold (fn (ty, _) => ConstNameMangler.declare thy
- (idf_of_name thy nsp_overl c, (Sign.the_const_type thy c, ty)) #> snd) tytab))
+ |> fold (fn (ty, (_, thyname)) => ConstNameMangler.declare (thy, deftab)
+ (c, (Sign.the_const_type thy c, ty)) #> snd) tytab))
else I
) deftab
- |> add_monoeq thy;
+ |> add_monoeq thy deftab;
fun mk_dtcontab thy =
DatatypeconsNameMangler.empty
|> fold_map
--- a/src/Pure/Tools/codegen_serializer.ML Tue Feb 14 13:03:00 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Tue Feb 14 17:07:11 2006 +0100
@@ -92,7 +92,7 @@
brackify fxy (mk_app c es)
| mk (SOME ((i, k), pr)) es =
let
- val (es1, es2) = splitAt (k, es);
+ val (es1, es2) = Library.chop k es;
in
brackify fxy (pr fxy from_expr es1 :: map (from_expr BR) es2)
end;
@@ -209,7 +209,7 @@
--| $$ "`" >> (fn ["_"] => Name | s => error ("malformed antiquote: " ^ implode s)))
|| Scan.repeat1
(Scan.unless ($$ "`") (Scan.one Symbol.not_eof)) >> (CodegenThingol.Pretty o str o implode)
- )) (Symbol.explode s)
+ )) ((Symbol.explode o Symbol.strip_blanks) s)
of (p, []) => p
| (p, ss) => error ("Malformed definition: " ^ quote s ^ " - " ^ commas ss);
@@ -343,8 +343,9 @@
local
fun ml_from_defs (is_cons, needs_type)
- (from_prim, (_, tyco_syntax, const_syntax)) resolv defs =
+ (from_prim, (_, tyco_syntax, const_syntax)) resolver prefix defs =
let
+ val resolv = resolver prefix;
fun chunk_defs ps =
let
val (p_init, p_last) = split_last ps
@@ -443,10 +444,12 @@
]
else
str v
- | ml_from_expr fxy (IAbs ((v, _), e)) =
- brackify fxy [
- str ("fn " ^ v ^ " =>"),
- ml_from_expr NOBR e
+ | ml_from_expr fxy (IAbs (e1, e2)) =
+ brackify BR [
+ str "fn",
+ ml_from_expr NOBR e1,
+ str "=>",
+ ml_from_expr NOBR e2
]
| ml_from_expr fxy (e as ICase (_, [_])) =
let
@@ -485,13 +488,24 @@
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)]
+ [(str o resolv) f, Pretty.enum "," "(" ")" (map (ml_from_expr BR) es)]
else
(str o resolv) f :: map (ml_from_expr BR) es
- and ml_from_app fxy (((c, _), lss), es) =
+ and ml_from_app fxy (((c, ty), lss), es) =
case map (ml_from_sortlookup BR) lss
of [] =>
- from_app ml_mk_app ml_from_expr const_syntax fxy (c, es)
+ let
+ val p = from_app ml_mk_app ml_from_expr const_syntax fxy (c, es)
+ in if needs_type ty
+ then
+ Pretty.enclose "(" ")" [
+ p,
+ str ":",
+ ml_from_type NOBR ty
+ ]
+ else
+ p
+ end
| lss =>
brackify fxy (
(str o resolv) c
@@ -551,7 +565,7 @@
:: separate (Pretty.block [str " *", Pretty.brk 1])
(map (ml_from_type NOBR) tys)
)
- fun mk_datatype definer (t, ((vs, cs), _)) =
+ fun mk_datatype definer (t, (vs, cs)) =
(Pretty.block o Pretty.breaks) (
str definer
:: ml_from_tycoexpr NOBR (t, map IVarT vs)
@@ -583,7 +597,7 @@
str ";"
]
) |> SOME
- | ml_from_def (name, Class ((supclasses, (v, membrs)), _)) =
+ | ml_from_def (name, Class (supclasses, (v, membrs))) =
let
val pv = str ("'" ^ v);
fun from_supclass class =
@@ -702,7 +716,7 @@
| _ => if has_nsp s nsp_dtcon
then case get_def module s
of Datatypecons dtname => case get_def module dtname
- of Datatype ((_, cs), _) =>
+ of Datatype (_, cs) =>
let val l = AList.lookup (op =) cs s |> the |> length
in if l >= 2 then l else 0 end
else 0;
@@ -735,8 +749,14 @@
local
fun hs_from_defs with_typs (from_prim, (class_syntax, tyco_syntax, const_syntax))
- resolv defs =
+ resolver prefix defs =
let
+ fun resolv s = if NameSpace.is_qualified s
+ then resolver "" s
+ else if nth_string s 0 = "~"
+ then enclose "(" ")" ("negate " ^ unprefix "~" s)
+ else s;
+ val resolv_here = (resolver o NameSpace.base) prefix;
fun hs_from_sctxt vs =
let
fun from_class cls =
@@ -793,13 +813,13 @@
str v
| hs_from_expr fxy (e as IAbs _) =
let
- val (vs, body) = unfold_abs e
+ val (es, e) = unfold_abs e
in
- brackify fxy (
+ brackify BR (
str "\\"
- :: map (str o fst) vs @ [
+ :: map (hs_from_expr BR) es @ [
str "->",
- hs_from_expr NOBR body
+ hs_from_expr NOBR e
])
end
| hs_from_expr fxy (e as ICase (_, [_])) =
@@ -841,7 +861,7 @@
let
fun from_eq name (args, rhs) =
Pretty.block [
- (str o resolv) name,
+ (str o resolv_here) name,
Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, hs_from_expr BR p]) args),
Pretty.brk 1,
str ("="),
@@ -852,14 +872,14 @@
fun hs_from_def (name, Undef) =
error ("empty statement during serialization: " ^ quote name)
| hs_from_def (name, Prim prim) =
- from_prim resolv (name, prim)
+ from_prim resolv_here (name, prim)
| hs_from_def (name, Fun (eqs, (sctxt, ty))) =
let
val body = hs_from_funeqs (name, eqs);
in if with_typs then
Pretty.chunks [
Pretty.block [
- (str o suffix " ::" o resolv) name,
+ (str o suffix " ::" o resolv_here) name,
Pretty.brk 1,
hs_from_sctxt_type (sctxt, ty)
],
@@ -869,22 +889,22 @@
| hs_from_def (name, Typesyn (vs, ty)) =
Pretty.block [
str "type ",
- hs_from_sctxt_tycoexpr (vs, (name, map IVarT vs)),
+ hs_from_sctxt_tycoexpr (vs, (resolv_here name, map IVarT vs)),
str " =",
Pretty.brk 1,
hs_from_sctxt_type ([], ty)
] |> SOME
- | hs_from_def (name, Datatype ((vs, constrs), _)) =
+ | hs_from_def (name, Datatype (vs, constrs)) =
let
fun mk_cons (co, tys) =
(Pretty.block o Pretty.breaks) (
- (str o resolv) co
+ (str o resolv_here) co
:: map (hs_from_type NOBR) tys
)
in
Pretty.block ((
str "data "
- :: hs_from_sctxt_type (vs, IType (name, map IVarT vs))
+ :: hs_from_sctxt_type (vs, IType (resolv_here name, map IVarT vs))
:: str " ="
:: Pretty.brk 1
:: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs)
@@ -895,11 +915,11 @@
end |> SOME
| hs_from_def (_, Datatypecons _) =
NONE
- | hs_from_def (name, Class ((supclasss, (v, membrs)), _)) =
+ | hs_from_def (name, Class (supclasss, (v, membrs))) =
let
fun mk_member (m, (sctxt, ty)) =
Pretty.block [
- str (resolv m ^ " ::"),
+ str (resolv_here m ^ " ::"),
Pretty.brk 1,
hs_from_sctxt_type (sctxt, ty)
]
@@ -907,7 +927,7 @@
Pretty.block [
str "class ",
hs_from_sctxt (map (fn class => (v, [class])) supclasss),
- str (resolv name ^ " " ^ v),
+ str (resolv_here name ^ " " ^ v),
str " where",
Pretty.fbrk,
Pretty.chunks (map mk_member membrs)
@@ -943,12 +963,12 @@
"Bool", "fst", "snd", "Integer", "True", "False", "negate"
];
fun hs_from_module imps ((_, name), ps) =
- (Pretty.block o Pretty.fbreaks) (
- str ("module " ^ name ^ " where")
- :: map (str o prefix "import qualified ") imps @ [
- str "",
- Pretty.chunks (separate (str "") ps)
- ]);
+ (Pretty.chunks) (
+ str ("module " ^ name ^ " where")
+ :: map (str o prefix "import qualified ") imps @ (
+ str ""
+ :: separate (str "") ps
+ ));
fun postproc (shallow, n) =
let
fun ch_first f = String.implode o nth_map 0 f o String.explode;
--- a/src/Pure/Tools/codegen_thingol.ML Tue Feb 14 13:03:00 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Tue Feb 14 17:07:11 2006 +0100
@@ -18,18 +18,18 @@
IConst of (string * itype) * classlookup list list
| IVarE of vname * itype
| IApp of iexpr * iexpr
- | IAbs of (vname * itype) * iexpr
+ | IAbs of iexpr * iexpr
| 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;
+ val mk_abss: iexpr 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 -> (vname * itype) list * iexpr;
+ val unfold_abs: iexpr -> iexpr list * iexpr;
val unfold_let: iexpr -> (iexpr * iexpr) list * iexpr;
val unfold_const_app: iexpr ->
(((string * itype) * classlookup list list) * iexpr list) option;
@@ -41,8 +41,8 @@
val `--> : itype list * itype -> itype;
val `$ : iexpr * iexpr -> iexpr;
val `$$ : iexpr * iexpr list -> iexpr;
- val `|-> : (vname * itype) * iexpr -> iexpr;
- val `|--> : (vname * itype) list * iexpr -> iexpr;
+ val `|-> : iexpr * iexpr -> iexpr;
+ val `|--> : iexpr list * iexpr -> iexpr;
type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype);
datatype prim =
@@ -52,12 +52,10 @@
Undef
| Prim of (string * prim list) list
| Fun of funn
- | Typesyn of (vname * string list) list * itype
- | Datatype of ((vname * string list) list * (string * itype list) list)
- * string list
+ | Typesyn of (vname * sort) list * itype
+ | Datatype of (vname * sort) list * (string * itype list) list
| Datatypecons of string
- | Class of (class list * (vname * (string * (ClassPackage.sortcontext * itype)) list))
- * string list
+ | Class of class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)
| Classmember of class
| Classinst of ((class * (string * (vname * sort) list))
* (class * classlookup list list) list)
@@ -91,7 +89,7 @@
val soft_exc: bool ref;
val serialize:
- ((string -> string) -> (string * def) list -> 'a option)
+ ((string -> string -> string) -> string -> (string * def) list -> 'a option)
-> (string list -> (string * string) * 'a list -> 'a option)
-> (string -> string option)
-> (string * string -> string)
@@ -161,7 +159,7 @@
IConst of (string * itype) * classlookup list list
| IVarE of vname * itype
| IApp of iexpr * iexpr
- | IAbs of (vname * itype) * iexpr
+ | IAbs of iexpr * iexpr
| ICase of iexpr * (iexpr * iexpr) list;
(*
@@ -213,8 +211,8 @@
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 (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 ",
@@ -334,40 +332,6 @@
| instant y = map_itype instant y;
in map_itype instant end;
-
-(* simple diagnosis *)
-
-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)
- ];
-
-
-(* language auxiliary *)
-
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
@@ -378,7 +342,7 @@
^ ", " ^ (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 ((_, ty1), e2)) = ty1 `-> itype_of_iexpr e2
+ | 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
@@ -391,7 +355,8 @@
fun type_vnames ty =
let
fun extr (IVarT (v, _)) =
- insert (op =) v
+ insert (op =) v
+ | extr _ = I;
in fold_atype extr ty end;
fun expr_names e =
@@ -423,12 +388,10 @@
Undef
| Prim of (string * prim list) list
| Fun of funn
- | Typesyn of (vname * string list) list * itype
- | Datatype of ((vname * string list) list * (string * itype list) list)
- * string list
+ | Typesyn of (vname * sort) list * itype
+ | Datatype of (vname * sort) list * (string * itype list) list
| Datatypecons of string
- | Class of (class list * (vname * (string * (ClassPackage.sortcontext * itype)) list))
- * string list
+ | Class of class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)
| Classmember of class
| Classinst of ((class * (string * (vname * sort) list))
* (class * classlookup list list) list)
@@ -468,28 +431,24 @@
Pretty.str " |=> ",
pretty_itype ty
]
- | pretty_def (Datatype ((vs, cs), insts)) =
+ | pretty_def (Datatype (vs, cs)) =
Pretty.block [
Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
Pretty.str " |=> ",
Pretty.enum " |" "" ""
(map (fn (c, tys) => (Pretty.block o Pretty.breaks)
- (Pretty.str c :: map pretty_itype tys)) cs),
- Pretty.str ", instances ",
- Pretty.enum "," "[" "]" (map Pretty.str insts)
+ (Pretty.str c :: map pretty_itype tys)) cs)
]
| pretty_def (Datatypecons dtname) =
Pretty.str ("cons " ^ dtname)
- | pretty_def (Class ((supcls, (v, mems)), insts)) =
+ | pretty_def (Class (supcls, (v, mems))) =
Pretty.block [
Pretty.str ("class var " ^ v ^ "extending "),
Pretty.enum "," "[" "]" (map Pretty.str supcls),
Pretty.str " with ",
Pretty.enum "," "[" "]"
(map (fn (m, (_, ty)) => Pretty.block
- [Pretty.str (m ^ "::"), pretty_itype ty]) mems),
- Pretty.str " instances ",
- Pretty.enum "," "[" "]" (map Pretty.str insts)
+ [Pretty.str (m ^ "::"), pretty_itype ty]) mems)
]
| pretty_def (Classmember clsname) =
Pretty.block [
@@ -609,7 +568,9 @@
val add_edge =
if null r1 andalso null r2
then Graph.add_edge
- else Graph.add_edge_acyclic
+ else fn edge => (Graph.add_edge_acyclic edge
+ handle Graph.CYCLES _ => error ("adding dependency "
+ ^ quote name1 ^ " -> " ^ quote name2 ^ " would result in module dependency cycle"))
fun add [] node =
node
|> add_edge (s1, s2)
@@ -776,24 +737,17 @@
Fun (check_funeqs eqs, d)
| check_prep_def modl (d as Typesyn _) =
d
- | check_prep_def modl (d as Datatype (_, insts)) =
- if null insts
- then d
- else error "attempted to add datatype with bare instances"
+ | check_prep_def modl (d as Datatype _) =
+ d
| check_prep_def modl (Datatypecons dtco) =
error "attempted to add bare datatype constructor"
- | check_prep_def modl (d as Class ((_, (v, membrs)), insts)) =
- if null insts
- then
- if member (op =) (map fst (Library.flat (map (fst o snd) membrs))) v
- then error "incorrectly abstracted class type variable"
- else d
- else error "attempted to add class with bare instances"
+ | check_prep_def modl (d as Class _) =
+ d
| check_prep_def modl (Classmember _) =
error "attempted to add bare class member"
| check_prep_def modl (Classinst ((d as ((class, (tyco, arity)), _), memdefs))) =
let
- val Class ((_, (v, membrs)), _) = get_def modl class;
+ val Class (_, (v, membrs)) = get_def modl class;
val _ = if length memdefs > length memdefs
then error "too many member definitions given"
else ();
@@ -808,7 +762,7 @@
else error ("inconsistent type for member definition " ^ quote m)
in Classinst (d, map mk_memdef membrs) end;
-fun postprocess_def (name, Datatype ((_, constrs), _)) =
+fun postprocess_def (name, Datatype (_, constrs)) =
(check_samemodule (name :: map fst constrs);
fold (fn (co, _) =>
ensure_def (co, Datatypecons name)
@@ -816,7 +770,7 @@
#> add_dep (name, co)
) constrs
)
- | postprocess_def (name, Class ((_, (_, membrs)), _)) =
+ | postprocess_def (name, Class (_, (_, membrs))) =
(check_samemodule (name :: map fst membrs);
fold (fn (m, _) =>
ensure_def (m, Classmember name)
@@ -824,10 +778,6 @@
#> add_dep (name, m)
) membrs
)
- | postprocess_def (name, Classinst (((class, (tyco, _)), _), _)) =
- map_def class (fn Datatype (d, insts) => Datatype (d, name::insts)
- | d => d)
- #> map_def class (fn Class (d, insts) => Class (d, name::insts))
| postprocess_def _ =
I;
@@ -942,9 +892,9 @@
|> curry Library.drop (length es)
|> curry Library.take add_n
val add_vars =
- Term.invent_names (fold expr_names es []) "x" add_n ~~ tys;
+ map2 (curry IVarE) (Term.invent_names (fold expr_names es []) "x" add_n) tys;
in
- add_vars `|--> IConst ((f, ty), ls) `$$ es `$$ map IVarE add_vars
+ add_vars `|--> IConst ((f, ty), ls) `$$ es `$$ add_vars
end
| NONE => map_iexpr eta e;
in (map_defs o map_def_fun o map_def_fun_expr) eta end;
@@ -956,9 +906,13 @@
orelse null (type_vnames ty [])
then funn
else
- let
- val add_var = (hd (Term.invent_names (expr_names e []) "x" 1), ty1)
- in (([([IVarE add_var], add_var `|-> e)], cty)) end
+ (case unfold_abs e
+ of ([], e) =>
+ let
+ val add_var = IVarE (hd (Term.invent_names (expr_names e []) "x" 1), ty1)
+ in (([([add_var], add_var `|-> e)], cty)) end
+ | eq =>
+ (([eq], cty)))
| eta funn = funn;
in (map_defs o map_def_fun) eta end;
@@ -1075,6 +1029,7 @@
fun serialize seri_defs seri_module validate postprocess nsp_conn name_root module =
let
val resolver = mk_deresolver module nsp_conn postprocess validate;
+ fun sresolver s = (resolver o NameSpace.unpack) s
fun mk_name prfx name =
let
val name_qual = NameSpace.pack (prfx @ [name])
@@ -1086,7 +1041,7 @@
seri_module (map (resolver []) (imports_of module (prfx @ [name])))
(mk_name prfx name, mk_contents (prfx @ [name]) modl)
| seri prfx ds =
- seri_defs (resolver prfx)
+ seri_defs sresolver (NameSpace.pack prfx)
(map (fn (name, Def def) => (fst (mk_name prfx name), def)) ds)
in
seri_module (map (resolver []) (Graph.strong_conn module |> List.concat |> rev))