{-# 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
        Int
vn <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets MyState -> Int
myVSupply
        forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\MyState
s -> MyState
s { myVSupply :: Int
myVSupply = Int
vnforall a. Num a => a -> a -> a
+Int
1 })
        forall (m :: * -> *) a. Monad m => a -> m a
return (Var
v forall a. [a] -> [a] -> [a]
++ Var
"_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Var
show Int
vn)

extractTypes :: TyEnv -> Type -> (Type,Type)
extractTypes :: TyEnv -> Type -> (Type, Type)
extractTypes TyEnv
env (TyVar Var
v)
    = forall a. [a] -> a
head [ (Var -> Type
TyVar Var
t1,Var -> Type
TyVar Var
t2) | (Var
v',Var
_,Var
t1,Var
t2) <- TyEnv
env, Var
v 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,forall a. HasCallStack => a
undefined,Var
v,Var
v)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 = forall a b. (a -> b) -> [a] -> [b]
map (TyEnv -> Type -> (Type, Type)
extractTypes TyEnv
env) [Type]
ts
      in ([Type] -> Type
TyTuple (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Type, Type)]
ts12), [Type] -> Type
TyTuple (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Type, Type)]
ts12))
extractTypes TyEnv
env (TyCons Var
c [Type]
ts)
    = let ts12 :: [(Type, Type)]
ts12 = forall a b. (a -> b) -> [a] -> [b]
map (TyEnv -> Type -> (Type, Type)
extractTypes TyEnv
env) [Type]
ts
      in (Var -> [Type] -> Type
TyCons Var
c (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Type, Type)]
ts12), Var -> [Type] -> Type
TyCons Var
c (forall a b. (a -> b) -> [a] -> [b]
map 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 forall a. ParseS a -> [Token] -> ParseResult a
parse (do
                    Var
v <- ParseS (Maybe Token)
getToken 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) -> forall (m :: * -> *) a. Monad m => a -> m a
return Var
v
                       Maybe Token
_ -> forall (m :: * -> *) a. MonadFail m => Var -> m a
fail Var
"Try `free <ident>` or `free <ident> :: <type>`"
                    (forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (do Token -> ParseS ()
match Token
OpColonColon
                               Type
t <- ParseS Type
parseType
                               forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (Var
v,Type
t))
                           (forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right Var
v)))) (Var -> [Token]
lexer Var
s) of
        ParseSuccess (Left (Var
v,Type
t)) [] -> forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> Type -> Var
run' Var
v Type
t)
        ParseSuccess (Right Var
v)    [] -> do Var
tStr <- Var -> m Var
tf Var
s
                                           case forall a. ParseS a -> [Token] -> ParseResult a
parse ParseS Type
parseType (Var -> [Token]
lexer Var
tStr) of
                                             ParseSuccess Type
t [] -> forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> Type -> Var
run' Var
v Type
t)
                                             ParseSuccess Type
_ [Token]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Var
"Extra stuff at end of line in retrieved type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Var
show Var
tStr
                                             ParseError Var
msg -> forall (m :: * -> *) a. Monad m => a -> m a
return Var
msg
        ParseSuccess Either (Var, Type) Var
_ [Token]
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return Var
"Extra stuff at end of line"
        ParseError Var
msg        -> 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 (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
    = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ do
        (Theorem
th,MyState
_) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (TyEnv -> Expr -> Expr -> Type -> MyMon Theorem
freeTheorem' [] Expr
v0 Expr
v0 Type
t) MyState
initState
        let th' :: Theorem
th' = Theorem -> Theorem
theoremSimplify Theorem
th
        forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall s a. State s a -> s -> (a, s)
runState (Var -> Var -> RN ()
insertRn Var
name Var
name forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Theorem -> StateT RnSt Identity Theorem
rename Theorem
th') RnSt
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 -> ShowS
[RnSt] -> ShowS
RnSt -> Var
forall a.
(Int -> a -> ShowS) -> (a -> Var) -> ([a] -> ShowS) -> Show a
showList :: [RnSt] -> ShowS
$cshowList :: [RnSt] -> ShowS
show :: RnSt -> Var
$cshow :: RnSt -> Var
showsPrec :: Int -> RnSt -> ShowS
$cshowsPrec :: Int -> RnSt -> ShowS
Show

initRnSt :: RnSt
initRnSt
    = Map Var Var -> [Var] -> [Var] -> [Var] -> RnSt
RnSt forall k a. Map k a
M.empty [Var]
suggestionsVal [Var]
suggestionsList [Var]
suggestionsFun
    where
        suggestionsVal :: [Var]
suggestionsVal = forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> [a] -> [a]
:[]) Var
"xyzuvabcstdeilmnorw"
                            forall a. [a] -> [a] -> [a]
++ [ Char
'x' forall a. a -> [a] -> [a]
: forall a. Show a => a -> Var
show Integer
i | Integer
i <- [Integer
1..] ]
        suggestionsList :: [Var]
suggestionsList = forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> [a] -> [a]
:Var
"s") Var
"xyzuvabcstdeilmnorw"
                            forall a. [a] -> [a] -> [a]
++ [ Var
"xs" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Var
show Integer
i | Integer
i <- [Integer
1..] ]
        suggestionsFun :: [Var]
suggestionsFun = forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> [a] -> [a]
:[]) Var
"fghkpq"
                            forall a. [a] -> [a] -> [a]
++ [ Char
'f' forall a. a -> [a] -> [a]
: 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
    RnSt
s <- forall s (m :: * -> *). MonadState s m => m s
get
    let ns :: [Var]
ns    = RnSt -> [Var]
unique RnSt
s
        fresh :: Var
fresh = forall a. [a] -> a
head [Var]
ns
    forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ RnSt
s { unique :: [Var]
unique = forall a. [a] -> [a]
tail [Var]
ns }
    case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
fresh (RnSt -> Map Var Var
gamma RnSt
s) of
        Maybe Var
Nothing -> 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
    RnSt
s <- forall s (m :: * -> *). MonadState s m => m s
get
    let ns :: [Var]
ns    = RnSt -> [Var]
uniquefn RnSt
s
        fresh :: Var
fresh = forall a. [a] -> a
head [Var]
ns
    forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ RnSt
s { uniquefn :: [Var]
uniquefn = forall a. [a] -> [a]
tail [Var]
ns }
    case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
fresh (RnSt -> Map Var Var
gamma RnSt
s) of
        Maybe Var
Nothing -> 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
    RnSt
s <- forall s (m :: * -> *). MonadState s m => m s
get
    let ns :: [Var]
ns    = RnSt -> [Var]
uniquelist RnSt
s
        fresh :: Var
fresh = forall a. [a] -> a
head [Var]
ns
    forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ RnSt
s { uniquelist :: [Var]
uniquelist = forall a. [a] -> [a]
tail [Var]
ns }
    case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
fresh (RnSt -> Map Var Var
gamma RnSt
s) of
        Maybe Var
Nothing -> 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 = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \RnSt
s ->
    let gamma' :: Map Var Var
gamma' = 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 :: Map Var Var
gamma = Map Var Var
gamma' }

-- lookup the binding
lookupRn :: Var -> RN Var
lookupRn :: Var -> RN Var
lookupRn Var
old = do
    Map Var Var
m <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets RnSt -> Map Var Var
gamma
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
old Map Var Var
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 -> StateT RnSt Identity Theorem
rename (ThImplies Theorem
th1 Theorem
th2) = do
    Theorem
th1' <- Theorem -> StateT RnSt Identity Theorem
rename Theorem
th1
    Theorem
th2' <- Theorem -> StateT RnSt Identity Theorem
rename Theorem
th2
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Theorem -> Theorem -> Theorem
ThImplies Theorem
th1' Theorem
th2'

rename (ThEqual Expr
e1 Expr
e2) = do
    Expr
e1' <- Expr -> RN Expr
rnExp Expr
e1
    Expr
e2' <- Expr -> RN Expr
rnExp Expr
e2
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Theorem
ThEqual Expr
e1' Expr
e2'

rename (ThAnd Theorem
th1 Theorem
th2) = do
    Theorem
th1' <- Theorem -> StateT RnSt Identity Theorem
rename Theorem
th1
    Theorem
th2' <- Theorem -> StateT RnSt Identity Theorem
rename Theorem
th2
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Theorem -> Theorem -> Theorem
ThAnd Theorem
th1' Theorem
th2'

rename (ThForall Var
v Type
ty Theorem
th) = do
    Var
v' <- case Type
ty of
                TyArr Type
_ Type
_     -> RN Var
freshFunctionName
                TyCons Var
"[]" [Type]
_ -> RN Var
freshListName
                Type
_             -> RN Var
freshName
    Var -> Var -> RN ()
insertRn Var
v Var
v'
    Type
ty' <- Type -> RN Type
rnTy Type
ty
    Theorem
th' <- Theorem -> StateT RnSt Identity Theorem
rename Theorem
th
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Var -> Type -> Theorem -> Theorem
ThForall Var
v' Type
ty' Theorem
th'

rnExp :: Expr -> RN Expr
rnExp :: Expr -> RN Expr
rnExp e :: Expr
e@(EBuiltin Builtin
_) = forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
rnExp (EVar Var
v)       = Var -> Expr
EVar       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 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
    Expr
e1' <- Expr -> RN Expr
rnExp Expr
e1
    Expr
e2' <- Expr -> RN Expr
rnExp Expr
e2
    forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr
EApp Expr
e1' Expr
e2')

rnExp (ETyApp Expr
e Type
ty) = do
    Expr
e'  <- Expr -> RN Expr
rnExp Expr
e
    Type
ty' <- Type -> RN Type
rnTy Type
ty
    forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Type -> Expr
ETyApp Expr
e' Type
ty')

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

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

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

freeTheorem' :: TyEnv -> Expr -> Expr -> Type -> MyMon Theorem
freeTheorem' TyEnv
env Expr
e1 Expr
e2 t' :: Type
t'@(TyForall Var
v Type
t)
    = do
        Var
mv <- Var -> MyMon Var
makeVar Var
"f"
        Var
t1 <- Var -> MyMon Var
makeVar Var
v
        Var
t2 <- Var -> MyMon Var
makeVar Var
v
        let tymv :: Type
tymv = Type -> Type -> Type
TyArr (Var -> Type
TyVar Var
t1) (Var -> Type
TyVar Var
t2)
        Theorem
pt <- TyEnv -> Expr -> Expr -> Type -> MyMon Theorem
freeTheorem' ((Var
v,Var
mv,Var
t1,Var
t2)forall a. a -> [a] -> [a]
:TyEnv
env) (Expr -> Type -> Expr
ETyApp Expr
e1 (Var -> Type
TyVar Var
t1))
                                              (Expr -> Type -> Expr
ETyApp Expr
e2 (Var -> Type
TyVar Var
t2)) Type
t
        forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> Type -> Theorem -> Theorem
ThForall Var
mv Type
tymv Theorem
pt)

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

freeTheorem' TyEnv
env Expr
e1 Expr
e2 t' :: Type
t'@(TyTuple [])
    = do
        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 = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts

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

freeTheorem' TyEnv
env Expr
e1 Expr
e2 t' :: Type
t'@(TyVar Var
v)
    = do
        let f :: Var
f = forall a. [a] -> a
head [ Var
f | (Var
v',Var
f,Var
_,Var
_) <- TyEnv
env, Var
v' forall a. Eq a => a -> a -> Bool
== Var
v ]
        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
        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
        Var
f <- Var -> MyMon Var
makeVar Var
"f"
        Var
x <- Var -> MyMon Var
makeVar Var
"x"
        Var
y <- Var -> MyMon Var
makeVar Var
"y"
        let (Type
t1,Type
t2) = TyEnv -> Type -> (Type, Type)
extractTypes TyEnv
env Type
t
        Theorem
p1 <- TyEnv -> Expr -> Expr -> Type -> MyMon Theorem
freeTheorem' TyEnv
env (Var -> Expr
EVar Var
x) (Var -> Expr
EVar Var
y) Type
t
        let p2 :: Theorem
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 :: Theorem
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
        forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> Type -> Theorem -> Theorem
ThForall Var
f (Type -> Type -> Type
TyArr Type
t1 Type
t2) (
                Theorem -> Theorem -> Theorem
ThImplies (Var -> Type -> Theorem -> Theorem
ThForall Var
x Type
t1 (Var -> Type -> Theorem -> Theorem
ThForall Var
y Type
t2 (Theorem -> Theorem -> Theorem
ThImplies Theorem
p1 Theorem
p2)))
                            Theorem
p3))

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

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

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