diff --git a/misc/dex.el b/misc/dex.el index a5dfa2509..bc56b2934 100644 --- a/misc/dex.el +++ b/misc/dex.el @@ -5,12 +5,18 @@ ;; https://developers.google.com/open-source/licenses/bsd (setq dex-highlights - '(("--\\([^o].*$\\|$\\)" . font-lock-comment-face) + `(("--\\([^o].*$\\|$\\)" . font-lock-comment-face) ("^> .*$" . font-lock-comment-face) ("^'\\(.\\|\n.\\)*\n\n" . font-lock-comment-face) ("\\w+:" . font-lock-comment-face) ("^:\\w*" . font-lock-preprocessor-face) - ("\\bdef\\b\\|\\bfor\\b\\|\\brof\\b\\|\\bcase\\b\\|\\bstruct\\b\\|\\bdata\\b\\|\\bwhere\\b\\|\\bof\\b\\|\\bif\\b\\|\\bthen\\b\\|\\belse\\b\\|\\binterface\\b\\|\\binstance\\b\\|\\bgiven\\b\\|\\bdo\\b\\|\\bview\\b\\|\\bimport\\b\\|\\bforeign\\b\\|\\bsatisfying\\b\\|\\bself\\b" . + (,(concat + "\\bdef\\b\\|\\bfor\\b\\|\\brof\\b\\|\\bcase\\b\\|" + "\\bstruct\\b\\|\\bdata\\b\\|\\bwhere\\b\\|\\bof\\b\\|" + "\\bif\\b\\|\\bthen\\b\\|\\belse\\b\\|\\binterface\\b\\|" + "\\binstance\\b\\|\\bgiven\\b\\|\\bdo\\b\\|\\bview\\b\\|" + "\\bwith\\b\\|\\bself\\b\\|" + "\\bimport\\b\\|\\bforeign\\b\\|\\bsatisfying\\b") . font-lock-keyword-face) ("--o" . font-lock-variable-name-face) ("[-.,!;$^&*:~+/=<>|?\\\\]" . font-lock-variable-name-face) diff --git a/src/lib/AbstractSyntax.hs b/src/lib/AbstractSyntax.hs index d8776fce3..185be5073 100644 --- a/src/lib/AbstractSyntax.hs +++ b/src/lib/AbstractSyntax.hs @@ -463,7 +463,7 @@ expr = propagateSrcE expr' where EvalBinOp s -> evalOp s DepAmpersand -> do lhs' <- tyOptPat lhs - UDepPairTy . (UDepPairType lhs') <$> expr rhs + UDepPairTy . (UDepPairType ExplicitDepPair lhs') <$> expr rhs DepComma -> UDepPair <$> (expr lhs) <*> expr rhs CSEqual -> throw SyntaxErr "Equal sign must be used as a separator for labels or binders, not a standalone operator" Colon -> throw SyntaxErr "Colon separates binders from their type annotations, is not a standalone operator.\nIf you are trying to write a dependent type, use parens: (i:Fin 4) => (..i)" @@ -534,6 +534,13 @@ expr = propagateSrcE expr' where return $ UCase p' [ UAlt (nsB $ UPatCon "True" Empty) c' , UAlt (nsB $ UPatCon "False" Empty) a'] + expr' (CWith lhs rhs) = do + ty <- expr lhs + case rhs of + [b] -> do + b' <- binderOptTy b + return $ UDepPairTy $ UDepPairType ImplicitDepPair b' ty + _ -> error "n-ary dependent pairs not implemented" charExpr :: Char -> (UExpr' VoidS) charExpr c = UPrim (UPrimCon $ Lit $ Word8Lit $ fromIntegral $ fromEnum c) [] diff --git a/src/lib/Builder.hs b/src/lib/Builder.hs index 8280dd074..115c0b145 100644 --- a/src/lib/Builder.hs +++ b/src/lib/Builder.hs @@ -1397,14 +1397,14 @@ buildTelescopeVal xsTop tyTop = fst <$> go tyTop xsTop where (x1, ~(xDep : rest')) <- go ty1 rest ty2' <- applySubst (b@>SubstVal xDep) ty2 (x2, rest'') <- go ty2' rest' - let depPairTy = DepPairType b (telescopeTypeType ty2) + let depPairTy = DepPairType ExplicitDepPair b (telescopeTypeType ty2) return (PairVal x1 (DepPair xDep x2 depPairTy), rest'') telescopeTypeType :: TelescopeType (AtomNameC r) (Type r) n -> Type r n telescopeTypeType (ProdTelescope tys) = ProdTy tys telescopeTypeType (DepTelescope lhs (Abs b rhs)) = do let lhs' = telescopeTypeType lhs - let rhs' = DepPairTy (DepPairType b (telescopeTypeType rhs)) + let rhs' = DepPairTy (DepPairType ExplicitDepPair b (telescopeTypeType rhs)) PairTy lhs' rhs' unpackTelescope diff --git a/src/lib/CheapReduction.hs b/src/lib/CheapReduction.hs index f7cc546e7..2e02582a0 100644 --- a/src/lib/CheapReduction.hs +++ b/src/lib/CheapReduction.hs @@ -386,7 +386,7 @@ liftSimpAtom ty simpAtom = case simpAtom of (BaseTy _ , Con (Lit v)) -> return $ Con $ Lit v (ProdTy tys, Con (ProdCon xs)) -> Con . ProdCon <$> zipWithM rec tys xs (SumTy tys, Con (SumCon _ i x)) -> Con . SumCon tys i <$> rec (tys!!i) x - (DepPairTy dpt@(DepPairType (b:>t1) t2), DepPair x1 x2 _) -> do + (DepPairTy dpt@(DepPairType _ (b:>t1) t2), DepPair x1 x2 _) -> do x1' <- rec t1 x1 t2' <- applySubst (b@>SubstVal x1') t2 x2' <- rec t2' x2 @@ -414,7 +414,7 @@ confuseGHC = getDistinct -- CheapReduction and QueryType import? depPairLeftTy :: DepPairType r n -> Type r n -depPairLeftTy (DepPairType (_:>ty) _) = ty +depPairLeftTy (DepPairType _ (_:>ty) _) = ty {-# INLINE depPairLeftTy #-} unwrapNewtypeType :: EnvReader m => NewtypeTyCon n -> m n (NewtypeCon n, Type CoreIR n) @@ -467,7 +467,7 @@ makeStructRepVal tyConName args = do _ -> return $ ProdVal args instantiateDepPairTy :: (IRRep r, EnvReader m) => DepPairType r n -> Atom r n -> m n (Type r n) -instantiateDepPairTy (DepPairType b rhsTy) x = applyAbs (Abs b rhsTy) (SubstVal x) +instantiateDepPairTy (DepPairType _ b rhsTy) x = applyAbs (Abs b rhsTy) (SubstVal x) {-# INLINE instantiateDepPairTy #-} projType :: (IRRep r, EnvReader m) => Int -> Type r n -> Atom r n -> m n (Type r n) diff --git a/src/lib/CheckType.hs b/src/lib/CheckType.hs index 95f63ef1a..7eec90584 100644 --- a/src/lib/CheckType.hs +++ b/src/lib/CheckType.hs @@ -339,7 +339,7 @@ instance HasType CoreIR DictExpr where getTypeE e = dictExprType e instance IRRep r => HasType r (DepPairType r) where - getTypeE (DepPairType b ty) = do + getTypeE (DepPairType _ b ty) = do checkB b \_ -> ty |: TyKind return TyKind @@ -1074,7 +1074,7 @@ checkDataLike ty = case ty of TabPi (TabPiType b eltTy) -> do renameBinders b \_ -> checkDataLike eltTy - DepPairTy (DepPairType b@(_:>l) r) -> do + DepPairTy (DepPairType _ b@(_:>l) r) -> do recur l renameBinders b \_ -> checkDataLike r NewtypeTyCon LabelType -> notData diff --git a/src/lib/ConcreteSyntax.hs b/src/lib/ConcreteSyntax.hs index 0df765eb8..d371844fb 100644 --- a/src/lib/ConcreteSyntax.hs +++ b/src/lib/ConcreteSyntax.hs @@ -439,6 +439,9 @@ givenClause = keyWord GivenKW >> do (,) <$> parens (commaSep cGroup) <*> optional (parens (commaSep cGroup)) +withClause :: Parser WithClause +withClause = keyWord WithKW >> parens (commaSep cGroup) + arrowOptEffs :: Parser (Maybe CEffs) arrowOptEffs = sym "->" >> optional cEffs @@ -704,6 +707,7 @@ ops = , [symOpR ":"] , [symOpR ",>"] , [symOpR "&>"] + , [withClausePostfix] , [symOpL "="] ] where other = ("other", anySymOp) @@ -760,6 +764,13 @@ binApp :: Bin' -> SrcPos -> Group -> Group -> Group binApp f pos x y = joinSrc3 f' x y $ CBin f' x y where f' = WithSrc (Just pos) f +withClausePostfix :: (SourceName, Expr.Operator Parser Group) +withClausePostfix = ("with", op) + where + op = Expr.Postfix do + rhs <- withClause + return \lhs -> WithSrc Nothing $ CWith lhs rhs -- TODO: source info + withSrc :: Parser a -> Parser (WithSrc a) withSrc p = do (x, pos) <- withPos p diff --git a/src/lib/GenericTraversal.hs b/src/lib/GenericTraversal.hs index 3917be146..bf835bb4e 100644 --- a/src/lib/GenericTraversal.hs +++ b/src/lib/GenericTraversal.hs @@ -170,10 +170,10 @@ instance GenericallyTraversableE CoreIR TyConParams where TyConParams infs <$> mapM tge params instance IRRep r => GenericallyTraversableE r (DepPairType r) where - traverseGenericE (DepPairType (b:>lty) rty) = do + traverseGenericE (DepPairType expl (b:>lty) rty) = do lty' <- tge lty withFreshBinder (getNameHint b) lty' \b' -> do - extendRenamer (b@>binderName b') $ DepPairType b' <$> tge rty + extendRenamer (b@>binderName b') $ DepPairType expl b' <$> tge rty instance IRRep r => GenericallyTraversableE r (BaseMonoid r) where traverseGenericE (BaseMonoid x f) = BaseMonoid <$> tge x <*> tge f diff --git a/src/lib/Imp.hs b/src/lib/Imp.hs index 673209c06..eb2cd8d71 100644 --- a/src/lib/Imp.hs +++ b/src/lib/Imp.hs @@ -710,7 +710,7 @@ typeToTree tyTop = return $ go REmpty tyTop BaseTy b -> Leaf $ LeafType (unRNest ctx) b TabTy b bodyTy -> go (RNest ctx (TabCtx b)) bodyTy RefTy _ t -> go (RNest ctx RefCtx) t - DepPairTy (DepPairType (b:>t1) (t2)) -> do + DepPairTy (DepPairType _ (b:>t1) (t2)) -> do let tree1 = rec t1 let tree2 = go (RNest ctx (DepPairCtx (JustB (b:>t1)))) t2 Branch [tree1, tree2] @@ -746,7 +746,7 @@ valueToTree (RepVal tyTop valTop) = do BaseTy b -> return $ Leaf $ LeafType (unRNest ctx) b TabTy b bodyTy -> go (RNest ctx (TabCtx b)) bodyTy val RefTy _ t -> go (RNest ctx RefCtx) t val - DepPairTy (DepPairType (b:>t1) (t2)) -> case val of + DepPairTy (DepPairType _ (b:>t1) (t2)) -> case val of Branch [v1, v2] -> do case ctx of REmpty -> do diff --git a/src/lib/Inference.hs b/src/lib/Inference.hs index fb26c56eb..88fe4d2dd 100644 --- a/src/lib/Inference.hs +++ b/src/lib/Inference.hs @@ -705,8 +705,8 @@ hoistInfStateRec env emissions !infVars defaults !subst decls e = case emissions -- If a variable is solved, we eliminate it. Just bSolutionUnhoisted -> do bSolution <- - liftHoistExcept' "Failed to eliminate solved variable in hoistInfStateRec" - $ hoist frag bSolutionUnhoisted + liftHoistExcept' "Failed to eliminate solved variable in hoistInfStateRec " + $ hoist frag bSolutionUnhoisted case exchangeBs $ PairB b infVars of -- This used to be accepted by the code at some point (and handled the same way -- as the Nothing) branch above, but I don't understand why. We don't even seem @@ -850,6 +850,15 @@ checkSigma hint expr sTy = confuseGHC >>= \_ -> case sTy of _ -> Nothing expr' <- inferWithoutInstantiation expr >>= zonk dropSubst $ checkOrInferApp expr' explicits [] (Check resultTy) + DepPairTy depPairTy -> case depPairTy of + DepPairType ImplicitDepPair (_ :> lhsTy) _ -> do + -- TODO: check for the case that we're given some of the implicit dependent pair args explicitly + lhsVal <- Var <$> freshInferenceName MiscInfVar lhsTy + -- TODO: make an InfVarDesc case for dep pair instantiation + rhsTy <- instantiateDepPairTy depPairTy lhsVal + rhsVal <- checkSigma noHint expr rhsTy + return $ DepPair lhsVal rhsVal depPairTy + _ -> fallback _ -> fallback where fallback = checkOrInferRho hint expr (Check sTy) @@ -898,6 +907,8 @@ withUDecl (WithSrcB src d) cont = addSrcContext src case d of var <- emitDecl (getNameHint p) letAnn $ Atom val bindLetPat p var cont +-- "rho" means the required type here should not be (at the top level) an implicit pi type or +-- an implicit dependent pair type. We don't want to unify those directly. -- The name hint names the object being computed checkOrInferRho :: forall i o. EmitsBoth o @@ -939,16 +950,16 @@ checkOrInferRho hint uExprWithSrc@(WithSrcE pos expr) reqTy = do let msg = "Can't reduce type expression: " ++ docAsStr (pretty ty) withReducibleEmissions msg $ checkUType ty matchRequirement $ TabPi piTy - UDepPairTy (UDepPairType (UAnnBinder b ann cs) rhs) -> do + UDepPairTy (UDepPairType expl (UAnnBinder b ann cs) rhs) -> do unless (null cs) $ throw TypeErr "Dependent pair binders shouldn't have constraints" ann' <- checkAnn (getSourceName b) ann matchRequirement =<< liftM DepPairTy do - buildDepPairTyInf (getNameHint b) ann' \v -> extendRenamer (b@>v) do + buildDepPairTyInf (getNameHint b) expl ann' \v -> extendRenamer (b@>v) do let msg = "Can't reduce type expression: " ++ docAsStr (pretty rhs) withReducibleEmissions msg $ checkUType rhs UDepPair lhs rhs -> do case reqTy of - Check (DepPairTy ty@(DepPairType (_ :> lhsTy) _)) -> do + Check (DepPairTy ty@(DepPairType _ (_ :> lhsTy) _)) -> do lhs' <- checkSigmaDependent noHint lhs lhsTy rhsTy <- instantiateDepPairTy ty lhs' rhs' <- checkSigma noHint rhs rhsTy @@ -1178,13 +1189,19 @@ instantiateSigma sigmaAtom = getType sigmaAtom >>= \case Pi (CorePiType ImplicitApp bs _ resultTy) -> do args <- inferMixedArgs @UExpr fDesc (Abs bs resultTy) [] [] applySigmaAtom sigmaAtom args - _ -> case sigmaAtom of - SigmaAtom _ x -> return x - SigmaUVar _ v -> case v of - UAtomVar v' -> return $ Var v' - _ -> applySigmaAtom sigmaAtom [] - SigmaPartialApp _ _ -> error "shouldn't hit this case because we should have a pi type here" - where + DepPairTy (DepPairType ImplicitDepPair _ _) -> + -- TODO: we should probably call instantiateSigma again here in case + -- we have nested dependent pairs. Also, it looks like this doesn't + -- get called after function application. We probably want to fix that. + fallback >>= getSnd + _ -> fallback + where + fallback = case sigmaAtom of + SigmaAtom _ x -> return x + SigmaUVar _ v -> case v of + UAtomVar v' -> return $ Var v' + _ -> applySigmaAtom sigmaAtom [] + SigmaPartialApp _ _ -> error "shouldn't hit this case because we should have a pi type here" fDesc :: SourceName fDesc = getSourceName sigmaAtom @@ -1388,7 +1405,7 @@ applyDataCon tc conIx topArgs = do where nargs = length args; ntys = length tys (curArgs, remArgs) = splitAt (ntys - 1) args - DepPairTy dpt@(DepPairType b rty') -> do + DepPairTy dpt@(DepPairType _ b rty') -> do rty'' <- applySubst (b@>SubstVal h) rty' ans <- wrap rty'' t return $ DepPair h ans dpt @@ -1744,7 +1761,7 @@ dataConRepTy (Abs topBs UnitE) = case topBs of (tailTy, tailIdxs) = go [] (ProjectProduct 1 : (depTyIdxs ++ projIdxs)) bs idxs = (iota accSize <&> \i -> ProjectProduct i : projIdxs) ++ ((ProjectProduct 0 : (depTyIdxs ++ projIdxs)) : tailIdxs) - depTy = DepPairTy $ DepPairType b tailTy + depTy = DepPairTy $ DepPairType ExplicitDepPair b tailTy inferClassDef :: EmitsInf o @@ -3075,7 +3092,7 @@ synthDictForData dictTy@(DictType "Data" dName [ty]) = case ty of -- The "Var" case is different Var _ -> synthDictFromGiven dictTy TabPi (TabPiType b eltTy) -> recurBinder (Abs b eltTy) >> success - DepPairTy (DepPairType b@(_:>l) r) -> do + DepPairTy (DepPairType _ b@(_:>l) r) -> do recur l >> recurBinder (Abs b r) >> success NewtypeTyCon LabelType -> notData NewtypeTyCon nt -> do @@ -3219,12 +3236,12 @@ buildTabPiInf hint ixTy body = do buildDepPairTyInf :: EmitsInf n - => NameHint -> CType n + => NameHint -> DepPairExplicitness -> CType n -> (forall l. (EmitsInf l, Ext n l) => CAtomName l -> InfererM i l (CType l)) -> InfererM i n (DepPairType CoreIR n) -buildDepPairTyInf hint ty body = do +buildDepPairTyInf hint expl ty body = do Abs b resultTy <- buildAbsInf hint Explicit ty body - return $ DepPairType (withoutExpl b) resultTy + return $ DepPairType expl (withoutExpl b) resultTy buildAltInf :: EmitsInf n diff --git a/src/lib/Lexing.hs b/src/lib/Lexing.hs index f3b4be315..34bf6cc53 100644 --- a/src/lib/Lexing.hs +++ b/src/lib/Lexing.hs @@ -80,7 +80,7 @@ checkNotKeyword p = try $ do data KeyWord = DefKW | ForKW | For_KW | RofKW | Rof_KW | CaseKW | OfKW | DataKW | StructKW | InterfaceKW - | InstanceKW | GivenKW | SatisfyingKW + | InstanceKW | GivenKW | WithKW | SatisfyingKW | IfKW | ThenKW | ElseKW | DoKW | ImportKW | ForeignKW | NamedInstanceKW | EffectKW | HandlerKW | JmpKW | CtlKW | ReturnKW | ResumeKW @@ -105,6 +105,7 @@ keyWordToken = \case InstanceKW -> "instance" NamedInstanceKW -> "named-instance" GivenKW -> "given" + WithKW -> "with" SatisfyingKW -> "satisfying" DoKW -> "do" ImportKW -> "import" diff --git a/src/lib/PPrint.hs b/src/lib/PPrint.hs index e5974c93c..af901158a 100644 --- a/src/lib/PPrint.hs +++ b/src/lib/PPrint.hs @@ -259,7 +259,7 @@ instance Pretty (DictType n) where instance IRRep r => Pretty (DepPairType r n) where pretty = prettyFromPrettyPrec instance IRRep r => PrettyPrec (DepPairType r n) where - prettyPrec (DepPairType b rhs) = + prettyPrec (DepPairType _ b rhs) = atPrec ArgPrec $ align $ group $ parens $ p b <+> "&>" <+> p rhs instance Pretty (EffectOpType n) where @@ -656,7 +656,8 @@ instance PrettyPrec (UTabPiExpr n) where instance Pretty (UDepPairType n) where pretty = prettyFromPrettyPrec instance PrettyPrec (UDepPairType n) where - prettyPrec (UDepPairType pat ty) = atPrec LowestPrec $ align $ + -- TODO: print explicitness info + prettyPrec (UDepPairType _ pat ty) = atPrec LowestPrec $ align $ p pat <+> "&>" <+> pLowest ty instance Pretty (UBlock' n) where diff --git a/src/lib/QueryType.hs b/src/lib/QueryType.hs index 562118a41..66b55e4e8 100644 --- a/src/lib/QueryType.hs +++ b/src/lib/QueryType.hs @@ -755,7 +755,7 @@ rawStrType :: IRRep r => EnvReader m => m n (Type r n) rawStrType = liftEnvReaderM do withFreshBinder "n" IdxRepTy \b -> do tabTy <- rawFinTabType (Var $ binderName b) CharRepTy - return $ DepPairTy $ DepPairType b tabTy + return $ DepPairTy $ DepPairType ExplicitDepPair b tabTy -- `n` argument is IdxRepVal, not Nat rawFinTabType :: IRRep r => EnvReader m => Atom r n -> Atom r n -> m n (Type r n) diff --git a/src/lib/Simplify.hs b/src/lib/Simplify.hs index 8c936a4de..2aa745b6e 100644 --- a/src/lib/Simplify.hs +++ b/src/lib/Simplify.hs @@ -143,12 +143,12 @@ getRepType ty = go ty where RefType h a -> RefType <$> toDataAtomIgnoreReconAssumeNoDecls h <*> go a TypeKind -> error $ notDataType HeapType -> return $ HeapType - DepPairTy (DepPairType b@(_:>l) r) -> do + DepPairTy (DepPairType expl b@(_:>l) r) -> do l' <- go l withFreshBinder (getNameHint b) l' \b' -> do x <- liftSimpAtom (sink l) (Var $ binderName b') r' <- go =<< applySubst (b@>SubstVal x) r - return $ DepPairTy $ DepPairType b' r' + return $ DepPairTy $ DepPairType expl b' r' TabPi (TabPiType (b:>ixTy) bodyTy) -> do ixTy' <- simplifyIxType ixTy withFreshBinder (getNameHint b) ixTy' \b' -> do diff --git a/src/lib/SourceRename.hs b/src/lib/SourceRename.hs index dab3445f8..7c793a300 100644 --- a/src/lib/SourceRename.hs +++ b/src/lib/SourceRename.hs @@ -188,9 +188,9 @@ instance SourceRenamableE UExpr' where UTabPi (UTabPiExpr pat body) -> sourceRenameB pat \pat' -> UTabPi <$> (UTabPiExpr pat' <$> sourceRenameE body) - UDepPairTy (UDepPairType pat body) -> + UDepPairTy (UDepPairType expl pat body) -> sourceRenameB pat \pat' -> - UDepPairTy <$> (UDepPairType pat' <$> sourceRenameE body) + UDepPairTy <$> (UDepPairType expl pat' <$> sourceRenameE body) UDepPair lhs rhs -> UDepPair <$> sourceRenameE lhs <*> sourceRenameE rhs UTabApp f x -> UTabApp <$> sourceRenameE f <*> mapM sourceRenameE x diff --git a/src/lib/Types/Core.hs b/src/lib/Types/Core.hs index f6bd3b507..b346d1e18 100644 --- a/src/lib/Types/Core.hs +++ b/src/lib/Types/Core.hs @@ -243,7 +243,7 @@ data CorePiType (n::S) where CorePiType :: AppExplicitness -> CoreBinders n l -> EffectRow CoreIR l -> Type CoreIR l -> CorePiType n data DepPairType (r::IR) (n::S) where - DepPairType :: Binder r n l -> Type r l -> DepPairType r n + DepPairType :: DepPairExplicitness -> Binder r n l -> Type r l -> DepPairType r n data Projection = UnwrapNewtype -- TODO: add `HasCore r` constraint @@ -2009,10 +2009,10 @@ deriving via WrapE (PiType r) n instance IRRep r => Generic (PiType r n) instance IRRep r => Store (PiType r n) instance GenericE (DepPairType r) where - type RepE (DepPairType r) = Abs (Binder r) (Type r) - fromE (DepPairType b resultTy) = Abs b resultTy + type RepE (DepPairType r) = PairE (LiftE DepPairExplicitness) (Abs (Binder r) (Type r)) + fromE (DepPairType expl b resultTy) = LiftE expl `PairE` Abs b resultTy {-# INLINE fromE #-} - toE (Abs b resultTy) = DepPairType b resultTy + toE (LiftE expl `PairE` Abs b resultTy) = DepPairType expl b resultTy {-# INLINE toE #-} instance IRRep r => SinkableE (DepPairType r) diff --git a/src/lib/Types/Primitives.hs b/src/lib/Types/Primitives.hs index 9751f5a5d..98112b0a4 100644 --- a/src/lib/Types/Primitives.hs +++ b/src/lib/Types/Primitives.hs @@ -158,6 +158,7 @@ data Explicitness = Explicit | Inferred (Maybe SourceName) InferenceMechanism deriving (Show, Eq, Ord, Generic) data AppExplicitness = ExplicitApp | ImplicitApp deriving (Show, Generic, Eq) +data DepPairExplicitness = ExplicitDepPair | ImplicitDepPair deriving (Show, Generic, Eq) data WithExpl (b::B) (n::S) (l::S) = WithExpl { getExpl :: Explicitness , withoutExpl :: b n l } @@ -312,6 +313,7 @@ instance Store ScalarBaseType instance Store Device instance Store Explicitness instance Store AppExplicitness +instance Store DepPairExplicitness instance Store InferenceMechanism instance Store a => Store (PrimCon r a) @@ -336,6 +338,7 @@ instance Hashable Device instance Hashable LetAnn instance Hashable Explicitness instance Hashable AppExplicitness +instance Hashable DepPairExplicitness instance Hashable InferenceMechanism instance Hashable RequiredMethodAccess diff --git a/src/lib/Types/Source.hs b/src/lib/Types/Source.hs index 5e39af128..8f33c9a6a 100644 --- a/src/lib/Types/Source.hs +++ b/src/lib/Types/Source.hs @@ -64,7 +64,8 @@ pattern SIInternalName n a = SourceOrInternalName (InternalName n a) -- optional arrow, effects, result type type ExplicitParams = [Group] -type GivenClause = ([Group], Maybe [Group]) +type GivenClause = ([Group], Maybe [Group]) -- implicits, classes +type WithClause = [Group] -- no classes because we don't want to carry class dicts at runtime type CTopDecl = WithSrc CTopDecl' data CTopDecl' @@ -149,6 +150,7 @@ data Group' | CDo CSBlock | CGivens GivenClause | CArrow Group (Maybe CEffs) Group + | CWith Group WithClause deriving (Show, Generic) type Bin = WithSrc Bin' @@ -291,7 +293,7 @@ data UTabPiExpr (n::S) where UTabPiExpr :: UOptAnnBinder n l -> UType l -> UTabPiExpr n data UDepPairType (n::S) where - UDepPairType :: UOptAnnBinder n l -> UType l -> UDepPairType n + UDepPairType :: DepPairExplicitness -> UOptAnnBinder n l -> UType l -> UDepPairType n type UConDef (n::S) (l::S) = (SourceName, Nest UReqAnnBinder n l) diff --git a/tests/struct-tests.dx b/tests/struct-tests.dx index 2f196b1e1..eaf31b7f0 100644 --- a/tests/struct-tests.dx +++ b/tests/struct-tests.dx @@ -20,7 +20,7 @@ my_struct = MyStruct 1 2 "abc" > 12 | :p my_struct.(1 + 1) > | ^^ > unexpected ".(" -> expecting "->", "..", "<..", backquoted name, end of input, end of line, infix operator, name, or symbol name +> expecting "->", "..", "<..", "with", backquoted name, end of input, end of line, infix operator, name, or symbol name :p my_struct > MyStruct(1, 2., "abc") diff --git a/tests/type-tests.dx b/tests/type-tests.dx index bf6a0bc59..03ea48568 100644 --- a/tests/type-tests.dx +++ b/tests/type-tests.dx @@ -692,3 +692,11 @@ def my_id2(x:a) -> a given (a, b:Type) = x > > :p my_id2 1.0 > ^^^^^^^^^^ + +def returns_dep_pair(n:Nat) -> (Fin new => Nat with (new:Nat)) = + n2 = n + n + for i:(Fin n2). ordinal i + +xs = returns_dep_pair 4 +:p sum xs +> 28