From c52b029986e47d02f60fd2d59d79d1c9baaba0c1 Mon Sep 17 00:00:00 2001 From: "G. Allais" Date: Fri, 1 Sep 2023 11:35:52 +0100 Subject: [PATCH] [ new ] function options for case blocks (#3062) --- idris2api.ipkg | 1 + libs/base/Language/Reflection/TTImp.idr | 18 +-- src/Core/Binary.idr | 2 +- src/Idris/Desugar.idr | 22 +-- src/Idris/Parser.idr | 120 ++++++++-------- src/Idris/Pretty.idr | 2 +- src/Idris/Resugar.idr | 14 +- src/Idris/Syntax.idr | 6 +- src/Idris/Syntax/Traversals.idr | 11 +- src/TTImp/Elab/App.idr | 2 +- src/TTImp/Elab/Case.idr | 12 +- src/TTImp/Elab/Quote.idr | 7 +- src/TTImp/Elab/Record.idr | 2 +- src/TTImp/Elab/Term.idr | 4 +- src/TTImp/Parser.idr | 3 +- src/TTImp/ProcessFnOpt.idr | 180 ++++++++++++++++++++++++ src/TTImp/ProcessType.idr | 169 +--------------------- src/TTImp/Reflect.idr | 10 +- src/TTImp/TTImp.idr | 6 +- src/TTImp/TTImp/Functor.idr | 4 +- src/TTImp/TTImp/TTC.idr | 8 +- src/TTImp/TTImp/Traversals.idr | 4 +- src/TTImp/Unelab.idr | 3 +- src/TTImp/Utils.idr | 13 +- src/TTImp/WithClause.idr | 4 +- tests/Main.idr | 1 + tests/idris2/case001/InlineCase.idr | 27 ++++ tests/idris2/case001/expected | 1 + tests/idris2/case001/run | 4 + tests/idris2/reg033/DerivingEq.idr | 2 +- 30 files changed, 363 insertions(+), 299 deletions(-) create mode 100644 src/TTImp/ProcessFnOpt.idr create mode 100644 tests/idris2/case001/InlineCase.idr create mode 100644 tests/idris2/case001/expected create mode 100755 tests/idris2/case001/run diff --git a/idris2api.ipkg b/idris2api.ipkg index 1724a3373..88429b16d 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -257,6 +257,7 @@ modules = TTImp.ProcessDecls, TTImp.ProcessDecls.Totality, TTImp.ProcessDef, + TTImp.ProcessFnOpt, TTImp.ProcessParams, TTImp.ProcessRecord, TTImp.ProcessRunElab, diff --git a/libs/base/Language/Reflection/TTImp.idr b/libs/base/Language/Reflection/TTImp.idr index 569f4c33a..34c6ac3ad 100644 --- a/libs/base/Language/Reflection/TTImp.idr +++ b/libs/base/Language/Reflection/TTImp.idr @@ -39,7 +39,7 @@ mutual ILet : FC -> (lhsFC : FC) -> Count -> Name -> (nTy : TTImp) -> (nVal : TTImp) -> (scope : TTImp) -> TTImp - ICase : FC -> TTImp -> (ty : TTImp) -> + ICase : FC -> List FnOpt -> TTImp -> (ty : TTImp) -> List Clause -> TTImp ILocal : FC -> List Decl -> TTImp -> TTImp IUpdate : FC -> List IFieldUpdate -> TTImp -> TTImp @@ -203,7 +203,7 @@ getFC (IVar fc _) = fc getFC (IPi fc _ _ _ _ _) = fc getFC (ILam fc _ _ _ _ _) = fc getFC (ILet fc _ _ _ _ _ _) = fc -getFC (ICase fc _ _ _) = fc +getFC (ICase fc _ _ _ _) = fc getFC (ILocal fc _ _) = fc getFC (IUpdate fc _ _) = fc getFC (IApp fc _ _) = fc @@ -236,7 +236,7 @@ mapTopmostFC fcf $ IVar fc a = IVar (fcf fc) a mapTopmostFC fcf $ IPi fc a b c d e = IPi (fcf fc) a b c d e mapTopmostFC fcf $ ILam fc a b c d e = ILam (fcf fc) a b c d e mapTopmostFC fcf $ ILet fc a b c d e f = ILet (fcf fc) a b c d e f -mapTopmostFC fcf $ ICase fc a b c = ICase (fcf fc) a b c +mapTopmostFC fcf $ ICase fc opts a b c = ICase (fcf fc) opts a b c mapTopmostFC fcf $ ILocal fc a b = ILocal (fcf fc) a b mapTopmostFC fcf $ IUpdate fc a b = IUpdate (fcf fc) a b mapTopmostFC fcf $ IApp fc a b = IApp (fcf fc) a b @@ -403,7 +403,7 @@ Eq TTImp where c == c' && (assert_total $ i == i') && n == n' && a == a' && r == r' ILet _ _ c n ty val s == ILet _ _ c' n' ty' val' s' = c == c' && n == n' && ty == ty' && val == val' && s == s' - ICase _ t ty cs == ICase _ t' ty' cs' + ICase _ _ t ty cs == ICase _ _ t' ty' cs' = t == t' && ty == ty' && (assert_total $ cs == cs') ILocal _ ds e == ILocal _ ds' e' = (assert_total $ ds == ds') && e == e' @@ -573,7 +573,7 @@ mutual showPrec d (ILet fc lhsFC rig nm nTy nVal scope) = showParens (d > Open) $ "let \{showCount rig (show nm)} : \{show nTy} = \{show nVal} in \{show scope}" - showPrec d (ICase fc s ty xs) + showPrec d (ICase fc _ s ty xs) = showParens (d > Open) $ unwords $ [ "case", show s ] ++ typeFor ty ++ [ "of", "{" , joinBy "; " (assert_total $ map (showClause InCase) xs) @@ -783,8 +783,8 @@ parameters (f : TTImp -> TTImp) = f $ ILam fc rig (mapPiInfo pinfo) x (mapTTImp argTy) (mapTTImp lamTy) mapTTImp (ILet fc lhsFC rig n nTy nVal scope) = f $ ILet fc lhsFC rig n (mapTTImp nTy) (mapTTImp nVal) (mapTTImp scope) - mapTTImp (ICase fc t ty cls) - = f $ ICase fc (mapTTImp t) (mapTTImp ty) (assert_total $ map mapClause cls) + mapTTImp (ICase fc opts t ty cls) + = f $ ICase fc opts (mapTTImp t) (mapTTImp ty) (assert_total $ map mapClause cls) mapTTImp (ILocal fc xs t) = f $ ILocal fc (assert_total $ map mapDecl xs) (mapTTImp t) mapTTImp (IUpdate fc upds t) = f $ IUpdate fc (assert_total map mapIFieldUpdate upds) (mapTTImp t) @@ -909,8 +909,8 @@ parameters {0 m : Type -> Type} {auto mon : Monad m} (f : TTImp -> m TTImp) = f =<< ILam fc rig <$> mapMPiInfo pinfo <*> pure x <*> mapMTTImp argTy <*> mapMTTImp lamTy mapMTTImp (ILet fc lhsFC rig n nTy nVal scope) = f =<< ILet fc lhsFC rig n <$> mapMTTImp nTy <*> mapMTTImp nVal <*> mapMTTImp scope - mapMTTImp (ICase fc t ty cls) - = f =<< ICase fc <$> mapMTTImp t <*> mapMTTImp ty <*> assert_total (traverse mapMClause cls) + mapMTTImp (ICase fc opts t ty cls) + = f =<< ICase fc opts <$> mapMTTImp t <*> mapMTTImp ty <*> assert_total (traverse mapMClause cls) mapMTTImp (ILocal fc xs t) = f =<< ILocal fc <$> assert_total (traverse mapMDecl xs) <*> mapMTTImp t mapMTTImp (IUpdate fc upds t) diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 1c3a1cec3..087af8569 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -29,7 +29,7 @@ import public Libraries.Utils.Binary ||| version number if you're changing the version more than once in the same day. export ttcVersion : Int -ttcVersion = 20230414 * 100 + 0 +ttcVersion = 20230829 * 100 + 0 export checkTTCVersion : String -> Int -> Int -> Core () diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 499bac7dd..140b046f5 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -245,7 +245,7 @@ mutual !(desugar AnyExpr (n :: ps) scope) else pure $ ILam EmptyFC rig !(traverse (desugar AnyExpr ps) p) (Just (MN "lamc" 0)) !(desugarB AnyExpr ps argTy) $ - ICase fc (IVar EmptyFC (MN "lamc" 0)) (Implicit fc False) + ICase fc [] (IVar EmptyFC (MN "lamc" 0)) (Implicit fc False) [snd !(desugarClause ps True (MkPatClause fc pat scope []))] desugarB side ps (PLam fc rig p (PRef _ n@(MN _ _)) argTy scope) = pure $ ILam fc rig !(traverse (desugar AnyExpr ps) p) @@ -258,7 +258,7 @@ mutual desugarB side ps (PLam fc rig p pat argTy scope) = pure $ ILam EmptyFC rig !(traverse (desugar AnyExpr ps) p) (Just (MN "lamc" 0)) !(desugarB AnyExpr ps argTy) $ - ICase fc (IVar EmptyFC (MN "lamc" 0)) (Implicit fc False) + ICase fc [] (IVar EmptyFC (MN "lamc" 0)) (Implicit fc False) [snd !(desugarClause ps True (MkPatClause fc pat scope []))] desugarB side ps (PLet fc rig (PRef prefFC n) nTy nVal scope []) = do whenJust (isConcreteFC prefFC) $ \nfc => @@ -266,13 +266,15 @@ mutual pure $ ILet fc prefFC rig n !(desugarB side ps nTy) !(desugarB side ps nVal) !(desugar side (n :: ps) scope) desugarB side ps (PLet fc rig pat nTy nVal scope alts) - = pure $ ICase fc !(desugarB side ps nVal) !(desugarB side ps nTy) + = pure $ ICase fc [] !(desugarB side ps nVal) !(desugarB side ps nTy) !(traverse (map snd . desugarClause ps True) (MkPatClause fc pat scope [] :: alts)) - desugarB side ps (PCase fc x xs) - = pure $ ICase fc !(desugarB side ps x) - (Implicit (virtualiseFC fc) False) - !(traverse (map snd . desugarClause ps True) xs) + desugarB side ps (PCase fc opts scr cls) + = do opts <- traverse (desugarFnOpt ps) opts + scr <- desugarB side ps scr + let scrty = Implicit (virtualiseFC fc) False + cls <- traverse (map snd . desugarClause ps True) cls + pure $ ICase fc opts scr scrty cls desugarB side ps (PLocal fc xs scope) = let ps' = definedIn xs ++ ps in pure $ ILocal fc (concat !(traverse (desugarDecl ps') xs)) @@ -454,7 +456,7 @@ mutual IVar fc (UN $ Basic "MkUnit")] desugarB side ps (PIfThenElse fc x t e) = let fc = virtualiseFC fc in - pure $ ICase fc !(desugarB side ps x) (IVar fc (UN $ Basic "Bool")) + pure $ ICase fc [] !(desugarB side ps x) (IVar fc (UN $ Basic "Bool")) [PatClause fc (IVar fc (UN $ Basic "True")) !(desugar side ps t), PatClause fc (IVar fc (UN $ Basic "False")) !(desugar side ps e)] desugarB side ps (PComprehension fc ret conds) = do @@ -674,7 +676,7 @@ mutual pure $ bindFun fc ns exp' $ ILam EmptyFC top Explicit (Just (MN "_" 0)) (Implicit fc False) - (ICase fc (IVar patFC (MN "_" 0)) + (ICase fc [] (IVar patFC (MN "_" 0)) (Implicit fc False) (PatClause fcOriginal bpat rest' :: alts')) @@ -700,7 +702,7 @@ mutual bd <- get Bang let fc = virtualiseFC fc pure $ bindBangs (bangNames bd) ns $ - ICase fc tm' ty' + ICase fc [] tm' ty' (PatClause fc bpat rest' :: alts') expandDo side ps topfc ns (DoLetLocal fc decls :: rest) diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 9ed85ae9c..d31360de4 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -211,6 +211,17 @@ debugString fname = do DebugLine => "\{show (startLine di.bounds)}" DebugCol => "\{show (startCol di.bounds)}" +totalityOpt : OriginDesc -> Rule TotalReq +totalityOpt fname + = (decoratedKeyword fname "partial" $> PartialOK) + <|> (decoratedKeyword fname "total" $> Total) + <|> (decoratedKeyword fname "covering" $> CoveringOnly) + +fnOpt : OriginDesc -> Rule PFnOpt +fnOpt fname + = do x <- totalityOpt fname + pure $ IFnOpt (Totality x) + mutual appExpr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm appExpr q fname indents @@ -753,7 +764,7 @@ mutual fcCase = virtualiseFC $ boundToFC fname endCase n = MN "lcase" 0 in PLam fcCase top Explicit (PRef fcCase n) (PInfer fcCase) $ - PCase (virtualiseFC fc) (PRef fcCase n) b.val) + PCase (virtualiseFC fc) [] (PRef fcCase n) b.val) letBlock : OriginDesc -> IndentInfo -> Rule (WithBounds (Either LetBinder LetDecl)) letBlock fname indents = bounds (letBinder <||> letDecl) where @@ -782,13 +793,14 @@ mutual case_ : OriginDesc -> IndentInfo -> Rule PTerm case_ fname indents - = do b <- bounds (do decoratedKeyword fname "case" + = do opts <- many (fnDirectOpt fname) + b <- bounds (do decoratedKeyword fname "case" scr <- expr pdef fname indents mustWork (commitKeyword fname indents "of") alts <- block (caseAlt fname) pure (scr, alts)) (scr, alts) <- pure b.val - pure (PCase (virtualiseFC $ boundToFC fname b) scr alts) + pure (PCase (virtualiseFC $ boundToFC fname b) opts scr alts) caseAlt : OriginDesc -> IndentInfo -> Rule PClause @@ -1055,6 +1067,52 @@ mutual $ acc :< (line <>> [StrLiteral fc str]) <>< map (\str => [StrLiteral fc str]) (init strs) + fnDirectOpt : OriginDesc -> Rule PFnOpt + fnDirectOpt fname + = do decoratedPragma fname "hint" + pure $ IFnOpt (Hint True) + <|> do decoratedPragma fname "globalhint" + pure $ IFnOpt (GlobalHint False) + <|> do decoratedPragma fname "defaulthint" + pure $ IFnOpt (GlobalHint True) + <|> do decoratedPragma fname "inline" + commit + pure $ IFnOpt Inline + <|> do decoratedPragma fname "unsafe" + commit + pure $ IFnOpt Unsafe + <|> do decoratedPragma fname "noinline" + commit + pure $ IFnOpt NoInline + <|> do decoratedPragma fname "deprecate" + commit + pure $ IFnOpt Deprecate + <|> do decoratedPragma fname "tcinline" + commit + pure $ IFnOpt TCInline + <|> do decoratedPragma fname "extern" + pure $ IFnOpt ExternFn + <|> do decoratedPragma fname "macro" + pure $ IFnOpt Macro + <|> do decoratedPragma fname "spec" + ns <- sepBy (decoratedSymbol fname ",") name + pure $ IFnOpt (SpecArgs ns) + <|> do decoratedPragma fname "foreign" + cs <- block (expr pdef fname) + pure $ PForeign cs + <|> do (decoratedPragma fname "export" + <|> withWarning noMangleWarning + (decoratedPragma fname "nomangle")) + cs <- block (expr pdef fname) + pure $ PForeignExport cs + where + noMangleWarning : String + noMangleWarning = """ + DEPRECATED: "%nomangle". + Use "%export" instead + """ + + visOption : OriginDesc -> Rule Visibility visOption fname = (decoratedKeyword fname "public" *> decoratedKeyword fname "export" $> Public) @@ -1268,12 +1326,6 @@ dataDeclBody fname indents (col, n) <- pure b.val simpleData fname b n indents <|> gadtData fname col b n indents -totalityOpt : OriginDesc -> Rule TotalReq -totalityOpt fname - = (decoratedKeyword fname "partial" $> PartialOK) - <|> (decoratedKeyword fname "total" $> Total) - <|> (decoratedKeyword fname "covering" $> CoveringOnly) - -- a data declaration can have a visibility and an optional totality (#1404) dataVisOpt : OriginDesc -> EmptyRule (Visibility, Maybe TotalReq) dataVisOpt fname @@ -1507,56 +1559,6 @@ usingDecls fname indents (us, ds) <- pure b.val pure (PUsing (boundToFC fname b) us (collectDefs (concat ds))) -fnOpt : OriginDesc -> Rule PFnOpt -fnOpt fname - = do x <- totalityOpt fname - pure $ IFnOpt (Totality x) - -fnDirectOpt : OriginDesc -> Rule PFnOpt -fnDirectOpt fname - = do decoratedPragma fname "hint" - pure $ IFnOpt (Hint True) - <|> do decoratedPragma fname "globalhint" - pure $ IFnOpt (GlobalHint False) - <|> do decoratedPragma fname "defaulthint" - pure $ IFnOpt (GlobalHint True) - <|> do decoratedPragma fname "inline" - commit - pure $ IFnOpt Inline - <|> do decoratedPragma fname "unsafe" - commit - pure $ IFnOpt Unsafe - <|> do decoratedPragma fname "noinline" - commit - pure $ IFnOpt NoInline - <|> do decoratedPragma fname "deprecate" - commit - pure $ IFnOpt Deprecate - <|> do decoratedPragma fname "tcinline" - commit - pure $ IFnOpt TCInline - <|> do decoratedPragma fname "extern" - pure $ IFnOpt ExternFn - <|> do decoratedPragma fname "macro" - pure $ IFnOpt Macro - <|> do decoratedPragma fname "spec" - ns <- sepBy (decoratedSymbol fname ",") name - pure $ IFnOpt (SpecArgs ns) - <|> do decoratedPragma fname "foreign" - cs <- block (expr pdef fname) - pure $ PForeign cs - <|> do (decoratedPragma fname "export" - <|> withWarning noMangleWarning - (decoratedPragma fname "nomangle")) - cs <- block (expr pdef fname) - pure $ PForeignExport cs - where - noMangleWarning : String - noMangleWarning = """ - DEPRECATED: "%nomangle". - Use "%export" instead - """ - builtinDecl : OriginDesc -> IndentInfo -> Rule PDecl builtinDecl fname indents = do b <- bounds (do decoratedPragma fname "builtin" diff --git a/src/Idris/Pretty.idr b/src/Idris/Pretty.idr index 6d517f0b5..6c4cffa8f 100644 --- a/src/Idris/Pretty.idr +++ b/src/Idris/Pretty.idr @@ -281,7 +281,7 @@ mutual ; _ => hardline <+> indent 4 (vsep (prettyAlt <$> alts)) <+> hardline <+> in_ } <+> group (align $ hang 2 $ pretty sc) - prettyPrec d (PCase _ tm cs) = + prettyPrec d (PCase _ _ tm cs) = parenthesise (d > startPrec) $ case_ <++> pretty tm <++> of_ <+> nest 2 ( let punctuation = lcurly :: (semi <$ fromMaybe [] (tail' [1..length cs])) in diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index 33a72cabc..85ccd0b6b 100644 --- a/src/Idris/Resugar.idr +++ b/src/Idris/Resugar.idr @@ -315,20 +315,22 @@ mutual sc' <- toPTerm startPrec sc let var = PRef lhsFC (MkKindedName (Just Bound) n n) bracket p startPrec (PLet fc rig var ty' val' sc' []) - toPTerm p (ICase fc sc scty [PatClause _ lhs rhs]) + toPTerm p (ICase fc _ sc scty [PatClause _ lhs rhs]) = do sc' <- toPTerm startPrec sc lhs' <- toPTerm startPrec lhs rhs' <- toPTerm startPrec rhs bracket p startPrec (PLet fc top lhs' (PImplicit fc) sc' rhs' []) - toPTerm p (ICase fc sc scty alts) - = do sc' <- toPTerm startPrec sc + toPTerm p (ICase fc opts sc scty alts) + = do opts' <- traverse toPFnOpt opts + sc' <- toPTerm startPrec sc alts' <- traverse toPClause alts - bracket p startPrec (mkIf (PCase fc sc' alts')) + bracket p startPrec (mkIf (PCase fc opts' sc' alts')) where mkIf : IPTerm -> IPTerm - mkIf tm@(PCase loc sc [MkPatClause _ (PRef _ tval) t [], - MkPatClause _ (PRef _ fval) f []]) + mkIf tm@(PCase loc opts sc + [ MkPatClause _ (PRef _ tval) t [] + , MkPatClause _ (PRef _ fval) f []]) = if dropNS (rawName tval) == UN (Basic "True") && dropNS (rawName fval) == UN (Basic "False") then PIfThenElse loc sc t f diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index b0bc35ff1..8e746a0b3 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -107,7 +107,7 @@ mutual PLet : FC -> RigCount -> (pat : PTerm' nm) -> (nTy : PTerm' nm) -> (nVal : PTerm' nm) -> (scope : PTerm' nm) -> (alts : List (PClause' nm)) -> PTerm' nm - PCase : FC -> PTerm' nm -> List (PClause' nm) -> PTerm' nm + PCase : FC -> List (PFnOpt' nm) -> PTerm' nm -> List (PClause' nm) -> PTerm' nm PLocal : FC -> List (PDecl' nm) -> (scope : PTerm' nm) -> PTerm' nm PUpdate : FC -> List (PFieldUpdate' nm) -> PTerm' nm PApp : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm @@ -178,7 +178,7 @@ mutual getPTermLoc (PPi fc _ _ _ _ _) = fc getPTermLoc (PLam fc _ _ _ _ _) = fc getPTermLoc (PLet fc _ _ _ _ _ _) = fc - getPTermLoc (PCase fc _ _) = fc + getPTermLoc (PCase fc _ _ _) = fc getPTermLoc (PLocal fc _ _) = fc getPTermLoc (PUpdate fc _) = fc getPTermLoc (PApp fc _ _) = fc @@ -755,7 +755,7 @@ parameters {0 nm : Type} (toName : nm -> Name) = "let " ++ showCount rig ++ showPTermPrec d n ++ " : " ++ showPTermPrec d ty ++ " = " ++ showPTermPrec d val ++ concatMap showAlt alts ++ " in " ++ showPTermPrec d sc - showPTermPrec _ (PCase _ tm cs) + showPTermPrec _ (PCase _ _ tm cs) = "case " ++ showPTerm tm ++ " of { " ++ showSep " ; " (map showCase cs) ++ " }" where diff --git a/src/Idris/Syntax/Traversals.idr b/src/Idris/Syntax/Traversals.idr index de16afd48..f57c13de6 100644 --- a/src/Idris/Syntax/Traversals.idr +++ b/src/Idris/Syntax/Traversals.idr @@ -36,8 +36,9 @@ mapPTermM f = goPTerm where <*> goPTerm scope <*> goPClauses alts >>= f - goPTerm (PCase fc x xs) = - PCase fc <$> goPTerm x + goPTerm (PCase fc opts x xs) = + PCase fc <$> goPFnOpts opts + <*> goPTerm x <*> goPClauses xs >>= f goPTerm (PLocal fc xs scope) = @@ -395,8 +396,8 @@ mapPTerm f = goPTerm where = f $ PLam fc x (goPiInfo info) z (goPTerm argTy) (goPTerm scope) goPTerm (PLet fc x pat nTy nVal scope alts) = f $ PLet fc x (goPTerm pat) (goPTerm nTy) (goPTerm nVal) (goPTerm scope) (goPClause <$> alts) - goPTerm (PCase fc x xs) - = f $ PCase fc (goPTerm x) (goPClause <$> xs) + goPTerm (PCase fc opts x xs) + = f $ PCase fc (goPFnOpt <$> opts) (goPTerm x) (goPClause <$> xs) goPTerm (PLocal fc xs scope) = f $ PLocal fc (goPDecl <$> xs) (goPTerm scope) goPTerm (PUpdate fc xs) @@ -596,7 +597,7 @@ substFC fc = mapPTerm $ \case PPi _ x y z argTy retTy => PPi fc x y z argTy retTy PLam _ x y pat argTy scope => PLam fc x y pat argTy scope PLet _ x pat nTy nVal scope alts => PLet fc x pat nTy nVal scope alts - PCase _ x xs => PCase fc x xs + PCase _ opts x xs => PCase fc opts x xs PLocal _ xs scope => PLocal fc xs scope PUpdate _ xs => PUpdate fc xs PApp _ x y => PApp fc x y diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index 8a38ae19c..06141ff62 100644 --- a/src/TTImp/Elab/App.idr +++ b/src/TTImp/Elab/App.idr @@ -306,7 +306,7 @@ mutual needsDelayExpr True (IAutoApp _ f _) = needsDelayExpr True f needsDelayExpr True (INamedApp _ f _ _) = needsDelayExpr True f needsDelayExpr True (ILam _ _ _ _ _ _) = pure True - needsDelayExpr True (ICase _ _ _ _) = pure True + needsDelayExpr True (ICase _ _ _ _ _) = pure True needsDelayExpr True (ILocal _ _ _) = pure True needsDelayExpr True (IUpdate _ _ _) = pure True needsDelayExpr True (IAlternative _ _ _) = pure True diff --git a/src/TTImp/Elab/Case.idr b/src/TTImp/Elab/Case.idr index fc03a8ea1..ba5e03f34 100644 --- a/src/TTImp/Elab/Case.idr +++ b/src/TTImp/Elab/Case.idr @@ -17,6 +17,7 @@ import TTImp.Elab.Check import TTImp.Elab.Delayed import TTImp.Elab.ImplicitBind import TTImp.Elab.Utils +import TTImp.ProcessFnOpt import TTImp.TTImp import TTImp.Utils @@ -165,13 +166,14 @@ caseBlock : {vars : _} -> ElabInfo -> FC -> NestedNames vars -> Env Term vars -> + List FnOpt -> RawImp -> -- original scrutinee Term vars -> -- checked scrutinee Term vars -> -- its type RigCount -> -- its multiplicity List ImpClause -> Maybe (Glued vars) -> Core (Term vars, Glued vars) -caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected +caseBlock {vars} rigc elabinfo fc nest env opts scr scrtm scrty caseRig alts expected = do -- TODO (or to decide): Blodwen allowed ambiguities in the scrutinee -- to be delayed, but now I think it's better to have simpler -- resolution rules, and not delay @@ -235,6 +237,8 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected (newDef fc casen (if isErased rigc then erased else top) [] casefnty vis None)) + traverse_ (processFnOpt fc False casen) opts + -- set the totality of the case block to be the same as that -- of the parent function let tot = fromMaybe PartialOK $ do findSetTotal (flags !parentDef) @@ -384,10 +388,10 @@ checkCase : {vars : _} -> {auto o : Ref ROpts REPLOpts} -> RigCount -> ElabInfo -> NestedNames vars -> Env Term vars -> - FC -> (scr : RawImp) -> (ty : RawImp) -> List ImpClause -> + FC -> List FnOpt -> (scr : RawImp) -> (ty : RawImp) -> List ImpClause -> Maybe (Glued vars) -> Core (Term vars, Glued vars) -checkCase rig elabinfo nest env fc scr scrty_in alts exp +checkCase rig elabinfo nest env fc opts scr scrty_in alts exp = delayElab fc rig env exp CaseBlock $ do scrty_exp <- case scrty_in of Implicit _ _ => guessScrType alts @@ -419,7 +423,7 @@ checkCase rig elabinfo nest env fc scr scrty_in alts exp logTermNF "elab.case" 5 "Scrutinee type" env scrty defs <- get Ctxt checkConcrete !(nf defs env scrty) - caseBlock rig elabinfo fc nest env scr scrtm_in scrty caseRig alts exp + caseBlock rig elabinfo fc nest env opts scr scrtm_in scrty caseRig alts exp where -- For the moment, throw an error if we haven't been able to work out -- the type of the case scrutinee, because we'll need it to build the diff --git a/src/TTImp/Elab/Quote.idr b/src/TTImp/Elab/Quote.idr index 6f60e5436..420779cdf 100644 --- a/src/TTImp/Elab/Quote.idr +++ b/src/TTImp/Elab/Quote.idr @@ -35,9 +35,10 @@ mutual = pure $ ILam fc c p n !(getUnquote arg) !(getUnquote sc) getUnquote (ILet fc lhsFC c n ty val sc) = pure $ ILet fc lhsFC c n !(getUnquote ty) !(getUnquote val) !(getUnquote sc) - getUnquote (ICase fc sc ty cs) - = pure $ ICase fc !(getUnquote sc) !(getUnquote ty) - !(traverse getUnquoteClause cs) + getUnquote (ICase fc opts sc ty cs) + = pure $ ICase fc opts + !(getUnquote sc) !(getUnquote ty) + !(traverse getUnquoteClause cs) getUnquote (ILocal fc ds sc) = pure $ ILocal fc !(traverse getUnquoteDecl ds) !(getUnquote sc) getUnquote (IUpdate fc ds sc) diff --git a/src/TTImp/Elab/Record.idr b/src/TTImp/Elab/Record.idr index 39dd4270f..5b2a3409a 100644 --- a/src/TTImp/Elab/Record.idr +++ b/src/TTImp/Elab/Record.idr @@ -196,7 +196,7 @@ recUpdate rigc elabinfo iloc nest env flds rec grecty fldn <- genFieldName "__fld" sides <- getAllSides iloc flds rectyn rec (Field Nothing fldn (IVar vloc (UN $ Basic fldn))) - pure $ ICase vloc rec (Implicit vloc False) [mkClause sides] + pure $ ICase vloc [] rec (Implicit vloc False) [mkClause sides] where vloc : FC vloc = virtualiseFC iloc diff --git a/src/TTImp/Elab/Term.idr b/src/TTImp/Elab/Term.idr index ae1128f41..a552d20f3 100644 --- a/src/TTImp/Elab/Term.idr +++ b/src/TTImp/Elab/Term.idr @@ -146,8 +146,8 @@ checkTerm rig elabinfo nest env (ILam fc r p Nothing argTy scope) exp checkLambda rig elabinfo nest env fc r p n argTy scope exp checkTerm rig elabinfo nest env (ILet fc lhsFC r n nTy nVal scope) exp = checkLet rig elabinfo nest env fc lhsFC r n nTy nVal scope exp -checkTerm rig elabinfo nest env (ICase fc scr scrty alts) exp - = checkCase rig elabinfo nest env fc scr scrty alts exp +checkTerm rig elabinfo nest env (ICase fc opts scr scrty alts) exp + = checkCase rig elabinfo nest env fc opts scr scrty alts exp checkTerm rig elabinfo nest env (ILocal fc nested scope) exp = checkLocal rig elabinfo nest env fc nested scope exp checkTerm rig elabinfo nest env (ICaseLocal fc uname iname args scope) exp diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index b8a1415fe..427792ce5 100644 --- a/src/TTImp/Parser.idr +++ b/src/TTImp/Parser.idr @@ -376,13 +376,14 @@ mutual case_ : OriginDesc -> IndentInfo -> Rule RawImp case_ fname indents = do start <- location + opts <- many fnOpt keyword "case" scr <- expr fname indents keyword "of" alts <- block (caseAlt fname) end <- location pure (let fc = MkFC fname start end in - ICase fc scr (Implicit fc False) alts) + ICase fc opts scr (Implicit fc False) alts) caseAlt : OriginDesc -> IndentInfo -> Rule ImpClause caseAlt fname indents diff --git a/src/TTImp/ProcessFnOpt.idr b/src/TTImp/ProcessFnOpt.idr new file mode 100644 index 000000000..1696a369b --- /dev/null +++ b/src/TTImp/ProcessFnOpt.idr @@ -0,0 +1,180 @@ +module TTImp.ProcessFnOpt + +import Core.Context +import Core.Context.Log +import Core.Env +import Core.Normalise +import Core.Value + +import TTImp.TTImp + +import Libraries.Data.NameMap + +getRetTy : Defs -> NF [] -> Core Name +getRetTy defs (NBind fc _ (Pi _ _ _ _) sc) + = getRetTy defs !(sc defs (toClosure defaultOpts [] (Erased fc Placeholder))) +getRetTy defs (NTCon _ n _ _ _) = pure n +getRetTy defs ty + = throw (GenericMsg (getLoc ty) + "Can only add hints for concrete return types") + +throwIfHasFlag : {auto c : Ref Ctxt Defs} -> FC -> Name -> DefFlag -> String -> Core () +throwIfHasFlag fc ndef fl msg + = when !(hasFlag fc ndef fl) $ throw (GenericMsg fc msg) + +export +processFnOpt : {auto c : Ref Ctxt Defs} -> + FC -> Bool -> -- ^ top level name? + Name -> FnOpt -> Core () +processFnOpt fc _ ndef Unsafe + = do setIsEscapeHatch fc ndef +processFnOpt fc _ ndef Inline + = do throwIfHasFlag fc ndef NoInline "%noinline and %inline are mutually exclusive" + setFlag fc ndef Inline +processFnOpt fc _ ndef NoInline + = do throwIfHasFlag fc ndef Inline "%inline and %noinline are mutually exclusive" + setFlag fc ndef NoInline +processFnOpt fc _ ndef Deprecate + = setFlag fc ndef Deprecate +processFnOpt fc _ ndef TCInline + = setFlag fc ndef TCInline +processFnOpt fc True ndef (Hint d) + = do defs <- get Ctxt + Just ty <- lookupTyExact ndef (gamma defs) + | Nothing => undefinedName fc ndef + target <- getRetTy defs !(nf defs [] ty) + addHintFor fc target ndef d False +processFnOpt fc _ ndef (Hint d) + = do logC "elab" 5 $ do pure $ "Adding local hint " ++ show !(toFullNames ndef) + addLocalHint ndef +processFnOpt fc True ndef (GlobalHint a) + = addGlobalHint ndef a +processFnOpt fc _ ndef (GlobalHint a) + = throw (GenericMsg fc "%globalhint is not valid in local definitions") +processFnOpt fc _ ndef ExternFn + = setFlag fc ndef Inline -- if externally defined, inline when compiling +processFnOpt fc _ ndef (ForeignFn _) + = setFlag fc ndef Inline -- if externally defined, inline when compiling +processFnOpt fc _ ndef (ForeignExport _) + = pure () +processFnOpt fc _ ndef Invertible + = setFlag fc ndef Invertible +processFnOpt fc _ ndef (Totality tot) + = setFlag fc ndef (SetTotal tot) +processFnOpt fc _ ndef Macro + = setFlag fc ndef Macro +processFnOpt fc _ ndef (SpecArgs ns) + = do defs <- get Ctxt + Just gdef <- lookupCtxtExact ndef (gamma defs) + | Nothing => undefinedName fc ndef + nty <- nf defs [] (type gdef) + ps <- getNamePos 0 nty + ddeps <- collectDDeps nty + specs <- collectSpec [] ddeps ps nty + ignore $ addDef ndef ({ specArgs := specs } gdef) + where + insertDeps : List Nat -> List (Name, Nat) -> List Name -> List Nat + insertDeps acc ps [] = acc + insertDeps acc ps (n :: ns) + = case lookup n ps of + Nothing => insertDeps acc ps ns + Just pos => if pos `elem` acc + then insertDeps acc ps ns + else insertDeps (pos :: acc) ps ns + + -- Collect the argument names which the dynamic args depend on + collectDDeps : NF [] -> Core (List Name) + collectDDeps (NBind tfc x (Pi _ _ _ nty) sc) + = do defs <- get Ctxt + empty <- clearDefs defs + sc' <- sc defs (toClosure defaultOpts [] (Ref tfc Bound x)) + if x `elem` ns + then collectDDeps sc' + else do aty <- quote empty [] nty + -- Get names depended on by nty + let deps = keys (getRefs (UN Underscore) aty) + rest <- collectDDeps sc' + pure (rest ++ deps) + collectDDeps _ = pure [] + + -- Return names the type depends on, and whether it's a parameter + mutual + getDepsArgs : Bool -> List (NF []) -> NameMap Bool -> + Core (NameMap Bool) + getDepsArgs inparam [] ns = pure ns + getDepsArgs inparam (a :: as) ns + = do ns' <- getDeps inparam a ns + getDepsArgs inparam as ns' + + getDeps : Bool -> NF [] -> NameMap Bool -> + Core (NameMap Bool) + getDeps inparam (NBind _ x (Pi _ _ _ pty) sc) ns + = do defs <- get Ctxt + ns' <- getDeps inparam !(evalClosure defs pty) ns + sc' <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder)) + getDeps inparam sc' ns' + getDeps inparam (NBind _ x b sc) ns + = do defs <- get Ctxt + ns' <- getDeps False !(evalClosure defs (binderType b)) ns + sc' <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder)) + getDeps False sc' ns + getDeps inparam (NApp _ (NRef Bound n) args) ns + = do defs <- get Ctxt + ns' <- getDepsArgs False !(traverse (evalClosure defs . snd) args) ns + pure (insert n inparam ns') + getDeps inparam (NDCon _ n t a args) ns + = do defs <- get Ctxt + getDepsArgs False !(traverse (evalClosure defs . snd) args) ns + getDeps inparam (NTCon _ n t a args) ns + = do defs <- get Ctxt + params <- case !(lookupDefExact n (gamma defs)) of + Just (TCon _ _ ps _ _ _ _ _) => pure ps + _ => pure [] + let (ps, ds) = splitPs 0 params (map snd args) + ns' <- getDepsArgs True !(traverse (evalClosure defs) ps) ns + getDepsArgs False !(traverse (evalClosure defs) ds) ns' + where + -- Split into arguments in parameter position, and others + splitPs : Nat -> List Nat -> List (Closure []) -> + (List (Closure []), List (Closure [])) + splitPs n params [] = ([], []) + splitPs n params (x :: xs) + = let (ps', ds') = splitPs (1 + n) params xs in + if n `elem` params + then (x :: ps', ds') + else (ps', x :: ds') + getDeps inparam (NDelayed _ _ t) ns = getDeps inparam t ns + getDeps inparams nf ns = pure ns + + -- If the name of an argument is in the list of specialisable arguments, + -- record the position. Also record the position of anything the argument + -- depends on which is only dependend on by declared static arguments. + collectSpec : List Nat -> -- specialisable so far + List Name -> -- things depended on by dynamic args + -- We're assuming it's a short list, so just use + -- List and don't worry about duplicates. + List (Name, Nat) -> NF [] -> Core (List Nat) + collectSpec acc ddeps ps (NBind tfc x (Pi _ _ _ nty) sc) + = do defs <- get Ctxt + empty <- clearDefs defs + sc' <- sc defs (toClosure defaultOpts [] (Ref tfc Bound x)) + if x `elem` ns + then do deps <- getDeps True !(evalClosure defs nty) NameMap.empty + -- Get names depended on by nty + -- Keep the ones which are either: + -- * parameters + -- * not depended on by a dynamic argument (the ddeps) + let rs = filter (\x => snd x || + not (fst x `elem` ddeps)) + (toList deps) + let acc' = insertDeps acc ps (x :: map fst rs) + collectSpec acc' ddeps ps sc' + else collectSpec acc ddeps ps sc' + collectSpec acc ddeps ps _ = pure acc + + getNamePos : Nat -> NF [] -> Core (List (Name, Nat)) + getNamePos i (NBind tfc x (Pi _ _ _ _) sc) + = do defs <- get Ctxt + ns' <- getNamePos (1 + i) !(sc defs (toClosure defaultOpts [] (Erased tfc Placeholder))) + pure ((x, i) :: ns') + getNamePos _ _ = pure [] diff --git a/src/TTImp/ProcessType.idr b/src/TTImp/ProcessType.idr index 40b13c4fb..748bd3c7e 100644 --- a/src/TTImp/ProcessType.idr +++ b/src/TTImp/ProcessType.idr @@ -17,6 +17,7 @@ import Idris.Syntax import TTImp.Elab.Check import TTImp.Elab.Utils import TTImp.Elab +import TTImp.ProcessFnOpt import TTImp.TTImp import Data.List @@ -27,174 +28,6 @@ import Libraries.Data.StringMap %default covering -getRetTy : Defs -> NF [] -> Core Name -getRetTy defs (NBind fc _ (Pi _ _ _ _) sc) - = getRetTy defs !(sc defs (toClosure defaultOpts [] (Erased fc Placeholder))) -getRetTy defs (NTCon _ n _ _ _) = pure n -getRetTy defs ty - = throw (GenericMsg (getLoc ty) - "Can only add hints for concrete return types") - -throwIfHasFlag : {auto c : Ref Ctxt Defs} -> FC -> Name -> DefFlag -> String -> Core () -throwIfHasFlag fc ndef fl msg - = when !(hasFlag fc ndef fl) $ throw (GenericMsg fc msg) - -processFnOpt : {auto c : Ref Ctxt Defs} -> - FC -> Bool -> -- ^ top level name? - Name -> FnOpt -> Core () -processFnOpt fc _ ndef Unsafe - = do setIsEscapeHatch fc ndef -processFnOpt fc _ ndef Inline - = do throwIfHasFlag fc ndef NoInline "%noinline and %inline are mutually exclusive" - setFlag fc ndef Inline -processFnOpt fc _ ndef NoInline - = do throwIfHasFlag fc ndef Inline "%inline and %noinline are mutually exclusive" - setFlag fc ndef NoInline -processFnOpt fc _ ndef Deprecate - = setFlag fc ndef Deprecate -processFnOpt fc _ ndef TCInline - = setFlag fc ndef TCInline -processFnOpt fc True ndef (Hint d) - = do defs <- get Ctxt - Just ty <- lookupTyExact ndef (gamma defs) - | Nothing => undefinedName fc ndef - target <- getRetTy defs !(nf defs [] ty) - addHintFor fc target ndef d False -processFnOpt fc _ ndef (Hint d) - = do logC "elab" 5 $ do pure $ "Adding local hint " ++ show !(toFullNames ndef) - addLocalHint ndef -processFnOpt fc True ndef (GlobalHint a) - = addGlobalHint ndef a -processFnOpt fc _ ndef (GlobalHint a) - = throw (GenericMsg fc "%globalhint is not valid in local definitions") -processFnOpt fc _ ndef ExternFn - = setFlag fc ndef Inline -- if externally defined, inline when compiling -processFnOpt fc _ ndef (ForeignFn _) - = setFlag fc ndef Inline -- if externally defined, inline when compiling -processFnOpt fc _ ndef (ForeignExport _) - = pure () -processFnOpt fc _ ndef Invertible - = setFlag fc ndef Invertible -processFnOpt fc _ ndef (Totality tot) - = setFlag fc ndef (SetTotal tot) -processFnOpt fc _ ndef Macro - = setFlag fc ndef Macro -processFnOpt fc _ ndef (SpecArgs ns) - = do defs <- get Ctxt - Just gdef <- lookupCtxtExact ndef (gamma defs) - | Nothing => undefinedName fc ndef - nty <- nf defs [] (type gdef) - ps <- getNamePos 0 nty - ddeps <- collectDDeps nty - specs <- collectSpec [] ddeps ps nty - ignore $ addDef ndef ({ specArgs := specs } gdef) - where - insertDeps : List Nat -> List (Name, Nat) -> List Name -> List Nat - insertDeps acc ps [] = acc - insertDeps acc ps (n :: ns) - = case lookup n ps of - Nothing => insertDeps acc ps ns - Just pos => if pos `elem` acc - then insertDeps acc ps ns - else insertDeps (pos :: acc) ps ns - - -- Collect the argument names which the dynamic args depend on - collectDDeps : NF [] -> Core (List Name) - collectDDeps (NBind tfc x (Pi _ _ _ nty) sc) - = do defs <- get Ctxt - empty <- clearDefs defs - sc' <- sc defs (toClosure defaultOpts [] (Ref tfc Bound x)) - if x `elem` ns - then collectDDeps sc' - else do aty <- quote empty [] nty - -- Get names depended on by nty - let deps = keys (getRefs (UN Underscore) aty) - rest <- collectDDeps sc' - pure (rest ++ deps) - collectDDeps _ = pure [] - - -- Return names the type depends on, and whether it's a parameter - mutual - getDepsArgs : Bool -> List (NF []) -> NameMap Bool -> - Core (NameMap Bool) - getDepsArgs inparam [] ns = pure ns - getDepsArgs inparam (a :: as) ns - = do ns' <- getDeps inparam a ns - getDepsArgs inparam as ns' - - getDeps : Bool -> NF [] -> NameMap Bool -> - Core (NameMap Bool) - getDeps inparam (NBind _ x (Pi _ _ _ pty) sc) ns - = do defs <- get Ctxt - ns' <- getDeps inparam !(evalClosure defs pty) ns - sc' <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder)) - getDeps inparam sc' ns' - getDeps inparam (NBind _ x b sc) ns - = do defs <- get Ctxt - ns' <- getDeps False !(evalClosure defs (binderType b)) ns - sc' <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder)) - getDeps False sc' ns - getDeps inparam (NApp _ (NRef Bound n) args) ns - = do defs <- get Ctxt - ns' <- getDepsArgs False !(traverse (evalClosure defs . snd) args) ns - pure (insert n inparam ns') - getDeps inparam (NDCon _ n t a args) ns - = do defs <- get Ctxt - getDepsArgs False !(traverse (evalClosure defs . snd) args) ns - getDeps inparam (NTCon _ n t a args) ns - = do defs <- get Ctxt - params <- case !(lookupDefExact n (gamma defs)) of - Just (TCon _ _ ps _ _ _ _ _) => pure ps - _ => pure [] - let (ps, ds) = splitPs 0 params (map snd args) - ns' <- getDepsArgs True !(traverse (evalClosure defs) ps) ns - getDepsArgs False !(traverse (evalClosure defs) ds) ns' - where - -- Split into arguments in parameter position, and others - splitPs : Nat -> List Nat -> List (Closure []) -> - (List (Closure []), List (Closure [])) - splitPs n params [] = ([], []) - splitPs n params (x :: xs) - = let (ps', ds') = splitPs (1 + n) params xs in - if n `elem` params - then (x :: ps', ds') - else (ps', x :: ds') - getDeps inparam (NDelayed _ _ t) ns = getDeps inparam t ns - getDeps inparams nf ns = pure ns - - -- If the name of an argument is in the list of specialisable arguments, - -- record the position. Also record the position of anything the argument - -- depends on which is only dependend on by declared static arguments. - collectSpec : List Nat -> -- specialisable so far - List Name -> -- things depended on by dynamic args - -- We're assuming it's a short list, so just use - -- List and don't worry about duplicates. - List (Name, Nat) -> NF [] -> Core (List Nat) - collectSpec acc ddeps ps (NBind tfc x (Pi _ _ _ nty) sc) - = do defs <- get Ctxt - empty <- clearDefs defs - sc' <- sc defs (toClosure defaultOpts [] (Ref tfc Bound x)) - if x `elem` ns - then do deps <- getDeps True !(evalClosure defs nty) NameMap.empty - -- Get names depended on by nty - -- Keep the ones which are either: - -- * parameters - -- * not depended on by a dynamic argument (the ddeps) - let rs = filter (\x => snd x || - not (fst x `elem` ddeps)) - (toList deps) - let acc' = insertDeps acc ps (x :: map fst rs) - collectSpec acc' ddeps ps sc' - else collectSpec acc ddeps ps sc' - collectSpec acc ddeps ps _ = pure acc - - getNamePos : Nat -> NF [] -> Core (List (Name, Nat)) - getNamePos i (NBind tfc x (Pi _ _ _ _) sc) - = do defs <- get Ctxt - ns' <- getNamePos (1 + i) !(sc defs (toClosure defaultOpts [] (Erased tfc Placeholder))) - pure ((x, i) :: ns') - getNamePos _ _ = pure [] - getFnString : {auto c : Ref Ctxt Defs} -> {auto m : Ref MD Metadata} -> {auto u : Ref UST UState} -> diff --git a/src/TTImp/Reflect.idr b/src/TTImp/Reflect.idr index 68e3a0891..cc007cbf0 100644 --- a/src/TTImp/Reflect.idr +++ b/src/TTImp/Reflect.idr @@ -118,12 +118,13 @@ mutual val' <- reify defs !(evalClosure defs val) sc' <- reify defs !(evalClosure defs sc) pure (ILet fc' lhsFC' c' n' ty' val' sc') - (UN (Basic "ICase"), [fc, sc, ty, cs]) + (UN (Basic "ICase"), [fc, opts, sc, ty, cs]) => do fc' <- reify defs !(evalClosure defs fc) + opts' <- reify defs !(evalClosure defs opts) sc' <- reify defs !(evalClosure defs sc) ty' <- reify defs !(evalClosure defs ty) cs' <- reify defs !(evalClosure defs cs) - pure (ICase fc' sc' ty' cs') + pure (ICase fc' opts' sc' ty' cs') (UN (Basic "ILocal"), [fc, ds, sc]) => do fc' <- reify defs !(evalClosure defs fc) ds' <- reify defs !(evalClosure defs ds) @@ -501,12 +502,13 @@ mutual aval' <- reflect fc defs lhs env aval sc' <- reflect fc defs lhs env sc appCon fc defs (reflectionttimp "ILet") [fc', lhsFC', c', n', aty', aval', sc'] - reflect fc defs lhs env (ICase tfc sc ty cs) + reflect fc defs lhs env (ICase tfc opts sc ty cs) = do fc' <- reflect fc defs lhs env tfc + opts' <- reflect fc defs lhs env opts sc' <- reflect fc defs lhs env sc ty' <- reflect fc defs lhs env ty cs' <- reflect fc defs lhs env cs - appCon fc defs (reflectionttimp "ICase") [fc', sc', ty', cs'] + appCon fc defs (reflectionttimp "ICase") [fc', opts', sc', ty', cs'] reflect fc defs lhs env (ILocal tfc ds sc) = do fc' <- reflect fc defs lhs env tfc ds' <- reflect fc defs lhs env ds diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 0c1bd6e12..71f685794 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -68,7 +68,7 @@ mutual ILet : FC -> (lhsFC : FC) -> RigCount -> Name -> (nTy : RawImp' nm) -> (nVal : RawImp' nm) -> (scope : RawImp' nm) -> RawImp' nm - ICase : FC -> RawImp' nm -> (ty : RawImp' nm) -> + ICase : FC -> List (FnOpt' nm) -> RawImp' nm -> (ty : RawImp' nm) -> List (ImpClause' nm) -> RawImp' nm ILocal : FC -> List (ImpDecl' nm) -> RawImp' nm -> RawImp' nm -- Local definitions made elsewhere, but that we're pushing @@ -163,7 +163,7 @@ mutual show (ILet fc lhsFC c n ty val sc) = "(%let " ++ show c ++ " " ++ " " ++ show n ++ " " ++ show ty ++ " " ++ show val ++ " " ++ show sc ++ ")" - show (ICase _ scr scrty alts) + show (ICase _ _ scr scrty alts) = "(%case (" ++ show scr ++ " : " ++ show scrty ++ ") " ++ show alts ++ ")" show (ILocal _ def scope) = "(%local (" ++ show def ++ ") " ++ show scope ++ ")" @@ -844,7 +844,7 @@ getFC (IVar x _) = x getFC (IPi x _ _ _ _ _) = x getFC (ILam x _ _ _ _ _) = x getFC (ILet x _ _ _ _ _ _) = x -getFC (ICase x _ _ _) = x +getFC (ICase x _ _ _ _) = x getFC (ILocal x _ _) = x getFC (ICaseLocal x _ _ _ _) = x getFC (IUpdate x _ _) = x diff --git a/src/TTImp/TTImp/Functor.idr b/src/TTImp/TTImp/Functor.idr index ecd33bcad..8504c72f3 100644 --- a/src/TTImp/TTImp/Functor.idr +++ b/src/TTImp/TTImp/Functor.idr @@ -16,8 +16,8 @@ mutual = ILam fc rig (map (map f) info) nm (map f a) (map f sc) map f (ILet fc lhsFC rig nm ty val sc) = ILet fc lhsFC rig nm (map f ty) (map f val) (map f sc) - map f (ICase fc sc ty cls) - = ICase fc (map f sc) (map f ty) (map (map f) cls) + map f (ICase fc opts sc ty cls) + = ICase fc (map (map f) opts) (map f sc) (map f ty) (map (map f) cls) map f (ILocal fc ds sc) = ILocal fc (map (map f) ds) (map f sc) map f (ICaseLocal fc userN intN args sc) diff --git a/src/TTImp/TTImp/TTC.idr b/src/TTImp/TTImp/TTC.idr index 7a7052455..4548995c5 100644 --- a/src/TTImp/TTImp/TTC.idr +++ b/src/TTImp/TTImp/TTC.idr @@ -23,8 +23,8 @@ mutual toBuf b (ILet fc lhsFC r n nTy nVal scope) = do tag 3; toBuf b fc; toBuf b lhsFC; toBuf b r; toBuf b n; toBuf b nTy; toBuf b nVal; toBuf b scope - toBuf b (ICase fc y ty xs) - = do tag 4; toBuf b fc; toBuf b y; toBuf b ty; toBuf b xs + toBuf b (ICase fc opts y ty xs) + = do tag 4; toBuf b fc; toBuf b opts; toBuf b y; toBuf b ty; toBuf b xs toBuf b (ILocal fc xs sc) = do tag 5; toBuf b fc; toBuf b xs; toBuf b sc toBuf b (ICaseLocal fc _ _ _ sc) @@ -109,9 +109,9 @@ mutual nTy <- fromBuf b; nVal <- fromBuf b scope <- fromBuf b pure (ILet fc lhsFC r n nTy nVal scope) - 4 => do fc <- fromBuf b; y <- fromBuf b; + 4 => do fc <- fromBuf b; opts <- fromBuf b; y <- fromBuf b; ty <- fromBuf b; xs <- fromBuf b - pure (ICase fc y ty xs) + pure (ICase fc opts y ty xs) 5 => do fc <- fromBuf b; xs <- fromBuf b; sc <- fromBuf b pure (ILocal fc xs sc) diff --git a/src/TTImp/TTImp/Traversals.idr b/src/TTImp/TTImp/Traversals.idr index b44e4db99..110d68421 100644 --- a/src/TTImp/TTImp/Traversals.idr +++ b/src/TTImp/TTImp/Traversals.idr @@ -94,8 +94,8 @@ parameters (f : RawImp' nm -> RawImp' nm) = f $ ILam fc rig (mapPiInfo pinfo) x (mapTTImp argTy) (mapTTImp lamTy) mapTTImp (ILet fc lhsFC rig n nTy nVal scope) = f $ ILet fc lhsFC rig n (mapTTImp nTy) (mapTTImp nVal) (mapTTImp scope) - mapTTImp (ICase fc t ty cls) - = f $ ICase fc (mapTTImp t) (mapTTImp ty) (assert_total $ map mapImpClause cls) + mapTTImp (ICase fc opts t ty cls) + = f $ ICase fc opts (mapTTImp t) (mapTTImp ty) (assert_total $ map mapImpClause cls) mapTTImp (ILocal fc xs t) = f $ ILocal fc (assert_total $ map mapImpDecl xs) (mapTTImp t) mapTTImp (ICaseLocal fc unm inm args t) = f $ ICaseLocal fc unm inm args (mapTTImp t) diff --git a/src/TTImp/Unelab.idr b/src/TTImp/Unelab.idr index 5e8a96881..825250820 100644 --- a/src/TTImp/Unelab.idr +++ b/src/TTImp/Unelab.idr @@ -165,7 +165,8 @@ mutual (tm, _) <- unelabTy Full nest env scrutinee Just pats' <- map sequence $ traverse (mkClause fc argpos args) pats | _ => pure Nothing - pure $ Just $ ICase fc tm (Implicit fc False) pats' + -- TODO: actually grab the fnopts? + pure $ Just $ ICase fc [] tm (Implicit fc False) pats' dropParams : {auto c : Ref Ctxt Defs} -> List (Name, Nat) -> (IRawImp, Glued vars) -> diff --git a/src/TTImp/Utils.idr b/src/TTImp/Utils.idr index 5dc4e0f72..5fa57d8f3 100644 --- a/src/TTImp/Utils.idr +++ b/src/TTImp/Utils.idr @@ -131,7 +131,7 @@ findBindableNamesQuot env used (ILam fc x y z argTy lamTy) = findBindableNamesQuot env used ![argTy, lamTy] findBindableNamesQuot env used (ILet fc lhsfc x y nTy nVal scope) = findBindableNamesQuot env used ![nTy, nVal, scope] -findBindableNamesQuot env used (ICase fc x ty xs) +findBindableNamesQuot env used (ICase fc _ x ty xs) = findBindableNamesQuot env used !([x, ty] ++ getRawImp !xs) where getRawImp : ImpClause -> List RawImp getRawImp (PatClause fc1 lhs rhs) = [lhs, rhs] @@ -319,9 +319,10 @@ mutual ILet fc lhsFC r n (substNames' bvar bound ps nTy) (substNames' bvar bound ps nVal) (substNames' bvar bound' ps scope) - substNames' bvar bound ps (ICase fc y ty xs) - = ICase fc (substNames' bvar bound ps y) (substNames' bvar bound ps ty) - (map (substNamesClause' bvar bound ps) xs) + substNames' bvar bound ps (ICase fc opts y ty xs) + = ICase fc opts + (substNames' bvar bound ps y) (substNames' bvar bound ps ty) + (map (substNamesClause' bvar bound ps) xs) substNames' bvar bound ps (ILocal fc xs y) = let bound' = definedInBlock emptyNS xs ++ bound in ILocal fc (map (substNamesDecl' bvar bound ps) xs) @@ -426,8 +427,8 @@ mutual = ILet fc' fc' r n (substLoc fc' nTy) (substLoc fc' nVal) (substLoc fc' scope) - substLoc fc' (ICase fc y ty xs) - = ICase fc' (substLoc fc' y) (substLoc fc' ty) + substLoc fc' (ICase fc opts y ty xs) + = ICase fc' opts (substLoc fc' y) (substLoc fc' ty) (map (substLocClause fc') xs) substLoc fc' (ILocal fc xs y) = ILocal fc' (map (substLocDecl fc') xs) diff --git a/src/TTImp/WithClause.idr b/src/TTImp/WithClause.idr index e967afd62..c48148f4c 100644 --- a/src/TTImp/WithClause.idr +++ b/src/TTImp/WithClause.idr @@ -251,8 +251,8 @@ withRHS fc drop wname wargnames tm toplhs = pure $ ILam fc c p n !(wrhs ty) !(wrhs sc) wrhs (ILet fc lhsFC c n ty val sc) = pure $ ILet fc lhsFC c n !(wrhs ty) !(wrhs val) !(wrhs sc) - wrhs (ICase fc sc ty clauses) - = pure $ ICase fc !(wrhs sc) !(wrhs ty) !(traverse wrhsC clauses) + wrhs (ICase fc opts sc ty clauses) + = pure $ ICase fc opts !(wrhs sc) !(wrhs ty) !(traverse wrhsC clauses) wrhs (ILocal fc decls sc) = pure $ ILocal fc decls !(wrhs sc) -- TODO! wrhs (IUpdate fc upds tm) diff --git a/tests/Main.idr b/tests/Main.idr index 10fa4f05a..e30b721df 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -47,6 +47,7 @@ idrisTestsBasic = MkTestPool "Fundamental language features" [] Nothing "idiom001", "literals001", "dotted001", + "case001", "rewrite001", "interpolation001", "interpolation002", "interpolation003", "interpolation004"] diff --git a/tests/idris2/case001/InlineCase.idr b/tests/idris2/case001/InlineCase.idr new file mode 100644 index 000000000..e514bbb2a --- /dev/null +++ b/tests/idris2/case001/InlineCase.idr @@ -0,0 +1,27 @@ +module InlineCase + +data BTree : Type where + Leaf : BTree + Node : BTree -> Nat -> BTree -> BTree + +product : BTree -> Nat +product Leaf = 1 +product (Node l n r) + = %inline case n of + Z => Z + _ => %inline case product l of + Z => Z + pl => %inline case product r of + Z => Z + pr => pl * n * pr + +myfun : Nat -> Nat +myfun Z = Z +myfun n = S $ case n of + Z => Z + S n => myfun n + +main : IO () +main = do + l <- getLine + print (product $ Node Leaf (length l) Leaf) diff --git a/tests/idris2/case001/expected b/tests/idris2/case001/expected new file mode 100644 index 000000000..1b6f58dee --- /dev/null +++ b/tests/idris2/case001/expected @@ -0,0 +1 @@ +(define InlineCase-product (lambda (arg-0) (case (vector-ref arg-0 0) ((0) 1) (else (let ((e-0 (vector-ref arg-0 1))) (let ((e-1 (vector-ref arg-0 2))) (let ((e-2 (vector-ref arg-0 3))) (cond ((equal? e-1 0) 0)(else (let ((sc1 (InlineCase-product e-0))) (cond ((equal? sc1 0) 0)(else (let ((sc1 (InlineCase-product e-2))) (cond ((equal? sc1 0) 0)(else (* (* (InlineCase-product e-0) e-1) (InlineCase-product e-2))))))))))))))))) diff --git a/tests/idris2/case001/run b/tests/idris2/case001/run new file mode 100755 index 000000000..167500c1d --- /dev/null +++ b/tests/idris2/case001/run @@ -0,0 +1,4 @@ +rm -rf build + +$1 --no-color --console-width 0 --no-banner --codegen chez InlineCase.idr -o inline-case +grep "define InlineCase-product" build/exec/inline-case_app/inline-case.ss \ No newline at end of file diff --git a/tests/idris2/reg033/DerivingEq.idr b/tests/idris2/reg033/DerivingEq.idr index 84d4dd890..1fcfffaea 100644 --- a/tests/idris2/reg033/DerivingEq.idr +++ b/tests/idris2/reg033/DerivingEq.idr @@ -37,7 +37,7 @@ genEq typeName = do finalClause = PatClause pos `(_) `(False) clauses <- traverse makeClause constrs let allClauses = clauses ++ [finalClause] - caseExpr = ICase pos `(MkPair x y) (Implicit pos True) allClauses + caseExpr = ICase pos [] `(MkPair x y) (Implicit pos True) allClauses result = `(\x, y => ~(caseExpr)) check result %logging 0