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