plutils

programming language utilities
git clone git://git.rr3.xyz/plutils
Log | Files | Refs | Submodules

DeBruijn.hs (2970B)

      1 module PlUtils.DeBruijn (
      2     Depth (..),
      3     Index (..),
      4     Level (..),
      5     descend,
      6     idxInBounds,
      7     lvlInBounds,
      8     assertIdxInBounds,
      9     assertLvlInBounds,
     10     idxToLvl,
     11     lvlToIdx,
     12 ) where
     13 
     14 import Naturals.Nat
     15 
     16 import PlUtils.Util
     17 
     18 --------------------------------------------------------------------------------
     19 -- Indices and levels
     20 
     21 -- | A @Nat@ representing the number of free variables in some context.
     22 newtype Depth = Depth {unDepth :: Nat} deriving (Show, Eq)
     23 
     24 -- | A de Bruijn index represented as a @Nat@, that is, an index into a context
     25 -- "from the right", such that the innermost free variable gets index 0.
     26 newtype Index = Index {unIndex :: Nat} deriving (Show, Eq)
     27 
     28 -- | A de Bruijn level represented as a @Nat@, that is, an index into a context
     29 -- "from the left", such that the outermost free variable gets index 0.
     30 newtype Level = Level {unLevel :: Nat} deriving (Show, Eq)
     31 
     32 descend :: Depth -> (Level, Depth)
     33 descend (Depth d) = assert (d < maxBound) "PlUtils: depth overflow" (Level d, Depth (d + 1))
     34 
     35 idxInBounds :: Depth -> Index -> Bool
     36 idxInBounds (Depth d) (Index i) = i < d
     37 
     38 lvlInBounds :: Depth -> Level -> Bool
     39 lvlInBounds (Depth d) (Level l) = l < d
     40 
     41 assertIdxInBounds :: Depth -> Index -> a -> a
     42 assertIdxInBounds d i = assert (idxInBounds d i) "PlUtils: index out of bounds"
     43 
     44 assertLvlInBounds :: Depth -> Level -> a -> a
     45 assertLvlInBounds d l = assert (lvlInBounds d l) "PlUtils: level out of bounds"
     46 
     47 idxToLvl :: Depth -> Index -> Level
     48 idxToLvl d i = assertIdxInBounds d i $ Level (unDepth d - unIndex i - 1)
     49 
     50 lvlToIdx :: Depth -> Level -> Index
     51 lvlToIdx d l = assertLvlInBounds d l $ Index (unDepth d - unLevel l - 1)
     52 
     53 --------------------------------------------------------------------------------
     54 -- TODO
     55 
     56 {-
     57 Data structures required for elaboration of surface (shadowing names) to
     58 core (de Bruijn indices):
     59 
     60 ULC (standard):
     61     Depth: `Nat` (Peano-indexed?)
     62     VarMap: `ShadowMap Name Level` OR `ShadowMap Name Value`
     63         The latter provides a convenient way to implement predeclared names.
     64 STLC (no type variables):
     65     Depth: `Nat`
     66     DVarMap: `ShadowMap DName (DLevel, Type)` OR `ShadowMap DName (DValue, Type)`
     67 STLC/PLC (type variables but no higher kinds):
     68     Depth: `Nat`
     69     DVarMap: `ShadowMap DName (DLevel, Type)` OR `ShadowMap DName (DValue, Type)`
     70     SVarMap: `ShadowMap SName SLevel` OR `ShadowMap SName SValue`
     71 STLC/HOPLC (type variables and higher kinds):
     72     Depth: `Nat`
     73     DVarMap: `ShadowMap DName (DLevel, Type)` OR `ShadowMap DName (DValue, Type)`
     74     SVarMap: `ShadowMap SName (SLevel, Kind)` OR `ShadowMap SName (SValue, Kind)`
     75 -}
     76 
     77 {-
     78 TODO: Do same thing but with evaluation.
     79 TODO: Do we need to carry a substitution on static variables during elaboration?
     80 This is what I've done in the past, but I don't think it's necessary. At times
     81 when we need to evaluate during elaboration, we can just convert the elaboration
     82 context to an evaluation environment with an empty substitution.
     83 -}