# HG changeset patch # User wenzelm # Date 1122556798 -7200 # Node ID 0bda949449ee9bcd26de22cd5a9eb376bae38343 # Parent d14ec6f2d29ba1d6641e2109d486aadb4faedb08 added add_const_constraint(_i), const_constraint; added typ_match, typ_unify; diff -r d14ec6f2d29b -r 0bda949449ee src/Pure/sign.ML --- a/src/Pure/sign.ML Thu Jul 28 15:19:57 2005 +0200 +++ b/src/Pure/sign.ML Thu Jul 28 15:19:58 2005 +0200 @@ -25,6 +25,8 @@ val del_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory val add_consts: (bstring * string * mixfix) list -> theory -> theory val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory + val add_const_constraint: xstring * string -> theory -> theory + val add_const_constraint_i: string * typ -> theory -> theory val add_classes: (bstring * xstring list) list -> theory -> theory val add_classes_i: (bstring * class list) list -> theory -> theory val add_classrel: (xstring * xstring) list -> theory -> theory @@ -76,7 +78,7 @@ {naming: NameSpace.naming, syn: Syntax.syntax, tsig: Type.tsig, - consts: (typ * stamp) NameSpace.table} + consts: (typ * stamp) NameSpace.table * typ Symtab.table} val naming_of: theory -> NameSpace.naming val base_name: string -> bstring val full_name: theory -> bstring -> string @@ -92,7 +94,10 @@ val universal_witness: theory -> (typ * sort) option val all_sorts_nonempty: theory -> bool val typ_instance: theory -> typ * typ -> bool + val typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv + val typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int val is_logtype: theory -> string -> bool + val const_constraint: theory -> string -> typ option val const_type: theory -> string -> typ option val the_const_type: theory -> string -> typ val declared_tyname: theory -> string -> bool @@ -178,7 +183,10 @@ {naming: NameSpace.naming, (*common naming conventions*) syn: Syntax.syntax, (*concrete syntax for terms, types, sorts*) tsig: Type.tsig, (*order-sorted signature of types*) - consts: (typ * stamp) NameSpace.table}; (*type schemes of term constants*) + consts: + (typ * stamp) NameSpace.table * (*type schemes of declared term constants*) + typ Symtab.table}; (*type constraints for constants*) + fun make_sign (naming, syn, tsig, consts) = Sign {naming = naming, syn = syn, tsig = tsig, consts = consts}; @@ -186,6 +194,9 @@ fun err_dup_consts cs = error ("Duplicate declaration of constant(s) " ^ commas_quote cs); +fun err_inconsistent_constraints cs = + error ("Inconsistent type constraints for constant(s) " ^ commas_quote cs); + structure SignData = TheoryDataFun (struct val name = "Pure/sign"; @@ -193,20 +204,22 @@ val copy = I; val extend = I; - val empty = - make_sign (NameSpace.default_naming, Syntax.pure_syn, Type.empty_tsig, NameSpace.empty_table); + val empty = make_sign (NameSpace.default_naming, Syntax.pure_syn, Type.empty_tsig, + (NameSpace.empty_table, Symtab.empty)); fun merge pp (sign1, sign2) = let - val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1; - val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2; + val Sign {naming = _, syn = syn1, tsig = tsig1, consts = (consts1, constraints1)} = sign1; + val Sign {naming = _, syn = syn2, tsig = tsig2, consts = (consts2, constraints2)} = sign2; val naming = NameSpace.default_naming; val syn = Syntax.merge_syntaxes syn1 syn2; val tsig = Type.merge_tsigs pp (tsig1, tsig2); val consts = NameSpace.merge_tables eq_snd (consts1, consts2) handle Symtab.DUPS cs => err_dup_consts cs; - in make_sign (naming, syn, tsig, consts) end; + val constraints = Symtab.merge (op =) (constraints1, constraints2) + handle Symtab.DUPS cs => err_inconsistent_constraints cs; + in make_sign (naming, syn, tsig, (consts, constraints)) end; fun print _ _ = (); end); @@ -249,12 +262,21 @@ val universal_witness = Type.universal_witness o tsig_of; val all_sorts_nonempty = is_some o universal_witness; val typ_instance = Type.typ_instance o tsig_of; +val typ_match = Type.typ_match o tsig_of; +val typ_unify = Type.unify o tsig_of; fun is_logtype thy c = c mem_string Type.logical_types (tsig_of thy); (* consts signature *) -fun const_type thy c = Option.map #1 (Symtab.lookup (#2 (#consts (rep_sg thy)), c)); +fun const_constraint thy c = + let val ((_, consts), constraints) = #consts (rep_sg thy) in + (case Symtab.lookup (constraints, c) of + NONE => Option.map #1 (Symtab.lookup (consts, c)) + | some => some) + end; + +fun const_type thy c = Option.map #1 (Symtab.lookup (#2 (#1 (#consts (rep_sg thy))), c)); fun the_const_type thy c = (case const_type thy c of SOME T => T @@ -269,7 +291,7 @@ val class_space = #1 o #classes o Type.rep_tsig o tsig_of; val type_space = #1 o #types o Type.rep_tsig o tsig_of; -val const_space = #1 o #consts o rep_sg +val const_space = #1 o #1 o #consts o rep_sg val intern_class = NameSpace.intern o class_space; val extern_class = NameSpace.extern o class_space; @@ -509,7 +531,7 @@ map (fn (_, T) => certify_typ thy T handle TYPE (msg, _, _) => error msg) args; fun infer ts = OK (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy) - (const_type thy) def_type def_sort (intern_const thy) (intern_tycons thy) + (const_constraint thy) def_type def_sort (intern_const thy) (intern_tycons thy) (intern_sort thy) used freeze typs ts) handle TYPE (msg, _, _) => Error msg; @@ -660,7 +682,7 @@ handle Symtab.DUPS cs => err_dup_consts cs; in thy - |> map_consts extend_consts + |> map_consts (apfst extend_consts) |> add_syntax_i args end; @@ -668,6 +690,21 @@ val add_consts_i = gen_add_consts certify_typ; +(* add constraints *) + +fun gen_add_constraint int_const prep_typ (raw_c, raw_T) thy = + let + val c = int_const thy raw_c; + val T = Term.zero_var_indexesT (Term.no_dummyT (prep_typ thy raw_T)) + handle TYPE (msg, _, _) => error msg; + val _ = cert_term thy (Const (c, T)) + handle TYPE (msg, _, _) => error msg; + in thy |> map_consts (apsnd (curry Symtab.update (c, T))) end; + +val add_const_constraint = gen_add_constraint intern_const (read_typ o no_def_sort); +val add_const_constraint_i = gen_add_constraint (K I) certify_typ; + + (* add type classes *) val classN = "_class"; @@ -757,7 +794,7 @@ fun hide_types b xs thy = thy |> map_tsig (Type.hide_types b (map (intern_type thy) xs)); val hide_types_i = map_tsig oo Type.hide_types; fun hide_consts b xs thy = - thy |> map_consts (apfst (fold (NameSpace.hide b o intern_const thy) xs)); -val hide_consts_i = (map_consts o apfst) oo (fold o NameSpace.hide); + thy |> map_consts (apfst (apfst (fold (NameSpace.hide b o intern_const thy) xs))); +val hide_consts_i = (map_consts o apfst o apfst) oo (fold o NameSpace.hide); end;