systemqfw

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

Ledger.hs (1514B)

      1 module Ledger where
      2 import Data.IntMap.Strict (IntMap)
      3 import qualified Data.IntMap.Strict as IntMap
      4 
      5 import Algebra
      6 import qualified Value as V
      7 
      8 -- A ledger maps from de Bruijn levels (represented as Ints) to quantities.
      9 -- This mapping is implemented with an IntMap and a default quantity for all
     10 -- variables not in the IntMap.
     11 data Ledger q = Ledger (V.Type q) (IntMap (V.Type q))
     12 
     13 {-
     14 -- Pointwise LUB
     15 instance LubMonoid q => LubMonoid (Ledger q) where
     16     bot = Ledger bot IntMap.empty
     17 
     18     Ledger d0 m0 <^> Ledger d1 m1 = Ledger (d0 <^> d1) (IntMap.unionWith (<^>) m0 m1)
     19 -}
     20 
     21 -- Pointwise sum
     22 instance AddMonoid q => AddMonoid (Ledger q) where
     23     zero = Ledger zero IntMap.empty
     24 
     25     Ledger d0 m0 <+> Ledger d1 m1 = Ledger (d0 <+> d1) (IntMap.unionWith (<+>) m0 m1)
     26 
     27 -- Scalar multiply mapped over the entire ledger
     28 instance (MulAction q, MulActionScalar q ~ q) => MulAction (Ledger q) where
     29     type MulActionScalar (Ledger q) = V.Type q
     30 
     31     q <⋅> Ledger d m = Ledger (q <⋅> d) ((q <⋅>) <$> m)
     32 
     33 singleton :: AddMonoid q => V.TermLvl -> V.Type q -> Ledger q
     34 singleton (V.TermLvl l) q = Ledger zero (IntMap.singleton l q)
     35 
     36 -- split is like uncons for ledgers: given a ledger L that maps a de Bruijn
     37 -- level l to quantity q, "split l L" returns (q, L'), where L' is L with the
     38 -- mapping for l removed (i.e., l is reset to the default quantity).
     39 split :: V.TermLvl -> Ledger q -> (V.Type q, Ledger q)
     40 split (V.TermLvl l) (Ledger d m) =
     41     (IntMap.findWithDefault d l m, Ledger d (IntMap.delete l m))