Skip to content

Commit

Permalink
Improve error messages for unclosed #section and extra #end
Browse files Browse the repository at this point in the history
  • Loading branch information
@fizruk
fizruk committed Sep 22, 2023
1 parent 67f7d5a commit 9c5e5b2
Show file tree
Hide file tree
Showing 10 changed files with 3,466 additions and 3,458 deletions.
3 changes: 2 additions & 1 deletion rzk/src/Language/Rzk/Syntax.cf
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,8 @@ define commandVariable name term = CommandAssume [name] term ;
commandVariables. Command ::= "#variables" [VarIdent] ":" Term ;
define commandVariables names term = CommandAssume names term ;

CommandSection. Command ::= "#section" SectionName ";" [Command] "#end" SectionName ;
CommandSection. Command ::= "#section" SectionName ;
CommandSectionEnd. Command ::= "#end" SectionName ;

CommandDefine. Command ::= "#define" VarIdent DeclUsedVars [Param] ":" Term ":=" Term ;
commandDefineNoParams. Command ::= "#define" VarIdent DeclUsedVars ":" Term ":=" Term ;
Expand Down
6 changes: 4 additions & 2 deletions rzk/src/Language/Rzk/Syntax/Abs.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,8 @@ data Command' a
| CommandComputeNF a (Term' a)
| CommandPostulate a (VarIdent' a) (DeclUsedVars' a) [Param' a] (Term' a)
| CommandAssume a [VarIdent' a] (Term' a)
| CommandSection a (SectionName' a) [Command' a] (SectionName' a)
| CommandSection a (SectionName' a)
| CommandSectionEnd a (SectionName' a)
| CommandDefine a (VarIdent' a) (DeclUsedVars' a) [Param' a] (Term' a) (Term' a)
deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)

Expand Down Expand Up @@ -234,7 +235,8 @@ instance HasPosition Command where
CommandComputeNF p _ -> p
CommandPostulate p _ _ _ _ -> p
CommandAssume p _ _ -> p
CommandSection p _ _ _ -> p
CommandSection p _ -> p
CommandSectionEnd p _ -> p
CommandDefine p _ _ _ _ _ -> p

instance HasPosition DeclUsedVars where
Expand Down
3 changes: 2 additions & 1 deletion rzk/src/Language/Rzk/Syntax/Doc.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,8 @@ All other symbols are terminals.
| | **|** | ``#assume`` //[VarIdent]// ``:`` //Term//
| | **|** | ``#variable`` //VarIdent// ``:`` //Term//
| | **|** | ``#variables`` //[VarIdent]// ``:`` //Term//
| | **|** | ``#section`` //SectionName// ``;`` //[Command]// ``#end`` //SectionName//
| | **|** | ``#section`` //SectionName//
| | **|** | ``#end`` //SectionName//
| | **|** | ``#define`` //VarIdent// //DeclUsedVars// //[Param]// ``:`` //Term// ``:=`` //Term//
| | **|** | ``#define`` //VarIdent// //DeclUsedVars// ``:`` //Term// ``:=`` //Term//
| | **|** | ``#def`` //VarIdent// //DeclUsedVars// //[Param]// ``:`` //Term// ``:=`` //Term//
Expand Down
417 changes: 210 additions & 207 deletions rzk/src/Language/Rzk/Syntax/Par.hs
View file

Large diffs are not rendered by default.

6,387 changes: 3,182 additions & 3,205 deletions rzk/src/Language/Rzk/Syntax/Par.info
View file

Large diffs are not rendered by default.

3 changes: 2 additions & 1 deletion rzk/src/Language/Rzk/Syntax/Par.y
View file
Original file line number Diff line number Diff line change
Expand Up @@ -203,7 +203,8 @@ Command
| '#assume' ListVarIdent ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandAssume (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
| '#variable' VarIdent ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandVariable (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
| '#variables' ListVarIdent ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandVariables (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
| '#section' SectionName ';' ListCommand '#end' SectionName { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandSection (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }
| '#section' SectionName { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandSection (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
| '#end' SectionName { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandSectionEnd (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
| '#define' VarIdent DeclUsedVars ListParam ':' Term ':=' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandDefine (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $4) (snd $6) (snd $8)) }
| '#define' VarIdent DeclUsedVars ':' Term ':=' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandDefineNoParams (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $5) (snd $7)) }
| '#def' VarIdent DeclUsedVars ListParam ':' Term ':=' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandDef (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $4) (snd $6) (snd $8)) }
Expand Down
60 changes: 32 additions & 28 deletions rzk/src/Language/Rzk/Syntax/Print.hs
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
-- File generated by the BNF Converter (bnfc 2.9.4.1).

{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
#if __GLASGOW_HASKELL__ <= 708
{-# LANGUAGE OverlappingInstances #-}
#endif
Expand All @@ -11,13 +11,16 @@

module Language.Rzk.Syntax.Print where

import Data.Char (Char, isSpace)
import Prelude
( ($), (.)
, Bool(..), (==), (<)
, Int, Integer, Double, (+), (-), (*)
, String, (++)
, ShowS, showChar, showString
, all, elem, foldr, id, map, null, replicate, shows, span
)
import Data.Char ( Char, isSpace )
import qualified Language.Rzk.Syntax.Abs
import Prelude (Bool (..), Double, Int, Integer,
ShowS, String, all, elem, foldr, id,
map, null, replicate, showChar,
showString, shows, span, ($), (*),
(+), (++), (-), (.), (<), (==))

-- | The top-level printing method.

Expand All @@ -40,9 +43,9 @@ render d = rend 0 False (map ($ "") $ d []) ""
rend i p = \case
"[" :ts -> char '[' . rend i False ts
"(" :ts -> char '(' . rend i False ts
-- "{" :ts -> onNewLine i p . showChar '{' . new (i+1) ts
-- "}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts
-- "}" :ts -> onNewLine (i-1) p . showChar '}' . new (i-1) ts
"{" :ts -> onNewLine i p . showChar '{' . new (i+1) ts
"}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts
"}" :ts -> onNewLine (i-1) p . showChar '}' . new (i-1) ts
[";"] -> char ';'
";" :ts -> char ';' . new i ts
t : ts@(s:_) | closingOrPunctuation s
Expand Down Expand Up @@ -121,10 +124,10 @@ printString s = doc (showChar '"' . concatS (map (mkEsc '"') s) . showChar '"')
mkEsc :: Char -> Char -> ShowS
mkEsc q = \case
s | s == q -> showChar '\\' . showChar s
'\\' -> showString "\\\\"
'\n' -> showString "\\n"
'\t' -> showString "\\t"
s -> showChar s
'\\' -> showString "\\\\"
'\n' -> showString "\\n"
'\t' -> showString "\\t"
s -> showChar s

prPrec :: Int -> Int -> Doc -> Doc
prPrec i j = if j < i then parenth else id
Expand Down Expand Up @@ -152,8 +155,8 @@ instance Print (Language.Rzk.Syntax.Abs.VarIdent' a) where
Language.Rzk.Syntax.Abs.VarIdent _ varidenttoken -> prPrec i 0 (concatD [prt 0 varidenttoken])

instance Print [Language.Rzk.Syntax.Abs.VarIdent' a] where
prt _ [] = concatD []
prt _ [x] = concatD [prt 0 x]
prt _ [] = concatD []
prt _ [x] = concatD [prt 0 x]
prt _ (x:xs) = concatD [prt 0 x, prt 0 xs]

instance Print (Language.Rzk.Syntax.Abs.LanguageDecl' a) where
Expand All @@ -174,11 +177,12 @@ instance Print (Language.Rzk.Syntax.Abs.Command' a) where
Language.Rzk.Syntax.Abs.CommandComputeNF _ term -> prPrec i 0 (concatD [doc (showString "#compute-nf"), prt 0 term])
Language.Rzk.Syntax.Abs.CommandPostulate _ varident declusedvars params term -> prPrec i 0 (concatD [doc (showString "#postulate"), prt 0 varident, prt 0 declusedvars, prt 0 params, doc (showString ":"), prt 0 term])
Language.Rzk.Syntax.Abs.CommandAssume _ varidents term -> prPrec i 0 (concatD [doc (showString "#assume"), prt 0 varidents, doc (showString ":"), prt 0 term])
Language.Rzk.Syntax.Abs.CommandSection _ sectionname1 commands sectionname2 -> prPrec i 0 (concatD [doc (showString "#section"), prt 0 sectionname1, doc (showString ";"), prt 0 commands, doc (showString "#end"), prt 0 sectionname2])
Language.Rzk.Syntax.Abs.CommandSection _ sectionname -> prPrec i 0 (concatD [doc (showString "#section"), prt 0 sectionname])
Language.Rzk.Syntax.Abs.CommandSectionEnd _ sectionname -> prPrec i 0 (concatD [doc (showString "#end"), prt 0 sectionname])
Language.Rzk.Syntax.Abs.CommandDefine _ varident declusedvars params term1 term2 -> prPrec i 0 (concatD [doc (showString "#define"), prt 0 varident, prt 0 declusedvars, prt 0 params, doc (showString ":"), prt 0 term1, doc (showString ":="), prt 0 term2])

instance Print [Language.Rzk.Syntax.Abs.Command' a] where
prt _ [] = concatD []
prt _ [] = concatD []
prt _ (x:xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs]

instance Print (Language.Rzk.Syntax.Abs.DeclUsedVars' a) where
Expand All @@ -197,8 +201,8 @@ instance Print (Language.Rzk.Syntax.Abs.Pattern' a) where
Language.Rzk.Syntax.Abs.PatternPair _ pattern_1 pattern_2 -> prPrec i 0 (concatD [doc (showString "("), prt 0 pattern_1, doc (showString ","), prt 0 pattern_2, doc (showString ")")])

instance Print [Language.Rzk.Syntax.Abs.Pattern' a] where
prt _ [] = concatD []
prt _ [x] = concatD [prt 0 x]
prt _ [] = concatD []
prt _ [x] = concatD [prt 0 x]
prt _ (x:xs) = concatD [prt 0 x, prt 0 xs]

instance Print (Language.Rzk.Syntax.Abs.Param' a) where
Expand All @@ -209,8 +213,8 @@ instance Print (Language.Rzk.Syntax.Abs.Param' a) where
Language.Rzk.Syntax.Abs.ParamPatternShapeDeprecated _ pattern_ term1 term2 -> prPrec i 0 (concatD [doc (showString "{"), prt 0 pattern_, doc (showString ":"), prt 0 term1, doc (showString "|"), prt 0 term2, doc (showString "}")])

instance Print [Language.Rzk.Syntax.Abs.Param' a] where
prt _ [] = concatD []
prt _ [x] = concatD [prt 0 x]
prt _ [] = concatD []
prt _ [x] = concatD [prt 0 x]
prt _ (x:xs) = concatD [prt 0 x, prt 0 xs]

instance Print (Language.Rzk.Syntax.Abs.ParamDecl' a) where
Expand All @@ -227,8 +231,8 @@ instance Print (Language.Rzk.Syntax.Abs.Restriction' a) where
Language.Rzk.Syntax.Abs.ASCII_Restriction _ term1 term2 -> prPrec i 0 (concatD [prt 0 term1, doc (showString "|->"), prt 0 term2])

instance Print [Language.Rzk.Syntax.Abs.Restriction' a] where
prt _ [] = concatD []
prt _ [x] = concatD [prt 0 x]
prt _ [] = concatD []
prt _ [x] = concatD [prt 0 x]
prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs]

instance Print (Language.Rzk.Syntax.Abs.Term' a) where
Expand Down Expand Up @@ -288,6 +292,6 @@ instance Print (Language.Rzk.Syntax.Abs.Term' a) where
Language.Rzk.Syntax.Abs.ASCII_Second _ term -> prPrec i 6 (concatD [doc (showString "second"), prt 7 term])

instance Print [Language.Rzk.Syntax.Abs.Term' a] where
prt _ [] = concatD []
prt _ [x] = concatD [prt 0 x]
prt _ [] = concatD []
prt _ [x] = concatD [prt 0 x]
prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs]
3 changes: 2 additions & 1 deletion rzk/src/Language/Rzk/Syntax/Skel.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,8 @@ transCommand x = case x of
Language.Rzk.Syntax.Abs.CommandComputeNF _ term -> failure x
Language.Rzk.Syntax.Abs.CommandPostulate _ varident declusedvars params term -> failure x
Language.Rzk.Syntax.Abs.CommandAssume _ varidents term -> failure x
Language.Rzk.Syntax.Abs.CommandSection _ sectionname1 commands sectionname2 -> failure x
Language.Rzk.Syntax.Abs.CommandSection _ sectionname -> failure x
Language.Rzk.Syntax.Abs.CommandSectionEnd _ sectionname -> failure x
Language.Rzk.Syntax.Abs.CommandDefine _ varident declusedvars params term1 term2 -> failure x

transDeclUsedVars :: Show a => Language.Rzk.Syntax.Abs.DeclUsedVars' a -> Result
Expand Down
4 changes: 2 additions & 2 deletions rzk/src/Language/Rzk/VSCode/Tokenize.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,8 +40,8 @@ tokenizeCommand command = case command of
[ foldMap (\var -> mkToken var vs_parameter [vs_declaration]) vars
, tokenizeTerm type_
]
CommandSection _loc _nameStart commands _nameEnd ->
foldMap tokenizeCommand commands
CommandSection _loc _nameStart -> []
CommandSectionEnd _loc _nameEnd -> []

tokenizeParam :: Param -> [VSToken]
tokenizeParam = \case
Expand Down
38 changes: 28 additions & 10 deletions rzk/src/Rzk/TypeCheck.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -72,10 +72,7 @@ typecheckModuleWithLocation (path, module_) = do
typecheckModule (Just path) module_

countCommands :: Integral a => [Rzk.Command] -> a
countCommands [] = 0
countCommands (Rzk.CommandSection _loc _name sectionCommands _name2 : commands) =
countCommands sectionCommands + countCommands commands
countCommands (_ : commands) = 1 + countCommands commands
countCommands = fromIntegral . length

typecheckModule :: Maybe FilePath -> Rzk.Module -> TypeCheck VarIdent [Decl']
typecheckModule path (Rzk.Module _moduleLoc _lang commands) =
Expand Down Expand Up @@ -170,13 +167,32 @@ typecheckModule path (Rzk.Module _moduleLoc _lang commands) =
localDeclsPrepared decls $
go (i + 1) moreCommands

go i (command@(Rzk.CommandSection _loc name sectionCommands endName) : moreCommands) = do
go i (command@(Rzk.CommandSection _loc name) : moreCommands) = do
(sectionCommands, moreCommands') <- splitSectionCommands name moreCommands
withCommand command $ do
when (Rzk.printTree name /= Rzk.printTree endName) $
issueTypeError $ TypeErrorOther $
"unexpected #end " <> Rzk.printTree endName <> ", expecting #end " <> Rzk.printTree name
withSection (Just name) (go i sectionCommands) $ do
go (i + countCommands sectionCommands) moreCommands
go (i + countCommands sectionCommands) moreCommands'

go _i (Rzk.CommandSectionEnd _loc endName : _moreCommands) = do
issueTypeError $ TypeErrorOther $
"unexpected #end " <> Rzk.printTree endName <> ", no section was declared!"


splitSectionCommands :: Rzk.SectionName -> [Rzk.Command] -> TypeCheck var ([Rzk.Command], [Rzk.Command])
splitSectionCommands name [] =
issueTypeError (TypeErrorOther $ "Section " <> show name <> " is not closed with an #end")
splitSectionCommands name (Rzk.CommandSection _loc name' : moreCommands) = do
(cs1, cs2) <- splitSectionCommands name' moreCommands
(cs3, cs4) <- splitSectionCommands name cs2
return (cs1 <> cs3, cs4)
splitSectionCommands name (Rzk.CommandSectionEnd _loc endName : moreCommands) = do
when (Rzk.printTree name /= Rzk.printTree endName) $
issueTypeError $ TypeErrorOther $
"unexpected #end " <> Rzk.printTree endName <> ", expecting #end " <> Rzk.printTree name
return ([], moreCommands)
splitSectionCommands name (command : moreCommands) = do
(cs1, cs2) <- splitSectionCommands name moreCommands
return (command : cs1, cs2)

setOption :: String -> String -> TypeCheck var a -> TypeCheck var a
setOption "verbosity" = \case
Expand Down Expand Up @@ -784,8 +800,10 @@ ppContext' ctx@Context{..} = unlines
" Error occurred when trying to unset option\n " <> Rzk.printTree command
Just command@Rzk.CommandAssume{} ->
" Error occurred when checking assumption\n " <> Rzk.printTree command
Just (Rzk.CommandSection _loc name _commands _endName) ->
Just (Rzk.CommandSection _loc name) ->
" Error occurred when checking\n #section " <> Rzk.printTree name
Just (Rzk.CommandSectionEnd _loc name) ->
" Error occurred when checking\n #end " <> Rzk.printTree name
Nothing -> " Error occurred"
-- , "Local tope context (expanded):"
-- , intercalate "\n" (map ((" " <>) . show . untyped) (intercalate [TopeAndT topeT topeBottomT topeBottomT] (saturateTopes [] <$> simplifyLHS localTopes)))
Expand Down

0 comments on commit 9c5e5b2

Please sign in to comment.