plutils

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

Env.hs (2929B)

      1 module PlUtils.Env (
      2     Env,
      3     empty,
      4     depth,
      5     bind,
      6     idxToLvl,
      7     lvlToIdx,
      8     assign,
      9     lookup,
     10     define,
     11     eval,
     12 ) where
     13 
     14 import Control.Exception hiding (assert)
     15 import Data.IntMap (IntMap)
     16 import Data.IntMap qualified as IntMap
     17 import Data.Maybe (fromMaybe)
     18 import Prelude hiding (lookup)
     19 
     20 import PlUtils.DeBruijn
     21 
     22 -- We really ought to use natural numbers here instead of integers, but Haskell
     23 -- makes that difficult (e.g., fixed-precision natural number types are called
     24 -- "WordXX" instead of "NatXX", and there's IntMap but not NatMap).
     25 
     26 assert :: Bool -> String -> a -> a
     27 assert b s a = if b then a else throw (AssertionFailed s)
     28 
     29 -- | A collection of free variables and a substitution on them, intended for
     30 -- semantic elaboration and evaluation with semantic variables represented as
     31 -- de Bruijn levels (which are stable under weakening, so we don't need to
     32 -- modify the environment when descending under a binder) and with syntactic
     33 -- variables represented as de Bruijn indices.
     34 data Env idx val = Env Int (IntMap val) deriving (Show)
     35 
     36 empty :: (IsIndex idx, SemValue val) => Env idx val
     37 empty = Env 0 IntMap.empty
     38 
     39 depth :: (IsIndex idx, SemValue val) => Env idx val -> Int
     40 depth (Env d _) = d
     41 
     42 -- | Bind a new variable (without introducing a substitution for it).
     43 bind :: (IsIndex idx, SemValue val) => Env idx val -> (Level val, Env idx val)
     44 bind (Env d s) = assert (d < maxBound) "PlUtils.Env.bind: depth overflow" (intToLvl d, Env (d + 1) s)
     45 
     46 idxToLvl :: (IsIndex idx, SemValue val) => idx -> Env idx val -> Level val
     47 idxToLvl idx (Env d _) =
     48     let i = idxToInt idx
     49     in assert (0 <= i && i < d) "PlUtils.Env.idxToLvl: index out of range" $ intToLvl (d - i - 1)
     50 
     51 lvlToIdx :: (IsIndex idx, SemValue val) => Level val -> Env idx val -> idx
     52 lvlToIdx lvl (Env d _) =
     53     let l = lvlToInt lvl
     54     in assert (0 <= l && l < d) "PlUtils.Env.lvlToIdx: level out of range" $ intToIdx (d - l - 1)
     55 
     56 -- | Assign a value to an existing variable.
     57 assign :: (IsIndex idx, SemValue val) => Level val -> val -> Env idx val -> Env idx val
     58 assign lvl val (Env d s) =
     59     let l = lvlToInt lvl
     60     in assert (0 <= l && l < d) "PlUtils.Env.assign: level out of range" $ Env d (IntMap.insert l val s)
     61 
     62 -- | Lookup the substitution for a variable.
     63 lookup :: (IsIndex idx, SemValue val) => Level val -> Env idx val -> Maybe val
     64 lookup lvl (Env d s) =
     65     let l = lvlToInt lvl
     66     in assert (0 <= l && l < d) "PlUtils.Env.lookup: level out of range" $ IntMap.lookup l s
     67 
     68 -- | Bind and a new variable and assign a value to it.
     69 define :: (IsIndex idx, SemValue val) => (Level val -> val) -> Env idx val -> Env idx val
     70 define makeVal env =
     71     let (lvl, env') = bind env
     72     in assign lvl (makeVal lvl) env'
     73 
     74 -- | Lookup the substitution for a variable.
     75 eval :: (IsIndex idx, SemValue val) => idx -> Env idx val -> val
     76 eval idx env =
     77     let lvl = idxToLvl idx env
     78     in fromMaybe (generic lvl) (lookup lvl env)