plutils

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

Environment.hs (1973B)

      1 module PlUtils.Environment (
      2     Environment,
      3     empty,
      4     depth,
      5     bind,
      6     assign,
      7     lookup,
      8     define,
      9     eval,
     10 ) where
     11 
     12 import Data.Maybe (fromMaybe)
     13 import Naturals.NatMap (NatMap)
     14 import Naturals.NatMap qualified as NatMap
     15 import Prelude hiding (lookup)
     16 
     17 import PlUtils.DeBruijn
     18 
     19 -- | A collection of free variables and a substitution on them, intended for
     20 -- evaluation with semantic variables represented as de Bruijn levels (which are
     21 -- stable under weakening, so we don't need to modify the environment when
     22 -- descending under a binder) and with syntactic variables represented as
     23 -- de Bruijn indices.
     24 data Environment v = Environment Depth (NatMap v) deriving (Show)
     25 
     26 empty :: Environment v
     27 empty = Environment (Depth 0) NatMap.empty
     28 
     29 depth :: Environment v -> Depth
     30 depth (Environment d _) = d
     31 
     32 -- | Bind a new variable (without introducing a substitution for it).
     33 bind :: Environment v -> (Level, Environment v)
     34 bind (Environment d s) =
     35     let (l, d') = descend d
     36     in (l, Environment d' s)
     37 
     38 weaken :: Environment v -> Environment v
     39 weaken = snd . bind
     40 
     41 -- | Assign a value to an existing variable.
     42 assign :: Level -> v -> Environment v -> Environment v
     43 assign l v (Environment d s) = assertLvlInBounds d l $ Environment d (NatMap.insert (unLevel l) v s)
     44 
     45 -- | Lookup the substitution for a variable.
     46 lookup :: Level -> Environment v -> Maybe v
     47 lookup l (Environment d s) = assertLvlInBounds d l $ NatMap.lookup (unLevel l) s
     48 
     49 -- | Bind and a new variable and assign a value to it.
     50 define :: (Level -> v) -> Environment v -> Environment v
     51 define makeVal env =
     52     let (l, env') = bind env
     53     in assign l (makeVal l) env'
     54 
     55 -- | Evaluate an index in an environment, falling back to making a value with
     56 -- the given function in case the environment doesn't have a substitution for
     57 -- the index.
     58 eval :: (Level -> v) -> Index -> Environment v -> v
     59 eval makeVal i env =
     60     let l = idxToLvl (depth env) i
     61     in fromMaybe (makeVal l) $ lookup l env