arithexpr2

open import Function using (_∘_)
open import Data.Integer.Base as ℤ using (ℤ)
open import Data.Fin.Base as Nat using (Fin; zero; suc)
open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
open import Data.Vec.Base as Vec using (Vec; []; _∷_)
open import Data.Maybe.Base as Maybe using (Maybe; nothing; just)

private variable n m l : ℕ

data UnOp : Set where
  neg : UnOp

data BinOp : Set where
  add : BinOp

data Expr : ℕ → Set where
  pinf : Expr n
  ninf : Expr n
  lit : ℤ → Expr n
  var : Fin n → Expr n
  abs : Expr (suc n) → Expr n
  app : Expr n → Expr n → Expr n
  uop : UnOp → Expr n → Expr n
  bop : BinOp → Expr n → Expr n → Expr n

record Range (n : ℕ) : Set where
  constructor [_,_]
  field
    min max : Expr n

data Type (n : ℕ) : Set where
  int : Range n → Type n
  depfun : Type n → Type (suc n) → Type n

data univ : Set where
  expr type : univ

U[_∶_] : univ → ℕ → Set
U[_∶_] expr = Expr
U[_∶_] type = Type

private variable u : univ


|> : (Fin n → Fin m) → (Fin n → U[ u ∶ m ])
|> {u = expr} f i = var (f i)
|> {u = type} f i = int [ var (f i) , var (f i) ]

lift : U[ u ∶ m ] → U[ u ∶ suc m ]
lift {expr} pinf = pinf
lift {expr} ninf = ninf
lift {expr} (lit x) = lit x
lift {expr} (var x) = var (suc x)
lift {expr} (abs t) = abs (lift t)
lift {expr} (app t t₁) = app (lift t) (lift t₁)
lift {expr} (uop x t) = uop x (lift t)
lift {expr} (bop x t t₁) = bop x (lift t) (lift t₁)
lift {type} (int [ min , max ]) = int [ (lift min) , (lift max) ]
lift {type} (depfun t t₁) = depfun (lift t) (lift t₁)

_<|_ : (Fin n → Expr m) → (Expr n → Expr m)
_<|_ f pinf = pinf
_<|_ f ninf = ninf
_<|_ f (lit x) = lit x
_<|_ f (var x) = f x
_<|_ f (abs t) = abs ((λ { zero → |> (λ x → x) zero ; (suc x) → lift (f x)}) <| t)
_<|_ f (app t₁ t₂) = app (f <| t₁) (f <| t₂)
_<|_ f (uop x t) = uop x (f <| t)
_<|_ f (bop x t₁ t₂) = bop x (f <| t₁) (f <| t₂)

_<|ₜ_ : (∀ {u} → Fin n → U[ u ∶ m ]) → (U[ u ∶ n ] → U[ u ∶ m ])
_<|ₜ_ {u = expr } f e = f <| e
_<|ₜ_ {u = type } f (int [ min , max ]) = int [ f <| min , f <| max ]
_<|ₜ_ {u = type } f (depfun s t) = depfun (f <|ₜ s) ((λ { zero → |> (λ x → x) zero ; (suc x) → lift (f x)}) <|ₜ t)

_<>_ : (∀ {u} → Fin n → U[ u ∶ m ]) → (∀ {u} → Fin l → U[ u ∶ n ]) → (∀ {u} → Fin l → U[ u ∶ m ])
(f <> g) x = f <|ₜ g x

thin : Fin (suc n) → Fin n → Fin (suc n)
thin zero y = suc y
thin (suc x) zero = zero
thin (suc x) (suc y) = suc (thin x y)

thick : Fin (suc n) → Fin (suc n) → Maybe (Fin n)
thick zero zero = nothing
thick zero (suc y) = just y
thick {suc _} (suc x) zero = just zero
thick {suc _} (suc x) (suc y) = thick x y Maybe.>>= just ∘ suc

_for_ : Expr n → Fin (suc n) → Fin (suc n) → Expr n
(e for r) x = Maybe.maybe var e (thick r x)

_∶_for_ : Expr n → Type n → Fin (suc n) → (∀ {u} → Fin (suc n) → U[ u ∶ n ])
(e ∶ t for r) {expr} x = (e for r) x
(e ∶ t for r) {type} x = Maybe.maybe (λ e → int [ var e , var e ]) t (thick r x)

check : Fin (suc n) → U[ u ∶ (suc n) ] → Maybe (U[ u ∶ n ])
check {u = expr} r pinf = just pinf
check {u = expr} r ninf = just ninf
check {u = expr} r (lit x) = just (lit x)
check {u = expr} r (var x) = thick r x Maybe.>>= just ∘ var
check {u = expr} r (abs t) = check (suc r) t Maybe.>>= just ∘ abs
check {u = expr} r (app t t₁) = check r t Maybe.>>= λ t' → check r t₁ Maybe.>>= λ t₁' → just (app t' t₁')
check {u = expr} r (uop x t) = check r t Maybe.>>= just ∘ uop x
check {u = expr} r (bop x t t₁) = check r t Maybe.>>= λ t' → check r t₁ Maybe.>>= λ t₁' → just (bop x t' t₁')
check {u = type} r (int [ min , max ]) = check r min Maybe.>>= λ min' → check r max Maybe.>>= λ max' → just (int [ min' , max' ])
check {u = type} r (depfun t t₁) = check r t Maybe.>>= λ t' → check (suc r) t₁ Maybe.>>= λ t₁' → just (depfun t' t₁')

data Ctx : ℕ → Set where
  ∅ : Ctx zero
  _-,_ : Ctx n → Type n → Ctx (suc n)

private
  variable
    i : Fin n
    e e₁ e₂ lb lb₁ lb₂ ub ub₁ ub₂ : Expr n
    Γ : Ctx n
    t s : Type n

data _∋_∶_ : Ctx n → Fin n → Type n → Set where
  zero : (Γ -, t) ∋ zero ∶ (|> suc <|ₜ t)
  suc : Γ ∋ i ∶ t → (Γ -, s) ∋ suc i ∶ (|> suc <|ₜ t)

data _⊢_∶_ : Ctx n → Expr n → Type n → Set where
  pinf : Γ ⊢ pinf ∶ int [ pinf , pinf ]
  ninf : Γ ⊢ ninf ∶ int [ ninf , ninf ]
  lit : (l : ℤ) → Γ ⊢ lit l ∶ int [ lit l , lit l ]
  var : Γ ∋ i ∶ t → Γ ⊢ var i ∶ t
  abs : (Γ -, s) ⊢ e ∶ t → Γ ⊢ abs e ∶ depfun s t
  app : Γ ⊢ e₁ ∶ depfun s t → Γ ⊢ e₂ ∶ s → Γ ⊢ app e₁ e₂ ∶ ((e₂ ∶ s for zero) <|ₜ t)
  neg : Γ ⊢ e ∶ int [ lb , ub ] → Γ ⊢ uop neg e ∶ int [ uop neg ub , uop neg lb ]
  add : Γ ⊢ e₁ ∶ int [ lb₁ , ub₁ ] → Γ ⊢ e₂ ∶ int [ lb₂ , ub₂ ] → Γ ⊢ bop add e₁ e₂ ∶ int [ bop add lb₁ lb₂ , bop add ub₁ ub₂ ]


data _~>_ : Expr m → Expr n → Set where
  beta : app (abs e) e₁ ~> ((e₁ for zero) <| e)


subject-reduction : Γ ⊢ e ∶ t → e ~> e₁ → Γ ⊢ e₁ ∶ t
subject-reduction {Γ = Γ} (app (abs e) e₁) beta = {!!}