Convert Daniels Term to my Expr, and insert into theorem

diff --git a/ExFindExtended.hs b/ExFindExtended.hs
index 9cdf0f4..f648a25 100644 (file)
--- a/ExFindExtended.hs
+++ b/ExFindExtended.hs
@@ -1,4 +1,4 @@
-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(..))
@@ -26,7 +26,7 @@ type TermCont = Map.Map TermVar (TermPlus,TermPlus)
 
 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
@@ -999,11 +999,16 @@ getComplete tau = do {printTyp tau;
                     }
 
 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

diff --git a/Expr.hs b/Expr.hs
index b895827..17dba20 100644 (file)
--- a/Expr.hs
+++ b/Expr.hs
@@ -32,8 +32,10 @@ data Expr
        | Pair Expr Expr
        | Map
        | ConstUnit
+       | CaseUnit Expr Expr
        | EitherMap
        | EUnit
+       | Bottom
             deriving (Eq, Typeable, Data)
 
 data LambdaBE = CurriedEquals Typ
@@ -339,7 +341,7 @@ instance Show Expr where
                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 $ 
@@ -349,7 +351,13 @@ instance Show Expr where
        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

diff --git a/polyfix-cgi.hs b/polyfix-cgi.hs
index e78ee05..0b3d966 100644 (file)
--- a/polyfix-cgi.hs
+++ b/polyfix-cgi.hs
@@ -3,7 +3,7 @@ module Main where
 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
@@ -16,6 +16,7 @@ import Language.Haskell.FreeTheorems
        , prettyUnfoldedLift
        , LanguageSubset(BasicSubset)
        )
+import Term2Expr (term2Expr, termCond2Exprs, insertTermsInCondition)
 
 import Network.CGI
 import Data.ByteString.Lazy.UTF8 (fromString)
@@ -23,6 +24,8 @@ import Text.XHtml
 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, " +++
@@ -55,7 +58,7 @@ generateResult typeStr typ = askDiv typeStr noHtml +++
        ) +++
        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 "+++
@@ -64,6 +67,16 @@ generateResult typeStr typ = askDiv typeStr noHtml +++
                        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
@@ -85,6 +98,7 @@ generateResult typeStr typ = askDiv typeStr noHtml +++
                    
        ft_simple = freeTheorem typ
         counter_example = getComplete' typ
+       counter_example_raw = getCompleteRaw typ
        
 main = runCGI (handleErrors cgiMain)