47
'let' { TokKeyword KwLet $$ }
48
'in' { TokKeyword KwIn $$ }
49
'where' { TokKeyword KwWhere $$ }
50
'with' { TokKeyword KwWith $$ }
51
'postulate' { TokKeyword KwPostulate $$ }
52
'primitive' { TokKeyword KwPrimitive $$ }
53
'open' { TokKeyword KwOpen $$ }
54
'import' { TokKeyword KwImport $$ }
55
'using' { TokKeyword KwUsing $$ }
56
'hiding' { TokKeyword KwHiding $$ }
57
'renaming' { TokKeyword KwRenaming $$ }
58
'to' { TokKeyword KwTo $$ }
59
'public' { TokKeyword KwPublic $$ }
60
'module' { TokKeyword KwModule $$ }
61
'data' { TokKeyword KwData $$ }
62
'codata' { TokKeyword KwCoData $$ }
63
'record' { TokKeyword KwRecord $$ }
64
'field' { TokKeyword KwField $$ }
65
'infix' { TokKeyword KwInfix $$ }
66
'infixl' { TokKeyword KwInfixL $$ }
67
'infixr' { TokKeyword KwInfixR $$ }
68
'mutual' { TokKeyword KwMutual $$ }
69
'abstract' { TokKeyword KwAbstract $$ }
70
'private' { TokKeyword KwPrivate $$ }
71
'Prop' { TokKeyword KwProp $$ }
72
'Set' { TokKeyword KwSet $$ }
73
'forall' { TokKeyword KwForall $$ }
74
'OPTIONS' { TokKeyword KwOPTIONS $$ }
75
'BUILTIN' { TokKeyword KwBUILTIN $$ }
76
'IMPORT' { TokKeyword KwIMPORT $$ }
77
'COMPILED' { TokKeyword KwCOMPILED $$ }
51
'let' { TokKeyword KwLet $$ }
52
'in' { TokKeyword KwIn $$ }
53
'where' { TokKeyword KwWhere $$ }
54
'with' { TokKeyword KwWith $$ }
55
'rewrite' { TokKeyword KwRewrite $$ }
56
'postulate' { TokKeyword KwPostulate $$ }
57
'primitive' { TokKeyword KwPrimitive $$ }
58
'open' { TokKeyword KwOpen $$ }
59
'import' { TokKeyword KwImport $$ }
60
'using' { TokKeyword KwUsing $$ }
61
'hiding' { TokKeyword KwHiding $$ }
62
'renaming' { TokKeyword KwRenaming $$ }
63
'to' { TokKeyword KwTo $$ }
64
'public' { TokKeyword KwPublic $$ }
65
'module' { TokKeyword KwModule $$ }
66
'data' { TokKeyword KwData $$ }
67
'codata' { TokKeyword KwCoData $$ }
68
'record' { TokKeyword KwRecord $$ }
69
'constructor' { TokKeyword KwConstructor $$ }
70
'field' { TokKeyword KwField $$ }
71
'infix' { TokKeyword KwInfix $$ }
72
'infixl' { TokKeyword KwInfixL $$ }
73
'infixr' { TokKeyword KwInfixR $$ }
74
'mutual' { TokKeyword KwMutual $$ }
75
'abstract' { TokKeyword KwAbstract $$ }
76
'private' { TokKeyword KwPrivate $$ }
77
'Prop' { TokKeyword KwProp $$ }
78
'Set' { TokKeyword KwSet $$ }
79
'forall' { TokKeyword KwForall $$ }
80
'OPTIONS' { TokKeyword KwOPTIONS $$ }
81
'BUILTIN' { TokKeyword KwBUILTIN $$ }
82
'IMPORT' { TokKeyword KwIMPORT $$ }
83
'IMPOSSIBLE' { TokKeyword KwIMPOSSIBLE $$ }
84
'COMPILED' { TokKeyword KwCOMPILED $$ }
78
85
'COMPILED_DATA' { TokKeyword KwCOMPILED_DATA $$ }
79
86
'COMPILED_TYPE' { TokKeyword KwCOMPILED_TYPE $$ }
80
'LINE' { TokKeyword KwLINE $$ }
82
88
setN { TokSetN $$ }
270
277
Id : id {% mkName $1 }
279
-- Space separated list of one or more identifiers.
280
SpaceIds :: { [Name] }
282
: Id SpaceIds { $1 : $2 }
285
-- Space separated list of one or more identifiers, some of which may
286
-- be surrounded by braces.
287
HiddenIds :: { [(Hiding, Name)] }
289
: Id HiddenIds { (NotHidden, $1) : $2 }
290
| Id { [(NotHidden, $1)] }
291
| '{' SpaceIds '}' HiddenIds { map ((,) Hidden) $2 ++ $4 }
292
| '{' SpaceIds '}' { map ((,) Hidden) $2 }
272
294
-- Qualified operators are treated as identifiers, i.e. they have to be back
273
295
-- quoted to appear infix.
566
588
-- A left hand side of a function clause. We parse it as an expression, and
567
589
-- then check that it is a valid left hand side.
569
LHS : Expr1 WithExpressions {% exprToLHS $1 >>= \p -> return (p $2) }
570
| '...' WithPats WithExpressions { Ellipsis (fuseRange $1 $3) $2 $3 }
591
LHS : Expr1 RewriteEquations WithExpressions
592
{% exprToLHS $1 >>= \p -> return (p $2 $3) }
593
| '...' WithPats RewriteEquations WithExpressions
594
{ Ellipsis (fuseRange $1 $3) $2 $3 $4 }
572
596
WithPats :: { [Pattern] }
573
597
WithPats : {- empty -} { [] }
623
654
TypeSig :: { Declaration }
624
655
TypeSig : Id ':' Expr { TypeSig $1 $3 }
657
-- Type signatures of the form "n1 n2 n3 ... : Type", with at least
659
TypeSigs :: { [Declaration] }
660
TypeSigs : SpaceIds ':' Expr { map (flip TypeSig $3) $1 }
662
-- A variant of TypeSigs where any sub-sequence of names can be marked
663
-- as hidden using braces: {n1 n2} n3 n4 {n5} {n6} ... : Type.
664
HiddenTypeSigs :: { [(Hiding, Declaration)] }
665
HiddenTypeSigs : HiddenIds ':' Expr { map (id *** flip TypeSig $3) $1 }
627
667
-- Function declarations. The left hand side is parsed as an expression to allow
628
668
-- declarations like 'x::xs ++ ys = e', when '::' has higher precedence than '++'.
776
818
ImportPragma :: { Pragma }
778
: '{-#' 'IMPORT' PragmaStrings '#-}'
779
{ ImportPragma (fuseRange $1 $4) (unwords $3) }
782
LinePragma :: { Pragma }
784
: '{-#' 'LINE' string string '#-}' {% do
785
let r = fuseRange $1 $5
787
| head f == '"' && last f == '"' = return $ init (tail f)
788
| otherwise = parseErrorAt (iStart i) $ "Expected \"filename\", found " ++ f
790
| all isDigit l = return $ read l
791
| otherwise = parseErrorAt (iStart i) $ "Expected line number, found " ++ l
794
currentPos <- fmap parsePos get
797
, posPos = posPos currentPos
801
return $ LinePragma r line file
820
: '{-#' 'IMPORT' string '#-}'
822
if validHaskellModuleName s
823
then return $ ImportPragma (fuseRange $1 $4) s
824
else parseError $ "Malformed module name: " ++ s ++ "."
827
ImpossiblePragma :: { Pragma }
828
: '{-#' 'IMPOSSIBLE' '#-}' { ImpossiblePragma (fuseRange $1 $3) }
804
830
{--------------------------------------------------------------------------
805
831
Sequences of declarations
806
832
--------------------------------------------------------------------------}
834
-- Non-empty list of type signatures, with several identifiers allowed
835
-- for every signature.
808
836
TypeSignatures :: { [TypeSignature] }
810
838
: TeX vopen TypeSignatures1 TeX close { reverse $3 }
816
840
-- Inside the layout block.
817
841
TypeSignatures1 :: { [TypeSignature] }
819
: TypeSignatures1 semi TeX TypeSig { $4 : $1 }
820
| TeX TypeSig { [$2] }
843
: TypeSignatures1 semi TeX TypeSigs { reverse $4 ++ $1 }
844
| TeX TypeSigs { reverse $2 }
846
-- A variant of TypeSignatures which uses HiddenTypeSigs instead of
848
HiddenTypeSignatures :: { [(Hiding, TypeSignature)] }
850
: TeX vopen HiddenTypeSignatures1 TeX close { reverse $3 }
852
-- Inside the layout block.
853
HiddenTypeSignatures1 :: { [(Hiding, TypeSignature)] }
854
HiddenTypeSignatures1
855
: HiddenTypeSignatures1 semi TeX HiddenTypeSigs { reverse $4 ++ $1 }
856
| TeX HiddenTypeSigs { reverse $2 }
822
858
-- Constructors are type signatures. But constructor lists can be empty.
823
859
Constructors :: { [Constructor] }
825
: TypeSignatures { $1 }
826
| TeX vopen TeX close { [] }
861
: TeX vopen TeX close { [] }
862
| TypeSignatures { $1 }
864
-- Record declarations, including an optional record constructor name.
865
RecordDeclarations :: { (Maybe Name, [Declaration]) }
867
: TeX vopen TeX close { (Nothing, []) }
868
| TeX vopen TeX RecordConstructorName TeX close { (Just $4, []) }
869
| TeX vopen TeX RecordConstructorName semi Declarations1 TeX close { (Just $4, reverse $6) }
870
| TeX vopen Declarations1 TeX close { (Nothing, reverse $3) }
828
872
-- Arbitrary declarations
829
873
Declarations :: { [Declaration] }
939
983
names (Using xs) = xs
940
984
names (Hiding xs) = xs
986
-- | Breaks up a string into substrings. Returns every maximal
987
-- subsequence of zero or more characters distinct from @'.'@.
989
-- > splitOnDots "" == [""]
990
-- > splitOnDots "foo.bar" == ["foo", "bar"]
991
-- > splitOnDots ".foo.bar" == ["", "foo", "bar"]
992
-- > splitOnDots "foo.bar." == ["foo", "bar", ""]
993
-- > splitOnDots "foo..bar" == ["foo", "", "bar"]
994
splitOnDots :: String -> [String]
995
splitOnDots "" = [""]
996
splitOnDots ('.' : s) = [] : splitOnDots s
997
splitOnDots (c : s) = case splitOnDots s of
998
p : ps -> (c : p) : ps
1000
prop_splitOnDots = and
1001
[ splitOnDots "" == [""]
1002
, splitOnDots "foo.bar" == ["foo", "bar"]
1003
, splitOnDots ".foo.bar" == ["", "foo", "bar"]
1004
, splitOnDots "foo.bar." == ["foo", "bar", ""]
1005
, splitOnDots "foo..bar" == ["foo", "", "bar"]
1008
-- | Returns 'True' iff the name is a valid Haskell (hierarchical)
1010
validHaskellModuleName :: String -> Bool
1011
validHaskellModuleName = all ok . splitOnDots
1013
-- Checks if a dot-less module name is well-formed.
1014
ok :: String -> Bool
1018
all (\c -> isLower c || c == '_' ||
1020
generalCategory c == DecimalNumber ||
942
1024
{--------------------------------------------------------------------------
944
1026
--------------------------------------------------------------------------}
946
1028
-- | Turn an expression into a left hand side.
947
exprToLHS :: Expr -> Parser ([Expr] -> LHS)
1029
exprToLHS :: Expr -> Parser ([Expr] -> [Expr] -> LHS)
948
1030
exprToLHS e = case e of
949
1031
WithApp r e es -> LHS <$> exprToPattern e <*> mapM exprToPattern es
950
1032
_ -> LHS <$> exprToPattern e <*> return []
added
removed
src/full/Agda/Syntax/Parser/Parser.y
