--- a/src/Pure/Tools/class_package.ML Sat Feb 25 15:11:35 2006 +0100
+++ b/src/Pure/Tools/class_package.ML Sat Feb 25 15:19:00 2006 +0100
@@ -12,16 +12,16 @@
val add_class_i: bstring -> class list -> Element.context_i list -> theory
-> ProofContext.context * theory
val add_instance_arity: (xstring * string list) * string
- -> ((bstring * Attrib.src list) * string) list
+ -> bstring * Attrib.src list -> ((bstring * Attrib.src list) * string) list
-> theory -> Proof.state
val add_instance_arity_i: (string * sort list) * sort
- -> ((bstring * attribute list) * term) list
+ -> bstring * attribute list -> ((bstring * attribute list) * term) list
-> theory -> Proof.state
val prove_instance_arity: tactic -> (xstring * string list) * string
- -> ((bstring * Attrib.src list) * string) list
+ -> bstring * Attrib.src list -> ((bstring * Attrib.src list) * string) list
-> theory -> theory
val prove_instance_arity_i: tactic -> (string * sort list) * sort
- -> ((bstring * attribute list) * term) list
+ -> 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
@@ -372,7 +372,7 @@
|> map (apsnd Syntax.unlocalize_mixfix)
val v = (extract_tyvar_name thy o map (snd o fst)) consts1;
val consts2 = map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) consts1;
- in (v, Library.chop (length supcs) consts2) end;
+ in (v, chop (length supcs) consts2) end;
fun add_consts v raw_cs_sup raw_cs_this thy =
let
val mapp_sub = map2 (fn ((c, _), _) => pair c) raw_cs_sup supcs
@@ -397,7 +397,7 @@
end;
fun add_global_constraint v class (c, ty) thy =
thy
- |> Sign.add_const_constraint_i (c, SOME (subst_clsvar v (TVar ((v, 0), [class])) ty));
+ |> Sign.add_const_constraint_i (c, SOME (subst_clsvar v (TFree (v, [class])) ty));
fun mk_const thy class v (c, ty) =
Const (c, subst_clsvar v (TFree (v, [class])) ty);
in
@@ -460,11 +460,15 @@
val add_defs_overloaded = gen_add_defs_overloaded Attrib.attribute Sign.read_term PureThy.add_defs;
val add_defs_overloaded_i = gen_add_defs_overloaded (K I) (K I) PureThy.add_defs_i;
-fun gen_instance_arity prep_arity add_defs tap_def do_proof raw_arity raw_defs theory =
+fun gen_instance_arity prep_arity prep_att add_defs tap_def do_proof raw_arity (raw_name, raw_atts) raw_defs theory =
let
val pp = Sign.pp theory;
val arity as (tyco, asorts, sort) = prep_arity theory ((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)
+ val name = case raw_name
+ of "" => Thm.def_name ((space_implode "_" o map NameSpace.base) sort ^ "_" ^ NameSpace.base tyco)
+ | _ => raw_name;
+ val atts = map (prep_att theory) raw_atts;
fun get_classes thy tyco sort =
let
fun get class classes =
@@ -489,7 +493,7 @@
in
thy
|> Sign.add_const_constraint_i (c, NONE)
- |> pair (c, ty)
+ |> pair (c, Type.unvarifyT ty)
end;
fun check_defs raw_defs c_req thy =
let
@@ -519,7 +523,7 @@
Thm.def_name ((space_implode "_" o map NameSpace.base) sort ^ "_" ^ NameSpace.base tyco);
fun note_all tyco sort thms thy =
thy
- |> PureThy.note_thmss_i PureThy.internalK [((mangle_alldef_name tyco sort, []), [(thms, [])])]
+ |> PureThy.note_thmss_i PureThy.internalK [((name, atts), [(thms, [])])]
|> snd;
fun after_qed cs thy =
thy
@@ -534,9 +538,9 @@
|-> (fn cs => do_proof (after_qed cs) arity)
end;
-fun instance_arity do_proof = gen_instance_arity AxClass.read_arity 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 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;
@@ -552,21 +556,60 @@
local
-val _ = ();
+fun fish_thms (name, expr) after_qed thy =
+ let
+ val _ = writeln ("sub " ^ name)
+ val suplocales = (fn Locale.Merge es => map (fn Locale.Locale n => n) es) expr;
+ val _ = writeln ("super " ^ commas suplocales)
+ fun get_c name =
+ (map (NameSpace.base o fst o fst) o Locale.parameters_of thy) name;
+ fun get_a name =
+ (map (NameSpace.base o fst o fst) o Locale.local_asms_of thy) name;
+ fun get_t supname =
+ map (NameSpace.append (NameSpace.append name ((space_implode "_" o get_c) supname)) o NameSpace.base)
+ (get_a name);
+ val names = map get_t suplocales;
+ val _ = writeln ("fishing for " ^ (commas o map commas) names);
+ in
+ thy
+ |> after_qed ((map o map) (Drule.standard o get_thm thy o Name) names)
+ end;
+
+fun add_interpretation_in (after_qed : thm list list -> theory -> theory) (name, expr) thy =
+ thy
+ |> Locale.interpretation_in_locale (name, expr);
+
+fun prove_interpretation_in tac (after_qed : thm list list -> theory -> theory) (name, expr) thy =
+ thy
+ |> Locale.interpretation_in_locale (name, expr)
+ |> 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 =
let
val class = prep_class theory raw_class;
val sort = prep_sort theory raw_sort;
+ val loc_name = (#name_locale o the_class_data theory) class;
+ val loc_expr = if null sort
+ then Locale.empty
+ else
+ (Locale.Merge o map (Locale.Locale o #name_locale o the_class_data theory)) sort;
+ fun after_qed thmss thy =
+ (writeln "---"; (Pretty.writeln o Display.pretty_thms o Library.flat) thmss; writeln "---"; fold (fn supclass =>
+ AxClass.add_inst_subclass_i (class, supclass)
+ (ALLGOALS (K (intro_classes_tac [])) THEN
+ (ALLGOALS o resolve_tac o Library.flat) thmss)
+ ) sort thy)
in
theory
- |> do_proof
+ |> 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;
-val setup_proof = AxClass.instance_arity_i I ("", [], []);
-fun tactic_proof tac = AxClass.add_inst_arity_i ("", [], []) tac;
+
+val setup_proof = add_interpretation_in;
+val tactic_proof = prove_interpretation_in;
in
@@ -575,13 +618,6 @@
val prove_instance_sort = instance_sort o tactic_proof;
val prove_instance_sort_i = instance_sort_i o tactic_proof;
-(*
-interpretation_in_locale: loc_name * loc_expr -> theory -> Proof.state
- --> rausdestilieren
-*)
-(* switch: wenn es nur axclasses sind
- --> alte Methode, diesen switch möglichst weit am Parser dran *)
-
end; (* local *)
(* extracting dictionary obligations from types *)
@@ -630,10 +666,15 @@
in map mk_look sort_def end;
in
sortctxt
+(* |> print *)
|> map (tab_lookup o fst)
+(* |> print *)
|> map (apfst (operational_sort_of thy))
+(* |> print *)
|> filter (not o null o fst)
+(* |> print *)
|> map mk_lookup
+(* |> print *)
end;
fun extract_classlookup thy (c, raw_typ_use) =
@@ -662,8 +703,8 @@
fun extract_classlookup_inst thy (class, tyco) supclass =
let
fun mk_typ class = Type (tyco, (map TFree o fst o the_inst_sign thy) (class, tyco))
- val typ_def = mk_typ class;
- val typ_use = mk_typ supclass;
+ val typ_def = mk_typ supclass;
+ val typ_use = mk_typ class;
in
extract_lookup thy (extract_sortctxt thy typ_def) typ_def typ_use
end;
@@ -680,12 +721,22 @@
val (classK, instanceK) = ("class", "instance")
+fun wrap_add_instance_subclass (class, sort) thy =
+ case Sign.read_sort thy sort
+ of [class'] =>
+ 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
+ else
+ AxClass.instance_subclass (class, sort) thy
+ | _ => add_instance_sort (class, sort) thy;
+
val parse_inst =
- P.xname -- (
- Scan.repeat P.sort --| P.$$$ "::" -- P.sort
- || P.$$$ "::" |-- P.!!! P.arity
- )
- >> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort))
+ (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 P.sort --| P.$$$ ")")) [] -- P.xname --| P.$$$ "::" -- P.sort)
+ >> (fn ((asorts, tyco), sort) => ((tyco, asorts), sort))
+ || (P.xname --| P.$$$ "::" -- P.!!! P.arity)
+ >> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort));
val locale_val =
(P.locale_expr --
@@ -702,12 +753,10 @@
val instanceP =
OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
- P.$$$ "target_atom" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.sort)
- >> (fn (class, sort) => add_instance_sort (class, sort))
- || P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> AxClass.instance_subclass
- || parse_inst -- Scan.repeat (P.opt_thm_name ":" -- P.prop)
- >> (fn (((tyco, asorts), sort), []) => AxClass.instance_arity I (tyco, asorts, sort)
- | (inst, defs) => add_instance_arity inst defs)
+ P.xname -- ((P.$$$ "\\<subseteq>" || 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)
) >> (Toplevel.print oo Toplevel.theory_to_proof));
val _ = OuterSyntax.add_parsers [classP, instanceP];
--- a/src/Pure/Tools/codegen_package.ML Sat Feb 25 15:11:35 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML Sat Feb 25 15:19:00 2006 +0100
@@ -13,7 +13,6 @@
-> string * typ -> (thm list * typ) option;
type eqextr_default = theory -> auxtab
-> string * typ -> ((thm list * term option) * typ) option;
- type defgen;
type appgen = theory -> auxtab
-> (string * typ) * term list -> CodegenThingol.transact
-> CodegenThingol.iexpr * CodegenThingol.transact;
@@ -26,7 +25,7 @@
-> theory -> theory;
val add_prim_tyco: xstring -> (string * string)
-> theory -> theory;
- val add_prim_const: xstring * string option -> (string * string)
+ val add_prim_const: xstring -> (string * string)
-> theory -> theory;
val add_prim_i: string -> (string * CodegenThingol.prim list)
-> theory -> theory;
@@ -39,7 +38,10 @@
-> theory -> theory;
val set_int_tyco: string -> theory -> theory;
- val codegen_incr: term -> theory -> (string * CodegenThingol.def) list * theory;
+ val codegen_incr: term -> theory -> (CodegenThingol.iexpr * (string * CodegenThingol.def) list) * theory;
+ val is_dtcon: string -> bool;
+ val consts_of_idfs: theory -> string list -> (string * (string * typ)) list
+
val get_ml_fun_datatype: theory -> (string -> string)
-> ((string * CodegenThingol.funn) list -> Pretty.T)
* ((string * CodegenThingol.datatyp) list -> Pretty.T);
@@ -141,6 +143,11 @@
Sign.typ_instance thy (ty1, ty2)
andalso Sign.typ_instance thy (ty2, ty1);
+fun is_overloaded thy c = case Defs.specifications_of (Theory.defs_of thy) c
+ of [] => false
+ | [(ty, _)] => not (eq_typ thy (ty, Sign.the_const_type thy c))
+ | _ => true;
+
structure InstNameMangler = NameManglerFun (
type ctxt = theory;
type src = string * (class * string);
@@ -154,25 +161,24 @@
);
structure ConstNameMangler = NameManglerFun (
- 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, deftab) ((c, (ty_decl, ty)), i) =
+ type ctxt = theory;
+ type src = string * typ;
+ val ord = prod_ord string_ord Term.typ_ord;
+ fun mk thy ((c, ty), i) =
let
- val thyname = case (get_first
- (fn (ty', (_, thyname)) => if eq_typ thy (ty, ty') then SOME thyname else NONE)
- o these o Symtab.lookup deftab) c
- of SOME thyname => thyname
- | _ => (NameSpace.drop_base o alias_get thy o fst o dest_Type o hd o fst o strip_type) ty
val c' = idf_of_name thy nsp_overl c;
- val c'' = NameSpace.append thyname (NameSpace.append nsp_overl (NameSpace.base c'));
+ val prefix = case (AList.lookup (eq_typ thy)
+ (Defs.specifications_of (Theory.defs_of thy) c)) ty
+ of SOME thyname => NameSpace.append thyname nsp_overl
+ | NONE => NameSpace.drop_base c';
+ val c'' = NameSpace.append prefix (NameSpace.base c');
fun mangle (Type (tyco, tys)) =
(NameSpace.base o alias_get thy) tyco :: Library.flat (List.mapPartial mangle tys) |> SOME
| mangle _ =
NONE
in
Vartab.empty
- |> Sign.typ_match thy (ty_decl, ty)
+ |> Sign.typ_match thy (Sign.the_const_type thy c, ty)
|> map (snd o snd) o Vartab.dest
|> List.mapPartial mangle
|> Library.flat
@@ -182,8 +188,14 @@
|> curry (op ^ o swap) ((implode oo replicate) i "'")
end;
fun is_valid _ _ = true;
- fun maybe_unique _ _ = NONE;
- fun re_mangle _ dst = error ("no such constant: " ^ quote dst);
+ fun maybe_unique thy (c, ty) =
+ if is_overloaded thy c
+ then NONE
+ else (SOME o idf_of_name thy nsp_const) c;
+ fun re_mangle thy idf =
+ case name_of_idf thy nsp_const idf
+ of NONE => error ("no such constant: " ^ quote idf)
+ | SOME c => (c, Sign.the_const_type thy c);
);
structure DatatypeconsNameMangler = NameManglerFun (
@@ -212,13 +224,12 @@
);
type auxtab = (deftab * string Symtab.table)
- * (InstNameMangler.T * ((typ * typ list) Symtab.table * ConstNameMangler.T)
+ * (InstNameMangler.T * (typ list Symtab.table * ConstNameMangler.T)
* DatatypeconsNameMangler.T);
type eqextr = theory -> auxtab
-> string * typ -> (thm list * typ) option;
type eqextr_default = theory -> auxtab
-> string * typ -> ((thm list * term option) * typ) option;
-type defgen = theory -> auxtab -> gen_defgen;
type appgen = theory -> auxtab
-> (string * typ) * term list -> transact -> iexpr * transact;
@@ -395,10 +406,10 @@
let
fun get_overloaded (c, ty) =
case Symtab.lookup overltab1 c
- of SOME (ty_decl, tys) =>
+ of SOME tys =>
(case find_first (curry (Sign.typ_instance thy) ty) tys
- of SOME ty' => ConstNameMangler.get (thy, deftab) overltab2
- (c, (ty_decl, ty')) |> SOME
+ of SOME ty' => ConstNameMangler.get thy overltab2
+ (c, ty') |> SOME
| _ => NONE)
| _ => NONE
fun get_datatypecons (c, ty) =
@@ -422,8 +433,7 @@
case dest_nsp nsp_overl idf
of SOME _ =>
idf
- |> ConstNameMangler.rev (thy, deftab) overltab2
- |> apsnd snd
+ |> ConstNameMangler.rev thy overltab2
|> SOME
| NONE => NONE
);
@@ -607,7 +617,7 @@
in
trns
|> debug 4 (fn _ => "generating class " ^ quote cls)
- |> gen_ensure_def [("class", defgen_class thy tabs)] ("generating class " ^ quote cls) cls'
+ |> ensure_def [("class", defgen_class thy tabs)] ("generating class " ^ quote cls) cls'
|> pair cls'
end
and ensure_def_tyco thy tabs tyco trns =
@@ -638,7 +648,7 @@
in
trns
|> debug 4 (fn _ => "generating type constructor " ^ quote tyco)
- |> gen_ensure_def [("datatype", defgen_datatype thy tabs)] ("generating type constructor " ^ quote tyco) tyco'
+ |> ensure_def [("datatype", defgen_datatype thy tabs)] ("generating type constructor " ^ quote tyco) tyco'
|> pair tyco'
end
and exprgen_tyvar_sort thy tabs (v, sort) trns =
@@ -715,14 +725,15 @@
val (arity, memdefs) = ClassPackage.the_inst_sign thy (class, tyco);
fun gen_suparity supclass trns =
trns
- |> (fold_map o fold_map) (exprgen_classlookup thy tabs)
- (ClassPackage.extract_classlookup_inst thy (supclass, tyco) supclass)
+ |> ensure_def_class thy tabs supclass
||>> ensure_def_inst thy tabs (supclass, tyco)
- |-> (fn (ls, _) => pair (supclass, ls));
+ ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
+ (ClassPackage.extract_classlookup_inst thy (supclass, tyco) supclass)
+ |-> (fn ((supclass, inst), lss) => pair (supclass, (inst, lss)));
fun gen_membr (m, ty) trns =
trns
|> mk_fun thy tabs (m, ty)
- |-> (fn SOME funn => pair (idf_of_name thy nsp_mem m, funn)
+ |-> (fn SOME funn => pair (idf_of_name thy nsp_mem m, (idf_of_name thy nsp_mem m ^ "'", funn))
| NONE => error ("could not derive definition for member " ^ quote m));
in
trns
@@ -743,7 +754,7 @@
in
trns
|> debug 4 (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco)
- |> gen_ensure_def [("instance", defgen_inst thy tabs)]
+ |> ensure_def [("instance", defgen_inst thy tabs)]
("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst
|> pair inst
end
@@ -791,30 +802,28 @@
in
trns
|> debug 4 (fn _ => "generating constant " ^ quote c)
- |> gen_ensure_def ((single o get_defgen) idf) ("generating constant " ^ quote c) idf
+ |> ensure_def ((single o get_defgen) idf) ("generating constant " ^ quote c) idf
|> pair idf
end
and exprgen_term thy tabs (Const (f, ty)) trns =
trns
|> appgen thy tabs ((f, ty), [])
|-> (fn e => pair e)
- (* | exprgen_term thy tabs (Var ((v, 0), ty)) trns =
- trns
- |> (exprgen_type thy tabs) ty
- |-> (fn ty => pair (IVarE (v, ty)))
- | exprgen_term thy tabs (Var ((_, _), _)) trns =
- error "Var with index greater 0 encountered during code generation" *)
| exprgen_term thy tabs (Var _) trns =
error "Var encountered during code generation"
| exprgen_term thy tabs (Free (v, ty)) trns =
trns
|> exprgen_type thy tabs ty
|-> (fn ty => pair (IVarE (v, ty)))
- | exprgen_term thy tabs (Abs (v, ty, t)) trns =
- trns
- |> exprgen_type thy tabs ty
- ||>> exprgen_term thy tabs (subst_bound (Free (v, ty), t))
- |-> (fn (ty, e) => pair (IVarE (v, ty) `|-> e))
+ | exprgen_term thy tabs (Abs (abs as (_, ty, _))) trns =
+ let
+ val (v, t) = Term.variant_abs abs
+ in
+ trns
+ |> exprgen_type thy tabs ty
+ ||>> exprgen_term thy tabs t
+ |-> (fn (ty, e) => pair (IVarE (v, ty) `|-> e))
+ end
| exprgen_term thy tabs (t as t1 $ t2) trns =
let
val (t', ts) = strip_comb t
@@ -925,7 +934,25 @@
val idf = idf_of_const thy tabs (c, ty);
in
trns
- |> gen_ensure_def [("wfrec", (K o succeed) Undef)] ("generating wfrec") idf
+ |> 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))
+ ||>> exprsgen_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 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
+ |> 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))
@@ -992,8 +1019,6 @@
fun mk_tabs thy =
let
- fun get_specifications thy c =
- Defs.specifications_of (Theory.defs_of thy) c;
fun extract_defs thy =
let
fun dest thm =
@@ -1027,56 +1052,39 @@
(fn (tyco, thyname) => InstNameMangler.declare thy (thyname, (cls, tyco))) clsinsts)
(ClassPackage.get_classtab thy)
|-> (fn _ => I);
- fun add_monoeq thy deftab (overltab1, overltab2) =
- let
- val c = "op =";
- val ty = Sign.the_const_type thy c;
- 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) [];
- val tys = map inst dtcos;
- in
- (overltab1
- |> Symtab.update_new (c, (ty, tys)),
- overltab2
- |> fold (fn ty' => ConstNameMangler.declare (thy, deftab)
- (c, (ty, ty')) #> snd) tys)
- end;
- (* über *alle*: (map fst o NameSpace.dest_table o Consts.space_of o Sign.consts_of) thy
- * (c, ty) reicht dann zur zünftigen Deklaration
- * somit fliegt ein Haufen Grusch raus, deftab bleibt allerdings wegen thyname
- fun mk_overltabs thy =
+ fun mk_overltabs thy =
(Symtab.empty, ConstNameMangler.empty)
|> Symtab.fold
- (fn c => if (is_none o ClassPackage.lookup_const_class thy) c
- then case get_specifications thy c
- of [_] => NONE
- | tys => fold
- (fn (overltab1, overltab2) => (
- overltab1
- |> Symtab.update_new (c, (Sign.the_const_type thy c, tys)),
- overltab2
- |> fold (fn (ty, (_, thyname)) => ConstNameMangler.declare (thy, deftab)
- (c, (Sign.the_const_type thy c, ty)) #> snd) tys))
- else I
- ) deftab
- |> add_monoeq thy deftab;*)
- fun mk_overltabs thy deftab =
- (Symtab.empty, ConstNameMangler.empty)
- |> Symtab.fold
- (fn (c, [_]) => I
- | (c, tytab) =>
- if (is_none o ClassPackage.lookup_const_class thy) c
- then (fn (overltab1, overltab2) => (
- overltab1
- |> Symtab.update_new (c, (Sign.the_const_type thy c, map fst tytab)),
- overltab2
- |> fold (fn (ty, (_, thyname)) => ConstNameMangler.declare (thy, deftab)
- (c, (Sign.the_const_type thy c, ty)) #> snd) tytab))
- else I
- ) deftab
- |> add_monoeq thy deftab;
+ (fn (c, _) =>
+ let
+ val deftab = Defs.specifications_of (Theory.defs_of thy) c
+ val is_overl = (is_none o ClassPackage.lookup_const_class thy) c
+ andalso case deftab
+ of [] => false
+ | [(ty, _)] => not (eq_typ thy (ty, Sign.the_const_type thy c))
+ | _ => true;
+ in if is_overl then (fn (overltab1, overltab2) => (
+ overltab1
+ |> Symtab.update_new (c, map fst deftab),
+ overltab2
+ |> fold_map (fn (ty, _) => ConstNameMangler.declare thy (c, ty)) deftab
+ |-> (fn _ => I))) else I
+ end) ((#2 o #constants o Consts.dest o #consts o Sign.rep_sg) thy)
+ |> (fn (overltab1, overltab2) =>
+ let
+ val c = "op =";
+ val ty = Sign.the_const_type thy c;
+ 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) [];
+ val tys = map inst dtcos;
+ in
+ (overltab1
+ |> Symtab.update_new (c, tys),
+ overltab2
+ |> fold (fn ty => ConstNameMangler.declare thy (c, ty) #> snd) tys)
+ end);
fun mk_dtcontab thy =
DatatypeconsNameMangler.empty
|> fold_map
@@ -1095,7 +1103,7 @@
(ClassPackage.get_classtab thy);
val deftab = extract_defs thy;
val insttab = mk_insttab thy;
- val overltabs = mk_overltabs thy deftab;
+ val overltabs = mk_overltabs thy;
val dtcontab = mk_dtcontab thy;
val clsmemtab = mk_clsmemtab thy;
in ((deftab, clsmemtab), (insttab, overltabs, dtcontab)) end;
@@ -1109,9 +1117,9 @@
map_codegen_data (fn (modl, gens, target_data, logic_data) =>
(f modl, gens, target_data, logic_data));
-fun expand_module init gen thy =
+fun expand_module init gen arg thy =
(#modl o CodegenData.get) thy
- |> start_transact init (gen thy (mk_tabs thy))
+ |> start_transact init (gen thy (mk_tabs thy) arg)
|-> (fn x:'a => fn modl => (x, map_module (K modl) thy));
fun rename_inconsistent thy =
@@ -1154,9 +1162,18 @@
fun codegen_incr t thy =
thy
|> `(#modl o CodegenData.get)
- ||>> expand_module NONE (fn thy => fn tabs => exprsgen_term thy tabs [t])
+ ||>> expand_module NONE exprsgen_term [t]
||>> `(#modl o CodegenData.get)
- |-> (fn ((modl_old, _), modl_new) => pair (CodegenThingol.diff_module (modl_new, modl_old)));
+ |-> (fn ((modl_old, [t]), modl_new) => pair (t, CodegenThingol.diff_module (modl_new, modl_old)));
+
+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;
fun get_ml_fun_datatype thy resolv =
let
@@ -1177,21 +1194,13 @@
fun read_typ thy =
Sign.read_typ (thy, K NONE);
-fun read_const thy (raw_c, raw_ty) =
- let
- val c = Sign.intern_const thy raw_c;
- val _ = if Sign.declared_const thy c
- then ()
- else error ("no such constant: " ^ quote c);
- val ty = case raw_ty
- of NONE => Sign.the_const_type thy c
- | SOME raw_ty => read_typ thy raw_ty;
- in (c, ty) end;
+fun read_const thy =
+ (dest_Const o Sign.read_term thy);
fun read_quote get reader gen raw thy =
thy
|> expand_module ((SOME o get) thy)
- (fn thy => fn tabs => (gen thy tabs o single o reader thy) raw)
+ (fn thy => fn tabs => gen thy tabs o single o reader thy) raw
|-> (fn [x] => pair x);
fun gen_add_prim prep_name prep_primdef raw_name (target, raw_primdef) thy =
@@ -1337,10 +1346,9 @@
fun generate_code (SOME raw_consts) thy =
let
val consts = map (read_const thy) raw_consts;
- fun generate thy tabs = fold_map (ensure_def_const thy tabs) consts
in
thy
- |> expand_module NONE generate
+ |> expand_module NONE (fold_map oo ensure_def_const) consts
|-> (fn cs => pair (SOME cs))
end
| generate_code NONE thy =
@@ -1381,7 +1389,7 @@
val generateP =
OuterSyntax.command generateK "generate executable code for constants" K.thy_decl (
- Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ))
+ Scan.repeat1 P.term
>> (fn raw_consts =>
Toplevel.theory (generate_code (SOME raw_consts) #> snd))
);
@@ -1389,7 +1397,7 @@
val serializeP =
OuterSyntax.command serializeK "serialize executable code for constants" K.thy_decl (
P.name
- -- Scan.option (Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)))
+ -- Scan.option (Scan.repeat1 P.term)
#-> (fn (target, raw_consts) =>
P.$$$ "("
|-- get_serializer target
@@ -1423,7 +1431,7 @@
val primconstP =
OuterSyntax.command primconstK "define target-lanugage specific constant" K.thy_decl (
- (P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
+ P.term
-- Scan.repeat1 (P.name -- P.text)
>> (fn (raw_const, primdefs) =>
(Toplevel.theory oo fold) (add_prim_const raw_const) primdefs)
@@ -1456,7 +1464,7 @@
val syntax_constP =
OuterSyntax.command syntax_constK "define code syntax for constant" K.thy_decl (
Scan.repeat1 (
- (P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
+ P.term
#-> (fn raw_const => Scan.repeat1 (
P.name -- parse_syntax_const raw_const
))
--- a/src/Pure/Tools/codegen_serializer.ML Sat Feb 25 15:11:35 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Sat Feb 25 15:19:00 2006 +0100
@@ -92,16 +92,19 @@
fun brackify_infix infx fxy_ctxt ps =
gen_brackify (eval_fxy (INFX infx) fxy_ctxt) (Pretty.breaks ps);
-fun from_app mk_app from_expr const_syntax fxy (c, es) =
+fun from_app mk_app from_expr const_syntax fxy ((c, ty), es) =
let
fun mk NONE es =
brackify fxy (mk_app c es)
| mk (SOME ((i, k), pr)) es =
- let
- val (es1, es2) = Library.chop k es;
- in
- brackify fxy (pr fxy from_expr es1 :: map (from_expr BR) es2)
- end;
+ (*if i <= length es then*)
+ let
+ val (es1, es2) = chop k es;
+ in
+ brackify fxy (pr fxy from_expr es1 :: map (from_expr BR) es2)
+ end
+ (*else
+ error ("illegal const_syntax")*)
in mk (const_syntax c) es end;
fun fillin_mixfix fxy_this ms fxy_ctxt pr args =
@@ -253,7 +256,6 @@
module
|> debug 3 (fn _ => "selecting submodule...")
|> (if is_some select then (partof o the) select else I)
- |> tap (Pretty.writeln o pretty_deps)
|> debug 3 (fn _ => "preprocessing...")
|> preprocess
|> debug 3 (fn _ => "serializing...")
@@ -477,16 +479,17 @@
| ml_from_expr _ e =
error ("dubious expression: " ^ (Pretty.output o pretty_iexpr) e)
and ml_mk_app f es =
- if is_cons f andalso length es > 1
- then
+ if is_cons f andalso length es > 1 then
[(str o resolv) f, Pretty.enum "," "(" ")" (map (ml_from_expr BR) es)]
+ else if has_nsp f "mem" then
+ Pretty.block [str "#", ml_from_label f] :: map (ml_from_expr BR) es
else
(str o resolv) f :: map (ml_from_expr BR) es
and ml_from_app fxy (((c, ty), lss), es) =
case map (ml_from_sortlookup BR) lss
of [] =>
let
- val p = from_app ml_mk_app ml_from_expr const_syntax fxy (c, es)
+ val p = from_app ml_mk_app ml_from_expr const_syntax fxy ((c, ty), es)
in if needs_type ty
then
Pretty.enclose "(" ")" [
@@ -525,15 +528,28 @@
if mk_definer pats = definer
then SOME definer
else error ("mixing simultaneous vals and funs not implemented")
+ fun mk_class v class =
+ str (prefix "'" v ^ " " ^ resolv class)
+ fun from_tyvar (v, sort) =
+ Pretty.block [
+ str "(",
+ str v,
+ str ":",
+ case sort
+ of [class] => mk_class v class
+ | _ => Pretty.enum " *" "" "" (map (mk_class v) sort),
+ str ")"
+ ];
fun mk_fun definer (name, (eqs as eq::eq_tl, (sortctxt, ty))) =
let
- val shift = if null eq_tl then I else map (Pretty.block o single);
+ val shift = if null eq_tl then I else
+ map (Pretty.block o single o Pretty.block o single);
fun mk_eq definer (pats, expr) =
(Pretty.block o Pretty.breaks) (
[str definer, (str o resolv) name]
@ (if null pats
then [str ":", ml_from_type NOBR ty]
- else map (str o fst) sortctxt @ map (ml_from_expr BR) pats)
+ else map from_tyvar sortctxt @ map (ml_from_expr BR) pats)
@ [str "=", ml_from_expr NOBR expr]
)
in
@@ -553,13 +569,12 @@
fun mk_cons (co, []) =
str (resolv co)
| mk_cons (co, tys) =
- Pretty.block (
- str (resolv co)
- :: str " of"
- :: Pretty.brk 1
- :: separate (Pretty.block [str " *", Pretty.brk 1])
- (map (ml_from_type NOBR) tys)
- )
+ Pretty.block [
+ str (resolv co),
+ str " of",
+ Pretty.brk 1,
+ Pretty.enum " *" "" "" (map (ml_from_type NOBR) tys)
+ ]
fun mk_datatype definer (t, (vs, cs)) =
(Pretty.block o Pretty.breaks) (
str definer
@@ -589,6 +604,54 @@
| (name, Datatypecons _) => NONE
| (name, def) => error ("datatype block containing illegal def: "
^ (Pretty.output o pretty_def) def));
+ fun filter_class defs =
+ case List.mapPartial
+ (fn (name, Class info) => SOME (name, info)
+ | (name, Classmember _) => NONE
+ | (name, def) => error ("class block containing illegal def: "
+ ^ (Pretty.output o pretty_def) def)) defs
+ of [class] => class
+ | _ => error ("class block without class: " ^ (commas o map (quote o fst)) defs)
+ fun ml_from_class (name, (supclasses, (v, membrs))) =
+ let
+ fun from_supclass class =
+ Pretty.block [
+ ml_from_label class,
+ str ":",
+ Pretty.brk 1,
+ str ("'" ^ v),
+ Pretty.brk 1,
+ (str o resolv) class
+ ];
+ fun from_membr (m, (_, ty)) =
+ Pretty.block [
+ ml_from_label m,
+ str ":",
+ Pretty.brk 1,
+ ml_from_type NOBR ty
+ ];
+ fun from_membr_fun (m, _) =
+ (Pretty.block o Pretty.breaks) [
+ str "fun",
+ (str o resolv) m,
+ Pretty.enclose "(" ")" [str (v ^ ":'" ^ v ^ " " ^ resolv name)],
+ str "=",
+ Pretty.block [str "#", ml_from_label m],
+ str (v ^ ";")
+ ];
+ in
+ Pretty.chunks (
+ (Pretty.block o Pretty.breaks) [
+ str "type",
+ str ("'" ^ v),
+ (str o resolv) name,
+ str "=",
+ Pretty.enum "," "{" "};" (
+ map from_supclass supclasses @ map from_membr membrs
+ )
+ ]
+ :: map from_membr_fun membrs)
+ end
fun ml_from_def (name, Undef) =
error ("empty definition during serialization: " ^ quote name)
| ml_from_def (name, Prim prim) =
@@ -605,59 +668,23 @@
str ";"
]
) |> SOME
- | ml_from_def (name, Class (supclasses, (v, membrs))) =
- let
- val pv = str ("'" ^ v);
- fun from_supclass class =
- Pretty.block [
- ml_from_label class,
- str ":",
- Pretty.brk 1,
- pv,
- Pretty.brk 1,
- (str o resolv) class
- ]
- fun from_membr (m, (_, ty)) =
- Pretty.block [
- ml_from_label m,
- str ":",
- Pretty.brk 1,
- ml_from_type NOBR ty
- ]
- in
- Pretty.block [
- str "type",
- Pretty.brk 1,
- pv,
- Pretty.brk 1,
- (str o resolv) name,
- Pretty.brk 1,
- str "=",
- Pretty.brk 1,
- Pretty.enum "," "{" "};" (
- map from_supclass supclasses @ map from_membr membrs
- )
- ] |> SOME
- end
- | ml_from_def (_, Classmember _) =
- NONE
| ml_from_def (name, Classinst (((class, (tyco, arity)), suparities), memdefs)) =
let
val definer = if null arity then "val" else "fun"
- fun from_supclass (supclass, lss) =
+ fun from_supclass (supclass, (supinst, lss)) =
(Pretty.block o Pretty.breaks) (
ml_from_label supclass
:: str "="
+ :: (str o resolv) supinst
:: map (ml_from_sortlookup NOBR) lss
);
- fun from_memdef (m, def) =
- (ml_from_funs [(m, def)], Pretty.block [
- ml_from_label m,
- Pretty.brk 1,
- str "=",
- Pretty.brk 1,
- (str o resolv) m
- ]);
+ fun from_memdef (m, (_, def)) =
+ (ml_from_funs [(m, def)], (Pretty.block o Pretty.breaks) (
+ ml_from_label m
+ :: str "="
+ :: (str o resolv) m
+ :: map (str o fst) arity
+ ));
fun mk_memdefs supclassexprs [] =
Pretty.enum "," "{" "};" (
supclassexprs
@@ -669,7 +696,7 @@
Pretty.chunks [
[str ("let"), Pretty.fbrk, defs |> Pretty.chunks]
|> Pretty.block,
- [str ("in "), Pretty.enum "," "{" "};" (supclassexprs @ assigns)]
+ [str ("in "), Pretty.enum "," "{" "} end;" (supclassexprs @ assigns)]
|> Pretty.block
]
end;
@@ -690,7 +717,10 @@
of (_, Fun _)::_ => (SOME o ml_from_funs o map (fn (name, Fun info) => (name, info))) defs
| (_, Datatypecons _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs
| (_, Datatype _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs
+ | (_, Class _)::_ => (SOME o ml_from_class o filter_class) defs
+ | (_, Classmember _)::_ => (SOME o ml_from_class o filter_class) defs
| [def] => ml_from_def def
+ | defs => error ("illegal mutual dependencies: " ^ (commas o map fst) defs)
end;
fun ml_annotators (nsp_dtcon, nsp_class, is_int_tyco) =
@@ -708,7 +738,7 @@
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", "o"
+ "bool", "int", "list", "true", "false", "not", "o"
];
fun ml_from_module _ ((_, name), ps) =
Pretty.chunks ([
@@ -735,7 +765,6 @@
else 0;
fun preprocess const_syntax module =
module
- |> tap (Pretty.writeln o pretty_deps)
|> debug 3 (fn _ => "eta-expanding...")
|> eta_expand (eta_expander module const_syntax)
|> debug 3 (fn _ => "eta-expanding polydefs...")
@@ -871,8 +900,8 @@
] end
and hs_mk_app c es =
(str o resolv) c :: map (hs_from_expr BR) es
- and hs_from_app fxy (((c, _), ls), es) =
- from_app hs_mk_app hs_from_expr const_syntax fxy (c, es);
+ and hs_from_app fxy (((c, ty), ls), es) =
+ from_app hs_mk_app hs_from_expr const_syntax fxy ((c, ty), es);
fun hs_from_funeqs (name, eqs) =
let
fun from_eq name (args, rhs) =
@@ -959,7 +988,7 @@
hs_from_sctxt_tycoexpr (arity, (tyco, map (IVarT o rpair [] o fst) arity)),
str " where",
Pretty.fbrk,
- Pretty.chunks (map (fn (m, (eqs, _)) => hs_from_funeqs (m, eqs)) memdefs)
+ Pretty.chunks (map (fn (m, (_, (eqs, _))) => hs_from_funeqs (m, eqs)) memdefs)
] |> SOME
in
case List.mapPartial (fn (name, def) => hs_from_def (name, def)) defs
@@ -1000,7 +1029,6 @@
|> the_default 0;
fun preprocess const_syntax module =
module
- |> tap (Pretty.writeln o pretty_deps)
|> debug 3 (fn _ => "eta-expanding...")
|> eta_expand (eta_expander const_syntax)
in
--- a/src/Pure/Tools/codegen_thingol.ML Sat Feb 25 15:11:35 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Sat Feb 25 15:19:00 2006 +0100
@@ -5,7 +5,7 @@
Intermediate language ("Thin-gol") for code extraction.
*)
-signature CODEGEN_THINGOL =
+signature BASIC_CODEGEN_THINGOL =
sig
type vname = string;
datatype classlookup = Instance of string * classlookup list list
@@ -20,6 +20,11 @@
| IApp of iexpr * iexpr
| IAbs of iexpr * iexpr
| ICase of iexpr * (iexpr * iexpr) list;
+end;
+
+signature CODEGEN_THINGOL =
+sig
+ include BASIC_CODEGEN_THINGOL;
val mk_funs: itype list * itype -> itype;
val mk_apps: iexpr * iexpr list -> iexpr;
val mk_abss: iexpr list * iexpr -> iexpr;
@@ -59,12 +64,11 @@
| 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)
- * (string * funn) list;
+ * (class * (string * classlookup list list)) list)
+ * (string * (string * funn)) list;
type module;
type transact;
type 'dst transact_fin;
- type gen_defgen = string -> transact -> def transact_fin;
val pretty_def: def -> Pretty.T;
val pretty_module: module -> Pretty.T;
val pretty_deps: module -> Pretty.T;
@@ -78,7 +82,7 @@
val has_nsp: string -> string -> bool;
val succeed: 'a -> transact -> 'a transact_fin;
val fail: string -> transact -> 'a transact_fin;
- val gen_ensure_def: (string * gen_defgen) list -> string
+ val ensure_def: (string * (string -> transact -> def transact_fin)) list -> string
-> string -> transact -> transact;
val start_transact: string option -> (transact -> 'a * transact) -> module -> 'a * module;
@@ -397,15 +401,14 @@
| 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)
- * (string * funn) list;
+ * (class * (string * classlookup list list)) list)
+ * (string * (string * funn)) list;
datatype node = Def of def | Module of node Graph.T;
type module = node Graph.T;
type transact = Graph.key option * module;
datatype 'dst transact_res = Succeed of 'dst | Fail of string list * exn option;
type 'dst transact_fin = 'dst transact_res * module;
-type gen_defgen = string -> transact -> def transact_fin;
exception FAIL of string list * exn option;
val eq_def = (op =);
@@ -611,12 +614,12 @@
modl
|> fold add_dep ([] |> fold_defs (append o f) modl);
-fun ensure_def (name, Undef) module =
+fun add_def_incr (name, Undef) module =
(case try (get_def module) name
of NONE => (error "attempted to add Undef to module")
| SOME Undef => (error "attempted to add Undef to module")
| SOME def' => map_def name (K def') module)
- | ensure_def (name, def) module =
+ | add_def_incr (name, def) module =
(case try (get_def module) name
of NONE => add_def (name, def) module
| SOME Undef => map_def name (K def) module
@@ -776,16 +779,16 @@
fun mk_memdef (m, (ctxt, ty)) =
case AList.lookup (op =) memdefs m
of NONE => error ("missing definition for member " ^ quote m)
- | SOME (eqs, (ctxt', ty')) =>
+ | SOME (m', (eqs, (ctxt', ty'))) =>
if eq_itype (instant_itype (instant (v, tyco `%% map IVarT arity)) ty, ty')
- then (m, (check_funeqs eqs, (ctxt', ty')))
+ then (m, (m', (check_funeqs eqs, (ctxt', ty'))))
else error ("inconsistent type for member definition " ^ quote m)
in Classinst (d, map mk_memdef membrs) end;
fun postprocess_def (name, Datatype (_, constrs)) =
(check_samemodule (name :: map fst constrs);
fold (fn (co, _) =>
- ensure_def (co, Datatypecons name)
+ add_def_incr (co, Datatypecons name)
#> add_dep (co, name)
#> add_dep (name, co)
) constrs
@@ -793,7 +796,7 @@
| postprocess_def (name, Class (_, (_, membrs))) =
(check_samemodule (name :: map fst membrs);
fold (fn (m, _) =>
- ensure_def (m, Classmember name)
+ add_def_incr (m, Classmember name)
#> add_dep (m, name)
#> add_dep (name, m)
) membrs
@@ -835,7 +838,7 @@
end;
in select [] gens end;
-fun gen_ensure_def defgens msg name (dep, modl) =
+fun ensure_def defgens msg name (dep, modl) =
let
val msg' = case dep
of NONE => msg
@@ -866,7 +869,7 @@
debug 10 (fn _ => "addition of " ^ name
^ " := " ^ (Pretty.output o pretty_def) def)
#> debug 10 (fn _ => "adding")
- #> ensure_def (name, def)
+ #> add_def_incr (name, def)
#> debug 10 (fn _ => "postprocessing")
#> postprocess_def (name, def)
#> debug 10 (fn _ => "adding done")
@@ -914,7 +917,7 @@
val add_vars =
map2 (curry IVarE) (Term.invent_names (fold expr_names es []) "x" add_n) tys;
in
- add_vars `|--> IConst ((f, ty), ls) `$$ es `$$ add_vars
+ add_vars `|--> IConst ((f, ty), ls) `$$ map eta es `$$ add_vars
end
| NONE => map_iexpr eta e;
in (map_defs o map_def_fun o map_def_fun_expr) eta end;
@@ -1069,3 +1072,5 @@
end;
end; (* struct *)
+
+structure BasicCodegenThingol: BASIC_CODEGEN_THINGOL = CodegenThingol;
\ No newline at end of file