git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/src/Idris/Elab/Transform.hs
99 lines 3.5 kB history raw
1{-# LANGUAGE PatternGuards #-}
2module Idris.Elab.Transform where
4import Idris.AbsSyntax
5import Idris.ASTUtils
6import Idris.DSL
7import Idris.Error
8import Idris.Delaborate
9import Idris.Imports
10import Idris.ElabTerm
11import Idris.Coverage
12import Idris.DataOpts
13import Idris.Providers
14import Idris.Primitives
15import Idris.Inliner
16import Idris.PartialEval
17import Idris.DeepSeq
18import Idris.Output (iputStrLn, pshow, iWarn)
19import IRTS.Lang
21import Idris.Elab.Utils
23import Idris.Core.TT
24import Idris.Core.Elaborate hiding (Tactic(..))
25import Idris.Core.Evaluate
26import Idris.Core.Execute
27import Idris.Core.Typecheck
28import Idris.Core.CaseTree
30import Idris.Docstrings
32import Prelude hiding (id, (.))
33import Control.Category
35import Control.Applicative hiding (Const)
36import Control.DeepSeq
37import Control.Monad
38import Control.Monad.State.Strict as State
39import Data.List
40import Data.Maybe
41import Debug.Trace
43import qualified Data.Map as Map
44import qualified Data.Set as S
45import qualified Data.Text as T
46import Data.Char(isLetter, toLower)
47import Data.List.Split (splitOn)
49import Util.Pretty(pretty, text)
51elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Term, Term)
52elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in
53 = do ctxt <- getContext
54 i <- getIState
55 let lhs = addImplPat i lhs_in
56 ((lhs', dlhs, []), _) <-
57 tclift $ elaborate ctxt (sMN 0 "transLHS") infP []
58 (erun fc (buildTC i info ELHS [] (sUN "transform")
59 (infTerm lhs)))
60 let lhs_tm = orderPats (getInferTerm lhs')
61 let lhs_ty = getInferType lhs'
62 let newargs = pvars i lhs_tm
64 (clhs_tm, clhs_ty) <- recheckC fc [] lhs_tm
65 logLvl 3 ("Transform LHS " ++ show clhs_tm)
66 let rhs = addImplBound i (map fst newargs) rhs_in
67 ((rhs', defer), _) <-
68 tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty []
69 (do pbinds i lhs_tm
70 setNextName
71 erun fc (build i info ERHS [] (sUN "transform") rhs)
72 erun fc $ psolve lhs_tm
73 tt <- get_term
74 return (runState (collectDeferred Nothing tt) []))
75 (crhs_tm, crhs_ty) <- recheckC fc [] rhs'
76 logLvl 3 ("Transform RHS " ++ show crhs_tm)
77 -- Types must always convert
78 case converts ctxt [] clhs_ty crhs_ty of
79 OK _ -> return ()
80 Error e -> ierror (At fc (CantUnify False clhs_tm crhs_tm e [] 0))
81 -- In safe mode, values must convert (Thinks: This is probably not
82 -- useful as is, perhaps it should require a proof of equality instead)
83 when safe $ case converts ctxt [] clhs_tm crhs_tm of
84 OK _ -> return ()
85 Error e -> ierror (At fc (CantUnify False clhs_tm crhs_tm e [] 0))
87 case unApply (depat clhs_tm) of
88 (P _ tfname _, _) -> do addTrans tfname (clhs_tm, crhs_tm)
89 addIBC (IBCTrans tf (clhs_tm, crhs_tm))
90 _ -> ierror (At fc (Msg "Invalid transformation rule (must be function application)"))
91 return (clhs_tm, crhs_tm)
93 where
94 depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)
95 depat x = x
97elabTransform info fc safe lhs_in rhs_in
98 = ierror (At fc (Msg "Invalid transformation rule (must be function application)"))