From 7b8926c4cf9aa52f8c2c84361fafb82e621f3225 Mon Sep 17 00:00:00 2001 From: Anders Date: Thu, 18 Jun 2015 15:52:59 +0200 Subject: [PATCH] Remove commented code for GlueLine, GlueLineElem, CompElem and ElimComp --- CTT.hs | 68 -------------------------------------------------- Exp.cf | 4 --- Resolver.hs | 8 ------ TypeChecker.hs | 37 --------------------------- 4 files changed, 117 deletions(-) diff --git a/CTT.hs b/CTT.hs index edd290b..8eab044 100644 --- 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 8d8c841..db7234f 100644 --- 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 46cdde1..8d8585b 100644 --- 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 c1b33e4..e395350 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -209,14 +209,6 @@ check a t = case (a,t) of -- check va u -- vu <- evalTyping u -- checkGlueElem vu ts us - -- (VU,GlueLine b phi psi) -> do - -- check VU b - -- checkFormula phi - -- checkFormula psi - -- (VGlueLine vb phi psi,GlueLineElem r phi' psi') -> do - -- check vb r - -- unlessM ((phi,psi) === (phi',psi')) $ - -- throwError "GlueLineElem: formulas don't match" _ -> do v <- infer t unlessM (v === a) $ @@ -413,10 +405,6 @@ infer e = case e of case t of VIdP a _ _ -> return $ a @@ phi _ -> throwError (show e ++ " is not a path") - -- Trans p t -> do - -- (a0,a1) <- checkPath (constPath VU) p - -- check a0 t - -- return a1 Comp a t0 ps -> do (va0, va1) <- checkPath (constPath VU) a va <- evalTyping a @@ -432,31 +420,6 @@ infer e = case e of rho <- asks env let vps = evalSystem rho ps return (VIdP va vt (compLine va vt vps)) - -- CompElem a es u us -> do - -- check VU a - -- rho <- asks env - -- let va = eval rho a - -- ts <- checkPathSystem a VU es - -- let ves = evalSystem rho es - -- unless (keys es == keys us) - -- (throwError ("Keys don't match in " ++ show es ++ " and " ++ show us)) - -- check va u - -- let vu = eval rho u - -- checkSystemsWith ts us (const check) - -- let vus = evalSystem rho us - -- checkCompSystem vus - -- checkSystemsWith ves vus (\alpha eA vuA -> - -- unlessM (transNegLine eA vuA === (vu `face` alpha)) $ - -- throwError $ "Malformed compElem: " ++ show us) - -- return $ compLine VU va ves - -- ElimComp a es u -> do - -- check VU a - -- rho <- asks env - -- let va = eval rho a - -- checkPathSystem a VU es - -- let ves = evalSystem rho es - -- check (compLine VU va ves) u - -- return va PCon c a es phis -> do check VU a va <- evalTyping a -- 2.34.1