git.iko.soy/Idris-dev
on master help sign in
Fix for name clashes when applying transformations

Fixes #1684, and most likely a lot of other partial evaluation problems. IBC version updated since the problem may show up in any library code that's currently built.

commit2c3928683c895e450e72dd8ec52e061e6c5504a7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 9 Dec 2014, 12:46 (12 years ago) parentf01c1a1
3 files changed+20−3
compare with master
unifiedsplit
src/Idris/Elab/Transform.hs+14−2 src/Idris/IBC.hs+1−1 src/Idris/Transforms.hs+5
src/Idris/Elab/Transform.hs+14−2
@@ -61,8 +61,10 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in
6161 let lhs_ty = getInferType lhs'
6262 let newargs = pvars i lhs_tm
6363
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
6566 logLvl 3 ("Transform LHS " ++ show clhs_tm)
67+
6668 let rhs = addImplBound i (map fst newargs) rhs_in
6769 ((rhs', defer), _) <-
6870 tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty []
@@ -72,8 +74,10 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in
7274 erun fc $ psolve lhs_tm
7375 tt <- get_term
7476 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
7679 logLvl 3 ("Transform RHS " ++ show crhs_tm)
80+
7781 -- Types must always convert
7882 case converts ctxt [] clhs_ty crhs_ty of
7983 OK _ -> return ()
@@ -94,6 +98,14 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in
9498 depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)
9599 depat x = x
96100
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+
97109elabTransform info fc safe lhs_in rhs_in
98110 = ierror (At fc (Msg "Invalid transformation rule (must be function application)"))
99111
src/Idris/IBC.hs+1−1
@@ -32,7 +32,7 @@ import Codec.Compression.Zlib (compress)
3232import Util.Zlib (decompressEither)
3333
3434ibcVersion :: Word8
35−ibcVersion = 85
35+ibcVersion = 86
3636
3737data IBCFile = IBCFile { ver :: Word8,
3838 sourcefile :: FilePath,
src/Idris/Transforms.hs+5
@@ -71,6 +71,11 @@ applyRule (lhs, rhs) tm
7171-- ++ "\n" ++ show tm ++ " GIVES\n" ++ show (depat ms rhs)) $
7272 = Just $ depat ms rhs
7373 | 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).
7479 where depat ms (Bind n (PVar t) sc)
7580 = case lookup n ms of
7681 Just tm -> depat ms (subst n tm sc)