From: Anders Date: Thu, 26 Mar 2015 15:52:26 +0000 (+0100) Subject: Finish adding HITs X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=da91f4869b11632f7b2b3bb6d7128632b4c3fd62;p=cubicaltt.git Finish adding HITs --- diff --git a/CTT.hs b/CTT.hs index 459afac..caebb10 100644 --- a/CTT.hs +++ b/CTT.hs @@ -60,6 +60,9 @@ labelTeles = map labelTele lookupLabel :: LIdent -> [Label] -> Maybe Tele lookupLabel x xs = lookup x (labelTeles xs) +lookupPLabel :: LIdent -> [Label] -> Maybe (Tele,Ter,Ter) +lookupPLabel x xs = listToMaybe [ (ts,t0,t1) | PLabel y ts t0 t1 <- xs, x == y ] + branchName :: Branch -> LIdent branchName (OBranch c _ _) = c branchName (PBranch c _ _ _) = c @@ -86,9 +89,9 @@ data Ter = App Ter Ter | Snd Ter -- constructor c Ms | Con LIdent [Ter] - | PCon LIdent [Ter] Formula Ter Ter -- c ts phi @ t0 ~ t1 + | PCon LIdent Ter [Ter] Formula -- c A ts phi (A is the data type) -- branches c1 xs1 -> M1,..., cn xsn -> Mn - | Split Loc Ter [Branch] + | Split Ident Loc Ter [Branch] -- labelled sum c1 A1s,..., cn Ans (assumes terms are constructors) | Sum Loc Ident [Label] -- undefined @@ -134,8 +137,7 @@ data Val = VU | VPair Val Val | VCon LIdent [Val] -- The Formula is the direction of the equality in VPCon - | VPCon LIdent [Val] Formula Val Val - + | VPCon LIdent Val [Val] Formula -- Id values | VIdP Val Val Val @@ -222,6 +224,9 @@ data Env = Empty upds :: Env -> [(Ident,Val)] -> Env upds = foldl Upd +updsTele :: Env -> Tele -> [Val] -> Env +updsTele rho tele vs = upds rho (zip (map fst tele) vs) + mapEnv :: (Val -> Val) -> (Formula -> Formula) -> Env -> Env mapEnv f g e = case e of Empty -> Empty @@ -290,14 +295,14 @@ showTer v = case v of Fst e -> showTer e <> text ".1" Snd e -> showTer e <> text ".2" Sigma e0 -> text "Sigma" <+> showTer e0 - Pair e0 e1 -> parens (showTer1 e0 <> comma <> showTer1 e1) + Pair e0 e1 -> parens (showTer e0 <> comma <> showTer e1) Where e d -> showTer e <+> text "where" <+> showDecls d Var x -> text x Con c es -> text c <+> showTers es - PCon c es phi t0 t1 -> text c <+> showTers es <+> showFormula phi <+> - char '@' <+> showTer t0 <+> char '~' <+> showTer t1 - Split l _ _ -> text "split" <+> showLoc l - Sum _ n _ -> text "sum" <+> text n + PCon c a es phi -> text c <+> char '{' <+> showTer a <+> char '}' <+> + showTers es <+> showFormula phi + Split f _ _ _ -> text f + Sum _ n _ -> text n Undef _ -> text "undefined" IdP e0 e1 e2 -> text "IdP" <+> showTers [e0,e1,e2] Path i e -> char '<' <> text (show i) <> char '>' <+> showTer e @@ -336,10 +341,10 @@ showVal v = case v of VU -> char 'U' Ter t env -> showTer t <+> showEnv env VCon c us -> text c <+> showVals us - VPCon c us phi v0 v1 -> text c <+> showVals us <+> showFormula phi <+> - char '@' <+> showVal v0 <+> char '~' <+> showVal v1 + VPCon c a us phi -> text c <+> char '{' <+> showVal a <+> char '}' <+> + showVals us <+> showFormula phi VPi a b -> text "Pi" <+> showVals [a,b] - VPair u v -> parens (showVal1 u <> comma <> showVal1 v) + VPair u v -> parens (showVal u <> comma <> showVal v) VSigma u v -> text "Sigma" <+> showVals [u,v] VApp u v -> showVal u <+> showVal1 v VSplit u v -> showVal u <+> showVal1 v @@ -363,6 +368,7 @@ showVal1 v = case v of VU -> char 'U' VCon c [] -> text c VVar{} -> showVal v + Ter t@Sum{} _ -> showTer t _ -> parens (showVal v) showVals :: [Val] -> Doc diff --git a/Eval.hs b/Eval.hs index c142e96..62f5345 100644 --- a/Eval.hs +++ b/Eval.hs @@ -57,7 +57,7 @@ instance Nominal Val where support (VFst u) = support u support (VSnd u) = support u support (VCon _ vs) = support vs - support (VPCon _ vs phi u v) = support (vs,phi,u,v) + support (VPCon _ a vs phi) = support (a,vs,phi) support (VVar _ v) = support v support (VApp u v) = support (u,v) support (VAppFormula u phi) = support (u,phi) @@ -87,8 +87,7 @@ instance Nominal Val where VFst u -> VFst (acti u) VSnd u -> VSnd (acti u) VCon c vs -> VCon c (acti vs) - VPCon c vs phi u0 u1 -> - pcon c (acti vs) (acti phi) (acti u0) (acti u1) + VPCon c a vs phi -> pcon c (acti a) (acti vs) (acti phi) VVar x v -> VVar x (acti v) VAppFormula u psi -> acti u @@ acti psi VApp u v -> app (acti u) (acti v) @@ -103,19 +102,19 @@ instance Nominal Val where 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) - VTrans u v -> VTrans (sw u) (sw v) - VSigma a f -> VSigma (sw a) (sw f) - VPair u v -> VPair (sw u) (sw v) - VFst u -> VFst (sw u) - VSnd u -> VSnd (sw u) - VCon c vs -> VCon c (sw vs) - VPCon c vs phi u0 u1 -> VPCon c (sw vs) (sw phi) (sw u0) (sw u1) + 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) + VTrans u v -> VTrans (sw u) (sw v) + VSigma a f -> VSigma (sw a) (sw f) + VPair u v -> VPair (sw u) (sw v) + VFst u -> VFst (sw u) + VSnd u -> VSnd (sw u) + VCon c vs -> VCon c (sw vs) + VPCon c a vs phi -> VPCon c (sw a) (sw vs) (sw phi) VVar x v -> VVar x (sw v) VAppFormula u psi -> VAppFormula (sw u) (sw psi) VApp u v -> VApp (sw u) (sw v) @@ -141,8 +140,8 @@ eval rho v = case v of Snd a -> sndVal (eval rho a) Where t decls -> eval (Def decls rho) t Con name ts -> VCon name (map (eval rho) ts) - PCon name ts phi t0 t1 -> pcon name (map (eval rho) ts) (evalFormula rho phi) - (eval rho t0) (eval rho t1) + PCon name a ts phi -> + pcon name (eval rho a) (map (eval rho) ts) (evalFormula rho phi) Split{} -> Ter v rho Sum{} -> Ter v rho Undef l -> error $ "eval: undefined at " ++ show l @@ -181,16 +180,16 @@ evalSystem rho ts = -- TODO: Write using case-of app :: Val -> Val -> Val app (Ter (Lam x _ t) e) u = eval (Upd e (x,u)) t -app (Ter (Split _ _ nvs) e) (VCon c us) = case lookupBranch c nvs of +app (Ter (Split _ _ _ nvs) e) (VCon c us) = case lookupBranch c nvs of Just (OBranch _ xs t) -> eval (upds e (zip xs us)) t _ -> error $ "app: Split with insufficient arguments; " ++ " missing case for " ++ c -app u@(Ter (Split _ _ _) _) v | isNeutral v = VSplit u v -app (Ter (Split _ _ nvs) e) (VPCon c us phi _ _) = case lookupBranch c nvs of +app u@(Ter Split{} _) v | isNeutral v = VSplit u v +app (Ter (Split _ _ _ nvs) e) (VPCon c _ us phi) = case lookupBranch c nvs of Just (PBranch _ xs i t) -> eval (Sub (upds e (zip xs us)) (i,phi)) t _ -> error ("app: Split with insufficient arguments; " ++ " missing case for " ++ c) -app u@(Ter (Split _ f hbr) e) kan@(VComp v w ws) = +app u@(Ter (Split _ _ f hbr) e) kan@(VComp v w ws) = let j = fresh (e,kan) wsj = Map.map (@@ j) ws ws' = mapWithKey (\alpha -> app (u `face` alpha)) wsj @@ -230,7 +229,7 @@ inferType v = case v of VSigma _ f -> app f (VFst t) ty -> error $ "inferType: expected Sigma type for " ++ show v ++ ", got " ++ show ty - VSplit (Ter (Split _ f _) rho) v1 -> app (eval rho f) v1 + VSplit (Ter (Split _ _ f _) rho) v1 -> app (eval rho f) v1 VApp t0 t1 -> case inferType t0 of VPi _ f -> app f t1 ty -> error $ "inferType: expected Pi type for " ++ show v @@ -252,10 +251,13 @@ v @@ phi | isNeutral v = case (inferType v,toFormula phi) of _ -> VAppFormula v (toFormula phi) v @@ phi = error $ "(@@): " ++ show v ++ " should be neutral." -pcon :: LIdent -> [Val] -> Formula -> Val -> Val -> Val -pcon c us (Dir 0) u0 _ = u0 -pcon c us (Dir 1) _ u1 = u1 -pcon c us phi u0 u1 = VPCon c us phi u0 u1 +pcon :: LIdent -> Val -> [Val] -> Formula -> Val +pcon c a@(Ter (Sum _ _ lbls) rho) us phi = case lookupPLabel c lbls of + Just (tele,t0,t1) | phi == Dir 0 -> eval (updsTele rho tele us) t0 + | phi == Dir 1 -> eval (updsTele rho tele us) t1 + | otherwise -> VPCon c a us phi + Nothing -> error "pcon" +-- pcon c a us phi = VPCon c a us phi ----------------------------------------------------------- -- Transport @@ -285,10 +287,9 @@ trans i v0 v1 = case (v0,v1) of (Ter (Sum _ _ nass) env,VCon c us) -> case lookupLabel c nass of Just as -> VCon c $ transps i as env us Nothing -> error $ "trans: missing constructor " ++ c ++ " in " ++ show v0 - (Ter (Sum _ _ nass) env,VPCon c ws0 phi e0 e1) -> case lookupLabel c nass of + (Ter (Sum _ _ nass) env,VPCon c _ ws0 phi) -> case lookupLabel c nass of -- v1 should be independent of i, so i # phi - Just as -> -- the endpoints should be correct because of restrictions on HITs - VPCon c (transps i as env ws0) phi (trans i v0 e0) (trans i v0 e1) + Just as -> VPCon c (v0 `face` (i ~> 1)) (transps i as env ws0) phi Nothing -> error $ "trans: missing path constructor " ++ c ++ " in " ++ show v0 _ | isNeutral v0 || isNeutral v1 -> VTrans (VPath i v0) v1 @@ -674,7 +675,7 @@ instance Convertible Val where (u',Ter (Lam x a u) e) -> let v = mkVar k (eval e a) in conv (k+1) (app u' v) (eval (Upd e (x,v)) u) - (Ter (Split p _ _) e,Ter (Split p' _ _) e') -> (p == p') && conv k e e' + (Ter (Split _ p _ _) e,Ter (Split _ p' _ _) e') -> (p == p') && conv k e e' (Ter (Sum p _ _) e,Ter (Sum p' _ _) e') -> (p == p') && conv k e e' (Ter (Undef p) e,Ter (Undef p') e') -> (p == p') && conv k e e' (VPi u v,VPi u' v') -> diff --git a/Exp.cf b/Exp.cf index 37c62a9..3033a2c 100644 --- a/Exp.cf +++ b/Exp.cf @@ -31,6 +31,7 @@ App. Exp2 ::= Exp2 Exp3 ; Var. Exp3 ::= AIdent ; AppFormula. Exp3 ::= Exp3 "@" Formula ; U. Exp3 ::= "U" ; +PCon. Exp3 ::= AIdent "{" Exp "}" ; -- c{T A B} x1 x2 @ phi Fst. Exp3 ::= Exp3 ".1" ; Snd. Exp3 ::= Exp3 ".2" ; IdP. Exp3 ::= "IdP" ; @@ -62,11 +63,13 @@ Dir. Formula2 ::= Dir ; coercions Formula 2 ; -- Branches -Branch. Branch ::= AIdent [AIdent] "->" ExpWhere ; +OBranch. Branch ::= AIdent [AIdent] "->" ExpWhere ; +PBranch. Branch ::= AIdent [AIdent] "@" AIdent "->" ExpWhere ; separator Branch ";" ; -- Labelled sum alternatives -Label. Label ::= AIdent [Tele] ; +OLabel. Label ::= AIdent [Tele] ; +PLabel. Label ::= AIdent [Tele] "@" Exp "~" Exp ; separator Label "|" ; -- Telescopes diff --git a/Resolver.hs b/Resolver.hs index b11a675..de37567 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -66,7 +66,7 @@ flattenPTele (PTele exp typ : xs) = case appsToIdents exp of ------------------------------------------------------------------------------- -- | Resolver and environment -data SymKind = Variable | Constructor | Name +data SymKind = Variable | Constructor | PConstructor | Name deriving (Eq,Show) -- local environment for constructors @@ -138,6 +138,7 @@ resolveVar (AIdent (l,x)) case lookup x vars of Just Variable -> return $ CTT.Var x Just Constructor -> return $ CTT.Con x [] + Just PConstructor -> undefined -- error! Just Name -> throwError $ "Name " ++ x ++ " used as a variable at position " ++ show l ++ " in module " ++ modName @@ -220,7 +221,13 @@ resolveExp e = case e of (rdecls,names) <- resolveDecls decls CTT.mkWheres rdecls <$> local (insertIdents names) (resolveExp e) Path is e -> paths is (resolveExp e) - AppFormula e phi -> CTT.AppFormula <$> resolveExp e <*> resolveFormula phi + AppFormula e phi -> + let (x,xs) = unApps e [] + in case x of + PCon n a -> CTT.PCon (unAIdent n) <$> resolveExp a + <*> mapM resolveExp xs + <*> resolveFormula phi + _ -> CTT.AppFormula <$> resolveExp e <*> resolveFormula phi _ -> do modName <- asks envModule throwError ("Could not resolve " ++ show e ++ " in module " ++ modName) @@ -254,22 +261,25 @@ resolveFormula (Disj phi psi) = C.orFormula <$> resolveFormula phi <*> resolveFormula psi resolveBranch :: Branch -> Resolver CTT.Branch -resolveBranch (Branch (AIdent (_,lbl)) args e) = do - re <- local (insertAIdents args) $ resolveWhere e - return $ CTT.OBranch lbl (map unAIdent args) re +resolveBranch (OBranch (AIdent (_,lbl)) args e) = do + re <- local (insertAIdents args) $ resolveWhere e + return $ CTT.OBranch lbl (map unAIdent args) re +resolveBranch (PBranch (AIdent (_,lbl)) args i e) = do + re <- local (insertName i . insertAIdents args) $ resolveWhere e + return $ CTT.PBranch lbl (map unAIdent args) (C.Name $ unAIdent i) re resolveTele :: [(Ident,Exp)] -> Resolver CTT.Tele resolveTele [] = return [] resolveTele ((i,d):t) = ((i,) <$> resolveExp d) <:> local (insertVar i) (resolveTele t) -resolveLabel :: Label -> Resolver CTT.Label -- (CTT.LIdent,CTT.Tele) -resolveLabel (Label n vdecl) = +resolveLabel :: [(Ident,SymKind)] -> Label -> Resolver CTT.Label +resolveLabel _ (OLabel n vdecl) = CTT.OLabel (unAIdent n) <$> resolveTele (flattenTele vdecl) - -declsLabels :: [Decl] -> [Ident] -declsLabels decls = map unAIdent [ lbl | Label lbl _ <- sums ] - where sums = concat [ sum | DeclData _ _ sum <- decls ] +resolveLabel cs (PLabel n vdecl t0 t1) = + CTT.PLabel (unAIdent n) <$> resolveTele (flattenTele vdecl) + <*> local (insertIdents cs) (resolveExp t0) + <*> local (insertIdents cs) (resolveExp t1) piToFam :: Exp -> Resolver Ter piToFam (Fun a b) = lam ("_",a) $ resolveExp b @@ -287,11 +297,12 @@ resolveDecl d = case d of return ((f,(a,d)),[(f,Variable)]) DeclData (AIdent (l,f)) tele sums -> do let tele' = flattenTele tele - a <- binds CTT.Pi tele' (return CTT.U) - d <- lams tele' $ local (insertVar f) $ - CTT.Sum <$> getLoc l <*> pure f <*> mapM resolveLabel sums - let cs = map unAIdent [ lbl | Label lbl _ <- sums ] - return ((f,(a,d)),(f,Variable):map (,Constructor) cs) + a <- binds CTT.Pi tele' (return CTT.U) + let cs = [ (unAIdent lbl,Constructor) | OLabel lbl _ <- sums ] + d <- lams tele' $ local (insertVar f) $ + CTT.Sum <$> getLoc l <*> pure f <*> mapM (resolveLabel cs) sums + let pcs = [ (unAIdent lbl,PConstructor) | PLabel lbl _ _ _ <- sums ] + return ((f,(a,d)),(f,Variable):cs ++ pcs) DeclSplit (AIdent (l,f)) tele t brs -> do let tele' = flattenTele tele loc <- getLoc l @@ -299,7 +310,7 @@ resolveDecl d = case d of let vars = map fst tele' fam <- local (insertVars vars) $ piToFam t brs' <- local (insertVars (f:vars)) (mapM resolveBranch brs) - body <- lams tele' (return $ CTT.Split loc fam brs') + body <- lams tele' (return $ CTT.Split f loc fam brs') return ((f,(a,body)),[(f,Variable)]) resolveDecls :: [Decl] -> Resolver ([[CTT.Decl]],[(Ident,SymKind)]) diff --git a/TypeChecker.hs b/TypeChecker.hs index b574a4d..d3d6dac 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -134,7 +134,6 @@ check a t = case (a,t) of (_,Con c es) -> do (bs,nu) <- getLblType c a checks (bs,nu) es - -- TODO: Add PCon (VU,Pi f) -> checkFam f (VU,Sigma f) -> checkFam f (VU,Sum _ _ bs) -> forM_ bs $ \lbl -> case lbl of @@ -145,13 +144,13 @@ check a t = case (a,t) of localM (addTele tele) $ do check (Ter t rho) t0 check (Ter t rho) t1 - (VPi (Ter (Sum _ _ cas) nu) f,Split _ f' ces) -> do + (VPi va@(Ter (Sum _ _ cas) nu) f,Split _ _ f' ces) -> do checkFam f' k <- asks index rho <- asks env unless (conv k f (eval rho f')) $ throwError "check: split annotations" if map labelName cas == map branchName ces - then sequence_ [ checkBranch (lbl,nu) f brc (Ter t rho) + then sequence_ [ checkBranch (lbl,nu) f brc (Ter t rho) va | (brc, lbl) <- zip ces cas ] else throwError "case branches does not match the data type" (VPi a f,Lam x a' t) -> do @@ -256,12 +255,12 @@ mkSection _ vb vf vg = where [b,y,f,g] = map Var ["b","y","f","g"] rho = Upd (Upd (Upd Empty ("b",vb)) ("f",vf)) ("g",vg) -checkBranch :: (Label,Env) -> Val -> Branch -> Val -> Typing () -checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ = do +checkBranch :: (Label,Env) -> Val -> Branch -> Val -> Val -> Typing () +checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ _ = do k <- asks index let us = map snd $ mkVars k tele nu local (addBranch (zip ns us) (tele,nu)) $ check (app f (VCon c us)) e -checkBranch (PLabel _ tele t0 t1,nu) f (PBranch c ns i e) g = do +checkBranch (PLabel _ tele t0 t1,nu) f (PBranch c ns i e) g va = do k <- asks index let us = mkVars k tele nu vus = map snd us @@ -270,7 +269,7 @@ checkBranch (PLabel _ tele t0 t1,nu) f (PBranch c ns i e) g = do checkFresh i local (addBranch (zip ns vus) (tele,nu)) $ do local (addSub (i,Atom i)) - (check (app f (VPCon c vus (Atom i) vt0 vt1)) e) + (check (app f (VPCon c va vus (Atom i))) e) rho <- asks env k' <- asks index unless (conv k' (eval (Sub rho (i,Dir 0)) e) (app g vt0) && @@ -368,6 +367,14 @@ infer e = case e of let ves = evalSystem rho es check (compLine VU va ves) u return va + PCon c a es phi -> do + check VU a + rho <- asks env + let va = eval rho a + (bs,nu) <- getLblType c va + checks (bs,nu) es + checkFormula phi + return va _ -> throwError ("infer " ++ show e) -- Return system us such that: