1.1 --- a/src/Pure/sign.ML Fri Jun 17 18:33:26 2005 +0200
1.2 +++ b/src/Pure/sign.ML Fri Jun 17 18:33:27 2005 +0200
1.3 @@ -2,482 +2,256 @@
1.4 ID: $Id$
1.5 Author: Lawrence C Paulson and Markus Wenzel
1.6
1.7 -The abstract type "sg" of signatures.
1.8 +Logical signature content: naming conventions, concrete syntax, type
1.9 +signature, constant declarations.
1.10 *)
1.11
1.12 +signature SIGN_THEORY =
1.13 +sig
1.14 + val add_defsort: string -> theory -> theory
1.15 + val add_defsort_i: sort -> theory -> theory
1.16 + val add_types: (bstring * int * mixfix) list -> theory -> theory
1.17 + val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
1.18 + val add_nonterminals: bstring list -> theory -> theory
1.19 + val add_tyabbrs: (bstring * string list * string * mixfix) list -> theory -> theory
1.20 + val add_tyabbrs_i: (bstring * string list * typ * mixfix) list -> theory -> theory
1.21 + val add_arities: (xstring * string list * string) list -> theory -> theory
1.22 + val add_arities_i: (string * sort list * sort) list -> theory -> theory
1.23 + val add_syntax: (bstring * string * mixfix) list -> theory -> theory
1.24 + val add_syntax_i: (bstring * typ * mixfix) list -> theory -> theory
1.25 + val add_modesyntax: (string * bool) -> (bstring * string * mixfix) list -> theory -> theory
1.26 + val add_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
1.27 + val del_modesyntax: (string * bool) -> (bstring * string * mixfix) list -> theory -> theory
1.28 + val del_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
1.29 + val add_consts: (bstring * string * mixfix) list -> theory -> theory
1.30 + val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
1.31 + val add_classes: (bstring * xstring list) list -> theory -> theory
1.32 + val add_classes_i: (bstring * class list) list -> theory -> theory
1.33 + val add_classrel: (xstring * xstring) list -> theory -> theory
1.34 + val add_classrel_i: (class * class) list -> theory -> theory
1.35 + val add_trfuns:
1.36 + (string * (ast list -> ast)) list *
1.37 + (string * (term list -> term)) list *
1.38 + (string * (term list -> term)) list *
1.39 + (string * (ast list -> ast)) list -> theory -> theory
1.40 + val add_trfunsT:
1.41 + (string * (bool -> typ -> term list -> term)) list -> theory -> theory
1.42 + val add_advanced_trfuns:
1.43 + (string * (theory -> ast list -> ast)) list *
1.44 + (string * (theory -> term list -> term)) list *
1.45 + (string * (theory -> term list -> term)) list *
1.46 + (string * (theory -> ast list -> ast)) list -> theory -> theory
1.47 + val add_advanced_trfunsT:
1.48 + (string * (theory -> bool -> typ -> term list -> term)) list -> theory -> theory
1.49 + val add_tokentrfuns:
1.50 + (string * string * (string -> string * real)) list -> theory -> theory
1.51 + val add_mode_tokentrfuns: string -> (string * (string -> string * real)) list
1.52 + -> theory -> theory
1.53 + val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
1.54 + val add_trrules_i: ast Syntax.trrule list -> theory -> theory
1.55 + val add_path: string -> theory -> theory
1.56 + val parent_path: theory -> theory
1.57 + val root_path: theory -> theory
1.58 + val absolute_path: theory -> theory
1.59 + val local_path: theory -> theory
1.60 + val qualified_names: theory -> theory
1.61 + val no_base_names: theory -> theory
1.62 + val custom_accesses: (string list -> string list list) -> theory -> theory
1.63 + val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
1.64 + theory -> theory
1.65 + val restore_naming: theory -> theory -> theory
1.66 + val hide_classes: bool -> xstring list -> theory -> theory
1.67 + val hide_classes_i: bool -> string list -> theory -> theory
1.68 + val hide_types: bool -> xstring list -> theory -> theory
1.69 + val hide_types_i: bool -> string list -> theory -> theory
1.70 + val hide_consts: bool -> xstring list -> theory -> theory
1.71 + val hide_consts_i: bool -> string list -> theory -> theory
1.72 +end
1.73 +
1.74 signature SIGN =
1.75 sig
1.76 - type sg
1.77 - type sg_ref
1.78 - type data
1.79 - val rep_sg: sg ->
1.80 - {self: sg_ref,
1.81 + type syn
1.82 + type sg (*obsolete*)
1.83 + val init: theory -> theory
1.84 + val rep_sg: theory ->
1.85 + {naming: NameSpace.naming,
1.86 + syn: syn,
1.87 tsig: Type.tsig,
1.88 - consts: (typ * stamp) NameSpace.table,
1.89 - naming: NameSpace.naming,
1.90 - data: data}
1.91 - val stamp_names_of: sg -> string list
1.92 - val exists_stamp: string -> sg -> bool
1.93 - val pretty_sg: sg -> Pretty.T
1.94 - val pprint_sg: sg -> pprint_args -> unit
1.95 - val pretty_abbrev_sg: sg -> Pretty.T
1.96 - val str_of_sg: sg -> string
1.97 - val is_stale: sg -> bool
1.98 - val self_ref: sg -> sg_ref
1.99 - val deref: sg_ref -> sg
1.100 - val name_of: sg -> string
1.101 - val is_draft: sg -> bool
1.102 - val eq_sg: sg * sg -> bool
1.103 - val subsig: sg * sg -> bool
1.104 - val same_sg: sg * sg -> bool
1.105 - val joinable: sg * sg -> bool
1.106 - val prep_ext: sg -> sg
1.107 - val copy: sg -> sg
1.108 - val add_name: string -> sg -> sg
1.109 - val data_kinds: data -> string list
1.110 - val print_all_data: sg -> unit
1.111 - val pre_pure: sg
1.112 - val PureN: string
1.113 - val CPureN: string
1.114 - val naming_of: sg -> NameSpace.naming
1.115 + consts: (typ * stamp) NameSpace.table}
1.116 + val naming_of: theory -> NameSpace.naming
1.117 val base_name: string -> bstring
1.118 - val full_name: sg -> bstring -> string
1.119 - val full_name_path: sg -> string -> bstring -> string
1.120 - val declare_name: sg -> string -> NameSpace.T -> NameSpace.T
1.121 - val syn_of: sg -> Syntax.syntax
1.122 - val tsig_of: sg -> Type.tsig
1.123 - val classes: sg -> class list
1.124 - val defaultS: sg -> sort
1.125 - val subsort: sg -> sort * sort -> bool
1.126 - val of_sort: sg -> typ * sort -> bool
1.127 - val witness_sorts: sg -> sort list -> sort list -> (typ * sort) list
1.128 - val universal_witness: sg -> (typ * sort) option
1.129 - val typ_instance: sg -> typ * typ -> bool
1.130 - val is_logtype: sg -> string -> bool
1.131 - val const_type: sg -> string -> typ option
1.132 - val the_const_type: sg -> string -> typ
1.133 - val declared_tyname: sg -> string -> bool
1.134 - val declared_const: sg -> string -> bool
1.135 - val class_space: sg -> NameSpace.T
1.136 - val type_space: sg -> NameSpace.T
1.137 - val const_space: sg -> NameSpace.T
1.138 - val intern_class: sg -> xstring -> string
1.139 - val extern_class: sg -> string -> xstring
1.140 - val intern_type: sg -> xstring -> string
1.141 - val extern_type: sg -> string -> xstring
1.142 - val intern_const: sg -> xstring -> string
1.143 - val extern_const: sg -> string -> xstring
1.144 - val intern_sort: sg -> sort -> sort
1.145 - val extern_sort: sg -> sort -> sort
1.146 - val intern_typ: sg -> typ -> typ
1.147 - val extern_typ: sg -> typ -> typ
1.148 - val intern_term: sg -> term -> term
1.149 - val extern_term: sg -> term -> term
1.150 - val intern_tycons: sg -> typ -> typ
1.151 - val pretty_term': Syntax.syntax -> sg -> term -> Pretty.T
1.152 - val pretty_term: sg -> term -> Pretty.T
1.153 - val pretty_typ: sg -> typ -> Pretty.T
1.154 - val pretty_sort: sg -> sort -> Pretty.T
1.155 - val pretty_classrel: sg -> class list -> Pretty.T
1.156 - val pretty_arity: sg -> arity -> Pretty.T
1.157 - val string_of_term: sg -> term -> string
1.158 - val string_of_typ: sg -> typ -> string
1.159 - val string_of_sort: sg -> sort -> string
1.160 - val string_of_classrel: sg -> class list -> string
1.161 - val string_of_arity: sg -> arity -> string
1.162 - val pprint_term: sg -> term -> pprint_args -> unit
1.163 - val pprint_typ: sg -> typ -> pprint_args -> unit
1.164 - val pp: sg -> Pretty.pp
1.165 - val certify_class: sg -> class -> class
1.166 - val certify_sort: sg -> sort -> sort
1.167 - val certify_typ: sg -> typ -> typ
1.168 - val certify_typ_syntax: sg -> typ -> typ
1.169 - val certify_typ_abbrev: sg -> typ -> typ
1.170 - val certify_term: Pretty.pp -> sg -> term -> term * typ * int
1.171 - val read_sort': Syntax.syntax -> sg -> string -> sort
1.172 - val read_sort: sg -> string -> sort
1.173 - val read_typ': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
1.174 - val read_typ_syntax': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
1.175 - val read_typ_abbrev': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
1.176 - val read_typ: sg * (indexname -> sort option) -> string -> typ
1.177 - val read_typ_syntax: sg * (indexname -> sort option) -> string -> typ
1.178 - val read_typ_abbrev: sg * (indexname -> sort option) -> string -> typ
1.179 - val read_tyname: sg -> string -> typ
1.180 - val read_const: sg -> string -> term
1.181 - val infer_types_simult: Pretty.pp -> sg -> (indexname -> typ option) ->
1.182 + val full_name: theory -> bstring -> string
1.183 + val full_name_path: theory -> string -> bstring -> string
1.184 + val declare_name: theory -> string -> NameSpace.T -> NameSpace.T
1.185 + val syn_of: theory -> Syntax.syntax
1.186 + val tsig_of: theory -> Type.tsig
1.187 + val classes: theory -> class list
1.188 + val defaultS: theory -> sort
1.189 + val subsort: theory -> sort * sort -> bool
1.190 + val of_sort: theory -> typ * sort -> bool
1.191 + val witness_sorts: theory -> sort list -> sort list -> (typ * sort) list
1.192 + val universal_witness: theory -> (typ * sort) option
1.193 + val typ_instance: theory -> typ * typ -> bool
1.194 + val is_logtype: theory -> string -> bool
1.195 + val const_type: theory -> string -> typ option
1.196 + val the_const_type: theory -> string -> typ
1.197 + val declared_tyname: theory -> string -> bool
1.198 + val declared_const: theory -> string -> bool
1.199 + val class_space: theory -> NameSpace.T
1.200 + val type_space: theory -> NameSpace.T
1.201 + val const_space: theory -> NameSpace.T
1.202 + val intern_class: theory -> xstring -> string
1.203 + val extern_class: theory -> string -> xstring
1.204 + val intern_type: theory -> xstring -> string
1.205 + val extern_type: theory -> string -> xstring
1.206 + val intern_const: theory -> xstring -> string
1.207 + val extern_const: theory -> string -> xstring
1.208 + val intern_sort: theory -> sort -> sort
1.209 + val extern_sort: theory -> sort -> sort
1.210 + val intern_typ: theory -> typ -> typ
1.211 + val extern_typ: theory -> typ -> typ
1.212 + val intern_term: theory -> term -> term
1.213 + val extern_term: theory -> term -> term
1.214 + val intern_tycons: theory -> typ -> typ
1.215 + val pretty_term': Syntax.syntax -> theory -> term -> Pretty.T
1.216 + val pretty_term: theory -> term -> Pretty.T
1.217 + val pretty_typ: theory -> typ -> Pretty.T
1.218 + val pretty_sort: theory -> sort -> Pretty.T
1.219 + val pretty_classrel: theory -> class list -> Pretty.T
1.220 + val pretty_arity: theory -> arity -> Pretty.T
1.221 + val string_of_term: theory -> term -> string
1.222 + val string_of_typ: theory -> typ -> string
1.223 + val string_of_sort: theory -> sort -> string
1.224 + val string_of_classrel: theory -> class list -> string
1.225 + val string_of_arity: theory -> arity -> string
1.226 + val pprint_term: theory -> term -> pprint_args -> unit
1.227 + val pprint_typ: theory -> typ -> pprint_args -> unit
1.228 + val pp: theory -> Pretty.pp
1.229 + val certify_class: theory -> class -> class
1.230 + val certify_sort: theory -> sort -> sort
1.231 + val certify_typ: theory -> typ -> typ
1.232 + val certify_typ_syntax: theory -> typ -> typ
1.233 + val certify_typ_abbrev: theory -> typ -> typ
1.234 + val certify_term: Pretty.pp -> theory -> term -> term * typ * int
1.235 + val read_sort': Syntax.syntax -> theory -> string -> sort
1.236 + val read_sort: theory -> string -> sort
1.237 + val read_typ': Syntax.syntax -> theory * (indexname -> sort option) -> string -> typ
1.238 + val read_typ_syntax': Syntax.syntax -> theory * (indexname -> sort option) -> string -> typ
1.239 + val read_typ_abbrev': Syntax.syntax -> theory * (indexname -> sort option) -> string -> typ
1.240 + val read_typ: theory * (indexname -> sort option) -> string -> typ
1.241 + val read_typ_syntax: theory * (indexname -> sort option) -> string -> typ
1.242 + val read_typ_abbrev: theory * (indexname -> sort option) -> string -> typ
1.243 + val read_tyname: theory -> string -> typ
1.244 + val read_const: theory -> string -> term
1.245 + val infer_types_simult: Pretty.pp -> theory -> (indexname -> typ option) ->
1.246 (indexname -> sort option) -> string list -> bool
1.247 -> (term list * typ) list -> term list * (indexname * typ) list
1.248 - val infer_types: Pretty.pp -> sg -> (indexname -> typ option) ->
1.249 + val infer_types: Pretty.pp -> theory -> (indexname -> typ option) ->
1.250 (indexname -> sort option) -> string list -> bool
1.251 -> term list * typ -> term * (indexname * typ) list
1.252 val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax ->
1.253 - sg * (indexname -> typ option) * (indexname -> sort option) ->
1.254 + theory * (indexname -> typ option) * (indexname -> sort option) ->
1.255 string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
1.256 val read_def_terms:
1.257 - sg * (indexname -> typ option) * (indexname -> sort option) ->
1.258 + theory * (indexname -> typ option) * (indexname -> sort option) ->
1.259 string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
1.260 - val simple_read_term: sg -> typ -> string -> term
1.261 - val add_defsort: string -> sg -> sg
1.262 - val add_defsort_i: sort -> sg -> sg
1.263 - val add_types: (bstring * int * mixfix) list -> sg -> sg
1.264 - val add_nonterminals: bstring list -> sg -> sg
1.265 - val add_tyabbrs: (bstring * string list * string * mixfix) list -> sg -> sg
1.266 - val add_tyabbrs_i: (bstring * string list * typ * mixfix) list -> sg -> sg
1.267 - val add_arities: (xstring * string list * string) list -> sg -> sg
1.268 - val add_arities_i: (string * sort list * sort) list -> sg -> sg
1.269 - val add_syntax: (bstring * string * mixfix) list -> sg -> sg
1.270 - val add_syntax_i: (bstring * typ * mixfix) list -> sg -> sg
1.271 - val add_modesyntax: (string * bool) * (bstring * string * mixfix) list -> sg -> sg
1.272 - val add_modesyntax_i: (string * bool) * (bstring * typ * mixfix) list -> sg -> sg
1.273 - val del_modesyntax: (string * bool) * (bstring * string * mixfix) list -> sg -> sg
1.274 - val del_modesyntax_i: (string * bool) * (bstring * typ * mixfix) list -> sg -> sg
1.275 - val add_consts: (bstring * string * mixfix) list -> sg -> sg
1.276 - val add_consts_i: (bstring * typ * mixfix) list -> sg -> sg
1.277 + val simple_read_term: theory -> typ -> string -> term
1.278 val const_of_class: class -> string
1.279 val class_of_const: string -> class
1.280 - val add_classes: (bstring * xstring list) list -> sg -> sg
1.281 - val add_classes_i: (bstring * class list) list -> sg -> sg
1.282 - val add_classrel: (xstring * xstring) list -> sg -> sg
1.283 - val add_classrel_i: (class * class) list -> sg -> sg
1.284 - val add_trfuns:
1.285 - (string * (ast list -> ast)) list *
1.286 - (string * (term list -> term)) list *
1.287 - (string * (term list -> term)) list *
1.288 - (string * (ast list -> ast)) list -> sg -> sg
1.289 - val add_trfunsT:
1.290 - (string * (bool -> typ -> term list -> term)) list -> sg -> sg
1.291 - val add_advanced_trfuns:
1.292 - (string * (sg -> ast list -> ast)) list *
1.293 - (string * (sg -> term list -> term)) list *
1.294 - (string * (sg -> term list -> term)) list *
1.295 - (string * (sg -> ast list -> ast)) list -> sg -> sg
1.296 - val add_advanced_trfunsT:
1.297 - (string * (sg -> bool -> typ -> term list -> term)) list -> sg -> sg
1.298 - val add_tokentrfuns:
1.299 - (string * string * (string -> string * real)) list -> sg -> sg
1.300 - val add_trrules: (xstring * string) Syntax.trrule list -> sg -> sg
1.301 - val add_trrules_i: ast Syntax.trrule list -> sg -> sg
1.302 - val add_path: string -> sg -> sg
1.303 - val qualified_names: sg -> sg
1.304 - val no_base_names: sg -> sg
1.305 - val custom_accesses: (string list -> string list list) -> sg -> sg
1.306 - val set_policy: (string -> bstring -> string) * (string list -> string list list) -> sg -> sg
1.307 - val restore_naming: sg -> sg -> sg
1.308 - val hide_classes: bool -> xstring list -> sg -> sg
1.309 - val hide_classes_i: bool -> string list -> sg -> sg
1.310 - val hide_types: bool -> xstring list -> sg -> sg
1.311 - val hide_types_i: bool -> string list -> sg -> sg
1.312 - val hide_consts: bool -> xstring list -> sg -> sg
1.313 - val hide_consts_i: bool -> string list -> sg -> sg
1.314 - val merge_refs: sg_ref * sg_ref -> sg_ref
1.315 - val merge: sg * sg -> sg
1.316 - val prep_ext_merge: sg list -> sg
1.317 -end;
1.318 + include SIGN_THEORY
1.319 +end
1.320
1.321 -signature PRIVATE_SIGN =
1.322 -sig
1.323 - include SIGN
1.324 - val init_data: Object.kind * (Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
1.325 - (Object.T * Object.T -> Object.T) * (sg -> Object.T -> unit)) -> sg -> sg
1.326 - val get_data: Object.kind -> (Object.T -> 'a) -> sg -> 'a
1.327 - val put_data: Object.kind -> ('a -> Object.T) -> 'a -> sg -> sg
1.328 - val print_data: Object.kind -> sg -> unit
1.329 -end;
1.330 -
1.331 -structure Sign: PRIVATE_SIGN =
1.332 +structure Sign: SIGN =
1.333 struct
1.334
1.335 -(** datatype sg **)
1.336 +type sg = theory;
1.337
1.338 -(* types sg, data, syn, sg_ref *)
1.339
1.340 -datatype sg =
1.341 - Sg of
1.342 - {id: string ref,
1.343 - stamps: string ref list, (*unique theory indentifier*)
1.344 - syn: syn} * (*syntax for parsing and printing*)
1.345 - {self: sg_ref, (*mutable self reference*)
1.346 - tsig: Type.tsig, (*order-sorted signature of types*)
1.347 - consts: (typ * stamp) NameSpace.table, (*type schemes of constants*)
1.348 - naming: NameSpace.naming,
1.349 - data: data}
1.350 -and data =
1.351 - Data of
1.352 - (Object.kind * (*kind (for authorization)*)
1.353 - (Object.T * (*value*)
1.354 - ((Object.T -> Object.T) * (*copy method*)
1.355 - (Object.T -> Object.T) * (*prepare extend method*)
1.356 - (Object.T * Object.T -> Object.T) * (*merge and prepare extend method*)
1.357 - (sg -> Object.T -> unit)))) (*print method*)
1.358 - Symtab.table
1.359 -and syn =
1.360 +(** datatype syn **) (* FIXME use Syntax.syntax here (include advanced trfuns there) *)
1.361 +
1.362 +datatype syn =
1.363 Syn of
1.364 Syntax.syntax *
1.365 - (((sg -> ast list -> ast) * stamp) Symtab.table *
1.366 - ((sg -> term list -> term) * stamp) Symtab.table *
1.367 - ((sg -> bool -> typ -> term list -> term) * stamp) list Symtab.table *
1.368 - ((sg -> ast list -> ast) * stamp) list Symtab.table)
1.369 -and sg_ref =
1.370 - SgRef of sg ref option;
1.371 + (((theory -> ast list -> ast) * stamp) Symtab.table *
1.372 + ((theory -> term list -> term) * stamp) Symtab.table *
1.373 + ((theory -> bool -> typ -> term list -> term) * stamp) list Symtab.table *
1.374 + ((theory -> ast list -> ast) * stamp) list Symtab.table)
1.375
1.376 -(* FIXME assign!??? *)
1.377 -fun make_sg (id, self, stamps) naming data (syn, tsig, consts) =
1.378 - Sg ({id = id, stamps = stamps, syn = syn}, {self = self, tsig = tsig,
1.379 - consts = consts, naming = naming, data = data});
1.380 -
1.381 -fun rep_sg (Sg (_, args)) = args;
1.382 -
1.383 -
1.384 -(* stamps *)
1.385 -
1.386 -fun stamps_of (Sg ({stamps, ...}, _)) = stamps;
1.387 -val stamp_names_of = rev o map ! o stamps_of;
1.388 -fun exists_stamp name = exists (equal name o !) o stamps_of;
1.389 -
1.390 -fun is_stale (Sg ({id, ...}, {self = SgRef (SOME (ref (Sg ({id = id', ...}, _)))), ...})) =
1.391 - id <> id'
1.392 - | is_stale _ = false;
1.393 -
1.394 -fun pretty_sg sg =
1.395 - Pretty.str_list "{" "}" (stamp_names_of sg @ (if is_stale sg then ["!"] else []));
1.396 -
1.397 -val pprint_sg = Pretty.pprint o pretty_sg;
1.398 -
1.399 -fun pretty_abbrev_sg sg =
1.400 - let
1.401 - val stamps = map ! (stamps_of sg);
1.402 - val abbrev = if length stamps > 5 then "..." :: rev (List.take (stamps, 5)) else rev stamps;
1.403 - in Pretty.str_list "{" "}" abbrev end;
1.404 -
1.405 -val str_of_sg = Pretty.str_of o pretty_abbrev_sg;
1.406 -
1.407 -
1.408 -(* id and self *)
1.409 -
1.410 -fun check_stale pos sg =
1.411 - if is_stale sg then raise TERM ("Stale signature (in " ^ pos ^ "): " ^ str_of_sg sg, [])
1.412 - else sg;
1.413 -
1.414 -fun self_ref (sg as Sg (_, {self, ...})) = (check_stale "Sign.self_ref" sg; self);
1.415 -
1.416 -fun deref (SgRef (SOME (ref sg))) = sg
1.417 - | deref (SgRef NONE) = sys_error "Sign.deref";
1.418 -
1.419 -fun assign (SgRef (SOME r)) sg = r := sg
1.420 - | assign (SgRef NONE) _ = sys_error "Sign.assign";
1.421 -
1.422 -fun name_of (sg as Sg ({id = ref name, ...}, _)) =
1.423 - if name = "" orelse ord name = ord "#" then
1.424 - raise TERM ("Nameless signature " ^ str_of_sg sg, [])
1.425 - else name;
1.426 -
1.427 -fun is_draft (Sg ({stamps = ref name :: _, ...}, _)) =
1.428 - name = "" orelse ord name = ord "#"
1.429 - | is_draft _ = sys_error "Sign.is_draft";
1.430 -
1.431 -
1.432 -(* inclusion and equality *)
1.433 -
1.434 -local
1.435 - (*avoiding polymorphic equality: factor 10 speedup*)
1.436 - fun mem_stamp (_: string ref, []) = false
1.437 - | mem_stamp (x, y :: ys) = x = y orelse mem_stamp (x, ys);
1.438 -
1.439 - fun subset_stamp ([], ys) = true
1.440 - | subset_stamp (x :: xs, ys) =
1.441 - mem_stamp (x, ys) andalso subset_stamp (xs, ys);
1.442 -in
1.443 - fun eq_sg (sg1 as Sg ({id = id1, ...}, _), sg2 as Sg ({id = id2, ...}, _)) =
1.444 - (check_stale "Sign.eq_sg" sg1; check_stale "Sign.eq_sg" sg2; id1 = id2);
1.445 -
1.446 - fun subsig (sg1, sg2) =
1.447 - eq_sg (sg1, sg2) orelse mem_stamp (hd (stamps_of sg1), stamps_of sg2);
1.448 -
1.449 - fun subsig_internal (sg1, sg2) =
1.450 - eq_sg (sg1, sg2) orelse subset_stamp (stamps_of sg1, stamps_of sg2);
1.451 -end;
1.452 -
1.453 -
1.454 -fun joinable (sg1, sg2) = subsig (sg1, sg2) orelse subsig (sg2, sg1);
1.455 -
1.456 -(*test if same theory names are contained in signatures' stamps,
1.457 - i.e. if signatures belong to same theory but not necessarily to the
1.458 - same version of it*)
1.459 -fun same_sg (sg1, sg2) =
1.460 - eq_sg (sg1, sg2) orelse eq_set_string (pairself (map ! o stamps_of) (sg1, sg2));
1.461 -
1.462 -
1.463 -(* data operations *)
1.464 -
1.465 -fun err_method name kind e = (* FIXME wrap exn msg!? *)
1.466 - (warning ("Error while invoking " ^ quote kind ^ " " ^ name ^ " method"); raise e);
1.467 -
1.468 -fun err_inconsistent kinds =
1.469 - error ("Attempt to merge different versions of " ^ commas_quote kinds ^ " data");
1.470 -
1.471 -val empty_data = Data Symtab.empty;
1.472 -
1.473 -fun merge_data (Data tab1, Data tab2) =
1.474 - let
1.475 - val data1 = map snd (Symtab.dest tab1);
1.476 - val data2 = map snd (Symtab.dest tab2);
1.477 - val all_data = data1 @ data2;
1.478 - val kinds = gen_distinct Object.eq_kind (map fst all_data);
1.479 -
1.480 - fun entry data kind =
1.481 - (case gen_assoc Object.eq_kind (data, kind) of
1.482 - NONE => []
1.483 - | SOME x => [(kind, x)]);
1.484 -
1.485 - fun merge_entries [(kind, (e, mths as (_, ext, _, _)))] =
1.486 - (kind, (ext e handle exn => err_method "prep_ext" (Object.name_of_kind kind) exn, mths))
1.487 - | merge_entries [(kind, (e1, mths as (_, _, mrg, _))), (_, (e2, _))] =
1.488 - (kind, (mrg (e1, e2)
1.489 - handle exn => err_method "merge" (Object.name_of_kind kind) exn, mths))
1.490 - | merge_entries _ = sys_error "merge_entries";
1.491 -
1.492 - val data = map (fn k => merge_entries (entry data1 k @ entry data2 k)) kinds;
1.493 - val data_idx = map (fn (k, x) => (Object.name_of_kind k, (k, x))) data;
1.494 - in
1.495 - Data (Symtab.make data_idx)
1.496 - handle Symtab.DUPS dups => err_inconsistent dups
1.497 - end;
1.498 -
1.499 -fun prep_ext_data data = merge_data (data, empty_data);
1.500 -
1.501 -fun copy_data (Data tab) =
1.502 - let
1.503 - fun cp_data (k, (e, mths as (cp, _, _, _))) =
1.504 - (k, (cp e handle exn => err_method "copy" (Object.name_of_kind k) exn, mths));
1.505 - in Data (Symtab.map cp_data tab) end;
1.506 -
1.507 -
1.508 -
1.509 -(** build signatures **)
1.510 -
1.511 -fun create_sg name self stamps naming data sign =
1.512 - let
1.513 - val id = ref name;
1.514 - val stamps' = (case stamps of ref "#" :: ss => ss | ss => ss);
1.515 - val _ = conditional (exists (equal name o !) stamps')
1.516 - (fn () => error ("Theory already contains a " ^ quote name ^ " component"));
1.517 - val sg = make_sg (id, self, id :: stamps') naming data sign;
1.518 - in assign self sg; sg end;
1.519 -
1.520 -fun new_sg f (sg as Sg ({stamps, syn, ...}, {self = _, tsig, consts, naming, data})) =
1.521 - let
1.522 - val _ = check_stale "Sign.new_sg" sg;
1.523 - val self' = SgRef (SOME (ref sg));
1.524 - val data' = f data;
1.525 - in create_sg "#" self' stamps naming data' (syn, tsig, consts) end;
1.526 -
1.527 -val prep_ext = new_sg prep_ext_data;
1.528 -val copy = new_sg copy_data;
1.529 -
1.530 -fun add_name name (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, data})) =
1.531 - let
1.532 - val _ = check_stale "Sign.add_name" sg;
1.533 - val (self', data') =
1.534 - if is_draft sg then (self, data)
1.535 - else (SgRef (SOME (ref sg)), prep_ext_data data);
1.536 - in create_sg name self' stamps naming data' (syn, tsig, consts) end;
1.537 -
1.538 -fun map_sg keep f (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, data})) =
1.539 - let
1.540 - val _ = check_stale "Sign.map_sg" sg;
1.541 - val (self', data') =
1.542 - if is_draft sg andalso keep then (self, data)
1.543 - else (SgRef (SOME (ref sg)), prep_ext_data data);
1.544 - val (naming', data', sign') = f (naming, data', (syn, tsig, consts));
1.545 - in create_sg "#" self' stamps naming' data' sign' end;
1.546 -
1.547 -fun map_naming f = map_sg true (fn (naming, data, sign) => (f naming, data, sign));
1.548 -fun map_data f = map_sg true (fn (naming, data, sign) => (naming, f data, sign));
1.549 -fun map_sign f = map_sg true (fn (naming, data, sign) => (naming, data, f sign));
1.550 -fun map_syn f = map_sign (fn (syn, tsig, consts) => (f syn, tsig, consts));
1.551 -fun map_tsig f = map_sign (fn (syn, tsig, consts) => (syn, f tsig, consts));
1.552 -fun map_consts f = map_sign (fn (syn, tsig, consts) => (syn, tsig, f consts));
1.553 -
1.554 -
1.555 -
1.556 -(** signature data **)
1.557 -
1.558 -(* errors *)
1.559 -
1.560 -fun of_theory sg = "\nof theory " ^ str_of_sg sg;
1.561 -
1.562 -fun err_dup_init sg kind =
1.563 - error ("Duplicate initialization of " ^ quote kind ^ " data" ^ of_theory sg);
1.564 -
1.565 -fun err_uninit sg kind =
1.566 - error ("Tried to access uninitialized " ^ quote kind ^ " data" ^ of_theory sg);
1.567 -
1.568 -fun err_access sg kind =
1.569 - error ("Unauthorized access to " ^ quote kind ^ " data" ^ of_theory sg);
1.570 -
1.571 -
1.572 -(* access data *)
1.573 -
1.574 -fun data_kinds (Data tab) = Symtab.keys tab;
1.575 -
1.576 -fun lookup_data sg tab kind =
1.577 - let val name = Object.name_of_kind kind in
1.578 - (case Symtab.lookup (tab, name) of
1.579 - SOME (k, x) =>
1.580 - if Object.eq_kind (kind, k) then x
1.581 - else err_access sg name
1.582 - | NONE => err_uninit sg name)
1.583 - end;
1.584 -
1.585 -fun init_data (kind, (e, cp, ext, mrg, prt)) sg = sg |> map_data (fn Data tab =>
1.586 - Data (Symtab.update_new ((Object.name_of_kind kind, (kind, (e, (cp, ext, mrg, prt)))), tab))
1.587 - handle Symtab.DUP name => err_dup_init sg name);
1.588 -
1.589 -fun get_data kind dest (sg as Sg (_, {data = Data tab, ...})) =
1.590 - let val x = fst (lookup_data sg tab kind)
1.591 - in dest x handle Match => Object.kind_error kind end;
1.592 -
1.593 -fun put_data kind mk x sg = sg |> map_data (fn Data tab =>
1.594 - Data (Symtab.update ((Object.name_of_kind kind,
1.595 - (kind, (mk x, snd (lookup_data sg tab kind)))), tab)));
1.596 -
1.597 -fun print_data kind (sg as Sg (_, {data = Data tab, ...})) =
1.598 - let val (e, (_, _, _, prt)) = lookup_data sg tab kind in
1.599 - prt sg e handle exn =>
1.600 - err_method ("print" ^ of_theory sg) (Object.name_of_kind kind) exn
1.601 - end;
1.602 -
1.603 -fun print_all_data (sg as Sg (_, {data = Data tab, ...})) =
1.604 - List.app (fn kind => print_data kind sg) (map (#1 o #2) (Symtab.dest tab));
1.605 -
1.606 -
1.607 -
1.608 -(** primitive signatures **)
1.609 +fun merge_trfuns
1.610 + (parse_ast_trtab1, parse_trtab1, print_trtab1, print_ast_trtab1)
1.611 + (parse_ast_trtab2, parse_trtab2, print_trtab2, print_ast_trtab2) =
1.612 + (Syntax.merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2,
1.613 + Syntax.merge_trtabs "parse translation" parse_trtab1 parse_trtab2,
1.614 + Syntax.merge_tr'tabs print_trtab1 print_trtab2,
1.615 + Syntax.merge_tr'tabs print_ast_trtab1 print_ast_trtab2);
1.616
1.617 val pure_syn =
1.618 Syn (Syntax.pure_syn, (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
1.619
1.620 -val dummy_sg = make_sg (ref "", SgRef NONE, []) NameSpace.default_naming empty_data
1.621 - (pure_syn, Type.empty_tsig, NameSpace.empty_table);
1.622
1.623 -val pre_pure =
1.624 - create_sg "#" (SgRef (SOME (ref dummy_sg))) [] NameSpace.default_naming empty_data
1.625 - (pure_syn, Type.empty_tsig, NameSpace.empty_table);
1.626
1.627 -val PureN = "Pure";
1.628 -val CPureN = "CPure";
1.629 +(** datatype sign **)
1.630
1.631 +datatype sign = Sign of
1.632 + {naming: NameSpace.naming, (*common naming conventions*)
1.633 + syn: syn, (*concrete syntax for terms, types, sorts*)
1.634 + tsig: Type.tsig, (*order-sorted signature of types*)
1.635 + consts: (typ * stamp) NameSpace.table}; (*type schemes of term constants*)
1.636
1.637 +fun make_sign (naming, syn, tsig, consts) =
1.638 + Sign {naming = naming, syn = syn, tsig = tsig, consts = consts};
1.639
1.640 -(** signature content **)
1.641 +fun err_dup_consts cs =
1.642 + error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
1.643 +
1.644 +structure SignData = TheoryDataFun
1.645 +(struct
1.646 + val name = "Pure/sign";
1.647 + type T = sign;
1.648 + val copy = I;
1.649 + val extend = I;
1.650 +
1.651 + val empty =
1.652 + make_sign (NameSpace.default_naming, pure_syn, Type.empty_tsig, NameSpace.empty_table);
1.653 +
1.654 + fun merge pp (sign1, sign2) =
1.655 + let
1.656 + val Sign {naming = _, syn = Syn (syntax1, trfuns1), tsig = tsig1,
1.657 + consts = consts1} = sign1;
1.658 + val Sign {naming = _, syn = Syn (syntax2, trfuns2), tsig = tsig2,
1.659 + consts = consts2} = sign2;
1.660 +
1.661 + val naming = NameSpace.default_naming;
1.662 + val syntax = Syntax.merge_syntaxes syntax1 syntax2;
1.663 + val trfuns = merge_trfuns trfuns1 trfuns2;
1.664 + val syn = Syn (syntax, trfuns);
1.665 + val tsig = Type.merge_tsigs pp (tsig1, tsig2);
1.666 + val consts = NameSpace.merge_tables eq_snd (consts1, consts2)
1.667 + handle Symtab.DUPS cs => err_dup_consts cs;
1.668 + in make_sign (naming, syn, tsig, consts) end;
1.669 +
1.670 + fun print _ _ = ();
1.671 +end);
1.672 +
1.673 +val init = SignData.init;
1.674 +
1.675 +fun rep_sg thy = SignData.get thy |> (fn Sign args => args);
1.676 +
1.677 +fun map_sign f = SignData.map (fn Sign {naming, syn, tsig, consts} =>
1.678 + make_sign (f (naming, syn, tsig, consts)));
1.679 +
1.680 +fun map_naming f = map_sign (fn (naming, syn, tsig, consts) => (f naming, syn, tsig, consts));
1.681 +fun map_syn f = map_sign (fn (naming, syn, tsig, consts) => (naming, f syn, tsig, consts));
1.682 +fun map_tsig f = map_sign (fn (naming, syn, tsig, consts) => (naming, syn, f tsig, consts));
1.683 +fun map_consts f = map_sign (fn (naming, syn, tsig, consts) => (naming, syn, tsig, f consts));
1.684 +
1.685
1.686 (* naming *)
1.687
1.688 -fun naming_of (Sg (_, {naming, ...})) = naming;
1.689 -
1.690 +val naming_of = #naming o rep_sg;
1.691 val base_name = NameSpace.base;
1.692 val full_name = NameSpace.full o naming_of;
1.693 -fun full_name_path sg elems = NameSpace.full (NameSpace.add_path elems (naming_of sg));
1.694 +fun full_name_path thy elems = NameSpace.full (NameSpace.add_path elems (naming_of thy));
1.695 val declare_name = NameSpace.declare o naming_of;
1.696
1.697
1.698 @@ -485,14 +259,14 @@
1.699
1.700 fun map_syntax f (Syn (syntax, trfuns)) = Syn (f syntax, trfuns);
1.701
1.702 -fun make_syntax sg (Syn (syntax, (atrs, trs, tr's, atr's))) =
1.703 +fun make_syntax thy (Syn (syntax, (atrs, trs, tr's, atr's))) =
1.704 let
1.705 - fun apply (c, (f, s)) = (c, (f sg, s));
1.706 + fun apply (c, (f, s)) = (c, (f thy, s));
1.707 fun prep tab = map apply (Symtab.dest tab);
1.708 fun prep' tab = map apply (Symtab.dest_multi tab);
1.709 in syntax |> Syntax.extend_trfuns (prep atrs, prep trs, prep' tr's, prep' atr's) end;
1.710
1.711 -fun syn_of (sg as Sg ({syn, ...}, _)) = make_syntax sg syn;
1.712 +fun syn_of thy = make_syntax thy (#syn (rep_sg thy));
1.713
1.714
1.715 (* advanced translation functions *)
1.716 @@ -504,19 +278,10 @@
1.717 Syntax.extend_tr'tab tr's print_trtab,
1.718 Syntax.extend_tr'tab atr's print_ast_trtab));
1.719
1.720 -fun merge_trfuns
1.721 - (parse_ast_trtab1, parse_trtab1, print_trtab1, print_ast_trtab1)
1.722 - (parse_ast_trtab2, parse_trtab2, print_trtab2, print_ast_trtab2) =
1.723 - (Syntax.merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2,
1.724 - Syntax.merge_trtabs "parse translation" parse_trtab1 parse_trtab2,
1.725 - Syntax.merge_tr'tabs print_trtab1 print_trtab2,
1.726 - Syntax.merge_tr'tabs print_ast_trtab1 print_ast_trtab2);
1.727 -
1.728
1.729 (* type signature *)
1.730
1.731 val tsig_of = #tsig o rep_sg;
1.732 -
1.733 val classes = Type.classes o tsig_of;
1.734 val defaultS = Type.defaultS o tsig_of;
1.735 val subsort = Type.subsort o tsig_of;
1.736 @@ -524,21 +289,21 @@
1.737 val witness_sorts = Type.witness_sorts o tsig_of;
1.738 val universal_witness = Type.universal_witness o tsig_of;
1.739 val typ_instance = Type.typ_instance o tsig_of;
1.740 -fun is_logtype sg c = c mem_string Type.logical_types (tsig_of sg);
1.741 +fun is_logtype thy c = c mem_string Type.logical_types (tsig_of thy);
1.742
1.743
1.744 (* consts signature *)
1.745
1.746 -fun const_type (Sg (_, {consts, ...})) c = Option.map #1 (Symtab.lookup (#2 consts, c));
1.747 +fun const_type thy c = Option.map #1 (Symtab.lookup (#2 (#consts (rep_sg thy)), c));
1.748
1.749 -fun the_const_type sg c =
1.750 - (case const_type sg c of SOME T => T
1.751 +fun the_const_type thy c =
1.752 + (case const_type thy c of SOME T => T
1.753 | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
1.754
1.755 -fun declared_tyname sg c =
1.756 - is_some (Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of sg))), c));
1.757 +fun declared_tyname thy c =
1.758 + is_some (Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of thy))), c));
1.759
1.760 -fun declared_const sg c = is_some (const_type sg c);
1.761 +val declared_const = is_some oo const_type;
1.762
1.763
1.764
1.765 @@ -567,16 +332,16 @@
1.766 fun get x = if_none (assoc_string (tab, x)) x;
1.767 in get end;
1.768
1.769 -fun typ_mapping f g sg T =
1.770 +fun typ_mapping f g thy T =
1.771 T |> Term.map_typ
1.772 - (mapping add_typ_classes (f sg) T)
1.773 - (mapping add_typ_tycons (g sg) T);
1.774 + (mapping add_typ_classes (f thy) T)
1.775 + (mapping add_typ_tycons (g thy) T);
1.776
1.777 -fun term_mapping f g h sg t =
1.778 +fun term_mapping f g h thy t =
1.779 t |> Term.map_term
1.780 - (mapping add_term_classes (f sg) t)
1.781 - (mapping add_term_tycons (g sg) t)
1.782 - (mapping add_term_consts (h sg) t);
1.783 + (mapping add_term_classes (f thy) t)
1.784 + (mapping add_term_tycons (g thy) t)
1.785 + (mapping add_term_consts (h thy) t);
1.786
1.787 in
1.788
1.789 @@ -592,21 +357,22 @@
1.790
1.791 (** pretty printing of terms, types etc. **)
1.792
1.793 -fun pretty_term' syn sg t = Syntax.pretty_term syn (exists_stamp CPureN sg) (extern_term sg t);
1.794 -fun pretty_term sg t = pretty_term' (syn_of sg) sg t;
1.795 -fun pretty_typ sg T = Syntax.pretty_typ (syn_of sg) (extern_typ sg T);
1.796 -fun pretty_sort sg S = Syntax.pretty_sort (syn_of sg) (extern_sort sg S);
1.797 +fun pretty_term' syn thy t =
1.798 + Syntax.pretty_term syn (Context.exists_name Context.CPureN thy) (extern_term thy t);
1.799 +fun pretty_term thy t = pretty_term' (syn_of thy) thy t;
1.800 +fun pretty_typ thy T = Syntax.pretty_typ (syn_of thy) (extern_typ thy T);
1.801 +fun pretty_sort thy S = Syntax.pretty_sort (syn_of thy) (extern_sort thy S);
1.802
1.803 -fun pretty_classrel sg cs = Pretty.block (List.concat
1.804 - (separate [Pretty.str " <", Pretty.brk 1] (map (single o pretty_sort sg o single) cs)));
1.805 +fun pretty_classrel thy cs = Pretty.block (List.concat
1.806 + (separate [Pretty.str " <", Pretty.brk 1] (map (single o pretty_sort thy o single) cs)));
1.807
1.808 -fun pretty_arity sg (a, Ss, S) =
1.809 +fun pretty_arity thy (a, Ss, S) =
1.810 let
1.811 - val a' = extern_type sg a;
1.812 + val a' = extern_type thy a;
1.813 val dom =
1.814 if null Ss then []
1.815 - else [Pretty.list "(" ")" (map (pretty_sort sg) Ss), Pretty.brk 1];
1.816 - in Pretty.block ([Pretty.str (a' ^ " ::"), Pretty.brk 1] @ dom @ [pretty_sort sg S]) end;
1.817 + else [Pretty.list "(" ")" (map (pretty_sort thy) Ss), Pretty.brk 1];
1.818 + in Pretty.block ([Pretty.str (a' ^ " ::"), Pretty.brk 1] @ dom @ [pretty_sort thy S]) end;
1.819
1.820 val string_of_term = Pretty.string_of oo pretty_term;
1.821 val string_of_typ = Pretty.string_of oo pretty_typ;
1.822 @@ -617,8 +383,8 @@
1.823 val pprint_term = (Pretty.pprint o Pretty.quote) oo pretty_term;
1.824 val pprint_typ = (Pretty.pprint o Pretty.quote) oo pretty_typ;
1.825
1.826 -fun pp sg = Pretty.pp (pretty_term sg, pretty_typ sg, pretty_sort sg,
1.827 - pretty_classrel sg, pretty_arity sg);
1.828 +fun pp thy = Pretty.pp (pretty_term thy, pretty_typ thy, pretty_sort thy,
1.829 + pretty_classrel thy, pretty_arity thy);
1.830
1.831
1.832
1.833 @@ -626,7 +392,7 @@
1.834
1.835 (* certify wrt. type signature *)
1.836
1.837 -fun certify cert = cert o tsig_of o check_stale "Sign.certify";
1.838 +fun certify cert = cert o tsig_of o Context.check_thy "Sign.certify";
1.839
1.840 val certify_class = certify Type.cert_class;
1.841 val certify_sort = certify Type.cert_sort;
1.842 @@ -669,11 +435,11 @@
1.843
1.844 in
1.845
1.846 -fun certify_term pp sg tm =
1.847 +fun certify_term pp thy tm =
1.848 let
1.849 - val _ = check_stale "Sign.certify_term" sg;
1.850 + val _ = Context.check_thy "Sign.certify_term" thy;
1.851
1.852 - val tm' = map_term_types (Type.cert_typ (tsig_of sg)) tm;
1.853 + val tm' = map_term_types (certify_typ thy) tm;
1.854 val tm' = if tm = tm' then tm else tm'; (*avoid copying of already normal term*)
1.855
1.856 fun err msg = raise TYPE (msg, [], [tm']);
1.857 @@ -683,10 +449,10 @@
1.858 fun check_atoms (t $ u) = (check_atoms t; check_atoms u)
1.859 | check_atoms (Abs (_, _, t)) = check_atoms t
1.860 | check_atoms (Const (a, T)) =
1.861 - (case const_type sg a of
1.862 + (case const_type thy a of
1.863 NONE => err ("Undeclared constant " ^ show_const a T)
1.864 | SOME U =>
1.865 - if typ_instance sg (T, U) then ()
1.866 + if typ_instance thy (T, U) then ()
1.867 else err ("Illegal type for constant " ^ show_const a T))
1.868 | check_atoms (Var ((x, i), _)) =
1.869 if i < 0 then err ("Malformed variable: " ^ quote x) else ()
1.870 @@ -700,60 +466,61 @@
1.871
1.872
1.873
1.874 -(** read and certify entities **) (*exception ERROR/TYPE*)
1.875 +(** read and certify entities **) (*exception ERROR*)
1.876
1.877 (* sorts *)
1.878
1.879 -fun read_sort' syn sg str =
1.880 +fun read_sort' syn thy str =
1.881 let
1.882 - val _ = check_stale "Sign.read_sort'" sg;
1.883 - val S = intern_sort sg (Syntax.read_sort syn str);
1.884 - in Type.cert_sort (tsig_of sg) S handle TYPE (msg, _, _) => error msg end;
1.885 + val _ = Context.check_thy "Sign.read_sort'" thy;
1.886 + val S = intern_sort thy (Syntax.read_sort syn str);
1.887 + in certify_sort thy S handle TYPE (msg, _, _) => error msg end;
1.888
1.889 -fun read_sort sg str = read_sort' (syn_of sg) sg str;
1.890 +fun read_sort thy str = read_sort' (syn_of thy) thy str;
1.891
1.892
1.893 (* types *)
1.894
1.895 local
1.896
1.897 -fun gen_read_typ' cert syn (sg, def_sort) str =
1.898 +fun gen_read_typ' cert syn (thy, def_sort) str =
1.899 let
1.900 - val _ = check_stale "Sign.gen_read_typ'" sg;
1.901 - val get_sort = TypeInfer.get_sort (tsig_of sg) def_sort (intern_sort sg);
1.902 - val T = intern_tycons sg (Syntax.read_typ syn get_sort (intern_sort sg) str);
1.903 - in cert (tsig_of sg) T handle TYPE (msg, _, _) => error msg end
1.904 + val _ = Context.check_thy "Sign.gen_read_typ'" thy;
1.905 + val get_sort = TypeInfer.get_sort (tsig_of thy) def_sort (intern_sort thy);
1.906 + val T = intern_tycons thy (Syntax.read_typ syn get_sort (intern_sort thy) str);
1.907 + in cert thy T handle TYPE (msg, _, _) => error msg end
1.908 handle ERROR => error ("The error(s) above occurred in type " ^ quote str);
1.909
1.910 -fun gen_read_typ cert (sg, def_sort) str = gen_read_typ' cert (syn_of sg) (sg, def_sort) str;
1.911 +fun gen_read_typ cert (thy, def_sort) str =
1.912 + gen_read_typ' cert (syn_of thy) (thy, def_sort) str;
1.913
1.914 in
1.915
1.916 -fun no_def_sort sg = (sg, K NONE);
1.917 +fun no_def_sort thy = (thy: theory, K NONE);
1.918
1.919 -val read_typ' = gen_read_typ' Type.cert_typ;
1.920 -val read_typ_syntax' = gen_read_typ' Type.cert_typ_syntax;
1.921 -val read_typ_abbrev' = gen_read_typ' Type.cert_typ_abbrev;
1.922 -val read_typ = gen_read_typ Type.cert_typ;
1.923 -val read_typ_syntax = gen_read_typ Type.cert_typ_syntax;
1.924 -val read_typ_abbrev = gen_read_typ Type.cert_typ_abbrev;
1.925 +val read_typ' = gen_read_typ' certify_typ;
1.926 +val read_typ_syntax' = gen_read_typ' certify_typ_syntax;
1.927 +val read_typ_abbrev' = gen_read_typ' certify_typ_abbrev;
1.928 +val read_typ = gen_read_typ certify_typ;
1.929 +val read_typ_syntax = gen_read_typ certify_typ_syntax;
1.930 +val read_typ_abbrev = gen_read_typ certify_typ_abbrev;
1.931
1.932 end;
1.933
1.934
1.935 (* type and constant names *)
1.936
1.937 -fun read_tyname sg raw_c =
1.938 - let val c = intern_type sg raw_c in
1.939 - (case Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of sg))), c) of
1.940 +fun read_tyname thy raw_c =
1.941 + let val c = intern_type thy raw_c in
1.942 + (case Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of thy))), c) of
1.943 SOME (Type.LogicalType n, _) => Type (c, replicate n dummyT)
1.944 | _ => error ("Undeclared type constructor: " ^ quote c))
1.945 end;
1.946
1.947 -fun read_const sg raw_c =
1.948 +fun read_const thy raw_c =
1.949 let
1.950 - val c = intern_const sg raw_c;
1.951 - val _ = the_const_type sg c handle TYPE (msg, _, _) => error msg;
1.952 + val c = intern_const thy raw_c;
1.953 + val _ = the_const_type thy c handle TYPE (msg, _, _) => error msg;
1.954 in Const (c, dummyT) end;
1.955
1.956
1.957 @@ -770,17 +537,15 @@
1.958 typs: expected types
1.959 *)
1.960
1.961 -fun infer_types_simult pp sg def_type def_sort used freeze args =
1.962 +fun infer_types_simult pp thy def_type def_sort used freeze args =
1.963 let
1.964 - val tsig = tsig_of sg;
1.965 -
1.966 val termss = foldr multiply [[]] (map fst args);
1.967 val typs =
1.968 - map (fn (_, T) => certify_typ sg T handle TYPE (msg, _, _) => error msg) args;
1.969 + map (fn (_, T) => certify_typ thy T handle TYPE (msg, _, _) => error msg) args;
1.970
1.971 - fun infer ts = OK (TypeInfer.infer_types (Syntax.pp_show_brackets pp) tsig
1.972 - (const_type sg) def_type def_sort (intern_const sg) (intern_tycons sg)
1.973 - (intern_sort sg) used freeze typs ts)
1.974 + fun infer ts = OK (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
1.975 + (const_type thy) def_type def_sort (intern_const thy) (intern_tycons thy)
1.976 + (intern_sort thy) used freeze typs ts)
1.977 handle TYPE (msg, _, _) => Error msg;
1.978
1.979 val err_results = map infer termss;
1.980 @@ -806,26 +571,25 @@
1.981 cat_lines (map (Pretty.string_of_term pp) (List.concat (map fst results)))))
1.982 end;
1.983
1.984 +fun infer_types pp thy def_type def_sort used freeze tsT =
1.985 + apfst hd (infer_types_simult pp thy def_type def_sort used freeze [tsT]);
1.986
1.987 -fun infer_types pp sg def_type def_sort used freeze tsT =
1.988 - apfst hd (infer_types_simult pp sg def_type def_sort used freeze [tsT]);
1.989
1.990
1.991 +(** read_def_terms -- read terms and infer types **) (*exception ERROR*)
1.992
1.993 -(** read_def_terms -- read terms and infer types **)
1.994 -
1.995 -fun read_def_terms' pp is_logtype syn (sg, types, sorts) used freeze sTs =
1.996 +fun read_def_terms' pp is_logtype syn (thy, types, sorts) used freeze sTs =
1.997 let
1.998 fun read (s, T) =
1.999 - let val T' = certify_typ sg T handle TYPE (msg, _, _) => error msg
1.1000 + let val T' = certify_typ thy T handle TYPE (msg, _, _) => error msg
1.1001 in (Syntax.read is_logtype syn T' s, T') end;
1.1002 - in infer_types_simult pp sg types sorts used freeze (map read sTs) end;
1.1003 + in infer_types_simult pp thy types sorts used freeze (map read sTs) end;
1.1004
1.1005 -fun read_def_terms (sg, types, sorts) =
1.1006 - read_def_terms' (pp sg) (is_logtype sg) (syn_of sg) (sg, types, sorts);
1.1007 +fun read_def_terms (thy, types, sorts) =
1.1008 + read_def_terms' (pp thy) (is_logtype thy) (syn_of thy) (thy, types, sorts);
1.1009
1.1010 -fun simple_read_term sg T s =
1.1011 - let val ([t], _) = read_def_terms (sg, K NONE, K NONE) [] true [(s, T)]
1.1012 +fun simple_read_term thy T s =
1.1013 + let val ([t], _) = read_def_terms (thy, K NONE, K NONE) [] true [(s, T)]
1.1014 in t end
1.1015 handle ERROR => error ("The error(s) above occurred for term " ^ s);
1.1016
1.1017 @@ -835,8 +599,8 @@
1.1018
1.1019 (* add default sort *)
1.1020
1.1021 -fun gen_add_defsort prep_sort s sg =
1.1022 - sg |> map_tsig (Type.set_defsort (prep_sort sg s));
1.1023 +fun gen_add_defsort prep_sort s thy =
1.1024 + thy |> map_tsig (Type.set_defsort (prep_sort thy s));
1.1025
1.1026 val add_defsort = gen_add_defsort read_sort;
1.1027 val add_defsort_i = gen_add_defsort certify_sort;
1.1028 @@ -844,34 +608,41 @@
1.1029
1.1030 (* add type constructors *)
1.1031
1.1032 -fun add_types types sg = sg |> map_sign (fn (syn, tsig, consts) =>
1.1033 +fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
1.1034 let
1.1035 val syn' = map_syntax (Syntax.extend_type_gram types) syn;
1.1036 val decls = map (fn (a, n, mx) => (Syntax.type_name a mx, n)) types;
1.1037 - val tsig' = Type.add_types (naming_of sg) decls tsig;
1.1038 - in (syn', tsig', consts) end);
1.1039 + val tsig' = Type.add_types naming decls tsig;
1.1040 + in (naming, syn', tsig', consts) end);
1.1041 +
1.1042 +fun add_typedecls decls thy =
1.1043 + let
1.1044 + fun type_of (a, vs, mx) =
1.1045 + if null (duplicates vs) then (a, length vs, mx)
1.1046 + else error ("Duplicate parameters in type declaration: " ^ quote a);
1.1047 + in add_types (map type_of decls) thy end;
1.1048
1.1049
1.1050 (* add nonterminals *)
1.1051
1.1052 -fun add_nonterminals bnames sg = sg |> map_sign (fn (syn, tsig, consts) =>
1.1053 +fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
1.1054 let
1.1055 - val syn' = map_syntax (Syntax.extend_consts bnames) syn;
1.1056 - val tsig' = Type.add_nonterminals (naming_of sg) bnames tsig;
1.1057 - in (syn', tsig', consts) end);
1.1058 + val syn' = map_syntax (Syntax.extend_consts ns) syn;
1.1059 + val tsig' = Type.add_nonterminals naming ns tsig;
1.1060 + in (naming, syn', tsig', consts) end);
1.1061
1.1062
1.1063 (* add type abbreviations *)
1.1064
1.1065 -fun gen_add_tyabbr prep_typ (a, vs, rhs, mx) sg =
1.1066 - sg |> map_sign (fn (syn, tsig, consts) =>
1.1067 +fun gen_add_tyabbr prep_typ (a, vs, rhs, mx) thy =
1.1068 + thy |> map_sign (fn (naming, syn, tsig, consts) =>
1.1069 let
1.1070 val syn' = map_syntax (Syntax.extend_type_gram [(a, length vs, mx)]) syn;
1.1071 val a' = Syntax.type_name a mx;
1.1072 - val abbr = (a', vs, prep_typ sg rhs) handle ERROR =>
1.1073 - error ("in type abbreviation " ^ quote a');
1.1074 - val tsig' = Type.add_abbrevs (naming_of sg) [abbr] tsig;
1.1075 - in (syn', tsig', consts) end);
1.1076 + val abbr = (a', vs, prep_typ thy rhs)
1.1077 + handle ERROR => error ("in type abbreviation " ^ quote a');
1.1078 + val tsig' = Type.add_abbrevs naming [abbr] tsig;
1.1079 + in (naming, syn', tsig', consts) end);
1.1080
1.1081 val add_tyabbrs = fold (gen_add_tyabbr (read_typ_syntax o no_def_sort));
1.1082 val add_tyabbrs_i = fold (gen_add_tyabbr certify_typ_syntax);
1.1083 @@ -879,11 +650,11 @@
1.1084
1.1085 (* add type arities *)
1.1086
1.1087 -fun gen_add_arities int_type prep_sort arities sg = sg |> map_tsig (fn tsig =>
1.1088 +fun gen_add_arities int_type prep_sort arities thy = thy |> map_tsig (fn tsig =>
1.1089 let
1.1090 - fun prep_arity (a, Ss, S) = (int_type sg a, map (prep_sort sg) Ss, prep_sort sg S)
1.1091 + fun prep_arity (a, Ss, S) = (int_type thy a, map (prep_sort thy) Ss, prep_sort thy S)
1.1092 handle ERROR => error ("in arity for type " ^ quote a);
1.1093 - val tsig' = Type.add_arities (pp sg) (map prep_arity arities) tsig;
1.1094 + val tsig' = Type.add_arities (pp thy) (map prep_arity arities) tsig;
1.1095 in tsig' end);
1.1096
1.1097 val add_arities = gen_add_arities intern_type read_sort;
1.1098 @@ -892,37 +663,39 @@
1.1099
1.1100 (* modify syntax *)
1.1101
1.1102 -fun gen_syntax change_gram prep_typ (prmode, args) sg =
1.1103 +fun gen_syntax change_gram prep_typ prmode args thy =
1.1104 let
1.1105 - fun prep (c, T, mx) = (c, prep_typ sg T, mx) handle ERROR =>
1.1106 - error ("in syntax declaration " ^ quote (Syntax.const_name c mx));
1.1107 - in sg |> map_syn (map_syntax (change_gram (is_logtype sg) prmode (map prep args))) end;
1.1108 + fun prep (c, T, mx) = (c, prep_typ thy T, mx)
1.1109 + handle ERROR => error ("in syntax declaration " ^ quote (Syntax.const_name c mx));
1.1110 + in thy |> map_syn (map_syntax (change_gram (is_logtype thy) prmode (map prep args))) end;
1.1111
1.1112 fun gen_add_syntax x = gen_syntax Syntax.extend_const_gram x;
1.1113
1.1114 val add_modesyntax = gen_add_syntax (read_typ_syntax o no_def_sort);
1.1115 val add_modesyntax_i = gen_add_syntax certify_typ_syntax;
1.1116 -val add_syntax = curry add_modesyntax Syntax.default_mode;
1.1117 -val add_syntax_i = curry add_modesyntax_i Syntax.default_mode;
1.1118 +val add_syntax = add_modesyntax Syntax.default_mode;
1.1119 +val add_syntax_i = add_modesyntax_i Syntax.default_mode;
1.1120 val del_modesyntax = gen_syntax Syntax.remove_const_gram (read_typ_syntax o no_def_sort);
1.1121 val del_modesyntax_i = gen_syntax Syntax.remove_const_gram certify_typ_syntax;
1.1122
1.1123
1.1124 (* add constants *)
1.1125
1.1126 -fun err_dup_consts cs =
1.1127 - error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
1.1128 -
1.1129 -fun gen_add_consts prep_typ raw_args sg =
1.1130 +fun gen_add_consts prep_typ raw_args thy =
1.1131 let
1.1132 - val prepT = compress_type o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ sg;
1.1133 + val prepT = compress_type o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
1.1134 fun prep (c, T, mx) = ((c, prepT T, mx) handle TYPE (msg, _, _) => error msg)
1.1135 handle ERROR => error ("in declaration of constant " ^ quote (Syntax.const_name c mx));
1.1136 val args = map prep raw_args;
1.1137 val decls = args |> map (fn (c, T, mx) => (Syntax.const_name c mx, (T, stamp ())));
1.1138 - fun extend_consts consts = NameSpace.extend_table (naming_of sg) (consts, decls)
1.1139 +
1.1140 + fun extend_consts consts = NameSpace.extend_table (naming_of thy) (consts, decls)
1.1141 handle Symtab.DUPS cs => err_dup_consts cs;
1.1142 - in sg |> map_consts extend_consts |> add_syntax_i args end;
1.1143 + in
1.1144 + thy
1.1145 + |> map_consts extend_consts
1.1146 + |> add_syntax_i args
1.1147 + end;
1.1148
1.1149 val add_consts = gen_add_consts (read_typ o no_def_sort);
1.1150 val add_consts_i = gen_add_consts certify_typ;
1.1151 @@ -936,13 +709,13 @@
1.1152 fun class_of_const c = unsuffix classN c
1.1153 handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
1.1154
1.1155 -fun gen_add_class int_class (bclass, raw_classes) sg =
1.1156 - sg |> map_sign (fn (syn, tsig, consts) =>
1.1157 +fun gen_add_class int_class (bclass, raw_classes) thy =
1.1158 + thy |> map_sign (fn (naming, syn, tsig, consts) =>
1.1159 let
1.1160 - val classes = map (int_class sg) raw_classes;
1.1161 + val classes = map (int_class thy) raw_classes;
1.1162 val syn' = map_syntax (Syntax.extend_consts [bclass]) syn;
1.1163 - val tsig' = Type.add_classes (pp sg) (naming_of sg) [(bclass, classes)] tsig;
1.1164 - in (syn', tsig', consts) end)
1.1165 + val tsig' = Type.add_classes (pp thy) naming [(bclass, classes)] tsig;
1.1166 + in (naming, syn', tsig', consts) end)
1.1167 |> add_consts_i [(const_of_class bclass, a_itselfT --> propT, Syntax.NoSyn)];
1.1168
1.1169 val add_classes = fold (gen_add_class intern_class);
1.1170 @@ -951,10 +724,10 @@
1.1171
1.1172 (* add to classrel *)
1.1173
1.1174 -fun gen_add_classrel int_class raw_pairs sg = sg |> map_tsig (fn tsig =>
1.1175 +fun gen_add_classrel int_class raw_pairs thy = thy |> map_tsig (fn tsig =>
1.1176 let
1.1177 - val pairs = map (pairself (int_class sg)) raw_pairs;
1.1178 - val tsig' = Type.add_classrel (pp sg) pairs tsig;
1.1179 + val pairs = map (pairself (int_class thy)) raw_pairs;
1.1180 + val tsig' = Type.add_classrel (pp thy) pairs tsig;
1.1181 in tsig' end);
1.1182
1.1183 val add_classrel = gen_add_classrel intern_class;
1.1184 @@ -967,13 +740,13 @@
1.1185
1.1186 fun mk trs = map Syntax.mk_trfun trs;
1.1187
1.1188 -fun gen_add_trfuns ext non_typed (atrs, trs, tr's, atr's) sg = sg |> map_syn (fn syn =>
1.1189 +fun gen_add_trfuns ext non_typed (atrs, trs, tr's, atr's) thy = thy |> map_syn (fn syn =>
1.1190 let val syn' = syn |> ext (mk atrs, mk trs, mk (map (apsnd non_typed) tr's), mk atr's)
1.1191 - in make_syntax sg syn'; syn' end);
1.1192 + in make_syntax thy syn'; syn' end);
1.1193
1.1194 -fun gen_add_trfunsT ext tr's sg = sg |> map_syn (fn syn =>
1.1195 +fun gen_add_trfunsT ext tr's thy = thy |> map_syn (fn syn =>
1.1196 let val syn' = syn |> ext ([], [], mk tr's, [])
1.1197 - in make_syntax sg syn'; syn' end);
1.1198 + in make_syntax thy syn'; syn' end);
1.1199
1.1200 in
1.1201
1.1202 @@ -985,13 +758,14 @@
1.1203 end;
1.1204
1.1205 val add_tokentrfuns = map_syn o map_syntax o Syntax.extend_tokentrfuns;
1.1206 +fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f));
1.1207
1.1208
1.1209 (* add translation rules *)
1.1210
1.1211 -fun add_trrules args sg = sg |> map_syn (fn syn =>
1.1212 - let val rules = map (Syntax.map_trrule (apfst (intern_type sg))) args
1.1213 - in map_syntax (Syntax.extend_trrules (is_logtype sg) (make_syntax sg syn) rules) syn end);
1.1214 +fun add_trrules args thy = thy |> map_syn (fn syn =>
1.1215 + let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args
1.1216 + in map_syntax (Syntax.extend_trrules (is_logtype thy) (make_syntax thy syn) rules) syn end);
1.1217
1.1218 val add_trrules_i = map_syn o map_syntax o Syntax.extend_trrules_i;
1.1219
1.1220 @@ -1005,89 +779,21 @@
1.1221 val set_policy = map_naming o NameSpace.set_policy;
1.1222 val restore_naming = map_naming o K o naming_of;
1.1223
1.1224 +val parent_path = add_path "..";
1.1225 +val root_path = add_path "/";
1.1226 +val absolute_path = add_path "//";
1.1227 +
1.1228 +fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
1.1229 +
1.1230
1.1231 (* hide names *)
1.1232
1.1233 -fun hide_classes b xs sg = sg |> map_tsig (Type.hide_classes b (map (intern_class sg) xs));
1.1234 +fun hide_classes b xs thy = thy |> map_tsig (Type.hide_classes b (map (intern_class thy) xs));
1.1235 val hide_classes_i = map_tsig oo Type.hide_classes;
1.1236 -fun hide_types b xs sg = sg |> map_tsig (Type.hide_types b (map (intern_type sg) xs));
1.1237 +fun hide_types b xs thy = thy |> map_tsig (Type.hide_types b (map (intern_type thy) xs));
1.1238 val hide_types_i = map_tsig oo Type.hide_types;
1.1239 -fun hide_consts b xs sg =
1.1240 - sg |> map_consts (apfst (fold (NameSpace.hide b o intern_const sg) xs));
1.1241 +fun hide_consts b xs thy =
1.1242 + thy |> map_consts (apfst (fold (NameSpace.hide b o intern_const thy) xs));
1.1243 val hide_consts_i = (map_consts o apfst) oo (fold o NameSpace.hide);
1.1244
1.1245 -
1.1246 -
1.1247 -(** merge signatures **)
1.1248 -
1.1249 -fun merge_stamps stamps1 stamps2 =
1.1250 - let val stamps = merge_lists' stamps1 stamps2 in
1.1251 - (case duplicates (map ! stamps) of
1.1252 - [] => stamps
1.1253 - | dups => error ("Attempt to merge different versions of theories " ^ commas_quote dups))
1.1254 - end;
1.1255 -
1.1256 -
1.1257 -(* trivial merge *)
1.1258 -
1.1259 -fun merge_refs (sgr1 as SgRef (SOME (ref (sg1 as Sg ({stamps = s1, ...}, _)))),
1.1260 - sgr2 as SgRef (SOME (ref (sg2 as Sg ({stamps = s2, ...}, _))))) =
1.1261 - if subsig (sg2, sg1) then sgr1
1.1262 - else if subsig (sg1, sg2) then sgr2
1.1263 - else (merge_stamps s1 s2; (*check for different versions*)
1.1264 - error ("Attempt to do non-trivial merge of signature\n" ^
1.1265 - str_of_sg sg1 ^ " and " ^ str_of_sg sg2))
1.1266 - | merge_refs _ = sys_error "Sign.merge_refs";
1.1267 -
1.1268 -val merge = deref o merge_refs o pairself self_ref;
1.1269 -
1.1270 -
1.1271 -(* non-trivial merge *) (*exception TERM/ERROR*)
1.1272 -
1.1273 -local
1.1274 -
1.1275 -fun nontriv_merge (sg1, sg2) =
1.1276 - if subsig_internal (sg2, sg1) then sg1
1.1277 - else if subsig_internal (sg1, sg2) then sg2
1.1278 - else
1.1279 - if exists_stamp CPureN sg1 <> exists_stamp CPureN sg2
1.1280 - then error "Cannot merge Pure and CPure developments"
1.1281 - else
1.1282 - let
1.1283 - val Sg ({id = _, stamps = stamps1, syn = Syn (syntax1, trfuns1)},
1.1284 - {self = _, tsig = tsig1, consts = consts1, naming = _, data = data1}) = sg1;
1.1285 - val Sg ({id = _, stamps = stamps2, syn = Syn (syntax2, trfuns2)},
1.1286 - {self = _, tsig = tsig2, consts = consts2, naming = _, data = data2}) = sg2;
1.1287 -
1.1288 - val stamps = merge_stamps stamps1 stamps2;
1.1289 - val syntax = Syntax.merge_syntaxes syntax1 syntax2;
1.1290 - val trfuns = merge_trfuns trfuns1 trfuns2;
1.1291 - val syn = Syn (syntax, trfuns);
1.1292 - val consts = NameSpace.merge_tables eq_snd (consts1, consts2)
1.1293 - handle Symtab.DUPS cs => err_dup_consts cs;
1.1294 - val naming = NameSpace.default_naming;
1.1295 - val data = merge_data (data1, data2);
1.1296 -
1.1297 - val pre_sg = make_sg (ref "", SgRef (SOME (ref dummy_sg)), ref "#" :: stamps1)
1.1298 - naming data (syn, tsig1, consts);
1.1299 - val tsig = Type.merge_tsigs (pp pre_sg) (tsig1, tsig2);
1.1300 -
1.1301 - val self = SgRef (SOME (ref dummy_sg));
1.1302 - val sg = make_sg (ref "", self, stamps) naming data (syn, tsig, consts);
1.1303 - in assign self sg; syn_of sg; sg end;
1.1304 -
1.1305 -in
1.1306 -
1.1307 -fun prep_ext_merge sgs =
1.1308 - if null sgs then
1.1309 - error "Merge: no parent theories"
1.1310 - else if exists is_draft sgs then
1.1311 - error "Attempt to merge draft theories"
1.1312 - else
1.1313 - Library.foldl nontriv_merge (hd sgs, tl sgs)
1.1314 - |> prep_ext
1.1315 - |> add_path "/";
1.1316 -
1.1317 end;
1.1318 -
1.1319 -end;