git.iko.soy/Idris-dev
on master help sign in
Implemented @-patterns

By popular request. Fixes #1706. It's not the most efficient desugaring, merely translating the @s on the left to lets on the right, so the case tree builder won't be aware of it. Still, it provides the notation and it works nicely with showing what is in scope and what is available in the prover and so on.

commit941ba6eacb13c104c7bbb26b965ba5a343c8418f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 15 Dec 2014, 00:09 (12 years ago) parent3c19722
8 files changed+41−5
compare with master
unifiedsplit
idris.cabal+1 src/Idris/AbsSyntaxTree.hs+1 src/Idris/Elab/AsPat.hs+28 src/Idris/Elab/Clause.hs+3−1 src/Idris/ElabTerm.hs+1 src/Idris/Output.hs+1−1 src/Idris/ParseExpr.hs+4−1 test/reg050/expected+2−2
idris.cabal+1
@@ -607,6 +607,7 @@ Library
607607
608608 , Idris.Elab.Utils
609609 , Idris.Elab.Type
610+ , Idris.Elab.AsPat
610611 , Idris.Elab.Clause
611612 , Idris.Elab.Data
612613 , Idris.Elab.Record
src/Idris/AbsSyntaxTree.hs+1
@@ -728,6 +728,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua
728728 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type
729729 | PPair FC PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration)
730730 | PDPair FC PunInfo PTerm PTerm PTerm -- ^ A dependent pair (tm : a ** b) and whether it's a sigma type or a pair that inhabits one (solved by elaboration)
731+ | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
731732 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)
732733 | PHidden PTerm -- ^ Irrelevant or hidden pattern
733734 | PType -- ^ 'Type' type
src/Idris/Elab/AsPat.hsnew file+28
@@ -0,0 +1,28 @@
1+module Idris.Elab.AsPat(desugarAs) where
2+
3+import Idris.Core.TT
4+import Idris.AbsSyntax
5+import Control.Monad.State.Strict
6+
7+-- Desugar by changing x@y on lhs to let x = y in ... or rhs
8+desugarAs :: PTerm -> PTerm -> (PTerm, PTerm)
9+desugarAs lhs rhs
10+ = let (lhs', pats) = runState (collectAs lhs) [] in
11+ (lhs', bindPats pats rhs)
12+ where
13+ bindPats :: [(Name, FC, PTerm)] -> PTerm -> PTerm
14+ bindPats [] rhs = rhs
15+ bindPats ((n, fc, tm) : ps) rhs
16+ = PLet n Placeholder tm (bindPats ps rhs)
17+
18+collectAs :: PTerm -> State [(Name, FC, PTerm)] PTerm
19+collectAs (PAs fc n tm) = do tm' <- collectAs tm
20+ pats <- get
21+ put (pats ++ [(n, fc, tm')])
22+ return tm'
23+collectAs (PApp fc t as)
24+ = do as_tm <- mapM collectAs (map getTm as)
25+ let as' = zipWith (\a tm -> a { getTm = tm }) as as_tm
26+ return (PApp fc t as') -- only valid on args
27+collectAs x = return x
28+
src/Idris/Elab/Clause.hs+3−1
@@ -19,6 +19,7 @@ import Idris.DeepSeq
1919import Idris.Output (iputStrLn, pshow, iWarn, iRenderResult)
2020import IRTS.Lang
2121
22+import Idris.Elab.AsPat
2223import Idris.Elab.Type
2324import Idris.Elab.Transform
2425import Idris.Elab.Utils
@@ -543,9 +544,10 @@ elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
543544 (Msg $ show lhs_in ++ " is a valid case"))
544545 False -> do ptm <- mkPatTm lhs_in
545546 return (Left ptm, lhs)
546−elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
547+elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as whereblock)
547548 = do let tcgen = Dictionary `elem` opts
548549 ctxt <- getContext
550+ let (lhs_in, rhs_in) = desugarAs lhs_in_as rhs_in_as
549551
550552 -- Build the LHS as an "Infer", and pull out its type and
551553 -- pattern bindings
src/Idris/ElabTerm.hs+1
@@ -858,6 +858,7 @@ elab ist info emode opts fn tm
858858
859859
860860 elab' ina fc (PUnquote t) = fail "Found unquote outside of quasiquote"
861+ elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here"
861862 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
862863
863864 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
src/Idris/Output.hs+1−1
@@ -1,4 +1,4 @@
1−{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
1+{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}
22
33module Idris.Output where
44
src/Idris/ParseExpr.hs+4−1
@@ -332,7 +332,10 @@ simpleExpr syn =
332332 [pexp (PConstant (Str (show str)))])
333333 <|> do fc <- getFC
334334 x <- fnName
335− return (PRef fc x)
335+ option (PRef fc x)
336+ (do reservedOp "@"
337+ s <- simpleExpr syn
338+ return (PAs fc x s))
336339 <|> idiom syn
337340 <|> listExpr syn
338341 <|> alt syn
test/reg050/expected+2−2
@@ -17,8 +17,8 @@ When elaborating an application of function Prelude.Monad.>>=:
1717 "<", "<#>", "<$", "<$>", "<*>",
1818 "<+>", "<->", "<<", "<=", "<|>",
1919 "=", "==", ">", ">=", ">>",
20− ">>=", "\\\\", "`", "in", "||",
21− "~=~",
20+ ">>=", "@", "\\\\", "`", "in",
21+ "||", "~=~",
2222 ambiguous use of a left-associative operator,
2323 ambiguous use of a non-associative operator,
2424 ambiguous use of a right-associative operator,