systemqfw

system Q F omega elaborator
git clone git://git.rr3.xyz/systemqfw
Log | Files | Refs | Submodules | README | LICENSE

Context.hs (1864B)

      1 module Context where
      2 import Data.Map.Strict (Map)
      3 import qualified Data.Map.Strict as Map
      4 import Safe (atMay)
      5 
      6 import Environment (Value (..), Env', Env)
      7 import qualified Environment as Env
      8 
      9 mapInsertCons :: Ord k => k -> v -> Map k [v] -> Map k [v]
     10 mapInsertCons k v =
     11     let f (Just vs) = Just (v : vs)
     12         f Nothing   = Just [v]
     13     in Map.alter f k
     14 
     15 type Ctx' name idx val a = (Ord name, Env' idx val)
     16 data Ctx name idx val a = Ctx {
     17     map :: Map name [(val, a)],
     18     env :: Env idx val
     19 }
     20 
     21 empty :: Ctx' name idx val a
     22       => Ctx name idx val a
     23 empty = Ctx Map.empty Env.empty
     24 
     25 assign :: Ctx' name idx val a
     26        => name -> val -> a -> Ctx name idx val a -> Ctx name idx val a
     27 assign x val a ctx = ctx { map = mapInsertCons x (val, a) ctx.map }
     28 
     29 lookup :: Ctx' name idx val a
     30        => name -> Int -> Ctx name idx val a -> Maybe (val, a)
     31 lookup x i ctx = do
     32     xAsns <- Map.lookup x ctx.map
     33     xAsns `atMay` i
     34 
     35 bind :: Ctx' name idx val a
     36      => Ctx name idx val a -> (Level val, Ctx name idx val a)
     37 bind ctx =
     38     let (lvl, env') = Env.bind ctx.env
     39     in (lvl, ctx { env = env' })
     40 
     41 bindAndAssign :: Ctx' name idx val a
     42               => name -> a -> Ctx name idx val a -> (Level val, Ctx name idx val a)
     43 bindAndAssign x a ctx =
     44     let (lvl, ctx') = bind ctx
     45     in (lvl, assign x (generic lvl) a ctx')
     46 
     47 idxToLvl :: Ctx' name idx val a
     48          => idx -> Ctx name idx val a -> Level val
     49 idxToLvl idx ctx = Env.idxToLvl idx ctx.env
     50 
     51 lvlToIdx :: Ctx' name idx val a
     52          => Level val -> Ctx name idx val a -> idx
     53 lvlToIdx lvl ctx = Env.lvlToIdx lvl ctx.env
     54 
     55 define :: Ctx' name idx val a
     56        => Level val -> val -> Ctx name idx val a -> Ctx name idx val a
     57 define lvl val ctx = ctx { env = Env.define lvl val ctx.env }
     58 
     59 subst :: Ctx' name idx val a
     60       => Level val -> Ctx name idx val a -> Maybe val
     61 subst lvl ctx = Env.subst lvl ctx.env