f436c5f · Idris-dev · git.iko.soy

CHANGELOG.md+3

compare with master

unifiedsplit

@@ -2,6 +2,9 @@

2

3+ Addition of `Text.Literate`, a module for working with literate

4 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.

5

8

6# New in 1.1.1

9# New in 1.1.1

7

10

src/Idris/Elab/AsPat.hs+21−9

@@ -12,18 +12,30 @@ import Idris.Core.TT

12

13import Control.Applicative

14import Control.Monad.State.Strict

15−import Data.Generics.Uniplate.Data (transformM)

15+import Data.Generics.Uniplate.Data (transformM, universe)

16

17-- | Desugar by changing x@y on lhs to let x = y in ... or rhs

18−desugarAs :: PTerm -> PTerm -> (PTerm, PTerm)

18+desugarAs :: PTerm -> PTerm -> [PDecl] -> (PTerm, PTerm, [PDecl])

19−desugarAs lhs rhs

19+desugarAs lhs rhs whereblock

20− = let (lhs', pats) = runState (collectAs (replaceUnderscore lhs)) [] in

20+ = (lhs', bindOnRight rhs pats, map (bindInWhereDecl pats) whereblock)

21− (lhs', bindPats pats rhs)

22 where

21 where

22+ (lhs', pats) = runState (collectAs (replaceUnderscore lhs)) []

23+

23− bindPats :: [(Name, FC, PTerm)] -> PTerm -> PTerm

24+ bindOnRight :: PTerm -> [(Name, FC, PTerm)] -> PTerm

24− bindPats [] rhs = rhs

25− bindPats ((n, fc, tm) : ps) rhs

26− = PLet fc n NoFC Placeholder tm (bindPats ps rhs)

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

27

39

28collectAs :: PTerm -> State [(Name, FC, PTerm)] PTerm

40collectAs :: PTerm -> State [(Name, FC, PTerm)] PTerm

29collectAs (PAs fc n tm) = do tm' <- collectAs tm

41collectAs (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 [])

683 logElab 5 $ "Elaborated impossible case " ++ showTmImpls lhs ++

684 "\n" ++ show ptm

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

687 = do let tcgen = Dictionary `elem` opts

688 push_estack fname False

689 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

691

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

693 -- pattern bindings

test/TestData.hs+2−1

@@ -71,7 +71,8 @@ testFamiliesData = [

71 ( 16, ANY ),

72 ( 17, ANY ),

73 ( 18, ANY ),

74− ( 19, ANY )]),

74+ ( 19, ANY ),

75+ ( 20, ANY )]),

75 ("bignum", "Bignum",

76 ("bignum", "Bignum",

76 [ ( 1, ANY ),

77 [ ( 1, ANY ),

77 ( 2, ANY )]),

78 ( 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