From 371e1dc0eb956858344091339d87d6e9c6b50efb Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 7 Jul 2016 16:14:51 +0200 Subject: [PATCH] rename visible to transparent and fix printing of glue --- CTT.hs | 30 +++++++++++++++--------------- Eval.hs | 2 +- Exp.cf | 20 ++++++++++---------- Resolver.hs | 6 +++--- TypeChecker.hs | 10 +++++----- examples/torsor.ctt | 10 +++++----- 6 files changed, 39 insertions(+), 39 deletions(-) diff --git a/CTT.hs b/CTT.hs index c21d2e6..f0b9a6a 100644 --- a/CTT.hs +++ b/CTT.hs @@ -39,8 +39,8 @@ data Branch = OBranch LIdent [Ident] Ter type Decl = (Ident,(Ter,Ter)) data Decls = MutualDecls [Decl] | OpaqueDecl Ident - | VisibleDecl Ident - | VisibleAllDecl + | TransparentDecl Ident + | TransparentAllDecl deriving Eq declIdents :: [Decl] -> [Ident] @@ -237,14 +237,14 @@ emptyEnv = (Empty,[],[],Nameless Set.empty) def :: Decls -> Env -> Env def (MutualDecls ds) (rho,vs,fs,Nameless os) = (Def ds rho,vs,fs,Nameless (os Set.\\ Set.fromList (declIdents ds))) def (OpaqueDecl n) (rho,vs,fs,Nameless os) = (rho,vs,fs,Nameless (Set.insert n os)) -def (VisibleDecl n) (rho,vs,fs,Nameless os) = (rho,vs,fs,Nameless (Set.delete n os)) -def VisibleAllDecl (rho,vs,fs,Nameless os) = (rho,vs,fs,Nameless Set.empty) +def (TransparentDecl n) (rho,vs,fs,Nameless os) = (rho,vs,fs,Nameless (Set.delete n os)) +def TransparentAllDecl (rho,vs,fs,Nameless os) = (rho,vs,fs,Nameless Set.empty) defWhere :: Decls -> Env -> Env defWhere (MutualDecls ds) (rho,vs,fs,Nameless os) = (Def ds rho,vs,fs,Nameless (os Set.\\ Set.fromList (declIdents ds))) defWhere (OpaqueDecl _) rho = rho -defWhere (VisibleDecl _) rho = rho -defWhere VisibleAllDecl rho = rho +defWhere (TransparentDecl _) rho = rho +defWhere TransparentAllDecl rho = rho sub :: (Name,Formula) -> Env -> Env sub (i,phi) (rho,vs,fs,os) = (Sub i rho,vs,phi:fs,os) @@ -358,9 +358,9 @@ showTer v = case v of AppFormula e phi -> showTer1 e <+> char '@' <+> showFormula phi Comp e t ts -> text "comp" <+> showTers [e,t] <+> text (showSystem ts) 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) - UnGlueElem a ts -> text "unglueElem" <+> showTer1 a <+> text (showSystem ts) + Glue a ts -> text "Glue" <+> showTer1 a <+> text (showSystem ts) + GlueElem a ts -> text "glue" <+> showTer1 a <+> text (showSystem ts) + UnGlueElem a ts -> text "unglue" <+> showTer1 a <+> text (showSystem ts) showTers :: [Ter] -> Doc showTers = hsep . map showTer1 @@ -384,8 +384,8 @@ showDecls (MutualDecls defs) = hsep $ punctuate comma [ text x <+> equals <+> showTer d | (x,(_,d)) <- defs ] showDecls (OpaqueDecl i) = text "opaque" <+> text i -showDecls (VisibleDecl i) = text "visible" <+> text i -showDecls VisibleAllDecl = text "visible_all" +showDecls (TransparentDecl i) = text "transparent" <+> text i +showDecls TransparentAllDecl = text "transparent_all" instance Show Val where show = render . showVal @@ -419,10 +419,10 @@ showVal v = case v of VAppFormula v phi -> showVal v <+> char '@' <+> showFormula phi 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) - VUnGlueElem a ts -> text "unglueElem" <+> showVal1 a <+> text (showSystem ts) - VUnGlueElemU v b es -> text "unGlueElemU" <+> showVals [v,b] + VGlue a ts -> text "Glue" <+> showVal1 a <+> text (showSystem ts) + VGlueElem a ts -> text "glue" <+> showVal1 a <+> text (showSystem ts) + VUnGlueElem a ts -> text "unglue" <+> showVal1 a <+> text (showSystem ts) + VUnGlueElemU v b es -> text "unglue U" <+> showVals [v,b] <+> text (showSystem es) VCompU a ts -> text "comp (<_> U)" <+> showVal1 a <+> text (showSystem ts) diff --git a/Eval.hs b/Eval.hs index cb3bd24..3626107 100644 --- a/Eval.hs +++ b/Eval.hs @@ -502,7 +502,7 @@ unGlue :: Val -> Val -> System Val -> Val unGlue w b equivs | eps `member` equivs = app (equivFun (equivs ! eps)) w | otherwise = case w of VGlueElem v us -> v - _ -> error ("unGlue: neutral" ++ show w) + _ -> error ("unglue: neutral" ++ show w) isNeutralGlue :: Name -> System Val -> Val -> System Val -> Bool isNeutralGlue i equivs u0 ts = (eps `notMember` equivsi0 && isNeutral u0) || diff --git a/Exp.cf b/Exp.cf index bd013b9..d5afd2f 100644 --- a/Exp.cf +++ b/Exp.cf @@ -12,16 +12,16 @@ Module. Module ::= "module" AIdent "where" "{" [Imp] [Decl] "}" ; Import. Imp ::= "import" AIdent ; separator Imp ";" ; -DeclDef. Decl ::= AIdent [Tele] ":" Exp "=" ExpWhere ; -DeclData. Decl ::= "data" AIdent [Tele] "=" [Label] ; -DeclHData. Decl ::= "hdata" AIdent [Tele] "=" [Label] ; -DeclSplit. Decl ::= AIdent [Tele] ":" Exp "=" "split" "{" [Branch] "}" ; -DeclUndef. Decl ::= AIdent [Tele] ":" Exp "=" "undefined" ; -DeclMutual. Decl ::= "mutual" "{" [Decl] "}" ; -DeclOpaque. Decl ::= "opaque" AIdent ; -DeclVisible. Decl ::= "visible" AIdent ; -DeclVisibleAll. Decl ::= "visible_all" ; -separator Decl ";" ; +DeclDef. Decl ::= AIdent [Tele] ":" Exp "=" ExpWhere ; +DeclData. Decl ::= "data" AIdent [Tele] "=" [Label] ; +DeclHData. Decl ::= "hdata" AIdent [Tele] "=" [Label] ; +DeclSplit. Decl ::= AIdent [Tele] ":" Exp "=" "split" "{" [Branch] "}" ; +DeclUndef. Decl ::= AIdent [Tele] ":" Exp "=" "undefined" ; +DeclMutual. Decl ::= "mutual" "{" [Decl] "}" ; +DeclOpaque. Decl ::= "opaque" AIdent ; +DeclTransparent. Decl ::= "transparent" AIdent ; +DeclTransparentAll. Decl ::= "transparent_all" ; +separator Decl ";" ; Where. ExpWhere ::= Exp "where" "{" [Decl] "}" ; NoWhere. ExpWhere ::= Exp ; diff --git a/Resolver.hs b/Resolver.hs index 4f6c4ff..aba0d77 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -349,10 +349,10 @@ resolveDecl d = case d of DeclOpaque i -> do resolveVar i return (CTT.OpaqueDecl (unAIdent i), []) - DeclVisible i -> do + DeclTransparent i -> do resolveVar i - return (CTT.VisibleDecl (unAIdent i), []) - DeclVisibleAll -> return (CTT.VisibleAllDecl, []) + return (CTT.TransparentDecl (unAIdent i), []) + DeclTransparentAll -> return (CTT.TransparentAllDecl, []) _ -> do let (f,typ,body,ns) = resolveNonMutualDecl d a <- typ d <- body diff --git a/TypeChecker.hs b/TypeChecker.hs index 370649b..35d8bda 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -223,7 +223,7 @@ check a t = case (a,t) of -- Check a list of declarations checkDecls :: Decls -> Typing () checkDecls (MutualDecls []) = return () -checkDecls (MutualDecls d) = do +checkDecls (MutualDecls d) = do a <- asks env let (idents,tele,ters) = (declIdents d,declTele d,declTers d) ind <- asks indent @@ -232,9 +232,9 @@ checkDecls (MutualDecls d) = do local (addDecls (MutualDecls d)) $ do rho <- asks env checks (tele,rho) ters -checkDecls (OpaqueDecl _) = return () -checkDecls (VisibleDecl _) = return () -checkDecls VisibleAllDecl = return () +checkDecls (OpaqueDecl _) = return () +checkDecls (TransparentDecl _) = return () +checkDecls TransparentAllDecl = return () -- Check a telescope checkTele :: Tele -> Typing () @@ -278,7 +278,7 @@ checkGlueElem vu ts us = do let vus = evalSystem rho us checkSystemsWith ts vus (\alpha vt vAlpha -> unlessM (app (equivFun vt) vAlpha === (vu `face` alpha)) $ - throwError $ "Image of glueElem component " ++ show vAlpha ++ + throwError $ "Image of glue component " ++ show vAlpha ++ " doesn't match " ++ show vu) checkCompSystem vus diff --git a/examples/torsor.ctt b/examples/torsor.ctt index 0193c6a..85b5b0a 100644 --- a/examples/torsor.ctt +++ b/examples/torsor.ctt @@ -734,7 +734,7 @@ multZ (A B : BZ) : BZ = (T, (TNE, (TShift A B, TEquiv))) (compBZ (decodeZ ZBZ (inr n)) loopZ) (decodeZ ZBZ (inr (suc n))) ( compBZ (hole0 n @ i) loopZ) (decodeLoop (inr n)) - visible decodeZ + transparent decodeZ TEquiv''' : isEquiv Z (Path BZ ZBZ ZBZ) (action (Path BZ ZBZ ZBZ) (TShift ZBZ ZBZ) (<_> ZBZ)) = transport ( isEquiv Z loopBZ (\(y : Z) -> hole y @ -i)) (gradLemma Z loopBZ (decodeZ ZBZ) (encodeZ ZBZ) (decodeEncodeZ ZBZ) (encodeDecodeZ ZBZ)) TEquiv'' (b : BZSet B) (x : Path BZ ZBZ B) : isEquiv Z (Path BZ ZBZ B) (action (Path BZ ZBZ B) (TShift ZBZ B) x) @@ -747,7 +747,7 @@ multZ (A B : BZ) : BZ = (T, (TNE, (TShift A B, TEquiv))) = BZNE A (isEquiv Z T (action T (TShift A B) x), propIsEquiv Z T (action T (TShift A B) x)) (\(a : BZSet A) -> BZNE B (isEquiv Z T (action T (TShift A B) x), propIsEquiv Z T (action T (TShift A B) x)) (\(b : BZSet B) -> TEquiv' a b x)) -visible decodeZ +transparent decodeZ loopBZequalsZ : Path U loopBZ Z = isoPath loopBZ Z (encodeZ ZBZ) (decodeZ ZBZ) (encodeDecodeZ ZBZ) (decodeEncodeZ ZBZ) @@ -850,12 +850,12 @@ doubleLoopBZ : loopBZ -> loopBZ = transport ( loopS1equalsLoopBZ@i -> loopS1e -- EVAL: inr (suc (suc zero)) -- Time: 0m25.191s --- > let visible_all in let doubleLoop : Path BZ (multZ ZBZ ZBZ) (multZ ZBZ ZBZ) = multZ (loopZ@-i) (loopZ@i) in transport ( BZSet (transport ( BZSet (doubleLoop @ i)) (<_> ZBZ) @ j)) zeroZ +-- > let transparent_all in let doubleLoop : Path BZ (multZ ZBZ ZBZ) (multZ ZBZ ZBZ) = multZ (loopZ@-i) (loopZ@i) in transport ( BZSet (transport ( BZSet (doubleLoop @ i)) (<_> ZBZ) @ j)) zeroZ -- too slow --- > let visible_all in transport ( BZSet (transport ( BZSet (multZ (loopZ@-i) (loopZ@i))) (<_> ZBZ) @ j)) zeroZ +-- > let transparent_all in transport ( BZSet (transport ( BZSet (multZ (loopZ@-i) (loopZ@i))) (<_> ZBZ) @ j)) zeroZ -- EVAL: inr (suc (suc zero)) -- multS1 : S1 -> S1 -> S1 = transport ( S1equalsBZ@-i -> S1equalsBZ@-i -> S1equalsBZ@-i) multZ -visible_all +transparent_all -- 2.34.1