[ fix ] Fix Show of TTImp for functions with with clauses (#2631)

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
This commit is contained in:
Denis Buzdalov 2024-06-05 16:02:04 +03:00 committed by GitHub
parent 1c588f77ec
commit 1522c3a92c
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
12 changed files with 41 additions and 5 deletions

View File

@ -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,7 +64,7 @@ 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 on `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.

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

3
tests/base/ttimp_show001/run Executable file
View File

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