--- a/src/Pure/axclass.ML Wed Jun 02 10:50:53 2010 +0200
+++ b/src/Pure/axclass.ML Wed Jun 02 10:51:55 2010 +0200
@@ -412,17 +412,15 @@
(* primitive rules *)
-fun gen_add_classrel store raw_th thy =
+fun add_classrel raw_th thy =
let
val th = Thm.strip_shyps (Thm.transfer thy raw_th);
val prop = Thm.plain_prop_of th;
fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
val rel = Logic.dest_classrel prop handle TERM _ => err ();
val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
- val (th', thy') =
- if store then PureThy.store_thm
- (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy
- else (th, thy);
+ val (th', thy') = PureThy.store_thm
+ (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy;
val th'' = th'
|> Thm.unconstrainT
|> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
@@ -433,17 +431,15 @@
|> perhaps complete_arities
end;
-fun gen_add_arity store raw_th thy =
+fun add_arity raw_th thy =
let
val th = Thm.strip_shyps (Thm.transfer thy raw_th);
val prop = Thm.plain_prop_of th;
fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
- val (th', thy') =
- if store then PureThy.store_thm
- (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy
- else (th, thy);
+ val (th', thy') = PureThy.store_thm
+ (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
val args = Name.names Name.context Name.aT Ss;
val T = Type (t, map TFree args);
@@ -463,9 +459,6 @@
|> put_arity ((t, Ss, c), th'')
end;
-val add_classrel = gen_add_classrel true;
-val add_arity = gen_add_arity true;
-
(* tactical proofs *)
@@ -477,10 +470,7 @@
cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
quote (Syntax.string_of_classrel ctxt [c1, c2]));
in
- thy
- |> PureThy.add_thms [((Binding.name
- (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])]
- |-> (fn [th'] => gen_add_classrel false th')
+ thy |> add_classrel th
end;
fun prove_arity raw_arity tac thy =
@@ -494,9 +484,7 @@
cat_error msg ("The error(s) above occurred while trying to prove type arity " ^
quote (Syntax.string_of_arity ctxt arity));
in
- thy
- |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths))
- |-> fold (gen_add_arity false)
+ thy |> fold add_arity ths
end;
@@ -613,10 +601,6 @@
local
(*old-style axioms*)
-fun add_axiom (b, prop) =
- Thm.add_axiom (b, prop) #->
- (fn (_, thm) => PureThy.add_thm ((b, Drule.export_without_context thm), []));
-
fun axiomatize prep mk name add raw_args thy =
let
val args = prep thy raw_args;
@@ -624,17 +608,17 @@
val names = name args;
in
thy
- |> fold_map add_axiom (map Binding.name names ~~ specs)
- |-> fold add
+ |> fold_map Thm.add_axiom (map Binding.name names ~~ specs)
+ |-> fold (add o Drule.export_without_context o snd)
end;
fun ax_classrel prep =
axiomatize (map o prep) (map Logic.mk_classrel)
- (map (prefix classrel_prefix o Logic.name_classrel)) (gen_add_classrel false);
+ (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
fun ax_arity prep =
axiomatize (prep o ProofContext.init_global) Logic.mk_arities
- (map (prefix arity_prefix) o Logic.name_arities) (gen_add_arity false);
+ (map (prefix arity_prefix) o Logic.name_arities) add_arity;
fun class_const c =
(Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);
--- a/src/Pure/display.ML Wed Jun 02 10:50:53 2010 +0200
+++ b/src/Pure/display.ML Wed Jun 02 10:51:55 2010 +0200
@@ -129,7 +129,7 @@
fun prt_cls c = Syntax.pretty_sort ctxt [c];
fun prt_sort S = Syntax.pretty_sort ctxt S;
- fun prt_arity t (c, (_, Ss)) = Syntax.pretty_arity ctxt (t, Ss, [c]);
+ fun prt_arity t (c, Ss) = Syntax.pretty_arity ctxt (t, Ss, [c]);
fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty);
val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global;
fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
--- a/src/Pure/sorts.ML Wed Jun 02 10:50:53 2010 +0200
+++ b/src/Pure/sorts.ML Wed Jun 02 10:51:55 2010 +0200
@@ -26,7 +26,7 @@
val insert_terms: term list -> sort OrdList.T -> sort OrdList.T
type algebra
val classes_of: algebra -> serial Graph.T
- val arities_of: algebra -> (class * (class * sort list)) list Symtab.table
+ val arities_of: algebra -> (class * sort list) list Symtab.table
val all_classes: algebra -> class list
val super_classes: algebra -> class -> class list
val class_less: algebra -> class * class -> bool
@@ -105,15 +105,14 @@
arities: table of association lists of all type arities; (t, ars)
means that type constructor t has the arities ars; an element
- (c, (c0, Ss)) of ars represents the arity t::(Ss)c being derived
- via c0 <= c. "Coregularity" of the arities structure requires
- that for any two declarations t::(Ss1)c1 and t::(Ss2)c2 such that
- c1 <= c2 holds Ss1 <= Ss2.
+ (c, Ss) of ars represents the arity t::(Ss)c. "Coregularity" of
+ the arities structure requires that for any two declarations
+ t::(Ss1)c1 and t::(Ss2)c2 such that c1 <= c2 holds Ss1 <= Ss2.
*)
datatype algebra = Algebra of
{classes: serial Graph.T,
- arities: (class * (class * sort list)) list Symtab.table};
+ arities: (class * sort list) list Symtab.table};
fun classes_of (Algebra {classes, ...}) = classes;
fun arities_of (Algebra {arities, ...}) = arities;
@@ -225,9 +224,9 @@
Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n " ^
Pretty.string_of_arity pp (t, Ss', [c']));
-fun coregular pp algebra t (c, (c0, Ss)) ars =
+fun coregular pp algebra t (c, Ss) ars =
let
- fun conflict (c', (_, Ss')) =
+ fun conflict (c', Ss') =
if class_le algebra (c, c') andalso not (sorts_le algebra (Ss, Ss')) then
SOME ((c, c'), (c', Ss'))
else if class_le algebra (c', c) andalso not (sorts_le algebra (Ss', Ss)) then
@@ -236,19 +235,18 @@
in
(case get_first conflict ars of
SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss')
- | NONE => (c, (c0, Ss)) :: ars)
+ | NONE => (c, Ss) :: ars)
end;
-fun complete algebra (c0, Ss) = map (rpair (c0, Ss)) (c0 :: super_classes algebra c0);
+fun complete algebra (c, Ss) = map (rpair Ss) (c :: super_classes algebra c);
-fun insert pp algebra t (c, (c0, Ss)) ars =
+fun insert pp algebra t (c, Ss) ars =
(case AList.lookup (op =) ars c of
- NONE => coregular pp algebra t (c, (c0, Ss)) ars
- | SOME (_, Ss') =>
+ NONE => coregular pp algebra t (c, Ss) ars
+ | SOME Ss' =>
if sorts_le algebra (Ss, Ss') then ars
- else if sorts_le algebra (Ss', Ss) then
- coregular pp algebra t (c, (c0, Ss))
- (filter_out (fn (c'', (_, Ss'')) => c = c'' andalso Ss'' = Ss') ars)
+ else if sorts_le algebra (Ss', Ss)
+ then coregular pp algebra t (c, Ss) (remove (op =) (c, Ss') ars)
else err_conflict pp t NONE (c, Ss) (c, Ss'));
in
@@ -265,7 +263,7 @@
algebra |> map_arities (insert_complete_ars pp algebra arg);
fun add_arities_table pp algebra =
- Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, map snd ars));
+ Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, ars));
end;
@@ -310,16 +308,17 @@
in make_algebra (classes', arities') end;
-(* algebra projections *)
+(* algebra projections *) (* FIXME potentially violates abstract type integrity *)
fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
let
val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
- fun restrict_arity tyco (c, (_, Ss)) =
- if P c then case sargs (c, tyco)
- of SOME sorts => SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) sorts
- |> map restrict_sort))
- | NONE => NONE
+ fun restrict_arity t (c, Ss) =
+ if P c then
+ (case sargs (c, t) of
+ SOME sorts =>
+ SOME (c, Ss |> map2 (curry (inter_sort algebra)) sorts |> map restrict_sort)
+ | NONE => NONE)
else NONE;
val classes' = classes |> Graph.subgraph P;
val arities' = arities |> Symtab.map' (map_filter o restrict_arity);
@@ -355,7 +354,7 @@
fun dom c =
(case AList.lookup (op =) (Symtab.lookup_list arities a) c of
NONE => raise CLASS_ERROR (No_Arity (a, c))
- | SOME (_, Ss) => Ss);
+ | SOME Ss => Ss);
fun dom_inter c Ss = ListPair.map (inter_sort algebra) (dom c, Ss);
in
(case S of
@@ -380,11 +379,8 @@
in uncurry meet end;
fun meet_sort_typ algebra (T, S) =
- let
- val tab = meet_sort algebra (T, S) Vartab.empty;
- in Term.map_type_tvar (fn (v, _) =>
- TVar (v, (the o Vartab.lookup tab) v))
- end;
+ let val tab = meet_sort algebra (T, S) Vartab.empty;
+ in Term.map_type_tvar (fn (v, _) => TVar (v, (the o Vartab.lookup tab) v)) end;
(* of_sort *)
@@ -425,9 +421,9 @@
in
S |> map (fn c =>
let
- val (c0, Ss') = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
+ val Ss' = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
val dom' = map (fn ((U, d), S') => weaken U d S' ~~ S') ((Us ~~ dom) ~~ Ss');
- in class_relation T (type_constructor (a, Us) dom' c0, c0) c end)
+ in type_constructor (a, Us) dom' c end)
end
| derive (T, S) = weaken T (type_variable T) S;
in derive end;