{-# 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 :: String -> MyMon String
makeVar String
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 })
        String -> MyMon String
forall (m :: * -> *) a. Monad m => a -> m a
return (String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
vn)

extractTypes :: TyEnv -> Type -> (Type,Type)
extractTypes :: TyEnv -> Type -> (Type, Type)
extractTypes TyEnv
env (TyVar String
v)
    = [(Type, Type)] -> (Type, Type)
forall a. [a] -> a
head [ (String -> Type
TyVar String
t1,String -> Type
TyVar String
t2) | (String
v',String
_,String
t1,String
t2) <- TyEnv
env, String
v String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
v' ]
extractTypes TyEnv
env (TyForall String
v Type
t)
    = let (Type
t1,Type
t2) = TyEnv -> Type -> (Type, Type)
extractTypes ((String
v,String
forall a. HasCallStack => a
undefined,String
v,String
v)(String, String, String, String) -> TyEnv -> TyEnv
forall a. a -> [a] -> [a]
:TyEnv
env) Type
t
      in (String -> Type -> Type
TyForall String
v Type
t1, String -> Type -> Type
TyForall String
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 String
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 (String -> [Type] -> Type
TyCons String
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), String -> [Type] -> Type
TyCons String
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 :: (String -> m String) -> String -> m String
freeTheoremStr String -> m String
tf String
s
    = case ParseS (Either (String, Type) String)
-> [Token] -> ParseResult (Either (String, Type) String)
forall a. ParseS a -> [Token] -> ParseResult a
parse (do
                    String
v <- ParseS (Maybe Token)
getToken ParseS (Maybe Token)
-> (Maybe Token -> ParseS String) -> ParseS String
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Maybe Token
v -> case Maybe Token
v of
                       Just (QVarId String
v) -> String -> ParseS String
forall (m :: * -> *) a. Monad m => a -> m a
return String
v
                       Maybe Token
_ -> String -> ParseS String
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Try `free <ident>` or `free <ident> :: <type>`"
                    (ParseS (Either (String, Type) String)
-> ParseS (Either (String, Type) String)
-> ParseS (Either (String, Type) String)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (do Token -> ParseS ()
match Token
OpColonColon
                               Type
t <- ParseS Type
parseType
                               Either (String, Type) String
-> ParseS (Either (String, Type) String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (String, Type) String
 -> ParseS (Either (String, Type) String))
-> Either (String, Type) String
-> ParseS (Either (String, Type) String)
forall a b. (a -> b) -> a -> b
$ (String, Type) -> Either (String, Type) String
forall a b. a -> Either a b
Left (String
v,Type
t))
                           (Either (String, Type) String
-> ParseS (Either (String, Type) String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Either (String, Type) String
forall a b. b -> Either a b
Right String
v)))) (String -> [Token]
lexer String
s) of
        ParseSuccess (Left (String
v,Type
t)) [] -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Type -> String
run' String
v Type
t)
        ParseSuccess (Right String
v)    [] -> do String
tStr <- String -> m String
tf String
s
                                           case ParseS Type -> [Token] -> ParseResult Type
forall a. ParseS a -> [Token] -> ParseResult a
parse ParseS Type
parseType (String -> [Token]
lexer String
tStr) of
                                             ParseSuccess Type
t [] -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Type -> String
run' String
v Type
t)
                                             ParseSuccess Type
_ [Token]
_ -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ String
"Extra stuff at end of line in retrieved type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
tStr
                                             ParseError String
msg -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return String
msg
        ParseSuccess Either (String, Type) String
_ [Token]
_      -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return String
"Extra stuff at end of line"
        ParseError String
msg        -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return String
msg
    where
        run' :: String -> Type -> String
run' String
v Type
t = Style -> Doc -> String
renderStyle Style
defstyle (Theorem -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Type -> Theorem
freeTheorem String
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 :: String -> Type -> Theorem
freeTheorem String
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 (String -> String -> RN ()
insertRn String
name String
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 = String -> Expr
EVar String
name
        initState :: MyState
initState   = MyState :: Int -> MyState
MyState { myVSupply :: Int
myVSupply = Int
1 }

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

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

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

type RN a = State RnSt a

-- generate a nice fresh name
freshName :: RN Var
freshName :: RN String
freshName = do
    RnSt
s <- StateT RnSt Identity RnSt
forall s (m :: * -> *). MonadState s m => m s
get
    let ns :: [String]
ns    = RnSt -> [String]
unique RnSt
s
        fresh :: String
fresh = [String] -> String
forall a. [a] -> a
head [String]
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 :: [String]
unique = [String] -> [String]
forall a. [a] -> [a]
tail [String]
ns }
    case String -> Map String String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
fresh (RnSt -> Map String String
gamma RnSt
s) of
        Maybe String
Nothing -> String -> RN String
forall (m :: * -> *) a. Monad m => a -> m a
return String
fresh
        Maybe String
_       -> RN String
freshName

-- generate a nice function name
freshFunctionName :: RN Var
freshFunctionName :: RN String
freshFunctionName = do
    RnSt
s <- StateT RnSt Identity RnSt
forall s (m :: * -> *). MonadState s m => m s
get
    let ns :: [String]
ns    = RnSt -> [String]
uniquefn RnSt
s
        fresh :: String
fresh = [String] -> String
forall a. [a] -> a
head [String]
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 :: [String]
uniquefn = [String] -> [String]
forall a. [a] -> [a]
tail [String]
ns }
    case String -> Map String String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
fresh (RnSt -> Map String String
gamma RnSt
s) of
        Maybe String
Nothing -> String -> RN String
forall (m :: * -> *) a. Monad m => a -> m a
return String
fresh
        Maybe String
_       -> RN String
freshFunctionName

-- generate a nice list name
freshListName :: RN Var
freshListName :: RN String
freshListName = do
    RnSt
s <- StateT RnSt Identity RnSt
forall s (m :: * -> *). MonadState s m => m s
get
    let ns :: [String]
ns    = RnSt -> [String]
uniquelist RnSt
s
        fresh :: String
fresh = [String] -> String
forall a. [a] -> a
head [String]
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 :: [String]
uniquelist = [String] -> [String]
forall a. [a] -> [a]
tail [String]
ns }
    case String -> Map String String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
fresh (RnSt -> Map String String
gamma RnSt
s) of
        Maybe String
Nothing -> String -> RN String
forall (m :: * -> *) a. Monad m => a -> m a
return String
fresh
        Maybe String
_       -> RN String
freshListName

-- insert a new association into the heap
insertRn :: Var -> Var -> RN ()
insertRn :: String -> String -> RN ()
insertRn String
old String
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 String String
gamma' = String -> String -> Map String String -> Map String String
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert String
old String
new (RnSt -> Map String String
gamma RnSt
s) in RnSt
s { gamma :: Map String String
gamma = Map String String
gamma' }

-- lookup the binding
lookupRn :: Var -> RN Var
lookupRn :: String -> RN String
lookupRn String
old = do
    Map String String
m <- (RnSt -> Map String String)
-> StateT RnSt Identity (Map String String)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets RnSt -> Map String String
gamma
    String -> RN String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> RN String) -> String -> RN String
forall a b. (a -> b) -> a -> b
$ case String -> Map String String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
old Map String String
m of
        Maybe String
Nothing  -> String
old
        Just String
new -> String
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 String
v Type
ty Theorem
th) = do
    String
v' <- case Type
ty of
                TyArr Type
_ Type
_     -> RN String
freshFunctionName
                TyCons String
"[]" [Type]
_ -> RN String
freshListName
                Type
_             -> RN String
freshName
    String -> String -> RN ()
insertRn String
v String
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
$ String -> Type -> Theorem -> Theorem
ThForall String
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 String
v)       = String -> Expr
EVar       (String -> Expr) -> RN String -> RN Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` String -> RN String
lookupRn String
v
rnExp (EVarOp Fixity
f Int
n String
v) = Fixity -> Int -> String -> Expr
EVarOp Fixity
f Int
n (String -> Expr) -> RN String -> RN Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` String -> RN String
lookupRn String
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 String
v Type
t)
    = do
        String
mv <- String -> MyMon String
makeVar String
"f"
        String
t1 <- String -> MyMon String
makeVar String
v
        String
t2 <- String -> MyMon String
makeVar String
v
        let tymv :: Type
tymv = Type -> Type -> Type
TyArr (String -> Type
TyVar String
t1) (String -> Type
TyVar String
t2)
        Theorem
pt <- TyEnv -> Expr -> Expr -> Type -> StateT MyState Identity Theorem
freeTheorem' ((String
v,String
mv,String
t1,String
t2)(String, String, String, String) -> TyEnv -> TyEnv
forall a. a -> [a] -> [a]
:TyEnv
env) (Expr -> Type -> Expr
ETyApp Expr
e1 (String -> Type
TyVar String
t1))
                                              (Expr -> Type -> Expr
ETyApp Expr
e2 (String -> Type
TyVar String
t2)) Type
t
        Theorem -> StateT MyState Identity Theorem
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Type -> Theorem -> Theorem
ThForall String
mv Type
tymv Theorem
pt)

freeTheorem' TyEnv
env Expr
e1 Expr
e2 t' :: Type
t'@(TyArr Type
t1 Type
t2)
    = do
        String
mv1 <- String -> MyMon String
makeVar String
"v1"
        String
mv2 <- String -> MyMon String
makeVar String
"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 (String -> Expr
EVar String
mv1) (String -> Expr
EVar String
mv2) Type
t1
        Theorem
p2 <- TyEnv -> Expr -> Expr -> Type -> StateT MyState Identity Theorem
freeTheorem' TyEnv
env (Expr -> Expr -> Expr
EApp Expr
e1 (String -> Expr
EVar String
mv1)) (Expr -> Expr -> Expr
EApp Expr
e2 (String -> Expr
EVar String
mv2)) Type
t2
        Theorem -> StateT MyState Identity Theorem
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Type -> Theorem -> Theorem
ThForall String
mv1 Type
tmv1 (String -> Type -> Theorem -> Theorem
ThForall String
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

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

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

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

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

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