added add_const_constraint(_i), const_constraint;
authorwenzelm
Thu Jul 28 15:19:58 2005 +0200 (2005-07-28)
changeset 169410bda949449ee
parent 16940 d14ec6f2d29b
child 16942 c01816b32c04
added add_const_constraint(_i), const_constraint;
added typ_match, typ_unify;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Thu Jul 28 15:19:57 2005 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Jul 28 15:19:58 2005 +0200
     1.3 @@ -25,6 +25,8 @@
     1.4    val del_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
     1.5    val add_consts: (bstring * string * mixfix) list -> theory -> theory
     1.6    val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
     1.7 +  val add_const_constraint: xstring * string -> theory -> theory
     1.8 +  val add_const_constraint_i: string * typ -> theory -> theory
     1.9    val add_classes: (bstring * xstring list) list -> theory -> theory
    1.10    val add_classes_i: (bstring * class list) list -> theory -> theory
    1.11    val add_classrel: (xstring * xstring) list -> theory -> theory
    1.12 @@ -76,7 +78,7 @@
    1.13     {naming: NameSpace.naming,
    1.14      syn: Syntax.syntax,
    1.15      tsig: Type.tsig,
    1.16 -    consts: (typ * stamp) NameSpace.table}
    1.17 +    consts: (typ * stamp) NameSpace.table * typ Symtab.table}
    1.18    val naming_of: theory -> NameSpace.naming
    1.19    val base_name: string -> bstring
    1.20    val full_name: theory -> bstring -> string
    1.21 @@ -92,7 +94,10 @@
    1.22    val universal_witness: theory -> (typ * sort) option
    1.23    val all_sorts_nonempty: theory -> bool
    1.24    val typ_instance: theory -> typ * typ -> bool
    1.25 +  val typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv
    1.26 +  val typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int
    1.27    val is_logtype: theory -> string -> bool
    1.28 +  val const_constraint: theory -> string -> typ option
    1.29    val const_type: theory -> string -> typ option
    1.30    val the_const_type: theory -> string -> typ
    1.31    val declared_tyname: theory -> string -> bool
    1.32 @@ -178,7 +183,10 @@
    1.33   {naming: NameSpace.naming,                 (*common naming conventions*)
    1.34    syn: Syntax.syntax,                       (*concrete syntax for terms, types, sorts*)
    1.35    tsig: Type.tsig,                          (*order-sorted signature of types*)
    1.36 -  consts: (typ * stamp) NameSpace.table};   (*type schemes of term constants*)
    1.37 +  consts:
    1.38 +    (typ * stamp) NameSpace.table *         (*type schemes of declared term constants*)
    1.39 +    typ Symtab.table};                      (*type constraints for constants*)
    1.40 +
    1.41  
    1.42  fun make_sign (naming, syn, tsig, consts) =
    1.43    Sign {naming = naming, syn = syn, tsig = tsig, consts = consts};
    1.44 @@ -186,6 +194,9 @@
    1.45  fun err_dup_consts cs =
    1.46    error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
    1.47  
    1.48 +fun err_inconsistent_constraints cs =
    1.49 +  error ("Inconsistent type constraints for constant(s) " ^ commas_quote cs);
    1.50 +
    1.51  structure SignData = TheoryDataFun
    1.52  (struct
    1.53    val name = "Pure/sign";
    1.54 @@ -193,20 +204,22 @@
    1.55    val copy = I;
    1.56    val extend = I;
    1.57  
    1.58 -  val empty =
    1.59 -    make_sign (NameSpace.default_naming, Syntax.pure_syn, Type.empty_tsig, NameSpace.empty_table);
    1.60 +  val empty = make_sign (NameSpace.default_naming, Syntax.pure_syn, Type.empty_tsig,
    1.61 +    (NameSpace.empty_table, Symtab.empty));
    1.62  
    1.63    fun merge pp (sign1, sign2) =
    1.64      let
    1.65 -      val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1;
    1.66 -      val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
    1.67 +      val Sign {naming = _, syn = syn1, tsig = tsig1, consts = (consts1, constraints1)} = sign1;
    1.68 +      val Sign {naming = _, syn = syn2, tsig = tsig2, consts = (consts2, constraints2)} = sign2;
    1.69  
    1.70        val naming = NameSpace.default_naming;
    1.71        val syn = Syntax.merge_syntaxes syn1 syn2;
    1.72        val tsig = Type.merge_tsigs pp (tsig1, tsig2);
    1.73        val consts = NameSpace.merge_tables eq_snd (consts1, consts2)
    1.74          handle Symtab.DUPS cs => err_dup_consts cs;
    1.75 -    in make_sign (naming, syn, tsig, consts) end;
    1.76 +      val constraints = Symtab.merge (op =) (constraints1, constraints2)
    1.77 +        handle Symtab.DUPS cs => err_inconsistent_constraints cs;
    1.78 +    in make_sign (naming, syn, tsig, (consts, constraints)) end;
    1.79  
    1.80    fun print _ _ = ();
    1.81  end);
    1.82 @@ -249,12 +262,21 @@
    1.83  val universal_witness = Type.universal_witness o tsig_of;
    1.84  val all_sorts_nonempty = is_some o universal_witness;
    1.85  val typ_instance = Type.typ_instance o tsig_of;
    1.86 +val typ_match = Type.typ_match o tsig_of;
    1.87 +val typ_unify = Type.unify o tsig_of;
    1.88  fun is_logtype thy c = c mem_string Type.logical_types (tsig_of thy);
    1.89  
    1.90  
    1.91  (* consts signature *)
    1.92  
    1.93 -fun const_type thy c = Option.map #1 (Symtab.lookup (#2 (#consts (rep_sg thy)), c));
    1.94 +fun const_constraint thy c =
    1.95 +  let val ((_, consts), constraints) = #consts (rep_sg thy) in
    1.96 +    (case Symtab.lookup (constraints, c) of
    1.97 +      NONE => Option.map #1 (Symtab.lookup (consts, c))
    1.98 +    | some => some)
    1.99 +  end;
   1.100 +
   1.101 +fun const_type thy c = Option.map #1 (Symtab.lookup (#2 (#1 (#consts (rep_sg thy))), c));
   1.102  
   1.103  fun the_const_type thy c =
   1.104    (case const_type thy c of SOME T => T
   1.105 @@ -269,7 +291,7 @@
   1.106  
   1.107  val class_space = #1 o #classes o Type.rep_tsig o tsig_of;
   1.108  val type_space = #1 o #types o Type.rep_tsig o tsig_of;
   1.109 -val const_space = #1 o #consts o rep_sg
   1.110 +val const_space = #1 o #1 o #consts o rep_sg
   1.111  
   1.112  val intern_class = NameSpace.intern o class_space;
   1.113  val extern_class = NameSpace.extern o class_space;
   1.114 @@ -509,7 +531,7 @@
   1.115        map (fn (_, T) => certify_typ thy T handle TYPE (msg, _, _) => error msg) args;
   1.116  
   1.117      fun infer ts = OK (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
   1.118 -        (const_type thy) def_type def_sort (intern_const thy) (intern_tycons thy)
   1.119 +        (const_constraint thy) def_type def_sort (intern_const thy) (intern_tycons thy)
   1.120          (intern_sort thy) used freeze typs ts)
   1.121        handle TYPE (msg, _, _) => Error msg;
   1.122  
   1.123 @@ -660,7 +682,7 @@
   1.124        handle Symtab.DUPS cs => err_dup_consts cs;
   1.125    in
   1.126      thy
   1.127 -    |> map_consts extend_consts
   1.128 +    |> map_consts (apfst extend_consts)
   1.129      |> add_syntax_i args
   1.130    end;
   1.131  
   1.132 @@ -668,6 +690,21 @@
   1.133  val add_consts_i = gen_add_consts certify_typ;
   1.134  
   1.135  
   1.136 +(* add constraints *)
   1.137 +
   1.138 +fun gen_add_constraint int_const prep_typ (raw_c, raw_T) thy =
   1.139 +  let
   1.140 +    val c = int_const thy raw_c;
   1.141 +    val T = Term.zero_var_indexesT (Term.no_dummyT (prep_typ thy raw_T))
   1.142 +      handle TYPE (msg, _, _) => error msg;
   1.143 +    val _ = cert_term thy (Const (c, T))
   1.144 +      handle TYPE (msg, _, _) => error msg;
   1.145 +  in thy |> map_consts (apsnd (curry Symtab.update (c, T))) end;
   1.146 +
   1.147 +val add_const_constraint = gen_add_constraint intern_const (read_typ o no_def_sort);
   1.148 +val add_const_constraint_i = gen_add_constraint (K I) certify_typ;
   1.149 +
   1.150 +
   1.151  (* add type classes *)
   1.152  
   1.153  val classN = "_class";
   1.154 @@ -757,7 +794,7 @@
   1.155  fun hide_types b xs thy = thy |> map_tsig (Type.hide_types b (map (intern_type thy) xs));
   1.156  val hide_types_i = map_tsig oo Type.hide_types;
   1.157  fun hide_consts b xs thy =
   1.158 -  thy |> map_consts (apfst (fold (NameSpace.hide b o intern_const thy) xs));
   1.159 -val hide_consts_i = (map_consts o apfst) oo (fold o NameSpace.hide);
   1.160 +  thy |> map_consts (apfst (apfst (fold (NameSpace.hide b o intern_const thy) xs)));
   1.161 +val hide_consts_i = (map_consts o apfst o apfst) oo (fold o NameSpace.hide);
   1.162  
   1.163  end;