-module ExFindExtended (TypVar(..),Typ(..),TermVar(..),Term,TermCont,TermPlus,PlusElem(..),AbsTerm(..),testTerm,getTerm,getComplete,getComplete',getCompleteRaw,getWithDebug,getIt) where
+module ExFindExtended (TypVar(..),Typ(..),TermVar(..),Term,TermCont,TermPlus,PlusElem(..),AbsTerm(..),testTerm,getTerm,getComplete,showTerm,showUsedTermCont,getCompleteRaw,getWithDebug,getIt) where
import Prelude hiding (Either(..))
import qualified Prelude as E (Either(..))
}
}
-getComplete' :: Typ -> E.Either String (String, String)
-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."
| Lambda TypedExpr Expr
| Pair Expr Expr
| Map
- | ConstUnit
+ | Const Expr
+ | ELeft Expr
+ | ERight Expr
| CaseUnit Expr Expr
| EitherMap
| EUnit
equal' e1 e2 | (Just (lf,lv)) <- isFunctionApplication e1
, (Just (rf,rv)) <- isFunctionApplication e2
, lv == rv
+ , False
= equal' lf rf
-- This makes it return True...
| e1 == e2 = beTrue
-- Nothing left to optizmize
condition vars cond concl = Condition vars cond concl
+
+caseUnit Bottom e = Bottom
+caseUnit EUnit e = e
+caseUnit v e = CaseUnit v e
+
-- | Replaces a Term in a BoolExpr
replaceTermBE :: Expr -> Expr -> BoolExpr -> BoolExpr
replaceTermBE d r = go
go (Conc es) = foldr conc (Conc []) (map go es)
go (Lambda te e) = lambda' te (go e)
go (Pair e1 e2) = Pair (go e1) (go e2)
+ go (Const e) = Const (go e)
+ go (CaseUnit v e) = caseUnit (go v) (go e)
go e = e
show te1 ++ " " ++ show te2
app' :: Expr -> Expr -> Expr
+app' Bottom _ = Bottom -- _|_ x = _|_
+app' (Lambda tv e1) (e2) = replaceExpr (unTypeExpr tv) e2 e1 -- lambda application
app' Map (Conc []) = Conc [] -- map id = id
-app' ConstUnit _ = EUnit -- id x = x
+app' (Const e) _ = e -- const x y = x
app' (Conc []) v = v -- id x = x
app' f v = App f v
lambda tv e = TypedExpr (lambda' tv (unTypeExpr e)) (Arrow (typeOf tv) (typeOf e))
lambda' :: TypedExpr -> Expr -> Expr
-lambda' tv e | (Just e') <- isApplOn (unTypeExpr tv) e
+lambda' tv e | e == EUnit = Const EUnit
+ | (Just e') <- isApplOn (unTypeExpr tv) e
, not (unTypeExpr tv `occursIn` e')
= e'
| unTypeExpr tv == e = Conc []
| otherwise = Lambda tv e
conc :: Expr -> Expr -> Expr
-conc (Conc xs) (Conc ys) = Conc (xs ++ ys)
-conc (Conc xs) y = Conc (xs ++ [y])
-conc x (Conc ys) = Conc ([x] ++ ys)
-conc x y = Conc ([x,y])
+conc (Lambda v (CaseUnit v' e)) (Conc ((Const EUnit):r))
+ | unTypeExpr v == v' = conc (Const e) (Conc r)
+conc (Lambda v (CaseUnit v' e)) (Const EUnit) | unTypeExpr v == v' = Const e
+conc (Conc xs) (Conc ys) = Conc (xs ++ ys)
+conc (Conc xs) y = Conc (xs ++ [y])
+conc x (Conc ys) = Conc ([x] ++ ys)
+conc x y = Conc ([x,y])
-- Specialization of g'
specialize :: BoolExpr -> BoolExpr
specialize (TypeVarInst strict i be') =
- replaceTermBE (Var (FromTypVar i)) (if strict then Conc [] else ConstUnit) .
+ replaceTermBE (Var (FromTypVar i)) (if strict then Conc [] else Const EUnit) .
everywhere (mkT $ go) $
be
where be = specialize be'
showsPrec 0 e2
showsPrec _ EUnit = showString "()"
showsPrec _ Map = showString "map"
- showsPrec d ConstUnit = showParen (d>10) $ showString "const ()"
+ showsPrec d (ELeft e) = showParen (d>10) $
+ showString "Left ".
+ showsPrec 11 e
+ showsPrec d (ERight e) = showParen (d>10) $
+ showString "Right ".
+ showsPrec 11 e
+ showsPrec d (Const e) = showParen (d>10) $ showString "const ".showsPrec 11 e
showsPrec d (CaseUnit t1 t2) = showParen (d>5) $
showString "case " .
showsPrec 0 t1 .
import ParseType (parseType')
import SimpleFT (freeTheorem)
import Expr (specialize)
-import ExFindExtended (getComplete', getCompleteRaw)
+import ExFindExtended (getCompleteRaw, showTerm, showUsedTermCont)
import Language.Haskell.FreeTheorems.Parser.Haskell98 as FTP
import Language.Haskell.FreeTheorems
( runChecks
p << "Specializing relations to functions, canceling irrelvant terms and eta-reduction, this theorem can be written as:" +++
pre << show ft_simple +++
p << "Further specializing all types to (), all strict functions to id and all non-strict functions to const (), this theorem can be written as:" +++
- pre << show (specialize ft_simple)
+ pre << show ft_simple_special
) +++
maindiv << (
h3 << "The counter-example" +++
( case counter_example of
Left err -> p << "No term could be derived: " +++ pre << err
- Right (res,used) ->
+ Right result ->
p << ("By disregarding the strictness conditions for the chosen "+++
"relations, the following term is a counter example:" +++
- pre << ("f = " ++ res) ) +++
+ pre << ("f = " ++ showTerm (fst result)) ) +++
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)))
- ) +++
+ pre << uncurry showUsedTermCont result) +++
+ p << ("Inserting these defintions in the above theorem yields:" +++
+ -- p << (show result) +++
+ -- p << (show (term2Expr (fst result))) +++
+ -- p << (show (termCond2Exprs (snd result))) +++
+ pre << (show (insertTermsInCondition result ft_simple_special))
+ )
+ -- p << (gshow (insertTermsInCondition result (specialize ft_simple)))
+ )) +++
maindiv ( p << ("In the simplified theorems, the following custom haskell " +++
"functions might appear:") +++
pre << addDefs
else Left (unlines (map render es))
ft_simple = freeTheorem typ
- counter_example = getComplete' typ
- counter_example_raw = getCompleteRaw typ
+ ft_simple_special = specialize ft_simple
+ counter_example = getCompleteRaw typ
main = runCGI (handleErrors cgiMain)