-module ExFindExtended (TypVar(..),Typ(..),TermVar(..),Term,AbsTerm(..),testTerm,getTerm,getComplete,getComplete',getWithDebug,getIt) where
+module ExFindExtended (TypVar(..),Typ(..),TermVar(..),Term,TermCont,TermPlus,PlusElem(..),AbsTerm(..),testTerm,getTerm,getComplete,getComplete',getCompleteRaw,getWithDebug,getIt) where
import Prelude hiding (Either(..))
import qualified Prelude as E (Either(..))
newtype TermVar = TermVar Int deriving (Show, Eq, Ord)
-data PlusElem = PlusElem TypVar Int
+data PlusElem = PlusElem TypVar Int deriving (Show, Eq)
type Term = AbsTerm ()
type TermPlus = AbsTerm PlusElem
}
getComplete' :: Typ -> E.Either String (String, String)
-getComplete' tau = case runM $ alg emptyCont tau emptyTermCont of
- Nothing -> E.Left "No Term."
- Just (result,debug) -> E.Right (showTerm (fst result),
+getComplete' tau = case getCompleteRaw tau of
+ E.Left err -> E.Left err
+ E.Right (result) -> E.Right (showTerm (fst result),
uncurry showUsedTermCont result)
+getCompleteRaw :: Typ -> E.Either String (Term,TermCont)
+getCompleteRaw tau = case runM $ alg emptyCont tau emptyTermCont of
+ Nothing -> E.Left "No Term."
+ Just (result,debug) -> E.Right (result)
+
getWithDebug tau = do {printTyp tau;
putStr "\n";
case runM $ alg emptyCont tau emptyTermCont of
| Pair Expr Expr
| Map
| ConstUnit
+ | CaseUnit Expr Expr
| EitherMap
| EUnit
+ | Bottom
deriving (Eq, Typeable, Data)
data LambdaBE = CurriedEquals Typ
showIntercalate (showString " . ") (map (showsPrec 10) es)
showsPrec _ (Lambda tv e) = showParen True $
showString "\\" .
- showsPrec 0 tv .
+ showsPrec 11 tv .
showString " -> ".
showsPrec 0 e
showsPrec _ (Pair e1 e2) = showParen True $
showsPrec _ EUnit = showString "()"
showsPrec _ Map = showString "map"
showsPrec d ConstUnit = showParen (d>10) $ showString "const ()"
+ showsPrec d (CaseUnit t1 t2) = showParen (d>5) $
+ showString "case " .
+ showsPrec 0 t1 .
+ showString " of () -> " .
+ showsPrec 11 t2
showsPrec _ EitherMap = showString "eitherMap"
+ showsPrec _ Bottom = showString "_|_"
showIntercalate :: ShowS -> [ShowS] -> ShowS
showIntercalate _ [] = id
import ParseType (parseType')
import SimpleFT (freeTheorem)
import Expr (specialize)
-import ExFindExtended (getComplete')
+import ExFindExtended (getComplete', getCompleteRaw)
import Language.Haskell.FreeTheorems.Parser.Haskell98 as FTP
import Language.Haskell.FreeTheorems
( runChecks
, prettyUnfoldedLift
, LanguageSubset(BasicSubset)
)
+import Term2Expr (term2Expr, termCond2Exprs, insertTermsInCondition)
import Network.CGI
import Data.ByteString.Lazy.UTF8 (fromString)
import Control.Monad
import Data.Maybe
import Text.PrettyPrint.HughesPJ (render)
+import qualified Data.Map as M
+import Data.Generics
askDiv v e = maindiv << (
p << ( "Please enter a function type, prepended with a list of type variables, " +++
) +++
maindiv << (
h3 << "The counter-example" +++
- case counter_example of
+ ( case counter_example of
Left err -> p << "No term could be derived: " +++ pre << err
Right (res,used) ->
p << ("By disregarding the strictness conditions for the chosen "+++
p << ("Whereas the abstraced variables are chosen as follows:" +++
pre << used)
) +++
+ h3 << "The raw counter-example" +++
+ case counter_example_raw of
+ Left err -> p << "No term could be derived: " +++ pre << err
+ Right result ->
+ p << (show result) +++
+ p << (show (term2Expr (fst result))) +++
+ p << (show (termCond2Exprs (snd result))) +++
+ p << (show (insertTermsInCondition result (specialize ft_simple))) +++
+ p << (gshow (insertTermsInCondition result (specialize ft_simple)))
+ ) +++
maindiv ( p << ("In the simplified theorems, the following custom haskell " +++
"functions might appear:") +++
pre << addDefs
ft_simple = freeTheorem typ
counter_example = getComplete' typ
+ counter_example_raw = getCompleteRaw typ
main = runCGI (handleErrors cgiMain)