    {-# OPTIONS -w #-}

    module Lambdabot.Plugin.Haskell.Free.FreeTheorem where

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

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

    import Data.Char
    import qualified Data.Map as M

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

    type MyMon a = StateT MyState Identity a

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

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

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

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

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

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

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

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

    type RN a = State RnSt a

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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