@@ -1,6 +1,6 @@
1{-# LANGUAGE PatternGuards, ViewPatterns #-}
1{-# LANGUAGE PatternGuards, ViewPatterns #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3−module Idris.Elab.Rewrite(elabRewrite) where
3+module Idris.Elab.Rewrite(elabRewrite, elabRewriteLemma) where
5import Idris.AbsSyntax
5import Idris.AbsSyntax
6import Idris.AbsSyntaxTree
6import Idris.AbsSyntaxTree
@@ -9,6 +9,7 @@ import Idris.Error
9import Idris.Core.TT
9import Idris.Core.TT
10import Idris.Core.Elaborate
10import Idris.Core.Elaborate
11import Idris.Core.Evaluate
11import Idris.Core.Evaluate
12+import Idris.Docstrings
13import Control.Monad
14import Control.Monad
14import Control.Monad.State.Strict
15import Control.Monad.State.Strict
@@ -121,11 +122,134 @@ findSubstFn Nothing ist lt rt
121 | lt == rt = return (sUN "rewrite__impl")
122 | lt == rt = return (sUN "rewrite__impl")
122 -- TODO: Find correct rewriting lemma, if it exists, and tidy up this
123 -- TODO: Find correct rewriting lemma, if it exists, and tidy up this
125+ | (P _ lcon _, _) <- unApply lt,
126+ (P _ rcon _, _) <- unApply rt,
128+ = case lookupTyExact (rewrite_name lcon) (tt_ctxt ist) of
129+ Just _ -> return (rewrite_name lcon)
130+ Nothing -> rewriteFail lt rt
124− | otherwise = lift . tfail .
131+ | otherwise = rewriteFail lt rt
132+ where rewriteFail lt rt = lift . tfail .
125 Msg $ "Can't rewrite heterogeneous equality on types " ++
133 Msg $ "Can't rewrite heterogeneous equality on types " ++
126 show (delab ist lt) ++ " and " ++ show (delab ist rt)
134 show (delab ist lt) ++ " and " ++ show (delab ist rt)
127findSubstFn (Just substfn_in) ist lt rt
136findSubstFn (Just substfn_in) ist lt rt
128 = case lookupTyName substfn_in (tt_ctxt ist) of
137 = case lookupTyName substfn_in (tt_ctxt ist) of
129 [(n, t)] -> return n
138 [(n, t)] -> return n
130 [] -> lift . tfail . NoSuchVariable $ substfn_in
139 [] -> lift . tfail . NoSuchVariable $ substfn_in
131 more -> lift . tfail . CantResolveAlts $ map fst more
140 more -> lift . tfail . CantResolveAlts $ map fst more
142+rewrite_name :: Name -> Name
143+rewrite_name n = sMN 0 (show n ++ "_rewrite_lemma")
145+data ParamInfo = Index
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 _ _ _ _ = []
161+isParam Index = False
163+isParam ImplicitIndex = False
164+isParam ImplicitParam = True
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 =
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
177+ let imps = case lookupCtxtExact n (idris_implicits ist) of
178+ Nothing -> repeat (pexp Placeholder)
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)
186+mkLemma :: ElabInfo -> Name -> Name -> [ParamInfo] -> Type -> Idris ()
187+mkLemma info lemma tcon ps ty =
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))
195+ let xarg = sMN 0 "x"
196+ let yarg = sMN 0 "y"
197+ let parg = sMN 0 "P"
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)]
210+ let lemLHS = PApp fc (PRef fc [] lemma)
211+ [pexp (PRef fc [] parg),
212+ pexp (PRef fc [] (sUN "Refl")),
213+ pexp (PRef fc [] prop)]
215+ let lemRHS = PRef fc [] prop
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 []])
227+ namesFrom x i = sMN i x : namesFrom x (i + 1)
230+ = PApp fc (PRef fc [] fn) (mkArgs pinfo ps is)
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
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