@@ -1,6 +1,6 @@
11{-# LANGUAGE PatternGuards, ViewPatterns #-}
22{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3−module Idris.Elab.Rewrite(elabRewrite) where
3+module Idris.Elab.Rewrite(elabRewrite, elabRewriteLemma) where
44
55import Idris.AbsSyntax
66import Idris.AbsSyntaxTree
@@ -9,6 +9,7 @@ import Idris.Error
99import Idris.Core.TT
1010import Idris.Core.Elaborate
1111import Idris.Core.Evaluate
12+import Idris.Docstrings
1213
1314import Control.Monad
1415import Control.Monad.State.Strict
@@ -121,11 +122,134 @@ findSubstFn Nothing ist lt rt
121122 | lt == rt = return (sUN "rewrite__impl")
122123 -- TODO: Find correct rewriting lemma, if it exists, and tidy up this
123124 -- error
124− | otherwise = lift . tfail .
125+ | (P _ lcon _, _) <- unApply lt,
126+ (P _ rcon _, _) <- unApply rt,
127+ lcon == rcon
128+ = case lookupTyExact (rewrite_name lcon) (tt_ctxt ist) of
129+ Just _ -> return (rewrite_name lcon)
130+ Nothing -> rewriteFail lt rt
131+ | otherwise = rewriteFail lt rt
132+ where rewriteFail lt rt = lift . tfail .
125133 Msg $ "Can't rewrite heterogeneous equality on types " ++
126134 show (delab ist lt) ++ " and " ++ show (delab ist rt)
135+
127136findSubstFn (Just substfn_in) ist lt rt
128137 = case lookupTyName substfn_in (tt_ctxt ist) of
129138 [(n, t)] -> return n
130139 [] -> lift . tfail . NoSuchVariable $ substfn_in
131140 more -> lift . tfail . CantResolveAlts $ map fst more
141+
142+rewrite_name :: Name -> Name
143+rewrite_name n = sMN 0 (show n ++ "_rewrite_lemma")
144+
145+data ParamInfo = Index
146+ | Param
147+ | ImplicitIndex
148+ | ImplicitParam
149+ deriving Show
150+
151+getParamInfo :: Type -> [PArg] -> Int -> [Int] -> [ParamInfo]
152+-- Skip the top level implicits, we just need the explicit ones
153+getParamInfo (Bind n (Pi _ _ _) sc) (PExp{} : is) i ps
154+ | i `elem` ps = Param : getParamInfo sc is (i + 1) ps
155+ | otherwise = Index : getParamInfo sc is (i + 1) ps
156+getParamInfo (Bind n (Pi _ _ _) sc) (_ : is) i ps
157+ | i `elem` ps = ImplicitParam : getParamInfo sc is (i + 1) ps
158+ | otherwise = ImplicitIndex : getParamInfo sc is (i + 1) ps
159+getParamInfo _ _ _ _ = []
160+
161+isParam Index = False
162+isParam Param = True
163+isParam ImplicitIndex = False
164+isParam ImplicitParam = True
165+
166+-- Make a rewriting lemma for the given type constructor.
167+-- If it fails, fail silently (it may well fail for some very complex types.
168+-- We can fix this later, for now this gives us a lot more working rewrites...)
169+elabRewriteLemma :: ElabInfo -> Name -> Type -> Idris ()
170+elabRewriteLemma info n cty_in =
171+ do ist <- getIState
172+ let cty = normalise (tt_ctxt ist) [] cty_in
173+ let rewrite_lem = rewrite_name n
174+ case lookupCtxtExact n (idris_datatypes ist) of
175+ Nothing -> fail $ "Can't happen, elabRewriteLemma for " ++ show n
176+ Just ti -> do
177+ let imps = case lookupCtxtExact n (idris_implicits ist) of
178+ Nothing -> repeat (pexp Placeholder)
179+ Just is -> is
180+ let pinfo = getParamInfo cty imps 0 (param_pos ti)
181+ if all isParam pinfo
182+ then return () -- no need for a lemma, = will be homogeneous
183+ else idrisCatch (mkLemma info rewrite_lem n pinfo cty)
184+ (\_ -> return ())
185+
186+mkLemma :: ElabInfo -> Name -> Name -> [ParamInfo] -> Type -> Idris ()
187+mkLemma info lemma tcon ps ty =
188+ do ist <- getIState
189+ let leftty = mkTy tcon ps (namesFrom "p" 0) (namesFrom "left" 0)
190+ rightty = mkTy tcon ps (namesFrom "p" 0) (namesFrom "right" 0)
191+ predty = bindIdxs ist ps ty (namesFrom "pred" 0) $
192+ PPi expl (sMN 0 "rep") fc
193+ (mkTy tcon ps (namesFrom "p" 0) (namesFrom "pred" 0))
194+ (PType fc)
195+ let xarg = sMN 0 "x"
196+ let yarg = sMN 0 "y"
197+ let parg = sMN 0 "P"
198+ let eq = sMN 0 "eq"
199+ let prop = sMN 0 "prop"
200+ let lemTy = PPi impl xarg fc leftty $
201+ PPi impl yarg fc rightty $
202+ PPi expl parg fc predty $
203+ PPi expl eq fc (PApp fc (PRef fc [] (sUN "="))
204+ [pexp (PRef fc [] xarg),
205+ pexp (PRef fc [] yarg)]) $
206+ PPi expl prop fc (PApp fc (PRef fc [] parg)
207+ [pexp (PRef fc [] yarg)]) $
208+ PApp fc (PRef fc [] parg) [pexp (PRef fc [] xarg)]
209+
210+ let lemLHS = PApp fc (PRef fc [] lemma)
211+ [pexp (PRef fc [] parg),
212+ pexp (PRef fc [] (sUN "Refl")),
213+ pexp (PRef fc [] prop)]
214+
215+ let lemRHS = PRef fc [] prop
216+
217+ -- Elaborate the type of the lemma
218+ rec_elabDecl info EAll info
219+ (PTy emptyDocstring [] defaultSyntax fc [] lemma fc lemTy)
220+ -- Elaborate the definition
221+ rec_elabDecl info EAll info
222+ (PClauses fc [] lemma [PClause fc lemma lemLHS [] lemRHS []])
223+
224+ where
225+ fc = emptyFC
226+
227+ namesFrom x i = sMN i x : namesFrom x (i + 1)
228+
229+ mkTy fn pinfo ps is
230+ = PApp fc (PRef fc [] fn) (mkArgs pinfo ps is)
231+
232+ mkArgs [] ps is = []
233+ mkArgs (Param : pinfo) (p : ps) is
234+ = pexp (PRef fc [] p) : mkArgs pinfo ps is
235+ mkArgs (Index : pinfo) ps (i : is)
236+ = pexp (PRef fc [] i) : mkArgs pinfo ps is
237+ mkArgs (ImplicitParam : pinfo) (p : ps) is
238+ = mkArgs pinfo ps is
239+ mkArgs (ImplicitIndex : pinfo) ps (i : is)
240+ = mkArgs pinfo ps is
241+ mkArgs _ _ _ = []
242+
243+ bindIdxs ist [] ty is tm = tm
244+ bindIdxs ist (Param : pinfo) (Bind n (Pi _ ty _) sc) is tm
245+ = bindIdxs ist pinfo (instantiate (P Bound n ty) sc) is tm
246+ bindIdxs ist (Index : pinfo) (Bind n (Pi _ ty _) sc) (i : is) tm
247+ = PPi forall_imp i fc (delab ist ty)
248+ (bindIdxs ist pinfo (instantiate (P Bound n ty) sc) is tm)
249+ bindIdxs ist (ImplicitParam : pinfo) (Bind n (Pi _ ty _) sc) is tm
250+ = bindIdxs ist pinfo (instantiate (P Bound n ty) sc) is tm
251+ bindIdxs ist (ImplicitIndex : pinfo) (Bind n (Pi _ ty _) sc) (i : is) tm
252+ = bindIdxs ist pinfo (instantiate (P Bound n ty) sc) is tm
253+ bindIdxs _ _ _ _ tm = tm
254+
255+