--- 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;