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 :: Typ -> Either String String
makeFTFull = makeFTFullWithFlag True

--makeFTFullWithFlag :: Typ -> Either String String
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))



--makeFTFullFuncWithFlag :: Typ -> Either String String
makeFTFullFunc = makeFTFullFuncWithFlag True

--makeFTFullFunc :: Bool -> Typ -> Either String String
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))