module llinterp.

import lollisig.

kind   context  type.
type   empty    context.
type   del      context -> context.
type   '++'     o -> context -> context.
infixr '++'     5.

type isR         o -> o.
type isG         o -> o.
type isA         o -> o.
type subcontext  context -> context -> o.
type prove       context -> context -> o -> o.
type pickR       context -> context -> o -> o.
type bc          context -> context -> o -> o -> o.

isR erase.
isR B          :- isA B.
isR (B1 & B2)  :- isR B1,  isR B2.
isR (B1 -o B2) :- isG B1,  isR B2.
isR (B1 => B2) :- isG B1,  isR B2.
isR (pi B)     :- pi x\(isR (B x)).
  
isG one.
isG erase.
isG B          :- isA B.
isG (B1 -o B2) :- isR B1, isG B2.
isG (B1 => B2) :- isR B1, isG B2.
isG (B1 &  B2) :- isG B1, isG B2.
isG (B1 x  B2) :- isG B1, isG B2.
isG (bang B)   :- isG B.
isG (pi B)     :- pi x\(isG (B x)).

prove I I one.
prove I O erase     :- subcontext O I.
prove I O (G1 & G2) :- prove I O G1,  prove I O G2.
prove I O (R -o G)  :- prove (R ++ I) (del O) G.
prove I O (R => G)  :- prove ((bang R) ++ I) ((bang R) ++ O) G.
prove I O (G1 x G2) :- prove I M G1,  prove M O G2.
prove I I (bang G)  :- prove I I G.
prove I I (pi   G)  :- pi x\(prove I I (G x)).
prove I O A         :- isA A, (A <- G), prove I O G.
prove I O A         :- isA A, pickR I M R, bc M O A R.
prove I I (X is Y)  :- X is Y.
  
bc I I A A.
bc I O A (G -o R)  :- bc I M A R, prove M O G.
bc I O A (G => R)  :- bc I O A R, prove O O G.
bc I O A (pi R)    :- bc I O A (R T).
bc I O A (R1 & R2) :- bc I O A R1 ; bc I O A R2.
  
pickR ((bang R) ++ I) ((bang R) ++ I) R.
pickR (R ++ I) (del  I) R :- isR R.
pickR (S ++ I) (S ++ O) R :- pickR I O R.

subcontext (del  O) (R ++ I) :- isR R, subcontext O I.
subcontext (S ++ O) (S ++ I) :- subcontext O I. 
subcontext  empty    empty.
 
type notA   o -> o.

notA erase.
notA one.
notA (X & Y).
notA (X x Y).
notA (X -o Y).
notA (X => Y).
notA (bang X).
notA (pi X).
notA (X is Y).

isA A  :- not (notA A).

type go    o -> o.

go G :- prove empty empty G.