{-# OPTIONS --allow-unsolved-metas #-}

open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_)

module Syntax

  {{ Α : Set }} -- Alpha, type-level constants
  {{ C : Set }} -- C, term-level constants

  {{ Var : Set }} -- term variables
  {{ decEqVar : Decidable (_≡_ {A = Var}) }}


  {{ Κ : Set }} -- proof term symbols

  where

import LF
open LF
  {{ Α }} -- Alpha, type-level constants
  {{ C }} -- C, term-level constants

  {{ Var }} -- term variables
  {{ decEqVar }}
  public

-- Definite clauses and Goals
mutual
  data De : Set where
    at : T → De
    _⇒_ : Go → De → De
    ∀De : Var → T → De → De 

  data Go : Set where
    at : T → Go
    _⇒_ : De → Go → Go
    ∃Go : Var → T → Go → Go
    ∀Go : Var → T → Go → Go

-- We define substitution on Definite clauses and Goal

open import Relation.Nullary using (yes ; no)

_[_/_]De : De → t → Var → De
_[_/_]Go : Go → t → Var → Go

at A [ M / x ]Go = at (A [ M / x ]T)
(D ⇒ G) [ M / x ]Go = (D [ M / x ]De) ⇒ (G [ M / x ]Go)
∃Go x' A G [ M / x ]Go with decEqVar x x'
... | yes _ = ∃Go x' A G
... | no _  = ∃Go x' (A [ M / x ]T) (G [ M / x ]Go) 
∀Go x' A G [ M / x ]Go -- with decEqVar x x'
-- ... | yes _ = ∀Go x' A G
-- ... | no _  = ∀Go x' (A [ M / x ]T) (G [ M / x ]Go) 
  = ∀Go x' (A [ M / x ]T) (G [ M / x ]Go) --assume always fresh
  
at A [ M / x ]De = at (A [ M / x ]T)
(G ⇒ D) [ M / x ]De = (G [ M / x ]Go) ⇒ (D [ M / x ]De)
∀De x' A D [ M / x ]De -- with decEqVar x x'
--... | yes _ = ∀De x' A D
--... | no _  = ∀De x' (A [ M / x ]T) (D [ M / x ]De) 
  = ∀De x' (A [ M / x ]T) (D [ M / x ]De) -- assume always fresh

open import Relation.Binary.PropositionalEquality using (refl ; cong ; cong₂)

de-eq-helper : ∀ {D x } →  (D [ var x / x ]De) ≡ D
de-eq-helper {at x} = {!!}
de-eq-helper {x ⇒ D} = cong₂ _⇒_ {!!} de-eq-helper
-- de-eq-helper {∀De y A D} {x} with decEqVar x y
-- de-eq-helper {∀De y A D} {x} | yes p = refl
-- de-eq-helper {∀De y A D} {x} | no ¬p = cong₂ (∀De y) {!!} de-eq-helper
de-eq-helper {∀De y A D} {x} = cong₂ (∀De y) {!!} de-eq-helper


-- big substitution application
_ΘGo_ : ∀ {S Γ Γ'} → Θ S Γ Γ' → Go → Go
_ΘDe_ : ∀ {S Γ Γ'} → Θ S Γ Γ' → De → De

θ ΘGo at A = at (θ ΘT A)
θ ΘGo (D ⇒ G) = (θ ΘDe D) ⇒ (θ ΘGo G)
θ ΘGo ∃Go x A G = ∃Go x (θ ΘT A) (θ ΘGo G)
θ ΘGo ∀Go x A G = ∀Go x (θ ΘT A) (θ ΘGo G)

θ ΘDe at A = at (θ ΘT A)
θ ΘDe (G ⇒ D) = (θ ΘGo G) ⇒ (θ ΘDe D)
θ ΘDe ∀De x A D = ∀De x (θ ΘT A) (θ ΘDe D)



{- well-formednes of definite clauses and goals -}

mutual
  data _+_⊢_∷De : Sig → Ctx → De → Set where

    at-de : ∀ {S Γ A} → S + Γ ⊢ A ∷T o → S + Γ ⊢ at A ∷De
    ⇒-de : ∀ {S Γ G D} → S + Γ ⊢ G ∷Go → S + Γ ⊢ D ∷De → S + Γ ⊢ G ⇒ D ∷De
    ∀-de : ∀ {S Γ x A D} → S + (Γ , x ∷ A ) ⊢ D ∷De → S + Γ ⊢ ∀De x A D ∷De

  data _+_⊢_∷Go : Sig → Ctx → Go → Set where
    at-go : ∀ {S Γ A} → S + Γ ⊢ A ∷T o → S + Γ ⊢ at A ∷Go
    ⇒-go : ∀ {S Γ G D} → S + Γ ⊢ D ∷De → S + Γ ⊢ G ∷Go → S + Γ ⊢ D ⇒ G ∷Go
    ∃-go : ∀ {S Γ x A G} → S + (Γ , x ∷ A ) ⊢ G ∷Go → S + Γ ⊢ ∃Go x A G ∷Go
    ∀-go : ∀ {S Γ x A G} → S + (Γ , x ∷ A ) ⊢ G ∷Go → S + Γ ⊢ ∀Go x A G ∷Go


open import Data.Empty

de-stab : ∀ {S : Sig} {Γ : Ctx} {D : De} {x : Var} {M : t} {A : T}→
      S + Γ ⊢ D ∷De →
      (x ∷ A ∈ Γ → ⊥) →
      S + Γ ⊢ D [ M / x ]De ∷De

go-stab : ∀ {S : Sig} {Γ : Ctx} {G : Go} {x : Var} {M : t} {A : T} →
      S + Γ ⊢ G ∷Go →
      (x ∷ A ∈ Γ → ⊥) →
      S + Γ ⊢ G [ M / x ]Go ∷Go

de-stab (at-de x₁) nin = at-de {!!}
de-stab (⇒-de x₁ wf) nin = ⇒-de (go-stab x₁ nin) (de-stab wf nin)
de-stab (∀-de wf) nin = ∀-de {!!}

go-stab (at-go x₁) nin = at-go {!!}
go-stab (⇒-go x₁ wf) nin = ⇒-go (de-stab x₁ nin) (go-stab wf nin)
go-stab (∃-go wf) nin = {!!}
go-stab (∀-go wf) nin = {!!} -- ∀-go ({!!})



open import Relation.Binary.PropositionalEquality


--congruence
{-
unit-ε-Go : {G : Go} → ε ΘGo G ≡ G
unit-ε-De : {D : De} → ε ΘDe D ≡ D

unit-ε-Go {G = at A} = cong (λ A' → at A') unit-ε-T -- unit-ε-T
unit-ε-Go {G = D ⇒ G} = cong₂ (λ D' G' → D' ⇒ G') unit-ε-De unit-ε-Go
unit-ε-Go {G = ∃Go x A G} = cong₂ (λ A' G' → ∃Go x A' G') unit-ε-T unit-ε-Go
unit-ε-Go {G = ∀Go x A G} = cong₂ (λ A' G' → ∀Go x A' G') unit-ε-T unit-ε-Go

unit-ε-De {D = at A} = cong (λ A' → at A') unit-ε-T -- unit-ε-T
unit-ε-De {D = G ⇒ D} = cong₂ (λ G' D' → G' ⇒ D') unit-ε-Go unit-ε-De
unit-ε-De {D = ∀De x A D} = cong₂ (λ A' D' → ∀De x A' D') unit-ε-T unit-ε-De
-}

open import Data.Product

unit-ε-De : ∀  {D : De} {S} {Γ'} →
       (_ΘDe_ {S = S} {Γ = Γ'} {Γ' = Γ'  } (λ {X} → var X , wf-var)  D) ≡ D
unit-ε-Go : ∀  {G : Go} {S} {Γ'} →
       (_ΘGo_ {S = S} {Γ = Γ'} {Γ' = Γ'} (λ {X} → var X , wf-var) G) ≡ G
       
unit-ε-De {at x} = {!!}
unit-ε-De {x ⇒ D} = cong₂ (λ x₁ x₂ → x₁ ⇒ x₂) unit-ε-Go unit-ε-De
unit-ε-De {∀De x x₁ D} = cong₂ (λ x₂ x₃ → ∀De x x₂ x₃) {!!} unit-ε-De

unit-ε-Go {at x} = {!!}
unit-ε-Go {x ⇒ G} = cong₂ (λ x₁ x₂ → x₁ ⇒ x₂) unit-ε-De unit-ε-Go
unit-ε-Go {∃Go x x₁ G} = cong₂ (λ x₂ x₃ → ∃Go x x₂ x₃) {!!} unit-ε-Go
unit-ε-Go {∀Go x x₁ G} = cong₂ (λ x₂ x₃ → ∀Go x x₂ x₃) {!!} unit-ε-Go

-- we define Programs
data Prog : Set where
  · : Prog
  _,_∷_ : Prog → Κ → De → Prog

-- Helper predicate where κ ∷ D is in program P

data _∷_∈P_ : Κ → De → Prog → Set where
  here : {κ : Κ} {D : De} {P : Prog} →
    κ ∷ D ∈P (P , κ ∷ D) 
  there : {κ κ' : Κ} {D D' : De} {P : Prog} →
    κ ∷ D ∈P P → 
    κ ∷ D ∈P (P , κ' ∷ D') 


open import Data.Empty


-- Well-fromedness of programs is constructed from given well-formedness of types
open import Data.Empty

data _⊢prog_ : Sig → Prog → Set where

  ·-prog : {S : Sig} → ⊢ S → S ⊢prog ·

  ,∷-prog : {S : Sig } {P : Prog} {κ : Κ } {D : De} →
    S ⊢prog P →
    S + · ⊢ D ∷De →
    (∀ {D'} → κ ∷ D' ∈P P → ⊥ )→
    S ⊢prog (P , κ ∷ D)  


{- implicit validity -}
impl-val-sig : {S : Sig} {P : Prog} →
  S ⊢prog P →
  ⊢ S
impl-val-sig (·-prog x) = x
impl-val-sig (,∷-prog prog x x₁) = impl-val-sig prog


{- implicit validity -}
strenghten-val-sig : {S : Sig} {P : Prog} {c : C} {A : T} →
  (S , c ∷T A) ⊢prog P →
  S ⊢prog P
strenghten-val-sig (·-prog (,∷-wfctx-c x x₁)) = ·-prog x
strenghten-val-sig (,∷-prog wf x x₁) = ,∷-prog {!!} {!!} {!!}


{- implicit validity -}
prog-weaken-sig : {S : Sig} {P : Prog} {c : C} {A : T} →
  S ⊢prog P →
  ⊢ (S , c ∷T A) →
  (S , c ∷T A) ⊢prog  P
prog-weaken-sig {P = ·} wfP wfS = ·-prog wfS
prog-weaken-sig {P = P , x ∷ x₁} (,∷-prog wfP x₂ x₃) wfS = ,∷-prog (prog-weaken-sig wfP wfS) {!trm-weaken-sig!} x₃



prog-stab : ∀ {S : Sig} {P : Prog} {D : De} {x : Var} {M : t} {κ : Κ} →
      S ⊢prog (P , κ ∷ D) →
      S ⊢prog (P , κ ∷ (D [ M / x ]De))

prog-stab (,∷-prog wf x₁ x₂)  = ,∷-prog wf (de-stab x₁ (λ { () } )) x₂




-- Proof terms

data PT : Set where
  symbP : Κ → PT
  _apP_ : PT → PT → PT
  <_,_>P : t → PT → PT
  lamP : Κ → PT → PT

open import Data.Product using (_×_ ; _,_ )

inspect-ap : {e₁ e₂ : PT} {ê₁ ê₂ : PT} →
  e₁ apP ê₁ ≡ e₂ apP ê₂ →
  e₁ ≡ e₂ × ê₁ ≡ ê₂
inspect-ap refl = refl , refl

inspect-<> : {M₁ M₂ : t} {ê₁ ê₂ : PT} →
  < M₁ , ê₁ >P ≡ < M₂ , ê₂ >P →
  M₁ ≡ M₂ × ê₁ ≡ ê₂
inspect-<> refl = refl , refl

inspect-lam : {κ₁ κ₂ : Κ} {ê₁ ê₂ : PT} →
  lamP κ₁ ê₁ ≡ lamP κ₂ ê₂ →
  κ₁ ≡ κ₂ × ê₁ ≡ ê₂
inspect-lam refl = refl , refl


-- Substitution of proof terms

_[_/_]PT : PT → t → Var → PT
symbP κ [ M / x ]PT = symbP κ
(e apP e') [ M / x ]PT = (e [ M / x ]PT) apP (e' [ M / x ]PT)
< M , e >P [ N / x ]PT = < M [ N / x ]t , e [ N / x ]PT >P
lamP κ e [ M / x ]PT = lamP κ (e [ M / x ]PT)


{-
mutual
  data _+_+_⊢PT_∷De_ : Sig → Prog → Ctx → PT → De → Set where

    wf-symbP-de : ∀ {S P Γ κ D} → S ⊢prog P → κ ∷ D ∈P P → S + P + Γ ⊢PT (symbP κ) ∷De D

    wf-apP-de : ∀ {S P Γ e e' G D} → S + P + Γ ⊢PT e ∷De (G ⇒ D) → S + P + Γ ⊢PT e' ∷Go G  →  S + P + Γ ⊢PT e apP e' ∷De D


    wf-forallP-de : ∀ {S P Γ x A₁ D e}  → S + P + ( Γ , x ∷ A₁ ) ⊢PT e  ∷De D  → S + P + Γ ⊢PT e ∷De ∀De x A₁ D 


  data _+_+_⊢PT_∷Go_ : Sig → Prog → Ctx → PT → Go → Set where

    wf-symbP-go : ∀ {S P Γ κ A} → S ⊢prog P → κ ∷ (at A) ∈P P → S + P + Γ ⊢PT (symbP κ) ∷Go (at A)

    wf-existsP-de : ∀ {S P Γ x A₁ G e M}  →  S + P + (Γ , x ∷ A₁) ⊢PT e ∷Go G  → S + · ⊢ M ∷ A₁
      → S + P + Γ ⊢PT < M , e >P ∷Go ∃Go x A₁ G


impl-val-ptde : {S : Sig} {P : Prog} {Γ : Ctx} {e : PT} {D : De} →
  S + P + Γ ⊢PT e ∷De D →
  S ⊢prog P

impl-val-ptde (wf-symbP-de wf _) = wf
impl-val-ptde (wf-apP-de wf _) = impl-val-ptde wf
impl-val-ptde (wf-forallP-de wf) = impl-val-ptde wf

subst-de : {S : Sig} {P : Prog} {Γ : Ctx} {e : PT} {x : Var} {A : T} {M : t} {D : De} →
  S + P + Γ , x ∷ A  ⊢PT e ∷De D →
  S + · ⊢ M ∷ A →
  S + P + · ⊢PT e ∷De (D [ M / x ]De)

subst-de = {!!}

subst-de' : {S : Sig} {P : Prog} {Γ : Ctx} {e : PT} {x : Var} {A : T} {M : t} {D : De} →
  S + P + Γ  ⊢PT e ∷De ∀De x  A  D →
  S + · ⊢ M ∷ A →
  S + P + Γ ⊢PT e ∷De (D [ M / x ]De)
subst-de' = {!!}


subst-go : {S : Sig} {P : Prog} {Γ : Ctx} {e : PT} {x : Var} {A : T} {M : t} {G : Go} →
  S + P + Γ , x ∷ A ⊢PT e ∷Go G →
  S + · ⊢ M ∷ A →
  S + P + · ⊢PT e ∷Go (G [ M / x ]Go)

subst-go = {!!}
-}