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

git.iko.soy/Idris-dev

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

Replace _ patterns with fresh variables under @-patterns

commit02d26ec1dca6546fa0927bb65e04d2be4cabafe4 authorDavid Christiansen <david@davidchristiansen.dk> dateTue 13 Jan 2015, 08:30 (12 years ago) parent267b79c 48fd842

7 files changed+110−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+24−4 test/sugar005/As.idr+36 test/sugar005/expected+9 test/sugar005/run+4

idris.cabal+8

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

529529 test/sugar003/run

530530 test/sugar003/*.idr

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

532539

533540 test/totality001/run

534541 test/totality001/*.idr

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

755762 , time >= 1.4 && < 1.6

756763 , transformers < 0.5

757764 , trifecta >= 1.1 && < 1.6

765+ , uniplate >=1.6 && < 1.7

758766 , unordered-containers < 0.3

759767 , utf8-string < 0.4

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

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

499501 | TacImp { pargopts :: [ArgOpt],

500502 pstatic :: Static,

501503 pscript :: PTerm }

502− deriving (Show, Eq)

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

503505

504506{-!

505507deriving instance Binary Plicity

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

732734-- (map (updateDNs ns) ds)

733735-- updateDNs ns c = c

734736

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

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

736738

737739-- | High level language terms

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

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

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

778780 | PUnquote PTerm -- ^ ,Term

779− deriving Eq

781+ deriving (Eq, Data, Typeable)

780782

781783

782784{-!

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

838840 | TFail [ErrorReportPart]

839841 | Qed | Abandon

840842 | SourceFC

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

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

842844{-!

843845deriving instance Binary PTactic'

844846deriving instance NFData PTactic'

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

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

878880 | DoLet FC Name t t

879881 | DoLetP FC t t

880− deriving (Eq, Functor)

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

881883{-!

882884deriving instance Binary PDo'

883885deriving instance NFData PDo'

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

913915 pname :: Name,

914916 getScript :: t,

915917 getTm :: t }

916− deriving (Show, Eq, Functor)

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

917919

918920data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg

919− deriving (Show, Eq)

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

920922

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

922924 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

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

707710 | PVar { binderTy :: !b }

708711 -- ^ A pattern variable

709712 | PVTy { binderTy :: !b }

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

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

711714{-!

712715deriving instance Binary Binder

713716deriving instance NFData Binder

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

749752-- | Universe expressions for universe checking

750753data UExp = UVar Int -- ^ universe variable

751754 | UVal Int -- ^ explicit universe level

752− deriving (Eq, Ord)

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

753756{-!

754757deriving instance NFData UExp

755758!-}

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

786789 | Ref

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

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

789− deriving (Show, Ord)

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

790793{-!

791794deriving instance Binary NameType

792795deriving instance NFData NameType

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

821824 | Impossible -- ^ special case for totality checking

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

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

824− deriving (Ord, Functor)

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

825828{-!

826829deriving instance Binary TT

827830deriving instance NFData TT

src/Idris/Elab/AsPat.hs+24−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,29 @@ 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 (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