more explicit support for object-logic constraint;
authorwenzelm
Wed Mar 30 23:32:50 2016 +0200 (2016-03-30)
changeset 62773e6443edaebff
parent 62772 77bbe5af41c3
child 62774 cfcb20bbdbd8
more explicit support for object-logic constraint;
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Mar 30 22:35:41 2016 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Mar 30 23:32:50 2016 +0200
     1.3 @@ -600,7 +600,7 @@
     1.4        let
     1.5          val ctxt' =
     1.6            ctxt |> is_none (Variable.default_type ctxt x) ?
     1.7 -            Variable.declare_constraints (Free (x, Mixfix.mixfixT mx));
     1.8 +            Variable.declare_constraints (Free (x, Proof_Context.default_constraint ctxt mx));
     1.9          val t = Free (#1 (Proof_Context.inferred_param x ctxt'));
    1.10        in ((t, mx), ctxt') end
    1.11    | t => ((t, mx), ctxt));
     2.1 --- a/src/Pure/Isar/proof_context.ML	Wed Mar 30 22:35:41 2016 +0200
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Mar 30 23:32:50 2016 +0200
     2.3 @@ -130,6 +130,9 @@
     2.4    val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
     2.5      Proof.context -> (string * thm list) list * Proof.context
     2.6    val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
     2.7 +  val set_object_logic_constraint: Proof.context -> Proof.context
     2.8 +  val restore_object_logic_constraint: Proof.context -> Proof.context -> Proof.context
     2.9 +  val default_constraint: Proof.context -> mixfix -> typ
    2.10    val read_var: binding * string option * mixfix -> Proof.context ->
    2.11      (binding * typ option * mixfix) * Proof.context
    2.12    val cert_var: binding * typ option * mixfix -> Proof.context ->
    2.13 @@ -1056,10 +1059,33 @@
    2.14  
    2.15  (** basic logical entities **)
    2.16  
    2.17 +(* default type constraint *)
    2.18 +
    2.19 +val object_logic_constraint =
    2.20 +  Config.bool
    2.21 +    (Config.declare ("Proof_Context.object_logic_constraint", @{here}) (K (Config.Bool false)));
    2.22 +
    2.23 +val set_object_logic_constraint = Config.put object_logic_constraint true;
    2.24 +fun restore_object_logic_constraint ctxt =
    2.25 +  Config.put object_logic_constraint (Config.get ctxt object_logic_constraint);
    2.26 +
    2.27 +fun default_constraint ctxt mx =
    2.28 +  let
    2.29 +    val A =
    2.30 +      (case (Object_Logic.get_base_sort ctxt, Config.get ctxt object_logic_constraint) of
    2.31 +        (SOME S, true) => Type_Infer.anyT S
    2.32 +      | _ => dummyT);
    2.33 +  in
    2.34 +    (case mx of
    2.35 +      Binder _ => (A --> A) --> A
    2.36 +    | _ => replicate (Mixfix.mixfix_args mx) A ---> A)
    2.37 +  end;
    2.38 +
    2.39 +
    2.40  (* variables *)
    2.41  
    2.42  fun declare_var (x, opt_T, mx) ctxt =
    2.43 -  let val T = (case opt_T of SOME T => T | NONE => Mixfix.mixfixT mx)
    2.44 +  let val T = (case opt_T of SOME T => T | NONE => default_constraint ctxt mx)
    2.45    in (T, ctxt |> Variable.declare_constraints (Free (x, T))) end;
    2.46  
    2.47  fun add_syntax vars ctxt =
     3.1 --- a/src/Pure/Syntax/mixfix.ML	Wed Mar 30 22:35:41 2016 +0200
     3.2 +++ b/src/Pure/Syntax/mixfix.ML	Wed Mar 30 23:32:50 2016 +0200
     3.3 @@ -27,7 +27,6 @@
     3.4    val reset_pos: mixfix -> mixfix
     3.5    val pretty_mixfix: mixfix -> Pretty.T
     3.6    val mixfix_args: mixfix -> int
     3.7 -  val mixfixT: mixfix -> typ
     3.8    val make_type: int -> typ
     3.9    val binder_name: string -> string
    3.10    val syn_ext_types: (string * typ * mixfix) list -> Syntax_Ext.syn_ext
    3.11 @@ -118,9 +117,6 @@
    3.12    | mixfix_args (Binder _) = 1
    3.13    | mixfix_args (Structure _) = 0;
    3.14  
    3.15 -fun mixfixT (Binder _) = (dummyT --> dummyT) --> dummyT
    3.16 -  | mixfixT mx = replicate (mixfix_args mx) dummyT ---> dummyT;
    3.17 -
    3.18  
    3.19  (* syn_ext_types *)
    3.20