941ba6e · Idris-dev · git.iko.soy

idris.cabal+1

compare with master

unifiedsplit

@@ -607,6 +607,7 @@ Library

607

608 , Idris.Elab.Utils

609 , Idris.Elab.Type

610+ , Idris.Elab.AsPat

610 , Idris.Elab.Clause

611 , Idris.Elab.Clause

611 , Idris.Elab.Data

612 , Idris.Elab.Data

612 , Idris.Elab.Record

613 , 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

728 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type

729 | PPair FC PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration)

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

731 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)

732 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)

732 | PHidden PTerm -- ^ Irrelevant or hidden pattern

733 | PHidden PTerm -- ^ Irrelevant or hidden pattern

733 | PType -- ^ 'Type' type

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

19import Idris.Output (iputStrLn, pshow, iWarn, iRenderResult)

20import IRTS.Lang

21

22+import Idris.Elab.AsPat

22import Idris.Elab.Type

23import Idris.Elab.Type

23import Idris.Elab.Transform

24import Idris.Elab.Transform

24import Idris.Elab.Utils

25import Idris.Elab.Utils

@@ -543,9 +544,10 @@ elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

543 (Msg $ show lhs_in ++ " is a valid case"))

544 (Msg $ show lhs_in ++ " is a valid case"))

544 False -> do ptm <- mkPatTm lhs_in

545 False -> do ptm <- mkPatTm lhs_in

545 return (Left ptm, lhs)

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

547 = do let tcgen = Dictionary `elem` opts

548 = do let tcgen = Dictionary `elem` opts

548 ctxt <- getContext

549 ctxt <- getContext

550+ let (lhs_in, rhs_in) = desugarAs lhs_in_as rhs_in_as

549

551

550 -- Build the LHS as an "Infer", and pull out its type and

552 -- Build the LHS as an "Infer", and pull out its type and

551 -- pattern bindings

553 -- pattern bindings

src/Idris/ElabTerm.hs+1

@@ -858,6 +858,7 @@ elab ist info emode opts fn tm

858

859

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

861 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

862 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

862

863

863 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))

864 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 #-}

2

3module Idris.Output where

4

src/Idris/ParseExpr.hs+4−1

@@ -332,7 +332,10 @@ simpleExpr syn =

332 [pexp (PConstant (Str (show str)))])

333 <|> do fc <- getFC

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

336 <|> idiom syn

339 <|> idiom syn

337 <|> listExpr syn

340 <|> listExpr syn

338 <|> alt syn

341 <|> alt syn

test/reg050/expected+2−2

@@ -17,8 +17,8 @@ When elaborating an application of function Prelude.Monad.>>=:

17 "<", "<#>", "<$", "<$>", "<*>",

18 "<+>", "<->", "<<", "<=", "<|>",

19 "=", "==", ">", ">=", ">>",

20− ">>=", "\\\\", "`", "in", "||",

20+ ">>=", "@", "\\\\", "`", "in",

21− "~=~",

21+ "||", "~=~",

22 ambiguous use of a left-associative operator,

23 ambiguous use of a non-associative operator,

24 ambiguous use of a right-associative operator,