Skip to content

Commit

Permalink
[ issue 953 ] the parser now inserts module _ where if no top-level m…
Browse files Browse the repository at this point in the history 
…odule is defined

  - todo: handle that when checking module name
  • Loading branch information
@UlfNorell
UlfNorell committed Nov 13, 2013
1 parent bf5c94b commit f304322
Show file tree
Hide file tree
Showing 8 changed files with 61 additions and 39 deletions.
6 changes: 3 additions & 3 deletions src/full/Agda/Syntax/Parser.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,15 +56,15 @@ parse :: Parser a -> String -> IO a
parse p = wrapM . return . M.parse (parseFlags p) [normal] (parser p)

parseFile :: Parser a -> AbsolutePath -> IO a
parseFile p = wrapM . M.parseFile (parseFlags p) [normal] (parser p)
parseFile p = wrapM . M.parseFile (parseFlags p) [layout, normal] (parser p)

parseLiterate :: Parser a -> String -> IO a
parseLiterate p =
wrapM . return . M.parse (parseFlags p) [literate, code] (parser p)
wrapM . return . M.parse (parseFlags p) [literate, layout, code] (parser p)

parseLiterateFile :: Parser a -> AbsolutePath -> IO a
parseLiterateFile p =
wrapM . M.parseFile (parseFlags p) [literate, code] (parser p)
wrapM . M.parseFile (parseFlags p) [literate, layout, code] (parser p)

parsePosString :: Parser a -> Position -> String -> IO a
parsePosString p pos =
Expand Down
6 changes: 5 additions & 1 deletion src/full/Agda/Syntax/Parser/Monad.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ module Agda.Syntax.Parser.Monad
, topContext, popContext, pushContext
, pushCurrentContext
-- ** Errors
, parseError, parseErrorAt
, parseError, parseErrorAt, parseError'
, lexError
)
where
Expand Down Expand Up @@ -262,6 +262,10 @@ parseErrorAt p msg =
do setLastPos p
parseError msg

-- | Use 'parseErrorAt' or 'parseError' as appropriate.
parseError' :: Maybe Position -> String -> Parser a
parseError' = maybe parseError parseErrorAt


-- | For lexical errors we want to report the current position as the site of
-- the error, whereas for parse errors the previous position is the one
Expand Down
68 changes: 42 additions & 26 deletions src/full/Agda/Syntax/Parser/Parser.y
View file
Original file line number Diff line number Diff line change
Expand Up @@ -254,10 +254,13 @@ Token
--------------------------------------------------------------------------}
File :: { ([Pragma], [Declaration]) }
File : File1 { $1 }
File : vopen File1 maybe_vclose { $2 }
File1 : TopLevel { ([], $1) }
| TopLevelPragma File1 { let (ps,m) = $2 in ($1 : ps, m) }
maybe_vclose : {- empty -} { () }
| vclose { () }
File1 : TopLevel { ([], $1) }
| TopLevelPragma semi File1 { let (ps,m) = $3 in ($1 : ps, m) }
{--------------------------------------------------------------------------
Expand Down Expand Up @@ -1135,31 +1138,25 @@ ModuleApplication : ModuleName '{{' '...' DoubleCloseBrace { (\ts ->

-- Module instantiation
ModuleMacro :: { Declaration }
ModuleMacro : 'module' Id TypedUntypedBindings '=' ModuleApplication ImportDirective
{% do {ma <- $5 (map addType $3); return $ ModuleMacro (getRange ($1, $2, ma, $6)) $2 ma DontOpen $6 } }
ModuleMacro : 'module' ModuleName TypedUntypedBindings '=' ModuleApplication ImportDirective
{% do { ma <- $5 (map addType $3)
; name <- ensureUnqual $2
; return $ ModuleMacro (getRange ($1, $2, ma, $6)) name ma DontOpen $6 } }
| 'open' 'module' Id TypedUntypedBindings '=' ModuleApplication ImportDirective
{% do {ma <- $6 (map addType $4); return $ ModuleMacro (getRange ($1, $2, $3, ma, $7)) $3 ma DoOpen $7 } }

-- Module
Module :: { Declaration }
Module : 'module' Id TypedUntypedBindings 'where' Declarations0
{ Module (getRange ($1,$2,$3,$4,$5)) (QName $2) (map addType $3) $5 }
Module : 'module' ModuleName TypedUntypedBindings 'where' Declarations0
{ Module (getRange ($1,$2,$3,$4,$5)) $2 (map addType $3) $5 }
| 'module' Underscore TypedUntypedBindings 'where' Declarations0
{ Module (getRange ($1,$2,$3,$4,$5)) (QName $2) (map addType $3) $5 }

Underscore :: { Name }
Underscore : '_' { noName (getRange $1) }

-- The top-level consist of a bunch of import and open followed by a top-level module.
TopLevel :: { [Declaration] }
TopLevel : TopModule { [$1] }
-- | Import TopLevel { $1 : $2 }
| Open TopLevel { $1 ++ $2 }

-- The top-level module can have a qualified name.
TopModule :: { Declaration }
TopModule : 'module' ModuleName TypedUntypedBindings 'where' Declarations0
{ Module (getRange ($1,$2,$3,$4,$5)) $2 (map addType $3) $5 }
TopLevel : TopDeclarations { figureOutTopLevelModule $1 }

Pragma :: { Declaration }
Pragma : DeclarationPragma { Pragma $1 }
Expand Down Expand Up @@ -1292,12 +1289,12 @@ RecordDeclarations :: { (Maybe Induction, Maybe Name, [Declaration]) }
RecordDeclarations
: vopen close { (Nothing, Nothing, []) }
| vopen RecordConstructorName close { (Nothing, Just $2, []) }
| vopen RecordConstructorName semi Declarations1 close { (Nothing, Just $2, reverse $4) }
| vopen Declarations1 close { (Nothing, Nothing, reverse $2) }
| vopen RecordConstructorName semi Declarations1 close { (Nothing, Just $2, $4) }
| vopen Declarations1 close { (Nothing, Nothing, $2) }
| vopen RecordInduction close { (Just $2, Nothing, []) }
| vopen RecordInduction semi RecordConstructorName close { (Just $2, Just $4, []) }
| vopen RecordInduction semi RecordConstructorName semi Declarations1 close { (Just $2, Just $4, reverse $6) }
| vopen RecordInduction semi Declarations1 close { (Just $2, Nothing, reverse $4) }
| vopen RecordInduction semi RecordConstructorName semi Declarations1 close { (Just $2, Just $4, $6) }
| vopen RecordInduction semi Declarations1 close { (Just $2, Nothing, $4) }

-- Declaration of record as 'inductive' or 'coinductive'.
RecordInduction :: { Induction }
Expand All @@ -1308,7 +1305,7 @@ RecordInduction
-- Arbitrary declarations
Declarations :: { [Declaration] }
Declarations
: vopen Declarations1 close { reverse $2 }
: vopen Declarations1 close { $2 }

-- Arbitrary declarations
Declarations0 :: { [Declaration] }
Expand All @@ -1318,9 +1315,13 @@ Declarations0

Declarations1 :: { [Declaration] }
Declarations1
: Declarations1 semi Declaration { reverse $3 ++ $1 }
| Declaration { reverse $1 }
: Declaration semi Declarations1 { $1 ++ $3 }
| Declaration { $1 }

TopDeclarations :: { [Declaration] }
TopDeclarations
: {- empty -} { [] }
| Declarations1 { $1 }

{

Expand Down Expand Up @@ -1351,6 +1352,19 @@ happyError = parseError "Parse error"
Utility functions
--------------------------------------------------------------------------}

-- | Insert a top-level module if there is none.
figureOutTopLevelModule :: [Declaration] -> [Declaration]
figureOutTopLevelModule ds =
case span isAllowedBeforeModule ds of
(ds0, Module r m tel ds1 : ds2) -> ds0 ++ [Module r m tel $ ds1 ++ ds2]
(ds0, ds1) -> ds0 ++ [Module noRange (QName noName_) [] ds1]
where
isAllowedBeforeModule (Private _ ds) = all isAllowedBeforeModule ds
isAllowedBeforeModule Import{} = True
isAllowedBeforeModule ModuleMacro{} = True
isAllowedBeforeModule Open{} = True
isAllowedBeforeModule _ = False

-- | Create a name from a string.

mkName :: (Interval, String) -> Parser Name
Expand Down Expand Up @@ -1382,6 +1396,10 @@ mkQName ss = do
xs <- mapM mkName ss
return $ foldr Qual (QName $ last xs) (init xs)

ensureUnqual :: QName -> Parser Name
ensureUnqual (QName x) = return x
ensureUnqual q@Qual{} = parseError' (rStart $ getRange q) "Qualified name not allowed here"
-- | Match a particular name.
isName :: String -> (Interval, String) -> Parser ()
isName s (_,s')
Expand All @@ -1405,9 +1423,7 @@ mergeImportDirectives is = do
where
merge mi i2 = do
i1 <- mi
let err = case rStart $ getRange i2 of
Nothing -> parseError "Cannot mix using and hiding module directives"
Just p -> parseErrorAt p "Cannot mix using and hiding module directives"
let err = parseError' (rStart $ getRange i2) "Cannot mix using and hiding module directives"
uh <- case (usingOrHiding i1, usingOrHiding i2) of
(Hiding [], u) -> return u
(u, Hiding []) -> return u
Expand Down
6 changes: 3 additions & 3 deletions test/interaction/HighlightCopattern.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,14 +3,14 @@ Agda2> (agda2-status-action "")
(agda2-highlight-clear)
(agda2-info-action "*Type-checking*" "Checking HighlightCopattern (HighlightCopattern.agda).\n" t)
(agda2-highlight-add-annotations '(1 4 (symbol) nil) '(5 12 (keyword) nil) '(26 29 (symbol) nil) '(31 37 (keyword) nil) '(57 62 (keyword) nil) '(64 70 (keyword) nil) '(79 80 (symbol) nil) '(81 85 (primitivetype) nil) '(86 91 (keyword) nil) '(94 99 (keyword) nil) '(112 113 (symbol) nil) '(114 118 (primitivetype) nil) '(119 123 (keyword) nil) '(136 137 (symbol) nil) '(157 158 (symbol) nil) '(159 162 (primitivetype) nil) '(166 220 (comment) nil) '(227 228 (symbol) nil) '(237 238 (symbol) nil) '(239 243 (primitivetype) nil) '(251 252 (symbol) nil) '(264 318 (comment) nil))
(agda2-highlight-add-annotations '(31 37 (keyword) nil) '(38 56 (module) nil ("HighlightCopattern.agda" . 1)) '(57 62 (keyword) nil) '(64 70 (keyword) nil) '(71 78 (record) nil ("HighlightCopattern.agda" . 71)) '(79 80 (symbol) nil) '(81 85 (primitivetype) nil) '(86 91 (keyword) nil) '(94 99 (keyword) nil) '(104 111 (field) nil ("HighlightCopattern.agda" . 104)) '(112 113 (symbol) nil) '(114 118 (primitivetype) nil) '(119 123 (keyword) nil) '(124 131 (module) nil ("HighlightCopattern.agda" . 71)) '(133 135 (function) nil ("HighlightCopattern.agda" . 133)) '(136 137 (symbol) nil) '(138 145 (record) nil ("HighlightCopattern.agda" . 71)) '(146 153 (field) nil ("HighlightCopattern.agda" . 104)) '(154 156 (function) nil ("HighlightCopattern.agda" . 133)) '(157 158 (symbol) nil) '(159 162 (primitivetype) nil) '(166 220 (comment) nil) '(222 226 (function) nil ("HighlightCopattern.agda" . 222)) '(227 228 (symbol) nil) '(229 236 (record) nil ("HighlightCopattern.agda" . 71)) '(237 238 (symbol) nil) '(239 243 (primitivetype) nil) '(244 248 (function) nil ("HighlightCopattern.agda" . 222)) '(249 250 (bound) nil ("HighlightCopattern.agda" . 249)) '(251 252 (symbol) nil) '(253 260 (field) nil ("HighlightCopattern.agda" . 104)) '(261 262 (bound) nil ("HighlightCopattern.agda" . 249)))
(agda2-highlight-add-annotations '(31 37 (keyword) nil) '(38 56 (module) nil ("HighlightCopattern.agda" . 1)) '(57 62 (keyword) nil) '(71 78 (record) nil ("HighlightCopattern.agda" . 71)) '(104 111 (field) nil ("HighlightCopattern.agda" . 104)) '(124 131 (module) nil ("HighlightCopattern.agda" . 71)) '(133 135 (function) nil ("HighlightCopattern.agda" . 133)) '(138 145 (record) nil ("HighlightCopattern.agda" . 71)) '(146 153 (field) nil ("HighlightCopattern.agda" . 104)) '(154 156 (function) nil ("HighlightCopattern.agda" . 133)) '(222 226 (function) nil ("HighlightCopattern.agda" . 222)) '(229 236 (record) nil ("HighlightCopattern.agda" . 71)) '(244 248 (function) nil ("HighlightCopattern.agda" . 222)) '(249 250 (bound) nil ("HighlightCopattern.agda" . 249)) '(253 260 (field) nil ("HighlightCopattern.agda" . 104)) '(261 262 (bound) nil ("HighlightCopattern.agda" . 249)))
(agda2-highlight-add-annotations '(71 78 (postulate) nil ("HighlightCopattern.agda" . 71)) '(79 80 (symbol) nil) '(81 85 (primitivetype) nil))
(agda2-highlight-add-annotations '(71 78 (record) nil ("HighlightCopattern.agda" . 71)) '(104 111 (field) nil ("HighlightCopattern.agda" . 104)))
(agda2-highlight-add-annotations '(124 131 (module) nil ("HighlightCopattern.agda" . 71)))
(agda2-highlight-add-annotations '(133 135 (function) nil ("HighlightCopattern.agda" . 133)) '(136 137 (symbol) nil) '(138 145 (record) nil ("HighlightCopattern.agda" . 71)) '(146 153 (field) nil ("HighlightCopattern.agda" . 104)) '(154 156 (function) nil ("HighlightCopattern.agda" . 133)) '(157 158 (symbol) nil) '(159 162 (primitivetype) nil))
(agda2-highlight-add-annotations '(222 226 (function) nil ("HighlightCopattern.agda" . 222)) '(227 228 (symbol) nil) '(229 236 (record) nil ("HighlightCopattern.agda" . 71)) '(237 238 (symbol) nil) '(239 243 (primitivetype) nil) '(244 248 (function) nil ("HighlightCopattern.agda" . 222)) '(249 250 (bound) nil ("HighlightCopattern.agda" . 249)) '(251 252 (symbol) nil) '(253 260 (field) nil ("HighlightCopattern.agda" . 104)) '(261 262 (bound) nil ("HighlightCopattern.agda" . 249)))
(agda2-highlight-add-annotations '(31 37 (keyword) nil) '(38 56 (module) nil ("HighlightCopattern.agda" . 1)) '(57 62 (keyword) nil) '(64 70 (keyword) nil) '(86 91 (keyword) nil) '(94 99 (keyword) nil) '(112 113 (symbol) nil) '(114 118 (primitivetype) nil) '(119 123 (keyword) nil) '(166 220 (comment) nil))
(agda2-highlight-add-annotations '(1 4 (symbol) nil) '(5 12 (keyword) nil) '(26 29 (symbol) nil) '(264 318 (comment) nil))
(agda2-highlight-add-annotations '(31 37 (keyword) nil) '(38 56 (module) nil ("HighlightCopattern.agda" . 1)) '(57 62 (keyword) nil))
(agda2-highlight-add-annotations '(1 4 (symbol) nil) '(5 12 (keyword) nil) '(26 29 (symbol) nil) '(64 70 (keyword) nil) '(86 91 (keyword) nil) '(94 99 (keyword) nil) '(112 113 (symbol) nil) '(114 118 (primitivetype) nil) '(119 123 (keyword) nil) '(166 220 (comment) nil) '(264 318 (comment) nil))
(agda2-info-action "*Type-checking*" "Finished HighlightCopattern.\n" t)
(agda2-status-action "Checked")
(agda2-info-action "*All Goals*" "" nil)
Expand Down

0 comments on commit f304322

Please sign in to comment.