eb41a1d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow capitalized pattern variables via switch

eb41a1dAhmad Salim Al-Sibahi9 years ago

CHANGELOG.md+2−1

compare with master

unifiedsplit

@@ -6,7 +6,7 @@

7## Library updates

9−+ changed rndInt in Effect.Random so that it does not alternate between odd

9++ Changed rndInt in Effect.Random so that it does not alternate between odd

10 and even.

11+ Additions to `contrib`:

12 * `Data.SortedBag`: Bag (or Multiset) implemention based on `Data.SortedMap`.

@@ -15,6 +15,7 @@

15 combinators for working with them.

17## Tool updates

18++ Added a switch `--allow-capitalized-pattern-variables` to optionally allow capitalized pattern variables after they were prohibited in 1.2.0.

18+ REPL now prints an error message if program compiled by `:exec` terminates

19+ REPL now prints an error message if program compiled by `:exec` terminates

19 abnormally.

20 abnormally.

src/Idris/AbsSyntax.hs+18−13

@@ -1847,6 +1847,8 @@ addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm

1847addImpl' inpat env infns imp_meths ist ptm

1848 = ai inpat False (zip env (repeat Nothing)) [] (mkUniqueNames env [] ptm)

1849 where

1850+ allowcap = AllowCapitalizedPatternVariables `elem` opt_cmdline (idris_options ist)

1851+

1850 topname = case ptm of

1852 topname = case ptm of

1851 PRef _ _ n -> n

1853 PRef _ _ n -> n

1852 PApp _ (PRef _ _ n) _ -> n

1854 PApp _ (PRef _ _ n) _ -> n

@@ -1855,9 +1857,9 @@ addImpl' inpat env infns imp_meths ist ptm

1855 ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm

1857 ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm

1856 ai inpat qq env ds (PRef fc fcs f)

1858 ai inpat qq env ds (PRef fc fcs f)

1857 | f `elem` infns = PInferRef fc fcs f

1859 | f `elem` infns = PInferRef fc fcs f

1858− | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds []

1860+ | not (f `elem` map fst env) = handleErr $ aiFn topname allowcap inpat inpat qq imp_meths ist fc f fc ds []

1859 ai inpat qq env ds (PHidden (PRef fc hl f))

1861 ai inpat qq env ds (PHidden (PRef fc hl f))

1860− | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [])

1862+ | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname allowcap inpat False qq imp_meths ist fc f fc ds [])

1861 ai inpat qq env ds (PRewrite fc by l r g)

1863 ai inpat qq env ds (PRewrite fc by l r g)

1862 = let l' = ai inpat qq env ds l

1864 = let l' = ai inpat qq env ds l

1863 r' = ai inpat qq env ds r

1865 r' = ai inpat qq env ds r

@@ -1887,7 +1889,7 @@ addImpl' inpat env infns imp_meths ist ptm

1887 | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)

1889 | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)

1888 | not (f `elem` map fst env)

1890 | not (f `elem` map fst env)

1889 = let as' = map (fmap (ai inpat qq env ds)) as in

1891 = let as' = map (fmap (ai inpat qq env ds)) as in

1890− handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as'

1892+ handleErr $ aiFn topname allowcap inpat False qq imp_meths ist fc f ffc ds as'

1891 | Just (Just ty) <- lookup f env =

1893 | Just (Just ty) <- lookup f env =

1892 let as' = map (fmap (ai inpat qq env ds)) as

1894 let as' = map (fmap (ai inpat qq env ds)) as

1893 arity = getPArity ty in

1895 arity = getPArity ty in

@@ -1972,28 +1974,31 @@ addImpl' inpat env infns imp_meths ist ptm

1972-- if in a pattern, and there are no arguments, and there's no possible

1974-- if in a pattern, and there are no arguments, and there's no possible

1973-- names with zero explicit arguments, don't add implicits.

1975-- names with zero explicit arguments, don't add implicits.

1974

1976

1977+aiFn :: Name -> Bool -- ^ Allow capitalization of pattern variables

1975−aiFn :: Name -> Bool -> Bool -> Bool

1978+ -> Bool -> Bool -> Bool

1976 -> [Name]

1979 -> [Name]

1977 -> IState -> FC

1980 -> IState -> FC

1978 -> Name -- ^ function being applied

1981 -> Name -- ^ function being applied

1979 -> FC -> [[T.Text]]

1982 -> FC -> [[T.Text]]

1980 -> [PArg] -- ^ initial arguments (if in a pattern)

1983 -> [PArg] -- ^ initial arguments (if in a pattern)

1981 -> Either Err PTerm

1984 -> Either Err PTerm

1982−aiFn topname inpat True qq imp_meths ist fc f ffc ds []

1985+aiFn topname allowcap inpat True qq imp_meths ist fc f ffc ds []

1983 | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f

1986 | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f

1984 | otherwise

1987 | otherwise

1985 = case lookupDef f (tt_ctxt ist) of

1988 = case lookupDef f (tt_ctxt ist) of

1989+ [] -> if allowcap

1990+ then Right $ PPatvar ffc f

1986− [] -> case f of

1991+ else case f of

1987− MN _ _ -> Right $ PPatvar ffc f

1992+ MN _ _ -> Right $ PPatvar ffc f

1988− UN xs | isDigit (T.head xs) -- for partial evaluation vars

1993+ UN xs | isDigit (T.head xs) -- for partial evaluation vars

1989− -> Right $ PPatvar ffc f

1994+ -> Right $ PPatvar ffc f

1990− _ -> Left $ Msg $ show f ++ " is not a valid name for a pattern variable"

1995+ _ -> Left $ Msg $ show f ++ " is not a valid name for a pattern variable"

1991 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in

1996 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in

1992 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $

1997 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $

1993 if (not (vname f) || tcname f

1998 if (not (vname f) || tcname f

1994 || any (conCaf (tt_ctxt ist)) ialts)

1999 || any (conCaf (tt_ctxt ist)) ialts)

1995-- any constructor alts || any allImp ialts))

2000-- any constructor alts || any allImp ialts))

1996− then aiFn topname inpat False qq imp_meths ist fc f ffc ds [] -- use it as a constructor

2001+ then aiFn topname allowcap inpat False qq imp_meths ist fc f ffc ds [] -- use it as a constructor

1997 else Right $ PPatvar ffc f

2002 else Right $ PPatvar ffc f

1998 where imp (PExp _ _ _ _) = False

2003 where imp (PExp _ _ _ _) = False

1999 imp _ = True

2004 imp _ = True

@@ -2008,9 +2013,9 @@ aiFn topname inpat True qq imp_meths ist fc f ffc ds []

2008 vname (UN n) = True -- non qualified

2013 vname (UN n) = True -- non qualified

2009 vname _ = False

2014 vname _ = False

2010

2015

2011−aiFn topname inpat expat qq imp_meths ist fc f ffc ds as

2016+aiFn topname allowcap inpat expat qq imp_meths ist fc f ffc ds as

2012 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as

2017 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as

2013−aiFn topname inpat expat qq imp_meths ist fc f ffc ds as

2018+aiFn topname allowcap inpat expat qq imp_meths ist fc f ffc ds as

2014 -- This is where namespaces get resolved by adding PAlternative

2019 -- This is where namespaces get resolved by adding PAlternative

2015 = do let ns = lookupCtxtName f (idris_implicits ist)

2020 = do let ns = lookupCtxtName f (idris_implicits ist)

2016 let nh = filter (\(n, _) -> notHidden n) ns

2021 let nh = filter (\(n, _) -> notHidden n) ns

src/Idris/CmdOptions.hs+1

@@ -223,6 +223,7 @@ parseFlags = many $

223 <|> flag' DumpHighlights (long "highlight" <> help "Emit source code highlighting")

224

225 <|> flag' NoOldTacticDeprecationWarnings (long "no-tactic-deprecation-warnings" <> help "Disable deprecation warnings for the old tactic sublanguage")

226+ <|> flag' AllowCapitalizedPatternVariables (long "allow-capitalized-pattern-variables" <> help "Allow pattern variables to be capitalized")

226

227

227 where

228 where

228 getExt :: String -> LanguageExt

229 getExt :: String -> LanguageExt

src/Idris/Options.hs+1

@@ -94,6 +94,7 @@ data Opt = Filename String

94 | DumpHighlights

95 | DesugarNats

96 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics

97+ | AllowCapitalizedPatternVariables -- ^ Allow pattern variables to be capitalized

97 deriving (Show, Eq, Generic)

98 deriving (Show, Eq, Generic)

100