{-|
Module      : Idris.Elab.Transform
Description : Transformations for elaborate terms.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE PatternGuards #-}
module Idris.Elab.Transform where

import Idris.AbsSyntax
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Elab.Term
import Idris.Elab.Utils
import Idris.Error
import Idris.Output (sendHighlighting)

import Prelude hiding (id, (.))

import Control.Category
import Control.Monad
import Control.Monad.State.Strict as State

elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Term, Term)
elabTransform :: ElabInfo
-> FC -> Bool -> PTerm -> PTerm -> Idris (TT Name, TT Name)
elabTransform ElabInfo
info FC
fc Bool
safe lhs_in :: PTerm
lhs_in@(PApp FC
_ (PRef FC
_ [FC]
_ Name
tf) [PArg]
_) PTerm
rhs_in
    = do Context
ctxt <- Idris Context
getContext
         IState
i <- Idris IState
getIState
         let lhs :: PTerm
lhs = IState -> PTerm -> PTerm
addImplPat IState
i PTerm
lhs_in
         Int -> String -> Idris ()
logElab Int
5 (String
"Transform LHS input: " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs)
         (ElabResult TT Name
lhs' [(Name, (Int, Maybe Name, TT Name, [Name]))]
dlhs [] Context
ctxt' [RDeclInstructions]
newDecls Set (FC', OutputAnnotation)
highlights Int
newGName, String
_) <-
              forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall aux a.
String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> TT Name
-> aux
-> Elab' aux a
-> TC (a, String)
elaborate (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
i) (IState -> Int
idris_name IState
i) (Int -> String -> Name
sMN Int
0 String
"transLHS") TT Name
infP EState
initEState
                       (forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc (IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> [Name]
-> PTerm
-> ElabD ElabResult
buildTC IState
i ElabInfo
info ElabMode
ETransLHS [] (String -> Name
sUN String
"transform")
                                   (PTerm -> [Name]
allNamesIn PTerm
lhs_in) (PTerm -> PTerm
infTerm PTerm
lhs)))
         Context -> Idris ()
setContext Context
ctxt'
         ElabInfo -> [RDeclInstructions] -> Idris ()
processTacticDecls ElabInfo
info [RDeclInstructions]
newDecls
         Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting Set (FC', OutputAnnotation)
highlights
         (IState -> IState) -> Idris ()
updateIState forall a b. (a -> b) -> a -> b
$ \IState
i -> IState
i { idris_name :: Int
idris_name = Int
newGName }
         let lhs_tm :: TT Name
lhs_tm = TT Name -> TT Name
orderPats (TT Name -> TT Name
getInferTerm TT Name
lhs')
         let newargs :: [(Name, PTerm)]
newargs = IState -> TT Name -> [(Name, PTerm)]
pvars IState
i TT Name
lhs_tm

         (TT Name
clhs_tm_in, TT Name
clhs_ty) <- Bool
-> Bool
-> [Name]
-> String
-> FC
-> (Err -> Err)
-> Env
-> TT Name
-> Idris (TT Name, TT Name)
recheckC_borrowing Bool
False Bool
False [] (ElabInfo -> String
constraintNS ElabInfo
info) FC
fc forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] TT Name
lhs_tm
         let clhs_tm :: TT Name
clhs_tm = forall {n}. [n] -> TT n -> TT n
renamepats [Name]
pnames TT Name
clhs_tm_in
         Int -> String -> Idris ()
logElab Int
3 (String
"Transform LHS " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TT Name
clhs_tm)
         Int -> String -> Idris ()
logElab Int
3 (String
"Transform type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TT Name
clhs_ty)

         let rhs :: PTerm
rhs = IState -> [Name] -> PTerm -> PTerm
addImplBound IState
i (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, PTerm)]
newargs) PTerm
rhs_in
         Int -> String -> Idris ()
logElab Int
5 (String
"Transform RHS input: " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
rhs)

         ((TT Name
rhs', [(Name, (Int, Maybe Name, TT Name, [Name]))]
defer, Context
ctxt', [RDeclInstructions]
newDecls, Int
newGName), String
_) <-
              forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall aux a.
String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> TT Name
-> aux
-> Elab' aux a
-> TC (a, String)
elaborate (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
i) (IState -> Int
idris_name IState
i) (Int -> String -> Name
sMN Int
0 String
"transRHS") TT Name
clhs_ty EState
initEState
                       (do IState -> TT Name -> ElabD ()
pbinds IState
i TT Name
lhs_tm
                           forall aux. Elab' aux ()
setNextName
                           (ElabResult TT Name
_ [(Name, (Int, Maybe Name, TT Name, [Name]))]
_ [PDecl]
_ Context
ctxt' [RDeclInstructions]
newDecls Set (FC', OutputAnnotation)
highlights Int
newGName) <- forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc (IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> PTerm
-> ElabD ElabResult
build IState
i ElabInfo
info ElabMode
ERHS [] (String -> Name
sUN String
"transform") PTerm
rhs)
                           forall aux. Int -> Elab' aux ()
set_global_nextname Int
newGName
                           forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc forall a b. (a -> b) -> a -> b
$ forall {n} {aux}. TT n -> StateT (ElabState aux) TC ()
psolve TT Name
lhs_tm
                           TT Name
tt <- forall aux. Elab' aux (TT Name)
get_term
                           let (TT Name
rhs', [(Name, (Int, Maybe Name, TT Name, [Name]))]
defer) = forall s a. State s a -> s -> (a, s)
runState (Maybe Name
-> [Name]
-> Context
-> TT Name
-> State [(Name, (Int, Maybe Name, TT Name, [Name]))] (TT Name)
collectDeferred forall a. Maybe a
Nothing [] Context
ctxt TT Name
tt) []
                           Int
newGName <- forall aux. Elab' aux Int
get_global_nextname
                           forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name
rhs', [(Name, (Int, Maybe Name, TT Name, [Name]))]
defer, Context
ctxt', [RDeclInstructions]
newDecls, Int
newGName))
         Context -> Idris ()
setContext Context
ctxt'
         ElabInfo -> [RDeclInstructions] -> Idris ()
processTacticDecls ElabInfo
info [RDeclInstructions]
newDecls
         Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting Set (FC', OutputAnnotation)
highlights
         (IState -> IState) -> Idris ()
updateIState forall a b. (a -> b) -> a -> b
$ \IState
i -> IState
i { idris_name :: Int
idris_name = Int
newGName }

         (TT Name
crhs_tm_in, TT Name
crhs_ty) <- Bool
-> Bool
-> [Name]
-> String
-> FC
-> (Err -> Err)
-> Env
-> TT Name
-> Idris (TT Name, TT Name)
recheckC_borrowing Bool
False Bool
False [] (ElabInfo -> String
constraintNS ElabInfo
info) FC
fc forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] TT Name
rhs'
         let crhs_tm :: TT Name
crhs_tm = forall {n}. [n] -> TT n -> TT n
renamepats [Name]
pnames TT Name
crhs_tm_in
         Int -> String -> Idris ()
logElab Int
3 (String
"Transform RHS " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TT Name
crhs_tm)

         -- Types must always convert
         case Context -> Env -> TT Name -> TT Name -> TC ()
converts Context
ctxt [] TT Name
clhs_ty TT Name
crhs_ty of
              OK ()
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Error Err
e -> forall a. Err -> Idris a
ierror (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
False (TT Name
clhs_tm, forall a. Maybe a
Nothing) (TT Name
crhs_tm, forall a. Maybe a
Nothing) Err
e [] Int
0))
         -- In safe mode, values must convert (Thinks: This is probably not
         -- useful as is, perhaps it should require a proof of equality instead)
         forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
safe forall a b. (a -> b) -> a -> b
$ case Context -> Env -> TT Name -> TT Name -> TC ()
converts Context
ctxt [] TT Name
clhs_tm TT Name
crhs_tm of
              OK ()
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Error Err
e -> forall a. Err -> Idris a
ierror (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
False (TT Name
clhs_tm, forall a. Maybe a
Nothing) (TT Name
crhs_tm, forall a. Maybe a
Nothing) Err
e [] Int
0))

         case forall n. TT n -> (TT n, [TT n])
unApply (forall {n}. TT n -> TT n
depat TT Name
clhs_tm) of
              (P NameType
_ Name
tfname TT Name
_, [TT Name]
_) -> do Name -> (TT Name, TT Name) -> Idris ()
addTrans Name
tfname (TT Name
clhs_tm, TT Name
crhs_tm)
                                      IBCWrite -> Idris ()
addIBC (Name -> (TT Name, TT Name) -> IBCWrite
IBCTrans Name
tf (TT Name
clhs_tm, TT Name
crhs_tm))
              (TT Name, [TT Name])
_ -> forall a. Err -> Idris a
ierror (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. String -> Err' t
Msg String
"Invalid transformation rule (must be function application)"))
         forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name
clhs_tm, TT Name
crhs_tm)

  where
    depat :: TT n -> TT n
depat (Bind n
n (PVar RigCount
_ TT n
t) TT n
sc) = TT n -> TT n
depat (forall n. TT n -> TT n -> TT n
instantiate (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
n TT n
t) TT n
sc)
    depat TT n
x = TT n
x

    renamepats :: [n] -> TT n -> TT n
renamepats (n
n' : [n]
ns) (Bind n
n (PVar RigCount
rig TT n
t) TT n
sc)
       = forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n' (forall b. RigCount -> b -> Binder b
PVar RigCount
rig TT n
t) ([n] -> TT n -> TT n
renamepats [n]
ns TT n
sc) -- all Vs
    renamepats [n]
_ TT n
sc = TT n
sc

    -- names for transformation variables. Need to ensure these don't clash
    -- with any other names when applying rules, so rename here.
    pnames :: [Name]
pnames = forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> Int -> String -> Name
sMN Int
i (String
"tvar" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i)) [Int
0..]

elabTransform ElabInfo
info FC
fc Bool
safe PTerm
lhs_in PTerm
rhs_in
   = forall a. Err -> Idris a
ierror (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. String -> Err' t
Msg String
"Invalid transformation rule (must be function application)"))