38 val restore_mode: Proof.context -> Proof.context -> Proof.context |
38 val restore_mode: Proof.context -> Proof.context -> Proof.context |
39 val cert_typ_mode: mode -> tsig -> typ -> typ |
39 val cert_typ_mode: mode -> tsig -> typ -> typ |
40 val cert_typ: tsig -> typ -> typ |
40 val cert_typ: tsig -> typ -> typ |
41 val arity_number: tsig -> string -> int |
41 val arity_number: tsig -> string -> int |
42 val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list |
42 val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list |
|
43 val the_tags: tsig -> string -> Markup.property list |
43 |
44 |
44 (*special treatment of type vars*) |
45 (*special treatment of type vars*) |
45 val strip_sorts: typ -> typ |
46 val strip_sorts: typ -> typ |
46 val similar_types: term * term -> bool |
47 val similar_types: term * term -> bool |
47 val no_tvars: typ -> typ |
48 val no_tvars: typ -> typ |
70 |
71 |
71 (*extend and merge type signatures*) |
72 (*extend and merge type signatures*) |
72 val add_class: Pretty.pp -> NameSpace.naming -> bstring * class list -> tsig -> tsig |
73 val add_class: Pretty.pp -> NameSpace.naming -> bstring * class list -> tsig -> tsig |
73 val hide_class: bool -> string -> tsig -> tsig |
74 val hide_class: bool -> string -> tsig -> tsig |
74 val set_defsort: sort -> tsig -> tsig |
75 val set_defsort: sort -> tsig -> tsig |
75 val add_types: NameSpace.naming -> (bstring * int) list -> tsig -> tsig |
76 val add_type: NameSpace.naming -> Markup.property list -> bstring * int -> tsig -> tsig |
76 val add_abbrevs: NameSpace.naming -> (string * string list * typ) list -> tsig -> tsig |
77 val add_abbrev: NameSpace.naming -> Markup.property list -> string * string list * typ -> tsig -> tsig |
77 val add_nonterminals: NameSpace.naming -> string list -> tsig -> tsig |
78 val add_nonterminal: NameSpace.naming -> Markup.property list -> string -> tsig -> tsig |
78 val hide_type: bool -> string -> tsig -> tsig |
79 val hide_type: bool -> string -> tsig -> tsig |
79 val add_arity: Pretty.pp -> arity -> tsig -> tsig |
80 val add_arity: Pretty.pp -> arity -> tsig -> tsig |
80 val add_classrel: Pretty.pp -> class * class -> tsig -> tsig |
81 val add_classrel: Pretty.pp -> class * class -> tsig -> tsig |
81 val merge_tsigs: Pretty.pp -> tsig * tsig -> tsig |
82 val merge_tsigs: Pretty.pp -> tsig * tsig -> tsig |
82 end; |
83 end; |
102 |
103 |
103 datatype tsig = |
104 datatype tsig = |
104 TSig of { |
105 TSig of { |
105 classes: NameSpace.T * Sorts.algebra, (*order-sorted algebra of type classes*) |
106 classes: NameSpace.T * Sorts.algebra, (*order-sorted algebra of type classes*) |
106 default: sort, (*default sort on input*) |
107 default: sort, (*default sort on input*) |
107 types: (decl * serial) NameSpace.table, (*declared types*) |
108 types: ((decl * Markup.property list) * serial) NameSpace.table, (*declared types*) |
108 log_types: string list}; (*logical types sorted by number of arguments*) |
109 log_types: string list}; (*logical types sorted by number of arguments*) |
109 |
110 |
110 fun rep_tsig (TSig comps) = comps; |
111 fun rep_tsig (TSig comps) = comps; |
111 |
112 |
112 fun make_tsig (classes, default, types, log_types) = |
113 fun make_tsig (classes, default, types, log_types) = |
113 TSig {classes = classes, default = default, types = types, log_types = log_types}; |
114 TSig {classes = classes, default = default, types = types, log_types = log_types}; |
114 |
115 |
115 fun build_tsig ((space, classes), default, types) = |
116 fun build_tsig ((space, classes), default, types) = |
116 let |
117 let |
117 val log_types = |
118 val log_types = |
118 Symtab.fold (fn (c, (LogicalType n, _)) => cons (c, n) | _ => I) (snd types) [] |
119 Symtab.fold (fn (c, ((LogicalType n, _), _)) => cons (c, n) | _ => I) (snd types) [] |
119 |> Library.sort (Library.int_ord o pairself snd) |> map fst; |
120 |> Library.sort (Library.int_ord o pairself snd) |> map fst; |
120 in make_tsig ((space, classes), default, types, log_types) end; |
121 in make_tsig ((space, classes), default, types, log_types) end; |
121 |
122 |
122 fun map_tsig f (TSig {classes, default, types, log_types = _}) = |
123 fun map_tsig f (TSig {classes, default, types, log_types = _}) = |
123 build_tsig (f (classes, default, types)); |
124 build_tsig (f (classes, default, types)); |
124 |
125 |
125 val empty_tsig = |
126 val empty_tsig = |
126 build_tsig ((NameSpace.empty, Sorts.empty_algebra), [], NameSpace.empty_table); |
127 build_tsig ((NameSpace.empty, Sorts.empty_algebra), [], NameSpace.empty_table); |
|
128 |
|
129 fun lookup_type (TSig {types, ...}) = Option.map fst o Symtab.lookup (snd types); |
|
130 |
|
131 fun the_tags tsig = snd o the o lookup_type tsig; |
127 |
132 |
128 |
133 |
129 (* classes and sorts *) |
134 (* classes and sorts *) |
130 |
135 |
131 fun defaultS (TSig {default, ...}) = default; |
136 fun defaultS (TSig {default, ...}) = default; |
187 fun cert (T as Type (c, Ts)) = |
191 fun cert (T as Type (c, Ts)) = |
188 let |
192 let |
189 val Ts' = map cert Ts; |
193 val Ts' = map cert Ts; |
190 fun nargs n = if length Ts <> n then err (bad_nargs c) else (); |
194 fun nargs n = if length Ts <> n then err (bad_nargs c) else (); |
191 in |
195 in |
192 (case Symtab.lookup types c of |
196 (case lookup_type tsig c of |
193 SOME (LogicalType n, _) => (nargs n; Type (c, Ts')) |
197 SOME (LogicalType n, _) => (nargs n; Type (c, Ts')) |
194 | SOME (Abbreviation (vs, U, syn), _) => |
198 | SOME (Abbreviation (vs, U, syn), _) => |
195 (nargs (length vs); |
199 (nargs (length vs); |
196 if syn then check_logical c else (); |
200 if syn then check_logical c else (); |
197 if normalize then inst_typ (vs ~~ Ts') U |
201 if normalize then inst_typ (vs ~~ Ts') U |
213 end; |
217 end; |
214 |
218 |
215 |
219 |
216 (* type arities *) |
220 (* type arities *) |
217 |
221 |
218 fun arity_number (TSig {types = (_, types), ...}) a = |
222 fun arity_number tsig a = |
219 (case Symtab.lookup types a of |
223 (case lookup_type tsig a of |
220 SOME (LogicalType n, _) => n |
224 SOME (LogicalType n, _) => n |
221 | _ => error (undecl_type a)); |
225 | _ => error (undecl_type a)); |
222 |
226 |
223 fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) [] |
227 fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) [] |
224 | arity_sorts pp (TSig {classes, ...}) a S = Sorts.mg_domain (#2 classes) a S |
228 | arity_sorts pp (TSig {classes, ...}) a S = Sorts.mg_domain (#2 classes) a S |
512 (* arities *) |
516 (* arities *) |
513 |
517 |
514 fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) => |
518 fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) => |
515 let |
519 let |
516 val _ = |
520 val _ = |
517 (case Symtab.lookup (#2 types) t of |
521 (case lookup_type tsig t of |
518 SOME (LogicalType n, _) => if length Ss <> n then error (bad_nargs t) else () |
522 SOME (LogicalType n, _) => if length Ss <> n then error (bad_nargs t) else () |
519 | SOME (decl, _) => error ("Illegal " ^ str_of_decl decl ^ ": " ^ quote t) |
523 | SOME (decl, _) => error ("Illegal " ^ str_of_decl decl ^ ": " ^ quote t) |
520 | NONE => error (undecl_type t)); |
524 | NONE => error (undecl_type t)); |
521 val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S) |
525 val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S) |
522 handle TYPE (msg, _, _) => error msg; |
526 handle TYPE (msg, _, _) => error msg; |
552 let val s = str_of_decl decl and s' = str_of_decl decl' in |
556 let val s = str_of_decl decl and s' = str_of_decl decl' in |
553 if s = s' then error ("Duplicate declaration of " ^ s ^ ": " ^ quote c) |
557 if s = s' then error ("Duplicate declaration of " ^ s ^ ": " ^ quote c) |
554 else error ("Conflict of " ^ s ^ " with " ^ s' ^ ": " ^ quote c) |
558 else error ("Conflict of " ^ s ^ " with " ^ s' ^ ": " ^ quote c) |
555 end; |
559 end; |
556 |
560 |
557 fun new_decl naming (c, decl) (space, types) = |
561 fun new_decl naming tags (c, decl) (space, types) = |
558 let |
562 let |
559 val c' = NameSpace.full naming c; |
563 val c' = NameSpace.full naming c; |
560 val space' = NameSpace.declare naming c' space; |
564 val space' = NameSpace.declare naming c' space; |
561 val types' = |
565 val types' = |
562 (case Symtab.lookup types c' of |
566 (case Symtab.lookup types c' of |
563 SOME (decl', _) => err_in_decls c' decl decl' |
567 SOME ((decl', _), _) => err_in_decls c' decl decl' |
564 | NONE => Symtab.update (c', (decl, serial ())) types); |
568 | NONE => Symtab.update (c', ((decl, tags), serial ())) types); |
565 in (space', types') end; |
569 in (space', types') end; |
566 |
570 |
567 fun the_decl (_, types) = fst o the o Symtab.lookup types; |
571 fun the_decl (_, types) = fst o fst o the o Symtab.lookup types; |
568 |
572 |
569 fun map_types f = map_tsig (fn (classes, default, types) => |
573 fun map_types f = map_tsig (fn (classes, default, types) => |
570 let |
574 let |
571 val (space', tab') = f types; |
575 val (space', tab') = f types; |
572 val _ = NameSpace.intern space' "dummy" = "dummy" orelse |
576 val _ = NameSpace.intern space' "dummy" = "dummy" orelse |
573 error "Illegal declaration of dummy type"; |
577 error "Illegal declaration of dummy type"; |
574 in (classes, default, (space', tab')) end); |
578 in (classes, default, (space', tab')) end); |
575 |
579 |
576 fun syntactic types (Type (c, Ts)) = |
580 fun syntactic types (Type (c, Ts)) = |
577 (case Symtab.lookup types c of SOME (Nonterminal, _) => true | _ => false) |
581 (case Symtab.lookup types c of SOME ((Nonterminal, _), _) => true | _ => false) |
578 orelse exists (syntactic types) Ts |
582 orelse exists (syntactic types) Ts |
579 | syntactic _ _ = false; |
583 | syntactic _ _ = false; |
580 |
584 |
581 fun add_abbrev naming (a, vs, rhs) tsig = tsig |> map_types (fn types => |
585 in |
|
586 |
|
587 fun add_type naming tags (c, n) = if n < 0 then err_neg_args c else |
|
588 map_types (new_decl naming tags (c, LogicalType n)); |
|
589 |
|
590 fun add_abbrev naming tags (a, vs, rhs) tsig = tsig |> map_types (fn types => |
582 let |
591 let |
583 fun err msg = cat_error msg ("The error(s) above occurred in type abbreviation: " ^ quote a); |
592 fun err msg = cat_error msg ("The error(s) above occurred in type abbreviation: " ^ quote a); |
584 val rhs' = strip_sorts (no_tvars (cert_typ_mode mode_syntax tsig rhs)) |
593 val rhs' = strip_sorts (no_tvars (cert_typ_mode mode_syntax tsig rhs)) |
585 handle TYPE (msg, _, _) => err msg; |
594 handle TYPE (msg, _, _) => err msg; |
586 in |
595 in |
588 [] => [] |
597 [] => [] |
589 | dups => err ("Duplicate variables on lhs: " ^ commas_quote dups)); |
598 | dups => err ("Duplicate variables on lhs: " ^ commas_quote dups)); |
590 (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of |
599 (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of |
591 [] => [] |
600 [] => [] |
592 | extras => err ("Extra variables on rhs: " ^ commas_quote extras)); |
601 | extras => err ("Extra variables on rhs: " ^ commas_quote extras)); |
593 types |> new_decl naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) |
602 types |> new_decl naming tags (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) |
594 end); |
603 end); |
595 |
604 |
596 in |
605 fun add_nonterminal naming tags = map_types o new_decl naming tags o rpair Nonterminal; |
597 |
|
598 fun add_types naming ps = map_types (fold (new_decl naming) (ps |> map (fn (c, n) => |
|
599 if n < 0 then err_neg_args c else (c, LogicalType n)))); |
|
600 |
|
601 val add_abbrevs = fold o add_abbrev; |
|
602 |
|
603 fun add_nonterminals naming = map_types o fold (new_decl naming) o map (rpair Nonterminal); |
|
604 |
606 |
605 fun merge_types (types1, types2) = |
607 fun merge_types (types1, types2) = |
606 NameSpace.merge_tables (Library.eq_snd (op = : serial * serial -> bool)) (types1, types2) |
608 NameSpace.merge_tables (Library.eq_snd (op = : serial * serial -> bool)) (types1, types2) |
607 handle Symtab.DUP d => err_in_decls d (the_decl types1 d) (the_decl types2 d); |
609 handle Symtab.DUP d => err_in_decls d (the_decl types1 d) (the_decl types2 d); |
608 |
610 |