module Dino.Verification where

import Prelude

import Data.Text (Text)
import qualified Data.Text as Text
import Text.PrettyPrint.ANSI.Leijen (Doc)
import qualified Text.PrettyPrint.ANSI.Leijen as PP

import Dino.AST.Diff
import Dino.Interpretation

-- | Check each 'assertEq' assertion by structurally comparing the ASTs of the
-- two expressions
--
-- This limited form of formal verification is useful two ways:
--
-- * It can be used to verify refactorings that don't affect the AST; for
--   example, introducing a meta-level helper function (i.e. a normal Haskell
--   function).
--
-- * When the ASTs do differ, the resulting 'Edit' will show only the parts of
--   the expressions where the difference occurs, which can make it easier to
--   manually verify equivalence.
verifyAssertEqStructurally ::
     CollectAssertions Reified a -> [(Text, Maybe (Edit NumRep))]
verifyAssertEqStructurally :: CollectAssertions Reified a -> [(Text, Maybe (Edit NumRep))]
verifyAssertEqStructurally CollectAssertions Reified a
e =
  [ (Text
lab, AST NumRep -> AST NumRep -> Maybe (Diff (AST NumRep))
forall a. Diffable a => a -> a -> Maybe (Diff a)
diff (Reified a -> AST NumRep
forall a. Reified a -> AST NumRep
unReified Reified a
ref) (Reified a -> AST NumRep
forall a. Reified a -> AST NumRep
unReified Reified a
act))
  | (Text
lab, AssertEq Reified a
ref Reified a
act) <- [(Text, Assertion Reified)]
as
  ]
  where
    as :: [(Text, Assertion Reified)]
as = Fold [(Text, Assertion Reified)] a -> [(Text, Assertion Reified)]
forall e a. Fold e a -> e
fold (Fold [(Text, Assertion Reified)] a -> [(Text, Assertion Reified)])
-> Fold [(Text, Assertion Reified)] a
-> [(Text, Assertion Reified)]
forall a b. (a -> b) -> a -> b
$ (:×:) Reified (Fold [(Text, Assertion Reified)]) a
-> Fold [(Text, Assertion Reified)] a
forall (e1 :: * -> *) (e2 :: * -> *) a. (:×:) e1 e2 a -> e2 a
prodSnd ((:×:) Reified (Fold [(Text, Assertion Reified)]) a
 -> Fold [(Text, Assertion Reified)] a)
-> (:×:) Reified (Fold [(Text, Assertion Reified)]) a
-> Fold [(Text, Assertion Reified)] a
forall a b. (a -> b) -> a -> b
$ (:×:)
  (Fold BindSet) (Reified :×: Fold [(Text, Assertion Reified)]) a
-> (:×:) Reified (Fold [(Text, Assertion Reified)]) a
forall (e1 :: * -> *) (e2 :: * -> *) a. (:×:) e1 e2 a -> e2 a
prodSnd ((:×:)
   (Fold BindSet) (Reified :×: Fold [(Text, Assertion Reified)]) a
 -> (:×:) Reified (Fold [(Text, Assertion Reified)]) a)
-> (:×:)
     (Fold BindSet) (Reified :×: Fold [(Text, Assertion Reified)]) a
-> (:×:) Reified (Fold [(Text, Assertion Reified)]) a
forall a b. (a -> b) -> a -> b
$ Intensional (Reified :×: Fold [(Text, Assertion Reified)]) a
-> (:×:)
     (Fold BindSet) (Reified :×: Fold [(Text, Assertion Reified)]) a
forall (e :: * -> *) a. Intensional e a -> (:×:) (Fold BindSet) e a
unIntensional (Intensional (Reified :×: Fold [(Text, Assertion Reified)]) a
 -> (:×:)
      (Fold BindSet) (Reified :×: Fold [(Text, Assertion Reified)]) a)
-> Intensional (Reified :×: Fold [(Text, Assertion Reified)]) a
-> (:×:)
     (Fold BindSet) (Reified :×: Fold [(Text, Assertion Reified)]) a
forall a b. (a -> b) -> a -> b
$ CollectAssertions Reified a
-> Intensional (Reified :×: Fold [(Text, Assertion Reified)]) a
forall (e :: * -> *) a.
CollectAssertions e a
-> Intensional (e :×: Fold [(Text, Assertion e)]) a
unCollectAssertions CollectAssertions Reified a
e

-- | Present the output of 'verifyAssertEqStructurally' as a list of test cases
-- that either succeed or fail with a diff
presentStructuralVerificationAsDocs :: [(Text, Maybe (Edit NumRep))] -> [Doc]
presentStructuralVerificationAsDocs :: [(Text, Maybe (Edit NumRep))] -> [Doc]
presentStructuralVerificationAsDocs [(Text, Maybe (Edit NumRep))]
as = ((Text, Maybe (Edit NumRep)) -> Doc)
-> [(Text, Maybe (Edit NumRep))] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Maybe (Edit NumRep)) -> Doc
mkCase [(Text, Maybe (Edit NumRep))]
as
  where
    l :: Int
l  = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: ((Text, Maybe (Edit NumRep)) -> Int)
-> [(Text, Maybe (Edit NumRep))] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Text -> Int
Text.length (Text -> Int)
-> ((Text, Maybe (Edit NumRep)) -> Text)
-> (Text, Maybe (Edit NumRep))
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text, Maybe (Edit NumRep)) -> Text
forall a b. (a, b) -> a
fst) [(Text, Maybe (Edit NumRep))]
as)
    l' :: Int
l' = Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
l Int
20

    showLabel :: Text -> [Char]
showLabel Text
lab =
      Text -> [Char]
Text.unpack Text
lab [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
":" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> Char -> [Char]
forall a. Int -> a -> [a]
replicate (Int
l' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Text -> Int
Text.length Text
lab) Char
' '

    mkCase :: (Text, Maybe (Edit NumRep)) -> Doc
mkCase (Text
lab, Maybe (Edit NumRep)
d) =
      [Char] -> Doc
PP.string (Text -> [Char]
showLabel Text
lab) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
PP.space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Maybe (Edit NumRep) -> Doc
forall a. Show a => Maybe (Edit a) -> Doc
diffAsTestResult Maybe (Edit NumRep)
d Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
end
      where
        end :: Doc
end = Doc -> (Edit NumRep -> Doc) -> Maybe (Edit NumRep) -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
forall a. Monoid a => a
mempty (Doc -> Edit NumRep -> Doc
forall a b. a -> b -> a
const (Doc -> Edit NumRep -> Doc) -> Doc -> Edit NumRep -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
forall a. Monoid a => a
mempty Doc -> Doc -> Doc
PP.<$> Doc
forall a. Monoid a => a
mempty) Maybe (Edit NumRep)
d

presentStructuralVerification :: [(Text, Maybe (Edit NumRep))] -> IO ()
presentStructuralVerification :: [(Text, Maybe (Edit NumRep))] -> IO ()
presentStructuralVerification =
  Doc -> IO ()
PP.putDoc (Doc -> IO ())
-> ([(Text, Maybe (Edit NumRep))] -> Doc)
-> [(Text, Maybe (Edit NumRep))]
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
PP.vsep ([Doc] -> Doc)
-> ([(Text, Maybe (Edit NumRep))] -> [Doc])
-> [(Text, Maybe (Edit NumRep))]
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Text, Maybe (Edit NumRep))] -> [Doc]
presentStructuralVerificationAsDocs