02d26ec · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1841 from david-christiansen/issue/1806

02d26ecDavid Christiansen12 years ago

idris.cabal+8

compare with master

unifiedsplit

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

529 test/sugar003/run

530 test/sugar003/*.idr

531 test/sugar003/expected

532+ test/sugar004/run

533+ test/sugar004/*.idr

534+ test/sugar004/expected

535+ test/sugar005/run

536+ test/sugar005/*.idr

537+ test/sugar005/expected

538+

532

539

533 test/totality001/run

540 test/totality001/run

534 test/totality001/*.idr

541 test/totality001/*.idr

@@ -755,6 +762,7 @@ Library

755 , time >= 1.4 && < 1.6

762 , time >= 1.4 && < 1.6

756 , transformers < 0.5

763 , transformers < 0.5

757 , trifecta >= 1.1 && < 1.6

764 , trifecta >= 1.1 && < 1.6

765+ , uniplate >=1.6 && < 1.7

758 , unordered-containers < 0.3

766 , unordered-containers < 0.3

759 , utf8-string < 0.4

767 , utf8-string < 0.4

760 , vector < 0.11

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

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

499 | TacImp { pargopts :: [ArgOpt],

501 | TacImp { pargopts :: [ArgOpt],

500 pstatic :: Static,

502 pstatic :: Static,

501 pscript :: PTerm }

503 pscript :: PTerm }

502− deriving (Show, Eq)

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

503

505

504{-!

506{-!

505deriving instance Binary Plicity

507deriving instance Binary Plicity

@@ -732,7 +734,7 @@ updateNs ns t = mapPT updateRef t

732-- (map (updateDNs ns) ds)

734-- (map (updateDNs ns) ds)

733-- updateDNs ns c = c

735-- updateDNs ns c = c

734

736

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

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

736

738

737-- | High level language terms

739-- | High level language terms

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

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

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

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

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

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

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

778 | PUnquote PTerm -- ^ ,Term

780 | PUnquote PTerm -- ^ ,Term

779− deriving Eq

781+ deriving (Eq, Data, Typeable)

780

782

781

783

782{-!

784{-!

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

838 | TFail [ErrorReportPart]

840 | TFail [ErrorReportPart]

839 | Qed | Abandon

841 | Qed | Abandon

840 | SourceFC

842 | SourceFC

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

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

842{-!

844{-!

843deriving instance Binary PTactic'

845deriving instance Binary PTactic'

844deriving instance NFData PTactic'

846deriving instance NFData PTactic'

@@ -877,7 +879,7 @@ data PDo' t = DoExp FC t

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

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

878 | DoLet FC Name t t

880 | DoLet FC Name t t

879 | DoLetP FC t t

881 | DoLetP FC t t

880− deriving (Eq, Functor)

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

881{-!

883{-!

882deriving instance Binary PDo'

884deriving instance Binary PDo'

883deriving instance NFData PDo'

885deriving instance NFData PDo'

@@ -913,10 +915,10 @@ data PArg' t = PImp { priority :: Int,

913 pname :: Name,

915 pname :: Name,

914 getScript :: t,

916 getScript :: t,

915 getTm :: t }

917 getTm :: t }

916− deriving (Show, Eq, Functor)

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

917

919

918data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg

920data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg

919− deriving (Show, Eq)

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

920

922

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

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

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

924 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

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

707 | PVar { binderTy :: !b }

710 | PVar { binderTy :: !b }

708 -- ^ A pattern variable

711 -- ^ A pattern variable

709 | PVTy { binderTy :: !b }

712 | PVTy { binderTy :: !b }

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

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

711{-!

714{-!

712deriving instance Binary Binder

715deriving instance Binary Binder

713deriving instance NFData Binder

716deriving instance NFData Binder

@@ -749,7 +752,7 @@ raw_unapply t = ua [] t where

749-- | Universe expressions for universe checking

752-- | Universe expressions for universe checking

750data UExp = UVar Int -- ^ universe variable

753data UExp = UVar Int -- ^ universe variable

751 | UVal Int -- ^ explicit universe level

754 | UVal Int -- ^ explicit universe level

752− deriving (Eq, Ord)

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

753{-!

756{-!

754deriving instance NFData UExp

757deriving instance NFData UExp

755!-}

758!-}

@@ -786,7 +789,7 @@ data NameType = Bound

786 | Ref

789 | Ref

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

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

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

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

789− deriving (Show, Ord)

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

790{-!

793{-!

791deriving instance Binary NameType

794deriving instance Binary NameType

792deriving instance NFData NameType

795deriving instance NFData NameType

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

821 | Impossible -- ^ special case for totality checking

824 | Impossible -- ^ special case for totality checking

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

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

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

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

824− deriving (Ord, Functor)

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

825{-!

828{-!

826deriving instance Binary TT

829deriving instance Binary TT

827deriving instance NFData TT

830deriving instance NFData TT

src/Idris/Elab/AsPat.hs+24−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,29 @@ 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 (underAs replaceUnderscore') tm) 0

37+ where

38+ underAs :: (PTerm -> State Int PTerm) -> PTerm -> State Int PTerm

39+ underAs f (PAs fc n tm) = PAs fc n <$> transformM f tm

40+ underAs f x = return x

41+

42+ fresh :: State Int Name

43+ fresh = modify (+1) >> flip sMN "underscorePatVar" <$> get

44+

45+

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

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

48+ replaceUnderscore' tm = return tm

test/sugar005/As.idrnew file+36

@@ -0,0 +1,36 @@

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+-- Test two @-patterns

20+same : Nat -> Nat -> Maybe Nat

21+same x@(S _) y@(S _) = Just $ x + y

22+same Z Z = Just 42

23+same _ _ = Nothing

24+

25+namespace Main

26+ main : IO ()

27+ main = do print $ isS 0

28+ print $ isS 1

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

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

31+ print $ isSS 5

32+ print $ isSS 0

33+ print $ same 1 1

34+ print $ same 0 0

35+ print $ same 1 0

36+

test/sugar005/expectednew file+9

@@ -0,0 +1,9 @@

1+Nothing

2+Just 1

3+Nothing

4+Just 1

5+Just (5, 4)

6+Nothing

7+Just 2

8+Just 42

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