From 3a1e275825ff61e0a3efe2e5197340d25110612a Mon Sep 17 00:00:00 2001 From: Anders Date: Wed, 25 Mar 2015 19:06:44 +0100 Subject: [PATCH] Add HITs (parsing and resolver missing) --- CTT.hs | 62 +++++++++++++++++++++++++++++++++++++------- Eval.hs | 62 ++++++++++++++++++++++++++++++++++++-------- Resolver.hs | 9 ++++--- TypeChecker.hs | 59 +++++++++++++++++++++++++++++------------ examples/bool.ctt | 11 +++++--- examples/nat.ctt | 2 ++ examples/prelude.ctt | 1 - 7 files changed, 160 insertions(+), 46 deletions(-) diff --git a/CTT.hs b/CTT.hs index d713c18..459afac 100644 --- a/CTT.hs +++ b/CTT.hs @@ -17,16 +17,20 @@ data Loc = Loc { locFile :: String deriving Eq type Ident = String -type Label = String - --- Branch of the form: c x1 .. xn -> e -type Branch = (Label,([Ident],Ter)) +type LIdent = String -- Telescope (x1 : A1) .. (xn : An) type Tele = [(Ident,Ter)] --- Labelled sum: c (x1 : A1) .. (xn : An) -type LblSum = [(Ident,Tele)] +data Label = OLabel LIdent Tele -- Object label + | PLabel LIdent Tele Ter Ter -- Path label + deriving (Eq,Show) + +-- OBranch of the form: c x1 .. xn -> e +-- PBranch of the form: c x1 .. xn i -> e +data Branch = OBranch LIdent [Ident] Ter + | PBranch LIdent [Ident] Name Ter + deriving (Eq,Show) -- Declarations: x : A = e type Decl = (Ident,(Ter,Ter)) @@ -43,6 +47,31 @@ declTele decls = [ (x,t) | (x,(t,_)) <- decls ] declDefs :: [Decl] -> [(Ident,Ter)] declDefs decls = [ (x,d) | (x,(_,d)) <- decls ] +labelTele :: Label -> (LIdent,Tele) +labelTele (OLabel c ts) = (c,ts) +labelTele (PLabel c ts _ _) = (c,ts) + +labelName :: Label -> LIdent +labelName = fst . labelTele + +labelTeles :: [Label] -> [(LIdent,Tele)] +labelTeles = map labelTele + +lookupLabel :: LIdent -> [Label] -> Maybe Tele +lookupLabel x xs = lookup x (labelTeles xs) + +branchName :: Branch -> LIdent +branchName (OBranch c _ _) = c +branchName (PBranch c _ _ _) = c + +lookupBranch :: LIdent -> [Branch] -> Maybe Branch +lookupBranch _ [] = Nothing +lookupBranch x (b:brs) = case b of + OBranch c _ _ | x == c -> Just b + | otherwise -> lookupBranch x brs + PBranch c _ _ _ | x == c -> Just b + | otherwise -> lookupBranch x brs + -- Terms data Ter = App Ter Ter | Pi Ter @@ -56,11 +85,12 @@ data Ter = App Ter Ter | Fst Ter | Snd Ter -- constructor c Ms - | Con Label [Ter] + | Con LIdent [Ter] + | PCon LIdent [Ter] Formula Ter Ter -- c ts phi @ t0 ~ t1 -- branches c1 xs1 -> M1,..., cn xsn -> Mn | Split Loc Ter [Branch] -- labelled sum c1 A1s,..., cn Ans (assumes terms are constructors) - | Sum Loc Ident LblSum + | Sum Loc Ident [Label] -- undefined | Undef Loc @@ -102,7 +132,10 @@ data Val = VU | VPi Val Val | VSigma Val Val | VPair Val Val - | VCon Label [Val] + | VCon LIdent [Val] + -- The Formula is the direction of the equality in VPCon + | VPCon LIdent [Val] Formula Val Val + -- Id values | VIdP Val Val Val @@ -173,6 +206,10 @@ unCon (VCon _ vs) = vs -- unCon (KanUElem _ u) = unCon u unCon v = error $ "unCon: not a constructor: " ++ show v +isCon :: Val -> Bool +isCon VCon{} = True +isCon _ = False + -------------------------------------------------------------------------------- -- | Environments @@ -257,6 +294,8 @@ 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 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 Undef _ -> text "undefined" @@ -292,11 +331,13 @@ showDecls defs = hsep $ punctuate comma instance Show Val where show = render . showVal -showVal, showVal1 :: Val -> Doc +showVal :: Val -> Doc 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 VPi a b -> text "Pi" <+> showVals [a,b] VPair u v -> parens (showVal1 u <> comma <> showVal1 v) VSigma u v -> text "Sigma" <+> showVals [u,v] @@ -317,6 +358,7 @@ showVal v = case v of VElimComp a es t -> text "elimComp" <+> showVal1 a <+> text (showSystem es) <+> showVal1 t +showVal1 :: Val -> Doc showVal1 v = case v of VU -> char 'U' VCon c [] -> text c diff --git a/Eval.hs b/Eval.hs index 43bdeaa..2e704bb 100644 --- a/Eval.hs +++ b/Eval.hs @@ -57,6 +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 (VVar _ v) = support v support (VApp u v) = support (u,v) support (VAppFormula u phi) = support (u,phi) @@ -86,6 +87,8 @@ 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) VVar x v -> VVar x (acti v) VAppFormula u psi -> acti u @@ acti psi VApp u v -> app (acti u) (acti v) @@ -112,6 +115,7 @@ instance Nominal Val where 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) VVar x v -> VVar x (sw v) VAppFormula u psi -> VAppFormula (sw u) (sw psi) VApp u v -> VApp (sw u) (sw v) @@ -137,6 +141,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) Split{} -> Ter v rho Sum{} -> Ter v rho Undef l -> error $ "eval: undefined at " ++ show l @@ -175,11 +181,23 @@ 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 name us) = case lookup name nvs of - Just (xs,t) -> eval (upds e (zip xs us)) t - Nothing -> error $ "app: Split with insufficient arguments; " ++ - " missing case for " ++ name +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 + 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) = + let j = fresh (e,kan) + wsj = Map.map (@@ j) ws + ws' = mapWithKey (\alpha -> app (u `face` alpha)) wsj + w' = app u w + ffill = app (eval e f) (fill j v w wsj) + in genComp j ffill w' ws' + app kan@(VTrans (VPath i (VPi a f)) li0) ui1 = let j = fresh (kan,ui1) (aj,fj) = (a,f) `swap` (i,j) @@ -221,6 +239,8 @@ inferType v = case v of VIdP a _ _ -> a @@ phi ty -> error $ "inferType: expected IdP type for " ++ show v ++ ", got " ++ show ty + VComp a _ _ -> a + VTrans a _ -> a @@ One _ -> error $ "inferType: not neutral " ++ show v (@@) :: ToFormula a => Val -> a -> Val @@ -232,6 +252,11 @@ 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 + ----------------------------------------------------------- -- Transport @@ -257,10 +282,22 @@ trans i v0 v1 = case (v0,v1) of comp_u2 = trans i (app f fill_u1) u2 in VPair ui1 comp_u2 (VPi{},_) -> VTrans (VPath i v0) v1 - (Ter (Sum _ _ nass) env,VCon n us) -> case lookup n nass of - Just as -> VCon n $ transps i as env us - Nothing -> error $ "comp: missing constructor in labelled sum " ++ n ++ " v0 = " ++ show v0 + (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 + -- 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) + Nothing -> error $ "trans: missing path constructor " ++ c ++ + " in " ++ show v0 _ | isNeutral v0 || isNeutral v1 -> VTrans (VPath i v0) v1 + (Ter (Sum _ _ nass) env,VComp b w ws) -> comp k v01 (trans i v0 w) ws' + where v01 = v0 `face` (i ~> 1) -- b is vi0 and independent of j + k = fresh (v0,v1,Atom i) + transp alpha w = trans i (v0 `face` alpha) (w @@ k) + ws' = mapWithKey transp ws + (VGlue a ts,_) -> transGlue i a ts v1 (VComp VU a es,_) -> transU i a es v1 _ | otherwise -> error $ "trans not implemented for v0 = " ++ show v0 @@ -404,13 +441,16 @@ comp i a u ts = let j = fresh (Atom i,a,u,ts) -- maybe only in vid?? VGlue b hisos -> compGlue i b hisos u ts VComp VU a es -> compU i a es u ts Ter (Sum _ _ nass) env -> case u of - VCon n us -> case lookup n nass of - Just as -> VCon n $ comps i as env tsus - where tsus = transposeSystemAndList (Map.map unCon ts) us + VCon n us -> case lookupLabel n nass of + Just as -> + if all isCon (elems ts) + then let tsus = transposeSystemAndList (Map.map unCon ts) us + in VCon n $ comps i as env tsus + else VComp a u (Map.map (VPath i) ts) Nothing -> error $ "comp: missing constructor in labelled sum " ++ n + VPCon{} -> VComp a u (Map.map (VPath i) ts) _ -> error "comp ter sum" - compNeg :: Name -> Val -> Val -> System Val -> Val compNeg i a u ts = comp i a u (ts `sym` i) diff --git a/Resolver.hs b/Resolver.hs index 3c36ef3..b11a675 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -253,18 +253,19 @@ resolveFormula (Conj phi psi) = C.andFormula <$> resolveFormula phi resolveFormula (Disj phi psi) = C.orFormula <$> resolveFormula phi <*> resolveFormula psi -resolveBranch :: Branch -> Resolver (CTT.Label,([CTT.Label],Ter)) +resolveBranch :: Branch -> Resolver CTT.Branch resolveBranch (Branch (AIdent (_,lbl)) args e) = do re <- local (insertAIdents args) $ resolveWhere e - return (lbl, (map unAIdent args, re)) + return $ CTT.OBranch lbl (map unAIdent args) 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.Tele) -resolveLabel (Label n vdecl) = (unAIdent n,) <$> resolveTele (flattenTele vdecl) +resolveLabel :: Label -> Resolver CTT.Label -- (CTT.LIdent,CTT.Tele) +resolveLabel (Label n vdecl) = + CTT.OLabel (unAIdent n) <$> resolveTele (flattenTele vdecl) declsLabels :: [Decl] -> [Ident] declsLabels decls = map unAIdent [ lbl | Label lbl _ <- sums ] diff --git a/TypeChecker.hs b/TypeChecker.hs index 7d247ea..b574a4d 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -86,7 +86,7 @@ runInfer lenv e = runTyping lenv (infer e) -- Extract the type of a label as a closure getLblType :: String -> Val -> Typing (Tele, Env) -getLblType c (Ter (Sum _ _ cas) r) = case lookup c cas of +getLblType c (Ter (Sum _ _ cas) r) = case lookupLabel c cas of Just as -> return (as,r) Nothing -> throwError ("getLblType: " ++ show c) getLblType c u = throwError ("expected a data type for the constructor " @@ -134,19 +134,25 @@ 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) -> sequence_ [checkTele as | (_,as) <- bs] + (VU,Sum _ _ bs) -> forM_ bs $ \lbl -> case lbl of + OLabel _ tele -> checkTele tele + PLabel n tele t0 t1 -> do + checkTele tele + rho <- asks env + localM (addTele tele) $ do + check (Ter t rho) t0 + check (Ter t rho) t1 (VPi (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" - let cas' = sortBy (compare `on` fst) cas - ces' = sortBy (compare `on` fst) ces - if map fst cas' == map fst ces' - then sequence_ [ checkBranch (as,nu) f brc - | (brc, (_,as)) <- zip ces' cas' ] + if map labelName cas == map branchName ces + then sequence_ [ checkBranch (lbl,nu) f brc (Ter t rho) + | (brc, lbl) <- zip ces cas ] else throwError "case branches does not match the data type" (VPi a f,Lam x a' t) -> do check VU a' @@ -250,17 +256,32 @@ 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 :: (Tele,Env) -> Val -> Branch -> Typing () -checkBranch (xas,nu) f (c,(xs,e)) = do - k <- asks index - env <- asks env - let us = mkVars k xas nu - local (addBranch (zip xs us) (xas,nu)) $ check (app f (VCon c us)) e +checkBranch :: (Label,Env) -> Val -> Branch -> 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 + 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 + local (addBranch (zip ns vus) (tele,nu)) $ do + local (addSub (i,Atom i)) + (check (app f (VPCon c vus (Atom i) vt0 vt1)) 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" +mkVars :: Int -> Tele -> Env -> [(Ident,Val)] mkVars k [] _ = [] mkVars k ((x,a):xas) nu = let w = mkVar k (eval nu a) - in w : mkVars (k+1) xas (Upd nu (x,w)) + in (x,w) : mkVars (k+1) xas (Upd nu (x,w)) checkFormula :: Formula -> Typing () checkFormula phi = do @@ -389,12 +410,18 @@ checkPathSystem t0 va ps = do --inferCompElem :: Ter -> System Ter +checkFresh :: Name -> Typing () +checkFresh i = do + rho <- asks env + when (i `elem` support rho) + (throwError $ show i ++ " is already declared") + + -- Check that a term is a path and output the source and target checkPath :: Val -> Ter -> Typing (Val,Val) checkPath v (Path i a) = do rho <- asks env - when (i `elem` support rho) - (throwError $ show i ++ " is already declared") + checkFresh i local (addSub (i,Atom i)) $ check (v @@ i) a return (eval (Sub rho (i,Dir 0)) a,eval (Sub rho (i,Dir 1)) a) checkPath v t = do diff --git a/examples/bool.ctt b/examples/bool.ctt index 7fe411e..12469e2 100644 --- a/examples/bool.ctt +++ b/examples/bool.ctt @@ -3,15 +3,15 @@ module bool where import prelude import nat -data bool = true | false +data bool = false | true neg : bool -> bool = split - true -> false false -> true + true -> false negK : (b : bool) -> Id bool (neg (neg b)) b = split - true -> refl bool true false -> refl bool false + true -> refl bool true negEq : Id U bool bool = glue bool [ (i = 0) -> (bool,neg,neg,negK,negK) ] @@ -91,4 +91,7 @@ test8 : Id U F2 F2 = subst U (\(X:U) -> Id U X X) bool F2 boolEqF2 (refl U bool) test9 : Id U F2 F2 = - transport ( Id U (boolEqF2 @ i) (boolEqF2 @ i)) (refl U bool) \ No newline at end of file + transport ( Id U (boolEqF2 @ i) (boolEqF2 @ i)) (refl U bool) + +p : Id U F2 bool = comp U bool [ (i = 0) -> boolEqF2 ] +q : Id U F2 F2 = p @ (i /\ - i) \ No newline at end of file diff --git a/examples/nat.ctt b/examples/nat.ctt index 19c20fe..8733fe7 100644 --- a/examples/nat.ctt +++ b/examples/nat.ctt @@ -1,5 +1,7 @@ module nat where +import prelude + data nat = zero | suc (n : nat) zero' : nat = zero diff --git a/examples/prelude.ctt b/examples/prelude.ctt index b3818a7..51c1594 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -41,7 +41,6 @@ isoId (A B : U) (f : A -> B) (g : B -> A) (t : (x:A) -> Id A (g (f x)) x) : Id U A B = glue B [ (i = 0) -> (A,f,g,s,t) ] - -- u -- a0 ----- a1 -- | | -- 2.34.1