{-# 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 <- (MyState -> Int) -> StateT MyState Identity Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets MyState -> Int
myVSupply
        (MyState -> MyState) -> StateT MyState Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\MyState
s -> MyState
s { myVSupply :: Int
myVSupply = Int
vnInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1 })
        Var -> MyMon Var
forall (m :: * -> *) a. Monad m => a -> m a
return (Var
v Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Var
"_" Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Int -> Var
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)
    = [(Type, Type)] -> (Type, Type)
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 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
                    Var
v <- ParseS (Maybe Token)
getToken ParseS (Maybe Token) -> (Maybe Token -> ParseS Var) -> ParseS Var
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 (m :: * -> *) a. Monad m => a -> m a
return Var
v
                       Maybe Token
_ -> Var -> ParseS Var
forall (m :: * -> *) a. MonadFail m => Var -> m a
fail Var
"Try `free <ident>` or `free <ident> :: <type>`"
                    (ParseS (Either (Var, Type) Var)
-> ParseS (Either (Var, Type) Var)
-> ParseS (Either (Var, Type) Var)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (do Token -> ParseS ()
match Token
OpColonColon
                               Type
t <- ParseS Type
parseType
                               Either (Var, Type) Var -> ParseS (Either (Var, Type) Var)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Var, Type) Var -> ParseS (Either (Var, Type) Var))
-> Either (Var, Type) Var -> ParseS (Either (Var, Type) Var)
forall a b. (a -> b) -> a -> b
$ (Var, Type) -> Either (Var, Type) Var
forall a b. a -> Either a b
Left (Var
v,Type
t))
                           (Either (Var, Type) Var -> ParseS (Either (Var, Type) Var)
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> Either (Var, Type) Var
forall a b. b -> Either a b
Right Var
v)))) (Var -> [Token]
lexer Var
s) of
        ParseSuccess (Left (Var
v,Type
t)) [] -> Var -> m Var
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 ParseS Type -> [Token] -> ParseResult Type
forall a. ParseS a -> [Token] -> ParseResult a
parse ParseS Type
parseType (Var -> [Token]
lexer Var
tStr) of
                                             ParseSuccess Type
t [] -> Var -> m Var
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> Type -> Var
run' Var
v Type
t)
                                             ParseSuccess Type
_ [Token]
_ -> Var -> m Var
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 (m :: * -> *) a. Monad m => a -> m a
return Var
msg
        ParseSuccess Either (Var, Type) Var
_ [Token]
_      -> Var -> m Var
forall (m :: * -> *) a. Monad m => a -> m a
return Var
"Extra stuff at end of line"
        ParseError Var
msg        -> Var -> m Var
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 -> Int -> Float -> Style
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
        (Theorem
th,MyState
_) <- 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
th' = Theorem -> Theorem
theoremSimplify Theorem
th
        Theorem -> Identity Theorem
forall (m :: * -> *) a. Monad m => a -> m a
return (Theorem -> Identity Theorem)
-> ((Theorem, RnSt) -> Theorem)
-> (Theorem, RnSt)
-> Identity Theorem
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Theorem, RnSt) -> Theorem
forall a b. (a, b) -> a
fst ((Theorem, RnSt) -> Identity Theorem)
-> (Theorem, RnSt) -> Identity Theorem
forall a b. (a -> b) -> a -> b
$ State RnSt Theorem -> RnSt -> (Theorem, RnSt)
forall s a. State s a -> s -> (a, s)
runState (Var -> Var -> RN ()
insertRn Var
name Var
name RN () -> State RnSt Theorem -> State RnSt Theorem
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Theorem -> State RnSt Theorem
rename Theorem
th') RnSt
initRnSt
    where
        v0 :: Expr
v0 = Var -> Expr
EVar Var
name
        initState :: MyState
initState   = MyState :: Int -> MyState
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
showList :: [RnSt] -> Var -> Var
$cshowList :: [RnSt] -> Var -> Var
show :: RnSt -> Var
$cshow :: RnSt -> Var
showsPrec :: Int -> RnSt -> Var -> Var
$cshowsPrec :: Int -> 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
    RnSt
s <- StateT RnSt Identity RnSt
forall s (m :: * -> *). MonadState s m => m s
get
    let ns :: [Var]
ns    = RnSt -> [Var]
unique RnSt
s
        fresh :: Var
fresh = [Var] -> Var
forall a. [a] -> a
head [Var]
ns
    RnSt -> RN ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (RnSt -> RN ()) -> RnSt -> RN ()
forall a b. (a -> b) -> a -> b
$ RnSt
s { unique :: [Var]
unique = [Var] -> [Var]
forall a. [a] -> [a]
tail [Var]
ns }
    case Var -> Map Var Var -> Maybe Var
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 -> Var -> RN Var
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 <- StateT RnSt Identity RnSt
forall s (m :: * -> *). MonadState s m => m s
get
    let ns :: [Var]
ns    = RnSt -> [Var]
uniquefn RnSt
s
        fresh :: Var
fresh = [Var] -> Var
forall a. [a] -> a
head [Var]
ns
    RnSt -> RN ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (RnSt -> RN ()) -> RnSt -> RN ()
forall a b. (a -> b) -> a -> b
$ RnSt
s { uniquefn :: [Var]
uniquefn = [Var] -> [Var]
forall a. [a] -> [a]
tail [Var]
ns }
    case Var -> Map Var Var -> Maybe Var
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 -> Var -> RN Var
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 <- StateT RnSt Identity RnSt
forall s (m :: * -> *). MonadState s m => m s
get
    let ns :: [Var]
ns    = RnSt -> [Var]
uniquelist RnSt
s
        fresh :: Var
fresh = [Var] -> Var
forall a. [a] -> a
head [Var]
ns
    RnSt -> RN ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (RnSt -> RN ()) -> RnSt -> RN ()
forall a b. (a -> b) -> a -> b
$ RnSt
s { uniquelist :: [Var]
uniquelist = [Var] -> [Var]
forall a. [a] -> [a]
tail [Var]
ns }
    case Var -> Map Var Var -> Maybe Var
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 -> Var -> RN Var
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 :: 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 <- (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
    Var -> RN Var
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> RN Var) -> Var -> RN Var
forall a b. (a -> b) -> a -> b
$ case Var -> Map Var Var -> Maybe Var
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 -> State RnSt Theorem
rename (ThImplies Theorem
th1 Theorem
th2) = do
    Theorem
th1' <- Theorem -> State RnSt Theorem
rename Theorem
th1
    Theorem
th2' <- Theorem -> State RnSt Theorem
rename Theorem
th2
    Theorem -> State RnSt Theorem
forall (m :: * -> *) a. Monad m => a -> m a
return (Theorem -> State RnSt Theorem) -> Theorem -> State RnSt Theorem
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
    Theorem -> State RnSt Theorem
forall (m :: * -> *) a. Monad m => a -> m a
return (Theorem -> State RnSt Theorem) -> Theorem -> State RnSt Theorem
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 -> State RnSt Theorem
rename Theorem
th1
    Theorem
th2' <- Theorem -> State RnSt Theorem
rename Theorem
th2
    Theorem -> State RnSt Theorem
forall (m :: * -> *) a. Monad m => a -> m a
return (Theorem -> State RnSt Theorem) -> Theorem -> State RnSt Theorem
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 -> State RnSt Theorem
rename Theorem
th
    Theorem -> State RnSt Theorem
forall (m :: * -> *) a. Monad m => a -> m a
return (Theorem -> State RnSt Theorem) -> Theorem -> State RnSt Theorem
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
_) = Expr -> RN Expr
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 (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 (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
    Expr -> RN Expr
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
    Expr -> RN Expr
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 = Type -> RN Type
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
        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 -> StateT MyState Identity Theorem
freeTheorem' ((Var
v,Var
mv,Var
t1,Var
t2)(Var, Var, Var, Var) -> TyEnv -> TyEnv
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
        Theorem -> StateT MyState Identity Theorem
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 -> StateT MyState Identity Theorem
freeTheorem' TyEnv
env (Var -> Expr
EVar Var
mv1) (Var -> Expr
EVar Var
mv2) Type
t1
        Theorem
p2 <- TyEnv -> Expr -> Expr -> Type -> StateT MyState Identity 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
        Theorem -> StateT MyState Identity Theorem
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
        Theorem -> StateT MyState Identity Theorem
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 (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts

        [((Var, Type), Theorem)]
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)
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 -> StateT MyState Identity 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)
                ((Var, Type), Theorem)
-> StateT MyState Identity ((Var, Type), Theorem)
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 ((Expr -> ((Var, Type), Theorem) -> Expr)
-> Expr -> [((Var, Type), Theorem)] -> Expr
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
        Theorem -> StateT MyState Identity Theorem
forall (m :: * -> *) a. Monad m => a -> m a
return ((((Var, Type), Theorem) -> Theorem -> Theorem)
-> Theorem -> [((Var, Type), Theorem)] -> Theorem
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 = [Var] -> Var
forall a. [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 (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 (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 -> StateT MyState Identity 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
        Theorem -> StateT MyState Identity Theorem
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 <- (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)
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 -> StateT MyState Identity 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)
                ((Var, Type), Theorem)
-> StateT MyState Identity ((Var, Type), Theorem)
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 ((Expr -> ((Var, Type), Theorem) -> Expr)
-> Expr -> [((Var, Type), Theorem)] -> Expr
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
        Theorem -> StateT MyState Identity Theorem
forall (m :: * -> *) a. Monad m => a -> m a
return ((((Var, Type), Theorem) -> Theorem -> Theorem)
-> Theorem -> [((Var, Type), Theorem)] -> Theorem
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
_ = 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