{-# LANGUAGE RecordWildCards, PatternGuards, FlexibleContexts #-}

-- | Check the coverage of the hints given a list of Isabelle theorems
module Test.Proof(proof) where

import Data.Tuple.Extra
import Control.Applicative
import Control.Monad
import Control.Monad.Trans.State
import Data.Char
import Data.List.Extra
import Data.Maybe
import Data.Function
import System.FilePath
import Config.Type
import HSE.All
import Prelude


data Theorem = Theorem
    {Theorem -> Maybe HintRule
original :: Maybe HintRule
    ,Theorem -> String
location :: String
    ,Theorem -> String
lemma :: String
    }

instance Eq Theorem where
    t1 :: Theorem
t1 == :: Theorem -> Theorem -> Bool
== t2 :: Theorem
t2 = Theorem -> String
lemma Theorem
t1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Theorem -> String
lemma Theorem
t2

instance Ord Theorem where
    compare :: Theorem -> Theorem -> Ordering
compare t1 :: Theorem
t1 t2 :: Theorem
t2 = String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Theorem -> String
lemma Theorem
t1) (Theorem -> String
lemma Theorem
t2)

instance Show Theorem where
    show :: Theorem -> String
show Theorem{..} = String
location String -> ShowS
forall a. [a] -> [a] -> [a]
++ ":\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> (HintRule -> String) -> Maybe HintRule -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "" HintRule -> String
f Maybe HintRule
original String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
lemma String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n"
        where f :: HintRule -> String
f HintRule{..} = "(* " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp SrcSpanInfo -> String
forall a. Pretty a => a -> String
prettyPrint Exp SrcSpanInfo
hintRuleLHS String -> ShowS
forall a. [a] -> [a] -> [a]
++ " ==> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp SrcSpanInfo -> String
forall a. Pretty a => a -> String
prettyPrint Exp SrcSpanInfo
hintRuleRHS String -> ShowS
forall a. [a] -> [a] -> [a]
++ " *)\n"

proof :: [FilePath] -> [Setting] -> FilePath -> IO ()
proof :: [String] -> [Setting] -> String -> IO ()
proof reports :: [String]
reports hints :: [Setting]
hints thy :: String
thy = do
    [Theorem]
got <- String -> String -> [Theorem]
isabelleTheorems (ShowS
takeFileName String
thy) (String -> [Theorem]) -> IO String -> IO [Theorem]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO String
readFile String
thy
    let want :: [Theorem]
want = [Theorem] -> [Theorem]
forall a. Ord a => [a] -> [a]
nubOrd ([Theorem] -> [Theorem]) -> [Theorem] -> [Theorem]
forall a b. (a -> b) -> a -> b
$ [Setting] -> [Theorem]
hintTheorems [Setting]
hints
    let unused :: [Theorem]
unused = [Theorem]
got [Theorem] -> [Theorem] -> [Theorem]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Theorem]
want
    let missing :: [Theorem]
missing = [Theorem]
want [Theorem] -> [Theorem] -> [Theorem]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Theorem]
got
    let reasons :: [(String, [Theorem])]
reasons = ([(String, Theorem)] -> (String, [Theorem]))
-> [[(String, Theorem)]] -> [(String, [Theorem])]
forall a b. (a -> b) -> [a] -> [b]
map (\x :: [(String, Theorem)]
x -> ((String, Theorem) -> String
forall a b. (a, b) -> a
fst ((String, Theorem) -> String) -> (String, Theorem) -> String
forall a b. (a -> b) -> a -> b
$ [(String, Theorem)] -> (String, Theorem)
forall a. [a] -> a
head [(String, Theorem)]
x, ((String, Theorem) -> Theorem) -> [(String, Theorem)] -> [Theorem]
forall a b. (a -> b) -> [a] -> [b]
map (String, Theorem) -> Theorem
forall a b. (a, b) -> b
snd [(String, Theorem)]
x)) ([[(String, Theorem)]] -> [(String, [Theorem])])
-> [[(String, Theorem)]] -> [(String, [Theorem])]
forall a b. (a -> b) -> a -> b
$ ((String, Theorem) -> (String, Theorem) -> Bool)
-> [(String, Theorem)] -> [[(String, Theorem)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
(==) (String -> String -> Bool)
-> ((String, Theorem) -> String)
-> (String, Theorem)
-> (String, Theorem)
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (String, Theorem) -> String
forall a b. (a, b) -> a
fst) ([(String, Theorem)] -> [[(String, Theorem)]])
-> [(String, Theorem)] -> [[(String, Theorem)]]
forall a b. (a -> b) -> a -> b
$
                  ((String, Theorem) -> (String, Theorem) -> Ordering)
-> [(String, Theorem)] -> [(String, Theorem)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (String -> String -> Ordering)
-> ((String, Theorem) -> String)
-> (String, Theorem)
-> (String, Theorem)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (String, Theorem) -> String
forall a b. (a, b) -> a
fst) ([(String, Theorem)] -> [(String, Theorem)])
-> [(String, Theorem)] -> [(String, Theorem)]
forall a b. (a -> b) -> a -> b
$ (Theorem -> (String, Theorem)) -> [Theorem] -> [(String, Theorem)]
forall a b. (a -> b) -> [a] -> [b]
map (Theorem -> String
classifyMissing (Theorem -> String)
-> (Theorem -> Theorem) -> Theorem -> (String, Theorem)
forall a b c. (a -> b) -> (a -> c) -> a -> (b, c)
&&& Theorem -> Theorem
forall a. a -> a
id) [Theorem]
missing
    let summary :: [String]
summary = [(String, [Theorem])] -> [String]
forall (t :: * -> *) a. Foldable t => [(String, t a)] -> [String]
table ([(String, [Theorem])] -> [String])
-> [(String, [Theorem])] -> [String]
forall a b. (a -> b) -> a -> b
$ let * :: a -> b -> (a, b)
(*) = (,) in
            ["HLint hints" String -> [Theorem] -> (String, [Theorem])
forall a b. a -> b -> (a, b)
* [Theorem]
want
            ,"HOL proofs" String -> [Theorem] -> (String, [Theorem])
forall a b. a -> b -> (a, b)
* [Theorem]
got
            ,"Useful proofs" String -> [Theorem] -> (String, [Theorem])
forall a b. a -> b -> (a, b)
* ([Theorem]
got [Theorem] -> [Theorem] -> [Theorem]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Theorem]
want)
            ,"Unused proofs" String -> [Theorem] -> (String, [Theorem])
forall a b. a -> b -> (a, b)
* [Theorem]
unused
            ,"Unproved hints" String -> [Theorem] -> (String, [Theorem])
forall a b. a -> b -> (a, b)
* [Theorem]
missing] [(String, [Theorem])]
-> [(String, [Theorem])] -> [(String, [Theorem])]
forall a. [a] -> [a] -> [a]
++
            [("  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
name) String -> [Theorem] -> (String, [Theorem])
forall a b. a -> b -> (a, b)
* [Theorem]
ps | (name :: String
name,ps :: [Theorem]
ps) <- [(String, [Theorem])]
reasons]
    String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String]
summary
    [String] -> (String -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [String]
reports ((String -> IO ()) -> IO ()) -> (String -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \report :: String
report -> do
        let out :: [(String, [Theorem])]
out = ("Unused proofs",[Theorem]
unused) (String, [Theorem])
-> [(String, [Theorem])] -> [(String, [Theorem])]
forall a. a -> [a] -> [a]
: ((String, [Theorem]) -> (String, [Theorem]))
-> [(String, [Theorem])] -> [(String, [Theorem])]
forall a b. (a -> b) -> [a] -> [b]
map (ShowS -> (String, [Theorem]) -> (String, [Theorem])
forall a a' b. (a -> a') -> (a, b) -> (a', b)
first ("Unproved hints - " String -> ShowS
forall a. [a] -> [a] -> [a]
++)) [(String, [Theorem])]
reasons
        String -> String -> IO ()
writeFile String
report (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String]
summary [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ "" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [("== " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ " ==") String -> [String] -> [String]
forall a. a -> [a] -> [a]
: "" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Theorem -> String) -> [Theorem] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Theorem -> String
forall a. Show a => a -> String
show [Theorem]
b | (a :: String
a,b :: [Theorem]
b) <- [(String, [Theorem])]
out]
        String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Report written to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
report
    where
        table :: [(String, t a)] -> [String]
table xs :: [(String, t a)]
xs = [String
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 6 Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
a Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
bb) ' ' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
bb | (a :: String
a,b :: t a
b) <- [(String, t a)]
xs, let bb :: String
bb = Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
b]
            where n :: Int
n = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ ((String, t a) -> Int) -> [(String, t a)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int)
-> ((String, t a) -> String) -> (String, t a) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, t a) -> String
forall a b. (a, b) -> a
fst) [(String, t a)]
xs


missingFuncs :: [(String, String)]
missingFuncs :: [(String, String)]
missingFuncs = let a :: b
a* :: b -> String -> [(String, b)]
*b :: String
b = [(String
b,b
a) | String
b <- String -> [String]
words String
b] in [[(String, String)]] -> [(String, String)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    ["IO" String -> String -> [(String, String)]
forall b. b -> String -> [(String, b)]
* "putChar putStr print putStrLn getLine getChar getContents hReady hPrint stdin"
    ,"Exit" String -> String -> [(String, String)]
forall b. b -> String -> [(String, b)]
* "exitSuccess"
    ,"Ord" String -> String -> [(String, String)]
forall b. b -> String -> [(String, b)]
* "(>) (<=) (>=) (<) compare minimum maximum sort sortBy"
    ,"Show" String -> String -> [(String, String)]
forall b. b -> String -> [(String, b)]
* "show shows showIntAtBase"
    ,"Read" String -> String -> [(String, String)]
forall b. b -> String -> [(String, b)]
* "reads read"
    ,"String" String -> String -> [(String, String)]
forall b. b -> String -> [(String, b)]
* "lines unlines words unwords"
    ,"Monad" String -> String -> [(String, String)]
forall b. b -> String -> [(String, b)]
* "mapM mapM_ sequence sequence_ msum mplus mzero liftM when unless return evaluate join void (>>=) (<=<) (>=>) forever ap"
    ,"Functor" String -> String -> [(String, String)]
forall b. b -> String -> [(String, b)]
* "fmap"
    ,"Numeric" String -> String -> [(String, String)]
forall b. b -> String -> [(String, b)]
* "(+) (*) fromInteger fromIntegral negate log (/) (-) (*) (^^) (^) subtract sqrt even odd"
    ,"Char" String -> String -> [(String, String)]
forall b. b -> String -> [(String, b)]
* "isControl isPrint isUpper isLower isAlpha isDigit"
    ,"Arrow" String -> String -> [(String, String)]
forall b. b -> String -> [(String, b)]
* "second first (***) (&&&)"
    ,"Applicative+" String -> String -> [(String, String)]
forall b. b -> String -> [(String, b)]
* "traverse for traverse_ for_ pure (<|>) (<**>)"
    ,"Exception" String -> String -> [(String, String)]
forall b. b -> String -> [(String, b)]
* "catch handle catchJust bracket error toException"
    ,"WeakPtr" String -> String -> [(String, String)]
forall b. b -> String -> [(String, b)]
* "mkWeak"
    ]


-- | Guess why a theorem is missing
classifyMissing :: Theorem -> String
classifyMissing :: Theorem -> String
classifyMissing Theorem{original :: Theorem -> Maybe HintRule
original = Just HintRule{..}}
    | _:_ <- [Exp SrcSpanInfo
v :: Exp_ | v :: Exp SrcSpanInfo
v@Case{} <- (Exp SrcSpanInfo, Exp SrcSpanInfo) -> [Exp SrcSpanInfo]
forall from to. Biplate from to => from -> [to]
universeBi (Exp SrcSpanInfo
hintRuleLHS,Exp SrcSpanInfo
hintRuleRHS)] = "case"
    | _:_ <- [Exp SrcSpanInfo
v :: Exp_ | v :: Exp SrcSpanInfo
v@ListComp{} <- (Exp SrcSpanInfo, Exp SrcSpanInfo) -> [Exp SrcSpanInfo]
forall from to. Biplate from to => from -> [to]
universeBi (Exp SrcSpanInfo
hintRuleLHS,Exp SrcSpanInfo
hintRuleRHS)] = "list-comp"
    | v :: String
v:_ <- (String -> Maybe String) -> [String] -> [String]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(String, String)]
missingFuncs) [Name SrcSpanInfo -> String
forall a. Pretty a => a -> String
prettyPrint (Name SrcSpanInfo
v :: Name S) | Name SrcSpanInfo
v <- (Exp SrcSpanInfo, Exp SrcSpanInfo) -> [Name SrcSpanInfo]
forall from to. Biplate from to => from -> [to]
universeBi (Exp SrcSpanInfo
hintRuleLHS,Exp SrcSpanInfo
hintRuleRHS)] = String
v
classifyMissing _ = "?unknown"


-- Extract theorems out of Isabelle code (HLint.thy)
isabelleTheorems :: FilePath -> String -> [Theorem]
isabelleTheorems :: String -> String -> [Theorem]
isabelleTheorems file :: String
file = [(Int, String)] -> [Theorem]
forall a. Show a => [(a, String)] -> [Theorem]
find ([(Int, String)] -> [Theorem])
-> (String -> [(Int, String)]) -> String -> [Theorem]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String -> [(Int, String)]
lexer 1
    where
        find :: [(a, String)] -> [Theorem]
find ((i :: a
i,"lemma"):(_,'\"':lemma :: String
lemma):rest :: [(a, String)]
rest) = Maybe HintRule -> String -> String -> Theorem
Theorem Maybe HintRule
forall a. Maybe a
Nothing (String
file String -> ShowS
forall a. [a] -> [a] -> [a]
++ ":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i) String
lemma Theorem -> [Theorem] -> [Theorem]
forall a. a -> [a] -> [a]
: [(a, String)] -> [Theorem]
find [(a, String)]
rest
        find ((i :: a
i,"lemma"):(_,name :: String
name):(_,":"):(_,'\"':lemma :: String
lemma):rest :: [(a, String)]
rest) = Maybe HintRule -> String -> String -> Theorem
Theorem Maybe HintRule
forall a. Maybe a
Nothing (String
file String -> ShowS
forall a. [a] -> [a] -> [a]
++ ":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i) String
lemma Theorem -> [Theorem] -> [Theorem]
forall a. a -> [a] -> [a]
: [(a, String)] -> [Theorem]
find [(a, String)]
rest
        find ((i :: a
i,"lemma"):(_,"assumes"):(_,'\"':assumes :: String
assumes):(_,"shows"):(_,'\"':lemma :: String
lemma):rest :: [(a, String)]
rest) =
            Maybe HintRule -> String -> String -> Theorem
Theorem Maybe HintRule
forall a. Maybe a
Nothing (String
file String -> ShowS
forall a. [a] -> [a] -> [a]
++ ":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i) (String
assumes String -> ShowS
forall a. [a] -> [a] -> [a]
++ " \\<Longrightarrow> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
lemma) Theorem -> [Theorem] -> [Theorem]
forall a. a -> [a] -> [a]
: [(a, String)] -> [Theorem]
find [(a, String)]
rest

        find ((i :: a
i,"lemma"):rest :: [(a, String)]
rest) = Maybe HintRule -> String -> String -> Theorem
Theorem Maybe HintRule
forall a. Maybe a
Nothing (String
file String -> ShowS
forall a. [a] -> [a] -> [a]
++ ":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i) "Unsupported lemma format" Theorem -> [Theorem] -> [Theorem]
forall a. a -> [a] -> [a]
: [(a, String)] -> [Theorem]
find [(a, String)]
rest
        find (x :: (a, String)
x:xs :: [(a, String)]
xs) = [(a, String)] -> [Theorem]
find [(a, String)]
xs
        find [] = []

        lexer :: Int -> String -> [(Int, String)]
lexer i :: Int
i x :: String
x
            | Int
i Int -> Bool -> Bool
forall a b. a -> b -> b
`seq` Bool
False = []
            | Just x :: String
x <- String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "(*" String
x, (a :: String
a,b :: String
b) <- String -> String -> (String, String)
breaks "*)" String
x = Int -> String -> [(Int, String)]
lexer (String -> Int -> Int
add String
a Int
i) String
b
            | Just x :: String
x <- String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "\"" String
x, (a :: String
a,b :: String
b) <- String -> String -> (String, String)
breaks "\"" String
x = (Int
i,'\"'Char -> ShowS
forall a. a -> [a] -> [a]
:String
a) (Int, String) -> [(Int, String)] -> [(Int, String)]
forall a. a -> [a] -> [a]
: Int -> String -> [(Int, String)]
lexer (String -> Int -> Int
add String
a Int
i) String
b -- NOTE: drop the final "
            | x :: Char
x:xs :: String
xs <- String
x, Char -> Bool
isSpace Char
x = Int -> String -> [(Int, String)]
lexer (String -> Int -> Int
add [Char
x] Int
i) String
xs
            | (a :: String
a@(_:_),b :: String
b) <- (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (\y :: Char
y -> Char
y Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '_' Bool -> Bool -> Bool
|| Char -> Bool
isAlpha Char
y) String
x = (Int
i,String
a) (Int, String) -> [(Int, String)] -> [(Int, String)]
forall a. a -> [a] -> [a]
: Int -> String -> [(Int, String)]
lexer (String -> Int -> Int
add String
a Int
i) String
b
        lexer i :: Int
i (x :: Char
x:xs :: String
xs) = (Int
i,[Char
x]) (Int, String) -> [(Int, String)] -> [(Int, String)]
forall a. a -> [a] -> [a]
: Int -> String -> [(Int, String)]
lexer (String -> Int -> Int
add [Char
x] Int
i) String
xs
        lexer i :: Int
i [] = []

        add :: String -> Int -> Int
add s :: String
s i :: Int
i = String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '\n') String
s) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i

        breaks :: String -> String -> (String, String)
breaks s :: String
s x :: String
x | Just x :: String
x <- String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix String
s String
x = ("",String
x)
        breaks s :: String
s (x :: Char
x:xs :: String
xs) = let (a :: String
a,b :: String
b) = String -> String -> (String, String)
breaks String
s String
xs in (Char
xChar -> ShowS
forall a. a -> [a] -> [a]
:String
a,String
b)
        breaks s :: String
s [] = ([],[])


reparen :: Setting -> Setting
reparen :: Setting -> Setting
reparen (SettingMatchExp m :: HintRule
m@HintRule{..}) = HintRule -> Setting
SettingMatchExp HintRule
m{hintRuleLHS :: Exp SrcSpanInfo
hintRuleLHS = Bool -> Exp SrcSpanInfo -> Exp SrcSpanInfo
forall p l. p -> Exp l -> Exp l
f Bool
False Exp SrcSpanInfo
hintRuleLHS, hintRuleRHS :: Exp SrcSpanInfo
hintRuleRHS = Bool -> Exp SrcSpanInfo -> Exp SrcSpanInfo
forall p l. p -> Exp l -> Exp l
f Bool
True Exp SrcSpanInfo
hintRuleRHS}
    where f :: p -> Exp l -> Exp l
f right :: p
right x :: Exp l
x = if Exp l -> Bool
forall l. Exp l -> Bool
isLambda Exp l
x Bool -> Bool -> Bool
|| Exp l -> Bool
forall l. Exp l -> Bool
isIf Exp l
x Bool -> Bool -> Bool
|| Exp l -> Bool
forall l. Exp l -> Bool
badInfix Exp l
x then l -> Exp l -> Exp l
forall l. l -> Exp l -> Exp l
Paren (Exp l -> l
forall (ast :: * -> *) l. Annotated ast => ast l -> l
ann Exp l
x) Exp l
x else Exp l
x
          badInfix :: Exp l -> Bool
badInfix (InfixApp _ _ op :: QOp l
op _) = QOp l -> String
forall a. Pretty a => a -> String
prettyPrint QOp l
op String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String -> [String]
words "|| && ."
          badInfix _ = Bool
False
reparen x :: Setting
x = Setting
x


-- Extract theorems out of the hints
hintTheorems :: [Setting] -> [Theorem]
hintTheorems :: [Setting] -> [Theorem]
hintTheorems xs :: [Setting]
xs =
    [ Maybe HintRule -> String -> String -> Theorem
Theorem (HintRule -> Maybe HintRule
forall a. a -> Maybe a
Just HintRule
m) (SrcSpanInfo -> String
loc (SrcSpanInfo -> String) -> SrcSpanInfo -> String
forall a b. (a -> b) -> a -> b
$ Exp SrcSpanInfo -> SrcSpanInfo
forall (ast :: * -> *) l. Annotated ast => ast l -> l
ann Exp SrcSpanInfo
hintRuleLHS) (String -> Theorem) -> String -> Theorem
forall a b. (a -> b) -> a -> b
$ String
-> (Exp SrcSpanInfo -> String) -> Maybe (Exp SrcSpanInfo) -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "" Exp SrcSpanInfo -> String
forall l. Named (Exp l) => Exp l -> String
assumes Maybe (Exp SrcSpanInfo)
hintRuleSide String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Note] -> String -> ShowS
forall (t :: * -> *). Foldable t => t Note -> String -> ShowS
relationship [Note]
hintRuleNotes String
a String
b
    | SettingMatchExp m :: HintRule
m@HintRule{..} <- (Setting -> Setting) -> [Setting] -> [Setting]
forall a b. (a -> b) -> [a] -> [b]
map Setting -> Setting
reparen [Setting]
xs, let a :: String
a = Exp SrcSpanInfo -> String
exp1 (Exp SrcSpanInfo -> String) -> Exp SrcSpanInfo -> String
forall a b. (a -> b) -> a -> b
$ [Note] -> Exp SrcSpanInfo -> Exp SrcSpanInfo
forall (t :: * -> *).
Foldable t =>
t Note -> Exp SrcSpanInfo -> Exp SrcSpanInfo
typeclasses [Note]
hintRuleNotes Exp SrcSpanInfo
hintRuleLHS, let b :: String
b = Exp SrcSpanInfo -> String
exp1 Exp SrcSpanInfo
hintRuleRHS, String
a String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
b]
    where
        loc :: SrcSpanInfo -> String
loc (SrcSpanInfo (SrcSpan file :: String
file ln :: Int
ln _ _ _) _) = ShowS
takeFileName String
file String -> ShowS
forall a. [a] -> [a] -> [a]
++ ":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
ln

        subs :: String -> String -> Maybe String
subs xs :: String
xs = (String -> [(String, String)] -> Maybe String)
-> [(String, String)] -> String -> Maybe String
forall a b c. (a -> b -> c) -> b -> a -> c
flip String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [(ShowS
forall a. [a] -> [a]
reverse String
b, ShowS
forall a. [a] -> [a]
reverse String
a) | String
x <- String -> [String]
words String
xs, let (a :: String
a,'=':b :: String
b) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '=') (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ ShowS
forall a. [a] -> [a]
reverse String
x]
        funs :: String -> Maybe String
funs = String -> String -> Maybe String
subs "id=ID not=neg or=the_or and=the_and (||)=tror (&&)=trand (++)=append (==)=eq (/=)=neq ($)=dollar"
        ops :: String -> Maybe String
ops = String -> String -> Maybe String
subs "||=orelse &&=andalso .=oo ===eq /==neq ++=++ !!=!! $=dollar $!=dollarBang"
        pre :: String -> Bool
pre = (String -> [String] -> Bool) -> [String] -> String -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ([String] -> String -> Bool) -> [String] -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String -> [String]
words "eq neq dollar dollarBang"
        cons :: String -> Maybe String
cons = String -> String -> Maybe String
subs "True=TT False=FF"

        typeclasses :: t Note -> Exp SrcSpanInfo -> Exp SrcSpanInfo
typeclasses hintRuleNotes :: t Note
hintRuleNotes x :: Exp SrcSpanInfo
x = (Note -> Exp SrcSpanInfo -> Exp SrcSpanInfo)
-> Exp SrcSpanInfo -> t Note -> Exp SrcSpanInfo
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Note -> Exp SrcSpanInfo -> Exp SrcSpanInfo
f Exp SrcSpanInfo
x t Note
hintRuleNotes
            where
                f :: Note -> Exp SrcSpanInfo -> Exp SrcSpanInfo
f (ValidInstance cls :: String
cls var :: String
var) x :: Exp SrcSpanInfo
x = State Bool (Exp SrcSpanInfo) -> Bool -> Exp SrcSpanInfo
forall s a. State s a -> s -> a
evalState ((Exp SrcSpanInfo -> State Bool (Exp SrcSpanInfo))
-> Exp SrcSpanInfo -> State Bool (Exp SrcSpanInfo)
forall (m :: * -> *) on.
(Monad m, Uniplate on) =>
(on -> m on) -> on -> m on
transformM Exp SrcSpanInfo -> State Bool (Exp SrcSpanInfo)
g Exp SrcSpanInfo
x) Bool
True
                    where g :: Exp SrcSpanInfo -> State Bool (Exp SrcSpanInfo)
g v :: Exp SrcSpanInfo
v@Var{} | Exp SrcSpanInfo
v Exp SrcSpanInfo -> String -> Bool
forall a. Named a => a -> String -> Bool
~= String
var = do
                                Bool
b <- StateT Bool Identity Bool
forall (m :: * -> *) s. Monad m => StateT s m s
get; Bool -> StateT Bool Identity ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put Bool
False
                                Exp SrcSpanInfo -> State Bool (Exp SrcSpanInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp SrcSpanInfo -> State Bool (Exp SrcSpanInfo))
-> Exp SrcSpanInfo -> State Bool (Exp SrcSpanInfo)
forall a b. (a -> b) -> a -> b
$ if Bool
b then SrcSpanInfo -> Exp SrcSpanInfo -> Exp SrcSpanInfo
forall l. l -> Exp l -> Exp l
Paren SrcSpanInfo
an (Exp SrcSpanInfo -> Exp SrcSpanInfo)
-> Exp SrcSpanInfo -> Exp SrcSpanInfo
forall a b. (a -> b) -> a -> b
$ String -> Exp SrcSpanInfo
forall a. Named a => String -> a
toNamed (String -> Exp SrcSpanInfo) -> String -> Exp SrcSpanInfo
forall a b. (a -> b) -> a -> b
$ Exp SrcSpanInfo -> String
forall a. Pretty a => a -> String
prettyPrint Exp SrcSpanInfo
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ "::'a::" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
cls String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_sym" else Exp SrcSpanInfo
v
                          g v :: Exp SrcSpanInfo
v = Exp SrcSpanInfo -> State Bool (Exp SrcSpanInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return Exp SrcSpanInfo
v :: State Bool Exp_
                f _  x :: Exp SrcSpanInfo
x = Exp SrcSpanInfo
x

        relationship :: t Note -> String -> ShowS
relationship hintRuleNotes :: t Note
hintRuleNotes a :: String
a b :: String
b | (Note -> Bool) -> t Note -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Note -> Bool
lazier t Note
hintRuleNotes = String
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ " \\<sqsubseteq> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
b
                               | Note
DecreasesLaziness Note -> t Note -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Note
hintRuleNotes = String
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ " \\<sqsubseteq> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
a
                               | Bool
otherwise = String
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ " = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
b
            where lazier :: Note -> Bool
lazier IncreasesLaziness = Bool
True
                  lazier RemovesError{} = Bool
True
                  lazier _ = Bool
False

        assumes :: Exp l -> String
assumes (App _ op :: Exp l
op var :: Exp l
var)
            | Exp l
op Exp l -> String -> Bool
forall a. Named a => a -> String -> Bool
~= "isNat" = "le\\<cdot>0\\<cdot>" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp l -> String
forall a. Pretty a => a -> String
prettyPrint Exp l
var String -> ShowS
forall a. [a] -> [a] -> [a]
++ " \\<noteq> FF \\<Longrightarrow> "
            | Exp l
op Exp l -> String -> Bool
forall a. Named a => a -> String -> Bool
~= "isNegZero" = "gt\\<cdot>0\\<cdot>" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp l -> String
forall a. Pretty a => a -> String
prettyPrint Exp l
var String -> ShowS
forall a. [a] -> [a] -> [a]
++ " \\<noteq> FF \\<Longrightarrow> "
        assumes (App _ op :: Exp l
op var :: Exp l
var) | Exp l
op Exp l -> String -> Bool
forall a. Named a => a -> String -> Bool
~= "isWHNF" = Exp l -> String
forall a. Pretty a => a -> String
prettyPrint Exp l
var String -> ShowS
forall a. [a] -> [a] -> [a]
++ " \\<noteq> \\<bottom> \\<Longrightarrow> "
        assumes _ = ""

        exp1 :: Exp SrcSpanInfo -> String
exp1 = Exp SrcSpanInfo -> String
forall l.
(Default l, Named (Pat l), Named (Exp l), Data l, Ord l) =>
Exp l -> String
exp (Exp SrcSpanInfo -> String)
-> (Exp SrcSpanInfo -> Exp SrcSpanInfo)
-> Exp SrcSpanInfo
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName SrcSpanInfo -> QName SrcSpanInfo)
-> Exp SrcSpanInfo -> Exp SrcSpanInfo
forall from to. Biplate from to => (to -> to) -> from -> from
transformBi QName SrcSpanInfo -> QName SrcSpanInfo
unqual

        -- Syntax translations
        exp :: Exp l -> String
exp (App _ a :: Exp l
a b :: Exp l
b) = Exp l -> String
exp Exp l
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\\<cdot>" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp l -> String
exp Exp l
b
        exp (Paren _ x :: Exp l
x) = "(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp l -> String
exp Exp l
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
        exp (Var _ x :: QName l
x) | Just x :: String
x <- String -> Maybe String
funs (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ QName l -> String
forall a. Pretty a => a -> String
prettyPrint QName l
x = String
x
        exp (Con _ (Special _ (TupleCon _ _ i :: Int
i))) = "\\<langle>" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) ',' String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\\<rangle>"
        exp (Con _ x :: QName l
x) | Just x :: String
x <- String -> Maybe String
cons (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ QName l -> String
forall a. Pretty a => a -> String
prettyPrint QName l
x = String
x
        exp (Tuple _ _ xs :: [Exp l]
xs) = "\\<langle>" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " ((Exp l -> String) -> [Exp l] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Exp l -> String
exp [Exp l]
xs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\\<rangle>"
        exp (If _ a :: Exp l
a b :: Exp l
b c :: Exp l
c) = "If " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp l -> String
exp Exp l
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ " then " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp l -> String
exp Exp l
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ " else " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp l -> String
exp Exp l
c
        exp (Lambda _ xs :: [Pat l]
xs y :: Exp l
y) = "\\<Lambda> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Pat l -> String) -> [Pat l] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Pat l -> String
forall l. Pat l -> String
pat [Pat l]
xs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ ". " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp l -> String
exp Exp l
y
        exp (InfixApp _ x :: Exp l
x op :: QOp l
op y :: Exp l
y) | Just op :: String
op <- String -> Maybe String
ops (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ QOp l -> String
forall a. Pretty a => a -> String
prettyPrint QOp l
op =
            if String -> Bool
pre String
op then String
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\\<cdot>" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp l -> String
exp (Exp l -> Exp l
forall l. (Data l, Default l) => Exp l -> Exp l
paren Exp l
x) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\\<cdot>" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp l -> String
exp (Exp l -> Exp l
forall l. (Data l, Default l) => Exp l -> Exp l
paren Exp l
y) else Exp l -> String
exp Exp l
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp l -> String
exp Exp l
y

        -- Translations from the Haskell 2010 report
        exp (InfixApp l :: l
l a :: Exp l
a (QVarOp _ b :: QName l
b) c :: Exp l
c) = Exp l -> String
exp (Exp l -> String) -> Exp l -> String
forall a b. (a -> b) -> a -> b
$ l -> Exp l -> Exp l -> Exp l
forall l. l -> Exp l -> Exp l -> Exp l
App l
l (l -> Exp l -> Exp l -> Exp l
forall l. l -> Exp l -> Exp l -> Exp l
App l
l (l -> QName l -> Exp l
forall l. l -> QName l -> Exp l
Var l
l QName l
b) Exp l
a) Exp l
c -- S3.4
        exp x :: Exp l
x@(LeftSection l :: l
l e :: Exp l
e op :: QOp l
op) = let v :: String
v = Exp l -> String
forall a. FreeVars a => a -> String
fresh Exp l
x in Exp l -> String
exp (Exp l -> String) -> Exp l -> String
forall a b. (a -> b) -> a -> b
$ l -> Exp l -> Exp l
forall l. l -> Exp l -> Exp l
Paren l
l (Exp l -> Exp l) -> Exp l -> Exp l
forall a b. (a -> b) -> a -> b
$ l -> [Pat l] -> Exp l -> Exp l
forall l. l -> [Pat l] -> Exp l -> Exp l
Lambda l
l [String -> Pat l
forall a. Named a => String -> a
toNamed String
v] (Exp l -> Exp l) -> Exp l -> Exp l
forall a b. (a -> b) -> a -> b
$ l -> Exp l -> QOp l -> Exp l -> Exp l
forall l. l -> Exp l -> QOp l -> Exp l -> Exp l
InfixApp l
l Exp l
e QOp l
op (String -> Exp l
forall a. Named a => String -> a
toNamed String
v) -- S3.5
        exp x :: Exp l
x@(RightSection l :: l
l op :: QOp l
op e :: Exp l
e) = let v :: String
v = Exp l -> String
forall a. FreeVars a => a -> String
fresh Exp l
x in Exp l -> String
exp (Exp l -> String) -> Exp l -> String
forall a b. (a -> b) -> a -> b
$ l -> Exp l -> Exp l
forall l. l -> Exp l -> Exp l
Paren l
l (Exp l -> Exp l) -> Exp l -> Exp l
forall a b. (a -> b) -> a -> b
$ l -> [Pat l] -> Exp l -> Exp l
forall l. l -> [Pat l] -> Exp l -> Exp l
Lambda l
l [String -> Pat l
forall a. Named a => String -> a
toNamed String
v] (Exp l -> Exp l) -> Exp l -> Exp l
forall a b. (a -> b) -> a -> b
$ l -> Exp l -> QOp l -> Exp l -> Exp l
forall l. l -> Exp l -> QOp l -> Exp l -> Exp l
InfixApp l
l (String -> Exp l
forall a. Named a => String -> a
toNamed String
v) QOp l
op Exp l
e -- S3.5
        exp x :: Exp l
x = Exp l -> String
forall a. Pretty a => a -> String
prettyPrint Exp l
x

        pat :: Pat l -> String
pat (PTuple _ _ xs :: [Pat l]
xs) = "\\<langle>" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " ((Pat l -> String) -> [Pat l] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Pat l -> String
pat [Pat l]
xs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\\<rangle>"
        pat x :: Pat l
x = Pat l -> String
forall a. Pretty a => a -> String
prettyPrint Pat l
x

        fresh :: a -> String
fresh x :: a
x = [String] -> String
forall a. [a] -> a
head ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ("z"String -> [String] -> [String]
forall a. a -> [a] -> [a]
:["v" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i | Integer
i <- [1..]]) [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
\\ a -> [String]
forall a. FreeVars a => a -> [String]
vars a
x