# HG changeset patch # User wenzelm # Date 1146522037 -7200 # Node ID 7fbac32cded0430960dbb49f515cf44987936289 # Parent 9b5c38e8e780da90b2c36a385fc41deef4c69c88 of_sort: option; of_sort: simplified implementation, use Sorts.of_sort_derivation; tuned; diff -r 9b5c38e8e780 -r 7fbac32cded0 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Mon May 01 18:10:40 2006 +0200 +++ b/src/Pure/axclass.ML Tue May 02 00:20:37 2006 +0200 @@ -29,7 +29,7 @@ val axiomatize_classrel_i: (class * class) list -> theory -> theory val axiomatize_arity: xstring * string list * string -> theory -> theory val axiomatize_arity_i: arity -> theory -> theory - val of_sort: theory -> typ * sort -> thm list + val of_sort: theory -> typ * sort -> thm list option end; structure AxClass: AX_CLASS = @@ -149,11 +149,18 @@ val get_instances = AxClassData.get #> (fn (_, ref (Instances insts)) => insts); +fun lookup_classrel thy = + Option.map (Thm.transfer thy) o AList.lookup (op =) (#classrel (get_instances thy)); + +fun lookup_arity thy = + Option.map (Thm.transfer thy) oo + (AList.lookup (op =) o Symtab.lookup_list (#arities (get_instances thy))); + +val lookup_type = AList.lookup (op =) oo (Typtab.lookup_list o #types o get_instances); + + fun store_instance f thy (x, th) = - let - val th' = Drule.standard' th; - val _ = change (#2 (AxClassData.get thy)) (map_instances (f (x, th'))); - in th' end; + (change (#2 (AxClassData.get thy)) (map_instances (f (x, th))); th); val store_classrel = store_instance (fn ((c1, c2), th) => fn (classes, classrel, arities, types) => (classes @@ -222,9 +229,10 @@ fun add_arity th thy = let + fun err () = raise THM ("add_arity: malformed type arity", 0, [th]); val prop = Drule.plain_prop_of (Thm.transfer thy th); - val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => - raise THM ("add_arity: malformed type arity", 0, [th]); + val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err (); + val _ = if map (Sign.certify_sort thy) Ss = Ss then () else err (); val thy' = thy |> Sign.primitive_arity (t, Ss, [c]); val _ = store_arity thy' ((t, Ss, c), Drule.unconstrainTs th); in thy' end; @@ -382,70 +390,55 @@ local -fun derive_classrel thy (c1, c2) = +fun derive_classrel thy (th, c1) c2 = let - val {classes, classrel, ...} = get_instances thy; - val lookup = AList.lookup (op =) classrel; - fun derive [c, c'] = the (lookup (c, c')) + fun derive [c, c'] = the (lookup_classrel thy (c, c')) | derive (c :: c' :: cs) = derive [c, c'] RS derive (c' :: cs); - in - (case lookup (c1, c2) of - SOME rule => rule - | NONE => - (case Graph.find_paths classes (c1, c2) of - [] => error ("Cannot derive class relation " ^ Sign.string_of_classrel thy [c1, c2]) - | path :: _ => store_classrel thy ((c1, c2), derive path))) - end; + val th' = + (case lookup_classrel thy (c1, c2) of + SOME rule => rule + | NONE => + (case Graph.find_paths (#classes (get_instances thy)) (c1, c2) of + [] => error ("Cannot derive class relation " ^ Sign.string_of_classrel thy [c1, c2]) + | path :: _ => store_classrel thy ((c1, c2), derive path))) + in th RS th' end; -fun weaken_subclass thy (c1, th) c2 = - if c1 = c2 then th - else th RS derive_classrel thy (c1, c2); - -fun weaken_subsort thy S1 S2 = S2 |> map (fn c2 => - (case S1 |> find_first (fn (c1, _) => Sign.subsort thy ([c1], [c2])) of - SOME c1 => weaken_subclass thy c1 c2 - | NONE => error ("Cannot derive subsort relation " ^ - Sign.string_of_sort thy (map #1 S1) ^ " < " ^ Sign.string_of_sort thy S2))); - -fun apply_arity thy t dom c = - let - val {arities, ...} = get_instances thy; - val subsort = Sign.subsort thy; - val Ss = map (map #1) dom; - in - (case Symtab.lookup_list arities t |> find_first (fn ((c', Ss'), _) => - subsort ([c'], [c]) andalso ListPair.all subsort (Ss, Ss')) of - SOME ((c', Ss'), rule) => - weaken_subclass thy (c', rule OF flat (map2 (weaken_subsort thy) dom Ss')) c - | NONE => error ("Cannot derive type arity " ^ Sign.string_of_arity thy (t, Ss, [c]))) +fun derive_constructor thy a dom c = + let val Ss = map (map snd) dom and ths = maps (map fst) dom in + (case lookup_arity thy a (c, Ss) of + SOME rule => ths MRS rule + | NONE => error ("Cannot derive type arity " ^ Sign.string_of_arity thy (a, Ss, [c]))) end; fun derive_type _ (_, []) = [] | derive_type thy (typ, sort) = let - val hyps = Term.fold_atyps + val vars = Term.fold_atyps (fn T as TFree (_, S) => insert (eq_fst op =) (T, S) | T as TVar (_, S) => insert (eq_fst op =) (T, S) - | _ => I) typ [] - |> map (fn (T, S) => (T, S ~~ Drule.sort_triv thy (T, S))); - - fun derive (Type (a, Ts)) S = - let - val Ss = Sign.arity_sorts thy a S; - val ds = map (fn (T, S) => S ~~ derive T S) (Ts ~~ Ss); - in map (apply_arity thy a ds) S end - | derive T S = weaken_subsort thy (the_default [] (AList.lookup (op =) hyps T)) S; - - val ths = derive typ sort; + | _ => I) typ []; + val hyps = vars |> map (fn (T, S) => (T, Drule.sort_triv thy (T, S) ~~ S)); + val ths = (typ, sort) + |> Sorts.of_sort_derivation (Sign.pp thy) (Sign.classes_of thy, Sign.arities_of thy) + {classrel = derive_classrel thy, + constructor = derive_constructor thy, + variable = the_default [] o AList.lookup (op =) hyps}; in map (store_type thy) (map (pair typ) sort ~~ ths) end; in fun of_sort thy (typ, sort) = - let - fun lookup () = AList.lookup (op =) (Typtab.lookup_list (#types (get_instances thy)) typ); - val _ = derive_type thy (typ, filter (is_none o lookup ()) sort); - in map (the o lookup ()) sort end; + if Sign.of_sort thy (typ, sort) then + let + val cert = Thm.cterm_of thy; + fun derive c = + Goal.finish (the (lookup_type thy typ c) RS Goal.init (cert (Logic.mk_inclass (typ, c)))) + |> Thm.adjust_maxidx_thm; + val _ = derive_type thy (typ, filter (is_none o lookup_type thy typ) sort) + handle ERROR msg => cat_error msg ("The error(s) above occurred for sort derivation: " ^ + Sign.string_of_typ thy typ ^ " :: " ^ Sign.string_of_sort thy sort); + in SOME (map derive sort) end + else NONE; end;