Add evaluation of Glue and GlueElem

diff --git a/CTT.hs b/CTT.hs
index dde18a65b3a940d36b9f153e8b5cf25c5379561b..562ddb98ae4e917737a5042a08f4030f5f9aaafa 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -3,6 +3,8 @@ module CTT where
 import Control.Applicative
 import Data.List
 import Data.Maybe
+import Data.Map (Map,(!))
+import qualified Data.Map as Map
 import Text.PrettyPrint as PP
 
 import Connections
@@ -50,7 +52,7 @@ data Ter = App Ter Ter
          | U
            -- Sigma types:
          | Sigma Ter
-         | SPair Ter Ter
+         | Pair Ter Ter
          | Fst Ter
          | Snd Ter
            -- constructor c Ms
@@ -69,6 +71,9 @@ data Ter = App Ter Ter
            -- Kan Composition
          | Comp Ter Ter (System Ter)
          | Trans Ter Ter
+           -- Glue
+         | Glue Ter (System Ter)
+         | GlueElem Ter (System Ter)
   deriving Eq
 
 -- For an expression t, returns (u,ts) where u is no application and t = u ts
@@ -93,7 +98,7 @@ data Val = VU
          | Ter Ter Env
          | VPi Val Val
          | VSigma Val Val
-         | VSPair Val Val
+         | VPair Val Val
          | VCon Label [Val]
 
            -- Id values
@@ -102,6 +107,10 @@ data Val = VU
          | VComp Val Val (System Val)
          | VTrans Val Val
 
+           -- Glue values
+         | VGlue Val (System Val)
+         | VGlueElem Val (System Val)
+
            -- Neutral values:
          | VVar Ident Val
          | VFst Val
@@ -119,8 +128,34 @@ isNeutral v = case v of
   VSplit _ v      -> isNeutral v
   VApp v _        -> isNeutral v
   VAppFormula v _ -> isNeutral v
+  VComp a u ts    -> isNeutralComp a u ts
+  VTrans a u      -> isNeutralTrans a u -- isNeutral a || isNeutralComp (a @@ 0) u Map.empty
   _               -> False
 
+isNeutralSystem :: System Val -> Bool
+isNeutralSystem = any isNeutral . Map.elems
+
+isNeutralTrans :: Val -> Val -> Bool
+isNeutralTrans (VPath i a) u = foo i a u
+  where foo :: Name -> Val -> Val -> Bool
+        foo i a u | isNeutral a = True
+        foo i (Ter Sum{} _) u   = isNeutral u
+        foo i (VGlue _ as) u    =
+          let shasBeta = (shape as) `face` (i ~> 0)
+          in shasBeta /= Map.empty && eps `Map.notMember` shasBeta && isNeutral u
+isNeutralTrans u _ = isNeutral u
+
+isNeutralComp :: Val -> Val -> System Val -> Bool
+isNeutralComp a _ _ | isNeutral a = True
+isNeutralComp (Ter Sum{} _) u ts  = isNeutral u || isNeutralSystem ts
+isNeutralComp (VGlue _ as) u ts | isNeutral u = True
+                                | otherwise   =
+  let shas = shape as
+      testFace beta _ = let shasBeta = shas `face` beta
+                        in shasBeta /= Map.empty && eps `Map.notMember` shasBeta
+  in isNeutralSystem (Map.filterWithKey testFace ts)
+isNeutralComp _ _ _ = False
+
 mkVar :: Int -> Val -> Val
 mkVar k = VVar ('X' : show k)
 
@@ -133,29 +168,26 @@ unCon v           = error $ "unCon: not a constructor: " ++ show v
 -- | Environments
 
 data Env = Empty
-         | Pair Env (Ident,Val)
+         | Upd Env (Ident,Val)
          | Def [Decl] Env
          | Sub Env (Name,Formula)
   deriving Eq
 
-pairs :: Env -> [(Ident,Val)] -> Env
-pairs = foldl Pair
-
--- lookupIdent :: Ident -> [(Ident,a)] -> Maybe a
--- lookupIdent x defs = listToMaybe [ t | ((y,l),t) <- defs, x == y ]
+upds :: Env -> [(Ident,Val)] -> Env
+upds = foldl Upd
 
 mapEnv :: (Val -> Val) -> (Formula -> Formula) -> Env -> Env
 mapEnv f g e = case e of
   Empty         -> Empty
-  Pair e (x,v)  -> Pair (mapEnv f g e) (x,f v)
+  Upd e (x,v)   -> Upd (mapEnv f g e) (x,f v)
   Def ts e      -> Def ts (mapEnv f g e)
   Sub e (i,phi) -> Sub (mapEnv f g e) (i,g phi)
 
 valAndFormulaOfEnv :: Env -> ([Val],[Formula])
 valAndFormulaOfEnv rho = case rho of
   Empty -> ([],[])
-  Pair rho (_,u) -> let (us,phis) = valAndFormulaOfEnv rho
-                    in (u:us,phis)
+  Upd rho (_,u) -> let (us,phis) = valAndFormulaOfEnv rho
+                   in (u:us,phis)
   Sub rho (_,phi) -> let (us,phis) = valAndFormulaOfEnv rho
                      in (us,phi:phis)
   Def _ rho -> valAndFormulaOfEnv rho
@@ -168,10 +200,10 @@ formulaOfEnv = snd . valAndFormulaOfEnv
 
 domainEnv :: Env -> [Name]
 domainEnv rho = case rho of
-  Empty        -> []
-  Pair e (x,v) -> domainEnv e
-  Def ts e     -> domainEnv e
-  Sub e (i,_)  -> i : domainEnv e
+  Empty       -> []
+  Upd e (x,v) -> domainEnv e
+  Def ts e    -> domainEnv e
+  Sub e (i,_) -> i : domainEnv e
 
 --------------------------------------------------------------------------------
 -- | Pretty printing
@@ -183,10 +215,10 @@ showEnv, showEnv1 :: Env -> Doc
 showEnv e = case e of
   Empty           -> PP.empty
   Def _ env       -> showEnv env
-  Pair env (x,u)  -> parens (showEnv1 env <> showVal u)
+  Upd env (x,u)   -> parens (showEnv1 env <> showVal u)
   Sub env (i,phi) -> parens (showEnv1 env <> text (show phi))
-showEnv1 (Pair env (x,u)) = showEnv1 env <> showVal u <> text ", "
-showEnv1 e                = showEnv e
+showEnv1 (Upd env (x,u)) = showEnv1 env <> showVal u <> text ", "
+showEnv1 e               = showEnv e
 
 instance Show Loc where
   show = render . showLoc
@@ -212,7 +244,7 @@ showTer v = case v of
   Fst e            -> showTer e <> text ".1"
   Snd e            -> showTer e <> text ".2"
   Sigma e0         -> text "Sigma" <+> showTer e0
-  SPair e0 e1      -> parens (showTer1 e0 <> comma <> showTer1 e1)
+  Pair e0 e1       -> parens (showTer1 e0 <> comma <> showTer1 e1)
   Where e d        -> showTer e <+> text "where" <+> showDecls d
   Var x            -> text x
   Con c es         -> text c <+> showTers es
@@ -224,6 +256,8 @@ showTer v = case v of
   AppFormula e phi -> showTer1 e <+> char '@' <+> showFormula phi
   Comp e0 e1 es    -> text "comp" <+> showTers [e0,e1] <+> text (showSystem es)
   Trans e0 e1      -> text "transport" <+> showTers [e0,e1]
+  Glue a ts        -> text "glue" <+> showTer a <+> text (showSystem ts)
+  GlueElem a ts    -> text "glueElem" <+> showTer a <+> text (showSystem ts)
 
 showTers :: [Ter] -> Doc
 showTers = hsep . map showTer1
@@ -250,7 +284,7 @@ showVal v = case v of
   Ter t env         -> showTer t <+> showEnv env
   VCon c us         -> text c <+> showVals us
   VPi a b           -> text "Pi" <+> showVals [a,b]
-  VSPair u v        -> parens (showVal1 u <> comma <> showVal1 v)
+  VPair u v         -> parens (showVal1 u <> comma <> showVal1 v)
   VSigma u v        -> text "Sigma" <+> showVals [u,v]
   VApp u v          -> showVal u <+> showVal1 v
   VSplit u v        -> showVal u <+> showVal1 v
@@ -262,6 +296,8 @@ showVal v = case v of
   VAppFormula v phi -> showVal1 v <+> char '@' <+> showFormula phi
   VComp v0 v1 vs    -> text "comp" <+> showVals [v0,v1] <+> text (showSystem vs)
   VTrans v0 v1      -> text "trans" <+> showVals [v0,v1]
+  VGlue a ts        -> text "glue" <+> showVal a <+> text (showSystem ts)
+  VGlueElem a ts    -> text "glueElem" <+> showVal a <+> text (showSystem ts)
 showVal1 v = case v of
   VU        -> char 'U'
   VCon c [] -> text c
@@ -270,4 +306,3 @@ showVal1 v = case v of
 
 showVals :: [Val] -> Doc
 showVals = hsep . map showVal1
-

diff --git a/Eval.hs b/Eval.hs
index af4935776a7dc92de95beef053678f9a981e4763..ca49cc462d1259aebd868a0246e95b76902c81dc 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -4,14 +4,12 @@ import Data.List
 import Data.Maybe (fromMaybe)
 import Data.Map (Map,(!))
 import qualified Data.Map as Map
--- import Data.Set (Set)
--- import qualified Data.Set as Set
 
 import Connections
 import CTT
 
 look :: String -> Env -> Val
-look x (Pair rho (y,u)) | x == y    = u
+look x (Upd rho (y,u)) | x == y    = u
                         | otherwise = look x rho
 look x r@(Def rho r1) = case lookup x rho of
   Just (_,t) -> eval r t
@@ -19,7 +17,7 @@ look x r@(Def rho r1) = case lookup x rho of
 look x (Sub rho _) = look x rho
 
 lookType :: String -> Env -> Val
-lookType x (Pair rho (y,VVar _ a)) | x == y    = a
+lookType x (Upd rho (y,VVar _ a)) | x == y    = a
                                    | otherwise = lookType x rho
 lookType x r@(Def rho r1) = case lookup x rho of
   Just (a,_) -> eval r a
@@ -27,7 +25,7 @@ lookType x r@(Def rho r1) = case lookup x rho of
 lookType x (Sub rho _) = lookType x rho
 
 lookName :: Name -> Env -> Formula
-lookName i (Pair rho _) = lookName i rho
+lookName i (Upd rho _) = lookName i rho
 lookName i (Def _ rho)  = lookName i rho
 lookName i (Sub rho (j,phi)) | i == j    = phi
                              | otherwise = lookName i rho
@@ -37,7 +35,7 @@ lookName i (Sub rho (j,phi)) | i == j    = phi
 
 instance Nominal Env where
   support Empty             = []
-  support (Pair rho (_,u))  = support u `union` support rho
+  support (Upd rho (_,u))   = support u `union` support rho
   support (Sub rho (_,phi)) = support phi `union` support rho
   support (Def _ rho)       = support rho
 
@@ -53,7 +51,7 @@ instance Nominal Val where
   support (VPath i v)                   = i `delete` support v
   support (VTrans u v)                  = support (u,v)
   support (VSigma u v)                  = support (u,v)
-  support (VSPair u v)                  = support (u,v)
+  support (VPair u v)                   = support (u,v)
   support (VFst u)                      = support u
   support (VSnd u)                      = support u
   support (VCon _ vs)                   = support vs
@@ -61,6 +59,8 @@ instance Nominal Val where
   support (VApp u v)                    = support (u,v)
   support (VAppFormula u phi)           = support (u,phi)
   support (VSplit u v)                  = support (u,v)
+  support (VGlue a ts)                  = support (a,ts)
+  support (VGlueElem a ts)              = support (a,ts)
 
   act u (i, phi) =
     let acti :: Nominal a => a -> a
@@ -77,7 +77,7 @@ instance Nominal Val where
               where k = fresh (v, Atom i, phi)
          VTrans u v -> transLine (acti u) (acti v)
          VSigma a f -> VSigma (acti a) (acti f)
-         VSPair u v -> VSPair (acti u) (acti v)
+         VPair u v -> VPair (acti u) (acti v)
          VFst u     -> VFst (acti u)
          VSnd u     -> VSnd (acti u)
          VCon c vs  -> VCon c (acti vs)
@@ -85,6 +85,8 @@ instance Nominal Val where
          VAppFormula u psi -> acti u @@ acti psi
          VApp u v   -> app (acti u) (acti v)
          VSplit u v -> app (acti u) (acti v)
+         VGlue a ts -> glue (acti a) (acti ts)
+         VGlueElem a ts -> glueElem (acti a) (acti ts)
 
   -- This increases efficiency as it won't trigger computation.
   swap u ij@ (i,j) =
@@ -99,7 +101,7 @@ instance Nominal Val where
          VPath k v -> VPath (swapName k ij) (sw v)
          VTrans u v -> VTrans (sw u) (sw v)
          VSigma a f -> VSigma (sw a) (sw f)
-         VSPair u v -> VSPair (sw u) (sw v)
+         VPair u v -> VPair (sw u) (sw v)
          VFst u     -> VFst (sw u)
          VSnd u     -> VSnd (sw u)
          VCon c vs  -> VCon c (sw vs)
@@ -107,7 +109,8 @@ instance Nominal Val where
          VAppFormula u psi -> VAppFormula (sw u) (sw psi)
          VApp u v          -> VApp (sw u) (sw v)
          VSplit u v        -> VSplit (sw u) (sw v)
-
+         VGlue a ts        -> VGlue (sw a) (sw ts)
+         VGlueElem a ts    -> VGlueElem (sw a) (sw ts)
 -----------------------------------------------------------------------
 -- The evaluator
 
@@ -119,7 +122,7 @@ eval rho v = case v of
   Pi t@(Lam _ a _)    -> VPi (eval rho a) (eval rho t)
   Lam{}               -> Ter v rho
   Sigma t@(Lam _ a _) -> VSigma (eval rho a) (eval rho t)
-  SPair a b           -> VSPair (eval rho a) (eval rho b)
+  Pair a b            -> VPair (eval rho a) (eval rho b)
   Fst a               -> fstVal (eval rho a)
   Snd a               -> sndVal (eval rho a)
   Where t decls       -> eval (Def decls rho) t
@@ -134,6 +137,8 @@ eval rho v = case v of
   Trans u v        -> transLine (eval rho u) (eval rho v)
   AppFormula e phi -> (eval rho e) @@ (evalFormula rho phi)
   Comp a t0 ts     -> compLine (eval rho a) (eval rho t0) (evalSystem rho ts)
+  Glue a ts        -> glue (eval rho a) (evalSystem rho ts)
+  GlueElem a ts    -> glueElem (eval rho a) (evalSystem rho ts)
 
 evalFormula :: Env -> Formula -> Formula
 evalFormula rho phi = case phi of
@@ -156,13 +161,12 @@ evalSystem rho ts =
 
 -- TODO: Write using case-of
 app :: Val -> Val -> Val
-app (Ter (Lam x _ t) e) u                  = eval (Pair e (x,u)) t
+app (Ter (Lam x _ t) e) u                  = eval (Upd e (x,u)) t
 app (Ter (Split _ _ nvs) e) (VCon name us) = case lookup name nvs of
-  Just (xs,t) -> eval (pairs e (zip xs us)) t
+  Just (xs,t) -> eval (upds e (zip xs us)) t
   Nothing     -> error $ "app: Split with insufficient arguments; " ++
                          " missing case for " ++ name
 app u@(Ter (Split _ _ _) _) v | isNeutral v = VSplit u v
-
 app kan@(VTrans (VPath i (VPi a f)) li0) ui1 =
     let j   = fresh (kan,ui1)
         (aj,fj) = (a,f) `swap` (i,j)
@@ -178,9 +182,9 @@ app r s | isNeutral r = VApp r s
 app _ _ = error "app"
 
 fstVal, sndVal :: Val -> Val
-fstVal (VSPair a b)    = a
+fstVal (VPair a b)    = a
 fstVal u | isNeutral u = VFst u
-sndVal (VSPair a b)    = b
+sndVal (VPair a b)    = b
 sndVal u | isNeutral u = VSnd u
 
 -- infer the type of a neutral value
@@ -204,7 +208,7 @@ inferType v = case v of
     VIdP a _ _ -> a @@ phi
     ty         -> error $ "inferType: expected IdP type for " ++ show v
                   ++ ", got " ++ show ty
-  _ -> error "inferType: not neutral " ++ show v
+  _ -> error $ "inferType: not neutral " ++ show v
 
 (@@) :: ToFormula a => Val -> a -> Val
 (VPath i u) @@ phi = u `act` (i,toFormula phi)
@@ -233,13 +237,14 @@ trans i v0 v1 = case (v0,v1) of
         fill_u1 = transFill i a u1
         ui1     = trans i a u1
         comp_u2 = trans i (app f fill_u1) u2
-    in VSPair ui1 comp_u2
+    in VPair ui1 comp_u2
   (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
   _ | isNeutral v0 || isNeutral v1 -> VTrans (VPath i v0) v1
-    | otherwise -> error "trans not implemented"
+  (VGlue a ts,_) -> transGlue i a ts v1
+  _ | otherwise -> error "trans not implemented"
 transNeg i a u = trans i (a `sym` i) u
 
 transFill, transFillNeg :: Name -> Val -> Val -> Val
@@ -252,10 +257,74 @@ transps i []         _ []     = []
 transps i ((x,a):as) e (u:us) =
   let v   = transFill i (eval e a) u
       vi1 = trans i (eval e a) u
-      vs  = transps i as (Pair e (x,v)) us
+      vs  = transps i as (Upd e (x,v)) us
   in vi1 : vs
 transps _ _ _ _ = error "transps: different lengths of types and values"
 
+transGlue :: Name -> Val -> System Val -> Val -> Val
+transGlue i b hisos wi0 = glueElem vi1'' usi1
+  where vi0  = unGlue (hisos `face` (i ~> 0)) wi0 -- in b(i0)
+
+        v    = transFill i b vi0           -- in b
+        vi1  = trans i b vi0           -- in b(i1)
+
+        hisosI1 = hisos `face` (i ~> 1)
+        hisos'' =
+          Map.filterWithKey (\alpha _ -> alpha `Map.notMember` hisos) hisosI1
+
+        -- set of elements in hisos independent of i
+        hisos'  = Map.filterWithKey (\alpha _ -> i `Map.notMember` alpha) hisos
+
+        us'    = Map.mapWithKey (\gamma _ ->
+                  transFill i (b `face` gamma) (wi0 `face` gamma))
+                 hisos'
+        usi1'  = Map.mapWithKey (\gamma _ ->
+                  trans i (b `face` gamma) (wi0 `face` gamma))
+                 hisos'
+
+        ls'    = Map.mapWithKey (\gamma isoG ->
+                  pathComp i (hisoDom isoG) (v `face` gamma)
+                           ((hisoFun isoG) `app` (us' ! gamma)) Map.empty)
+                 hisos'
+        bi1   = b `face` (i ~> 1)
+        vi1'  = compLine bi1 vi1 ls'
+
+        uls''   = Map.mapWithKey (\gamma isoG ->
+                     gradLemma (bi1 `face` gamma) isoG (usi1' `face` gamma)
+                               (vi1' `face` gamma))
+                   hisos''
+
+        vi1''   = compLine bi1 vi1' (Map.map snd uls'')
+
+        usi1    = Map.mapWithKey (\gamma _ ->
+                    if gamma `Map.member` usi1'
+                       then usi1' ! gamma
+                       else fst (uls'' ! gamma))
+                  hisosI1
+
+-- Grad Lemma, takes a iso an L-system ts a value v s.t. sigma us = border v
+-- outputs u s.t. border u = us and an L-path between v and sigma u
+-- an theta is a L path if L-border theta is constant
+gradLemma :: Val -> Val -> System Val -> Val -> (Val, Val)
+gradLemma a hiso@(VPair b (VPair f (VPair g (VPair s t)))) us v = (u, VPath i theta'')
+  where i:j:_   = freshs (a,hiso,us,v)
+        us'     = Map.mapWithKey (\alpha uAlpha ->
+                                   app (t `face` alpha) uAlpha @@ i) us
+        theta   = fill i a (app g v) us'
+        u       = comp i a (app g v) us'
+        ws      = insertSystem (i ~> 1) (app t u @@ j) $
+                  Map.mapWithKey
+                    (\alpha uAlpha ->
+                      app (t `face` alpha) uAlpha @@ (Atom i :/\: Atom j)) us
+        theta'  = compNeg j a theta ws
+        xs      = insertSystem (i ~> 0) (app s v @@ j) $
+                  insertSystem (i ~> 1) (app s (app f u) @@ j) $
+                  Map.mapWithKey
+                    (\alpha uAlpha ->
+                      app (s `face` alpha) (app (f `face` alpha) uAlpha) @@ j) us
+        theta'' = comp j b (app f theta') xs
+
+
 -----------------------------------------------------------
 -- Composition
 
@@ -287,12 +356,10 @@ comps i []         _ []         = []
 comps i ((x,a):as) e ((ts,u):tsus) =
   let v   = genFill i (eval e a) u ts
       vi1 = genComp i (eval e a) u ts
-      vs  = comps i as (Pair e (x,v)) tsus
+      vs  = comps i as (Upd e (x,v)) tsus
   in vi1 : vs
 comps _ _ _ _ = error "comps: different lengths of types and values"
 
--- compNeg a u ts = comp a u (ts `sym` i)
-
 -- i is independent of a and u
 comp :: Name -> Val -> Val -> System Val -> Val
 comp i a u ts | eps `Map.member` ts    = (ts ! eps) `face` (i ~> 1)
@@ -302,7 +369,7 @@ comp i a u ts | not (Map.null indep)   = comp i a u ts'
 comp i a u ts = let j = fresh (Atom i,a,u,ts) -- maybe only in vid??
                 in case a of
   VIdP p _ _ -> VPath j $ comp i (p @@ j) (u @@ j) (Map.map (@@ j) ts)
-  VSigma a f -> VSPair ui1 comp_u2
+  VSigma a f -> VPair ui1 comp_u2
     where (t1s, t2s) = (Map.map fstVal ts, Map.map sndVal ts)
           (u1,  u2)  = (fstVal u, sndVal u)
           fill_u1    = fill i a u1 t1s
@@ -312,6 +379,7 @@ comp i a u ts = let j = fresh (Atom i,a,u,ts) -- maybe only in vid??
   VU -> VComp VU u (Map.map (VPath i) ts)
   _ | isNeutral a || isNeutralSystem ts || isNeutral u ->
     VComp a u (Map.map (VPath i) ts)
+  VGlue b hisos -> compGlue i b hisos u ts
   Ter (Sum _ _ nass) env -> case u of
     VCon n us -> case lookup n nass of
       Just as -> VCon n $ comps i as env tsus
@@ -319,21 +387,89 @@ comp i a u ts = let j = fresh (Atom i,a,u,ts) -- maybe only in vid??
       Nothing -> error $ "comp: missing constructor in labelled sum " ++ n
     _ -> error "comp ter sum"
 
+compNeg :: Name -> Val -> Val -> System Val -> Val
+compNeg i a u ts = comp i a u (ts `sym` i)
+
+unGlue :: System Val -> Val -> Val
+unGlue hisos w
+    | Map.null hisos         = w
+    | eps `Map.member` hisos = app (hisoFun (hisos ! eps)) w
+    | otherwise              = case w of
+       VGlueElem v us   -> v
+--       KanUElem _ v    -> app g v
+       _ -> error $ "unGlue: " ++ show w ++ " should be neutral!"
+
+compGlue :: Name -> Val -> System Val -> Val -> System Val -> Val
+compGlue i b hisos wi0 ws = glueElem vi1' usi1'
+  where vs   = Map.mapWithKey
+                 (\alpha wAlpha -> unGlue (hisos `face` alpha) wAlpha) ws
+        vi0  = unGlue hisos wi0 -- in b
+
+        v    = fill i b vi0 vs           -- in b
+        vi1  = comp i b vi0 vs           -- in b
+
+        us'    = Map.mapWithKey (\gamma _ ->
+                   fill i (b `face` gamma) (wi0 `face` gamma) (ws `face` gamma))
+                 hisos
+        usi1'  = Map.mapWithKey (\gamma _ ->
+                   comp i (b `face` gamma) (wi0 `face` gamma) (ws `face` gamma))
+                 hisos
+
+        ls'    = Map.mapWithKey (\gamma isoG ->
+                  pathComp i (hisoDom isoG) (v `face` gamma)
+                             (hisoFun isoG `app` (us' ! gamma)) (vs `face` gamma))
+                 hisos
+
+        vi1'  = compLine b vi1 ls'
+
+-- assumes u and u' : A are solutions of us + (i0 -> u(i0))
+-- The output is an L-path in A(i1) between u(i1) and u'(i1)
+pathComp :: Name -> Val -> Val -> Val -> System Val -> Val
+pathComp i a u u' us = VPath j $ genComp i a (u `face` (i ~> 0)) us'
+  where j   = fresh (Atom i, a, us, u, u')
+        us' = insertsSystem [(j ~> 0, u), (j ~> 1, u')] us
+
+
+
 -- fills :: Name -> [(Ident,Ter)] -> Env -> [(System Val,Val)] -> [Val]
 -- fills i []         _ []         = []
 -- fills i ((x,a):as) e ((ts,u):tsus) =
 --   let v  = genFill i (eval e a) ts u
---       vs = fills i as (Pair e (x,v)) tsus
+--       vs = fills i as (Upd e (x,v)) tsus
 --   in v : vs
 -- fills _ _ _ _ = error "fills: different lengths of types and values"
 
+-------------------------------------------------------------------------------
+-- | Glue
+-- 
+-- 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
+
+hisoDom :: Val -> Val
+hisoDom (VPair b _) = b
+hisoDom x           = error $ "HisoDom: Not an hiso: " ++ show x
+
+hisoFun :: Val -> Val
+hisoFun (VPair _ (VPair f _)) = f
+hisoFun x                     = error $ "HisoFun: Not an hiso: " ++ show x
+
+glue :: Val -> System Val -> Val
+glue b ts | Map.null ts         = b
+          | eps `Map.member` ts = hisoDom (ts ! eps)
+          | otherwise           = VGlue b ts
+
+glueElem :: Val -> System Val -> Val
+glueElem v us | Map.null us         = v
+              | eps `Map.member` us = us ! eps
+              | otherwise           = VGlueElem v us
 
 -------------------------------------------------------------------------------
 -- | Conversion
 
-isNeutralSystem :: System Val -> Bool
-isNeutralSystem = any isNeutral . Map.elems
-
 class Convertible a where
   conv :: Int -> a -> a -> Bool
 
@@ -350,13 +486,13 @@ instance Convertible Val where
              | otherwise = let j = fresh (u,v) in case (u,v) of
     (Ter (Lam x a u) e,Ter (Lam x' a' u') e') ->
       let v = mkVar k (eval e a)
-      in conv (k+1) (eval (Pair e (x,v)) u) (eval (Pair e' (x',v)) u')
+      in conv (k+1) (eval (Upd e (x,v)) u) (eval (Upd e' (x',v)) u')
     (Ter (Lam x a u) e,u') ->
       let v = mkVar k (eval e a)
-      in conv (k+1) (eval (Pair e (x,v)) u) (app u' v)
+      in conv (k+1) (eval (Upd e (x,v)) u) (app u' v)
     (u',Ter (Lam x a u) e) ->
       let v = mkVar k (eval e a)
-      in conv (k+1) (app u' v) (eval (Pair e (x,v)) u)
+      in conv (k+1) (app u' v) (eval (Upd e (x,v)) u)
     (Ter (Split p _ _) e,Ter (Split p' _ _) e') -> (p == p') && conv k e e'
     (Ter (Sum p _ _) e,Ter (Sum p' _ _) e')     -> (p == p') && conv k e e'
     (Ter (Undef p) e,Ter (Undef p') e')         -> (p == p') && conv k e e'
@@ -367,9 +503,9 @@ instance Convertible Val where
       let w = mkVar k u
       in conv k u u' && conv (k+1) (app v w) (app v' w)
     (VCon c us,VCon c' us')   -> (c == c') && conv k us us'
-    (VSPair u v,VSPair u' v') -> conv k u u' && conv k v v'
-    (VSPair u v,w)            -> conv k u (fstVal w) && conv k v (sndVal w)
-    (w,VSPair u v)            -> conv k (fstVal w) u && conv k (sndVal w) v
+    (VPair u v,VPair u' v') -> conv k u u' && conv k v v'
+    (VPair u v,w)            -> conv k u (fstVal w) && conv k v (sndVal w)
+    (w,VPair u v)            -> conv k (fstVal w) u && conv k (sndVal w) v
     (VFst u,VFst u')          -> conv k u u'
     (VSnd u,VSnd u')          -> conv k u u'
     (VApp u v,VApp u' v')     -> conv k u u' && conv k v v'

diff --git a/TypeChecker.hs b/TypeChecker.hs
index a71aa285a5dd918784ddf6a3e406a4bb6831c896..9f9a60187b595fd92517208ed6be8ce4aae4f86d 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -35,7 +35,7 @@ silentEnv  = TEnv 0 Empty False
 \r
 addTypeVal :: (Ident,Val) -> TEnv -> TEnv\r
 addTypeVal (x,a) (TEnv k rho v) =\r
-  TEnv (k+1) (Pair rho (x,mkVar k a)) v\r
+  TEnv (k+1) (Upd rho (x,mkVar k a)) v\r
 \r
 addSub :: (Name,Formula) -> TEnv -> TEnv\r
 addSub iphi (TEnv k rho v) = TEnv k (Sub rho iphi) v\r
@@ -45,7 +45,7 @@ addType (x,a) tenv@(TEnv _ rho _) = return $ addTypeVal (x,eval rho a) tenv
 \r
 addBranch :: [(Ident,Val)] -> (Tele,Env) -> TEnv -> TEnv\r
 addBranch nvs (tele,env) (TEnv k rho v) =\r
-  TEnv (k + length nvs) (pairs rho nvs) v\r
+  TEnv (k + length nvs) (upds rho nvs) v\r
 \r
 addDecls :: [Decl] -> TEnv -> TEnv\r
 addDecls d (TEnv k rho v) = TEnv k (Def d rho) v\r
@@ -152,7 +152,7 @@ check a t = case (a,t) of
     unless (conv k a (eval rho a')) $ throwError "check: lam types don't match"\r
     var <- getFresh a\r
     local (addTypeVal (x,a)) $ check (app f var) t\r
-  (VSigma a f, SPair t1 t2) -> do\r
+  (VSigma a f, Pair t1 t2) -> do\r
     check a t1\r
     e <- asks env\r
     let v = eval e t1\r
@@ -191,7 +191,7 @@ checkBranch (xas,nu) f (c,(xs,e)) = do
 mkVars k [] _ = []\r
 mkVars k ((x,a):xas) nu =\r
   let w = mkVar k (eval nu a)\r
-  in w : mkVars (k+1) xas (Pair nu (x,w))\r
+  in w : mkVars (k+1) xas (Upd nu (x,w))\r
 \r
 checkFormula :: Formula -> Typing ()\r
 checkFormula phi = do\r
@@ -292,7 +292,7 @@ checks ((x,a):xas,nu) (e:es) = do
   check v e\r
   rho <- asks env\r
   let v' = eval rho e\r
-  checks (xas,Pair nu (x,v')) es\r
+  checks (xas,Upd nu (x,v')) es\r
 checks _              _      = throwError "checks"\r
 \r
 -- Not used since we have U : U\r