git.iko.soy/Idris-dev
on master help sign in
Modify the way of finding rewriting lemma
40182daEdwin Brady
CHANGELOG.md+7
compare with master
unifiedsplit
@@ -1,5 +1,12 @@
1# New in 0.12:
1# New in 0.12:
2
2
3+## Language updates
4+
5+* `rewrite` can now be given an optional rewriting lemma, with the syntax
6+ `rewrite [rule] using [rewrite_lemma] in [scope]`.
7+
8+## Miscellaneous updates
9+
3* Improved startup performance by reducing the processing of an already imported
10* Improved startup performance by reducing the processing of an already imported
4 module that has changed accessibility.
11 module that has changed accessibility.
5
12
src/Idris/Elab/Rewrite.hs+18−10
@@ -40,14 +40,8 @@ elabRewrite elab ist fc Nothing rule sc newg
40 Just t -> doEquiv elab fc t sc
40 Just t -> doEquiv elab fc t sc
41 solve
41 solve
42 -}
42 -}
43−elabRewrite elab ist fc Nothing rule sc newg
44− = elabRewrite elab ist fc (Just (sUN "rewrite__impl")) rule sc newg
45−elabRewrite elab ist fc (Just substfn_in) rule sc_in newg
43+elabRewrite elab ist fc substfn_in rule sc_in newg
46− = do substfn <- case lookupTyName substfn_in (tt_ctxt ist) of
47− [(n, t)] -> return n
48− [] -> lift . tfail . NoSuchVariable $ substfn_in
49− more -> lift . tfail . CantResolveAlts $ map fst more
50− attack
44+ = do attack
51 sc <- case newg of
45 sc <- case newg of
52 Nothing -> return sc_in
46 Nothing -> return sc_in
53 Just t -> do
47 Just t -> do
@@ -70,7 +64,8 @@ elabRewrite elab ist fc (Just substfn_in) rule sc_in newg
70 rname <- unique_hole (sMN 0 "replaced")
64 rname <- unique_hole (sMN 0 "replaced")
71 case unApply ttrule of
65 case unApply ttrule of
72 (P _ (UN q) _, [lt, rt, l, r]) | q == txt "=" ->
66 (P _ (UN q) _, [lt, rt, l, r]) | q == txt "=" ->
67+ do substfn <- findSubstFn substfn_in ist lt rt
73− do let pred_tt = mkP (P Bound rname rt) l r g
68+ let pred_tt = mkP (P Bound rname rt) l r g
74 when (g == pred_tt) $ lift $ tfail (NoRewriting g)
69 when (g == pred_tt) $ lift $ tfail (NoRewriting g)
75 let pred = PLam fc rname fc Placeholder
70 let pred = PLam fc rname fc Placeholder
76 (delab ist pred_tt)
71 (delab ist pred_tt)
@@ -120,4 +115,17 @@ elabRewrite elab ist fc (Just substfn_in) rule sc_in newg
120 where removeImp tm@(PImp{}) = tm { getTm = Placeholder }
115 where removeImp tm@(PImp{}) = tm { getTm = Placeholder }
121 removeImp t = t
116 removeImp t = t
122 phApps tm = tm
117 phApps tm = tm
123−
118+
119+findSubstFn :: Maybe Name -> IState -> Type -> Type -> ElabD Name
120+findSubstFn Nothing ist lt rt
121+ | lt == rt = return (sUN "rewrite__impl")
122+ -- TODO: Find correct rewriting lemma, if it exists, and tidy up this
123+ -- error
124+ | otherwise = lift . tfail .
125+ Msg $ "Can't rewrite heterogeneous equality on types " ++
126+ show (delab ist lt) ++ " and " ++ show (delab ist rt)
127+findSubstFn (Just substfn_in) ist lt rt
128+ = case lookupTyName substfn_in (tt_ctxt ist) of
129+ [(n, t)] -> return n
130+ [] -> lift . tfail . NoSuchVariable $ substfn_in
131+ more -> lift . tfail . CantResolveAlts $ map fst more
src/Idris/Elab/Term.hs+2−2
@@ -996,8 +996,8 @@ elab ist info emode opts fn tm
996 | not pattern = do mapM_ (runTac False ist fc fn) ts
996 | not pattern = do mapM_ (runTac False ist fc fn) ts
997 | otherwise = elab' ina fc Placeholder
997 | otherwise = elab' ina fc Placeholder
998 elab' ina fc (PElabError e) = lift $ tfail e
998 elab' ina fc (PElabError e) = lift $ tfail e
999− elab' ina _ (PRewrite fc substfn rule sc newg)
999+ elab' ina mfc (PRewrite fc substfn rule sc newg)
1000− = elabRewrite (elab' ina (Just fc)) ist fc substfn rule sc newg
1000+ = elabRewrite (elab' ina mfc) ist fc substfn rule sc newg
1001 elab' ina _ c@(PCase fc scr opts)
1001 elab' ina _ c@(PCase fc scr opts)
1002 = do attack
1002 = do attack
1003
1003