From 95a6ee7f8959a68796ea850531efadeece1abda5 Mon Sep 17 00:00:00 2001 From: Anders Date: Thu, 19 Mar 2015 16:25:55 +0100 Subject: [PATCH] Started adding comp --- Connections.hs | 9 ++++++++- Eval.hs | 45 ++++++++++++++++++++++++++------------------- TypeChecker.hs | 22 ++++++++++++++++++++++ examples/nat.ctt | 4 ++-- 4 files changed, 58 insertions(+), 22 deletions(-) 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 -- 2.34.1