git.iko.soy/Idris-dev
on master help sign in
Expose `@` patterns to where functions (#4057)

* Pass whereblock to desugarAs * Bind @ variables in where clauses * @ patterns don't shadow where-functions' lhs-bound names * m@... doesn't shadow lhs vars in nested where block * Simplify bindPats * Rename for clarity * Test case for doubly-nested @ pattern * Update CHANGELOG.md

commitf436c5ffb32dfda19b41f0cbf8049e46e62d7093 authorJason Felice <jason.m.felice@gmail.com> dateWed 13 Sep 2017, 10:35 (9 years ago) parenta071dab
7 files changed+75−12
compare with master
unifiedsplit
CHANGELOG.md+3 src/Idris/Elab/AsPat.hs+21−9 src/Idris/Elab/Clause.hs+2−2 test/TestData.hs+2−1 test/basic020/basic020.idr+42 test/basic020/expected+1 test/basic020/run+4
CHANGELOG.md+3
@@ -2,6 +2,9 @@
22
33+ Addition of `Text.Literate`, a module for working with literate
44 source files.
5++ In `@`-patterns such as `x@p`, `x` is now in scope on the right-hand side
6+ of any definitions in `where` clauses, provided the left-hand side of the
7+ definition does not shadow it.
58
69# New in 1.1.1
710
src/Idris/Elab/AsPat.hs+21−9
@@ -12,18 +12,30 @@ import Idris.Core.TT
1212
1313import Control.Applicative
1414import Control.Monad.State.Strict
15−import Data.Generics.Uniplate.Data (transformM)
15+import Data.Generics.Uniplate.Data (transformM, universe)
1616
1717-- | Desugar by changing x@y on lhs to let x = y in ... or rhs
18−desugarAs :: PTerm -> PTerm -> (PTerm, PTerm)
19−desugarAs lhs rhs
20− = let (lhs', pats) = runState (collectAs (replaceUnderscore lhs)) [] in
21− (lhs', bindPats pats rhs)
18+desugarAs :: PTerm -> PTerm -> [PDecl] -> (PTerm, PTerm, [PDecl])
19+desugarAs lhs rhs whereblock
20+ = (lhs', bindOnRight rhs pats, map (bindInWhereDecl pats) whereblock)
2221 where
23− bindPats :: [(Name, FC, PTerm)] -> PTerm -> PTerm
24− bindPats [] rhs = rhs
25− bindPats ((n, fc, tm) : ps) rhs
26− = PLet fc n NoFC Placeholder tm (bindPats ps rhs)
22+ (lhs', pats) = runState (collectAs (replaceUnderscore lhs)) []
23+
24+ bindOnRight :: PTerm -> [(Name, FC, PTerm)] -> PTerm
25+ bindOnRight = foldr (\(n, fc, tm) -> PLet fc n NoFC Placeholder tm)
26+
27+ bindInWhereDecl :: [(Name, FC, PTerm)] -> PDecl -> PDecl
28+ bindInWhereDecl pats (PClauses fc opts n clauses)
29+ = PClauses fc opts n $ map (bindInWhereClause pats) clauses
30+ bindInWhereDecl _ d = d
31+
32+ bindInWhereClause :: [(Name, FC, PTerm)] -> PClause -> PClause
33+ bindInWhereClause pats (PClause fc n lhs ws rhs wb)
34+ = let bound = [ n | (PRef _ _ n) <- universe lhs ]
35+ pats' = filter (not . (`elem` bound) . \(n,_,_) -> n) pats
36+ rhs' = bindOnRight rhs pats' in
37+ PClause fc n lhs ws rhs' $ map (bindInWhereDecl pats') wb
38+ bindInWhereClause _ c = c
2739
2840collectAs :: PTerm -> State [(Name, FC, PTerm)] PTerm
2941collectAs (PAs fc n tm) = do tm' <- collectAs tm
src/Idris/Elab/Clause.hs+2−2
@@ -683,11 +683,11 @@ elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
683683 logElab 5 $ "Elaborated impossible case " ++ showTmImpls lhs ++
684684 "\n" ++ show ptm
685685 return (Left ptm, lhs)
686−elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as whereblock)
686+elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as whereblock_as)
687687 = do let tcgen = Dictionary `elem` opts
688688 push_estack fname False
689689 ctxt <- getContext
690− let (lhs_in, rhs_in) = desugarAs lhs_in_as rhs_in_as
690+ let (lhs_in, rhs_in, whereblock) = desugarAs lhs_in_as rhs_in_as whereblock_as
691691
692692 -- Build the LHS as an "Infer", and pull out its type and
693693 -- pattern bindings
test/TestData.hs+2−1
@@ -71,7 +71,8 @@ testFamiliesData = [
7171 ( 16, ANY ),
7272 ( 17, ANY ),
7373 ( 18, ANY ),
74− ( 19, ANY )]),
74+ ( 19, ANY ),
75+ ( 20, ANY )]),
7576 ("bignum", "Bignum",
7677 [ ( 1, ANY ),
7778 ( 2, ANY )]),
test/basic020/basic020.idrnew file+42
@@ -0,0 +1,42 @@
1+%default total
2+
3+data Ty = Ctor Int
4+
5+fn : Ty -> Ty
6+fn m@(Ctor _) = y
7+ where
8+ y = m -- from @ pattern
9+
10+asPatternVisibleInWhere : fn (Ctor 42) = Ctor 42
11+asPatternVisibleInWhere = Refl
12+
13+fn2 : Ty -> Ty
14+fn2 m@(Ctor _) = y (Ctor 99)
15+ where
16+ y m = m -- should be the arg `m`, not the @ pattern
17+
18+lhsVariablesShadowAsPattern : fn2 (Ctor 42) = Ctor 99
19+lhsVariablesShadowAsPattern = Refl
20+
21+fn3 : Ty -> Ty
22+fn3 m@(Ctor _) = y (Ctor 99)
23+ where
24+ y m = z
25+ where
26+ z = m -- should be y's arg `m`, not @ pattern
27+
28+nestedWhereShadowsAsPattern : fn3 (Ctor 42) = Ctor 99
29+nestedWhereShadowsAsPattern = Refl
30+
31+fn4 : Ty -> Ty
32+fn4 m@(Ctor _) = y (Ctor 99)
33+ where
34+ y _ = z
35+ where
36+ z = m -- should be @ pattern
37+
38+nestedWhereExposesAsPattern : fn4 (Ctor 42) = Ctor 42
39+nestedWhereExposesAsPattern = Refl
40+
41+main : IO ()
42+main = putStrLn "OK"
test/basic020/expectednew file+1
@@ -0,0 +1 @@
1+OK
test/basic020/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ basic020.idr -o basic020
3+./basic020
4+rm -f basic020 *.ibc