From bb6db779ef71adecc1caa11da3790b602909fd98 Mon Sep 17 00:00:00 2001 From: Justus Matthiesen Date: Fri, 26 May 2023 15:19:54 +0100 Subject: [PATCH] [ fix #1066 ] do not insert `TForce` on LHS When we encounter a delayed (explicit) function type during elaboration of a LHS, we strip off the delay modality, continue elaboration and return a delayed version of the resulting type. Note: defining delayed function via pattern matching is not currently supported. Doing so will require adding a delay marker to LHSs/contexts familiar from modal type theories. Implicit function are also currently not supported. --- src/Core/Context.idr | 4 ++++ src/Core/Core.idr | 8 ++++++++ src/Idris/Error.idr | 4 ++++ src/TTImp/Elab/App.idr | 15 ++++++++++++--- 4 files changed, 28 insertions(+), 3 deletions(-) diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 1733160cb..34ca8a8a9 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -796,6 +796,8 @@ HasNames Error where full gam (TTCError x) = pure (TTCError x) full gam (FileErr x y) = pure (FileErr x y) full gam (CantFindPackage x) = pure (CantFindPackage x) + full gam (LazyImplicitFunction fc) = pure (LazyImplicitFunction fc) + full gam (LazyPatternVar fc) = pure (LazyPatternVar fc) full gam (LitFail fc) = pure (LitFail fc) full gam (LexFail fc x) = pure (LexFail fc x) full gam (ParseFail xs) = pure (ParseFail xs) @@ -885,6 +887,8 @@ HasNames Error where resolved gam (TTCError x) = pure (TTCError x) resolved gam (FileErr x y) = pure (FileErr x y) resolved gam (CantFindPackage x) = pure (CantFindPackage x) + resolved gam (LazyImplicitFunction fc) = pure (LazyImplicitFunction fc) + resolved gam (LazyPatternVar fc) = pure (LazyPatternVar fc) resolved gam (LitFail fc) = pure (LitFail fc) resolved gam (LexFail fc x) = pure (LexFail fc x) resolved gam (ParseFail xs) = pure (ParseFail xs) diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 3b53d5944..9a743737d 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -161,6 +161,8 @@ data Error : Type where TTCError : TTCErrorMsg -> Error FileErr : String -> FileError -> Error CantFindPackage : String -> Error + LazyImplicitFunction : FC -> Error + LazyPatternVar : FC -> Error LitFail : FC -> Error LexFail : FC -> String -> Error ParseFail : List1 (FC, String) -> Error @@ -346,6 +348,8 @@ Show Error where show (TTCError msg) = "Error in TTC file: " ++ show msg show (FileErr fname err) = "File error (" ++ fname ++ "): " ++ show err show (CantFindPackage fname) = "Can't find package " ++ fname + show (LazyImplicitFunction fc) = "Implicit lazy functions are not yet supported" + show (LazyPatternVar fc) = "Defining lazy functions via pattern matching is not yet supported" show (LitFail fc) = show fc ++ ":Can't parse literate" show (LexFail fc err) = show fc ++ ":Lexer error (" ++ show err ++ ")" show (ParseFail errs) = "Parse errors (" ++ show errs ++ ")" @@ -452,6 +456,8 @@ getErrorLoc (GenericMsg loc _) = Just loc getErrorLoc (TTCError _) = Nothing getErrorLoc (FileErr _ _) = Nothing getErrorLoc (CantFindPackage _) = Nothing +getErrorLoc (LazyImplicitFunction loc) = Just loc +getErrorLoc (LazyPatternVar loc) = Just loc getErrorLoc (LitFail loc) = Just loc getErrorLoc (LexFail loc _) = Just loc getErrorLoc (ParseFail ((loc, _) ::: _)) = Just loc @@ -537,6 +543,8 @@ killErrorLoc (GenericMsg fc x) = GenericMsg emptyFC x killErrorLoc (TTCError x) = TTCError x killErrorLoc (FileErr x y) = FileErr x y killErrorLoc (CantFindPackage x) = CantFindPackage x +killErrorLoc (LazyImplicitFunction fc) = LazyImplicitFunction emptyFC +killErrorLoc (LazyPatternVar fc) = LazyPatternVar emptyFC killErrorLoc (LitFail fc) = LitFail emptyFC killErrorLoc (LexFail fc x) = LexFail emptyFC x killErrorLoc (ParseFail xs) = ParseFail $ map ((emptyFC,) . snd) $ xs diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index 579e516ae..892cdf537 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -614,6 +614,10 @@ perrorRaw (FileErr fname err) <++> byShow err perrorRaw (CantFindPackage fname) = pure $ errorDesc (reflow "Can't find package " <++> pretty0 fname) +perrorRaw (LazyImplicitFunction fc) + = pure $ errorDesc (reflow "Implicit lazy functions are not yet supported.") <+> line <+> !(ploc fc) +perrorRaw (LazyPatternVar fc) + = pure $ errorDesc (reflow "Defining lazy functions via pattern matching is not yet supported.") <+> line <+> !(ploc fc) perrorRaw (LitFail fc) = pure $ errorDesc (reflow "Can't parse literate.") <+> line <+> !(ploc fc) diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index 34d572126..8a38ae19c 100644 --- a/src/TTImp/Elab/App.idr +++ b/src/TTImp/Elab/App.idr @@ -632,9 +632,18 @@ mutual checkExp rig elabinfo env fc tm (glueBack defs env ty) expty else -- Some user defined binding is present while we are out of explicit arguments, that's an error throw (InvalidArgs fc env (map (const (UN $ Basic "")) autoargs ++ map fst namedargs) tm) - -- Function type is delayed, so force the term and continue - checkAppWith' rig elabinfo nest env fc tm (NDelayed dfc r ty@(NBind _ _ (Pi _ _ _ _) sc)) argdata expargs autoargs namedargs kr expty - = checkAppWith' rig elabinfo nest env fc (TForce dfc r tm) ty argdata expargs autoargs namedargs kr expty + -- Function type is delayed: + -- RHS: force the term + -- LHS: strip off delay but only for explicit functions and disallow any further patterns + checkAppWith' rig elabinfo nest env fc tm (NDelayed dfc r ty@(NBind _ _ (Pi _ _ i _) sc)) argdata expargs autoargs namedargs kr expty + = if onLHS (elabMode elabinfo) + then do when (isImplicit i) $ throw (LazyImplicitFunction fc) + let ([], [], []) = (expargs, autoargs, namedargs) + | _ => throw (LazyPatternVar fc) + (tm, gfty) <- checkAppWith' rig elabinfo nest env fc tm ty argdata expargs autoargs namedargs kr expty + fty <- getTerm gfty + pure (tm, gnf env (TDelayed dfc r fty)) + else checkAppWith' rig elabinfo nest env fc (TForce dfc r tm) ty argdata expargs autoargs namedargs kr expty -- If there's no more arguments given, and the plicities of the type and -- the expected type line up, stop checkAppWith' rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Implicit aty) sc)