1.1 --- a/src/Pure/type.ML Sat May 29 15:05:02 2004 +0200
1.2 +++ b/src/Pure/type.ML Sat May 29 15:05:25 2004 +0200
1.3 @@ -32,7 +32,6 @@
1.4 val cert_class: tsig -> class -> class
1.5 val cert_sort: tsig -> sort -> sort
1.6 val witness_sorts: tsig -> sort list -> sort list -> (typ * sort) list
1.7 - val norm_typ: tsig -> typ -> typ
1.8 val cert_typ: tsig -> typ -> typ
1.9 val cert_typ_syntax: tsig -> typ -> typ
1.10 val cert_typ_raw: tsig -> typ -> typ
1.11 @@ -47,8 +46,8 @@
1.12 val freeze_thaw : term -> term * (term -> term)
1.13
1.14 (*matching and unification*)
1.15 - val inst_term_tvars: tsig -> (indexname * typ) list -> term -> term
1.16 - val inst_typ_tvars: tsig -> (indexname * typ) list -> typ -> typ
1.17 + val inst_typ_tvars: Pretty.pp -> tsig -> (indexname * typ) list -> typ -> typ
1.18 + val inst_term_tvars: Pretty.pp -> tsig -> (indexname * typ) list -> term -> term
1.19 exception TYPE_MATCH
1.20 val typ_match: tsig -> typ Vartab.table * (typ * typ) -> typ Vartab.table
1.21 val typ_instance: tsig -> typ * typ -> bool
1.22 @@ -57,14 +56,14 @@
1.23 val raw_unify: typ * typ -> bool
1.24
1.25 (*extend and merge type signatures*)
1.26 - val add_classes: (class * class list) list -> tsig -> tsig
1.27 - val add_classrel: (class * class) list -> tsig -> tsig
1.28 + val add_classes: Pretty.pp -> (class * class list) list -> tsig -> tsig
1.29 + val add_classrel: Pretty.pp -> (class * class) list -> tsig -> tsig
1.30 val set_defsort: sort -> tsig -> tsig
1.31 val add_types: (string * int) list -> tsig -> tsig
1.32 val add_abbrs: (string * string list * typ) list -> tsig -> tsig
1.33 val add_nonterminals: string list -> tsig -> tsig
1.34 - val add_arities: (string * sort list * sort) list -> tsig -> tsig
1.35 - val merge_tsigs: tsig * tsig -> tsig
1.36 + val add_arities: Pretty.pp -> arity list -> tsig -> tsig
1.37 + val merge_tsigs: Pretty.pp -> tsig * tsig -> tsig
1.38 end;
1.39
1.40 structure Type: TYPE =
1.41 @@ -147,6 +146,9 @@
1.42 (* certified types *)
1.43
1.44 fun bad_nargs t = "Bad number of arguments for type constructor: " ^ quote t;
1.45 +fun undecl_type c = "Undeclared type constructor: " ^ quote c;
1.46 +
1.47 +local
1.48
1.49 fun inst_typ tye =
1.50 let
1.51 @@ -156,7 +158,6 @@
1.52 | None => TVar var);
1.53 in map_type_tvar inst end;
1.54
1.55 -(*expand type abbreviations and normalize sorts*)
1.56 fun norm_typ (tsig as TSig {types, ...}) ty =
1.57 let
1.58 val idx = Term.maxidx_of_typ ty + 1;
1.59 @@ -172,7 +173,6 @@
1.60 val ty' = norm ty;
1.61 in if ty = ty' then ty else ty' end; (*avoid copying of already normal type*)
1.62
1.63 -(*check validity of (not necessarily normal) type*) (*exception TYPE*)
1.64 fun certify_typ normalize syntax tsig ty =
1.65 let
1.66 val TSig {types, ...} = tsig;
1.67 @@ -186,7 +186,7 @@
1.68 Some (LogicalType n, _) => nargs n
1.69 | Some (Abbreviation (vs, _), _) => nargs (length vs)
1.70 | Some (Nonterminal, _) => nargs 0
1.71 - | None => err ("Undeclared type constructor: " ^ quote c));
1.72 + | None => err (undecl_type c));
1.73 seq check_typ Ts
1.74 end
1.75 | check_typ (TFree (_, S)) = check_sort S
1.76 @@ -206,10 +206,13 @@
1.77 val _ = if not syntax then no_syntax ty' else ();
1.78 in ty' end;
1.79
1.80 +in
1.81 +
1.82 val cert_typ = certify_typ true false;
1.83 val cert_typ_syntax = certify_typ true true;
1.84 val cert_typ_raw = certify_typ false true;
1.85
1.86 +end;
1.87
1.88
1.89 (** special treatment of type vars **)
1.90 @@ -226,7 +229,7 @@
1.91 fun no_tvars T =
1.92 (case typ_tvars T of [] => T
1.93 | vs => raise TYPE ("Illegal schematic type variable(s): " ^
1.94 - commas (map (Term.string_of_vname o #1) vs), [T], []));
1.95 + commas_quote (map (Term.string_of_vname o #1) vs), [T], []));
1.96
1.97
1.98 (* varify, unvarify *)
1.99 @@ -263,7 +266,7 @@
1.100 raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []);
1.101
1.102 fun thaw_one alist (a,sort) = TVar (the (assoc (alist,a)), sort)
1.103 - handle OPTION => TFree(a,sort);
1.104 + handle OPTION => TFree(a, sort);
1.105
1.106 in
1.107
1.108 @@ -295,20 +298,20 @@
1.109
1.110 (* instantiation *)
1.111
1.112 -fun type_of_sort tsig (T, S) =
1.113 +fun type_of_sort pp tsig (T, S) =
1.114 if of_sort tsig (T, S) then T
1.115 - else raise TYPE ("Type not of sort " ^ Sorts.str_of_sort S, [T], []);
1.116 + else raise TYPE ("Type not of sort " ^ Pretty.string_of_sort pp S, [T], []);
1.117
1.118 -fun inst_typ_tvars tsig tye =
1.119 +fun inst_typ_tvars pp tsig tye =
1.120 let
1.121 fun inst (var as (v, S)) =
1.122 (case assoc_string_int (tye, v) of
1.123 - Some U => type_of_sort tsig (U, S)
1.124 + Some U => type_of_sort pp tsig (U, S)
1.125 | None => TVar var);
1.126 in map_type_tvar inst end;
1.127
1.128 -fun inst_term_tvars _ [] t = t
1.129 - | inst_term_tvars tsig tye t = map_term_types (inst_typ_tvars tsig tye) t;
1.130 +fun inst_term_tvars _ _ [] t = t
1.131 + | inst_term_tvars pp tsig tye t = map_term_types (inst_typ_tvars pp tsig tye) t;
1.132
1.133
1.134 (* matching *)
1.135 @@ -319,7 +322,7 @@
1.136 let
1.137 fun match (subs, (TVar (v, S), T)) =
1.138 (case Vartab.lookup (subs, v) of
1.139 - None => (Vartab.update_new ((v, type_of_sort tsig (T, S)), subs)
1.140 + None => (Vartab.update_new ((v, type_of_sort Pretty.pp_undef tsig (T, S)), subs)
1.141 handle TYPE _ => raise TYPE_MATCH)
1.142 | Some U => if U = T then subs else raise TYPE_MATCH)
1.143 | match (subs, (Type (a, Ts), Type (b, Us))) =
1.144 @@ -417,14 +420,17 @@
1.145 local
1.146
1.147 fun err_decl t decl = error ("Illegal " ^ str_of_decl decl ^ ": " ^ quote t);
1.148 -fun err_undecl t = error ("Undeclared type constructor: " ^ quote t);
1.149
1.150 -fun err_conflict t (c1, c2) (c, Ss) (c', Ss') =
1.151 - error ("Conflict of type arities for classes " ^ quote c1 ^ " < " ^ quote c2 ^ ":\n " ^
1.152 - Sorts.str_of_arity (t, Ss, [c]) ^ " and\n " ^
1.153 - Sorts.str_of_arity (t, Ss', [c']));
1.154 +fun for_classes _ None = ""
1.155 + | for_classes pp (Some (c1, c2)) =
1.156 + " for classes " ^ Pretty.string_of_classrel pp [c1, c2];
1.157
1.158 -fun coregular C t (c, Ss) ars =
1.159 +fun err_conflict pp t cc (c, Ss) (c', Ss') =
1.160 + error ("Conflict of type arities" ^ for_classes pp cc ^ ":\n " ^
1.161 + Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n " ^
1.162 + Pretty.string_of_arity pp (t, Ss', [c']));
1.163 +
1.164 +fun coregular pp C t (c, Ss) ars =
1.165 let
1.166 fun conflict (c', Ss') =
1.167 if Sorts.class_le C (c, c') andalso not (Sorts.sorts_le C (Ss, Ss')) then
1.168 @@ -434,33 +440,33 @@
1.169 else None;
1.170 in
1.171 (case Library.get_first conflict ars of
1.172 - Some ((c1, c2), (c', Ss')) => err_conflict t (c1, c2) (c, Ss) (c', Ss')
1.173 + Some ((c1, c2), (c', Ss')) => err_conflict pp t (Some (c1, c2)) (c, Ss) (c', Ss')
1.174 | None => (c, Ss) :: ars)
1.175 end;
1.176
1.177 -fun insert C t ((c, Ss), ars) =
1.178 +fun insert pp C t ((c, Ss), ars) =
1.179 (case assoc_string (ars, c) of
1.180 - None => coregular C t (c, Ss) ars
1.181 + None => coregular pp C t (c, Ss) ars
1.182 | Some Ss' =>
1.183 if Sorts.sorts_le C (Ss, Ss') then ars
1.184 else if Sorts.sorts_le C (Ss', Ss)
1.185 - then coregular C t (c, Ss) (ars \ (c, Ss'))
1.186 - else coregular C t (c, Ss) ars);
1.187 + then coregular pp C t (c, Ss) (ars \ (c, Ss'))
1.188 + else err_conflict pp t None (c, Ss) (c, Ss'));
1.189
1.190 fun complete C (c, Ss) = map (rpair Ss) (Graph.all_succs C [c]);
1.191
1.192 -fun insert_arities classes (arities, (t, ars)) =
1.193 +fun insert_arities pp classes (arities, (t, ars)) =
1.194 let val ars' =
1.195 Symtab.lookup_multi (arities, t)
1.196 - |> curry (foldr (insert classes t)) (flat (map (complete classes) ars))
1.197 + |> curry (foldr (insert pp classes t)) (flat (map (complete classes) ars))
1.198 in Symtab.update ((t, ars'), arities) end;
1.199
1.200 -fun insert_table classes = Symtab.foldl (fn (arities, (t, ars)) =>
1.201 - insert_arities classes (arities, (t, map (apsnd (map (Sorts.norm_sort classes))) ars)));
1.202 +fun insert_table pp classes = Symtab.foldl (fn (arities, (t, ars)) =>
1.203 + insert_arities pp classes (arities, (t, map (apsnd (map (Sorts.norm_sort classes))) ars)));
1.204
1.205 in
1.206
1.207 -fun add_arities decls tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
1.208 +fun add_arities pp decls tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
1.209 let
1.210 fun prep (t, Ss, S) =
1.211 (case Symtab.lookup (types, t) of
1.212 @@ -470,17 +476,17 @@
1.213 handle TYPE (msg, _, _) => error msg
1.214 else error (bad_nargs t)
1.215 | Some (decl, _) => err_decl t decl
1.216 - | None => err_undecl t);
1.217 + | None => error (undecl_type t));
1.218
1.219 val ars = decls |> map ((fn (t, Ss, S) => (t, map (fn c => (c, Ss)) S)) o prep);
1.220 - val arities' = foldl (insert_arities classes) (arities, ars);
1.221 + val arities' = foldl (insert_arities pp classes) (arities, ars);
1.222 in (classes, default, types, arities') end);
1.223
1.224 -fun rebuild_arities classes arities =
1.225 - insert_table classes (Symtab.empty, arities);
1.226 +fun rebuild_arities pp classes arities =
1.227 + insert_table pp classes (Symtab.empty, arities);
1.228
1.229 -fun merge_arities classes (arities1, arities2) =
1.230 - insert_table classes (insert_table classes (Symtab.empty, arities1), arities2);
1.231 +fun merge_arities pp classes (arities1, arities2) =
1.232 + insert_table pp classes (insert_table pp classes (Symtab.empty, arities1), arities2);
1.233
1.234 end;
1.235
1.236 @@ -492,37 +498,37 @@
1.237 fun err_dup_classes cs =
1.238 error ("Duplicate declaration of class(es): " ^ commas_quote cs);
1.239
1.240 -fun err_cyclic_classes css =
1.241 +fun err_cyclic_classes pp css =
1.242 error (cat_lines (map (fn cs =>
1.243 - "Cycle in class relation: " ^ space_implode " < " (map quote cs)) css));
1.244 + "Cycle in class relation: " ^ Pretty.string_of_classrel pp cs) css));
1.245
1.246 -fun add_class (c, cs) tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
1.247 +fun add_class pp (c, cs) tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
1.248 let
1.249 val cs' = map (cert_class tsig) cs
1.250 handle TYPE (msg, _, _) => error msg;
1.251 val classes' = classes |> Graph.new_node (c, stamp ())
1.252 handle Graph.DUP d => err_dup_classes [d];
1.253 val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs')
1.254 - handle Graph.CYCLES css => err_cyclic_classes css;
1.255 + handle Graph.CYCLES css => err_cyclic_classes pp css;
1.256 in (classes'', default, types, arities) end);
1.257
1.258 in
1.259
1.260 -val add_classes = fold add_class;
1.261 +val add_classes = fold o add_class;
1.262
1.263 -fun add_classrel ps tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
1.264 +fun add_classrel pp ps tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
1.265 let
1.266 val ps' = map (pairself (cert_class tsig)) ps
1.267 handle TYPE (msg, _, _) => error msg;
1.268 val classes' = classes |> fold Graph.add_edge_trans_acyclic ps'
1.269 - handle Graph.CYCLES css => err_cyclic_classes css;
1.270 + handle Graph.CYCLES css => err_cyclic_classes pp css;
1.271 val default' = default |> Sorts.norm_sort classes';
1.272 - val arities' = arities |> rebuild_arities classes';
1.273 + val arities' = arities |> rebuild_arities pp classes';
1.274 in (classes', default', types, arities') end);
1.275
1.276 -fun merge_classes CC = Graph.merge_trans_acyclic (op =) CC
1.277 +fun merge_classes pp CC = Graph.merge_trans_acyclic (op =) CC
1.278 handle Graph.DUPS cs => err_dup_classes cs
1.279 - | Graph.CYCLES css => err_cyclic_classes css;
1.280 + | Graph.CYCLES css => err_cyclic_classes pp css;
1.281
1.282 end;
1.283
1.284 @@ -545,8 +551,9 @@
1.285 val s = str_of_decl decl;
1.286 val s' = str_of_decl decl';
1.287 in
1.288 - if s = s' then error ("Duplicate declaration of " ^ s ^ ": " ^ quote c)
1.289 - else error ("Conflicting declarations of " ^ s ^ " with " ^ s' ^ ": " ^ quote c)
1.290 + if s = s' then
1.291 + error ("Duplicate declaration of " ^ s ^ ": " ^ quote c)
1.292 + else error ("Conflict of " ^ s ^ " with " ^ s' ^ ": " ^ quote c)
1.293 end;
1.294
1.295 fun new_decl (c, decl) types =
1.296 @@ -592,17 +599,17 @@
1.297
1.298 (* merge type signatures *)
1.299
1.300 -fun merge_tsigs (tsig1, tsig2) =
1.301 +fun merge_tsigs pp (tsig1, tsig2) =
1.302 let
1.303 val (TSig {classes = classes1, default = default1, types = types1, arities = arities1,
1.304 log_types = _, witness = _}) = tsig1;
1.305 val (TSig {classes = classes2, default = default2, types = types2, arities = arities2,
1.306 log_types = _, witness = _}) = tsig2;
1.307
1.308 - val classes' = merge_classes (classes1, classes2);
1.309 + val classes' = merge_classes pp (classes1, classes2);
1.310 val default' = Sorts.inter_sort classes' (default1, default2);
1.311 val types' = merge_types (types1, types2);
1.312 - val arities' = merge_arities classes' (arities1, arities2);
1.313 + val arities' = merge_arities pp classes' (arities1, arities2);
1.314 in build_tsig (classes', default', types', arities') end;
1.315
1.316 end;