From: Anders Date: Wed, 18 Mar 2015 17:20:06 +0000 (+0100) Subject: Add Id, Path, AppFormula and Trans. X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=67c202dfc27c22568c24be828b821732d33ca83a;p=cubicaltt.git Add Id, Path, AppFormula and Trans. funExt is working! --- diff --git a/CTT.hs b/CTT.hs index ea7c891..543c0ed 100644 --- a/CTT.hs +++ b/CTT.hs @@ -30,9 +30,8 @@ type Tele = [(Binder,Ter)] -- Labelled sum: c (x1 : A1) .. (xn : An) type LblSum = [(Binder,Tele)] +-- Declarations: x : A = e type Decl = (Binder,(Ter,Ter)) - --- Mutual recursive definitions: (x1 : A1) .. (xn : An) and x1 = e1 .. xn = en type Decls = [Decl] declBinders :: Decls -> [Binder] @@ -73,7 +72,8 @@ data Ter = App Ter Ter | Path Name Ter | AppFormula Ter Formula -- Kan Composition - | Comp Name Ter Ter (System Ter) + | Comp Ter Ter (System Ter) + | Trans Ter Ter deriving Eq -- For an expression t, returns (u,ts) where u is no application and t = u ts @@ -104,7 +104,8 @@ data Val = VU -- Id values | VIdP Val Val Val | VPath Name Val - | VComp Name Val Val (System Val) + | VComp Val Val (System Val) + | VTrans Val Val -- Neutral values: | VVar String Val @@ -133,7 +134,8 @@ mkVar k = VVar ('X' : show k) data Env = Empty | Pair Env (Binder,Val) - | PDef Decls Env + | Def Decls Env + | Sub Env (Name,Formula) deriving Eq pairs :: Env -> [(Binder,Val)] -> Env @@ -142,15 +144,32 @@ pairs = foldl Pair lookupIdent :: Ident -> [(Binder,a)] -> Maybe a lookupIdent x defs = listToMaybe [ t | ((y,l),t) <- defs, x == y ] -mapEnv :: (Val -> Val) -> Env -> Env -mapEnv _ Empty = Empty -mapEnv f (Pair e (x,v)) = Pair (mapEnv f e) (x,f v) -mapEnv f (PDef ts e) = PDef ts (mapEnv f e) +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) + Def ts e -> Def ts (mapEnv f g e) + Sub e (i,phi) -> Sub (mapEnv f g e) (i,g phi) valOfEnv :: Env -> [Val] valOfEnv Empty = [] valOfEnv (Pair env (_,v)) = v : valOfEnv env -valOfEnv (PDef _ env) = valOfEnv env +valOfEnv (Def _ env) = valOfEnv env +valOfEnv (Sub env _) = valOfEnv env + +formulaOfEnv :: Env -> [Formula] +formulaOfEnv e = case e of + Empty -> [] + Pair rho _ -> formulaOfEnv rho + Def _ rho -> formulaOfEnv rho + Sub rho (_,phi) -> phi : formulaOfEnv rho + +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 -------------------------------------------------------------------------------- -- | Pretty printing @@ -158,14 +177,14 @@ valOfEnv (PDef _ env) = valOfEnv env instance Show Env where show = render . showEnv -showEnv :: Env -> Doc +showEnv, showEnv1 :: Env -> Doc showEnv e = case e of - Empty -> PP.empty - PDef _ env -> showEnv env - Pair env (x,u) -> parens (showEnv1 env <> showVal u) - where - showEnv1 (Pair env (x,u)) = showEnv1 env <> showVal u <> text ", " - showEnv1 e = showEnv e + Empty -> PP.empty + Def _ env -> showEnv env + Pair 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 instance Show Loc where show = render . showLoc @@ -195,8 +214,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 '@' <> text (show phi) - Comp i e0 e1 es -> text "comp" <+> text (show i) <+> showTers [e0,e1] <+> - text (showSystem es) + Comp e0 e1 es -> text "comp" <+> showTers [e0,e1] <+> text (showSystem es) + Trans e0 e1 -> text "trans" <+> showTers [e0,e1] showTers :: [Ter] -> Doc showTers = hsep . map showTer1 @@ -233,8 +252,8 @@ showVal v = case v of VIdP v0 v1 v2 -> text "IdP" <+> showVals [v0,v1,v2] VPath i v -> char '<' <> text (show i) <> char '>' <+> showVal v VAppFormula v phi -> showVal1 v <> char '@' <> text (show phi) - VComp i v0 v1 vs -> text "comp" <+> text (show i) <+> showVals [v0,v1] <+> - text (showSystem vs) + VComp v0 v1 vs -> text "comp" <+> showVals [v0,v1] <+> text (showSystem vs) + VTrans v0 v1 -> text "trans" <+> showVals [v0,v1] showVal1 v = case v of VU -> char 'U' VCon c [] -> text c diff --git a/Connections.hs b/Connections.hs index 536e4a0..6e6bb18 100644 --- a/Connections.hs +++ b/Connections.hs @@ -22,7 +22,6 @@ swapName k (i,j) | k == i = j | k == j = i | otherwise = k - -- | Directions data Dir = Zero | One deriving (Eq,Ord) @@ -68,16 +67,6 @@ showFace alpha = concat [ "(" ++ show i ++ "," ++ show d ++ ")" swapFace :: Face -> (Name,Name) -> Face swapFace alpha ij = Map.mapKeys (`swapName` ij) alpha --- i,j,k,l :: Name --- i = Name 0 --- j = Name 1 --- k = Name 2 --- l = Name 3 - --- f1,f2 :: Face --- f1 = Map.fromList [(i,0),(j,1),(k,0)] --- f2 = Map.fromList [(i,0),(j,1),(l,1)] - -- Check if two faces are compatible compatible :: Face -> Face -> Bool compatible xs ys = and (Map.elems (Map.intersectionWith (==) xs ys)) @@ -107,8 +96,6 @@ meetId xs = xs `meet` xs == xs meets :: [Face] -> [Face] -> [Face] meets xs ys = nub [ meet x y | x <- xs, y <- ys, compatible x y ] --- instance Ord Face where - leq :: Face -> Face -> Bool alpha `leq` beta = meetMaybe alpha beta == Just alpha @@ -129,12 +116,6 @@ eps = Map.empty -- leqW :: Face -> Face -> Face -- leqW = undefined --- data Faces = Faces (Set Face) - --- instance Nominal Faces where --- support (Faces f) = --- act (Faces f) (i, phi) = Faces f - -- | Formulas data Formula = Dir Dir | Atom Name @@ -199,9 +180,9 @@ orFormula (Dir Zero) phi = phi orFormula phi (Dir Zero) = phi orFormula phi psi = phi :\/: psi -evalFormula :: Formula -> Face -> Formula -evalFormula phi alpha = - Map.foldWithKey (\i d psi -> act psi (i,Dir d)) phi alpha +-- evalFormula :: Formula -> Face -> Formula +-- evalFormula phi alpha = +-- Map.foldWithKey (\i d psi -> act psi (i,Dir d)) phi alpha -- (Dir b) alpha = Dir b -- evalFormula (Atom i) alpha = case Map.lookup i alpha of @@ -218,22 +199,17 @@ evalFormula phi alpha = invFormula :: Formula -> Dir -> [Face] invFormula (Dir b') b = [ eps | b == b' ] invFormula (Atom i) b = [ Map.singleton i b ] -invFormula (NegAtom i) b = [ Map.singleton i (- b) ] +invFormula (NegAtom i) b = [ Map.singleton i (- b) ] invFormula (phi :/\: psi) Zero = invFormula phi 0 `union` invFormula psi 0 -invFormula (phi :/\: psi) One = - meets (invFormula phi 1) (invFormula psi 1) +invFormula (phi :/\: psi) One = meets (invFormula phi 1) (invFormula psi 1) invFormula (phi :\/: psi) b = invFormula (negFormula phi :/\: negFormula psi) (- b) --- primeImplicants :: Formula -> Dir -> System () --- primeImplicants phi Zero = primeImplicants (NegAtom phi) One --- primeImplicants phi One = undefined - propInvFormulaIncomp :: Formula -> Dir -> Bool propInvFormulaIncomp phi b = incomparables (invFormula phi b) -prop_invFormula :: Formula -> Dir -> Bool -prop_invFormula phi b = - all (\alpha -> phi `evalFormula` alpha == Dir b) (invFormula phi b) +-- prop_invFormula :: Formula -> Dir -> Bool +-- prop_invFormula phi b = +-- all (\alpha -> phi `evalFormula` alpha == Dir b) (invFormula phi b) testInvFormula :: [Face] testInvFormula = invFormula (Atom (Name 0) :/\: Atom (Name 1)) 1 @@ -249,12 +225,8 @@ gensyms d = let x = gensym d in x : gensyms (x : d) class Nominal a where support :: a -> [Name] --- act u (i,phi) should have u # (phi - i) ?? act :: a -> (Name,Formula) -> a - - swap :: a -> (Name,Name) -> a - -- swap u (i,j) = - -- where k = fresh (u,i,j) + swap :: a -> (Name,Name) -> a fresh :: Nominal a => a -> Name fresh = gensym . support @@ -351,11 +323,10 @@ showSystem ts = concat $ intersperse ", " [ showFace alpha ++ " |-> " ++ show u | (alpha,u) <- Map.toList ts ] insertSystem :: Face -> a -> System a -> System a -insertSystem alpha v ts = - case find (comparable alpha) (Map.keys ts) of - Just beta | alpha `leq` beta -> ts - | otherwise -> Map.insert alpha v (Map.delete beta ts) - Nothing -> Map.insert alpha v ts +insertSystem alpha v ts = case find (comparable alpha) (Map.keys ts) of + Just beta | alpha `leq` beta -> ts + | otherwise -> Map.insert alpha v (Map.delete beta ts) + Nothing -> Map.insert alpha v ts insertsSystem :: [(Face, a)] -> System a -> System a insertsSystem faces us = @@ -364,7 +335,7 @@ insertsSystem faces us = mkSystem :: [(Face, a)] -> System a mkSystem = flip insertsSystem Map.empty -unionSystem :: System a -> System a -> System a +unionSystem :: System a -> System a -> System a unionSystem us vs = insertsSystem (Map.assocs us) vs -- could something like that work?? @@ -377,10 +348,6 @@ transposeSystemAndList _ [] = [] transposeSystemAndList tss (u:us) = (Map.map head tss,u):transposeSystemAndList (Map.map tail tss) us --- transposeSystem :: System [a] -> [System a] --- transposeSystem ts = --- Map.map (\as -> head a) ts : transposeSystem (Map.map (\as -> tail as) ts) - -- Quickcheck this: -- (i = phi) * beta = (beta - i) * (i = phi beta) @@ -426,8 +393,9 @@ sym a i = a `act` (i, NegAtom i) rename :: Nominal a => a -> (Name, Name) -> a rename a (i, j) = a `act` (i, Atom j) -connect :: Nominal a => a -> (Name, Name) -> a -connect a (i, j) = a `act` (i, Atom i :/\: Atom j) +conj, disj :: Nominal a => a -> (Name, Name) -> a +conj a (i, j) = a `act` (i, Atom i :/\: Atom j) +disj a (i, j) = a `act` (i, Atom i :\/: Atom j) leqSystem :: Face -> System a -> Bool alpha `leqSystem` us = @@ -440,6 +408,3 @@ proj us alpha | eps `Map.member` usalpha = usalpha ! eps error $ "proj: eps not in " ++ show usalpha ++ "\nwhich is the " ++ show alpha ++ "\nface of " ++ show us where usalpha = us `face` alpha - --- actSystemCom :: Formula -> Name -> Formula -> Bool --- actSystemCom psi i phi = border phi diff --git a/Eval.hs b/Eval.hs index 4df8e14..936f59f 100644 --- a/Eval.hs +++ b/Eval.hs @@ -2,6 +2,10 @@ module Eval where 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 @@ -9,17 +13,97 @@ import CTT look :: String -> Env -> Val look x (Pair rho ((y,_),u)) | x == y = u | otherwise = look x rho -look x r@(PDef es r1) = case lookupIdent x es of +look x r@(Def rho r1) = case lookupIdent x rho of Just (_,t) -> eval r t - Nothing -> look x r1 + Nothing -> look x r1 +look x (Sub rho _) = look x rho lookType :: String -> Env -> Val lookType x (Pair rho ((y,_),VVar _ a)) | x == y = a | otherwise = lookType x rho -lookType x r@(PDef es r1) = case lookupIdent x es of +lookType x r@(Def rho r1) = case lookupIdent x rho of Just (a,_) -> eval r a Nothing -> lookType x r1 +lookType x (Sub rho _) = lookType x rho +lookName :: Name -> Env -> Formula +lookName i (Pair rho _) = lookName i rho +lookName i (Def _ rho) = lookName i rho +lookName i (Sub rho (j,phi)) | i == j = phi + | otherwise = lookName i rho + +----------------------------------------------------------------------- +-- Nominal instances + +instance Nominal Env where + support = support . formulaOfEnv + act e iphi = mapEnv (`act` iphi) (`act` iphi) e + swap e ij = mapEnv (`swap` ij) (`swap` ij) e + +instance Nominal Val where + support VU = [] + support (Ter _ e) = support e + support (VPi v1 v2) = support [v1,v2] + support (VComp a u ts) = support (a,u,ts) + support (VIdP a v0 v1) = support [a,v0,v1] + support (VPath i v) = i `delete` support v + support (VSigma u v) = support (u,v) + support (VSPair u v) = support (u,v) + support (VFst u) = support u + support (VSnd u) = support u + support (VCon _ vs) = support vs + support (VVar _ v) = support v + support (VApp u v) = support (u, v) + support (VAppFormula u phi) = support (u, phi) + support (VSplit u v) = support (u, v) + + act u (i, phi) = + let acti :: Nominal a => a -> a + acti u = act u (i, phi) + sphi = support phi + in case u of + 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) + 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) + VSigma a f -> VSigma (acti a) (acti f) + VSPair u v -> VSPair (acti u) (acti v) + VFst u -> VFst (acti u) + VSnd u -> VSnd (acti u) + VCon c vs -> VCon c (acti vs) + VVar x v -> VVar x (acti v) + VAppFormula u psi -> acti u @@ acti psi + VApp u v -> app (acti u) (acti v) + VSplit u v -> app (acti u) (acti v) + + -- This increases efficiency as it won't trigger computation. + swap u ij@ (i,j) = + let sw :: Nominal a => a -> a + sw u = swap u ij + in case u of + VU -> VU + Ter t e -> Ter t (sw e) + VPi a f -> VPi (sw a) (sw f) + VComp a v ts -> VComp (sw a) (sw v) (sw ts) + VIdP a u v -> VIdP (sw a) (sw u) (sw v) + VPath k v -> VPath (swapName k ij) (sw v) + VSigma a f -> VSigma (sw a) (sw f) + VSPair u v -> VSPair (sw u) (sw v) + VFst u -> VFst (sw u) + VSnd u -> VSnd (sw u) + VCon c vs -> VCon c (sw vs) + VVar x v -> VVar x (sw v) + VAppFormula u psi -> VAppFormula (sw u) (sw psi) + VApp u v -> VApp (sw u) (sw v) + VSplit u v -> VSplit (sw u) (sw v) + +----------------------------------------------------------------------- +-- The evaluator + eval :: Env -> Ter -> Val eval rho v = case v of U -> VU @@ -31,16 +115,28 @@ eval rho v = case v of SPair a b -> VSPair (eval rho a) (eval rho b) Fst a -> fstVal (eval rho a) Snd a -> sndVal (eval rho a) - Where t decls -> eval (PDef decls rho) t + Where t decls -> eval (Def decls rho) t Con name ts -> VCon name (map (eval rho) ts) Split l t brcs -> Ter (Split l t brcs) rho Sum pr lbls -> Ter (Sum pr lbls) rho Undef l -> error $ "eval: undefined at " ++ show l IdP a e0 e1 -> VIdP (eval rho a) (eval rho e0) (eval rho e1) - Path i t -> Ter (Path i t) rho - -- let j = fresh (t,rho) - -- in VPath j (eval rho (t `swap` (i,j))) + Path i t -> + let j = fresh rho + in VPath j (eval (Sub rho (i,Atom j)) t) + Trans u v -> case eval rho u of + VPath i u0 -> trans i u0 (eval rho v) + u0 -> VTrans u0 (eval rho v) + AppFormula e phi -> (eval rho e) @@ (evalFormula rho phi) +-- Comp +evalFormula :: Env -> Formula -> Formula +evalFormula rho phi = case phi of + Atom i -> lookName i rho + NegAtom i -> negFormula (lookName i rho) + phi1 :/\: phi2 -> evalFormula rho phi1 `andFormula` evalFormula rho phi2 + phi1 :\/: phi2 -> evalFormula rho phi1 `orFormula` evalFormula rho phi2 + _ -> phi evals :: Env -> [(Binder,Ter)] -> [(Binder,Val)] evals env bts = [ (b,eval env t) | (b,t) <- bts ] @@ -61,12 +157,93 @@ fstVal u | isNeutral u = VFst u sndVal (VSPair a b) = b sndVal u | isNeutral u = VSnd u +(@@) :: ToFormula a => Val -> a -> Val +(VPath i u) @@ phi = u `act` (i, toFormula phi) +-- (KanUElem _ u) @@ phi = u @@ phi +v @@ phi = VAppFormula v (toFormula phi) + +----------------------------------------------------------- +-- Transport + +trans :: Name -> Val -> Val -> Val +trans i v0 v1 = case (v0,v1) of + (VIdP a u v,w) -> + let j = fresh (Atom i, v0, w) + ts' = mkSystem [(j ~> 0,u),(j ~> 1,v)] + in VPath j $ genComp i (a @@ j) (w @@ j) ts' + (VSigma a f,u) -> + let (u1,u2) = (fstVal u,sndVal u) + 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 + (VPi{},_) -> VTrans (VPath i v0) v1 + (Ter (Sum _ nass) env,VCon n us) -> case lookupIdent 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" + +transFill, transFillNeg :: Name -> Val -> Val -> Val +transFill i a u = trans j (a `conj` (i,j)) u + where j = fresh (Atom i,a,u) +transFillNeg i a u = (transFill i (a `sym` i) u) `sym` i + +transps :: Name -> [(Binder,Ter)] -> Env -> [Val] -> [Val] +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 + in vi1 : vs +transps _ _ _ _ = error "transps: different lengths of types and values" + +----------------------------------------------------------- +-- Composition + +comp :: Val -> Val -> System Val -> Val +comp a u ts = error "comp" +-- compNeg a u ts = comp a u (ts `sym` i) + +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) + 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) + +genFill, genFillNeg :: Name -> Val -> Val -> System Val -> Val +genFill i a u ts = genComp j (a `conj` (i,j)) u (ts `conj` (i,j)) + where j = fresh (Atom i,a,u,ts) +genFillNeg i a u ts = (genFill i (a `sym` i) u (ts `sym` i)) `sym` i + +comps :: Name -> [(Binder,Ter)] -> Env -> [(System Val,Val)] -> [Val] +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 + in vi1 : vs +comps _ _ _ _ = error "comps: different lengths of types and values" + + +-- fills :: Name -> [(Binder,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 +-- in v : vs +-- fills _ _ _ _ = error "fills: different lengths of types and values" + + ------------------------------------------------------------------------------- -- | Conversion conv :: Int -> Val -> Val -> Bool conv k u v | u == v = True - | otherwise = case (u,v) of + | 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') @@ -94,6 +271,13 @@ conv k u v | u == v = True (VApp u v,VApp u' v') -> conv k u u' && conv k v v' (VSplit u v,VSplit u' v') -> conv k u u' && conv k v v' (VVar x _, VVar x' _) -> x == x' + (VIdP a b c,VIdP a' b' c') -> conv k a a' && conv k b b' && conv k c c' + (VPath i a,VPath i' a') -> conv k (a `swap` (i,j)) (a' `swap` (i',j)) + (VPath i a,p') -> conv k (a `swap` (i,j)) (p' @@ j) + (p,VPath i' a') -> conv k (p @@ j) (a' `swap` (i',j)) + -- VAppformula + -- VTrans + -- VComp _ -> False convEnv :: Int -> Env -> Env -> Bool diff --git a/Exp.cf b/Exp.cf index 928b5ab..5fee375 100644 --- a/Exp.cf +++ b/Exp.cf @@ -21,17 +21,21 @@ separator Decl ";" ; Where. ExpWhere ::= Exp "where" "{" [Decl] "}" ; NoWhere. ExpWhere ::= Exp ; -Let. Exp ::= "let" "{" [Decl] "}" "in" Exp ; -Lam. Exp ::= "\\" [PTele] "->" Exp ; -Fun. Exp1 ::= Exp2 "->" Exp1 ; -Pi. Exp1 ::= [PTele] "->" Exp1 ; -Sigma. Exp1 ::= [PTele] "*" Exp1 ; -App. Exp2 ::= Exp2 Exp3 ; -Var. Exp3 ::= AIdent ; -U. Exp3 ::= "U" ; -Fst. Exp3 ::= Exp3 ".1" ; -Snd. Exp3 ::= Exp3 ".2" ; -Pair. Exp3 ::= "(" Exp "," Exp ")" ; +Let. Exp ::= "let" "{" [Decl] "}" "in" Exp ; +Lam. Exp ::= "\\" [PTele] "->" Exp ; +Path. Exp ::= "<" Name ">" Exp ; +Fun. Exp1 ::= Exp2 "->" Exp1 ; +Pi. Exp1 ::= [PTele] "->" Exp1 ; +Sigma. Exp1 ::= [PTele] "*" Exp1 ; +App. Exp2 ::= Exp2 Exp3 ; +Var. Exp3 ::= AIdent ; +AppFormula. Exp3 ::= Exp3 "@" Name ; +U. Exp3 ::= "U" ; +Fst. Exp3 ::= Exp3 ".1" ; +Snd. Exp3 ::= Exp3 ".2" ; +IdP. Exp3 ::= "IdP" ; +Trans. Exp3 ::= "transport" ; +Pair. Exp3 ::= "(" Exp "," Exp ")" ; coercions Exp 3 ; -- Branches @@ -52,4 +56,7 @@ PTele. PTele ::= "(" Exp ":" Exp ")" ; terminator nonempty PTele "" ; position token AIdent ((letter|'\''|'_')(letter|digit|'\''|'_')*) ; -terminator AIdent "" ; \ No newline at end of file +terminator AIdent "" ; + +position token Name (('?')(digit)*); +terminator Name "" ; \ No newline at end of file diff --git a/Resolver.hs b/Resolver.hs index d6a1a5d..968dfc3 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -5,6 +5,7 @@ module Resolver where import Exp.Abs import qualified CTT +import qualified Connections as C import Control.Applicative import Control.Monad.Trans @@ -102,7 +103,10 @@ noLoc = AIdent ((0,0),"_") resolveAIdent :: AIdent -> Resolver CTT.Binder resolveAIdent (AIdent (l,x)) = (x,) <$> getLoc l - + +resolveName :: Name -> Resolver C.Name +resolveName (Name (_,n)) = return $ C.Name $ read $ tail n + resolveVar :: AIdent -> Resolver Ter resolveVar (AIdent (l,x)) | (x == "_") || (x == "undefined") = CTT.Undef <$> getLoc l @@ -130,11 +134,20 @@ bind f (x,t) e = f <$> lam (x,t) e binds :: (Ter -> Ter) -> [(AIdent,Exp)] -> Resolver Ter -> Resolver Ter binds f = flip $ foldr $ bind f +resolveApps :: Exp -> [Exp] -> Resolver Ter +resolveApps Trans (x:y:xs) = do + let c = CTT.Trans <$> resolveExp x <*> resolveExp y + CTT.mkApps <$> c <*> mapM resolveExp xs +resolveApps IdP (x:y:z:xs) = do + let c = CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z + CTT.mkApps <$> c <*> mapM resolveExp xs +resolveApps x xs = CTT.mkApps <$> resolveExp x <*> mapM resolveExp xs + resolveExp :: Exp -> Resolver Ter resolveExp e = case e of U -> return CTT.U Var x -> resolveVar x - App t s -> CTT.mkApps <$> resolveExp x <*> mapM resolveExp xs + App t s -> resolveApps x xs where (x,xs) = unApps t [s] Sigma ptele b -> do tele <- flattenPTele ptele @@ -152,7 +165,9 @@ resolveExp e = case e of Let decls e -> do (rdecls,names) <- resolveDecls decls CTT.mkWheres rdecls <$> local (insertBinders names) (resolveExp e) - + Path i e -> CTT.Path <$> resolveName i <*> resolveExp e + AppFormula e n -> CTT.AppFormula <$> resolveExp e <*> (C.Atom <$> resolveName n) + resolveWhere :: ExpWhere -> Resolver Ter resolveWhere = resolveExp . unWhere diff --git a/TypeChecker.hs b/TypeChecker.hs index f9e5e8c..0595e37 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -12,6 +12,7 @@ import Control.Monad.Trans.Reader import Control.Monad.Error (throwError) import Control.Applicative +import Connections import CTT import Eval @@ -34,6 +35,9 @@ addTypeVal :: (Binder,Val) -> TEnv -> TEnv addTypeVal (x,a) (TEnv k rho v) = TEnv (k+1) (Pair rho (x,mkVar k a)) v +addSub :: (Name,Formula) -> TEnv -> TEnv +addSub iphi (TEnv k rho v) = TEnv k (Sub rho iphi) v + addType :: (Binder,Ter) -> TEnv -> Typing TEnv addType (x,a) tenv@(TEnv _ rho _) = return $ addTypeVal (x,eval rho a) tenv @@ -42,7 +46,7 @@ addBranch nvs (tele,env) (TEnv k rho v) = TEnv (k + length nvs) (pairs rho nvs) v addDecls :: Decls -> TEnv -> TEnv -addDecls d (TEnv k rho v) = TEnv k (PDef d rho) v +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 @@ -149,6 +153,24 @@ check a t = case (a,t) of checkDecls d local (addDecls d) $ check a e (_,Undef _) -> return () + (VU,IdP a e0 e1) -> case a of + Path i b -> do + rho <- asks env + when (i `elem` support rho) (throwError (show i ++ " is already declared")) + local (addSub (i,Atom i)) $ check VU b + check (eval (Sub rho (i,Dir 0)) b) e0 + check (eval (Sub rho (i,Dir 1)) b) e1 + _ -> do + b <- infer a + case b of + VIdP (VPath _ VU) b0 b1 -> do + check b0 e0 + check b1 e1 + _ -> throwError ("IdP expects a path but got " ++ show a) + (VIdP p a b,Path i e) -> do + rho <- asks env + when (i `elem` support rho) (throwError (show i ++ " is already declared")) + local (addSub (i,Atom i)) $ check (p @@ i) e _ -> do v <- infer t k <- index <$> ask @@ -167,9 +189,13 @@ mkVars k ((x,a):xas) nu = let w = mkVar k (eval nu a) in w : mkVars (k+1) xas (Pair nu (x,w)) --- inferNeutral :: Val -> Val --- inferNeutral (VN (VVar _ a)) = a --- inferNeutral _ = error "not done yet" +checkFormula :: Formula -> Typing () +checkFormula phi = do + rho <- asks env + let dom = domainEnv rho + if all (\x -> x `elem` dom) (support phi) + then return () + else throwError ("checkFormula: " ++ show phi) -- infer the type of e infer :: Ter -> Typing Val @@ -203,6 +229,12 @@ infer e = case e of Where t d -> do checkDecls d local (addDecls d) $ infer t + AppFormula e phi -> do + checkFormula phi + t <- infer e + case t of + VIdP a _ _ -> return $ a @@ phi + _ -> throwError (show e ++ " is not a path") _ -> throwError ("infer " ++ show e) checks :: (Tele,Env) -> [Ter] -> Typing () diff --git a/examples/nat.ctt b/examples/nat.ctt index 47c9f44..58dad5d 100644 --- a/examples/nat.ctt +++ b/examples/nat.ctt @@ -21,7 +21,6 @@ add' : nat -> nat -> nat = split id (A : U) (a : A) : A = a - data list (A : U) = nil | cons (a : A) (as : list A) l : list nat = cons one (cons two nil) @@ -33,4 +32,25 @@ append (A : U) : list A -> list A -> list A = split reverse (A : U) : list A -> list A = split nil -> nil cons x xs -> append A (reverse A xs) (cons x nil) - \ No newline at end of file + + +Id (A : U) (a0 a1 : A) : U = IdP ( A) a0 a1 + +refl (A : U) (a : A) : Id A a a = a + +mapOnPath (A B : U) (f : A -> B) (a b : A) + (p : Id A a b) : Id B (f a) (f b) = f (p @ ?0) + +funExt (A : U) (B : A -> U) (f g : (x : A) -> B x) + (p : (x : A) -> Id (B x) (f x) (g x)) : + Id ((y : A) -> B y) f g = \(a : A) -> (p a) @ ?0 + +idnat : nat -> nat = split + zero -> zero + suc n -> suc (idnat n) + +test : Id (nat -> nat) idnat (id nat) = funExt nat (\(_ : nat) -> nat) idnat (id nat) rem + where + rem : (n : nat) -> Id nat (idnat n) n = split + zero -> refl nat zero + suc n -> mapOnPath nat nat (\(x : nat) -> suc x) (idnat n) n (rem n) \ No newline at end of file