commit 909a7e64900d98cceb0f591e721cc2c1a09a1261
parent 4cab45d1225520984f81a0602d66087e1eec8667
Author: Robert Russell <robert@rr3.xyz>
Date: Wed, 28 Aug 2024 21:04:05 -0700
Clean up and move some work over from systemq
Diffstat:
| A | Common.hs | | | 16 | ++++++++++++++++ |
| M | Context.hs | | | 121 | +++++++++++++++++++++++++------------------------------------------------------ |
| M | Core.hs | | | 13 | +++++-------- |
| M | Environment.hs | | | 61 | +++++++++++++++++++++++++++++++++++++++---------------------- |
| M | Ledger.hs | | | 8 | ++++---- |
| M | Main.hs | | | 159 | ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++--------------------- |
| M | Surface.hs | | | 10 | ++-------- |
| D | Util.hs | | | 9 | --------- |
| M | Value.hs | | | 148 | ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++------------------- |
9 files changed, 334 insertions(+), 211 deletions(-)
diff --git a/Common.hs b/Common.hs
@@ -0,0 +1,16 @@
+module Common where
+
+class IsInt a where
+ toInt :: a -> Int
+ fromInt :: Int -> a
+
+instance IsInt Int where
+ toInt = id
+ fromInt = id
+
+data Kind
+ = KindT
+ | KindQ
+ | KindQT
+ | KindArrow Kind Kind
+ deriving (Eq, Show)
diff --git a/Context.hs b/Context.hs
@@ -3,8 +3,7 @@ import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Safe (atMay)
-import Util
-import Environment (Env)
+import Environment (Value (..), Env', Env)
import qualified Environment as Env
mapInsertCons :: Ord k => k -> v -> Map k [v] -> Map k [v]
@@ -13,94 +12,50 @@ mapInsertCons k v =
f Nothing = Just [v]
in Map.alter f k
-class Value a where
- type Generic a
- generic :: Generic a -> a
-
-type Ctx' name idx lvl a b =
- (Ord name, IsInt idx, IsInt lvl, Value a, Generic a ~ lvl)
-data Ctx name idx lvl a b = Ctx {
- map :: Map name [(a, b)],
- env :: Env idx lvl a
+type Ctx' name idx val a = (Ord name, Env' idx val)
+data Ctx name idx val a = Ctx {
+ map :: Map name [(val, a)],
+ env :: Env idx val
}
-empty :: Ctx' name idx lvl a b
- => Ctx name idx lvl a b
+empty :: Ctx' name idx val a
+ => Ctx name idx val a
empty = Ctx Map.empty Env.empty
-assign :: Ctx' name idx lvl a b
- => name -> a -> b -> Ctx name idx lvl a b -> Ctx name idx lvl a b
-assign x a b ctx = ctx { map = mapInsertCons x (a, b) ctx.map }
+assign :: Ctx' name idx val a
+ => name -> val -> a -> Ctx name idx val a -> Ctx name idx val a
+assign x val a ctx = ctx { map = mapInsertCons x (val, a) ctx.map }
-lookup :: Ctx' name idx lvl a b
- => name -> Int -> Ctx name idx lvl a b -> Maybe (a, b)
+lookup :: Ctx' name idx val a
+ => name -> Int -> Ctx name idx val a -> Maybe (val, a)
lookup x i ctx = do
xAsns <- Map.lookup x ctx.map
xAsns `atMay` i
-bind :: Ctx' name idx lvl a b
- => Ctx name idx lvl a b -> (lvl, Ctx name idx lvl a b)
+bind :: Ctx' name idx val a
+ => Ctx name idx val a -> (Level val, Ctx name idx val a)
bind ctx =
- let (l, env') = Env.bind ctx.env
- in (l, ctx { env = env' })
-
-bindAndAssign :: Ctx' name idx lvl a b
- => name -> b -> Ctx name idx lvl a b -> (lvl, Ctx name idx lvl a b)
-bindAndAssign x b ctx =
- let (l, ctx') = bind ctx
- in (l, assign x (generic l) b ctx')
-
-idxToLvl :: Ctx' name idx lvl a b
- => idx -> Ctx name idx lvl a b -> lvl
-idxToLvl i ctx = Env.idxToLvl i ctx.env
-
-lvlToIdx :: Ctx' name idx lvl a b
- => lvl -> Ctx name idx lvl a b -> idx
-lvlToIdx l ctx = Env.lvlToIdx l ctx.env
-
-define :: Ctx' name idx lvl a b
- => lvl -> a -> Ctx name idx lvl a b -> Ctx name idx lvl a b
-define l a ctx = ctx { env = Env.define l a ctx.env }
-
-eval :: Ctx' name idx lvl a b
- => lvl -> Ctx name idx lvl a b -> Maybe a
-eval l ctx = Env.eval l ctx.env
-
-{-
-data Ctx q = Ctx (TypeCtx q) (TermCtx q)
-
-ctxEmpty :: Ctx q
-ctxEmpty = Ctx 0 Map.empty 0 Map.empty
-
-ctxBindType :: S.TypeName -> Kind -> Ctx q -> Ctx q
-ctxBindType x k ctx =
- let lvl = C.TypeLevel ctx.nTypes in
- ctx {
- nTypes = ctx.nTypes + 1,
- types = mapInsertCons x (lvl, k) ctx.types
- }
-
-ctxLookupType :: S.TypeName -> Ctx q -> Maybe (C.TypeLevel, Kind)
-ctxLookupType x ctx = do
- xBindings <- Map.lookup x ctx.types
- xBindings `atMay` 0
-
-ctxTypeLevelToIndex :: C.TypeLevel -> Ctx q -> C.TypeIndex
-ctxTypeLevelToIndex (C.TypeLevel lvl) ctx = C.TypeIndex (ctx.nTypes - lvl - 1)
-
-ctxBindTerm :: S.TermName -> V.Type q -> Ctx q -> Ctx q
-ctxBindTerm x a ctx =
- let lvl = C.TermLevel ctx.nTerms in
- ctx {
- nTerms = ctx.nTerms + 1,
- terms = mapInsertCons x (lvl, a) ctx.terms
- }
-
-ctxLookupTerm :: S.TermName -> Ctx q -> Maybe (C.TermLevel, V.Type q)
-ctxLookupTerm x ctx = do
- xBindings <- Map.lookup x ctx.terms
- xBindings `atMay` 0
-
-ctxTermLevelToIndex :: C.TermLevel -> Ctx q -> C.TermIndex
-ctxTermLevelToIndex (C.TermLevel lvl) ctx = C.TermIndex (ctx.nTerms - lvl - 1)
--}
+ let (lvl, env') = Env.bind ctx.env
+ in (lvl, ctx { env = env' })
+
+bindAndAssign :: Ctx' name idx val a
+ => name -> a -> Ctx name idx val a -> (Level val, Ctx name idx val a)
+bindAndAssign x a ctx =
+ let (lvl, ctx') = bind ctx
+ in (lvl, assign x (generic lvl) a ctx')
+
+idxToLvl :: Ctx' name idx val a
+ => idx -> Ctx name idx val a -> Level val
+idxToLvl idx ctx = Env.idxToLvl idx ctx.env
+
+lvlToIdx :: Ctx' name idx val a
+ => Level val -> Ctx name idx val a -> idx
+lvlToIdx lvl ctx = Env.lvlToIdx lvl ctx.env
+
+define :: Ctx' name idx val a
+ => Level val -> val -> Ctx name idx val a -> Ctx name idx val a
+define lvl val ctx = ctx { env = Env.define lvl val ctx.env }
+
+subst :: Ctx' name idx val a
+ => Level val -> Ctx name idx val a -> Maybe val
+subst lvl ctx = Env.subst lvl ctx.env
diff --git a/Core.hs b/Core.hs
@@ -1,15 +1,12 @@
module Core where
-import Util
-import qualified Surface as S
+import Common
-newtype TypeIndex = TypeIndex Int deriving (Show, IsInt)
-newtype TermIndex = TermIndex Int deriving (Show, IsInt)
-
-type Kind = S.Kind
+newtype TypeIdx = TypeIdx Int deriving (Show, IsInt)
+newtype TermIdx = TermIdx Int deriving (Show, IsInt)
data Type q
- = TypeVar TypeIndex
+ = TypeVar TypeIdx
| TypeTArrow (Type q) (Type q)
| TypeTForall Kind (Type q)
@@ -27,7 +24,7 @@ data Type q
deriving Show
data Term q
- = TermVar TermIndex
+ = TermVar TermIdx
| TermArrowAbs (Term q)
| TermArrowApp (Term q) (Term q)
diff --git a/Environment.hs b/Environment.hs
@@ -2,41 +2,58 @@ module Environment where
import Data.IntMap.Strict (IntMap)
import qualified Data.IntMap.Strict as IntMap
-import Util
+import Common
-type Env' idx lvl = (IsInt idx, IsInt lvl)
-data Env idx lvl a = Env Int (IntMap a)
+-- Env represents a collection of free variables and a substitution on them.
+-- Free variables are represented using de Bruijn levels, and there must be
+-- an injection `generic` (as in "generic value") for turning levels into
+-- values. The terms which Env tracks free variables of should use de Bruijn
+-- indices, and Env is indexed by an `idx` type, so that multiple de Bruijn
+-- syntaxes may be handled without accidentally confusing indices and levels
+-- from different syntaxes.
-empty :: Env' idx lvl => Env idx lvl a
+class Value a where
+ type Level a
+ generic :: Level a -> a
+
+type Env' idx val = (IsInt idx, IsInt (Level val), Value val)
+data Env idx val = Env Int (IntMap val)
+
+empty :: Env' idx val => Env idx val
empty = Env 0 IntMap.empty
-bind :: Env' idx lvl => Env idx lvl a -> (lvl, Env idx lvl a)
+bind :: Env' idx val => Env idx val -> (Level val, Env idx val)
bind (Env size map) = (fromInt size, Env (size + 1) map)
-idxToLvl :: Env' idx lvl => idx -> Env idx lvl a -> lvl
-idxToLvl i (Env size _) =
- if toInt i >= size then
+idxToLvl :: Env' idx val => idx -> Env idx val -> Level val
+idxToLvl idx (Env size _) =
+ if toInt idx >= size then
error "Env.idxToLvl: index out of range"
else
- fromInt $ size - toInt i - 1
+ fromInt $ size - toInt idx - 1
-lvlToIdx :: Env' idx lvl => lvl -> Env idx lvl a -> idx
-lvlToIdx l (Env size _) =
- if toInt l >= size then
+lvlToIdx :: Env' idx val => Level val -> Env idx val -> idx
+lvlToIdx lvl (Env size _) =
+ if toInt lvl >= size then
error "Env.lvlToIdx: level out of range"
else
- fromInt $ size - toInt l - 1
+ fromInt $ size - toInt lvl - 1
-define :: Env' idx lvl => lvl -> a -> Env idx lvl a -> Env idx lvl a
-define l v (Env size map) =
- if toInt l >= size then
+define :: Env' idx val => Level val -> val -> Env idx val -> Env idx val
+define lvl val (Env size map) =
+ if toInt lvl >= size then
error "Env.define: level out of range"
else
- Env size (IntMap.insert (toInt l) v map)
+ Env size (IntMap.insert (toInt lvl) val map)
+
+bindAndDefine :: Env' idx val => val -> Env idx val -> (Level val, Env idx val)
+bindAndDefine val env =
+ let (lvl, env') = bind env
+ in (lvl, define lvl val env')
-eval :: Env' idx lvl => lvl -> Env idx lvl a -> Maybe a
-eval l (Env size map) =
- if toInt l >= size then
- error "Env.eval: level out of range"
+subst :: Env' idx val => Level val -> Env idx val -> Maybe val
+subst lvl (Env size map) =
+ if toInt lvl >= size then
+ error "Env.subst: level out of range"
else
- IntMap.lookup (toInt l) map
+ IntMap.lookup (toInt lvl) map
diff --git a/Ledger.hs b/Ledger.hs
@@ -30,12 +30,12 @@ instance (MulAction q, MulActionScalar q ~ q) => MulAction (Ledger q) where
q <⋅> Ledger d m = Ledger (q <⋅> d) ((q <⋅>) <$> m)
-singleton :: AddMonoid q => V.TermLevel -> V.Type q -> Ledger q
-singleton (V.TermLevel l) q = Ledger zero (IntMap.singleton l q)
+singleton :: AddMonoid q => V.TermLvl -> V.Type q -> Ledger q
+singleton (V.TermLvl l) q = Ledger zero (IntMap.singleton l q)
-- split is like uncons for ledgers: given a ledger L that maps a de Bruijn
-- level l to quantity q, "split l L" returns (q, L'), where L' is L with the
-- mapping for l removed (i.e., l is reset to the default quantity).
-split :: V.TermLevel -> Ledger q -> (V.Type q, Ledger q)
-split (V.TermLevel l) (Ledger d m) =
+split :: V.TermLvl -> Ledger q -> (V.Type q, Ledger q)
+split (V.TermLvl l) (Ledger d m) =
(IntMap.findWithDefault d l m, Ledger d (IntMap.delete l m))
diff --git a/Main.hs b/Main.hs
@@ -2,14 +2,13 @@ module Main where
import Control.Monad
import Control.Monad.Except
import Control.Monad.Reader
-import Data.Functor
import Algebra
import Ledger (Ledger)
import qualified Ledger as L
+import Common
import Context (Ctx)
import qualified Context as Ctx
-import Surface (Kind (..))
import qualified Surface as S
import qualified Core as C
import qualified Value as V
@@ -26,46 +25,55 @@ a `orThrowError` e =
--------------------------------------------------------------------------------
-- Elaboration monad
-type TypeCtx q = Ctx S.TypeName C.TypeIndex V.TypeLevel (V.Type q) Kind
+type TypeCtx q = Ctx S.TypeName C.TypeIdx (V.Type q) Kind
+type TermCtx q = Ctx S.TermName C.TermIdx V.Term (V.Type q)
+data BothCtx q = BothCtx {
+ typeCtx :: TypeCtx q,
+ termCtx :: TermCtx q
+}
-type TermCtx q = Ctx S.TermName C.TermIndex V.TermLevel V.Term (V.Type q)
+data Err = Err -- TODO
-data Err = Err
-
-type Elab q a = ReaderT (TypeCtx q, TermCtx q) (Except Err) a
-
-askTypeCtx :: Elab q (TypeCtx q)
-askTypeCtx = asks fst
-
-askTermCtx :: Elab q (TermCtx q)
-askTermCtx = asks snd
+type Elab q a = ReaderT (BothCtx q) (Except Err) a
--------------------------------------------------------------------------------
-- Type-level elaboration
-bindAndAssignType :: S.TypeName -> Kind -> Elab q a -> Elab q a
-bindAndAssignType x k = local \(typeCtx, termCtx) ->
- (snd $ Ctx.bindAndAssign x k typeCtx, termCtx)
+evalType :: QuantityAlgebra q => C.Type q -> Elab q (V.Type q)
+evalType a = V.evalType <$> asks (.typeCtx.env) <*> pure a
-lookupType :: S.TypeName -> Elab q (V.Type q, Kind)
-lookupType x = (Ctx.lookup x 0 <$> askTypeCtx) >>= (`orThrowError` Err) -- TODO
+quoteType :: QuantityAlgebra q => V.Type q -> Elab q (C.Type q)
+quoteType a = V.quoteType <$> asks (.typeCtx.env) <*> pure a
-typeLvlToIdx :: V.TypeLevel -> Elab q C.TypeIndex
-typeLvlToIdx lvl = Ctx.lvlToIdx lvl <$> askTypeCtx
+convType :: QuantityAlgebra q => V.Type q -> V.Type q -> Elab q Bool
+convType a b = V.convType <$> asks (.typeCtx.env) <*> pure a <*> pure b
-inferType :: S.Type q -> Elab q (C.Type q, Kind)
+bindAndAssignType :: QuantityAlgebra q
+ => S.TypeName
+ -> Kind
+ -> (V.TypeLvl -> Elab q a)
+ -> Elab q a
+bindAndAssignType x k f = do
+ ctx <- ask
+ let (lvl, typeCtx') = Ctx.bindAndAssign x k ctx.typeCtx
+ local (const $ ctx { typeCtx = typeCtx' }) (f lvl)
+
+lookupType :: QuantityAlgebra q => S.TypeName -> Elab q (V.Type q, Kind)
+lookupType x = (Ctx.lookup x 0 <$> asks (.typeCtx)) >>= (`orThrowError` Err) -- TODO
+
+inferType :: QuantityAlgebra q => S.Type q -> Elab q (C.Type q, Kind)
inferType = \case
S.TypeVar x -> do
(va, k) <- lookupType x
- typeEnv <- askTypeCtx <&> (.env)
- pure (V.quote typeEnv va, k)
+ a <- quoteType va
+ pure (a, k)
S.TypeAnnot a k -> (, k) <$> checkType a k
S.TypeTArrow dom cod -> do
dom' <- checkType dom KindQT
cod' <- checkType cod KindQT
pure (C.TypeTArrow dom' cod', KindT)
S.TypeTForall x k a -> do
- a' <- bindAndAssignType x k $ checkType a KindQT
+ a' <- bindAndAssignType x k \_ -> checkType a KindQT
pure (C.TypeTForall k a', KindT)
S.TypeQ q -> pure (C.TypeQ q, KindQ)
S.TypeQTPair q a -> do
@@ -87,10 +95,10 @@ inferType = \case
pure (C.TypeArrowApp fun' arg', cod)
_ -> throwError Err -- TODO
-checkType :: S.Type q -> Kind -> Elab q (C.Type q)
+checkType :: QuantityAlgebra q => S.Type q -> Kind -> Elab q (C.Type q)
checkType a k = case (a, k) of
(S.TypeArrowAbs x body, KindArrow dom cod) ->
- bindAndAssignType x dom $ checkType body cod
+ bindAndAssignType x dom \_ -> checkType body cod
(a, k) -> do
(a', k') <- inferType a
unless (k' == k) $ throwError Err -- TODO
@@ -99,28 +107,95 @@ checkType a k = case (a, k) of
--------------------------------------------------------------------------------
-- Term-level elaboration
-{-
-bindTerm :: S.TermName -> V.Type q -> Elab q a -> Elab q a
-bindTerm x a = local (ctxBindTerm x a)
-
-lookupTerm :: S.TermName -> Elab q (C.TermLevel, V.Type q)
-lookupTerm x = asks (ctxLookupTerm x) >>= (`orThrowError` Err) -- TODO
-
-termLevelToIndex :: C.TermLevel -> Elab q C.TermIndex
-termLevelToIndex lvl = asks (ctxTermLevelToIndex lvl)
-
-inferTerm :: S.Term q -> V.Term q -> Elab q (C.Term q, V.Type q, Ledger q)
+-- TODO: Think of a better way of tracking ledgers
+
+bindAndAssignTerm :: QuantityAlgebra q
+ => S.TermName
+ -> V.Type q
+ -> (V.TermLvl -> Elab q a)
+ -> Elab q a
+bindAndAssignTerm x a f = do
+ ctx <- ask
+ let (lvl, termCtx') = Ctx.bindAndAssign x a ctx.termCtx
+ local (const $ ctx { termCtx = termCtx' }) (f lvl)
+
+lookupTerm :: QuantityAlgebra q => S.TermName -> Elab q (V.TermLvl, V.Type q)
+lookupTerm x = do
+ m <- Ctx.lookup x 0 <$> asks (.termCtx)
+ (V.TermGeneric lvl, a) <- m `orThrowError` Err -- TODO
+ pure (lvl, a)
+
+termLvlToIdx :: QuantityAlgebra q => V.TermLvl -> Elab q C.TermIdx
+termLvlToIdx lvl = Ctx.lvlToIdx lvl <$> asks (.termCtx)
+
+inferTerm :: QuantityAlgebra q
+ => S.Term q
+ -> V.Type q
+ -> Elab q (C.Term q, V.Type q, Ledger q)
inferTerm t q = case t of
S.TermVar x -> do
(lvl, a) <- lookupTerm x
- idx <- termLevelToIndex lvl
- pure (C.TermVar idx, a, Ledger.singleton lvl q)
+ idx <- termLvlToIdx lvl
+ pure (C.TermVar idx, a, L.singleton lvl q)
+
S.TermAnnot t a -> do
a' <- checkType a KindT
+ a'' <- evalType a'
+ (t', tLedger) <- checkTerm t q a''
+ pure (t', a'', tLedger)
+
+ S.TermArrowAbs _ _ -> throwError Err -- TODO
+
+ S.TermArrowApp fun arg -> do
+ (fun', funType, funLedger) <- inferTerm fun one
+ case funType of
+ V.TypeTArrow dom cod -> do
+ (arg', argLedger) <- checkTerm arg (V.qtFst dom) (V.qtSnd dom)
+ unless (V.qtFst cod `V.qGeq` q) $ throwError Err -- TODO
+ pure (C.TermArrowApp fun' arg', V.qtSnd cod, funLedger <+> argLedger)
+ _ -> throwError Err -- TODO
+
+ S.TermForallAbs _ _ -> throwError Err -- TODO
+
+ S.TermForallApp fun arg -> do
+ (fun', funType, funLedger) <- inferTerm fun one
+ case funType of
+ V.TypeTForall k clo -> do
+ arg' <- checkType arg k
+ arg'' <- evalType arg'
+ let qa = V.applyClosure clo arg''
+ unless (V.qtFst qa `V.qGeq` q) $ throwError Err -- TODO
+ pure (C.TermForallApp fun' arg', V.qtSnd qa, funLedger)
+ _ -> throwError Err -- TODO
-checkTerm :: S.Term q -> V.Type q -> V.Type q -> Elab q (C.Term q, Ledger q)
-checkTerm t a =
--}
+checkTerm :: QuantityAlgebra q
+ => S.Term q
+ -> V.Type q
+ -> V.Type q
+ -> Elab q (C.Term q, Ledger q)
+checkTerm t q a = case (t, a) of
+ (S.TermArrowAbs x body, V.TypeTArrow dom cod) -> do
+ bindAndAssignTerm x (V.qtSnd dom) \lvl -> do
+ (body', bodyLedger) <- checkTerm body (V.qtFst cod) (V.qtSnd cod)
+ let (domDemand, absLedger) = L.split lvl bodyLedger
+ unless (V.qtFst dom `V.qGeq` domDemand) $ throwError Err -- TODO
+ pure (C.TermArrowAbs body', q <⋅> absLedger)
+
+ (S.TermArrowAbs _ _, _) -> throwError Err -- TODO
+
+ (S.TermForallAbs x body, V.TypeTForall k clo) ->
+ bindAndAssignType x k \lvl -> do
+ let qa = V.applyClosure clo (V.TypeGeneric lvl)
+ (body', bodyLedger) <- checkTerm body (V.qtFst qa) (V.qtSnd qa)
+ pure (C.TermForallAbs body', q <⋅> bodyLedger)
+
+ (S.TermForallAbs _ _, _) -> throwError Err -- TODO
+
+ (t, a) -> do
+ (t', a', tLedger) <- inferTerm t q
+ equal <- convType a' a
+ unless equal $ throwError Err -- TODO
+ pure (t', tLedger)
--------------------------------------------------------------------------------
diff --git a/Surface.hs b/Surface.hs
@@ -1,17 +1,11 @@
module Surface where
import Data.ByteString (ByteString)
+import Common
+
newtype TypeName = TypeName ByteString deriving (Eq, Ord, Show)
newtype TermName = TermName ByteString deriving (Eq, Ord, Show)
--- TODO: Move this?
-data Kind
- = KindT
- | KindQ
- | KindQT
- | KindArrow Kind Kind
- deriving (Eq, Show)
-
data Type q
= TypeVar TypeName
| TypeAnnot (Type q) Kind
diff --git a/Util.hs b/Util.hs
@@ -1,9 +0,0 @@
-module Util where
-
-class IsInt a where
- toInt :: a -> Int
- fromInt :: Int -> a
-
-instance IsInt Int where
- toInt = id
- fromInt = id
diff --git a/Value.hs b/Value.hs
@@ -1,50 +1,46 @@
module Value where
+import Data.Maybe (fromMaybe)
-import Util
import Algebra
-import Environment (Env)
+import Common
+import Environment (Value (..), Env)
import qualified Environment as Env
-import qualified Context as Ctx
-import Surface (Kind (..))
import qualified Core as C
-newtype TypeLevel = TypeLevel Int deriving (Show, IsInt)
-newtype TermLevel = TermLevel Int deriving (Show, IsInt)
+newtype TypeLvl = TypeLvl Int deriving (Eq, Show, IsInt)
+newtype TermLvl = TermLvl Int deriving (Eq, Show, IsInt)
-type TypeEnv q = Env C.TypeIndex TypeLevel (Type q)
-data TypeClosure q = TypeClosure (TypeEnv q) (C.Type q)
+type TypeEnv q = Env C.TypeIdx (Type q)
+type TermEnv q = Env C.TermIdx Term
-data TypeElim q
- = TypeElimFst
- | TypeElimSnd
- | TypeElimApp (Type q)
- | TypeElimAdd (Type q)
- | TypeElimMul (Type q)
+data TypeClosure q = TypeClosure {
+ env :: TypeEnv q,
+ abs :: C.Type q
+}
data Type q
- = TypeNeutral TypeLevel [TypeElim q]
+ = TypeGeneric TypeLvl
| TypeTArrow (Type q) (Type q)
| TypeTForall Kind (TypeClosure q)
| TypeQ q
+ | TypeQAdd (Type q) (Type q)
+ | TypeQMul (Type q) (Type q)
| TypeQTPair (Type q) (Type q)
+ | TypeQTFst (Type q)
+ | TypeQTSnd (Type q)
| TypeArrowAbs (TypeClosure q)
-
-instance Ctx.Value (Type q) where
- type Generic (Type q) = TypeLevel
- generic l = TypeNeutral l []
+ | TypeArrowApp (Type q) (Type q)
instance AddMonoid q => AddMonoid (Type q) where
zero = TypeQ zero
- a <+> b = case (a, b) of
+ x <+> y = case (x, y) of
(TypeQ q, TypeQ r) -> TypeQ (q <+> r)
- (TypeNeutral l es, a) -> TypeNeutral l (TypeElimAdd a : es)
- (a, TypeNeutral l es) -> TypeNeutral l (TypeElimAdd a : es)
- _ -> error "impossible"
+ (x, y) -> TypeQAdd x y
instance MulScalar q => MulScalar (Type q) where
one = TypeQ one
@@ -52,21 +48,103 @@ instance MulScalar q => MulScalar (Type q) where
instance (MulAction q, MulActionScalar q ~ q) => MulAction (Type q) where
type MulActionScalar (Type q) = Type q
- a <⋅> b = case (a, b) of
+ x <⋅> y = case (x, y) of
(TypeQ q, TypeQ r) -> TypeQ (q <⋅> r)
- (TypeNeutral l es, a) -> TypeNeutral l (TypeElimMul a : es)
- (a, TypeNeutral l es) -> TypeNeutral l (TypeElimMul a : es)
- _ -> error "impossible"
+ (x, y) -> TypeQMul x y
+
+instance Value (Type q) where
+ type Level (Type q) = TypeLvl
+ generic = TypeGeneric
-- During elaboration, we only need to "evaluate" term variables.
-data Term = TermGeneric TermLevel
+newtype Term = TermGeneric TermLvl
-instance Ctx.Value Term where
- type Generic Term = TermLevel
+instance Value Term where
+ type Level Term = TermLvl
generic = TermGeneric
-eval :: TypeEnv q -> C.Type q -> Type q
-eval = eval
-
-quote :: TypeEnv q -> Type q -> C.Type q
-quote = quote
+qGeq :: QuantityAlgebra q => Type q -> Type q -> Bool
+x `qGeq` y = case (x, y) of
+ (TypeQ q, TypeQ r) -> q ?>= r
+ _ -> False
+
+qtFst :: QuantityAlgebra q => Type q -> Type q
+qtFst = \case
+ TypeQTPair q _ -> q
+ x -> TypeQTFst x
+
+qtSnd :: QuantityAlgebra q => Type q -> Type q
+qtSnd = \case
+ TypeQTPair _ a -> a
+ x -> TypeQTSnd x
+
+applyClosure :: QuantityAlgebra q => TypeClosure q -> Type q -> Type q
+applyClosure (TypeClosure env abs) arg =
+ let (_, env') = Env.bindAndDefine arg env
+ in evalType env' abs
+
+evalType :: QuantityAlgebra q => TypeEnv q -> C.Type q -> Type q
+evalType env a =
+ let eval = evalType env in
+ case a of
+ C.TypeVar idx ->
+ let lvl = Env.idxToLvl idx env in
+ fromMaybe (TypeGeneric lvl) (Env.subst lvl env)
+ C.TypeTArrow dom cod -> TypeTArrow (eval dom) (eval cod)
+ C.TypeTForall k body -> TypeTForall k (TypeClosure env body)
+ C.TypeQ q -> TypeQ q
+ C.TypeQAdd q r -> (eval q) <+> (eval r)
+ C.TypeQMul q r -> (eval q) <⋅> (eval r)
+ C.TypeQTPair q a -> TypeQTPair (eval q) (eval a)
+ C.TypeQTFst qa -> qtFst (eval qa)
+ C.TypeQTSnd qa -> qtSnd (eval qa)
+ C.TypeArrowAbs body -> TypeArrowAbs (TypeClosure env body)
+ C.TypeArrowApp fun arg ->
+ let varg = eval arg in
+ case eval fun of
+ TypeArrowAbs body -> applyClosure body varg
+ vfun -> TypeArrowApp vfun varg
+
+quoteType :: QuantityAlgebra q => TypeEnv q -> Type q -> C.Type q
+quoteType env a =
+ let quote = quoteType env in
+ case a of
+ TypeGeneric lvl -> C.TypeVar $ Env.lvlToIdx lvl env
+ TypeTArrow dom cod -> C.TypeTArrow (quote dom) (quote cod)
+ TypeTForall k body -> C.TypeTForall k $ quoteTypeClosure env body
+ TypeQ q -> C.TypeQ q
+ TypeQAdd q r -> C.TypeQAdd (quote q) (quote r)
+ TypeQMul q r -> C.TypeQMul (quote q) (quote r)
+ TypeQTPair q a -> C.TypeQTPair (quote q) (quote a)
+ TypeQTFst qa -> C.TypeQTFst (quote qa)
+ TypeQTSnd qa -> C.TypeQTFst (quote qa)
+ TypeArrowAbs body -> C.TypeArrowAbs $ quoteTypeClosure env body
+ TypeArrowApp fun arg -> C.TypeArrowApp (quote fun) (quote arg)
+
+quoteTypeClosure :: QuantityAlgebra q => TypeEnv q -> TypeClosure q -> C.Type q
+quoteTypeClosure env clo =
+ let (lvl, env') = Env.bind env in
+ quoteType env' $ applyClosure clo (TypeGeneric lvl)
+
+convType :: QuantityAlgebra q => TypeEnv q -> Type q -> Type q -> Bool
+convType env x y =
+ let conv = convType env in
+ case (x, y) of
+ (TypeGeneric xlvl, TypeGeneric ylvl) -> xlvl == ylvl
+ (TypeTArrow xdom xcod, TypeTArrow ydom ycod) -> conv xdom ydom && conv xcod ycod
+ (TypeTForall xk xclo, TypeTForall yk yclo) -> xk == yk && convTypeClosure env xclo yclo
+ (TypeQ q, TypeQ r) -> q == r
+ (TypeQAdd xq xr, TypeQAdd yq yr) -> conv xq yq && conv xr yr
+ (TypeQMul xq xr, TypeQMul yq yr) -> conv xq yq && conv xr yr
+ (TypeQTPair q a, TypeQTPair r b) -> conv q r && conv a b
+ (TypeQTFst qa, TypeQTFst rb) -> conv qa rb
+ (TypeQTSnd qa, TypeQTSnd rb) -> conv qa rb
+ (TypeArrowAbs xclo, TypeArrowAbs yclo) -> convTypeClosure env xclo yclo
+ (TypeArrowApp xfun xarg, TypeArrowApp yfun yarg) -> conv xfun yfun && conv xarg yarg
+ (_, _) -> False
+
+convTypeClosure :: QuantityAlgebra q => TypeEnv q -> TypeClosure q -> TypeClosure q -> Bool
+convTypeClosure env xclo yclo =
+ let (lvl, env') = Env.bind env
+ arg = TypeGeneric lvl
+ in convType env' (applyClosure xclo arg) (applyClosure yclo arg)
