Type checking and elaboration for HSum and HCon

examples/PropTrunc.ctt

@@ -0,0 +1,5 @@
+module PropTrunc where
+
+data PropTrunc (A : U) : U
+  = eta (a : A)
+  | squash (u v : PropTrunc A) <i> [(i=0) -> u, (i=1) -> v]

examples/S1.ctt

@@ -5,3 +5,8 @@ data S1 : U
   | loopAt <i> [ (i=0) -> base, (i=1) -> base ]
 
 loop : Path S1 base base = \i. loopAt i
+
+-- stating this w/o PathP seems annoying
+-- indS1 (M : S1 -> U) (b : M base) (l : _) : (z : S1) -> M z = hsplit
+--   base   -> b
+--   loop i -> l i

examples/Torus.ctt

@@ -15,4 +15,8 @@ data Torus : U
       , (i=1) -> loop2At j
       , (j=0) -> loop1At i
       , (j=1) -> loop1At i
-      ] 
+      ]
+
+loop1 : Path Torus base base = \i. loop1At i
+
+loop2 : Path Torus base base = \i. loop2At i

src/PosTT/Conversion.hs

@@ -1,14 +1,11 @@
 module PosTT.Conversion (conv) where
 
-import Control.Monad (zipWithM_, unless)
-import Control.Monad.Except (throwError)
+import Control.Monad (zipWithM_)
 
 import PosTT.Common
-import PosTT.Poset
-import PosTT.Quotation
+import PosTT.Quotation ()
 import PosTT.Errors
 import PosTT.Eval
-import PosTT.Terms
 import PosTT.Values
 
 
@@ -62,6 +59,11 @@ instance Conv Val where
     (VCon c₀ as₀       , VCon c₁ as₁       ) | c₀ == c₁ -> as₀ `conv` as₁
     (VSplitPartial f₀ _, VSplitPartial f₁ _) -> f₀ `conv` f₁
 
+    (VHSum d₀ _        , d₁                ) -> d₀ `conv` d₁
+    (d₀                , VHSum d₁ _        ) -> d₀ `conv` d₁
+    -- TODO: hsplit; is the above correct?
+    (VHCon c₀ as₀ is₀ _, VHCon c₁ as₁ is₁ _) | c₀ == c₁ -> (as₀, is₀) `conv` (as₁, is₁)
+
     (VNeu k₀, VNeu k₁) -> k₀ `conv` k₁
 
     (u, v) -> Left $ ConvErrorTm (readBack u) (readBack v)

src/PosTT/Eval.hs

@@ -34,9 +34,9 @@ lookupInt :: Env -> Gen -> VI
 lookupInt (EnvInt _ y r)  x | y == x = r
 lookupInt (EnvCons ρ _ _) x = ρ `lookupInt` x
 
-reAppDef :: AtStage (Name -> Env -> Val)
-reAppDef d (EnvDef _   x _ _) | x == d = VVar d
-reAppDef d (EnvFib rho x v)   | x /= d = reAppDef d rho `doApp` v
+reAppDef :: AtStage (Env -> Name -> Val)
+reAppDef (EnvCons _   x _) d | x == d = VVar d
+reAppDef (EnvFib rho x v)  d | x /= d = reAppDef rho d `doApp` v
 
 
 --------------------------------------------------------------------------------
@@ -71,9 +71,13 @@ eval rho = \case
   ExtElm s ts -> vExtElm (eval rho s) (evalSys eval rho ts)
   ExtFun ws t -> doExtFun' (evalSys eval rho ws) (eval rho t)
 
-  Sum d lbl  -> VSum (reAppDef d rho) (map (evalLabel rho) lbl)
+  Sum d lbl  -> VSum (reAppDef rho d) (map (evalLabel rho) lbl)
   Con c args -> VCon c (map (eval rho) args)
-  Split f bs -> VSplitPartial (reAppDef f rho) (map (evalBranch rho) bs)
+  Split f bs -> VSplitPartial (reAppDef rho f) (map (evalBranch rho) bs)
+
+  HSum d lbl       -> VHSum (reAppDef rho d) (map (evalHLabel rho) lbl)
+  HCon c as is sys -> vHCon c (map (eval rho) as) (map (evalI rho) is) (evalSys eval rho sys)
+
 
 evalI :: Env -> I -> VI
 evalI rho = \case
@@ -116,6 +120,9 @@ evalLabel rho (Label c tel) = (c, evalTel rho tel)
 evalTel :: AtStage (Env -> Tel -> VTel)
 evalTel rho (Tel ts) = VTel ts rho
 
+evalHLabel :: AtStage (Env -> HLabel -> VHLabel)
+evalHLabel rho (HLabel c (Tel tel) is at) = (c, VHTel tel is at rho)
+
 
 --------------------------------------------------------------------------------
 ---- Closure Evaluation
@@ -182,6 +189,20 @@ tailVTel (VTel ((x, _):tel) ρ) v = VTel tel (EnvFib ρ x v)
 pattern VTelNil :: VTel
 pattern VTelNil <- VTel [] _
 
+headVHTel :: AtStage (VHTel -> Maybe VTy)
+headVHTel (VHTel ((_, a):_) _     _ ρ) = Just (eval ρ a)
+headVHTel (VHTel _          (_:_) _ _) = Nothing -- I
+
+pattern VHTelNil :: (?s :: Stage) => VSys Val -> VHTel
+pattern VHTelNil vtel <- (evalVHTelSys -> Right vtel) -- TODO: can this one simplify?
+
+evalVHTelSys :: AtStage (VHTel -> Either Val (VSys Val))
+evalVHTelSys (VHTel [] [] sys ρ) = evalSys eval ρ sys
+
+tailVHTel :: VHTel -> Either Val VI -> VHTel
+tailVHTel (VHTel ((x, _):tel) is     sys ρ) (Left v)  = VHTel tel is sys (EnvFib ρ x v)
+tailVHTel (VHTel []           (i:is) sys ρ) (Right v) = VHTel []  is sys (EnvInt ρ i v)
+
 
 --------------------------------------------------------------------------------
 ---- Prelude Combinators
@@ -323,6 +344,9 @@ doSplit :: AtStage (Val -> [VBranch] -> Val -> Val)
 doSplit _ bs (VCon c as) | Just cl <- lookup c bs = cl $$ as
 doSplit f bs (VNeu k)    = VSplit f bs k
 
+vHCon :: Name -> [Val] -> [VI] -> Either Val (VSys Val) -> Val 
+vHCon c as is = either id (VHCon c as is)
+
 
 --------------------------------------------------------------------------------
 ---- Extension Types
@@ -518,6 +542,9 @@ instance Restrictable Val where
     VCon c as          -> VCon c (as @ f)
     VSplitPartial v bs -> VSplitPartial (v @ f) (bs @ f)
 
+    VHSum _ _         -> error "VHSum @ f"
+    VHCon c as is sys -> vHCon c (as @ f) (is @ f) (sys @ f)
+
     VNeu k -> k @ f
 
 instance Restrictable Neu where

src/PosTT/Frontend/PreTerms.hs

@@ -57,7 +57,7 @@ data PTm where
   Split :: SrcSpan -> Name -> [Branch] -> PTm
 
   HSum :: SrcSpan -> Name -> [HLabel] -> PTm
-  HCon :: SrcSpan -> Name -> [PTm] -> PTm
+  -- HCon :: SrcSpan -> Name -> [PTm] -> PTm -- TODO: we could omitt this
 deriving instance Show PTm
 
 type PTy = PTm
@@ -91,8 +91,9 @@ data Sys a = Sys SrcSpan [([(ITm, ITm)], a)] deriving Show
 data Decl = Decl SrcSpan Name PTm PTy
 
 app :: SrcSpan -> PTm -> PTm -> PTm
-app _  (Con ss c as) v = Con ss c (as ++ [v])
-app ss u             v = App ss u v
+app _  (Con ss c as)  v = Con ss c (as ++ [v])
+-- app _  (HCon ss c as) v = HCon ss c (as ++ [v])
+app ss u              v = App ss u v
 
 srcSpan :: PTm -> SrcSpan
 srcSpan = \case
@@ -121,4 +122,4 @@ srcSpan = \case
   Con ss _ _         -> ss
   Split ss _ _       -> ss
   HSum ss _ _        -> ss
-  HCon ss _ _        -> ss
+  -- HCon ss _ _        -> ss

src/PosTT/Frontend/ScopeChecker.hs

@@ -55,7 +55,7 @@ moduleImports (Module _ _ imps _) = [ name | Import _ (AIdent (_, name)) <- imps
 --------------------------------------------------------------------------------
 ---- Scope Checker
 
-data SymKind = Variable | Constructor deriving Eq
+data SymKind = Variable | Constructor deriving Eq -- | HigherConstructor
 
 type ScopingEnv = [(Name, (((Int, Int), (Int, Int)), SymKind))]
 
@@ -147,14 +147,15 @@ checkExp e                     = error $ "[ScopeChecker] Missing Case: " ++ prin
 
 checkVar :: AIdent -> ScopeChecker PTm
 checkVar (AIdent (ss, id)) = asks (\ids -> guard (not $ "_" `isPrefixOf` id) *> fromString id `lookup` ids) >>= \case
-  Nothing               -> throwError $ NotBoundError id ss
-  Just (_, Variable)    -> return $ P.Var (Just ss) (fromString id)
-  Just (_, Constructor) -> return $ P.Con (Just ss) (fromString id) []
+  Nothing                     -> throwError $ NotBoundError id ss
+  Just (_, Variable)          -> return $ P.Var (Just ss) (fromString id)
+  Just (_, Constructor)       -> return $ P.Con (Just ss) (fromString id) []
+--  Just (_, HigherConstructor) -> return $ P.HCon (Just ss) (fromString id) []
 
 checkCon :: AIdent -> ScopeChecker Name
 checkCon (AIdent (ss, id)) = asks (fromString id `lookup`) >>= \case
   Just (_, Constructor) -> return $ fromString id
-  _                       -> throwError $ NotBoundError id ss
+  _                     -> throwError $ NotBoundError id ss
 
 checkFreshAIdent :: AIdent -> ScopeChecker (Name, ((Int, Int), (Int, Int)))
 checkFreshAIdent (AIdent (ss, "_")) = return ("_", ss)
@@ -165,6 +166,9 @@ checkFreshAIdent (AIdent (ss, id))  = asks (lookup (fromString id)) >>= \case
 bindAIdent' :: AIdent -> (Name -> ((Int, Int), (Int, Int)) -> ScopeChecker a) -> ScopeChecker a
 bindAIdent' id k = checkFreshAIdent id >>= \(id', ss) -> local ((id', (ss, Variable)):) (k id' ss)
 
+bindHCon :: AIdent -> (Name -> ((Int, Int), (Int, Int)) -> ScopeChecker a) -> ScopeChecker a
+bindHCon id k = checkFreshAIdent id >>= \(id', ss) -> local ((id', (ss, Constructor)):) (k id' ss)
+
 bindAIdent :: AIdent -> (Name -> ScopeChecker a) -> ScopeChecker a
 bindAIdent id k = bindAIdent' id (\id' _ -> k id')
 
@@ -210,10 +214,10 @@ uniformLabel = unifyEither (\(ssLbl, idC, argsC) -> (ssLbl, idC, argsC, [], Sys
 
 
 checkDeclHIT :: [(SrcSpan, AIdent, [Tele], [AIdent], Sys)] -> ScopeChecker [((Name, ((Int, Int),(Int, Int))), P.HLabel)]
-checkDeclHIT []                                                   = return []
-checkDeclHIT ((ssLbl, idC@(AIdent (ssIdC, _)), args, is, sys):cs) = do
+checkDeclHIT []                               = return []
+checkDeclHIT ((ssLbl, idC, args, is, sys):cs) = do
   (args', is', sys') <- checkTeles args $ \args' -> bindAIdents is $ \is' -> (args', is',) <$> checkSys sys
-  bindAIdent idC $ \idC' -> (((idC', ssIdC), P.HLabel ssLbl idC' args' is' sys'):) <$> checkDeclHIT cs
+  bindHCon idC $ \idC' ss -> (((idC', ss), P.HLabel ssLbl idC' args' is' sys'):) <$> checkDeclHIT cs
 
 checkDeclSum :: [(SrcSpan, AIdent, [Tele])] -> ScopeChecker [((Name, ((Int, Int),(Int, Int))), P.Label)]
 checkDeclSum = mapM $ \(ssLbl, idC@(AIdent (ssIdC, idCStr)), argsC) -> do

src/PosTT/HeadLinearReduction.hs

@@ -31,9 +31,9 @@ headUnfold δ = go M.empty
 
     go :: M.Map Name Int -> Tm -> Maybe Int -> (M.Map Name Int, Tm)
     go u t (Just 0) = (u, t)
-    go u t s        = case unfold t of
+    go u t steps    = case unfold t of
       Nothing      -> (u, t)
-      Just (d, t') -> go (M.alter (\e -> fmap succ e <|> Just 1) d u) t' (pred <$> s)
+      Just (d, t') -> go (M.alter (\e -> fmap succ e <|> Just 1) d u) t' (pred <$> steps)
 
 
 --------------------------------------------------------------------------------

src/PosTT/Pretty.hs

@@ -70,6 +70,8 @@ reflect = \case
   Sum _ _                -> R.Var () (reflectName "[Sum]") -- Should only occur if we print non-normalized term!
   Con c as               -> foldl1 (R.App ()) (R.Var () (reflectName c) : map reflect as)
   Split _ _              -> R.Var () (reflectName "[Split]") -- Should only occur if we print non-normalized term!
+  HSum _ _               -> R.Var () (reflectName "[HSum]") -- Should only occur if we print non-normalized term!
+  HCon c as is _         -> foldl1 (R.App ()) (R.Var () (reflectName c) : map reflect as ++ map reflectFormula is)
 
 reflectSysBinder :: Sys (TrIntBinder Tm) -> R.SysBinder' ()
 reflectSysBinder (Sys bs) = R.SysBinder () (map reflectSideBinder bs)

src/PosTT/Quotation.hs

@@ -39,6 +39,8 @@ instance ReadBack Val where
    VSum d _            -> readBack d
    VCon c as           -> Con c (map readBack as)
    VSplitPartial f _   -> readBack f
+   VHSum d _           -> readBack d
+   VHCon c as is sys   -> HCon c (map readBack as) (map readBack is) (readBack sys)
    VNeu k              -> readBack k
 
 instance ReadBack Neu where

src/PosTT/Terms.hs

@@ -40,9 +40,15 @@ data Tm where
   Sum :: Name -> [Label] -> Tm
   Con :: Name -> [Tm] -> Tm
   Split :: Name -> [Branch] -> Tm
+
+  HSum :: Name -> [HLabel] -> Tm
+  HCon :: Name -> [Tm] -> [I] -> Sys Tm -> Tm
 type Ty = Tm
 
-instance IsString Tm where fromString = Var . fromString
+instance IsString Tm where 
+  fromString :: String -> Tm
+  fromString = Var . fromString
+
 
 ---- Binder (We explicitly mark how variables are bound above)
 
@@ -87,6 +93,8 @@ data Branch = Branch Name SplitBinder
 pattern BBranch :: Name -> [Name] -> Tm -> Branch
 pattern BBranch n xs t = Branch n (SplitBinder xs t)
 
+data HLabel = HLabel Name Tel [Gen] (Sys Tm)
+
 
 --------------------------------------------------------------------------------
 ---- Base Category