# 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;