From 750961a28b36b3f064154fcb946e803ff8339fb8 Mon Sep 17 00:00:00 2001
From: Simon Huber <hubsim@gmail.com>
Date: Wed, 3 Jun 2015 14:27:03 +0200
Subject: [PATCH] Adapted compGlue

---
 CTT.hs         |  5 ++++
 Eval.hs        | 68 ++++++++++++++++++++++++++++++++++++--------------
 TypeChecker.hs |  4 ---
 3 files changed, 54 insertions(+), 23 deletions(-)

diff --git a/CTT.hs b/CTT.hs
index b3bc093..6932cc6 100644
--- a/CTT.hs
+++ b/CTT.hs
@@ -253,6 +253,11 @@ isCon :: Val -> Bool
 isCon VCon{} = True
 isCon _      = False
 
+-- Constant path: <_> v
+constPath :: Val -> Val
+constPath = VPath (Name "_")
+
+
 --------------------------------------------------------------------------------
 -- | Environments
 
diff --git a/Eval.hs b/Eval.hs
index 0e958ed..eda61ac 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -42,16 +42,16 @@ instance Nominal Ctxt where
   act e _   = e
   swap e _  = e
 
-instance Nominal HIso where
-  support h = case h of
-    Iso a f g s t -> support [a,f,g,s,t]
-    Eq v -> support v
-  act h iphi = case h of
-    Iso a f g s t -> Iso (a `act` iphi) (f `act` iphi) (g `act` iphi) (s `act` iphi) (t `act` iphi)
-    Eq v -> Eq (v `act` iphi)
-  swap h ij = case h of
-    Iso a f g s t -> Iso (a `swap` ij) (f`swap` ij) (g`swap` ij) (s`swap` ij) (t`swap` ij)
-    Eq v -> Eq (v`swap` ij)
+-- instance Nominal HIso where
+--   support h = case h of
+--     Iso a f g s t -> support [a,f,g,s,t]
+--     Eq v -> support v
+--   act h iphi = case h of
+--     Iso a f g s t -> Iso (a `act` iphi) (f `act` iphi) (g `act` iphi) (s `act` iphi) (t `act` iphi)
+--     Eq v -> Eq (v `act` iphi)
+--   swap h ij = case h of
+--     Iso a f g s t -> Iso (a `swap` ij) (f`swap` ij) (g`swap` ij) (s`swap` ij) (t`swap` ij)
+--     Eq v -> Eq (v`swap` ij)
 
 instance Nominal Val where
   support v = case v of
@@ -560,27 +560,57 @@ transGlue i b hisos wi0 = glueElem vi1'' usi1
                   hisosI1
 
 compGlue :: Name -> Val -> System Val -> Val -> System Val -> Val
-compGlue i b hisos wi0 ws = glueElem vi1' usi1'
-  where vs   = mapWithKey
+compGlue i b hisos wi0 ws = glueElem vi1'' usi1''
+  where bi1 = b `face` (i ~> 1)
+        vs   = mapWithKey
                  (\alpha wAlpha -> unGlue (hisos `face` alpha) wAlpha) ws
-        vi0  = unGlue hisos wi0 -- in b
+        vsi1 = vs `face` (i ~> 1) -- same as: border vi1 vs
+        vi0  = unGlue (hisos `face` (i ~> 0)) wi0 -- in b(i0)
 
         v    = fill i b vi0 vs           -- in b
-        vi1  = comp i b vi0 vs           -- in b
+        vi1  = comp i b vi0 vs           -- is v `face` (i ~> 1) in b(i1)
+
+        hisosI1 = hisos `face` (i ~> 1)
+        hisos'  = filterWithKey (\alpha _ -> i `Map.notMember` alpha) hisos
+        -- hisos'' = filterWithKey (\alpha _ -> not (alpha `Map.member` hisos)) hisosI1
+        hisos'' = filterWithKey (\alpha _ -> not (alpha `Map.member` hisos')) hisosI1
 
         us'    = mapWithKey (\gamma isoG ->
                    fill i (hisoDom isoG) (wi0 `face` gamma) (ws `face` gamma))
-                 hisos
+                 hisos'
         usi1'  = mapWithKey (\gamma isoG ->
                    comp i (hisoDom isoG) (wi0 `face` gamma) (ws `face` gamma))
-                 hisos
+                 hisos'
 
         ls'    = mapWithKey (\gamma isoG ->
                    pathComp i (b `face` gamma) (v `face` gamma)
-                   (hisoFun isoG `app` (us' ! gamma)) (vs `face` gamma))
-                 hisos
+                     (hisoFun isoG `app` (us' ! gamma)) (vs `face` gamma))
+                 hisos'
+
+        vi1' = compLine (constPath bi1) vi1 (ls' `unionSystem` vsi1)
+
+        wsi1 = ws `face` (i ~> 1)
+
+        -- for gamma in hisos'', (i1) gamma is in hisos, so wsi1 gamma
+        -- is in the domain of isoGamma
+        uls'' = mapWithKey (\gamma isoG ->
+                  gradLemma (bi1 `face` gamma) isoG
+                    ((usi1' `face` gamma) `unionSystem` (wsi1 `face` gamma))
+                    (vi1' `face` gamma))
+                  hisos''
+
+        vsi1' = border vi1' hisos'
+
+        vi1'' = compLine (constPath bi1) vi1'
+                  (Map.map snd uls'' `unionSystem` vsi1' `unionSystem` vsi1)
+
+        usi1'' = Map.mapWithKey (\gamma _ ->
+                     if gamma `Map.member` usi1' then usi1' ! gamma
+                     else fst (uls'' ! gamma))
+                   hisosI1
+
+
 
-        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)
diff --git a/TypeChecker.hs b/TypeChecker.hs
index b8fa058..d70220a 100644
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -103,10 +103,6 @@ getLblType c u = throwError ("expected a data type for the constructor "
 unlessM :: Monad m => m Bool -> m () -> m ()
 unlessM mb x = mb >>= flip unless x
 
--- Constant path: <_> v
-constPath :: Val -> Val
-constPath = VPath (Name "_")
-
 mkVars :: [String] -> Tele -> Env -> [(Ident,Val)]
 mkVars _ [] _           = []
 mkVars ns ((x,a):xas) nu =
-- 
2.34.1