src/Provers/classical.ML
changeset 1927 6f97cb16e453
parent 1814 89f8d4a88cca
child 1938 4e29ea45520d
     1.1 --- a/src/Provers/classical.ML	Tue Aug 20 12:36:58 1996 +0200
     1.2 +++ b/src/Provers/classical.ML	Tue Aug 20 12:39:30 1996 +0200
     1.3 @@ -226,16 +226,34 @@
     1.4  
     1.5  val delete = delete_tagged_list o joinrules;
     1.6  
     1.7 +(*Warn if the rule is already present ELSEWHERE in the claset.  The addition
     1.8 +  is still allowed.*)
     1.9 +fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = 
    1.10 +       if gen_mem eq_thm (th, safeIs) then 
    1.11 +	 warning ("rule already in claset as Safe Intr\n" ^ string_of_thm th)
    1.12 +  else if gen_mem eq_thm (th, safeEs) then
    1.13 +         warning ("rule already in claset as Safe Elim\n" ^ string_of_thm th)
    1.14 +  else if gen_mem eq_thm (th, hazIs) then 
    1.15 +         warning ("rule already in claset as unsafe Intr\n" ^ string_of_thm th)
    1.16 +  else if gen_mem eq_thm (th, hazEs) then 
    1.17 +         warning ("rule already in claset as unsafe Elim\n" ^ string_of_thm th)
    1.18 +  else ();
    1.19 +
    1.20  (*** Safe rules ***)
    1.21  
    1.22 -fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
    1.23 -	safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) 
    1.24 -    addSIs  ths  =
    1.25 +fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
    1.26 +	      safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
    1.27 +	   th)  =
    1.28 +  if gen_mem eq_thm (th, safeIs) then 
    1.29 +	 (warning ("ignoring duplicate Safe Intr\n" ^ string_of_thm th);
    1.30 +	  cs)
    1.31 +  else
    1.32    let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
    1.33 -          partition (fn rl => nprems_of rl=0) ths
    1.34 -      val nI = length safeIs + length ths
    1.35 +          partition (fn rl => nprems_of rl=0) [th]
    1.36 +      val nI = length safeIs + 1
    1.37        and nE = length safeEs
    1.38 -  in CS{safeIs	= ths@safeIs,
    1.39 +  in warn_dup th cs;
    1.40 +     CS{safeIs	= th::safeIs,
    1.41          safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair,
    1.42  	safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair,
    1.43  	safeEs	= safeEs,
    1.44 @@ -246,15 +264,19 @@
    1.45  	dup_netpair = dup_netpair}
    1.46    end;
    1.47  
    1.48 -fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
    1.49 -	safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) 
    1.50 -    addSEs  ths  =
    1.51 +fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
    1.52 +		    safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
    1.53 +	   th)  =
    1.54 +  if gen_mem eq_thm (th, safeEs) then 
    1.55 +	 (warning ("ignoring duplicate Safe Elim\n" ^ string_of_thm th);
    1.56 +	  cs)
    1.57 +  else
    1.58    let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
    1.59 -          partition (fn rl => nprems_of rl=1) ths
    1.60 +          partition (fn rl => nprems_of rl=1) [th]
    1.61        val nI = length safeIs
    1.62 -      and nE = length safeEs + length ths
    1.63 -  in 
    1.64 -     CS{safeEs	= ths@safeEs,
    1.65 +      and nE = length safeEs + 1
    1.66 +  in warn_dup th cs;
    1.67 +     CS{safeEs	= th::safeEs,
    1.68          safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair,
    1.69  	safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair,
    1.70  	safeIs	= safeIs,
    1.71 @@ -265,20 +287,29 @@
    1.72  	dup_netpair = dup_netpair}
    1.73    end;
    1.74  
    1.75 +fun rev_foldl f (e, l) = foldl f (e, rev l);
    1.76 +
    1.77 +val op addSIs = rev_foldl addSI;
    1.78 +val op addSEs = rev_foldl addSE;
    1.79 +
    1.80  fun cs addSDs ths = cs addSEs (map make_elim ths);
    1.81  
    1.82  
    1.83  (*** Hazardous (unsafe) rules ***)
    1.84  
    1.85 -fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
    1.86 -	safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) 
    1.87 -    addIs  ths  =
    1.88 -  let val nI = length hazIs + length ths
    1.89 +fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
    1.90 +		   safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
    1.91 +	  th)=
    1.92 +  if gen_mem eq_thm (th, hazIs) then 
    1.93 +	 (warning ("ignoring duplicate unsafe Intr\n" ^ string_of_thm th);
    1.94 +	  cs)
    1.95 +  else
    1.96 +  let val nI = length hazIs + 1
    1.97        and nE = length hazEs
    1.98 -  in 
    1.99 -     CS{hazIs	= ths@hazIs,
   1.100 -	haz_netpair = insert (nI,nE) (ths, []) haz_netpair,
   1.101 -	dup_netpair = insert (nI,nE) (map dup_intr ths, []) dup_netpair,
   1.102 +  in warn_dup th cs;
   1.103 +     CS{hazIs	= th::hazIs,
   1.104 +	haz_netpair = insert (nI,nE) ([th], []) haz_netpair,
   1.105 +	dup_netpair = insert (nI,nE) (map dup_intr [th], []) dup_netpair,
   1.106  	safeIs 	= safeIs, 
   1.107  	safeEs	= safeEs,
   1.108  	hazEs	= hazEs,
   1.109 @@ -287,15 +318,19 @@
   1.110  	safep_netpair = safep_netpair}
   1.111    end;
   1.112  
   1.113 -fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   1.114 -	safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) 
   1.115 -    addEs  ths  =
   1.116 +fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   1.117 +		   safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
   1.118 +	  th) =
   1.119 +  if gen_mem eq_thm (th, hazEs) then 
   1.120 +	 (warning ("ignoring duplicate unsafe Elim\n" ^ string_of_thm th);
   1.121 +	  cs)
   1.122 +  else
   1.123    let val nI = length hazIs 
   1.124 -      and nE = length hazEs + length ths
   1.125 -  in 
   1.126 -     CS{hazEs	= ths@hazEs,
   1.127 -	haz_netpair = insert (nI,nE) ([], ths) haz_netpair,
   1.128 -	dup_netpair = insert (nI,nE) ([], map dup_elim ths) dup_netpair,
   1.129 +      and nE = length hazEs + 1
   1.130 +  in warn_dup th cs;
   1.131 +     CS{hazEs	= th::hazEs,
   1.132 +	haz_netpair = insert (nI,nE) ([], [th]) haz_netpair,
   1.133 +	dup_netpair = insert (nI,nE) ([], map dup_elim [th]) dup_netpair,
   1.134  	safeIs	= safeIs, 
   1.135  	safeEs	= safeEs,
   1.136  	hazIs	= hazIs,
   1.137 @@ -304,17 +339,20 @@
   1.138  	safep_netpair = safep_netpair}
   1.139    end;
   1.140  
   1.141 +val op addIs = rev_foldl addI;
   1.142 +val op addEs = rev_foldl addE;
   1.143 +
   1.144  fun cs addDs ths = cs addEs (map make_elim ths);
   1.145  
   1.146  
   1.147  (*** Deletion of rules 
   1.148       Working out what to delete, requires repeating much of the code used
   1.149  	to insert.
   1.150 -     Separate functions delSIs, etc., are not exported; instead delrules
   1.151 +     Separate functions delSI, etc., are not exported; instead delrules
   1.152          searches in all the lists and chooses the relevant delXX function.
   1.153  ***)
   1.154  
   1.155 -fun delSIs (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   1.156 +fun delSI (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   1.157                 safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
   1.158              th) =
   1.159    let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=0) [th]
   1.160 @@ -329,7 +367,7 @@
   1.161  	dup_netpair = dup_netpair}
   1.162    end;
   1.163  
   1.164 -fun delSEs (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   1.165 +fun delSE (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   1.166  	       safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
   1.167              th) =
   1.168    let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=1) [th]
   1.169 @@ -345,7 +383,7 @@
   1.170    end;
   1.171  
   1.172  
   1.173 -fun delIs (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   1.174 +fun delI (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   1.175  	      safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
   1.176  	   th) =
   1.177       CS{hazIs	= gen_rem eq_thm (hazIs,th),
   1.178 @@ -358,7 +396,7 @@
   1.179  	safe0_netpair = safe0_netpair,
   1.180  	safep_netpair = safep_netpair};
   1.181  
   1.182 -fun delEs (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   1.183 +fun delE (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   1.184  	      safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
   1.185  	   th) =
   1.186       CS{hazEs	= gen_rem eq_thm (hazEs,th),
   1.187 @@ -372,10 +410,10 @@
   1.188  	safep_netpair = safep_netpair};
   1.189  
   1.190  fun delrule (cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, th) =
   1.191 -       if gen_mem eq_thm (th, safeIs) then delSIs(cs,th)
   1.192 -  else if gen_mem eq_thm (th, safeEs) then delSEs(cs,th)
   1.193 -  else if gen_mem eq_thm (th, hazIs) then delIs(cs,th)
   1.194 -  else if gen_mem eq_thm (th, hazEs) then delEs(cs,th)
   1.195 +       if gen_mem eq_thm (th, safeIs) then delSI(cs,th)
   1.196 +  else if gen_mem eq_thm (th, safeEs) then delSE(cs,th)
   1.197 +  else if gen_mem eq_thm (th, hazIs) then delI(cs,th)
   1.198 +  else if gen_mem eq_thm (th, hazEs) then delE(cs,th)
   1.199    else (warning ("rule not in claset\n" ^ (string_of_thm th)); 
   1.200  	cs);
   1.201