From a1ee1930644ca12e2b21ee8e38fbb6ad5a11a04d Mon Sep 17 00:00:00 2001
From: Simon Huber <hubsim@gmail.com>
Date: Thu, 4 Jun 2015 18:03:22 +0200
Subject: [PATCH] Added fill as a term and comp is now genComp

---
 CTT.hs         | 16 ++++------------
 Eval.hs        | 20 ++++++++++++++++++++
 Exp.cf         |  2 +-
 Resolver.hs    |  7 ++-----
 TypeChecker.hs |  9 +++++++++
 5 files changed, 36 insertions(+), 18 deletions(-)

diff --git a/CTT.hs b/CTT.hs
index 1e9f5de..3dbe30c 100644
--- a/CTT.hs
+++ b/CTT.hs
@@ -105,8 +105,9 @@ data Ter = App Ter Ter
          | IdP Ter Ter Ter
          | Path Name Ter
          | AppFormula Ter Formula
-           -- Kan Composition
+           -- Kan composition and filling
          | Comp Ter Ter (System Ter)
+         | Fill Ter Ter (System Ter)
          -- | Trans Ter Ter
            -- Composition in the Universe
          -- | CompElem Ter (System Ter) Ter (System Ter)
@@ -183,15 +184,6 @@ data Val = VU
          | VLam Ident Val Val
   deriving Eq
 
--- data HIso = Iso Val Val Val Val Val
---           | Eq Val
---   deriving (Eq,Show)
-
--- toHIso :: Val -> HIso
--- toHIso (VPair a (VPair f (VPair g (VPair s t)))) = Iso a f g s t
--- toHIso v = Eq v
--- toHIso _ = error "toHIso"
-
 isNeutral :: Val -> Bool
 isNeutral v = case v of
   Ter Undef{} _  -> True
@@ -407,8 +399,8 @@ showTer v = case v of
   IdP e0 e1 e2       -> text "IdP" <+> showTers [e0,e1,e2]
   Path i e           -> char '<' <> text (show i) <> char '>' <+> showTer e
   AppFormula e phi   -> showTer1 e <+> char '@' <+> showFormula phi
-  Comp e0 e1 es      -> text "comp" <+> showTers [e0,e1]
-                        <+> text (showSystem es)
+  Comp e t ts        -> text "comp" <+> showTers [e,t] <+> text (showSystem ts)
+  Fill e t ts        -> text "fill" <+> showTers [e,t] <+> text (showSystem ts)
   -- Trans e0 e1        -> text "transport" <+> showTers [e0,e1]
   Glue a ts          -> text "glue" <+> showTer1 a <+> text (showSystem ts)
   GlueElem a ts      -> text "glueElem" <+> showTer1 a <+> text (showSystem ts)
diff --git a/Eval.hs b/Eval.hs
index 3144eef..db7827e 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -159,6 +159,7 @@ eval rho v = case v of
     in VPath j (eval (sub (i,Atom j) rho) t)
   AppFormula e phi    -> eval rho e @@ evalFormula rho phi
   Comp a t0 ts        -> compLine (eval rho a) (eval rho t0) (evalSystem rho ts)
+  Fill a t0 ts        -> fillLine (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)
   _                   -> error $ "Cannot evaluate " ++ show v
@@ -443,6 +444,25 @@ hisoFun :: Val -> Val
 hisoFun (VPair _ (VPair f _)) = f
 hisoFun x                     = error $ "HisoFun: Not an hiso: " ++ show x
 
+-- -- Every line in the universe induces an hiso
+-- eqToIso :: Val -> Val
+-- eqToIso e = VPair e0 (VPair f (VPair g (VPair s t)))
+--   where e0 = e @@ Zero
+--         (i,j,x,y,ev) = (Name "i",Name "j",Var "x",Var "y",Var "E")
+--         evinv = Path "i" $ AppFormula ev (NegAtom i)
+--         (ev0, ev1) = (AppFormula ev (Dir Zero),AppFormula ev (Dir One))
+--         eenv = upd ("E",e) empty
+--         (eplus z,eminus z) = (Comp ev z Map.empty,Comp evinv z Map.empty)
+--         (eup z,edown z) = (Comp )
+--         f = Ter (Lam x ev1 (eminus x)) eenv
+--         g = Ter (Lam y ev0 (eplus y)) eenv
+--         -- s : (y : b) -> f (g y) = y
+--         ssys = mkSystem [(j ~> 0, transFill j (e @@ j) b)
+--                         ,(j ~> 1, transFillNeg j (e @@ j)
+--                                   (trans j (e @@ j) b))])
+--         s = Ter (Lam y ev0 $ Path j $ Comp einv
+--               ) eenv
+
 -- eqToIso :: Name -> Val -> Val
 -- eqToIso i u = VPair a (VPair f (VPair g (VPair s t)))
 --   where a = u `face` (i ~> 1)
diff --git a/Exp.cf b/Exp.cf
index 0c0dcf3..718647d 100644
--- a/Exp.cf
+++ b/Exp.cf
@@ -33,7 +33,7 @@ App.          Exp2 ::= Exp2 Exp3 ;
 IdP.          Exp3 ::= "IdP" Exp4 Exp4 Exp4 ;
 Trans.        Exp3 ::= "transport" Exp4 Exp4 ;
 Comp.         Exp3 ::= "comp" Exp4 Exp4 System ;
-GenComp.      Exp3 ::= "genComp" Exp4 Exp4 System ;
+Fill.         Exp3 ::= "fill" Exp4 Exp4 System ;
 Glue.         Exp3 ::= "glue" Exp4 System ;
 -- GlueElem.     Exp3 ::= "glueElem" Exp4 System ;
 -- CompElem.     Exp3 ::= "compElem" Exp4 System Exp4 System ;
diff --git a/Resolver.hs b/Resolver.hs
index 60c9ebc..734d5c9 100644
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -204,11 +204,8 @@ resolveExp e = case e of
       _ -> CTT.AppFormula <$> resolveExp t <*> resolveFormula phi
   Trans x y   -> CTT.Comp <$> resolveExp x <*> resolveExp y <*> pure Map.empty
   IdP x y z   -> CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z
-  Comp u v ts -> CTT.Comp <$> (CTT.Path (C.Name "_") <$> resolveExp u)
-                   <*> resolveExp v <*> resolveSystem ts
-
-  GenComp u v ts -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
-
+  Comp u v ts -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
+  Fill u v ts -> CTT.Fill <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
   Glue u ts   -> do
     rs <- resolveSystem ts
     let isIso (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ _)))) = True
diff --git a/TypeChecker.hs b/TypeChecker.hs
index c94f8ab..82f51bf 100644
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -429,6 +429,15 @@ infer e = case e of
     check va0 t0
     checkPathSystem t0 va ps
     return va1
+  Fill a t0 ps -> do
+    (va0, va1) <- checkPath (constPath VU) a
+    va <- evalTyping a
+    check va0 t0
+    checkPathSystem t0 va ps
+    vt  <- evalTyping t0
+    rho <- asks env
+    let vps = evalSystem rho ps
+    return (VIdP va vt (compLine va vt vps))
   -- CompElem a es u us -> do
   --   check VU a
   --   rho <- asks env
-- 
2.34.1