{-|
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 (Term, Term)
elabTransform info :: ElabInfo
info fc :: FC
fc safe :: Bool
safe lhs_in :: PTerm
lhs_in@(PApp _ (PRef _ _ tf :: Name
tf) _) rhs_in :: 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 5 ("Transform LHS input: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs)
         (ElabResult lhs' :: Term
lhs' dlhs :: [(Name, (Int, Maybe Name, Term, [Name]))]
dlhs [] ctxt' :: Context
ctxt' newDecls :: [RDeclInstructions]
newDecls highlights :: Set (FC', OutputAnnotation)
highlights newGName :: Int
newGName, _) <-
              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
-> Term
-> EState
-> Elab' EState ElabResult
-> TC (ElabResult, String)
forall aux a.
String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Term
-> 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 0 "transLHS") Term
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 "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
$ \i :: IState
i -> IState
i { idris_name :: Int
idris_name = Int
newGName }
         let lhs_tm :: Term
lhs_tm = Term -> Term
orderPats (Term -> Term
getInferTerm Term
lhs')
         let newargs :: [(Name, PTerm)]
newargs = IState -> Term -> [(Name, PTerm)]
pvars IState
i Term
lhs_tm

         (clhs_tm_in :: Term
clhs_tm_in, clhs_ty :: Term
clhs_ty) <- Bool
-> Bool
-> [Name]
-> String
-> FC
-> (Err' Term -> Err' Term)
-> Env
-> Term
-> Idris (Term, Term)
recheckC_borrowing Bool
False Bool
False [] (ElabInfo -> String
constraintNS ElabInfo
info) FC
fc Err' Term -> Err' Term
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] Term
lhs_tm
         let clhs_tm :: Term
clhs_tm = [Name] -> Term -> Term
forall n. [n] -> TT n -> TT n
renamepats [Name]
pnames Term
clhs_tm_in
         Int -> String -> Idris ()
logElab 3 ("Transform LHS " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
clhs_tm)
         Int -> String -> Idris ()
logElab 3 ("Transform type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
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 5 ("Transform RHS input: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
rhs)

         ((rhs' :: Term
rhs', defer :: [(Name, (Int, Maybe Name, Term, [Name]))]
defer, ctxt' :: Context
ctxt', newDecls :: [RDeclInstructions]
newDecls, newGName :: Int
newGName), _) <-
              TC
  ((Term, [(Name, (Int, Maybe Name, Term, [Name]))], Context,
    [RDeclInstructions], Int),
   String)
-> Idris
     ((Term, [(Name, (Int, Maybe Name, Term, [Name]))], Context,
       [RDeclInstructions], Int),
      String)
forall a. TC a -> Idris a
tclift (TC
   ((Term, [(Name, (Int, Maybe Name, Term, [Name]))], Context,
     [RDeclInstructions], Int),
    String)
 -> Idris
      ((Term, [(Name, (Int, Maybe Name, Term, [Name]))], Context,
        [RDeclInstructions], Int),
       String))
-> TC
     ((Term, [(Name, (Int, Maybe Name, Term, [Name]))], Context,
       [RDeclInstructions], Int),
      String)
-> Idris
     ((Term, [(Name, (Int, Maybe Name, Term, [Name]))], Context,
       [RDeclInstructions], Int),
      String)
forall a b. (a -> b) -> a -> b
$ String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Term
-> EState
-> Elab'
     EState
     (Term, [(Name, (Int, Maybe Name, Term, [Name]))], Context,
      [RDeclInstructions], Int)
-> TC
     ((Term, [(Name, (Int, Maybe Name, Term, [Name]))], Context,
       [RDeclInstructions], Int),
      String)
forall aux a.
String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Term
-> 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 0 "transRHS") Term
clhs_ty EState
initEState
                       (do IState -> Term -> ElabD ()
pbinds IState
i Term
lhs_tm
                           ElabD ()
forall aux. Elab' aux ()
setNextName
                           (ElabResult _ _ _ ctxt' :: Context
ctxt' newDecls :: [RDeclInstructions]
newDecls highlights :: Set (FC', OutputAnnotation)
highlights newGName :: 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 "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
$ Term -> ElabD ()
forall n aux. TT n -> StateT (ElabState aux) TC ()
psolve Term
lhs_tm
                           Term
tt <- Elab' EState Term
forall aux. Elab' aux Term
get_term
                           let (rhs' :: Term
rhs', defer :: [(Name, (Int, Maybe Name, Term, [Name]))]
defer) = State [(Name, (Int, Maybe Name, Term, [Name]))] Term
-> [(Name, (Int, Maybe Name, Term, [Name]))]
-> (Term, [(Name, (Int, Maybe Name, Term, [Name]))])
forall s a. State s a -> s -> (a, s)
runState (Maybe Name
-> [Name]
-> Context
-> Term
-> State [(Name, (Int, Maybe Name, Term, [Name]))] Term
collectDeferred Maybe Name
forall a. Maybe a
Nothing [] Context
ctxt Term
tt) []
                           Int
newGName <- Elab' EState Int
forall aux. Elab' aux Int
get_global_nextname
                           (Term, [(Name, (Int, Maybe Name, Term, [Name]))], Context,
 [RDeclInstructions], Int)
-> Elab'
     EState
     (Term, [(Name, (Int, Maybe Name, Term, [Name]))], Context,
      [RDeclInstructions], Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
rhs', [(Name, (Int, Maybe Name, Term, [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
$ \i :: IState
i -> IState
i { idris_name :: Int
idris_name = Int
newGName }

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

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

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

  where
    depat :: TT n -> TT n
depat (Bind n :: n
n (PVar _ t :: TT n
t) sc :: 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 x :: TT n
x = TT n
x

    renamepats :: [n] -> TT n -> TT n
renamepats (n' :: n
n' : ns :: [n]
ns) (Bind n :: n
n (PVar rig :: RigCount
rig t :: TT n
t) sc :: 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) -- all Vs
    renamepats _ sc :: 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 = (Int -> Name) -> [Int] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (\i :: Int
i -> Int -> String -> Name
sMN Int
i ("tvar" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)) [0..]

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