{-# OPTIONS -w #-}

module Lambdabot.Plugin.Haskell.Free.FreeTheorem where

import Lambdabot.Plugin.Haskell.Free.Type
import Lambdabot.Plugin.Haskell.Free.Expr
import Lambdabot.Plugin.Haskell.Free.Theorem
import Lambdabot.Plugin.Haskell.Free.Parse
import Lambdabot.Plugin.Haskell.Free.Util

import Control.Monad
import Control.Monad.Fail (MonadFail)
import Control.Monad.State
import Control.Monad.Identity

import Data.Char
import qualified Data.Map as M

newtype MyState
    = MyState {
        MyState -> Int
myVSupply :: Int
    }

type MyMon a = StateT MyState Identity a

type TyEnv = [(TyVar,Var,TyVar,TyVar)]

makeVar :: String -> MyMon String
makeVar :: Var -> MyMon Var
makeVar Var
v
    = do
        vn <- (MyState -> Int) -> StateT MyState Identity Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets MyState -> Int
myVSupply
        modify (\MyState
s -> MyState
s { myVSupply = vn+1 })
        return (v ++ "_" ++ show vn)

extractTypes :: TyEnv -> Type -> (Type,Type)
extractTypes :: TyEnv -> Type -> (Type, Type)
extractTypes TyEnv
env (TyVar Var
v)
    = [(Type, Type)] -> (Type, Type)
forall a. HasCallStack => [a] -> a
head [ (Var -> Type
TyVar Var
t1,Var -> Type
TyVar Var
t2) | (Var
v',Var
_,Var
t1,Var
t2) <- TyEnv
env, Var
v Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
v' ]
extractTypes TyEnv
env (TyForall Var
v Type
t)
    = let (Type
t1,Type
t2) = TyEnv -> Type -> (Type, Type)
extractTypes ((Var
v,Var
forall a. HasCallStack => a
undefined,Var
v,Var
v)(Var, Var, Var, Var) -> TyEnv -> TyEnv
forall a. a -> [a] -> [a]
:TyEnv
env) Type
t
      in (Var -> Type -> Type
TyForall Var
v Type
t1, Var -> Type -> Type
TyForall Var
v Type
t2)
extractTypes TyEnv
env (TyArr Type
t1 Type
t2)
    = let (Type
t1a,Type
t1b) = TyEnv -> Type -> (Type, Type)
extractTypes TyEnv
env Type
t1
          (Type
t2a,Type
t2b) = TyEnv -> Type -> (Type, Type)
extractTypes TyEnv
env Type
t2
      in (Type -> Type -> Type
TyArr Type
t1a Type
t2a, Type -> Type -> Type
TyArr Type
t1b Type
t2b)
extractTypes TyEnv
env (TyTuple [Type]
ts)
    = let ts12 :: [(Type, Type)]
ts12 = (Type -> (Type, Type)) -> [Type] -> [(Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (TyEnv -> Type -> (Type, Type)
extractTypes TyEnv
env) [Type]
ts
      in ([Type] -> Type
TyTuple (((Type, Type) -> Type) -> [(Type, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Type) -> Type
forall a b. (a, b) -> a
fst [(Type, Type)]
ts12), [Type] -> Type
TyTuple (((Type, Type) -> Type) -> [(Type, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Type) -> Type
forall a b. (a, b) -> b
snd [(Type, Type)]
ts12))
extractTypes TyEnv
env (TyCons Var
c [Type]
ts)
    = let ts12 :: [(Type, Type)]
ts12 = (Type -> (Type, Type)) -> [Type] -> [(Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (TyEnv -> Type -> (Type, Type)
extractTypes TyEnv
env) [Type]
ts
      in (Var -> [Type] -> Type
TyCons Var
c (((Type, Type) -> Type) -> [(Type, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Type) -> Type
forall a b. (a, b) -> a
fst [(Type, Type)]
ts12), Var -> [Type] -> Type
TyCons Var
c (((Type, Type) -> Type) -> [(Type, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Type) -> Type
forall a b. (a, b) -> b
snd [(Type, Type)]
ts12))

freeTheoremStr :: (MonadFail m) => (String -> m String) -> String -> m String
freeTheoremStr :: forall (m :: * -> *). MonadFail m => (Var -> m Var) -> Var -> m Var
freeTheoremStr Var -> m Var
tf Var
s
    = case ParseS (Either (Var, Type) Var)
-> [Token] -> ParseResult (Either (Var, Type) Var)
forall a. ParseS a -> [Token] -> ParseResult a
parse (do
                    v <- ParseS (Maybe Token)
getToken ParseS (Maybe Token) -> (Maybe Token -> ParseS Var) -> ParseS Var
forall a b. ParseS a -> (a -> ParseS b) -> ParseS b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Maybe Token
v -> case Maybe Token
v of
                       Just (QVarId Var
v) -> Var -> ParseS Var
forall a. a -> ParseS a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
v
                       Maybe Token
_ -> Var -> ParseS Var
forall a. Var -> ParseS a
forall (m :: * -> *) a. MonadFail m => Var -> m a
fail Var
"Try `free <ident>` or `free <ident> :: <type>`"
                    (mplus (do match OpColonColon
                               t <- parseType
                               return $ Left (v,t))
                           (return (Right v)))) (Var -> [Token]
lexer Var
s) of
        ParseSuccess (Left (Var
v,Type
t)) [] -> Var -> m Var
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> Type -> Var
run' Var
v Type
t)
        ParseSuccess (Right Var
v)    [] -> do tStr <- Var -> m Var
tf Var
s
                                           case parse parseType (lexer tStr) of
                                             ParseSuccess Type
t [] -> Var -> m Var
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> Type -> Var
run' Var
v Type
t)
                                             ParseSuccess Type
_ [Token]
_ -> Var -> m Var
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> m Var) -> Var -> m Var
forall a b. (a -> b) -> a -> b
$ Var
"Extra stuff at end of line in retrieved type " Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Var -> Var
forall a. Show a => a -> Var
show Var
tStr
                                             ParseError Var
msg -> Var -> m Var
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
msg
        ParseSuccess Either (Var, Type) Var
_ [Token]
_      -> Var -> m Var
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
"Extra stuff at end of line"
        ParseError Var
msg        -> Var -> m Var
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
msg
    where
        run' :: Var -> Type -> Var
run' Var
v Type
t = Style -> Doc -> Var
renderStyle Style
defstyle (Theorem -> Doc
forall a. Pretty a => a -> Doc
pretty (Var -> Type -> Theorem
freeTheorem Var
v Type
t))
        defstyle :: Style
defstyle = Style {
                        mode :: Mode
mode = Mode
PageMode,
                        lineLength :: Int
lineLength = Int
78,
                        ribbonsPerLine :: Float
ribbonsPerLine = Float
1.5
                    }

freeTheorem :: String -> Type -> Theorem
freeTheorem :: Var -> Type -> Theorem
freeTheorem Var
name Type
t
    = Identity Theorem -> Theorem
forall a. Identity a -> a
runIdentity (Identity Theorem -> Theorem) -> Identity Theorem -> Theorem
forall a b. (a -> b) -> a -> b
$ do
        (th,_) <- StateT MyState Identity Theorem
-> MyState -> Identity (Theorem, MyState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (TyEnv -> Expr -> Expr -> Type -> StateT MyState Identity Theorem
freeTheorem' [] Expr
v0 Expr
v0 Type
t) MyState
initState
        let th' = Theorem -> Theorem
theoremSimplify Theorem
th
        return . fst $ runState (insertRn name name >> rename th') initRnSt
    where
        v0 :: Expr
v0 = Var -> Expr
EVar Var
name
        initState :: MyState
initState   = MyState { myVSupply :: Int
myVSupply = Int
1 }

------------------------------------------------------------------------
-- Rename monad, and pretty alpha renamer

data RnSt = RnSt { RnSt -> Map Var Var
gamma  :: M.Map Var Var
                 , RnSt -> [Var]
unique   :: [Var]
                 , RnSt -> [Var]
uniquelist :: [Var]
                 , RnSt -> [Var]
uniquefn :: [Var]
                 }
    deriving Int -> RnSt -> Var -> Var
[RnSt] -> Var -> Var
RnSt -> Var
(Int -> RnSt -> Var -> Var)
-> (RnSt -> Var) -> ([RnSt] -> Var -> Var) -> Show RnSt
forall a.
(Int -> a -> Var -> Var)
-> (a -> Var) -> ([a] -> Var -> Var) -> Show a
$cshowsPrec :: Int -> RnSt -> Var -> Var
showsPrec :: Int -> RnSt -> Var -> Var
$cshow :: RnSt -> Var
show :: RnSt -> Var
$cshowList :: [RnSt] -> Var -> Var
showList :: [RnSt] -> Var -> Var
Show

initRnSt :: RnSt
initRnSt
    = Map Var Var -> [Var] -> [Var] -> [Var] -> RnSt
RnSt Map Var Var
forall k a. Map k a
M.empty [Var]
suggestionsVal [Var]
suggestionsList [Var]
suggestionsFun
    where
        suggestionsVal :: [Var]
suggestionsVal = (Char -> Var) -> Var -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (Char -> Var -> Var
forall a. a -> [a] -> [a]
:[]) Var
"xyzuvabcstdeilmnorw"
                            [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [ Char
'x' Char -> Var -> Var
forall a. a -> [a] -> [a]
: Integer -> Var
forall a. Show a => a -> Var
show Integer
i | Integer
i <- [Integer
1..] ]
        suggestionsList :: [Var]
suggestionsList = (Char -> Var) -> Var -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (Char -> Var -> Var
forall a. a -> [a] -> [a]
:Var
"s") Var
"xyzuvabcstdeilmnorw"
                            [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [ Var
"xs" Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Integer -> Var
forall a. Show a => a -> Var
show Integer
i | Integer
i <- [Integer
1..] ]
        suggestionsFun :: [Var]
suggestionsFun = (Char -> Var) -> Var -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (Char -> Var -> Var
forall a. a -> [a] -> [a]
:[]) Var
"fghkpq"
                            [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [ Char
'f' Char -> Var -> Var
forall a. a -> [a] -> [a]
: Integer -> Var
forall a. Show a => a -> Var
show Integer
i | Integer
i <- [Integer
1..] ]

type RN a = State RnSt a

-- generate a nice fresh name
freshName :: RN Var
freshName :: RN Var
freshName = do
    s <- StateT RnSt Identity RnSt
forall s (m :: * -> *). MonadState s m => m s
get
    let ns    = RnSt -> [Var]
unique RnSt
s
        fresh = [Var] -> Var
forall a. HasCallStack => [a] -> a
head [Var]
ns
    put $ s { unique = tail ns }
    case M.lookup fresh (gamma s) of
        Maybe Var
Nothing -> Var -> RN Var
forall a. a -> StateT RnSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
fresh
        Maybe Var
_       -> RN Var
freshName

-- generate a nice function name
freshFunctionName :: RN Var
freshFunctionName :: RN Var
freshFunctionName = do
    s <- StateT RnSt Identity RnSt
forall s (m :: * -> *). MonadState s m => m s
get
    let ns    = RnSt -> [Var]
uniquefn RnSt
s
        fresh = [Var] -> Var
forall a. HasCallStack => [a] -> a
head [Var]
ns
    put $ s { uniquefn = tail ns }
    case M.lookup fresh (gamma s) of
        Maybe Var
Nothing -> Var -> RN Var
forall a. a -> StateT RnSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
fresh
        Maybe Var
_       -> RN Var
freshFunctionName

-- generate a nice list name
freshListName :: RN Var
freshListName :: RN Var
freshListName = do
    s <- StateT RnSt Identity RnSt
forall s (m :: * -> *). MonadState s m => m s
get
    let ns    = RnSt -> [Var]
uniquelist RnSt
s
        fresh = [Var] -> Var
forall a. HasCallStack => [a] -> a
head [Var]
ns
    put $ s { uniquelist = tail ns }
    case M.lookup fresh (gamma s) of
        Maybe Var
Nothing -> Var -> RN Var
forall a. a -> StateT RnSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
fresh
        Maybe Var
_       -> RN Var
freshListName

-- insert a new association into the heap
insertRn :: Var -> Var -> RN ()
insertRn :: Var -> Var -> RN ()
insertRn Var
old Var
new = (RnSt -> RnSt) -> RN ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((RnSt -> RnSt) -> RN ()) -> (RnSt -> RnSt) -> RN ()
forall a b. (a -> b) -> a -> b
$ \RnSt
s ->
    let gamma' :: Map Var Var
gamma' = Var -> Var -> Map Var Var -> Map Var Var
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Var
old Var
new (RnSt -> Map Var Var
gamma RnSt
s) in RnSt
s { gamma = gamma' }

-- lookup the binding
lookupRn :: Var -> RN Var
lookupRn :: Var -> RN Var
lookupRn Var
old = do
    m <- (RnSt -> Map Var Var) -> StateT RnSt Identity (Map Var Var)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets RnSt -> Map Var Var
gamma
    return $ case M.lookup old m of
        Maybe Var
Nothing  -> Var
old
        Just Var
new -> Var
new

-- alpha rename a simplified theory to something nice
rename :: Theorem -> RN Theorem
rename :: Theorem -> State RnSt Theorem
rename (ThImplies Theorem
th1 Theorem
th2) = do
    th1' <- Theorem -> State RnSt Theorem
rename Theorem
th1
    th2' <- rename th2
    return $ ThImplies th1' th2'

rename (ThEqual Expr
e1 Expr
e2) = do
    e1' <- Expr -> RN Expr
rnExp Expr
e1
    e2' <- rnExp e2
    return $ ThEqual e1' e2'

rename (ThAnd Theorem
th1 Theorem
th2) = do
    th1' <- Theorem -> State RnSt Theorem
rename Theorem
th1
    th2' <- rename th2
    return $ ThAnd th1' th2'

rename (ThForall Var
v Type
ty Theorem
th) = do
    v' <- case Type
ty of
                TyArr Type
_ Type
_     -> RN Var
freshFunctionName
                TyCons Var
"[]" [Type]
_ -> RN Var
freshListName
                Type
_             -> RN Var
freshName
    insertRn v v'
    ty' <- rnTy ty
    th' <- rename th
    return $ ThForall v' ty' th'

rnExp :: Expr -> RN Expr
rnExp :: Expr -> RN Expr
rnExp e :: Expr
e@(EBuiltin Builtin
_) = Expr -> RN Expr
forall a. a -> StateT RnSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
rnExp (EVar Var
v)       = Var -> Expr
EVar       (Var -> Expr) -> RN Var -> RN Expr
forall a b.
(a -> b) -> StateT RnSt Identity a -> StateT RnSt Identity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Var -> RN Var
lookupRn Var
v
rnExp (EVarOp Fixity
f Int
n Var
v) = Fixity -> Int -> Var -> Expr
EVarOp Fixity
f Int
n (Var -> Expr) -> RN Var -> RN Expr
forall a b.
(a -> b) -> StateT RnSt Identity a -> StateT RnSt Identity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Var -> RN Var
lookupRn Var
v

rnExp (EApp Expr
e1 Expr
e2) = do
    e1' <- Expr -> RN Expr
rnExp Expr
e1
    e2' <- rnExp e2
    return (EApp e1' e2')

rnExp (ETyApp Expr
e Type
ty) = do
    e'  <- Expr -> RN Expr
rnExp Expr
e
    ty' <- rnTy ty
    return (ETyApp e' ty')

rnTy :: Type -> RN Type
rnTy :: Type -> RN Type
rnTy Type
ty = Type -> RN Type
forall a. a -> StateT RnSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty

------------------------------------------------------------------------

freeTheorem' :: TyEnv -> Expr -> Expr -> Type -> MyMon Theorem

freeTheorem' :: TyEnv -> Expr -> Expr -> Type -> StateT MyState Identity Theorem
freeTheorem' TyEnv
env Expr
e1 Expr
e2 t' :: Type
t'@(TyForall Var
v Type
t)
    = do
        mv <- Var -> MyMon Var
makeVar Var
"f"
        t1 <- makeVar v
        t2 <- makeVar v
        let tymv = Type -> Type -> Type
TyArr (Var -> Type
TyVar Var
t1) (Var -> Type
TyVar Var
t2)
        pt <- freeTheorem' ((v,mv,t1,t2):env) (ETyApp e1 (TyVar t1))
                                              (ETyApp e2 (TyVar t2)) t
        return (ThForall mv tymv pt)

freeTheorem' TyEnv
env Expr
e1 Expr
e2 t' :: Type
t'@(TyArr Type
t1 Type
t2)
    = do
        mv1 <- Var -> MyMon Var
makeVar Var
"v1"
        mv2 <- makeVar "v2"
        let (tmv1,tmv2) = extractTypes env t1
        p1 <- freeTheorem' env (EVar mv1) (EVar mv2) t1
        p2 <- freeTheorem' env (EApp e1 (EVar mv1)) (EApp e2 (EVar mv2)) t2
        return (ThForall mv1 tmv1 (ThForall mv2 tmv2 (ThImplies p1 p2)))

freeTheorem' TyEnv
env Expr
e1 Expr
e2 t' :: Type
t'@(TyTuple [])
    = do
        Theorem -> StateT MyState Identity Theorem
forall a. a -> StateT MyState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Theorem
ThEqual Expr
e1 Expr
e2)

freeTheorem' TyEnv
env Expr
e1 Expr
e2 t' :: Type
t'@(TyTuple [Type]
ts)
    = do
        let len :: Int
len = [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts

        fts <- (Type -> StateT MyState Identity ((Var, Type), Theorem))
-> [Type] -> StateT MyState Identity [((Var, Type), Theorem)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Type
t -> do
                let (Type
t1,Type
t2) = TyEnv -> Type -> (Type, Type)
extractTypes TyEnv
env Type
t
                f <- Var -> MyMon Var
makeVar Var
"f"
                x <- makeVar "x"
                y <- makeVar "y"
                th <- freeTheorem' env (EVar x) (EVar y) t
                let eq = Expr -> Expr -> Theorem
ThEqual (Expr -> Expr -> Expr
EApp (Var -> Expr
EVar Var
f) (Var -> Expr
EVar Var
x)) (Var -> Expr
EVar Var
y)
                return ((f,TyArr t1 t2),
                        ThForall x t1 (
                            ThForall y t2 (
                                ThImplies th eq
                            )
                        )
                    )
            ) [Type]
ts
        let thf = Expr -> Expr -> Theorem
ThEqual (Expr -> Expr -> Expr
EApp ((Expr -> ((Var, Type), Theorem) -> Expr)
-> Expr -> [((Var, Type), Theorem)] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Expr
e ((Var
f,Type
_),Theorem
_) -> Expr -> Expr -> Expr
EApp Expr
e (Var -> Expr
EVar Var
f))
                            (Builtin -> Expr
EBuiltin (Builtin -> Expr) -> Builtin -> Expr
forall a b. (a -> b) -> a -> b
$ Int -> Builtin
BMapTuple Int
len) [((Var, Type), Theorem)]
fts) Expr
e1) Expr
e2
        return (foldr (\((Var
f,Type
t),Theorem
e1) Theorem
e2 -> Var -> Type -> Theorem -> Theorem
ThForall Var
f Type
t (Theorem -> Theorem -> Theorem
ThImplies Theorem
e1 Theorem
e2))
                thf fts)

freeTheorem' TyEnv
env Expr
e1 Expr
e2 t' :: Type
t'@(TyVar Var
v)
    = do
        let f :: Var
f = [Var] -> Var
forall a. HasCallStack => [a] -> a
head [ Var
f | (Var
v',Var
f,Var
_,Var
_) <- TyEnv
env, Var
v' Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
v ]
        Theorem -> StateT MyState Identity Theorem
forall a. a -> StateT MyState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Theorem
ThEqual (Expr -> Expr -> Expr
EApp (Var -> Expr
EVar Var
f) Expr
e1) Expr
e2)

freeTheorem' TyEnv
env Expr
e1 Expr
e2 t' :: Type
t'@(TyCons Var
_ [])
    = do
        Theorem -> StateT MyState Identity Theorem
forall a. a -> StateT MyState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Theorem
ThEqual Expr
e1 Expr
e2)

freeTheorem' TyEnv
env Expr
e1 Expr
e2 t' :: Type
t'@(TyCons Var
c [Type
t])
    = do
        f <- Var -> MyMon Var
makeVar Var
"f"
        x <- makeVar "x"
        y <- makeVar "y"
        let (t1,t2) = extractTypes env t
        p1 <- freeTheorem' env (EVar x) (EVar y) t
        let p2 = Expr -> Expr -> Theorem
ThEqual (Expr -> Expr -> Expr
EApp (Var -> Expr
EVar Var
f) (Var -> Expr
EVar Var
x)) (Var -> Expr
EVar Var
y)
        let p3 = Expr -> Expr -> Theorem
ThEqual (Expr -> Expr -> Expr
EApp (Expr -> Expr -> Expr
EApp (Builtin -> Expr
EBuiltin (Var -> Builtin
BMap Var
c)) (Var -> Expr
EVar Var
f)) Expr
e1) Expr
e2
        return (ThForall f (TyArr t1 t2) (
                ThImplies (ThForall x t1 (ThForall y t2 (ThImplies p1 p2)))
                            p3))

freeTheorem' TyEnv
env Expr
e1 Expr
e2 t' :: Type
t'@(TyCons c :: Var
c@Var
"Either" ts :: [Type]
ts@[Type
_,Type
_])
    = do
        fts <- (Type -> StateT MyState Identity ((Var, Type), Theorem))
-> [Type] -> StateT MyState Identity [((Var, Type), Theorem)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Type
t -> do
                let (Type
t1,Type
t2) = TyEnv -> Type -> (Type, Type)
extractTypes TyEnv
env Type
t
                f <- Var -> MyMon Var
makeVar Var
"f"
                x <- makeVar "x"
                y <- makeVar "y"
                th <- freeTheorem' env (EVar x) (EVar y) t
                let eq = Expr -> Expr -> Theorem
ThEqual (Expr -> Expr -> Expr
EApp (Var -> Expr
EVar Var
f) (Var -> Expr
EVar Var
x)) (Var -> Expr
EVar Var
y)
                return ((f,TyArr t1 t2),
                        ThForall x t1 (
                            ThForall y t2 (
                                ThImplies th eq
                            )
                        )
                    )
            ) [Type]
ts
        let thf = Expr -> Expr -> Theorem
ThEqual (Expr -> Expr -> Expr
EApp ((Expr -> ((Var, Type), Theorem) -> Expr)
-> Expr -> [((Var, Type), Theorem)] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Expr
e ((Var
f,Type
_),Theorem
_) -> Expr -> Expr -> Expr
EApp Expr
e (Var -> Expr
EVar Var
f))
                            (Builtin -> Expr
EBuiltin (Builtin -> Expr) -> Builtin -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Builtin
BMap Var
c) [((Var, Type), Theorem)]
fts) Expr
e1) Expr
e2
        return (foldr (\((Var
f,Type
t),Theorem
e1) Theorem
e2 -> Var -> Type -> Theorem -> Theorem
ThForall Var
f Type
t (Theorem -> Theorem -> Theorem
ThImplies Theorem
e1 Theorem
e2))
                thf fts)

freeTheorem' TyEnv
env Expr
e1 Expr
e2 t' :: Type
t'@Type
_ = Var -> StateT MyState Identity Theorem
forall a. HasCallStack => Var -> a
error Var
"Sorry, this type is too difficult for me."

-- vim: ts=4:sts=4:expandtab:ai