# HG changeset patch # User wenzelm # Date 1085167311 -7200 # Node ID d6ce35a1c3866c2acfb537860fcc8ac416d7c9ad # Parent 2be804d1dda903f43de78996e93bcecaaaa23cda incorporate sort ops from term.ML; use Graph.T; misc cleanup; diff -r 2be804d1dda9 -r d6ce35a1c386 src/Pure/sorts.ML --- a/src/Pure/sorts.ML Fri May 21 21:21:38 2004 +0200 +++ b/src/Pure/sorts.ML Fri May 21 21:21:51 2004 +0200 @@ -7,32 +7,37 @@ signature SORTS = sig - type classrel - type arities - val str_of_classrel: class * class -> string val str_of_sort: sort -> string val str_of_arity: string * sort list * sort -> string - val class_eq: classrel -> class * class -> bool - val class_less: classrel -> class * class -> bool - val class_le: classrel -> class * class -> bool - val sort_eq: classrel -> sort * sort -> bool - val sort_less: classrel -> sort * sort -> bool - val sort_le: classrel -> sort * sort -> bool - val sorts_le: classrel -> sort list * sort list -> bool - val inter_class: classrel -> class * sort -> sort - val inter_sort: classrel -> sort * sort -> sort - val norm_sort: classrel -> sort -> sort - val of_sort: classrel * arities -> typ * sort -> bool + val eq_sort: sort * sort -> bool + val mem_sort: sort * sort list -> bool + val subset_sort: sort list * sort list -> bool + val eq_set_sort: sort list * sort list -> bool + val ins_sort: sort * sort list -> sort list + val union_sort: sort list * sort list -> sort list + val rems_sort: sort list * sort list -> sort list + type classes + type arities + val class_eq: classes -> class * class -> bool + val class_less: classes -> class * class -> bool + val class_le: classes -> class * class -> bool + val sort_eq: classes -> sort * sort -> bool + val sort_less: classes -> sort * sort -> bool + val sort_le: classes -> sort * sort -> bool + val sorts_le: classes -> sort list * sort list -> bool + val inter_class: classes -> class * sort -> sort + val inter_sort: classes -> sort * sort -> sort + val norm_sort: classes -> sort -> sort + val of_sort: classes * arities -> typ * sort -> bool exception DOMAIN of string * class - val mg_domain: classrel * arities -> string -> sort -> sort list - val witness_sorts: classrel * arities * string list + val mg_domain: classes * arities -> string -> sort -> sort list (*exception DOMAIN*) + val witness_sorts: classes * arities -> string list -> sort list -> sort list -> (typ * sort) list end; structure Sorts: SORTS = struct - (** type classes and sorts **) (* @@ -44,36 +49,59 @@ represented by lists of classes. Normal forms of sorts are sorted lists of minimal classes (wrt. current class inclusion). - (already defined in Pure/term.ML) + (types already defined in Pure/term.ML) *) +(* simple printing -- lacks pretty printing, translations etc. *) + +fun str_of_sort [c] = c + | str_of_sort cs = Library.enclose "{" "}" (Library.commas cs); + +fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S + | str_of_arity (t, Ss, S) = t ^ " :: " ^ + Library.enclose "(" ")" (Library.commas (map str_of_sort Ss)) ^ " " ^ str_of_sort S; + + +(* equality, membership and insertion of sorts *) + +fun eq_sort ([]: sort, []) = true + | eq_sort ((S1 :: Ss1), (S2 :: Ss2)) = S1 = S2 andalso eq_sort (Ss1, Ss2) + | eq_sort (_, _) = false; + +fun mem_sort (_: sort, []) = false + | mem_sort (S, S' :: Ss) = eq_sort (S, S') orelse mem_sort (S, Ss); + +fun ins_sort (S, Ss) = if mem_sort (S, Ss) then Ss else S :: Ss; + +fun union_sort (Ss, []) = Ss + | union_sort ([], Ss) = Ss + | union_sort ((S :: Ss), Ss') = union_sort (Ss, ins_sort (S, Ss')); + +fun subset_sort ([], Ss) = true + | subset_sort (S :: Ss, Ss') = mem_sort (S, Ss') andalso subset_sort (Ss, Ss'); + +fun eq_set_sort (Ss, Ss') = + Ss = Ss' orelse (subset_sort (Ss, Ss') andalso subset_sort (Ss', Ss)); + +val rems_sort = gen_rems eq_sort; + + (* sort signature information *) (* - classrel: - table representing the proper subclass relation; entries (c, cs) - represent the superclasses cs of c; + classes: graph representing class declarations together with proper + subclass relation, which needs to be transitive and acyclic. - arities: - table of association lists of all type arities; (t, ars) means - that type constructor t has the arities ars; an element (c, Ss) of - ars represents the arity t::(Ss)c; + arities: table of association lists of all type arities; (t, ars) + means that type constructor t has the arities ars; an element (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. *) -type classrel = (class list) Symtab.table; -type arities = ((class * sort list) list) Symtab.table; - - -(* print sorts and arities *) - -val str_of_sort = Syntax.simple_str_of_sort; -fun str_of_classrel (c1, c2) = str_of_sort [c1] ^ " < " ^ str_of_sort [c2]; -fun str_of_dom Ss = enclose "(" ")" (commas (map str_of_sort Ss)); - -fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S - | str_of_arity (t, Ss, S) = - t ^ " :: " ^ str_of_dom Ss ^ " " ^ str_of_sort S; +type classes = stamp Graph.T; +type arities = (class * sort list) list Symtab.table; @@ -81,56 +109,50 @@ (* classes *) -fun class_eq _ (c1, c2:class) = c1 = c2; - -fun class_less classrel (c1, c2) = - (case Symtab.lookup (classrel, c1) of - Some cs => c2 mem_string cs - | None => false); - -fun class_le classrel (c1, c2) = - c1 = c2 orelse class_less classrel (c1, c2); +fun class_eq (_: classes) (c1, c2:class) = c1 = c2; +val class_less: classes -> class * class -> bool = Graph.is_edge; +fun class_le classes (c1, c2) = c1 = c2 orelse class_less classes (c1, c2); (* sorts *) -fun sort_le classrel (S1, S2) = - forall (fn c2 => exists (fn c1 => class_le classrel (c1, c2)) S1) S2; +fun sort_le classes (S1, S2) = + forall (fn c2 => exists (fn c1 => class_le classes (c1, c2)) S1) S2; -fun sorts_le classrel (Ss1, Ss2) = - ListPair.all (sort_le classrel) (Ss1, Ss2); +fun sorts_le classes (Ss1, Ss2) = + ListPair.all (sort_le classes) (Ss1, Ss2); -fun sort_eq classrel (S1, S2) = - sort_le classrel (S1, S2) andalso sort_le classrel (S2, S1); +fun sort_eq classes (S1, S2) = + sort_le classes (S1, S2) andalso sort_le classes (S2, S1); -fun sort_less classrel (S1, S2) = - sort_le classrel (S1, S2) andalso not (sort_le classrel (S2, S1)); +fun sort_less classes (S1, S2) = + sort_le classes (S1, S2) andalso not (sort_le classes (S2, S1)); (* normal forms of sorts *) -fun minimal_class classrel S c = - not (exists (fn c' => class_less classrel (c', c)) S); +fun minimal_class classes S c = + not (exists (fn c' => class_less classes (c', c)) S); -fun norm_sort classrel S = - sort_strings (distinct (filter (minimal_class classrel S) S)); +fun norm_sort classes S = + sort_strings (distinct (filter (minimal_class classes S) S)); (** intersection **) (*intersect class with sort (preserves minimality)*) -fun inter_class classrel (c, S) = +fun inter_class classes (c, S) = let fun intr [] = [c] | intr (S' as c' :: c's) = - if class_le classrel (c', c) then S' - else if class_le classrel (c, c') then intr c's + if class_le classes (c', c) then S' + else if class_le classes (c, c') then intr c's else c' :: intr c's in intr S end; (*instersect sorts (preserves minimality)*) -fun inter_sort classrel = sort_strings o foldr (inter_class classrel); +fun inter_sort classes = sort_strings o foldr (inter_class classes); @@ -140,27 +162,26 @@ exception DOMAIN of string * class; -fun mg_dom arities a c = - (case Symtab.lookup (arities, a) of - None => raise DOMAIN (a, c) - | Some ars => (case assoc (ars, c) of None => raise DOMAIN (a, c) | Some Ss => Ss)); - fun mg_domain _ _ [] = sys_error "mg_domain" (*don't know number of args!*) - | mg_domain (classrel, arities) a S = - let val doms = map (mg_dom arities a) S in - foldl (ListPair.map (inter_sort classrel)) (hd doms, tl doms) - end; + | mg_domain (classes, arities) a S = + let + fun mg_dom c = + (case Library.assoc_string (Symtab.lookup_multi (arities, a), c) of + None => raise DOMAIN (a, c) + | Some Ss => Ss); + val doms = map mg_dom S; + in foldl (ListPair.map (inter_sort classes)) (hd doms, tl doms) end; (* of_sort *) -fun of_sort (classrel, arities) = +fun of_sort (classes, arities) = let fun ofS (_, []) = true - | ofS (TFree (_, S), S') = sort_le classrel (S, S') - | ofS (TVar (_, S), S') = sort_le classrel (S, S') + | ofS (TFree (_, S), S') = sort_le classes (S, S') + | ofS (TVar (_, S), S') = sort_le classes (S, S') | ofS (Type (a, Ts), S) = - let val Ss = mg_domain (classrel, arities) a S in + let val Ss = mg_domain (classes, arities) a S in ListPair.all ofS (Ts, Ss) end handle DOMAIN _ => false; in ofS end; @@ -169,13 +190,13 @@ (** witness_sorts **) -fun witness_sorts_aux (classrel, arities, log_types) hyps sorts = +fun witness_sorts_aux (classes, arities) log_types hyps sorts = let val top_witn = (propT, []); - fun le S1 S2 = sort_le classrel (S1, S2); + fun le S1 S2 = sort_le classes (S1, S2); fun get_solved S2 (T, S1) = if le S1 S2 then Some (T, S2) else None; fun get_hyp S2 S1 = if le S1 S2 then Some (TFree ("'hyp", S1), S2) else None; - fun mg_dom t S = Some (mg_domain (classrel, arities) t S) handle DOMAIN _ => None; + fun mg_dom t S = Some (mg_domain (classes, arities) t S) handle DOMAIN _ => None; fun witn_sort _ (solved_failed, []) = (solved_failed, Some top_witn) | witn_sort path ((solved, failed), S) = @@ -209,13 +230,14 @@ in witn_sorts [] (([], []), sorts) end; -fun witness_sorts (classrel, arities, log_types) hyps sorts = +fun witness_sorts (classes, arities) log_types hyps sorts = let + (*double check result of witness search*) fun check_result None = None | check_result (Some (T, S)) = - if of_sort (classrel, arities) (T, S) then Some (T, S) - else (warning ("witness_sorts: rejected bad witness for " ^ str_of_sort S); None); - in mapfilter check_result (#2 (witness_sorts_aux (classrel, arities, log_types) hyps sorts)) end; + if of_sort (classes, arities) (T, S) then Some (T, S) + else sys_error ("Sorts.witness_sorts: bad witness for sort " ^ str_of_sort S); + in mapfilter check_result (#2 (witness_sorts_aux (classes, arities) log_types hyps sorts)) end; end;