Skip to content

Commit

Permalink
rename visible to transparent and fix printing of glue
Browse files Browse the repository at this point in the history
  • Loading branch information
@mortberg
mortberg committed Jul 7, 2016
1 parent 26a03d7 commit 371e1dc
Show file tree
Hide file tree
Showing 6 changed files with 39 additions and 39 deletions.
30 changes: 15 additions & 15 deletions CTT.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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)

Expand Down
2 changes: 1 addition & 1 deletion Eval.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) ||
Expand Down
20 changes: 10 additions & 10 deletions Exp.cf
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 ;
Expand Down
6 changes: 3 additions & 3 deletions Resolver.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
10 changes: 5 additions & 5 deletions TypeChecker.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 ()
Expand Down Expand Up @@ -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

Expand Down
10 changes: 5 additions & 5 deletions examples/torsor.ctt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)))
(<i> 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 (<i> 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)
Expand All @@ -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)

Expand Down Expand Up @@ -850,12 +850,12 @@ doubleLoopBZ : loopBZ -> loopBZ = transport (<i> 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) = <i> multZ (loopZ@-i) (loopZ@i) in transport (<j> BZSet (transport (<i> BZSet (doubleLoop @ i)) (<_> ZBZ) @ j)) zeroZ
-- > 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
-- too slow

-- > let visible_all in transport (<j> BZSet (transport (<i> BZSet (multZ (loopZ@-i) (loopZ@i))) (<_> ZBZ) @ j)) zeroZ
-- > let transparent_all in transport (<j> BZSet (transport (<i> BZSet (multZ (loopZ@-i) (loopZ@i))) (<_> ZBZ) @ j)) zeroZ
-- EVAL: inr (suc (suc zero))

-- multS1 : S1 -> S1 -> S1 = transport (<i> S1equalsBZ@-i -> S1equalsBZ@-i -> S1equalsBZ@-i) multZ

visible_all
transparent_all

0 comments on commit 371e1dc

Please sign in to comment.