simplified check/uncheck interfaces: result comparison is hardwired by default;
authorwenzelm
Tue Apr 19 14:57:09 2011 +0200 (2011-04-19)
changeset 42402c7139609b67d
parent 42401 9bfaf6819291
child 42403 38b29c9fc742
simplified check/uncheck interfaces: result comparison is hardwired by default;
tuned;
src/HOL/Tools/code_evaluation.ML
src/Pure/Isar/class.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/overloading.ML
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/syntax.ML
src/Tools/adhoc_overloading.ML
src/Tools/subtyping.ML
     1.1 --- a/src/HOL/Tools/code_evaluation.ML	Tue Apr 19 10:50:54 2011 +0200
     1.2 +++ b/src/HOL/Tools/code_evaluation.ML	Tue Apr 19 14:57:09 2011 +0200
     1.3 @@ -150,8 +150,8 @@
     1.4        | NONE => NONE)
     1.5    | subst_termify t = subst_termify_app (strip_comb t) 
     1.6  
     1.7 -fun check_termify ts ctxt = map_default subst_termify ts
     1.8 -  |> Option.map (rpair ctxt)
     1.9 +fun check_termify ctxt ts =
    1.10 +  the_default ts (map_default subst_termify ts);
    1.11  
    1.12  
    1.13  (** evaluation **)
     2.1 --- a/src/Pure/Isar/class.ML	Tue Apr 19 10:50:54 2011 +0200
     2.2 +++ b/src/Pure/Isar/class.ML	Tue Apr 19 14:57:09 2011 +0200
     2.3 @@ -462,7 +462,7 @@
     2.4        handle Sorts.CLASS_ERROR e => error (Sorts.class_error ctxt e);
     2.5      val inst = map_type_tvar
     2.6        (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
     2.7 -  in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end;
     2.8 +  in if Vartab.is_empty tvartab then ts else (map o map_types) inst ts end;
     2.9  
    2.10  
    2.11  (* target *)
    2.12 @@ -535,10 +535,7 @@
    2.13      val consts = Sign.consts_of thy;
    2.14      val improve_constraints = AList.lookup (op =)
    2.15        (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
    2.16 -    fun resort_check ts ctxt =
    2.17 -      (case resort_terms ctxt algebra consts improve_constraints ts of
    2.18 -        NONE => NONE
    2.19 -      | SOME ts' => SOME (ts', ctxt));
    2.20 +    fun resort_check ctxt ts = resort_terms ctxt algebra consts improve_constraints ts;
    2.21      val lookup_inst_param = AxClass.lookup_inst_param consts params;
    2.22      fun improve (c, ty) =
    2.23        (case lookup_inst_param (c, ty) of
     3.1 --- a/src/Pure/Isar/class_declaration.ML	Tue Apr 19 10:50:54 2011 +0200
     3.2 +++ b/src/Pure/Isar/class_declaration.ML	Tue Apr 19 14:57:09 2011 +0200
     3.3 @@ -139,19 +139,18 @@
     3.4            (fn T as TFree _ => T | T as TVar (vi, _) =>
     3.5              if Type_Infer.is_param vi then Type_Infer.param 0 (Name.aT, sort') else T) Ts
     3.6        end;
     3.7 -    fun add_typ_check level name f = Context.proof_map
     3.8 -      (Syntax.add_typ_check level name (fn Ts => fn ctxt =>
     3.9 -        let val Ts' = f Ts in if eq_list (op =) (Ts, Ts') then NONE else SOME (Ts', ctxt) end));
    3.10  
    3.11      (* preprocessing elements, retrieving base sort from type-checked elements *)
    3.12 -    val raw_supexpr = (map (fn sup => (sup, (("", false),
    3.13 -      Expression.Positional []))) sups, []);
    3.14 -    val init_class_body = fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
    3.15 +    val raw_supexpr =
    3.16 +      (map (fn sup => (sup, (("", false), Expression.Positional []))) sups, []);
    3.17 +    val init_class_body =
    3.18 +      fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
    3.19        #> Class.redeclare_operations thy sups
    3.20 -      #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
    3.21 -      #> add_typ_check ~10 "singleton_fixate" singleton_fixate;
    3.22 -    val ((raw_supparams, _, raw_inferred_elems), _) = Proof_Context.init_global thy
    3.23 -      |> add_typ_check 5 "after_infer_fixate" after_infer_fixate
    3.24 +      #> Context.proof_map (Syntax.add_typ_check 10 "reject_bcd_etc" (K reject_bcd_etc))
    3.25 +      #> Context.proof_map (Syntax.add_typ_check ~10 "singleton_fixate" (K singleton_fixate));
    3.26 +    val ((raw_supparams, _, raw_inferred_elems), _) =
    3.27 +      Proof_Context.init_global thy
    3.28 +      |> Context.proof_map (Syntax.add_typ_check 5 "after_infer_fixate" (K after_infer_fixate))
    3.29        |> prep_decl raw_supexpr init_class_body raw_elems;
    3.30      fun filter_element (Element.Fixes []) = NONE
    3.31        | filter_element (e as Element.Fixes _) = SOME e
    3.32 @@ -165,7 +164,7 @@
    3.33      fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
    3.34        | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
    3.35        | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) =>
    3.36 -          fold_types f t #> (fold o fold_types) f ts) o snd) assms
    3.37 +          fold_types f t #> (fold o fold_types) f ts) o snd) assms;
    3.38      val base_sort = if null inferred_elems then proto_base_sort else
    3.39        case (fold o fold_element_types) Term.add_tfreesT inferred_elems []
    3.40         of [] => error "No type variable in class specification"
     4.1 --- a/src/Pure/Isar/overloading.ML	Tue Apr 19 10:50:54 2011 +0200
     4.2 +++ b/src/Pure/Isar/overloading.ML	Tue Apr 19 14:57:09 2011 +0200
     4.3 @@ -113,8 +113,8 @@
     4.4  
     4.5  val activate_improvable_syntax =
     4.6    Context.proof_map
     4.7 -    (Syntax.add_term_check 0 "improvement" improve_term_check
     4.8 -    #> Syntax.add_term_uncheck 0 "improvement" improve_term_uncheck)
     4.9 +    (Syntax.context_term_check 0 "improvement" improve_term_check
    4.10 +    #> Syntax.context_term_uncheck 0 "improvement" improve_term_uncheck)
    4.11    #> set_primary_constraints;
    4.12  
    4.13  
     5.1 --- a/src/Pure/Isar/proof_context.ML	Tue Apr 19 10:50:54 2011 +0200
     5.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Apr 19 14:57:09 2011 +0200
     5.3 @@ -700,16 +700,13 @@
     5.4  fun standard_term_uncheck ctxt =
     5.5    map (contract_abbrevs ctxt);
     5.6  
     5.7 -fun add eq what f = Context.>> (what (fn xs => fn ctxt =>
     5.8 -  let val xs' = f ctxt xs in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end));
     5.9 -
    5.10  in
    5.11  
    5.12 -val _ = add (op =) (Syntax.add_typ_check 0 "standard") standard_typ_check;
    5.13 -val _ = add (op aconv) (Syntax.add_term_check 0 "standard") standard_term_check;
    5.14 -val _ = add (op aconv) (Syntax.add_term_check 100 "fixate") prepare_patterns;
    5.15 -
    5.16 -val _ = add (op aconv) (Syntax.add_term_uncheck 0 "standard") standard_term_uncheck;
    5.17 +val _ = Context.>>
    5.18 + (Syntax.add_typ_check 0 "standard" standard_typ_check #>
    5.19 +  Syntax.add_term_check 0 "standard" standard_term_check #>
    5.20 +  Syntax.add_term_check 100 "fixate" prepare_patterns #>
    5.21 +  Syntax.add_term_uncheck 0 "standard" standard_term_uncheck);
    5.22  
    5.23  end;
    5.24  
     6.1 --- a/src/Pure/Syntax/syntax.ML	Tue Apr 19 10:50:54 2011 +0200
     6.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Apr 19 14:57:09 2011 +0200
     6.3 @@ -31,18 +31,26 @@
     6.4    val unparse_typ: Proof.context -> typ -> Pretty.T
     6.5    val unparse_term: Proof.context -> term -> Pretty.T
     6.6    val print_checks: Proof.context -> unit
     6.7 -  val add_typ_check: int -> string ->
     6.8 +  val context_typ_check: int -> string ->
     6.9      (typ list -> Proof.context -> (typ list * Proof.context) option) ->
    6.10      Context.generic -> Context.generic
    6.11 -  val add_term_check: int -> string ->
    6.12 +  val context_term_check: int -> string ->
    6.13      (term list -> Proof.context -> (term list * Proof.context) option) ->
    6.14      Context.generic -> Context.generic
    6.15 -  val add_typ_uncheck: int -> string ->
    6.16 +  val context_typ_uncheck: int -> string ->
    6.17      (typ list -> Proof.context -> (typ list * Proof.context) option) ->
    6.18      Context.generic -> Context.generic
    6.19 -  val add_term_uncheck: int -> string ->
    6.20 +  val context_term_uncheck: int -> string ->
    6.21      (term list -> Proof.context -> (term list * Proof.context) option) ->
    6.22      Context.generic -> Context.generic
    6.23 +  val add_typ_check: int -> string -> (Proof.context -> typ list -> typ list) ->
    6.24 +    Context.generic -> Context.generic
    6.25 +  val add_term_check: int -> string -> (Proof.context -> term list -> term list) ->
    6.26 +    Context.generic -> Context.generic
    6.27 +  val add_typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) ->
    6.28 +    Context.generic -> Context.generic
    6.29 +  val add_term_uncheck: int -> string -> (Proof.context -> term list -> term list) ->
    6.30 +    Context.generic -> Context.generic
    6.31    val typ_check: Proof.context -> typ list -> typ list
    6.32    val term_check: Proof.context -> term list -> term list
    6.33    val typ_uncheck: Proof.context -> typ list -> typ list
    6.34 @@ -224,13 +232,11 @@
    6.35  
    6.36  (* context-sensitive (un)checking *)
    6.37  
    6.38 -local
    6.39 -
    6.40  type key = int * bool;
    6.41 -type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
    6.42  
    6.43  structure Checks = Generic_Data
    6.44  (
    6.45 +  type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
    6.46    type T =
    6.47      ((key * ((string * typ check) * stamp) list) list *
    6.48       (key * ((string * term check) * stamp) list) list);
    6.49 @@ -241,27 +247,6 @@
    6.50       AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
    6.51  );
    6.52  
    6.53 -fun gen_add which (key: key) name f =
    6.54 -  Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
    6.55 -
    6.56 -fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
    6.57 -
    6.58 -fun gen_check which uncheck ctxt0 xs0 =
    6.59 -  let
    6.60 -    val funs = which (Checks.get (Context.Proof ctxt0))
    6.61 -      |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
    6.62 -      |> Library.sort (int_ord o pairself fst) |> map snd
    6.63 -      |> not uncheck ? map rev;
    6.64 -    val check_all = perhaps_apply (map check_stage funs);
    6.65 -  in #1 (perhaps check_all (xs0, ctxt0)) end;
    6.66 -
    6.67 -fun map_sort f S =
    6.68 -  (case f (TFree ("", S)) of
    6.69 -    TFree ("", S') => S'
    6.70 -  | _ => raise TYPE ("map_sort", [TFree ("", S)], []));
    6.71 -
    6.72 -in
    6.73 -
    6.74  fun print_checks ctxt =
    6.75    let
    6.76      fun split_checks checks =
    6.77 @@ -283,15 +268,52 @@
    6.78      pretty_checks "term_unchecks" term_unchecks
    6.79    end |> Pretty.chunks |> Pretty.writeln;
    6.80  
    6.81 -fun add_typ_check stage = gen_add apfst (stage, false);
    6.82 -fun add_term_check stage = gen_add apsnd (stage, false);
    6.83 -fun add_typ_uncheck stage = gen_add apfst (stage, true);
    6.84 -fun add_term_uncheck stage = gen_add apsnd (stage, true);
    6.85 +
    6.86 +local
    6.87 +
    6.88 +fun context_check which (key: key) name f =
    6.89 +  Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
    6.90 +
    6.91 +fun simple_check eq f xs ctxt =
    6.92 +  let val xs' = f ctxt xs in
    6.93 +    if pointer_eq (xs, xs') orelse eq_list eq (xs, xs') then NONE
    6.94 +    else SOME (xs', ctxt)
    6.95 +  end;
    6.96 +
    6.97 +in
    6.98 +
    6.99 +fun context_typ_check stage = context_check apfst (stage, false);
   6.100 +fun context_term_check stage = context_check apsnd (stage, false);
   6.101 +fun context_typ_uncheck stage = context_check apfst (stage, true);
   6.102 +fun context_term_uncheck stage = context_check apsnd (stage, true);
   6.103  
   6.104 -val typ_check = gen_check fst false;
   6.105 -val term_check = gen_check snd false;
   6.106 -val typ_uncheck = gen_check fst true;
   6.107 -val term_uncheck = gen_check snd true;
   6.108 +fun add_typ_check key name f = context_typ_check key name (simple_check (op =) f);
   6.109 +fun add_term_check key name f = context_term_check key name (simple_check (op aconv) f);
   6.110 +fun add_typ_uncheck key name f = context_typ_uncheck key name (simple_check (op =) f);
   6.111 +fun add_term_uncheck key name f = context_term_uncheck key name (simple_check (op aconv) f);
   6.112 +
   6.113 +end;
   6.114 +
   6.115 +
   6.116 +local
   6.117 +
   6.118 +fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
   6.119 +fun check_all fs = perhaps_apply (map check_stage fs);
   6.120 +
   6.121 +fun check which uncheck ctxt0 xs0 =
   6.122 +  let
   6.123 +    val funs = which (Checks.get (Context.Proof ctxt0))
   6.124 +      |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
   6.125 +      |> Library.sort (int_ord o pairself fst) |> map snd
   6.126 +      |> not uncheck ? map rev;
   6.127 +  in #1 (perhaps (check_all funs) (xs0, ctxt0)) end;
   6.128 +
   6.129 +in
   6.130 +
   6.131 +val typ_check = check fst false;
   6.132 +val term_check = check snd false;
   6.133 +val typ_uncheck = check fst true;
   6.134 +val term_uncheck = check snd true;
   6.135  
   6.136  val check_typs = operation #check_typs;
   6.137  val check_terms = operation #check_terms;
   6.138 @@ -300,17 +322,30 @@
   6.139  val check_typ = singleton o check_typs;
   6.140  val check_term = singleton o check_terms;
   6.141  val check_prop = singleton o check_props;
   6.142 -val check_sort = map_sort o check_typ;
   6.143  
   6.144  val uncheck_typs = operation #uncheck_typs;
   6.145  val uncheck_terms = operation #uncheck_terms;
   6.146 +
   6.147 +end;
   6.148 +
   6.149 +
   6.150 +(* derived operations for algebra of sorts *)
   6.151 +
   6.152 +local
   6.153 +
   6.154 +fun map_sort f S =
   6.155 +  (case f (TFree ("", S)) of
   6.156 +    TFree ("", S') => S'
   6.157 +  | _ => raise TYPE ("map_sort", [TFree ("", S)], []));
   6.158 +
   6.159 +in
   6.160 +
   6.161 +val check_sort = map_sort o check_typ;
   6.162  val uncheck_sort = map_sort o singleton o uncheck_typs;
   6.163  
   6.164  end;
   6.165  
   6.166  
   6.167 -(* derived operations for classrel and arity *)
   6.168 -
   6.169  val uncheck_classrel = map o singleton o uncheck_sort;
   6.170  
   6.171  fun unparse_classrel ctxt cs = Pretty.block (flat
     7.1 --- a/src/Tools/adhoc_overloading.ML	Tue Apr 19 10:50:54 2011 +0200
     7.2 +++ b/src/Tools/adhoc_overloading.ML	Tue Apr 19 14:57:09 2011 +0200
     7.3 @@ -134,8 +134,8 @@
     7.4  (* setup *)
     7.5  
     7.6  val setup = Context.theory_map 
     7.7 -  (Syntax.add_term_check 0 "adhoc_overloading" check
     7.8 -   #> Syntax.add_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
     7.9 -   #> Syntax.add_term_uncheck 0 "adhoc_overloading" uncheck);
    7.10 +  (Syntax.context_term_check 0 "adhoc_overloading" check
    7.11 +   #> Syntax.context_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
    7.12 +   #> Syntax.context_term_uncheck 0 "adhoc_overloading" uncheck);
    7.13  
    7.14  end
     8.1 --- a/src/Tools/subtyping.ML	Tue Apr 19 10:50:54 2011 +0200
     8.2 +++ b/src/Tools/subtyping.ML	Tue Apr 19 14:57:09 2011 +0200
     8.3 @@ -713,15 +713,12 @@
     8.4  
     8.5  (* term check *)
     8.6  
     8.7 -val (coercion_enabled, coercion_enabled_setup) = Attrib.config_bool "coercion_enabled" (K false);
     8.8 +val (coercion_enabled, coercion_enabled_setup) =
     8.9 +  Attrib.config_bool "coercion_enabled" (K false);
    8.10  
    8.11  val add_term_check =
    8.12    Syntax.add_term_check ~100 "coercions"
    8.13 -    (fn xs => fn ctxt =>
    8.14 -      if Config.get ctxt coercion_enabled then
    8.15 -        let val xs' = coercion_infer_types ctxt xs
    8.16 -        in if eq_list (op aconv) (xs, xs') then NONE else SOME (xs', ctxt) end
    8.17 -      else NONE);
    8.18 +    (fn ctxt => Config.get ctxt coercion_enabled ? coercion_infer_types ctxt);
    8.19  
    8.20  
    8.21  (* declarations *)