git.iko.soy/Idris-dev
on master help sign in
Moved pinfo back into the where block
e8ea34bTimo Petteri Sinnemäki
src/Idris/ElabDecls.hs+13−12
compare with master
unifiedsplit
@@ -1505,6 +1505,19 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1505 addErrRev (crhs, clhs)
1505 addErrRev (crhs, clhs)
1506 return $ Right (clhs, crhs)
1506 return $ Right (clhs, crhs)
1507 where
1507 where
1508+ pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo
1509+ pinfo info ns ds i
1510+ = let newps = params info ++ ns
1511+ dsParams = map (\n -> (n, map fst newps)) ds
1512+ newb = addAlist dsParams (inblock info)
1513+ l = liftname info in
1514+ info { params = newps,
1515+ inblock = newb,
1516+ liftname = id -- (\n -> case lookupCtxt n newb of
1517+ -- Nothing -> n
1518+ -- _ -> MN i (show n)) . l
1519+ }
1520+
1508 mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []
1521 mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []
1509 mkLHSapp t = t
1522 mkLHSapp t = t
1510
1523
@@ -2157,18 +2170,6 @@ psolve tm = return ()
2157pvars ist (Bind n (PVar t) sc) = (n, delab ist t) : pvars ist sc
2170pvars ist (Bind n (PVar t) sc) = (n, delab ist t) : pvars ist sc
2158pvars ist _ = []
2171pvars ist _ = []
2159
2172
2160−pinfo info ns ds i
2161− = let newps = params info ++ ns
2162− dsParams = map (\n -> (n, map fst newps)) ds
2163− newb = addAlist dsParams (inblock info)
2164− l = liftname info in
2165− info { params = newps,
2166− inblock = newb,
2167− liftname = id -- (\n -> case lookupCtxt n newb of
2168− -- Nothing -> n
2169− -- _ -> MN i (show n)) . l
2170− }
2171−
2172data ElabWhat = ETypes | EDefns | EAll
2173data ElabWhat = ETypes | EDefns | EAll
2173 deriving (Show, Eq)
2174 deriving (Show, Eq)
2174
2175