{-# 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)
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))
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)
renamepats [n]
_ TT n
sc = TT n
sc
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)"))