c66bf01 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Don't uniquify MN patvar names in reflected Elab

c66bf01David Raymond Christiansen11 years ago

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

compare with master

unifiedsplit

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

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

399equiv tm = processTactic' (Equiv tm)

400

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

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

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

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

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

404patvar n = do env <- get_env

405patvar n = do env <- get_env

405 hs <- get_holes

406 hs <- get_holes

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

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

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

411 x -> return $! n

412 x -> return $! n

412 processTactic' (PatVar n')

413 processTactic' (PatVar n')

413

414

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+

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

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

415patbind n = processTactic' (PatBind n)

425patbind n = processTactic' (PatBind n)

416

426

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

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

1883 returnUnit

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

1885 = do n' <- reifyTTName n

1886− patvar n'

1886+ patvar' n'

1887 returnUnit

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

1889 = do n' <- reifyTTName n