src/Provers/Arith/fast_lin_arith.ML
changeset 9073 40d8dfac96b8
parent 8263 699d4ad2ced3
child 9420 d4e9f60fe25a
     1.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Thu Jun 15 16:02:12 2000 +0200
     1.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Jun 16 13:13:55 2000 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  (in)equations. lin_arith_prover tries to prove or disprove the term.
     1.5  *)
     1.6  
     1.7 -(* Debugging: (*? -> (*?*), !*) -> (*!*) *)
     1.8 +(* Debugging: set Fast_Arith.trace *)
     1.9  
    1.10  (*** Data needed for setting up the linear arithmetic package ***)
    1.11  
    1.12 @@ -73,6 +73,7 @@
    1.13  
    1.14  signature FAST_LIN_ARITH =
    1.15  sig
    1.16 +  val trace           : bool ref
    1.17    val lin_arith_prover: Sign.sg -> thm list -> term -> thm option
    1.18    val     lin_arith_tac:             int -> tactic
    1.19    val cut_lin_arith_tac: thm list -> int -> tactic
    1.20 @@ -89,6 +90,8 @@
    1.21     treat non-negative atoms separately rather than adding 0 <= atom
    1.22  *)
    1.23  
    1.24 +val trace = ref false;
    1.25 +
    1.26  datatype lineq_type = Eq | Le | Lt;
    1.27  
    1.28  datatype injust = Asm of int
    1.29 @@ -194,16 +197,16 @@
    1.30          | extract xs []      = (None,xs)
    1.31    in extract [] end;
    1.32  
    1.33 -(*?
    1.34  fun print_ineqs ineqs =
    1.35 - writeln(cat_lines(""::map (fn Lineq(c,t,l,_) =>
    1.36 -   string_of_int c ^
    1.37 -   (case t of Eq => " =  " | Lt=> " <  " | Le => " <= ") ^
    1.38 -   commas(map string_of_int l)) ineqs));
    1.39 -!*)
    1.40 +  if !trace then
    1.41 +     writeln(cat_lines(""::map (fn Lineq(c,t,l,_) =>
    1.42 +       string_of_int c ^
    1.43 +       (case t of Eq => " =  " | Lt=> " <  " | Le => " <= ") ^
    1.44 +       commas(map string_of_int l)) ineqs))
    1.45 +  else ();
    1.46  
    1.47  fun elim ineqs =
    1.48 -  let (*?val dummy = print_ineqs ineqs;!*)
    1.49 +  let val dummy = print_ineqs ineqs;
    1.50        val (triv,nontriv) = partition is_trivial ineqs in
    1.51    if not(null triv)
    1.52    then case find_first is_answer triv of
    1.53 @@ -243,6 +246,12 @@
    1.54  (* Translate back a proof.                                                   *)
    1.55  (* ------------------------------------------------------------------------- *)
    1.56  
    1.57 +fun trace_thm msg th = 
    1.58 +    if !trace then (writeln msg; prth th) else th;
    1.59 +
    1.60 +fun trace_msg msg = 
    1.61 +    if !trace then writeln msg else ();
    1.62 +
    1.63  (* FIXME OPTIMIZE!!!!
    1.64     Addition/Multiplication need i*t representation rather than t+t+...
    1.65  
    1.66 @@ -272,16 +281,18 @@
    1.67          let val thm' = simplify (!LA_Data.ss_ref) thm
    1.68          in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end
    1.69  
    1.70 -      fun mk(Asm i) = ((*?writeln"Asm";prth!*)(nth_elem(i,asms)))
    1.71 -        | mk(Nat(i)) = ((*?writeln"Nat";!*)LA_Logic.mk_nat_thm sg (nth_elem(i,atoms)))
    1.72 -        | mk(LessD(j)) = ((*?writeln"L";prth!*)(hd([mk j] RL !LA_Data.lessD)))
    1.73 -        | mk(NotLeD(j)) = ((*?writeln"NLe";prth!*)(mk j RS LA_Logic.not_leD))
    1.74 -        | mk(NotLeDD(j)) = ((*?writeln"NLeD";prth!*)(hd([mk j RS LA_Logic.not_leD] RL !LA_Data.lessD)))
    1.75 -        | mk(NotLessD(j)) = ((*?writeln"NL";prth!*)(mk j RS LA_Logic.not_lessD))
    1.76 -        | mk(Added(j1,j2)) = ((*?writeln"+";prth!*)(simp((*?prth!*)(addthms (mk j1) (mk j2)))))
    1.77 -        | mk(Multiplied(n,j)) = ((*?writeln"*";!*)multn(n,mk j))
    1.78 +      fun mk(Asm i) = trace_thm "Asm" (nth_elem(i,asms))
    1.79 +        | mk(Nat(i)) = (trace_msg "Nat";
    1.80 +			LA_Logic.mk_nat_thm sg (nth_elem(i,atoms)))
    1.81 +        | mk(LessD(j)) = trace_thm "L" (hd([mk j] RL !LA_Data.lessD))
    1.82 +        | mk(NotLeD(j)) = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
    1.83 +        | mk(NotLeDD(j)) = trace_thm "NLeD" (hd([mk j RS LA_Logic.not_leD] RL 
    1.84 +						!LA_Data.lessD))
    1.85 +        | mk(NotLessD(j)) = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
    1.86 +        | mk(Added(j1,j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2)))
    1.87 +        | mk(Multiplied(n,j)) = (trace_msg "*"; multn(n,mk j))
    1.88  
    1.89 -  in (*?writeln"mkthm";!*)
    1.90 +  in trace_msg "mkthm";
    1.91       simplify (!LA_Data.ss_ref) (mk just) handle FalseE thm => thm end
    1.92  end;
    1.93