@@ -692,24 +692,36 @@ expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
692 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
692 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
693 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
693 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
694 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
694 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
695− n' = if n `elem` ns then dec n else n in
695+ n' = if n `elem` ns then dec n else n
696+ -- names bound on the lhs should not be expanded on the rhs
697+ ns' = removeBound lhs ns in
696 PClause fc n' lhs'
698 PClause fc n' lhs'
697− (map (expandParams dec ps'' ns []) ws)
699+ (map (expandParams dec ps'' ns' []) ws)
698− (expandParams dec ps'' ns [] rhs)
700+ (expandParams dec ps'' ns' [] rhs)
699− (map (expandParamsD True ist dec ps'' ns) ds)
701+ (map (expandParamsD True ist dec ps'' ns') ds)
700 expandParamsC (PWith fc n lhs ws wval ds)
702 expandParamsC (PWith fc n lhs ws wval ds)
701 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
703 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
702 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
704 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
703 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
705 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
704− n' = if n `elem` ns then dec n else n in
706+ n' = if n `elem` ns then dec n else n
707+ ns' = removeBound lhs ns in
705 PWith fc n' lhs'
708 PWith fc n' lhs'
706− (map (expandParams dec ps'' ns []) ws)
709+ (map (expandParams dec ps'' ns' []) ws)
707− (expandParams dec ps'' ns [] wval)
710+ (expandParams dec ps'' ns' [] wval)
708− (map (expandParamsD rhsonly ist dec ps'' ns) ds)
711+ (map (expandParamsD rhsonly ist dec ps'' ns') ds)
709 updateps yn nm [] = []
712 updateps yn nm [] = []
710 updateps yn nm (((a, t), i):as)
713 updateps yn nm (((a, t), i):as)
711 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
714 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
712 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
715 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
717+ removeBound lhs ns = ns \\ nub (bnames lhs)
719+ bnames (PRef _ n) = [n]
720+ bnames (PApp _ _ args) = concatMap bnames (map getTm args)
721+ bnames (PPair _ l r) = bnames l ++ bnames r
722+ bnames (PDPair _ l Placeholder r) = bnames l ++ bnames r
713expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
725expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
714 = PData doc syn fc co (expandPData pd)
726 = PData doc syn fc co (expandPData pd)