Skip to content

Commit

Permalink
Merge pull request #591 from conjure-cp/imply-non-assoc
Browse files Browse the repository at this point in the history
imply is non-associative
  • Loading branch information
ozgurakgun committed Oct 19, 2023
2 parents e2867d5 + c878c92 commit f6adf91
Show file tree
Hide file tree
Showing 18 changed files with 265 additions and 226 deletions.
2 changes: 2 additions & 0 deletions .github/workflows/test.yml
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ on:
- src/**
- tests/**
- etc/build/**
- etc/savilerow
- .github/workflows/test.yml
pull_request: # and for PRs
paths:
Expand All @@ -19,6 +20,7 @@ on:
- src/**
- tests/**
- etc/build/**
- etc/savilerow
- .github/workflows/test.yml
# other branches that want testing must create a PR

Expand Down
5 changes: 5 additions & 0 deletions .vscode/extensions.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
{
"recommendations": [
"haskell.haskell"
]
}
3 changes: 3 additions & 0 deletions conjure-cp.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -333,6 +333,7 @@ Library
ScopedTypeVariables
TypeOperators
ViewPatterns
ImportQualifiedPost
ghc-options:
-O1
-fwarn-incomplete-patterns
Expand Down Expand Up @@ -370,6 +371,7 @@ Executable conjure
ScopedTypeVariables
TypeOperators
ViewPatterns
ImportQualifiedPost
ghc-options:
-O1
-fwarn-incomplete-patterns
Expand Down Expand Up @@ -432,6 +434,7 @@ Test-Suite conjure-testing
ScopedTypeVariables
TypeOperators
ViewPatterns
ImportQualifiedPost
ghc-options:
-fwarn-incomplete-patterns
-fwarn-incomplete-uni-patterns
Expand Down
Binary file modified etc/savilerow/savilerow.jar
Binary file not shown.
2 changes: 1 addition & 1 deletion src/Conjure/Language/Expression/Op/Internal/Common.hs
Original file line number Diff line number Diff line change
Expand Up @@ -211,7 +211,7 @@ operators =
, ( BinaryOp L_Eq FNone , 400 )
, ( BinaryOp L_Or FLeft , 110 )
, ( BinaryOp L_And FLeft , 120 )
, ( BinaryOp L_Imply FLeft , 50 )
, ( BinaryOp L_Imply FNone , 50 )
, ( BinaryOp L_Iff FNone , 50 )
, ( BinaryOp L_union FLeft , 600 )
, ( BinaryOp L_intersect FLeft , 700 )
Expand Down
2 changes: 1 addition & 1 deletion src/Conjure/Prelude.hs
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ import Control.Category as X ( (<<<), (>>>) )

import Data.Data as X ( Data, Typeable )
import Data.Default as X ( Default, def )
import Data.Either as X ( Either(..), either, lefts, rights, partitionEithers )
import Data.Either as X ( Either(..), either, lefts, rights, partitionEithers, fromRight, fromLeft )
import Data.Function as X ( id, const, flip, on, ($), (.) )
import Data.List as X ( (\\), intercalate, intersperse, minimumBy, nub, nubBy
, group, groupBy, sort, sortBy
Expand Down
194 changes: 94 additions & 100 deletions src/Conjure/UI/ErrorDisplay.hs
Original file line number Diff line number Diff line change
@@ -1,42 +1,42 @@
module Conjure.UI.ErrorDisplay where
import Conjure.Prelude
import Conjure.Language.Validator
import Text.Megaparsec

import qualified Data.Set as Set
import Conjure.Language.AST.Syntax
import Conjure.Language.AST.ASTParser
import Conjure.Language.Lexer
import Conjure.Language.AST.Reformer
import Conjure.Language.AST.Syntax
import Conjure.Language.Lexemes
import qualified Data.Text
import qualified Data.Text as T
import Data.Map.Strict (assocs)
import Conjure.Language.Lexer
import Conjure.Language.Pretty
import Conjure.Language.AST.Reformer
import Conjure.Language.Validator
import Conjure.Prelude
import Data.Data

import Data.Map.Strict (assocs)
import qualified Data.Set as Set
import qualified Data.Text
import qualified Data.Text as T
import Text.Megaparsec

type Parser t = Parsec DiagnosticForPrint Text t

data DiagnosticForPrint = DiagnosticForPrint {
dStart :: Int,
data DiagnosticForPrint = DiagnosticForPrint
{ dStart :: Int,
dLength :: Int,
dMessage :: Diagnostic
} deriving (Show,Eq,Ord)
}
deriving (Show, Eq, Ord)

instance ShowErrorComponent DiagnosticForPrint where
errorComponentLen (DiagnosticForPrint {dLength = l}) = l

errorComponentLen (DiagnosticForPrint {dLength=l}) = l

showErrorComponent DiagnosticForPrint {dMessage=message}= case message of
Error et -> displayError et
showErrorComponent DiagnosticForPrint {dMessage = message} = case message of
Error et -> displayError et
Warning wt -> displayWarning wt
Info it -> "Info: " ++ show it

tokenErrorToDisplay :: LToken -> String
tokenErrorToDisplay (RealToken _ ) = error "tokenError with valid token"
tokenErrorToDisplay (RealToken _) = error "tokenError with valid token"
tokenErrorToDisplay (SkippedToken t) = "Unexpected " ++ lexemeFace (lexeme t)
tokenErrorToDisplay (MissingToken (lexeme->l)) = "Missing " ++ case l of
tokenErrorToDisplay (MissingToken (lexeme -> l)) =
"Missing " ++ case l of
L_Missing s -> show s
LMissingIdentifier -> "<identifier>"
_ -> T.unpack $ lexemeText l
Expand All @@ -52,116 +52,110 @@ displayError x = case x of
SemanticError txt -> "Error: " ++ T.unpack txt
CustomError txt -> "Error: " ++ T.unpack txt
TypeError expected got -> "Type error:\n\tExpected: " ++ show (pretty expected) ++ "\n\tGot: " ++ show (pretty got)
ComplexTypeError msg ty -> "Type error:\n\tExpected: " ++ show msg ++ "\n\tGot: " ++ (show $ pretty ty)
ComplexTypeError msg ty -> "Type error:\n\tExpected: " ++ show msg ++ "\n\tGot: " ++ show (pretty ty)
SkippedTokens -> "Skipped tokens"
UnexpectedArg -> "Unexpected argument"
MissingArgsError expected got -> "Insufficient args, expected " ++ (show expected) ++ " got " ++ (show got)
MissingArgsError expected got -> "Insufficient args, expected " ++ show expected ++ " got " ++ show got
InternalError -> "Pattern match failiure"
InternalErrorS txt -> "Something went wrong: " ++ T.unpack txt
WithReplacements e alts -> displayError e ++ "\n\tValid alternatives: " ++ intercalate "," (show <$> alts)
KindError a b -> show $ "Tried to use a " <> pretty b <> " where " <> pretty a <> " was expected"
CategoryError categ reason -> show $ "Cannot use variable of category :" <+> pretty categ <+> "in the context of " <> pretty reason

showDiagnosticsForConsole :: [ValidatorDiagnostic] -> Maybe String -> Text -> String
showDiagnosticsForConsole errs fileName text
= case runParser (captureErrors errs) (fromMaybe "Errors" fileName) text of
Left peb -> errorBundlePretty peb
Right _ -> "No printable errors from :" ++ (show . length $ errs)

showDiagnosticsForConsole errs fileName text =
case runParser (captureErrors errs) (fromMaybe "Errors" fileName) text of
Left peb -> errorBundlePretty peb
Right _ -> "No printable errors from :" ++ (show . length $ errs)

printSymbolTable :: SymbolTable -> IO ()
printSymbolTable tab = putStrLn "Symbol table" >> ( mapM_ printEntry $ assocs tab)
where
printEntry :: (Text ,SymbolTableValue) -> IO ()
printEntry (a,(_,c,t)) = putStrLn $ T.unpack a ++ ":" ++ show (pretty t) ++ if c then " Enum" else ""
printSymbolTable tab = putStrLn "Symbol table" >> mapM_ printEntry (assocs tab)
where
printEntry :: (Text, SymbolTableValue) -> IO ()
printEntry (a, (_, c, t)) = putStrLn $ T.unpack a ++ ":" ++ show (pretty t) ++ if c then " Enum" else ""

captureErrors :: [ValidatorDiagnostic] -> Parser ()
captureErrors = (mapM_ captureError) . collapseSkipped . removeAmbiguousTypeWarning
captureErrors = mapM_ captureError . collapseSkipped . removeAmbiguousTypeWarning

--Remove these warnings from a console print of errors as they are just clutter
-- Remove these warnings from a console print of errors as they are just clutter
removeAmbiguousTypeWarning :: [ValidatorDiagnostic] -> [ValidatorDiagnostic]
removeAmbiguousTypeWarning = filter (
\(ValidatorDiagnostic _ x)->
removeAmbiguousTypeWarning =
filter
( \(ValidatorDiagnostic _ x) ->
case x of
Warning AmbiguousTypeWarning->False;
_->True
Warning AmbiguousTypeWarning -> False
_ -> True
)


collapseSkipped :: [ValidatorDiagnostic] -> [ValidatorDiagnostic]
collapseSkipped [] = []
collapseSkipped [x] = [x]
collapseSkipped ((ValidatorDiagnostic regx ex) :(ValidatorDiagnostic regy ey):rs)
| isSkipped ex && isSkipped ey && sameLine (drSourcePos regx) (drSourcePos regy)
= collapseSkipped $ ValidatorDiagnostic (catDr regx regy) (Error $ SkippedTokens ) : rs
where
isSkipped (Error (TokenError (SkippedToken _))) = True
isSkipped (Error SkippedTokens) = True
isSkipped _ = False
sameLine :: SourcePos -> SourcePos -> Bool
sameLine (SourcePos _ l1 _) (SourcePos _ l2 _) = l1 == l2
catDr :: DiagnosticRegion -> DiagnosticRegion -> DiagnosticRegion
catDr (DiagnosticRegion sp _ o _) (DiagnosticRegion _ en _ _) = DiagnosticRegion sp en o ((unPos (sourceColumn en) - unPos (sourceColumn sp)))
collapseSkipped (x:xs) = x : collapseSkipped xs

collapseSkipped ((ValidatorDiagnostic regx ex) : (ValidatorDiagnostic regy ey) : rs)
| isSkipped ex && isSkipped ey && sameLine (drSourcePos regx) (drSourcePos regy) =
collapseSkipped $ ValidatorDiagnostic (catDr regx regy) (Error $ SkippedTokens) : rs
where
isSkipped (Error (TokenError (SkippedToken _))) = True
isSkipped (Error SkippedTokens) = True
isSkipped _ = False
sameLine :: SourcePos -> SourcePos -> Bool
sameLine (SourcePos _ l1 _) (SourcePos _ l2 _) = l1 == l2
catDr :: DiagnosticRegion -> DiagnosticRegion -> DiagnosticRegion
catDr (DiagnosticRegion sp _ o _) (DiagnosticRegion _ en _ _) = DiagnosticRegion sp en o (unPos (sourceColumn en) - unPos (sourceColumn sp))
collapseSkipped (x : xs) = x : collapseSkipped xs

captureError :: ValidatorDiagnostic -> Parser ()
captureError (ValidatorDiagnostic reg message) |reg == global = do
let printError = DiagnosticForPrint 0 0 message
registerFancyFailure (Set.singleton(ErrorCustom printError) )
captureError (ValidatorDiagnostic reg message) | reg == global = do
let printError = DiagnosticForPrint 0 0 message
registerFancyFailure (Set.singleton (ErrorCustom printError))
captureError (ValidatorDiagnostic area message) = do
setOffset $ drOffset area
let printError = DiagnosticForPrint (drOffset area) (drLength area) message
registerFancyFailure (Set.singleton(ErrorCustom printError) )


setOffset $ drOffset area
let printError = DiagnosticForPrint (drOffset area) (drLength area) message
registerFancyFailure (Set.singleton (ErrorCustom printError))

val :: String -> String -> IO ()
val path s = do
let str = s
let other = []
let txt = Data.Text.pack str
let lexed = runLexer txt (Just path)
let stream = either (const $ ETokenStream txt other) id lexed
let (ETokenStream _ toks) = stream
putStrLn $ concat $ map (T.unpack . capture) toks

-- parseTest parseProgram stream
let progStruct = runParser parseProgram "TEST" stream

case progStruct of
Left _ -> putStrLn "error"
Right p@(ProgramTree{}) -> let qpr = runValidator (validateModel p) (initialState p (Just txt)){typeChecking=True} in
case qpr of
(model, vds,st) -> do
print (show model)
putStrLn $ show vds
printSymbolTable $ symbolTable st
putStrLn $ show $ (regionInfo st)
putStrLn $ showDiagnosticsForConsole vds Nothing txt
putStrLn $ show . reformList $ flatten p
putStrLn $ show p

-- putStrLn $ show qpr

let str = s
let other = []
let txt = Data.Text.pack str
let lexed = runLexer txt (Just path)
let stream = fromRight (ETokenStream txt other) lexed
let (ETokenStream _ toks) = stream
putStrLn $ concatMap (T.unpack . capture) toks

-- parseTest parseProgram stream
let progStruct = runParser parseProgram "TEST" stream

case progStruct of
Left _ -> putStrLn "error"
Right p@(ProgramTree {}) ->
let qpr = runValidator (validateModel p) (initialState p (Just txt)) {typeChecking = True}
in case qpr of
(model, vds, st) -> do
print (show model)
print vds
printSymbolTable $ symbolTable st
print (regionInfo st)
putStrLn $ showDiagnosticsForConsole vds Nothing txt
print (reformList $ flatten p)
print p

valFile :: String -> IO ()
valFile p = do
path <- readFileIfExists p
case path of
Nothing -> putStrLn "NO such file"
Just s -> val p s
return ()
-- putStrLn validateFind

withParseTree :: String -> (ProgramTree -> IO ()) -> IO()
path <- readFileIfExists p
case path of
Nothing -> putStrLn "NO such file"
Just s -> val p s
return ()


withParseTree :: String -> (ProgramTree -> IO ()) -> IO ()
withParseTree pa f = do
fil <- readFileIfExists pa
case runParser parseProgram "TEST" (either (const $ error "bad") id $ runLexer (maybe "" T.pack fil) Nothing) of
Left _ -> error "bad"
Right pt -> void $ f pt
fil <- readFileIfExists pa
case runParser parseProgram "TEST" (fromRight (error "bad") $ runLexer (maybe "" T.pack fil) Nothing) of
Left _ -> error "bad"
Right pt -> void $ f pt

listBounds :: Int -> Int -> ProgramTree -> IO ()
listBounds :: Int -> Int -> ProgramTree -> IO ()
listBounds a b t = do
let hlt = makeTree t
sequence_ [print $ toConstr t' | x@(HLTagged t' _) <- universe hlt,contains (SourcePos "" (mkPos a) (mkPos b)) x]
let hlt = makeTree t
sequence_ [print $ toConstr t' | x@(HLTagged t' _) <- universe hlt, contains (SourcePos "" (mkPos a) (mkPos b)) x]
77 changes: 77 additions & 0 deletions tests/custom/basic/parsing-imply/stderr.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,77 @@
Error:
1_noparens.essence:7:19:
|
7 | such that a -> !b -> c -> d
| ^
Missing Expression

1_noparens.essence:7:19:
|
7 | such that a -> !b -> c -> d
| ^
Missing ,

1_noparens.essence:7:24:
|
7 | such that a -> !b -> c -> d
| ^
Missing Expression

1_noparens.essence:7:24:
|
7 | such that a -> !b -> c -> d
| ^
Missing ,

Error:
1_noparens.essence:7:19:
|
7 | such that a -> !b -> c -> d
| ^
Missing Expression

1_noparens.essence:7:19:
|
7 | such that a -> !b -> c -> d
| ^
Missing ,

1_noparens.essence:7:24:
|
7 | such that a -> !b -> c -> d
| ^
Missing Expression

1_noparens.essence:7:24:
|
7 | such that a -> !b -> c -> d
| ^
Missing ,

cat: conjure-output/model000001.solutions: No such file or directory
Error:
4_mixparens.essence:7:26:
|
7 | such that a -> (!b -> c) -> d
| ^
Missing Expression

4_mixparens.essence:7:26:
|
7 | such that a -> (!b -> c) -> d
| ^
Missing ,

Error:
4_mixparens.essence:7:26:
|
7 | such that a -> (!b -> c) -> d
| ^
Missing Expression

4_mixparens.essence:7:26:
|
7 | such that a -> (!b -> c) -> d
| ^
Missing ,

0 comments on commit f6adf91

Please sign in to comment.