abstract interfaces for type algebra;
authorwenzelm
Tue May 16 13:01:28 2006 +0200 (2006-05-16)
changeset 19645bbda28f2d379
parent 19644 0b01436e1843
child 19646 91c0ae7e542b
abstract interfaces for type algebra;
tuned;
src/Pure/sorts.ML
     1.1 --- a/src/Pure/sorts.ML	Tue May 16 13:01:27 2006 +0200
     1.2 +++ b/src/Pure/sorts.ML	Tue May 16 13:01:28 2006 +0200
     1.3 @@ -24,34 +24,36 @@
     1.4    val insert_typs: typ list -> sort list -> sort list
     1.5    val insert_term: term -> sort list -> sort list
     1.6    val insert_terms: term list -> sort list -> sort list
     1.7 -  type classes
     1.8 -  type arities
     1.9 -  val class_eq: classes -> class * class -> bool
    1.10 -  val class_less: classes -> class * class -> bool
    1.11 -  val class_le: classes -> class * class -> bool
    1.12 -  val sort_eq: classes -> sort * sort -> bool
    1.13 -  val sort_le: classes -> sort * sort -> bool
    1.14 -  val sorts_le: classes -> sort list * sort list -> bool
    1.15 -  val inter_sort: classes -> sort * sort -> sort
    1.16 -  val norm_sort: classes -> sort -> sort
    1.17 -  val add_arities: Pretty.pp -> classes -> string * (class * sort list) list -> arities -> arities
    1.18 -  val rebuild_arities: Pretty.pp -> classes -> arities -> arities
    1.19 -  val merge_arities: Pretty.pp -> classes -> arities * arities -> arities
    1.20 -  val add_class: Pretty.pp -> class * class list -> classes -> classes
    1.21 -  val add_classrel: Pretty.pp -> class * class -> classes -> classes
    1.22 -  val merge_classes: Pretty.pp -> classes * classes -> classes
    1.23 +  type algebra
    1.24 +  val rep_algebra: algebra ->
    1.25 +   {classes: stamp Graph.T,
    1.26 +    arities: (class * (class * sort list)) list Symtab.table}
    1.27 +  val classes: algebra -> class list
    1.28 +  val super_classes: algebra -> class -> class list
    1.29 +  val class_less: algebra -> class * class -> bool
    1.30 +  val class_le: algebra -> class * class -> bool
    1.31 +  val sort_eq: algebra -> sort * sort -> bool
    1.32 +  val sort_le: algebra -> sort * sort -> bool
    1.33 +  val sorts_le: algebra -> sort list * sort list -> bool
    1.34 +  val inter_sort: algebra -> sort * sort -> sort
    1.35 +  val certify_class: algebra -> class -> class    (*exception TYPE*)
    1.36 +  val certify_sort: algebra -> sort -> sort       (*exception TYPE*)
    1.37 +  val add_class: Pretty.pp -> class * class list -> algebra -> algebra
    1.38 +  val add_classrel: Pretty.pp -> class * class -> algebra -> algebra
    1.39 +  val add_arities: Pretty.pp -> string * (class * sort list) list -> algebra -> algebra
    1.40 +  val empty_algebra: algebra
    1.41 +  val merge_algebra: Pretty.pp -> algebra * algebra -> algebra
    1.42    type class_error
    1.43    val class_error: Pretty.pp -> class_error -> 'a
    1.44    exception CLASS_ERROR of class_error
    1.45 -  val mg_domain: classes * arities -> string -> sort -> sort list   (*exception CLASS_ERROR*)
    1.46 -  val of_sort: classes * arities -> typ * sort -> bool
    1.47 -  val of_sort_derivation: Pretty.pp -> classes * arities ->
    1.48 +  val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
    1.49 +  val of_sort: algebra -> typ * sort -> bool
    1.50 +  val of_sort_derivation: Pretty.pp -> algebra ->
    1.51      {classrel: 'a * class -> class -> 'a,
    1.52       constructor: string -> ('a * class) list list -> class -> 'a,
    1.53       variable: typ -> ('a * class) list} ->
    1.54      typ * sort -> 'a list   (*exception CLASS_ERROR*)
    1.55 -  val witness_sorts: classes * arities -> string list ->
    1.56 -    sort list -> sort list -> (typ * sort) list
    1.57 +  val witness_sorts: algebra -> string list -> sort list -> sort list -> (typ * sort) list
    1.58  end;
    1.59  
    1.60  structure Sorts: SORTS =
    1.61 @@ -99,60 +101,84 @@
    1.62      c1 <= c2 holds Ss1 <= Ss2.
    1.63  *)
    1.64  
    1.65 -type classes = stamp Graph.T;
    1.66 -type arities = (class * (class * sort list)) list Symtab.table;
    1.67 +datatype algebra = Algebra of
    1.68 + {classes: stamp Graph.T,
    1.69 +  arities: (class * (class * sort list)) list Symtab.table};
    1.70 +
    1.71 +fun rep_algebra (Algebra args) = args;
    1.72 +
    1.73 +val classes_of = #classes o rep_algebra;
    1.74 +val arities_of = #arities o rep_algebra;
    1.75 +
    1.76 +fun make_algebra (classes, arities) =
    1.77 +  Algebra {classes = classes, arities = arities};
    1.78 +
    1.79 +fun map_classes f (Algebra {classes, arities}) = make_algebra (f classes, arities);
    1.80 +fun map_arities f (Algebra {classes, arities}) = make_algebra (classes, f arities);
    1.81 +
    1.82 +
    1.83 +(* classes *)
    1.84 +
    1.85 +val classes = Graph.keys o classes_of;
    1.86 +val super_classes = Graph.imm_succs o classes_of;
    1.87  
    1.88  
    1.89  (* class relations *)
    1.90  
    1.91 -fun class_eq (_: classes) (c1, c2:class) = c1 = c2;
    1.92 -val class_less: classes -> class * class -> bool = Graph.is_edge;
    1.93 -fun class_le classes (c1, c2) = c1 = c2 orelse class_less classes (c1, c2);
    1.94 +val class_less = Graph.is_edge o classes_of;
    1.95 +fun class_le algebra (c1, c2) = c1 = c2 orelse class_less algebra (c1, c2);
    1.96  
    1.97  
    1.98  (* sort relations *)
    1.99  
   1.100 -fun sort_le classes (S1, S2) =
   1.101 -  forall (fn c2 => exists (fn c1 => class_le classes (c1, c2)) S1) S2;
   1.102 +fun sort_le algebra (S1, S2) =
   1.103 +  forall (fn c2 => exists (fn c1 => class_le algebra (c1, c2)) S1) S2;
   1.104  
   1.105 -fun sorts_le classes (Ss1, Ss2) =
   1.106 -  ListPair.all (sort_le classes) (Ss1, Ss2);
   1.107 +fun sorts_le algebra (Ss1, Ss2) =
   1.108 +  ListPair.all (sort_le algebra) (Ss1, Ss2);
   1.109  
   1.110 -fun sort_eq classes (S1, S2) =
   1.111 -  sort_le classes (S1, S2) andalso sort_le classes (S2, S1);
   1.112 +fun sort_eq algebra (S1, S2) =
   1.113 +  sort_le algebra (S1, S2) andalso sort_le algebra (S2, S1);
   1.114  
   1.115  
   1.116  (* intersection *)
   1.117  
   1.118 -fun inter_class classes c S =
   1.119 +fun inter_class algebra c S =
   1.120    let
   1.121      fun intr [] = [c]
   1.122        | intr (S' as c' :: c's) =
   1.123 -          if class_le classes (c', c) then S'
   1.124 -          else if class_le classes (c, c') then intr c's
   1.125 +          if class_le algebra (c', c) then S'
   1.126 +          else if class_le algebra (c, c') then intr c's
   1.127            else c' :: intr c's
   1.128    in intr S end;
   1.129  
   1.130 -fun inter_sort classes (S1, S2) =
   1.131 -  sort_strings (fold (inter_class classes) S1 S2);
   1.132 +fun inter_sort algebra (S1, S2) =
   1.133 +  sort_strings (fold (inter_class algebra) S1 S2);
   1.134  
   1.135  
   1.136 -(* normal forms *)
   1.137 +(* normal form *)
   1.138  
   1.139  fun norm_sort _ [] = []
   1.140    | norm_sort _ (S as [_]) = S
   1.141 -  | norm_sort classes S =
   1.142 -      filter (fn c => not (exists (fn c' => class_less classes (c', c)) S)) S
   1.143 +  | norm_sort algebra S =
   1.144 +      filter (fn c => not (exists (fn c' => class_less algebra (c', c)) S)) S
   1.145        |> sort_distinct string_ord;
   1.146  
   1.147  
   1.148 +(* certify *)
   1.149 +
   1.150 +fun certify_class algebra c =
   1.151 +  if can (Graph.get_node (classes_of algebra)) c then c
   1.152 +  else raise TYPE ("Undeclared class: " ^ quote c, [], []);
   1.153 +
   1.154 +fun certify_sort classes = norm_sort classes o map (certify_class classes);
   1.155 +
   1.156 +
   1.157  
   1.158  (** build algebras **)
   1.159  
   1.160  (* classes *)
   1.161  
   1.162 -local
   1.163 -
   1.164  fun err_dup_classes cs =
   1.165    error ("Duplicate declaration of class(es): " ^ commas_quote cs);
   1.166  
   1.167 @@ -160,26 +186,13 @@
   1.168    error (cat_lines (map (fn cs =>
   1.169      "Cycle in class relation: " ^ Pretty.string_of_classrel pp cs) css));
   1.170  
   1.171 -in
   1.172 -
   1.173 -fun add_class pp (c, cs) classes =
   1.174 +fun add_class pp (c, cs) = map_classes (fn classes =>
   1.175    let
   1.176      val classes' = classes |> Graph.new_node (c, stamp ())
   1.177        handle Graph.DUP dup => err_dup_classes [dup];
   1.178      val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs)
   1.179        handle Graph.CYCLES css => err_cyclic_classes pp css;
   1.180 -  in classes'' end;
   1.181 -
   1.182 -fun add_classrel pp rel classes =
   1.183 -  classes |> Graph.add_edge_trans_acyclic rel
   1.184 -    handle Graph.CYCLES css => err_cyclic_classes pp css;
   1.185 -
   1.186 -fun merge_classes pp args : classes =
   1.187 -  Graph.merge_trans_acyclic (op =) args
   1.188 -    handle Graph.DUPS cs => err_dup_classes cs
   1.189 -        | Graph.CYCLES css => err_cyclic_classes pp css;
   1.190 -
   1.191 -end;
   1.192 +  in classes'' end);
   1.193  
   1.194  
   1.195  (* arities *)
   1.196 @@ -195,12 +208,12 @@
   1.197      Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n  " ^
   1.198      Pretty.string_of_arity pp (t, Ss', [c']));
   1.199  
   1.200 -fun coregular pp C t (c, (c0, Ss)) ars =
   1.201 +fun coregular pp algebra t (c, (c0, Ss)) ars =
   1.202    let
   1.203      fun conflict (c', (_, Ss')) =
   1.204 -      if class_le C (c, c') andalso not (sorts_le C (Ss, Ss')) then
   1.205 +      if class_le algebra (c, c') andalso not (sorts_le algebra (Ss, Ss')) then
   1.206          SOME ((c, c'), (c', Ss'))
   1.207 -      else if class_le C (c', c) andalso not (sorts_le C (Ss', Ss)) then
   1.208 +      else if class_le algebra (c', c) andalso not (sorts_le algebra (Ss', Ss)) then
   1.209          SOME ((c', c), (c', Ss'))
   1.210        else NONE;
   1.211    in
   1.212 @@ -209,41 +222,63 @@
   1.213      | NONE => (c, (c0, Ss)) :: ars)
   1.214    end;
   1.215  
   1.216 -fun insert pp C t (c, (c0, Ss)) ars =
   1.217 +fun complete algebra (c0, Ss) = map (rpair (c0, Ss)) (c0 :: super_classes algebra c0);
   1.218 +
   1.219 +fun insert pp algebra t (c, (c0, Ss)) ars =
   1.220    (case AList.lookup (op =) ars c of
   1.221 -    NONE => coregular pp C t (c, (c0, Ss)) ars
   1.222 +    NONE => coregular pp algebra t (c, (c0, Ss)) ars
   1.223    | SOME (_, Ss') =>
   1.224 -      if sorts_le C (Ss, Ss') then ars
   1.225 -      else if sorts_le C (Ss', Ss) then
   1.226 -        coregular pp C t (c, (c0, Ss))
   1.227 +      if sorts_le algebra (Ss, Ss') then ars
   1.228 +      else if sorts_le algebra (Ss', Ss) then
   1.229 +        coregular pp algebra t (c, (c0, Ss))
   1.230            (filter_out (fn (c'', (_, Ss'')) => c = c'' andalso Ss'' = Ss') ars)
   1.231        else err_conflict pp t NONE (c, Ss) (c, Ss'));
   1.232  
   1.233 -fun complete C (c0, Ss) = map (rpair (c0, Ss)) (Graph.all_succs C [c0]);
   1.234 +fun insert_ars pp algebra (t, ars) arities =
   1.235 +  let val ars' =
   1.236 +    Symtab.lookup_list arities t
   1.237 +    |> fold_rev (fold_rev (insert pp algebra t)) (map (complete algebra) ars)
   1.238 +  in Symtab.update (t, ars') arities end;
   1.239  
   1.240  in
   1.241  
   1.242 -fun add_arities pp classes (t, ars) arities =
   1.243 -  let val ars' =
   1.244 -    Symtab.lookup_list arities t
   1.245 -    |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars)
   1.246 -  in Symtab.update (t, ars') arities end;
   1.247 -
   1.248 -fun add_arities_table pp classes =
   1.249 -  Symtab.fold (fn (t, ars) => add_arities pp classes (t, map snd ars));
   1.250 +fun add_arities pp arg algebra = algebra |> map_arities (insert_ars pp algebra arg);
   1.251  
   1.252 -fun rebuild_arities pp classes arities =
   1.253 -  Symtab.empty
   1.254 -  |> add_arities_table pp classes arities;
   1.255 -
   1.256 -fun merge_arities pp classes (arities1, arities2) =
   1.257 -  Symtab.empty
   1.258 -  |> add_arities_table pp classes arities1
   1.259 -  |> add_arities_table pp classes arities2;
   1.260 +fun add_arities_table pp algebra =
   1.261 +  Symtab.fold (fn (t, ars) => insert_ars pp algebra (t, map snd ars));
   1.262  
   1.263  end;
   1.264  
   1.265  
   1.266 +(* classrel *)
   1.267 +
   1.268 +fun rebuild_arities pp algebra = algebra |> map_arities (fn arities =>
   1.269 +  Symtab.empty
   1.270 +  |> add_arities_table pp algebra arities);
   1.271 +
   1.272 +fun add_classrel pp rel = rebuild_arities pp o map_classes (fn classes =>
   1.273 +  classes |> Graph.add_edge_trans_acyclic rel
   1.274 +    handle Graph.CYCLES css => err_cyclic_classes pp css);
   1.275 +
   1.276 +
   1.277 +(* empty and merge *)
   1.278 +
   1.279 +val empty_algebra = make_algebra (Graph.empty, Symtab.empty);
   1.280 +
   1.281 +fun merge_algebra pp
   1.282 +   (Algebra {classes = classes1, arities = arities1},
   1.283 +    Algebra {classes = classes2, arities = arities2}) =
   1.284 +  let
   1.285 +    val classes' = Graph.merge_trans_acyclic (op =) (classes1, classes2)
   1.286 +      handle Graph.DUPS cs => err_dup_classes cs
   1.287 +          | Graph.CYCLES css => err_cyclic_classes pp css;
   1.288 +    val algebra0 = make_algebra (classes', Symtab.empty);
   1.289 +    val arities' = Symtab.empty
   1.290 +      |> add_arities_table pp algebra0 arities1
   1.291 +      |> add_arities_table pp algebra0 arities2;
   1.292 +  in make_algebra (classes', arities') end;
   1.293 +
   1.294 +
   1.295  
   1.296  (** sorts of types **)
   1.297  
   1.298 @@ -261,13 +296,14 @@
   1.299  
   1.300  (* mg_domain *)
   1.301  
   1.302 -fun mg_domain (classes, arities) a S =
   1.303 +fun mg_domain algebra a S =
   1.304    let
   1.305 +    val arities = arities_of algebra;
   1.306      fun dom c =
   1.307        (case AList.lookup (op =) (Symtab.lookup_list arities a) c of
   1.308          NONE => raise CLASS_ERROR (NoArity (a, c))
   1.309        | SOME (_, Ss) => Ss);
   1.310 -    fun dom_inter c Ss = ListPair.map (inter_sort classes) (dom c, Ss);
   1.311 +    fun dom_inter c Ss = ListPair.map (inter_sort algebra) (dom c, Ss);
   1.312    in
   1.313      (case S of
   1.314        [] => raise Fail "Unknown domain of empty intersection"
   1.315 @@ -277,13 +313,13 @@
   1.316  
   1.317  (* of_sort *)
   1.318  
   1.319 -fun of_sort (classes, arities) =
   1.320 +fun of_sort algebra =
   1.321    let
   1.322      fun ofS (_, []) = true
   1.323 -      | ofS (TFree (_, S), S') = sort_le classes (S, S')
   1.324 -      | ofS (TVar (_, S), S') = sort_le classes (S, S')
   1.325 +      | ofS (TFree (_, S), S') = sort_le algebra (S, S')
   1.326 +      | ofS (TVar (_, S), S') = sort_le algebra (S, S')
   1.327        | ofS (Type (a, Ts), S) =
   1.328 -          let val Ss = mg_domain (classes, arities) a S in
   1.329 +          let val Ss = mg_domain algebra a S in
   1.330              ListPair.all ofS (Ts, Ss)
   1.331            end handle CLASS_ERROR _ => false;
   1.332    in ofS end;
   1.333 @@ -291,8 +327,9 @@
   1.334  
   1.335  (* of_sort_derivation *)
   1.336  
   1.337 -fun of_sort_derivation pp (classes, arities) {classrel, constructor, variable} =
   1.338 +fun of_sort_derivation pp algebra {classrel, constructor, variable} =
   1.339    let
   1.340 +    val {classes, arities} = rep_algebra algebra;
   1.341      fun weaken_path (x, c1 :: c2 :: cs) = weaken_path (classrel (x, c1) c2, c2 :: cs)
   1.342        | weaken_path (x, _) = x;
   1.343      fun weaken (x, c1) c2 =
   1.344 @@ -301,7 +338,7 @@
   1.345        | cs :: _ => weaken_path (x, cs));
   1.346  
   1.347      fun weakens S1 S2 = S2 |> map (fn c2 =>
   1.348 -      (case S1 |> find_first (fn (_, c1) => class_le classes (c1, c2)) of
   1.349 +      (case S1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of
   1.350          SOME d1 => weaken d1 c2
   1.351        | NONE => error ("Cannot derive subsort relation " ^
   1.352            Pretty.string_of_sort pp (map #2 S1) ^ " < " ^ Pretty.string_of_sort pp S2)));
   1.353 @@ -309,7 +346,7 @@
   1.354      fun derive _ [] = []
   1.355        | derive (Type (a, Ts)) S =
   1.356            let
   1.357 -            val Ss = mg_domain (classes, arities) a S;
   1.358 +            val Ss = mg_domain algebra a S;
   1.359              val dom = map2 (fn T => fn S => derive T S ~~ S) Ts Ss;
   1.360            in
   1.361              S |> map (fn c =>
   1.362 @@ -324,12 +361,12 @@
   1.363  
   1.364  (* witness_sorts *)
   1.365  
   1.366 -fun witness_sorts (classes, arities) types hyps sorts =
   1.367 +fun witness_sorts algebra types hyps sorts =
   1.368    let
   1.369 -    fun le S1 S2 = sort_le classes (S1, S2);
   1.370 +    fun le S1 S2 = sort_le algebra (S1, S2);
   1.371      fun get_solved S2 (T, S1) = if le S1 S2 then SOME (T, S2) else NONE;
   1.372      fun get_hyp S2 S1 = if le S1 S2 then SOME (TFree ("'hyp", S1), S2) else NONE;
   1.373 -    fun mg_dom t S = SOME (mg_domain (classes, arities) t S) handle CLASS_ERROR _ => NONE;
   1.374 +    fun mg_dom t S = SOME (mg_domain algebra t S) handle CLASS_ERROR _ => NONE;
   1.375  
   1.376      fun witn_sort _ [] solved_failed = (SOME (propT, []), solved_failed)
   1.377        | witn_sort path S (solved, failed) =