git.iko.soy/Idris-dev
on master help sign in
Fix for name clashes when applying transformations
2c39286Edwin Brady
src/Idris/Elab/Transform.hs+14−2
compare with master
unifiedsplit
@@ -61,8 +61,10 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in
61 let lhs_ty = getInferType lhs'
61 let lhs_ty = getInferType lhs'
62 let newargs = pvars i lhs_tm
62 let newargs = pvars i lhs_tm
63
63
64− (clhs_tm, clhs_ty) <- recheckC fc [] lhs_tm
64+ (clhs_tm_in, clhs_ty) <- recheckC fc [] lhs_tm
65+ let clhs_tm = renamepats pnames clhs_tm_in
65 logLvl 3 ("Transform LHS " ++ show clhs_tm)
66 logLvl 3 ("Transform LHS " ++ show clhs_tm)
67+
66 let rhs = addImplBound i (map fst newargs) rhs_in
68 let rhs = addImplBound i (map fst newargs) rhs_in
67 ((rhs', defer), _) <-
69 ((rhs', defer), _) <-
68 tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty []
70 tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty []
@@ -72,8 +74,10 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in
72 erun fc $ psolve lhs_tm
74 erun fc $ psolve lhs_tm
73 tt <- get_term
75 tt <- get_term
74 return (runState (collectDeferred Nothing tt) []))
76 return (runState (collectDeferred Nothing tt) []))
75− (crhs_tm, crhs_ty) <- recheckC fc [] rhs'
77+ (crhs_tm_in, crhs_ty) <- recheckC fc [] rhs'
78+ let crhs_tm = renamepats pnames crhs_tm_in
76 logLvl 3 ("Transform RHS " ++ show crhs_tm)
79 logLvl 3 ("Transform RHS " ++ show crhs_tm)
80+
77 -- Types must always convert
81 -- Types must always convert
78 case converts ctxt [] clhs_ty crhs_ty of
82 case converts ctxt [] clhs_ty crhs_ty of
79 OK _ -> return ()
83 OK _ -> return ()
@@ -94,6 +98,14 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in
94 depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)
98 depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)
95 depat x = x
99 depat x = x
96
100
101+ renamepats (n' : ns) (Bind n (PVar t) sc)
102+ = Bind n' (PVar t) (renamepats ns sc) -- all Vs
103+ renamepats _ sc = sc
104+
105+ -- names for transformation variables. Need to ensure these don't clash
106+ -- with any other names when applying rules, so rename here.
107+ pnames = map (\i -> sMN i ("tvar" ++ show i)) [0..]
108+
97elabTransform info fc safe lhs_in rhs_in
109elabTransform info fc safe lhs_in rhs_in
98 = ierror (At fc (Msg "Invalid transformation rule (must be function application)"))
110 = ierror (At fc (Msg "Invalid transformation rule (must be function application)"))
99
111
src/Idris/IBC.hs+1−1
@@ -32,7 +32,7 @@ import Codec.Compression.Zlib (compress)
32import Util.Zlib (decompressEither)
32import Util.Zlib (decompressEither)
33
33
34ibcVersion :: Word8
34ibcVersion :: Word8
35−ibcVersion = 85
35+ibcVersion = 86
36
36
37data IBCFile = IBCFile { ver :: Word8,
37data IBCFile = IBCFile { ver :: Word8,
38 sourcefile :: FilePath,
38 sourcefile :: FilePath,
src/Idris/Transforms.hs+5
@@ -71,6 +71,11 @@ applyRule (lhs, rhs) tm
71-- ++ "\n" ++ show tm ++ " GIVES\n" ++ show (depat ms rhs)) $
71-- ++ "\n" ++ show tm ++ " GIVES\n" ++ show (depat ms rhs)) $
72 = Just $ depat ms rhs
72 = Just $ depat ms rhs
73 | otherwise = Nothing
73 | otherwise = Nothing
74+-- ASSUMPTION: The names in the transformation rule bindings cannot occur
75+-- in the term being transformed.
76+-- (In general, this would not be true, but when we elaborate transformation
77+-- rules we mangle the names so that it is true. While this feels a bit
78+-- hacky, it's much easier to think about than mangling de Bruijn indices).
74 where depat ms (Bind n (PVar t) sc)
79 where depat ms (Bind n (PVar t) sc)
75 = case lookup n ms of
80 = case lookup n ms of
76 Just tm -> depat ms (subst n tm sc)
81 Just tm -> depat ms (subst n tm sc)