idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

[ fix #2655 ] Add support for DataOpts in records (#2658)

Browse Source
This commit is contained in:
G. Allais 2022-09-14 14:57:04 +01:00 committed by GitHub
parent 188de8b4cc
commit 55926f30c5
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
23 changed files with 123 additions and 57 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
libs/base/Language/Reflection/TTImp.idr
View File

@ -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

2
src/Core/Binary.idr
View File

@ -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 ()

4
src/Idris/Desugar.idr
View File

@ -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

4
src/Idris/Desugar/Mutual.idr
View File

@ -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

27
src/Idris/Parser.idr
View File

@ -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

9
src/Idris/Resugar.idr
View File

@ -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')))

3
src/Idris/Syntax.idr
View File

@ -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

7
src/Idris/Syntax/Traversals.idr
View File

@ -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

3
src/TTImp/Elab/Local.idr
View File

@ -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)

4
src/TTImp/Elab/Quote.idr
View File

@ -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) ->

15
src/TTImp/Parser.idr
View File

@ -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

9
src/TTImp/ProcessRecord.idr
View File

@ -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

10
src/TTImp/Reflect.idr
View File

@ -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

5
src/TTImp/TTImp.idr
View File

@ -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

4
src/TTImp/TTImp/Functor.idr
View File

@ -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

8
src/TTImp/TTImp/TTC.idr
View File

@ -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

4
src/TTImp/TTImp/Traversals.idr
View File

@ -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

2
src/TTImp/Utils.idr
View File

@ -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

2
tests/Main.idr
View File

@ -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

38
tests/idris2/record017/RecordOptions.idr Normal file
View File

@ -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

1
tests/idris2/record017/expected Normal file
View File

@ -0,0 +1 @@
1/1: Building RecordOptions (RecordOptions.idr)

3
tests/idris2/record017/run Executable file
View File

@ -0,0 +1,3 @@
rm -rf build
$1 --no-color --console-width 0 --no-banner -c RecordOptions.idr

2
tests/idris2/reflection004/refdecl.idr
View File

@ -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)