build classes/arities: refer to operations in sorts.ML;
authorwenzelm
Sun Apr 30 22:50:09 2006 +0200 (2006-04-30 ago)
changeset 195159f650083da65
parent 19514 1f0218dab849
child 19516 dcc4b1d5b732
build classes/arities: refer to operations in sorts.ML;
simplified add_class/classrel/arity;
tuned;
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Sun Apr 30 22:50:08 2006 +0200
     1.2 +++ b/src/Pure/type.ML	Sun Apr 30 22:50:09 2006 +0200
     1.3 @@ -65,15 +65,15 @@
     1.4    val eq_type: tyenv -> typ * typ -> bool
     1.5  
     1.6    (*extend and merge type signatures*)
     1.7 -  val add_classes: Pretty.pp -> NameSpace.naming -> (bstring * class list) list -> tsig -> tsig
     1.8 +  val add_class: Pretty.pp -> NameSpace.naming -> bstring * class list -> tsig -> tsig
     1.9    val hide_classes: bool -> string list -> tsig -> tsig
    1.10 -  val add_classrel: Pretty.pp -> (class * class) list -> tsig -> tsig
    1.11    val set_defsort: sort -> tsig -> tsig
    1.12    val add_types: NameSpace.naming -> (bstring * int) list -> tsig -> tsig
    1.13    val add_abbrevs: NameSpace.naming -> (string * string list * typ) list -> tsig -> tsig
    1.14    val add_nonterminals: NameSpace.naming -> string list -> tsig -> tsig
    1.15    val hide_types: bool -> string list -> tsig -> tsig
    1.16 -  val add_arities: Pretty.pp -> arity list -> tsig -> tsig
    1.17 +  val add_arity: Pretty.pp -> arity -> tsig -> tsig
    1.18 +  val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
    1.19    val merge_tsigs: Pretty.pp -> tsig * tsig -> tsig
    1.20  end;
    1.21  
    1.22 @@ -140,8 +140,12 @@
    1.23  fun of_sort (TSig {classes, arities, ...}) = Sorts.of_sort (#2 classes, arities);
    1.24  fun inter_sort (TSig {classes, ...}) = Sorts.inter_sort (#2 classes);
    1.25  
    1.26 -fun cert_class (TSig {classes, ...}) = Sorts.certify_class (#2 classes);
    1.27 -fun cert_sort (TSig {classes, ...}) = Sorts.certify_sort (#2 classes);
    1.28 +fun cert_class (TSig {classes, ...}) c =
    1.29 +  if can (Graph.get_node (#2 classes)) c then c
    1.30 +  else raise TYPE ("Undeclared class: " ^ quote c, [], []);
    1.31 +
    1.32 +fun cert_sort (tsig as TSig {classes, ...}) =
    1.33 +  Sorts.norm_sort (#2 classes) o map (cert_class tsig);
    1.34  
    1.35  fun witness_sorts (tsig as TSig {classes, arities, log_types, ...}) =
    1.36    Sorts.witness_sorts (#2 classes, arities) log_types;
    1.37 @@ -160,7 +164,7 @@
    1.38  
    1.39  fun certify_typ normalize syntax tsig ty =
    1.40    let
    1.41 -    val TSig {classes = (_, classes), types = (_, types), ...} = tsig;
    1.42 +    val TSig {types = (_, types), ...} = tsig;
    1.43      fun err msg = raise TYPE (msg, [ty], []);
    1.44  
    1.45      val check_syntax =
    1.46 @@ -181,11 +185,11 @@
    1.47              | SOME (Nonterminal, _) => (nargs 0; check_syntax c; T)
    1.48              | NONE => err (undecl_type c))
    1.49            end
    1.50 -      | cert (TFree (x, S)) = TFree (x, Sorts.certify_sort classes S)
    1.51 +      | cert (TFree (x, S)) = TFree (x, cert_sort tsig S)
    1.52        | cert (TVar (xi as (_, i), S)) =
    1.53            if i < 0 then
    1.54              err ("Malformed type variable: " ^ quote (Term.string_of_vname xi))
    1.55 -          else TVar (xi, Sorts.certify_sort classes S);
    1.56 +          else TVar (xi, cert_sort tsig S);
    1.57  
    1.58      val ty' = cert ty;
    1.59    in if ty = ty' then ty else ty' end;  (*avoid copying of already normal type*)
    1.60 @@ -463,96 +467,8 @@
    1.61  
    1.62  (** extend and merge type signatures **)
    1.63  
    1.64 -(* arities *)
    1.65 -
    1.66 -local
    1.67 -
    1.68 -fun err_decl t decl = error ("Illegal " ^ str_of_decl decl ^ ": " ^ quote t);
    1.69 -
    1.70 -fun for_classes _ NONE = ""
    1.71 -  | for_classes pp (SOME (c1, c2)) =
    1.72 -      " for classes " ^ Pretty.string_of_classrel pp [c1, c2];
    1.73 -
    1.74 -fun err_conflict pp t cc (c, Ss) (c', Ss') =
    1.75 -  error ("Conflict of type arities" ^ for_classes pp cc ^ ":\n  " ^
    1.76 -    Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n  " ^
    1.77 -    Pretty.string_of_arity pp (t, Ss', [c']));
    1.78 -
    1.79 -fun coregular pp C t (c, Ss) ars =
    1.80 -  let
    1.81 -    fun conflict (c', Ss') =
    1.82 -      if Sorts.class_le C (c, c') andalso not (Sorts.sorts_le C (Ss, Ss')) then
    1.83 -        SOME ((c, c'), (c', Ss'))
    1.84 -      else if Sorts.class_le C (c', c) andalso not (Sorts.sorts_le C (Ss', Ss)) then
    1.85 -        SOME ((c', c), (c', Ss'))
    1.86 -      else NONE;
    1.87 -  in
    1.88 -    (case Library.get_first conflict ars of
    1.89 -      SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss')
    1.90 -    | NONE => (c, Ss) :: ars)
    1.91 -  end;
    1.92 -
    1.93 -fun insert pp C t (c, Ss) ars =
    1.94 -  (case AList.lookup (op =) ars c of
    1.95 -    NONE => coregular pp C t (c, Ss) ars
    1.96 -  | SOME Ss' =>
    1.97 -      if Sorts.sorts_le C (Ss, Ss') then ars
    1.98 -      else if Sorts.sorts_le C (Ss', Ss)
    1.99 -      then coregular pp C t (c, Ss) (remove (op =) (c, Ss') ars)
   1.100 -      else err_conflict pp t NONE (c, Ss) (c, Ss'));
   1.101 -
   1.102 -fun complete C (c, Ss) = map (rpair Ss) (Graph.all_succs C [c]);
   1.103 -
   1.104 -fun insert_arities pp classes (t, ars) arities =
   1.105 -  let val ars' =
   1.106 -    Symtab.lookup_list arities t
   1.107 -    |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars)
   1.108 -  in Symtab.update (t, ars') arities end;
   1.109 -
   1.110 -fun insert_table pp classes = Symtab.fold (fn (t, ars) =>
   1.111 -  insert_arities pp classes (t, map (apsnd (map (Sorts.norm_sort classes))) ars));
   1.112 -
   1.113 -in
   1.114 -
   1.115 -fun add_arities pp decls tsig = tsig |> map_tsig (fn (classes, default, types, arities) =>
   1.116 -  let
   1.117 -    fun prep (t, Ss, S) =
   1.118 -      (case Symtab.lookup (snd types) t of
   1.119 -        SOME (LogicalType n, _) =>
   1.120 -          if length Ss = n then
   1.121 -            (t, map (cert_sort tsig) Ss, cert_sort tsig S)
   1.122 -              handle TYPE (msg, _, _) => error msg
   1.123 -          else error (bad_nargs t)
   1.124 -      | SOME (decl, _) => err_decl t decl
   1.125 -      | NONE => error (undecl_type t));
   1.126 -
   1.127 -    val ars = decls |> map ((fn (t, Ss, S) => (t, map (fn c => (c, Ss)) S)) o prep);
   1.128 -    val arities' = fold (insert_arities pp (snd classes)) ars arities;
   1.129 -  in (classes, default, types, arities') end);
   1.130 -
   1.131 -fun rebuild_arities pp classes arities =
   1.132 -  Symtab.empty
   1.133 -  |> insert_table pp classes arities;
   1.134 -
   1.135 -fun merge_arities pp classes (arities1, arities2) =
   1.136 -  Symtab.empty
   1.137 -  |> insert_table pp classes arities1
   1.138 -  |> insert_table pp classes arities2;
   1.139 -
   1.140 -end;
   1.141 -
   1.142 -
   1.143  (* classes *)
   1.144  
   1.145 -local
   1.146 -
   1.147 -fun err_dup_classes cs =
   1.148 -  error ("Duplicate declaration of class(es): " ^ commas_quote cs);
   1.149 -
   1.150 -fun err_cyclic_classes pp css =
   1.151 -  error (cat_lines (map (fn cs =>
   1.152 -    "Cycle in class relation: " ^ Pretty.string_of_classrel pp cs) css));
   1.153 -
   1.154  fun add_class pp naming (c, cs) tsig =
   1.155    tsig |> map_tsig (fn ((space, classes), default, types, arities) =>
   1.156      let
   1.157 @@ -560,42 +476,41 @@
   1.158        val cs' = map (cert_class tsig) cs
   1.159          handle TYPE (msg, _, _) => error msg;
   1.160        val space' = space |> NameSpace.declare naming c';
   1.161 -      val classes' = classes |> Graph.new_node (c', stamp ())
   1.162 -        handle Graph.DUP dup => err_dup_classes [dup];
   1.163 -      val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c') cs')
   1.164 -        handle Graph.CYCLES css => err_cyclic_classes pp css;
   1.165 -    in ((space', classes''), default, types, arities) end);
   1.166 -
   1.167 -in
   1.168 -
   1.169 -val add_classes = fold oo add_class;
   1.170 -
   1.171 -fun add_classrel pp ps tsig =
   1.172 -  tsig |> map_tsig (fn ((space, classes), default, types, arities) =>
   1.173 -    let
   1.174 -      val ps' = map (pairself (cert_class tsig)) ps
   1.175 -        handle TYPE (msg, _, _) => error msg;
   1.176 -      val classes' = classes |> fold Graph.add_edge_trans_acyclic ps'
   1.177 -        handle Graph.CYCLES css => err_cyclic_classes pp css;
   1.178 -      val default' = default |> Sorts.norm_sort classes';
   1.179 -      val arities' = arities |> rebuild_arities pp classes';
   1.180 -    in ((space, classes'), default', types, arities') end);
   1.181 -
   1.182 -fun merge_classes pp ((space1, classes1), (space2, classes2)) =
   1.183 -  let
   1.184 -    val space = NameSpace.merge (space1, space2);
   1.185 -    val classes =
   1.186 -      Graph.merge_trans_acyclic (op =) (classes1, classes2)
   1.187 -        handle Graph.DUPS cs => err_dup_classes cs
   1.188 -          | Graph.CYCLES css => err_cyclic_classes pp css;
   1.189 -  in (space, classes) end;
   1.190 -
   1.191 -end;
   1.192 +      val classes' = classes |> Sorts.add_class pp (c', cs');
   1.193 +    in ((space', classes'), default, types, arities) end);
   1.194  
   1.195  fun hide_classes fully cs = map_tsig (fn ((space, classes), default, types, arities) =>
   1.196    ((fold (NameSpace.hide fully) cs space, classes), default, types, arities));
   1.197  
   1.198  
   1.199 +(* arities *)
   1.200 +
   1.201 +fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn (classes, default, types, arities) =>
   1.202 +  let
   1.203 +    val _ =
   1.204 +      (case Symtab.lookup (#2 types) t of
   1.205 +        SOME (LogicalType n, _) => if length Ss <> n then error (bad_nargs t) else ()
   1.206 +      | SOME (decl, _) => error ("Illegal " ^ str_of_decl decl ^ ": " ^ quote t)
   1.207 +      | NONE => error (undecl_type t));
   1.208 +    val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
   1.209 +      handle TYPE (msg, _, _) => error msg;
   1.210 +    val arities' = arities |> Sorts.add_arities pp (#2 classes) ((t, map (fn c' => (c', Ss')) S'));
   1.211 +  in (classes, default, types, arities') end);
   1.212 +
   1.213 +
   1.214 +(* classrel *)
   1.215 +
   1.216 +fun add_classrel pp rel tsig =
   1.217 +  tsig |> map_tsig (fn ((space, classes), default, types, arities) =>
   1.218 +    let
   1.219 +      val rel' = pairself (cert_class tsig) rel
   1.220 +        handle TYPE (msg, _, _) => error msg;
   1.221 +      val classes' = classes |> Sorts.add_classrel pp rel;
   1.222 +      val default' = default |> Sorts.norm_sort classes';
   1.223 +      val arities' = arities |> Sorts.rebuild_arities pp classes';
   1.224 +    in ((space, classes'), default', types, arities') end);
   1.225 +
   1.226 +
   1.227  (* default sort *)
   1.228  
   1.229  fun set_defsort S tsig = tsig |> map_tsig (fn (classes, _, types, arities) =>
   1.230 @@ -673,15 +588,16 @@
   1.231  
   1.232  fun merge_tsigs pp (tsig1, tsig2) =
   1.233    let
   1.234 -    val (TSig {classes = classes1, default = default1, types = types1, arities = arities1,
   1.235 -      log_types = _, witness = _}) = tsig1;
   1.236 -    val (TSig {classes = classes2, default = default2, types = types2, arities = arities2,
   1.237 -      log_types = _, witness = _}) = tsig2;
   1.238 +    val (TSig {classes = (space1, classes1), default = default1, types = types1,
   1.239 +      arities = arities1, log_types = _, witness = _}) = tsig1;
   1.240 +    val (TSig {classes = (space2, classes2), default = default2, types = types2,
   1.241 +      arities = arities2, log_types = _, witness = _}) = tsig2;
   1.242  
   1.243 -    val classes' = merge_classes pp (classes1, classes2);
   1.244 -    val default' = Sorts.inter_sort (#2 classes') (default1, default2);
   1.245 +    val space' = NameSpace.merge (space1, space2);
   1.246 +    val classes' = Sorts.merge_classes pp (classes1, classes2);
   1.247 +    val default' = Sorts.inter_sort classes' (default1, default2);
   1.248      val types' = merge_types (types1, types2);
   1.249 -    val arities' = merge_arities pp (#2 classes') (arities1, arities2);
   1.250 -  in build_tsig (classes', default', types', arities') end;
   1.251 +    val arities' = Sorts.merge_arities pp classes' (arities1, arities2);
   1.252 +  in build_tsig ((space', classes'), default', types', arities') end;
   1.253  
   1.254  end;