Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Added a primitive composition for Id types which reduces with refl on… #71

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Added a primitive composition for Id types which reduces with refl on… #71

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
dc5e64f
Added a primitive composition for Id types which reduces with refl on…
IanOrton Jun 14, 2017
e92bbb2
Fixing bugs/nits from feedback
IanOrton Jun 14, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions CTT.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -123,6 +123,7 @@ data Ter = Pi Ter
| Id Ter Ter Ter
| IdPair Ter (System Ter)
| IdJ Ter Ter Ter Ter Ter Ter
| IdComp Ter Ter Ter Ter Ter Ter
deriving Eq

-- For an expression t, returns (u,ts) where u is no application and t = u ts
Expand Down Expand Up @@ -182,6 +183,7 @@ data Val = VU
| VLam Ident Val Val
| VUnGlueElemU Val Val (System Val)
| VIdJ Val Val Val Val Val Val
| VIdComp Val Val Val Val Val Val
deriving Eq

isNeutral :: Val -> Bool
Expand All @@ -199,6 +201,7 @@ isNeutral v = case v of
VUnGlueElemU{} -> True
VUnGlueElem{} -> True
VIdJ{} -> True
VIdComp{} -> True
_ -> False

isNeutralSystem :: System Val -> Bool
Expand Down Expand Up @@ -387,6 +390,7 @@ showTer v = case v of
Id a u v -> text "Id" <+> showTers [a,u,v]
IdPair b ts -> text "idC" <+> showTer1 b <+> text (showSystem ts)
IdJ a t c d x p -> text "idJ" <+> showTers [a,t,c,d,x,p]
IdComp a u v w p q -> text "idComp" <+> showTers [a,u,v,w,p,q]

showTers :: [Ter] -> Doc
showTers = hsep . map showTer1
Expand Down Expand Up @@ -454,6 +458,7 @@ showVal v = case v of
VId a u v -> text "Id" <+> showVals [a,u,v]
VIdPair b ts -> text "idC" <+> showVal1 b <+> text (showSystem ts)
VIdJ a t c d x p -> text "idJ" <+> showVals [a,t,c,d,x,p]
VIdComp a u v w p q -> text "idComp" <+> showVals [a,u,v,w,p,q]

showPLam :: Val -> Doc
showPLam e = case e of
Expand Down
26 changes: 26 additions & 0 deletions Eval.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,6 +85,7 @@ instance Nominal Val where
VIdPair u us -> support (u,us)
VId a u v -> support (a,u,v)
VIdJ a u c d x p -> support [a,u,c,d,x,p]
VIdComp a u v w p q -> support [a,u,v,w,p,q]

act u (i, phi) | i `notElem` support u = u
| otherwise =
Expand Down Expand Up @@ -123,6 +124,8 @@ instance Nominal Val where
VId a u v -> VId (acti a) (acti u) (acti v)
VIdJ a u c d x p ->
idJ (acti a) (acti u) (acti c) (acti d) (acti x) (acti p)
VIdComp a u v w p q ->
idComp (acti a) (acti u) (acti v) (acti w) (acti p) (acti q)

-- This increases efficiency as it won't trigger computation.
swap u ij@(i,j) =
Expand Down Expand Up @@ -157,6 +160,8 @@ instance Nominal Val where
VId a u v -> VId (sw a) (sw u) (sw v)
VIdJ a u c d x p ->
VIdJ (sw a) (sw u) (sw c) (sw d) (sw x) (sw p)
VIdComp a u v w p q ->
VIdComp (sw a) (sw u) (sw v) (sw w) (sw p) (sw q)

-----------------------------------------------------------------------
-- The evaluator
Expand Down Expand Up @@ -198,6 +203,8 @@ eval rho@(Env (_,_,_,Nameless os)) v = case v of
IdPair b ts -> VIdPair (eval rho b) (evalSystem rho ts)
IdJ a t c d x p -> idJ (eval rho a) (eval rho t) (eval rho c)
(eval rho d) (eval rho x) (eval rho p)
IdComp a u v w p q -> idComp (eval rho a) (eval rho u) (eval rho v)
(eval rho w) (eval rho p) (eval rho q)
_ -> error $ "Cannot evaluate " ++ show v

evals :: Env -> [(Ident,Ter)] -> [(Ident,Val)]
Expand Down Expand Up @@ -286,6 +293,7 @@ inferType v = case v of
-- VUnGlueElem _ b _ -> b -- This is wrong! Store the type??
VUnGlueElemU _ b _ -> b
VIdJ _ _ c _ x p -> app (app c x) p
VIdComp a u _ w _ _ -> VId a u w
_ -> error $ "inferType: not neutral " ++ show v

(@@) :: ToFormula a => Val -> a -> Val
Expand Down Expand Up @@ -444,6 +452,22 @@ isIdPair :: Val -> Bool
isIdPair VIdPair{} = True
isIdPair _ = False

idComp :: Val -> Val -> Val -> Val -> Val -> Val -> Val
idComp a u v w pId qId = case (pId, qId) of
(VIdPair p ps, VIdPair q qs) ->
let i:j:_ = freshs [a,u,v,w,pId,qId] in
let
rs = unionSystem
(unionSystem
(border (q @@ (Atom i :/\: Atom j)) ps)
(border (p @@ (Atom i :\/: NegAtom j)) qs))
(mkSystem [((i ~> 0), p @@ NegAtom j), ((i ~> 1), q @@ Atom j)])
in
VIdPair (VPLam i (comp j a v rs)) (joinSystem (border ps qs))
(VIdPair p ps, qId) | eps `member` ps -> qId
(pId, VIdPair q qs) | eps `member` qs -> pId
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm still a bit unsure about these two reduction rules. It seems dangerous to add them, but I don't have any concrete evidence why.

@simhu : Maybe you have more thoughts about this?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As some justification, imagine that face formulae were first class objects and we could see that Id types were pairs of a path and a face formula. Then, using eta for pairs and paths, we would have:

idComp (<i> a , 1) qId
   = idComp (<i> a , 1) (qId.1 , qId.2)
   = (<i> comp j A [ 1 -> qId.1 @ (i /\ j) , qId.2 \/ (i=0) -> a ] a , 1 /\ qId.2)
   = (<i> qId.1 @ i , qId.2)
   = (qId.1 , qId.2)
   = qId

_ -> VIdComp a u v w pId qId


-------------------------------------------------------------------------------
-- | HITs
Expand Down Expand Up @@ -897,6 +921,8 @@ instance Convertible Val where
(VId a u v,VId a' u' v') -> conv ns (a,u,v) (a',u',v')
(VIdJ a u c d x p,VIdJ a' u' c' d' x' p') ->
conv ns [a,u,c,d,x,p] [a',u',c',d',x',p']
(VIdComp a u b w p q,VIdComp a' u' b' w' p' q') ->
conv ns [a,u,b,w,p,q] [a',u',b',w',p',q']
_ -> False

instance Convertible Ctxt where
Expand Down
1 change: 1 addition & 0 deletions Exp.cf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,7 @@ UnGlueElem. Exp3 ::= "unglue" Exp4 System ;
Id. Exp3 ::= "Id" Exp4 Exp4 Exp3 ;
IdPair. Exp3 ::= "idC" Exp4 System ;
IdJ. Exp3 ::= "idJ" Exp4 Exp4 Exp4 Exp4 Exp4 Exp4 ;
IdComp. Exp3 ::= "idComp" Exp4 Exp4 Exp4 Exp4 Exp4 Exp4 ;
Fst. Exp4 ::= Exp4 ".1" ;
Snd. Exp4 ::= Exp4 ".2" ;
Pair. Exp5 ::= "(" Exp "," [Exp] ")" ;
Expand Down
2 changes: 2 additions & 0 deletions Resolver.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -223,6 +223,8 @@ resolveExp e = case e of
IdPair u ts -> CTT.IdPair <$> resolveExp u <*> resolveSystem ts
IdJ a t c d x p -> CTT.IdJ <$> resolveExp a <*> resolveExp t <*> resolveExp c
<*> resolveExp d <*> resolveExp x <*> resolveExp p
IdComp a u v w p q -> CTT.IdComp <$> resolveExp a <*> resolveExp u <*> resolveExp v
<*> resolveExp w <*> resolveExp p <*> resolveExp q
_ -> do
modName <- asks envModule
throwError ("Could not resolve " ++ show e ++ " in module " ++ modName)
Expand Down
14 changes: 14 additions & 0 deletions TypeChecker.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -516,6 +516,20 @@ infer e = case e of
check (VId va vu vx) p
vp <- evalTyping p
return (app (app vc vx) vp)
IdComp a u v w p q -> do
check VU a
va <- evalTyping a
check va u
vu <- evalTyping u
check va v
vv <- evalTyping v
check va w
vw <- evalTyping w
let vIduv = VId va vu vv
let vIdvw = VId va vv vw
check vIduv p
check vIdvw q
return (VId va vu vw)
_ -> throwError ("infer " ++ show e)

-- Not used since we have U : U
Expand Down
Loading