moved certify_class/sort to type.ML;
authorwenzelm
Sun Apr 30 22:50:08 2006 +0200 (2006-04-30)
changeset 195141f0218dab849
parent 19513 77ff7cd602d7
child 19515 9f650083da65
moved certify_class/sort to type.ML;
added operations to build sort algebras (from type.ML);
tuned;
src/Pure/sorts.ML
     1.1 --- a/src/Pure/sorts.ML	Sun Apr 30 22:50:07 2006 +0200
     1.2 +++ b/src/Pure/sorts.ML	Sun Apr 30 22:50:08 2006 +0200
     1.3 @@ -2,12 +2,11 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     1.6  
     1.7 -Type classes and sorts.
     1.8 +The order-sorted algebra of type classes.
     1.9  *)
    1.10  
    1.11  signature SORTS =
    1.12  sig
    1.13 -  (*operations on ordered lists*)
    1.14    val eq_set: sort list * sort list -> bool
    1.15    val union: sort list -> sort list -> sort list
    1.16    val subtract: sort list -> sort list -> sort list
    1.17 @@ -17,7 +16,6 @@
    1.18    val insert_typs: typ list -> sort list -> sort list
    1.19    val insert_term: term -> sort list -> sort list
    1.20    val insert_terms: term list -> sort list -> sort list
    1.21 -  (*signature information*)
    1.22    type classes
    1.23    type arities
    1.24    val class_eq: classes -> class * class -> bool
    1.25 @@ -28,18 +26,23 @@
    1.26    val sorts_le: classes -> sort list * sort list -> bool
    1.27    val inter_sort: classes -> sort * sort -> sort
    1.28    val norm_sort: classes -> sort -> sort
    1.29 -  val certify_class: classes -> class -> class
    1.30 -  val certify_sort: classes -> sort -> sort
    1.31    val of_sort: classes * arities -> typ * sort -> bool
    1.32    exception DOMAIN of string * class
    1.33    val mg_domain: classes * arities -> string -> sort -> sort list  (*exception DOMAIN*)
    1.34    val witness_sorts: classes * arities -> string list ->
    1.35      sort list -> sort list -> (typ * sort) list
    1.36 +  val add_arities: Pretty.pp -> classes -> string * (class * sort list) list -> arities -> arities
    1.37 +  val rebuild_arities: Pretty.pp -> classes -> arities -> arities
    1.38 +  val merge_arities: Pretty.pp -> classes -> arities * arities -> arities
    1.39 +  val add_class: Pretty.pp -> class * class list -> classes -> classes
    1.40 +  val add_classrel: Pretty.pp -> class * class -> classes -> classes
    1.41 +  val merge_classes: Pretty.pp -> classes * classes -> classes
    1.42  end;
    1.43  
    1.44  structure Sorts: SORTS =
    1.45  struct
    1.46  
    1.47 +
    1.48  (** type classes and sorts **)
    1.49  
    1.50  (*
    1.51 @@ -50,8 +53,6 @@
    1.52    Sorts are intersections of finitely many classes. They are
    1.53    represented by lists of classes.  Normal forms of sorts are sorted
    1.54    lists of minimal classes (wrt. current class inclusion).
    1.55 -
    1.56 -  (types already defined in Pure/term.ML)
    1.57  *)
    1.58  
    1.59  
    1.60 @@ -130,19 +131,9 @@
    1.61    | norm_sort classes S = sort_distinct string_ord (filter (minimal_class classes S) S);
    1.62  
    1.63  
    1.64 -(* certify *)
    1.65 -
    1.66 -fun certify_class classes c =
    1.67 -  if can (Graph.get_node classes) c then c
    1.68 -  else raise TYPE ("Undeclared class: " ^ quote c, [], []);
    1.69  
    1.70 -fun certify_sort classes = norm_sort classes o map (certify_class classes);
    1.71 -
    1.72 -
    1.73 +(** intersection -- preserving minimality **)
    1.74  
    1.75 -(** intersection **)
    1.76 -
    1.77 -(*intersect class with sort (preserves minimality)*)
    1.78  fun inter_class classes c S =
    1.79    let
    1.80      fun intr [] = [c]
    1.81 @@ -152,7 +143,6 @@
    1.82            else c' :: intr c's
    1.83    in intr S end;
    1.84  
    1.85 -(*instersect sorts (preserves minimality)*)
    1.86  fun inter_sort classes (S1, S2) =
    1.87    sort_strings (fold (inter_class classes) S1 S2);
    1.88  
    1.89 @@ -252,4 +242,101 @@
    1.90  
    1.91  end;
    1.92  
    1.93 +
    1.94 +
    1.95 +(** build sort algebras **)
    1.96 +
    1.97 +(* classes *)
    1.98 +
    1.99 +local
   1.100 +
   1.101 +fun err_dup_classes cs =
   1.102 +  error ("Duplicate declaration of class(es): " ^ commas_quote cs);
   1.103 +
   1.104 +fun err_cyclic_classes pp css =
   1.105 +  error (cat_lines (map (fn cs =>
   1.106 +    "Cycle in class relation: " ^ Pretty.string_of_classrel pp cs) css));
   1.107 +
   1.108 +in
   1.109 +
   1.110 +fun add_class pp (c, cs) classes =
   1.111 +  let
   1.112 +    val classes' = classes |> Graph.new_node (c, stamp ())
   1.113 +      handle Graph.DUP dup => err_dup_classes [dup];
   1.114 +    val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs)
   1.115 +      handle Graph.CYCLES css => err_cyclic_classes pp css;
   1.116 +  in classes'' end;
   1.117 +
   1.118 +fun add_classrel pp rel classes =
   1.119 +  classes |> Graph.add_edge_trans_acyclic rel
   1.120 +    handle Graph.CYCLES css => err_cyclic_classes pp css;
   1.121 +
   1.122 +fun merge_classes pp args : classes =
   1.123 +  Graph.merge_trans_acyclic (op =) args
   1.124 +    handle Graph.DUPS cs => err_dup_classes cs
   1.125 +        | Graph.CYCLES css => err_cyclic_classes pp css;
   1.126 +
   1.127  end;
   1.128 +
   1.129 +
   1.130 +(* arities *)
   1.131 +
   1.132 +local
   1.133 +
   1.134 +fun for_classes _ NONE = ""
   1.135 +  | for_classes pp (SOME (c1, c2)) =
   1.136 +      " for classes " ^ Pretty.string_of_classrel pp [c1, c2];
   1.137 +
   1.138 +fun err_conflict pp t cc (c, Ss) (c', Ss') =
   1.139 +  error ("Conflict of type arities" ^ for_classes pp cc ^ ":\n  " ^
   1.140 +    Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n  " ^
   1.141 +    Pretty.string_of_arity pp (t, Ss', [c']));
   1.142 +
   1.143 +fun coregular pp C t (c, Ss) ars =
   1.144 +  let
   1.145 +    fun conflict (c', Ss') =
   1.146 +      if class_le C (c, c') andalso not (sorts_le C (Ss, Ss')) then
   1.147 +        SOME ((c, c'), (c', Ss'))
   1.148 +      else if class_le C (c', c) andalso not (sorts_le C (Ss', Ss)) then
   1.149 +        SOME ((c', c), (c', Ss'))
   1.150 +      else NONE;
   1.151 +  in
   1.152 +    (case get_first conflict ars of
   1.153 +      SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss')
   1.154 +    | NONE => (c, Ss) :: ars)
   1.155 +  end;
   1.156 +
   1.157 +fun insert pp C t (c, Ss) ars =
   1.158 +  (case AList.lookup (op =) ars c of
   1.159 +    NONE => coregular pp C t (c, Ss) ars
   1.160 +  | SOME Ss' =>
   1.161 +      if sorts_le C (Ss, Ss') then ars
   1.162 +      else if sorts_le C (Ss', Ss)
   1.163 +      then coregular pp C t (c, Ss) (remove (op =) (c, Ss') ars)
   1.164 +      else err_conflict pp t NONE (c, Ss) (c, Ss'));
   1.165 +
   1.166 +fun complete C (c, Ss) = map (rpair Ss) (Graph.all_succs C [c]);
   1.167 +
   1.168 +in
   1.169 +
   1.170 +fun add_arities pp classes (t, ars) arities =
   1.171 +  let val ars' =
   1.172 +    Symtab.lookup_list arities t
   1.173 +    |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars)
   1.174 +  in Symtab.update (t, ars') arities end;
   1.175 +
   1.176 +fun add_arities_table pp classes = Symtab.fold (fn (t, ars) =>
   1.177 +  add_arities pp classes (t, map (apsnd (map (norm_sort classes))) ars));
   1.178 +
   1.179 +fun rebuild_arities pp classes arities =
   1.180 +  Symtab.empty
   1.181 +  |> add_arities_table pp classes arities;
   1.182 +
   1.183 +fun merge_arities pp classes (arities1, arities2) =
   1.184 +  Symtab.empty
   1.185 +  |> add_arities_table pp classes arities1
   1.186 +  |> add_arities_table pp classes arities2;
   1.187 +
   1.188 +end;
   1.189 +
   1.190 +end;