/*

  SIMPLIFY

copyright  P. H. Roosen-Runge, October 1992, 1997
%=====================================================
%      1.3.1 July 8: expects rules to be loaded from theory files
%                rather than the file simplification rules.
%                Rules can be asserted interactively.
%      1.4   Nov. 30, 1997: rename any Prolog variables in result
%      1.4.2SWI   January 6, 2007: SWI Prolog version
%=====================================================
  The program 'simplify' uses the predicate simplify/2 found in 
  /cs/fac/src/SVT-lib/simp.pl to simplify terms read from the standard input, 
  using simplification rules loaded from theory modules such arithmetic.simp.

  theory files are loaded by including 
      theory('<file specification>').
  in the  input data.

*/

% :- no_style_check(single_var). 
% not in SWI. Use style_check(-singleton) if needed.

:- fileerrors(_, off).
:- multifile '->>'/2.
:- dynamic '->>'/2.      % so rules can be asserted interactively.

% use .plrc for paths.
:- ensure_loaded(lib('simp.pl')).  % simplify/2 and canonical/2

% user_error_handler(_,_,_,_) :-  error('!! Something wrong.').
% error(X) :- write('!! '), write(X), nl. 

activate :- 
 write('Version 1.4.2SWI, January 6, 2007')
     , nl,
       simplifyTerms
     ;
     nl, write('!! Something wrong.'), nl, halt.

simplifyTerms :- read(T),
	  (T==end_of_file, halt
  	;
	   (T = theory(File) -> theory(File)
           ;
            T = assert((Rule)) -> addRule((Rule))
	   ;
	    simplify(T, Result), 
	    copy_term(T ->> Result, Pretty),
            numbervars(Pretty, 0, _),    Pretty = (PT ->> PR),
            nl, write(PT), write(' ->> '),
            nl, write('   '), write(PR), nl
	   ),
	   simplifyTerms, nl
	  ).

