--- a/src/Pure/Tools/class_package.ML Fri Feb 03 11:47:57 2006 +0100
+++ b/src/Pure/Tools/class_package.ML Fri Feb 03 11:48:11 2006 +0100
@@ -151,7 +151,7 @@
local
-fun gen_add_class add_locale prep_class bname raw_supclasses raw_body thy =
+fun gen_add_class add_locale prep_class do_proof bname raw_supclasses raw_body thy =
let
val supclasses = map (prep_class thy) raw_supclasses;
fun get_allcs class =
@@ -170,46 +170,39 @@
supclasses;
fun mk_c_lookup c_global supcs c_adds =
map2 (fn ((c, _), _) => pair c) c_global supcs @ c_adds
- fun extract_assumes v c_lookup elems =
- elems
- |> (map o List.mapPartial)
- (fn (Element.Assumes asms) => (SOME o map (map fst o snd)) asms
- | _ => NONE)
- |> Library.flat o Library.flat o Library.flat
+ fun extract_tyvar_consts thy name_locale =
+ let
+ fun extract_tyvar_name thy tys =
+ fold (curry add_typ_tfrees) tys []
+ |> (fn [(v, sort)] =>
+ if Sorts.sort_le (Sign.classes_of thy) (swap (sort, supsort))
+ then v
+ else error ("illegal sort constraint on class type variable: " ^ Sign.string_of_sort thy sort)
+ | [] => error ("no class type variable")
+ | vs => error ("more than one type variable: " ^ (commas o map (Sign.string_of_typ thy o TFree)) vs))
+ val raw_consts =
+ Locale.parameters_of thy name_locale
+ |> map (apsnd Syntax.unlocalize_mixfix)
+ |> ((curry splitAt o length) supcs);
+ val v = (extract_tyvar_name thy o map (snd o fst) o op @) raw_consts;
+ fun subst_ty cs =
+ map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) cs;
+ val consts = (subst_ty (fst raw_consts), subst_ty (snd raw_consts));
+ val _ = (writeln o commas o map (fst o fst)) (fst consts);
+ val _ = (writeln o commas o map (fst o fst)) (snd consts);
+ in (v, consts) end;
+ fun add_global_const v ((c, ty), syn) thy =
+ thy
+ |> Sign.add_consts_i [(c, ty |> subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)]
+ |> `(fn thy => (c, (Sign.intern_const thy c |> print, ty)))
+ fun extract_assumes thy name_locale c_lookup =
+ Locale.local_asms_of thy name_locale
+ |> map snd
+ |> Library.flat
|> (map o map_aterms) (fn Free (c, ty) => Const ((fst o the o AList.lookup (op =) c_lookup) c, ty)
| t => t)
|> tap (fn ts => writeln ("(1) axclass axioms: " ^
(commas o map (Sign.string_of_term thy)) ts));
- fun extract_tyvar_name thy tys =
- fold (curry add_typ_tfrees) tys []
- |> (fn [(v, sort)] =>
- if Sorts.sort_le (Sign.classes_of thy) (swap (sort, supsort))
- then v
- else error ("illegal sort constraint on class type variable: " ^ Sign.string_of_sort thy sort)
- | [] => error ("no class type variable")
- | vs => error ("more than one type variable: " ^ (commas o map (Sign.string_of_typ thy o TFree)) vs))
- fun extract_tyvar_consts thy (import_elems, body_elems) =
- let
- fun get_elems elems =
- elems
- |> Library.flat
- |> List.mapPartial
- (fn (Element.Fixes consts) => SOME consts
- | _ => NONE)
- |> Library.flat
- |> map (fn (c, ty, syn) => ((c, the ty), Syntax.unlocalize_mixfix syn))
- val import_consts = get_elems import_elems;
- val body_consts = get_elems body_elems;
- val v = extract_tyvar_name thy (map (snd o fst) (import_consts @ body_consts));
- fun subst_ty cs =
- map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) cs;
- val import_cs = subst_ty import_consts;
- val body_cs = subst_ty body_consts;
- in (v, (import_cs, body_cs)) end;
- fun add_global_const v ((c, ty), syn) thy =
- thy
- |> Sign.add_consts_i [(c, ty |> subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)]
- |> `(fn thy => (c, (Sign.intern_const thy c, ty)))
fun add_global_constraint v class (_, (c, ty)) thy =
thy
|> Sign.add_const_constraint_i (c, subst_clsvar v (TVar ((v, 0), [class])) ty);
@@ -217,36 +210,37 @@
thy
|> Locale.interpretation (NameSpace.base name_locale, [])
(Locale.Locale name_locale) (map (SOME o fst) cs)
- |> Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE);
- fun print_ctxt ctxt elem =
- map Pretty.writeln (Element.pretty_ctxt ctxt elem)
+ |> do_proof ax_axioms;
in
thy
|> add_locale bname locexpr raw_body
- |-> (fn ((import_elems, body_elems), ctxt) =>
+ |-> (fn ctxt =>
`(fn thy => Locale.intern thy bname)
#-> (fn name_locale =>
- `(fn thy => extract_tyvar_consts thy (import_elems, body_elems))
+ `(fn thy => extract_tyvar_consts thy name_locale)
#-> (fn (v, (c_global, c_defs)) =>
fold_map (add_global_const v) c_defs
#-> (fn c_adds =>
- AxClass.add_axclass_i (bname, supsort)
- (map (Thm.no_attributes o pair "") (extract_assumes v (mk_c_lookup c_global supcs c_adds) body_elems))
+ `(fn thy => extract_assumes thy name_locale (mk_c_lookup c_global supcs c_adds))
+ #-> (fn assumes =>
+ AxClass.add_axclass_i (bname, supsort) (map (Thm.no_attributes o pair "") assumes))
#-> (fn { axioms = ax_axioms : thm list, ...} =>
`(fn thy => Sign.intern_class thy bname)
#-> (fn name_axclass =>
fold (add_global_constraint v name_axclass) c_adds
#> add_class_data (name_locale, (supclasses, name_locale, name_axclass, v, map snd c_adds))
- #> tap (fn _ => (map o map) (print_ctxt ctxt) import_elems)
- #> tap (fn _ => (map o map) (print_ctxt ctxt) body_elems)
#> interpret name_locale (supcs @ (map (fn ((c, ty), _) => (Sign.intern_const thy c, ty)) c_defs)) ax_axioms
))))))
end;
in
-val add_class = gen_add_class (Locale.add_locale_context true) intern_class;
-val add_class_i = gen_add_class (Locale.add_locale_context_i true) certify_class;
+val add_class = gen_add_class (Locale.add_locale true) intern_class
+ (fn ax_axioms => Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE));
+val add_class_i = gen_add_class (Locale.add_locale_i true) certify_class
+ (fn ax_axioms => Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE));
+val add_class_exp = gen_add_class (Locale.add_locale true) intern_class
+ (K I);
end; (* local *)
@@ -271,9 +265,10 @@
|> Sign.add_const_constraint_i (c, ty2)
|> pair (c, ty1)
end;
- fun get_c_given thy = map (fst o dest_def o snd o tap_def thy o fst) raw_defs;
- fun check_defs c_given c_req thy =
+ fun check_defs raw_defs c_req thy =
let
+ val thy' = Sign.add_arities_i [(tyco, asorts, sort)] thy;
+ val c_given = map (fst o dest_def o snd o tap_def thy' o fst) raw_defs;
fun eq_c ((c1, ty1), (c2, ty2)) =
let
val ty1' = Type.varifyT ty1;
@@ -297,12 +292,18 @@
#> fold (fn class => add_inst_data (class, (tyco, Context.theory_name thy))) sort;
in
thy
+ |> tap (fn thy => check_defs raw_defs c_req thy)
|> fold_map get_remove_contraint (map fst c_req)
- ||> tap (fn thy => check_defs (get_c_given thy) c_req thy)
||> add_defs (true, raw_defs)
|-> (fn cs => AxClass.instance_arity_i (after_qed cs) arity)
end;
+val _ : string option ->
+ ((string * typ option * mixfix) option * ((string * Attrib.src list) * term)) list ->
+ theory -> (term * (bstring * thm)) list * (Proof.context * theory)
+ = Specification.definition_i;
+
+
val add_instance_arity = fn x => gen_instance_arity (AxClass.read_arity) IsarThy.add_defs read_axm x;
val add_instance_arity_i = fn x => gen_instance_arity (AxClass.cert_arity) IsarThy.add_defs_i (K I) x;
@@ -521,6 +522,14 @@
>> (Toplevel.theory_context
o (fn ((bname, supclasses), elems) => add_class bname supclasses elems)));
+val classP_exp =
+ OuterSyntax.command (classK ^ "_exp") "operational type classes" K.thy_goal (
+ P.name --| P.$$$ "="
+ -- Scan.optional (Scan.repeat1 (P.name --| P.$$$ "+")) []
+ -- Scan.optional (P.!!! (Scan.repeat1 P.context_element)) []
+ >> (Toplevel.theory_to_proof
+ o (fn ((bname, supclasses), elems) => add_class_exp bname supclasses elems)));
+
val instanceP =
OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> AxClass.instance_subclass
@@ -529,7 +538,7 @@
| (inst, defs) => add_instance_arity inst defs)
) >> (Toplevel.print oo Toplevel.theory_to_proof));
-val _ = OuterSyntax.add_parsers [classP, instanceP];
+val _ = OuterSyntax.add_parsers [classP, classP_exp, instanceP];
end; (* local *)
--- a/src/Pure/Tools/codegen_package.ML Fri Feb 03 11:47:57 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML Fri Feb 03 11:48:11 2006 +0100
@@ -505,19 +505,19 @@
let
fun add_rename (var as ((v, _), sort)) used =
let
- val v' = variant used v
+ val v' = "'" ^ variant used (unprefix "'" v)
in (((var, TFree (v', sort)), (v', TVar var)), v' :: used) end;
fun typ_names (Type (tyco, tys)) (vars, names) =
(vars, names |> insert (op =) (NameSpace.base tyco))
|> fold typ_names tys
| typ_names (TFree (v, _)) (vars, names) =
- (vars, names |> insert (op =) v)
- | typ_names (TVar (v, sort)) (vars, names) =
- (vars |> AList.update (op =) (v, sort), names);
+ (vars, names |> insert (op =) (unprefix "'" v))
+ | typ_names (TVar (vi, sort)) (vars, names) =
+ (vars |> AList.update (op =) (vi, sort), names);
val (vars, used) = fold typ_names tys ([], []);
val (renames, reverse) = fold_map add_rename vars used |> fst |> split_list;
in
- (reverse, (map o map_atyps) (Term.instantiateT renames) tys)
+ (reverse, map (Term.instantiateT renames) tys)
end;
fun burrow_typs_yield f ts =
@@ -553,7 +553,7 @@
val (vars, used) = fold term_names ts ([], []);
val (renames, reverse) = fold_map add_rename vars used |> fst |> split_list;
in
- (reverse, (map o map_aterms) (Term.instantiate ([], renames)) ts)
+ (reverse, map (Term.instantiate ([], renames)) ts)
end;
fun devarify_term_typs ts =
--- a/src/Pure/Tools/codegen_serializer.ML Fri Feb 03 11:47:57 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Fri Feb 03 11:48:11 2006 +0100
@@ -404,11 +404,11 @@
(case tyco_syntax tyco
of NONE =>
let
- val f' = (str o resolv) tyco
+ val tyco' = (str o resolv) tyco
in case map (ml_from_type BR) tys
- of [] => f'
- | [p] => Pretty.block [p, Pretty.brk 1, f']
- | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, f']
+ of [] => tyco'
+ | [p] => Pretty.block [p, Pretty.brk 1, tyco']
+ | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
end
| SOME ((i, k), pr) =>
if not (i <= length tys andalso length tys <= k)
@@ -442,8 +442,16 @@
])
| ml_from_expr fxy (e as IConst x) =
ml_from_app fxy (x, [])
- | ml_from_expr fxy (IVarE (v, _)) =
- str v
+ | ml_from_expr fxy (IVarE (v, ty)) =
+ if needs_type ty
+ then
+ Pretty.enclose "(" ")" [
+ str v,
+ str ":",
+ ml_from_type NOBR ty
+ ]
+ else
+ str v
| ml_from_expr fxy (IAbs ((v, _), e)) =
brackify fxy [
str ("fn " ^ v ^ " =>"),
@@ -537,7 +545,7 @@
fun ml_from_datatypes defs =
let
val defs' = List.mapPartial
- (fn (name, Datatype info) => SOME (resolv name, info)
+ (fn (name, Datatype info) => SOME (name, info)
| (name, Datatypecons _) => NONE
| (name, def) => error ("datatype block containing illegal def: "
^ (Pretty.output o pretty_def) def)
@@ -563,7 +571,7 @@
case defs'
of (def::defs_tl) =>
chunk_defs (
- mk_datatype "datatype " def
+ mk_datatype "datatype" def
:: map (mk_datatype "and ") defs_tl
) |> SOME
| _ => NONE
@@ -877,7 +885,7 @@
| hs_from_def (name, Fun (eqs, (sctxt, ty))) =
Pretty.chunks [
Pretty.block [
- (str o lower_first o resolv) (name ^ " ::"),
+ (str o suffix " ::" o lower_first o resolv) name,
Pretty.brk 1,
hs_from_sctxt_type (sctxt, ty)
],
--- a/src/Pure/Tools/codegen_thingol.ML Fri Feb 03 11:47:57 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Fri Feb 03 11:48:11 2006 +0100
@@ -1044,27 +1044,20 @@
([], SOME tab)
| get_path_name [p] tab =
let
- val _ = writeln ("(1) " ^ p);
val SOME (N (p', tab')) = Symtab.lookup tab p
in ([p'], tab') end
| get_path_name [p1, p2] tab =
- let
- val _ = (writeln o prefix "(2) " o NameSpace.pack) [p1, p2];
- in case Symtab.lookup tab p1
+ case Symtab.lookup tab p1
of SOME (N (p', SOME tab')) =>
let
- val _ = writeln ("(2) 'twas a module");
val (ps', tab'') = get_path_name [p2] tab'
in (p' :: ps', tab'') end
| NONE =>
let
- val _ = writeln ("(2) 'twas a definition");
val SOME (N (p', NONE)) = Symtab.lookup tab (NameSpace.pack [p1, p2])
in ([p'], NONE) end
- end
| get_path_name (p::ps) tab =
let
- val _ = (writeln o prefix "(3) " o commas) (p::ps);
val SOME (N (p', SOME tab')) = Symtab.lookup tab p
val (ps', tab'') = get_path_name ps tab'
in (p' :: ps', tab'') end;
@@ -1072,107 +1065,18 @@
if (is_some o Int.fromString) name
then name
else let
- val _ = writeln ("(0) prefix: " ^ commas prefix);
- val _ = writeln ("(0) name: " ^ name)
val (common, (_, rem)) = get_prefix (op =) (prefix, NameSpace.unpack name);
- val _ = writeln ("(0) common: " ^ commas common);
- val _ = writeln ("(0) rem: " ^ commas rem);
val (_, SOME tab') = get_path_name common tab;
val (name', _) = get_path_name rem tab';
in NameSpace.pack name' end;
in deresolv (mk module (AList.make (K NameMangler.empty) nsp_conn) Symtab.empty) end;
-val _ : module -> string list list -> (string * string -> string) -> (string -> string option) -> string list -> string -> string = mk_deresolver;
-
-fun mk_resolvtab' nsp_conn validate module =
- let
- fun validate' n = perhaps validate n;
- fun ensure_unique prfix prfix' name name' (locals, tab) =
- let
- fun uniquify name n =
- let
- val name' = if n = 0 then name else name ^ "_" ^ string_of_int n
- in
- if member (op =) locals name'
- then uniquify name (n+1)
- else case validate name
- of NONE => name'
- | SOME name' => uniquify name' n
- end;
- val name'' = uniquify name' 0;
- in
- (locals, tab)
- |> apsnd (Symtab.update_new
- (NameSpace.pack (prfix @ [name]), NameSpace.pack (prfix' @ [name''])))
- |> apfst (cons name'')
- |> pair name''
- end;
- fun fill_in prfix prfix' node tab =
- let
- val keys = Graph.keys node;
- val nodes = AList.make (Graph.get_node node) keys;
- val (mods, defs) =
- nodes
- |> List.partition (fn (_, Module _) => true | _ => false)
- |> apfst (map (fn (name, Module m) => (name, m)))
- |> apsnd (map fst)
- fun modl_validate (name, modl) (locals, tab) =
- (locals, tab)
- |> ensure_unique prfix prfix' name name
- |-> (fn name' => apsnd (fill_in (prfix @ [name]) (prfix @ [name']) modl))
- fun ensure_unique_sidf sidf =
- let
- val [shallow, name] = NameSpace.unpack sidf;
- in
- nsp_conn
- |> get_first
- (fn grp => if member (op =) grp shallow
- then grp |> remove (op =) shallow |> SOME else NONE)
- |> these
- |> map (fn s => NameSpace.pack [s, name])
- |> exists (member (op =) defs)
- |> (fn b => if b then sidf else name)
- end;
- fun def_validate sidf (locals, tab) =
- (locals, tab)
- |> ensure_unique prfix prfix' sidf (ensure_unique_sidf sidf)
- |> snd
- in
- ([], tab)
- |> fold modl_validate mods
- |> fold def_validate defs
- |> snd
- end;
- in
- Symtab.empty
- |> fill_in [] [] module
- end;
-
-fun mk_resolv tab =
- let
- fun resolver modl name =
- if NameSpace.is_qualified name then
- let
- val _ = debug 12 (fn name' => "resolving " ^ quote name ^ " in "
- ^ (quote o NameSpace.pack) modl) ();
- val modl' = if null modl then [] else
- (NameSpace.unpack o the o Symtab.lookup tab o NameSpace.pack) modl;
- val name' = (NameSpace.unpack o the o Symtab.lookup tab) name
- in
- (NameSpace.pack o snd o snd o get_prefix (op =)) (modl', name')
- |> debug 12 (fn name' => "resolving " ^ quote name ^ " to "
- ^ quote name' ^ " in " ^ (quote o NameSpace.pack) modl)
- end
- else name
- in resolver end;
-
(* serialization *)
fun serialize seri_defs seri_module validate nsp_conn name_root module =
let
val resolver = mk_deresolver module nsp_conn snd validate;
-(* val resolver = mk_resolv (mk_resolvtab' nsp_conn validate module); *)
fun mk_name prfx name =
let
val name_qual = NameSpace.pack (prfx @ [name])