# HG changeset patch # User blanchet # Date 1275468715 -7200 # Node ID e14dc033287b480c80220f4617980f9715608904 # Parent 119c2901304c144edc5c4d22fc2abac82962de96# Parent e7544b9ce6afd87019fcc668d4b012c1c660a700 merge diff -r 119c2901304c -r e14dc033287b src/Pure/axclass.ML --- 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); diff -r 119c2901304c -r e14dc033287b src/Pure/display.ML --- 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); diff -r 119c2901304c -r e14dc033287b src/Pure/sorts.ML --- 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;