# HG changeset patch # User wenzelm # Date 1192556757 -7200 # Node ID 17c313217998b58f8b2bcf81c37992aa8e134f0f # Parent e6e0ee56a67282894b2f49e12d816c490151861c Syntax.(un)check: explicit result option; diff -r e6e0ee56a672 -r 17c313217998 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Tue Oct 16 19:45:56 2007 +0200 +++ b/src/Pure/Isar/class.ML Tue Oct 16 19:45:57 2007 +0200 @@ -18,7 +18,7 @@ -> string list -> theory -> string * Proof.context val class_cmd: bstring -> xstring list -> Element.context Locale.element list -> xstring list -> theory -> string * Proof.context - val init: class -> Proof.context -> Proof.context; + val init: class -> Proof.context -> Proof.context val add_const_in_class: string -> (string * mixfix) * (string * term) -> theory -> string * theory val add_abbrev_in_class: string -> Syntax.mode -> (string * mixfix) * (string * term) @@ -588,7 +588,7 @@ #> (map_types o map_type_tvar) (fn var as (vi, _) => if member (op =) typarams vi then TFree (Name.aT, local_sort) else TVar var)) ts; val ctxt' = fold (ProofContext.add_const_constraint o apsnd SOME) constraints ctxt; - in (ts', ctxt') end; + in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt') end; val uncheck = ref false; @@ -605,7 +605,7 @@ | NONE => t) | globalize t = t; val ts' = if ! uncheck then (map o map_aterms) globalize ts else ts; - in (ts', ctxt) end; + in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end; fun init_class_ctxt sups local_sort ctxt = let diff -r e6e0ee56a672 -r 17c313217998 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Oct 16 19:45:56 2007 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Oct 16 19:45:57 2007 +0200 @@ -585,16 +585,17 @@ fun standard_term_uncheck ctxt = map (contract_abbrevs ctxt); -fun add what f = Context.add_setup - (Context.theory_map (what (fn xs => fn ctxt => (f ctxt xs, ctxt)))); +fun add eq what f = Context.add_setup + (Context.theory_map (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 (Syntax.add_typ_check 0 "standard") standard_typ_check; -val _ = add (Syntax.add_term_check 0 "standard") standard_term_check; -val _ = add (Syntax.add_term_check 100 "fixate") prepare_patterns; +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 (Syntax.add_term_uncheck 0 "standard") standard_term_uncheck; +val _ = add (op aconv) (Syntax.add_term_uncheck 0 "standard") standard_term_uncheck; end; diff -r e6e0ee56a672 -r 17c313217998 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Tue Oct 16 19:45:56 2007 +0200 +++ b/src/Pure/Syntax/syntax.ML Tue Oct 16 19:45:57 2007 +0200 @@ -105,16 +105,16 @@ unparse_term: Proof.context -> term -> Pretty.T} -> unit val print_checks: Proof.context -> unit val add_typ_check: int -> string -> - (typ list -> Proof.context -> typ list * Proof.context) -> + (typ list -> Proof.context -> (typ list * Proof.context) option) -> Context.generic -> Context.generic val add_term_check: int -> string -> - (term list -> Proof.context -> term list * Proof.context) -> + (term list -> Proof.context -> (term list * Proof.context) option) -> Context.generic -> Context.generic val add_typ_uncheck: int -> string -> - (typ list -> Proof.context -> typ list * Proof.context) -> + (typ list -> Proof.context -> (typ list * Proof.context) option) -> Context.generic -> Context.generic val add_term_uncheck: int -> string -> - (term list -> Proof.context -> term list * Proof.context) -> + (term list -> Proof.context -> (term list * Proof.context) option) -> Context.generic -> Context.generic val check_sort: Proof.context -> sort -> sort val check_typ: Proof.context -> typ -> typ @@ -684,7 +684,7 @@ local type key = int * bool; -type 'a check = 'a list -> Proof.context -> 'a list * Proof.context; +type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option; structure Checks = GenericDataFun ( @@ -701,19 +701,16 @@ fun gen_add which (key: key) name f = Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ())))); -fun gen_check which uncheck eq ctxt0 xs0 = +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) - |> not uncheck ? map (apsnd rev); - - fun check_fixpoint fs (xs, ctxt) = - let val (xs', ctxt') = fold uncurry fs (xs, ctxt) in - if eq_list eq (xs, xs') then (xs, ctxt) - else check_fixpoint fs (xs', ctxt') - end; - in #1 (fold (check_fixpoint o snd) funs (xs0, ctxt0)) end; + |> 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 @@ -748,8 +745,8 @@ fun add_typ_uncheck stage = gen_add apfst (stage, true); fun add_term_uncheck stage = gen_add apsnd (stage, true); -val check_typs = gen_check fst false (op =); -val check_terms = gen_check snd false (op aconv); +val check_typs = gen_check fst false; +val check_terms = gen_check snd false; fun check_props ctxt = map (TypeInfer.constrain propT) #> check_terms ctxt; val check_typ = singleton o check_typs; @@ -757,8 +754,8 @@ val check_prop = singleton o check_props; val check_sort = map_sort o check_typ; -val uncheck_typs = gen_check fst true (op =); -val uncheck_terms = gen_check snd true (op aconv); +val uncheck_typs = gen_check fst true; +val uncheck_terms = gen_check snd true; val uncheck_sort = map_sort o singleton o uncheck_typs; end;