systemqfw

commit b36eb6c5d887e88d250964a02d4d882050e349b8
parent bf7697253345e223aee8062cdfc976060211070d
Author: Robert Russell <robert@rr3.xyz>
Date:   Thu, 29 Aug 2024 15:46:22 -0700

Clean up

Diffstat:
M
Core.hs
 | 
9
++++++++-
M
Parser.hs
 | 
22
+++++++++++++++++-----
M
Surface.hs
 | 
11
+++++++++--
M
Value.hs
 | 
26
+++++++++++++++++---------

4 files changed, 51 insertions(+), 17 deletions(-)
diff --git a/Core.hs b/Core.hs
@@ -2,8 +2,10 @@ module Core where
 
 import Common
 
+--------------------------------------------------------------------------------
+-- Types
+
 newtype TypeIdx = TypeIdx Int deriving (Show, IsInt)
-newtype TermIdx = TermIdx Int deriving (Show, IsInt)
 
 data Type q
     = TypeVar TypeIdx
@@ -23,6 +25,11 @@ data Type q
     | TypeArrowApp (Type q) (Type q)
     deriving Show
 
+--------------------------------------------------------------------------------
+-- Terms
+
+newtype TermIdx = TermIdx Int deriving (Show, IsInt)
+
 data Term q
     = TermVar TermIdx
 
diff --git a/Parser.hs b/Parser.hs
@@ -37,6 +37,9 @@ pQular = pWord "bot" *> pure Qular.Alpha
     <|> pWord "top" *> pure Qular.Omega
     -- TODO: syntax for Aff and Rel
 
+--------------------------------------------------------------------------------
+-- General lexical elements
+
 isWordStart :: Char -> Bool
 isWordStart c = isLetter c || isDigit c || c == '_'
 
@@ -78,11 +81,8 @@ pAnyIdent = do
 pDelim :: Monad m => String -> ParseT Err m a -> String -> ParseT Err m a
 pDelim l p r = pSym l *> (p <* pSym r) `cut` Err
 
-pTypeName :: P q TypeName
-pTypeName = TypeName <$> pAnyIdent
-
-pTermName :: P q TermName
-pTermName = TermName <$> pAnyIdent
+--------------------------------------------------------------------------------
+-- Kinds
 
 pKindArrow :: Kind -> P q Kind
 pKindArrow dom = pSym "->" *> (KindArrow dom <$> pKind 0) `cut` Err
@@ -101,6 +101,12 @@ pKind = \case
 pTopKind :: P q Kind
 pTopKind = pWs *> pKind 0 <* eof
 
+--------------------------------------------------------------------------------
+-- Types
+
+pTypeName :: P q TypeName
+pTypeName = TypeName <$> pAnyIdent
+
 pTypeAnnot :: Type q -> P q (Type q)
 pTypeAnnot a = pSym ":" *> (TypeAnnot a <$> pKind 0) `cut` Err
 
@@ -150,6 +156,12 @@ pType = \case
 pTopType :: P q (Type q)
 pTopType = pWs *> pType 0 <* eof
 
+--------------------------------------------------------------------------------
+-- Terms
+
+pTermName :: P q TermName
+pTermName = TermName <$> pAnyIdent
+
 pTermAnnot :: Term q -> P q (Term q)
 pTermAnnot t = pSym ":" *> (TermAnnot t <$> pType 0) `cut` Err
 
diff --git a/Surface.hs b/Surface.hs
@@ -3,8 +3,10 @@ import Data.ByteString (ByteString)
 
 import Common
 
+--------------------------------------------------------------------------------
+-- Types
+
 newtype TypeName = TypeName ByteString deriving (Eq, Ord, Show)
-newtype TermName = TermName ByteString deriving (Eq, Ord, Show)
 
 data Type q
     = TypeVar TypeName
@@ -14,7 +16,7 @@ data Type q
     | TypeTForall TypeName Kind (Type q)
 
     | TypeQ q
-    -- TODO: Internal Mul and Add operations?
+    -- TODO: Internal Mul and Add operations
 
     | TypeQTPair (Type q) (Type q)
     | TypeQTFst (Type q)
@@ -24,6 +26,11 @@ data Type q
     | TypeArrowApp (Type q) (Type q)
     deriving Show
 
+--------------------------------------------------------------------------------
+-- Terms
+
+newtype TermName = TermName ByteString deriving (Eq, Ord, Show)
+
 data Term q
     = TermVar TermName
     | TermAnnot (Term q) (Type q)
diff --git a/Value.hs b/Value.hs
@@ -7,11 +7,12 @@ import Environment (Value (..), Env)
 import qualified Environment as Env
 import qualified Core as C
 
+--------------------------------------------------------------------------------
+-- Types
+
 newtype TypeLvl = TypeLvl Int deriving (Eq, Show, IsInt)
-newtype TermLvl = TermLvl Int deriving (Eq, Show, IsInt)
 
 type TypeEnv q = Env C.TypeIdx (Type q)
-type TermEnv q = Env C.TermIdx Term
 
 data TypeClosure q = TypeClosure {
     env :: TypeEnv q,
@@ -56,13 +57,6 @@ instance Value (Type q) where
     type Level (Type q) = TypeLvl
     generic = TypeGeneric
 
--- During elaboration, we only need to "evaluate" term variables.
-newtype Term = TermGeneric TermLvl
-
-instance Value Term where
-    type Level Term = TermLvl
-    generic = TermGeneric
-
 qGeq :: QuantityAlgebra q => Type q -> Type q -> Bool
 x `qGeq` y = case (x, y) of
     (TypeQ q, TypeQ r) -> q ?>= r
@@ -148,3 +142,17 @@ convTypeClosure env xclo yclo =
     let (lvl, env') = Env.bind env
         arg = TypeGeneric lvl
     in convType env' (applyClosure xclo arg) (applyClosure yclo arg)
+
+--------------------------------------------------------------------------------
+-- Terms
+
+newtype TermLvl = TermLvl Int deriving (Eq, Show, IsInt)
+
+type TermEnv q = Env C.TermIdx Term
+
+-- During elaboration, we only need to "evaluate" term variables.
+newtype Term = TermGeneric TermLvl
+
+instance Value Term where
+    type Level Term = TermLvl
+    generic = TermGeneric