Remove commented code for GlueLine, GlueLineElem, CompElem and ElimComp

diff --git a/CTT.hs b/CTT.hs
index edd290ba955b52a57a7c7371a22024c4e5eaea1a..8eab044815242ebc5faa421fc4692d1074863b2e 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -96,11 +96,9 @@ data Ter = App Ter Ter
            -- labelled sum c1 A1s,..., cn Ans (assumes terms are constructors)
          | Sum Loc Ident [Label] -- TODO: should only contain OLabels
          | HSum Loc Ident [Label]
-
            -- undefined and holes
          | Undef Loc Ter -- Location and type
          | Hole Loc
-
            -- Id type
          | IdP Ter Ter Ter
          | Path Name Ter
@@ -111,9 +109,6 @@ data Ter = App Ter Ter
            -- Glue
          | Glue Ter (System Ter)
          | GlueElem Ter (System Ter)
-           -- GlueLine: connecting any type to its glue with identities
-         -- | GlueLine Ter Formula Formula
-         -- | GlueLineElem Ter Formula Formula
   deriving Eq
 
 -- For an expression t, returns (u,ts) where u is no application and t = u ts
@@ -146,7 +141,6 @@ data Val = VU
          | VIdP Val Val Val
          | VPath Name Val
          | VComp Val Val (System Val)
-         -- | VTrans Val Val
 
            -- Glue values
          | VGlue Val (System Val)
@@ -155,15 +149,10 @@ data Val = VU
            -- Composition for HITs; the type is constant
          | VHComp Val Val (System Val)
 
-           -- GlueLine values
-         -- | VGlueLine Val Formula Formula
-         -- | VGlueLineElem Val Formula Formula
-
            -- Neutral values:
          | VVar Ident Val
          | VFst Val
          | VSnd Val
-           -- VUnGlueElem val type equivs
          | VUnGlueElem Val Val (System Val)
          | VSplit Val Val
          | VApp Val Val
@@ -192,55 +181,6 @@ isNeutralSystem = any isNeutral . Map.elems
 -- isNeutralPath (VPath _ v) = isNeutral v
 -- isNeutralPath _ = True
 
--- isNeutralTrans :: Val -> Val -> Bool
--- isNeutralTrans (VPath i a) u = foo i a u
---   where foo :: Name -> Val -> Val -> Bool
---         foo i a u | isNeutral a = True
---         foo i (Ter Sum{} _) u   = isNeutral u
---         foo i (VGlue _ as) u    =
---           let shasBeta = shape as `face` (i ~> 0)
---           in shasBeta /= Map.empty && eps `Map.notMember` shasBeta && isNeutral u
---         foo _ _ _ = False
--- -- TODO: case for VGLueLine
--- isNeutralTrans u _ = isNeutral u
-
--- -- TODO: fix
--- isNeutralComp :: Val -> Val -> System Val -> Bool
--- isNeutralComp (VPath i a) u ts = isNeutralComp' i a u ts
---   where isNeutralComp' i a u ts | isNeutral a = True
---         isNeutralComp' i (Ter Sum{} _) u ts   = isNeutral u || isNeutralSystem ts
---         isNeutralComp' i (VGlue _ as) u ts    =
---           isNeutral u && isNeutralSystem (filterWithKey testFace ts)
---             where shas = shape as `face` (i ~> 0)
---                   testFace beta _ = let shasBeta = shas `face` beta
---                                     in shasBeta /= Map.empty && eps `Map.member` shasBeta
---         isNeutralComp' _ _ _ _ = False
--- isNeutralComp _ u _ = isNeutral u
-
--- -- TODO: adapt for non-regular setting
--- isNeutralComp :: Val -> Val -> System Val -> Bool
--- isNeutralComp a _ _ | isNeutral a = True
--- isNeutralComp (Ter Sum{} _) u ts  = isNeutral u || isNeutralSystem ts
--- isNeutralComp (VGlue _ as) u ts =
---   isNeutral u || isNeutralSystem (filterWithKey testFace ts)
---   where shas = shape as
---         testFace beta _ = let shasBeta = shas `face` beta
---                           in not (Map.null shasBeta || eps `Map.member` shasBeta)
-
-
--- TODO
--- isNeutralComp (VGlueLine _ phi psi) u ts =
---   isNeutral u || isNeutralSystem (filterWithKey (not . test) ts) || and (elems ws)
---   where fs = invFormula psi One
---         test alpha _ = phi `face` alpha `elem` [Dir Zero, Dir One] ||
---                        psi `face` alpha == Dir One
---         ws = mapWithKey
---                (\alpha -> let phiAlpha0 = invFormula (phi `face` alpha) Zero
---                           in isNeutral (u `face` alpha) || isNeutralSystem )
---                  fs
--- isNeutralComp _ _ _ = False
-
-
 mkVar :: Int -> String -> Val -> Val
 mkVar k x = VVar (x ++ show k)
 
@@ -389,10 +329,6 @@ showTer v = case v of
   Fill e t ts        -> text "fill" <+> showTers [e,t] <+> text (showSystem ts)
   Glue a ts          -> text "glue" <+> showTer1 a <+> text (showSystem ts)
   GlueElem a ts      -> text "glueElem" <+> showTer1 a <+> text (showSystem ts)
-  -- GlueLine a phi psi -> text "glueLine" <+> showTer1 a <+>
-  --                       showFormula phi <+> showFormula psi
-  -- GlueLineElem a phi psi -> text "glueLineElem" <+> showTer1 a <+>
-  --                           showFormula phi <+> showFormula psi
 
 showTers :: [Ter] -> Doc
 showTers = hsep . map showTer1
@@ -447,10 +383,6 @@ showVal v = case v of
   VComp v0 v1 vs    -> text "comp" <+> showVals [v0,v1] <+> text (showSystem vs)
   VGlue a ts        -> text "glue" <+> showVal1 a <+> text (showSystem ts)
   VGlueElem a ts    -> text "glueElem" <+> showVal1 a <+> text (showSystem ts)
-  -- VGlueLine a phi psi     -> text "glueLine" <+> showFormula phi
-  --                            <+> showFormula psi  <+> showVal1 a
-  -- VGlueLineElem a phi psi -> text "glueLineElem" <+> showFormula phi
-  --                            <+> showFormula psi  <+> showVal1 a
 
 showPath :: Val -> Doc
 showPath e = case e of

diff --git a/Exp.cf b/Exp.cf
index 8d8c8410d39687850cc2dc2f2f6009754484b5ca..db7234face5a359b2e1076f07a6fcca34cd9eafb 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -36,10 +36,6 @@ Trans.        Exp3 ::= "transport" Exp4 Exp4 ;
 Fill.         Exp3 ::= "fill" Exp4 Exp4 System ;
 Glue.         Exp3 ::= "glue" Exp4 System ;
 GlueElem.     Exp3 ::= "glueElem" Exp4 System ;
--- CompElem.     Exp3 ::= "compElem" Exp4 System Exp4 System ;
--- GlueLine.     Exp3 ::= "glueLine" Formula Formula Exp4 ;
--- GlueLineElem. Exp3 ::= "glueLineElem" Formula Formula Exp4 ;
--- ElimComp.     Exp3 ::= "elimComp" Exp4 System Exp4 ;
 Fst.          Exp4 ::= Exp4 ".1" ;
 Snd.          Exp4 ::= Exp4 ".2" ;
 Pair.         Exp5 ::= "(" Exp "," [Exp] ")" ;

diff --git a/Resolver.hs b/Resolver.hs
index 46cdde1ea4840c528e1eaa8c67ad848790fb05c7..8d8585bc55ec078cf9986c60a1bbfafa02d1ff3f 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -208,14 +208,6 @@ resolveExp e = case e of
   Trans u v     -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> pure Map.empty
   Glue u ts     -> CTT.Glue <$> resolveExp u <*> resolveSystem ts
   GlueElem u ts -> CTT.GlueElem <$> resolveExp u <*> resolveSystem ts
-  -- GlueLine phi psi u ->
-  --   CTT.GlueLine <$> resolveExp u <*> resolveFormula phi <*> resolveFormula psi
-  -- GlueLineElem phi psi u ->
-  --   CTT.GlueLineElem <$> resolveExp u <*> resolveFormula phi
-  --     <*> resolveFormula psi
-  -- CompElem a es t ts -> CTT.CompElem <$> resolveExp a <*> resolveSystem es
-  --                                    <*> resolveExp t <*> resolveSystem ts
-  -- ElimComp a es t    -> CTT.ElimComp <$> resolveExp a <*> resolveSystem es <*> resolveExp t
   _ -> do
     modName <- asks envModule
     throwError ("Could not resolve " ++ show e ++ " in module " ++ modName)

diff --git a/TypeChecker.hs b/TypeChecker.hs
index c1b33e41c8cf8d7505af9ea09d019e1c22eafa43..e39535068c0a503413570ead8c01c9b24250f443 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -209,14 +209,6 @@ check a t = case (a,t) of
   --   check va u\r
   --   vu <- evalTyping u\r
   --   checkGlueElem vu ts us\r
-  -- (VU,GlueLine b phi psi) -> do\r
-  --   check VU b\r
-  --   checkFormula phi\r
-  --   checkFormula psi\r
-  -- (VGlueLine vb phi psi,GlueLineElem r phi' psi') -> do\r
-  --   check vb r\r
-  --   unlessM ((phi,psi) === (phi',psi')) $\r
-  --     throwError "GlueLineElem: formulas don't match"\r
   _ -> do\r
     v <- infer t\r
     unlessM (v === a) $\r
@@ -413,10 +405,6 @@ infer e = case e of
     case t of\r
       VIdP a _ _ -> return $ a @@ phi\r
       _ -> throwError (show e ++ " is not a path")\r
-  -- Trans p t -> do\r
-  --   (a0,a1) <- checkPath (constPath VU) p\r
-  --   check a0 t\r
-  --   return a1\r
   Comp a t0 ps -> do\r
     (va0, va1) <- checkPath (constPath VU) a\r
     va <- evalTyping a\r
@@ -432,31 +420,6 @@ infer e = case e of
     rho <- asks env\r
     let vps = evalSystem rho ps\r
     return (VIdP va vt (compLine va vt vps))\r
-  -- CompElem a es u us -> do\r
-  --   check VU a\r
-  --   rho <- asks env\r
-  --   let va = eval rho a\r
-  --   ts <- checkPathSystem a VU es\r
-  --   let ves = evalSystem rho es\r
-  --   unless (keys es == keys us)\r
-  --     (throwError ("Keys don't match in " ++ show es ++ " and " ++ show us))\r
-  --   check va u\r
-  --   let vu = eval rho u\r
-  --   checkSystemsWith ts us (const check)\r
-  --   let vus = evalSystem rho us\r
-  --   checkCompSystem vus\r
-  --   checkSystemsWith ves vus (\alpha eA vuA ->\r
-  --     unlessM (transNegLine eA vuA === (vu `face` alpha)) $\r
-  --       throwError $ "Malformed compElem: " ++ show us)\r
-  --   return $ compLine VU va ves\r
-  -- ElimComp a es u -> do\r
-  --   check VU a\r
-  --   rho <- asks env\r
-  --   let va = eval rho a\r
-  --   checkPathSystem a VU es\r
-  --   let ves = evalSystem rho es\r
-  --   check (compLine VU va ves) u\r
-  --   return va\r
   PCon c a es phis -> do\r
     check VU a\r
     va <- evalTyping a\r