    {-|
    Description      : Type-level lists.
    Copyright        : (c) Galois, Inc 2015-2019
    Maintainer       : Joe Hendrix <jhendrix@galois.com>

    This module defines type-level lists used for representing the type of
    variables in a context.

    A 'Ctx' is never intended to be manipulated at the value level; it is
    used purely as a type-level list, just like @'[]@. To see how it is
    used, see the module header for "Data.Parameterized.Context".
    -}
    {-# LANGUAGE ConstraintKinds #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE Safe #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE UndecidableInstances #-}
    module Data.Parameterized.Ctx
      ( type Ctx(..)
      , EmptyCtx
      , SingleCtx
      , (::>)
      , type (<+>)

        -- * Type context manipulation
      , CtxSize
      , CtxLookup
      , CtxUpdate
      , CtxLookupRight
      , CtxUpdateRight
      , CtxFlatten
      , CheckIx
      , ValidIx
      , FromLeft
      ) where

    import Data.Kind (Constraint)
    import GHC.TypeLits (Nat, type (+), type (-), type (<=?), TypeError, ErrorMessage(..))

    ------------------------------------------------------------------------
    -- Ctx

    type EmptyCtx = 'EmptyCtx
    type (c :: Ctx k) ::> (a::k) = c '::> a

    type SingleCtx x = EmptyCtx ::> x

    -- | Kind @'Ctx' k@ comprises lists of types of kind @k@.
    data Ctx k
      = EmptyCtx
      | Ctx k ::> k

    -- | Append two type-level contexts.
    type family (<+>) (x :: Ctx k) (y :: Ctx k) :: Ctx k where
      x <+> EmptyCtx = x
      x <+> (y ::> e) = (x <+> y) ::> e

    -- | This type family computes the number of elements in a 'Ctx'
    type family CtxSize (a :: Ctx k) :: Nat where
      CtxSize 'EmptyCtx   = 0
      CtxSize (xs '::> x) = 1 + CtxSize xs

    -- | Helper type family used to generate descriptive error messages when
    -- an index is larger than the length of the 'Ctx' being indexed.
    type family CheckIx (ctx :: Ctx k) (n :: Nat) (b :: Bool) :: Constraint where
      CheckIx ctx n 'True = ()
      CheckIx ctx n 'False = TypeError ('Text "Index "            ':<>: 'ShowType n
                                  ':<>: 'Text " out of range in " ':<>: 'ShowType ctx)

    -- | A constraint that checks that the nat @n@ is a valid index into the
    --   context @ctx@, and raises a type error if not.
    type ValidIx (n :: Nat) (ctx :: Ctx k)
      = CheckIx ctx n (n+1 <=? CtxSize ctx)

    -- | 'Ctx' is a snoc-list. In order to use the more intuitive left-to-right
    -- ordering of elements the desired index is subtracted from the total
    -- number of elements.
    type FromLeft ctx n = CtxSize ctx - 1 - n

    -- | Lookup the value in a context by number, from the right
    type family CtxLookupRight (n :: Nat) (ctx :: Ctx k) :: k where
      CtxLookupRight 0 (ctx '::> r) = r
      CtxLookupRight n (ctx '::> r) = CtxLookupRight (n-1) ctx

    -- | Update the value in a context by number, from the right.  If the index
    --   is out of range, the context is unchanged.
    type family CtxUpdateRight (n :: Nat) (x::k) (ctx :: Ctx k) :: Ctx k where
      CtxUpdateRight n x 'EmptyCtx      = 'EmptyCtx
      CtxUpdateRight 0 x (ctx '::> old) = ctx '::> x
      CtxUpdateRight n x (ctx '::> y)   = CtxUpdateRight (n-1) x ctx '::> y

    -- | Lookup the value in a context by number, from the left.
    --   Produce a type error if the index is out of range.
    type CtxLookup (n :: Nat) (ctx :: Ctx k)
      = CtxLookupRight (FromLeft ctx n) ctx

    -- | Update the value in a context by number, from the left.  If the index
    --   is out of range, the context is unchanged.
    type CtxUpdate (n :: Nat) (x :: k) (ctx :: Ctx k)
      = CtxUpdateRight (FromLeft ctx n) x ctx

    -- | Flatten a nested context
    type family CtxFlatten (ctx :: Ctx (Ctx a)) :: Ctx a where
      CtxFlatten EmptyCtx = EmptyCtx
      CtxFlatten (ctxs ::> ctx) = CtxFlatten ctxs <+> ctx