mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-10-26 17:33:47 +03:00
Take account of env in record elaboration
Also need to make sure that the constructor and fields are included in the nested names so that the parameters get expanded properly. Fixes #138
This commit is contained in:
parent
344a565a49
commit
cbf8785d32
@ -693,7 +693,7 @@ mutual
|
||||
elabImplementation fc vis pass env nest isb consb
|
||||
tn paramsb impname nusing
|
||||
body')]
|
||||
desugarDecl ps (PRecord fc vis tn params conname fields)
|
||||
desugarDecl ps (PRecord fc vis tn params conname_in fields)
|
||||
= do params' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm)
|
||||
pure (fst ntm, tm')) params
|
||||
let fnames = map fname fields
|
||||
@ -706,6 +706,7 @@ mutual
|
||||
let paramsb = map (\ (n, tm) => (n, doBind bnames tm)) params'
|
||||
fields' <- traverse (desugarField (ps ++ map fname fields ++
|
||||
map fst params)) fields
|
||||
let conname = maybe (mkConName tn) id conname_in
|
||||
-- True flag set so that the parent namespace can look inside the
|
||||
-- record definition
|
||||
pure [IRecord fc (Just (nameRoot tn))
|
||||
@ -713,6 +714,11 @@ mutual
|
||||
where
|
||||
fname : PField -> Name
|
||||
fname (MkField _ _ _ n _) = n
|
||||
|
||||
mkConName : Name -> Name
|
||||
mkConName (NS ns (UN n)) = NS ns (DN n (MN ("__mk" ++ n) 0))
|
||||
mkConName n = DN (show n) (MN ("__mk" ++ show n) 0)
|
||||
|
||||
desugarDecl ps (PFixity fc Prefix prec (UN n))
|
||||
= do syn <- get Syn
|
||||
put Syn (record { prefixes $= insert n prec } syn)
|
||||
|
@ -330,7 +330,7 @@ mutual
|
||||
do ty' <- toPTerm startPrec ty
|
||||
pure (n, ty')) ps
|
||||
fs' <- traverse toPField fs
|
||||
pure (n, ps', con, fs')
|
||||
pure (n, ps', Just con, fs')
|
||||
|
||||
toPFnOpt : {auto c : Ref Ctxt Defs} ->
|
||||
{auto s : Ref Syn SyntaxInfo} ->
|
||||
|
@ -595,9 +595,8 @@ recordDecl fname indents
|
||||
n <- name
|
||||
params <- many (ifaceParam fname indents)
|
||||
keyword "where"
|
||||
dc <- option Nothing (do exactIdent "constructor"
|
||||
n <- name
|
||||
pure (Just n))
|
||||
exactIdent "constructor"
|
||||
dc <- name
|
||||
flds <- assert_total (blockAfter col (fieldDecl fname))
|
||||
end <- location
|
||||
let fc = MkFC fname start end
|
||||
|
@ -20,23 +20,19 @@ mkDataTy fc [] = IType fc
|
||||
mkDataTy fc ((n, ty) :: ps)
|
||||
= IPi fc RigW Explicit (Just n) ty (mkDataTy fc ps)
|
||||
|
||||
mkCon : Name -> Name
|
||||
mkCon (NS ns (UN n)) = NS ns (DN n (MN ("__mk" ++ n) 0))
|
||||
mkCon n = DN (show n) (MN ("__mk" ++ show n) 0)
|
||||
|
||||
elabRecord : {auto c : Ref Ctxt Defs} ->
|
||||
elabRecord : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
List ElabOpt -> FC -> Env Term vars ->
|
||||
NestedNames vars -> Maybe String ->
|
||||
Visibility -> Name ->
|
||||
(params : List (Name, RawImp)) ->
|
||||
(conName : Maybe Name) ->
|
||||
(conName : Name) ->
|
||||
List IField ->
|
||||
Core ()
|
||||
elabRecord {vars} eopts fc env nest newns vis tn params rcon fields
|
||||
= do let conName_in = maybe (mkCon tn) id rcon
|
||||
conName <- inCurrentNS conName_in
|
||||
elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
|
||||
= do conName <- inCurrentNS conName_in
|
||||
elabAsData conName
|
||||
defs <- get Ctxt
|
||||
Just conty <- lookupTyExact conName (gamma defs)
|
||||
@ -92,7 +88,8 @@ elabRecord {vars} eopts fc env nest newns vis tn params rcon fields
|
||||
countExp _ = 0
|
||||
|
||||
-- Generate getters from the elaborated record constructor type
|
||||
elabGetters : Name -> RawImp ->
|
||||
elabGetters : {vs : _} ->
|
||||
Name -> RawImp ->
|
||||
(done : Nat) -> -- number of explicit fields processed
|
||||
List (Name, RawImp) -> -- names to update in types
|
||||
-- (for dependent records, where a field's type may depend
|
||||
@ -100,9 +97,9 @@ elabRecord {vars} eopts fc env nest newns vis tn params rcon fields
|
||||
Env Term vs -> Term vs ->
|
||||
Core ()
|
||||
elabGetters con recTy done upds tyenv (Bind bfc n b@(Pi rc imp ty_chk) sc)
|
||||
= if n `elem` map fst params
|
||||
= if (n `elem` map fst params) || (n `elem` vars)
|
||||
then elabGetters con recTy
|
||||
(if imp == Explicit
|
||||
(if imp == Explicit && not (n `elem` vars)
|
||||
then S done else done)
|
||||
upds (b :: tyenv) sc
|
||||
else
|
||||
@ -110,6 +107,7 @@ elabRecord {vars} eopts fc env nest newns vis tn params rcon fields
|
||||
gname <- inCurrentNS fldName
|
||||
ty <- unelab tyenv ty_chk
|
||||
let ty' = substNames vars upds ty
|
||||
log 5 $ "Field type: " ++ show ty'
|
||||
let rname = MN "rec" 0
|
||||
gty <- bindTypeNames []
|
||||
(map fst params ++ map fname fields ++ vars) $
|
||||
@ -128,6 +126,7 @@ elabRecord {vars} eopts fc env nest newns vis tn params rcon fields
|
||||
then lhs_exp
|
||||
else IImplicitApp fc lhs_exp (Just n)
|
||||
(IBindVar fc (nameRoot fldName)))
|
||||
log 5 $ "Projection LHS " ++ show lhs
|
||||
processDecl [] nest env
|
||||
(IClaim fc (if rc == Rig0
|
||||
then Rig0
|
||||
|
@ -260,7 +260,7 @@ mutual
|
||||
data ImpRecord : Type where
|
||||
MkImpRecord : FC -> (n : Name) ->
|
||||
(params : List (Name, RawImp)) ->
|
||||
(conName : Maybe Name) ->
|
||||
(conName : Name) ->
|
||||
(fields : List IField) ->
|
||||
ImpRecord
|
||||
|
||||
@ -498,6 +498,9 @@ definedInBlock ns = concatMap (defName ns)
|
||||
getName : ImpTy -> Name
|
||||
getName (MkImpTy _ n _) = n
|
||||
|
||||
getFieldName : IField -> Name
|
||||
getFieldName (MkIField _ _ _ n _) = n
|
||||
|
||||
expandNS : List String -> Name -> Name
|
||||
expandNS [] n = n
|
||||
expandNS ns (UN n) = NS ns (UN n)
|
||||
@ -512,7 +515,12 @@ definedInBlock ns = concatMap (defName ns)
|
||||
defName ns (IData _ _ (MkImpLater _ n _)) = [expandNS ns n]
|
||||
defName ns (IParameters _ _ pds) = concatMap (defName ns) pds
|
||||
defName ns (INamespace _ n nds) = concatMap (defName (n ++ ns)) nds
|
||||
defName ns (IRecord _ _ _ (MkImpRecord _ n _ _ _)) = [n]
|
||||
defName ns (IRecord _ fldns _ (MkImpRecord _ n _ con flds))
|
||||
= let fldns = maybe ns (\f => f :: ns) fldns
|
||||
all : List Name
|
||||
= expandNS ns n ::
|
||||
map (expandNS fldns) (map getFieldName flds) in
|
||||
expandNS ns con :: all
|
||||
defName _ _ = []
|
||||
|
||||
export
|
||||
|
@ -73,7 +73,7 @@ idrisTests
|
||||
"record001", "record002",
|
||||
-- Miscellaneous regressions
|
||||
"reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
|
||||
"reg008", "reg009", "reg010", "reg011",
|
||||
"reg008", "reg009", "reg010", "reg011", "reg012",
|
||||
-- Totality checking
|
||||
"total001", "total002", "total003", "total004", "total005",
|
||||
"total006",
|
||||
|
9
tests/idris2/reg012/Foo.idr
Normal file
9
tests/idris2/reg012/Foo.idr
Normal file
@ -0,0 +1,9 @@
|
||||
import Data.Vect
|
||||
|
||||
parameters (len : Nat)
|
||||
record Foo where
|
||||
constructor Bar
|
||||
Gnat : Vect len Nat
|
||||
|
||||
foo : Foo 1
|
||||
foo = Bar _ [0]
|
1
tests/idris2/reg012/expected
Normal file
1
tests/idris2/reg012/expected
Normal file
@ -0,0 +1 @@
|
||||
1/1: Building Foo (Foo.idr)
|
3
tests/idris2/reg012/run
Executable file
3
tests/idris2/reg012/run
Executable file
@ -0,0 +1,3 @@
|
||||
$1 Foo.idr --check
|
||||
|
||||
rm -rf build
|
Loading…
Reference in New Issue
Block a user