
  0 | module TTImp.ProcessTransform
  1 | 
  2 | import Core.Env
  3 | import Core.Metadata
  4 | import Core.UnifyState
  5 | 
  6 | import Idris.REPL.Opts
  7 | import Idris.Syntax
  8 | 
  9 | import TTImp.Elab
 10 | import TTImp.Elab.Check
 11 | import TTImp.ProcessDef -- for checking LHS
 12 | import TTImp.TTImp
 13 | 
 14 | %default covering
 15 | 
 16 | export
 17 | processTransform : {vars : _} ->
 18 |                    {auto c : Ref Ctxt Defs} ->
 19 |                    {auto m : Ref MD Metadata} ->
 20 |                    {auto u : Ref UST UState} ->
 21 |                    {auto s : Ref Syn SyntaxInfo} ->
 22 |                    {auto o : Ref ROpts REPLOpts} ->
 23 |                    List ElabOpt -> NestedNames vars -> Env Term vars -> FC ->
 24 |                    Name -> RawImp -> RawImp -> Core ()
 25 | processTransform eopts nest env fc tn_in lhs rhs
 26 |     = do tn <- inCurrentNS tn_in
 27 |          tidx <- resolveName tn
 28 |          (_, (vars'  ** (sub', env', nest', lhstm, lhsty))) <-
 29 |              checkLHS True top tidx eopts nest env fc lhs
 30 |          logTerm "transform.lhs" 3 "Transform LHS" lhstm
 31 |          rhstm <- wrapError (InRHS fc tn_in) $
 32 |                        checkTermSub tidx InExpr (InTrans :: eopts) nest' env' env sub' rhs (gnf env' lhsty)
 33 |          clearHoleLHS
 34 |          logTerm "transform.rhs" 3 "Transform RHS" rhstm
 35 |          addTransform fc (MkTransform tn env' lhstm rhstm)
 36 |