module Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeq where
import Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeqAlg
import Language.Haskell.FreeTheorems.Variations.PolySeq.AlgCommon(removeTrue,getEquals,instantiateWithEpsilon)
import Language.Haskell.FreeTheorems.Variations.PolySeq.M
import Language.Haskell.FreeTheorems.Variations.PolySeq.TheoremGen
import Language.Haskell.FreeTheorems.Variations.PolySeq.ConstraintSolver
import Text.PrettyPrint(renderStyle,Style(..),Mode(..),(<+>),text)
import Language.Haskell.FreeTheorems.Variations.PolySeq.PrettyPrint
import Language.Haskell.FreeTheorems.Variations.PolySeq.Parser.ParseTerm(parseTerm, parseTermWithFlag)
import Language.Haskell.FreeTheorems.Variations.PolySeq.Highlight
import Text.XHtml hiding(text)
polySeq = runM.algPolySeq
shellStyle = Style PageMode 80 0.2
webStyle = Style PageMode 80 0.2
getItT t =
case polySeq t of
Just ((t',c,tau),_) -> do{ putStr "The term: ";
putStr (renderStyle shellStyle (prettyMarkedTerm t'));
putStr "\n\nThe Constraint: ";
putStr (renderStyle shellStyle (prettyConstraint (removeTrue c)));
putStr "\n\nWith the equations: ";
putStr (show (getEquals c));
putStr "\n\nThe Type:";
putStr (renderStyle shellStyle (prettyMarkedTyp tau));
putStr "\n\nUsed Label Variables: ";
putStr "\n\n newSimplify:\n\n";
let (ts,taus,cs) = simplifyConstraint (t',tau,c) in
do{putStr "The term: ";
putStr (renderStyle shellStyle (prettyMarkedTerm ts));
putStr "\n\nThe Constraint: ";
putStr (renderStyle shellStyle (prettyConstraint cs));
putStr "\n\nThe Type:";
putStr (renderStyle shellStyle (prettyMarkedTyp taus));
putStr "\n\nWhich optimal would be:";
putStr (show (getOpt True taus));
putStr "\n\nThat means, it is typable to the following concrete Types\n\n";
putStr (foldr (\x y->(renderStyle shellStyle (prettyMarkedTyp x))++"\n"++y) ""
(makeTypes taus ((filterTyp taus).solveConstraint$cs)));
putStr "\n\nAnd consequently, it is typable to the following minimal concrete Types\n\n";
putStr (foldr (\x y->(renderStyle shellStyle (prettyMarkedTyp x))++"\n\n"++y) ""
(makeMinimalTypes taus ((filterTyp taus).solveConstraint$cs)));
};
putStr "\n\n";
}
Nothing -> putStr "Term is not typable at all.\n"
getItTRaw t =
case polySeq t of
Just ((t',c,tau),_) -> do{ putStr "The term: ";
putStr (renderStyle shellStyle (prettyMarkedTerm t'));
putStr "\n\nThe Constraint: ";
putStr (renderStyle shellStyle (prettyConstraint (removeTrue c)));
putStr "\n\nWith the equations: ";
putStr (show (getEquals c));
putStr "\n\nThe Type:";
putStr (renderStyle shellStyle (prettyMarkedTyp tau));
putStr "\n\nUsed Label Variables: ";
putStr "\n\n newSimplify:\n\n";
let (ts,taus,cs) = simplifyConstraint (t',tau,c) in
do{putStr "The term: ";
putStr (renderStyle shellStyle (prettyMarkedTerm ts));
putStr "\n\nThe Constraint: ";
putStr (renderStyle shellStyle (prettyConstraint cs));
putStr "\n\nThe Type:";
putStr (renderStyle shellStyle (prettyMarkedTyp taus));
putStr "\n\nWhich optimal would be:";
putStr (show (getOpt True taus));
putStr "\n\nThat means, it is typable to the following concrete Types\n\n";
putStr (foldr (\x y->(show x)++"\n\n"++y) ""
(makeTypes taus ((filterTyp taus).solveConstraint$cs)));
putStr "\n\nAnd consequently, it is typable to the following minimal concrete Types\n\n";
putStr (foldr (\x y->(show x)++"\n\n"++y) ""
(makeMinimalTypes taus ((filterTyp taus).solveConstraint$cs)));
};
putStr "\n\n";
}
Nothing -> putStr "Term is not typable at all.\n"
getIt str =
case parseTerm str of
Left err -> putStr (show err)
Right t -> getItT t
getItRaw str =
case parseTerm str of
Left err -> putStr (show err)
Right t -> getItTRaw t
getForWebInterface :: String -> Either (String, String) (String,String, String,String, [(String,String)])
getForWebInterface termstr =
case parseTermWithFlag termstr of
Left err -> Left ("ParseError",(show err))
Right (t,flag) -> case polySeq t of
Just ((t'',c',tau'),_) ->
let (t',tau,c) = simplifyConstraint (t'',tau',c')
minTypes = makeMinimalTypes tau ((filterTyp tau).solveConstraint$c)
optFT = map (fromRight.(makeFTFullFuncWithFlag flag)) minTypes
minTypFTList = zip (map ((renderStyle webStyle).prettyMarkedTyp) minTypes) optFT
normalFT = fromRight.(makeFTFullFuncWithFlag flag).instantiateWithEpsilon$ tau'
termStr = renderStyle webStyle (text "t =" <+> prettyUnMarkedTerm (adjustTypAbstraction flag t'))
constStr = renderStyle webStyle (prettyConstraint c)
tauStr = renderStyle webStyle (prettyMarkedTyp tau)
in
Right (termStr, constStr, tauStr,normalFT,minTypFTList)
Nothing -> Left ("NotTypable",renderStyle webStyle (prettyUnMarkedTerm t))
where fromRight (Right x) = x
testTerm = "/\\a.\\p::a->Bool.let! p' = p in (fix (\\f::[a]->[a]. \\ys::[a]. case ys of {[] -> []_{a}; x:xs-> let! x' = x in if p x then (let! xs' = xs in x):(f xs) else f xs }))"
test = case getForWebInterface testTerm of
Left _ -> putStr "shit happened."
Right (t,c,tau,nft,l) -> do{ putStr "\n\nThe normal Theorem:\n\n";
putStr nft;
putStr "\n\nThe highlighted version:\n\n";
putStr (show.highlight$nft);
}
foldl'' = "/\\a./\\b.\\c :: a -> b -> a.let! c' = c in fix ( \\h :: a -> [b] -> a.\\n :: a.\\ys :: [b].let c'' = c n in case ys of {[] -> n; x:xs -> let! xs' = xs in let! x' = x in let n' = c'' x' in h n' xs' })"