{-|
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 ctxt <- Idris Context
getContext
         i <- getIState
         let lhs = IState -> PTerm -> PTerm
addImplPat IState
i PTerm
lhs_in
         logElab 5 ("Transform LHS input: " ++ showTmImpls lhs)
         (ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, _) <-
              tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "transLHS") infP initEState
                       (erun fc (buildTC i info ETransLHS [] (sUN "transform")
                                   (allNamesIn lhs_in) (infTerm lhs)))
         setContext ctxt'
         processTacticDecls info newDecls
         sendHighlighting highlights
         updateIState $ \IState
i -> IState
i { idris_name = newGName }
         let lhs_tm = TT Name -> TT Name
orderPats (TT Name -> TT Name
getInferTerm TT Name
lhs')
         let newargs = IState -> TT Name -> [(Name, PTerm)]
pvars IState
i TT Name
lhs_tm

         (clhs_tm_in, clhs_ty) <- recheckC_borrowing False False [] (constraintNS info) fc id [] lhs_tm
         let clhs_tm = [Name] -> TT Name -> TT Name
forall {n}. [n] -> TT n -> TT n
renamepats [Name]
pnames TT Name
clhs_tm_in
         logElab 3 ("Transform LHS " ++ show clhs_tm)
         logElab 3 ("Transform type " ++ show clhs_ty)

         let 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
         logElab 5 ("Transform RHS input: " ++ showTmImpls rhs)

         ((rhs', defer, ctxt', newDecls, newGName), _) <-
              tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "transRHS") clhs_ty initEState
                       (do pbinds i lhs_tm
                           setNextName
                           (ElabResult _ _ _ ctxt' newDecls highlights newGName) <- erun fc (build i info ERHS [] (sUN "transform") rhs)
                           set_global_nextname newGName
                           erun fc $ psolve lhs_tm
                           tt <- get_term
                           let (rhs', defer) = runState (collectDeferred Nothing [] ctxt tt) []
                           newGName <- get_global_nextname
                           return (rhs', defer, ctxt', newDecls, newGName))
         setContext ctxt'
         processTacticDecls info newDecls
         sendHighlighting highlights
         updateIState $ \IState
i -> IState
i { idris_name = newGName }

         (crhs_tm_in, crhs_ty) <- recheckC_borrowing False False [] (constraintNS info) fc id [] rhs'
         let crhs_tm = [Name] -> TT Name -> TT Name
forall {n}. [n] -> TT n -> TT n
renamepats [Name]
pnames TT Name
crhs_tm_in
         logElab 3 ("Transform RHS " ++ show crhs_tm)

         -- Types must always convert
         case converts ctxt [] clhs_ty 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))
         -- In safe mode, values must convert (Thinks: This is probably not
         -- useful as is, perhaps it should require a proof of equality instead)
         when safe $ case converts ctxt [] clhs_tm 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 unApply (depat 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)"))
         return (clhs_tm, 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) -- 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 = (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)"))