{-# 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: " String -> String -> String
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
_) <-
TC (ElabResult, String) -> Idris (ElabResult, String)
forall a. TC a -> Idris a
tclift (TC (ElabResult, String) -> Idris (ElabResult, String))
-> TC (ElabResult, String) -> Idris (ElabResult, String)
forall a b. (a -> b) -> a -> b
$ String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> TT Name
-> EState
-> Elab' EState ElabResult
-> TC (ElabResult, String)
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
(FC -> Elab' EState ElabResult -> Elab' EState ElabResult
forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc (IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> [Name]
-> PTerm
-> Elab' EState 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 ((IState -> IState) -> Idris ()) -> (IState -> IState) -> Idris ()
forall a b. (a -> b) -> a -> b
$ \IState
i -> IState
i { idris_name = 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 Err -> Err
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] TT Name
lhs_tm
let clhs_tm :: TT Name
clhs_tm = [Name] -> TT Name -> TT Name
forall {n}. [n] -> TT n -> TT n
renamepats [Name]
pnames TT Name
clhs_tm_in
Int -> String -> Idris ()
logElab Int
3 (String
"Transform LHS " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TT Name -> String
forall a. Show a => a -> String
show TT Name
clhs_tm)
Int -> String -> Idris ()
logElab Int
3 (String
"Transform type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TT Name -> String
forall a. Show a => a -> String
show TT Name
clhs_ty)
let rhs :: PTerm
rhs = IState -> [Name] -> PTerm -> PTerm
addImplBound IState
i (((Name, PTerm) -> Name) -> [(Name, PTerm)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, PTerm) -> Name
forall a b. (a, b) -> a
fst [(Name, PTerm)]
newargs) PTerm
rhs_in
Int -> String -> Idris ()
logElab Int
5 (String
"Transform RHS input: " String -> String -> String
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
_) <-
TC
((TT Name, [(Name, (Int, Maybe Name, TT Name, [Name]))], Context,
[RDeclInstructions], Int),
String)
-> Idris
((TT Name, [(Name, (Int, Maybe Name, TT Name, [Name]))], Context,
[RDeclInstructions], Int),
String)
forall a. TC a -> Idris a
tclift (TC
((TT Name, [(Name, (Int, Maybe Name, TT Name, [Name]))], Context,
[RDeclInstructions], Int),
String)
-> Idris
((TT Name, [(Name, (Int, Maybe Name, TT Name, [Name]))], Context,
[RDeclInstructions], Int),
String))
-> TC
((TT Name, [(Name, (Int, Maybe Name, TT Name, [Name]))], Context,
[RDeclInstructions], Int),
String)
-> Idris
((TT Name, [(Name, (Int, Maybe Name, TT Name, [Name]))], Context,
[RDeclInstructions], Int),
String)
forall a b. (a -> b) -> a -> b
$ String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> TT Name
-> EState
-> Elab'
EState
(TT Name, [(Name, (Int, Maybe Name, TT Name, [Name]))], Context,
[RDeclInstructions], Int)
-> TC
((TT Name, [(Name, (Int, Maybe Name, TT Name, [Name]))], Context,
[RDeclInstructions], Int),
String)
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
ElabD ()
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) <- FC -> Elab' EState ElabResult -> Elab' EState ElabResult
forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc (IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> PTerm
-> Elab' EState ElabResult
build IState
i ElabInfo
info ElabMode
ERHS [] (String -> Name
sUN String
"transform") PTerm
rhs)
Int -> ElabD ()
forall aux. Int -> Elab' aux ()
set_global_nextname Int
newGName
FC -> ElabD () -> ElabD ()
forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc (ElabD () -> ElabD ()) -> ElabD () -> ElabD ()
forall a b. (a -> b) -> a -> b
$ TT Name -> ElabD ()
forall {n} {aux}. TT n -> StateT (ElabState aux) TC ()
psolve TT Name
lhs_tm
TT Name
tt <- Elab' EState (TT Name)
forall aux. Elab' aux (TT Name)
get_term
let (TT Name
rhs', [(Name, (Int, Maybe Name, TT Name, [Name]))]
defer) = State [(Name, (Int, Maybe Name, TT Name, [Name]))] (TT Name)
-> [(Name, (Int, Maybe Name, TT Name, [Name]))]
-> (TT Name, [(Name, (Int, Maybe Name, TT Name, [Name]))])
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 Maybe Name
forall a. Maybe a
Nothing [] Context
ctxt TT Name
tt) []
Int
newGName <- Elab' EState Int
forall aux. Elab' aux Int
get_global_nextname
(TT Name, [(Name, (Int, Maybe Name, TT Name, [Name]))], Context,
[RDeclInstructions], Int)
-> Elab'
EState
(TT Name, [(Name, (Int, Maybe Name, TT Name, [Name]))], Context,
[RDeclInstructions], Int)
forall a. a -> StateT (ElabState EState) TC a
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 ((IState -> IState) -> Idris ()) -> (IState -> IState) -> Idris ()
forall a b. (a -> b) -> a -> b
$ \IState
i -> IState
i { idris_name = 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 Err -> Err
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] TT Name
rhs'
let crhs_tm :: TT Name
crhs_tm = [Name] -> TT Name -> TT Name
forall {n}. [n] -> TT n -> TT n
renamepats [Name]
pnames TT Name
crhs_tm_in
Int -> String -> Idris ()
logElab Int
3 (String
"Transform RHS " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TT Name -> String
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 ()
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Error Err
e -> Err -> Idris ()
forall a. Err -> Idris a
ierror (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
False (TT Name
clhs_tm, Maybe Provenance
forall a. Maybe a
Nothing) (TT Name
crhs_tm, Maybe Provenance
forall a. Maybe a
Nothing) Err
e [] Int
0))
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
safe (Idris () -> Idris ()) -> Idris () -> Idris ()
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 ()
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Error Err
e -> Err -> Idris ()
forall a. Err -> Idris a
ierror (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
False (TT Name
clhs_tm, Maybe Provenance
forall a. Maybe a
Nothing) (TT Name
crhs_tm, Maybe Provenance
forall a. Maybe a
Nothing) Err
e [] Int
0))
case TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply (TT Name -> TT Name
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])
_ -> Err -> Idris ()
forall a. Err -> Idris a
ierror (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (String -> Err
forall t. String -> Err' t
Msg String
"Invalid transformation rule (must be function application)"))
(TT Name, TT Name) -> Idris (TT Name, TT Name)
forall a. a -> StateT IState (ExceptT Err IO) a
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 (TT n -> TT n -> TT n
forall n. TT n -> TT n -> TT n
instantiate (NameType -> n -> TT n -> TT n
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)
= n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n' (RigCount -> TT n -> Binder (TT 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 = (Int -> Name) -> [Int] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> Int -> String -> Name
sMN Int
i (String
"tvar" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)) [Int
0..]
elabTransform ElabInfo
info FC
fc Bool
safe PTerm
lhs_in PTerm
rhs_in
= Err -> Idris (TT Name, TT Name)
forall a. Err -> Idris a
ierror (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (String -> Err
forall t. String -> Err' t
Msg String
"Invalid transformation rule (must be function application)"))