Skip to content

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

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

Open
IanOrton 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 1 commit
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, qId) | eps `member` ps -> qId
(pId, VIdPair q qs) | eps `member` qs -> pId
Copy link
Owner

@mortberg mortberg Jun 14, 2017

Choose a reason for hiding this comment

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

Are these two cases really needed? Isn't it possible to get the next case to cover them?

Copy link
Contributor

@favonia favonia Jun 14, 2017

Choose a reason for hiding this comment

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

I would guess @IanOrton just wanted to take some shortcuts here?

Copy link
Owner

@mortberg mortberg Jun 14, 2017

Choose a reason for hiding this comment

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

They seem a little dangerous to me, and if I comment them out the examples doesn't go through (even if one fixes the bug I found).

Copy link
Author

@IanOrton IanOrton Jun 14, 2017

Choose a reason for hiding this comment

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

Hmmm, I'm not sure. I think that they are needed to make sure that refl . p will reduce even when p is just a variable. To hit the other case you need to know that p is in fact a VIdPair. The behaviour should agree when the cases overlap so I've now moved these two cases after the third one. But maybe this behaviour is too strong? Do we want refl . p to reduce in the case when p is an undetermined variables of type Id A a b?

(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))
Copy link
Owner

@mortberg mortberg Jun 14, 2017 •
edited
Loading

Choose a reason for hiding this comment

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

Shouldn't this be i \/ -j?

Copy link
Author

@IanOrton IanOrton Jun 14, 2017

Choose a reason for hiding this comment

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

Yep, now fixed

(mkSystem [((i ~> 0), p @@ NegAtom j), ((i ~> 1), q @@ Atom j)])
in
VIdPair (VPLam i (comp j a v rs)) (joinSystem (border ps qs))
_ -> 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