git.iko.soy/Idris-dev
on master help sign in
Reinstate checking of rewrite result type
b66865fEdwin Brady
src/Idris/Elab/Rewrite.hs+7−17
compare with master
unifiedsplit
@@ -42,12 +42,18 @@ elabRewrite elab ist fc Nothing rule sc newg
42 -}
42 -}
43elabRewrite elab ist fc Nothing rule sc newg
43elabRewrite elab ist fc Nothing rule sc newg
44 = elabRewrite elab ist fc (Just (sUN "rewrite__impl")) 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 newg
45+elabRewrite elab ist fc (Just substfn_in) rule sc_in newg
46 = do substfn <- case lookupTyName substfn_in (tt_ctxt ist) of
46 = do substfn <- case lookupTyName substfn_in (tt_ctxt ist) of
47 [(n, t)] -> return n
47 [(n, t)] -> return n
48 [] -> lift . tfail . NoSuchVariable $ substfn_in
48 [] -> lift . tfail . NoSuchVariable $ substfn_in
49 more -> lift . tfail . CantResolveAlts $ map fst more
49 more -> lift . tfail . CantResolveAlts $ map fst more
50 attack
50 attack
51+ sc <- case newg of
52+ Nothing -> return sc_in
53+ Just t -> do
54+ letn <- getNameFrom (sMN 0 "rewrite_result")
55+ return $ PLet fc letn fc t sc_in
56+ (PRef fc [] letn)
51 tyn <- getNameFrom (sMN 0 "rty")
57 tyn <- getNameFrom (sMN 0 "rty")
52 claim tyn RType
58 claim tyn RType
53 valn <- getNameFrom (sMN 0 "rval")
59 valn <- getNameFrom (sMN 0 "rval")
@@ -115,19 +121,3 @@ elabRewrite elab ist fc (Just substfn_in) rule sc newg
115 removeImp t = t
121 removeImp t = t
116 phApps tm = tm
122 phApps tm = tm
117
123
118−doEquiv elab fc t sc
119− = do attack
120− tyn <- getNameFrom (sMN 0 "ety")
121− claim tyn RType
122− valn <- getNameFrom (sMN 0 "eqval")
123− claim valn (Var tyn)
124− letn <- getNameFrom (sMN 0 "equiv_val")
125− letbind letn (Var tyn) (Var valn)
126− focus tyn
127− elab t
128− focus valn
129− elab sc
130− elab (PRef fc [] letn)
131− solve
132−
133−