From: Anders <mortberg@chalmers.se>
Date: Mon, 23 Mar 2015 17:13:12 +0000 (+0100)
Subject: Finish adding glue
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=02cb774a6b3303f45818cb1bb972ee5846171864;p=cubicaltt.git

Finish adding glue
---

diff --git a/Eval.hs b/Eval.hs
index ca49cc4..2d99b8b 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
 module Eval where
 
 import Data.List
@@ -241,7 +242,7 @@ trans i v0 v1 = case (v0,v1) of
   (VPi{},_) -> VTrans (VPath i v0) v1
   (Ter (Sum _ _ nass) env,VCon n us) -> case lookup n nass of
     Just as -> VCon n $ transps i as env us
-    Nothing -> error $ "comp: missing constructor in labelled sum " ++ n
+    Nothing -> error $ "comp: missing constructor in labelled sum " ++ n ++ " v0 = " ++ show v0
   _ | isNeutral v0 || isNeutral v1 -> VTrans (VPath i v0) v1
   (VGlue a ts,_) -> transGlue i a ts v1
   _ | otherwise -> error "trans not implemented"
@@ -519,14 +520,22 @@ instance Convertible Val where
     (u,VTrans p v) | isIndep k j (p @@ j) -> conv k u v
     (VTrans p u,VTrans p' u') -> conv k p p' && conv k u u'
     (VAppFormula u x,VAppFormula u' x') -> conv k (u,x) (u',x')
-    -- VComp
+    (VComp a u ts,v)  | isIndep k j (Map.map (@@ j) ts) -> conv k u v
+    (VComp a u ts,v') | not (Map.null indep) -> conv k (VComp a u ts') v'
+      where (ts',indep) = Map.partition (\t -> isIndep k j (t @@ j)) ts
+    (v,VComp a u ts)  | isIndep k j (Map.map (@@ j) ts) -> conv k u v
+    (v',VComp a u ts) | not (Map.null indep) -> conv k (VComp a u ts') v'
+      where (ts',indep) = Map.partition (\t -> isIndep k j (t @@ j)) ts
+    (VComp a u ts,VComp a' u' ts') -> conv k (a,u,ts) (a',u',ts')
+    (VGlue v hisos,VGlue v' hisos') -> conv k (v,hisos) (v',hisos')
+    (VGlueElem u us,VGlueElem u' us') -> conv k (u,us) (u',us')
     _                         -> False
 
 instance Convertible Env where
-  conv k e e' =
-    conv k (valAndFormulaOfEnv e) (valAndFormulaOfEnv e')
+  conv k e e' = conv k (valAndFormulaOfEnv e) (valAndFormulaOfEnv e')
 
-instance Convertible () where conv _ _ _ = True
+instance Convertible () where
+  conv _ _ _ = True
 
 instance (Convertible a, Convertible b) => Convertible (a, b) where
   conv k (u, v) (u', v') = conv k u u' && conv k v v'
@@ -543,5 +552,9 @@ instance Convertible a => Convertible [a] where
   conv k us us' = length us == length us' &&
                   and [conv k u u' | (u,u') <- zip us us']
 
+instance Convertible a => Convertible (System a) where
+  conv k ts ts' = Map.keys ts == Map.keys ts' &&
+                  and (Map.elems (Map.intersectionWith (conv k) ts ts'))
+
 instance Convertible Formula where
   conv _ phi psi = sort (invFormula phi 1) == sort (invFormula psi 1)
diff --git a/Exp.cf b/Exp.cf
index e45460b..074fc15 100644
--- a/Exp.cf
+++ b/Exp.cf
@@ -36,6 +36,8 @@ Snd.        Exp3 ::= Exp3 ".2" ;
 IdP.        Exp3 ::= "IdP" ;
 Trans.      Exp3 ::= "transport" ;
 Comp.       Exp3 ::= "comp" ;
+Glue.       Exp3 ::= "glue" ;
+GlueElem.   Exp3 ::= "glueElem" ;
 System.     Exp3 ::= "[" [Side] "]" ;
 Pair.       Exp3 ::= "(" Exp "," Exp ")" ;
 coercions Exp 3 ;
diff --git a/Resolver.hs b/Resolver.hs
index 42d13e4..a656f1d 100644
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -12,7 +12,7 @@ import Control.Monad.Trans
 import Control.Monad.Trans.Reader
 import Control.Monad.Trans.Error hiding (throwError)
 import Control.Monad.Error (throwError)
-import Control.Monad (when)
+import Control.Monad
 import Data.Functor.Identity
 import Data.List (nub)
 import Data.Map (Map,(!))
@@ -173,6 +173,17 @@ resolveApps IdP (x:y:z:xs) = do
 resolveApps Comp (u:v:ts:xs) = do
   let c = CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
   CTT.mkApps <$> c <*> mapM resolveExp xs
+resolveApps Glue (u:ts:xs) = do
+  rs <- resolveSystem ts
+  let isIso (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ _)))) = True
+      isIso _ = False
+  unless (all isIso $ Map.elems rs)
+    (throwError $ "Not a system of isomorphisms: " ++ show rs)
+  let c = CTT.Glue <$> resolveExp u <*> pure rs
+  CTT.mkApps <$> c <*> mapM resolveExp xs
+resolveApps GlueElem (u:ts:xs) = do
+  let c = CTT.GlueElem <$> resolveExp u <*> resolveSystem ts
+  CTT.mkApps <$> c <*> mapM resolveExp xs
 resolveApps x xs = CTT.mkApps <$> resolveExp x <*> mapM resolveExp xs
 
 resolveExp :: Exp -> Resolver Ter
@@ -193,7 +204,7 @@ resolveExp e = case e of
     lams tele (resolveExp t)
   Fst t         -> CTT.Fst <$> resolveExp t
   Snd t         -> CTT.Snd <$> resolveExp t
-  Pair t0 t1    -> CTT.SPair <$> resolveExp t0 <*> resolveExp t1
+  Pair t0 t1    -> CTT.Pair <$> resolveExp t0 <*> resolveExp t1
   Let decls e   -> do
     (rdecls,names) <- resolveDecls decls
     CTT.mkWheres rdecls <$> local (insertIdents names) (resolveExp e)
diff --git a/TypeChecker.hs b/TypeChecker.hs
index 9f9a601..783d3a5 100644
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -174,13 +174,80 @@ check a t = case (a,t) of
     let u0 = eval (Sub rho (i,Dir 0)) e
         u1 = eval (Sub rho (i,Dir 1)) e
     unless (conv k a0 u0 && conv k a1 u1) $
-      throwError $ "path endpoints don't match " ++ show e ++ " \nu0 = " ++ show u0 ++ " \nu1 = " ++ show u1 ++ " \na0 = " ++ show a0 ++ " \na1 = " ++ show a1 ++ " \np = " ++ show p
+      throwError $ "path endpoints don't match " ++ show e ++
+                   " \nu0 = " ++ show u0 ++ " \nu1 = " ++ show u1 ++
+                   " \na0 = " ++ show a0 ++ " \na1 = " ++ show a1 ++
+                   " \np = " ++ show p
+  (VU,Glue a ts) -> do
+    check VU a
+    rho <- asks env
+    checkGlue (eval rho a) ts
+  (VGlue va ts,GlueElem u us) -> do
+    check va u
+    rho <- asks env
+    let vu = eval rho u
+    checkGlueElem vu ts us
   _ -> do
     v <- infer t
     k <- index <$> ask
     unless (conv k v a) $
       throwError $ "check conv: " ++ show v ++ " /= " ++ show a
 
+checkGlueElem :: Val -> System Val -> System Ter -> Typing ()
+checkGlueElem vu ts us = do
+  unless (Map.keys ts == Map.keys us)
+    (throwError ("Keys don't match in " ++ show ts ++ " and " ++ show us))
+  rho <- asks env
+  k <- asks index
+  sequence_ $ Map.elems $ Map.intersectionWithKey
+    (\alpha vt u -> check (hisoDom vt) u) ts us
+    
+  let vus = evalSystem rho us
+  sequence_ $ Map.elems $ Map.intersectionWithKey
+    (\alpha vt vAlpha -> do
+       unless (conv k (app (hisoFun vt) vAlpha) (vu `face` alpha))
+          (throwError $ "Image of glueElem component " ++ show vAlpha ++
+                        " doesn't match " ++ show vu)) ts vus
+  unless (isCompSystem k vus)
+    (throwError $ "Incompatible system " ++ show vus)
+
+checkGlue :: Val -> System Ter -> Typing ()
+checkGlue va ts = do
+  sequence_ $ Map.elems $
+    Map.mapWithKey (\alpha tAlpha -> checkIso (va `face` alpha) tAlpha) ts
+  k <- asks index
+  rho <- asks env
+  unless (isCompSystem k (evalSystem rho ts))
+    (throwError ("Incompatible system " ++ show ts))
+
+-- An hiso for a type a is a five-tuple: (b,f,g,r,s)   where
+--  b : U
+--  f : b -> a
+--  g : a -> b
+--  s : forall (y : a), f (g y) = y
+--  t : forall (x : b), g (f x) = x
+checkIso :: Val -> Ter -> Typing ()
+checkIso va (Pair b (Pair f (Pair g (Pair s t)))) = do
+  check VU b
+  rho <- asks env
+  let vb = eval rho b
+  check (mkFun vb va) f
+  check (mkFun va vb) g
+  let vf = eval rho f
+      vg = eval rho g
+  check (mkSection va vb vf vg) s
+  check (mkSection vb va vg vf) t
+
+mkFun :: Val -> Val -> Val
+mkFun va vb = VPi va (eval rho (Lam "_" (Var "a") (Var "b")))
+  where rho = Upd (Upd Empty ("a",va)) ("b",vb)
+
+mkSection :: Val -> Val -> Val -> Val -> Val
+mkSection va _ vf vg =
+  VPi va (eval rho (Lam "y" a (IdP (Path (Name "_") a) (App f (App g y)) y)))
+  where [a,y,f,g] = map Var ["a","y","f","g"]
+        rho = Upd (Upd (Upd Empty ("a",va)) ("f",vf)) ("g",vg)
+  
 checkBranch :: (Tele,Env) -> Val -> Branch -> Typing ()
 checkBranch (xas,nu) f (c,(xs,e)) = do
   k   <- asks index
diff --git a/cubical.el b/cubical.el
index a5a0ce1..3230779 100644
--- a/cubical.el
+++ b/cubical.el
@@ -5,7 +5,7 @@
 
 ;; create regex strings
 (setq cubical-keywords-regexp (regexp-opt cubical-keywords 'words))
-(setq cubical-operators-regexp (regexp-opt '(":" "->" "=" "\\" "|" "\\" "*" "_") t))
+(setq cubical-operators-regexp (regexp-opt '(":" "->" "=" "\\" "|" "\\" "*" "_" "<" ">") t))
 (setq cubical-special-regexp (regexp-opt cubical-special 'words))
 (setq cubical-def-regexp "^[[:word:]]+")
 
diff --git a/examples/bool.ctt b/examples/bool.ctt
new file mode 100644
index 0000000..71520f1
--- /dev/null
+++ b/examples/bool.ctt
@@ -0,0 +1,50 @@
+module bool where
+
+import prelude
+
+data bool = true | false
+
+neg : bool -> bool = split
+  true  -> false
+  false -> true
+
+negK : (b : bool) -> Id bool (neg (neg b)) b = split
+  true -> refl bool true
+  false -> refl bool false
+
+negEq : Id U bool bool =
+  <i> glue bool [ (i = 0) -> (bool,(neg,(neg,(negK,negK)))) ]
+
+test : bool = transport negEq true
+
+data F2 = zero | one
+
+f2ToBool : F2 -> bool = split
+  zero -> false
+  one -> true
+
+boolToF2 : bool -> F2 = split
+  false -> zero
+  true -> one
+
+f2ToBoolK : (x : F2) -> Id F2 (boolToF2 (f2ToBool x)) x = split
+  zero -> refl F2 zero
+  one -> refl F2 one
+
+boolToF2K : (b : bool) -> Id bool (f2ToBool (boolToF2 b)) b = split
+  false -> refl bool false
+  true -> refl bool true
+
+boolEqF2 : Id U bool F2 =
+ -- <i> glue F2 [ (i = 0) -> (bool,(boolToF2,(f2ToBool,(f2ToBoolK,boolToF2K))))]
+  isoId bool F2 boolToF2 f2ToBool f2ToBoolK boolToF2K
+  
+negF2 : F2 -> F2 = subst U (\(X : U) -> (X -> X)) bool F2 boolEqF2 neg
+
+test : IdP boolEqF2 true one = <i> glueElem one [ (i = 0) -> true ]
+test1 : IdP boolEqF2 true one = lemTest bool F2 boolEqF2 true
+
+F2EqBool : Id U F2 bool = inv U bool F2 boolEqF2
+
+negBool : bool -> bool = subst U (\(X : U) -> (X -> X)) F2 bool F2EqBool negF2
+
diff --git a/examples/nat.ctt b/examples/nat.ctt
index 627d842..b673a6e 100644
--- a/examples/nat.ctt
+++ b/examples/nat.ctt
@@ -32,17 +32,6 @@ reverse (A : U) : list A -> list A = split
   nil -> nil
   cons x xs -> append A (reverse A xs) (cons x nil)
 
-Id (A : U) (a0 a1 : A) : U = IdP (<i> A) a0 a1
-
-refl (A : U) (a : A) : Id A a a = <i> a
-
-mapOnPath (A B : U) (f : A -> B) (a b : A)
-          (p : Id A a b) : Id B (f a) (f b) = <i> f (p @ i)
-
-funExt (A : U) (B : A -> U) (f g : (x : A) -> B x)
-       (p : (x : A) -> Id (B x) (f x) (g x)) :
-       Id ((y : A) -> B y) f g = <i> \(a : A) -> (p a) @ i
-
 idnat : nat -> nat = split
   zero -> zero
   suc n -> suc (idnat n)
@@ -53,25 +42,6 @@ test : Id (nat -> nat) idnat (id nat) = funExt nat (\(_ : nat) -> nat) idnat (id
     zero -> refl nat zero
     suc n -> mapOnPath nat nat (\(x : nat) -> suc x) (idnat n) n (rem n)
 
-subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b =
-  transport (mapOnPath A U P a b p) e
-
-substRefl (A : U) (P : A -> U) (a : A) (e : P a) : Id (P a) (subst A P a a (refl A a) e) e =
-  refl (P a) e
-
-singl (A : U) (a : A) : U = (x : A) * Id A a x
-
-contrSingl (A : U) (a b : A) (p : Id A a b) :
-  Id (singl A a) (a,refl A a) (b,p) = <i> (p @ i,<j> p @ i /\ j)
-
-J (A : U) (a : A) (C : (x : A) -> Id A a x -> U)
-  (d : C a (refl A a)) (x : A) (p : Id A a x) : C x p =
-    subst (singl A a) T (a, refl A a) (x, p) (contrSingl A a x p) d
-      where T (z : singl A a) : U = C (z.1) (z.2)
-
-defEqJ (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refl A a)) :
-       Id (C a (refl A a)) (J A a C d a (refl A a)) d = refl (C a (refl A a)) d
-
 test0 (A : U) (a b : A) (p : Id A a b) : Id A a a = refl A (p @ 0)
 test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1)
 
@@ -85,7 +55,6 @@ kan (A : U) (a b c d : A) (p : Id A a b) (q : Id A a c)
                           (r : Id A b d) : Id A c d =
   <i> comp A (p @ i) [ (i = 0) -> q, (i = 1) -> r ]
 
-inv (A : U) (a b : A) (p : Id A a b) : Id A b a = <i> p @ -i
 
 -- lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c)
 --          (s : Id (Id A a c) (compId A a b c p q) (compId A a b c p q')) : Id (Id A b c) q q' =
diff --git a/examples/prelude.ctt b/examples/prelude.ctt
new file mode 100644
index 0000000..b0fee3c
--- /dev/null
+++ b/examples/prelude.ctt
@@ -0,0 +1,43 @@
+module prelude where
+
+Id (A : U) (a0 a1 : A) : U = IdP (<i> A) a0 a1
+
+refl (A : U) (a : A) : Id A a a = <i> a
+
+mapOnPath (A B : U) (f : A -> B) (a b : A)
+          (p : Id A a b) : Id B (f a) (f b) = <i> f (p @ i)
+
+funExt (A : U) (B : A -> U) (f g : (x : A) -> B x)
+       (p : (x : A) -> Id (B x) (f x) (g x)) :
+       Id ((y : A) -> B y) f g = <i> \(a : A) -> (p a) @ i
+
+
+subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b =
+  transport (mapOnPath A U P a b p) e
+
+substRefl (A : U) (P : A -> U) (a : A) (e : P a) :
+  Id (P a) (subst A P a a (refl A a) e) e = refl (P a) e
+
+singl (A : U) (a : A) : U = (x : A) * Id A a x
+
+contrSingl (A : U) (a b : A) (p : Id A a b) :
+  Id (singl A a) (a,refl A a) (b,p) = <i> (p @ i,<j> p @ i /\ j)
+
+J (A : U) (a : A) (C : (x : A) -> Id A a x -> U)
+  (d : C a (refl A a)) (x : A) (p : Id A a x) : C x p =
+    subst (singl A a) T (a, refl A a) (x, p) (contrSingl A a x p) d
+      where T (z : singl A a) : U = C (z.1) (z.2)
+
+defEqJ (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refl A a)) :
+       Id (C a (refl A a)) (J A a C d a (refl A a)) d = refl (C a (refl A a)) d
+
+inv (A : U) (a b : A) (p : Id A a b) : Id A b a = <i> p @ -i
+
+isoId (A B : U) (f : A -> B) (g : B -> A)
+      (s : (y:B) -> Id B (f (g y)) y)
+      (t : (x:A) -> Id A (g (f x)) x) : Id U A B =
+      <i> glue B [ (i = 0) -> (A,(f,(g,(s,t)))) ]
+
+lemTest (A : U) : (B : U) (p : Id U A B) (a : A) -> IdP p a (transport p a) =
+  J U A (\(B : U) (p : Id U A B) -> (a : A) -> IdP p a (transport p a)) rem
+    where rem (a : A) : Id A a a = refl A a
\ No newline at end of file