c66bf01 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Don't uniquify MN patvar names in reflected Elab

This should be done in Idris code.

commitc66bf01c65d4a0d782e0ef90924c938f3930ea33 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 28 May 2015, 10:37 (11 years ago) parent4dabdba

2 files changed+13−3

compare with master

unifiedsplit

src/Idris/Core/Elaborate.hs+12−2 src/Idris/Elab/Term.hs+1−1

src/Idris/Core/Elaborate.hs+12−2

@@ -398,9 +398,10 @@ casetac tm = processTactic' (CaseTac tm)

398398equiv :: Raw -> Elab' aux ()

399399equiv tm = processTactic' (Equiv tm)

400400

401−-- | Turn the current hole into a pattern variable with the provided name, made unique if MN

401+-- | Turn the current hole into a pattern variable with the provided

402+-- name, made unique if MN

402403patvar :: Name -> Elab' aux ()

403−patvar n@(SN _) = do apply (Var n) []; solve

404+patvar n@(SN _) = do apply (Var n) []; solve

404405patvar n = do env <- get_env

405406 hs <- get_holes

406407 if (n `elem` map fst env) then do apply (Var n) []; solve

@@ -411,6 +412,15 @@ patvar n = do env <- get_env

411412 x -> return $! n

412413 processTactic' (PatVar n')

413414

415+-- | Turn the current hole into a pattern variable with the provided

416+-- name, but don't make MNs unique.

417+patvar' :: Name -> Elab' aux ()

418+patvar' n@(SN _) = do apply (Var n) [] ; solve

419+patvar' n = do env <- get_env

420+ hs <- get_holes

421+ if (n `elem` map fst env) then do apply (Var n) [] ; solve

422+ else processTactic' (PatVar n)

423+

414424patbind :: Name -> Elab' aux ()

415425patbind n = processTactic' (PatBind n)

416426

src/Idris/Elab/Term.hs+1−1

@@ -1883,7 +1883,7 @@ runTactical ist fc env tm = do tm' <- eval tm

18831883 returnUnit

18841884 | n == tacN "prim__PatVar", [n] <- args

18851885 = do n' <- reifyTTName n

1886− patvar n'

1886+ patvar' n'

18871887 returnUnit

18881888 | n == tacN "prim__PatBind", [n] <- args

18891889 = do n' <- reifyTTName n