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

git.iko.soy/Idris-dev

on master help sign in

Replace _ patterns with fresh variables under @-patterns

0b23ef2David Raymond Christiansen12 years ago

idris.cabal+8

compare with master

unifiedsplit

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

526 test/sugar003/run

527 test/sugar003/*.idr

528 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+

529

536

530 test/totality001/run

537 test/totality001/run

531 test/totality001/*.idr

538 test/totality001/*.idr

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

752 , time >= 1.4 && < 1.6

759 , time >= 1.4 && < 1.6

753 , transformers < 0.5

760 , transformers < 0.5

754 , trifecta >= 1.1 && < 1.6

761 , trifecta >= 1.1 && < 1.6

762+ , uniplate >=1.6 && < 1.7

755 , unordered-containers < 0.3

763 , unordered-containers < 0.3

756 , utf8-string < 0.4

764 , utf8-string < 0.4

757 , vector < 0.11

765 , vector < 0.11

src/Idris/AbsSyntaxTree.hs+11−9

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

1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

2− TypeSynonymInstances, PatternGuards #-}

2+ DeriveDataTypeable, TypeSynonymInstances, PatternGuards #-}

4module Idris.AbsSyntaxTree where

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

21import Control.Monad.Trans.State.Strict

22import Control.Monad.Trans.Except

24+import Data.Data (Data)

24import Data.Function (on)

25import Data.Function (on)

25import Data.List hiding (group)

26import Data.List hiding (group)

26import Data.Char

27import Data.Char

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

31import Data.Word (Word)

32import Data.Word (Word)

32import Data.Maybe (fromMaybe, mapMaybe)

33import Data.Maybe (fromMaybe, mapMaybe)

33import Data.Traversable (Traversable)

34import Data.Traversable (Traversable)

35+import Data.Typeable

34import Data.Foldable (Foldable)

36import Data.Foldable (Foldable)

36import Debug.Trace

38import Debug.Trace

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

479

481

480

482

481data Static = Static | Dynamic

483data Static = Static | Dynamic

482− deriving (Show, Eq)

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

483{-!

485{-!

484deriving instance Binary Static

486deriving instance Binary Static

485deriving instance NFData Static

487deriving instance NFData Static

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

497 | TacImp { pargopts :: [ArgOpt],

499 | TacImp { pargopts :: [ArgOpt],

498 pstatic :: Static,

500 pstatic :: Static,

499 pscript :: PTerm }

501 pscript :: PTerm }

500− deriving (Show, Eq)

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

501

503

502{-!

504{-!

503deriving instance Binary Plicity

505deriving instance Binary Plicity

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

724-- (map (updateDNs ns) ds)

726-- (map (updateDNs ns) ds)

725-- updateDNs ns c = c

727-- updateDNs ns c = c

726

728

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

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

728

730

729-- | High level language terms

731-- | High level language terms

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

732data 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

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

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

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

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

770 | PUnquote PTerm -- ^ ,Term

772 | PUnquote PTerm -- ^ ,Term

771− deriving Eq

773+ deriving (Eq, Data, Typeable)

772

774

773

775

774{-!

776{-!

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

830 | TFail [ErrorReportPart]

832 | TFail [ErrorReportPart]

831 | Qed | Abandon

833 | Qed | Abandon

832 | SourceFC

834 | SourceFC

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

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

834{-!

836{-!

835deriving instance Binary PTactic'

837deriving instance Binary PTactic'

836deriving instance NFData PTactic'

838deriving instance NFData PTactic'

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

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

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

870 | DoLet FC Name t t

872 | DoLet FC Name t t

871 | DoLetP FC t t

873 | DoLetP FC t t

872− deriving (Eq, Functor)

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

873{-!

875{-!

874deriving instance Binary PDo'

876deriving instance Binary PDo'

875deriving instance NFData PDo'

877deriving instance NFData PDo'

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

905 pname :: Name,

907 pname :: Name,

906 getScript :: t,

908 getScript :: t,

907 getTm :: t }

909 getTm :: t }

908− deriving (Show, Eq, Functor)

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

909

911

910data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg

912data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg

911− deriving (Show, Eq)

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

912

914

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

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

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

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

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

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

27import Debug.Trace

28import qualified Data.Map.Strict as Map

29import Data.Char

30+import Data.Data (Data)

30import Numeric (showIntAtBase)

31import Numeric (showIntAtBase)

31import qualified Data.Text as T

32import qualified Data.Text as T

32import Data.List hiding (insert)

33import Data.List hiding (insert)

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

34import Data.Maybe (listToMaybe)

35import Data.Maybe (listToMaybe)

35import Data.Foldable (Foldable)

36import Data.Foldable (Foldable)

36import Data.Traversable (Traversable)

37import Data.Traversable (Traversable)

38+import Data.Typeable (Typeable)

37import Data.Vector.Unboxed (Vector)

39import Data.Vector.Unboxed (Vector)

38import qualified Data.Vector.Unboxed as V

40import qualified Data.Vector.Unboxed as V

39import qualified Data.Binary as B

41import qualified Data.Binary as B

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

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

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

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

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

53 }

55 }

56+ deriving (Data, Typeable)

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

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

56instance Eq FC where

59instance Eq FC where

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

111 | NamePart Name

114 | NamePart Name

112 | TermPart Term

115 | TermPart Term

113 | SubReport [ErrorReportPart]

116 | SubReport [ErrorReportPart]

114− deriving (Show, Eq)

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

115

118

116

119

117-- Please remember to keep Err synchronised with

120-- Please remember to keep Err synchronised with

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

159 | LoadingFailed String (Err' t)

162 | LoadingFailed String (Err' t)

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

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

161 | ReflectionFailed String (Err' t)

164 | ReflectionFailed String (Err' t)

162− deriving (Eq, Functor)

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

163

166

164type Err = Err' Term

167type Err = Err' Term

165

168

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

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

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

308 | SN SpecialName -- ^ Decorated function names

311 | SN SpecialName -- ^ Decorated function names

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

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

310− deriving (Eq, Ord)

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

311

314

312txt :: String -> T.Text

315txt :: String -> T.Text

313txt = T.pack

316txt = T.pack

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

344 | CaseN Name

347 | CaseN Name

345 | ElimN Name

348 | ElimN Name

346 | InstanceCtorN Name

349 | InstanceCtorN Name

347− deriving (Eq, Ord)

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

348{-!

351{-!

349deriving instance Binary SpecialName

352deriving instance Binary SpecialName

350deriving instance NFData SpecialName

353deriving instance NFData SpecialName

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

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

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

495

498

496data NativeTy = IT8 | IT16 | IT32 | IT64

499data NativeTy = IT8 | IT16 | IT32 | IT64

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

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

498

501

499instance Pretty NativeTy OutputAnnotation where

502instance Pretty NativeTy OutputAnnotation where

500 pretty IT8 = text "Bits8"

503 pretty IT8 = text "Bits8"

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

504

507

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

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

506 | ITVec NativeTy Int

509 | ITVec NativeTy Int

507− deriving (Show, Eq, Ord)

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

508

511

509intTyName :: IntTy -> String

512intTyName :: IntTy -> String

510intTyName ITNative = "Int"

513intTyName ITNative = "Int"

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

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

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

515

518

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

519data 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)

518{-!

521{-!

519deriving instance NFData IntTy

522deriving instance NFData IntTy

520deriving instance NFData NativeTy

523deriving instance NFData NativeTy

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

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

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

549 | AType ArithTy | StrType

552 | AType ArithTy | StrType

551− deriving (Eq, Ord)

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

552{-!

555{-!

553deriving instance Binary Const

556deriving instance Binary Const

554deriving instance NFData Const

557deriving instance NFData Const

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

639constDocs prim = "Undocumented"

642constDocs prim = "Undocumented"

640

643

641data Universe = NullType | UniqueType | AllTypes

644data Universe = NullType | UniqueType | AllTypes

642− deriving (Eq, Ord)

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

643

646

644instance Show Universe where

647instance Show Universe where

645 show UniqueType = "UniqueType"

648 show UniqueType = "UniqueType"

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

653 | RUType Universe

656 | RUType Universe

654 | RForce Raw

657 | RForce Raw

655 | RConstant Const

658 | RConstant Const

656− deriving (Show, Eq)

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

657

660

658instance Sized Raw where

661instance Sized Raw where

659 size (Var name) = 1

662 size (Var name) = 1

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

695 | PVar { binderTy :: !b }

698 | PVar { binderTy :: !b }

696 -- ^ A pattern variable

699 -- ^ A pattern variable

697 | PVTy { binderTy :: !b }

700 | PVTy { binderTy :: !b }

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

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

699{-!

702{-!

700deriving instance Binary Binder

703deriving instance Binary Binder

701deriving instance NFData Binder

704deriving instance NFData Binder

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

737-- | Universe expressions for universe checking

740-- | Universe expressions for universe checking

738data UExp = UVar Int -- ^ universe variable

741data UExp = UVar Int -- ^ universe variable

739 | UVal Int -- ^ explicit universe level

742 | UVal Int -- ^ explicit universe level

740− deriving (Eq, Ord)

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

741{-!

744{-!

742deriving instance NFData UExp

745deriving instance NFData UExp

743!-}

746!-}

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

774 | Ref

777 | Ref

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

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

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

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

777− deriving (Show, Ord)

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

778{-!

781{-!

779deriving instance Binary NameType

782deriving instance Binary NameType

780deriving instance NFData NameType

783deriving instance NFData NameType

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

809 | Impossible -- ^ special case for totality checking

812 | Impossible -- ^ special case for totality checking

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

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

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

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

812− deriving (Ord, Functor)

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

813{-!

816{-!

814deriving instance Binary TT

817deriving instance Binary TT

815deriving instance NFData TT

818deriving instance NFData TT

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

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

3import Idris.Core.TT

4import Idris.AbsSyntax

6+import Control.Applicative

5import Control.Monad.State.Strict

7import Control.Monad.State.Strict

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

10+

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

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

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

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

9desugarAs lhs rhs

13desugarAs lhs rhs

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

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

11 (lhs', bindPats pats rhs)

15 (lhs', bindPats pats rhs)

12 where

16 where

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

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

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

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

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

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

22collectAs :: 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

20 pats <- get

24 pats <- get

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

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

22 return tm'

26 return tm'

23−collectAs (PApp fc t as)

27+collectAs (PApp fc t as)

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

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

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

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

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

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

27collectAs x = return x

31collectAs x = return x

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