Syntax.(un)check: explicit result option;
authorwenzelm
Tue Oct 16 19:45:57 2007 +0200 (2007-10-16)
changeset 2506017c313217998
parent 25059 e6e0ee56a672
child 25061 250e1da3204b
Syntax.(un)check: explicit result option;
src/Pure/Isar/class.ML
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Isar/class.ML	Tue Oct 16 19:45:56 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Tue Oct 16 19:45:57 2007 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4      -> string list -> theory -> string * Proof.context
     1.5    val class_cmd: bstring -> xstring list -> Element.context Locale.element list
     1.6      -> xstring list -> theory -> string * Proof.context
     1.7 -  val init: class -> Proof.context -> Proof.context;
     1.8 +  val init: class -> Proof.context -> Proof.context
     1.9    val add_const_in_class: string -> (string * mixfix) * (string * term)
    1.10      -> theory -> string * theory
    1.11    val add_abbrev_in_class: string -> Syntax.mode -> (string * mixfix) * (string * term)
    1.12 @@ -588,7 +588,7 @@
    1.13        #> (map_types o map_type_tvar) (fn var as (vi, _) => if member (op =) typarams vi
    1.14             then TFree (Name.aT, local_sort) else TVar var)) ts;
    1.15      val ctxt' = fold (ProofContext.add_const_constraint o apsnd SOME) constraints ctxt;
    1.16 -  in (ts', ctxt') end;
    1.17 +  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt') end;
    1.18  
    1.19  val uncheck = ref false;
    1.20  
    1.21 @@ -605,7 +605,7 @@
    1.22            | NONE => t)
    1.23        | globalize t = t;
    1.24      val ts' = if ! uncheck then (map o map_aterms) globalize ts else ts;
    1.25 -  in (ts', ctxt) end;
    1.26 +  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
    1.27  
    1.28  fun init_class_ctxt sups local_sort ctxt =
    1.29    let
     2.1 --- a/src/Pure/Isar/proof_context.ML	Tue Oct 16 19:45:56 2007 +0200
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Oct 16 19:45:57 2007 +0200
     2.3 @@ -585,16 +585,17 @@
     2.4  fun standard_term_uncheck ctxt =
     2.5    map (contract_abbrevs ctxt);
     2.6  
     2.7 -fun add what f = Context.add_setup
     2.8 -  (Context.theory_map (what (fn xs => fn ctxt => (f ctxt xs, ctxt))));
     2.9 +fun add eq what f = Context.add_setup
    2.10 +  (Context.theory_map (what (fn xs => fn ctxt =>
    2.11 +    let val xs' = f ctxt xs in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end)));
    2.12  
    2.13  in
    2.14  
    2.15 -val _ = add (Syntax.add_typ_check 0 "standard") standard_typ_check;
    2.16 -val _ = add (Syntax.add_term_check 0 "standard") standard_term_check;
    2.17 -val _ = add (Syntax.add_term_check 100 "fixate") prepare_patterns;
    2.18 +val _ = add (op =) (Syntax.add_typ_check 0 "standard") standard_typ_check;
    2.19 +val _ = add (op aconv) (Syntax.add_term_check 0 "standard") standard_term_check;
    2.20 +val _ = add (op aconv) (Syntax.add_term_check 100 "fixate") prepare_patterns;
    2.21  
    2.22 -val _ = add (Syntax.add_term_uncheck 0 "standard") standard_term_uncheck;
    2.23 +val _ = add (op aconv) (Syntax.add_term_uncheck 0 "standard") standard_term_uncheck;
    2.24  
    2.25  end;
    2.26  
     3.1 --- a/src/Pure/Syntax/syntax.ML	Tue Oct 16 19:45:56 2007 +0200
     3.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Oct 16 19:45:57 2007 +0200
     3.3 @@ -105,16 +105,16 @@
     3.4      unparse_term: Proof.context -> term -> Pretty.T} -> unit
     3.5    val print_checks: Proof.context -> unit
     3.6    val add_typ_check: int -> string ->
     3.7 -    (typ list -> Proof.context -> typ list * Proof.context) ->
     3.8 +    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
     3.9      Context.generic -> Context.generic
    3.10    val add_term_check: int -> string ->
    3.11 -    (term list -> Proof.context -> term list * Proof.context) ->
    3.12 +    (term list -> Proof.context -> (term list * Proof.context) option) ->
    3.13      Context.generic -> Context.generic
    3.14    val add_typ_uncheck: int -> string ->
    3.15 -    (typ list -> Proof.context -> typ list * Proof.context) ->
    3.16 +    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
    3.17      Context.generic -> Context.generic
    3.18    val add_term_uncheck: int -> string ->
    3.19 -    (term list -> Proof.context -> term list * Proof.context) ->
    3.20 +    (term list -> Proof.context -> (term list * Proof.context) option) ->
    3.21      Context.generic -> Context.generic
    3.22    val check_sort: Proof.context -> sort -> sort
    3.23    val check_typ: Proof.context -> typ -> typ
    3.24 @@ -684,7 +684,7 @@
    3.25  local
    3.26  
    3.27  type key = int * bool;
    3.28 -type 'a check = 'a list -> Proof.context -> 'a list * Proof.context;
    3.29 +type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
    3.30  
    3.31  structure Checks = GenericDataFun
    3.32  (
    3.33 @@ -701,19 +701,16 @@
    3.34  fun gen_add which (key: key) name f =
    3.35    Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
    3.36  
    3.37 -fun gen_check which uncheck eq ctxt0 xs0 =
    3.38 +fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
    3.39 +
    3.40 +fun gen_check which uncheck ctxt0 xs0 =
    3.41    let
    3.42      val funs = which (Checks.get (Context.Proof ctxt0))
    3.43        |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
    3.44 -      |> Library.sort (int_ord o pairself fst)
    3.45 -      |> not uncheck ? map (apsnd rev);
    3.46 -
    3.47 -    fun check_fixpoint fs (xs, ctxt) =
    3.48 -      let val (xs', ctxt') = fold uncurry fs (xs, ctxt) in
    3.49 -        if eq_list eq (xs, xs') then (xs, ctxt)
    3.50 -        else check_fixpoint fs (xs', ctxt')
    3.51 -      end;
    3.52 -  in #1 (fold (check_fixpoint o snd) funs (xs0, ctxt0)) end;
    3.53 +      |> Library.sort (int_ord o pairself fst) |> map snd
    3.54 +      |> not uncheck ? map rev;
    3.55 +    val check_all = perhaps_apply (map check_stage funs);
    3.56 +  in #1 (perhaps check_all (xs0, ctxt0)) end;
    3.57  
    3.58  fun map_sort f S =
    3.59    (case f (TFree ("", S)) of
    3.60 @@ -748,8 +745,8 @@
    3.61  fun add_typ_uncheck stage = gen_add apfst (stage, true);
    3.62  fun add_term_uncheck stage = gen_add apsnd (stage, true);
    3.63  
    3.64 -val check_typs = gen_check fst false (op =);
    3.65 -val check_terms = gen_check snd false (op aconv);
    3.66 +val check_typs = gen_check fst false;
    3.67 +val check_terms = gen_check snd false;
    3.68  fun check_props ctxt = map (TypeInfer.constrain propT) #> check_terms ctxt;
    3.69  
    3.70  val check_typ = singleton o check_typs;
    3.71 @@ -757,8 +754,8 @@
    3.72  val check_prop = singleton o check_props;
    3.73  val check_sort = map_sort o check_typ;
    3.74  
    3.75 -val uncheck_typs = gen_check fst true (op =);
    3.76 -val uncheck_terms = gen_check snd true (op aconv);
    3.77 +val uncheck_typs = gen_check fst true;
    3.78 +val uncheck_terms = gen_check snd true;
    3.79  val uncheck_sort = map_sort o singleton o uncheck_typs;
    3.80  
    3.81  end;