ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-21 14:09:30 +03:00
Code Issues Projects Releases Wiki Activity

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

Browse Source 
Replace _ patterns with fresh variables under @-patterns
This commit is contained in:
David Christiansen 2015-01-13 08:30:40 -08:00
commit 02d26ec1dc
7 changed files with 110 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
idris.cabal
View File

@ -529,6 +529,13 @@ Extra-source-files:
test/sugar003/run
test/sugar003/*.idr
test/sugar003/expected
test/sugar004/run
test/sugar004/*.idr
test/sugar004/expected
test/sugar005/run
test/sugar005/*.idr
test/sugar005/expected
test/totality001/run
test/totality001/*.idr
@ -755,6 +762,7 @@ Library
, time >= 1.4 && < 1.6
, transformers < 0.5
, trifecta >= 1.1 && < 1.6
, uniplate >=1.6 && < 1.7
, unordered-containers < 0.3
, utf8-string < 0.4
, vector < 0.11

20
src/Idris/AbsSyntaxTree.hs
View File

@ -1,5 +1,5 @@
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
TypeSynonymInstances, PatternGuards #-}
DeriveDataTypeable, TypeSynonymInstances, PatternGuards #-}
module Idris.AbsSyntaxTree where
@ -21,6 +21,7 @@ import System.IO
import Control.Monad.Trans.State.Strict
import Control.Monad.Trans.Except
import Data.Data (Data)
import Data.Function (on)
import Data.List hiding (group)
import Data.Char
@ -31,6 +32,7 @@ import qualified Data.Set as S
import Data.Word (Word)
import Data.Maybe (fromMaybe, mapMaybe)
import Data.Traversable (Traversable)
import Data.Typeable
import Data.Foldable (Foldable)
import Debug.Trace
@ -479,7 +481,7 @@ instance Ord FixDecl where
data Static = Static | Dynamic
deriving (Show, Eq)
deriving (Show, Eq, Data, Typeable)
{-!
deriving instance Binary Static
deriving instance NFData Static
@ -499,7 +501,7 @@ data Plicity = Imp { pargopts :: [ArgOpt],
| TacImp { pargopts :: [ArgOpt],
pstatic :: Static,
pscript :: PTerm }
deriving (Show, Eq)
deriving (Show, Eq, Data, Typeable)
{-!
deriving instance Binary Plicity
@ -732,7 +734,7 @@ updateNs ns t = mapPT updateRef t
-- (map (updateDNs ns) ds)
-- updateDNs ns c = c
data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show)
data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show, Data, Typeable)
-- | High level language terms
data 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
| PNoImplicits PTerm -- ^ never run implicit converions on the term
| PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
| PUnquote PTerm -- ^ ,Term
deriving Eq
deriving (Eq, Data, Typeable)
{-!
@ -838,7 +840,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name
| TFail [ErrorReportPart]
| Qed | Abandon
| SourceFC
deriving (Show, Eq, Functor, Foldable, Traversable)
deriving (Show, Eq, Functor, Foldable, Traversable, Data, Typeable)
{-!
deriving instance Binary PTactic'
deriving instance NFData PTactic'
@ -877,7 +879,7 @@ data PDo' t = DoExp FC t
| DoBindP FC t t [(t,t)]
| DoLet FC Name t t
| DoLetP FC t t
deriving (Eq, Functor)
deriving (Eq, Functor, Data, Typeable)
{-!
deriving instance Binary PDo'
deriving instance NFData PDo'
@ -913,10 +915,10 @@ data PArg' t = PImp { priority :: Int,
pname :: Name,
getScript :: t,
getTm :: t }
deriving (Show, Eq, Functor)
deriving (Show, Eq, Functor, Data, Typeable)
data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg
deriving (Show, Eq)
deriving (Show, Eq, Data, Typeable)
instance Sized a => Sized (PArg' a) where
size (PImp p _ l nm trm) = 1 + size nm + size trm

33
src/Idris/Core/TT.hs
View File

@ -1,4 +1,4 @@
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor, DeriveDataTypeable #-}
{-| TT is the core language of Idris. The language has:
@ -27,6 +27,7 @@ import Control.Monad.Trans.Except (Except (..))
import Debug.Trace
import qualified Data.Map.Strict as Map
import Data.Char
import Data.Data (Data)
import Numeric (showIntAtBase)
import qualified Data.Text as T
import Data.List hiding (insert)
@ -34,6 +35,7 @@ import Data.Set(Set, member, fromList, insert)
import Data.Maybe (listToMaybe)
import Data.Foldable (Foldable)
import Data.Traversable (Traversable)
import Data.Typeable (Typeable)
import Data.Vector.Unboxed (Vector)
import qualified Data.Vector.Unboxed as V
import qualified Data.Binary as B
@ -51,6 +53,7 @@ data FC = FC { fc_fname :: String, -- ^ Filename
fc_start :: (Int, Int), -- ^ Line and column numbers for the start of the location span
fc_end :: (Int, Int) -- ^ Line and column numbers for the end of the location span
}
deriving (Data, Typeable)
-- | Ignore source location equality (so deriving classes do not compare FCs)
instance Eq FC where
@ -111,7 +114,7 @@ data ErrorReportPart = TextPart String
| NamePart Name
| TermPart Term
| SubReport [ErrorReportPart]
deriving (Show, Eq)
deriving (Show, Eq, Data, Typeable)
-- Please remember to keep Err synchronised with
@ -159,7 +162,7 @@ data Err' t
| LoadingFailed String (Err' t)
| ReflectionError [[ErrorReportPart]] (Err' t)
| ReflectionFailed String (Err' t)
deriving (Eq, Functor)
deriving (Eq, Functor, Data, Typeable)
type Err = Err' Term
@ -307,7 +310,7 @@ data Name = UN T.Text -- ^ User-provided name
| NErased -- ^ Name of something which is never used in scope
| SN SpecialName -- ^ Decorated function names
| SymRef Int -- ^ Reference to IBC file symbol table (used during serialisation)
deriving (Eq, Ord)
deriving (Eq, Ord, Data, Typeable)
txt :: String -> T.Text
txt = T.pack
@ -344,7 +347,7 @@ data SpecialName = WhereN Int Name Name
| CaseN Name
| ElimN Name
| InstanceCtorN Name
deriving (Eq, Ord)
deriving (Eq, Ord, Data, Typeable)
{-!
deriving instance Binary SpecialName
deriving instance NFData SpecialName
@ -494,7 +497,7 @@ addAlist [] ctxt = ctxt
addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)
data NativeTy = IT8 | IT16 | IT32 | IT64
deriving (Show, Eq, Ord, Enum)
deriving (Show, Eq, Ord, Enum, Data, Typeable)
instance Pretty NativeTy OutputAnnotation where
pretty IT8 = text "Bits8"
@ -504,7 +507,7 @@ instance Pretty NativeTy OutputAnnotation where
data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar
| ITVec NativeTy Int
deriving (Show, Eq, Ord)
deriving (Show, Eq, Ord, Data, Typeable)
intTyName :: IntTy -> String
intTyName ITNative = "Int"
@ -514,7 +517,7 @@ intTyName (ITChar) = "Char"
intTyName (ITVec ity count) = "B" ++ show (nativeTyWidth ity) ++ "x" ++ show count
data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors https://github.com/idris-lang/Idris-dev/issues/1723
deriving (Show, Eq, Ord)
deriving (Show, Eq, Ord, Data, Typeable)
{-!
deriving instance NFData IntTy
deriving instance NFData NativeTy
@ -548,7 +551,7 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String
| B32V (Vector Word32) | B64V (Vector Word64)
| AType ArithTy | StrType
| PtrType | ManagedPtrType | BufferType | VoidType | Forgot
deriving (Eq, Ord)
deriving (Eq, Ord, Data, Typeable)
{-!
deriving instance Binary Const
deriving instance NFData Const
@ -639,7 +642,7 @@ constDocs (B64V v) = "A vector of sixty-four-bit values"
constDocs prim = "Undocumented"
data Universe = NullType | UniqueType | AllTypes
deriving (Eq, Ord)
deriving (Eq, Ord, Data, Typeable)
instance Show Universe where
show UniqueType = "UniqueType"
@ -653,7 +656,7 @@ data Raw = Var Name
| RUType Universe
| RForce Raw
| RConstant Const
deriving (Show, Eq)
deriving (Show, Eq, Data, Typeable)
instance Sized Raw where
size (Var name) = 1
@ -707,7 +710,7 @@ data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}
| PVar { binderTy :: !b }
-- ^ A pattern variable
| PVTy { binderTy :: !b }
deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Typeable)
{-!
deriving instance Binary Binder
deriving instance NFData Binder
@ -749,7 +752,7 @@ raw_unapply t = ua [] t where
-- | Universe expressions for universe checking
data UExp = UVar Int -- ^ universe variable
| UVal Int -- ^ explicit universe level
deriving (Eq, Ord)
deriving (Eq, Ord, Data, Typeable)
{-!
deriving instance NFData UExp
!-}
@ -786,7 +789,7 @@ data NameType = Bound
| Ref
| DCon {nt_tag :: Int, nt_arity :: Int, nt_unique :: Bool} -- ^ Data constructor
| TCon {nt_tag :: Int, nt_arity :: Int} -- ^ Type constructor
deriving (Show, Ord)
deriving (Show, Ord, Data, Typeable)
{-!
deriving instance Binary NameType
deriving instance NFData NameType
@ -821,7 +824,7 @@ data TT n = P NameType n (TT n) -- ^ named references with type
| Impossible -- ^ special case for totality checking
| TType UExp -- ^ the type of types at some level
| UType Universe -- ^ Uniqueness type universe (disjoint from TType)
deriving (Ord, Functor)
deriving (Ord, Functor, Data, Typeable)
{-!
deriving instance Binary TT
deriving instance NFData TT

28
src/Idris/Elab/AsPat.hs
View File

@ -2,12 +2,16 @@ module Idris.Elab.AsPat(desugarAs) where
import Idris.Core.TT
import Idris.AbsSyntax
import Control.Applicative
import Control.Monad.State.Strict
-- Desugar by changing x@y on lhs to let x = y in ... or rhs
import Data.Generics.Uniplate.Data (transformM)
-- | Desugar by changing x@y on lhs to let x = y in ... or rhs
desugarAs :: PTerm -> PTerm -> (PTerm, PTerm)
desugarAs lhs rhs
= let (lhs', pats) = runState (collectAs lhs) [] in
= let (lhs', pats) = runState (collectAs (replaceUnderscore lhs)) [] in
(lhs', bindPats pats rhs)
where
bindPats :: [(Name, FC, PTerm)] -> PTerm -> PTerm
@ -16,13 +20,29 @@ desugarAs lhs rhs
= PLet fc n Placeholder tm (bindPats ps rhs)
collectAs :: PTerm -> State [(Name, FC, PTerm)] PTerm
collectAs (PAs fc n tm) = do tm' <- collectAs tm
collectAs (PAs fc n tm) = do tm' <- collectAs tm
pats <- get
put (pats ++ [(n, fc, tm')])
return tm'
collectAs (PApp fc t as)
collectAs (PApp fc t as)
= do as_tm <- mapM collectAs (map getTm as)
let as' = zipWith (\a tm -> a { getTm = tm }) as as_tm
return (PApp fc t as') -- only valid on args
collectAs x = return x
-- | Replace _-patterns under @-patterns with fresh names that can be
-- used on the RHS
replaceUnderscore :: PTerm -> PTerm
replaceUnderscore tm = evalState (transformM (underAs replaceUnderscore') tm) 0
where
underAs :: (PTerm -> State Int PTerm) -> PTerm -> State Int PTerm
underAs f (PAs fc n tm) = PAs fc n <$> transformM f tm
underAs f x = return x
fresh :: State Int Name
fresh = modify (+1) >> flip sMN "underscorePatVar" <$> get
replaceUnderscore' :: PTerm -> State Int PTerm
replaceUnderscore' Placeholder = PRef emptyFC <$> fresh
replaceUnderscore' tm = return tm

36
test/sugar005/As.idr Normal file
View File

@ -0,0 +1,36 @@
module As
-- Test @
isS : Nat -> Maybe Nat
isS Z = Nothing
isS n@(S _) = Just n
-- Test @ under a constructor
hasS : List Nat -> Maybe Nat
hasS (Z::xs) = hasS xs
hasS (n@(S_)::xs) = Just n
hasS _ = Nothing
-- Test nested @s
isSS : Nat -> Maybe (Nat, Nat)
isSS n@(S m@(S _)) = Just (n,m)
isSS _ = Nothing
-- Test two @-patterns
same : Nat -> Nat -> Maybe Nat
same x@(S _) y@(S _) = Just $ x + y
same Z Z = Just 42
same _ _ = Nothing
namespace Main
main : IO ()
main = do print $ isS 0
print $ isS 1
print $ hasS [0,0,0]
print $ hasS [0,1,2]
print $ isSS 5
print $ isSS 0
print $ same 1 1
print $ same 0 0
print $ same 1 0

9
test/sugar005/expected Normal file
View File

@ -0,0 +1,9 @@
Nothing
Just 1
Nothing
Just 1
Just (5, 4)
Nothing
Just 2
Just 42
Nothing

4
test/sugar005/run Executable file
View File

@ -0,0 +1,4 @@
#!/usr/bin/env bash
idris $@ As.idr -o sugar005
./sugar005
rm -f sugar005 *.ibc