[ fix ] Parse with-applications at LHS as PWithApp instead of PApp

src/Idris/Desugar.idr

@@ -785,6 +785,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"

src/Idris/Elab/Implementation.idr

@@ -486,6 +486,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)

src/Idris/Parser.idr

@@ -1177,7 +1177,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
@@ -1188,11 +1188,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)) ->

src/Idris/Syntax.idr

@@ -279,6 +279,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

src/TTImp/Impossible.idr

@@ -159,6 +159,8 @@ mutual
      = buildApp fc n 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
@@ -196,6 +198,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

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)

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

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

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!

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 } }]

tests/base/ttimp_show001/run

@@ -0,0 +1,3 @@
+. ../../testutils.sh
+
+idris2 < input