implement composition for HITs

intro.tt

@@ -278,6 +278,9 @@ hcomp {A} {phi} u a0 = comp (\i -> A) {phi} u a0
 transRefl : {A : Type} {x : A} {y : A} (p : Path x y) -> Path (trans p refl) p
 transRefl p j i = fill (\i -> A) {ior i (inot i)} (\k [ (i = i0) -> x, (i = i1) -> y ]) (inS (p i)) (inot j)
 
+transpFill : {A : Type} (x : A) -> Path x (transp (\i -> A) x)
+transpFill {A} x i = fill (\i -> A) (\k []) (inS x) i
+
 -- Reduction of composition
 ---------------------------
 --
@@ -623,11 +626,13 @@ notp = univalence (IsoToEquiv (not, involToIso not notInvol))
 --
 -- This follows from setting bottom := ∀ A, A.
 
-bottom : Type
-bottom = {A : Type} -> A
+data bottom : Type where {}
 
 elimBottom : (P : bottom -> Type) -> (b : bottom) -> P b
-elimBottom P x = x
+elimBottom P = \case {}
+
+absurd : {P : Type} -> bottom -> P
+absurd = \case {}
 
 -- We prove that true != false by transporting along the path
 --
@@ -642,7 +647,7 @@ elimBottom P x = x
 -- and evaluate the if at either end.
 
 trueNotFalse : Path true false -> bottom
-trueNotFalse p {A} = transp (\i -> if (Bool -> Bool) A (p i)) id
+trueNotFalse p = transp (\i -> if (Bool -> Bool) bottom (p i)) id
 
 -- To be an h-Set is to have no "higher path information". Alternatively,
 --
@@ -823,6 +828,9 @@ helix = \case
   base -> Int
   loop i -> intPath i
 
+loopP : Path base base
+loopP i = loop i
+
 winding : Path base base -> Int
 winding p = transp (\i -> helix (p i)) (pos zero)
 
@@ -898,6 +906,9 @@ Susp_to_poSusp_to_Susp = \case
 unitEta : (x : Unit) -> Path x tt
 unitEta = \case tt -> refl
 
+unitContr : isContr Unit
+unitContr = (tt, \x -> sym (unitEta x))
+
 poSusp_to_Susp_to_poSusp : {A : Type} -> (x : poSusp A) -> Path (Susp_to_poSusp (poSusp_to_Susp x)) x
 poSusp_to_Susp_to_poSusp {A} = \case
   inl x -> cong inl (sym (unitEta x))
@@ -1023,4 +1034,22 @@ four : Int
 four = multInt two two
 
 sixteen : Int
-sixteen = multInt four four
+sixteen = multInt four four
+
+isProp : Type -> Type
+isProp A = (x : A) (y : A) -> Path x y
+
+data Sq (A : Type) : Type where
+  inc : A -> Sq A
+  sq i : (x : A) (y : A) -> Sq A [ (i = i0) -> inc x, (i = i1) -> inc y ]
+
+Sq_rec : {A : Type} {B : Type}
+      -> isProp B
+      -> (f : A -> B)
+      -> Sq A -> B
+Sq_rec prop f = \case
+  inc x -> f x
+  sq x y i -> prop (f x) (f y) i
+
+hitTranspExample : Path (inc false) (inc true)
+hitTranspExample i = transp (\i -> Sq (notp i)) (sq true false i)

src/Elab.hs

@@ -4,6 +4,7 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE EmptyCase #-}
 module Elab where
 
 import Control.Arrow (Arrow(first))
@@ -330,7 +331,11 @@ skipLams k = do
   (Lam P.Im n . ) <$> skipLams (k - 1)
 
 checkLetItems :: Map Text (Maybe (Name, NFType)) -> [P.LetItem] -> ([(Name, Term, Term)] -> ElabM a) -> ElabM a
-checkLetItems _   [] cont = cont []
+checkLetItems map   [] cont = do
+  for_ (Map.toList map) $ \case
+    (_, Nothing) -> pure ()
+    (n, Just _) -> throwElab $ DeclaredUndefined (Bound n 0)
+  cont []
 checkLetItems map (P.LetDecl v t:xs) cont = do
   t <- check t VTypeω
   t_nf <- eval t
@@ -616,3 +621,6 @@ data UnsaturatedCon = UnsaturatedCon { theConstr :: Name }
 data NotACon = NotACon { theNotConstr :: Name }
   deriving          (Show, Typeable)
   deriving anyclass (Exception)
+
+newtype DeclaredUndefined = DeclaredUndefined { declaredUndefName :: Name }
+  deriving (Eq, Show, Exception)

src/Elab/Eval.hs

@@ -588,7 +588,7 @@ forceIO x = pure x
 force :: Value -> Value
 force = unsafePerformIO . forceIO
 
-applProj :: Value -> Projection -> Value
+applProj :: HasCallStack => Value -> Projection -> Value
 applProj fun (PApp p arg)     = vApp p fun arg
 applProj fun (PIElim l x y i) = ielim l x y fun i
 applProj fun (POuc a phi u)   = outS a phi u fun

src/Elab/WiredIn.hs

@@ -302,10 +302,10 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
     VNe (HData False _) args ->
       case force a0 of
         VNe (HCon con_type con_name) con_args ->
-          VNe (HCon con_type con_name) $ compConArgs (length args) (a @@) con_type con_args phi u
+          VNe (HCon con_type con_name) $ compConArgs makeSetFiller (length args) (a @@) con_type con_args phi u
         _ -> VComp a phi u (VInc (a @@ VI0) phi a0)
 
-    VNe (HData True _) args -> compHIT (length args) (a @@) phi u incA0
+    VNe (HData True name) args -> compHIT name (length args) (a @@) phi u incA0
 
     VLam{} -> error $ "comp VLam " ++ show (prettyTm (quote a))
     sys@VSystem{} -> error $ "comp VSystem: " ++ show (prettyTm (quote sys))
@@ -328,50 +328,55 @@ forceAndGlue v =
     v@VGlueTy{} -> v
     y -> VGlueTy y VI1 (fun (const y)) (fun (const (idEquiv y)))
 
-compHIT :: HasCallStack => Int -> (NFEndp -> NFSort) -> NFEndp -> Value -> Value -> Value
-compHIT 0 a phi u a0 =
-  case phi of
+compHIT :: HasCallStack => Name -> Int -> (NFEndp -> NFSort) -> NFEndp -> Value -> Value -> Value
+compHIT name n a phi u a0 =
+  case force phi of
     VI1 -> u @@ VI1 @@ VItIsOne
-    VI0 -> compOutS (a VI0) phi u a0
-    _ -> VHComp (a VI0) phi u a0
-compHIT _ a phi u a0 = error $ unlines
-  [ "*** TODO: composition for HIT: "
-  , "domain = " ++ show (prettyTm (quote (zonk (fun a))))
-  , "phi = " ++ show (prettyTm (quote (zonk phi)))
-  , "u = " ++ show (prettyTm (quote (zonk u)))
-  , "a0 = " ++ show (prettyTm (quote (zonk a0)))
-  ]
-
-compConArgs :: Int -> (NFEndp -> Value) -> Value -> Seq.Seq Projection -> NFEndp -> Value -> Seq.Seq Projection
-compConArgs total_args fam = go total_args where
+    VI0 -> transHit name a VI0 (compOutS (a VI0) phi u a0)
+    x -> go n a x u a0
+  where
+    go 0 a phi u a0 = VHComp (a VI0) phi u a0
+    go _ a phi u a0 = VHComp (a VI1) phi (system \i n -> squeezeHit name a VI0 (\i -> u @@ i @@ n) i) (transHit name a VI0 (compOutS (a VI1) phi (u @@ VI1 @@ VItIsOne) a0))
+
+compConArgs :: (Name -> Int -> Value -> t1 -> t2 -> Value -> Value)
+            -> Int
+            -> (Value -> Value)
+            -> Value
+            -> Seq.Seq Projection
+            -> t1 -> t2
+            -> Seq.Seq Projection
+compConArgs makeFiller total_args fam = go total_args where
   go _ _ Seq.Empty _ _ = Seq.Empty
   go nargs (VPi p dom (Closure _ rng)) (PApp p' y Seq.:<| xs) phi u
-    | nargs > 0 = assert (p == p') $ go (nargs - 1) (rng (smuggle (fun (\i -> nthArg (total_args - nargs) (fam i))))) xs phi u
+    | nargs > 0 = assert (p == p') $
+        PApp p' (nthArg (total_args - nargs) (fam VI1)) Seq.:<| go (nargs - 1) (rng (smuggle (fun (\i -> nthArg (total_args - nargs) (fam i))))) xs phi u
     | otherwise = assert (p == p') $
-      let fill = makeFiller nargs dom phi u y
+      let fill = makeFiller typeArgument nargs dom phi u y
        in PApp p' (fill @@ VI1) Seq.:<| go (nargs - 1) (rng fill) xs phi u
   go _ _ _ _ _ = error $ "invalid constructor"
 
-  nthArg i (VNe hd s) =
-    case s Seq.!? i of
-      Just (PApp _ t) -> t
-      _ -> error $ "invalid " ++ show i ++ "th argument to data type " ++ show hd
-  nthArg i (VSystem vs) = VSystem (fmap (nthArg i) vs)
-  nthArg i xs = error $ "can't get " ++ show i ++ "th argument of " ++ show (prettyTm (quote xs))
-
-  makeFiller nth (VNe (HData _ n') args) phi u a0
-    | n' == typeArgument =
-      fun $ fill (makeDomain args) phi (system \i is1 -> nthArg nth (u @@ i @@ is1) ) a0
-  makeFiller _ _ _ _ a0 = fun (const a0)
-
-  makeDomain (PApp _ x Seq.:<| xs) = fun \i -> foldl (\t (~(PApp _ x)) -> t @@ (x @@ i)) (x @@ i) xs
-  makeDomain _ = error "somebody smuggled something that smells"
-
   smuggle x = VNe (HData False typeArgument) (Seq.singleton (PApp P.Ex x))
 
   typeArgument = unsafePerformIO newName
   {-# NOINLINE typeArgument #-}
 
+makeSetFiller :: Name -> Int -> Value -> NFEndp -> Value -> Value -> Value
+makeSetFiller typeArgument nth (VNe (HData _ n') args) phi u a0
+  | n' == typeArgument =
+    fun $ fill (makeDomain args) phi (system \i is1 -> nthArg nth (u @@ i @@ is1) ) a0
+  where
+    makeDomain (PApp _ x Seq.:<| xs) = fun \i -> foldl (\t (~(PApp _ x)) -> t @@ (x @@ i)) (x @@ i) xs
+    makeDomain _ = error "somebody smuggled something that smells"
+makeSetFiller _ _ _ _ _ a0 = fun (const a0)
+
+nthArg :: Int -> Value -> Value
+nthArg i (VNe hd s) =
+  case s Seq.!? i of
+    Just (PApp _ t) -> t
+    _ -> error $ "invalid " ++ show i ++ "th argument to data type " ++ show hd
+nthArg i (VSystem vs) = VSystem (fmap (nthArg i) vs)
+nthArg i xs = error $ "can't get " ++ show i ++ "th argument of " ++ show (prettyTm (quote xs))
+
 compOutS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
 compOutS a b c d = compOutS a b c (force d) where
   compOutS _ _hi _0 vl@VComp{}   = vl
@@ -462,6 +467,43 @@ contr a aC phi u =
 transp :: (NFEndp -> Value) -> Value -> Value
 transp line a0 = comp (fun line) VI0 (system \_ _ -> VSystem mempty) (VInc (line VI0) VI0 a0)
 
+gtrans :: (NFEndp -> Value) -> NFEndp -> Value -> Value
+gtrans line phi a0 = comp (fun line) phi (system \_ _ -> mkVSystem (Map.singleton phi a0)) (VInc (line VI0) VI0 a0)
+
+transHit :: Name -> (NFEndp -> Value) -> NFEndp -> Value -> Value
+transHit name line phi (VHComp _ psi u u0) = VHComp (line VI1) psi (system \i j -> transHit name line phi (u @@ i @@ j)) (transHit name line phi u0)
+transHit name line phi (VNe (HCon con_type con_name) spine) | ourType = x' where
+  x' = VNe (HCon con_type con_name) $ compConArgs (makeTransFiller name) nargs line con_type spine phi ()
+  (_, VNe hd (length -> nargs)) = unPi con_type
+  ourType = case hd of
+    HData True n' -> n' == name
+    _ -> False
+
+transHit name line phi (VNe (HPCon sys con_type con_name) spine) | ourType = x' where
+  x' = VNe (HPCon (mapVSystem rec sys) con_type con_name) $ compConArgs (makeTransFiller name) nargs line con_type spine phi ()
+  rec = transHit name line phi
+  (_, VNe hd (length -> nargs)) = unPi con_type
+  ourType = case hd of
+    HData True n' -> n' == name
+    _ -> False
+
+transHit name line phi (VSystem xs) = mkVSystem (fmap (transHit name line phi) xs)
+transHit _ line phi a0 = gtrans line phi a0
+
+fillHit :: Name -> (NFEndp -> Value) -> NFEndp -> Value -> NFEndp -> Value
+fillHit name a phi a0 i = transHit name (\j -> a (iand i j)) (phi `ior` inot i) a0 where
+
+squeezeHit :: Name -> (NFEndp -> Value) -> NFEndp -> (NFEndp -> Value) -> NFEndp -> Value
+squeezeHit name a phi x i = transHit name (\j -> a (ior i j)) (phi `ior` i) (x i)
+
+makeTransFiller :: Name -> Name -> p -> Value -> NFEndp -> () -> Value -> Value
+makeTransFiller thedata typeArgument _ (VNe (HData _ n') args) phi () a0
+  | n' == typeArgument = fun (fillHit thedata (makeDomain args) phi a0)
+  where
+    makeDomain (PApp _ x Seq.:<| xs) = \i -> foldl (\t (~(PApp _ x)) -> t @@ (x @@ i)) (x @@ i) xs
+    makeDomain _ = error "somebody smuggled something that smells"
+makeTransFiller _ _ _ _ _ _ a0 = fun (const a0)
+
 makeEquiv :: Name -> Value -> Value
 makeEquiv var vne = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y)
   where

src/Main.hs

@@ -72,7 +72,7 @@ evalArgExpr env str =
 
 enterReplIn :: ElabEnv -> IO ()
 enterReplIn env = runInputT defaultSettings (loop env') where
-  env' = env { commHook = putStrLn . show . prettyTm . quote }
+  env' = env { commHook = T.putStrLn . render . prettyTm . quote . zonk }
 
   loop :: ElabEnv -> InputT IO ()
   loop env = do
@@ -102,7 +102,7 @@ checkFiles files = runElab (go files ask) =<< emptyEnv where
         | otherwise ->
           let
             pos = fromJust (Map.lookup v (whereBound env))
-           in withSpan (fst pos) (snd pos) $ throwElab $ DeclaredUndefined v
+           in withSpan (fst pos) (snd pos) $ throwElab $ Elab.DeclaredUndefined v
       _ -> pure ()
 
     metas <- liftIO $ readIORef (unsolvedMetas env)
@@ -182,7 +182,7 @@ displayExceptions lines =
       putStrLn $ "Unknown primitive: " ++ T.unpack x
   , Handler \(NotInScope x) -> do
       putStrLn $ "Variable not in scope: " ++ show (pretty x)
-  , Handler \(DeclaredUndefined n) -> do
+  , Handler \(Elab.DeclaredUndefined n) -> do
       putStrLn $ "Name declared but not defined: " ++ show (pretty n)
   ]
 
@@ -212,9 +212,6 @@ squiggleUnder (Posn l c) (Posn l' c') file
      in T.unlines [ padding, line, padding <> squiggle ]
   | otherwise = T.unlines (take (l' - l) (drop l (T.lines file)))
 
-newtype DeclaredUndefined = DeclaredUndefined { declaredUndefName :: Name }
-  deriving (Eq, Show, Exception)
-
 dumpTokens :: Alex ()
 dumpTokens = do
   t <- alexMonadScan

src/Presyntax/Lexer.x

@@ -7,6 +7,8 @@ import qualified Data.Text as T
 
 import Presyntax.Tokens
 
+import Debug.Trace
+
 }
 
 %wrapper "monadUserState-bytestring"
@@ -38,7 +40,7 @@ tokens :-
 <0> \[                            { always TokOSquare }
 
 <0> \)                            { always TokCParen }
-<0> \}                            { always TokCBrace }
+<0> \}                            { closeBrace }
 <0> \]                            { always TokCSquare }
 
 <0> \;                            { always TokSemi }
@@ -71,6 +73,7 @@ tokens :-
 -- layout: indentation of the next token is context for offside rule
 <layout> {
   \n ;
+  \{ { openBrace }
   () { startLayout }
 }
 
@@ -145,6 +148,20 @@ startLayout (AlexPn _ line col, _, _, _) _ = do
     else mapUserState $ \s -> s { layoutColumns = col:layoutColumns s }
   pure (Token TokLStart line col)
 
+openBrace :: AlexInput -> Int64 -> Alex Token
+openBrace (AlexPn _ line col, _, _, _) _ = do
+  popStartCode
+  mapUserState $ \s -> s { layoutColumns = minBound:layoutColumns s }
+  pure (Token TokOBrace line col)
+
+closeBrace :: AlexInput -> Int64 -> Alex Token
+closeBrace (AlexPn _ line col, _, _, _) _ = do
+  ~(col':tail) <- layoutColumns <$> getUserState
+  if col' < 0
+    then mapUserState $ \s -> s { layoutColumns = tail }
+    else pure ()
+  pure (Token TokCBrace line col)
+
 variableOrKeyword :: AlexAction Token
 variableOrKeyword (AlexPn _ l c, _, s, _) size =
   let text = T.decodeUtf8 (Lbs.toStrict (Lbs.take size s)) in

src/Presyntax/Parser.y

@@ -1,5 +1,5 @@
 {
-{-# LANGUAGE FlexibleInstances, ViewPatterns #-}
+{-# LANGUAGE FlexibleContexts, FlexibleInstances, ViewPatterns #-}
 module Presyntax.Parser where
 
 import qualified Data.Text as T
@@ -81,7 +81,7 @@ Exp :: { Expr }
 Exp
   : '\\' LambdaList '->' Exp             { span $1 $4 $ makeLams $2 $4 }
   | '\\' MaybeLambdaList '[' System ']'  { span $1 $5 $ makeLams $2 $ LamSystem $4 }
-  | '\\' 'case' START CaseList END       { span $1 $5 $ LamCase $4 }
+  | '\\' 'case' Block(CaseList)          { span $1 $3 $ LamCase (thd $3) }
   | '(' var ':' Exp ')' ProdTail         { span $1 $6 $ Pi Ex (getVar $2) $4 $6 }
   | '{' var ':' Exp '}' ProdTail         { span $1 $6 $ Pi Im (getVar $2) $4 $6 }
   | ExpApp '->' Exp                      { span $1 $3 $ Pi Ex (T.singleton '_') $1 $3 }
@@ -89,8 +89,7 @@ Exp
   | '(' var ':' Exp ')' '*'  Exp         { span $1 $7 $ Sigma (getVar $2) $4 $7 }
   | ExpApp '*' Exp                       { span $1 $3 $ Sigma (T.singleton '_') $1 $3 }
 
-  | 'let' START LetList END 'in' Exp     { span $1 $6 $ Let $3 $6 }
-  | 'let' START LetList END Exp          { span $1 $5 $ Let $3 $5 }
+  | 'let' Block(LetList) 'in' Exp        { span $1 $4 $ Let (thd $2) $4 }
 
   | ExpApp                               { $1 }
 
@@ -149,7 +148,8 @@ CaseItem :: { (Pattern, Expr) }
   : Pattern '->' Exp { ($1, $3) }
   
 CaseList :: { [(Pattern, Expr)] }
-  : CaseItem                { [$1] }
+  :                         { [] }
+  | CaseItem                { [$1] }
   | CaseItem Semis CaseList { $1:$3 }
 
 Pattern :: { Pattern }
@@ -163,12 +163,14 @@ Statement :: { Statement }
   : VarList ':' Exp                  { spanSt $1 $3 $ Decl (thd $1) $3 }
   | var LhsList '=' Rhs              { spanSt $1 $4 $ Defn (getVar $1) (makeLams $2 $4) }
   | '{-#' Pragma '#-}'               { spanSt $1 $3 $ $2 }
-  | 'postulate' START Postulates END { spanSt $1 $4 $ Postulate $3 }
-  | 'data' var Parameters ':' Exp 'where' START Constructors END
-    { spanSt $1 $9 $ Data (getVar $2) $3 $5 $8 }
+
+  | 'postulate' Block(Postulates)    { spanSt $1 $2 $ Postulate (thd $2) }
+  | 'data' var Parameters ':' Exp 'where' Block(Constructors)
+    { spanSt $1 $7 $ Data (getVar $2) $3 $5 (thd $7) }
 
 Constructors :: { [(Posn, Posn, Constructor)] }
-  : var ':' Exp                          { [(startPosn $1, endPosn $3, Point (getVar $1) $3)] }
+  :                                      { [] }
+  | var ':' Exp                          { [(startPosn $1, endPosn $3, Point (getVar $1) $3)] }
   | var PatVarList ':' Exp '[' Faces ']' { [(startPosn $1, endPosn $7, Path (getVar $1) (thd $2) $4 $6)] }
   | var ':' Exp Semis Constructors       { (startPosn $1, endPosn $3, Point (getVar $1) $3):$5 }
   | var PatVarList ':' Exp '[' Faces ']' Semis Constructors
@@ -250,6 +252,10 @@ FAtom :: { Formula }
       x -> parseError (x, ["i0", "i1"])
   }
 
+Block(p)
+  : START p END { (startPosn $1, endPosn $3, $2) }
+  | '{' p '}'   { (startPosn $1, endPosn $3, $2) }
+
 {
 lexer cont = alexMonadScan >>= cont
 

src/Syntax.hs

@@ -308,3 +308,9 @@ data Projection
 
 data Boundary = Boundary { getBoundaryNames :: [Name], getBoundaryMap :: Value }
   deriving (Eq, Show, Ord)
+
+unPi :: Value -> ([(Plicity, Value)], Value)
+unPi (VPi p d (Closure n k)) =
+  let (a, x) = unPi (k (VVar n))
+   in ((p, d):a, x)
+unPi x = ([], x)