# HG changeset patch # User haftmann # Date 1139933231 -3600 # Node ID 62c5f7591a433734d1383bb3de3614832c94522e # Parent 3be721728a6cfb428ab65ebcd90ea2996176b829 improved handling of iml abstractions diff -r 3be721728a6c -r 62c5f7591a43 src/Pure/Tools/class_package.ML --- 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 = diff -r 3be721728a6c -r 62c5f7591a43 src/Pure/Tools/codegen_package.ML --- 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 diff -r 3be721728a6c -r 62c5f7591a43 src/Pure/Tools/codegen_serializer.ML --- 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; diff -r 3be721728a6c -r 62c5f7591a43 src/Pure/Tools/codegen_thingol.ML --- 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))