From 55926f30c5becdd1dd0f51e7652647ef9aafa828 Mon Sep 17 00:00:00 2001 From: "G. Allais" Date: Wed, 14 Sep 2022 14:57:04 +0100 Subject: [PATCH] [ fix #2655 ] Add support for DataOpts in records (#2658) --- libs/base/Language/Reflection/TTImp.idr | 14 +++++---- src/Core/Binary.idr | 2 +- src/Idris/Desugar.idr | 4 +-- src/Idris/Desugar/Mutual.idr | 4 +-- src/Idris/Parser.idr | 27 +++++++++++------ src/Idris/Resugar.idr | 9 +++--- src/Idris/Syntax.idr | 3 +- src/Idris/Syntax/Traversals.idr | 7 +++-- src/TTImp/Elab/Local.idr | 3 +- src/TTImp/Elab/Quote.idr | 4 +-- src/TTImp/Parser.idr | 15 ++++++---- src/TTImp/ProcessRecord.idr | 9 +++--- src/TTImp/Reflect.idr | 10 ++++--- src/TTImp/TTImp.idr | 5 ++-- src/TTImp/TTImp/Functor.idr | 4 +-- src/TTImp/TTImp/TTC.idr | 8 ++--- src/TTImp/TTImp/Traversals.idr | 4 +-- src/TTImp/Utils.idr | 2 +- tests/Main.idr | 2 +- tests/idris2/record017/RecordOptions.idr | 38 ++++++++++++++++++++++++ tests/idris2/record017/expected | 1 + tests/idris2/record017/run | 3 ++ tests/idris2/reflection004/refdecl.idr | 2 +- 23 files changed, 123 insertions(+), 57 deletions(-) create mode 100644 tests/idris2/record017/RecordOptions.idr create mode 100644 tests/idris2/record017/expected create mode 100755 tests/idris2/record017/run diff --git a/libs/base/Language/Reflection/TTImp.idr b/libs/base/Language/Reflection/TTImp.idr index 51480cd50..b4c9f6c9b 100644 --- a/libs/base/Language/Reflection/TTImp.idr +++ b/libs/base/Language/Reflection/TTImp.idr @@ -157,6 +157,7 @@ mutual data Record : Type where MkRecord : FC -> (n : Name) -> (params : List (Name, Count, PiInfo TTImp, TTImp)) -> + (opts : List DataOpt) -> (conName : Name) -> (fields : List IField) -> Record @@ -368,8 +369,8 @@ parameters {auto eqTTImp : Eq TTImp} public export Eq Record where - MkRecord _ n ps cn fs == MkRecord _ n' ps' cn' fs' = - n == n' && ps == ps' && cn == cn' && fs == fs' + MkRecord _ n ps opts cn fs == MkRecord _ n' ps' opts' cn' fs' = + n == n' && ps == ps' && opts == opts' && cn == cn' && fs == fs' public export Eq Decl where @@ -460,7 +461,7 @@ mutual export Show Record where - show (MkRecord fc n params conName fields) + show (MkRecord fc n params opts conName fields) -- TODO: print opts = unwords [ "record", show n , unwords (map (\ (nm, rig, pinfo, ty) => @@ -747,8 +748,8 @@ parameters (f : TTImp -> TTImp) export mapRecord : Record -> Record - mapRecord (MkRecord fc n params conName fields) - = MkRecord fc n (map (map $ map $ bimap mapPiInfo mapTTImp) params) conName (map mapIField fields) + mapRecord (MkRecord fc n params opts conName fields) + = MkRecord fc n (map (map $ map $ bimap mapPiInfo mapTTImp) params) opts conName (map mapIField fields) export mapDecl : Decl -> Decl @@ -869,9 +870,10 @@ parameters {0 m : Type -> Type} {auto mon : Monad m} (f : TTImp -> m TTImp) export mapMRecord : Record -> m Record - mapMRecord (MkRecord fc n params conName fields) + mapMRecord (MkRecord fc n params opts conName fields) = MkRecord fc n <$> traverse (bitraverse pure $ bitraverse pure $ bitraverse mapMPiInfo mapMTTImp) params + <*> pure opts <*> pure conName <*> traverse mapMIField fields diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 969199c87..0cc267af1 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 = 20220425 * 100 + 0 +ttcVersion = 20220914 * 100 + 0 export checkTTCVersion : String -> Int -> Int -> Core () diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 81adf08aa..409a4ad99 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -985,7 +985,7 @@ mutual isNamed Nothing = False isNamed (Just _) = True - desugarDecl ps (PRecord fc doc vis mbtot tn params conname_in fields) + desugarDecl ps (PRecord fc doc vis mbtot tn params opts conname_in fields) = do addDocString tn doc params' <- traverse (\ (n,c,p,tm) => do tm' <- desugar AnyExpr ps tm @@ -1014,7 +1014,7 @@ mutual let conname = maybe (mkConName tn) id conname_in let _ = the Name conname pure [IRecord fc (Just recName) - vis mbtot (MkImpRecord fc tn paramsb conname fields')] + vis mbtot (MkImpRecord fc tn paramsb opts conname fields')] where fname : PField -> Name fname (MkField _ _ _ _ n _) = n diff --git a/src/Idris/Desugar/Mutual.idr b/src/Idris/Desugar/Mutual.idr index ec227ec13..f3a7645c2 100644 --- a/src/Idris/Desugar/Mutual.idr +++ b/src/Idris/Desugar/Mutual.idr @@ -23,7 +23,7 @@ getDecl AsType d@(PClaim _ _ _ _ _) = Just d getDecl AsType (PData fc doc vis mbtot (MkPData dfc tyn tyc _ _)) = Just (PData fc doc vis mbtot (MkPLater dfc tyn tyc)) getDecl AsType d@(PInterface _ _ _ _ _ _ _ _ _) = Just d -getDecl AsType d@(PRecord fc doc vis mbtot n ps _ _) +getDecl AsType d@(PRecord fc doc vis mbtot n ps _ _ _) = Just (PData fc doc vis mbtot (MkPLater fc n (mkRecType ps))) where mkRecType : List (Name, RigCount, PiInfo PTerm, PTerm) -> PTerm @@ -36,7 +36,7 @@ getDecl AsType d = Nothing getDecl AsDef (PClaim _ _ _ _ _) = Nothing getDecl AsDef d@(PData _ _ _ _ (MkPLater _ _ _)) = Just d getDecl AsDef (PInterface _ _ _ _ _ _ _ _ _) = Nothing -getDecl AsDef d@(PRecord _ _ _ _ _ _ _ _) = Just d +getDecl AsDef d@(PRecord _ _ _ _ _ _ _ _ _) = Just d getDecl AsDef (PFixity _ _ _ _) = Nothing getDecl AsDef (PDirective _ _) = Nothing getDecl AsDef d = Just d diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 152fe26f9..8e7ad0df4 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1177,13 +1177,21 @@ simpleData fname start tyName indents pure (MkPData (boundToFC fname (mergeBounds start b)) tyName.val (mkTyConType fname tyfc params) [] cons) -dataOpt : Rule DataOpt -dataOpt - = (exactIdent "noHints" $> NoHints) - <|> (exactIdent "uniqueSearch" $> UniqueSearch) - <|> (exactIdent "search" *> SearchBy <$> forget <$> some name) - <|> (exactIdent "external" $> External) - <|> (exactIdent "noNewtype" $> NoNewtype) +dataOpt : OriginDesc -> Rule DataOpt +dataOpt fname + = (decorate fname Keyword (exactIdent "noHints") $> NoHints) + <|> (decorate fname Keyword (exactIdent "uniqueSearch") $> UniqueSearch) + <|> (do decorate fname Keyword (exactIdent "search") + SearchBy <$> forget <$> some (decorate fname Bound name)) + <|> (decorate fname Keyword (exactIdent "external") $> External) + <|> (decorate fname Keyword (exactIdent "noNewtype") $> NoNewtype) + +dataOpts : OriginDesc -> EmptyRule (List DataOpt) +dataOpts fname = option [] $ do + decoratedSymbol fname "[" + opts <- sepBy1 (decoratedSymbol fname ",") (dataOpt fname) + decoratedSymbol fname "]" + pure (forget opts) dataBody : OriginDesc -> Int -> WithBounds t -> Name -> IndentInfo -> PTerm -> EmptyRule PDataDecl @@ -1191,7 +1199,7 @@ dataBody fname mincol start n indents ty = do atEndIndent indents pure (MkPLater (boundToFC fname start) n ty) <|> do b <- bounds (do decoratedKeyword fname "where" - opts <- option [] $ decoratedSymbol fname "[" *> forget <$> sepBy1 (decoratedSymbol fname ",") dataOpt <* decoratedSymbol fname "]" + opts <- dataOpts fname cs <- blockAfter mincol (tyDecls (mustWork $ decoratedDataConstructorName fname) "" fname) pure (opts, concatMap forget cs)) (opts, cs) <- pure b.val @@ -1674,10 +1682,11 @@ recordDecl fname indents paramss <- many (recordParam fname indents) let params = concat paramss decoratedKeyword fname "where" + opts <- dataOpts fname dcflds <- blockWithOptHeaderAfter col (\ idt => recordConstructor fname <* atEnd idt) (fieldDecl fname) - pure (\fc : FC => PRecord fc doc vis mbtot n params (fst dcflds) (concat (snd dcflds)))) + pure (\fc : FC => PRecord fc doc vis mbtot n params opts (fst dcflds) (concat (snd dcflds)))) pure (b.val (boundToFC fname b)) paramDecls : OriginDesc -> IndentInfo -> Rule PDecl diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index 9f4b95f65..d37d2a0a3 100644 --- a/src/Idris/Resugar.idr +++ b/src/Idris/Resugar.idr @@ -486,15 +486,16 @@ mutual ImpRecord' KindedName -> Core ( Name , List (Name, RigCount, PiInfo IPTerm, IPTerm) + , List DataOpt , Maybe Name , List (PField' KindedName)) - toPRecord (MkImpRecord fc n ps con fs) + toPRecord (MkImpRecord fc n ps opts con fs) = do ps' <- traverse (\ (n, c, p, ty) => do ty' <- toPTerm startPrec ty p' <- mapPiInfo p pure (n, c, p', ty')) ps fs' <- traverse toPField fs - pure (n, ps', Just con, fs') + pure (n, ps', opts, Just con, fs') where mapPiInfo : PiInfo IRawImp -> Core (PiInfo IPTerm) mapPiInfo Explicit = pure Explicit @@ -529,8 +530,8 @@ mutual pure (n, rig, info', tpe')) ps) (catMaybes ds'))) toPDecl (IRecord fc _ vis mbtot r) - = do (n, ps, con, fs) <- toPRecord r - pure (Just (PRecord fc "" vis mbtot n ps con fs)) + = do (n, ps, opts, con, fs) <- toPRecord r + pure (Just (PRecord fc "" vis mbtot n ps opts con fs)) toPDecl (IFail fc msg ds) = do ds' <- traverse toPDecl ds pure (Just (PFail fc msg (catMaybes ds'))) diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index cc275b032..cbf5991f6 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -410,6 +410,7 @@ mutual Visibility -> Maybe TotalReq -> Name -> (params : List (Name, RigCount, PiInfo (PTerm' nm), PTerm' nm)) -> + (opts : List DataOpt) -> (conName : Maybe Name) -> List (PField' nm) -> PDecl' nm @@ -438,7 +439,7 @@ mutual getPDeclLoc (PReflect fc _) = fc getPDeclLoc (PInterface fc _ _ _ _ _ _ _ _) = fc getPDeclLoc (PImplementation fc _ _ _ _ _ _ _ _ _ _) = fc - getPDeclLoc (PRecord fc _ _ _ _ _ _ _) = fc + getPDeclLoc (PRecord fc _ _ _ _ _ _ _ _) = fc getPDeclLoc (PMutual fc _) = fc getPDeclLoc (PFail fc _ _) = fc getPDeclLoc (PFixity fc _ _ _) = fc diff --git a/src/Idris/Syntax/Traversals.idr b/src/Idris/Syntax/Traversals.idr index 8bbb02e0f..21475e024 100644 --- a/src/Idris/Syntax/Traversals.idr +++ b/src/Idris/Syntax/Traversals.idr @@ -256,8 +256,9 @@ mapPTermM f = goPTerm where <*> pure mn <*> pure ns <*> goMPDecls mps - goPDecl (PRecord fc doc v tot n nts mn fs) = + goPDecl (PRecord fc doc v tot n nts opts mn fs) = PRecord fc doc v tot n <$> go4TupledPTerms nts + <*> pure opts <*> pure mn <*> goPFields fs goPDecl (PFail fc msg ps) = PFail fc msg <$> goPDecls ps @@ -525,8 +526,8 @@ mapPTerm f = goPTerm where goPDecl (PImplementation fc v opts p is cs n ts mn ns mps) = PImplementation fc v opts p (goImplicits is) (goPairedPTerms cs) n (goPTerm <$> ts) mn ns (map (goPDecl <$>) mps) - goPDecl (PRecord fc doc v tot n nts mn fs) - = PRecord fc doc v tot n (go4TupledPTerms nts) mn (goPField <$> fs) + goPDecl (PRecord fc doc v tot n nts opts mn fs) + = PRecord fc doc v tot n (go4TupledPTerms nts) opts mn (goPField <$> fs) goPDecl (PFail fc msg ps) = PFail fc msg $ goPDecl <$> ps goPDecl (PMutual fc ps) = PMutual fc $ goPDecl <$> ps goPDecl p@(PFixity _ _ _ _) = p diff --git a/src/TTImp/Elab/Local.idr b/src/TTImp/Elab/Local.idr index 88f5ebadf..d4c7b81e4 100644 --- a/src/TTImp/Elab/Local.idr +++ b/src/TTImp/Elab/Local.idr @@ -127,9 +127,10 @@ localHelper {vars} nest env nestdecls_in func = MkIField fc rigc piinfo (newName nest n) rawimp updateRecordName : NestedNames vars -> ImpRecord -> ImpRecord - updateRecordName nest (MkImpRecord fc n params conName fields) + updateRecordName nest (MkImpRecord fc n params opts conName fields) = MkImpRecord fc (newName nest n) params + opts (newName nest conName) (map (updateFieldName nest) fields) diff --git a/src/TTImp/Elab/Quote.idr b/src/TTImp/Elab/Quote.idr index 9b60ef742..7f76a5fa3 100644 --- a/src/TTImp/Elab/Quote.idr +++ b/src/TTImp/Elab/Quote.idr @@ -123,8 +123,8 @@ mutual {auto u : Ref UST UState} -> ImpRecord -> Core ImpRecord - getUnquoteRecord (MkImpRecord fc n ps cn fs) - = pure $ MkImpRecord fc n !(traverse unqPair ps) cn + getUnquoteRecord (MkImpRecord fc n ps opts cn fs) + = pure $ MkImpRecord fc n !(traverse unqPair ps) opts cn !(traverse getUnquoteField fs) where unqPair : (Name, RigCount, PiInfo RawImp, RawImp) -> diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index 37d72fd71..34dae8e04 100644 --- a/src/TTImp/Parser.idr +++ b/src/TTImp/Parser.idr @@ -577,6 +577,13 @@ dataOpt ns <- forget <$> some name pure (SearchBy ns) +dataOpts : EmptyRule (List DataOpt) +dataOpts = option [] $ do + symbol "[" + dopts <- sepBy1 (symbol ",") dataOpt + symbol "]" + pure $ forget dopts + dataDecl : OriginDesc -> IndentInfo -> Rule ImpData dataDecl fname indents = do start <- location @@ -585,10 +592,7 @@ dataDecl fname indents symbol ":" ty <- expr fname indents keyword "where" - opts <- option [] (do symbol "[" - dopts <- sepBy1 (symbol ",") dataOpt - symbol "]" - pure $ forget dopts) + opts <- dataOpts cs <- block (tyDecl fname) end <- location pure (MkImpData (MkFC fname start end) n ty opts cs) @@ -650,13 +654,14 @@ recordDecl fname indents paramss <- many (recordParam fname indents) let params = concat paramss keyword "where" + opts <- dataOpts exactIdent "constructor" dc <- name flds <- assert_total (blockAfter col (fieldDecl fname)) end <- location pure (let fc = MkFC fname start end in IRecord fc Nothing vis mbtot - (MkImpRecord fc n params dc (concat flds))) + (MkImpRecord fc n params opts dc (concat flds))) namespaceDecl : Rule Namespace namespaceDecl diff --git a/src/TTImp/ProcessRecord.idr b/src/TTImp/ProcessRecord.idr index 16cec49ec..9e26560b6 100644 --- a/src/TTImp/ProcessRecord.idr +++ b/src/TTImp/ProcessRecord.idr @@ -49,10 +49,11 @@ elabRecord : {vars : _} -> NestedNames vars -> Maybe String -> Visibility -> Maybe TotalReq -> Name -> (params : List (Name, RigCount, PiInfo RawImp, RawImp)) -> + (opts : List DataOpt) -> (conName : Name) -> List IField -> Core () -elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params conName_in fields +elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params opts conName_in fields = do tn <- inCurrentNS tn_in conName <- inCurrentNS conName_in elabAsData tn conName @@ -130,7 +131,7 @@ elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params conName_in fiel let boundNames = paramNames ++ map fname fields ++ vars let con = MkImpTy EmptyFC EmptyFC cname !(bindTypeNames fc [] boundNames conty) - let dt = MkImpData fc tn !(bindTypeNames fc [] boundNames (mkDataTy fc params)) [] [con] + let dt = MkImpData fc tn !(bindTypeNames fc [] boundNames (mkDataTy fc params)) opts [con] log "declare.record" 5 $ "Record data type " ++ show dt processDecl [] nest env (IData fc vis mbtot dt) @@ -257,5 +258,5 @@ processRecord : {vars : _} -> Env Term vars -> Maybe String -> Visibility -> Maybe TotalReq -> ImpRecord -> Core () -processRecord eopts nest env newns vis mbtot (MkImpRecord fc n ps cons fs) - = elabRecord eopts fc env nest newns vis mbtot n ps cons fs +processRecord eopts nest env newns vis mbtot (MkImpRecord fc n ps opts cons fs) + = elabRecord eopts fc env nest newns vis mbtot n ps opts cons fs diff --git a/src/TTImp/Reflect.idr b/src/TTImp/Reflect.idr index 32df9c642..3364bc04f 100644 --- a/src/TTImp/Reflect.idr +++ b/src/TTImp/Reflect.idr @@ -367,13 +367,14 @@ mutual Reify ImpRecord where reify defs val@(NDCon _ n _ _ args) = case (dropAllNS !(full (gamma defs) n), map snd args) of - (UN (Basic "MkRecord"), [v,w,x,y,z]) + (UN (Basic "MkRecord"), [v,w,x,y,z,a]) => do v' <- reify defs !(evalClosure defs v) w' <- reify defs !(evalClosure defs w) x' <- reify defs !(evalClosure defs x) y' <- reify defs !(evalClosure defs y) z' <- reify defs !(evalClosure defs z) - pure (MkImpRecord v' w' x' y' z') + a' <- reify defs !(evalClosure defs a) + pure (MkImpRecord v' w' x' y' z' a') _ => cantReify val "Record" reify defs val = cantReify val "Record" @@ -723,13 +724,14 @@ mutual export Reflect ImpRecord where - reflect fc defs lhs env (MkImpRecord v w x y z) + reflect fc defs lhs env (MkImpRecord v w x y z a) = do v' <- reflect fc defs lhs env v w' <- reflect fc defs lhs env w x' <- reflect fc defs lhs env x y' <- reflect fc defs lhs env y z' <- reflect fc defs lhs env z - appCon fc defs (reflectionttimp "MkRecord") [v', w', x', y', z'] + a' <- reflect fc defs lhs env a + appCon fc defs (reflectionttimp "MkRecord") [v', w', x', y', z', a'] export Reflect WithFlag where diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 5e503818e..8f2c2e68e 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -365,6 +365,7 @@ mutual data ImpRecord' : Type -> Type where MkImpRecord : FC -> (n : Name) -> (params : List (ImpParameter' nm)) -> + (opts : List DataOpt) -> (conName : Name) -> (fields : List (IField' nm)) -> ImpRecord' nm @@ -380,7 +381,7 @@ mutual export covering Show nm => Show (ImpRecord' nm) where - show (MkImpRecord _ n params con fields) + show (MkImpRecord _ n params opts con fields) = "record " ++ show n ++ " " ++ show params ++ " " ++ show con ++ "\n\t" ++ showSep "\n\t" (map show fields) ++ "\n" @@ -789,7 +790,7 @@ definedInBlock ns decls = defName ns (IParameters _ _ pds) = concatMap (defName ns) pds defName ns (IFail _ _ nds) = concatMap (defName ns) nds defName ns (INamespace _ n nds) = concatMap (defName (ns <.> n)) nds - defName ns (IRecord _ fldns _ _ (MkImpRecord _ n _ con flds)) + defName ns (IRecord _ fldns _ _ (MkImpRecord _ n _ opts con flds)) = expandNS ns con :: all where fldns' : Namespace diff --git a/src/TTImp/TTImp/Functor.idr b/src/TTImp/TTImp/Functor.idr index 97a29659d..0c3505b34 100644 --- a/src/TTImp/TTImp/Functor.idr +++ b/src/TTImp/TTImp/Functor.idr @@ -145,9 +145,9 @@ mutual export Functor ImpRecord' where - map f (MkImpRecord fc n params conName fields) + map f (MkImpRecord fc n params opts conName fields) = MkImpRecord fc n (map (map {f = ImpParameter'} f) params) - conName (map (map f) fields) + opts conName (map (map f) fields) export Functor ImpParameter' where diff --git a/src/TTImp/TTImp/TTC.idr b/src/TTImp/TTImp/TTC.idr index dcfb6fc26..e7c09db28 100644 --- a/src/TTImp/TTImp/TTC.idr +++ b/src/TTImp/TTImp/TTC.idr @@ -317,13 +317,13 @@ mutual export TTC ImpRecord where - toBuf b (MkImpRecord fc n ps con fs) - = do toBuf b fc; toBuf b n; toBuf b ps; toBuf b con; toBuf b fs + toBuf b (MkImpRecord fc n ps opts con fs) + = do toBuf b fc; toBuf b n; toBuf b ps; toBuf b opts; toBuf b con; toBuf b fs fromBuf b = do fc <- fromBuf b; n <- fromBuf b; ps <- fromBuf b - con <- fromBuf b; fs <- fromBuf b - pure (MkImpRecord fc n ps con fs) + opts <- fromBuf b; con <- fromBuf b; fs <- fromBuf b + pure (MkImpRecord fc n ps opts con fs) export TTC FnOpt where diff --git a/src/TTImp/TTImp/Traversals.idr b/src/TTImp/TTImp/Traversals.idr index c530e2f10..f25947b5f 100644 --- a/src/TTImp/TTImp/Traversals.idr +++ b/src/TTImp/TTImp/Traversals.idr @@ -56,8 +56,8 @@ parameters (f : RawImp' nm -> RawImp' nm) export mapImpRecord : ImpRecord' nm -> ImpRecord' nm - mapImpRecord (MkImpRecord fc n params conName fields) - = MkImpRecord fc n (map (map $ map $ bimap mapPiInfo mapTTImp) params) conName (map mapIField fields) + mapImpRecord (MkImpRecord fc n params opts conName fields) + = MkImpRecord fc n (map (map $ map $ bimap mapPiInfo mapTTImp) params) opts conName (map mapIField fields) export mapImpDecl : ImpDecl' nm -> ImpDecl' nm diff --git a/src/TTImp/Utils.idr b/src/TTImp/Utils.idr index 2c5df1c10..322295b64 100644 --- a/src/TTImp/Utils.idr +++ b/src/TTImp/Utils.idr @@ -35,7 +35,7 @@ rawImpFromDecl decl = case decl of IData fc1 y _ (MkImpLater fc2 n tycon) => [tycon] IDef fc1 y ys => getFromClause !ys IParameters fc1 ys zs => rawImpFromDecl !zs ++ map getParamTy ys - IRecord fc1 y z _ (MkImpRecord fc n params conName fields) => do + IRecord fc1 y z _ (MkImpRecord fc n params opts conName fields) => do (a, b) <- map (snd . snd) params getFromPiInfo a ++ [b] ++ getFromIField !fields IFail fc1 msg zs => rawImpFromDecl !zs diff --git a/tests/Main.idr b/tests/Main.idr index cd8f98883..89e5a23ae 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -166,7 +166,7 @@ idrisTestsData = MkTestPool "Data and record types" [] Nothing "record001", "record002", "record003", "record004", "record005", "record006", "record007", "record008", "record009", "record010", "record011", "record012", "record013", "record014", "record015", - "record016" ] + "record016", "record017" ] idrisTestsBuiltin : TestPool idrisTestsBuiltin = MkTestPool "Builtin types and functions" [] Nothing diff --git a/tests/idris2/record017/RecordOptions.idr b/tests/idris2/record017/RecordOptions.idr new file mode 100644 index 000000000..cf2d44d4f --- /dev/null +++ b/tests/idris2/record017/RecordOptions.idr @@ -0,0 +1,38 @@ +%default total + +-- We put it all in a failing block so as not to pollute the scope +-- The point is that because we have not specified `[search a]` when +-- defining `Wrap` then we cannot find the `Wrap` implementation in +-- the test. + +failing "Can't find an implementation for Wrap ?ph Nat." + + record Wrap (phantom : Type) (a : Type) where + constructor MkWrap + unWrap : a + + %hint + zero : Wrap Bool Nat + zero = MkWrap 0 + + getWrappedVal : Wrap ph a => a + getWrappedVal @{w} = unWrap w + + test : Main.getWrappedVal === Z + test = Refl + +record Wrap (phantom : Type) (a : Type) where + -- whereas this will give us the right behaviour + [search a] + constructor MkWrap + unWrap : a + +%hint +zero : Wrap Bool Nat +zero = MkWrap 0 + +getWrappedVal : Wrap ph a => a +getWrappedVal @{w} = unWrap w + +test : Main.getWrappedVal === Z +test = Refl diff --git a/tests/idris2/record017/expected b/tests/idris2/record017/expected new file mode 100644 index 000000000..592090711 --- /dev/null +++ b/tests/idris2/record017/expected @@ -0,0 +1 @@ +1/1: Building RecordOptions (RecordOptions.idr) diff --git a/tests/idris2/record017/run b/tests/idris2/record017/run new file mode 100755 index 000000000..796e1c37c --- /dev/null +++ b/tests/idris2/record017/run @@ -0,0 +1,3 @@ +rm -rf build + +$1 --no-color --console-width 0 --no-banner -c RecordOptions.idr diff --git a/tests/idris2/reflection004/refdecl.idr b/tests/idris2/reflection004/refdecl.idr index 7bc885e69..742230397 100644 --- a/tests/idris2/reflection004/refdecl.idr +++ b/tests/idris2/reflection004/refdecl.idr @@ -22,7 +22,7 @@ mkPoint n = let type = "Point" ++ show n ++ "D" in let mkMainUN = NS (MkNS ["Main"]) . UN . Basic in IRecord emptyFC Nothing Public Nothing - (MkRecord emptyFC (mkMainUN type) [] (mkMainUN ("Mk" ++ type)) + (MkRecord emptyFC (mkMainUN type) [] [] (mkMainUN ("Mk" ++ type)) (toList $ map (\axis => MkIField emptyFC MW ExplicitArg (UN (Field axis)) `(Double)) (axes n))) logDecls : TTImp -> Elab (Int -> Int)