git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/src/Idris/Elab/Transform.hs
117 lines 4.3 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 (ElabResult lhs' dlhs [] ctxt' newDecls, _) <-
57 tclift $ elaborate ctxt (sMN 0 "transLHS") infP initEState
58 (erun fc (buildTC i info ELHS [] (sUN "transform")
59 (infTerm lhs)))
60 setContext ctxt'
61 processTacticDecls newDecls
62 let lhs_tm = orderPats (getInferTerm lhs')
63 let lhs_ty = getInferType lhs'
64 let newargs = pvars i lhs_tm
66 (clhs_tm_in, clhs_ty) <- recheckC fc id [] lhs_tm
67 let clhs_tm = renamepats pnames clhs_tm_in
68 logLvl 3 ("Transform LHS " ++ show clhs_tm)
70 let rhs = addImplBound i (map fst newargs) rhs_in
71 ((rhs', defer, ctxt', newDecls), _) <-
72 tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty initEState
73 (do pbinds i lhs_tm
74 setNextName
75 (ElabResult _ _ _ ctxt' newDecls) <- erun fc (build i info ERHS [] (sUN "transform") rhs)
76 erun fc $ psolve lhs_tm
77 tt <- get_term
78 let (rhs', defer) = runState (collectDeferred Nothing tt) []
79 return (rhs', defer, ctxt', newDecls))
80 setContext ctxt'
81 processTacticDecls newDecls
83 (crhs_tm_in, crhs_ty) <- recheckC fc id [] rhs'
84 let crhs_tm = renamepats pnames crhs_tm_in
85 logLvl 3 ("Transform RHS " ++ show crhs_tm)
87 -- Types must always convert
88 case converts ctxt [] clhs_ty crhs_ty of
89 OK _ -> return ()
90 Error e -> ierror (At fc (CantUnify False (clhs_tm, Nothing) (crhs_tm, Nothing) e [] 0))
91 -- In safe mode, values must convert (Thinks: This is probably not
92 -- useful as is, perhaps it should require a proof of equality instead)
93 when safe $ case converts ctxt [] clhs_tm crhs_tm of
94 OK _ -> return ()
95 Error e -> ierror (At fc (CantUnify False (clhs_tm, Nothing) (crhs_tm, Nothing) e [] 0))
97 case unApply (depat clhs_tm) of
98 (P _ tfname _, _) -> do addTrans tfname (clhs_tm, crhs_tm)
99 addIBC (IBCTrans tf (clhs_tm, crhs_tm))
100 _ -> ierror (At fc (Msg "Invalid transformation rule (must be function application)"))
101 return (clhs_tm, crhs_tm)
103 where
104 depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)
105 depat x = x
107 renamepats (n' : ns) (Bind n (PVar t) sc)
108 = Bind n' (PVar t) (renamepats ns sc) -- all Vs
109 renamepats _ sc = sc
111 -- names for transformation variables. Need to ensure these don't clash
112 -- with any other names when applying rules, so rename here.
113 pnames = map (\i -> sMN i ("tvar" ++ show i)) [0..]
115elabTransform info fc safe lhs_in rhs_in
116 = ierror (At fc (Msg "Invalid transformation rule (must be function application)"))