From e492f26ca415092aeb701f039abe60e2834cf4e9 Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Fri, 13 Jan 2023 22:56:40 +0300 Subject: [PATCH] [ fix ] Parse with-applications at LHS as `PWithApp` instead of `PApp` --- CHANGELOG_NEXT.md | 10 +++++++--- src/Idris/Desugar.idr | 1 + src/Idris/Elab/Implementation.idr | 3 +++ src/Idris/Parser.idr | 6 +++--- src/Idris/Syntax.idr | 5 +++++ src/TTImp/Impossible.idr | 3 +++ src/TTImp/Interactive/CaseSplit.idr | 5 ++++- src/TTImp/Interactive/GenerateDef.idr | 4 ++++ src/TTImp/WithClause.idr | 4 ++++ tests/base/ttimp_show001/expected | 4 ++++ tests/base/ttimp_show001/input | 2 ++ tests/base/ttimp_show001/run | 3 +++ 12 files changed, 43 insertions(+), 7 deletions(-) create mode 100644 tests/base/ttimp_show001/expected create mode 100644 tests/base/ttimp_show001/input create mode 100755 tests/base/ttimp_show001/run diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index ce5919b8451..d22c179f8e5 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -52,6 +52,10 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO * The compiler now parses `~x.fun` as unquoting `x` rather than `x.fun` and `~(f 5).fun` as unquoting `(f 5)` rather than `(f 5).fun`. +* LHS of `with`-applications are parsed as `PWithApp` instead of `PApp`. As a + consequence, `IWithApp` appears in `TTImp` values in elaborator scripts instead + of `IApp`, as it should have been. + ### Backend changes #### RefC Backend @@ -60,10 +64,10 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO is dropped as soon as possible. This allows you to reuse unique variables and optimize memory consumption. -* Fix invalid memory read onf strSubStr. +* Fix invalid memory read in `strSubStr`. -* Fix memory leaks of IORef. Now that IORef holds values by itself, - global_IORef_Storage is no longer needed. +* Fix memory leaks of `IORef`. Now that `IORef` holds values by itself, + `global_IORef_Storage` is no longer needed. * Pattern matching generates simpler code. This reduces malloc/free and memory consumption. It also makes debugging easier. diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index e26787ea4b6..c8dc88d8c83 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -883,6 +883,7 @@ mutual getClauseFn : RawImp -> Core Name getClauseFn (IVar _ n) = pure n getClauseFn (IApp _ f _) = getClauseFn f + getClauseFn (IWithApp _ f _) = getClauseFn f getClauseFn (IAutoApp _ f _) = getClauseFn f getClauseFn (INamedApp _ f _ _) = getClauseFn f getClauseFn tm = throw $ GenericMsg (getFC tm) "Head term in pattern must be a function name" diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr index b263072629d..c55b50e7883 100644 --- a/src/Idris/Elab/Implementation.idr +++ b/src/Idris/Elab/Implementation.idr @@ -491,6 +491,9 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i updateApp ns (IApp fc f arg) = do f' <- updateApp ns f pure (IApp fc f' arg) + updateApp ns (IWithApp fc f arg) + = do f' <- updateApp ns f + pure (IWithApp fc f' arg) updateApp ns (IAutoApp fc f arg) = do f' <- updateApp ns f pure (IAutoApp fc f' arg) diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 4d07f893c90..e02f1591c26 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1235,7 +1235,7 @@ mutual mustWorkBecause b'.bounds "Not the end of a block entry, check indentation" $ atEnd indents (rhs, ws) <- pure b.val let fc = boundToFC fname (mergeBounds start b) - pure (MkPatClause fc (uncurry applyArgs lhs) rhs ws) + pure (MkPatClause fc (uncurry applyWithArgs lhs) rhs ws) <|> do b <- bounds $ do decoratedKeyword fname "with" commit @@ -1246,11 +1246,11 @@ mutual pure (flags, wps, forget ws) (flags, wps, ws) <- pure b.val let fc = boundToFC fname (mergeBounds start b) - pure (MkWithClause fc (uncurry applyArgs lhs) wps flags ws) + pure (MkWithClause fc (uncurry applyWithArgs lhs) wps flags ws) <|> do end <- bounds (decoratedKeyword fname "impossible") atEnd indents pure $ let fc = boundToFC fname (mergeBounds start end) in - MkImpossible fc (uncurry applyArgs lhs) + MkImpossible fc (uncurry applyWithArgs lhs) clause : (withArgs : Nat) -> IMaybe (isSucc withArgs) (PTerm, List (FC, PTerm)) -> diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index b09b3e5fd37..b456956eb5e 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -275,6 +275,11 @@ mutual applyArgs f [] = f applyArgs f ((fc, a) :: args) = applyArgs (PApp fc f a) args + export + applyWithArgs : PTerm' nm -> List (FC, PTerm' nm) -> PTerm' nm + applyWithArgs f [] = f + applyWithArgs f ((fc, a) :: args) = applyWithArgs (PWithApp fc f a) args + public export PTypeDecl : Type PTypeDecl = PTypeDecl' Name diff --git a/src/TTImp/Impossible.idr b/src/TTImp/Impossible.idr index da6b4052b42..a733747610f 100644 --- a/src/TTImp/Impossible.idr +++ b/src/TTImp/Impossible.idr @@ -161,6 +161,8 @@ mutual = mkTerm pat mty exps autos named mkTerm (IApp fc fn arg) mty exps autos named = mkTerm fn mty (arg :: exps) autos named + mkTerm (IWithApp fc fn arg) mty exps autos named + = mkTerm fn mty (arg :: exps) autos named mkTerm (IAutoApp fc fn arg) mty exps autos named = mkTerm fn mty exps (arg :: autos) named mkTerm (INamedApp fc fn nm arg) mty exps autos named @@ -198,6 +200,7 @@ getImpossibleTerm env nest tm -- the name to the proper one from the nested names map applyEnv : RawImp -> RawImp applyEnv (IApp fc fn arg) = IApp fc (applyEnv fn) arg + applyEnv (IWithApp fc fn arg) = IWithApp fc (applyEnv fn) arg applyEnv (IAutoApp fc fn arg) = IAutoApp fc (applyEnv fn) arg applyEnv (INamedApp fc fn n arg) = INamedApp fc (applyEnv fn) n arg diff --git a/src/TTImp/Interactive/CaseSplit.idr b/src/TTImp/Interactive/CaseSplit.idr index 774137cae0c..edd6283f121 100644 --- a/src/TTImp/Interactive/CaseSplit.idr +++ b/src/TTImp/Interactive/CaseSplit.idr @@ -161,9 +161,12 @@ updateArg allvars var con (IVar fc n) updateArg allvars var con (IApp fc f a) = pure $ IApp fc !(updateArg allvars var con f) !(updateArg allvars var con a) +updateArg allvars var con (IWithApp fc f a) + = pure $ IWithApp fc !(updateArg allvars var con f) + !(updateArg allvars var con a) updateArg allvars var con (IAutoApp fc f a) = pure $ IAutoApp fc !(updateArg allvars var con f) - !(updateArg allvars var con a) + !(updateArg allvars var con a) updateArg allvars var con (INamedApp fc f n a) = pure $ INamedApp fc !(updateArg allvars var con f) n !(updateArg allvars var con a) diff --git a/src/TTImp/Interactive/GenerateDef.idr b/src/TTImp/Interactive/GenerateDef.idr index 16f2153a67b..9ef21ec48c6 100644 --- a/src/TTImp/Interactive/GenerateDef.idr +++ b/src/TTImp/Interactive/GenerateDef.idr @@ -98,6 +98,10 @@ splittableNames (IApp _ f (IBindVar _ n)) = splittableNames f ++ [UN $ Basic n] splittableNames (IApp _ f _) = splittableNames f +splittableNames (IWithApp _ f (IBindVar _ n)) + = splittableNames f ++ [UN $ Basic n] +splittableNames (IWithApp _ f _) + = splittableNames f splittableNames (IAutoApp _ f _) = splittableNames f splittableNames (INamedApp _ f _ _) diff --git a/src/TTImp/WithClause.idr b/src/TTImp/WithClause.idr index c48148f4c4e..ab229c6ff48 100644 --- a/src/TTImp/WithClause.idr +++ b/src/TTImp/WithClause.idr @@ -22,6 +22,7 @@ matchFail loc = throw (GenericMsg loc "With clause does not match parent") getHeadLoc : RawImp -> Core FC getHeadLoc (IVar fc _) = pure fc getHeadLoc (IApp _ f _) = getHeadLoc f +getHeadLoc (IWithApp _ f _) = getHeadLoc f getHeadLoc (IAutoApp _ f _) = getHeadLoc f getHeadLoc (INamedApp _ f _ _) = getHeadLoc f getHeadLoc t = throw (InternalError $ "Could not find head of LHS: " ++ show t) @@ -210,6 +211,9 @@ getNewLHS iploc drop nest wname wargnames lhs_raw patlhs dropWithArgs (S k) (IApp _ f arg) = do (tm, rest) <- dropWithArgs k f pure (tm, arg :: rest) + dropWithArgs (S k) (IWithApp _ f arg) + = do (tm, rest) <- dropWithArgs k f + pure (tm, arg :: rest) -- Shouldn't happen if parsed correctly, but there's no guarantee that -- inputs come from parsed source so throw an error. dropWithArgs _ _ = throw (GenericMsg iploc "Badly formed 'with' clause") diff --git a/tests/base/ttimp_show001/expected b/tests/base/ttimp_show001/expected new file mode 100644 index 00000000000..44f95d799eb --- /dev/null +++ b/tests/base/ttimp_show001/expected @@ -0,0 +1,4 @@ +Main> Imported module Language.Reflection +Main> "[f a b with (expr) { f a b | x = one; f a b | y with (expr2) { f a a | y | z = e; f a a | y | zz = ee; f a a | y | zzz impossible } }]" +Main> +Bye for now! diff --git a/tests/base/ttimp_show001/input b/tests/base/ttimp_show001/input new file mode 100644 index 00000000000..3b2611c1824 --- /dev/null +++ b/tests/base/ttimp_show001/input @@ -0,0 +1,2 @@ +:module Language.Reflection +show `[f a b with (expr) { f a b | x = one; f a b | y with (expr2) { f a a | y | z = e; f a a | y | zz = ee; f a a | y | zzz impossible } }] diff --git a/tests/base/ttimp_show001/run b/tests/base/ttimp_show001/run new file mode 100755 index 00000000000..fecfb4b1075 --- /dev/null +++ b/tests/base/ttimp_show001/run @@ -0,0 +1,3 @@ +. ../../testutils.sh + +idris2 < input