--- 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 =
--- 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)
--- 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
--- 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 *)
--- 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
]
--- 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;