From 6eff2ccd0a78b2410aee14454808abd59500923a Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Sat, 18 Apr 2015 04:08:53 +0200 Subject: [PATCH] wip (not working yet) --- CTT.hs | 31 +++++++++++++++++------------ Connections.hs | 8 ++++---- Eval.hs | 52 ++++++++++++++++++++++++++---------------------- Exp.cf | 5 +++-- Resolver.hs | 33 ++++++++++++++++++++---------- TypeChecker.hs | 54 ++++++++++++++++++++++++++++++-------------------- 6 files changed, 109 insertions(+), 74 deletions(-) diff --git a/CTT.hs b/CTT.hs index e764036..0661d69 100644 --- a/CTT.hs +++ b/CTT.hs @@ -23,13 +23,13 @@ type LIdent = String type Tele = [(Ident,Ter)] data Label = OLabel LIdent Tele -- Object label - | PLabel LIdent Tele Ter Ter -- Path label + | PLabel LIdent Tele [Name] (System Ter) -- Path label deriving (Eq,Show) -- OBranch of the form: c x1 .. xn -> e --- PBranch of the form: c x1 .. xn i -> e +-- PBranch of the form: c x1 .. xn i1 .. im -> e data Branch = OBranch LIdent [Ident] Ter - | PBranch LIdent [Ident] Name Ter + | PBranch LIdent [Ident] [Name] Ter deriving (Eq,Show) -- Declarations: x : A = e @@ -60,8 +60,8 @@ 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 ] +lookupPLabel :: LIdent -> [Label] -> Maybe (Tele,[Name],System Ter) +lookupPLabel x xs = listToMaybe [ (ts,is,es) | PLabel y ts is es <- xs, x == y ] branchName :: Branch -> LIdent branchName (OBranch c _ _) = c @@ -89,7 +89,7 @@ data Ter = App Ter Ter | Snd Ter -- constructor c Ms | Con LIdent [Ter] - | PCon LIdent Ter [Ter] Formula -- c A ts phi (A is the data type) + | PCon LIdent Ter [Ter] [Formula] -- c A ts phis (A is the data type) -- branches c1 xs1 -> M1,..., cn xsn -> Mn | Split Ident Loc Ter [Branch] -- labelled sum c1 A1s,..., cn Ans (assumes terms are constructors) @@ -138,8 +138,7 @@ data Val = VU | VSigma Val Val | VPair Val Val | VCon LIdent [Val] - -- The Formula is the direction of the equality in VPCon - | VPCon LIdent Val [Val] Formula + | VPCon LIdent Val [Val] [Formula] -- Id values | VIdP Val Val Val @@ -237,6 +236,9 @@ upds = foldl Upd updsTele :: Env -> Tele -> [Val] -> Env updsTele rho tele vs = upds rho (zip (map fst tele) vs) +subs :: Env -> [(Name,Formula)] -> Env +subs = foldl Sub + mapEnv :: (Val -> Val) -> (Formula -> Formula) -> Env -> Env mapEnv f g e = case e of Empty -> Empty @@ -325,8 +327,9 @@ showTer v = case v of Where e d -> showTer e <+> text "where" <+> showDecls d Var x -> text x Con c es -> text c <+> showTers es - PCon c a es phi -> text c <+> char '{' <+> showTer a <+> char '}' <+> - showTers es <+> showFormula phi + PCon c a es phis -> text c <+> char '{' <+> showTer a <+> char '}' + <+> showTers es + <+> (hsep $ punctuate (char '@') (map showFormula phis)) Split f _ _ _ -> text f Sum _ n _ -> text n Undef{} -> text "undefined" @@ -372,9 +375,11 @@ showVal v = case v of Ter t@Split{} rho -> showTer t <+> showEnv False rho Ter t env -> showTer1 t <+> showEnv True env VCon c us -> text c <+> showVals us - VPCon c a us phi -> text c <+> char '{' <+> showVal a <+> char '}' <+> - showVals us <+> showFormula phi - VPi a l@(VLam x t b) | "_" `isPrefixOf` x -> showVal1 a <+> text "->" <+> showVal1 b + VPCon c a us phis -> text c <+> char '{' <+> showVal a <+> char '}' + <+> showVals us + <+> (hsep $ punctuate (char '@') (map showFormula phis)) + VPi a l@(VLam x t b) | "_" `isPrefixOf` x -> showVal1 a <+> text "->" + <+> showVal1 b | otherwise -> showVal l VPi a b -> text "Pi" <+> showVals [a,b] VPair u v -> parens (showVal u <> comma <> showVal v) diff --git a/Connections.hs b/Connections.hs index fe2c10b..ba1234a 100644 --- a/Connections.hs +++ b/Connections.hs @@ -4,7 +4,7 @@ module Connections where import Control.Applicative import Data.List -import Data.Map (Map,(!)) +import Data.Map (Map,(!),keys) import Data.Set (Set) import qualified Data.Map as Map import qualified Data.Set as Set @@ -375,9 +375,6 @@ mkSystem = flip insertsSystem Map.empty unionSystem :: System a -> System a -> System a unionSystem us vs = insertsSystem (Map.assocs us) vs --- could something like that work?? --- transposeSystem :: System [a] -> [System a] --- transposeSystem as = Map.tranverseWithKey (const . id) as -- TODO: add some checks transposeSystemAndList :: System [a] -> [b] -> [(System a,b)] @@ -445,3 +442,6 @@ 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 + +domain :: System a -> [Name] +domain = keys . Map.unions . keys diff --git a/Eval.hs b/Eval.hs index c2035a0..9675865 100644 --- a/Eval.hs +++ b/Eval.hs @@ -59,7 +59,7 @@ instance Nominal Val where VFst u -> support u VSnd u -> support u VCon _ vs -> support vs - VPCon _ a vs phi -> support (a,vs,phi) + VPCon _ a vs phis -> support (a,vs,phis) VVar _ v -> support v VApp u v -> support (u,v) VLam _ u v -> support (u,v) @@ -90,7 +90,7 @@ instance Nominal Val where VFst u -> fstVal (acti u) VSnd u -> sndVal (acti u) VCon c vs -> VCon c (acti vs) - VPCon c a vs phi -> pcon c (acti a) (acti vs) (acti phi) + VPCon c a vs phis -> pcon c (acti a) (acti vs) (acti phis) VVar x v -> VVar x (acti v) VAppFormula u psi -> acti u @@ acti psi VApp u v -> app (acti u) (acti v) @@ -118,7 +118,7 @@ instance Nominal Val where 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) + VPCon c a vs phis -> VPCon c (sw a) (sw vs) (sw phis) VVar x v -> VVar x (sw v) VAppFormula u psi -> VAppFormula (sw u) (sw psi) VApp u v -> VApp (sw u) (sw v) @@ -144,8 +144,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 a ts phi -> - pcon name (eval rho a) (map (eval rho) ts) (evalFormula rho phi) + PCon name a ts phis -> + pcon name (eval rho a) (map (eval rho) ts) (map (evalFormula rho) phis) Lam{} -> Ter v rho Split{} -> Ter v rho Sum{} -> Ter v rho @@ -190,8 +190,8 @@ app u v = case (u,v) of (Ter (Split _ _ _ nvs) e,VCon c vs) -> case lookupBranch c nvs of Just (OBranch _ xs t) -> eval (upds e (zip xs vs)) t _ -> error $ "app: missing case in split for " ++ c - (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 + (Ter (Split _ _ _ nvs) e,VPCon c _ us phis) -> case lookupBranch c nvs of + Just (PBranch _ xs is t) -> eval (subs (upds e (zip xs us)) (zip is phis)) t _ -> error $ "app: missing case in split for " ++ c (Ter Split{} _,_) | isNeutral v -> VSplit u v (Ter Split{} _,VCompElem _ _ w _) -> app u w @@ -267,11 +267,13 @@ v @@ phi | isNeutral v = case (inferType v,toFormula phi) of (VElimComp _ _ u) @@ phi = u @@ phi v @@ phi = error $ "(@@): " ++ show v ++ " should be neutral." -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 +pcon :: LIdent -> Val -> [Val] -> [Formula] -> Val +pcon c a@(Ter (Sum _ _ lbls) rho) us phis = case lookupPLabel c lbls of + -- TODO: is this correct? Double check! + Just (tele,is,ts) | eps `Map.member` vs -> vs ! eps + | otherwise -> VPCon c a us phis + where rho' = subs (updsTele rho tele us) (zip is phis) + vs = evalSystem rho' ts Nothing -> error "pcon" -- pcon c a us phi = VPCon c a us phi @@ -303,9 +305,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) -> case lookupLabel c nass of + (Ter (Sum _ _ nass) env,VPCon c _ ws0 phis) -> case lookupLabel c nass of -- v1 should be independent of i, so i # phi - Just as -> VPCon c (v0 `face` (i ~> 1)) (transps i as env ws0) phi + Just as -> VPCon c (v0 `face` (i ~> 1)) (transps i as env ws0) phis Nothing -> error $ "trans: missing path constructor " ++ c ++ " in " ++ show v0 _ | isNeutral w -> w @@ -709,19 +711,21 @@ instance Convertible Val where let w = mkVar k "X" u in conv k u u' && conv (k+1) (app v w) (app v' w) (VCon c us,VCon c' us') -> (c == c') && conv k us us' - (VPair u v,VPair u' v') -> conv k u u' && conv k v v' - (VPair u v,w) -> conv k u (fstVal w) && conv k v (sndVal w) - (w,VPair u v) -> conv k (fstVal w) u && conv k (sndVal w) v - (VFst u,VFst u') -> conv k u u' - (VSnd u,VSnd u') -> conv k u u' - (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' + (VPCon c v us phis,VPCon c' v' us' phis') -> + (c == c') && conv k (v,us,phis) (v',us',phis') + (VPair u v,VPair u' v') -> conv k u u' && conv k v v' + (VPair u v,w) -> conv k u (fstVal w) && conv k v (sndVal w) + (w,VPair u v) -> conv k (fstVal w) u && conv k (sndVal w) v + (VFst u,VFst u') -> conv k u u' + (VSnd u,VSnd u') -> conv k u u' + (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)) - (VTrans p u,VTrans p' u') -> conv k p p' && conv k u u' + (VTrans p u,VTrans p' u') -> conv k p p' && conv k u u' (VAppFormula u x,VAppFormula u' x') -> conv k (u,x) (u',x') (VComp a u ts,VComp a' u' ts') -> conv k (a,u,ts) (a',u',ts') (VGlue v hisos,VGlue v' hisos') -> conv k (v,hisos) (v',hisos') @@ -794,7 +798,7 @@ instance Normal Val where VSigma u v -> VSigma (normal k u) (normal k v) VPair u v -> VPair (normal k u) (normal k v) VCon n us -> VCon n (normal k us) - VPCon n u us phi -> VPCon n (normal k u) (normal k us) phi + VPCon n u us phis -> VPCon n (normal k u) (normal k us) phis VIdP a u0 u1 -> VIdP (normal k a) (normal k u0) (normal k u1) VPath i u -> VPath i (normal k u) VComp u v vs -> compLine (normal k u) (normal k v) (normal k vs) diff --git a/Exp.cf b/Exp.cf index b84064e..a22f225 100644 --- a/Exp.cf +++ b/Exp.cf @@ -67,12 +67,13 @@ coercions Formula 2 ; -- Branches OBranch. Branch ::= AIdent [AIdent] "->" ExpWhere ; -PBranch. Branch ::= AIdent [AIdent] "@" AIdent "->" ExpWhere ; +-- TODO: better have ... @ i @ j @ k -> ... ? +PBranch. Branch ::= AIdent [AIdent] "@" [AIdent] "->" ExpWhere ; separator Branch ";" ; -- Labelled sum alternatives OLabel. Label ::= AIdent [Tele] ; -PLabel. Label ::= AIdent [Tele] "@" Exp "~" Exp ; +PLabel. Label ::= AIdent [Tele] "<" [AIdent] ">" "@" System ; separator Label "|" ; -- Telescopes diff --git a/Resolver.hs b/Resolver.hs index 8e4e9c7..fd6b97e 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -45,6 +45,14 @@ unApps u ws = (u, ws) appsToIdents :: Exp -> Maybe [Ident] appsToIdents = mapM unVar . uncurry (:) . flip unApps [] +-- Transform a sequence of applications +-- (((u v1) .. vn) phi1) .. phim into (u,[v1,..,vn],[phi1,..,phim]) +unAppsFormulas :: Exp -> [Exp] -> [Formula]-> (Exp,[Exp],[Formula]) +unAppsFormulas (AppFormula u phi) ws phis = unAppsFormulas u ws (phi:phis) +unAppsFormulas u ws phis = (x,xs++ws,phis) + where (x,xs) = unApps u ws + + -- Flatten a tele flattenTele :: [Tele] -> [(Ident,Exp)] flattenTele tele = @@ -92,6 +100,9 @@ insertIdents = flip $ foldr insertIdent insertName :: AIdent -> Env -> Env insertName (AIdent (_,x)) = insertIdent (x,Name) +insertNames :: [AIdent] -> Env -> Env +insertNames = flip $ foldr insertName + insertVar :: Ident -> Env -> Env insertVar x = insertIdent (x,Variable) @@ -186,11 +197,11 @@ resolveExp e = case e of Path is e -> paths is (resolveExp e) Hole (HoleIdent (l,_)) -> CTT.Hole <$> getLoc l AppFormula e phi -> - let (x,xs) = unApps e [] + let (x,xs,phis) = unAppsFormulas e [] [] in case x of PCon n a -> CTT.PCon (unAIdent n) <$> resolveExp a <*> mapM resolveExp xs - <*> resolveFormula phi + <*> mapM resolveFormula phis _ -> CTT.AppFormula <$> resolveExp e <*> resolveFormula phi Trans x y -> CTT.Trans <$> resolveExp x <*> resolveExp y IdP x y z -> CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z @@ -241,9 +252,10 @@ resolveBranch :: Branch -> Resolver CTT.Branch 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 +resolveBranch (PBranch (AIdent (_,lbl)) args is e) = do + re <- local (insertNames is . insertAIdents args) $ resolveWhere e + names <- mapM resolveName is + return $ CTT.PBranch lbl (map unAIdent args) names re resolveTele :: [(Ident,Exp)] -> Resolver CTT.Tele resolveTele [] = return [] @@ -253,12 +265,13 @@ resolveTele ((i,d):t) = resolveLabel :: [(Ident,SymKind)] -> Label -> Resolver CTT.Label resolveLabel _ (OLabel n vdecl) = CTT.OLabel (unAIdent n) <$> resolveTele (flattenTele vdecl) -resolveLabel cs (PLabel n vdecl t0 t1) = do +resolveLabel cs (PLabel n vdecl is sys) = do let tele' = flattenTele vdecl - ts = map fst tele' - CTT.PLabel (unAIdent n) <$> resolveTele tele' - <*> local (insertIdents cs . insertVars ts) (resolveExp t0) - <*> local (insertIdents cs . insertVars ts) (resolveExp t1) + ts = map fst tele' + names = map (C.Name . unAIdent) is + CTT.PLabel (unAIdent n) <$> resolveTele tele' <*> pure names + <*> local (insertNames is . insertIdents cs . insertVars ts) + (resolveSystem sys) -- Resolve Data or Def or Split declarations resolveDecl :: Decl -> Resolver (CTT.Decl,[(Ident,SymKind)]) diff --git a/TypeChecker.hs b/TypeChecker.hs index 89235b5..dc5fb86 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -68,6 +68,9 @@ addTypeVal (x,a) (TEnv k ind rho v) = addSub :: (Name,Formula) -> TEnv -> TEnv addSub iphi (TEnv k ind rho v) = TEnv k ind (Sub rho iphi) v +addSubs :: [(Name,Formula)] -> TEnv -> TEnv +addSubs = flip $ foldr addSub + addType :: (Ident,Ter) -> TEnv -> Typing TEnv addType (x,a) tenv@(TEnv _ _ rho _) = return $ addTypeVal (x,eval rho a) tenv @@ -129,7 +132,7 @@ mkSection vb vf vg = rho = Upd (Upd (Upd Empty ("b",vb)) ("f",vf)) ("g",vg) -- Test if two values are convertible -(===) :: Val -> Val -> Typing Bool +(===) :: Convertible a => a -> a -> Typing Bool u === v = conv <$> asks index <*> pure u <*> pure v -- eval in the typing monad @@ -156,12 +159,20 @@ check a t = case (a,t) of (VU,Sigma f) -> checkFam f (VU,Sum _ _ bs) -> forM_ bs $ \lbl -> case lbl of OLabel _ tele -> checkTele tele - PLabel _ tele t0 t1 -> do + PLabel _ tele is ts -> do checkTele tele rho <- asks env - localM (addTele tele) $ do - check (Ter t rho) t0 - check (Ter t rho) t1 + unless (all (`elem` is) (domain ts)) $ + throwError $ "names in path label system" -- TODO + mapM_ checkFresh is + let iis = zip is (map Atom is) + local (addSubs iis) $ localM (addTele tele) $ do + checkSystemWith ts $ \alpha talpha -> + local (faceEnv alpha) $ do + rhoAlpha <- asks env + check (Ter t rhoAlpha) talpha + rho' <- asks env + checkCompSystem (evalSystem rho' ts) (VPi va@(Ter (Sum _ _ cas) nu) f,Split _ _ ty ces) -> do check VU ty rho <- asks env @@ -292,21 +303,21 @@ 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 va = do +checkBranch (PLabel _ tele is ts,nu) f (PBranch c ns js e) g va = do k <- asks index - let us = mkVars k tele nu - vus = map snd us - vt0 = eval (upds nu us) t0 - vt1 = eval (upds nu us) t1 - checkFresh i + mapM_ checkFresh is + let us = mkVars k tele nu + vus = map snd us + is' = map Atom is + vts = evalSystem (upds nu us) ts + vfts = intersectionWith app (border f ts) vts local (addBranch (zip ns vus) (tele,nu)) $ do - local (addSub (i,Atom i)) $ - check (app f (VPCon c va vus (Atom i))) e + local (addSubs (zip is is')) $ + check (app f (VPCon c va vus is')) e rho <- asks env - k' <- asks index - unless (conv k' (eval (Sub rho (i,Dir 0)) e) (app g vt0) && - conv k' (eval (Sub rho (i,Dir 1)) e) (app g vt1)) $ - throwError "Endpoints of branch don't match" + ve <- evalTyping e -- TODO: combine with next? + unlessM (border ve ts === vfts) $ + throwError $ "Faces of branch don't match" checkFormula :: Formula -> Typing () checkFormula phi = do @@ -428,12 +439,13 @@ infer e = case e of let ves = evalSystem rho es check (compLine VU va ves) u return va - PCon c a es phi -> do + PCon c a es phis -> do check VU a va <- evalTyping a - (bs,nu) <- getLblType c va - checks (bs,nu) es - checkFormula phi +-- (bs,nu) <- getLblType c va +-- checks (bs,nu) es +-- mapM_ checkFormula phis + trace $ "va = " ++ show va return va _ -> throwError ("infer " ++ show e) -- 2.34.1