# HG changeset patch # User wenzelm # Date 1303217829 -7200 # Node ID c7139609b67db6936f684ada2add0886e52dc88c # Parent 9bfaf681929105923ea461d30e3e93905b35c753 simplified check/uncheck interfaces: result comparison is hardwired by default; tuned; diff -r 9bfaf6819291 -r c7139609b67d src/HOL/Tools/code_evaluation.ML --- a/src/HOL/Tools/code_evaluation.ML Tue Apr 19 10:50:54 2011 +0200 +++ b/src/HOL/Tools/code_evaluation.ML Tue Apr 19 14:57:09 2011 +0200 @@ -150,8 +150,8 @@ | NONE => NONE) | subst_termify t = subst_termify_app (strip_comb t) -fun check_termify ts ctxt = map_default subst_termify ts - |> Option.map (rpair ctxt) +fun check_termify ctxt ts = + the_default ts (map_default subst_termify ts); (** evaluation **) diff -r 9bfaf6819291 -r c7139609b67d src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Tue Apr 19 10:50:54 2011 +0200 +++ b/src/Pure/Isar/class.ML Tue Apr 19 14:57:09 2011 +0200 @@ -462,7 +462,7 @@ handle Sorts.CLASS_ERROR e => error (Sorts.class_error ctxt e); val inst = map_type_tvar (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi))); - in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end; + in if Vartab.is_empty tvartab then ts else (map o map_types) inst ts end; (* target *) @@ -535,10 +535,7 @@ val consts = Sign.consts_of thy; val improve_constraints = AList.lookup (op =) (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params); - fun resort_check ts ctxt = - (case resort_terms ctxt algebra consts improve_constraints ts of - NONE => NONE - | SOME ts' => SOME (ts', ctxt)); + fun resort_check ctxt ts = resort_terms ctxt algebra consts improve_constraints ts; val lookup_inst_param = AxClass.lookup_inst_param consts params; fun improve (c, ty) = (case lookup_inst_param (c, ty) of diff -r 9bfaf6819291 -r c7139609b67d src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Tue Apr 19 10:50:54 2011 +0200 +++ b/src/Pure/Isar/class_declaration.ML Tue Apr 19 14:57:09 2011 +0200 @@ -139,19 +139,18 @@ (fn T as TFree _ => T | T as TVar (vi, _) => if Type_Infer.is_param vi then Type_Infer.param 0 (Name.aT, sort') else T) Ts end; - fun add_typ_check level name f = Context.proof_map - (Syntax.add_typ_check level name (fn Ts => fn ctxt => - let val Ts' = f Ts in if eq_list (op =) (Ts, Ts') then NONE else SOME (Ts', ctxt) end)); (* preprocessing elements, retrieving base sort from type-checked elements *) - val raw_supexpr = (map (fn sup => (sup, (("", false), - Expression.Positional []))) sups, []); - val init_class_body = fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints + val raw_supexpr = + (map (fn sup => (sup, (("", false), Expression.Positional []))) sups, []); + val init_class_body = + fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints #> Class.redeclare_operations thy sups - #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc - #> add_typ_check ~10 "singleton_fixate" singleton_fixate; - val ((raw_supparams, _, raw_inferred_elems), _) = Proof_Context.init_global thy - |> add_typ_check 5 "after_infer_fixate" after_infer_fixate + #> Context.proof_map (Syntax.add_typ_check 10 "reject_bcd_etc" (K reject_bcd_etc)) + #> Context.proof_map (Syntax.add_typ_check ~10 "singleton_fixate" (K singleton_fixate)); + val ((raw_supparams, _, raw_inferred_elems), _) = + Proof_Context.init_global thy + |> Context.proof_map (Syntax.add_typ_check 5 "after_infer_fixate" (K after_infer_fixate)) |> prep_decl raw_supexpr init_class_body raw_elems; fun filter_element (Element.Fixes []) = NONE | filter_element (e as Element.Fixes _) = SOME e @@ -165,7 +164,7 @@ fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) => - fold_types f t #> (fold o fold_types) f ts) o snd) assms + fold_types f t #> (fold o fold_types) f ts) o snd) assms; val base_sort = if null inferred_elems then proto_base_sort else case (fold o fold_element_types) Term.add_tfreesT inferred_elems [] of [] => error "No type variable in class specification" diff -r 9bfaf6819291 -r c7139609b67d src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Tue Apr 19 10:50:54 2011 +0200 +++ b/src/Pure/Isar/overloading.ML Tue Apr 19 14:57:09 2011 +0200 @@ -113,8 +113,8 @@ val activate_improvable_syntax = Context.proof_map - (Syntax.add_term_check 0 "improvement" improve_term_check - #> Syntax.add_term_uncheck 0 "improvement" improve_term_uncheck) + (Syntax.context_term_check 0 "improvement" improve_term_check + #> Syntax.context_term_uncheck 0 "improvement" improve_term_uncheck) #> set_primary_constraints; diff -r 9bfaf6819291 -r c7139609b67d src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Apr 19 10:50:54 2011 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Apr 19 14:57:09 2011 +0200 @@ -700,16 +700,13 @@ fun standard_term_uncheck ctxt = map (contract_abbrevs ctxt); -fun add eq what f = Context.>> (what (fn xs => fn ctxt => - let val xs' = f ctxt xs in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end)); - in -val _ = add (op =) (Syntax.add_typ_check 0 "standard") standard_typ_check; -val _ = add (op aconv) (Syntax.add_term_check 0 "standard") standard_term_check; -val _ = add (op aconv) (Syntax.add_term_check 100 "fixate") prepare_patterns; - -val _ = add (op aconv) (Syntax.add_term_uncheck 0 "standard") standard_term_uncheck; +val _ = Context.>> + (Syntax.add_typ_check 0 "standard" standard_typ_check #> + Syntax.add_term_check 0 "standard" standard_term_check #> + Syntax.add_term_check 100 "fixate" prepare_patterns #> + Syntax.add_term_uncheck 0 "standard" standard_term_uncheck); end; diff -r 9bfaf6819291 -r c7139609b67d src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Tue Apr 19 10:50:54 2011 +0200 +++ b/src/Pure/Syntax/syntax.ML Tue Apr 19 14:57:09 2011 +0200 @@ -31,18 +31,26 @@ val unparse_typ: Proof.context -> typ -> Pretty.T val unparse_term: Proof.context -> term -> Pretty.T val print_checks: Proof.context -> unit - val add_typ_check: int -> string -> + val context_typ_check: int -> string -> (typ list -> Proof.context -> (typ list * Proof.context) option) -> Context.generic -> Context.generic - val add_term_check: int -> string -> + val context_term_check: int -> string -> (term list -> Proof.context -> (term list * Proof.context) option) -> Context.generic -> Context.generic - val add_typ_uncheck: int -> string -> + val context_typ_uncheck: int -> string -> (typ list -> Proof.context -> (typ list * Proof.context) option) -> Context.generic -> Context.generic - val add_term_uncheck: int -> string -> + val context_term_uncheck: int -> string -> (term list -> Proof.context -> (term list * Proof.context) option) -> Context.generic -> Context.generic + val add_typ_check: int -> string -> (Proof.context -> typ list -> typ list) -> + Context.generic -> Context.generic + val add_term_check: int -> string -> (Proof.context -> term list -> term list) -> + Context.generic -> Context.generic + val add_typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) -> + Context.generic -> Context.generic + val add_term_uncheck: int -> string -> (Proof.context -> term list -> term list) -> + Context.generic -> Context.generic val typ_check: Proof.context -> typ list -> typ list val term_check: Proof.context -> term list -> term list val typ_uncheck: Proof.context -> typ list -> typ list @@ -224,13 +232,11 @@ (* context-sensitive (un)checking *) -local - type key = int * bool; -type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option; structure Checks = Generic_Data ( + type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option; type T = ((key * ((string * typ check) * stamp) list) list * (key * ((string * term check) * stamp) list) list); @@ -241,27 +247,6 @@ AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2)); ); -fun gen_add which (key: key) name f = - Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ())))); - -fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs)); - -fun gen_check which uncheck ctxt0 xs0 = - let - val funs = which (Checks.get (Context.Proof ctxt0)) - |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE) - |> Library.sort (int_ord o pairself fst) |> map snd - |> not uncheck ? map rev; - val check_all = perhaps_apply (map check_stage funs); - in #1 (perhaps check_all (xs0, ctxt0)) end; - -fun map_sort f S = - (case f (TFree ("", S)) of - TFree ("", S') => S' - | _ => raise TYPE ("map_sort", [TFree ("", S)], [])); - -in - fun print_checks ctxt = let fun split_checks checks = @@ -283,15 +268,52 @@ pretty_checks "term_unchecks" term_unchecks end |> Pretty.chunks |> Pretty.writeln; -fun add_typ_check stage = gen_add apfst (stage, false); -fun add_term_check stage = gen_add apsnd (stage, false); -fun add_typ_uncheck stage = gen_add apfst (stage, true); -fun add_term_uncheck stage = gen_add apsnd (stage, true); + +local + +fun context_check which (key: key) name f = + Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ())))); + +fun simple_check eq f xs ctxt = + let val xs' = f ctxt xs in + if pointer_eq (xs, xs') orelse eq_list eq (xs, xs') then NONE + else SOME (xs', ctxt) + end; + +in + +fun context_typ_check stage = context_check apfst (stage, false); +fun context_term_check stage = context_check apsnd (stage, false); +fun context_typ_uncheck stage = context_check apfst (stage, true); +fun context_term_uncheck stage = context_check apsnd (stage, true); -val typ_check = gen_check fst false; -val term_check = gen_check snd false; -val typ_uncheck = gen_check fst true; -val term_uncheck = gen_check snd true; +fun add_typ_check key name f = context_typ_check key name (simple_check (op =) f); +fun add_term_check key name f = context_term_check key name (simple_check (op aconv) f); +fun add_typ_uncheck key name f = context_typ_uncheck key name (simple_check (op =) f); +fun add_term_uncheck key name f = context_term_uncheck key name (simple_check (op aconv) f); + +end; + + +local + +fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs)); +fun check_all fs = perhaps_apply (map check_stage fs); + +fun check which uncheck ctxt0 xs0 = + let + val funs = which (Checks.get (Context.Proof ctxt0)) + |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE) + |> Library.sort (int_ord o pairself fst) |> map snd + |> not uncheck ? map rev; + in #1 (perhaps (check_all funs) (xs0, ctxt0)) end; + +in + +val typ_check = check fst false; +val term_check = check snd false; +val typ_uncheck = check fst true; +val term_uncheck = check snd true; val check_typs = operation #check_typs; val check_terms = operation #check_terms; @@ -300,17 +322,30 @@ val check_typ = singleton o check_typs; val check_term = singleton o check_terms; val check_prop = singleton o check_props; -val check_sort = map_sort o check_typ; val uncheck_typs = operation #uncheck_typs; val uncheck_terms = operation #uncheck_terms; + +end; + + +(* derived operations for algebra of sorts *) + +local + +fun map_sort f S = + (case f (TFree ("", S)) of + TFree ("", S') => S' + | _ => raise TYPE ("map_sort", [TFree ("", S)], [])); + +in + +val check_sort = map_sort o check_typ; val uncheck_sort = map_sort o singleton o uncheck_typs; end; -(* derived operations for classrel and arity *) - val uncheck_classrel = map o singleton o uncheck_sort; fun unparse_classrel ctxt cs = Pretty.block (flat diff -r 9bfaf6819291 -r c7139609b67d src/Tools/adhoc_overloading.ML --- a/src/Tools/adhoc_overloading.ML Tue Apr 19 10:50:54 2011 +0200 +++ b/src/Tools/adhoc_overloading.ML Tue Apr 19 14:57:09 2011 +0200 @@ -134,8 +134,8 @@ (* setup *) val setup = Context.theory_map - (Syntax.add_term_check 0 "adhoc_overloading" check - #> Syntax.add_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved - #> Syntax.add_term_uncheck 0 "adhoc_overloading" uncheck); + (Syntax.context_term_check 0 "adhoc_overloading" check + #> Syntax.context_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved + #> Syntax.context_term_uncheck 0 "adhoc_overloading" uncheck); end diff -r 9bfaf6819291 -r c7139609b67d src/Tools/subtyping.ML --- a/src/Tools/subtyping.ML Tue Apr 19 10:50:54 2011 +0200 +++ b/src/Tools/subtyping.ML Tue Apr 19 14:57:09 2011 +0200 @@ -713,15 +713,12 @@ (* term check *) -val (coercion_enabled, coercion_enabled_setup) = Attrib.config_bool "coercion_enabled" (K false); +val (coercion_enabled, coercion_enabled_setup) = + Attrib.config_bool "coercion_enabled" (K false); val add_term_check = Syntax.add_term_check ~100 "coercions" - (fn xs => fn ctxt => - if Config.get ctxt coercion_enabled then - let val xs' = coercion_infer_types ctxt xs - in if eq_list (op aconv) (xs, xs') then NONE else SOME (xs', ctxt) end - else NONE); + (fn ctxt => Config.get ctxt coercion_enabled ? coercion_infer_types ctxt); (* declarations *)