minor tuning and modernization;
authorwenzelm
Tue Apr 19 16:13:04 2011 +0200 (2011-04-19)
changeset 42404fbd136946b35
parent 42403 38b29c9fc742
child 42405 13ecdb3057d8
minor tuning and modernization;
src/Pure/Isar/overloading.ML
     1.1 --- a/src/Pure/Isar/overloading.ML	Tue Apr 19 15:58:05 2011 +0200
     1.2 +++ b/src/Pure/Isar/overloading.ML	Tue Apr 19 16:13:04 2011 +0200
     1.3 @@ -19,13 +19,13 @@
     1.4  structure Overloading: OVERLOADING =
     1.5  struct
     1.6  
     1.7 -(** generic check/uncheck combinators for improvable constants **)
     1.8 +(* generic check/uncheck combinators for improvable constants *)
     1.9  
    1.10  type improvable_syntax = ((((string * typ) list * (string * typ) list) *
    1.11    ((((string * typ -> (typ * typ) option) * (string * typ -> (typ * term) option)) * bool) *
    1.12      (term * term) list)) * bool);
    1.13  
    1.14 -structure ImprovableSyntax = Proof_Data
    1.15 +structure Improvable_Syntax = Proof_Data
    1.16  (
    1.17    type T = {
    1.18      primary_constraints: (string * typ) list,
    1.19 @@ -47,16 +47,17 @@
    1.20    };
    1.21  );
    1.22  
    1.23 -fun map_improvable_syntax f = ImprovableSyntax.map (fn { primary_constraints,
    1.24 -    secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed } =>
    1.25 +fun map_improvable_syntax f = Improvable_Syntax.map (fn {primary_constraints,
    1.26 +    secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed} =>
    1.27    let
    1.28      val (((primary_constraints', secondary_constraints'),
    1.29        (((improve', subst'), consider_abbrevs'), unchecks')), passed')
    1.30          = f (((primary_constraints, secondary_constraints),
    1.31              (((improve, subst), consider_abbrevs), unchecks)), passed)
    1.32 -  in { primary_constraints = primary_constraints', secondary_constraints = secondary_constraints',
    1.33 +  in
    1.34 +   {primary_constraints = primary_constraints', secondary_constraints = secondary_constraints',
    1.35      improve = improve', subst = subst', consider_abbrevs = consider_abbrevs',
    1.36 -    unchecks = unchecks', passed = passed' }
    1.37 +    unchecks = unchecks', passed = passed'}
    1.38    end);
    1.39  
    1.40  val mark_passed = (map_improvable_syntax o apsnd) (K true);
    1.41 @@ -65,8 +66,8 @@
    1.42    let
    1.43      val thy = Proof_Context.theory_of ctxt;
    1.44  
    1.45 -    val { secondary_constraints, improve, subst, consider_abbrevs, passed, ... } =
    1.46 -      ImprovableSyntax.get ctxt;
    1.47 +    val {secondary_constraints, improve, subst, consider_abbrevs, passed, ...} =
    1.48 +      Improvable_Syntax.get ctxt;
    1.49      val is_abbrev = consider_abbrevs andalso Proof_Context.abbrev_mode ctxt;
    1.50      val passed_or_abbrev = passed orelse is_abbrev;
    1.51      fun accumulate_improvements (Const (c, ty)) =
    1.52 @@ -87,28 +88,28 @@
    1.53          | _ => NONE) t;
    1.54      val ts'' = if is_abbrev then ts' else map apply_subst ts';
    1.55    in
    1.56 -    if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE else
    1.57 -    if passed_or_abbrev then SOME (ts'', ctxt)
    1.58 -    else SOME (ts'', ctxt
    1.59 -      |> fold (Proof_Context.add_const_constraint o apsnd SOME) secondary_constraints
    1.60 -      |> mark_passed)
    1.61 +    if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE
    1.62 +    else if passed_or_abbrev then SOME (ts'', ctxt)
    1.63 +    else
    1.64 +      SOME (ts'', ctxt
    1.65 +        |> fold (Proof_Context.add_const_constraint o apsnd SOME) secondary_constraints
    1.66 +        |> mark_passed)
    1.67    end;
    1.68  
    1.69  fun rewrite_liberal thy unchecks t =
    1.70 -  case try (Pattern.rewrite_term thy unchecks []) t
    1.71 -   of NONE => NONE
    1.72 -    | SOME t' => if t aconv t' then NONE else SOME t';
    1.73 +  (case try (Pattern.rewrite_term thy unchecks []) t of
    1.74 +    NONE => NONE
    1.75 +  | SOME t' => if t aconv t' then NONE else SOME t');
    1.76  
    1.77  fun improve_term_uncheck ts ctxt =
    1.78    let
    1.79      val thy = Proof_Context.theory_of ctxt;
    1.80 -    val unchecks = (#unchecks o ImprovableSyntax.get) ctxt;
    1.81 +    val {unchecks, ...} = Improvable_Syntax.get ctxt;
    1.82      val ts' = map (rewrite_liberal thy unchecks) ts;
    1.83    in if exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end;
    1.84  
    1.85  fun set_primary_constraints ctxt =
    1.86 -  let
    1.87 -    val { primary_constraints, ... } = ImprovableSyntax.get ctxt;
    1.88 +  let val {primary_constraints, ...} = Improvable_Syntax.get ctxt;
    1.89    in fold (Proof_Context.add_const_constraint o apsnd SOME) primary_constraints ctxt end;
    1.90  
    1.91  val activate_improvable_syntax =
    1.92 @@ -118,7 +119,7 @@
    1.93    #> set_primary_constraints;
    1.94  
    1.95  
    1.96 -(** overloading target **)
    1.97 +(* overloading target *)
    1.98  
    1.99  structure Data = Proof_Data
   1.100  (
   1.101 @@ -129,16 +130,18 @@
   1.102  val get_overloading = Data.get o Local_Theory.target_of;
   1.103  val map_overloading = Local_Theory.target o Data.map;
   1.104  
   1.105 -fun operation lthy b = get_overloading lthy
   1.106 +fun operation lthy b =
   1.107 +  get_overloading lthy
   1.108    |> get_first (fn ((c, _), (v, checked)) =>
   1.109        if Binding.name_of b = v then SOME (c, (v, checked)) else NONE);
   1.110  
   1.111  fun synchronize_syntax ctxt =
   1.112    let
   1.113      val overloading = Data.get ctxt;
   1.114 -    fun subst (c, ty) = case AList.lookup (op =) overloading (c, ty)
   1.115 -     of SOME (v, _) => SOME (ty, Free (v, ty))
   1.116 -      | NONE => NONE;
   1.117 +    fun subst (c, ty) =
   1.118 +      (case AList.lookup (op =) overloading (c, ty) of
   1.119 +        SOME (v, _) => SOME (ty, Free (v, ty))
   1.120 +      | NONE => NONE);
   1.121      val unchecks =
   1.122        map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading;
   1.123    in 
   1.124 @@ -155,12 +158,13 @@
   1.125    #-> (fn (_, def) => pair (Const (c, U), def))
   1.126  
   1.127  fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   1.128 -  case operation lthy b
   1.129 -   of SOME (c, (v, checked)) => if mx <> NoSyn
   1.130 -       then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
   1.131 -        else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
   1.132 -    | NONE => lthy |>
   1.133 -        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
   1.134 +  (case operation lthy b of
   1.135 +    SOME (c, (v, checked)) =>
   1.136 +      if mx <> NoSyn
   1.137 +      then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
   1.138 +      else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
   1.139 +  | NONE => lthy
   1.140 +      |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params));
   1.141  
   1.142  fun pretty lthy =
   1.143    let
   1.144 @@ -177,8 +181,8 @@
   1.145      val _ =
   1.146        if null overloading then ()
   1.147        else
   1.148 -        error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
   1.149 -          o Syntax.string_of_term lthy o Const o fst) overloading));
   1.150 +        error ("Missing definition(s) for parameter(s) " ^
   1.151 +          commas_quote (map (Syntax.string_of_term lthy o Const o fst) overloading));
   1.152    in lthy end;
   1.153  
   1.154  fun gen_overloading prep_const raw_overloading thy =