src/Provers/classical.ML
changeset 22674 1a610904bbca
parent 22474 ecdaec8cf13a
child 22846 fb79144af9a3
     1.1 --- a/src/Provers/classical.ML	Sat Apr 14 00:46:23 2007 +0200
     1.2 +++ b/src/Provers/classical.ML	Sat Apr 14 11:05:12 2007 +0200
     1.3 @@ -299,12 +299,8 @@
     1.4  
     1.5  fun rep_cs (CS args) = args;
     1.6  
     1.7 -local
     1.8 -  fun wrap l tac = foldr (fn ((name,tacf),w) => tacf w) tac l;
     1.9 -in
    1.10 -  fun appSWrappers (CS{swrappers,...}) = wrap swrappers;
    1.11 -  fun appWrappers  (CS{uwrappers,...}) = wrap uwrappers;
    1.12 -end;
    1.13 +fun appSWrappers (CS {swrappers, ...}) = fold snd swrappers;
    1.14 +fun appWrappers  (CS {uwrappers, ...}) = fold snd uwrappers;
    1.15  
    1.16  
    1.17  (*** Adding (un)safe introduction or elimination rules.
    1.18 @@ -586,53 +582,45 @@
    1.19  
    1.20  
    1.21  (*** Modifying the wrapper tacticals ***)
    1.22 -fun update_swrappers
    1.23 -(CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.24 -    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f =
    1.25 - CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
    1.26 +fun map_swrappers f
    1.27 +  (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.28 +    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.29 +  CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
    1.30      swrappers = f swrappers, uwrappers = uwrappers,
    1.31      safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
    1.32      haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
    1.33  
    1.34 -fun update_uwrappers
    1.35 -(CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.36 -    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f =
    1.37 - CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
    1.38 +fun map_uwrappers f
    1.39 +  (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.40 +    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.41 +  CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
    1.42      swrappers = swrappers, uwrappers = f uwrappers,
    1.43      safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
    1.44      haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
    1.45  
    1.46 -fun overwrite_warn msg (p as (key : string, v)) xs =
    1.47 -  let
    1.48 -    fun over ((q as (keyi, _)) :: xs) =
    1.49 -          if keyi = key then p :: xs else q :: over xs
    1.50 -      | over [] = [p];
    1.51 -  in (
    1.52 -    if AList.defined (op =) xs key then warning msg else ();
    1.53 -    over xs
    1.54 -  ) end;
    1.55 +fun update_warn msg (p as (key : string, _)) xs =
    1.56 +  (if AList.defined (op =) xs key then warning msg else ();
    1.57 +    AList.update (op =) p xs);
    1.58 +
    1.59 +fun delete_warn msg (key : string) xs =
    1.60 +  if AList.defined (op =) xs key then AList.delete (op =) key xs
    1.61 +    else (warning msg; xs);
    1.62  
    1.63  (*Add/replace a safe wrapper*)
    1.64 -fun cs addSWrapper new_swrapper = update_swrappers cs
    1.65 -  (overwrite_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper);
    1.66 +fun cs addSWrapper new_swrapper = map_swrappers
    1.67 +  (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs;
    1.68  
    1.69  (*Add/replace an unsafe wrapper*)
    1.70 -fun cs addWrapper new_uwrapper = update_uwrappers cs
    1.71 -  (overwrite_warn ("Overwriting unsafe wrapper "^fst new_uwrapper) new_uwrapper);
    1.72 +fun cs addWrapper new_uwrapper = map_uwrappers
    1.73 +  (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs;
    1.74  
    1.75  (*Remove a safe wrapper*)
    1.76 -fun cs delSWrapper name = update_swrappers cs (fn swrappers =>
    1.77 -  let val swrappers' = filter_out (equal name o fst) swrappers in
    1.78 -    if length swrappers <> length swrappers' then swrappers'
    1.79 -    else (warning ("No such safe wrapper in claset: "^ name); swrappers)
    1.80 -  end);
    1.81 +fun cs delSWrapper name = map_swrappers
    1.82 +  (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs;
    1.83  
    1.84  (*Remove an unsafe wrapper*)
    1.85 -fun cs delWrapper name = update_uwrappers cs (fn uwrappers =>
    1.86 -  let val uwrappers' = filter_out (equal name o fst) uwrappers in
    1.87 -    if length uwrappers <> length uwrappers' then uwrappers'
    1.88 -    else (warning ("No such unsafe wrapper in claset: " ^ name); uwrappers)
    1.89 -  end);
    1.90 +fun cs delWrapper name = map_uwrappers
    1.91 +  (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs;
    1.92  
    1.93  (* compose a safe tactic alternatively before/after safe_step_tac *)
    1.94  fun cs addSbefore  (name,    tac1) =
    1.95 @@ -658,20 +646,23 @@
    1.96  (*Merge works by adding all new rules of the 2nd claset into the 1st claset.
    1.97    Merging the term nets may look more efficient, but the rather delicate
    1.98    treatment of priority might get muddled up.*)
    1.99 -fun merge_cs (cs as CS{safeIs, safeEs, hazIs, hazEs, ...},
   1.100 -     CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, swrappers, uwrappers, ...}) =
   1.101 -  let val safeIs' = fold rem_thm safeIs safeIs2
   1.102 -      val safeEs' = fold rem_thm safeEs safeEs2
   1.103 -      val hazIs' = fold rem_thm hazIs hazIs2
   1.104 -      val hazEs' = fold rem_thm hazEs hazEs2
   1.105 -      val cs1   = cs addSIs safeIs'
   1.106 -                     addSEs safeEs'
   1.107 -                     addIs  hazIs'
   1.108 -                     addEs  hazEs'
   1.109 -      val cs2 = update_swrappers cs1 (fn ws => merge_alists ws swrappers);
   1.110 -      val cs3 = update_uwrappers cs2 (fn ws => merge_alists ws uwrappers);
   1.111 -  in cs3
   1.112 -  end;
   1.113 +fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...},
   1.114 +    CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2,
   1.115 +      swrappers, uwrappers, ...}) =
   1.116 +  let
   1.117 +    val safeIs' = fold rem_thm safeIs safeIs2;
   1.118 +    val safeEs' = fold rem_thm safeEs safeEs2;
   1.119 +    val hazIs' = fold rem_thm hazIs hazIs2;
   1.120 +    val hazEs' = fold rem_thm hazEs hazEs2;
   1.121 +    val cs1   = cs addSIs safeIs'
   1.122 +                   addSEs safeEs'
   1.123 +                   addIs  hazIs'
   1.124 +                   addEs  hazEs';
   1.125 +    val cs2 = map_swrappers
   1.126 +      (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1;
   1.127 +    val cs3 = map_uwrappers
   1.128 +      (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2;
   1.129 +  in cs3 end;
   1.130  
   1.131  
   1.132  (**** Simple tactics for theorem proving ****)
   1.133 @@ -841,7 +832,8 @@
   1.134    let
   1.135      fun add_wrapper add (name, f) claset = add (claset, (name, f ctxt));
   1.136    in
   1.137 -    cs |> fold_rev (add_wrapper (op addSWrapper)) swrappers
   1.138 +    cs
   1.139 +    |> fold_rev (add_wrapper (op addSWrapper)) swrappers
   1.140      |> fold_rev (add_wrapper (op addWrapper)) uwrappers
   1.141    end;
   1.142  
   1.143 @@ -854,9 +846,8 @@
   1.144    let
   1.145      val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1;
   1.146      val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2;
   1.147 -
   1.148 -    val swrappers' = merge_alists swrappers1 swrappers2;
   1.149 -    val uwrappers' = merge_alists uwrappers1 uwrappers2;
   1.150 +    val swrappers' = AList.merge (op =) (K true) (swrappers1, swrappers2);
   1.151 +    val uwrappers' = AList.merge (op =) (K true) (uwrappers1, uwrappers2);
   1.152    in make_context_cs (swrappers', uwrappers') end;
   1.153  
   1.154  
   1.155 @@ -907,11 +898,15 @@
   1.156  
   1.157  (* context dependent components *)
   1.158  
   1.159 -fun add_context_safe_wrapper wrapper = map_context_cs (apfst (merge_alists [wrapper]));
   1.160 -fun del_context_safe_wrapper name = map_context_cs (apfst (filter_out (equal name o #1)));
   1.161 +fun add_context_safe_wrapper wrapper = (map_context_cs o apfst)
   1.162 +  (AList.update (op =) wrapper);
   1.163 +fun del_context_safe_wrapper name = (map_context_cs o apfst)
   1.164 +  (AList.delete (op =) name);
   1.165  
   1.166 -fun add_context_unsafe_wrapper wrapper = map_context_cs (apsnd (merge_alists [wrapper]));
   1.167 -fun del_context_unsafe_wrapper name = map_context_cs (apsnd (filter_out (equal name o #1)));
   1.168 +fun add_context_unsafe_wrapper wrapper = (map_context_cs o apsnd)
   1.169 +  (AList.update (op =) wrapper);
   1.170 +fun del_context_unsafe_wrapper name = (map_context_cs o apsnd)
   1.171 +  (AList.delete (op =) name);
   1.172  
   1.173  
   1.174  (* local claset *)