module Language.Haskell.FreeTheorems.Variations.PolySeq.TheoremGen (makeFTFull, makeFTFullFunc, makeFTFullWithFlag, makeFTFullFuncWithFlag) where
import Language.Haskell.FreeTheorems.Variations.PolySeq.TypeTranslator(translate)
import Language.Haskell.FreeTheorems.Parser.Haskell98 as FTP
import Language.Haskell.FreeTheorems
( runChecks
, check
, prettyTheorem
, asTheorem
, asCompleteTheorem
, interpret
, unfoldLifts
, prettyUnfoldedLift
, LanguageSubset(SubsetWithSeq)
, TheoremType(EquationalTheorem)
, PrettyTheoremOption(OmitTypeInstantiations,OmitLanguageSubsets)
, specialise
, relationVariables
)
import Language.Haskell.FreeTheorems.BasicSyntax(Signature(..),Identifier(..))
import Language.Haskell.FreeTheorems.ValidSyntax(ValidSignature(..))
import Text.PrettyPrint.HughesPJ (render)
makeFTFull = makeFTFullWithFlag True
makeFTFullWithFlag flag tau =
let sig = ValidSignature (Signature (Ident "t") (translate tau))
bool = "data Bool = False | True"
parse_input = unlines [bool]
(ds,es) = runChecks (parse parse_input >>= check)
thmopts = if flag then [OmitLanguageSubsets] else [OmitLanguageSubsets, OmitTypeInstantiations]
in if null es
then case interpret ds (SubsetWithSeq EquationalTheorem) sig of
Nothing -> Left "interpret returned nothing"
Just i -> let i' = foldl specialise i (relationVariables i) in
Right $ render (prettyTheorem thmopts (asCompleteTheorem i)) ++
case unfoldLifts ds i of
[] -> ""
ls -> (if length ls == 1
then "\n\nThe structural lifting occuring therein is defined as follows:\n\n "
else "\n\nThe structural liftings occuring therein are defined as follows:\n\n") ++
unlines (map (render . prettyUnfoldedLift thmopts) ls)
else Left (unlines (map render es))
makeFTFullFunc = makeFTFullFuncWithFlag True
makeFTFullFuncWithFlag flag tau =
let sig = ValidSignature (Signature (Ident "t") (translate tau))
bool = "data Bool = False | True"
parse_input = unlines [bool]
(ds,es) = runChecks (parse parse_input >>= check)
thmopts = if flag then [OmitLanguageSubsets] else [OmitLanguageSubsets, OmitTypeInstantiations]
in if null es
then case interpret ds (SubsetWithSeq EquationalTheorem) sig of
Nothing -> Left "interpret returned nothing"
Just i -> let i' = foldl specialise i (relationVariables i) in
Right $ render (prettyTheorem thmopts (asCompleteTheorem i')) ++
case unfoldLifts ds i' of
[] -> ""
ls -> (if length ls == 1
then "\n\nThe structural lifting occuring therein is defined as follows:\n\n "
else "\n\nThe structural liftings occuring therein are defined as follows:\n\n") ++
unlines (map (render . prettyUnfoldedLift thmopts) ls)
else Left (unlines (map render es))