From 419a440dad1ca4c26f3c7a8ac2fb6c77d2e03812 Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Fri, 13 Oct 2023 17:26:42 +0300 Subject: [PATCH] [ impl ] Support `default` implicits in named implementations (#3100) --- CHANGELOG.md | 1 + src/Idris/Desugar.idr | 21 ++++++---- src/Idris/Elab/Implementation.idr | 29 ++++++++----- src/Idris/Parser.idr | 41 +++++++++++-------- src/Idris/Syntax.idr | 2 +- src/Idris/Syntax/Traversals.idr | 12 +++--- .../interface030/DefaultImplicitsInImpls.idr | 20 +++++++++ tests/idris2/interface/interface030/expected | 1 + tests/idris2/interface/interface030/run | 3 ++ 9 files changed, 88 insertions(+), 42 deletions(-) create mode 100644 tests/idris2/interface/interface030/DefaultImplicitsInImpls.idr create mode 100644 tests/idris2/interface/interface030/expected create mode 100644 tests/idris2/interface/interface030/run diff --git a/CHANGELOG.md b/CHANGELOG.md index fa1e22fc7a..7525577ded 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -20,6 +20,7 @@ * New `fromTTImp`, `fromName`, and `fromDecls` names for custom `TTImp`, `Name`, and `Decls` literals. * Call to `%macro`-functions do not require the `ElabReflection` extension. +* Default implicits are supported for named implementations. * Elaborator scripts were made to be able to access project files, allowing the support for type providers and similar stuff. diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index d8aa6e32df..b206b3fd98 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -911,6 +911,15 @@ mutual = do tms' <- traverse (desugar AnyExpr ps) tms pure (ForeignExport tms') + %inline + mapDesugarPiInfo : {auto s : Ref Syn SyntaxInfo} -> + {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> + List Name -> PiInfo PTerm -> Core (PiInfo RawImp) + mapDesugarPiInfo ps = PiInfo.traverse (desugar AnyExpr ps) + -- Given a high level declaration, return a list of TTImp declarations -- which process it, and update any necessary state on the way. export @@ -1019,9 +1028,10 @@ mutual desugarDecl ps (PImplementation fc vis fnopts pass is cons tn params impln nusing body) = do opts <- traverse (desugarFnOpt ps) fnopts - is' <- for is $ \ (fc, c,n,tm) => + is' <- for is $ \ (fc, c, n, pi, tm) => do tm' <- desugar AnyExpr ps tm - pure (fc, c, n, tm') + pi' <- mapDesugarPiInfo ps pi + pure (fc, c, n, pi', tm') cons' <- for cons $ \ (n, tm) => do tm' <- desugar AnyExpr ps tm pure (n, tm') @@ -1034,13 +1044,13 @@ mutual $ findUniqueBindableNames fc True ps [] let paramsb = map (doBind bnames) params' - let isb = map (\ (info, r, n, tm) => (info, r, n, doBind bnames tm)) is' + let isb = map (\ (info, r, n, p, tm) => (info, r, n, p, doBind bnames tm)) is' let consb = map (\(n, tm) => (n, doBind bnames tm)) cons' body' <- maybe (pure Nothing) (\b => do b' <- traverse (desugarDecl ps) b pure (Just (concat b'))) body - -- calculate the name of the interface, if it's not explicitly + -- calculate the name of the implementation, if it's not explicitly -- given. let impname = maybe (mkImplName fc tn paramsb) id impln @@ -1102,9 +1112,6 @@ mutual NS ns (DN str (MN ("__mk" ++ str) 0)) mkConName n = DN (show n) (MN ("__mk" ++ show n) 0) - mapDesugarPiInfo : List Name -> PiInfo PTerm -> Core (PiInfo RawImp) - mapDesugarPiInfo ps = traverse (desugar AnyExpr ps) - desugarDecl ps (PFixity fc vis fix prec opName) = do ctx <- get Ctxt -- We update the context of fixities by adding a namespaced fixity diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr index 1dc4301f4a..b263072629 100644 --- a/src/Idris/Elab/Implementation.idr +++ b/src/Idris/Elab/Implementation.idr @@ -47,10 +47,10 @@ bindConstraints fc p [] ty = ty bindConstraints fc p ((n, ty) :: rest) sc = IPi fc top p n ty (bindConstraints fc p rest sc) -bindImpls : List (FC, RigCount, Name, RawImp) -> RawImp -> RawImp +bindImpls : List (FC, RigCount, Name, PiInfo RawImp, RawImp) -> RawImp -> RawImp bindImpls [] ty = ty -bindImpls ((fc, r, n, ty) :: rest) sc - = IPi fc r Implicit (Just n) ty (bindImpls rest sc) +bindImpls ((fc, r, n, p, ty) :: rest) sc + = IPi fc r p (Just n) ty (bindImpls rest sc) addDefaults : FC -> Name -> (params : List (Name, RawImp)) -> -- parameters have been specialised, use them! @@ -99,11 +99,16 @@ addDefaults fc impName params allms defs body getMethImps : {vars : _} -> {auto c : Ref Ctxt Defs} -> Env Term vars -> Term vars -> - Core (List (Name, RigCount, RawImp)) + Core (List (Name, RigCount, Maybe RawImp, RawImp)) getMethImps env (Bind fc x (Pi fc' c Implicit ty) sc) = do rty <- map (map rawName) $ unelabNoSugar env ty ts <- getMethImps (Pi fc' c Implicit ty :: env) sc - pure ((x, c, rty) :: ts) + pure ((x, c, Nothing, rty) :: ts) +getMethImps env (Bind fc x (Pi fc' c (DefImplicit def) ty) sc) + = do rty <- map (map rawName) $ unelabNoSugar env ty + rdef <- map (map rawName) $ unelabNoSugar env def + ts <- getMethImps (Pi fc' c (DefImplicit def) ty :: env) sc + pure ((x, c, Just rdef, rty) :: ts) getMethImps env tm = pure [] export @@ -115,7 +120,7 @@ elabImplementation : {vars : _} -> {auto o : Ref ROpts REPLOpts} -> FC -> Visibility -> List FnOpt -> Pass -> Env Term vars -> NestedNames vars -> - (implicits : List (FC, RigCount, Name, RawImp)) -> + (implicits : List (FC, RigCount, Name, PiInfo RawImp, RawImp)) -> (constraints : List (Maybe Name, RawImp)) -> Name -> (ps : List RawImp) -> @@ -346,7 +351,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i -- When applying the method in the field for the record, eta expand -- the expected arguments based on the field type, so that implicits get -- inserted in the right place - mkMethField : List (Name, RigCount, RawImp) -> + mkMethField : List (Name, a) -> List (Name, List (Name, RigCount, PiInfo RawImp)) -> (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp) -> RawImp mkMethField methImps fldTys (topn, n, upds, c, treq, ty) @@ -378,16 +383,18 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i = do mn <- inCurrentNS (methName n) pure (dropNS n, IVar vfc mn) - bindImps : List (Name, RigCount, RawImp) -> RawImp -> RawImp + bindImps : List (Name, RigCount, Maybe RawImp, RawImp) -> RawImp -> RawImp bindImps [] ty = ty - bindImps ((n, c, t) :: ts) ty + bindImps ((n, c, Just def, t) :: ts) ty + = IPi vfc c (DefImplicit def) (Just n) t (bindImps ts ty) + bindImps ((n, c, Nothing, t) :: ts) ty = IPi vfc c Implicit (Just n) t (bindImps ts ty) -- Return method name, specialised method name, implicit name updates, -- and method type. Also return how the method name should be updated -- in later method types (specifically, putting implicits in) topMethType : List (Name, RawImp) -> - Name -> List (Name, RigCount, RawImp) -> + Name -> List (Name, RigCount, Maybe RawImp, RawImp) -> List String -> List Name -> List Name -> List Name -> Method -> Core ((Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp), @@ -445,7 +452,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i pure ((meth.name, n, upds, meth.count, meth.totalReq, mty), methupds') topMethTypes : List (Name, RawImp) -> - Name -> List (Name, RigCount, RawImp) -> + Name -> List (Name, RigCount, Maybe RawImp, RawImp) -> List String -> List Name -> List Name -> List Name -> List Method -> diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index d31360de44..30a7644653 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1594,6 +1594,16 @@ recordConstructor fname n <- mustWork $ decoratedDataConstructorName fname pure (doc, n) +autoImplicitField : OriginDesc -> IndentInfo -> Rule (PiInfo t) +autoImplicitField fname _ = AutoImplicit <$ decoratedKeyword fname "auto" + +defImplicitField : OriginDesc -> IndentInfo -> Rule (PiInfo PTerm) +defImplicitField fname indents = do + decoratedKeyword fname "default" + commit + t <- simpleExpr fname indents + pure (DefImplicit t) + constraints : OriginDesc -> IndentInfo -> EmptyRule (List (Maybe Name, PTerm)) constraints fname indents = do tm <- appExpr pdef fname indents @@ -1610,15 +1620,22 @@ constraints fname indents pure ((Just n, tm) :: more) <|> pure [] -implBinds : OriginDesc -> IndentInfo -> EmptyRule (List (FC, RigCount, Name, PTerm)) -implBinds fname indents = concatMap (map adjust) <$> go where +implBinds : OriginDesc -> IndentInfo -> (namedImpl : Bool) -> EmptyRule (List (FC, RigCount, Name, PiInfo PTerm, PTerm)) +implBinds fname indents namedImpl = concatMap (map adjust) <$> go where - adjust : (RigCount, WithBounds Name, PTerm) -> (FC, RigCount, Name, PTerm) + adjust : (RigCount, WithBounds Name, a) -> (FC, RigCount, Name, a) adjust (r, wn, ty) = (virtualiseFC (boundToFC fname wn), r, wn.val, ty) - go : EmptyRule (List (List (RigCount, WithBounds Name, PTerm))) + isDefaultImplicit : PiInfo a -> Bool + isDefaultImplicit (DefImplicit _) = True + isDefaultImplicit _ = False + + go : EmptyRule (List (List (RigCount, WithBounds Name, PiInfo PTerm, PTerm))) go = do decoratedSymbol fname "{" - ns <- pibindListName fname indents + piInfo <- bounds $ option Implicit $ defImplicitField fname indents + when (not namedImpl && isDefaultImplicit piInfo.val) $ + fatalLoc piInfo.bounds "Default implicits are allowed only for named implementations" + ns <- map @{Compose} (\(rc, wb, n) => (rc, wb, piInfo.val, n)) $ pibindListName fname indents commitSymbol fname "}" commitSymbol fname "->" more <- go @@ -1667,7 +1684,7 @@ implDecl fname indents iname <- optional $ decoratedSymbol fname "[" *> decorate fname Function name <* decoratedSymbol fname "]" - impls <- implBinds fname indents + impls <- implBinds fname indents (isJust iname) cons <- constraints fname indents n <- decorate fname Typ name params <- many (continue indents *> simpleExpr fname indents) @@ -1685,7 +1702,7 @@ fieldDecl fname indents = do doc <- optDocumentation fname decoratedSymbol fname "{" commit - impl <- option Implicit (autoImplicitField <|> defImplicitField) + impl <- option Implicit (autoImplicitField fname indents <|> defImplicitField fname indents) fs <- fieldBody doc impl decoratedSymbol fname "}" atEnd indents @@ -1695,16 +1712,6 @@ fieldDecl fname indents atEnd indents pure fs where - autoImplicitField : Rule (PiInfo t) - autoImplicitField = AutoImplicit <$ decoratedKeyword fname "auto" - - defImplicitField : Rule (PiInfo PTerm) - defImplicitField = do - decoratedKeyword fname "default" - commit - t <- simpleExpr fname indents - pure (DefImplicit t) - fieldBody : String -> PiInfo PTerm -> Rule (List PField) fieldBody doc p = do b <- bounds (do diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 8e746a0b3d..3abdb3d9ea 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -447,7 +447,7 @@ mutual PDecl' nm PImplementation : FC -> Visibility -> List PFnOpt -> Pass -> - (implicits : List (FC, RigCount, Name, PTerm' nm)) -> + (implicits : List (FC, RigCount, Name, PiInfo (PTerm' nm), PTerm' nm)) -> (constraints : List (Maybe Name, PTerm' nm)) -> Name -> (params : List (PTerm' nm)) -> diff --git a/src/Idris/Syntax/Traversals.idr b/src/Idris/Syntax/Traversals.idr index f57c13de63..b0648c5cbe 100644 --- a/src/Idris/Syntax/Traversals.idr +++ b/src/Idris/Syntax/Traversals.idr @@ -327,11 +327,11 @@ mapPTermM f = goPTerm where (::) . (\ c => (a, b, c)) <$> goPTerm t <*> go3TupledPTerms ts - goImplicits : List (x, y, z, PTerm' nm) -> - Core (List (x, y, z, PTerm' nm)) + goImplicits : List (x, y, z, PiInfo (PTerm' nm), PTerm' nm) -> + Core (List (x, y, z, PiInfo (PTerm' nm), PTerm' nm)) goImplicits [] = pure [] - goImplicits ((a, b, c, t) :: ts) = - ((::) . (a,b,c,)) <$> goPTerm t + goImplicits ((a, b, c, p, t) :: ts) = + ((::) . (a,b,c,)) <$> ((,) <$> goPiInfo p <*> goPTerm t) <*> goImplicits ts go4TupledPTerms : List (x, y, PiInfo (PTerm' nm), PTerm' nm) -> @@ -576,9 +576,9 @@ mapPTerm f = goPTerm where go3TupledPTerms [] = [] go3TupledPTerms ((a, b, t) :: ts) = (a, b, goPTerm t) :: go3TupledPTerms ts - goImplicits : List (x, y, z, PTerm' nm) -> List (x, y, z, PTerm' nm) + goImplicits : List (x, y, z, PiInfo (PTerm' nm), PTerm' nm) -> List (x, y, z, PiInfo (PTerm' nm), PTerm' nm) goImplicits [] = [] - goImplicits ((a, b, c, t) :: ts) = (a,b,c, goPTerm t) :: goImplicits ts + goImplicits ((a, b, c, p, t) :: ts) = (a,b,c, goPiInfo p, goPTerm t) :: goImplicits ts go4TupledPTerms : List (x, y, PiInfo (PTerm' nm), PTerm' nm) -> List (x, y, PiInfo (PTerm' nm), PTerm' nm) diff --git a/tests/idris2/interface/interface030/DefaultImplicitsInImpls.idr b/tests/idris2/interface/interface030/DefaultImplicitsInImpls.idr new file mode 100644 index 0000000000..0e196149f6 --- /dev/null +++ b/tests/idris2/interface/interface030/DefaultImplicitsInImpls.idr @@ -0,0 +1,20 @@ +module DefaultImplicitsInImpls + +import Data.Vect + +%default total + +[TunableImpl] {default False fancy : Bool} -> Show Nat where + show x = if fancy then "!!! hohoho !!!" else "no fancy" + +X0 : String +X0 = show @{TunableImpl} 5 + +x0Corr : X0 === "no fancy" +x0Corr = Refl + +X1 : String +X1 = show @{TunableImpl {fancy=True}} 5 + +x1Corr : X1 === "!!! hohoho !!!" +x1Corr = Refl diff --git a/tests/idris2/interface/interface030/expected b/tests/idris2/interface/interface030/expected new file mode 100644 index 0000000000..2eac914b83 --- /dev/null +++ b/tests/idris2/interface/interface030/expected @@ -0,0 +1 @@ +1/1: Building DefaultImplicitsInImpls (DefaultImplicitsInImpls.idr) diff --git a/tests/idris2/interface/interface030/run b/tests/idris2/interface/interface030/run new file mode 100644 index 0000000000..dcb75f8ca3 --- /dev/null +++ b/tests/idris2/interface/interface030/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check DefaultImplicitsInImpls.idr