module MJ.Types where

open import Prelude hiding (_≟_)
open import Data.Fin.Properties as FinP using ()
open import Data.Vec
open import Data.List

open import Relation.Binary.Core
open import Relation.Nullary

data Cid (c : ℕ) : Set where
  cls : Fin c → Cid c
  Object : Cid c

_cid≟_ : ∀ {c} → Decidable (_≡_ {A = Cid c})
cls x cid≟ cls y with x FinP.≟ y
cls x cid≟ cls .x | yes refl = yes refl
cls x cid≟ cls y | no ¬p = no (λ{ refl → ¬p refl})
cls x cid≟ Object = no (λ ())
Object cid≟ cls x = no (λ ())
Object cid≟ Object = yes refl

data Ty (c : ℕ) : Set where
  void : Ty c
  int  : Ty c
  ref  : Cid c → Ty c

data Ty⁺ (c : ℕ) : Set where
  vty : Ty c → Ty⁺ c
  obj : Cid c → Ty⁺ c

World : ℕ → Set
World c = List (Ty⁺ c)

Sig : ℕ → Set
Sig c = List (Ty c) × Ty c

_≟_ : ∀ {c} → Decidable (_≡_ {A = Ty c})
void ≟ void = yes refl
void ≟ int = no (λ ())
void ≟ ref x = no (λ ())
int ≟ void = no (λ ())
int ≟ int = yes refl
int ≟ ref x = no (λ ())
ref x ≟ void = no (λ ())
ref x ≟ int = no (λ ())
ref x ≟ ref y with x cid≟ y
ref x ≟ ref y | yes p = yes (cong ref p)
ref x ≟ ref y | no ¬p = no λ{ refl → ¬p refl }