{-# OPTIONS --allow-unsolved-metas #-}
{-# OPTIONS --rewriting #-}
module Polarized where
open import Library
postulate Atoms : Set
data Pol : Set where
+ - : Pol
data Form : Pol → Set where
True : ∀{p} → Form p
_∧_ : ∀{p} (A B : Form p) → Form p
Atom : (P : Atoms) → Form +
False : Form +
_∨_ : (A B : Form +) → Form +
_⇒_ : (A : Form +) (B : Form -) → Form -
Comp : (A : Form +) → Form -
Thunk : (A : Form -) → Form +
infixl 8 _∧_
infixl 7 _∨_
infixr 6 _⇒_
module _ (S : Set) where
data Cxt' : Set where
ε : Cxt'
_∙_ : (Γ : Cxt') (A : S) → Cxt'
data Hyp' (A : S) : (Γ : Cxt') → Set where
top : ∀{Γ} → Hyp' A (Γ ∙ A)
pop : ∀{B Γ} (x : Hyp' A Γ) → Hyp' A (Γ ∙ B)
infixl 4 _∙_
Cxt = Cxt' (Form -)
Hyp = Hyp' (Form -)
Atom- = λ P → Comp (Atom P)
HypAtom = λ P → Hyp (Atom- P)
module _ (Nf : (A : Form +) (Γ : Cxt) → Set) where
data Ne' (C : Form -) (Γ : Cxt) : Set where
hyp : ∀ (x : Hyp C Γ) → Ne' C Γ
impE : ∀{A} (t : Ne' (A ⇒ C) Γ) (u : Nf A Γ) → Ne' C Γ
andE₁ : ∀{D} (t : Ne' (C ∧ D) Γ) → Ne' C Γ
andE₂ : ∀{D} (t : Ne' (D ∧ C) Γ) → Ne' C Γ
mutual
AddHyp = λ A J Γ → AddHyp' Γ J A
data AddHyp' (Γ : Cxt) (J : Cxt → Set) : (A : Form +) → Set where
addAtom : ∀{P} (t : J (Γ ∙ Atom- P)) → AddHyp (Atom P) J Γ
addNeg : ∀{A} (t : J (Γ ∙ A)) → AddHyp (Thunk A) J Γ
trueE : (t : J Γ) → AddHyp True J Γ
andE : ∀{A B} (t : AddHyp A (AddHyp B J) Γ) → AddHyp (A ∧ B) J Γ
falseE : AddHyp False J Γ
orE : ∀{A B} (t : AddHyp A J Γ) (u : AddHyp B J Γ) → AddHyp (A ∨ B) J Γ
module _ (Ne : (A : Form +) (Γ : Cxt) → Set) where
data Cover' (i : Size) (J : Cxt → Set) (Γ : Cxt) : Set where
returnC : (t : J Γ) → Cover' i J Γ
matchC : ∀{j : Size< i} {A} (t : Ne A Γ) (c : AddHyp A (Cover' j J) Γ) → Cover' i J Γ
mutual
Ne : (i : Size) (C : Form -) (Γ : Cxt) → Set
Ne i = Ne' (RFoc i)
Cover : (i j : Size) (J : Cxt → Set) (Γ : Cxt) → Set
Cover i j = Cover' (λ A → Ne j (Comp A)) i
data RFoc : (i : Size) (A : Form +) (Γ : Cxt) → Set where
thunk : ∀{i Γ A} (t : RInv i A Γ) → RFoc (↑ i) (Thunk A) Γ
hyp : ∀{i Γ P} (x : HypAtom P Γ) → RFoc (↑ i) (Atom P) Γ
trueI : ∀{i Γ} → RFoc (↑ i) True Γ
andI : ∀{i Γ A B} (t : RFoc i A Γ) (u : RFoc i B Γ) → RFoc (↑ i) (A ∧ B) Γ
orI₁ : ∀{i Γ B A} (t : RFoc i A Γ) → RFoc (↑ i) (A ∨ B) Γ
orI₂ : ∀{i Γ A B} (u : RFoc i B Γ) → RFoc (↑ i) (A ∨ B) Γ
data RInv : (i : Size) (A : Form -) (Γ : Cxt) → Set where
ret : ∀{i Γ A} (t : Cover ∞ i (RFoc i A) Γ) → RInv (↑ i) (Comp A) Γ
trueI : ∀{i Γ} → RInv (↑ i) True Γ
andI : ∀{i Γ A B} (t : RInv i A Γ) (u : RInv i B Γ) → RInv (↑ i) (A ∧ B) Γ
impI : ∀{i Γ A B} (t : AddHyp A (RInv i B) Γ) → RInv (↑ i) (A ⇒ B) Γ
_→̇_ : (P Q : Cxt → Set) → Set
P →̇ Q = ∀{Γ} → P Γ → Q Γ
mapAddHyp : ∀{P Q} (f : P →̇ Q) → ∀{A} → AddHyp A P →̇ AddHyp A Q
mapAddHyp f (addAtom t) = addAtom (f t)
mapAddHyp f (addNeg t) = addNeg (f t)
mapAddHyp f (trueE t) = trueE (f t)
mapAddHyp f falseE = falseE
mapAddHyp f (andE t) = andE (mapAddHyp (mapAddHyp f) t)
mapAddHyp f (orE t u) = orE (mapAddHyp f t) (mapAddHyp f u)
mapCover : ∀{P Q} (f : P →̇ Q) {i j} → Cover i j P →̇ Cover i j Q
mapCover f (returnC t) = returnC (f t)
mapCover f (matchC t c) = matchC t (mapAddHyp (mapCover f) c)
joinCover : ∀{i j P} → Cover i j (Cover ∞ j P) →̇ Cover ∞ j P
joinCover (returnC t) = t
joinCover (matchC t c) = matchC t (mapAddHyp joinCover c)
infix 3 _≤_
data _≤_ : (Γ Δ : Cxt) → Set where
id≤ : ∀{Γ} → Γ ≤ Γ
weak : ∀{A Γ Δ} (τ : Γ ≤ Δ) → Γ ∙ A ≤ Δ
lift : ∀{A Γ Δ} (τ : Γ ≤ Δ) → Γ ∙ A ≤ Δ ∙ A
postulate lift-id≤ : ∀{Γ A} → lift id≤ ≡ id≤ {Γ ∙ A}
{-# REWRITE lift-id≤ #-}
_•_ : ∀{Γ Δ Φ} (τ : Γ ≤ Δ) (σ : Δ ≤ Φ) → Γ ≤ Φ
id≤ • σ = σ
weak τ • σ = weak (τ • σ)
lift τ • id≤ = lift τ
lift τ • weak σ = weak (τ • σ)
lift τ • lift σ = lift (τ • σ)
•-id : ∀{Γ Δ} (τ : Γ ≤ Δ) → τ • id≤ ≡ τ
•-id id≤ = refl
•-id (weak τ) = cong weak (•-id τ)
•-id (lift τ) = refl
{-# REWRITE •-id #-}
Mon : (P : Cxt → Set) → Set
Mon P = ∀{Γ Δ} (τ : Γ ≤ Δ) → P Δ → P Γ
monH : ∀{A} → Mon (Hyp A)
monH id≤ x = x
monH (weak τ) x = pop (monH τ x)
monH (lift τ) top = top
monH (lift τ) (pop x) = pop (monH τ x)
monH• : ∀{Γ Δ Φ A} (τ : Γ ≤ Δ) (σ : Δ ≤ Φ) (x : Hyp A Φ) → monH (τ • σ) x ≡ monH τ (monH σ x)
monH• id≤ σ x = refl
monH• (weak τ) σ x = cong pop (monH• τ σ x)
monH• (lift τ) id≤ x = refl
monH• (lift τ) (weak σ) x = cong pop (monH• τ σ x)
monH• (lift τ) (lift σ) top = refl
monH• (lift τ) (lift σ) (pop x) = cong pop (monH• τ σ x)
{-# REWRITE monH• #-}
monNe' : ∀{P : Form + → Cxt → Set}
(monP : ∀{A} → Mon (P A)) →
∀{A} → Mon (Ne' P A)
monNe' monP τ (hyp x) = hyp (monH τ x)
monNe' monP τ (impE t u) = impE (monNe' monP τ t) (monP τ u)
monNe' monP τ (andE₁ t) = andE₁ (monNe' monP τ t)
monNe' monP τ (andE₂ t) = andE₂ (monNe' monP τ t)
monAddHyp : ∀{P} (monP : Mon P) → ∀{A} → Mon (AddHyp A P)
monAddHyp monP τ (addAtom t) = addAtom (monP (lift τ) t)
monAddHyp monP τ (addNeg t) = addNeg (monP (lift τ) t)
monAddHyp monP τ (trueE t) = trueE (monP τ t)
monAddHyp monP τ falseE = falseE
monAddHyp monP τ (andE t) = andE (monAddHyp (monAddHyp monP) τ t)
monAddHyp monP τ (orE t u) = orE (monAddHyp monP τ t) (monAddHyp monP τ u)
mutual
monNe : ∀{i A} → Mon (Ne i A)
monNe {i} τ t = monNe' (monRFoc {i}) τ t
monCover : ∀{i j P} (monP : Mon P) → Mon (Cover i j P)
monCover monP τ (returnC t) = returnC (monP τ t)
monCover {i} {j} monP τ (matchC {i'} t c) = matchC (monNe τ t)
(monAddHyp (monCover {i'} {j} monP) τ c)
monRFoc : ∀{i A} → Mon (RFoc i A)
monRFoc τ (thunk t) = thunk (monRInv τ t)
monRFoc τ (hyp x) = hyp (monH τ x)
monRFoc τ trueI = trueI
monRFoc τ (andI t t₁) = andI (monRFoc τ t) (monRFoc τ t₁)
monRFoc τ (orI₁ t) = orI₁ (monRFoc τ t)
monRFoc τ (orI₂ t) = orI₂ (monRFoc τ t)
monRInv : ∀{i A} → Mon (RInv i A)
monRInv τ (ret {i} t) = ret (monCover (monRFoc {i}) τ t)
monRInv τ trueI = trueI
monRInv τ (andI t t₁) = andI (monRInv τ t) (monRInv τ t₁)
monRInv τ (impI {i} t) = impI (monAddHyp (monRInv {i}) τ t)
KFun : (P Q : Cxt → Set) (Γ : Cxt) → Set
KFun P Q Γ = ∀{Δ} (τ : Δ ≤ Γ) → P Δ → Q Δ
_⇒̂_ : (P Q : Cxt → Set) (Γ : Cxt) → Set
_⇒̂_ P Q Γ = ∀{Δ} (τ : Δ ≤ Γ) → P Δ → Q Δ
mapAddHyp' : ∀{P Q Γ} (f : (P ⇒̂ Q) Γ) → ∀{A} → AddHyp A P Γ → AddHyp A Q Γ
mapAddHyp' f (addAtom t) = addAtom (f (weak id≤) t)
mapAddHyp' f (addNeg t) = addNeg (f (weak id≤) t)
mapAddHyp' f (trueE t) = trueE (f id≤ t)
mapAddHyp' f falseE = falseE
mapAddHyp' f (andE t) = andE (mapAddHyp' (λ τ → mapAddHyp' λ τ' → f (τ' • τ)) t)
mapAddHyp' f (orE t u) = orE (mapAddHyp' f t) (mapAddHyp' f u)
mapCover' : ∀{P Q Γ} (f : (P ⇒̂ Q) Γ) {i j} (c : Cover i j P Γ) → Cover i j Q Γ
mapCover' f (returnC t) = returnC (f id≤ t)
mapCover' f (matchC t c) = matchC t (mapAddHyp' (λ τ → mapCover' λ τ' → f (τ' • τ)) c)
bindAddHyp : ∀{A B J K} (monJ : Mon J) → AddHyp A J →̇ ((J ⇒̂ AddHyp B K) ⇒̂ AddHyp (A ∧ B) K)
bindAddHyp monJ t τ k = andE (mapAddHyp' k (monAddHyp monJ τ t))
⟦_⟧ : ∀{p} (A : Form p) (Γ : Cxt) → Set
⟦ Atom P ⟧ Γ = HypAtom P Γ
⟦ False ⟧ Γ = ⊥
⟦ A ∨ B ⟧ Γ = ⟦ A ⟧ Γ ⊎ ⟦ B ⟧ Γ
⟦ True ⟧ Γ = ⊤
⟦ A ∧ B ⟧ Γ = ⟦ A ⟧ Γ × ⟦ B ⟧ Γ
⟦ A ⇒ B ⟧ Γ = ∀ {Δ} (τ : Δ ≤ Γ) (a : ⟦ A ⟧ Δ) → ⟦ B ⟧ Δ
⟦ Comp A ⟧ = Cover ∞ ∞ ⟦ A ⟧
⟦ Thunk A ⟧ = ⟦ A ⟧
mon⟦_⟧ : ∀{p} (A : Form p) → Mon ⟦ A ⟧
mon⟦ True ⟧ τ _ = _
mon⟦ A ∧ B ⟧ τ (a , b) = mon⟦ A ⟧ τ a , mon⟦ B ⟧ τ b
mon⟦ Atom P ⟧ = monH
mon⟦ False ⟧ τ ()
mon⟦ A ∨ B ⟧ τ = map-⊎ (mon⟦ A ⟧ τ) (mon⟦ B ⟧ τ)
mon⟦ A ⇒ B ⟧ τ f δ = f (δ • τ)
mon⟦ Comp A ⟧ = monCover mon⟦ A ⟧
mon⟦ Thunk A ⟧ = mon⟦ A ⟧
mutual
reify- : ∀ (A : Form -) → ⟦ A ⟧ →̇ RInv ∞ A
reify- True _ = trueI
reify- (A ∧ B) (a , b) = andI (reify- A a) (reify- B b)
reify- (A ⇒ B) f = impI (reflectHyp A λ τ a → reify- B (f τ a))
reify- (Comp A) c = ret (mapCover (reify+ A) c)
reify+ : ∀ (A : Form +) → ⟦ A ⟧ →̇ RFoc ∞ A
reify+ True _ = trueI
reify+ (A ∧ B) (a , b) = andI (reify+ A a) (reify+ B b)
reify+ (Atom P) x = hyp x
reify+ False ()
reify+ (A ∨ B) (inj₁ a) = orI₁ (reify+ A a)
reify+ (A ∨ B) (inj₂ b) = orI₂ (reify+ B b)
reify+ (Thunk A) a = thunk (reify- A a)
reflectHyp : ∀ A {Γ} {J} (k : ∀ {Δ} (τ : Δ ≤ Γ) → ⟦ A ⟧ Δ → J Δ) → AddHyp A J Γ
reflectHyp True k = trueE (k id≤ _)
reflectHyp (A ∧ B) k = andE (reflectHyp A λ τ a →
reflectHyp B λ τ' b → k (τ' • τ) (mon⟦ A ⟧ τ' a , b))
reflectHyp (Atom P) k = addAtom (k (weak id≤) top)
reflectHyp False k = falseE
reflectHyp (A ∨ B) k = orE (reflectHyp A (λ τ a → k τ (inj₁ a)))
(reflectHyp B (λ τ b → k τ (inj₂ b)))
reflectHyp (Thunk A) k = addNeg (k (weak id≤) (reflect A (hyp top)))
reflect : ∀ (A : Form -) → Ne ∞ A →̇ ⟦ A ⟧
reflect True t = _
reflect (A ∧ B) t = reflect A (andE₁ t) , reflect B (andE₂ t)
reflect (A ⇒ B) t τ a = reflect B (impE (monNe τ t) (reify+ A a))
reflect (Comp A) t = matchC t (reflectHyp A λ τ a → returnC a)
paste : ∀ (A : Form -) → Cover ∞ ∞ ⟦ A ⟧ →̇ ⟦ A ⟧
paste True _ = _
paste (A ∧ B) c = paste A (mapCover proj₁ c) , paste B (mapCover proj₂ c)
paste (A ⇒ B) c τ a = paste B (mapCover' (λ τ' f → f id≤ (mon⟦ A ⟧ τ' a)) (monCover mon⟦ A ⇒ B ⟧ τ c))
paste (Comp A) = joinCover
module Evaluation where
G⟦_⟧ : (Γ : Cxt) → Cxt → Set
G⟦ ε ⟧ Δ = ⊤
G⟦ Γ ∙ P ⟧ Δ = G⟦ Γ ⟧ Δ × ⟦ P ⟧ Δ
monG⟦_⟧ : (Γ : Cxt) → Mon (G⟦ Γ ⟧)
monG⟦ ε ⟧ = _
monG⟦ Γ ∙ P ⟧ τ (γ , a) = monG⟦ Γ ⟧ τ γ , mon⟦ P ⟧ τ a
Ev : (R : Set) (Δ Γ : Cxt) → Set
Ev R Δ Γ = G⟦ Γ ⟧ Δ → R
cut : ∀{R P Δ} → ⟦ P ⟧ Δ → AddHyp P (Ev R Δ) →̇ Ev R Δ
cut x (addAtom t) γ = t (γ , returnC x)
cut a (addNeg t) γ = t (γ , a)
cut _ (trueE t) = t
cut (a , b) (andE t) = cut a (mapAddHyp (cut b) t)
cut () falseE
cut (inj₁ a) (orE t u) = cut a t
cut (inj₂ b) (orE t u) = cut b u