6c39e35 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix parameter expansion in PEq case

commit6c39e35d9470bfe9df5fef99cbfd4a4191e7744b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 9 Jul 2014, 23:01 (12 years ago) parentecc5277

2 files changed+3−3

unifiedsplit

src/Idris/AbsSyntax.hs+1−1

@@ -853,7 +853,7 @@ expandParams dec ps ns infs tm = en tm

853853 | n `elem` (map fst ps ++ ns) && t /= Placeholder

854854 = let n' = mkShadow n in

855855 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))

856− en (PEq f lt rt l r) = PEq f (en lt) (en r) (en l) (en r)

856+ en (PEq f lt rt l r) = PEq f (en lt) (en rt) (en l) (en r)

857857 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)

858858 en (PTyped l r) = PTyped (en l) (en r)

859859 en (PPair f p l r) = PPair f p (en l) (en r)

src/Idris/ElabTerm.hs+2−2

@@ -255,8 +255,8 @@ elab ist info emode opts fn tm

255255 = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,

256256 pimp (sMN 0 "x") t False])

257257 elab' ina (PEq fc lt rt l r) = elab' ina (PApp fc (PRef fc eqTy)

258− [pimp (sUN "A") Placeholder True,

259− pimp (sUN "B") Placeholder False,

258+ [pimp (sUN "A") lt True,

259+ pimp (sUN "B") rt False,

260260 pexp l, pexp r])

261261 elab' ina@(_, a, inty, qq) (PPair fc _ l r)

262262 = do hnf_compute