summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Pure/sorts.ML

changeset 2956 | d128ae3e7421 |

child 2990 | 271062b8c461 |

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/sorts.ML Wed Apr 16 18:14:43 1997 +0200 @@ -0,0 +1,176 @@ +(* Title: Pure/sorts.ML + ID: $Id$ + Author: Markus Wenzel and Stefan Berghofer, TU Muenchen + +Type classes and sorts. +*) + +signature SORTS = +sig + type classrel + type arities + 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 least_sort: classrel -> arities -> typ -> sort + val mg_domain: classrel -> arities -> string -> sort -> sort list + val nonempty_sort: classrel -> arities -> sort list -> sort -> bool +end; + +structure Sorts: SORTS = +struct + + +(** type classes and sorts **) + +(* + Classes denote (possibly empty) collections of types that are + partially ordered by class inclusion. They are represented + symbolically by strings. + + Sorts are intersections of finitely many classes. They are + 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) +*) + + +(* sort signature information *) + +(* + classrel: + association list representing the proper subclass relation; + pairs (c, cs) represent the superclasses cs of c; + + arities: + two-fold association list 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. +*) + +type classrel = (class * class list) list; +type arities = (string * (class * sort list) list) list; + + +(* print sorts and arities *) + +fun str_of_sort [c] = c + | str_of_sort cs = enclose "{" "}" (commas cs); + +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; + + + +(** equality and inclusion **) + +(* classes *) + +fun class_eq _ (c1, c2:class) = c1 = c2; + +fun class_less classrel (c1, c2) = + (case assoc (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); + + +(* sorts *) + +fun sort_le classrel (S1, S2) = + forall (fn c2 => exists (fn c1 => class_le classrel (c1, c2)) S1) S2; + +fun sorts_le classrel (Ss1, Ss2) = + ListPair.all (sort_le classrel) (Ss1, Ss2); + +fun sort_eq classrel (S1, S2) = + sort_le classrel (S1, S2) andalso sort_le classrel (S2, S1); + +fun sort_less classrel (S1, S2) = + sort_le classrel (S1, S2) andalso not (sort_le classrel (S2, S1)); + + +(* normal forms of sorts *) + +fun minimal_class classrel S c = + not (exists (fn c' => class_less classrel (c', c)) S); + +fun norm_sort classrel S = + sort_strings (distinct (filter (minimal_class classrel S) S)); + + + +(** intersection **) + +(*intersect class with sort (preserves minimality)*) (* FIXME tune? *) +fun inter_class classrel (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 + else c' :: intr c's + in intr S end; + +(*instersect sorts (preserves minimality)*) +fun inter_sort classrel = foldr (inter_class classrel); + + + +(** sorts of types **) + +(* least_sort *) + +fun least_sort classrel arities T = + let + fun match_dom Ss (c, Ss') = + if sorts_le classrel (Ss, Ss') then Some c + else None; + + fun leastS (Type (a, Ts)) = + norm_sort classrel + (mapfilter (match_dom (map leastS Ts)) (assocs arities a)) + | leastS (TFree (_, S)) = S + | leastS (TVar (_, S)) = S + in leastS T end; + + +(* mg_domain *) (*exception TYPE*) + +fun mg_dom arities a c = + (case assoc2 (arities, (a, c)) of + None => raise_type ("No way to get " ^ 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; + + + +(** nonempty_sort **) + +(* FIXME improve: proper sorts; non-base, non-ground types (vars from hyps) *) +fun nonempty_sort classrel _ _ [] = true + | nonempty_sort classrel arities hyps S = + exists (exists (fn (c, Ss) => [c] = S andalso null Ss) o snd) arities + orelse exists (fn S' => sort_le classrel (S', S)) hyps; + +end;