From: Anders <mortberg@chalmers.se>
Date: Thu, 19 Mar 2015 15:25:55 +0000 (+0100)
Subject: Started adding comp
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=95a6ee7f8959a68796ea850531efadeece1abda5;p=cubicaltt.git

Started adding comp
---

diff --git a/Connections.hs b/Connections.hs
index a40b7cc..61002dc 100644
--- a/Connections.hs
+++ b/Connections.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE TypeSynonymInstances, FlexibleInstances,
-             GeneralizedNewtypeDeriving #-}
+             GeneralizedNewtypeDeriving, TupleSections #-}
 module Connections where
 
 import Control.Applicative
@@ -75,6 +75,10 @@ compatibles :: [Face] -> Bool
 compatibles []     = True
 compatibles (x:xs) = all (x `compatible`) xs && compatibles xs
 
+allCompatible :: [Face] -> [(Face,Face)]
+allCompatible []     = []
+allCompatible (f:fs) = map (f,) (filter (compatible f) fs) ++ allCompatible fs
+
 -- Partial composition operation
 meet :: Face -> Face -> Face
 meet = Map.unionWith f
@@ -112,6 +116,9 @@ i ~> d = Map.singleton i d
 eps :: Face
 eps = Map.empty
 
+minus :: Face -> Face -> Face
+minus alpha beta = alpha Map.\\ beta
+
 -- Compute the witness of A <= B, ie compute C s.t. B = CA
 -- leqW :: Face -> Face -> Face
 -- leqW = undefined
diff --git a/Eval.hs b/Eval.hs
index 6a4bc38..eca1162 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -70,12 +70,12 @@ instance Nominal Val where
          VU      -> VU
          Ter t e -> Ter t (acti e)
          VPi a f -> VPi (acti a) (acti f)
-         VComp a v ts -> comp (acti a) (acti v) (acti ts)
+         VComp a v ts -> compLine (acti a) (acti v) (acti ts)
          VIdP a u v -> VIdP (acti a) (acti u) (acti v)
          VPath j v | j `notElem` sphi -> VPath j (acti v)
                    | otherwise -> VPath k (v `swap` (j,k))
               where k = fresh (v, Atom i, phi)
-         VTrans u v -> trans' (acti u) (acti v)
+         VTrans u v -> transLine (acti u) (acti v)
          VSigma a f -> VSigma (acti a) (acti f)
          VSPair u v -> VSPair (acti u) (acti v)
          VFst u     -> VFst (acti u)
@@ -131,10 +131,9 @@ eval rho v = case v of
   Path i t            ->
     let j = fresh rho
     in VPath j (eval (Sub rho (i,Atom j)) t)
-  Trans u v -> trans' (eval rho u) (eval rho v)
+  Trans u v        -> transLine (eval rho u) (eval rho v)
   AppFormula e phi -> (eval rho e) @@ (evalFormula rho phi)
-
--- Comp
+  Comp a t0 ts     -> compLine (eval rho a) (eval rho t0) (evalSystem rho ts)
 
 evalFormula :: Env -> Formula -> Formula
 evalFormula rho phi = case phi of
@@ -147,6 +146,9 @@ evalFormula rho phi = case phi of
 evals :: Env -> [(Ident,Ter)] -> [(Ident,Val)]
 evals env bts = [ (b,eval env t) | (b,t) <- bts ]
 
+evalSystem :: Env -> System Ter -> System Val
+evalSystem rho = undefined -- Map.mapWithKey (\alpha -> eval (rho `face` alpha))
+
 app :: Val -> Val -> Val
 app (Ter (Lam x _ t) e) u                  = eval (Pair e (x,u)) t
 app (Ter (Split _ _ nvs) e) (VCon name us) = case lookup name nvs of
@@ -173,9 +175,7 @@ inferType v = case v of
   VSnd t -> case inferType t of
     VSigma _ f -> app f (VFst t)
     _       -> error $ "inferType: not neutral " ++ show v
-  VSplit t0 t1 -> case inferType t0 of
-    VPi _ f -> app f t1
-    _       -> error $ "inferType: not neutral " ++ show v
+  VSplit (Ter (Split _ f _) rho) v1 -> app (eval rho f) v1
   VApp t0 t1 -> case inferType t0 of
     VPi _ f -> app f t1
     _       -> error $ "inferType: not neutral " ++ show v
@@ -194,10 +194,9 @@ v @@ phi = case (inferType v,toFormula phi) of
 -----------------------------------------------------------
 -- Transport
 
-trans' :: Val -> Val -> Val
-trans' u v = case u of
-  VPath i u0 -> trans i u0 v
-  u0         -> VTrans u0 v
+transLine :: Val -> Val -> Val
+transLine u v = trans i (u @@ i) v
+  where i = fresh (u,v)
 
 trans :: Name -> Val -> Val -> Val
 trans i v0 v1 = case (v0,v1) of
@@ -235,15 +234,19 @@ transps _ _ _ _ = error "transps: different lengths of types and values"
 -----------------------------------------------------------
 -- Composition
 
-comp :: Val -> Val -> System Val -> Val
-comp a u ts = error "comp"
+compLine :: Val -> Val -> System Val -> Val
+compLine a u ts = comp i (a @@ i) u (Map.map (@@ i) ts)
+  where i = fresh (a,u,ts)
+
 -- compNeg a u ts = comp a u (ts `sym` i)
+comp :: Name -> Val -> Val -> System Val -> Val
+comp = undefined
 
 genComp, genCompNeg :: Name -> Val -> Val -> System Val -> Val
 genComp i a u ts | Map.null ts = trans i a u
-genComp i a u ts = comp ai1 (trans i a u) ts'
-  where ai1   = a `face` (i ~> 1)
-        j     = fresh (a,Atom i,ts,u)
+genComp i a u ts = comp i ai1 (trans i a u) ts'
+  where ai1 = a `face` (i ~> 1)
+        j   = fresh (a,Atom i,ts,u)
         comp' alpha u = VPath i (trans j ((a `face` alpha) `disj` (i,j)) u)
         ts' = Map.mapWithKey comp' ts
 genCompNeg i a u ts = genComp i (a `sym` i) u (ts `sym` i)
@@ -275,13 +278,17 @@ comps _ _ _ _ = error "comps: different lengths of types and values"
 -------------------------------------------------------------------------------
 -- | Conversion
 
-
 class Convertible a where
-  conv   :: Int -> a -> a -> Bool
+  conv :: Int -> a -> a -> Bool
 
 isIndep :: (Nominal a, Convertible a) => Int -> Name -> a -> Bool
 isIndep k i u = conv k u (u `face` (i ~> 0))
 
+isCompSystem :: (Nominal a, Convertible a) => Int -> System a -> Bool
+isCompSystem k ts = and [ conv k (getFace alpha beta) (getFace beta alpha)
+                        | (alpha,beta) <- allCompatible (Map.keys ts) ]
+    where getFace a b = face (ts ! a) (b `minus` a)
+
 instance Convertible Val where
   conv k u v | u == v    = True
              | otherwise = let j = fresh (u,v) in case (u,v) of
diff --git a/TypeChecker.hs b/TypeChecker.hs
index c2edbcd..029dc41 100644
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -4,6 +4,8 @@ import Data.Either
 import Data.Function
 import Data.List
 import Data.Maybe
+import Data.Map (Map,(!))
+import qualified Data.Map as Map
 import Data.Monoid hiding (Sum)
 import Control.Monad
 import Control.Monad.Trans
@@ -51,6 +53,9 @@ addDecls d (TEnv k rho v) = TEnv k (Def d rho) v
 addTele :: Tele -> TEnv -> Typing TEnv
 addTele xas lenv = foldM (flip addType) lenv xas
 
+faceEnv :: Face -> TEnv -> TEnv
+faceEnv alpha tenv = tenv{env=env tenv `face` alpha}
+
 trace :: String -> Typing ()
 trace s = do
   b <- verbose <$> ask
@@ -249,8 +254,25 @@ infer e = case e of
       case b of
         VIdP (VPath _ VU) _ b1 -> return b1
         _ -> throwError $ "transport expects a path but got " ++ show p
+  Comp a t0 ts -> do
+    check VU a
+    rho <- asks env
+    let va = eval rho a
+    check va t0
+
+    -- check rho alpha |- t_alpha : a alpha
+    sequence $ Map.elems $
+      Map.mapWithKey (\alpha talpha ->
+                       local (faceEnv alpha) (check (va `face` alpha) talpha)) ts
+
+    -- check that the system is compatible
+    k <- asks index
+    unless (isCompSystem k (evalSystem rho ts))
+      (throwError ("Incompatible system " ++ show ts))
+    return va
   _ -> throwError ("infer " ++ show e)
 
+
 -- Check that a term is a path and output the source and target
 checkPath :: Ter -> Typing (Val,Val)
 checkPath (Path i a) = do
diff --git a/examples/nat.ctt b/examples/nat.ctt
index e139873..2f736b4 100644
--- a/examples/nat.ctt
+++ b/examples/nat.ctt
@@ -72,5 +72,5 @@ J (A : U) (a : A) (C : (x : A) -> Id A a x -> U)
 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)
\ No newline at end of file
+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)
\ No newline at end of file