# HG changeset patch # User haftmann # Date 1141051897 -3600 # Node ID 1457d810b408a97e9772e8a914b1949a1f0a2773 # Parent 1c31769f9796f4381db4a5411234c2dfeed0131b class package and codegen refinements diff -r 1c31769f9796 -r 1457d810b408 src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Mon Feb 27 15:49:56 2006 +0100 +++ b/src/HOL/Datatype.thy Mon Feb 27 15:51:37 2006 +0100 @@ -286,6 +286,33 @@ ml (target_atom "(__,/ __)") haskell (target_atom "(__,/ __)") +code_generate Unity + +code_syntax_tyco + unit + ml (target_atom "unit") + haskell (target_atom "()") + +code_syntax_const + Unity + ml (target_atom "()") + haskell (target_atom "()") + +code_generate None Some + +code_syntax_tyco + option + ml ("_ option") + haskell ("Maybe _") + +code_syntax_const + None + ml (target_atom "NONE") + haskell (target_atom "Nothing") + Some + ml (target_atom "SOME") + haskell (target_atom "Just") + code_syntax_const "1 :: nat" ml ("{*Suc 0*}") diff -r 1c31769f9796 -r 1457d810b408 src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Mon Feb 27 15:49:56 2006 +0100 +++ b/src/Pure/Tools/class_package.ML Mon Feb 27 15:51:37 2006 +0100 @@ -7,26 +7,22 @@ signature CLASS_PACKAGE = sig - val add_class: bstring -> class list -> Element.context list -> theory + val class: bstring -> class list -> Element.context list -> theory -> ProofContext.context * theory - val add_class_i: bstring -> class list -> Element.context_i list -> theory + val class_i: bstring -> class list -> Element.context_i list -> theory -> ProofContext.context * theory - val add_instance_arity: (xstring * string list) * string + val instance_arity: (xstring * string list) * string -> bstring * Attrib.src list -> ((bstring * Attrib.src list) * string) list -> theory -> Proof.state - val add_instance_arity_i: (string * sort list) * sort + val instance_arity_i: (string * sort list) * sort -> bstring * attribute list -> ((bstring * attribute list) * term) list -> theory -> Proof.state - val prove_instance_arity: tactic -> (xstring * string list) * string - -> bstring * Attrib.src list -> ((bstring * Attrib.src list) * string) list - -> theory -> theory - val prove_instance_arity_i: tactic -> (string * sort list) * sort + val prove_instance_arity: tactic -> (string * sort list) * sort -> bstring * attribute list -> ((bstring * attribute list) * term) list -> theory -> theory - val add_instance_sort: string * string -> theory -> Proof.state - val add_instance_sort_i: class * sort -> theory -> Proof.state - val prove_instance_sort: tactic -> string * string -> theory -> theory - val prove_instance_sort_i: tactic -> class * sort -> theory -> theory + val instance_sort: string * string -> theory -> Proof.state + val instance_sort_i: class * sort -> theory -> Proof.state + val prove_instance_sort: tactic -> class * sort -> theory -> theory val intern_class: theory -> xstring -> class val intern_sort: theory -> sort -> sort @@ -343,7 +339,7 @@ |-> (fn _ => I) end; -fun gen_add_class add_locale prep_class bname raw_supclasses raw_elems thy = +fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy = let val supclasses = map (prep_class thy) raw_supclasses; val supsort = @@ -423,8 +419,8 @@ in -val add_class = gen_add_class (add_locale true) intern_class; -val add_class_i = gen_add_class (add_locale_i true) certify_class; +val class = gen_class (add_locale true) intern_class; +val class_i = gen_class (add_locale_i true) certify_class; end; (* local *) @@ -538,19 +534,18 @@ |-> (fn cs => do_proof (after_qed cs) arity) end; -fun instance_arity do_proof = gen_instance_arity AxClass.read_arity Attrib.attribute add_defs_overloaded +fun instance_arity' do_proof = gen_instance_arity AxClass.read_arity Attrib.attribute add_defs_overloaded (fn thy => fn t => (snd o read_axm thy) ("", t)) do_proof; -fun instance_arity_i do_proof = gen_instance_arity AxClass.cert_arity (K I) add_defs_overloaded_i +fun instance_arity_i' do_proof = gen_instance_arity AxClass.cert_arity (K I) add_defs_overloaded_i (K I) do_proof; val setup_proof = AxClass.instance_arity_i; fun tactic_proof tac after_qed arity = AxClass.add_inst_arity_i arity tac #> after_qed; in -val add_instance_arity = instance_arity setup_proof; -val add_instance_arity_i = instance_arity_i setup_proof; -val prove_instance_arity = instance_arity o tactic_proof; -val prove_instance_arity_i = instance_arity_i o tactic_proof; +val instance_arity = instance_arity' setup_proof; +val instance_arity_i = instance_arity_i' setup_proof; +val prove_instance_arity = instance_arity_i' o tactic_proof; end; (* local *) @@ -585,7 +580,7 @@ |> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE) |-> (fn _ => I); -fun gen_add_instance_sort prep_class prep_sort do_proof (raw_class, raw_sort) theory = +fun gen_instance_sort prep_class prep_sort do_proof (raw_class, raw_sort) theory = let val class = prep_class theory raw_class; val sort = prep_sort theory raw_sort; @@ -605,18 +600,16 @@ |> do_proof after_qed (loc_name, loc_expr) end; -fun instance_sort do_proof = gen_add_instance_sort intern_class read_sort do_proof; -fun instance_sort_i do_proof = gen_add_instance_sort certify_class certify_sort do_proof; - +fun instance_sort' do_proof = gen_instance_sort intern_class read_sort do_proof; +fun instance_sort_i' do_proof = gen_instance_sort certify_class certify_sort do_proof; val setup_proof = add_interpretation_in; val tactic_proof = prove_interpretation_in; in -val add_instance_sort = instance_sort setup_proof; -val add_instance_sort_i = instance_sort_i setup_proof; -val prove_instance_sort = instance_sort o tactic_proof; -val prove_instance_sort_i = instance_sort_i o tactic_proof; +val instance_sort = instance_sort' setup_proof; +val instance_sort_i = instance_sort_i' setup_proof; +val prove_instance_sort = instance_sort_i' o tactic_proof; end; (* local *) @@ -727,10 +720,10 @@ if (is_some o lookup_class_data thy o Sign.intern_class thy) class andalso (is_some o lookup_class_data thy o Sign.intern_class thy) class' then - add_instance_sort (class, sort) thy + instance_sort (class, sort) thy else AxClass.instance_subclass (class, sort) thy - | _ => add_instance_sort (class, sort) thy; + | _ => instance_sort (class, sort) thy; val parse_inst = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 P.sort --| P.$$$ ")")) [] -- P.xname --| P.$$$ "::" -- P.sort) @@ -749,14 +742,14 @@ -- Scan.optional (Scan.repeat1 (P.name --| P.$$$ "+")) [] -- Scan.optional (P.!!! (Scan.repeat1 P.context_element)) [] >> (Toplevel.theory_context - o (fn ((bname, supclasses), elems) => add_class bname supclasses elems))); + o (fn ((bname, supclasses), elems) => class bname supclasses elems))); val instanceP = OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal (( P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! P.xname) >> wrap_add_instance_subclass || P.opt_thm_name ":" -- (parse_inst -- Scan.repeat (P.opt_thm_name ":" -- P.prop)) >> (fn (("", []), (((tyco, asorts), sort), [])) => AxClass.instance_arity I (tyco, asorts, sort) - | (natts, (inst, defs)) => add_instance_arity inst natts defs) + | (natts, (inst, defs)) => instance_arity inst natts defs) ) >> (Toplevel.print oo Toplevel.theory_to_proof)); val _ = OuterSyntax.add_parsers [classP, instanceP]; diff -r 1c31769f9796 -r 1457d810b408 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Mon Feb 27 15:49:56 2006 +0100 +++ b/src/Pure/Tools/codegen_package.ML Mon Feb 27 15:51:37 2006 +0100 @@ -38,10 +38,11 @@ -> theory -> theory; val set_int_tyco: string -> theory -> theory; - val codegen_incr: term -> theory -> (CodegenThingol.iexpr * (string * CodegenThingol.def) list) * theory; + val codegen_term: term -> theory -> CodegenThingol.iexpr * theory; val is_dtcon: string -> bool; - val consts_of_idfs: theory -> string list -> (string * (string * typ)) list - + val consts_of_idfs: theory -> string list -> (string * typ) list; + val idfs_of_consts: theory -> (string * typ) list -> string list; + val get_root_module: theory -> CodegenThingol.module; val get_ml_fun_datatype: theory -> (string -> string) -> ((string * CodegenThingol.funn) list -> Pretty.T) * ((string * CodegenThingol.datatyp) list -> Pretty.T); @@ -188,7 +189,7 @@ |> curry (op ^ o swap) ((implode oo replicate) i "'") end; fun is_valid _ _ = true; - fun maybe_unique thy (c, ty) = + fun maybe_unique thy (c, ty) = if is_overloaded thy c then NONE else (SOME o idf_of_name thy nsp_const) c; @@ -475,7 +476,7 @@ gens |> map_gens (fn (appconst, eqextrs) => (appconst, eqextrs - |> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name) + |> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name) (name, (eqx, stamp ())))), target_data, logic_data)); @@ -660,7 +661,7 @@ | exprgen_type thy tabs (TFree v_s) trns = trns |> exprgen_tyvar_sort thy tabs v_s - |-> (fn v_s => pair (IVarT v_s)) + |-> (fn (v, sort) => pair (IVarT v)) | exprgen_type thy tabs (Type ("fun", [t1, t2])) trns = trns |> exprgen_type thy tabs t1 @@ -907,14 +908,15 @@ end; fun appgen_split strip_abs thy tabs (c, [t2]) trns = - let - val ([p], body) = strip_abs 1 (Const c $ t2) - in - trns - |> exprgen_term thy tabs p - ||>> exprgen_term thy tabs body - |-> (fn (e, body) => pair (e `|-> body)) - end; + case strip_abs 1 (Const c $ t2) + of ([p], body) => + trns + |> exprgen_term thy tabs p + ||>> exprgen_term thy tabs body + |-> (fn (e, body) => pair (e `|-> body)) + | _ => + trns + |> appgen_default thy tabs (c, [t2]); fun appgen_number_of mk_int_to_nat bin_to_int tyco_int tyco_nat thy tabs ((_, Type (_, [_, ty as Type (tyco, [])])), [bin]) trns = @@ -1074,7 +1076,7 @@ let val c = "op ="; val ty = Sign.the_const_type thy c; - fun inst dtco = + fun inst dtco = map_atyps (fn _ => Type (dtco, (map (fn (v, sort) => TVar ((v, 0), sort)) o fst o the o get_datatype thy) dtco)) ty val dtcos = fold (insert (op =) o snd) (get_all_datatype_cons thy) []; @@ -1096,7 +1098,7 @@ ) (get_all_datatype_cons thy) []) |-> (fn _ => I); fun mk_clsmemtab thy = - Symtab.empty + Symtab.empty |> Symtab.fold (fn (class, (clsmems, _)) => fold (fn clsmem => Symtab.update (clsmem, class)) clsmems) @@ -1159,25 +1161,24 @@ fold ensure (get_datatype_case_consts thy) thy end; -fun codegen_incr t thy = +fun codegen_term t thy = thy - |> `(#modl o CodegenData.get) - ||>> expand_module NONE exprsgen_term [t] - ||>> `(#modl o CodegenData.get) - |-> (fn ((modl_old, [t]), modl_new) => pair (t, CodegenThingol.diff_module (modl_new, modl_old))); + |> expand_module NONE exprsgen_term [t] + |-> (fn [t] => pair t); val is_dtcon = has_nsp nsp_dtcon; fun consts_of_idfs thy = - let - val tabs = mk_tabs thy; - in - map (fn idf => (idf, (the o recconst_of_idf thy tabs) idf)) - end; + map (the o recconst_of_idf thy (mk_tabs thy)); + +fun idfs_of_consts thy = + map (idf_of_const thy (mk_tabs thy)); + +val get_root_module = (#modl o CodegenData.get); fun get_ml_fun_datatype thy resolv = let - val target_data = + val target_data = ((fn data => (the o Symtab.lookup data) "ml") o #target_data o CodegenData.get) thy; in CodegenSerializer.ml_fun_datatype (nsp_dtcon, nsp_class, K false) @@ -1342,9 +1343,9 @@ (** toplevel interface **) local - + fun generate_code (SOME raw_consts) thy = - let + let val consts = map (read_const thy) raw_consts; in thy diff -r 1c31769f9796 -r 1457d810b408 src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Mon Feb 27 15:49:56 2006 +0100 +++ b/src/Pure/Tools/codegen_serializer.ML Mon Feb 27 15:51:37 2006 +0100 @@ -26,6 +26,7 @@ ml: string * (string * string * (string -> bool) -> serializer), haskell: string * (string list -> serializer) }; + val mk_flat_ml_resolver: string list -> string -> string; val ml_fun_datatype: string * string * (string -> bool) -> ((string -> CodegenThingol.itype pretty_syntax option) * (string -> CodegenThingol.iexpr pretty_syntax option)) @@ -264,6 +265,23 @@ |> K () end; +fun replace_invalid s = + let + fun replace_invalid c = + if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'" + andalso not (NameSpace.separator = c) + then c + else "_"; + fun contract "_" (acc as "_" :: _) = acc + | contract c acc = c :: acc; + fun contract_underscores s = + implode (fold_rev contract (explode s) []); + in + s + |> translate_string replace_invalid + |> contract_underscores + end; + fun abstract_validator keywords name = let fun replace_invalid c = @@ -351,6 +369,23 @@ local +val reserved_ml = ThmDatabase.ml_reserved @ [ + "bool", "int", "list", "unit", "option", "true", "false", "not", "None", "Some", "o" +]; + +structure NameMangler = NameManglerFun ( + type ctxt = string list; + type src = string; + val ord = string_ord; + fun mk reserved_ml (name, 0) = + (replace_invalid o NameSpace.base) name + | mk reserved_ml (name, i) = + (replace_invalid o NameSpace.base) name ^ replicate_string i "'"; + fun is_valid reserved_ml = not o member (op =) reserved_ml; + fun maybe_unique _ _ = NONE; + fun re_mangle _ dst = error ("no such definition name: " ^ quote dst); +); + fun ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv = let val ml_from_label = @@ -415,7 +450,7 @@ ml_from_type (INFX (1, R)) t2 ] end - | ml_from_type fxy (IVarT (v, _)) = + | ml_from_type fxy (IVarT v) = str ("'" ^ v); fun ml_from_expr fxy (e as IApp (e1, e2)) = (case unfold_const_app e @@ -578,7 +613,7 @@ fun mk_datatype definer (t, (vs, cs)) = (Pretty.block o Pretty.breaks) ( str definer - :: ml_from_tycoexpr NOBR (t, map IVarT vs) + :: ml_from_tycoexpr NOBR (t, map (IVarT o fst) vs) :: str "=" :: separate (str "|") (map mk_cons cs) ) @@ -661,7 +696,7 @@ error "can't serialize sort constrained type declaration to ML") vs; Pretty.block [ str "type ", - ml_from_tycoexpr NOBR (name, map IVarT vs), + ml_from_tycoexpr NOBR (name, map (IVarT o fst) vs), str " =", Pretty.brk 1, ml_from_type NOBR ty, @@ -737,9 +772,6 @@ fun ml_from_thingol target (nsp_dtcon, nsp_class, is_int_tyco) nspgrp = let - val reserved_ml = ThmDatabase.ml_reserved @ [ - "bool", "int", "list", "true", "false", "not", "o" - ]; fun ml_from_module _ ((_, name), ps) = Pretty.chunks ([ str ("structure " ^ name ^ " = "), @@ -786,6 +818,14 @@ (preprocess const_syntax) (class_syntax, tyco_syntax, const_syntax)) end; +fun mk_flat_ml_resolver names = + let + val mangler = + NameMangler.empty + |> fold_map (NameMangler.declare reserved_ml) names + |-> (fn _ => I) + in NameMangler.get reserved_ml mangler end; + fun ml_fun_datatype (nsp_dtcon, nsp_class, is_int_tyco) = ml_fun_datatyp (ml_annotators (nsp_dtcon, nsp_class, is_int_tyco)); @@ -838,7 +878,7 @@ str "->", hs_from_type (INFX (1, R)) t2 ] - | hs_from_type fxy (IVarT (v, _)) = + | hs_from_type fxy (IVarT v) = str v; fun hs_from_sctxt_tycoexpr (sctxt, tycoexpr) = Pretty.block [hs_from_sctxt sctxt, hs_from_tycoexpr NOBR tycoexpr] @@ -934,7 +974,7 @@ | hs_from_def (name, Typesyn (vs, ty)) = Pretty.block [ str "type ", - hs_from_sctxt_tycoexpr (vs, (resolv_here name, map IVarT vs)), + hs_from_sctxt_tycoexpr (vs, (resolv_here name, map (IVarT o fst) vs)), str " =", Pretty.brk 1, hs_from_sctxt_type ([], ty) @@ -949,7 +989,7 @@ in Pretty.block (( str "data " - :: hs_from_sctxt_type (vs, IType (resolv_here name, map IVarT vs)) + :: hs_from_sctxt_type (vs, IType (resolv_here name, map (IVarT o fst) vs)) :: str " =" :: Pretty.brk 1 :: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs) @@ -983,9 +1023,9 @@ | hs_from_def (_, Classinst (((clsname, (tyco, arity)), _), memdefs)) = Pretty.block [ str "instance ", - hs_from_sctxt_tycoexpr (arity, (clsname, map (IVarT o rpair [] o fst) arity)), + hs_from_sctxt_tycoexpr (arity, (clsname, map (IVarT o fst) arity)), str " ", - hs_from_sctxt_tycoexpr (arity, (tyco, map (IVarT o rpair [] o fst) arity)), + hs_from_sctxt_tycoexpr (arity, (tyco, map (IVarT o fst) arity)), str " where", Pretty.fbrk, Pretty.chunks (map (fn (m, (_, (eqs, _))) => hs_from_funeqs (m, eqs)) memdefs) @@ -1005,7 +1045,7 @@ "import", "default", "forall", "let", "in", "class", "qualified", "data", "newtype", "instance", "if", "then", "else", "type", "as", "do", "module" ] @ [ - "Bool", "Integer", "True", "False", "negate" + "Bool", "Integer", "Maybe", "True", "False", "Nothing", "Just", "negate" ]; fun hs_from_module imps ((_, name), ps) = (Pretty.chunks) ( diff -r 1c31769f9796 -r 1457d810b408 src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Mon Feb 27 15:49:56 2006 +0100 +++ b/src/Pure/Tools/codegen_thingol.ML Mon Feb 27 15:51:37 2006 +0100 @@ -13,7 +13,8 @@ datatype itype = IType of string * itype list | IFun of itype * itype - | IVarT of vname * sort; + | IVarT of vname; + type ityp = ClassPackage.sortcontext * itype; datatype iexpr = IConst of (string * itype) * classlookup list list | IVarE of vname * itype @@ -49,8 +50,8 @@ val `|-> : iexpr * iexpr -> iexpr; val `|--> : iexpr list * iexpr -> iexpr; - type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype); - type datatyp = (vname * sort) list * (string * itype list) list; + type funn = (iexpr list * iexpr) list * ityp; + type datatyp = ClassPackage.sortcontext * (string * itype list) list; datatype prim = Pretty of Pretty.T | Name; @@ -61,7 +62,7 @@ | Typesyn of (vname * sort) list * itype | Datatype of datatyp | Datatypecons of string - | Class of class list * (vname * (string * (ClassPackage.sortcontext * itype)) list) + | Class of class list * (vname * (string * ityp) list) | Classmember of class | Classinst of ((class * (string * (vname * sort) list)) * (class * (string * classlookup list list)) list) @@ -159,7 +160,8 @@ datatype itype = IType of string * itype list | IFun of itype * itype - | IVarT of vname * sort; + | IVarT of vname; +type ityp = ClassPackage.sortcontext * itype; datatype iexpr = IConst of (string * itype) * classlookup list list @@ -204,12 +206,16 @@ val op `$$ = mk_apps; val op `|--> = mk_abss; +val pretty_sortcontext = + Pretty.commas o map (fn (v, sort) => (Pretty.block o Pretty.breaks) + [Pretty.str v, Pretty.str "::", Pretty.enum "&" "" "" (map Pretty.str sort)]); + 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)); + | pretty_itype (IVarT v) = + Pretty.str v; fun pretty_iexpr (IConst ((c, ty), _)) = Pretty.block [Pretty.str (c ^ "::"), pretty_itype ty] @@ -307,19 +313,22 @@ | fold_aexpr f (e as IVarE _) = f e; -fun eq_itype (ty1, ty2) = +fun eq_ityp ((sctxt1, ty1), (sctxt2, ty2)) = let exception NO_MATCH; - fun eq (IVarT (v1, sort1)) (IVarT (v2, sort2)) subs = - if sort1 <> sort2 - then raise NO_MATCH - else - (case AList.lookup (op =) subs v1 - of NONE => subs |> AList.update (op =) (v1, v2) - | (SOME v1') => - if v1' <> v2 - then raise NO_MATCH - else subs) + fun eq_sctxt subs sctxt1 sctxt2 = + map (fn (v, sort) => case AList.lookup (op =) subs v + of NONE => raise NO_MATCH + | SOME v' => case AList.lookup (op =) sctxt2 v' + of NONE => raise NO_MATCH + | SOME sort' => if sort <> sort' then raise NO_MATCH else ()) sctxt1 + fun eq (IVarT v1) (IVarT v2) subs = + (case AList.lookup (op =) subs v1 + of NONE => subs |> AList.update (op =) (v1, v2) + | SOME v1' => + if v1' <> v2 + then raise NO_MATCH + else subs) | eq (IType (tyco1, tys1)) (IType (tyco2, tys2)) subs = if tyco1 <> tyco2 then raise NO_MATCH @@ -360,7 +369,7 @@ fun type_vnames ty = let - fun extr (IVarT (v, _)) = + fun extr (IVarT v) = insert (op =) v | extr _ = I; in fold_atype extr ty end; @@ -384,8 +393,8 @@ (* type definitions *) -type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype); -type datatyp = (vname * sort) list * (string * itype list) list; +type funn = (iexpr list * iexpr) list * ityp; +type datatyp = ClassPackage.sortcontext * (string * itype list) list; datatype prim = Pretty of Pretty.T @@ -398,7 +407,7 @@ | Typesyn of (vname * sort) list * itype | Datatype of datatyp | Datatypecons of string - | Class of class list * (vname * (string * (ClassPackage.sortcontext * itype)) list) + | Class of class list * (vname * (string * ityp) list) | Classmember of class | Classinst of ((class * (string * (vname * sort) list)) * (class * (string * classlookup list list)) list) @@ -433,13 +442,13 @@ ) | pretty_def (Typesyn (vs, ty)) = Pretty.block [ - Pretty.list "(" ")" (map (pretty_itype o IVarT) vs), + Pretty.list "(" ")" (pretty_sortcontext vs), Pretty.str " |=> ", pretty_itype ty ] | pretty_def (Datatype (vs, cs)) = Pretty.block [ - Pretty.list "(" ")" (map (pretty_itype o IVarT) vs), + Pretty.list "(" ")" (pretty_sortcontext vs), Pretty.str " |=> ", Pretty.enum " |" "" "" (map (fn (c, tys) => (Pretty.block o Pretty.breaks) @@ -774,14 +783,17 @@ val _ = if length memdefs > length memdefs then error "too many member definitions given" else (); - fun instant (w, ty) (var as (v, _)) = - if v = w then ty else IVarT var; - fun mk_memdef (m, (ctxt, ty)) = + fun instant (w, ty) v = + if v = w then ty else IVarT v; + fun mk_memdef (m, (sortctxt, ty)) = case AList.lookup (op =) memdefs m of NONE => error ("missing definition for member " ^ quote m) - | SOME (m', (eqs, (ctxt', ty'))) => - if eq_itype (instant_itype (instant (v, tyco `%% map IVarT arity)) ty, ty') - then (m, (m', (check_funeqs eqs, (ctxt', ty')))) + | SOME (m', (eqs, (sortctxt', ty'))) => + if eq_ityp + ((sortctxt |> fold (fn v_sort => AList.update (op =) v_sort) arity, + instant_itype (instant (v, tyco `%% map (IVarT o fst) arity)) ty), + (sortctxt', ty')) + then (m, (m', (check_funeqs eqs, (sortctxt', ty')))) else error ("inconsistent type for member definition " ^ quote m) in Classinst (d, map mk_memdef membrs) end; @@ -933,7 +945,7 @@ 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 + in (([([add_var], e `$ add_var)], cty)) end | eq => (([eq], cty))) | eta funn = funn; @@ -948,13 +960,13 @@ val used_type = map fst sortctxt; val clash = gen_union (op =) (used_expr, used_type); val rename_map = fold_map (fn c => invent c #-> (fn c' => pair (c, c'))) clash [] |> fst; - fun rename (v, sort) = - (perhaps (AList.lookup (op =) rename_map) v, sort); + val rename = + perhaps (AList.lookup (op =) rename_map); val rename_typ = instant_itype (IVarT o rename); val rename_expr = map_iexpr_itype rename_typ; fun rename_eq (args, rhs) = (map rename_expr args, rename_expr rhs) in - (map rename_eq eqs, (map rename sortctxt, rename_typ ty)) + (map rename_eq eqs, (map (apfst rename) sortctxt, rename_typ ty)) end; in (map_defs o map_def_fun) unclash end; @@ -975,10 +987,13 @@ | _ => mk (postprocess, validate) ((shallow, name), 1) end | mk (postprocess, validate) (("", name), i) = - postprocess ("", name ^ "_" ^ string_of_int (i+1)) + postprocess ("", name ^ replicate_string i "'") + |> perhaps validate + | mk (postprocess, validate) ((shallow, name), 1) = + postprocess (shallow, shallow ^ "_" ^ name) |> perhaps validate | mk (postprocess, validate) ((shallow, name), i) = - postprocess (shallow, shallow ^ "_" ^ name ^ "_" ^ string_of_int (i+1)) + postprocess (shallow, name ^ replicate_string i "'") |> perhaps validate; fun is_valid _ _ = true; fun maybe_unique _ _ = NONE; diff -r 1c31769f9796 -r 1457d810b408 src/Pure/Tools/nbe.ML --- a/src/Pure/Tools/nbe.ML Mon Feb 27 15:49:56 2006 +0100 +++ b/src/Pure/Tools/nbe.ML Mon Feb 27 15:51:37 2006 +0100 @@ -32,22 +32,28 @@ "\n---\n") true s); -val tab = ref Symtab.empty -fun lookup s = the(Symtab.lookup (!tab) s) -fun update sx = (tab := Symtab.update sx (!tab)) +val tab : NBE_Eval.Univ Symtab.table ref = ref Symtab.empty; +fun lookup s = the(Symtab.lookup (!tab) s); +fun update sx = (tab := Symtab.update sx (!tab)); fun defined s = Symtab.defined (!tab) s; fun top_nbe st thy = -let val t = Sign.read_term thy st - val ((t',diff),thy') = CodegenPackage.codegen_incr t thy - val _ = (tab := NBE_Data.get thy; + let + val t = Sign.read_term thy st; + val nbe_tab = NBE_Data.get thy; + val modl_old = CodegenThingol.partof (Symtab.keys nbe_tab) + (CodegenPackage.get_root_module thy); + val (t', thy') = CodegenPackage.codegen_term t thy + val modl_new = CodegenPackage.get_root_module thy; + val diff = CodegenThingol.diff_module (modl_old, modl_new); + val _ = (tab := nbe_tab; Library.seq (use_show o NBE_Codegen.generate defined) diff) val thy'' = NBE_Data.put (!tab) thy' val nt' = NBE_Eval.nbe (!tab) t' val _ = print nt' -in - thy'' -end + in + thy'' + end; structure P = OuterParse and K = OuterKeyword;