git.iko.soy/Idris-dev
on 54e4e41 help sign in
Idris-dev/src/Idris/Elab/Transform.hs
123 lines 4.6 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.Coverage
11import Idris.DataOpts
12import Idris.Providers
13import Idris.Primitives
14import Idris.Inliner
15import Idris.PartialEval
16import Idris.DeepSeq
17import Idris.Output (iputStrLn, pshow, iWarn, sendHighlighting)
18import IRTS.Lang
20import Idris.Elab.Utils
21import Idris.Elab.Term
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 logLvl 5 ("Transform LHS input: " ++ showTmImpls lhs)
57 (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-
58 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transLHS") infP initEState
59 (erun fc (buildTC i info ETransLHS [] (sUN "transform")
60 (infTerm lhs)))
61 setContext ctxt'
62 processTacticDecls info newDecls
63 sendHighlighting highlights
64 let lhs_tm = orderPats (getInferTerm lhs')
65 let lhs_ty = getInferType lhs'
66 let newargs = pvars i lhs_tm
68 (clhs_tm_in, clhs_ty) <- recheckC fc id [] lhs_tm
69 let clhs_tm = renamepats pnames clhs_tm_in
70 logLvl 3 ("Transform LHS " ++ show clhs_tm)
71 logLvl 3 ("Transform type " ++ show clhs_ty)
73 let rhs = addImplBound i (map fst newargs) rhs_in
74 logLvl 5 ("Transform RHS input: " ++ showTmImpls rhs)
76 ((rhs', defer, ctxt', newDecls), _) <-
77 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transRHS") clhs_ty initEState
78 (do pbinds i lhs_tm
79 setNextName
80 (ElabResult _ _ _ ctxt' newDecls highlights) <- erun fc (build i info ERHS [] (sUN "transform") rhs)
81 erun fc $ psolve lhs_tm
82 tt <- get_term
83 let (rhs', defer) = runState (collectDeferred Nothing [] ctxt tt) []
84 return (rhs', defer, ctxt', newDecls))
85 setContext ctxt'
86 processTacticDecls info newDecls
87 sendHighlighting highlights
89 (crhs_tm_in, crhs_ty) <- recheckC fc id [] rhs'
90 let crhs_tm = renamepats pnames crhs_tm_in
91 logLvl 3 ("Transform RHS " ++ show crhs_tm)
93 -- Types must always convert
94 case converts ctxt [] clhs_ty crhs_ty of
95 OK _ -> return ()
96 Error e -> ierror (At fc (CantUnify False (clhs_tm, Nothing) (crhs_tm, Nothing) e [] 0))
97 -- In safe mode, values must convert (Thinks: This is probably not
98 -- useful as is, perhaps it should require a proof of equality instead)
99 when safe $ case converts ctxt [] clhs_tm crhs_tm of
100 OK _ -> return ()
101 Error e -> ierror (At fc (CantUnify False (clhs_tm, Nothing) (crhs_tm, Nothing) e [] 0))
103 case unApply (depat clhs_tm) of
104 (P _ tfname _, _) -> do addTrans tfname (clhs_tm, crhs_tm)
105 addIBC (IBCTrans tf (clhs_tm, crhs_tm))
106 _ -> ierror (At fc (Msg "Invalid transformation rule (must be function application)"))
107 return (clhs_tm, crhs_tm)
109 where
110 depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)
111 depat x = x
113 renamepats (n' : ns) (Bind n (PVar t) sc)
114 = Bind n' (PVar t) (renamepats ns sc) -- all Vs
115 renamepats _ sc = sc
117 -- names for transformation variables. Need to ensure these don't clash
118 -- with any other names when applying rules, so rename here.
119 pnames = map (\i -> sMN i ("tvar" ++ show i)) [0..]
121elabTransform info fc safe lhs_in rhs_in
122 = ierror (At fc (Msg "Invalid transformation rule (must be function application)"))