{-# LANGUAGE RecordWildCards, PatternGuards, FlexibleContexts #-}
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"
]
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"
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
| 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
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
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
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
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)
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
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