modal

box.agda

module modal where

open import Data.Unit
open import Data.Nat
open import Data.Product
open import Data.String
open import Data.Bool

open import Agda.Builtin.String

data ty : Set where 
    𝕌 : ty
    _⇒_ _&_ : ty → ty → ty

data tm : Set where 
    var : String → tm 
    _●_ _,_ : tm → tm → tm
    π₁ π₂ : tm → tm
    ƛ_∷_∙_ : String → ty → tm → tm 
    u : tm
    -- adding box modality
    □ : tm → tm
    let□_≣_inn_ : tm → String → tm → tm

data _value : tm → Set where 
    ƛV : ∀ {x T t} → (ƛ x ∷ T ∙ t) value
    &V : ∀{t1 t2} → t1 value → t2 value → (t1 , t2) value
    uV : u value
    □V : ∀{t} → (□ t) value
 
_=ₛ_ : String → String → Bool 
_=ₛ_ = primStringEquality

[_/_]_ : tm → String → tm → tm
[ s / x ] t@(var y) = if (x =ₛ y) then s else t
[ s / x ] (t ● t') = ([ s / x ] t) ● ([ s / x ] t')
[ s / x ] (π₁ t') = π₁ ([ s / x ] t')
[ s / x ] (π₂ t') = π₂ ([ s / x ] t')
[ s / x ] (t , t') = [ s / x ] t , [ s / x ] t'
[ s / x ] t@(ƛ y ∷ T ∙ t') = if (x =ₛ y) then t else (ƛ x ∷ T ∙ [ s / x ] t')
[ s / x ] u = u
-- adding box modality
[ s / x ] t@(□ d) = t
[ s / x ] (let□ d ≣ x₁ inn d₁) = {!   !}

data _⟶_ : tm → tm → Set where
    st-ƛ : ∀{A N M x} → M value → ((ƛ x ∷ A ∙ N) ● M) ⟶ ([ M / x ] N)
    st-&₁ : ∀{M N} → M value → N value → (π₁(M , N)) ⟶ M 
    st-&₂ : ∀{M N} → M value → N value → (π₂(M , N)) ⟶ N
    st-&c₁ : ∀{M M' N} → (M ⟶ M') → (M , N) ⟶ (M' , N) 
    st-&c₂ : ∀{M N N'} → M value → (N ⟶ N') → (M , N) ⟶ (M , N')
    st-π₁c : ∀{M M'} → M ⟶ M' → (π₁ M) ⟶ (π₁ M')
    st-π₂c : ∀{M M'} → M ⟶ M' → (π₂ M) ⟶ (π₂ M')
    st-●c₁ : ∀{M M' N} → M ⟶ M' → (M ● N) ⟶ (M' ● N)
    st-●c₂ : ∀{M N N'} → M value → N ⟶ N' → (M ● N) ⟶ (M ● N')

data multi {X : Set}(R : X → X → Set) : X → X → Set where
    mrefl : ∀{x : X} → multi R x x 
    mstep : ∀ { x y z : X} → R x y → multi R y z → multi R x z

_~>*_ : tm → tm → Set 
t ~>* t' = multi _⟶_ t t'

_ : ((ƛ "x"  ∷ 𝕌 ∙ var "x") ● π₁ (u , u)) ~>* u
_ = mstep (st-●c₂ ƛV (st-&₁ uV uV)) 
    (mstep (st-ƛ uV) 
     mrefl)