free-theorems-counterexamples-0.3: Language/Haskell/FreeTheorems/Variations/CounterExamples/ExFind.hs
-- * The module ExFind contains the calling functions for the algorithm.
module Language.Haskell.FreeTheorems.Variations.CounterExamples.ExFind (getTerm, getComplete, getForWebInterface,
getWithDebug, testTerm, getIt, getContradiction, getItContradiction, getRawContradiction,
getItRawContradiction, getExample, getItExample, testSimple, webInterface) where
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Common.AlgCommon
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.ExFindExtended
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.M hiding (M)
import qualified Prelude as E (Either(..))
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.FTSync
import Prelude hiding (Either(..))
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType
import qualified Data.Map as Map
-- ** calling functions for ExFind
-- | takes the input in Typ format and returns the monad's debuging information and the result term
getTerm :: Typ -> IO()
getTerm tau = do printTyp tau
putStr "\n"
case runM $ alg emptyCont tau emptyTermCont of
Nothing -> putStr "No Term."
Just ((term,termCont,trackCont),debug,funcNames) -> do putStr (" " ++ (foldr (\x -> \y -> x ++ "\n " ++ y) "\n" debug))
printResult (term)
-- | takes the input in Typ format and returns the monad's tracking information, the result term t, the disrelater applied to 't' as variable and as term
getComplete :: Typ -> IO()
getComplete tau = do {printTyp tau;
putStr "\n";
case runM $ alg emptyCont tau emptyTermCont of
Nothing -> putStr "No Term."
Just ((term,termCont,trackCont),debug,funcs) ->
do {putStr (" " ++ (foldr (\x -> \y -> x ++ "\n " ++ y) "\n" debug));
printResult (term);
putStr ("Like webinterface:\n\n" ++ showTrackContApplication trackCont (Var (TermVar 0)) ++ "\n\n");
putStr ("With the disrelater:\n\n" ++ showTrackContApplication trackCont term ++"\n\n");
putStr ("And the variables are:\n\n" ++ showFuncNamesInt funcs ++ "\n\n");
putStr ("And completely solved: " ++ showTrackContApplicationSolved trackCont funcs term ++ "\n\n");
}
}
-- | Output for the webinterface defined in polyfix-cgi.hs (second version)
getForWebInterface :: Typ -> E.Either String (Term,TrackCont,[(Int,Term)])
getForWebInterface tau =
case runM $ alg emptyCont tau emptyTermCont of
Nothing -> E.Left "No Term."
Just ((term,termCont,trackCont),debug,funcs) -> E.Right (term,trackCont,funcs)
-- | takes the input in Typ format and returns the monad's tracking information, the result term t and all term variable environment entries
getWithDebug :: Typ -> IO()
getWithDebug tau = do {printTyp tau;
putStr "\n";
case runM $ alg emptyCont tau emptyTermCont of
Nothing -> putStr "No Term."
Just ((term,termCont,trackCont),debug,funcs) ->
do {putStr (" " ++ (foldr (\x -> \y -> x ++ "\n " ++ y) "\n" debug));
printResult (term);
printTermCont (termCont);
putStr (showTrackCont trackCont);
}
}
-- | takes the input in Typ format and returns the result term
testTerm :: Typ -> Maybe Term
testTerm tau = case runM $ alg emptyCont tau emptyTermCont of
Nothing -> Nothing
Just ((term,termCont,trackCont),_,_) -> Just (term)
-- | getComplete with prepended type parsing
getIt :: String -> IO()
getIt typstring = getComplete $ parseType typstring
-- | takes the input in Typ format and returns the monad's tracking information, the disrelater entries, the term environment entries, the result term t and the result of the application of the disrelater to the term t. All in pretty printing.
getContradiction :: Typ -> IO()
getContradiction tau =
case runM $ alg emptyCont tau emptyTermCont of
Nothing -> putStr "No Term.\n"
Just ((term,termCont,trackCont),debug,funcs) ->
let (t1',t2') = applyTrackCont term trackCont
(t1,t2) = (simplifyTerm t1', simplifyTerm t2') in
putStr (" " ++ (foldr (\x -> \y -> x ++ "\n " ++ y) "\n" debug) ++
"TrackCont:\n\n" ++ (showTrackCont trackCont) ++
"TermCont:\n\n" ++ (showTermCont termCont) ++
"Term: " ++ (showTerm term) ++ "\n\n" ++
(showTerm t1) ++ " == " ++ (showTerm t2) ++ "\n")
-- | getContradiction with prepended type parsing
getItContradiction :: String -> IO()
getItContradiction typstring = getContradiction $ parseType typstring
-- | takes the input in Typ format and returns the monad's tracking information, the disrelater entries, the term environment entries, the result term t and the result of the application of the disrelater to the term t. All _not_ in pretty printing
getRawContradiction :: Typ -> IO()
getRawContradiction tau =
case runM $ alg emptyCont tau emptyTermCont of
Nothing -> putStr "No Term.\n"
Just ((term,termCont,trackCont),debug,funcs) ->
let (t1',t2') = applyTrackCont term trackCont
(t1,t2) = (simplifyTerm t1', simplifyTerm t2') in
putStr (" " ++ (foldr (\x -> \y -> x ++ "\n " ++ y) "\n" debug) ++
"TrackCont:\n\n" ++ (showRawTrackCont trackCont) ++
"TermCont:\n\n" ++ (show termCont) ++
"Term: " ++ (show term) ++ "\n\n" ++
(showTerm t1) ++ " == " ++ (showTerm t2) ++ "\n")
-- | getRawContradiction with prepended type parsing
getItRawContradiction :: String -> IO()
getItRawContradiction typstring = getRawContradiction $ parseType typstring
-- | takes the input in Typ format and returns the result term, the disrelater and the application of the disrelater to the result term.
getExample:: Typ -> IO()
getExample tau =
case runM $ alg emptyCont tau emptyTermCont of
Nothing -> putStr "No Term.\n"
Just ((term,termCont,trackCont),debug,funcs) ->
let (t1',t2') = applyTrackCont term trackCont
(t1,t2) = (simplifyTerm t1', simplifyTerm t2')
t = Var (TermVar 0)
(td1,td2) = applyTrackCont t trackCont
[term',td1',td2'] = renumberVariables [term,simplifyAppOnly td1,simplifyAppOnly td2] in
putStr ("Term: " ++ (showTerm term') ++ "\n\n" ++
-- "Disrelater:\n\n" ++ (showTrackCont trackCont) ++
"The disrelater applied to the term leads to: \n\n" ++ (showTerm td1') ++ " == " ++ (showTerm td2') ++ "\n\n" ++
"which is resolved: " ++ (showTerm t1) ++ " == " ++ (showTerm t2) ++ "\n")
-- | getExample with prepended type parsing
getItExample :: String -> IO()
getItExample typstring = getExample $ parseType typstring
-- | test function for QuickCheck. It returns false, if the disrelater is not working properly, i.e. its application to the result term is not in (p+,_|_) or (_|_,_|_). It does not check for Pointedness, thus it would also accept the wrong result (_|_,_|_) on a pointed type.
testSimple :: Typ -> Bool
testSimple tau =
case runM $ alg emptyCont tau emptyTermCont of
Nothing -> True
Just ((term,termCont,trackCont),debug,funcs) ->
let (t1,t2) = getTrackContApplicationSolved trackCont funcs term in
case t2 of
Bottom _ -> case t1 of
Zero -> True
Brace -> True
Bottom _ -> True
Fls -> True
Cons _ _ -> True
Pair _ _ -> True
Left _ -> True
MJust _ -> True
_ -> error (showTerm t1) False
_ -> error (showTerm t1) False
-- | simulation of the web interface output of the counterexample
webInterface typString =
let typ = parseType typString in
putStr("The counterexample:\n\n" ++
( case getForWebInterface typ of
E.Left err -> "No term could be derived: " ++ err
E.Right result ->
let (term,trackCont,funcs) = result
names = zip (fst.unzip$funcs) drelNames in
("By disregarding the strictness conditions for the chosen "++
"relations, setting all selectable types to () and\n\n" ++
assignTypeRelFuncs typ funcNames ++
"\n\nthe following term is a counter example:\n\n" ++
(termName++" = " ++ (showTerm.head.renumberVariables $ [term]))) ++
("\n\nWhereas we confute the theorem by regarding:\n\n" ++
(prependRelFunc funcNames (fst trackCont) (showTrackContApplicationWithNames trackCont names (Var (TermVar 0)))) ++ "\n\n"++ showFuncNames (zip drelNames (snd.unzip$funcs)))
)
)