content: {-# LANGUAGE AllowAmbiguousTypes #-}
  {-# LANGUAGE LambdaCase #-}
  
  -- https://github.com/AndrasKovacs/elaboration-zoo/blob/master/01-eval-closures-debruijn/Main.hs
  
  -- This implementation relies on the laziness of Haskell to implement call-by-need normal order evaluation.
  
  -- SCW added well-scoped expressions to keep track of DeBruijn indices
  -- and levels.
  
  module NBE.Lazy.KovacsScoped where
  
  import Data.Type.Equality
  import Unsafe.Coerce (unsafeCoerce)
  import Util.IdInt
  import Util.Impl
  import Util.Nat
  import Util.Syntax.ScopedDeBruijn
  import qualified Util.Vec as V
  import Prelude hiding (length, lookup)
  
  impl :: LambdaImpl
  impl =
    LambdaImpl
      { impl_name = "NBE.Lazy.KovacsScoped",
        impl_fromLC = toDB,
        impl_toLC = fromDB,
        impl_nf = nf,
        impl_nfi = error "undefiend",
        impl_aeq = (==)
      }
  
  -- | de Bruijn index, type ensures within scope
  -- used in terms
  -- offset from the end of the context/environment
  --  A, B, C |- 0 : C
  -- terms must be updated (shifted) if context/scope is weakened/strengthened
  type Ix = Idx
  
  -- | de Bruijn level, used in values
  -- offset from the beginning of the context/environment
  -- A, B, C |- 0 : A
  -- values never need to be shifted
  type Lvl = Int
  
  -- | An environment provides definitions for *indices* and maps them
  -- to values. Values only refer to levels.
  -- n is the number of definitions in the environment
  data Env (n :: Nat) where
    Nil :: Env 'Z
    -- | Lazy RHS is essential for cbn evaluation
    Define :: Env n -> Val -> Env ('S n)
  
  -- | Representation of terms using de bruijn levels
  -- and closures (i.e. delayed substitutions) for
  -- abstractions
  -- This could be related to locally nameless
  -- representation, which works with "locally closed" terms
  -- only.
  data Val
    = VVar Lvl
    | -- | Original version had lazy argument, but that is not needed
      VApp Val Val
    | -- | existential in closure prevents unpacking, so we
      -- do it manually here
      -- Lambdas are "locally closed" all external bound variables
      -- in the term must have been substituted with values
      forall n. VLam (Env n) (Term ('S n))
    | VBool {-# UNPACK #-} !Bool
    | forall n. VIf Val (Env n) (Term n) (Term n)
  -- | Count bindings in the environment
  -- recovers the runtime value from the compiletime only version
  -- original version was tail recursive. But that is more difficult
  -- to type check.
  length :: Env n -> SNat n
  length Nil = SZ
  length (Define e _) = SS (length e)
  
  
  -- | lookup a value in the environment, based on an *index*
  lookupIx :: Ix n -> Env n -> Val
  lookupIx FZ (Define _env v) = v
  lookupIx (FS x) (Define env _) = lookupIx x env
  
  -- | Apply a closure (i.e. env + term) to a value
  cApp :: (Env n) -> (Term ('S n)) -> Val -> Val
  cApp env t ~u = eval (Define env u) t
  
  eval :: forall n. Env n -> Term n -> Val
  eval env = \case
    DVar x -> lookupIx x env
    DApp t u -> case (eval env t) of
      (VLam e0 t0) -> eval (Define e0 (eval env u)) t0
      t0 -> VApp t0 (eval env u)
    DLam t -> VLam env t
    DBool b -> VBool b
    DIf t u v -> case (eval env t) of
      VBool True -> eval env u
      VBool False -> eval env v
      t0 -> VIf t0 env u v
  -- | Convert a value to to a term by translating
  -- all level-based vars to index-based vars
  quote :: forall l. SNat l -> Val -> Term l
  quote l = \case
    VVar x -> DVar (lvl2Ix x l)
    VApp t u -> DApp (quote l t) (quote l u)
    VLam t e -> DLam (quote (SS l) (cApp t e (VVar vl)))
      where
        vl :: Lvl
        vl = sNat2Int l
    VBool b -> DBool b
    VIf t env u v -> 
      DIf (quote l t) (quote l (eval env u)) (quote l (eval env v))
  
  -- Normalization
  --------------------------------------------------------------------------------
  
  -- | invert the reference to the environment
  -- switching between indices and levels
  -- i.e.  lvl2Ix x n = n - x - 1
  -- unfortunately linear time instead of constant time.
  -- but adds minimal overhead.
  lvl2Ix :: forall n. Int -> SNat n -> Ix n
  lvl2Ix x l = toIdx l (sNat2Int l - x - 1)
  
  nf' :: Env n -> Term n -> Term n
  nf' env t = quote (length env) (eval env t)
  
  nf :: Term 'Z -> Term 'Z
  nf t = quote SZ (eval Nil t)