# HG changeset patch # User haftmann # Date 1156854675 -7200 # Node ID 67fa1c6ba89e7b77d09853f3d2f524bea5a5b6b0 # Parent 0b102b4182defd4e170faf00d3fd9c89cd261bf0 refinements diff -r 0b102b4182de -r 67fa1c6ba89e src/HOL/Tools/typedef_codegen.ML --- a/src/HOL/Tools/typedef_codegen.ML Tue Aug 29 14:31:14 2006 +0200 +++ b/src/HOL/Tools/typedef_codegen.ML Tue Aug 29 14:31:15 2006 +0200 @@ -7,10 +7,13 @@ signature TYPEDEF_CODEGEN = sig + val get_triv_typedef: theory -> string + -> ((((string * sort) list * (string * typ list) list) * thm) * + ((string * typ) * thm)) option val typedef_fun_extr: theory -> string * typ -> thm list option val typedef_type_extr: theory -> string - -> (((string * sort) list * (string * typ list) list) * tactic) option - val setup: theory -> theory; + -> (((string * sort) list * (string * typ list) list) * tactic) option + val setup: theory -> theory end; structure TypedefCodegen: TYPEDEF_CODEGEN = @@ -103,41 +106,36 @@ end) | typedef_tycodegen thy defs gr dep module brack _ = NONE; -fun typedef_type_extr thy tyco = +fun get_triv_typedef thy tyco = case TypedefPackage.get_info thy tyco of SOME {abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs, Rep_name = c_rep, - set_def = SOME def, Abs_inject = inject, ...} => + set_def = SOME def, Abs_inject = inject, Abs_inverse = inverse, ... } => let val exists_thm = UNIV_I - |> Drule.instantiate' [SOME (ctyp_of thy ty_rep)] [] + |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] [] |> rewrite_rule [symmetric def]; in case try (op OF) (inject, [exists_thm, exists_thm]) - of SOME eq_thm => SOME (((Term.typ_tfrees o Type.no_tvars) ty_abs, [(c_abs, [ty_rep])]), - (ALLGOALS o match_tac) [eq_reflection] - THEN (ALLGOALS o match_tac) [eq_thm]) + of SOME eq_thm => + SOME (((Term.add_tfreesT (Type.no_tvars ty_abs) [], [(c_abs, [ty_rep])]), eq_thm), + ((c_rep, ty_abs --> ty_rep), inverse OF [exists_thm])) | NONE => NONE end | _ => NONE; +fun typedef_type_extr thy tyco = + case get_triv_typedef thy tyco + of SOME ((vs_cs, thm), _) => SOME (vs_cs, + (ALLGOALS o match_tac) [eq_reflection] + THEN (ALLGOALS o match_tac) [thm]) + | NONE => NONE; + fun typedef_fun_extr thy (c, ty) = case (fst o strip_type) ty of Type (tyco, _) :: _ => - (case TypedefPackage.get_info thy tyco - of SOME {abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs, Rep_name = c_rep, - set_def = SOME def, Abs_inverse = inverse, ...} => - if c = c_rep then - let - val exists_thm = - UNIV_I - |> Drule.instantiate' [SOME (ctyp_of thy ty_rep)] [] - |> rewrite_rule [symmetric def] - in case try (op OF) (inverse, [exists_thm, exists_thm]) - of SOME eq_thm => SOME [eq_thm] - | NONE => NONE - end - else NONE - | _ => NONE) + (case get_triv_typedef thy tyco + of SOME (_, ((c', _), thm)) => if c = c' then SOME [thm] else NONE + | NONE => NONE) | _ => NONE; val setup = diff -r 0b102b4182de -r 67fa1c6ba89e src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Tue Aug 29 14:31:14 2006 +0200 +++ b/src/Pure/Tools/class_package.ML Tue Aug 29 14:31:15 2006 +0200 @@ -7,9 +7,9 @@ signature CLASS_PACKAGE = sig - val class: bstring -> class list -> Element.context list -> theory + val class: bstring -> class list -> Element.context Locale.element list -> theory -> Proof.context * theory - val class_i: bstring -> class list -> Element.context_i list -> theory + val class_i: bstring -> class list -> Element.context_i Locale.element list -> theory -> Proof.context * theory (*FIXME: in _i variants, bstring should be bstring option*) val instance_arity: ((xstring * string list) * string) list @@ -165,7 +165,7 @@ Name.context |> Name.declare clsvar |> fold (fn (_, ty) => fold Name.declare - ((map (fst o fst) o typ_tvars) ty @ (map fst o typ_tfrees) ty)) const_sign + ((map (fst o fst) o typ_tvars) ty @ map fst (Term.add_tfreesT ty []))) const_sign |> fold_map add_var asorts; val ty_inst = Type (tyco, map TFree vsorts); val inst_signs = map (apsnd (subst_clsvar clsvar ty_inst)) const_sign; @@ -305,20 +305,26 @@ fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy = let + val (elems, exprs) = fold_rev (fn Locale.Elem e => apfst (cons e) + | Locale.Expr e => apsnd (cons e)) + raw_elems ([], []); val supclasses = map (prep_class thy) raw_supclasses; val supsort = supclasses |> map (#name_axclass o fst o the_class_data thy) |> Sign.certify_sort thy |> null ? K (Sign.defaultS thy); - val expr = (Locale.Merge o map (Locale.Locale o #name_locale o fst o the_class_data thy)) supclasses; + val expr_supclasses = Locale.Merge + (map (Locale.Locale o #name_locale o fst o the_class_data thy) supclasses); + val expr = Locale.Merge (map (Locale.Locale o #name_locale o fst o the_class_data thy) supclasses + @ exprs); val mapp_sup = AList.make (the o AList.lookup (op =) ((flat o map (the_parm_map thy) o the_ancestry thy) supclasses)) - ((map (fst o fst) o Locale.parameters_of_expr thy) expr); + ((map (fst o fst) o Locale.parameters_of_expr thy) expr_supclasses); fun extract_tyvar_consts thy name_locale = let fun extract_classvar ((c, ty), _) w = - (case add_typ_tfrees (ty, []) + (case Term.add_tfreesT ty [] of [(v, _)] => (case w of SOME u => if u = v then w else error ("Additonal type variable in type signature of constant " ^ quote c) | NONE => SOME v) @@ -357,7 +363,7 @@ Const (c, subst_clsvar v (TFree (v, [class])) ty); in thy - |> add_locale bname expr raw_elems + |> add_locale bname expr elems |-> (fn (name_locale, ctxt) => `(fn thy => extract_tyvar_consts thy name_locale) #-> (fn (v, (raw_cs_sup, raw_cs_this)) => @@ -626,7 +632,7 @@ then instance_sort else axclass_instance_sort) (class, sort) thy; val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::); -val class_bodyP = P.!!! (Scan.repeat1 P.context_element); +val class_bodyP = P.!!! (Scan.repeat1 P.locale_element); val inst = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 P.sort --| P.$$$ ")")) [] -- P.xname --| P.$$$ "::" -- P.sort) diff -r 0b102b4182de -r 67fa1c6ba89e src/Pure/Tools/codegen_consts.ML --- a/src/Pure/Tools/codegen_consts.ML Tue Aug 29 14:31:14 2006 +0200 +++ b/src/Pure/Tools/codegen_consts.ML Tue Aug 29 14:31:15 2006 +0200 @@ -103,6 +103,7 @@ | class_of_classop thy (c, _) = NONE; fun insts_of_classop thy (c_tys as (c, tys)) = + (*get rid of this finally*) case AxClass.class_of_param thy c of NONE => [c_tys] | SOME class => let diff -r 0b102b4182de -r 67fa1c6ba89e src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Tue Aug 29 14:31:14 2006 +0200 +++ b/src/Pure/Tools/codegen_package.ML Tue Aug 29 14:31:15 2006 +0200 @@ -59,7 +59,6 @@ val nsp_dtcon = "dtcon"; val nsp_mem = "mem"; val nsp_inst = "inst"; -val nsp_instmem = "instmem"; val nsp_eval = "EVAL"; (*only for evaluation*) fun add_nsp shallow name = @@ -98,7 +97,7 @@ |> apsnd (fn seri => seri nsp_dtcon [[nsp_module], [nsp_class, nsp_tyco], - [nsp_const, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem]] + [nsp_const, nsp_dtcon, nsp_class, nsp_mem, nsp_inst]] ) ) |> Symtab.update ( @@ -106,7 +105,7 @@ |> apsnd (fn seri => seri (nsp_dtcon, [nsp_module, nsp_class, nsp_tyco, nsp_dtcon]) [[nsp_module], [nsp_class], [nsp_tyco], [nsp_const, nsp_mem], - [nsp_dtcon], [nsp_inst], [nsp_instmem]] + [nsp_dtcon], [nsp_inst]] ) ) ); @@ -121,25 +120,30 @@ bounds1 = bounds2 andalso stamp1 = stamp2) x type target_data = { - syntax_class: string Symtab.table, + syntax_class: ((string * (string -> string option)) * stamp) Symtab.table, + syntax_inst: unit Symtab.table, syntax_tyco: (itype CodegenSerializer.pretty_syntax * stamp) Symtab.table, syntax_const: (iterm CodegenSerializer.pretty_syntax * stamp) Symtab.table }; -fun map_target_data f { syntax_class, syntax_tyco, syntax_const } = +fun map_target_data f { syntax_class, syntax_inst, syntax_tyco, syntax_const } = let - val (syntax_class, syntax_tyco, syntax_const) = - f (syntax_class, syntax_tyco, syntax_const) + val (syntax_class, syntax_inst, syntax_tyco, syntax_const) = + f (syntax_class, syntax_inst, syntax_tyco, syntax_const) in { syntax_class = syntax_class, + syntax_inst = syntax_inst, syntax_tyco = syntax_tyco, syntax_const = syntax_const } : target_data end; fun merge_target_data - ({ syntax_class = syntax_class1, syntax_tyco = syntax_tyco1, syntax_const = syntax_const1 }, - { syntax_class = syntax_class2, syntax_tyco = syntax_tyco2, syntax_const = syntax_const2 }) = - { syntax_class = Symtab.merge (op =) (syntax_class1, syntax_class2), + ({ syntax_class = syntax_class1, syntax_inst = syntax_inst1, + syntax_tyco = syntax_tyco1, syntax_const = syntax_const1 }, + { syntax_class = syntax_class2, syntax_inst = syntax_inst2, + syntax_tyco = syntax_tyco2, syntax_const = syntax_const2 }) = + { syntax_class = Symtab.merge (eq_snd (op =)) (syntax_class1, syntax_class2), + syntax_inst = Symtab.merge (op =) (syntax_inst1, syntax_inst2), syntax_tyco = Symtab.merge (eq_snd (op =)) (syntax_tyco1, syntax_tyco2), syntax_const = Symtab.merge (eq_snd (op =)) (syntax_const1, syntax_const2) } : target_data; @@ -158,7 +162,8 @@ Symtab.empty |> Symtab.fold (fn (target, _) => Symtab.update (target, - { syntax_class = Symtab.empty, syntax_tyco = Symtab.empty, syntax_const = Symtab.empty }) + { syntax_class = Symtab.empty, syntax_inst = Symtab.empty, + syntax_tyco = Symtab.empty, syntax_const = Symtab.empty }) ) (! serializers) } : T; val copy = I; @@ -228,6 +233,10 @@ CodegenNames.const thy c_ty |> add_nsp nsp_const; +fun idf_of_classop thy c_ty = + CodegenNames.const thy c_ty + |> add_nsp nsp_mem; + fun const_of_idf thy idf = case dest_nsp nsp_const idf of SOME c => CodegenNames.const_rev thy c |> SOME @@ -423,9 +432,6 @@ case ClassPackage.operational_sort_of thy sort of [] => NONE | sort => SOME (v, sort)) arity; - fun mk_instmemname (m, ty) = - NameSpace.append (NameSpace.append ((NameSpace.drop_base o NameSpace.drop_base) - inst) nsp_instmem) (NameSpace.base (idf_of_const thy thmtab (m, ty))); fun gen_suparity supclass trns = trns |> ensure_def_class thy tabs supclass @@ -689,11 +695,9 @@ fun codegen_term t thy = let val _ = Thm.cterm_of thy t; -(* val _ = writeln "STARTING GENERATION"; *) -(* val _ = (writeln o Sign.string_of_term thy) t; *) in thy - |> expand_module (SOME [] (*(Symtab.keys (#target_data (CodegenData.get thy)))*)) (consts_of t) NONE exprgen_term t + |> expand_module (SOME []) (consts_of t) NONE exprgen_term t end; val is_dtcon = has_nsp nsp_dtcon; @@ -727,7 +731,7 @@ end; val target_data = ((fn data => (the o Symtab.lookup data) "ml") o #target_data o CodegenData.get) thy; - val eval = CodegenSerializer.eval_term nsp_eval nsp_dtcon [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem], [nsp_eval]] + val eval = CodegenSerializer.eval_term nsp_eval nsp_dtcon [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_dtcon, nsp_class, nsp_mem, nsp_inst], [nsp_eval]] ((Option.map fst oo Symtab.lookup) (#syntax_tyco target_data), (Option.map fst oo Symtab.lookup) (#syntax_const target_data)) (Symtab.keys (#syntax_tyco target_data) @ Symtab.keys (#syntax_const target_data)) @@ -768,18 +772,42 @@ |-> (fn [x] => pair x) end; -fun gen_add_syntax_class prep_class class target pretty thy = - thy - |> map_codegen_data - (fn (modl, gens, target_data) => - (modl, gens, - target_data |> Symtab.map_entry target - (map_target_data - (fn (syntax_class, syntax_tyco, syntax_const) => - (syntax_class - |> Symtab.update (prep_class thy class, pretty), syntax_tyco, syntax_const))))); +fun gen_add_syntax_class prep_class prep_const raw_class target (pretty, raw_ops) thy = + let + val class = (idf_of_class thy o prep_class thy) raw_class; + val ops = (map o apfst) (idf_of_classop thy o prep_const thy) raw_ops; + val syntax_ops = AList.lookup (op =) ops; + in + thy + |> map_codegen_data + (fn (modl, gens, target_data) => + (modl, gens, + target_data |> Symtab.map_entry target + (map_target_data + (fn (syntax_class, syntax_inst, syntax_tyco, syntax_const) => + (syntax_class + |> Symtab.update (class, ((pretty, syntax_ops), stamp ())), syntax_inst, + syntax_tyco, syntax_const))))) + end; -val add_syntax_class = gen_add_syntax_class Sign.intern_class; +val add_syntax_class = gen_add_syntax_class Sign.intern_class CodegenConsts.read_const_typ; + +fun gen_add_syntax_inst prep_class prep_tyco (raw_class, raw_tyco) target thy = + let + val inst = idf_of_inst thy (prep_class thy raw_class, prep_tyco thy raw_tyco); + in + thy + |> map_codegen_data + (fn (modl, gens, target_data) => + (modl, gens, + target_data |> Symtab.map_entry target + (map_target_data + (fn (syntax_class, syntax_inst, syntax_tyco, syntax_const) => + (syntax_class, syntax_inst |> Symtab.update (inst, ()), + syntax_tyco, syntax_const))))) + end; + +val add_syntax_inst = gen_add_syntax_inst Sign.intern_class Sign.intern_type; fun parse_syntax_tyco raw_tyco = let @@ -803,8 +831,8 @@ (modl, gens, target_data |> Symtab.map_entry target (map_target_data - (fn (syntax_class, syntax_tyco, syntax_const) => - (syntax_class, syntax_tyco |> Symtab.update + (fn (syntax_class, syntax_inst, syntax_tyco, syntax_const) => + (syntax_class, syntax_inst, syntax_tyco |> Symtab.update (tyco, (pretty, stamp ())), syntax_const)))))) end; @@ -821,8 +849,8 @@ (modl, gens, target_data |> Symtab.map_entry target (map_target_data - (fn (syntax_class, syntax_tyco, syntax_const) => - (syntax_class, syntax_tyco, + (fn (syntax_class, syntax_inst, syntax_tyco, syntax_const) => + (syntax_class, syntax_inst, syntax_tyco, syntax_const |> Symtab.update (c, (pretty, stamp ()))))))); @@ -924,14 +952,16 @@ |> #target_data |> (fn data => (the oo Symtab.lookup) data target); val s_class = #syntax_class target_data + val s_inst = #syntax_inst target_data val s_tyco = #syntax_tyco target_data val s_const = #syntax_const target_data in (seri ( - Symtab.lookup s_class, + (Option.map fst oo Symtab.lookup) s_class, (Option.map fst oo Symtab.lookup) s_tyco, (Option.map fst oo Symtab.lookup) s_const - ) (Symtab.keys s_class @ Symtab.keys s_tyco @ Symtab.keys s_const, cs) module : unit; thy) + ) (Symtab.keys s_class @ Symtab.keys s_inst + @ Symtab.keys s_tyco @ Symtab.keys s_const, cs) module : unit; thy) end; in thy @@ -950,10 +980,10 @@ in val (generateK, serializeK, - syntax_classK, syntax_tycoK, syntax_constK, + syntax_classK, syntax_instK, syntax_tycoK, syntax_constK, purgeK) = ("code_generate", "code_serialize", - "code_classapp", "code_typapp", "code_constapp", + "code_class", "code_instance", "code_typapp", "code_constapp", "code_purge"); val generateP = @@ -983,13 +1013,24 @@ Scan.repeat1 ( P.xname -- Scan.repeat1 ( - P.name -- P.string + P.name -- (P.string -- Scan.optional + (P.$$$ "(" |-- Scan.repeat1 (P.term -- P.string) --| P.$$$ ")") []) ) ) >> (Toplevel.theory oo fold) (fn (raw_class, syns) => fold (fn (target, p) => add_syntax_class raw_class target p) syns) ); +val syntax_instP = + OuterSyntax.command syntax_instK "define code syntax for instance" K.thy_decl ( + Scan.repeat1 ( + P.$$$ "(" |-- P.xname --| P.$$$ "::" -- P.xname --| P.$$$ ")" + -- Scan.repeat1 P.name + ) + >> (Toplevel.theory oo fold) (fn (raw_inst, targets) => + fold (fn target => add_syntax_inst raw_inst target) targets) + ); + val syntax_tycoP = OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl ( Scan.repeat1 ( @@ -1019,7 +1060,7 @@ (Scan.succeed (Toplevel.theory purge_code)); val _ = OuterSyntax.add_parsers [generateP, serializeP, - syntax_classP, syntax_tycoP, syntax_constP, + syntax_classP, syntax_instP, syntax_tycoP, syntax_constP, purgeP]; end; (* local *) diff -r 0b102b4182de -r 67fa1c6ba89e src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Tue Aug 29 14:31:14 2006 +0200 +++ b/src/Pure/Tools/codegen_serializer.ML Tue Aug 29 14:31:15 2006 +0200 @@ -12,7 +12,7 @@ type serializer = string list list -> OuterParse.token list -> - ((string -> string option) + ((string -> (string * (string -> string option)) option) * (string -> CodegenThingol.itype pretty_syntax option) * (string -> CodegenThingol.iterm pretty_syntax option) -> string list * string list option @@ -31,11 +31,11 @@ }; val mk_flat_ml_resolver: string list -> string -> string; val eval_term: string -> string -> string list list - -> (string -> CodegenThingol.itype pretty_syntax option) - * (string -> CodegenThingol.iterm pretty_syntax option) - -> string list - -> (string * 'a ref) * CodegenThingol.iterm -> CodegenThingol.module - -> 'a; + -> (string -> CodegenThingol.itype pretty_syntax option) + * (string -> CodegenThingol.iterm pretty_syntax option) + -> string list + -> (string * 'a ref) * CodegenThingol.iterm -> CodegenThingol.module + -> 'a; val eval_verbose: bool ref; val ml_fun_datatype: string -> ((string -> CodegenThingol.itype pretty_syntax option) @@ -207,7 +207,7 @@ type serializer = string list list -> OuterParse.token list -> - ((string -> string option) + ((string -> (string * (string -> string option)) option) * (string -> itype pretty_syntax option) * (string -> iterm pretty_syntax option) -> string list * string list option @@ -215,7 +215,7 @@ * OuterParse.token list; fun abstract_serializer (target, nspgrp) name_root (from_defs, from_module, validator, postproc) - postprocess (class_syntax, tyco_syntax, const_syntax) + postprocess (class_syntax : string -> (string * (string -> string option)) option, tyco_syntax, const_syntax) (drop: string list, select) module = let fun from_module' resolv imps ((name_qual, name), defs) = @@ -228,7 +228,7 @@ |> debug_msg (fn _ => "selecting submodule...") |> (if is_some select then (CodegenThingol.project_module o the) select else I) |> debug_msg (fn _ => "serializing...") - |> CodegenThingol.serialize (from_defs (class_syntax : string -> string option, tyco_syntax, const_syntax)) + |> CodegenThingol.serialize (from_defs (class_syntax, tyco_syntax, const_syntax)) from_module' validator postproc nspgrp name_root |> K () end; @@ -382,13 +382,17 @@ fun re_mangle _ dst = error ("No such definition name: " ^ quote dst); ); +fun first_upper s = + implode (nth_map 0 (Symbol.to_ascii_upper) (explode s)); + +fun ml_from_dictvar v = + first_upper v ^ "_"; + fun ml_expr_seri is_cons (tyco_syntax, const_syntax) resolv = let val ml_from_label = str o translate_string (fn "_" => "__" | "." => "_" | c => c) o NameSpace.base o resolv; - fun ml_from_dictvar v = - str (Symbol.to_ascii_upper v ^ "_"); fun ml_from_tyvar (v, []) = str "()" | ml_from_tyvar (v, sort) = @@ -398,7 +402,7 @@ in Pretty.block [ str "(", - ml_from_dictvar v, + (str o ml_from_dictvar) v, str ":", case sort of [class] => mk_class class @@ -432,10 +436,10 @@ ) | from_classlookup fxy (Lookup (classes, (v, ~1))) = from_lookup BR classes - (ml_from_dictvar v) + ((str o ml_from_dictvar) v) | from_classlookup fxy (Lookup (classes, (v, i))) = from_lookup BR (string_of_int (i+1) :: classes) - (ml_from_dictvar v) + ((str o ml_from_dictvar) v) in case lss of [] => str "()" | [ls] => from_classlookup fxy ls @@ -679,7 +683,7 @@ | _ => error ("Class block without class: " ^ (commas o map (quote o fst)) defs) fun ml_from_class (name, (supclasses, (v, membrs))) = let - val w = (Char.toString o Char.toUpper o the o Char.fromString) v; + val w = ml_from_dictvar v; fun from_supclass class = Pretty.block [ ml_from_label class, @@ -860,15 +864,20 @@ let val resolv = resolver ""; val resolv_here = resolver prefix; + fun hs_from_class cls = case class_syntax cls + of NONE => resolv cls + | SOME (cls, _) => cls; + fun hs_from_classop_name cls clsop = case class_syntax cls + of NONE => NameSpace.base clsop + | SOME (_, classop_syntax) => case classop_syntax clsop + of NONE => NameSpace.base clsop + | SOME clsop => clsop; fun hs_from_sctxt vs = let - fun from_class cls = - class_syntax cls - |> the_default (resolv cls) fun from_sctxt [] = str "" | from_sctxt vs = vs - |> map (fn (v, cls) => str (from_class cls ^ " " ^ v)) + |> map (fn (v, cls) => str (hs_from_class cls ^ " " ^ v)) |> Pretty.enum "," "(" ")" |> (fn p => Pretty.block [p, str " => "]) in @@ -1048,13 +1057,13 @@ Pretty.block [ str "instance ", hs_from_sctxt arity, - str (resolv clsname ^ " "), + str (hs_from_class clsname ^ " "), hs_from_type BR (tyco `%% map (ITyVar o fst) arity), str " where", Pretty.fbrk, Pretty.chunks (map (fn (m, e) => (Pretty.block o Pretty.breaks) [ - (str o NameSpace.base o resolv) m, + (str o hs_from_classop_name clsname) m, str "=", hs_from_expr NOBR e ] diff -r 0b102b4182de -r 67fa1c6ba89e src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Tue Aug 29 14:31:14 2006 +0200 +++ b/src/Pure/Tools/codegen_thingol.ML Tue Aug 29 14:31:15 2006 +0200 @@ -87,6 +87,7 @@ val diff_module: module * module -> (string * def) list; val project_module: string list -> module -> module; val purge_module: string list -> module -> module; +(* val flat_funs_datatypes: module -> (string * def) list; *) val add_eval_def: string (*shallow name space*) * iterm -> module -> string * module; val delete_garbage: string list (*hidden definitions*) -> module -> module; val has_nsp: string -> string -> bool; @@ -323,8 +324,8 @@ add_constnames e1 #> add_constnames e2 | add_constnames (_ `|-> e) = add_constnames e - | add_constnames (INum _) = - I + | add_constnames (INum (_, e)) = + add_constnames e | add_constnames (IChar (_, e)) = add_constnames e | add_constnames (ICase (_, e)) = @@ -338,10 +339,10 @@ add_varnames e1 #> add_varnames e2 | add_varnames ((v, _) `|-> e) = insert (op =) v #> add_varnames e - | add_varnames (INum _) = - I - | add_varnames (IChar _) = - I + | add_varnames (INum (_, e)) = + add_varnames e + | add_varnames (IChar (_, e)) = + add_varnames e | add_varnames (ICase (((de, _), bses), _)) = add_varnames de #> fold (fn (be, se) => add_varnames be #> add_varnames se) bses; @@ -694,6 +695,65 @@ |> dest_modl end; +fun flat_module modl = + maps ( + fn (name, Module modl) => map (apfst (NameSpace.append name)) (flat_module modl) + | (name, Def def) => [(name, def)] + ) ((AList.make (Graph.get_node modl) o flat o Graph.strong_conn) modl) + +(* +fun flat_funs_datatypes modl = + map ( + fn def as (_, Datatype _) => def + | (name, Fun (eqs, (sctxt, ty))) => let + val vs = fold (fn (rhs, lhs) => fold add_varnames rhs #> add_varnames lhs) eqs []; + fun fold_map_snd f (x, ys) = fold_map f ys #-> (fn zs => pair (x, zs)); + fun all_ops_of class = [] : (class * (string * itype) list) list + (*FIXME; itype within current context*); + fun name_ops class = + (fold_map o fold_map_snd) + (fn (c, ty) => Name.variants [c] #-> (fn [v] => pair (c, (ty, v)))) (all_ops_of class); + (*FIXME: should contain superclasses only once*) + val (octxt, _) = (fold_map o fold_map_snd) name_ops sctxt + (Name.make_context vs); + (* --> (iterm * itype) list *) + fun flat_classlookup (Instance (inst, lss)) = + (case get_def modl inst + of (Classinst (_, (suparities, ops))) + => maps (maps flat_classlookup o snd) suparities @ map (apsnd flat_iterm) ops + | _ => error ("Bad instance: " ^ quote inst)) + | flat_classlookup (Lookup (classes, (v, k))) = + let + val parm_map = nth ((the o AList.lookup (op =) octxt) v) + (if k = ~1 then 0 else k); + in map (apfst IVar o swap o snd) (case classes + of class::_ => (the o AList.lookup (op =) parm_map) class + | _ => (snd o hd) parm_map) + end + and flat_iterm (e as IConst (c, (lss, ty))) = + let + val (es, tys) = split_list ((maps o maps) flat_classlookup lss) + in IConst (c, ([], tys `--> ty)) `$$ es end + (*FIXME Eliminierung von Projektionen*) + | flat_iterm (e as IVar _) = + e + | flat_iterm (e1 `$ e2) = + flat_iterm e1 `$ flat_iterm e2 + | flat_iterm (v_ty `|-> e) = + v_ty `|-> flat_iterm e + | flat_iterm (INum (k, e)) = + INum (k, flat_iterm e) + | flat_iterm (IChar (s, e)) = + IChar (s, flat_iterm e) + | flat_iterm (ICase (((de, dty), es), e)) = + ICase (((flat_iterm de, dty), map (pairself flat_iterm) es), flat_iterm e); + in + (name, Fun (map (fn (lhs, rhs) => (map flat_iterm lhs, flat_iterm rhs)) eqs, + ([], maps ((maps o maps) (map (fst o snd) o snd) o snd) octxt `--> ty))) + end + ) (flat_module modl); +*) + val add_deps_of_sortctxt = fold (fn (v : vname, sort : sort) => fold (insert (op =)) sort); @@ -1099,7 +1159,7 @@ val (common, (_, rem)) = chop_prefix (op =) (prefix, NameSpace.unpack name); val (_, SOME tab') = get_path_name common tab; val (name', _) = get_path_name rem tab'; - in NameSpace.pack name' end handle BIND => (error "Missing name: " ^ quote name); + in NameSpace.pack name' end handle BIND => (error ("Missing name: " ^ quote name ^ ", in " ^ quote (NameSpace.pack prefix))); in deresolv (mk module (AList.make (K NameMangler.empty) nsp_conn) Symtab.empty) end;