plutils

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

Environment.hs (2195B)

      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 syn v = Environment (Depth syn) (NatMap v) deriving (Show)
     25 
     26 empty :: Environment syn v
     27 empty = Environment topLevel NatMap.empty
     28 
     29 depth :: Environment syn v -> Depth syn
     30 depth (Environment d _) = d
     31 
     32 -- | Bind a new variable (without introducing a substitution for it).
     33 bind :: Environment syn v -> (Level syn, Environment syn v)
     34 bind (Environment d s) =
     35     let (l, d') = descend d
     36     in (l, Environment d' s)
     37 
     38 weaken :: Environment syn v -> Environment syn v
     39 weaken = snd . bind
     40 
     41 -- | Assign a value to an existing variable.
     42 assign :: Level syn -> v -> Environment syn v -> Environment syn 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 syn -> Environment syn 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 defines :: (Level syn -> v) -> Environment syn v -> Environment syn v
     51 defines makeVal env =
     52     let (l, env') = bind env
     53     in assign l (makeVal l) env'
     54 
     55 -- | Bind and a new variable and assign a value to it.
     56 define :: v -> Environment syn v -> Environment syn v
     57 define = defines . const
     58 
     59 -- | Evaluate an index in an environment, falling back to making a value with
     60 -- the given function in case the environment doesn't have a substitution for
     61 -- the index.
     62 eval :: (Level syn -> v) -> Index syn -> Environment syn v -> v
     63 eval makeVal i env =
     64     let l = idxToLvl (depth env) i
     65     in fromMaybe (makeVal l) $ lookup l env