1(* Title: Pure/type.ML 2 Author: Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel 3 4Type signatures and certified types, special treatment of type vars, 5matching and unification of types, extend and merge type signatures. 6*) 7 8signature TYPE = 9sig 10 (*constraints*) 11 val mark_polymorphic: typ -> typ 12 val constraint: typ -> term -> term 13 val constraint_type: Proof.context -> typ -> typ 14 val strip_constraints: term -> term 15 val appl_error: Proof.context -> term -> typ -> term -> typ -> string 16 (*type signatures and certified types*) 17 datatype decl = 18 LogicalType of int | 19 Abbreviation of string list * typ * bool | 20 Nonterminal 21 type tsig 22 val eq_tsig: tsig * tsig -> bool 23 val rep_tsig: tsig -> 24 {classes: Name_Space.T * Sorts.algebra, 25 default: sort, 26 types: decl Name_Space.table, 27 log_types: string list} 28 val change_base: bool -> tsig -> tsig 29 val change_ignore: tsig -> tsig 30 val empty_tsig: tsig 31 val class_space: tsig -> Name_Space.T 32 val defaultS: tsig -> sort 33 val logical_types: tsig -> string list 34 val eq_sort: tsig -> sort * sort -> bool 35 val subsort: tsig -> sort * sort -> bool 36 val of_sort: tsig -> typ * sort -> bool 37 val inter_sort: tsig -> sort * sort -> sort 38 val cert_class: tsig -> class -> class 39 val cert_sort: tsig -> sort -> sort 40 val minimize_sort: tsig -> sort -> sort 41 val witness_sorts: tsig -> (typ * sort) list -> sort list -> (typ * sort) list 42 type mode 43 val mode_default: mode 44 val mode_syntax: mode 45 val mode_abbrev: mode 46 val get_mode: Proof.context -> mode 47 val set_mode: mode -> Proof.context -> Proof.context 48 val restore_mode: Proof.context -> Proof.context -> Proof.context 49 val type_space: tsig -> Name_Space.T 50 val type_alias: Name_Space.naming -> binding -> string -> tsig -> tsig 51 val check_decl: Context.generic -> tsig -> 52 xstring * Position.T -> (string * Position.report list) * decl 53 val the_decl: tsig -> string * Position.T -> decl 54 val cert_typ_mode: mode -> tsig -> typ -> typ 55 val cert_typ: tsig -> typ -> typ 56 val arity_number: tsig -> string -> int 57 val arity_sorts: Context.generic -> tsig -> string -> sort -> sort list 58 59 (*special treatment of type vars*) 60 val sort_of_atyp: typ -> sort 61 val strip_sorts: typ -> typ 62 val strip_sorts_dummy: typ -> typ 63 val no_tvars: typ -> typ 64 val varify_global: (string * sort) list -> term -> ((string * sort) * indexname) list * term 65 val legacy_freeze_thaw_type: typ -> typ * (typ -> typ) 66 val legacy_freeze_type: typ -> typ 67 val legacy_freeze_thaw: term -> term * (term -> term) 68 val legacy_freeze: term -> term 69 70 (*matching and unification*) 71 exception TYPE_MATCH 72 type tyenv = (sort * typ) Vartab.table 73 val lookup: tyenv -> indexname * sort -> typ option 74 val devar: tyenv -> typ -> typ 75 val typ_match: tsig -> typ * typ -> tyenv -> tyenv 76 val typ_instance: tsig -> typ * typ -> bool 77 val raw_match: typ * typ -> tyenv -> tyenv 78 val raw_matches: typ list * typ list -> tyenv -> tyenv 79 val could_match: typ * typ -> bool 80 val could_matches: typ list * typ list -> bool 81 val raw_instance: typ * typ -> bool 82 exception TUNIFY 83 val unify: tsig -> typ * typ -> tyenv * int -> tyenv * int 84 val raw_unify: typ * typ -> tyenv -> tyenv 85 val raw_unifys: typ list * typ list -> tyenv -> tyenv 86 val could_unify: typ * typ -> bool 87 val could_unifys: typ list * typ list -> bool 88 val unified: tyenv -> typ * typ -> bool 89 90 (*extend and merge type signatures*) 91 val add_class: Context.generic -> binding * class list -> tsig -> tsig 92 val hide_class: bool -> string -> tsig -> tsig 93 val set_defsort: sort -> tsig -> tsig 94 val add_type: Context.generic -> binding * int -> tsig -> tsig 95 val add_abbrev: Context.generic -> binding * string list * typ -> tsig -> tsig 96 val add_nonterminal: Context.generic -> binding -> tsig -> tsig 97 val hide_type: bool -> string -> tsig -> tsig 98 val add_arity: Context.generic -> arity -> tsig -> tsig 99 val add_classrel: Context.generic -> class * class -> tsig -> tsig 100 val merge_tsig: Context.generic -> tsig * tsig -> tsig 101end; 102 103structure Type: TYPE = 104struct 105 106(** constraints **) 107 108(*indicate polymorphic Vars*) 109fun mark_polymorphic T = Type ("_polymorphic_", [T]); 110 111fun constraint T t = 112 if T = dummyT then t 113 else Const ("_type_constraint_", T --> T) $ t; 114 115fun constraint_type ctxt T = 116 let fun err () = error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T); 117 in (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ()) end; 118 119fun strip_constraints (Const ("_type_constraint_", _) $ t) = strip_constraints t 120 | strip_constraints (t $ u) = strip_constraints t $ strip_constraints u 121 | strip_constraints (Abs (x, T, t)) = Abs (x, T, strip_constraints t) 122 | strip_constraints a = a; 123 124fun appl_error ctxt (Const ("_type_constraint_", Type ("fun", [T, _]))) _ u U = 125 cat_lines 126 ["Failed to meet type constraint:", "", 127 Pretty.string_of (Pretty.block 128 [Pretty.str "Term:", Pretty.brk 2, Syntax.pretty_term ctxt u, 129 Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt U]), 130 Pretty.string_of (Pretty.block 131 [Pretty.str "Type:", Pretty.brk 2, Syntax.pretty_typ ctxt T])] 132 | appl_error ctxt t T u U = 133 cat_lines 134 ["Type error in application: " ^ 135 (case T of 136 Type ("fun", _) => "incompatible operand type" 137 | _ => "operator not of function type"), 138 "", 139 Pretty.string_of (Pretty.block 140 [Pretty.str "Operator:", Pretty.brk 2, Syntax.pretty_term ctxt t, 141 Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt T]), 142 Pretty.string_of (Pretty.block 143 [Pretty.str "Operand:", Pretty.brk 3, Syntax.pretty_term ctxt u, 144 Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt U])]; 145 146 147 148(** type signatures and certified types **) 149 150(* type declarations *) 151 152datatype decl = 153 LogicalType of int | 154 Abbreviation of string list * typ * bool | 155 Nonterminal; 156 157 158(* type tsig *) 159 160datatype tsig = 161 TSig of { 162 classes: Name_Space.T * Sorts.algebra, (*order-sorted algebra of type classes*) 163 default: sort, (*default sort on input*) 164 types: decl Name_Space.table, (*declared types*) 165 log_types: string list}; (*logical types sorted by number of arguments*) 166 167fun eq_tsig 168 (TSig {classes = classes1, default = default1, types = types1, log_types = _}, 169 TSig {classes = classes2, default = default2, types = types2, log_types = _}) = 170 pointer_eq (classes1, classes2) andalso 171 default1 = default2 andalso 172 pointer_eq (types1, types2); 173 174fun rep_tsig (TSig comps) = comps; 175 176fun make_tsig (classes, default, types, log_types) = 177 TSig {classes = classes, default = default, types = types, log_types = log_types}; 178 179fun change_base begin (TSig {classes, default, types, log_types}) = 180 make_tsig (classes, default, Name_Space.change_base begin types, log_types); 181 182fun change_ignore (TSig {classes, default, types, log_types}) = 183 make_tsig (classes, default, Name_Space.change_ignore types, log_types); 184 185fun build_tsig (classes, default, types) = 186 let 187 val log_types = 188 Name_Space.fold_table (fn (c, LogicalType n) => cons (c, n) | _ => I) types [] 189 |> Library.sort (int_ord o apply2 snd) |> map fst; 190 in make_tsig (classes, default, types, log_types) end; 191 192fun map_tsig f (TSig {classes, default, types, log_types = _}) = 193 build_tsig (f (classes, default, types)); 194 195val empty_tsig = 196 build_tsig ((Name_Space.empty Markup.classN, Sorts.empty_algebra), [], 197 Name_Space.empty_table Markup.type_nameN); 198 199 200(* classes and sorts *) 201 202val class_space = #1 o #classes o rep_tsig; 203 204fun defaultS (TSig {default, ...}) = default; 205fun logical_types (TSig {log_types, ...}) = log_types; 206 207fun eq_sort (TSig {classes, ...}) = Sorts.sort_eq (#2 classes); 208fun subsort (TSig {classes, ...}) = Sorts.sort_le (#2 classes); 209fun of_sort (TSig {classes, ...}) = Sorts.of_sort (#2 classes); 210fun inter_sort (TSig {classes, ...}) = Sorts.inter_sort (#2 classes); 211 212fun cert_class (TSig {classes = (_, algebra), ...}) c = 213 if can (Graph.get_entry (Sorts.classes_of algebra)) c then c 214 else raise TYPE ("Undeclared class: " ^ quote c, [], []); 215 216val cert_sort = map o cert_class; 217 218fun minimize_sort (TSig {classes, ...}) = Sorts.minimize_sort (#2 classes); 219 220fun witness_sorts (TSig {classes, log_types, ...}) = 221 Sorts.witness_sorts (#2 classes) log_types; 222 223 224(* certification mode *) 225 226datatype mode = Mode of {normalize: bool, logical: bool}; 227 228val mode_default = Mode {normalize = true, logical = true}; 229val mode_syntax = Mode {normalize = true, logical = false}; 230val mode_abbrev = Mode {normalize = false, logical = false}; 231 232structure Mode = Proof_Data 233( 234 type T = mode; 235 fun init _ = mode_default; 236); 237 238val get_mode = Mode.get; 239fun set_mode mode = Mode.map (K mode); 240fun restore_mode ctxt = set_mode (get_mode ctxt); 241 242 243(* types *) 244 245val type_space = Name_Space.space_of_table o #types o rep_tsig; 246 247fun type_alias naming binding name = map_tsig (fn (classes, default, types) => 248 (classes, default, (Name_Space.alias_table naming binding name types))); 249 250 251fun undecl_type c = "Undeclared type constructor: " ^ quote c; 252 253fun lookup_type (TSig {types, ...}) = Name_Space.lookup types; 254 255fun check_decl context (TSig {types, ...}) (c, pos) = 256 Name_Space.check_reports context types (c, [pos]); 257 258fun the_decl tsig (c, pos) = 259 (case lookup_type tsig c of 260 NONE => error (undecl_type c ^ Position.here pos) 261 | SOME decl => decl); 262 263 264(* certified types *) 265 266fun bad_nargs t = "Bad number of arguments for type constructor: " ^ quote t; 267 268local 269 270fun inst_typ env (Type (c, Ts)) = Type (c, map (inst_typ env) Ts) 271 | inst_typ env (T as TFree (x, _)) = the_default T (AList.lookup (op =) env x) 272 | inst_typ _ T = T; 273 274in 275 276fun cert_typ_mode (Mode {normalize, logical}) tsig ty = 277 let 278 fun err msg = raise TYPE (msg, [ty], []); 279 280 val check_logical = 281 if logical then fn c => err ("Illegal occurrence of syntactic type: " ^ quote c) 282 else fn _ => (); 283 284 fun cert (T as Type (c, Ts)) = 285 let 286 val Ts' = map cert Ts; 287 fun nargs n = if length Ts <> n then err (bad_nargs c) else (); 288 in 289 (case the_decl tsig (c, Position.none) of 290 LogicalType n => (nargs n; Type (c, Ts')) 291 | Abbreviation (vs, U, syn) => 292 (nargs (length vs); 293 if syn then check_logical c else (); 294 if normalize then inst_typ (vs ~~ Ts') U 295 else Type (c, Ts')) 296 | Nonterminal => (nargs 0; check_logical c; T)) 297 end 298 | cert (TFree (x, S)) = TFree (x, cert_sort tsig S) 299 | cert (TVar (xi as (_, i), S)) = 300 if i < 0 then 301 err ("Malformed type variable: " ^ quote (Term.string_of_vname xi)) 302 else TVar (xi, cert_sort tsig S); 303 304 val ty' = cert ty; 305 in if ty = ty' then ty else ty' end; (*avoid copying of already normal type*) 306 307val cert_typ = cert_typ_mode mode_default; 308 309end; 310 311 312(* type arities *) 313 314fun arity_number tsig a = 315 (case lookup_type tsig a of 316 SOME (LogicalType n) => n 317 | _ => error (undecl_type a)); 318 319fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) [] 320 | arity_sorts context (TSig {classes, ...}) a S = 321 Sorts.mg_domain (#2 classes) a S 322 handle Sorts.CLASS_ERROR err => error (Sorts.class_error context err); 323 324 325 326(** special treatment of type vars **) 327 328(* sort_of_atyp *) 329 330fun sort_of_atyp (TFree (_, S)) = S 331 | sort_of_atyp (TVar (_, S)) = S 332 | sort_of_atyp T = raise TYPE ("sort_of_atyp", [T], []); 333 334 335(* strip_sorts *) 336 337val strip_sorts = map_atyps 338 (fn TFree (x, _) => TFree (x, []) 339 | TVar (xi, _) => TVar (xi, [])); 340 341val strip_sorts_dummy = map_atyps 342 (fn TFree (x, _) => TFree (x, dummyS) 343 | TVar (xi, _) => TVar (xi, dummyS)); 344 345 346(* no_tvars *) 347 348fun no_tvars T = 349 (case Term.add_tvarsT T [] of [] => T 350 | vs => raise TYPE ("Illegal schematic type variable(s): " ^ 351 commas_quote (map (Term.string_of_vname o #1) (rev vs)), [T], [])); 352 353 354(* varify_global *) 355 356fun varify_global fixed t = 357 let 358 val fs = Term.fold_types (Term.fold_atyps 359 (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t []; 360 val used = Name.context 361 |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t; 362 val fmap = fs ~~ map (rpair 0) (#1 (fold_map Name.variant (map fst fs) used)); 363 fun thaw (f as (_, S)) = 364 (case AList.lookup (op =) fmap f of 365 NONE => TFree f 366 | SOME xi => TVar (xi, S)); 367 in (fmap, map_types (map_type_tfree thaw) t) end; 368 369 370(* freeze_thaw: freeze TVars in a term; return the "thaw" inverse *) 371 372local 373 374fun new_name ix (pairs, used) = 375 let val v = singleton (Name.variant_list used) (string_of_indexname ix) 376 in ((ix, v) :: pairs, v :: used) end; 377 378fun freeze_one alist (ix, sort) = 379 TFree (the (AList.lookup (op =) alist ix), sort) 380 handle Option.Option => 381 raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []); 382 383fun thaw_one alist (a, sort) = TVar (the (AList.lookup (op =) alist a), sort) 384 handle Option.Option => TFree (a, sort); 385 386in 387 388fun legacy_freeze_thaw_type T = 389 let 390 val used = Term.add_tfree_namesT T []; 391 val (alist, _) = fold_rev new_name (map #1 (Term.add_tvarsT T [])) ([], used); 392 in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end; 393 394val legacy_freeze_type = #1 o legacy_freeze_thaw_type; 395 396fun legacy_freeze_thaw t = 397 let 398 val used = Term.add_tfree_names t []; 399 val (alist, _) = fold_rev new_name (map #1 (Term.add_tvars t [])) ([], used); 400 in 401 (case alist of 402 [] => (t, fn x => x) (*nothing to do!*) 403 | _ => (map_types (map_type_tvar (freeze_one alist)) t, 404 map_types (map_type_tfree (thaw_one (map swap alist))))) 405 end; 406 407val legacy_freeze = #1 o legacy_freeze_thaw; 408 409end; 410 411 412 413(** matching and unification of types **) 414 415type tyenv = (sort * typ) Vartab.table; 416 417fun tvar_clash ixn S S' = 418 raise TYPE ("Type variable has two distinct sorts", [TVar (ixn, S), TVar (ixn, S')], []); 419 420fun lookup tye (ixn, S) = 421 (case Vartab.lookup tye ixn of 422 NONE => NONE 423 | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S'); 424 425 426(* matching *) 427 428exception TYPE_MATCH; 429 430fun typ_match tsig = 431 let 432 fun match (TVar (v, S), T) subs = 433 (case lookup subs (v, S) of 434 NONE => 435 if of_sort tsig (T, S) then Vartab.update_new (v, (S, T)) subs 436 else raise TYPE_MATCH 437 | SOME U => if U = T then subs else raise TYPE_MATCH) 438 | match (Type (a, Ts), Type (b, Us)) subs = 439 if a <> b then raise TYPE_MATCH 440 else matches (Ts, Us) subs 441 | match (TFree x, TFree y) subs = 442 if x = y then subs else raise TYPE_MATCH 443 | match _ _ = raise TYPE_MATCH 444 and matches (T :: Ts, U :: Us) subs = matches (Ts, Us) (match (T, U) subs) 445 | matches _ subs = subs; 446 in match end; 447 448fun typ_instance tsig (T, U) = 449 (typ_match tsig (U, T) Vartab.empty; true) handle TYPE_MATCH => false; 450 451(*purely structural matching*) 452fun raw_match (TVar (v, S), T) subs = 453 (case lookup subs (v, S) of 454 NONE => Vartab.update_new (v, (S, T)) subs 455 | SOME U => if U = T then subs else raise TYPE_MATCH) 456 | raw_match (Type (a, Ts), Type (b, Us)) subs = 457 if a <> b then raise TYPE_MATCH 458 else raw_matches (Ts, Us) subs 459 | raw_match (TFree x, TFree y) subs = 460 if x = y then subs else raise TYPE_MATCH 461 | raw_match _ _ = raise TYPE_MATCH 462and raw_matches (T :: Ts, U :: Us) subs = raw_matches (Ts, Us) (raw_match (T, U) subs) 463 | raw_matches ([], []) subs = subs 464 | raw_matches _ _ = raise TYPE_MATCH; 465 466(*fast matching filter*) 467fun could_match (Type (a, Ts), Type (b, Us)) = a = b andalso could_matches (Ts, Us) 468 | could_match (TFree (a, _), TFree (b, _)) = a = b 469 | could_match (TVar _, _) = true 470 | could_match _ = false 471and could_matches (T :: Ts, U :: Us) = could_match (T, U) andalso could_matches (Ts, Us) 472 | could_matches ([], []) = true 473 | could_matches _ = false; 474 475fun raw_instance (T, U) = 476 if could_match (U, T) then 477 (raw_match (U, T) Vartab.empty; true) handle TYPE_MATCH => false 478 else false; 479 480 481(* unification *) 482 483exception TUNIFY; 484 485(*occurs check*) 486fun occurs v tye = 487 let 488 fun occ (Type (_, Ts)) = exists occ Ts 489 | occ (TFree _) = false 490 | occ (TVar (w, S)) = 491 Term.eq_ix (v, w) orelse 492 (case lookup tye (w, S) of 493 NONE => false 494 | SOME U => occ U); 495 in occ end; 496 497(*chase variable assignments; if devar returns a type var then it must be unassigned*) 498fun devar tye (T as TVar v) = 499 (case lookup tye v of 500 SOME U => devar tye U 501 | NONE => T) 502 | devar _ T = T; 503 504(*order-sorted unification*) 505fun unify (TSig {classes = (_, classes), ...}) TU (tyenv, maxidx) = 506 let 507 val tyvar_count = Unsynchronized.ref maxidx; 508 fun gen_tyvar S = TVar ((Name.aT, Unsynchronized.inc tyvar_count), S); 509 510 fun mg_domain a S = Sorts.mg_domain classes a S 511 handle Sorts.CLASS_ERROR _ => raise TUNIFY; 512 513 fun meet (_, []) tye = tye 514 | meet (TVar (xi, S'), S) tye = 515 if Sorts.sort_le classes (S', S) then tye 516 else Vartab.update_new 517 (xi, (S', gen_tyvar (Sorts.inter_sort classes (S', S)))) tye 518 | meet (TFree (_, S'), S) tye = 519 if Sorts.sort_le classes (S', S) then tye 520 else raise TUNIFY 521 | meet (Type (a, Ts), S) tye = meets (Ts, mg_domain a S) tye 522 and meets (T :: Ts, S :: Ss) tye = meets (Ts, Ss) (meet (devar tye T, S) tye) 523 | meets _ tye = tye; 524 525 fun unif (ty1, ty2) tye = 526 (case (devar tye ty1, devar tye ty2) of 527 (T as TVar (v, S1), U as TVar (w, S2)) => 528 if Term.eq_ix (v, w) then 529 if S1 = S2 then tye else tvar_clash v S1 S2 530 else if Sorts.sort_le classes (S1, S2) then 531 Vartab.update_new (w, (S2, T)) tye 532 else if Sorts.sort_le classes (S2, S1) then 533 Vartab.update_new (v, (S1, U)) tye 534 else 535 let val S = gen_tyvar (Sorts.inter_sort classes (S1, S2)) in 536 Vartab.update_new (v, (S1, S)) (Vartab.update_new (w, (S2, S)) tye) 537 end 538 | (TVar (v, S), T) => 539 if occurs v tye T then raise TUNIFY 540 else meet (T, S) (Vartab.update_new (v, (S, T)) tye) 541 | (T, TVar (v, S)) => 542 if occurs v tye T then raise TUNIFY 543 else meet (T, S) (Vartab.update_new (v, (S, T)) tye) 544 | (Type (a, Ts), Type (b, Us)) => 545 if a <> b then raise TUNIFY 546 else unifs (Ts, Us) tye 547 | (T, U) => if T = U then tye else raise TUNIFY) 548 and unifs (T :: Ts, U :: Us) tye = unifs (Ts, Us) (unif (T, U) tye) 549 | unifs _ tye = tye; 550 in (unif TU tyenv, ! tyvar_count) end; 551 552(*purely structural unification*) 553fun raw_unify (ty1, ty2) tye = 554 (case (devar tye ty1, devar tye ty2) of 555 (T as TVar (v, S1), TVar (w, S2)) => 556 if Term.eq_ix (v, w) then 557 if S1 = S2 then tye else tvar_clash v S1 S2 558 else Vartab.update_new (w, (S2, T)) tye 559 | (TVar (v, S), T) => 560 if occurs v tye T then raise TUNIFY 561 else Vartab.update_new (v, (S, T)) tye 562 | (T, TVar (v, S)) => 563 if occurs v tye T then raise TUNIFY 564 else Vartab.update_new (v, (S, T)) tye 565 | (Type (a, Ts), Type (b, Us)) => 566 if a <> b then raise TUNIFY 567 else raw_unifys (Ts, Us) tye 568 | (T, U) => if T = U then tye else raise TUNIFY) 569and raw_unifys (T :: Ts, U :: Us) tye = raw_unifys (Ts, Us) (raw_unify (T, U) tye) 570 | raw_unifys ([], []) tye = tye 571 | raw_unifys _ _ = raise TUNIFY; 572 573(*fast unification filter*) 574fun could_unify (Type (a, Ts), Type (b, Us)) = a = b andalso could_unifys (Ts, Us) 575 | could_unify (TFree (a, _), TFree (b, _)) = a = b 576 | could_unify (TVar _, _) = true 577 | could_unify (_, TVar _) = true 578 | could_unify _ = false 579and could_unifys (T :: Ts, U :: Us) = could_unify (T, U) andalso could_unifys (Ts, Us) 580 | could_unifys ([], []) = true 581 | could_unifys _ = false; 582 583(*equality with respect to a type environment*) 584fun unified tye = 585 let 586 fun unif (T, T') = 587 (case (devar tye T, devar tye T') of 588 (Type (s, Ts), Type (s', Ts')) => s = s' andalso unifs (Ts, Ts') 589 | (U, U') => U = U') 590 and unifs ([], []) = true 591 | unifs (T :: Ts, T' :: Ts') = unif (T', T') andalso unifs (Ts, Ts') 592 | unifs _ = false; 593 in if Vartab.is_empty tye then op = else unif end; 594 595 596 597(** extend and merge type signatures **) 598 599(* classes *) 600 601fun add_class context (c, cs) tsig = 602 tsig |> map_tsig (fn ((space, classes), default, types) => 603 let 604 val cs' = map (cert_class tsig) cs 605 handle TYPE (msg, _, _) => error msg; 606 val _ = Binding.check c; 607 val (c', space') = space |> Name_Space.declare context true c; 608 val classes' = classes |> Sorts.add_class context (c', cs'); 609 in ((space', classes'), default, types) end); 610 611fun hide_class fully c = map_tsig (fn ((space, classes), default, types) => 612 ((Name_Space.hide fully c space, classes), default, types)); 613 614 615(* arities *) 616 617fun add_arity context (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) => 618 let 619 val _ = 620 (case lookup_type tsig t of 621 SOME (LogicalType n) => if length Ss <> n then error (bad_nargs t) else () 622 | SOME _ => error ("Logical type constructor expected: " ^ quote t) 623 | NONE => error (undecl_type t)); 624 val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S) 625 handle TYPE (msg, _, _) => error msg; 626 val classes' = classes |> Sorts.add_arities context ((t, map (fn c' => (c', Ss')) S')); 627 in ((space, classes'), default, types) end); 628 629 630(* classrel *) 631 632fun add_classrel context rel tsig = 633 tsig |> map_tsig (fn ((space, classes), default, types) => 634 let 635 val rel' = apply2 (cert_class tsig) rel 636 handle TYPE (msg, _, _) => error msg; 637 val classes' = classes |> Sorts.add_classrel context rel'; 638 in ((space, classes'), default, types) end); 639 640 641(* default sort *) 642 643fun set_defsort S tsig = tsig |> map_tsig (fn (classes, _, types) => 644 (classes, cert_sort tsig S handle TYPE (msg, _, _) => error msg, types)); 645 646 647(* types *) 648 649local 650 651fun new_decl context (c, decl) types = 652 (Binding.check c; #2 (Name_Space.define context true (c, decl) types)); 653 654fun map_types f = map_tsig (fn (classes, default, types) => 655 let 656 val types' = f types; 657 val _ = 658 not (Name_Space.defined types' "dummy") orelse 659 Name_Space.intern (Name_Space.space_of_table types') "dummy" = "dummy" orelse 660 error "Illegal declaration of dummy type"; 661 in (classes, default, types') end); 662 663fun syntactic tsig (Type (c, Ts)) = 664 (case lookup_type tsig c of SOME Nonterminal => true | _ => false) 665 orelse exists (syntactic tsig) Ts 666 | syntactic _ _ = false; 667 668in 669 670fun add_type context (c, n) = 671 if n < 0 then error ("Bad type constructor declaration " ^ Binding.print c) 672 else map_types (new_decl context (c, LogicalType n)); 673 674fun add_abbrev context (a, vs, rhs) tsig = tsig |> map_types (fn types => 675 let 676 fun err msg = 677 cat_error msg ("The error(s) above occurred in type abbreviation " ^ Binding.print a); 678 val rhs' = strip_sorts (no_tvars (cert_typ_mode mode_syntax tsig rhs)) 679 handle TYPE (msg, _, _) => err msg; 680 val _ = 681 (case duplicates (op =) vs of 682 [] => [] 683 | dups => err ("Duplicate variables on lhs: " ^ commas_quote dups)); 684 val _ = 685 (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of 686 [] => [] 687 | extras => err ("Extra variables on rhs: " ^ commas_quote extras)); 688 in types |> new_decl context (a, Abbreviation (vs, rhs', syntactic tsig rhs')) end); 689 690fun add_nonterminal context = map_types o new_decl context o rpair Nonterminal; 691 692end; 693 694fun hide_type fully c = map_tsig (fn (classes, default, types) => 695 (classes, default, Name_Space.hide_table fully c types)); 696 697 698(* merge type signatures *) 699 700fun merge_tsig context (tsig1, tsig2) = 701 let 702 val (TSig {classes = (space1, classes1), default = default1, types = types1, 703 log_types = _}) = tsig1; 704 val (TSig {classes = (space2, classes2), default = default2, types = types2, 705 log_types = _}) = tsig2; 706 707 val space' = Name_Space.merge (space1, space2); 708 val classes' = Sorts.merge_algebra context (classes1, classes2); 709 val default' = Sorts.inter_sort classes' (default1, default2); 710 val types' = Name_Space.merge_tables (types1, types2); 711 in build_tsig ((space', classes'), default', types') end; 712 713end; 714