
% Verification Generator for Simple Imperative Programs
%
% by Bharat Jayaraman (VC Generation)
% State Univ of New York at Buffalo
% and
% M.K. Jinesh (Web Interface)
% Amrita University

:- op(550, xfx, '@').
:- op(650, xfy, '::').
:- op(650, xfx, '~>').
:- op(600, yfx, '&&').
:- op(620, yfx, '||').
:- op(650, xfx, '<=>').
:- op(650, xfx, '==>').

:- op(650, xfx, '=<').
:- op(650, xfx, '>=').
:- op(650, xfx, '!=').
:- op(650, xfx, '==').
:- op(650, xfx, '>').
:- op(650, xfx, '<').

:- dynamic array_type/2.
:- dynamic logic_vars/1.
:- dynamic context/1.

%  Web Interface

:- use_module(library(http/thread_httpd)).
:- use_module(library(http/http_dispatch)).
:- use_module(library(http/http_header)).
:- use_module(library(http/http_multipart_plugin)).
:- use_module(library(http/http_client)).
:- use_module(library(http/html_write)).
:- use_module(library(option)).
:- use_module(library(http/http_parameters)).
:- use_module(library(memfile)).
:- public save_file/3.
:- http_handler(root(.),	get_gui, []).
:- http_handler(root(upload),	upload,      []).
:- http_handler(root(verify),	 call_verify,      []).

%  swipl -O --goal=start_server --stand_alone=true -o vcgen -c vcgen.pl

go :-
          current_prolog_flag(argv, Argv),
          (length(Argv,2)
	     ->
		      nth0(1,Argv,File), verify(File)
	     ;
		      write("File missing"),halt
	  ).

start_server :- server(8080).

server(Port) :-
        http_server(http_dispatch, [port(Port)]).

get_gui(_Request) :-  get_template(X),
	format('Content-type: text/html~n~n'),
	format(X, [' ',' ']).

upload(Request) :-
                      multipart_post_request(Request), !,
                      http_read_data(Request, [file=Data], []),
                     get_template(X),
                     format('Content-type: text/html~n~n'),
                    format(X, [Data,' ']).
upload(_Request) :-
	throw(http_reply(bad_request(bad_file_upload))).

call_verify(Request) :-
    member(method(post), Request), !,
      http_read_data(Request,
                        [content=Data],[]),
     tmp_file('txt',Name),
       tell(Name), verify_data(Data),
       told,
          open(Name,read,Stream1),
      read_string(Stream1,_,Output), close(Stream1),
      get_template(X),
format('Content-type: text/html~n~n'),
format(X, [Data,Output]).


multipart_post_request(Request) :-
	memberchk(method(post), Request),
	memberchk(content_type(ContentType), Request),
	http_parse_header_value(
    content_type, ContentType,
    media(multipart/'form-data', _)).

save_file(In, file(FileName, File), Options) :-
   option(filename(FileName), Options),
   setup_call_cleanup(
   tmp_file_stream(octet, File, Out),
   copy_stream_data(In, Out),
   close(Out)).

get_template(X) :-
	open('index1.html','read', Stream),
      read_string(Stream,_,X),
	 close(Stream).


%:- dynamic counter_u/1, counter_e/1.
%
%
% set counters for quantifier variables to 0
%
%:- assert(counter_u(0)).
%:- assert(counter_e(0)).


% _______ TOP-LEVEL DRIVER __________________________

verify(File) :-
        retractall(array_type(_,_)),
        retractall(logic_vars(_)),
        retractall(context(_)),
        nl,
        write('(* Verification Conditions for Alt-Ergo *)'), nl,nl,
	open(File,read,Stream),
	lex(Stream,Tokens),
	parse(Tokens,Triple),
	prove(Triple),
	close(Stream),
        !.

verify(_) :-
           write('...'), nl, nl,
           write('Syntax error occurred near '),
           get_context([C|L]), write(C), write('. '),
           (L \== []
              ->  write('Full context of error:'), nl,nl,
                  reverse([C|L], Rev), write(Rev)
              ;  true
           ),
           !,
           write('\n\nNote VC-Gen and Alt-Ergo syntax differences:'), nl,nl,
           write('VC-Gen: function, all, &&, ||, =<, <=>, ==>'), nl,
           write('Alt-Ergo: logic, forall, and, or, <=, <->, ->'), nl.

verify_data(Data) :-
        retractall(array_type(_,_)),
        retractall(logic_vars(_)),
        retractall(context(_)),
        nl,
        write('(* Verification Conditions for Alt-Ergo *)'), nl,nl,
        retractall(array_type/2),
        open_string(Data,Stream),
        lex(Stream,Tokens),
	parse(Tokens,Triple),
	prove(Triple),
	close(Stream),
        !.

verify_data(_) :-
           write('...'), nl, nl,
           write('Syntax error occurred near '),
           get_context([C|L]), write(C),  write('.  '),
           (L \== []
              ->  write('Full context of error:'), nl,nl,
                  reverse([C|L], Rev), write(Rev)
              ;  true
           ),
           !,
           write('\n\nNote VC-Gen and Alt-Ergo syntax differences:'), nl,nl,
           write('VC-Gen: &&, ||, =<, <=>, ==>, all, function'), nl,
           write('Alt-Ergo: and, or, <=, <->, ->, forall, logic'), nl.


get_context(LC) :-
            findall(C,context(C),L),
            longest_context(L, LC).

longest_context([[C]], [C]).
longest_context([C1|L], LC) :-
            L \== [],
            length(C1,N),
            get_max_length(L, N, C1, LC).

get_max_length([],_,C,C).
get_max_length([Last],N,C,LC) :- !,
             length(Last,M),
             (M > N -> LC = Last ; LC = C).
get_max_length([Next|L],N,C,LC) :-
             length(Next,M),
             (M > N ->
                 get_max_length(L,M,Next,LC)
             ;  get_max_length(L,N,C,LC)
             ).

write_list([H]) :- write(H), !.
write_list([H|T]) :- write(H), nl, write_list(T).

% ______________________PROVER____________________________


prove(triple(Pre,Stmt,Post)) :-

        (prove(Pre,Stmt,Post)
          -> nl
          ;  nl, write('VC generation failed.')
        ), nl, nl.

prove(Pre,Stmt,Post) :-
	wp(WP,Stmt,Post,Post,false), !,
	theorem(start,(Pre ==> WP)).


% ________ THE WP PREDICATE: WEAKEST PRECONDITIONS _______

wp(Break, break, _, Break, _).

wp(Continue, continue, _, _, Continue).

wp(Pre, (X = Expr), Post, _, _) :-
	subst(Post, X, Expr, Pre).

wp(Pre,	(S ; REST), Post, Break, Continue) :-
	wp(Inter, REST, Post, Break, Continue),
	wp(Pre, S, Inter, Break, Continue).

wp(((X ==> TR) && (not(X) ==> Post)), if(X, Y), Post, Break, Continue) :-
	wp(TR, Y, Post, Break, Continue).

wp((((X ==> TR) && (not(X) ==> FA))), if(X, Y, Z), Post, Break, Continue) :-
	wp(TR, Y, Post, Break, Continue),
	wp(FA, Z, Post, Break, Continue).

wp(I, loop(I, B, S), Post, _, _) :-
	wp(Q, S, I, Post, I), !,
	theorem(intra,((B && I) ==> Q)),
	theorem(exit,((not(B) && I) ==> Post)).

wp((B ==> Post), assert(B), Post, _, _).

% _______________

theorem(Code,T) :- nl, %  write('Is the following true? '),
	      theorem2(Code),
              array_quantifiers,
	      nl,
	      pprin(T,0), !,
	      nl.
	      % write('Enter true./false.: '), read(Inp),
	      % Inp == true.

theorem2(intra):- write('goal intra_loop:').
theorem2(exit) :- write('goal exit:').
theorem2(start):- write('goal start:').

array_quantifiers :-
              array_type(T, L),   % dynamic predicate
              write_array_quants(T, L).
array_quantifiers.

write_array_quants(_, []).
write_array_quants(T, [A|Rest]) :-
              nl, write('forall '), write(A), write(' : '),
              write(T), write(' '),  write(farray), write('.'), nl,
              write_array_quants(T, Rest).



% __________ SUBSTITUTION:  P[V <- E] = Q ___________________

subst(V,V,E,E) :- !.
subst(P,V,E,Q) :-
	P =.. [Op|L],
	!,
	subst_list(L,V,E,L2),
	Q2 =.. [Op|L2],
        simplify(Q2,Q).
subst(A,_,_,A).

subst_list([],_,_,[]).
subst_list([H|T],V,E,[H2|T2]) :-
	subst(H,V,E,H2),
	subst_list(T,V,E,T2).


%___________________ PRETTY PRINTING ____________________

pprin((A && B), N) :-  !,
	simplify(A,A2),  pprin(A2,N),  write(' and '), nl,
	simplify(B,B2),  pprin(B2,N). % , newline(B2).
pprin((A '||' B), N) :- !,
	simplify(A,A2),	simplify(B,B2),
        tabs(N), pprin_or((A2 '||' B2)), nl.
pprin((A <=> B), N) :- !,
	simplify(A,A2), tabs(N), write('('), pprin(A2,0), write(' <-> '),
	simplify(B,B2), pprin(B2,0),write(')'), nl.
pprin((A ==> B), N) :-  !,
	simplify(A,A2), tabs(N), write('('), pprin(A2,0), % newline(A2),
	 write('  ->'),  nl, M is N+1,
        simplify(B,B2),  pprin(B2,M), write(')'),  nl.
pprin(all(Vs, L:H, P), N) :-
         tabs(N), write('('), write('forall '), write_domain_no_ops(Vs),  write(': int. '),
         simplify(L,L2), simplify(H,H2),
         write(L2), write( '<= '),  write_inequalities(Vs),  write(' <= '), write(H2),
         write( ' -> '),
         simplify(P, P2), pprin(P2,0), write(')').
pprin(exists(Vs, L:H, P), N) :-
         tabs(N), write('('), write('exists '), write_domain_no_ops(Vs), write(': int. '),
         simplify(L,L2), simplify(H,H2),
         write(L2), write( '<= '), write_inequalities(Vs),  write(' <= '),  write(H2),
         write( ' and '),
         simplify(P, P2), pprin(P2,0), write(')').


pprin(not(not(A)), N)  :-  !, simplify(A, A2), tabs(N), write_term(A2).
pprin(not(A), N)  :-  !, simplify(not, A, A2), tabs(N), write_term(A2).
pprin((X=<Y), N)  :-  !, simplify(X,X2),tabs(N), write_term(X2),
			 write('<='), simplify(Y,Y2), write_term(Y2).
pprin((X==Y), N)  :-  !, simplify(X,X2),tabs(N), write_term(X2),
			 write('='), simplify(Y,Y2), write_term(Y2).
pprin((X=Y), N)  :-  !, simplify(X,X2),tabs(N), write_term(X2),
			 write('='), simplify(Y,Y2), write_term(Y2).
pprin((X '!=' Y), N) :- !, simplify(X,X2), simplify(Y,Y2), tabs(N),
                        write('not('),write_term(X2),write(=),write_term(Y2),write(')').
pprin(A, N)  :- simplify(A, A2), tabs(N), write_term(A2).

pprin_or((A '||' B)) :- !, pprin_or(A), write(' or '), pprin_or(B).
pprin_or(A) :-  pprin(A,0).

write_inequalities([V])   :- write(V), !.
write_inequalities([V, OP |L]) :- write(V), write_op(OP), write_inequalities(L).

write_op('=<') :- !, write('<=').
write_op('==') :- !, write('=').
write_op(OP) :-  write(OP).

write_domain_no_ops(Vs) :-
          extract_vars(Vs, Ws),
          write_no_ops(Ws).

extract_vars([],[]).
extract_vars([E],L) :-
          (check_include(E) -> L = [E] ; L = []).
extract_vars([E,_|L],L2) :-
          (check_include(E) -> L2 = [E|L3] ; L2 = L3),
          extract_vars(L,L3).

write_no_ops([V]) :-  write(V).
write_no_ops([V|L]) :-
                 write(V), write(', '), write_no_ops(L).

check_include(E) :- atom(E), logic_vars(Vs), \+ is_logic_var(Vs,E).

is_logic_var([],_) :- fail.
is_logic_var([_:Vs | L], E) :-
          member(E,Vs) ;
          is_logic_var(L,E).

% __________________ WRITE TERM _____________

write_term(A) :- atomic(A), write(A).
write_term(array(A,T)) :- write(A), write('['), write(T), write(']').
write_term(not(T)) :- write('not('), write_term(T), write(')').
write_term((A =< B)) :- write(A), write('<='), write(B).
write_term((A mod B)) :- write(A), write('%'), write(B).
write_term(T) :-
          T =.. [OP,A1,A2],
          name(OP, L),
          (identifier(_,L,[])
             ->  write(T)
             ;   write('('), write_term(A1), write(OP),write_term(A2), write(')')
          ).
write_term(T) :- write(T).

tabs(0) :- !.
tabs(N) :- write('     '), M is N-1, tabs(M).

newline((_ && _)) :- !.
newline((_ ==> _)) :- !.
newline((_ <=> _)) :- !.
newline(_ '||' _) :- !.
newline(_) :- nl.


%__________________ SIMPLIFICATION RULES _________________


simplify((1-1), 0) :- !.
simplify((1*1), 1) :- !.
simplify((X+0), X) :- !.
simplify((X+1)-1, X) :- !.
simplify((X-1)+1, X) :- !.
simplify((X+1)=<(Y+1), (X=<Y)) :- !.
simplify(1=<(Y+1), (0=<Y)) :- !.
simplify(X @ [], X) :- !.
simplify([] @ X, X) :- !.
simplify(not(not(X)), X) :- !.
simplify((A '||' B), (C '||' D)) :- !,
	simplify(A,C),
	simplify(B,D).
simplify(array(X,T), array(X,T2)) :-
         simplify(T,T2).
% add a case for 2-d arrays
simplify(X, X).

simplify(not, true, false) :- !.
simplify(not, false, true) :- !.
simplify(not, (X '!=' Y), (X = Y)) :- !.
simplify(not, (X == Y), not(X = Y)) :- !.
simplify(not,(I=<J), (I>=A)) :-
	simplify(J+1,A), !.
simplify(not,(I=<J-1),I>=J) :- !.
% simplify(not,(X>Y), (X=<Y)) :- !.
simplify(not,(X<Y), (X>=Y)).
simplify(not, not(A), A) :- !.
simplify(not,(A && B), (C '||' D)) :-
	simplify(not, A, C),
        simplify(not, B, D).
simplify(not, T, not(T)).


% ________________________________________________________________
% ________________________________________________________________
%
% ___________________PARSER: GRAMMAR RULES _______________________
%
% ________________________________________________________________
% ________________________________________________________________


parse(Tokens,Triple) :- program(Triple,Tokens, []), !.

program(triple(Pre,ParseTree,Post))
		-->  types(Ts,[], TL),
                     functions(Fs,TL, FL),
                     axioms(As, FL, AL),
		     precondition(Pre, AL, PreCL),
                     postcondition(Post, PreCL,PostCL),
		     [@, program],
		     vars(Vs, PostCL, VL),
                     stmts(ParseTree, VL, _),
		     [@, end],
                     eop,
                     {write_preamble(Ts,Fs,As,Vs)}.

precondition(Pre,In,[requires|In]) --> [@, requires], {asserta(context([requires|In]))}, bexpr(Pre).

postcondition(Post,In,[ensures|In]) --> [@, ensures], {asserta(context([ensures|In]))}, bexpr(Post).

eop --> ['--'].

write_preamble(Ts,Fs,As,Vs) :-
          write_types(Ts),
          write_functions(Fs),
          write_axioms(As),
          nl,
          write_vars(Vs),
          assert(logic_vars(Vs)).


% ---------------- TYPES --------------------------------

types([], L, L) --> [].
types([(quote:TV):T|L], CL, CL_out) -->
                  [@, type], ['\'', id(TV), id(T)], {CL2 = [type:T | CL], asserta(context(CL2))},
                  types(L, CL2, CL_out).
types([T:EL|L], CL, CL_out) -->
                 [@, type, id(T), =], {CL2 = [type_enum:T | CL], asserta(context(CL2))}, enumeration(EL),
                 types(L, CL2, CL_out).

enumeration([N]) --> [id(N)].
enumeration([N|L]) --> [id(N)], ['|'], enumeration(L).

write_enumeration([H]) :- !, write(H), nl.
write_enumeration([H|T]) :-
                 write(H), write(' | '), write_enumeration(T).

write_types([]).
write_types([(quote:TV):T|L]) :- !,
                 write(type), write(' '), write('\''), write(TV), write(' '), write(T),nl,
                 write_types(L).
write_types([T:EL|L]) :-
                 write(type), write(' '), write(T), write(' = '),
                 write_enumeration(EL),
                 write_types(L).


% --------------------- FUNCTIONS ----------------------------


functions([],L,L) --> [].
functions([fun(F,D,R)|L],CL, CL_out) -->
          [@, function, id(F), ':'], domain(D), ['-','>'], base_type(R), !,
          {CL2 = [function:F|CL],  asserta(context(CL2))},
          functions(L, CL2, CL_out).
functions([fun(F,D)|L], CL, CL_out) -->
          [@, function, id(F), ':'],domain(D),
          {CL2 = [function:F|CL], asserta(context(CL2))},
          functions(L, CL2, CL_out).


domain([T]) --> base_type(T).
domain([T|L]) --> base_type(T), [ ','], domain(L).

base_type((quote:TV):T) --> ['\'', id(TV), id(T)].
base_type(quote:TV) --> ['\'', id(TV)].
base_type(type_inst(T,T2)) --> [id(T), id(T2)].
base_type(T) --> [id(T)].

write_base_type(T) :- atom(T), write(T).
write_base_type(type_inst(T,T2)) :-  write(T), write( ' '), write(T2).
write_base_type(quote:TV) :- write('\''), write(TV).
write_base_type((quote:TV):T) :- write('\''), write(TV), write(' '), write(T).

write_domain([E]) :- write_base_type(E), !.
write_domain([E|T]) :- write_base_type(E), write(', '), write_domain(T).

write_functions([]).
write_functions([fun(F,D,R)|L]) :-
          write(logic), write(' '), write(F), write(' : '),
          write_domain(D), write(' -> '), write_base_type(R), nl,
          write_functions(L).
write_functions([fun(F,D)|L]) :-
          write(logic), write(' '), write(F), write(' : '),
          write_domain(D), nl,
          write_functions(L).


% ---------------------------- AXIOMS -------------------------------

axioms([], L,L) --> [].
axioms([A:TQB|L],CL,CL_out) --> [@, axiom, id(A), ':'],
                  {CL2 = [axiom:A|CL],  asserta(context(CL2))},
                  typed_bexpr(TQB),
                  axioms(L,CL2,CL_out).

typed_bexpr(TQ:B) -->
                 type_quantifiers(TQ),
                 bexpr(B).

type_quantifiers([]) --> [].
type_quantifiers([DL:T | L]) -->
                  [all], ids(DL), [:],
                  base_type(T), ['.'],
                  type_quantifiers(L).

write_type_quantifiers([]).
write_type_quantifiers([DL:T | L]) :-
                  write(forall), write(' '),
                  write_comma_list(DL), write(': '),
                  write_base_type(T), write('. '),
                  write_type_quantifiers(L).

write_axioms([]).
write_axioms([A:(TQ:B)|L]) :-
           write(axiom), write(' '), write(A), write(': '),
           write_type_quantifiers(TQ),
           pprin(B,0), nl,
           write_axioms(L).

/*
You may have to do it recursively in general

write_func_body((L==>R)) :- !,
                 write(L), write(' -> '), write(R).
write_func_body((L<=>R)) :- !,
                 write(L), write(' <-> '), write(R).
write_func_body((L'||'R)) :- !,
                 write(L), write(' or '), write(R).
write_func_body((L&&R)) :- !,
                 write(L), write(' and '), write(R).
write_func_body(B) :- write(B).
*/


% --------------------- PROGRAM DECLARATIONS ----------------


type(T) --> [id(T)].
type(arr(T)) --> [id(T),'[]'].
%type(mat(T)) --> [id(T), '[]', '[]'].
type(type_inst(T1,T2)) --> [id(T1), id(T2)].

vars([], L, L) --> [].
vars([T:Vs|L], CL, CL_out) --> [@, var],
             {CL2 = [var_decl|CL], asserta(context(CL2))},
             ids(Vs), [:], type(T),
             vars(L,CL2,CL_out).

ids([I]) --> [id(I)].
ids([I|L]) -->  [id(I), ','], ids(L).

write_comma_list([H]) :- write(H), !.
write_comma_list([H|T]) :- write(H), write(','), write(' '), write_comma_list(T).

write_vars([]).
write_vars([arr(T):L1 | L]) :-
          !,
          assert(array_type(T,L1)),
          write_vars(L).
write_vars([T:L1 | L]) :-
          write(logic), write(' '),
          write_comma_list(L1),
          write(': '), write_base_type(T),
          nl,
          write_vars(L).

% C-like structs deprecated
%
% types([T|L]) --> [@, type, id(N), '{'],
% fields(F), {T=..[N|F]}, types(L).
%
% fields([F:T]) -->  type(T), [id(F), ';', '}'].
% fields([F:T | L]) -->  type(T), [id(F), ';'], fields(L).

% cmpdstmt AND OTHER STATEMENTS



% --------------------- PROGRAM CONTROL STRUCTURES --------------------


stmts((S1 ; S), CL_in, CL_out) -->
          stmt(S1, CL_in, CL2),
          stmts(S, CL2, CL_out).
stmts(S, CL_in, CL_out)  -->
          stmt(S, CL_in, CL_out).

stmt(S, CL_in, CL_out)   --> ifthenelse(S, CL_in, CL_out).
stmt(S, CL_in, CL_out)   --> while(S, CL_in, CL_out).
stmt(break, CL, CL)	--> [break], [';'].
stmt(continue, CL, CL)	--> [continue], [';'].
stmt(S, CL_in, CL_out)  --> assert(S, CL_in, CL_out).
stmt(S, CL_in, CL_out)	--> cmpdstmt(S, CL_in, CL_out).
stmt(S, CL_in, CL_out)  --> assign(S, CL_in, CL_out), [;].
stmt(S, CL_in, CL_out)  --> proc_call(S, CL_in, CL_out), [;].

cmpdstmt(S, CL_in, CL_out)  --> ['{'], stmts(S, CL_in, CL_out), ['}'].

assign((L = R), CL_in, CL_out) --> var(L), [=], expr(R),
                                   {CL_out = [assign|CL_in], asserta(context(CL_out))}.
assign((L = R), CL_in, CL_out) --> var(L), [=], bexpr(R),
                                   {CL_out = [assign|CL_in], asserta(context(CL_out))}.

proc_call(S, CL_in, CL_out) -->  [id(X)], ['('],
                                 {CL_out = [call:X|CL_in], asserta(context(CL_out))},
                                 exprlist(L), [')'], {S =.. [X|L]}.

ifthenelse(if(B,Then), CL_in, CL_out) --> [if, '('], {CL2 = [if|CL_in], asserta(context(CL2))},
                                          bexpr(B), [')'],
                                          stmt(Then, CL2, CL_out).

ifthenelse(if(B,Then,Else), CL_in, CL_out) --> [if, '('], {CL2 = [if|CL_in], asserta(context(CL2))},
                                               bexpr(B), [')'],
                                               stmt(Then, CL2, CL3), [else],
                                               {CL4 = [else|CL3], asserta(context(CL4))},
                                               stmt(Else,CL4,CL_out).

while(loop(I,B,W), CL_in, CL_out) -->
                       [@,invariant], {CL2 = [invariant|CL_in], asserta(context(CL2))},  bexpr(I),
                       [while], ['('], {CL3 = [while|CL2], asserta(context(CL3))}, bexpr(B), [')'],
                       stmt(W,CL3,CL_out).

assert(assert(B), CL_in, CL_out) --> [@, assert], {CL_out = [assert|CL_in], asserta(context(CL_out))}, bexpr(B).

% _______________ EXPRESSION GRAMMAR (expr and bexpr)

bexpr(T) --> imply_expr(T).

imply_expr(T) --> or_expr(T1), ['<=='], or_expr(T2), {T =.. ['<==', T1, T2]}.
imply_expr(T) --> or_expr(T1), ['==>'], or_expr(T2), {T =.. ['==>', T1, T2]}.
imply_expr(T) --> or_expr(T1), ['<=>'], or_expr(T2), {T =.. ['<=>', T1, T2]}.
imply_expr(T) --> or_expr(T).

or_expr(T)   --> and_term(T1), or_expr2(T1, T).

or_expr2(T,T)  --> [].
or_expr2(T1,T)  --> ['||'], and_term(T2), or_expr2((T1 '||' T2),T).

and_term(T)  --> not_term(T1), and_term2(T1,T).

and_term2(T,T)  --> [].
and_term2(T1,T)  --> ['&&'], not_term(T2), and_term2((T1 && T2),T).

not_term(not(T))  --> [not], ['('], bexpr(T), [')'].
not_term(true) --> [true].
not_term(false) --> [false].
not_term(T) -->
	[all, '('],   inequalities(L), [ ','],
	expr(From), [:], expr(To), [','],
	bexpr(B), [')'],
	{T = all(L,From:To,B)}.
        % {change_quant(all(V,From:To,B), T)}.
not_term(T) -->
	[exists, '('],  inequalities(L), [ ','],
	expr(From), [:], expr(To), [','],
	bexpr(B), [')'],
	{T = exists(L,From:To,B)}.
	% {change_quant(exists(V,From:To,B), T)}.
not_term(T) -->
	[all, '('], [id(V), ','], bexpr(B), [')'],
	{T = all(V,B)}.
        % {change_quant(all(V,From:To,B), T)}.
not_term(T) -->
	[exists, '('], [id(V), ','],	bexpr(B), [')'],
	{T = exists(V,B)}.
	% {change_quant(exists(V,From:To,B), T)}.


not_term(T) --> ['('], bexpr(T), [')'].
not_term(T) -->  rel_expr(T).
not_term(T) --> var(T).   % boolean variable

rel_expr(T) --> expr(T1), [ROP], rel_expr2(T2),
	        {rel_op(ROP), T =.. [ROP,T1,T2]}.

rel_expr2(T) --> expr(T).
rel_expr2(T) --> expr(T1), [ROP], rel_expr2(T2),
	        {rel_op(ROP), T =.. [ROP,T1,T2]}.


rel_op('!=').
rel_op('==').
rel_op(=).
rel_op(>).
rel_op(<).
rel_op(=<).
rel_op(>=).
rel_op('~>').

inequalities([E]) --> expr(E).
inequalities([E, OP |L]) --> expr(E), [OP], {member(OP, [<, >, '=<', '>=', =, '=='])},
                             inequalities(L).


% ____________________________

expr(T) --> term(T1), termX(T1, T).

termX(T1,T)  --> [OP], {member(OP, [+,-])}, term(T2),
	         {T3 =.. [OP,T1,T2]},
		 termX(T3,T).
termX(T,T)  --> [].

term(T) --> factor(T1), termY(T1, T).

termY(T1,T)  --> [OP], {operator(OP), \+ member(OP, [+,-])}, factor(T2),
	         {T3 =.. [OP,T1,T2]},
		 termY(T3,T).
termY(T,T)  --> [].


factor(null) --> [null].
factor([]) --> ['[]'].
factor(true) --> [true].
factor(false) --> [false].
factor(X) --> int(X).
factor(T) --> var(T).
factor(T) --> ['('], expr(T), [')'].

int(X)  --> [num(X)].
%int(X)  --> [id(X)].

var(T2) --> [id(X)], ['('], exprlist(L), [')'],
	   {T2=..[X|L]}.

var(T) --> [id(X)], ['['], expr(T1), [']'],
	   {T=array(X,T1)}.

var(T) --> [id(X)], ['['], expr(T1), [','], expr(T2), [']'],
	   {T=array(X,T1,T2)}.


var(X) --> [id(X)].


exprlist([])   --> [].
exprlist([E])   --> expr(E).
exprlist([E|L]) --> expr(E), [','], exprlist(L).

operator('@').
operator(+).
operator(-).
operator(/).
operator(*).
operator(:).
operator('::').
operator('~>').


% ______________________ LEXICAL ANALYZER  ________________________


lex(Stream,Tokens)  :-  get_chars(Stream,L,0), tokenize(L,Tokens), !.

get_chars(Str,L,N) :-  get_code(Str,C), get_chars(Str,C,L,N).

get_chars(Str, 45, [45|L], N) :-
          !, get_code(Str,C),
          (C==45 -> L = [45]
                 ;  L = [C|L2], M is N+1, get_chars(Str, L2, M)
          ).
          % 45 = -
get_chars(Str,C, [C|L1],N) :-
          (N < 10000 -> M is N+1, get_chars(Str,L1,M)
                      ; asserta(context([end_of_program])), fail
          ).

tokenize([], []).
tokenize([47,47|L], L3) :- skip_comment(L,L2), tokenize(L2,L3). %47 = /
tokenize([C|L], L3)	:- white(C), skip_whites(L,L2), tokenize(L2,L3).
tokenize([C|L], [X|L3]) :- alpha(C), identifier(X,[C|L],L2), tokenize(L2,L3).
tokenize([C|L], [X|L3]) :- d09(C), digits(X,[C|L],L2), tokenize(L2,L3).
tokenize(L, [X|L3])     :- special(X,L,L2), tokenize(L2,L3).

skip_whites([], []).
skip_whites([C|L], L2) :- (white(C) -> skip_whites(L,L2); L2 = [C|L]).

skip_comment([10|L],L) :- !.
skip_comment([_|L],L2) :- skip_comment(L,L2).

white(9).  % tab
white(10). % newline
white(32). % blank
white(13). % Mac CR

special('<==', [60,61,61|L],L).
special('==>', [61,61,62|L],L).
special('<=>', [60,61,62|L],L).

special('~>', [126,62|L], L).
special('==',[61,61|L],L).
special(=<,[61,60|L],L).
special(>=,[62,61|L],L).
special('!=',[33,61|L],L).
special('&&', [38,38|L],L).
special('||', [124,124|L],L).
special('|', [124|L], L).
special('::',[58,58|L],L).
special('[]',[91,93|L], L).

special(>,[62|L],L).
special(=,[61|L],L).
special(<,[60|L],L).
special('{',[123|L],L).
special('}',[125|L],L).
special('(',[40|L],L).
special(')',[41|L],L).
special('[',[91|L],L).
special(']',[93|L],L).
special(;,[59|L],L).
special(:,[58|L],L).
special(',',[44|L],L).
special(*,[42|L],L).
special(+,[43|L],L).
special('--', [45,45|L], L).
special(-,[45|L],L).
special(.,[46|L],L).
special(/,[47|L],L).
special('@', [64|L], L).
special('%', [37|L], L).
special('\'',[39|L], L).
special('_', [95|L], L).

identifier(X) --> ident(L), {name(N,L), (keyword(N) -> X=N; X=id(N))}.

ident([X|L]) --> letter(X), legits(L).
ident([X])   --> letter(X).

legits([X|W]) --> legit(X), legits(W).
legits([X])   --> legit(X).

legit(X) --> letter(X) ; digit(X).

letter(X) --> [X],  {alpha(X)}.

alpha(X) :-  X > 64,  X < 91.
alpha(X) :-  X > 96,  X < 123.

keyword(true).
keyword(false).
keyword(not).
keyword(if).
keyword(else).
keyword(while).
keyword(program).
keyword(break).
keyword(requires).
keyword(ensures).
keyword(invariant).
keyword(all).
keyword(exists).
keyword(null).
keyword(axiom).
keyword(var).
keyword(vars).
keyword(type).
keyword(continue).
keyword(function).
keyword(axiom).
keyword(assert).
keyword(end).

digits(num(N)) --> digs(L), {name(N,L)}.

digs([X|L]) --> digit(X), digs(L).
digs([X]) --> digit(X).

digit(X) -->  [X],  {d09(X)}.

d09(X) :- X > 47,  X < 58.



% ___________ QUANTIFIER RENAMING: NOT USED ___________________

%change_quant2(T,U) :-
%	    change_quant(T,U), !.
%change_quant2(T,U) :-
%	    T =.. [OP|Args],
%	    change_list(Args,Args2),
%	    U =.. [OP|Args2].
%
%change_list([],[]).
%change_list([H|T],[H2|T2]) :-
%	    change_quant2(H,H2),
%	    change_list(T,T2).
%
%change_quant(all,L,T) :- !,
%	     T1 =.. [all|L],
%	     change_quant(T1,T).
%change_quant(exists,L,T) :- !,
%	     T1 =.. [exists|L],
%	     change_quant(T1,T).
%change_quant(X,L,T1) :-
%	     T1 =.. [X|L].
%
%change_quant(all(V,T1,T2),all(V2,U1,U2)) :-
%	    new_sym(u,V2),
%	    subst(T1,V,V2,U1),
%	    subst(T2,V,V2,U2).
%change_quant(exists(V,T1,T2),exists(V2,U1,U2)) :-
%	    new_sym(e,V2),
%	    subst(T1,V,V2,U1),
%	    subst(T2,V,V2,U2).
%
%new_sym(A, B) :-
%   inc_counter_for(A, I),
%   user_concat_atom_number(A, I, B).
%
%user_concat_atom_number(Atom, N, AN) :-
%   number_codes(N, Ncodes),
%   atom_codes(Natom, Ncodes),
%   atom_concat(Atom, Natom, AN).
%
%inc_counter_for(u, I) :-
%   counter_u(Current),
  % write('Asserted '), write(counter_u(Current)),nl,
%   I is Current + 1,
%   retractall(counter_u(_)),
%   asserta(counter_u(I)), !.
%
%inc_counter_for(e, I) :-
%   counter_e(Current),
  % write('Asserted '), write(counter_e(Current)),nl,
%   I is Current + 1,
%   retractall(counter_e(_)),
%   asserta(counter_e(I)), !.

