eliminated aliases of Type.constraint;
authorwenzelm
Sun Sep 12 19:04:02 2010 +0200 (2010-09-12)
changeset 39288f1ae2493d93f
parent 39287 d30be6791038
child 39289 92b50c8bb67b
eliminated aliases of Type.constraint;
src/HOL/Import/proof_kernel.ML
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Quotient/quotient_typ.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
src/HOL/Tools/primrec.ML
src/HOLCF/Tools/Domain/domain_library.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/rule_insts.ML
src/Pure/Isar/specification.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/type_ext.ML
src/Pure/Thy/thy_output.ML
src/Pure/type.ML
src/Pure/type_infer.ML
src/Tools/misc_legacy.ML
src/Tools/nbe.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/inductive_package.ML
src/ZF/ind_syntax.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Sun Sep 12 17:39:02 2010 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Sun Sep 12 19:04:02 2010 +0200
     1.3 @@ -222,7 +222,7 @@
     1.4                  val str =
     1.5                    G n Syntax.string_of_term (Config.put show_brackets false ctxt) (term_of ct)
     1.6                  val u = Syntax.parse_term ctxt str
     1.7 -                  |> Type_Infer.constrain T |> Syntax.check_term ctxt
     1.8 +                  |> Type.constraint T |> Syntax.check_term ctxt
     1.9              in
    1.10                  if match u
    1.11                  then quote str
     2.1 --- a/src/HOL/Tools/Function/function_core.ML	Sun Sep 12 17:39:02 2010 +0200
     2.2 +++ b/src/HOL/Tools/Function/function_core.ML	Sun Sep 12 19:04:02 2010 +0200
     2.3 @@ -879,7 +879,7 @@
     2.4      val ranT = range_type fT
     2.5  
     2.6      val default = Syntax.parse_term lthy default_str
     2.7 -      |> Type_Infer.constrain fT |> Syntax.check_term lthy
     2.8 +      |> Type.constraint fT |> Syntax.check_term lthy
     2.9  
    2.10      val (globals, ctxt') = fix_globals domT ranT fvar lthy
    2.11  
     3.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Sun Sep 12 17:39:02 2010 +0200
     3.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Sun Sep 12 19:04:02 2010 +0200
     3.3 @@ -276,7 +276,7 @@
     3.4      val lthy1 = Variable.declare_typ rty lthy
     3.5      val rel = 
     3.6        Syntax.parse_term lthy1 rel_str
     3.7 -      |> Syntax.type_constraint (rty --> rty --> @{typ bool}) 
     3.8 +      |> Type.constraint (rty --> rty --> @{typ bool}) 
     3.9        |> Syntax.check_term lthy1 
    3.10      val lthy2 = Variable.declare_term rel lthy1 
    3.11    in
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun Sep 12 17:39:02 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun Sep 12 19:04:02 2010 +0200
     4.3 @@ -437,7 +437,7 @@
     4.4    in repair_tvar_sorts (do_formula true phi Vartab.empty) end
     4.5  
     4.6  fun check_formula ctxt =
     4.7 -  Type_Infer.constrain HOLogic.boolT
     4.8 +  Type.constraint HOLogic.boolT
     4.9    #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
    4.10  
    4.11  
     5.1 --- a/src/HOL/Tools/primrec.ML	Sun Sep 12 17:39:02 2010 +0200
     5.2 +++ b/src/HOL/Tools/primrec.ML	Sun Sep 12 19:04:02 2010 +0200
     5.3 @@ -196,8 +196,7 @@
     5.4      val def_name = Thm.def_name (Long_Name.base_name fname);
     5.5      val raw_rhs = fold_rev (fn T => fn t => Abs ("", T, t)) (map snd ls @ [dummyT])
     5.6        (list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1))))
     5.7 -    val rhs = singleton (Syntax.check_terms ctxt)
     5.8 -      (Type_Infer.constrain varT raw_rhs);
     5.9 +    val rhs = singleton (Syntax.check_terms ctxt) (Type.constraint varT raw_rhs);
    5.10    in (var, ((Binding.conceal (Binding.name def_name), []), rhs)) end;
    5.11  
    5.12  
     6.1 --- a/src/HOLCF/Tools/Domain/domain_library.ML	Sun Sep 12 17:39:02 2010 +0200
     6.2 +++ b/src/HOLCF/Tools/Domain/domain_library.ML	Sun Sep 12 19:04:02 2010 +0200
     6.3 @@ -185,7 +185,7 @@
     6.4  fun mk_lam  (x,T) = Abs(x,dummyT,T);
     6.5  fun mk_all  (x,P) = HOLogic.mk_all (x,dummyT,P);
     6.6  fun mk_ex   (x,P) = mk_exists (x,dummyT,P);
     6.7 -fun mk_constrainall (x,typ,P) = %%: @{const_name All} $ (Type_Infer.constrain (typ --> boolT) (mk_lam(x,P)));
     6.8 +fun mk_constrainall (x,typ,P) = %%: @{const_name All} $ (Type.constraint (typ --> boolT) (mk_lam(x,P)));
     6.9  end
    6.10  
    6.11  fun mk_All  (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
     7.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Sep 12 17:39:02 2010 +0200
     7.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Sep 12 19:04:02 2010 +0200
     7.3 @@ -463,7 +463,7 @@
     7.4  
     7.5    fun legacy_infer_term thy t =
     7.6        singleton (Syntax.check_terms (ProofContext.init_global thy)) (intern_term thy t);
     7.7 -  fun legacy_infer_prop thy t = legacy_infer_term thy (Type_Infer.constrain propT t);
     7.8 +  fun legacy_infer_prop thy t = legacy_infer_term thy (Type.constraint propT t);
     7.9    fun infer_props thy = map (apsnd (legacy_infer_prop thy));
    7.10    fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
    7.11    fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
     8.1 --- a/src/Pure/Isar/expression.ML	Sun Sep 12 17:39:02 2010 +0200
     8.2 +++ b/src/Pure/Isar/expression.ML	Sun Sep 12 19:04:02 2010 +0200
     8.3 @@ -164,7 +164,7 @@
     8.4      (* type inference and contexts *)
     8.5      val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types;
     8.6      val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
     8.7 -    val arg = type_parms @ map2 Type_Infer.constrain parm_types' insts';
     8.8 +    val arg = type_parms @ map2 Type.constraint parm_types' insts';
     8.9      val res = Syntax.check_terms ctxt arg;
    8.10      val ctxt' = ctxt |> fold Variable.auto_fixes res;
    8.11  
    8.12 @@ -206,7 +206,7 @@
    8.13  
    8.14  fun mk_type T = (Logic.mk_type T, []);
    8.15  fun mk_term t = (t, []);
    8.16 -fun mk_propp (p, pats) = (Syntax.type_constraint propT p, pats);
    8.17 +fun mk_propp (p, pats) = (Type.constraint propT p, pats);
    8.18  
    8.19  fun dest_type (T, []) = Logic.dest_type T;
    8.20  fun dest_term (t, []) = t;
    8.21 @@ -347,7 +347,7 @@
    8.22          val inst' = prep_inst ctxt parm_names inst;
    8.23          val parm_types' = map (Type_Infer.paramify_vars o
    8.24            Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global) parm_types;
    8.25 -        val inst'' = map2 Type_Infer.constrain parm_types' inst';
    8.26 +        val inst'' = map2 Type.constraint parm_types' inst';
    8.27          val insts' = insts @ [(loc, (prfx, inst''))];
    8.28          val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
    8.29          val inst''' = insts'' |> List.last |> snd |> snd;
     9.1 --- a/src/Pure/Isar/proof_context.ML	Sun Sep 12 17:39:02 2010 +0200
     9.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Sep 12 19:04:02 2010 +0200
     9.3 @@ -763,7 +763,7 @@
     9.4        if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
     9.5      val (syms, pos) = Syntax.parse_token ctxt markup text;
     9.6  
     9.7 -    fun check t = (Syntax.check_term ctxt (Type_Infer.constrain T' t); NONE)
     9.8 +    fun check t = (Syntax.check_term ctxt (Type.constraint T' t); NONE)
     9.9        handle ERROR msg => SOME msg;
    9.10      val t =
    9.11        Syntax.standard_parse_term check get_sort map_const map_free
    9.12 @@ -888,7 +888,7 @@
    9.13  in
    9.14  
    9.15  fun read_terms ctxt T =
    9.16 -  map (Syntax.parse_term ctxt #> Type_Infer.constrain T) #> Syntax.check_terms ctxt;
    9.17 +  map (Syntax.parse_term ctxt #> Type.constraint T) #> Syntax.check_terms ctxt;
    9.18  
    9.19  val match_bind = gen_bind read_terms;
    9.20  val match_bind_i = gen_bind (fn ctxt => fn _ => map (cert_term ctxt));
    10.1 --- a/src/Pure/Isar/rule_insts.ML	Sun Sep 12 17:39:02 2010 +0200
    10.2 +++ b/src/Pure/Isar/rule_insts.ML	Sun Sep 12 19:04:02 2010 +0200
    10.3 @@ -82,7 +82,7 @@
    10.4      fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
    10.5      val ts = map2 parse Ts ss;
    10.6      val ts' =
    10.7 -      map2 (Type_Infer.constrain o Type_Infer.paramify_vars) Ts ts
    10.8 +      map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts
    10.9        |> Syntax.check_terms ((schematic ? ProofContext.set_mode ProofContext.mode_schematic) ctxt)
   10.10        |> Variable.polymorphic ctxt;
   10.11      val Ts' = map Term.fastype_of ts';
    11.1 --- a/src/Pure/Isar/specification.ML	Sun Sep 12 17:39:02 2010 +0200
    11.2 +++ b/src/Pure/Isar/specification.ML	Sun Sep 12 19:04:02 2010 +0200
    11.3 @@ -102,7 +102,7 @@
    11.4      fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
    11.5        | abs_body lev y (t $ u) = abs_body lev y t $ abs_body lev y u
    11.6        | abs_body lev y (t as Free (x, T)) =
    11.7 -          if x = y then Type_Infer.constrain (uniform_typing x) (Type_Infer.constrain T (Bound lev))
    11.8 +          if x = y then Type.constraint (uniform_typing x) (Type.constraint T (Bound lev))
    11.9            else t
   11.10        | abs_body _ _ a = a;
   11.11      fun close (y, U) B =
    12.1 --- a/src/Pure/Proof/extraction.ML	Sun Sep 12 17:39:02 2010 +0200
    12.2 +++ b/src/Pure/Proof/extraction.ML	Sun Sep 12 19:04:02 2010 +0200
    12.3 @@ -164,7 +164,7 @@
    12.4        |> Proof_Syntax.strip_sorts_consttypes
    12.5        |> ProofContext.set_defsort [];
    12.6      val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
    12.7 -  in parse ctxt s |> Type_Infer.constrain T |> Syntax.check_term ctxt end;
    12.8 +  in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end;
    12.9  
   12.10  
   12.11  (**** theory data ****)
    13.1 --- a/src/Pure/Proof/proof_syntax.ML	Sun Sep 12 17:39:02 2010 +0200
    13.2 +++ b/src/Pure/Proof/proof_syntax.ML	Sun Sep 12 19:04:02 2010 +0200
    13.3 @@ -223,7 +223,7 @@
    13.4    in
    13.5      fn ty => fn s =>
    13.6        (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s
    13.7 -      |> Type_Infer.constrain ty |> Syntax.check_term ctxt
    13.8 +      |> Type.constraint ty |> Syntax.check_term ctxt
    13.9    end;
   13.10  
   13.11  fun read_proof thy topsort =
    14.1 --- a/src/Pure/Syntax/syntax.ML	Sun Sep 12 17:39:02 2010 +0200
    14.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Sep 12 19:04:02 2010 +0200
    14.3 @@ -286,7 +286,7 @@
    14.4  
    14.5  val check_typs = gen_check fst false;
    14.6  val check_terms = gen_check snd false;
    14.7 -fun check_props ctxt = map (Type_Ext.type_constraint propT) #> check_terms ctxt;
    14.8 +fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
    14.9  
   14.10  val check_typ = singleton o check_typs;
   14.11  val check_term = singleton o check_terms;
    15.1 --- a/src/Pure/Syntax/type_ext.ML	Sun Sep 12 17:39:02 2010 +0200
    15.2 +++ b/src/Pure/Syntax/type_ext.ML	Sun Sep 12 19:04:02 2010 +0200
    15.3 @@ -9,7 +9,6 @@
    15.4    val sort_of_term: term -> sort
    15.5    val term_sorts: term -> (indexname * sort) list
    15.6    val typ_of_term: (indexname -> sort) -> term -> typ
    15.7 -  val type_constraint: typ -> term -> term
    15.8    val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
    15.9      (string -> bool * string) -> (string -> string option) -> term -> term
   15.10    val term_of_typ: bool -> typ -> term
   15.11 @@ -104,19 +103,15 @@
   15.12  
   15.13  (* decode_term -- transform parse tree into raw term *)
   15.14  
   15.15 -fun type_constraint T t =
   15.16 -  if T = dummyT then t
   15.17 -  else Const ("_type_constraint_", T --> T) $ t;
   15.18 -
   15.19  fun decode_term get_sort map_const map_free tm =
   15.20    let
   15.21      val decodeT = typ_of_term (get_sort (term_sorts tm));
   15.22  
   15.23      fun decode (Const ("_constrain", _) $ t $ typ) =
   15.24 -          type_constraint (decodeT typ) (decode t)
   15.25 +          Type.constraint (decodeT typ) (decode t)
   15.26        | decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) =
   15.27            if T = dummyT then Abs (x, decodeT typ, decode t)
   15.28 -          else type_constraint (decodeT typ --> dummyT) (Abs (x, T, decode t))
   15.29 +          else Type.constraint (decodeT typ --> dummyT) (Abs (x, T, decode t))
   15.30        | decode (Abs (x, T, t)) = Abs (x, T, decode t)
   15.31        | decode (t $ u) = decode t $ decode u
   15.32        | decode (Const (a, T)) =
    16.1 --- a/src/Pure/Thy/thy_output.ML	Sun Sep 12 17:39:02 2010 +0200
    16.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Sep 12 19:04:02 2010 +0200
    16.3 @@ -482,7 +482,7 @@
    16.4  
    16.5  fun pretty_term_typ ctxt (style, t) =
    16.6    let val t' = style t
    16.7 -  in pretty_term ctxt (Type_Infer.constrain (Term.fastype_of t') t') end;
    16.8 +  in pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end;
    16.9  
   16.10  fun pretty_term_typeof ctxt (style, t) =
   16.11    Syntax.pretty_typ ctxt (Term.fastype_of (style t));
    17.1 --- a/src/Pure/type.ML	Sun Sep 12 17:39:02 2010 +0200
    17.2 +++ b/src/Pure/type.ML	Sun Sep 12 19:04:02 2010 +0200
    17.3 @@ -7,6 +7,8 @@
    17.4  
    17.5  signature TYPE =
    17.6  sig
    17.7 +  (*constraints*)
    17.8 +  val constraint: typ -> term -> term
    17.9    (*type signatures and certified types*)
   17.10    datatype decl =
   17.11      LogicalType of int |
   17.12 @@ -96,6 +98,14 @@
   17.13  structure Type: TYPE =
   17.14  struct
   17.15  
   17.16 +(** constraints **)
   17.17 +
   17.18 +fun constraint T t =
   17.19 +  if T = dummyT then t
   17.20 +  else Const ("_type_constraint_", T --> T) $ t;
   17.21 +
   17.22 +
   17.23 +
   17.24  (** type signatures and certified types **)
   17.25  
   17.26  (* type declarations *)
    18.1 --- a/src/Pure/type_infer.ML	Sun Sep 12 17:39:02 2010 +0200
    18.2 +++ b/src/Pure/type_infer.ML	Sun Sep 12 19:04:02 2010 +0200
    18.3 @@ -8,7 +8,6 @@
    18.4  sig
    18.5    val anyT: sort -> typ
    18.6    val polymorphicT: typ -> typ
    18.7 -  val constrain: typ -> term -> term
    18.8    val is_param: indexname -> bool
    18.9    val param: int -> string * sort -> typ
   18.10    val paramify_vars: typ -> typ
   18.11 @@ -31,8 +30,6 @@
   18.12  (*indicate polymorphic Vars*)
   18.13  fun polymorphicT T = Type ("_polymorphic_", [T]);
   18.14  
   18.15 -val constrain = Syntax.type_constraint;
   18.16 -
   18.17  
   18.18  (* type inference parameters -- may get instantiated *)
   18.19  
   18.20 @@ -418,8 +415,8 @@
   18.21      (*constrain vars*)
   18.22      val get_type = the_default dummyT o var_type;
   18.23      val constrain_vars = Term.map_aterms
   18.24 -      (fn Free (x, T) => constrain T (Free (x, get_type (x, ~1)))
   18.25 -        | Var (xi, T) => constrain T (Var (xi, get_type xi))
   18.26 +      (fn Free (x, T) => Type.constraint T (Free (x, get_type (x, ~1)))
   18.27 +        | Var (xi, T) => Type.constraint T (Var (xi, get_type xi))
   18.28          | t => t);
   18.29  
   18.30      (*convert to preterms*)
    19.1 --- a/src/Tools/misc_legacy.ML	Sun Sep 12 17:39:02 2010 +0200
    19.2 +++ b/src/Tools/misc_legacy.ML	Sun Sep 12 19:04:02 2010 +0200
    19.3 @@ -30,7 +30,7 @@
    19.4        |> ProofContext.allow_dummies
    19.5        |> ProofContext.set_mode ProofContext.mode_schematic;
    19.6      val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
    19.7 -  in parse ctxt s |> Type_Infer.constrain T |> Syntax.check_term ctxt end;
    19.8 +  in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end;
    19.9  
   19.10  
   19.11  (**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
    20.1 --- a/src/Tools/nbe.ML	Sun Sep 12 17:39:02 2010 +0200
    20.2 +++ b/src/Tools/nbe.ML	Sun Sep 12 19:04:02 2010 +0200
    20.3 @@ -551,7 +551,7 @@
    20.4      fun type_infer t =
    20.5        singleton (Type_Infer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
    20.6          (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
    20.7 -      (Type_Infer.constrain ty' t);
    20.8 +      (Type.constraint ty' t);
    20.9      val string_of_term =
   20.10        Syntax.string_of_term (Config.put show_types true (Syntax.init_pretty_global thy));
   20.11      fun check_tvars t =
    21.1 --- a/src/ZF/Tools/datatype_package.ML	Sun Sep 12 17:39:02 2010 +0200
    21.2 +++ b/src/ZF/Tools/datatype_package.ML	Sun Sep 12 19:04:02 2010 +0200
    21.3 @@ -403,7 +403,7 @@
    21.4    let
    21.5      val ctxt = ProofContext.init_global thy;
    21.6      fun read_is strs =
    21.7 -      map (Syntax.parse_term ctxt #> Type_Infer.constrain @{typ i}) strs
    21.8 +      map (Syntax.parse_term ctxt #> Type.constraint @{typ i}) strs
    21.9        |> Syntax.check_terms ctxt;
   21.10  
   21.11      val rec_tms = read_is srec_tms;
    22.1 --- a/src/ZF/Tools/inductive_package.ML	Sun Sep 12 17:39:02 2010 +0200
    22.2 +++ b/src/ZF/Tools/inductive_package.ML	Sun Sep 12 19:04:02 2010 +0200
    22.3 @@ -555,7 +555,7 @@
    22.4      (raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
    22.5    let
    22.6      val ctxt = ProofContext.init_global thy;
    22.7 -    val read_terms = map (Syntax.parse_term ctxt #> Type_Infer.constrain Ind_Syntax.iT)
    22.8 +    val read_terms = map (Syntax.parse_term ctxt #> Type.constraint Ind_Syntax.iT)
    22.9        #> Syntax.check_terms ctxt;
   22.10  
   22.11      val intr_atts = map (map (Attrib.attribute thy) o snd) intr_srcs;
    23.1 --- a/src/ZF/ind_syntax.ML	Sun Sep 12 17:39:02 2010 +0200
    23.2 +++ b/src/ZF/ind_syntax.ML	Sun Sep 12 19:04:02 2010 +0200
    23.3 @@ -66,7 +66,7 @@
    23.4  
    23.5  (*read a constructor specification*)
    23.6  fun read_construct ctxt (id: string, sprems, syn: mixfix) =
    23.7 -    let val prems = map (Syntax.parse_term ctxt #> Type_Infer.constrain FOLogic.oT) sprems
    23.8 +    let val prems = map (Syntax.parse_term ctxt #> Type.constraint FOLogic.oT) sprems
    23.9            |> Syntax.check_terms ctxt
   23.10          val args = map (#1 o dest_mem) prems
   23.11          val T = (map (#2 o dest_Free) args) ---> iT