Environment.hs (2024B)
1 module Environment where 2 import Data.IntMap.Strict (IntMap) 3 import qualified Data.IntMap.Strict as IntMap 4 5 import Common 6 7 -- Env represents a collection of free variables and a substitution on them. 8 -- Free variables are represented using de Bruijn levels, and there must be 9 -- an injection `generic` (as in "generic value") for turning levels into 10 -- values. The terms which Env tracks free variables of should use de Bruijn 11 -- indices, and Env is indexed by an `idx` type, so that multiple de Bruijn 12 -- syntaxes may be handled without accidentally confusing indices and levels 13 -- from different syntaxes. 14 15 class Value a where 16 type Level a 17 generic :: Level a -> a 18 19 type Env' idx val = (IsInt idx, IsInt (Level val), Value val) 20 data Env idx val = Env Int (IntMap val) 21 22 empty :: Env' idx val => Env idx val 23 empty = Env 0 IntMap.empty 24 25 bind :: Env' idx val => Env idx val -> (Level val, Env idx val) 26 bind (Env size map) = (fromInt size, Env (size + 1) map) 27 28 idxToLvl :: Env' idx val => idx -> Env idx val -> Level val 29 idxToLvl idx (Env size _) = 30 if toInt idx >= size then 31 error "Env.idxToLvl: index out of range" 32 else 33 fromInt $ size - toInt idx - 1 34 35 lvlToIdx :: Env' idx val => Level val -> Env idx val -> idx 36 lvlToIdx lvl (Env size _) = 37 if toInt lvl >= size then 38 error "Env.lvlToIdx: level out of range" 39 else 40 fromInt $ size - toInt lvl - 1 41 42 define :: Env' idx val => Level val -> val -> Env idx val -> Env idx val 43 define lvl val (Env size map) = 44 if toInt lvl >= size then 45 error "Env.define: level out of range" 46 else 47 Env size (IntMap.insert (toInt lvl) val map) 48 49 bindAndDefine :: Env' idx val => val -> Env idx val -> (Level val, Env idx val) 50 bindAndDefine val env = 51 let (lvl, env') = bind env 52 in (lvl, define lvl val env') 53 54 subst :: Env' idx val => Level val -> Env idx val -> Maybe val 55 subst lvl (Env size map) = 56 if toInt lvl >= size then 57 error "Env.subst: level out of range" 58 else 59 IntMap.lookup (toInt lvl) map