{-# OPTIONS --no-positivity-check --no-termination-check #-}
module NaPa.Examples.NBE-short where

open import  Level
open import  Function
open import  Data.Product
open import  Data.Maybe
open import  Data.Sum
open import  Data.Nat using (_+_)

open import  NaPa
open import  NaPa.Derived

module M (Abs : (World → Set) → World → Set) where
  data T α : Set where
    V    : ∀ (x : Name α) → T α
    ƛ    : ∀ (abs : Abs T α) → T α
    _·_  : ∀ (t u : T α) → T α

module MT = M SynAbs
module MS = M FunAbs
open MS renaming (T to Sem)
open MT renaming (T to Term)
-- Bug #279 force us to write these MT.* and open MT

shiftSem : Shift Sem
shiftSem k ⊆w (V a)    = V (coe ⊆w (a +nm k))
shiftSem k ⊆w (t · u)  = shiftSem k ⊆w t · shiftSem k ⊆w u
shiftSem k ⊆w (ƛ f)    = ƛ (shiftFunAbs k ⊆w f)

module NBE (envPack : ShiftableEnvPack _) where
  open ShiftableEnvPack envPack

  impEnv : ∀ {α β γ} k → α +[ k ] ⊆ β → Env (Sem α) α γ → Env (Sem β) β γ
  impEnv k ⊆w = shiftEnv k ⊆w ∘ mapEnv (shiftSem k ⊆w)

  app : ∀ {α} → Sem α → Sem α → Sem α
  app (ƛ f)  v = f  ⊆-refl v
  app n      v = n · v

  eval : ∀ {α β} → Env (Sem α) α β → Term β → Sem α
  eval Γ (ƛ t)   = ƛ (λ k ⊆w v → eval (impEnv k ⊆w Γ ,, v) t)
  eval Γ (V x)   = [ V , id ]′ (lookupEnv Γ x)
  eval Γ (t · u) = eval Γ t ⟨ app ⟩ eval Γ u

  reify : ∀ {α} → Sem α → Term α
  reify (V a)    = MT.V a
  reify (n · v)  = reify n · reify v where open MT
  reify (ƛ f)    = MT.ƛ (reify (f  ⊆-+1↑1 (V ze)))

  nf : ∀ {α β} → Env (Sem α) α β → Term β → Term α
  nf Γ = reify ∘ eval Γ

  nfC : ∀ {α} → Term α → Term α
  nfC = nf emptyEnv

  nfø : Term ø → Term ø
  nfø = nfC

open NBE shiftableFunEnv