TheoremGen.hs

module Language.Haskell.FreeTheorems.Variations.PolySeq.TheoremGen (makeFTFull, makeFTFullFunc) where

import Language.Haskell.FreeTheorems.Variations.PolySeq.TypeTranslator(translate)

import Language.Haskell.FreeTheorems.Parser.Haskell98 as FTP
import Language.Haskell.FreeTheorems
	( runChecks
	, check
	, prettyTheorem
	, 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 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)
    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 [OmitLanguageSubsets] (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 [OmitLanguageSubsets]) ls)
       else Left (unlines (map render es))


--makeFTFullFunc :: Typ -> Either String String
makeFTFullFunc 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)
    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 [OmitLanguageSubsets] (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 [OmitLanguageSubsets]) ls)
       else Left (unlines (map render es))