From e5802204b644258235552b443fb1029e05dc1e4c Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 16 Jun 2022 16:32:00 +0100 Subject: [PATCH] [ fix ] holes in record types --- idris2api.ipkg | 1 + src/TTImp/ProcessRecord.idr | 31 +++++-- src/TTImp/TTImp/Traversals.idr | 128 ++++++++++++++++++++++++++ tests/Main.idr | 3 +- tests/idris2/record016/HoleRecord.idr | 9 ++ tests/idris2/record016/expected | 7 ++ tests/idris2/record016/input | 4 + tests/idris2/record016/run | 3 + 8 files changed, 178 insertions(+), 8 deletions(-) create mode 100644 src/TTImp/TTImp/Traversals.idr create mode 100644 tests/idris2/record016/HoleRecord.idr create mode 100644 tests/idris2/record016/expected create mode 100644 tests/idris2/record016/input create mode 100755 tests/idris2/record016/run diff --git a/idris2api.ipkg b/idris2api.ipkg index 7c8ace6d8..fc93e4f89 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -257,6 +257,7 @@ modules = TTImp.Reflect, TTImp.TTImp, TTImp.TTImp.Functor, + TTImp.TTImp.Traversals, TTImp.TTImp.TTC, TTImp.Unelab, TTImp.Utils, diff --git a/src/TTImp/ProcessRecord.idr b/src/TTImp/ProcessRecord.idr index f1cd16a0a..16cec49ec 100644 --- a/src/TTImp/ProcessRecord.idr +++ b/src/TTImp/ProcessRecord.idr @@ -14,6 +14,7 @@ import TTImp.BindImplicits import TTImp.Elab.Check import TTImp.TTImp import TTImp.TTImp.Functor +import TTImp.TTImp.Traversals import TTImp.Unelab import TTImp.Utils @@ -21,10 +22,17 @@ import Data.List %default covering +-- Used to remove the holes so that we don't end up with "hole is already defined" +-- errors because they've been duplicarted when forming the various types of the +-- record constructor, getters, etc. +killHole : RawImp -> RawImp +killHole (IHole fc str) = Implicit fc True +killHole t = t + mkDataTy : FC -> List (Name, RigCount, PiInfo RawImp, RawImp) -> RawImp mkDataTy fc [] = IType fc mkDataTy fc ((n, c, p, ty) :: ps) - = IPi fc c p (Just n) ty (mkDataTy fc ps) + = IPi fc c (mapPiInfo killHole p) (Just n) (mapTTImp killHole ty) (mkDataTy fc ps) -- Projections are only visible if the record is public export projVis : Visibility -> Visibility @@ -72,6 +80,7 @@ elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params conName_in fiel nestedNS := newns :: nns } where + paramTelescope : List (FC, Maybe Name, RigCount, PiInfo RawImp, RawImp) paramTelescope = map jname params where @@ -81,6 +90,10 @@ elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params conName_in fiel -- and projections jname (n, _, _, t) = (EmptyFC, Just n, erased, Implicit, t) + removeIHoles : List (FC, Maybe Name, RigCount, PiInfo RawImp, RawImp) -> + List (FC, Maybe Name, RigCount, PiInfo RawImp, RawImp) + removeIHoles = map (map $ map $ map $ bimap (mapPiInfo killHole) (mapTTImp killHole)) + fname : IField -> Name fname (MkIField fc c p n ty) = n @@ -104,6 +117,9 @@ elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params conName_in fiel apply f ((n, arg, Explicit) :: xs) = apply (IApp (getFC f) f arg) xs apply f ((n, arg, _ ) :: xs) = apply (INamedApp (getFC f) f n arg) xs + paramNames : List Name + paramNames = map fst params + elabAsData : (tn : Name) -> -- fully qualified name of the record type (conName : Name) -> -- fully qualified name of the record type constructor Core () @@ -111,11 +127,10 @@ elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params conName_in fiel = do let fc = virtualiseFC fc let conty = mkTy paramTelescope $ mkTy (map farg fields) (recTy tn) - let con = MkImpTy EmptyFC EmptyFC cname !(bindTypeNames fc [] (map fst params ++ - map fname fields ++ vars) conty) - let dt = MkImpData fc tn !(bindTypeNames fc [] (map fst params ++ - map fname fields ++ vars) - (mkDataTy fc params)) [] [con] + 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] log "declare.record" 5 $ "Record data type " ++ show dt processDecl [] nest env (IData fc vis mbtot dt) @@ -163,7 +178,9 @@ elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params conName_in fiel -- Claim the projection type projTy <- bindTypeNames fc [] (map fst params ++ map fname fields ++ vars) $ - mkTy paramTelescope $ + -- Remove the holes here so that we don't end up with + -- "hole is already defined" errors + mkTy (removeIHoles paramTelescope) $ IPi bfc top Explicit (Just rname) (recTy tn) ty' let mkProjClaim = \ nm => diff --git a/src/TTImp/TTImp/Traversals.idr b/src/TTImp/TTImp/Traversals.idr new file mode 100644 index 000000000..5cf68ac4e --- /dev/null +++ b/src/TTImp/TTImp/Traversals.idr @@ -0,0 +1,128 @@ +module TTImp.TTImp.Traversals + +import Core.TT +import TTImp.TTImp + +%default total + +parameters (f : RawImp' nm -> RawImp' nm) + + export + mapTTImp :RawImp' nm -> RawImp' nm + + export + mapPiInfo : PiInfo (RawImp' nm) -> PiInfo (RawImp' nm) + mapPiInfo Implicit = Implicit + mapPiInfo Explicit = Explicit + mapPiInfo AutoImplicit = AutoImplicit + mapPiInfo (DefImplicit t) = DefImplicit (mapTTImp t) + + export + mapImpClause : ImpClause' nm -> ImpClause' nm + mapImpClause (PatClause fc lhs rhs) = PatClause fc (mapTTImp lhs) (mapTTImp rhs) + mapImpClause (WithClause fc lhs rig wval prf flags cls) + = WithClause fc (mapTTImp lhs) rig (mapTTImp wval) prf flags (assert_total $ map mapImpClause cls) + mapImpClause (ImpossibleClause fc lhs) = ImpossibleClause fc (mapTTImp lhs) + + export + mapImpTy : ImpTy' nm -> ImpTy' nm + mapImpTy (MkImpTy fc nameFC n ty) = MkImpTy fc nameFC n (mapTTImp ty) + + export + mapFnOpt : FnOpt' nm -> FnOpt' nm + mapFnOpt Inline = Inline + mapFnOpt NoInline = NoInline + mapFnOpt Deprecate = Deprecate + mapFnOpt TCInline = TCInline + mapFnOpt (Hint b) = Hint b + mapFnOpt (GlobalHint b) = GlobalHint b + mapFnOpt ExternFn = ExternFn + mapFnOpt (ForeignFn ts) = ForeignFn (map mapTTImp ts) + mapFnOpt (ForeignExport ts) = ForeignExport (map mapTTImp ts) + mapFnOpt Invertible = Invertible + mapFnOpt (Totality treq) = Totality treq + mapFnOpt Macro = Macro + mapFnOpt (SpecArgs ns) = SpecArgs ns + mapFnOpt (NoMangle mdir) = NoMangle mdir + + export + mapImpData : ImpData' nm -> ImpData' nm + mapImpData (MkImpData fc n tycon opts datacons) + = MkImpData fc n (mapTTImp tycon) opts (map mapImpTy datacons) + mapImpData (MkImpLater fc n tycon) = MkImpLater fc n (mapTTImp tycon) + + export + mapIField : IField' nm -> IField' nm + mapIField (MkIField fc rig pinfo n t) = MkIField fc rig (mapPiInfo pinfo) n (mapTTImp t) + + 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) + + export + mapImpDecl : ImpDecl' nm -> ImpDecl' nm + mapImpDecl (IClaim fc rig vis opts ty) + = IClaim fc rig vis (map mapFnOpt opts) (mapImpTy ty) + mapImpDecl (IData fc vis mtreq dat) = IData fc vis mtreq (mapImpData dat) + mapImpDecl (IDef fc n cls) = IDef fc n (map mapImpClause cls) + mapImpDecl (IParameters fc params xs) = IParameters fc params (assert_total $ map mapImpDecl xs) + mapImpDecl (IRecord fc mstr x y rec) = IRecord fc mstr x y (mapImpRecord rec) + mapImpDecl (IFail fc mstr xs) = IFail fc mstr (assert_total $ map mapImpDecl xs) + mapImpDecl (INamespace fc mi xs) = INamespace fc mi (assert_total $ map mapImpDecl xs) + mapImpDecl (ITransform fc n t u) = ITransform fc n (mapTTImp t) (mapTTImp u) + mapImpDecl (IRunElabDecl fc t) = IRunElabDecl fc (mapTTImp t) + mapImpDecl (IPragma ns g) = IPragma ns g + mapImpDecl (ILog x) = ILog x + mapImpDecl (IBuiltin fc x n) = IBuiltin fc x n + + export + mapIFieldUpdate : IFieldUpdate' nm -> IFieldUpdate' nm + mapIFieldUpdate (ISetField path t) = ISetField path (mapTTImp t) + mapIFieldUpdate (ISetFieldApp path t) = ISetFieldApp path (mapTTImp t) + + export + mapAltType : AltType' nm -> AltType' nm + mapAltType FirstSuccess = FirstSuccess + mapAltType Unique = Unique + mapAltType (UniqueDefault t) = UniqueDefault (mapTTImp t) + + mapTTImp t@(IVar _ _) = f t + mapTTImp (IPi fc rig pinfo x argTy retTy) + = f $ IPi fc rig (mapPiInfo pinfo) x (mapTTImp argTy) (mapTTImp retTy) + mapTTImp (ILam fc rig pinfo x argTy lamTy) + = 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 (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) + mapTTImp (IUpdate fc upds t) = f $ IUpdate fc (assert_total map mapIFieldUpdate upds) (mapTTImp t) + mapTTImp (IApp fc t u) = f $ IApp fc (mapTTImp t) (mapTTImp u) + mapTTImp (IAutoApp fc t u) = f $ IAutoApp fc (mapTTImp t) (mapTTImp u) + mapTTImp (INamedApp fc t n u) = f $ INamedApp fc (mapTTImp t) n (mapTTImp u) + mapTTImp (IWithApp fc t u) = f $ IWithApp fc (mapTTImp t) (mapTTImp u) + mapTTImp (ISearch fc depth) = f $ ISearch fc depth + mapTTImp (IAlternative fc alt ts) = f $ IAlternative fc (mapAltType alt) (assert_total map mapTTImp ts) + mapTTImp (IRewrite fc t u) = f $ IRewrite fc (mapTTImp t) (mapTTImp u) + mapTTImp (ICoerced fc t) = f $ ICoerced fc (mapTTImp t) + mapTTImp (IBindHere fc bm t) = f $ IBindHere fc bm (mapTTImp t) + mapTTImp (IBindVar fc str) = f $ IBindVar fc str + mapTTImp (IAs fc nameFC side n t) = f $ IAs fc nameFC side n (mapTTImp t) + mapTTImp (IMustUnify fc x t) = f $ IMustUnify fc x (mapTTImp t) + mapTTImp (IDelayed fc lz t) = f $ IDelayed fc lz (mapTTImp t) + mapTTImp (IDelay fc t) = f $ IDelay fc (mapTTImp t) + mapTTImp (IForce fc t) = f $ IForce fc (mapTTImp t) + mapTTImp (IQuote fc t) = f $ IQuote fc (mapTTImp t) + mapTTImp (IQuoteName fc n) = f $ IQuoteName fc n + mapTTImp (IQuoteDecl fc xs) = f $ IQuoteDecl fc (assert_total $ map mapImpDecl xs) + mapTTImp (IUnquote fc t) = f $ IUnquote fc (mapTTImp t) + mapTTImp (IRunElab fc t) = f $ IRunElab fc (mapTTImp t) + mapTTImp (IPrimVal fc c) = f $ IPrimVal fc c + mapTTImp (IType fc) = f $ IType fc + mapTTImp (IHole fc str) = f $ IHole fc str + mapTTImp (IUnifyLog fc x t) = f $ IUnifyLog fc x (mapTTImp t) + mapTTImp (Implicit fc bindIfUnsolved) = f $ Implicit fc bindIfUnsolved + mapTTImp (IWithUnambigNames fc xs t) = f $ IWithUnambigNames fc xs (mapTTImp t) diff --git a/tests/Main.idr b/tests/Main.idr index fc02a3ef0..fdf88eb66 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -157,7 +157,8 @@ idrisTestsData = MkTestPool "Data and record types" [] Nothing -- Records, access and dependent update "record001", "record002", "record003", "record004", "record005", "record006", "record007", "record008", "record009", "record010", - "record011", "record012", "record013", "record014", "record015" ] + "record011", "record012", "record013", "record014", "record015", + "record016" ] idrisTestsBuiltin : TestPool idrisTestsBuiltin = MkTestPool "Builtin types and functions" [] Nothing diff --git a/tests/idris2/record016/HoleRecord.idr b/tests/idris2/record016/HoleRecord.idr new file mode 100644 index 000000000..a0bec5897 --- /dev/null +++ b/tests/idris2/record016/HoleRecord.idr @@ -0,0 +1,9 @@ +record Wrap (a : ?hole) where + constructor MkWrap + proj : a + +record Unit (a : ?hole2) where + constructor MkUnit + +record Tree (a : ?hole3) where + isThree : 3 === a diff --git a/tests/idris2/record016/expected b/tests/idris2/record016/expected new file mode 100644 index 000000000..2517178ad --- /dev/null +++ b/tests/idris2/record016/expected @@ -0,0 +1,7 @@ +1/1: Building HoleRecord (HoleRecord.idr) +Main> Main.hole : Type +Main> Main.hole2 : Type +Main> Main.hole3 : Type +Main> 1 hole: Main.hole2 : Type +Main> +Bye for now! diff --git a/tests/idris2/record016/input b/tests/idris2/record016/input new file mode 100644 index 000000000..4befa82b1 --- /dev/null +++ b/tests/idris2/record016/input @@ -0,0 +1,4 @@ +:t hole +:t hole2 +:t hole3 +:m diff --git a/tests/idris2/record016/run b/tests/idris2/record016/run new file mode 100755 index 000000000..5d4614a7c --- /dev/null +++ b/tests/idris2/record016/run @@ -0,0 +1,3 @@ +rm -rf build + +$1 --no-color --console-width 0 --no-banner HoleRecord.idr < input