1.1 --- a/src/Pure/axclass.ML Wed Jun 02 10:50:53 2010 +0200
1.2 +++ b/src/Pure/axclass.ML Wed Jun 02 10:51:55 2010 +0200
1.3 @@ -412,17 +412,15 @@
1.4
1.5 (* primitive rules *)
1.6
1.7 -fun gen_add_classrel store raw_th thy =
1.8 +fun add_classrel raw_th thy =
1.9 let
1.10 val th = Thm.strip_shyps (Thm.transfer thy raw_th);
1.11 val prop = Thm.plain_prop_of th;
1.12 fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
1.13 val rel = Logic.dest_classrel prop handle TERM _ => err ();
1.14 val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
1.15 - val (th', thy') =
1.16 - if store then PureThy.store_thm
1.17 - (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy
1.18 - else (th, thy);
1.19 + val (th', thy') = PureThy.store_thm
1.20 + (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy;
1.21 val th'' = th'
1.22 |> Thm.unconstrainT
1.23 |> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
1.24 @@ -433,17 +431,15 @@
1.25 |> perhaps complete_arities
1.26 end;
1.27
1.28 -fun gen_add_arity store raw_th thy =
1.29 +fun add_arity raw_th thy =
1.30 let
1.31 val th = Thm.strip_shyps (Thm.transfer thy raw_th);
1.32 val prop = Thm.plain_prop_of th;
1.33 fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
1.34 val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
1.35
1.36 - val (th', thy') =
1.37 - if store then PureThy.store_thm
1.38 - (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy
1.39 - else (th, thy);
1.40 + val (th', thy') = PureThy.store_thm
1.41 + (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
1.42
1.43 val args = Name.names Name.context Name.aT Ss;
1.44 val T = Type (t, map TFree args);
1.45 @@ -463,9 +459,6 @@
1.46 |> put_arity ((t, Ss, c), th'')
1.47 end;
1.48
1.49 -val add_classrel = gen_add_classrel true;
1.50 -val add_arity = gen_add_arity true;
1.51 -
1.52
1.53 (* tactical proofs *)
1.54
1.55 @@ -477,10 +470,7 @@
1.56 cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
1.57 quote (Syntax.string_of_classrel ctxt [c1, c2]));
1.58 in
1.59 - thy
1.60 - |> PureThy.add_thms [((Binding.name
1.61 - (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])]
1.62 - |-> (fn [th'] => gen_add_classrel false th')
1.63 + thy |> add_classrel th
1.64 end;
1.65
1.66 fun prove_arity raw_arity tac thy =
1.67 @@ -494,9 +484,7 @@
1.68 cat_error msg ("The error(s) above occurred while trying to prove type arity " ^
1.69 quote (Syntax.string_of_arity ctxt arity));
1.70 in
1.71 - thy
1.72 - |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths))
1.73 - |-> fold (gen_add_arity false)
1.74 + thy |> fold add_arity ths
1.75 end;
1.76
1.77
1.78 @@ -613,10 +601,6 @@
1.79 local
1.80
1.81 (*old-style axioms*)
1.82 -fun add_axiom (b, prop) =
1.83 - Thm.add_axiom (b, prop) #->
1.84 - (fn (_, thm) => PureThy.add_thm ((b, Drule.export_without_context thm), []));
1.85 -
1.86 fun axiomatize prep mk name add raw_args thy =
1.87 let
1.88 val args = prep thy raw_args;
1.89 @@ -624,17 +608,17 @@
1.90 val names = name args;
1.91 in
1.92 thy
1.93 - |> fold_map add_axiom (map Binding.name names ~~ specs)
1.94 - |-> fold add
1.95 + |> fold_map Thm.add_axiom (map Binding.name names ~~ specs)
1.96 + |-> fold (add o Drule.export_without_context o snd)
1.97 end;
1.98
1.99 fun ax_classrel prep =
1.100 axiomatize (map o prep) (map Logic.mk_classrel)
1.101 - (map (prefix classrel_prefix o Logic.name_classrel)) (gen_add_classrel false);
1.102 + (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
1.103
1.104 fun ax_arity prep =
1.105 axiomatize (prep o ProofContext.init_global) Logic.mk_arities
1.106 - (map (prefix arity_prefix) o Logic.name_arities) (gen_add_arity false);
1.107 + (map (prefix arity_prefix) o Logic.name_arities) add_arity;
1.108
1.109 fun class_const c =
1.110 (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);
2.1 --- a/src/Pure/display.ML Wed Jun 02 10:50:53 2010 +0200
2.2 +++ b/src/Pure/display.ML Wed Jun 02 10:51:55 2010 +0200
2.3 @@ -129,7 +129,7 @@
2.4
2.5 fun prt_cls c = Syntax.pretty_sort ctxt [c];
2.6 fun prt_sort S = Syntax.pretty_sort ctxt S;
2.7 - fun prt_arity t (c, (_, Ss)) = Syntax.pretty_arity ctxt (t, Ss, [c]);
2.8 + fun prt_arity t (c, Ss) = Syntax.pretty_arity ctxt (t, Ss, [c]);
2.9 fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty);
2.10 val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global;
2.11 fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
3.1 --- a/src/Pure/sorts.ML Wed Jun 02 10:50:53 2010 +0200
3.2 +++ b/src/Pure/sorts.ML Wed Jun 02 10:51:55 2010 +0200
3.3 @@ -26,7 +26,7 @@
3.4 val insert_terms: term list -> sort OrdList.T -> sort OrdList.T
3.5 type algebra
3.6 val classes_of: algebra -> serial Graph.T
3.7 - val arities_of: algebra -> (class * (class * sort list)) list Symtab.table
3.8 + val arities_of: algebra -> (class * sort list) list Symtab.table
3.9 val all_classes: algebra -> class list
3.10 val super_classes: algebra -> class -> class list
3.11 val class_less: algebra -> class * class -> bool
3.12 @@ -105,15 +105,14 @@
3.13
3.14 arities: table of association lists of all type arities; (t, ars)
3.15 means that type constructor t has the arities ars; an element
3.16 - (c, (c0, Ss)) of ars represents the arity t::(Ss)c being derived
3.17 - via c0 <= c. "Coregularity" of the arities structure requires
3.18 - that for any two declarations t::(Ss1)c1 and t::(Ss2)c2 such that
3.19 - c1 <= c2 holds Ss1 <= Ss2.
3.20 + (c, Ss) of ars represents the arity t::(Ss)c. "Coregularity" of
3.21 + the arities structure requires that for any two declarations
3.22 + t::(Ss1)c1 and t::(Ss2)c2 such that c1 <= c2 holds Ss1 <= Ss2.
3.23 *)
3.24
3.25 datatype algebra = Algebra of
3.26 {classes: serial Graph.T,
3.27 - arities: (class * (class * sort list)) list Symtab.table};
3.28 + arities: (class * sort list) list Symtab.table};
3.29
3.30 fun classes_of (Algebra {classes, ...}) = classes;
3.31 fun arities_of (Algebra {arities, ...}) = arities;
3.32 @@ -225,9 +224,9 @@
3.33 Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n " ^
3.34 Pretty.string_of_arity pp (t, Ss', [c']));
3.35
3.36 -fun coregular pp algebra t (c, (c0, Ss)) ars =
3.37 +fun coregular pp algebra t (c, Ss) ars =
3.38 let
3.39 - fun conflict (c', (_, Ss')) =
3.40 + fun conflict (c', Ss') =
3.41 if class_le algebra (c, c') andalso not (sorts_le algebra (Ss, Ss')) then
3.42 SOME ((c, c'), (c', Ss'))
3.43 else if class_le algebra (c', c) andalso not (sorts_le algebra (Ss', Ss)) then
3.44 @@ -236,19 +235,18 @@
3.45 in
3.46 (case get_first conflict ars of
3.47 SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss')
3.48 - | NONE => (c, (c0, Ss)) :: ars)
3.49 + | NONE => (c, Ss) :: ars)
3.50 end;
3.51
3.52 -fun complete algebra (c0, Ss) = map (rpair (c0, Ss)) (c0 :: super_classes algebra c0);
3.53 +fun complete algebra (c, Ss) = map (rpair Ss) (c :: super_classes algebra c);
3.54
3.55 -fun insert pp algebra t (c, (c0, Ss)) ars =
3.56 +fun insert pp algebra t (c, Ss) ars =
3.57 (case AList.lookup (op =) ars c of
3.58 - NONE => coregular pp algebra t (c, (c0, Ss)) ars
3.59 - | SOME (_, Ss') =>
3.60 + NONE => coregular pp algebra t (c, Ss) ars
3.61 + | SOME Ss' =>
3.62 if sorts_le algebra (Ss, Ss') then ars
3.63 - else if sorts_le algebra (Ss', Ss) then
3.64 - coregular pp algebra t (c, (c0, Ss))
3.65 - (filter_out (fn (c'', (_, Ss'')) => c = c'' andalso Ss'' = Ss') ars)
3.66 + else if sorts_le algebra (Ss', Ss)
3.67 + then coregular pp algebra t (c, Ss) (remove (op =) (c, Ss') ars)
3.68 else err_conflict pp t NONE (c, Ss) (c, Ss'));
3.69
3.70 in
3.71 @@ -265,7 +263,7 @@
3.72 algebra |> map_arities (insert_complete_ars pp algebra arg);
3.73
3.74 fun add_arities_table pp algebra =
3.75 - Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, map snd ars));
3.76 + Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, ars));
3.77
3.78 end;
3.79
3.80 @@ -310,16 +308,17 @@
3.81 in make_algebra (classes', arities') end;
3.82
3.83
3.84 -(* algebra projections *)
3.85 +(* algebra projections *) (* FIXME potentially violates abstract type integrity *)
3.86
3.87 fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
3.88 let
3.89 val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
3.90 - fun restrict_arity tyco (c, (_, Ss)) =
3.91 - if P c then case sargs (c, tyco)
3.92 - of SOME sorts => SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) sorts
3.93 - |> map restrict_sort))
3.94 - | NONE => NONE
3.95 + fun restrict_arity t (c, Ss) =
3.96 + if P c then
3.97 + (case sargs (c, t) of
3.98 + SOME sorts =>
3.99 + SOME (c, Ss |> map2 (curry (inter_sort algebra)) sorts |> map restrict_sort)
3.100 + | NONE => NONE)
3.101 else NONE;
3.102 val classes' = classes |> Graph.subgraph P;
3.103 val arities' = arities |> Symtab.map' (map_filter o restrict_arity);
3.104 @@ -355,7 +354,7 @@
3.105 fun dom c =
3.106 (case AList.lookup (op =) (Symtab.lookup_list arities a) c of
3.107 NONE => raise CLASS_ERROR (No_Arity (a, c))
3.108 - | SOME (_, Ss) => Ss);
3.109 + | SOME Ss => Ss);
3.110 fun dom_inter c Ss = ListPair.map (inter_sort algebra) (dom c, Ss);
3.111 in
3.112 (case S of
3.113 @@ -380,11 +379,8 @@
3.114 in uncurry meet end;
3.115
3.116 fun meet_sort_typ algebra (T, S) =
3.117 - let
3.118 - val tab = meet_sort algebra (T, S) Vartab.empty;
3.119 - in Term.map_type_tvar (fn (v, _) =>
3.120 - TVar (v, (the o Vartab.lookup tab) v))
3.121 - end;
3.122 + let val tab = meet_sort algebra (T, S) Vartab.empty;
3.123 + in Term.map_type_tvar (fn (v, _) => TVar (v, (the o Vartab.lookup tab) v)) end;
3.124
3.125
3.126 (* of_sort *)
3.127 @@ -425,9 +421,9 @@
3.128 in
3.129 S |> map (fn c =>
3.130 let
3.131 - val (c0, Ss') = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
3.132 + val Ss' = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
3.133 val dom' = map (fn ((U, d), S') => weaken U d S' ~~ S') ((Us ~~ dom) ~~ Ss');
3.134 - in class_relation T (type_constructor (a, Us) dom' c0, c0) c end)
3.135 + in type_constructor (a, Us) dom' c end)
3.136 end
3.137 | derive (T, S) = weaken T (type_variable T) S;
3.138 in derive end;