module linear.Typecheck where
open import Function
open import Data.Nat
open import Data.Fin
open import Data.Vec hiding ([_] ; _++_ ; tail)
open import Data.Product as P using (proj₁ ; proj₂)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import linear.Type as Type
open import linear.Context as C hiding (_++_)
open import linear.Usage
open import linear.Usage.Equality as UsageEq
open import linear.Language
open import linear.Typing
open import linear.Typing.Inversion
open import linear.Typing.Functional
open import linear.RawIso
open import linear.Typecheck.Problem
consume : {n : ℕ} {γ : Context n} (Γ : Usages γ) (k : Fin n) → Dec $ CONSUME Γ k
consume ([ σ ] ∷ Γ) zero = yes (σ , ] σ [ ∷ Γ , z)
consume (] σ [ ∷ Γ) zero = no (λ { (_ , _ , ()) })
consume (σ ∷ Γ) (suc k) = consumeSuc Γ σ k <$> consume Γ k
checkPattern : {n : ℕ} (σ : Type) (p : Pattern n) → Dec $ PATTERN σ p
checkPattern σ `v = yes (σ ∷ [] , `v)
checkPattern 𝟙 `⟨⟩ = yes ([] , `⟨⟩)
checkPattern (σ ⊗ τ) (p ,, q) = patternTensor <$> checkPattern σ p <*> checkPattern τ q
checkPattern (κ x) `⟨⟩ = no (λ { (_ , ()) })
checkPattern 𝟘 `⟨⟩ = no (λ { (_ , ()) })
checkPattern (σ ⊗ τ) `⟨⟩ = no (λ { (_ , ()) })
checkPattern (σ ─o τ) `⟨⟩ = no (λ { (_ , ()) })
checkPattern (σ & τ) `⟨⟩ = no (λ { (_ , ()) })
checkPattern (σ ⊕ τ) `⟨⟩ = no (λ { (_ , ()) })
checkPattern 𝟙 (p ,, q) = no (λ { (_ , ()) })
checkPattern 𝟘 (p ,, q) = no (λ { (_ , ()) })
checkPattern (σ ─o τ) (p ,, q) = no (λ { (_ , ()) })
checkPattern (σ & τ) (p ,, q) = no (λ { (_ , ()) })
checkPattern (κ x) (p ,, q) = no (λ { (_ , ()) })
checkPattern (σ ⊕ τ) (p ,, q) = no (λ { (_ , ()) })
truncate : {n o : ℕ} {γ : Context n} (δ : Context o) (Γ : Usages (δ C.++ γ)) → Dec $ TRUNCATE δ Γ
truncate [] Γ = yes (Γ , refl)
truncate (a ∷ δ) ([ .a ] ∷ Γ) = no (λ { (_ , ()) })
truncate (a ∷ δ) (] .a [ ∷ Γ) = truncateUsed δ Γ <$> truncate δ Γ
mutual
infer : {n : ℕ} {γ : Context n} (Γ : Usages γ) (t : Infer n) → Dec $ INFER Γ t
infer Γ (`var k) = inferVar Γ k <$> consume Γ k
infer Γ (`app t u)
with infer Γ t
... | no ¬p = no $ λ p → ¬p (_ , _ , app-inv-function (INFER.proof p))
... | yes (𝟙 , _ , T) = no $ λ p → case functionalInfer _ T (app-inv-function $ INFER.proof p) of λ ()
... | yes (𝟘 , _ , T) = no $ λ p → case functionalInfer _ T (app-inv-function $ INFER.proof p) of λ ()
... | yes (σ ⊗ τ , _ , T) = no $ λ p → case functionalInfer _ T (app-inv-function $ INFER.proof p) of λ ()
... | yes (σ ⊕ τ , _ , T) = no $ λ p → case functionalInfer _ T (app-inv-function $ INFER.proof p) of λ ()
... | yes (σ & τ , _ , T) = no $ λ p → case functionalInfer _ T (app-inv-function $ INFER.proof p) of λ ()
... | yes (κ n , _ , T) = no $ λ p → case functionalInfer _ T (app-inv-function $ INFER.proof p) of λ ()
... | yes (σ ─o τ , Δ , T)
with check Δ σ u
... | no ¬p = no $ λ p → let eq = functionalInferPost _ (app-inv-function (INFER.proof p)) T
coerce = subst₂ (_⊢_∋ _ ⊠ _) (cong proj₂ eq) (proj₁ $ ─o-inj $ cong proj₁ eq)
in ¬p (_ , coerce (app-inv-argument (INFER.proof p)))
... | yes (θ , U) = yes (τ , θ , `app T U)
infer Γ (`fst t)
with infer Γ t
... | no ¬p = no $ λ p → ¬p (_ , _ , proj₂ (fst-inv (INFER.proof p)))
... | yes (𝟙 , _ , T) = no $ λ p → case functionalInfer _ T (proj₂ $ fst-inv $ INFER.proof p) of λ ()
... | yes (𝟘 , _ , T) = no $ λ p → case functionalInfer _ T (proj₂ $ fst-inv $ INFER.proof p) of λ ()
... | yes (σ ⊗ τ , _ , T) = no $ λ p → case functionalInfer _ T (proj₂ $ fst-inv $ INFER.proof p) of λ ()
... | yes (σ ⊕ τ , _ , T) = no $ λ p → case functionalInfer _ T (proj₂ $ fst-inv $ INFER.proof p) of λ ()
... | yes (σ ─o τ , _ , T) = no $ λ p → case functionalInfer _ T (proj₂ $ fst-inv $ INFER.proof p) of λ ()
... | yes (κ n , _ , T) = no $ λ p → case functionalInfer _ T (proj₂ $ fst-inv $ INFER.proof p) of λ ()
... | yes (σ & τ , Δ , T) = yes (σ , Δ , `fst T)
infer Γ (`snd t)
with infer Γ t
... | no ¬p = no $ λ p → ¬p (_ , _ , proj₂ (snd-inv (INFER.proof p)))
... | yes (𝟙 , _ , T) = no $ λ p → case functionalInfer _ T (proj₂ $ snd-inv $ INFER.proof p) of λ ()
... | yes (𝟘 , _ , T) = no $ λ p → case functionalInfer _ T (proj₂ $ snd-inv $ INFER.proof p) of λ ()
... | yes (σ ⊗ τ , _ , T) = no $ λ p → case functionalInfer _ T (proj₂ $ snd-inv $ INFER.proof p) of λ ()
... | yes (σ ⊕ τ , _ , T) = no $ λ p → case functionalInfer _ T (proj₂ $ snd-inv $ INFER.proof p) of λ ()
... | yes (σ ─o τ , _ , T) = no $ λ p → case functionalInfer _ T (proj₂ $ snd-inv $ INFER.proof p) of λ ()
... | yes (κ n , _ , T) = no $ λ p → case functionalInfer _ T (proj₂ $ snd-inv $ INFER.proof p) of λ ()
... | yes (σ & τ , Δ , T) = yes (τ , Δ , `snd T)
infer Γ (`case t return ν of l %% r)
with infer Γ t
... | no ¬p = no $ λ p → ¬p (_ , _ , case-inv-scrutinee (INFER.proof p))
... | yes (𝟙 , _ , T) = no $ λ p → case functionalInfer _ T (case-inv-scrutinee $ INFER.proof p) of λ ()
... | yes (𝟘 , _ , T) = no $ λ p → case functionalInfer _ T (case-inv-scrutinee $ INFER.proof p) of λ ()
... | yes (σ ⊗ τ , _ , T) = no $ λ p → case functionalInfer _ T (case-inv-scrutinee $ INFER.proof p) of λ ()
... | yes (σ & τ , _ , T) = no $ λ p → case functionalInfer _ T (case-inv-scrutinee $ INFER.proof p) of λ ()
... | yes (σ ─o τ , _ , T) = no $ λ p → case functionalInfer _ T (case-inv-scrutinee $ INFER.proof p) of λ ()
... | yes (κ n , _ , T) = no $ λ p → case functionalInfer _ T (case-inv-scrutinee $ INFER.proof p) of λ ()
... | yes (σ ⊕ τ , Δ , T)
with check ([ σ ] ∷ Δ) ν l | check ([ τ ] ∷ Δ) ν r
... | no ¬l | _ = no $ λ p →
let eq = functionalInferPost _ (case-inv-scrutinee $ INFER.proof p) T
coerce = subst₂ (λ Δ σ → [ σ ] ∷ Δ ⊢ ν ∋ l ⊠ ] σ [ ∷ _) (cong proj₂ eq) (proj₁ $ ⊕-inj $ cong proj₁ eq)
in ¬l (_ , coerce (case-inv-left (INFER.proof p)))
... | _ | no ¬r = no $ λ p →
let eq = functionalInferPost _ (case-inv-scrutinee $ INFER.proof p) T
coerce = subst₂ (λ Δ τ → [ τ ] ∷ Δ ⊢ ν ∋ r ⊠ ] τ [ ∷ _) (cong proj₂ eq) (proj₂ $ ⊕-inj $ cong proj₁ eq)
in ¬r (_ , coerce (case-inv-right (INFER.proof p)))
... | yes ([ .σ ] ∷ θ₁ , L) | _ = no $ λ p →
let eq = functionalInferPost _ (case-inv-scrutinee (INFER.proof p)) T
coerce = subst₂ (λ σ θ → [ σ ] ∷ θ ⊢ ν ∋ l ⊠ ] σ [ ∷ _) (proj₁ $ ⊕-inj $ cong proj₁ eq) (cong proj₂ eq)
in case functionalCheckPost _ (coerce (case-inv-left (INFER.proof p))) L of λ ()
... | _ | yes ([ .τ ] ∷ θ₂ , R) = no $ λ p →
let eq = functionalInferPost _ (case-inv-scrutinee (INFER.proof p)) T
coerce = subst₂ (λ σ θ → [ σ ] ∷ θ ⊢ ν ∋ r ⊠ ] σ [ ∷ _) (proj₂ $ ⊕-inj $ cong proj₁ eq) (cong proj₂ eq)
in case functionalCheckPost _ (coerce (case-inv-right (INFER.proof p))) R of λ ()
... | yes (] .σ [ ∷ θ₁ , L) | yes (] .τ [ ∷ θ₂ , R)
with eqs θ₁ θ₂
... | no ¬eq = no $ λ p →
let eq = functionalInferPost _ (case-inv-scrutinee (INFER.proof p)) T
coerceˡ = subst₂ (λ σ θ → [ σ ] ∷ θ ⊢ ν ∋ l ⊠ ] σ [ ∷ _) (proj₁ $ ⊕-inj $ cong proj₁ eq) (cong proj₂ eq)
coerceʳ = subst₂ (λ σ θ → [ σ ] ∷ θ ⊢ ν ∋ r ⊠ ] σ [ ∷ _) (proj₂ $ ⊕-inj $ cong proj₁ eq) (cong proj₂ eq)
eq₁ = functionalCheckPost _ (coerceˡ (case-inv-left (INFER.proof p))) L
eq₂ = functionalCheckPost _ (coerceʳ (case-inv-right (INFER.proof p))) R
in ¬eq $ trans (sym $ cong tail eq₁) (cong tail eq₂)
... | yes eq rewrite eq = yes (ν , _ , `case T return ν of L %% R)
infer Γ (`exfalso σ t) with infer Γ t
... | no ¬p = no $ λ p → case ¬p (_ , _ , exfalso-inv (INFER.proof p)) of λ ()
... | yes (𝟘 , Δ , p) = yes (σ , Δ , `exfalso σ p)
... | yes (κ _ , Δ , p) = no $ λ q → case functionalInferPost _ (exfalso-inv $ INFER.proof q) p of λ ()
... | yes (𝟙 , Δ , p) = no $ λ q → case functionalInferPost _ (exfalso-inv $ INFER.proof q) p of λ ()
... | yes (_ ⊗ _ , Δ , p) = no $ λ q → case functionalInferPost _ (exfalso-inv $ INFER.proof q) p of λ ()
... | yes (_ ─o _ , Δ , p) = no $ λ q → case functionalInferPost _ (exfalso-inv $ INFER.proof q) p of λ ()
... | yes (_ & _ , Δ , p) = no $ λ q → case functionalInferPost _ (exfalso-inv $ INFER.proof q) p of λ ()
... | yes (_ ⊕ _ , Δ , p) = no $ λ q → case functionalInferPost _ (exfalso-inv $ INFER.proof q) p of λ ()
infer Γ (`cut t σ) = inferCut Γ t σ <$> check Γ σ t
check : {n : ℕ} {γ : Context n} (Γ : Usages γ) (σ : Type) (t : Check n) → Dec $ CHECK Γ σ t
check Γ σ (`neu t)
with infer Γ t
... | no ¬p = no $ λ p → case ¬p (_ , _ , (neu-inv $ CHECK.proof p)) of λ ()
... | yes (τ , Δ , p)
with Type.eq σ τ
... | no ¬σ≡τ = no $ λ q → ¬σ≡τ $ functionalInfer _ (neu-inv $ CHECK.proof q) p
check Γ σ (`neu t) | yes (.σ , Δ , p) | yes refl = yes (Δ , `neu p)
check Γ σ (`let p ∷= t `in u)
with infer Γ t
... | no ¬p = no $ λ p → ¬p (_ , _ , let-inv-bound (CHECK.proof p))
... | yes (τ , Δ , T)
with checkPattern τ p
... | no ¬p = no $ λ p → let eq = functionalInfer _ (let-inv-bound (CHECK.proof p)) T
coerce = subst (_∋ _ ↝ (patternContext (let-inv-pattern (CHECK.proof p)))) eq
in ¬p (_ , (coerce (let-inv-pattern (CHECK.proof p))))
... | yes (δ , P)
with check ([[ δ ]] ++ Δ) σ u
... | no ¬q = no $ λ q →
let eq₁ = functionalInferPost _ (let-inv-bound (CHECK.proof q)) T
coerce₁ = subst (_∋ p ↝ patternContext (let-inv-pattern (CHECK.proof q))) (cong proj₁ eq₁)
eq₂ = functionalPattern _ (coerce₁ (let-inv-pattern (CHECK.proof q))) P
coerce₂ = subst₂ (λ δ Δ → [[ δ ]] ++ Δ ⊢ σ ∋ u ⊠ ]] δ [[ ++ _) eq₂ (cong proj₂ eq₁)
in ¬q (_ , coerce₂ (let-inv-body (CHECK.proof q)))
... | yes (θ , U)
with truncate δ θ
... | no ¬q = no $ λ q →
let eq₁ = functionalInferPost _ (let-inv-bound (CHECK.proof q)) T
coerce₁ = subst (_∋ p ↝ patternContext (let-inv-pattern (CHECK.proof q))) (cong proj₁ eq₁)
eq₂ = functionalPattern _ (coerce₁ (let-inv-pattern (CHECK.proof q))) P
coerce₂ = subst₂ (λ δ Δ → [[ δ ]] ++ Δ ⊢ σ ∋ u ⊠ ]] δ [[ ++ _) eq₂ (cong proj₂ eq₁)
eq₃ = functionalCheckPost _ (coerce₂ (let-inv-body (CHECK.proof q))) U
in ¬q (_ , sym eq₃)
... | yes (ξ , eq) rewrite eq = yes (_ , `let P ∷= T `in U)
check Γ 𝟙 `unit = yes (Γ , `unit)
check Γ (κ k) `unit = no (λ { (_ , ()) })
check Γ 𝟘 `unit = no (λ { (_ , ()) })
check Γ (σ ⊗ τ) `unit = no (λ { (_ , ()) })
check Γ (σ ─o τ) `unit = no (λ { (_ , ()) })
check Γ (σ & τ) `unit = no (λ { (_ , ()) })
check Γ (σ ⊕ τ) `unit = no (λ { (_ , ()) })
check Γ (σ ─o τ) (`lam b)
with check ([ σ ] ∷ Γ) τ b
... | no ¬p = no $ λ p → ¬p (_ , lam-inv (CHECK.proof p))
... | yes ([ .σ ] ∷ Δ , p) = no λ q → case functionalCheckPost _ p (lam-inv $ CHECK.proof q) of λ ()
... | yes (] .σ [ ∷ Δ , p) = yes (Δ , `lam p)
check Γ 𝟙 (`lam b) = no $ λ p → case CHECK.proof p of λ ()
check Γ 𝟘 (`lam b) = no $ λ p → case CHECK.proof p of λ ()
check Γ (σ & τ) (`lam b) = no $ λ p → case CHECK.proof p of λ ()
check Γ (σ ⊕ τ) (`lam b) = no $ λ p → case CHECK.proof p of λ ()
check Γ (σ ⊗ τ) (`lam b) = no $ λ p → case CHECK.proof p of λ ()
check Γ (κ n) (`lam b) = no $ λ p → case CHECK.proof p of λ ()
check Γ (σ ⊗ τ) (`prd t u)
with check Γ σ t
... | no ¬p = no $ λ p → ¬p (_ , prd-inv-fst (CHECK.proof p))
... | yes (θ , T)
with check θ τ u
... | no ¬p = no $ λ p → let eq = functionalCheckPost _ (prd-inv-fst (CHECK.proof p)) T
coerce = subst (_⊢ τ ∋ u ⊠ _) eq
in ¬p (_ , coerce (prd-inv-snd (CHECK.proof p)))
... | yes (Δ , U) = yes (Δ , `prd⊗ T U)
check Γ (σ & τ) (`prd t u)
with check Γ σ t | check Γ τ u
... | no ¬p | _ = no $ λ p → ¬p (_ , proj₁ (prd&-inv (CHECK.proof p)))
... | _ | no ¬q = no $ λ p → ¬q (_ , proj₂ (prd&-inv (CHECK.proof p)))
... | yes (Θ₁ , p) | yes (Θ₂ , q)
with eqs Θ₁ Θ₂
... | no ¬eq = no $ λ pq →
let (p′ P., q′) = prd&-inv (CHECK.proof pq)
eqp = functionalCheckPost _ p p′
eqq = functionalCheckPost _ q q′
in ¬eq (trans eqp (sym eqq))
... | yes eq rewrite eq = yes (Θ₂ , `prd& p q)
check Γ 𝟙 (`prd t u) = no $ λ p → case CHECK.proof p of λ ()
check Γ 𝟘 (`prd t u) = no $ λ p → case CHECK.proof p of λ ()
check Γ (σ ⊕ τ) (`prd t u) = no $ λ p → case CHECK.proof p of λ ()
check Γ (σ ─o τ) (`prd t u) = no $ λ p → case CHECK.proof p of λ ()
check Γ (κ n) (`prd t u) = no $ λ p → case CHECK.proof p of λ ()
check Γ (σ ⊕ τ) (`inl t) = checkInl Γ t σ τ <$> check Γ σ t
check Γ 𝟙 (`inl t) = no $ λ p → case CHECK.proof p of λ ()
check Γ 𝟘 (`inl t) = no $ λ p → case CHECK.proof p of λ ()
check Γ (σ ⊗ τ) (`inl t) = no $ λ p → case CHECK.proof p of λ ()
check Γ (σ ─o τ) (`inl t) = no $ λ p → case CHECK.proof p of λ ()
check Γ (σ & τ) (`inl t) = no $ λ p → case CHECK.proof p of λ ()
check Γ (κ n) (`inl t) = no $ λ p → case CHECK.proof p of λ ()
check Γ (σ ⊕ τ) (`inr t) = checkInr Γ t σ τ <$> check Γ τ t
check Γ 𝟙 (`inr t) = no $ λ p → case CHECK.proof p of λ ()
check Γ 𝟘 (`inr t) = no $ λ p → case CHECK.proof p of λ ()
check Γ (σ ⊗ τ) (`inr t) = no $ λ p → case CHECK.proof p of λ ()
check Γ (σ ─o τ) (`inr t) = no $ λ p → case CHECK.proof p of λ ()
check Γ (σ & τ) (`inr t) = no $ λ p → case CHECK.proof p of λ ()
check Γ (κ n) (`inr t) = no $ λ p → case CHECK.proof p of λ ()