src/HOL/Tools/refute.ML
changeset 14984 edbc81e60809
parent 14965 7155b319eafa
child 15125 5224130bc0d6
     1.1 --- a/src/HOL/Tools/refute.ML	Mon Jun 21 16:39:18 2004 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Mon Jun 21 16:39:39 2004 +0200
     1.3 @@ -59,9 +59,6 @@
     1.4  structure Refute : REFUTE =
     1.5  struct
     1.6  
     1.7 -	(* FIXME compatibility -- should avoid std_output altogether *)
     1.8 -	val std_output = Output.std_output o Output.output;
     1.9 -
    1.10  	open PropLogic;
    1.11  
    1.12  	(* We use 'REFUTE' only for internal error conditions that should    *)
    1.13 @@ -408,7 +405,7 @@
    1.14  
    1.15  	fun collect_axioms thy t =
    1.16  	let
    1.17 -		val _ = std_output "Adding axioms..."
    1.18 +		val _ = immediate_output "Adding axioms..."
    1.19  		(* (string * Term.term) list *)
    1.20  		val axioms = flat (map (Symtab.dest o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy))
    1.21  		(* given a constant 's' of type 'T', which is a subterm of 't', where  *)
    1.22 @@ -506,15 +503,15 @@
    1.23  								(* collect relevant type axioms for the argument types *)
    1.24  								foldl collect_type_axioms (axs, Ts)
    1.25  							else
    1.26 -								(std_output (" " ^ axname);
    1.27 +								(immediate_output (" " ^ axname);
    1.28  								collect_term_axioms (ax :: axs, ax))
    1.29  						| None =>
    1.30  							(* at least collect relevant type axioms for the argument types *)
    1.31  							foldl collect_type_axioms (axs, Ts))
    1.32  				end
    1.33  			(* TODO: include sort axioms *)
    1.34 -			| TFree (_, sorts)       => ((*if not (null sorts) then std_output " *ignoring sorts*" else ();*) axs)
    1.35 -			| TVar  (_, sorts)       => ((*if not (null sorts) then std_output " *ignoring sorts*" else ();*) axs)
    1.36 +			| TFree (_, sorts)       => ((*if not (null sorts) then immediate_output " *ignoring sorts*" else ();*) axs)
    1.37 +			| TVar  (_, sorts)       => ((*if not (null sorts) then immediate_output " *ignoring sorts*" else ();*) axs)
    1.38  		(* Term.term list * Term.term -> Term.term list *)
    1.39  		and collect_term_axioms (axs, t) =
    1.40  			case t of
    1.41 @@ -535,7 +532,7 @@
    1.42  					if mem_term (ax, axs) then
    1.43  						collect_type_axioms (axs, T)
    1.44  					else
    1.45 -						(std_output " HOL.the_eq_trivial";
    1.46 +						(immediate_output " HOL.the_eq_trivial";
    1.47  						collect_term_axioms (ax :: axs, ax))
    1.48  				end
    1.49  			| Const ("Hilbert_Choice.Eps", T) =>
    1.50 @@ -545,7 +542,7 @@
    1.51  					if mem_term (ax, axs) then
    1.52  						collect_type_axioms (axs, T)
    1.53  					else
    1.54 -						(std_output " Hilbert_Choice.someI";
    1.55 +						(immediate_output " Hilbert_Choice.someI";
    1.56  						collect_term_axioms (ax :: axs, ax))
    1.57  				end
    1.58  			| Const ("All", _) $ t1           => collect_term_axioms (axs, t1)
    1.59 @@ -638,7 +635,7 @@
    1.60  								(* collect relevant type axioms *)
    1.61  								collect_type_axioms (axs, T)
    1.62  							else
    1.63 -								(std_output (" " ^ axname);
    1.64 +								(immediate_output (" " ^ axname);
    1.65  								collect_term_axioms (ax :: axs, ax))
    1.66  						| None =>
    1.67  							(* collect relevant type axioms *)
    1.68 @@ -888,7 +885,7 @@
    1.69  			(let
    1.70  				val init_model             = (universe, [])
    1.71  				val init_args              = {maxvars = maxvars, next_idx = 1, bounds = [], wellformed = True}
    1.72 -				val _                      = std_output ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
    1.73 +				val _                      = immediate_output ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
    1.74  				(* translate 't' and all axioms *)
    1.75  				val ((model, args), intrs) = foldl_map (fn ((m, a), t') =>
    1.76  					let
    1.77 @@ -902,12 +899,12 @@
    1.78  				val fm_ax = PropLogic.all (map toTrue (tl intrs))
    1.79  				val fm    = PropLogic.all [#wellformed args, fm_ax, fm_t]
    1.80  			in
    1.81 -				std_output " invoking SAT solver...";
    1.82 +				immediate_output " invoking SAT solver...";
    1.83  				(case SatSolver.invoke_solver satsolver fm of
    1.84  				  SatSolver.SATISFIABLE assignment =>
    1.85  					writeln ("\n*** Model found: ***\n" ^ print_model thy model (fn i => case assignment i of Some b => b | None => true))
    1.86  				| _ =>  (* SatSolver.UNSATISFIABLE, SatSolver.UNKNOWN *)
    1.87 -					(std_output " no model found.\n";
    1.88 +					(immediate_output " no model found.\n";
    1.89  					case next_universe universe sizes minsize maxsize of
    1.90  					  Some universe' => find_model_loop universe'
    1.91  					| None           => writeln "Search terminated, no larger universe within the given limits."))