0b23ef2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Replace _ patterns with fresh variables under @-patterns

Also, add test. Fixes #1806.

commit0b23ef2a1925401042f6e818604f9eb4e8278bba authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSat 10 Jan 2015, 17:13 (12 years ago) parent68e96f0

7 files changed+92−28

compare with master

unifiedsplit

idris.cabal+8 src/Idris/AbsSyntaxTree.hs+11−9 src/Idris/Core/TT.hs+18−15 src/Idris/Elab/AsPat.hs+18−4 test/sugar005/As.idr+27 test/sugar005/expected+6 test/sugar005/run+4

idris.cabal+8

@@ -526,6 +526,13 @@ Extra-source-files:

526526 test/sugar003/run

527527 test/sugar003/*.idr

528528 test/sugar003/expected

529+ test/sugar004/run

530+ test/sugar004/*.idr

531+ test/sugar004/expected

532+ test/sugar005/run

533+ test/sugar005/*.idr

534+ test/sugar005/expected

535+

529536

530537 test/totality001/run

531538 test/totality001/*.idr

@@ -752,6 +759,7 @@ Library

752759 , time >= 1.4 && < 1.6

753760 , transformers < 0.5

754761 , trifecta >= 1.1 && < 1.6

762+ , uniplate >=1.6 && < 1.7

755763 , unordered-containers < 0.3

756764 , utf8-string < 0.4

757765 , vector < 0.11

src/Idris/AbsSyntaxTree.hs+11−9

@@ -1,5 +1,5 @@

11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

2− TypeSynonymInstances, PatternGuards #-}

2+ DeriveDataTypeable, TypeSynonymInstances, PatternGuards #-}

44module Idris.AbsSyntaxTree where

@@ -21,6 +21,7 @@ import System.IO

2121import Control.Monad.Trans.State.Strict

2222import Control.Monad.Trans.Except

2323

24+import Data.Data (Data)

2425import Data.Function (on)

2526import Data.List hiding (group)

2627import Data.Char

@@ -31,6 +32,7 @@ import qualified Data.Set as S

3132import Data.Word (Word)

3233import Data.Maybe (fromMaybe, mapMaybe)

3334import Data.Traversable (Traversable)

35+import Data.Typeable

3436import Data.Foldable (Foldable)

3537

3638import Debug.Trace

@@ -479,7 +481,7 @@ instance Ord FixDecl where

479481

480482

481483data Static = Static | Dynamic

482− deriving (Show, Eq)

484+ deriving (Show, Eq, Data, Typeable)

483485{-!

484486deriving instance Binary Static

485487deriving instance NFData Static

@@ -497,7 +499,7 @@ data Plicity = Imp { pargopts :: [ArgOpt],

497499 | TacImp { pargopts :: [ArgOpt],

498500 pstatic :: Static,

499501 pscript :: PTerm }

500− deriving (Show, Eq)

502+ deriving (Show, Eq, Data, Typeable)

501503

502504{-!

503505deriving instance Binary Plicity

@@ -724,7 +726,7 @@ updateNs ns t = mapPT updateRef t

724726-- (map (updateDNs ns) ds)

725727-- updateDNs ns c = c

726728

727−data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show)

729+data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show, Data, Typeable)

728730

729731-- | High level language terms

730732data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language

@@ -768,7 +770,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

768770 | PNoImplicits PTerm -- ^ never run implicit converions on the term

769771 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])

770772 | PUnquote PTerm -- ^ ,Term

771− deriving Eq

773+ deriving (Eq, Data, Typeable)

772774

773775

774776{-!

@@ -830,7 +832,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

830832 | TFail [ErrorReportPart]

831833 | Qed | Abandon

832834 | SourceFC

833− deriving (Show, Eq, Functor, Foldable, Traversable)

835+ deriving (Show, Eq, Functor, Foldable, Traversable, Data, Typeable)

834836{-!

835837deriving instance Binary PTactic'

836838deriving instance NFData PTactic'

@@ -869,7 +871,7 @@ data PDo' t = DoExp FC t

869871 | DoBindP FC t t [(t,t)]

870872 | DoLet FC Name t t

871873 | DoLetP FC t t

872− deriving (Eq, Functor)

874+ deriving (Eq, Functor, Data, Typeable)

873875{-!

874876deriving instance Binary PDo'

875877deriving instance NFData PDo'

@@ -905,10 +907,10 @@ data PArg' t = PImp { priority :: Int,

905907 pname :: Name,

906908 getScript :: t,

907909 getTm :: t }

908− deriving (Show, Eq, Functor)

910+ deriving (Show, Eq, Functor, Data, Typeable)

909911

910912data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg

911− deriving (Show, Eq)

913+ deriving (Show, Eq, Data, Typeable)

912914

913915instance Sized a => Sized (PArg' a) where

914916 size (PImp p _ l nm trm) = 1 + size nm + size trm

src/Idris/Core/TT.hs+18−15

@@ -1,4 +1,4 @@

1−{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}

1+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor, DeriveDataTypeable #-}

33{-| TT is the core language of Idris. The language has:

@@ -27,6 +27,7 @@ import Control.Monad.Trans.Except (Except (..))

2727import Debug.Trace

2828import qualified Data.Map.Strict as Map

2929import Data.Char

30+import Data.Data (Data)

3031import Numeric (showIntAtBase)

3132import qualified Data.Text as T

3233import Data.List hiding (insert)

@@ -34,6 +35,7 @@ import Data.Set(Set, member, fromList, insert)

3435import Data.Maybe (listToMaybe)

3536import Data.Foldable (Foldable)

3637import Data.Traversable (Traversable)

38+import Data.Typeable (Typeable)

3739import Data.Vector.Unboxed (Vector)

3840import qualified Data.Vector.Unboxed as V

3941import qualified Data.Binary as B

@@ -51,6 +53,7 @@ data FC = FC { fc_fname :: String, -- ^ Filename

5153 fc_start :: (Int, Int), -- ^ Line and column numbers for the start of the location span

5254 fc_end :: (Int, Int) -- ^ Line and column numbers for the end of the location span

5355 }

56+ deriving (Data, Typeable)

5457

5558-- | Ignore source location equality (so deriving classes do not compare FCs)

5659instance Eq FC where

@@ -111,7 +114,7 @@ data ErrorReportPart = TextPart String

111114 | NamePart Name

112115 | TermPart Term

113116 | SubReport [ErrorReportPart]

114− deriving (Show, Eq)

117+ deriving (Show, Eq, Data, Typeable)

115118

116119

117120-- Please remember to keep Err synchronised with

@@ -159,7 +162,7 @@ data Err' t

159162 | LoadingFailed String (Err' t)

160163 | ReflectionError [[ErrorReportPart]] (Err' t)

161164 | ReflectionFailed String (Err' t)

162− deriving (Eq, Functor)

165+ deriving (Eq, Functor, Data, Typeable)

163166

164167type Err = Err' Term

165168

@@ -307,7 +310,7 @@ data Name = UN T.Text -- ^ User-provided name

307310 | NErased -- ^ Name of something which is never used in scope

308311 | SN SpecialName -- ^ Decorated function names

309312 | SymRef Int -- ^ Reference to IBC file symbol table (used during serialisation)

310− deriving (Eq, Ord)

313+ deriving (Eq, Ord, Data, Typeable)

311314

312315txt :: String -> T.Text

313316txt = T.pack

@@ -344,7 +347,7 @@ data SpecialName = WhereN Int Name Name

344347 | CaseN Name

345348 | ElimN Name

346349 | InstanceCtorN Name

347− deriving (Eq, Ord)

350+ deriving (Eq, Ord, Data, Typeable)

348351{-!

349352deriving instance Binary SpecialName

350353deriving instance NFData SpecialName

@@ -494,7 +497,7 @@ addAlist [] ctxt = ctxt

494497addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

495498

496499data NativeTy = IT8 | IT16 | IT32 | IT64

497− deriving (Show, Eq, Ord, Enum)

500+ deriving (Show, Eq, Ord, Enum, Data, Typeable)

498501

499502instance Pretty NativeTy OutputAnnotation where

500503 pretty IT8 = text "Bits8"

@@ -504,7 +507,7 @@ instance Pretty NativeTy OutputAnnotation where

504507

505508data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar

506509 | ITVec NativeTy Int

507− deriving (Show, Eq, Ord)

510+ deriving (Show, Eq, Ord, Data, Typeable)

508511

509512intTyName :: IntTy -> String

510513intTyName ITNative = "Int"

@@ -514,7 +517,7 @@ intTyName (ITChar) = "Char"

514517intTyName (ITVec ity count) = "B" ++ show (nativeTyWidth ity) ++ "x" ++ show count

515518

516519data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors https://github.com/idris-lang/Idris-dev/issues/1723

517− deriving (Show, Eq, Ord)

520+ deriving (Show, Eq, Ord, Data, Typeable)

518521{-!

519522deriving instance NFData IntTy

520523deriving instance NFData NativeTy

@@ -548,7 +551,7 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

548551 | B32V (Vector Word32) | B64V (Vector Word64)

549552 | AType ArithTy | StrType

551− deriving (Eq, Ord)

554+ deriving (Eq, Ord, Data, Typeable)

552555{-!

553556deriving instance Binary Const

554557deriving instance NFData Const

@@ -639,7 +642,7 @@ constDocs (B64V v) = "A vector of sixty-four-bit values"

639642constDocs prim = "Undocumented"

640643

641644data Universe = NullType | UniqueType | AllTypes

642− deriving (Eq, Ord)

645+ deriving (Eq, Ord, Data, Typeable)

643646

644647instance Show Universe where

645648 show UniqueType = "UniqueType"

@@ -653,7 +656,7 @@ data Raw = Var Name

653656 | RUType Universe

654657 | RForce Raw

655658 | RConstant Const

656− deriving (Show, Eq)

659+ deriving (Show, Eq, Data, Typeable)

657660

658661instance Sized Raw where

659662 size (Var name) = 1

@@ -695,7 +698,7 @@ data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}

695698 | PVar { binderTy :: !b }

696699 -- ^ A pattern variable

697700 | PVTy { binderTy :: !b }

698− deriving (Show, Eq, Ord, Functor, Foldable, Traversable)

701+ deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Typeable)

699702{-!

700703deriving instance Binary Binder

701704deriving instance NFData Binder

@@ -737,7 +740,7 @@ raw_unapply t = ua [] t where

737740-- | Universe expressions for universe checking

738741data UExp = UVar Int -- ^ universe variable

739742 | UVal Int -- ^ explicit universe level

740− deriving (Eq, Ord)

743+ deriving (Eq, Ord, Data, Typeable)

741744{-!

742745deriving instance NFData UExp

743746!-}

@@ -774,7 +777,7 @@ data NameType = Bound

774777 | Ref

775778 | DCon {nt_tag :: Int, nt_arity :: Int, nt_unique :: Bool} -- ^ Data constructor

776779 | TCon {nt_tag :: Int, nt_arity :: Int} -- ^ Type constructor

777− deriving (Show, Ord)

780+ deriving (Show, Ord, Data, Typeable)

778781{-!

779782deriving instance Binary NameType

780783deriving instance NFData NameType

@@ -809,7 +812,7 @@ data TT n = P NameType n (TT n) -- ^ named references with type

809812 | Impossible -- ^ special case for totality checking

810813 | TType UExp -- ^ the type of types at some level

811814 | UType Universe -- ^ Uniqueness type universe (disjoint from TType)

812− deriving (Ord, Functor)

815+ deriving (Ord, Functor, Data, Typeable)

813816{-!

814817deriving instance Binary TT

815818deriving instance NFData TT

src/Idris/Elab/AsPat.hs+18−4

@@ -2,12 +2,16 @@ module Idris.Elab.AsPat(desugarAs) where

33import Idris.Core.TT

44import Idris.AbsSyntax

6+import Control.Applicative

57import Control.Monad.State.Strict

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

9+import Data.Generics.Uniplate.Data (transformM)

10+

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

812desugarAs :: PTerm -> PTerm -> (PTerm, PTerm)

913desugarAs lhs rhs

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

14+ = let (lhs', pats) = runState (collectAs (replaceUnderscore lhs)) [] in

1115 (lhs', bindPats pats rhs)

1216 where

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

@@ -16,13 +20,23 @@ desugarAs lhs rhs

1620 = PLet fc n Placeholder tm (bindPats ps rhs)

1721

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

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

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

2024 pats <- get

2125 put (pats ++ [(n, fc, tm')])

2226 return tm'

23−collectAs (PApp fc t as)

27+collectAs (PApp fc t as)

2428 = do as_tm <- mapM collectAs (map getTm as)

2529 let as' = zipWith (\a tm -> a { getTm = tm }) as as_tm

2630 return (PApp fc t as') -- only valid on args

2731collectAs x = return x

2832

33+-- | Replace _-patterns under @-patterns with fresh names that can be

34+-- used on the RHS

35+replaceUnderscore :: PTerm -> PTerm

36+replaceUnderscore tm = evalState (transformM replaceUnderscore' tm) 0

37+ where

38+ fresh :: State Int Name

39+ fresh = flip sMN "underscorePatVar" <$> get

40+ replaceUnderscore' :: PTerm -> State Int PTerm

41+ replaceUnderscore' Placeholder = PRef emptyFC <$> fresh

42+ replaceUnderscore' tm = return tm

test/sugar005/As.idrnew file+27

@@ -0,0 +1,27 @@

1+module As

3+-- Test @

4+isS : Nat -> Maybe Nat

5+isS Z = Nothing

6+isS n@(S _) = Just n

8+-- Test @ under a constructor

9+hasS : List Nat -> Maybe Nat

10+hasS (Z::xs) = hasS xs

11+hasS (n@(S_)::xs) = Just n

12+hasS _ = Nothing

13+

14+-- Test nested @s

15+isSS : Nat -> Maybe (Nat, Nat)

16+isSS n@(S m@(S _)) = Just (n,m)

17+isSS _ = Nothing

18+

19+namespace Main

20+ main : IO ()

21+ main = do print $ isS 0

22+ print $ isS 1

23+ print $ hasS [0,0,0]

24+ print $ hasS [0,1,2]

25+ print $ isSS 5

26+ print $ isSS 0

27+

test/sugar005/expectednew file+6

@@ -0,0 +1,6 @@

1+Nothing

2+Just 1

3+Nothing

4+Just 1

5+Just (5, 4)

6+Nothing

test/sugar005/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ As.idr -o sugar005

3+./sugar005

4+rm -f sugar005 *.ibc