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

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


module BigSem
  {{ Α : Set }}    -- type level constants
  {{ C : Set }}    -- term level constants

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


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

  where

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

  {{ Var }} -- term variables
  {{ decEqVar }} -- unification variables
-}

import Syntax
open Syntax 
  {{ Α }}    -- type level constants
  {{ C }}    -- term level constants

  {{ Var }}  -- variables
  {{ decEqVar }} -- unification variables

  {{ Κ }}    -- proof term constants



-- big step op sem
mutual
  data _+_⟶_∷_  : Sig → Prog → PT → Go → Set where
    decide : {S : Sig} {P : Prog} {e : PT} {A : T} {κ : Κ} {D : De} →
      S + P - symbP κ ∷ D ⟶ e ∷ A →
      κ ∷ D ∈P P →
      S + P ⟶ e ∷ (at A)

    ∃R : {S : Sig} {P : Prog} {e : PT} {G : Go} {M : t} {A : T} {x : Var} →
      S + P ⟶ e ∷ (G [ M / x ]Go ) →
      S + · ⊢ M ∷ A →
      S + P ⟶ < M , e >P ∷ ∃Go x A G

    ⇒R : {S : Sig} {P : Prog} {κ : Κ} {e : PT} {D : De} {G : Go} →
      S + (P , κ ∷ D) ⟶ e ∷ G →
      {- κ #prog P → comes from w.f. of P , κ ∷ D -}
      S + P ⟶ (lamP κ e) ∷ (D ⇒ G)

    ∀R : {S : Sig} {P : Prog} {e : PT} {A : T} {G : Go} {x : Var} {c : C} →
     (S , c ∷T A) + P ⟶ e [ (const c) / x ]PT ∷ (G [ const c / x ]Go) →
      {- c #csig S → comes from w.f. of S -}
      S + P ⟶ e ∷ ∀Go x A G
  
  data _+_-_∷_⟶_∷_  : Sig → Prog → PT → De → PT → T → Set where

    init : {S : Sig} {P : Prog} {e : PT} {A : T} →
      -- S ⊢prog P → 
      S + P - e ∷ at A ⟶ e ∷ A


    ⇒L : {S : Sig} {P : Prog} {e e₁ e₂ : PT} {A₁ A₂ : T} {D : De} →

      S + P ⟶ e₁ ∷ at A₁ →
      S + P - e apP e₁ ∷ D ⟶ e₂ ∷ A₂ →

      S + P - e ∷ at A₁ ⇒ D  ⟶ e₂ ∷ A₂

    ∀L : {S : Sig} {P : Prog} { e e₂ : PT} {x : Var} {A₁ A₂ : T} {D : De} {M : t} →
      S + P - e ∷ D [ M / x ]De ⟶ e₂ ∷ A₂ →
      S + · ⊢ M ∷ A₁ →
      S + P - e ∷ ∀De x A₁ D ⟶ e₂ ∷ A₂


import Syntax

{-

impl-valid-big : {S : Sig} {P : Prog} {e : PT} {G : Go} →
  S + P ⟶ e ∷ G →
  S + P + · ⊢PT e ∷Go G
impl-valid-big (decide x x₁) = {!!}
impl-valid-big (∃R big wfM) = Syntax.wf-existsP-de {!subst-de!} wfM
impl-valid-big (⇒R big) = {!!}
impl-valid-big (∀R big) = {!!}
-}