mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-21 14:09:30 +03:00
Replace _ patterns with fresh variables under @-patterns
Also, add test. Fixes #1806.
This commit is contained in:
parent
68e96f0871
commit
0b23ef2a19
@ -526,6 +526,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
|
||||
@ -752,6 +759,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
|
||||
|
@ -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
|
||||
@ -497,7 +499,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
|
||||
@ -724,7 +726,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
|
||||
@ -768,7 +770,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)
|
||||
|
||||
|
||||
{-!
|
||||
@ -830,7 +832,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'
|
||||
@ -869,7 +871,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'
|
||||
@ -905,10 +907,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
|
||||
|
@ -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
|
||||
@ -695,7 +698,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
|
||||
@ -737,7 +740,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
|
||||
!-}
|
||||
@ -774,7 +777,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
|
||||
@ -809,7 +812,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
|
||||
|
@ -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,23 @@ 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 replaceUnderscore' tm) 0
|
||||
where
|
||||
fresh :: State Int Name
|
||||
fresh = flip sMN "underscorePatVar" <$> get
|
||||
replaceUnderscore' :: PTerm -> State Int PTerm
|
||||
replaceUnderscore' Placeholder = PRef emptyFC <$> fresh
|
||||
replaceUnderscore' tm = return tm
|
||||
|
27
test/sugar005/As.idr
Normal file
27
test/sugar005/As.idr
Normal file
@ -0,0 +1,27 @@
|
||||
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
|
||||
|
||||
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
|
||||
|
6
test/sugar005/expected
Normal file
6
test/sugar005/expected
Normal file
@ -0,0 +1,6 @@
|
||||
Nothing
|
||||
Just 1
|
||||
Nothing
|
||||
Just 1
|
||||
Just (5, 4)
|
||||
Nothing
|
4
test/sugar005/run
Executable file
4
test/sugar005/run
Executable file
@ -0,0 +1,4 @@
|
||||
#!/usr/bin/env bash
|
||||
idris $@ As.idr -o sugar005
|
||||
./sugar005
|
||||
rm -f sugar005 *.ibc
|
Loading…
Reference in New Issue
Block a user