module parser.
import sign.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

type isG  o   -> o.
type isD  o   -> o.
%type isV o   -> o. 
type isV  Tau -> o. 
type isH  o   -> o.
type isA  o   -> o.
type isAv o   -> o. 
type p    Tau -> o.
type send o   -> o -> o.  
type obj  o   -> (o -> o) -> o.
type msg  o   -> o -> o. 

isA (p X).
isA (send Id Msg).
isA (obj  Id Def).
isA (msg  Id Msg). 

isAv A            :- isA A.
isAv A            :- isV A.     
%isAv (A X)       :- isAv A.

isH (A | B)       :- (isH A),(isH B).  
isH A             :- (isA A).
	
isG all.
isG anti.
isG (pi G)        :- pi x \ ( (isV x) => (isG (G x))).
isG (pi G)        :- sigma y \ pi x \ ((isA (x y)) => (isG (G x))).

% Su questi 2 si pone il vincolo di tipo 
isG (D >=> G)     :- isAv D,isG G.
isG (D >-o G)     :- isAv D,isG G.

isG (D => G)      :- isD(D),isG(G).
isG (D -o G)      :- isD(D),isG(G).
isG (G & H)       :- isG(G),isG(H).
isG (G | H)       :- isG(G),isG(H).
isG A             :- isAv A.  

isD (pi D)     :- pi x \ ( (isV x) => (isD (D x))).
isD (pi D)     :- sigma y \ pi x \ ((isA (x y)) => (isD (D x))).
isD (D & E)    :- (isD D),(isD E).
isD (H o- G)   :- (isH H),(isG G).
isD (D <= G)   :- (isD D),(isG G).
isD  A         :- (isA A).        

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

type fg o -> o.     
fg   (pi x \ ((x all) -o (p x))).

type ff o -> o.
ff (pi id \ (pi d \ (pi m \ 
    ( ((send id m) | (obj id d)) o- 
      ((d id)  >-o ((obj id d)  | (msg id m))
    ))))).

type pg o.
type pf o. 
pf  :- (ff F),(isD F).
pg  :- (fg G),(isG G).
 
type rl o.
rl :- load "parser",use "parser".

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%