rename visible to transparent and fix printing of glue

diff --git a/CTT.hs b/CTT.hs
index c21d2e60fcde5d4e02ec1481aef954d56c1d209a..f0b9a6ac672bfeed6bfb622921b1e56b585e14ab 100644 (file)
--- 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 cb3bd246fb320605eab826d2d1abd9f88d48d3ec..3626107185a5d8430c63e3760bca91be1f8f342b 100644 (file)
--- 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 bd013b9b27e7e86a19b17c0c7a02296e5296f8f8..d5afd2fa7d99d87f4ebb63f3e71e509dfa976c85 100644 (file)
--- 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 4f6c4ff7106e9dfe988b33d89e43ab16ec9787f4..aba0d774f8eab8f6c3cdba21f747939b541fa1d2 100644 (file)
--- 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 370649b32ca8c419563810742e69384550b53008..35d8bda31147cbfaa2988c3b592f4514deef20d0 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -223,7 +223,7 @@ check a t = case (a,t) of
 -- Check a list of declarations\r
 checkDecls :: Decls -> Typing ()\r
 checkDecls (MutualDecls []) = return ()\r
-checkDecls (MutualDecls d) = do\r
+checkDecls (MutualDecls d)  = do\r
   a <- asks env\r
   let (idents,tele,ters) = (declIdents d,declTele d,declTers d)\r
   ind <- asks indent\r
@@ -232,9 +232,9 @@ checkDecls (MutualDecls d) = do
   local (addDecls (MutualDecls d)) $ do\r
     rho <- asks env\r
     checks (tele,rho) ters\r
-checkDecls (OpaqueDecl _) = return ()\r
-checkDecls (VisibleDecl _) = return ()\r
-checkDecls VisibleAllDecl = return ()\r
+checkDecls (OpaqueDecl _)      = return ()\r
+checkDecls (TransparentDecl _) = return ()\r
+checkDecls TransparentAllDecl  = return ()\r
 \r
 -- Check a telescope\r
 checkTele :: Tele -> Typing ()\r
@@ -278,7 +278,7 @@ checkGlueElem vu ts us = do
   let vus = evalSystem rho us\r
   checkSystemsWith ts vus (\alpha vt vAlpha ->\r
     unlessM (app (equivFun vt) vAlpha === (vu `face` alpha)) $\r
-      throwError $ "Image of glueElem component " ++ show vAlpha ++\r
+      throwError $ "Image of glue component " ++ show vAlpha ++\r
                    " doesn't match " ++ show vu)\r
   checkCompSystem vus\r
 \r

diff --git a/examples/torsor.ctt b/examples/torsor.ctt
index 0193c6a24a113eb23c190b5d9ed682824bb2e20c..85b5b0a6527db775849f9fa7c1b0c78833e437cb 100644 (file)
--- 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)))\r
                           (<i> compBZ (hole0 n @ i) loopZ)\r
                           (decodeLoop (inr n))\r
-    visible decodeZ\r
+    transparent decodeZ\r
     TEquiv''' : isEquiv Z (Path BZ ZBZ ZBZ) (action (Path BZ ZBZ ZBZ) (TShift ZBZ ZBZ) (<_> ZBZ))\r
       = transport (<i> isEquiv Z loopBZ (\(y : Z) -> hole y @ -i)) (gradLemma Z loopBZ (decodeZ ZBZ) (encodeZ ZBZ) (decodeEncodeZ ZBZ) (encodeDecodeZ ZBZ))\r
     TEquiv'' (b : BZSet B) (x : Path BZ ZBZ B) : isEquiv Z (Path BZ ZBZ B) (action (Path BZ ZBZ B) (TShift ZBZ B) x)\r
@@ -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))\r
          (\(a : BZSet A) -> BZNE B (isEquiv Z T (action T (TShift A B) x), propIsEquiv Z T (action T (TShift A B) x))\r
          (\(b : BZSet B) -> TEquiv' a b x))\r
-visible decodeZ\r
+transparent decodeZ\r
 \r
 loopBZequalsZ : Path U loopBZ Z = isoPath loopBZ Z (encodeZ ZBZ) (decodeZ ZBZ) (encodeDecodeZ ZBZ) (decodeEncodeZ ZBZ)\r
 \r
@@ -850,12 +850,12 @@ doubleLoopBZ : loopBZ -> loopBZ = transport (<i> loopS1equalsLoopBZ@i -> loopS1e
 -- EVAL: inr (suc (suc zero))\r
 -- Time: 0m25.191s\r
 \r
--- > let visible_all in let doubleLoop : Path BZ (multZ ZBZ ZBZ) (multZ ZBZ ZBZ) = <i> multZ (loopZ@-i) (loopZ@i) in transport (<j> BZSet (transport (<i> BZSet (doubleLoop @ i)) (<_> ZBZ) @ j)) zeroZ\r
+-- > let transparent_all in let doubleLoop : Path BZ (multZ ZBZ ZBZ) (multZ ZBZ ZBZ) = <i> multZ (loopZ@-i) (loopZ@i) in transport (<j> BZSet (transport (<i> BZSet (doubleLoop @ i)) (<_> ZBZ) @ j)) zeroZ\r
 -- too slow\r
 \r
--- > let visible_all in transport (<j> BZSet (transport (<i> BZSet (multZ (loopZ@-i) (loopZ@i))) (<_> ZBZ) @ j)) zeroZ\r
+-- > let transparent_all in transport (<j> BZSet (transport (<i> BZSet (multZ (loopZ@-i) (loopZ@i))) (<_> ZBZ) @ j)) zeroZ\r
 -- EVAL: inr (suc (suc zero))\r
 \r
 -- multS1 : S1 -> S1 -> S1 = transport (<i> S1equalsBZ@-i -> S1equalsBZ@-i -> S1equalsBZ@-i) multZ\r
 \r
-visible_all\r
+transparent_all\r