{-# 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 = vn+1 })
Var -> MyMon Var
forall a. a -> StateT MyState Identity a
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)
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
Var
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>`"
(ParseS (Either (Var, Type) Var)
-> ParseS (Either (Var, Type) Var)
-> ParseS (Either (Var, Type) Var)
forall a. ParseS a -> ParseS a -> ParseS a
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 a. a -> ParseS a
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 a. a -> ParseS a
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 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 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 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
(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 a. a -> Identity a
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 a b.
StateT RnSt Identity a
-> StateT RnSt Identity b -> StateT RnSt Identity b
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 { myVSupply :: Int
myVSupply = Int
1 }
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
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. HasCallStack => [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 = tail 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 a. a -> StateT RnSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
fresh
Maybe Var
_ -> RN Var
freshName
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. HasCallStack => [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 = tail 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 a. a -> StateT RnSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
fresh
Maybe Var
_ -> RN Var
freshFunctionName
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. HasCallStack => [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 = tail 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 a. a -> StateT RnSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
fresh
Maybe Var
_ -> RN Var
freshListName
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' }
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 a. a -> StateT RnSt Identity a
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
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 a. a -> StateT RnSt Identity a
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 a. a -> StateT RnSt Identity a
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 a. a -> StateT RnSt Identity a
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 a. a -> StateT RnSt Identity a
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 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
Expr
e1' <- Expr -> RN Expr
rnExp Expr
e1
Expr
e2' <- Expr -> RN Expr
rnExp Expr
e2
Expr -> RN Expr
forall a. a -> StateT RnSt Identity a
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 a. a -> StateT RnSt Identity a
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 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
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 a. a -> StateT MyState Identity a
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 a. a -> StateT MyState Identity a
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 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
[((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)
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
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 a. a -> StateT MyState Identity a
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 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
Theorem -> StateT MyState Identity Theorem
forall a. a -> StateT MyState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ((((Var, Type), Theorem) -> Theorem -> Theorem)
-> Theorem -> [((Var, Type), Theorem)] -> Theorem
forall a b. (a -> b -> b) -> b -> [a] -> b
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. 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
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 a. a -> StateT MyState Identity a
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)
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
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 a. a -> StateT MyState Identity a
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 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
Theorem -> StateT MyState Identity Theorem
forall a. a -> StateT MyState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ((((Var, Type), Theorem) -> Theorem -> Theorem)
-> Theorem -> [((Var, Type), Theorem)] -> Theorem
forall a b. (a -> b -> b) -> b -> [a] -> b
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."