From 8e146c08767fb452ad59b6557cb8d723f614a1aa Mon Sep 17 00:00:00 2001 From: Stoeffel Date: Tue, 14 Sep 2021 17:24:32 +0200 Subject: [PATCH 01/17] Remove done todo --- src/Haskell/Verified/Examples.hs | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/Haskell/Verified/Examples.hs b/src/Haskell/Verified/Examples.hs index 8daeece..b154b76 100644 --- a/src/Haskell/Verified/Examples.hs +++ b/src/Haskell/Verified/Examples.hs @@ -39,10 +39,6 @@ import qualified System.IO import qualified Text.Read import qualified Prelude --- TODO imports need to support qualified and stuff. This is just a hack to see how things work so far. --- We can use setImportsQ. --- And obviously need to parse it. --- verify :: Module -> Prelude.IO (List ExampleResult) verify mod = mod From a6ff516efd8aa9d3a61bd2c0b94c2b7baf844ba7 Mon Sep 17 00:00:00 2001 From: Stoeffel Date: Tue, 14 Sep 2021 17:26:51 +0200 Subject: [PATCH 02/17] Add new comment type --- src/Haskell/Verified/Examples.hs | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/src/Haskell/Verified/Examples.hs b/src/Haskell/Verified/Examples.hs index b154b76..ba3999b 100644 --- a/src/Haskell/Verified/Examples.hs +++ b/src/Haskell/Verified/Examples.hs @@ -256,7 +256,7 @@ toComments cs = PlainText -> PlainTextComment (LHE.SrcLoc.noInfoSpan srcSpan, Text.fromList val) ) -data CommentType = CodeBlock | PlainText +data CommentType = CodeBlock | PlainText | ContextBlock deriving (Show) mergeComments :: List (CommentType, LHE.Comments.Comment) -> List LHE.Comments.Comment -> List (CommentType, LHE.Comments.Comment) @@ -286,10 +286,18 @@ cleanCodeBlock (LHE.Comments.Comment t s text) = commentType :: LHE.Comments.Comment -> CommentType commentType (LHE.Comments.Comment _ _ text) = - if Text.startsWith " > " (Text.fromList text) - || Text.trim (Text.fromList text) == ">" + if hasArrow text then CodeBlock - else PlainText + else + if hasAt text + then ContextBlock + else PlainText + +hasAt text = Text.trim (Text.fromList text) == "@" + +hasArrow text = + Text.startsWith " > " (Text.fromList text) + || Text.trim (Text.fromList text) == ">" concatComment :: LHE.Comments.Comment -> LHE.Comments.Comment -> LHE.Comments.Comment concatComment (LHE.Comments.Comment _ srcSpanA a) (LHE.Comments.Comment _ srcSpanB b) = From b828797bf116c46f0f88e38a6d0b196b1d58a600 Mon Sep 17 00:00:00 2001 From: Stoeffel Date: Tue, 14 Sep 2021 17:30:34 +0200 Subject: [PATCH 03/17] Parse context blocks --- src/Haskell/Verified/Examples.hs | 50 +++++++++++------- src/Haskell/Verified/Examples/Internal.hs | 1 + test/Main.hs | 9 +++- test/assets/WithContext.hs | 16 ++++++ test/golden-results/parse-with-context.hs | 62 +++++++++++++++++++++++ 5 files changed, 118 insertions(+), 20 deletions(-) create mode 100644 test/assets/WithContext.hs create mode 100644 test/golden-results/parse-with-context.hs diff --git a/src/Haskell/Verified/Examples.hs b/src/Haskell/Verified/Examples.hs index ba3999b..2bb5209 100644 --- a/src/Haskell/Verified/Examples.hs +++ b/src/Haskell/Verified/Examples.hs @@ -211,6 +211,7 @@ examples = ( \c -> case c of PlainTextComment _ -> Nothing + ContextBlockComment _ -> Nothing CodeBlockComment example -> Just example ) @@ -244,7 +245,7 @@ toModule parsed = toComments :: List LHE.Comments.Comment -> List Comment toComments cs = cs - |> mergeComments [] + |> mergeComments [] False |> List.map ( \(ct, LHE.Comments.Comment _ srcSpan val) -> case ct of @@ -254,29 +255,40 @@ toComments cs = (Text.fromList val) |> CodeBlockComment PlainText -> PlainTextComment (LHE.SrcLoc.noInfoSpan srcSpan, Text.fromList val) + ContextBlock -> ContextBlockComment (LHE.SrcLoc.noInfoSpan srcSpan, Text.fromList val) ) data CommentType = CodeBlock | PlainText | ContextBlock deriving (Show) -mergeComments :: List (CommentType, LHE.Comments.Comment) -> List LHE.Comments.Comment -> List (CommentType, LHE.Comments.Comment) -mergeComments acc [] = List.reverse acc -mergeComments [] (next : rest) = - mergeComments - [ case commentType next of - CodeBlock -> (CodeBlock, cleanCodeBlock next) - PlainText -> (PlainText, next) - ] - rest -mergeComments (prev@(prevCT, prevComment) : acc) (next : rest) = - mergeComments - ( case (prevCT, commentType next) of - (CodeBlock, CodeBlock) -> (CodeBlock, concatComment prevComment (cleanCodeBlock next)) : acc - (PlainText, PlainText) -> (PlainText, concatComment prevComment next) : acc - (PlainText, CodeBlock) -> (CodeBlock, cleanCodeBlock next) : prev : acc - (CodeBlock, PlainText) -> (PlainText, next) : prev : acc - ) - rest +mergeComments :: List (CommentType, LHE.Comments.Comment) -> Bool -> List LHE.Comments.Comment -> List (CommentType, LHE.Comments.Comment) +mergeComments acc _ [] = List.reverse acc +mergeComments [] _ (next : rest) = + case commentType next of + CodeBlock -> mergeComments [(CodeBlock, cleanCodeBlock next)] False rest + PlainText -> mergeComments [(PlainText, next)] False rest + ContextBlock -> mergeComments [(ContextBlock, next)] True rest +mergeComments ((_, prevComment) : acc) True (next : rest) = + case commentType next of + CodeBlock -> mergeComments ((ContextBlock, concatComment prevComment next) : acc) True rest + PlainText -> mergeComments ((ContextBlock, concatComment prevComment next) : acc) True rest + ContextBlock -> mergeComments ((ContextBlock, concatComment prevComment (cleanCodeBlock next)) : acc) False rest +mergeComments (prev@(prevCT, prevComment) : acc) False (next : rest) = + case (prevCT, commentType next) of + (CodeBlock, CodeBlock) -> mergeComments ((CodeBlock, concatComment prevComment (cleanCodeBlock next)) : acc) False rest + (PlainText, PlainText) -> mergeComments ((PlainText, concatComment prevComment next) : acc) False rest + (PlainText, CodeBlock) -> mergeComments ((CodeBlock, cleanCodeBlock next) : prev : acc) False rest + (CodeBlock, PlainText) -> mergeComments ((PlainText, next) : prev : acc) False rest + (_, ContextBlock) -> mergeComments ((ContextBlock, cleanCodeBlock next) : prev : acc) True rest + (ContextBlock, CodeBlock) -> mergeComments ((CodeBlock, cleanCodeBlock next) : prev : acc) False rest + (ContextBlock, PlainText) -> mergeComments ((PlainText, next) : prev : acc) False rest + +-- @ +-- +-- +-- +-- +-- @ cleanCodeBlock :: LHE.Comments.Comment -> LHE.Comments.Comment cleanCodeBlock (LHE.Comments.Comment t s text) = diff --git a/src/Haskell/Verified/Examples/Internal.hs b/src/Haskell/Verified/Examples/Internal.hs index a65294d..370cd9c 100644 --- a/src/Haskell/Verified/Examples/Internal.hs +++ b/src/Haskell/Verified/Examples/Internal.hs @@ -40,6 +40,7 @@ data ModuleInfo = ModuleInfo data Comment = PlainTextComment (LHE.SrcLoc.SrcSpanInfo, Text) | CodeBlockComment Example + | ContextBlockComment (LHE.SrcLoc.SrcSpanInfo, Text) deriving (Show, Eq) data Example diff --git a/test/Main.hs b/test/Main.hs index 4bb04d1..8162dd0 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -33,7 +33,14 @@ tests = |> Expect.fromIO result |> Debug.toString - |> Expect.equalToContentsOf "test/golden-results/parse-unverified-examples.hs" + |> Expect.equalToContentsOf "test/golden-results/parse-unverified-examples.hs", + test "parses context code" <| \() -> do + result <- + HVE.parse "test/assets/WithContext.hs" + |> Expect.fromIO + result + |> Debug.toString + |> Expect.equalToContentsOf "test/golden-results/parse-with-context.hs" ], describe "verifyExample" diff --git a/test/assets/WithContext.hs b/test/assets/WithContext.hs new file mode 100644 index 0000000..6ebb5f5 --- /dev/null +++ b/test/assets/WithContext.hs @@ -0,0 +1,16 @@ +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE NoImplicitPrelude #-} + +module WithContext where + +import NriPrelude + +-- TypeApplications +-- +-- @ +-- result = Just "a" +-- @ +-- +-- > id @(Maybe [Char]) test ==> result +test :: Maybe [Char] +test = Just "a" diff --git a/test/golden-results/parse-with-context.hs b/test/golden-results/parse-with-context.hs new file mode 100644 index 0000000..14fb5c1 --- /dev/null +++ b/test/golden-results/parse-with-context.hs @@ -0,0 +1,62 @@ +Module + { moduleInfo = + ModuleInfo + { moduleName = Just "WithContext" + , moduleSource = + SrcSpanInfo + { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 1 1 17 1 + , srcInfoPoints = + [ SrcSpan "test/assets/WithContext.hs" 1 1 1 1 + , SrcSpan "test/assets/WithContext.hs" 2 1 2 1 + , SrcSpan "test/assets/WithContext.hs" 4 1 4 1 + , SrcSpan "test/assets/WithContext.hs" 4 1 4 1 + , SrcSpan "test/assets/WithContext.hs" 6 1 6 1 + , SrcSpan "test/assets/WithContext.hs" 15 1 15 1 + , SrcSpan "test/assets/WithContext.hs" 16 1 16 1 + , SrcSpan "test/assets/WithContext.hs" 17 1 17 1 + , SrcSpan "test/assets/WithContext.hs" 17 1 17 1 + ] + } + , languageExtensions = [ "TypeApplications" , "NoImplicitPrelude" ] + , imports = + [ ModuleImport + { modName = "NriPrelude" + , modQual = NotQualified + , modImp = NoImportList + } + ] + , importPaths = [] + , packageDbs = [] + } + , comments = + [ PlainTextComment + ( SrcSpanInfo + { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 8 1 9 3 + , srcInfoPoints = [] + } + , " TypeApplications\n" + ) + , ContextBlockComment + ( SrcSpanInfo + { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 10 1 12 5 + , srcInfoPoints = [] + } + , "\n result = Just \"a\"\n" + ) + , PlainTextComment + ( SrcSpanInfo + { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 13 1 13 3 + , srcInfoPoints = [] + } + , "" + ) + , CodeBlockComment + (VerifiedExample + ( SrcSpanInfo + { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 14 1 14 40 + , srcInfoPoints = [] + } + , "id @(Maybe [Char]) test ==> result" + )) + ] + } \ No newline at end of file From 5a44694f6ccab8992fd4853e1635533220ca4c65 Mon Sep 17 00:00:00 2001 From: Stoeffel Date: Fri, 17 Sep 2021 15:00:10 +0200 Subject: [PATCH 04/17] Update golden results --- test/golden-results/integration-simple.hs | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) diff --git a/test/golden-results/integration-simple.hs b/test/golden-results/integration-simple.hs index 8377a3e..ae202b5 100644 --- a/test/golden-results/integration-simple.hs +++ b/test/golden-results/integration-simple.hs @@ -91,6 +91,22 @@ test/assets/UnverifiedExamples.hs:29 In an equation for ‘e_112341’: e_112341 = [1, 2, 3, ....] |> map (+ 1) ==> True +Examples of module WithContext unverified. + +test/assets/WithContext.hs:14 + 9: -- + 10: -- @ + 11: -- result = Just "a" + 12: -- @ + 13: -- +✗ 14: -- > id @(Maybe [Char]) test ==> result + 15: test :: Maybe [Char] + 16: test = Just "a" + 17: +The example doesn't compile: +:2:1: error: + Variable not in scope: id :: Maybe [Char] -> a0:2:29: error: Variable not in scope: result + Examples unverified. test/assets/Headless.hs:3 @@ -118,6 +134,7 @@ No examples: 2 In these files: * test/assets/Simple.hs * test/assets/UnverifiedExamples.hs -Evaluation failed: 1 +Evaluation failed: 2 In these files: - * test/assets/UnverifiedExamples.hs \ No newline at end of file + * test/assets/UnverifiedExamples.hs + * test/assets/WithContext.hs \ No newline at end of file From fd2505a8ab6dc82760582fc19752740a4dd8f7f8 Mon Sep 17 00:00:00 2001 From: Stoeffel Date: Fri, 17 Sep 2021 15:01:41 +0200 Subject: [PATCH 05/17] Better context test --- src/Haskell/Verified/Examples.hs | 1 + test/assets/WithContext.hs | 3 +++ test/golden-results/integration-simple.hs | 20 ++++++++++---------- test/golden-results/parse-with-context.hs | 18 +++++++++--------- 4 files changed, 23 insertions(+), 19 deletions(-) diff --git a/src/Haskell/Verified/Examples.hs b/src/Haskell/Verified/Examples.hs index 2bb5209..e8ecdc3 100644 --- a/src/Haskell/Verified/Examples.hs +++ b/src/Haskell/Verified/Examples.hs @@ -261,6 +261,7 @@ toComments cs = data CommentType = CodeBlock | PlainText | ContextBlock deriving (Show) +-- TODO wow this needs some cleaning up mergeComments :: List (CommentType, LHE.Comments.Comment) -> Bool -> List LHE.Comments.Comment -> List (CommentType, LHE.Comments.Comment) mergeComments acc _ [] = List.reverse acc mergeComments [] _ (next : rest) = diff --git a/test/assets/WithContext.hs b/test/assets/WithContext.hs index 6ebb5f5..31cfc5f 100644 --- a/test/assets/WithContext.hs +++ b/test/assets/WithContext.hs @@ -8,6 +8,9 @@ import NriPrelude -- TypeApplications -- -- @ +-- import Prelude +-- +-- result :: Maybe [Char] -- result = Just "a" -- @ -- diff --git a/test/golden-results/integration-simple.hs b/test/golden-results/integration-simple.hs index ae202b5..bd6d9da 100644 --- a/test/golden-results/integration-simple.hs +++ b/test/golden-results/integration-simple.hs @@ -93,16 +93,16 @@ test/assets/UnverifiedExamples.hs:29 Examples of module WithContext unverified. -test/assets/WithContext.hs:14 - 9: -- - 10: -- @ - 11: -- result = Just "a" - 12: -- @ - 13: -- -✗ 14: -- > id @(Maybe [Char]) test ==> result - 15: test :: Maybe [Char] - 16: test = Just "a" - 17: +test/assets/WithContext.hs:17 + 12: -- + 13: -- result :: Maybe [Char] + 14: -- result = Just "a" + 15: -- @ + 16: -- +✗ 17: -- > id @(Maybe [Char]) test ==> result + 18: test :: Maybe [Char] + 19: test = Just "a" + 20: The example doesn't compile: :2:1: error: Variable not in scope: id :: Maybe [Char] -> a0:2:29: error: Variable not in scope: result diff --git a/test/golden-results/parse-with-context.hs b/test/golden-results/parse-with-context.hs index 14fb5c1..d31d290 100644 --- a/test/golden-results/parse-with-context.hs +++ b/test/golden-results/parse-with-context.hs @@ -4,17 +4,17 @@ Module { moduleName = Just "WithContext" , moduleSource = SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 1 1 17 1 + { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 1 1 20 1 , srcInfoPoints = [ SrcSpan "test/assets/WithContext.hs" 1 1 1 1 , SrcSpan "test/assets/WithContext.hs" 2 1 2 1 , SrcSpan "test/assets/WithContext.hs" 4 1 4 1 , SrcSpan "test/assets/WithContext.hs" 4 1 4 1 , SrcSpan "test/assets/WithContext.hs" 6 1 6 1 - , SrcSpan "test/assets/WithContext.hs" 15 1 15 1 - , SrcSpan "test/assets/WithContext.hs" 16 1 16 1 - , SrcSpan "test/assets/WithContext.hs" 17 1 17 1 - , SrcSpan "test/assets/WithContext.hs" 17 1 17 1 + , SrcSpan "test/assets/WithContext.hs" 18 1 18 1 + , SrcSpan "test/assets/WithContext.hs" 19 1 19 1 + , SrcSpan "test/assets/WithContext.hs" 20 1 20 1 + , SrcSpan "test/assets/WithContext.hs" 20 1 20 1 ] } , languageExtensions = [ "TypeApplications" , "NoImplicitPrelude" ] @@ -38,14 +38,14 @@ Module ) , ContextBlockComment ( SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 10 1 12 5 + { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 10 1 15 5 , srcInfoPoints = [] } - , "\n result = Just \"a\"\n" + , "\n import Prelude\n\n result :: Maybe [Char]\n result = Just \"a\"\n" ) , PlainTextComment ( SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 13 1 13 3 + { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 16 1 16 3 , srcInfoPoints = [] } , "" @@ -53,7 +53,7 @@ Module , CodeBlockComment (VerifiedExample ( SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 14 1 14 40 + { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 17 1 17 40 , srcInfoPoints = [] } , "id @(Maybe [Char]) test ==> result" From 26bcaa4d1b5b515f90cd99c521e2a80262a38cae Mon Sep 17 00:00:00 2001 From: Stoeffel Date: Sat, 18 Sep 2021 08:54:07 +0200 Subject: [PATCH 06/17] Smaller context test --- test/assets/WithContext.hs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/test/assets/WithContext.hs b/test/assets/WithContext.hs index 31cfc5f..85bc8db 100644 --- a/test/assets/WithContext.hs +++ b/test/assets/WithContext.hs @@ -8,12 +8,10 @@ import NriPrelude -- TypeApplications -- -- @ --- import Prelude --- -- result :: Maybe [Char] -- result = Just "a" -- @ -- --- > id @(Maybe [Char]) test ==> result +-- > identity @(Maybe [Char]) test ==> result test :: Maybe [Char] test = Just "a" From 17c95b9bf1efe3fee99c2b3867572d573edbddc4 Mon Sep 17 00:00:00 2001 From: Stoeffel Date: Sat, 18 Sep 2021 09:14:53 +0200 Subject: [PATCH 07/17] Cleanup mergeComments --- src/Haskell/Verified/Examples.hs | 82 ++++++++----------- src/Haskell/Verified/Examples/Internal.hs | 8 +- test/Main.hs | 4 +- test/golden-results/integration-simple.hs | 24 +++--- test/golden-results/parse-simple.hs | 12 +-- .../parse-unverified-examples.hs | 26 +++--- test/golden-results/parse-with-context.hs | 22 ++--- .../verifyExample-multiline-unverified.hs | 12 ++- .../verifyExample-multiline-verified.hs | 12 ++- .../verifyExample-unverified.hs | 2 +- test/golden-results/verifyExample-verified.hs | 2 +- 11 files changed, 109 insertions(+), 97 deletions(-) diff --git a/src/Haskell/Verified/Examples.hs b/src/Haskell/Verified/Examples.hs index e8ecdc3..51eb98b 100644 --- a/src/Haskell/Verified/Examples.hs +++ b/src/Haskell/Verified/Examples.hs @@ -18,6 +18,7 @@ where import qualified Control.Concurrent.Async as Async import qualified Data.Foldable as Foldable +import qualified Data.List import qualified HIE.Bios.Cradle import qualified HIE.Bios.Environment import qualified HIE.Bios.Flags @@ -50,7 +51,7 @@ verifyExample :: ModuleInfo -> Example -> Prelude.IO ExampleResult verifyExample modInfo example = case example of VerifiedExample (_, code) -> do - result <- eval modInfo code + result <- eval modInfo (Prelude.unlines code) case result of Prelude.Left err -> Prelude.pure (ExampleVerifyFailed example err) @@ -117,7 +118,7 @@ makeImport importDecl = importToString (LHE.Syntax.IThingAll _ n) = getName n ++ "(..)" importToString (LHE.Syntax.IThingWith _ n ns) = getName n ++ "(" ++ (List.concat <| List.intersperse "," (List.map getCName ns)) ++ ")" -eval :: ModuleInfo -> Text -> Prelude.IO (Prelude.Either Hint.InterpreterError Verified) +eval :: ModuleInfo -> Prelude.String -> Prelude.IO (Prelude.Either Hint.InterpreterError Verified) eval moduleInfo s = do let modulePath = moduleFilePath moduleInfo let interpreter = case packageDbs moduleInfo of @@ -150,7 +151,7 @@ eval moduleInfo s = do ] Hint.setImportsF (exampleImports ++ imports moduleInfo) - Hint.interpret (Text.toList s) (Hint.as :: Verified) + Hint.interpret s (Hint.as :: Verified) trimPrefix :: Text -> Text -> Maybe Text trimPrefix prefix text @@ -166,9 +167,9 @@ getDefaultLanguageExtensions = List.filterMap <| trimPrefix "-X" getPackageDbs :: List Text -> List Text getPackageDbs options = List.concat [[l, r] | (l, r) <- Prelude.zip options (List.drop 1 options), l == "-package-db"] -exampleFromText :: Text -> Example +exampleFromText :: Prelude.String -> Example exampleFromText val = - toExample LHE.SrcLoc.noSrcSpan val + toExample LHE.SrcLoc.noSrcSpan (Prelude.lines val) parse :: Prelude.FilePath -> Prelude.IO Module parse path = do @@ -247,55 +248,40 @@ toComments cs = cs |> mergeComments [] False |> List.map - ( \(ct, LHE.Comments.Comment _ srcSpan val) -> + ( \(ct, (LHE.Comments.Comment _ srcSpan val)) -> case ct of CodeBlock -> - toExample - (LHE.SrcLoc.noInfoSpan srcSpan) - (Text.fromList val) + val + |> Prelude.lines + |> List.map (Prelude.dropWhile (/= '>') >> Prelude.drop 2) + |> toExample (LHE.SrcLoc.noInfoSpan srcSpan) |> CodeBlockComment - PlainText -> PlainTextComment (LHE.SrcLoc.noInfoSpan srcSpan, Text.fromList val) - ContextBlock -> ContextBlockComment (LHE.SrcLoc.noInfoSpan srcSpan, Text.fromList val) + PlainText -> PlainTextComment (LHE.SrcLoc.noInfoSpan srcSpan, [val]) + ContextBlock -> + val + |> Prelude.lines + |> Data.List.tail + |> Data.List.init + |> List.map (Prelude.drop 1) + |> (,) (LHE.SrcLoc.noInfoSpan srcSpan) + |> ContextBlockComment ) data CommentType = CodeBlock | PlainText | ContextBlock - deriving (Show) + deriving (Show, Eq) --- TODO wow this needs some cleaning up mergeComments :: List (CommentType, LHE.Comments.Comment) -> Bool -> List LHE.Comments.Comment -> List (CommentType, LHE.Comments.Comment) mergeComments acc _ [] = List.reverse acc -mergeComments [] _ (next : rest) = - case commentType next of - CodeBlock -> mergeComments [(CodeBlock, cleanCodeBlock next)] False rest - PlainText -> mergeComments [(PlainText, next)] False rest - ContextBlock -> mergeComments [(ContextBlock, next)] True rest -mergeComments ((_, prevComment) : acc) True (next : rest) = - case commentType next of - CodeBlock -> mergeComments ((ContextBlock, concatComment prevComment next) : acc) True rest - PlainText -> mergeComments ((ContextBlock, concatComment prevComment next) : acc) True rest - ContextBlock -> mergeComments ((ContextBlock, concatComment prevComment (cleanCodeBlock next)) : acc) False rest -mergeComments (prev@(prevCT, prevComment) : acc) False (next : rest) = - case (prevCT, commentType next) of - (CodeBlock, CodeBlock) -> mergeComments ((CodeBlock, concatComment prevComment (cleanCodeBlock next)) : acc) False rest - (PlainText, PlainText) -> mergeComments ((PlainText, concatComment prevComment next) : acc) False rest - (PlainText, CodeBlock) -> mergeComments ((CodeBlock, cleanCodeBlock next) : prev : acc) False rest - (CodeBlock, PlainText) -> mergeComments ((PlainText, next) : prev : acc) False rest - (_, ContextBlock) -> mergeComments ((ContextBlock, cleanCodeBlock next) : prev : acc) True rest - (ContextBlock, CodeBlock) -> mergeComments ((CodeBlock, cleanCodeBlock next) : prev : acc) False rest - (ContextBlock, PlainText) -> mergeComments ((PlainText, next) : prev : acc) False rest - --- @ --- --- --- --- --- @ - -cleanCodeBlock :: LHE.Comments.Comment -> LHE.Comments.Comment -cleanCodeBlock (LHE.Comments.Comment t s text) = - text - |> Prelude.drop 3 - |> LHE.Comments.Comment t s +mergeComments acc isInContext (next : restNext) = + let nextCt = commentType next + stillInContext = if isInContext then nextCt /= ContextBlock else nextCt == ContextBlock + newAcc = case acc of + [] -> [(nextCt, next)] + (prevCt, prev) : restPrev -> + if isInContext || prevCt == nextCt + then (prevCt, concatComment prev next) : restPrev + else (nextCt, next) : acc + in mergeComments newAcc stillInContext restNext commentType :: LHE.Comments.Comment -> CommentType commentType (LHE.Comments.Comment _ _ text) = @@ -313,12 +299,12 @@ hasArrow text = || Text.trim (Text.fromList text) == ">" concatComment :: LHE.Comments.Comment -> LHE.Comments.Comment -> LHE.Comments.Comment -concatComment (LHE.Comments.Comment _ srcSpanA a) (LHE.Comments.Comment _ srcSpanB b) = +concatComment commentA@(LHE.Comments.Comment _ srcSpanA a) commentB@(LHE.Comments.Comment _ srcSpanB b) = LHE.Comments.Comment True (LHE.SrcLoc.mergeSrcSpan srcSpanA srcSpanB) (a ++ "\n" ++ b) -toExample :: LHE.SrcLoc.SrcSpanInfo -> Text -> Example +toExample :: LHE.SrcLoc.SrcSpanInfo -> List Prelude.String -> Example toExample srcLocInfo source = - case LHE.Lexer.lexTokenStream (Text.toList source) of + case LHE.Lexer.lexTokenStream (Prelude.unlines source) of LHE.Parser.ParseOk tokens -> if Foldable.any ((== LHE.Lexer.VarSym "==>") << LHE.Lexer.unLoc) tokens then VerifiedExample (srcLocInfo, source) diff --git a/src/Haskell/Verified/Examples/Internal.hs b/src/Haskell/Verified/Examples/Internal.hs index 370cd9c..59a0c68 100644 --- a/src/Haskell/Verified/Examples/Internal.hs +++ b/src/Haskell/Verified/Examples/Internal.hs @@ -38,14 +38,14 @@ data ModuleInfo = ModuleInfo deriving (Show) data Comment - = PlainTextComment (LHE.SrcLoc.SrcSpanInfo, Text) + = PlainTextComment (LHE.SrcLoc.SrcSpanInfo, List Prelude.String) | CodeBlockComment Example - | ContextBlockComment (LHE.SrcLoc.SrcSpanInfo, Text) + | ContextBlockComment (LHE.SrcLoc.SrcSpanInfo, List Prelude.String) deriving (Show, Eq) data Example - = VerifiedExample (LHE.SrcLoc.SrcSpanInfo, Text) - | UnverifiedExample (LHE.SrcLoc.SrcSpanInfo, Text) + = VerifiedExample (LHE.SrcLoc.SrcSpanInfo, List Prelude.String) + | UnverifiedExample (LHE.SrcLoc.SrcSpanInfo, List Prelude.String) deriving (Show, Eq) exampleSrcSpan :: Example -> LHE.SrcLoc.SrcSpan diff --git a/test/Main.hs b/test/Main.hs index 8162dd0..544aef9 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -78,7 +78,7 @@ tests = ", 4", "]" ] - |> Text.join "\n" + |> Prelude.unlines |> HVE.exampleFromText result <- example @@ -101,7 +101,7 @@ tests = ", 5", "]" ] - |> Text.join "\n" + |> Prelude.unlines |> HVE.exampleFromText result <- example diff --git a/test/golden-results/integration-simple.hs b/test/golden-results/integration-simple.hs index bd6d9da..398e676 100644 --- a/test/golden-results/integration-simple.hs +++ b/test/golden-results/integration-simple.hs @@ -93,19 +93,19 @@ test/assets/UnverifiedExamples.hs:29 Examples of module WithContext unverified. -test/assets/WithContext.hs:17 - 12: -- - 13: -- result :: Maybe [Char] - 14: -- result = Just "a" - 15: -- @ - 16: -- -✗ 17: -- > id @(Maybe [Char]) test ==> result - 18: test :: Maybe [Char] - 19: test = Just "a" - 20: +test/assets/WithContext.hs:15 + 10: -- @ + 11: -- result :: Maybe [Char] + 12: -- result = Just "a" + 13: -- @ + 14: -- +✗ 15: -- > identity @(Maybe [Char]) test ==> result + 16: test :: Maybe [Char] + 17: test = Just "a" + 18: The example doesn't compile: -:2:1: error: - Variable not in scope: id :: Maybe [Char] -> a0:2:29: error: Variable not in scope: result +:2:35: error: + Variable not in scope: result :: Maybe [Char] Examples unverified. diff --git a/test/golden-results/parse-simple.hs b/test/golden-results/parse-simple.hs index 3b89dc5..6944830 100644 --- a/test/golden-results/parse-simple.hs +++ b/test/golden-results/parse-simple.hs @@ -32,7 +32,7 @@ Module { srcInfoSpan = SrcSpan "test/assets/Simple.hs" 7 1 8 3 , srcInfoPoints = [] } - , " hello world\n" + , [ " hello world\n" ] ) , CodeBlockComment (VerifiedExample @@ -40,14 +40,14 @@ Module { srcInfoSpan = SrcSpan "test/assets/Simple.hs" 9 1 10 11 , srcInfoPoints = [] } - , "test\n==> 1" + , [ "test" , "==> 1" ] )) , PlainTextComment ( SrcSpanInfo { srcInfoSpan = SrcSpan "test/assets/Simple.hs" 11 1 11 3 , srcInfoPoints = [] } - , "" + , [ "" ] ) , CodeBlockComment (VerifiedExample @@ -55,14 +55,14 @@ Module { srcInfoSpan = SrcSpan "test/assets/Simple.hs" 12 1 13 11 , srcInfoPoints = [] } - , "test + test\n==> 2" + , [ "test + test" , "==> 2" ] )) , PlainTextComment ( SrcSpanInfo { srcInfoSpan = SrcSpan "test/assets/Simple.hs" 14 1 14 3 , srcInfoPoints = [] } - , "" + , [ "" ] ) , CodeBlockComment (UnverifiedExample @@ -70,7 +70,7 @@ Module { srcInfoSpan = SrcSpan "test/assets/Simple.hs" 15 1 15 17 , srcInfoPoints = [] } - , "test + test" + , [ "test + test" ] )) ] } \ No newline at end of file diff --git a/test/golden-results/parse-unverified-examples.hs b/test/golden-results/parse-unverified-examples.hs index c2e1612..1b51dff 100644 --- a/test/golden-results/parse-unverified-examples.hs +++ b/test/golden-results/parse-unverified-examples.hs @@ -33,7 +33,7 @@ Module { srcInfoSpan = SrcSpan "test/assets/UnverifiedExamples.hs" 7 1 8 3 , srcInfoPoints = [] } - , " hello world\n" + , [ " hello world\n" ] ) , CodeBlockComment (VerifiedExample @@ -42,7 +42,7 @@ Module SrcSpan "test/assets/UnverifiedExamples.hs" 9 1 10 11 , srcInfoPoints = [] } - , "test\n==> 1" + , [ "test" , "==> 1" ] )) , PlainTextComment ( SrcSpanInfo @@ -50,7 +50,7 @@ Module SrcSpan "test/assets/UnverifiedExamples.hs" 11 1 11 3 , srcInfoPoints = [] } - , "" + , [ "" ] ) , CodeBlockComment (UnverifiedExample @@ -59,7 +59,7 @@ Module SrcSpan "test/assets/UnverifiedExamples.hs" 12 1 12 10 , srcInfoPoints = [] } - , "test" + , [ "test" ] )) , PlainTextComment ( SrcSpanInfo @@ -67,7 +67,7 @@ Module SrcSpan "test/assets/UnverifiedExamples.hs" 13 1 13 3 , srcInfoPoints = [] } - , "" + , [ "" ] ) , CodeBlockComment (VerifiedExample @@ -76,7 +76,7 @@ Module SrcSpan "test/assets/UnverifiedExamples.hs" 14 1 15 11 , srcInfoPoints = [] } - , "test + test\n==> 3" + , [ "test + test" , "==> 3" ] )) , PlainTextComment ( SrcSpanInfo @@ -84,7 +84,7 @@ Module SrcSpan "test/assets/UnverifiedExamples.hs" 18 1 19 3 , srcInfoPoints = [] } - , " | more stuff\n" + , [ " | more stuff\n" ] ) , CodeBlockComment (VerifiedExample @@ -93,7 +93,13 @@ Module SrcSpan "test/assets/UnverifiedExamples.hs" 20 1 25 21 , srcInfoPoints = [] } - , "[ 1\n, 2\n, 3\n, 4\n] |> map (+ 1)\n==> [ 2, 4, 5 ]" + , [ "[ 1" + , ", 2" + , ", 3" + , ", 4" + , "] |> map (+ 1)" + , "==> [ 2, 4, 5 ]" + ] )) , PlainTextComment ( SrcSpanInfo @@ -101,7 +107,7 @@ Module SrcSpan "test/assets/UnverifiedExamples.hs" 27 1 28 3 , srcInfoPoints = [] } - , " | compilation fails\n" + , [ " | compilation fails\n" ] ) , CodeBlockComment (VerifiedExample @@ -110,7 +116,7 @@ Module SrcSpan "test/assets/UnverifiedExamples.hs" 29 1 34 14 , srcInfoPoints = [] } - , "[ 1\n, 2\n, 3\n, 4\n] |> map (+ 1)\n==> True" + , [ "[ 1" , ", 2" , ", 3" , ", 4" , "] |> map (+ 1)" , "==> True" ] )) ] } \ No newline at end of file diff --git a/test/golden-results/parse-with-context.hs b/test/golden-results/parse-with-context.hs index d31d290..cc1fa90 100644 --- a/test/golden-results/parse-with-context.hs +++ b/test/golden-results/parse-with-context.hs @@ -4,17 +4,17 @@ Module { moduleName = Just "WithContext" , moduleSource = SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 1 1 20 1 + { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 1 1 18 1 , srcInfoPoints = [ SrcSpan "test/assets/WithContext.hs" 1 1 1 1 , SrcSpan "test/assets/WithContext.hs" 2 1 2 1 , SrcSpan "test/assets/WithContext.hs" 4 1 4 1 , SrcSpan "test/assets/WithContext.hs" 4 1 4 1 , SrcSpan "test/assets/WithContext.hs" 6 1 6 1 + , SrcSpan "test/assets/WithContext.hs" 16 1 16 1 + , SrcSpan "test/assets/WithContext.hs" 17 1 17 1 + , SrcSpan "test/assets/WithContext.hs" 18 1 18 1 , SrcSpan "test/assets/WithContext.hs" 18 1 18 1 - , SrcSpan "test/assets/WithContext.hs" 19 1 19 1 - , SrcSpan "test/assets/WithContext.hs" 20 1 20 1 - , SrcSpan "test/assets/WithContext.hs" 20 1 20 1 ] } , languageExtensions = [ "TypeApplications" , "NoImplicitPrelude" ] @@ -34,29 +34,29 @@ Module { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 8 1 9 3 , srcInfoPoints = [] } - , " TypeApplications\n" + , [ " TypeApplications\n" ] ) , ContextBlockComment ( SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 10 1 15 5 + { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 10 1 13 5 , srcInfoPoints = [] } - , "\n import Prelude\n\n result :: Maybe [Char]\n result = Just \"a\"\n" + , [ "result :: Maybe [Char]" , "result = Just \"a\"" ] ) , PlainTextComment ( SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 16 1 16 3 + { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 14 1 14 3 , srcInfoPoints = [] } - , "" + , [ "" ] ) , CodeBlockComment (VerifiedExample ( SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 17 1 17 40 + { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 15 1 15 46 , srcInfoPoints = [] } - , "id @(Maybe [Char]) test ==> result" + , [ "identity @(Maybe [Char]) test ==> result" ] )) ] } \ No newline at end of file diff --git a/test/golden-results/verifyExample-multiline-unverified.hs b/test/golden-results/verifyExample-multiline-unverified.hs index 06235f3..f3afaee 100644 --- a/test/golden-results/verifyExample-multiline-unverified.hs +++ b/test/golden-results/verifyExample-multiline-unverified.hs @@ -4,6 +4,16 @@ ExampleVerifySuccess { srcInfoSpan = SrcSpan "" (-1) (-1) (-1) (-1) , srcInfoPoints = [] } - , "[ 1\n, 2\n, 3\n]\n|> List.map (+ 1)\n==>\n[ 2\n, 3\n, 5\n]" + , [ "[ 1" + , ", 2" + , ", 3" + , "]" + , "|> List.map (+ 1)" + , "==>" + , "[ 2" + , ", 3" + , ", 5" + , "]" + ] )) (Unverified "[2,3,4]" "[2,3,5]") \ No newline at end of file diff --git a/test/golden-results/verifyExample-multiline-verified.hs b/test/golden-results/verifyExample-multiline-verified.hs index c0ec6fb..fefa33e 100644 --- a/test/golden-results/verifyExample-multiline-verified.hs +++ b/test/golden-results/verifyExample-multiline-verified.hs @@ -4,6 +4,16 @@ ExampleVerifySuccess { srcInfoSpan = SrcSpan "" (-1) (-1) (-1) (-1) , srcInfoPoints = [] } - , "[ 1\n, 2\n, 3\n]\n|> List.map (+ 1)\n==>\n[ 2\n, 3\n, 4\n]" + , [ "[ 1" + , ", 2" + , ", 3" + , "]" + , "|> List.map (+ 1)" + , "==>" + , "[ 2" + , ", 3" + , ", 4" + , "]" + ] )) Verified \ No newline at end of file diff --git a/test/golden-results/verifyExample-unverified.hs b/test/golden-results/verifyExample-unverified.hs index 42fbfca..bb4f990 100644 --- a/test/golden-results/verifyExample-unverified.hs +++ b/test/golden-results/verifyExample-unverified.hs @@ -4,6 +4,6 @@ ExampleVerifySuccess { srcInfoSpan = SrcSpan "" (-1) (-1) (-1) (-1) , srcInfoPoints = [] } - , "1 + 1 ==> 3" + , [ "1 + 1 ==> 3" ] )) (Unverified "2" "3") \ No newline at end of file diff --git a/test/golden-results/verifyExample-verified.hs b/test/golden-results/verifyExample-verified.hs index 9a97f0a..fe61fa1 100644 --- a/test/golden-results/verifyExample-verified.hs +++ b/test/golden-results/verifyExample-verified.hs @@ -4,6 +4,6 @@ ExampleVerifySuccess { srcInfoSpan = SrcSpan "" (-1) (-1) (-1) (-1) , srcInfoPoints = [] } - , "1 + 1 ==> 2" + , [ "1 + 1 ==> 2" ] )) Verified \ No newline at end of file From a105a164b58b2194c8d73d697922545a8f6918de Mon Sep 17 00:00:00 2001 From: Stoeffel Date: Mon, 20 Sep 2021 11:30:05 +0200 Subject: [PATCH 08/17] Don't keep plain text comments around --- src/Haskell/Verified/Examples.hs | 7 ++-- src/Haskell/Verified/Examples/Internal.hs | 3 +- test/golden-results/parse-simple.hs | 23 +---------- .../parse-unverified-examples.hs | 41 +------------------ test/golden-results/parse-with-context.hs | 16 +------- 5 files changed, 8 insertions(+), 82 deletions(-) diff --git a/src/Haskell/Verified/Examples.hs b/src/Haskell/Verified/Examples.hs index 51eb98b..d7f7201 100644 --- a/src/Haskell/Verified/Examples.hs +++ b/src/Haskell/Verified/Examples.hs @@ -211,7 +211,6 @@ examples = List.filterMap ( \c -> case c of - PlainTextComment _ -> Nothing ContextBlockComment _ -> Nothing CodeBlockComment example -> Just example ) @@ -247,16 +246,17 @@ toComments :: List LHE.Comments.Comment -> List Comment toComments cs = cs |> mergeComments [] False - |> List.map + |> List.filterMap ( \(ct, (LHE.Comments.Comment _ srcSpan val)) -> case ct of + PlainText -> Nothing CodeBlock -> val |> Prelude.lines |> List.map (Prelude.dropWhile (/= '>') >> Prelude.drop 2) |> toExample (LHE.SrcLoc.noInfoSpan srcSpan) |> CodeBlockComment - PlainText -> PlainTextComment (LHE.SrcLoc.noInfoSpan srcSpan, [val]) + |> Just ContextBlock -> val |> Prelude.lines @@ -265,6 +265,7 @@ toComments cs = |> List.map (Prelude.drop 1) |> (,) (LHE.SrcLoc.noInfoSpan srcSpan) |> ContextBlockComment + |> Just ) data CommentType = CodeBlock | PlainText | ContextBlock diff --git a/src/Haskell/Verified/Examples/Internal.hs b/src/Haskell/Verified/Examples/Internal.hs index 59a0c68..22124ee 100644 --- a/src/Haskell/Verified/Examples/Internal.hs +++ b/src/Haskell/Verified/Examples/Internal.hs @@ -38,8 +38,7 @@ data ModuleInfo = ModuleInfo deriving (Show) data Comment - = PlainTextComment (LHE.SrcLoc.SrcSpanInfo, List Prelude.String) - | CodeBlockComment Example + = CodeBlockComment Example | ContextBlockComment (LHE.SrcLoc.SrcSpanInfo, List Prelude.String) deriving (Show, Eq) diff --git a/test/golden-results/parse-simple.hs b/test/golden-results/parse-simple.hs index 6944830..a1d1011 100644 --- a/test/golden-results/parse-simple.hs +++ b/test/golden-results/parse-simple.hs @@ -27,14 +27,7 @@ Module , packageDbs = [] } , comments = - [ PlainTextComment - ( SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/Simple.hs" 7 1 8 3 - , srcInfoPoints = [] - } - , [ " hello world\n" ] - ) - , CodeBlockComment + [ CodeBlockComment (VerifiedExample ( SrcSpanInfo { srcInfoSpan = SrcSpan "test/assets/Simple.hs" 9 1 10 11 @@ -42,13 +35,6 @@ Module } , [ "test" , "==> 1" ] )) - , PlainTextComment - ( SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/Simple.hs" 11 1 11 3 - , srcInfoPoints = [] - } - , [ "" ] - ) , CodeBlockComment (VerifiedExample ( SrcSpanInfo @@ -57,13 +43,6 @@ Module } , [ "test + test" , "==> 2" ] )) - , PlainTextComment - ( SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/Simple.hs" 14 1 14 3 - , srcInfoPoints = [] - } - , [ "" ] - ) , CodeBlockComment (UnverifiedExample ( SrcSpanInfo diff --git a/test/golden-results/parse-unverified-examples.hs b/test/golden-results/parse-unverified-examples.hs index 1b51dff..43f35f6 100644 --- a/test/golden-results/parse-unverified-examples.hs +++ b/test/golden-results/parse-unverified-examples.hs @@ -28,14 +28,7 @@ Module , packageDbs = [] } , comments = - [ PlainTextComment - ( SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/UnverifiedExamples.hs" 7 1 8 3 - , srcInfoPoints = [] - } - , [ " hello world\n" ] - ) - , CodeBlockComment + [ CodeBlockComment (VerifiedExample ( SrcSpanInfo { srcInfoSpan = @@ -44,14 +37,6 @@ Module } , [ "test" , "==> 1" ] )) - , PlainTextComment - ( SrcSpanInfo - { srcInfoSpan = - SrcSpan "test/assets/UnverifiedExamples.hs" 11 1 11 3 - , srcInfoPoints = [] - } - , [ "" ] - ) , CodeBlockComment (UnverifiedExample ( SrcSpanInfo @@ -61,14 +46,6 @@ Module } , [ "test" ] )) - , PlainTextComment - ( SrcSpanInfo - { srcInfoSpan = - SrcSpan "test/assets/UnverifiedExamples.hs" 13 1 13 3 - , srcInfoPoints = [] - } - , [ "" ] - ) , CodeBlockComment (VerifiedExample ( SrcSpanInfo @@ -78,14 +55,6 @@ Module } , [ "test + test" , "==> 3" ] )) - , PlainTextComment - ( SrcSpanInfo - { srcInfoSpan = - SrcSpan "test/assets/UnverifiedExamples.hs" 18 1 19 3 - , srcInfoPoints = [] - } - , [ " | more stuff\n" ] - ) , CodeBlockComment (VerifiedExample ( SrcSpanInfo @@ -101,14 +70,6 @@ Module , "==> [ 2, 4, 5 ]" ] )) - , PlainTextComment - ( SrcSpanInfo - { srcInfoSpan = - SrcSpan "test/assets/UnverifiedExamples.hs" 27 1 28 3 - , srcInfoPoints = [] - } - , [ " | compilation fails\n" ] - ) , CodeBlockComment (VerifiedExample ( SrcSpanInfo diff --git a/test/golden-results/parse-with-context.hs b/test/golden-results/parse-with-context.hs index cc1fa90..59fa662 100644 --- a/test/golden-results/parse-with-context.hs +++ b/test/golden-results/parse-with-context.hs @@ -29,27 +29,13 @@ Module , packageDbs = [] } , comments = - [ PlainTextComment - ( SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 8 1 9 3 - , srcInfoPoints = [] - } - , [ " TypeApplications\n" ] - ) - , ContextBlockComment + [ ContextBlockComment ( SrcSpanInfo { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 10 1 13 5 , srcInfoPoints = [] } , [ "result :: Maybe [Char]" , "result = Just \"a\"" ] ) - , PlainTextComment - ( SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 14 1 14 3 - , srcInfoPoints = [] - } - , [ "" ] - ) , CodeBlockComment (VerifiedExample ( SrcSpanInfo From 350814e88e26a2f7d645512923069df3a5f23ad8 Mon Sep 17 00:00:00 2001 From: Stoeffel Date: Mon, 20 Sep 2021 11:50:36 +0200 Subject: [PATCH 09/17] More cleanup --- src/Haskell/Verified/Examples.hs | 38 ++++++++++++++++++++++---------- 1 file changed, 26 insertions(+), 12 deletions(-) diff --git a/src/Haskell/Verified/Examples.hs b/src/Haskell/Verified/Examples.hs index d7f7201..f5b98e5 100644 --- a/src/Haskell/Verified/Examples.hs +++ b/src/Haskell/Verified/Examples.hs @@ -247,23 +247,22 @@ toComments cs = cs |> mergeComments [] False |> List.filterMap - ( \(ct, (LHE.Comments.Comment _ srcSpan val)) -> + ( \(ct, comments) -> case ct of PlainText -> Nothing CodeBlock -> - val - |> Prelude.lines - |> List.map (Prelude.dropWhile (/= '>') >> Prelude.drop 2) - |> toExample (LHE.SrcLoc.noInfoSpan srcSpan) + comments + |> List.map (commentValue >> Prelude.dropWhile (/= '>') >> Prelude.drop 2) + |> toExample (LHE.SrcLoc.noInfoSpan (mergeSrcSpans comments)) |> CodeBlockComment |> Just ContextBlock -> - val - |> Prelude.lines + comments + |> List.map commentValue |> Data.List.tail |> Data.List.init |> List.map (Prelude.drop 1) - |> (,) (LHE.SrcLoc.noInfoSpan srcSpan) + |> (,) (LHE.SrcLoc.noInfoSpan (mergeSrcSpans comments)) |> ContextBlockComment |> Just ) @@ -271,17 +270,21 @@ toComments cs = data CommentType = CodeBlock | PlainText | ContextBlock deriving (Show, Eq) -mergeComments :: List (CommentType, LHE.Comments.Comment) -> Bool -> List LHE.Comments.Comment -> List (CommentType, LHE.Comments.Comment) +mergeComments :: + List (CommentType, List LHE.Comments.Comment) -> + Bool -> + List LHE.Comments.Comment -> + List (CommentType, List LHE.Comments.Comment) mergeComments acc _ [] = List.reverse acc mergeComments acc isInContext (next : restNext) = let nextCt = commentType next stillInContext = if isInContext then nextCt /= ContextBlock else nextCt == ContextBlock newAcc = case acc of - [] -> [(nextCt, next)] + [] -> [(nextCt, [next])] (prevCt, prev) : restPrev -> if isInContext || prevCt == nextCt - then (prevCt, concatComment prev next) : restPrev - else (nextCt, next) : acc + then (prevCt, prev ++ [next]) : restPrev + else (nextCt, [next]) : acc in mergeComments newAcc stillInContext restNext commentType :: LHE.Comments.Comment -> CommentType @@ -303,6 +306,17 @@ concatComment :: LHE.Comments.Comment -> LHE.Comments.Comment -> LHE.Comments.Co concatComment commentA@(LHE.Comments.Comment _ srcSpanA a) commentB@(LHE.Comments.Comment _ srcSpanB b) = LHE.Comments.Comment True (LHE.SrcLoc.mergeSrcSpan srcSpanA srcSpanB) (a ++ "\n" ++ b) +commentValue :: LHE.Comments.Comment -> Prelude.String +commentValue (LHE.Comments.Comment _ _ a) = a + +mergeSrcSpans :: List LHE.Comments.Comment -> LHE.SrcLoc.SrcSpan +mergeSrcSpans [] = LHE.SrcLoc.mkSrcSpan LHE.SrcLoc.noLoc LHE.SrcLoc.noLoc +mergeSrcSpans (LHE.Comments.Comment _ first _ : rest) = + List.foldl + (\(LHE.Comments.Comment _ srcSpan _) acc -> LHE.SrcLoc.mergeSrcSpan acc srcSpan) + first + rest + toExample :: LHE.SrcLoc.SrcSpanInfo -> List Prelude.String -> Example toExample srcLocInfo source = case LHE.Lexer.lexTokenStream (Prelude.unlines source) of From 5b4afe41a690ca7424f4bbcc427363f3558043d1 Mon Sep 17 00:00:00 2001 From: Stoeffel Date: Mon, 20 Sep 2021 12:14:12 +0200 Subject: [PATCH 10/17] Cleanup src spans --- src/Haskell/Verified/Examples.hs | 30 +++++----- src/Haskell/Verified/Examples/Internal.hs | 10 ++-- test/golden-results/parse-simple.hs | 22 ++----- .../parse-unverified-examples.hs | 57 ++++++------------- test/golden-results/parse-with-context.hs | 16 ++---- .../verifyExample-multiline-unverified.hs | 28 ++++----- .../verifyExample-multiline-verified.hs | 28 ++++----- .../verifyExample-unverified.hs | 7 +-- test/golden-results/verifyExample-verified.hs | 7 +-- 9 files changed, 71 insertions(+), 134 deletions(-) diff --git a/src/Haskell/Verified/Examples.hs b/src/Haskell/Verified/Examples.hs index f5b98e5..5145025 100644 --- a/src/Haskell/Verified/Examples.hs +++ b/src/Haskell/Verified/Examples.hs @@ -50,7 +50,7 @@ verify mod = verifyExample :: ModuleInfo -> Example -> Prelude.IO ExampleResult verifyExample modInfo example = case example of - VerifiedExample (_, code) -> do + VerifiedExample _ code -> do result <- eval modInfo (Prelude.unlines code) case result of Prelude.Left err -> @@ -58,7 +58,7 @@ verifyExample modInfo example = Prelude.Right execResult -> ExampleVerifySuccess example execResult |> Prelude.pure - UnverifiedExample (_, code) -> + UnverifiedExample _ code -> NoExampleResult |> ExampleVerifySuccess example |> Prelude.pure @@ -169,7 +169,7 @@ getPackageDbs options = List.concat [[l, r] | (l, r) <- Prelude.zip options (Lis exampleFromText :: Prelude.String -> Example exampleFromText val = - toExample LHE.SrcLoc.noSrcSpan (Prelude.lines val) + toExample emptySrcSpan (Prelude.lines val) parse :: Prelude.FilePath -> Prelude.IO Module parse path = do @@ -211,7 +211,7 @@ examples = List.filterMap ( \c -> case c of - ContextBlockComment _ -> Nothing + ContextBlockComment _ _ -> Nothing CodeBlockComment example -> Just example ) @@ -253,7 +253,7 @@ toComments cs = CodeBlock -> comments |> List.map (commentValue >> Prelude.dropWhile (/= '>') >> Prelude.drop 2) - |> toExample (LHE.SrcLoc.noInfoSpan (mergeSrcSpans comments)) + |> toExample (commentsSrcSpan comments) |> CodeBlockComment |> Just ContextBlock -> @@ -262,8 +262,7 @@ toComments cs = |> Data.List.tail |> Data.List.init |> List.map (Prelude.drop 1) - |> (,) (LHE.SrcLoc.noInfoSpan (mergeSrcSpans comments)) - |> ContextBlockComment + |> ContextBlockComment (commentsSrcSpan comments) |> Just ) @@ -309,21 +308,24 @@ concatComment commentA@(LHE.Comments.Comment _ srcSpanA a) commentB@(LHE.Comment commentValue :: LHE.Comments.Comment -> Prelude.String commentValue (LHE.Comments.Comment _ _ a) = a -mergeSrcSpans :: List LHE.Comments.Comment -> LHE.SrcLoc.SrcSpan -mergeSrcSpans [] = LHE.SrcLoc.mkSrcSpan LHE.SrcLoc.noLoc LHE.SrcLoc.noLoc -mergeSrcSpans (LHE.Comments.Comment _ first _ : rest) = +commentsSrcSpan :: List LHE.Comments.Comment -> LHE.SrcLoc.SrcSpan +commentsSrcSpan [] = emptySrcSpan +commentsSrcSpan (LHE.Comments.Comment _ first _ : rest) = List.foldl (\(LHE.Comments.Comment _ srcSpan _) acc -> LHE.SrcLoc.mergeSrcSpan acc srcSpan) first rest -toExample :: LHE.SrcLoc.SrcSpanInfo -> List Prelude.String -> Example -toExample srcLocInfo source = +emptySrcSpan :: LHE.SrcLoc.SrcSpan +emptySrcSpan = LHE.SrcLoc.mkSrcSpan LHE.SrcLoc.noLoc LHE.SrcLoc.noLoc + +toExample :: LHE.SrcLoc.SrcSpan -> List Prelude.String -> Example +toExample srcSpan source = case LHE.Lexer.lexTokenStream (Prelude.unlines source) of LHE.Parser.ParseOk tokens -> if Foldable.any ((== LHE.Lexer.VarSym "==>") << LHE.Lexer.unLoc) tokens - then VerifiedExample (srcLocInfo, source) - else UnverifiedExample (srcLocInfo, source) + then VerifiedExample srcSpan source + else UnverifiedExample srcSpan source LHE.Parser.ParseFailed _ msg -> let _ = Debug.log "msg" msg in Debug.todo "TODO" diff --git a/src/Haskell/Verified/Examples/Internal.hs b/src/Haskell/Verified/Examples/Internal.hs index 22124ee..9927cfa 100644 --- a/src/Haskell/Verified/Examples/Internal.hs +++ b/src/Haskell/Verified/Examples/Internal.hs @@ -39,17 +39,17 @@ data ModuleInfo = ModuleInfo data Comment = CodeBlockComment Example - | ContextBlockComment (LHE.SrcLoc.SrcSpanInfo, List Prelude.String) + | ContextBlockComment LHE.SrcLoc.SrcSpan (List Prelude.String) deriving (Show, Eq) data Example - = VerifiedExample (LHE.SrcLoc.SrcSpanInfo, List Prelude.String) - | UnverifiedExample (LHE.SrcLoc.SrcSpanInfo, List Prelude.String) + = VerifiedExample LHE.SrcLoc.SrcSpan (List Prelude.String) + | UnverifiedExample LHE.SrcLoc.SrcSpan (List Prelude.String) deriving (Show, Eq) exampleSrcSpan :: Example -> LHE.SrcLoc.SrcSpan -exampleSrcSpan (VerifiedExample (info, _)) = LHE.SrcLoc.srcInfoSpan info -exampleSrcSpan (UnverifiedExample (info, _)) = LHE.SrcLoc.srcInfoSpan info +exampleSrcSpan (VerifiedExample span _) = span +exampleSrcSpan (UnverifiedExample span _) = span data ExampleResult = ExampleVerifySuccess Example Verified diff --git a/test/golden-results/parse-simple.hs b/test/golden-results/parse-simple.hs index a1d1011..82b2962 100644 --- a/test/golden-results/parse-simple.hs +++ b/test/golden-results/parse-simple.hs @@ -29,27 +29,13 @@ Module , comments = [ CodeBlockComment (VerifiedExample - ( SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/Simple.hs" 9 1 10 11 - , srcInfoPoints = [] - } - , [ "test" , "==> 1" ] - )) + (SrcSpan "test/assets/Simple.hs" 9 1 10 11) [ "test" , "==> 1" ]) , CodeBlockComment (VerifiedExample - ( SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/Simple.hs" 12 1 13 11 - , srcInfoPoints = [] - } - , [ "test + test" , "==> 2" ] - )) + (SrcSpan "test/assets/Simple.hs" 12 1 13 11) + [ "test + test" , "==> 2" ]) , CodeBlockComment (UnverifiedExample - ( SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/Simple.hs" 15 1 15 17 - , srcInfoPoints = [] - } - , [ "test + test" ] - )) + (SrcSpan "test/assets/Simple.hs" 15 1 15 17) [ "test + test" ]) ] } \ No newline at end of file diff --git a/test/golden-results/parse-unverified-examples.hs b/test/golden-results/parse-unverified-examples.hs index 43f35f6..52d1ea9 100644 --- a/test/golden-results/parse-unverified-examples.hs +++ b/test/golden-results/parse-unverified-examples.hs @@ -30,54 +30,29 @@ Module , comments = [ CodeBlockComment (VerifiedExample - ( SrcSpanInfo - { srcInfoSpan = - SrcSpan "test/assets/UnverifiedExamples.hs" 9 1 10 11 - , srcInfoPoints = [] - } - , [ "test" , "==> 1" ] - )) + (SrcSpan "test/assets/UnverifiedExamples.hs" 9 1 10 11) + [ "test" , "==> 1" ]) , CodeBlockComment (UnverifiedExample - ( SrcSpanInfo - { srcInfoSpan = - SrcSpan "test/assets/UnverifiedExamples.hs" 12 1 12 10 - , srcInfoPoints = [] - } - , [ "test" ] - )) + (SrcSpan "test/assets/UnverifiedExamples.hs" 12 1 12 10) + [ "test" ]) , CodeBlockComment (VerifiedExample - ( SrcSpanInfo - { srcInfoSpan = - SrcSpan "test/assets/UnverifiedExamples.hs" 14 1 15 11 - , srcInfoPoints = [] - } - , [ "test + test" , "==> 3" ] - )) + (SrcSpan "test/assets/UnverifiedExamples.hs" 14 1 15 11) + [ "test + test" , "==> 3" ]) , CodeBlockComment (VerifiedExample - ( SrcSpanInfo - { srcInfoSpan = - SrcSpan "test/assets/UnverifiedExamples.hs" 20 1 25 21 - , srcInfoPoints = [] - } - , [ "[ 1" - , ", 2" - , ", 3" - , ", 4" - , "] |> map (+ 1)" - , "==> [ 2, 4, 5 ]" - ] - )) + (SrcSpan "test/assets/UnverifiedExamples.hs" 20 1 25 21) + [ "[ 1" + , ", 2" + , ", 3" + , ", 4" + , "] |> map (+ 1)" + , "==> [ 2, 4, 5 ]" + ]) , CodeBlockComment (VerifiedExample - ( SrcSpanInfo - { srcInfoSpan = - SrcSpan "test/assets/UnverifiedExamples.hs" 29 1 34 14 - , srcInfoPoints = [] - } - , [ "[ 1" , ", 2" , ", 3" , ", 4" , "] |> map (+ 1)" , "==> True" ] - )) + (SrcSpan "test/assets/UnverifiedExamples.hs" 29 1 34 14) + [ "[ 1" , ", 2" , ", 3" , ", 4" , "] |> map (+ 1)" , "==> True" ]) ] } \ No newline at end of file diff --git a/test/golden-results/parse-with-context.hs b/test/golden-results/parse-with-context.hs index 59fa662..bf61109 100644 --- a/test/golden-results/parse-with-context.hs +++ b/test/golden-results/parse-with-context.hs @@ -30,19 +30,11 @@ Module } , comments = [ ContextBlockComment - ( SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 10 1 13 5 - , srcInfoPoints = [] - } - , [ "result :: Maybe [Char]" , "result = Just \"a\"" ] - ) + (SrcSpan "test/assets/WithContext.hs" 10 1 13 5) + [ "result :: Maybe [Char]" , "result = Just \"a\"" ] , CodeBlockComment (VerifiedExample - ( SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 15 1 15 46 - , srcInfoPoints = [] - } - , [ "identity @(Maybe [Char]) test ==> result" ] - )) + (SrcSpan "test/assets/WithContext.hs" 15 1 15 46) + [ "identity @(Maybe [Char]) test ==> result" ]) ] } \ No newline at end of file diff --git a/test/golden-results/verifyExample-multiline-unverified.hs b/test/golden-results/verifyExample-multiline-unverified.hs index f3afaee..fcd672f 100644 --- a/test/golden-results/verifyExample-multiline-unverified.hs +++ b/test/golden-results/verifyExample-multiline-unverified.hs @@ -1,19 +1,15 @@ ExampleVerifySuccess (VerifiedExample - ( SrcSpanInfo - { srcInfoSpan = SrcSpan "" (-1) (-1) (-1) (-1) - , srcInfoPoints = [] - } - , [ "[ 1" - , ", 2" - , ", 3" - , "]" - , "|> List.map (+ 1)" - , "==>" - , "[ 2" - , ", 3" - , ", 5" - , "]" - ] - )) + (SrcSpan "" (-1) (-1) (-1) (-1)) + [ "[ 1" + , ", 2" + , ", 3" + , "]" + , "|> List.map (+ 1)" + , "==>" + , "[ 2" + , ", 3" + , ", 5" + , "]" + ]) (Unverified "[2,3,4]" "[2,3,5]") \ No newline at end of file diff --git a/test/golden-results/verifyExample-multiline-verified.hs b/test/golden-results/verifyExample-multiline-verified.hs index fefa33e..837f45c 100644 --- a/test/golden-results/verifyExample-multiline-verified.hs +++ b/test/golden-results/verifyExample-multiline-verified.hs @@ -1,19 +1,15 @@ ExampleVerifySuccess (VerifiedExample - ( SrcSpanInfo - { srcInfoSpan = SrcSpan "" (-1) (-1) (-1) (-1) - , srcInfoPoints = [] - } - , [ "[ 1" - , ", 2" - , ", 3" - , "]" - , "|> List.map (+ 1)" - , "==>" - , "[ 2" - , ", 3" - , ", 4" - , "]" - ] - )) + (SrcSpan "" (-1) (-1) (-1) (-1)) + [ "[ 1" + , ", 2" + , ", 3" + , "]" + , "|> List.map (+ 1)" + , "==>" + , "[ 2" + , ", 3" + , ", 4" + , "]" + ]) Verified \ No newline at end of file diff --git a/test/golden-results/verifyExample-unverified.hs b/test/golden-results/verifyExample-unverified.hs index bb4f990..6ea5be3 100644 --- a/test/golden-results/verifyExample-unverified.hs +++ b/test/golden-results/verifyExample-unverified.hs @@ -1,9 +1,4 @@ ExampleVerifySuccess (VerifiedExample - ( SrcSpanInfo - { srcInfoSpan = SrcSpan "" (-1) (-1) (-1) (-1) - , srcInfoPoints = [] - } - , [ "1 + 1 ==> 3" ] - )) + (SrcSpan "" (-1) (-1) (-1) (-1)) [ "1 + 1 ==> 3" ]) (Unverified "2" "3") \ No newline at end of file diff --git a/test/golden-results/verifyExample-verified.hs b/test/golden-results/verifyExample-verified.hs index fe61fa1..eb195f9 100644 --- a/test/golden-results/verifyExample-verified.hs +++ b/test/golden-results/verifyExample-verified.hs @@ -1,9 +1,4 @@ ExampleVerifySuccess (VerifiedExample - ( SrcSpanInfo - { srcInfoSpan = SrcSpan "" (-1) (-1) (-1) (-1) - , srcInfoPoints = [] - } - , [ "1 + 1 ==> 2" ] - )) + (SrcSpan "" (-1) (-1) (-1) (-1)) [ "1 + 1 ==> 2" ]) Verified \ No newline at end of file From 739f3875c1488a3a4dc9e0917959569ca0e4b255 Mon Sep 17 00:00:00 2001 From: Stoeffel Date: Tue, 21 Sep 2021 13:40:25 +0200 Subject: [PATCH 11/17] Load context module when there are context blocks --- src/Haskell/Verified/Examples.hs | 93 ++++++++++++++++++----- test/Main.hs | 4 + test/assets/WithContext.hs | 4 + test/golden-results/integration-simple.hs | 41 +++++----- test/golden-results/parse-with-context.hs | 24 ++++-- 5 files changed, 120 insertions(+), 46 deletions(-) diff --git a/src/Haskell/Verified/Examples.hs b/src/Haskell/Verified/Examples.hs index 5145025..e301641 100644 --- a/src/Haskell/Verified/Examples.hs +++ b/src/Haskell/Verified/Examples.hs @@ -19,6 +19,7 @@ where import qualified Control.Concurrent.Async as Async import qualified Data.Foldable as Foldable import qualified Data.List +import qualified Data.Text.IO import qualified HIE.Bios.Cradle import qualified HIE.Bios.Environment import qualified HIE.Bios.Flags @@ -42,16 +43,17 @@ import qualified Prelude verify :: Module -> Prelude.IO (List ExampleResult) verify mod = - mod - |> comments - |> examples - |> Prelude.traverse (verifyExample (moduleInfo mod)) - -verifyExample :: ModuleInfo -> Example -> Prelude.IO ExampleResult -verifyExample modInfo example = + withContext (comments mod) <| \maybeContext -> + mod + |> comments + |> examples + |> Prelude.traverse (verifyExample (moduleInfo mod) maybeContext) + +verifyExample :: ModuleInfo -> Maybe Context -> Example -> Prelude.IO ExampleResult +verifyExample modInfo maybeContext example = case example of VerifiedExample _ code -> do - result <- eval modInfo (Prelude.unlines code) + result <- eval modInfo (Prelude.unlines code) maybeContext case result of Prelude.Left err -> Prelude.pure (ExampleVerifyFailed example err) @@ -118,8 +120,12 @@ makeImport importDecl = importToString (LHE.Syntax.IThingAll _ n) = getName n ++ "(..)" importToString (LHE.Syntax.IThingWith _ n ns) = getName n ++ "(" ++ (List.concat <| List.intersperse "," (List.map getCName ns)) ++ ")" -eval :: ModuleInfo -> Prelude.String -> Prelude.IO (Prelude.Either Hint.InterpreterError Verified) -eval moduleInfo s = do +eval :: + ModuleInfo -> + Prelude.String -> + Maybe Context -> + Prelude.IO (Prelude.Either Hint.InterpreterError Verified) +eval moduleInfo s maybeContext = do let modulePath = moduleFilePath moduleInfo let interpreter = case packageDbs moduleInfo of [] -> Hint.runInterpreter @@ -133,22 +139,28 @@ eval moduleInfo s = do let searchPaths = List.map Text.toList <| importPaths moduleInfo Hint.set [Hint.languageExtensions Hint.:= langs, Hint.searchPath Hint.:= searchPaths] - Hint.loadModules - ( if modulePath == "" - then preload - else modulePath : preload - ) + [ if modulePath == "" + then [] + else [modulePath], + case maybeContext of + Nothing -> [] + Just Context {contextModulePath} -> [contextModulePath], + preload + ] + |> List.concat + |> Hint.loadModules case moduleName moduleInfo of Just name -> Hint.setTopLevelModules [Text.toList name] Nothing -> Prelude.return () let exampleImports = - List.map - makeSimpleImport - [ "Haskell.Verified.Examples.RunTime", - "Haskell.Verified.Examples.Verified" - ] + [ Just "Haskell.Verified.Examples.RunTime", + Just "Haskell.Verified.Examples.Verified", + Maybe.map contextModuleName maybeContext + ] + |> List.filterMap identity + |> List.map makeSimpleImport Hint.setImportsF (exampleImports ++ imports moduleInfo) Hint.interpret s (Hint.as :: Verified) @@ -215,6 +227,36 @@ examples = CodeBlockComment example -> Just example ) +contextBlocks :: List Comment -> List Prelude.String +contextBlocks = + List.concatMap + ( \c -> + case c of + ContextBlockComment _ context -> context + CodeBlockComment _ -> [] + ) + +data Context = Context + { contextModulePath :: Prelude.FilePath, + contextModuleName :: Text + } + +withContext :: List Comment -> (Maybe Context -> Prelude.IO a) -> Prelude.IO a +withContext comments go = do + let contextModuleName = "HaskellVerifiedExamplesContext" + case contextBlocks comments of + [] -> go Nothing + xs -> + withTempFile + ( \path handle -> do + System.IO.hPutStrLn handle ("module " ++ Text.toList contextModuleName ++ " where") + xs + |> Prelude.unlines + |> System.IO.hPutStr handle + Prelude.pure () + ) + (\contextModulePath -> go (Just Context {contextModulePath, contextModuleName})) + toModule :: ( LHE.Syntax.Module LHE.SrcLoc.SrcSpanInfo, List LHE.Comments.Comment @@ -356,3 +398,14 @@ report reporters results = ] |> List.filterMap identity |> Async.mapConcurrently_ identity + +withTempFile :: + (System.IO.FilePath -> System.IO.Handle -> Prelude.IO ()) -> + (Prelude.FilePath -> Prelude.IO a) -> + Prelude.IO a +withTempFile before go = do + (path, handle) <- + System.IO.openTempFile "/tmp" "HaskellVerifiedExamples.hs" + _ <- before path handle + System.IO.hClose handle + go path diff --git a/test/Main.hs b/test/Main.hs index 544aef9..96b0fe3 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -50,6 +50,7 @@ tests = example |> HVE.verifyExample (HVE.shimModuleWithImports ["NriPrelude"]) + Nothing |> Expect.fromIO result |> Debug.toString @@ -60,6 +61,7 @@ tests = example |> HVE.verifyExample (HVE.shimModuleWithImports ["NriPrelude"]) + Nothing |> Expect.fromIO result |> Debug.toString @@ -84,6 +86,7 @@ tests = example |> HVE.verifyExample (HVE.shimModuleWithImports ["List", "NriPrelude"]) + Nothing |> Expect.fromIO result |> Debug.toString @@ -107,6 +110,7 @@ tests = example |> HVE.verifyExample (HVE.shimModuleWithImports ["List", "NriPrelude"]) + Nothing |> Expect.fromIO result |> Debug.toString diff --git a/test/assets/WithContext.hs b/test/assets/WithContext.hs index 85bc8db..807d3af 100644 --- a/test/assets/WithContext.hs +++ b/test/assets/WithContext.hs @@ -8,10 +8,14 @@ import NriPrelude -- TypeApplications -- -- @ +-- import NriPrelude +-- -- result :: Maybe [Char] -- result = Just "a" -- @ -- -- > identity @(Maybe [Char]) test ==> result +-- +-- > Just "b" ==> result test :: Maybe [Char] test = Just "a" diff --git a/test/golden-results/integration-simple.hs b/test/golden-results/integration-simple.hs index 398e676..627f126 100644 --- a/test/golden-results/integration-simple.hs +++ b/test/golden-results/integration-simple.hs @@ -93,19 +93,24 @@ test/assets/UnverifiedExamples.hs:29 Examples of module WithContext unverified. -test/assets/WithContext.hs:15 - 10: -- @ - 11: -- result :: Maybe [Char] - 12: -- result = Just "a" - 13: -- @ - 14: -- -✗ 15: -- > identity @(Maybe [Char]) test ==> result - 16: test :: Maybe [Char] - 17: test = Just "a" - 18: -The example doesn't compile: -:2:35: error: - Variable not in scope: result :: Maybe [Char] +test/assets/WithContext.hs:19 + 14: -- result = Just "a" + 15: -- @ + 16: -- + 17: -- > identity @(Maybe [Char]) test ==> result + 18: -- +✗ 19: -- > Just "b" ==> result + 20: test :: Maybe [Char] + 21: test = Just "a" + 22: +The example was incorrect and couldn't be verified. + ▼ +"Just \"b\"" +╷ +│ ==> +╵ +"Just \"a\"" + ▲ Examples unverified. @@ -125,16 +130,16 @@ test/assets/Headless.hs:3 ▲ Not all examples verified! -Verified: 14 -Unverified: 3 +Verified: 15 +Unverified: 4 In these files: * test/assets/Headless.hs * test/assets/UnverifiedExamples.hs + * test/assets/WithContext.hs No examples: 2 In these files: * test/assets/Simple.hs * test/assets/UnverifiedExamples.hs -Evaluation failed: 2 +Evaluation failed: 1 In these files: - * test/assets/UnverifiedExamples.hs - * test/assets/WithContext.hs \ No newline at end of file + * test/assets/UnverifiedExamples.hs \ No newline at end of file diff --git a/test/golden-results/parse-with-context.hs b/test/golden-results/parse-with-context.hs index bf61109..80c1d27 100644 --- a/test/golden-results/parse-with-context.hs +++ b/test/golden-results/parse-with-context.hs @@ -4,17 +4,17 @@ Module { moduleName = Just "WithContext" , moduleSource = SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 1 1 18 1 + { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 1 1 22 1 , srcInfoPoints = [ SrcSpan "test/assets/WithContext.hs" 1 1 1 1 , SrcSpan "test/assets/WithContext.hs" 2 1 2 1 , SrcSpan "test/assets/WithContext.hs" 4 1 4 1 , SrcSpan "test/assets/WithContext.hs" 4 1 4 1 , SrcSpan "test/assets/WithContext.hs" 6 1 6 1 - , SrcSpan "test/assets/WithContext.hs" 16 1 16 1 - , SrcSpan "test/assets/WithContext.hs" 17 1 17 1 - , SrcSpan "test/assets/WithContext.hs" 18 1 18 1 - , SrcSpan "test/assets/WithContext.hs" 18 1 18 1 + , SrcSpan "test/assets/WithContext.hs" 20 1 20 1 + , SrcSpan "test/assets/WithContext.hs" 21 1 21 1 + , SrcSpan "test/assets/WithContext.hs" 22 1 22 1 + , SrcSpan "test/assets/WithContext.hs" 22 1 22 1 ] } , languageExtensions = [ "TypeApplications" , "NoImplicitPrelude" ] @@ -30,11 +30,19 @@ Module } , comments = [ ContextBlockComment - (SrcSpan "test/assets/WithContext.hs" 10 1 13 5) - [ "result :: Maybe [Char]" , "result = Just \"a\"" ] + (SrcSpan "test/assets/WithContext.hs" 10 1 15 5) + [ "import NriPrelude" + , "" + , "result :: Maybe [Char]" + , "result = Just \"a\"" + ] , CodeBlockComment (VerifiedExample - (SrcSpan "test/assets/WithContext.hs" 15 1 15 46) + (SrcSpan "test/assets/WithContext.hs" 17 1 17 46) [ "identity @(Maybe [Char]) test ==> result" ]) + , CodeBlockComment + (VerifiedExample + (SrcSpan "test/assets/WithContext.hs" 19 1 19 25) + [ "Just \"b\" ==> result" ]) ] } \ No newline at end of file From 308a83bd2196a01a6190ccd1124da10187865ed0 Mon Sep 17 00:00:00 2001 From: Stoeffel Date: Tue, 21 Sep 2021 17:06:33 +0200 Subject: [PATCH 12/17] Cleanup --- src/Haskell/Verified/Examples.hs | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/src/Haskell/Verified/Examples.hs b/src/Haskell/Verified/Examples.hs index e301641..dbc8e82 100644 --- a/src/Haskell/Verified/Examples.hs +++ b/src/Haskell/Verified/Examples.hs @@ -42,18 +42,19 @@ import qualified Text.Read import qualified Prelude verify :: Module -> Prelude.IO (List ExampleResult) -verify mod = - withContext (comments mod) <| \maybeContext -> - mod - |> comments +verify Module {comments, moduleInfo} = + withContext comments <| \maybeContext -> + comments |> examples - |> Prelude.traverse (verifyExample (moduleInfo mod) maybeContext) + |> Prelude.traverse (verifyExample moduleInfo maybeContext) verifyExample :: ModuleInfo -> Maybe Context -> Example -> Prelude.IO ExampleResult verifyExample modInfo maybeContext example = case example of VerifiedExample _ code -> do - result <- eval modInfo (Prelude.unlines code) maybeContext + result <- + Prelude.unlines code + |> eval modInfo maybeContext case result of Prelude.Left err -> Prelude.pure (ExampleVerifyFailed example err) @@ -122,10 +123,10 @@ makeImport importDecl = eval :: ModuleInfo -> - Prelude.String -> Maybe Context -> + Prelude.String -> Prelude.IO (Prelude.Either Hint.InterpreterError Verified) -eval moduleInfo s maybeContext = do +eval moduleInfo maybeContext s = do let modulePath = moduleFilePath moduleInfo let interpreter = case packageDbs moduleInfo of [] -> Hint.runInterpreter From a4f90adc775aa69314dfa6b84e7432695bd064c9 Mon Sep 17 00:00:00 2001 From: Stoeffel Date: Tue, 21 Sep 2021 17:27:04 +0200 Subject: [PATCH 13/17] Implicit imports --- src/Haskell/Verified/Examples.hs | 28 +++++++++++++++++++---- test/assets/WithContext.hs | 8 ++++--- test/golden-results/integration-simple.hs | 18 +++++++-------- test/golden-results/parse-with-context.hs | 20 +++++++--------- 4 files changed, 46 insertions(+), 28 deletions(-) diff --git a/src/Haskell/Verified/Examples.hs b/src/Haskell/Verified/Examples.hs index dbc8e82..0651b16 100644 --- a/src/Haskell/Verified/Examples.hs +++ b/src/Haskell/Verified/Examples.hs @@ -43,7 +43,7 @@ import qualified Prelude verify :: Module -> Prelude.IO (List ExampleResult) verify Module {comments, moduleInfo} = - withContext comments <| \maybeContext -> + withContext moduleInfo comments <| \maybeContext -> comments |> examples |> Prelude.traverse (verifyExample moduleInfo maybeContext) @@ -242,15 +242,20 @@ data Context = Context contextModuleName :: Text } -withContext :: List Comment -> (Maybe Context -> Prelude.IO a) -> Prelude.IO a -withContext comments go = do +withContext :: ModuleInfo -> List Comment -> (Maybe Context -> Prelude.IO a) -> Prelude.IO a +withContext modInfo comments go = do let contextModuleName = "HaskellVerifiedExamplesContext" case contextBlocks comments of [] -> go Nothing xs -> withTempFile ( \path handle -> do - System.IO.hPutStrLn handle ("module " ++ Text.toList contextModuleName ++ " where") + _ <- System.IO.hPutStrLn handle ("module " ++ Text.toList contextModuleName ++ " where") + _ <- + modInfo + |> imports + |> List.map printImport + |> Prelude.traverse (System.IO.hPutStrLn handle) xs |> Prelude.unlines |> System.IO.hPutStr handle @@ -258,6 +263,21 @@ withContext comments go = do ) (\contextModulePath -> go (Just Context {contextModulePath, contextModuleName})) +printImport :: Hint.ModuleImport -> Prelude.String +printImport m = + "import " + ++ ( case Hint.modQual m of + Hint.NotQualified -> Hint.modName m + Hint.ImportAs q -> Hint.modName m ++ " as " ++ q + Hint.QualifiedAs Nothing -> "qualified " ++ Hint.modName m + Hint.QualifiedAs (Just q) -> "qualified " ++ Hint.modName m ++ " as " ++ q + ) + ++ ( case Hint.modImp m of + Hint.NoImportList -> "" + Hint.ImportList l -> " (" ++ Data.List.intercalate "," l ++ ")" + Hint.HidingList l -> " hiding (" ++ Data.List.intercalate "," l ++ ")" + ) + toModule :: ( LHE.Syntax.Module LHE.SrcLoc.SrcSpanInfo, List LHE.Comments.Comment diff --git a/test/assets/WithContext.hs b/test/assets/WithContext.hs index 807d3af..6f93ae1 100644 --- a/test/assets/WithContext.hs +++ b/test/assets/WithContext.hs @@ -5,15 +5,17 @@ module WithContext where import NriPrelude --- TypeApplications +-- | TypeApplications -- --- @ --- import NriPrelude +-- Setup for examples below: -- +-- @ -- result :: Maybe [Char] -- result = Just "a" -- @ -- +-- Examples: +-- -- > identity @(Maybe [Char]) test ==> result -- -- > Just "b" ==> result diff --git a/test/golden-results/integration-simple.hs b/test/golden-results/integration-simple.hs index 627f126..80095be 100644 --- a/test/golden-results/integration-simple.hs +++ b/test/golden-results/integration-simple.hs @@ -93,16 +93,16 @@ test/assets/UnverifiedExamples.hs:29 Examples of module WithContext unverified. -test/assets/WithContext.hs:19 - 14: -- result = Just "a" - 15: -- @ +test/assets/WithContext.hs:17 + 12: -- result = Just "a" + 13: -- @ + 14: -- + 15: -- > identity @(Maybe [Char]) test ==> result  16: -- - 17: -- > identity @(Maybe [Char]) test ==> result - 18: -- -✗ 19: -- > Just "b" ==> result - 20: test :: Maybe [Char] - 21: test = Just "a" - 22: +✗ 17: -- > Just "b" ==> result + 18: test :: Maybe [Char] + 19: test = Just "a" + 20: The example was incorrect and couldn't be verified. ▼ "Just \"b\"" diff --git a/test/golden-results/parse-with-context.hs b/test/golden-results/parse-with-context.hs index 80c1d27..b9a870a 100644 --- a/test/golden-results/parse-with-context.hs +++ b/test/golden-results/parse-with-context.hs @@ -4,17 +4,17 @@ Module { moduleName = Just "WithContext" , moduleSource = SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 1 1 22 1 + { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 1 1 20 1 , srcInfoPoints = [ SrcSpan "test/assets/WithContext.hs" 1 1 1 1 , SrcSpan "test/assets/WithContext.hs" 2 1 2 1 , SrcSpan "test/assets/WithContext.hs" 4 1 4 1 , SrcSpan "test/assets/WithContext.hs" 4 1 4 1 , SrcSpan "test/assets/WithContext.hs" 6 1 6 1 + , SrcSpan "test/assets/WithContext.hs" 18 1 18 1 + , SrcSpan "test/assets/WithContext.hs" 19 1 19 1 + , SrcSpan "test/assets/WithContext.hs" 20 1 20 1 , SrcSpan "test/assets/WithContext.hs" 20 1 20 1 - , SrcSpan "test/assets/WithContext.hs" 21 1 21 1 - , SrcSpan "test/assets/WithContext.hs" 22 1 22 1 - , SrcSpan "test/assets/WithContext.hs" 22 1 22 1 ] } , languageExtensions = [ "TypeApplications" , "NoImplicitPrelude" ] @@ -30,19 +30,15 @@ Module } , comments = [ ContextBlockComment - (SrcSpan "test/assets/WithContext.hs" 10 1 15 5) - [ "import NriPrelude" - , "" - , "result :: Maybe [Char]" - , "result = Just \"a\"" - ] + (SrcSpan "test/assets/WithContext.hs" 10 1 13 5) + [ "result :: Maybe [Char]" , "result = Just \"a\"" ] , CodeBlockComment (VerifiedExample - (SrcSpan "test/assets/WithContext.hs" 17 1 17 46) + (SrcSpan "test/assets/WithContext.hs" 15 1 15 46) [ "identity @(Maybe [Char]) test ==> result" ]) , CodeBlockComment (VerifiedExample - (SrcSpan "test/assets/WithContext.hs" 19 1 19 25) + (SrcSpan "test/assets/WithContext.hs" 17 1 17 25) [ "Just \"b\" ==> result" ]) ] } \ No newline at end of file From 5917e984e4a1b6fa8b81d5d1a74f112b010a1599 Mon Sep 17 00:00:00 2001 From: Stoeffel Date: Tue, 21 Sep 2021 20:23:48 +0200 Subject: [PATCH 14/17] Cleanup print import --- src/Haskell/Verified/Examples.hs | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/src/Haskell/Verified/Examples.hs b/src/Haskell/Verified/Examples.hs index 0651b16..83d00d9 100644 --- a/src/Haskell/Verified/Examples.hs +++ b/src/Haskell/Verified/Examples.hs @@ -254,7 +254,7 @@ withContext modInfo comments go = do _ <- modInfo |> imports - |> List.map printImport + |> List.map renderImport |> Prelude.traverse (System.IO.hPutStrLn handle) xs |> Prelude.unlines @@ -263,20 +263,20 @@ withContext modInfo comments go = do ) (\contextModulePath -> go (Just Context {contextModulePath, contextModuleName})) -printImport :: Hint.ModuleImport -> Prelude.String -printImport m = - "import " - ++ ( case Hint.modQual m of - Hint.NotQualified -> Hint.modName m - Hint.ImportAs q -> Hint.modName m ++ " as " ++ q - Hint.QualifiedAs Nothing -> "qualified " ++ Hint.modName m - Hint.QualifiedAs (Just q) -> "qualified " ++ Hint.modName m ++ " as " ++ q - ) - ++ ( case Hint.modImp m of - Hint.NoImportList -> "" - Hint.ImportList l -> " (" ++ Data.List.intercalate "," l ++ ")" - Hint.HidingList l -> " hiding (" ++ Data.List.intercalate "," l ++ ")" - ) +renderImport :: Hint.ModuleImport -> Prelude.String +renderImport m = + Prelude.concat + [ "import ", + case Hint.modQual m of + Hint.NotQualified -> Hint.modName m + Hint.ImportAs q -> Hint.modName m ++ " as " ++ q + Hint.QualifiedAs Nothing -> "qualified " ++ Hint.modName m + Hint.QualifiedAs (Just q) -> "qualified " ++ Hint.modName m ++ " as " ++ q, + case Hint.modImp m of + Hint.NoImportList -> "" + Hint.ImportList l -> " (" ++ Data.List.intercalate "," l ++ ")" + Hint.HidingList l -> " hiding (" ++ Data.List.intercalate "," l ++ ")" + ] toModule :: ( LHE.Syntax.Module LHE.SrcLoc.SrcSpanInfo, From 79ff04754e680cc1a90828f8ce13b8ff36db4de6 Mon Sep 17 00:00:00 2001 From: Stoeffel Date: Tue, 21 Sep 2021 20:24:11 +0200 Subject: [PATCH 15/17] Update golden results --- test/golden-results/integration-simple.hs | 20 ++++++++++---------- test/golden-results/parse-with-context.hs | 16 ++++++++-------- 2 files changed, 18 insertions(+), 18 deletions(-) diff --git a/test/golden-results/integration-simple.hs b/test/golden-results/integration-simple.hs index 80095be..44c9442 100644 --- a/test/golden-results/integration-simple.hs +++ b/test/golden-results/integration-simple.hs @@ -93,16 +93,16 @@ test/assets/UnverifiedExamples.hs:29 Examples of module WithContext unverified. -test/assets/WithContext.hs:17 - 12: -- result = Just "a" - 13: -- @ - 14: -- - 15: -- > identity @(Maybe [Char]) test ==> result - 16: -- -✗ 17: -- > Just "b" ==> result - 18: test :: Maybe [Char] - 19: test = Just "a" - 20: +test/assets/WithContext.hs:21 + 16: -- + 17: -- Examples: + 18: -- + 19: -- > identity @(Maybe [Char]) test ==> result + 20: -- +✗ 21: -- > Just "b" ==> result + 22: test :: Maybe [Char] + 23: test = Just "a" + 24: The example was incorrect and couldn't be verified. ▼ "Just \"b\"" diff --git a/test/golden-results/parse-with-context.hs b/test/golden-results/parse-with-context.hs index b9a870a..0bfe965 100644 --- a/test/golden-results/parse-with-context.hs +++ b/test/golden-results/parse-with-context.hs @@ -4,17 +4,17 @@ Module { moduleName = Just "WithContext" , moduleSource = SrcSpanInfo - { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 1 1 20 1 + { srcInfoSpan = SrcSpan "test/assets/WithContext.hs" 1 1 24 1 , srcInfoPoints = [ SrcSpan "test/assets/WithContext.hs" 1 1 1 1 , SrcSpan "test/assets/WithContext.hs" 2 1 2 1 , SrcSpan "test/assets/WithContext.hs" 4 1 4 1 , SrcSpan "test/assets/WithContext.hs" 4 1 4 1 , SrcSpan "test/assets/WithContext.hs" 6 1 6 1 - , SrcSpan "test/assets/WithContext.hs" 18 1 18 1 - , SrcSpan "test/assets/WithContext.hs" 19 1 19 1 - , SrcSpan "test/assets/WithContext.hs" 20 1 20 1 - , SrcSpan "test/assets/WithContext.hs" 20 1 20 1 + , SrcSpan "test/assets/WithContext.hs" 22 1 22 1 + , SrcSpan "test/assets/WithContext.hs" 23 1 23 1 + , SrcSpan "test/assets/WithContext.hs" 24 1 24 1 + , SrcSpan "test/assets/WithContext.hs" 24 1 24 1 ] } , languageExtensions = [ "TypeApplications" , "NoImplicitPrelude" ] @@ -30,15 +30,15 @@ Module } , comments = [ ContextBlockComment - (SrcSpan "test/assets/WithContext.hs" 10 1 13 5) + (SrcSpan "test/assets/WithContext.hs" 12 1 15 5) [ "result :: Maybe [Char]" , "result = Just \"a\"" ] , CodeBlockComment (VerifiedExample - (SrcSpan "test/assets/WithContext.hs" 15 1 15 46) + (SrcSpan "test/assets/WithContext.hs" 19 1 19 46) [ "identity @(Maybe [Char]) test ==> result" ]) , CodeBlockComment (VerifiedExample - (SrcSpan "test/assets/WithContext.hs" 17 1 17 25) + (SrcSpan "test/assets/WithContext.hs" 21 1 21 25) [ "Just \"b\" ==> result" ]) ] } \ No newline at end of file From ad7d32a14c6d63d1ea27a428a3026c6f5132a674 Mon Sep 17 00:00:00 2001 From: Stoeffel Date: Wed, 22 Sep 2021 09:18:37 +0200 Subject: [PATCH 16/17] Verify examples concurrently --- src/Haskell/Verified/Examples.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Haskell/Verified/Examples.hs b/src/Haskell/Verified/Examples.hs index 83d00d9..a5353c5 100644 --- a/src/Haskell/Verified/Examples.hs +++ b/src/Haskell/Verified/Examples.hs @@ -46,7 +46,7 @@ verify Module {comments, moduleInfo} = withContext moduleInfo comments <| \maybeContext -> comments |> examples - |> Prelude.traverse (verifyExample moduleInfo maybeContext) + |> Async.mapConcurrently (verifyExample moduleInfo maybeContext) verifyExample :: ModuleInfo -> Maybe Context -> Example -> Prelude.IO ExampleResult verifyExample modInfo maybeContext example = From 0036cbe180e48e2be567a9d3327e74f37b0e6099 Mon Sep 17 00:00:00 2001 From: Stoeffel Date: Wed, 22 Sep 2021 09:26:47 +0200 Subject: [PATCH 17/17] Speed up tests --- test/Main.hs | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/test/Main.hs b/test/Main.hs index 96b0fe3..421c540 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -1,5 +1,6 @@ module Main (main) where +import qualified Control.Concurrent.Async as Async import qualified Data.Text.IO import qualified Expect import qualified Haskell.Verified.Examples as HVE @@ -125,17 +126,13 @@ tests = results <- assets |> List.map ("test/assets/" ++) - |> Prelude.traverse + |> Async.mapConcurrently ( \modulePath -> do - parsed <- - HVE.parse modulePath - |> Expect.fromIO - result <- - parsed - |> HVE.verify - |> Expect.fromIO - Expect.fromResult (Ok (HVE.moduleInfo parsed, result)) + parsed <- HVE.parse modulePath + result <- HVE.verify parsed + Prelude.pure (HVE.moduleInfo parsed, result) ) + |> Expect.fromIO contents <- withTempFile (\handle -> Reporter.Stdout.report handle results) contents