summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Parser/Parser.y
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Parser/Parser.y')
-rw-r--r--src/full/Agda/Syntax/Parser/Parser.y121
1 files changed, 76 insertions, 45 deletions
diff --git a/src/full/Agda/Syntax/Parser/Parser.y b/src/full/Agda/Syntax/Parser/Parser.y
index 2146e22..78c3b1e 100644
--- a/src/full/Agda/Syntax/Parser/Parser.y
+++ b/src/full/Agda/Syntax/Parser/Parser.y
@@ -20,7 +20,7 @@ module Agda.Syntax.Parser.Parser (
, exprParser
, exprWhereParser
, tokensParser
- , tests
+ , splitOnDots -- only used by the internal test-suite
) where
import Control.Monad
@@ -45,14 +45,14 @@ import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Literal
+import Agda.TypeChecking.Positivity.Occurrence hiding (tests)
+
import Agda.Utils.Either hiding (tests)
import Agda.Utils.Hash
-import Agda.Utils.List (spanJust)
+import Agda.Utils.List ( spanJust, chopWhen )
import Agda.Utils.Monad
import Agda.Utils.Pretty
-import Agda.Utils.QuickCheck
import Agda.Utils.Singleton
-import Agda.Utils.TestHelpers
import Agda.Utils.Tuple
import Agda.Utils.Impossible
@@ -97,6 +97,7 @@ import Agda.Utils.Impossible
'infixl' { TokKeyword KwInfixL $$ }
'infixr' { TokKeyword KwInfixR $$ }
'instance' { TokKeyword KwInstance $$ }
+ 'overlap' { TokKeyword KwOverlap $$ }
'let' { TokKeyword KwLet $$ }
'macro' { TokKeyword KwMacro $$ }
'module' { TokKeyword KwModule $$ }
@@ -145,11 +146,11 @@ import Agda.Utils.Impossible
'IMPOSSIBLE' { TokKeyword KwIMPOSSIBLE $$ }
'INLINE' { TokKeyword KwINLINE $$ }
'MEASURE' { TokKeyword KwMEASURE $$ }
- 'NO_SMASHING' { TokKeyword KwNO_SMASHING $$ }
'NO_TERMINATION_CHECK' { TokKeyword KwNO_TERMINATION_CHECK $$ }
'NO_POSITIVITY_CHECK' { TokKeyword KwNO_POSITIVITY_CHECK $$ }
'NON_TERMINATING' { TokKeyword KwNON_TERMINATING $$ }
'OPTIONS' { TokKeyword KwOPTIONS $$ }
+ 'POLARITY' { TokKeyword KwPOLARITY $$ }
'REWRITE' { TokKeyword KwREWRITE $$ }
'STATIC' { TokKeyword KwSTATIC $$ }
'TERMINATING' { TokKeyword KwTERMINATING $$ }
@@ -172,6 +173,8 @@ import Agda.Utils.Impossible
'|' { TokSymbol SymBar $$ }
'(' { TokSymbol SymOpenParen $$ }
')' { TokSymbol SymCloseParen $$ }
+ '(|' { TokSymbol SymOpenIdiomBracket $$ }
+ '|)' { TokSymbol SymCloseIdiomBracket $$ }
'{{' { TokSymbol SymDoubleOpenBrace $$ }
'}}' { TokSymbol SymDoubleCloseBrace $$ }
'{' { TokSymbol SymOpenBrace $$ }
@@ -224,6 +227,7 @@ Token
| 'infixl' { TokKeyword KwInfixL $1 }
| 'infixr' { TokKeyword KwInfixR $1 }
| 'instance' { TokKeyword KwInstance $1 }
+ | 'overlap' { TokKeyword KwOverlap $1 }
| 'let' { TokKeyword KwLet $1 }
| 'macro' { TokKeyword KwMacro $1 }
| 'module' { TokKeyword KwModule $1 }
@@ -272,11 +276,11 @@ Token
| 'IMPOSSIBLE' { TokKeyword KwIMPOSSIBLE $1 }
| 'INLINE' { TokKeyword KwINLINE $1 }
| 'MEASURE' { TokKeyword KwMEASURE $1 }
- | 'NO_SMASHING' { TokKeyword KwNO_SMASHING $1 }
| 'NO_TERMINATION_CHECK' { TokKeyword KwNO_TERMINATION_CHECK $1 }
| 'NO_POSITIVITY_CHECK' { TokKeyword KwNO_POSITIVITY_CHECK $1 }
| 'NON_TERMINATING' { TokKeyword KwNON_TERMINATING $1 }
| 'OPTIONS' { TokKeyword KwOPTIONS $1 }
+ | 'POLARITY' { TokKeyword KwPOLARITY $1 }
| 'REWRITE' { TokKeyword KwREWRITE $1 }
| 'STATIC' { TokKeyword KwSTATIC $1 }
| 'TERMINATING' { TokKeyword KwTERMINATING $1 }
@@ -299,6 +303,8 @@ Token
| '|' { TokSymbol SymBar $1 }
| '(' { TokSymbol SymOpenParen $1 }
| ')' { TokSymbol SymCloseParen $1 }
+ | '(|' { TokSymbol SymOpenIdiomBracket $1 }
+ | '|)' { TokSymbol SymCloseIdiomBracket $1 }
| '{{' { TokSymbol SymDoubleOpenBrace $1 }
| '}}' { TokSymbol SymDoubleCloseBrace $1 }
| '{' { TokSymbol SymOpenBrace $1 }
@@ -405,8 +411,9 @@ DoubleCloseBrace
-- A possibly dotted identifier.
MaybeDottedId :: { Arg Name }
MaybeDottedId
- : '.' Id { setRelevance Irrelevant $ defaultArg $2 }
- | Id { defaultArg $1 }
+ : '..' Id { setRelevance NonStrict $ defaultArg $2 }
+ | '.' Id { setRelevance Irrelevant $ defaultArg $2 }
+ | Id { defaultArg $1 }
-- Space separated list of one or more possibly dotted identifiers.
MaybeDottedIds :: { [Arg Name] }
@@ -563,7 +570,10 @@ PragmaName :: { Name }
PragmaName : string {% mkName $1 }
PragmaQName :: { QName }
-PragmaQName : string {% fmap QName (mkName $1) }
+PragmaQName : string {% pragmaQName $1 } -- Issue 2125. WAS: string {% fmap QName (mkName $1) }
+
+PragmaQNames :: { [QName] }
+PragmaQNames : Strings {% mapM pragmaQName $1 }
{--------------------------------------------------------------------------
Expressions (terms and types)
@@ -628,6 +638,7 @@ Expr2
ExtendedOrAbsurdLam :: { Expr }
ExtendedOrAbsurdLam
: '\\' '{' LamClauses '}' { ExtendedLam (getRange ($1,$2,$3,$4)) (reverse $3) }
+ | '\\' 'where' vopen LamClauses close { ExtendedLam (getRange ($1, $2, $4)) (reverse $4) }
| '\\' AbsurdLamBindings {% case $2 of
Left (bs, h) -> if null bs then return $ AbsurdLam r h else
return $ Lam r bs (AbsurdLam r h)
@@ -663,6 +674,7 @@ Expr3NoCurly
| '{{' Expr DoubleCloseBrace { InstanceArg (getRange ($1,$2,$3))
(maybeNamed $2) }
| '(' Expr ')' { Paren (getRange ($1,$2,$3)) $2 }
+ | '(|' Expr '|)' { IdiomBrackets (getRange ($1,$2,$3)) $2 }
| '(' ')' { Absurd (fuseRange $1 $2) }
| '{{' DoubleCloseBrace { let r = fuseRange $1 $2 in InstanceArg r $ unnamed $ Absurd r }
| Id '@' Expr3 { As (getRange ($1,$2,$3)) $1 $3 }
@@ -1018,8 +1030,8 @@ WhereClause :: { WhereClause }
WhereClause
: {- empty -} { NoWhere }
| 'where' Declarations0 { AnyWhere $2 }
- | 'module' Id 'where' Declarations0 { SomeWhere $2 $4 }
- | 'module' Underscore 'where' Declarations0 { SomeWhere $2 $4 }
+ | 'module' Id 'where' Declarations0 { SomeWhere $2 PublicAccess $4 }
+ | 'module' Underscore 'where' Declarations0 { SomeWhere $2 PublicAccess $4 }
ExprWhere :: { ExprWhere }
ExprWhere : Expr WhereClause { ExprWhere $1 $2 }
@@ -1070,6 +1082,9 @@ TypeSigs : SpaceIds ':' Expr { map (\ x -> TypeSig defaultArgInfo x $3) $1 }
ArgTypeSigs :: { [Arg Declaration] }
ArgTypeSigs
: ArgIds ':' Expr { map (fmap (\ x -> TypeSig defaultArgInfo x $3)) $1 }
+ | 'overlap' ArgIds ':' Expr {
+ let setOverlap (Arg i x) = Arg i{ argInfoOverlappable = True } x in
+ map (setOverlap . fmap (\ x -> TypeSig defaultArgInfo x $4)) $2 }
| 'instance' ArgTypeSignatures {
let
setInstance (TypeSig info x t) = TypeSig (setHiding Instance info) x t
@@ -1155,7 +1170,7 @@ Abstract : 'abstract' Declarations { Abstract (fuseRange $1 $2) $2 }
-- Private can only appear on the top-level (or rather the module level).
Private :: { Declaration }
-Private : 'private' Declarations { Private (fuseRange $1 $2) $2 }
+Private : 'private' Declarations { Private (fuseRange $1 $2) UserWritten $2 }
-- Instance declarations.
@@ -1261,7 +1276,7 @@ Open : MaybeOpen 'import' ModuleName OpenArgs ImportDirective {%
; impStm asR = Import mr m (Just (AsName fresh asR)) DontOpen defaultImportDir
; appStm m' es =
let r = getRange (m, es) in
- Private r
+ Private r Inserted
[ ModuleMacro r m'
(SectionApp (getRange es) []
(RawApp (getRange es) (Ident (QName fresh) : es)))
@@ -1299,18 +1314,19 @@ Open : MaybeOpen 'import' ModuleName OpenArgs ImportDirective {%
} in
[ case es of
{ [] -> Open r m dir
- ; _ -> Private r [ ModuleMacro r (noName $ beginningOf $ getRange m)
+ ; _ -> Private r Inserted
+ [ ModuleMacro r (noName $ beginningOf $ getRange m)
(SectionApp (getRange (m , es)) [] (RawApp (fuseRange m es) (Ident m : es)))
DoOpen dir
- ]
+ ]
}
]
}
| 'open' ModuleName '{{' '...' DoubleCloseBrace ImportDirective {
let r = getRange $2 in
- [ Private r [ ModuleMacro r (noName $ beginningOf $ getRange $2)
- (RecordModuleIFS r $2) DoOpen $6
- ]
+ [ Private r Inserted
+ [ ModuleMacro r (noName $ beginningOf $ getRange $2) (RecordModuleIFS r $2) DoOpen $6
+ ]
]
}
@@ -1366,7 +1382,6 @@ DeclarationPragma
| CompiledUHCPragma { $1 }
| CompiledDataUHCPragma { $1 }
| HaskellPragma { $1 }
- | NoSmashingPragma { $1 }
| StaticPragma { $1 }
| InlinePragma { $1 }
| ImportPragma { $1 }
@@ -1379,6 +1394,7 @@ DeclarationPragma
| CatchallPragma { $1 }
| DisplayPragma { $1 }
| NoPositivityCheckPragma { $1 }
+ | PolarityPragma { $1 }
| OptionsPragma { $1 }
-- Andreas, 2014-03-06
-- OPTIONS pragma not allowed everywhere, but don't give parse error.
@@ -1397,7 +1413,7 @@ BuiltinPragma
RewritePragma :: { Pragma }
RewritePragma
- : '{-#' 'REWRITE' PragmaQName '#-}'
+ : '{-#' 'REWRITE' PragmaQNames '#-}'
{ RewritePragma (getRange ($1,$2,$3,$4)) $3 }
CompiledPragma :: { Pragma }
@@ -1449,11 +1465,6 @@ HaskellPragma :: { Pragma }
HaskellPragma
: '{-#' 'HASKELL' Strings '#-}' { HaskellCodePragma (getRange ($1, $2, $4)) (recoverLayout $3) }
-NoSmashingPragma :: { Pragma }
-NoSmashingPragma
- : '{-#' 'NO_SMASHING' PragmaQName '#-}'
- { NoSmashingPragma (getRange ($1,$2,$3,$4)) $3 }
-
StaticPragma :: { Pragma }
StaticPragma
: '{-#' 'STATIC' PragmaQName '#-}'
@@ -1524,6 +1535,20 @@ NoPositivityCheckPragma
: '{-#' 'NO_POSITIVITY_CHECK' '#-}'
{ NoPositivityCheckPragma (getRange ($1,$2,$3)) }
+PolarityPragma :: { Pragma }
+PolarityPragma
+ : '{-#' 'POLARITY' PragmaName Polarities '#-}'
+ { let (rs, occs) = unzip (reverse $4) in
+ PolarityPragma (getRange ($1,$2,$3,rs,$5)) $3 occs }
+
+-- Possibly empty list of polarities. Reversed.
+Polarities :: { [(Range, Occurrence)] }
+Polarities : {- empty -} { [] }
+ | Polarities Polarity { $2 : $1 }
+
+Polarity :: { (Range, Occurrence) }
+Polarity : string {% polarity $1 }
+
{--------------------------------------------------------------------------
Sequences of declarations
--------------------------------------------------------------------------}
@@ -1692,6 +1717,29 @@ mkQName ss = do
xs <- mapM mkName ss
return $ foldr Qual (QName $ last xs) (init xs)
+-- | Create a qualified name from a string (used in pragmas).
+-- Range of each name component is range of whole string.
+-- TODO: precise ranges!
+
+pragmaQName :: (Interval, String) -> Parser QName
+pragmaQName (r, s) = do
+ let ss = chopWhen (== '.') s
+ mkQName $ map (r,) ss
+
+-- | Polarity parser.
+
+polarity :: (Interval, String) -> Parser (Range, Occurrence)
+polarity (i, s) =
+ case s of
+ "_" -> ret Unused
+ "++" -> ret StrictPos
+ "+" -> ret JustPos
+ "-" -> ret JustNeg
+ "*" -> ret Mixed
+ _ -> fail $ "Not a valid polarity: " ++ s
+ where
+ ret x = return (getRange i, x)
+
recoverLayout :: [(Interval, String)] -> String
recoverLayout [] = ""
recoverLayout xs@((i, _) : _) = go (iStart i) xs
@@ -1804,13 +1852,6 @@ splitOnDots ('.' : s) = [] : splitOnDots s
splitOnDots (c : s) = case splitOnDots s of
p : ps -> (c : p) : ps
-prop_splitOnDots = and
- [ splitOnDots "" == [""]
- , splitOnDots "foo.bar" == ["foo", "bar"]
- , splitOnDots ".foo.bar" == ["", "foo", "bar"]
- , splitOnDots "foo.bar." == ["foo", "bar", ""]
- , splitOnDots "foo..bar" == ["foo", "", "bar"]
- ]
-- | Returns 'True' iff the name is a valid Haskell (hierarchical)
-- module name.
@@ -1853,8 +1894,8 @@ exprToPattern e = do
Underscore r _ -> return $ WildP r
Absurd r -> return $ AbsurdP r
As r x e -> AsP r x <$> exprToPattern e
- Dot r (HiddenArg _ e) -> return $ HiddenP r $ fmap (DotP r) e
- Dot r e -> return $ DotP r e
+ Dot r (HiddenArg _ e) -> return $ HiddenP r $ fmap (DotP r UserWritten) e
+ Dot r e -> return $ DotP r UserWritten e
Lit l -> return $ LitP l
HiddenArg r e -> HiddenP r <$> T.mapM exprToPattern e
InstanceArg r e -> InstanceP r <$> T.mapM exprToPattern e
@@ -1916,7 +1957,7 @@ patternToNames p =
case p of
IdentP (QName i) -> return [(defaultArgInfo, i)]
WildP r -> return [(defaultArgInfo, C.noName r)]
- DotP _ (Ident (QName i)) -> return [(setRelevance Irrelevant defaultArgInfo, i)]
+ DotP _ _ (Ident (QName i)) -> return [(setRelevance Irrelevant defaultArgInfo, i)]
RawAppP _ ps -> concat <$> mapM patternToNames ps
_ -> parseError $
"Illegal name in type signature: " ++ prettyShow p
@@ -1942,14 +1983,4 @@ parseDisplayPragma r pos s =
return $ DisplayPragma r lhs rhs
_ -> parseError "Invalid DISPLAY pragma. Should have form {-# DISPLAY LHS = RHS #-}."
-{--------------------------------------------------------------------------
- Tests
- --------------------------------------------------------------------------}
-
--- | Test suite.
-tests :: IO Bool
-tests = runTests "Agda.Syntax.Parser.Parser"
- [ quickCheck' prop_splitOnDots
- ]
-
}