type qp.pl

%
%	SYNOPSIS: INTERVAL TEMPORAL LOGIC INTERPRETER
%   GPL(C) Mohsin Ahmed, http://www.cs.albany.edu/~mosh
%	Version for VAX/VMS Quintus Prolog		08 FEB 1988
%
%	References
%		1.Executing Temporal Logic Programs, Ben Moszkowski.
%		2.Programming In Prolog, Clocksin and Mellish.
%   Notes:
%		Quintus prolog comments are marked by the percent sign.

%	quintus prolog gives too many warnings.
:- no_style_check( all ).

%	quintus prolog errs on undefined procedures..
:- unknown( Old, fail ).

%	(Prec,Assoc,Operator )		 Operator Declaration

% ?- op( 1000, xfy , ',' ).	%	Causes problem with quintus
?- op( 970, xfy , &	 ).	%	Conjunction
?- op( 960, xfy , chp	 ).	%	Chop
?- op( 950, yf , cstar ).	%	Chop Star
?- op( 910, fy , process ).	%	Process
?- op( 900, xfy , exist ).	%	Existential Variables
?- op( 850, fy , @	 ).	%	Always
?- op( 850, fy , o	 ).	%	Next
?- op( 850, fy , wo	 ).	%	Weak Next
?- op( 810, xfy , +>	 ).	%	Implication, if
?- op( 810, xfy , <+>	 ).	%	Equivalence, iff
?- op( 800, fy , ~	 ).	%	Negation
?- op( 800, fy , display ).	%	Output
?- op( 800, fy , request ).	%	Input
?- op( 800, fy , stable ).	%	stable(e) == ( e gets e )
%					len(0)==empty
?- op( 800, fy , len	 ).	%	len(I) == o len( I - 1
?- op( 800, fy , fin	 ).	%	fin(W) == ( empty +> W )
?- op( 800, fy , halt	).	%	halt(W) == ( empty <+> W )
?- op( 800, fy , define ).	%	Function definitions
?- op( 750, xfy , gets	).	%	Gets
?- op( 750, xfy , get	 ).	%	Assignment across a state
?- op( 750, xfy , <+=	 ).	%	Temporal Assignment
% ?- op( 700, xfy , =	 ).	%	Assignment and Equality
% ?- op( 700, xfy , <	 ).	%	Less than, Integer Operands
% ?- op( 700, xfy , =<	 ).	%	Less than or equal
% ?- op( 700, xfy , >	 ).	%	Greater than
% ?- op( 700, xfy , >=	 ).	%	Greater than or equal
% ?- op( 500, yfx , +	 ).	%	Addition
% ?- op( 500, yfx , -	 ).	%	Substraction
% ?- op( 400, yfx , *	 ).	%	Multiplication,
% ?- op( 400, yfx , //	 ).	%	Division
% ?- op( 200, yfx , mod	 ).	%	Remainder

%
%	Symbolic Programming in Interval Temporal LOGic ,Print Eval Loop
%
spitlog :-
	write( '+---------------------+' ) , nl ,
	write( '| S P I T L O G - 2 1 |' ) , nl ,
	write( '+---------------------+' ) , nl ,
	itl_cleaner ,
	repeat ,
	write('-) ') ,
	read( W ) ,
	nl, write('>>-'), display(W), write('-<<'),nl,
	itl_main( W ) ,
	retract( itl_stop ) .


%
%	Evaluator of ITL programs
%

itl_main( Z ) :-
	assert( w( Z ) ) ,
	assert( time( 0 ) ) ,
	assert( irred( Z ) ) ,
	itl2 ,
	retractall( done(_) ) ,
	retractall( time( State ) ) ,
	retractall( w( Formula ) ) ,
	retractall( irred( Formula ) ) ,
	retractall( val( X , X_val , state ) ) ,
	retractall( val( X , X_val , next ) ) ,
	clean_error ,
	! .

%
%	Reduce Over States
%

itl2 :-
	repeat ,
	itl4 ,
	retract( itl2_over ) .

%
%	Execute One State
%

itl4 :-
	clear_done_cell ,
	show_time ,
	itl3 ,
	itl_tracing ,
	itl2_until ,
	next_time ,
	next_w ,
	retractall( val( X , X_val , state ) ) ,
	next_val ,
	! .

itl2_until :-
	itl_error( Message ) ,
	! ,
	assert( itl2_over ) .
itl2_until :-
	done( nil ) ,
	! ,
	assert( itl_error( done_not_set ) ) ,
	assert( itl2_over ) .
itl2_until :-
	done( true ) ,
	! ,
	assert( itl2_over ) .
itl2_until :-
	done( false ) ,
	! .

%
%	ReWrite until reduced
%

itl3 :-
	retract( w( W ) ) ,
	rw( W , V ) ,
	simple( V , Z ) ,
	assert( w( Z ) ) ,
	itl3_until( Z ) .

itl3_until( Z ) :-
	itl_error( Message ) ,
	! .
itl3_until( Z ) :-
	rd( Z ) ,
	! .
itl3_until( Z ) :-
	irrd( Z ) ,
	! .

%
%	Trace
%

itl_tracing :-
	itl_trace ,
	show_val ,
	w( W ) ,
	write( 'w = ' ) ,
	write( W ) ,
	nl ,
	! .
itl_tracing .

%
%	Error Message Display
%

clean_error :-
	retract( itl_error( Message ) ) ,
	write( 'Error : ' ) ,
	write( Message ) ,
	nl ,
	fail .
clean_error .

%
%	Time Display
%

show_time :-
	time( T ) ,
	write( 'state : ' ) ,
	write( T ) ,
	nl .

%
%	Display Variable Values
%

show_val :-
	val( X, X_val , Type ) ,
	write( X ) ,
	write( ' = ' ) ,
	write( X_val ) ,
	write( ' ' ) ,
	write( Type ) ,
	nl ,
	fail .
show_val .

%
%	Increment Time
%

next_time :-
	retract( time( T ) ) ,
	Next_T is T + 1 ,
	assert( time( Next_T ) ) .

%
%	Convert Program to Next State
%

next_w :-
	retract( w( A ) ) ,
	next_w( A , B ) ,
	assert( w( B ) ) .
next_w( ( wo A ) , A ) .
next_w( ( A & B ) , ( C & D ) ) :-
	next_w( A , C ) ,
	next_w( B , D ) .
next_w( Z , Z ) .

%
%	Future Values become the Present
%
next_val :-
	retract( val( X , X_val , next ) ) ,
	assert( val( X , X_val , state ) ) ,
	fail .
next_val .

%

clear_done_cell :-
	done(nil) ,
	! .
clear_done_cell :-
	retractall( done(_) ) ,
	assert( done(nil) ) ,
	! .

%

itl_op( arith , + ) .
itl_op( arith , - ) .
itl_op( arith , * ) .
itl_op( arith , // ) .
itl_op( arith , mod ) .
itl_op( boole , < ) .
itl_op( boole , =< ) .
itl_op( boole , > ) .
itl_op( boole , >= ) .

%

itl_var( Var ) :-
	not( atomic( Var ) ) ,
	! ,
	fail .
itl_var( true ) :-
	! ,
	fail .
itl_var( false ) :-
	! ,
	fail .
itl_var( more ) :-
	! ,
	fail .
itl_var( empty ) :-
	! ,
	fail .
itl_var( Z ) :-
	integer( Z ) ,
	! ,
	fail .
itl_var( Var ) .

%

itl_data( true ) :-
	! .
itl_data( false ) :-
	! .
itl_data( K ) :-
	integer( K ) ,
	! .
itl_data( [] ) :-
	! .
itl_data( [ A | B ] ) :-
	itl_data( A ) ,
	itl_data( B ) ,
	! .

%
%	To be before/after 'abort'
%
itl_cleaner :-
	retractall( define( Func , Para_count , N , Body ) ) ,
	retractall( done(_) ) ,
	retractall( irred( Formula ) ) ,
	retractall( itl_trace ) ,
	retractall( itl_error( Messages ) ) ,
	retractall( itl2_over ) ,
	retractall( sidey ) ,
	retractall( itl_stop ) ,
	retractall( time( State ) ) ,
	retractall( val( Var , Value , Var_type ) ) ,
	retractall( w( Formula ) ) .
%
%						 ReWrite Rules : rw(_,_)
%	ReWrite( Old_ITL_formula, New_ITL_formula ) :-
%	 conditions ,
%	 reduction of Old_ITL_formula to New_ITL_formula ,
%	 side_effects :
%	1. asserting present variable values, = as val(var,value,state),
%	2. asserting future variable values, gets as val(var,value,next),
%	3. end of interval : empty as done(true), more as done(false) .
%

rw( [] , [] ) :-
	! .

rw( L , L ) :-
	itl_data( L ) ,
	! .

rw( [ A | B ] , [ NA | NB ] ) :-
	rw( A , NA ) ,
	rw( B , NB ) ,
	! .

rw( X , X_val ) :-
	atomic( X ) ,
	get_val( X , X_val ) ,
	! .

%

rw( empty , true ) :-
	done( true ) ,
	! .
rw( empty , false ) :-
	done( false ) ,
	! .
rw( empty , true ) :-
	done( nil ) ,
	not( sidey ) ,
	retract( done( nil ) ) ,
	assert( done( true ) ) ,
	! .

%

rw( more , true ) :-
	done( false ) ,
	! .
rw( more , false ) :-
	done( true ) ,
	! .
rw( more , true ) :-
	done( nil ) ,
	not( sidey ) ,
	retract( done( nil ) ) ,
	assert( done( false ) ) ,
	! .

%

rw( skip , wo empty ) :-
	done( false ) ,
	! .
rw( skip , false ) :-
	done( true ) ,
	! .
rw( skip , ( more & ( wo empty ) ) ) :-
	! .

%

rw( abort , true ) :-
	assert( itl_error( abort ) ) ,
	! .

%
%	Meta Commands to Interpreter
%

%	Comments must be double quoted strings: comment("Yes Please")
rw( comment( C ) , wo comment( C ) ) :-
	! .

rw( static( I = A ) , Z ) :-
	val( I , B , static ) ,
	! ,
	rw_prolog( A = B , Z ) .
rw( static( I = V ) , true ) :-
	itl_var( I ) ,
	itl_data( V ) ,
	not( sidey ) ,
	! ,
	asserta( val( I , V , static ) ) .
rw( static( I = V ) , false ) :-
	sidey ,
	! .
rw( static( I = V ) , false ) :-
	assert( itl_error( static( I = V ) ) ) ,
	! .

rw( nostatic( I ) , true ) :-
	not( sidey ) ,
	retractall( val( I , _ , static ) ) ,
	! .
rw( nostatic( I ) , false ) :-
	sidey ,
	! .

rw( help , true ) :-
	write('Call Mosh @ 201-482-3075') ,
	nl ,
	! .

rw( file( F ) , FW ) :-
	see( F ) ,
	read( FW ) ,
	seen.

rw( stop , true ) :-
	itl_stop ,
	! .
rw( stop , true ) :-
	not( sidey ) ,
	assert( itl_stop ) ,
	! .

rw( trace_itl , true ) :-
	itl_trace ,
	! .
rw( trace_itl , true ) :-
	not( sidey ) ,
	assert( itl_trace ) ,
	! .
rw( notrace_itl , true ) :-
	not( sidey ) ,
	retractall( itl_trace ) ,
	! .

rw( trace , true ) :-
	not( sidey ) ,
	trace ,
	! .
rw( notrace , true ) :-
	not( sidey ) ,
	notrace ,
	! .
rw( spy( F ) , true ) :-
	not( sidey ) ,
	spy( F ) ,
	! .
rw( nospy( F ) , true ) :-
	not( sidey ) ,
	nospy( F ) ,
	! .

%

rw( nl , true ) :-
	nl ,
	!.

%

rw( ~ true , false ) :-
	! .
rw( ~ false , true ) :-
	! .
rw( ~ empty , more ) :-
	! .
rw( ~ more , empty ) :-
	! .
rw( ~ ~ W , New_W	) :-
	rw( W , New_W ) ,
	! .

%	Can you see why ~ A should free of side_effects ?

rw( ~ A , ~ F ) :-
	assert( sidey ) ,
	rw( A , C ) ,
	rw( A , C , F ) ,
	retract( sidey ) ,
	! .

%

rw( ifelse( true , A , B ) , A ) :-
	! .
rw( ifelse( false , A , B ) , B ) :-
	! .
rw( ifelse( ~ C , A , B ) , ifelse( C , B , A ) ) :-
	! .
rw( ifelse( C , A , B ) , Z ) :-
	assert( sidey ) ,
	rw( ~ ~ C , C , R ) ,
	retract( sidey ) ,
	rw_ifelse( R , A , B , Z ) ,
	! .

rw_ifelse( true , A , _ , A ) :-
	! .
rw_ifelse( false , _ , B , B ) :-
	! .

%

rw( if( C , A ) , ( C +> A ) ) :-
	! .

rw( true +> W , New_W ) :-
	rw( W , New_W ) ,
	! .
rw( false +> W , true ) :-
	! .
rw( W +> true , true ) :-
	! .
rw( C +> A , E +> A ) :-
	assert( sidey ) ,
	rw( ~ ~ C , C , E ) ,
	retract( sidey ) ,
	! .

%

rw( iff( A , B ) , A <+> B ) :-
	! .
rw( A <+> A , true ) :-
	! .
rw( true <+> B , New_B ) :-
	rw( B , New_B ) ,
	! .
rw( B <+> true , New_B ) :-
	rw( B , New_B ) ,
	! .
rw( false <+> B , ~ B ) :-
	! .
rw( B <+> false , ~ B ) :-
	! .
rw( A <+> B , G <+> H ) :-
	assert( sidey ) ,
	rw( A , C ) ,
	rw( A , C , G ) ,
	rw( B , D ) ,
	rw( B , D , H ) ,
	retract( sidey ) ,
	! .

%

rw( ( wo W ) , ( wo W ) ) :-
	! .

%

rw( ( @ W ) , ( New_W & wo( @ W ) ) ) :-
	rw( W , New_W ) ,
	! .

%

rw( ( o W ) , ( wo W ) ) :-
	done( false ) ,
	! .
rw( ( o W ) , false ) :-
	done( true ) ,
	! .
rw( ( o W ) , ( more & wo( W ) ) ) :-
	! .

%

rw( ( false & W ) , false ) :-
	! .
rw( ( W & false ) , false ):-
	! .
rw( ( W & true ) , New_W ) :-
	rw( W , New_W ) ,
	! .
rw( ( true & W ) , New_W ) :-
	rw( W , New_W ) ,
	! .
rw( ( A & B ) , ( C & D ) ) :-
	rw( A , C ) ,
	rw( B , D ) ,
	! .
rw( len(0) , empty ) :-
	! .
rw( len(K) , ( more & ( wo len(J) ) ) ) :-
	integer( K ) ,
	J is K - 1 ,
	! .
rw( len(E) , len( K ) ) :-
	rw( E , K ) ,
	! .

%

rw( halt( W ) , W ) :-
	done( true ) ,
	! .
rw( halt( W ) , ( ~(W) & wo( halt W ) ) ) :-
	done( false ) ,
	! .

rw( halt( W ) , empty ) :-
	assert( sidey ) ,
	rw( W , B ) ,
	rw( W , B , C ) ,
	retract( sidey ) ,
	C = true ,
	! .
rw( halt( W ) , ( more & ( wo( halt W ) ) ) ) :-
	assert( sidey ) ,
	rw( W , B ) ,
	rw( W , B , C ) ,
	retract( sidey ) ,
	C = false ,
	! .

%
%	Dynamic Function Definition :
%	example : define( add, lamda(a,b), a+b )
%		 undefine( add )
%		 define( next, lamda(z), o(z) )
%

rw( define( Func_name , L , Body ) , true ) :-
	functor( L , lamda , Para_count ) ,
	! ,
	L =.. [ lamda | Dummy_para_list ] ,
	assert( define( Func_name , Dummy_para_list , Para_count , Body ) ) .

rw( define( F , L , B ) , false ) :-
	assert( itl_error( define( F , L , B ) ) ) .

rw( undefine( F ) , true ) :-
	retractall( define( F , _ , _ , _ ) ) .


%

rw( fin( W ) , New_W ) :-
	done( true ) ,
	rw( W , New_W ) ,
	! .
rw( fin( W ) , wo( fin( W ) ) ) :-
	done( false ) ,
	! .

%

rw( stable( K ) , true ) :-
	itl_data( K ) ,
	! .
rw( stable( K ) , false ) :-
	not( atomic( K ) ) ,
	assert( itl_error( stable( K ) ) ) ,
	! .
rw( stable( K ) , K gets K ) :-
	! .

%

rw( display( E ) , true ) :-
	itl_data( E ) ,
	write( E ) ,
	nl ,
	! .
rw( display( E ) , display( H ) ) :-
	rw( E , H ) ,
	! .

%

rw( request( E ) , E = H ) :-
	write( E ) ,
	write( ' = ' ) ,
	read( H ) ,
	! .

%

rw( ( A chp B ) , chop( A , B , done( nil ) ) ) :-
	! .
rw( chop( false , _ , _ ) , false ) :-
	! .
rw( chop( A , B , done( true ) ) , B ) :-
	rd( A ) ,
	! .
rw( chop( A , B , done( false ) ) ,
	more & wo( chop( C , B , done( nil ) ) ) ) :-
	rd( A ) ,
	next_w( A , C ) ,
	! .
rw( chop( A , B , done( nil ) ) , false ) :-
	rd( A ) ,
	assert( itl_error( done_not_set( A chp B ) ) ) ,
	! .
rw( chop( A , B , done( D1 ) ) , chop( C , B , done( D2 ) ) ) :-
	! ,
	retract( done( Old ) ) ,
	assert( done( D1 ) ) ,
	rw( A , C ) ,
	retract( done( D2 ) ) ,
	assert( done( Old ) ) ,
	! .

%

rw( process( W ) , process( W , done( nil ) ) ) :-
	! .
rw( process( W , done( true ) ) , true ) :-
	rd( W ) ,
	! .
rw( process( W , done( false ) ) , wo( process( X , done( nil ) ) ) ) :-
	rd( W ) ,
	! ,
	next_w( W , X ) .
rw( process( W , done( nil ) ) , false ) :-
	rd( W ) ,
	! ,
	assert( itl_error( done_not_set( process( W ) ) ) ) .
rw( process( W , done( D ) ) , process( X , done( ND ) ) ) :-
	retract( done( Old ) ) ,
	! ,
	assert( done( D ) ) ,
	rw( W , X ) ,
	retract( done( ND ) ) ,
	assert( done( Old ) ) .

%

rw( ( W cstar ) , true ) :-
	done( true ) ,
	! .
rw( ( W cstar ) , ( W chp ( W cstar ) ) ) :-
	done( false ) ,
	! .

%

rw( A <+= B , false ) :-
	not( itl_var( A ) ) ,
	assert( itl_error( A <+= B ) ) ,
	! .
rw( A <+= B , fin( A = B ) ) :-
	itl_data( B ) ,
	! .
rw( A <+= B , A <+= C ) :-
	rw( B , C ) ,
	! .

%

rw( A gets B , true ) :-
	done( true ) ,
	! .

rw( A gets B , ( A get B ) & wo( A gets B ) ) :-
	done( false ) ,
	! .

%

rw( A get B , false ) :-
	not( itl_var( A ) ) ,
	assert( itl_error( A get B ) ) ,
	! .
rw( A get B , false ) :-
	done( true ) ,
	assert( itl_error( (A get B) & empty ) ) ,
	! .
rw( A get B , more & ( A get B ) ) :-
	done( nil ) ,
	! .

%	done( false )
rw( A get B , true ) :-
	itl_data( B ) ,
	get_val( A , B , next ) ,
	! .
rw( A get B , false ) :-
	itl_data( B ) ,
	get_val( A , C , next ) ,
	\+((B = C)) ,
	! .
rw( A get B , true ) :-
	itl_data( B ) ,
	set_val( A , B , next ) ,
	! .
rw( A get B , A get C ) :-
	rw( B , C ) ,
	! .

%

rw( A = A , true ) :-
	! .
rw( A = B , false ) :-
	itl_data( A ) ,
	itl_data( B ) ,
	\+((A = B)) ,
	! .

rw( A = B , New_A = B ) :-
	listp( A ) ,
	not( itl_data( A ) ) ,
	rw( A , New_A ) ,
	! .
rw( A = B , A = New_B ) :-
	listp( B ) ,
	not( itl_data( B ) ) ,
	rw( B , New_B ) ,
	! .

%	Here not both A, B are data
rw( A = B , New_A = B ) :-
	not( atomic( A ) ) ,
	not(listp( A ) ) ,
	rw( A , New_A ) ,
	! .
rw( A = B , A = New_B ) :-
	not( atomic( B ) ) ,
	not( listp( B ) ) ,
	rw( B , New_B ) ,
	! .

listp( [] ) .
listp( [_|_] ).
%	Here the possibilities are :
%	var = data, var = var, data = var
rw( A = B , Z ) :-
	get_val( A , VA ) ,
	rw( A = B , VA = B , Z ) ,
	! .
rw( A = B , Z ) :-
	get_val( B , VB ) ,
	rw( A = B , A = VB , Z ) ,
	! .
rw( B = A , true ) :-
	not( sidey ) ,
	itl_var( A ) ,
	itl_data( B ) ,
	set_val( A , B ) ,
	! .
rw( A = B , true ) :-
	not( sidey ) ,
	itl_var( A ) ,
	itl_data( B ) ,
	set_val( A , B ) ,
	! .

%
%	Arithmetic Simplification
rw( 0 + A , A ) :-
	! .
rw( A + 0 , A ) :-
	! .
rw( A - 0 , A ) :-
	! .

rw( 0 * _ , 0 ) :-
	! .
rw( _ * 0 , 0 ) :-
	! .
rw( 1 * A , A ) :-
	! .
rw( 1 * A , A ) :-
	! .

rw( A // 0 , false ) :-
	assert( itl_error( zero_divide( A // 0 ) ) ) ,
	! .
rw( A // 1 , A ) :-
	! .
rw( A // A , 1 ) :-
	! .

rw( A mod 0 , false ) :-
	assert( itl_error( zero_divide( A mod 0 ) ) ) ,
	! .
rw( A mod A , 1 ) :-
	! .
rw( A mod 1 , A ) :-
	! .

%
%	Arith Operators [+,-,*,//,mod]
rw( E , H ) :-
	not( atomic( E ) ) ,
	E =.. [ Op , L , R ] ,
	itl_op( arith , Op ) ,
	integer( L ) ,
	integer( R ) ,
	% Prolog-86  needs no call.
	call( H is E ),
	! .

rw( E , E2 ) :-
	not( atomic( E ) ) ,
	E =.. [ Op , L , R ] ,
	itl_op( arith , Op ) ,
	rw( L , L1 ) ,
	rw( R , R1 ) ,
	E1 =.. [ Op , L1 , R1 ] ,
	rw( E , E1 , E2 ) ,
	! .

%
%	Comparison Operators [>,>=,<,=<]
rw( E , H ) :-
	not( atomic( E ) ) ,
	E =.. [ Op , L , R ] ,
	itl_op( boole , Op ) ,
	integer( L ) ,
	integer( R ) ,
	rw_prolog( E , H ) ,
	! .

rw( E , E2 ) :-
	not( atomic( E ) ) ,
	E =.. [ Op , L , R ] ,
	itl_op( boole , Op ) ,
	assert( sidey ) ,
	rw( L , L1 ) ,
	rw( L , L1 , L2 ) ,
	rw( R , R1 ) ,
	rw( R , R1 , R2 ) ,
	retract( sidey ) ,
	E1 =.. [ Op , L2 , R2 ] ,
	rw( E , E1 , E2 ) ,
	! .

%
%	Some Goals need to rewritten immediately like those who are not
%	permitted to cause side effects, Using tail recursion.
%	rw( Old_w , Old_w_after_one_rw , New_w ) keeps rewriting w until
%	Old_w = Old_w_after_one_rw , that is there no change any longer.
%	rw( w , w after one rw , completely rw w )
%

rw( E , H , J ) :-
	\+((E = H )),
	! ,
	rw( H , K ) ,
	rw( H , K , J ) .
rw( E , H , H ) :-
	! .

%
%	Execute E as a Prolog Goal
rw_prolog( E , true ) :-
	call( E ) ,
	! .
rw_prolog( E , false ) .

%

rw( ( I exist W ) , env( W , [ I ] , [ nil ] , [ nil ] ) ) :-
	! .

%

rw( FA , FB ) :-
	functor( FA , Func , N ) ,
	define( Func , Dum , N , Body ) ,
	! ,
	FA =.. [ Func | Para ] ,
	rw_func( Func , Dum , Para , Body , FB ).

rw_func( _ , Dum , Para , Body , FB ) :-
	itl_data( Para ) ,
	! ,
	make_nil( Para , U ) ,
	FB = env( Body , Dum , Para , U ) .

rw_func( Func , _ , Para , _ , FB ) :-
	! ,
	rw( ~ ~ Para , Para , Para1 ) ,
	FB =.. [ Func | Para1 ] .

%

rw( env( D , _ , _ , _ ) , D ) :-
	itl_data( D ) ,
	! .

rw( env( W , Dum , Para , Next ) , wo( env( X , Dum , Next , U ) ) ) :-
	rd( W ) ,
	! ,
	next_w( W , X ) ,
	make_nil( Dum , U ) .

rw( env( W , Dum , Para , Next ) , env( X , Dum , Para1 , Next1 ) ) :-
	make_env( Dum , Para , Next ) ,
	rw( ~ ~ W , W , X ) ,
	get_env( Dum , Para1 , Next1 ) ,
	! .

%
%	Catch All for ReWrite Rules
rw( A , A ) .

%
%								Irreducible : ir
rd(_)
%	Irreducible( W ) :- Old_W = New_W, Succeeds only if W is Irreducible
%

irrd( W ) :-
	retract( irred( W ) ) ,
	assert( itl_error( irreducible( W ) ) ) ,
	! .
irrd( New ) :-
	retract( irred( Old ) ) ,
	assert( irred( New ) ) ,
	! ,
	fail .

%
%						 Reduced : rd(_)
%	ReDuced( Formula ) :-
%	 present state is completely evaluated ,
%

rd( true ) :-
	! .
rd( wo(_) ) :-
	! .

rd( W & V ) :-
	rd( W ) ,
	rd( V ) ,
	! .

%

simple( true , wo true ) :-
	! .
simple( false , false ) :-
	! ,
	assert( itl_error( false ) ) .

simple( trace , true ) :-
	! ,
	trace .
simple( notrace , true ) :-
	! ,
	notrace .
simple( abort , true ) :-
	! ,
	itl_cleaner ,
	abort .

simple( process( W , done( D ) ) , Z ) :-
	retract( done(_) ) ,
	assert( done( D ) ) ,
	simple( W , Z ) ,
	! .

simple( X , Y ) :-
	simplify( X , Y ) .

%

simplify( ( true & W ) , W ) :-
	! .
simplify( ( W & true ) , W ) :-
	! .
simplify( ( W & false ) , false ) :-
	! .
simplify( ( false & W ) , false ) :-
	! .
simplify( ( A & B ) , ( SA & SB ) ) :-
	! ,
	simplify( A , SA ) ,
	simplify( B , SB ) .
simplify( A , A ) .

%

set_val( A , V ) :-
	val( A , Z , state ) ,
	Z = nil ,
	! ,
	retract( val( A , nil , state ) ) ,
	asserta( val( A , V	 , state ) ) .
set_val( A , V ) :-
	val( A , Z , state ) ,
	! ,
	V = Z .
set_val( A , V ) :-
	asserta( val( A , V	 , state ) ) ,
	! .

set_val( A , V , next ) :-
	val( A , Z , next ) ,
	Z = nil ,
	! ,
	retract( val( A , nil , next ) ) ,
	asserta( val( A , V	 , next ) ) .
set_val( A , V , next ) :-
	val( A , Z , next ) ,
	! ,
	V = Z .
set_val( A , V , next ) :-
	asserta( val( A , V , next ) ) ,
	! .

%

get_val( A , V ) :-
	val( A , Z , state ) ,
	Z = nil ,
	! ,
	fail .
get_val( A , V ) :-
	val( A , V , state ) ,
	! .
get_val( A , V ) :-
	val( A , V , static ) ,
	! .

get_val( A , V , next ) :-
	val( A , Z , next ) ,
	Z = nil ,
	! ,
	fail .
get_val( A , V , next ) :-
	val( A , V , next ) ,
	! .


%

make_env( [] , [] , [] ) :-
	! .
make_env( [ A | B ] , [ C | D ] , [ E | F ] ) :-
	asserta( val( A , C , state ) ) ,
	asserta( val( A , E , next ) ) ,
	make_env( B , D , F ) ,
	! .

%

get_env( [] , [] , [] ) :-
	! .
get_env( [ A | B ] , [ C | D ] , [ E | F ] ) :-
	retract( val( A , C , state ) ) ,
	retract( val( A , E , next ) ) ,
	get_env( B , D , F ) ,
	! .

%

make_nil( [] , [] ) :-
	! .
make_nil( [ A | B ] , [ nil | UB ] ) :-
	make_nil( B , UB ) ,
	! .

%	Ported to quintus prolog
retractall( Term ) :-
	retract( Term ) ,
	fail .
retractall( Term ) .

not( T ) :-
	! ,
	\+( ( T ) ) .

%	Important Note 1.
%	Please remember Temporal Logic is Causal, for example
%	'o i = j' means 'i get j', but what about 'i = o j' does it
%	mean 'j get i' ???
%	Important Note 2.
%	The chop operator is commutative, so here i chose to parse it
%	right to left. This parse is more intutive and consistent.
%	Example:(U chp V chp W) parses as U chp (V chp W) and rewritten as
%	chop( U, (V chp W), done_cell_for_U(nil)).
%	Important Note 3.
%	The '=' operator has dual functions : both as the assignment
%	and as a comparison operator. It is only a comparator, when it
%	appears as a condition in '+>' .
%	1 Example: (i = 2) & (i = 3) is interpreted as
%		 assign 2 to i, and is i equal to 3 ?
%	It seems '&' is noncommutative but a little reflection will show
%	that the final boolean value is always the same.
%	2 Example: (i = 2 ) +> W , here the '=' is always assumed
%	to be a comparator.
%	Important Note 4.
%	The conditional of 'if' '+>' is not allowed to have side effects
%	in the temporal program environment, the global flag 'sidey'
%	indicates such environment.
%	1 Example: more +> W, will not set the 'done' cell.
%		i=2 +> W, will not set 'i' to the value 2.
%	Important Note 5.
%	x exist (x = 1) & x = 2 is true.
%	'i exist y' is read as there exist i such that y '.

$