2196023 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix patvar naming for implicits

There's no need to make the name unique if the pattern is going to have the same name as the hole. Otherwise, this can cause problems under the types of metavariables, where the name gets renamed and the generated type is then no longer valid because there's an undefined name in it. Fixes #3398

commit2196023e1603e7f1c0a1ff7b9ac7600d2b336ba1 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 11 Dec 2016, 22:35 (10 years ago) parent7e93d70

6 files changed+19−20

compare with master

unifiedsplit

src/Idris/Core/Elaborate.hs+6−7 src/Idris/Core/ProofTerm.hs+4−4 src/Idris/Elab/Term.hs+2−2 test/dsl001/expected+4−4 test/dsl001/input+1−1 test/interactive010/expected+2−2

src/Idris/Core/Elaborate.hs+6−7

@@ -463,18 +463,17 @@ equiv :: Raw -> Elab' aux ()

463463equiv tm = processTactic' (Equiv tm)

464464

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

466−-- name, made unique if MN

466+-- name, made unique if not the same as the head of the hole queue

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

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

469469patvar n = do env <- get_env

470470 hs <- get_holes

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

472− else do n' <- case n of

473− UN _ -> return $! n

474− MN _ _ -> unique_hole n

475− NS _ _ -> return $! n

476− x -> return $! n

477− processTactic' (PatVar n')

472+ else do n' <- case hs of

473+ (h : hs) -> if n == h then return n

474+ else unique_hole n

475+ _ -> unique_hole n

476+ processTactic' (PatVar n)

478477

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

480479-- name, but don't make MNs unique.

src/Idris/Core/ProofTerm.hs+4−4

@@ -170,10 +170,10 @@ updateSolvedTerm' xs x = updateSolved' xs x where

170170 _ -> let (t', _) = updateSolved' xs t in

171171 (updsubst n v t', True)

172172 updateSolved' xs tm@(Bind n b t)

173− | otherwise = let (t', ut) = updateSolved' xs t

174− (b', ub) = updateSolvedB' xs b in

175− if ut || ub then (Bind n b' t', True)

176− else (tm, False)

173+ = let (t', ut) = updateSolved' xs t

174+ (b', ub) = updateSolvedB' xs b in

175+ if ut || ub then (Bind n b' t', True)

176+ else (tm, False)

177177 updateSolved' xs t@(App Complete f a) = (t, False)

178178 updateSolved' xs t@(App s f a)

179179 = let (f', uf) = updateSolved' xs f

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

@@ -705,14 +705,14 @@ elab ist info emode opts fn tm

705705 solve

706706 highlightSource nfc (AnnBoundName n False)

707707 elab' ina fc (PPi p n nfc Placeholder sc)

708− = do attack; arg n (is_scoped p) (sMN 0 "ty")

708+ = do attack; arg n (is_scoped p) (sMN 0 "phTy")

709709 addAutoBind p n

710710 addPSname n -- okay for proof search

711711 elabE (ina { e_inarg = True, e_intype = True }) fc sc

712712 solve

713713 highlightSource nfc (AnnBoundName n False)

714714 elab' ina fc (PPi p n nfc ty sc)

715− = do attack; tyn <- getNameFrom (sMN 0 "ty")

715+ = do attack; tyn <- getNameFrom (sMN 0 "piTy")

716716 claim tyn RType

717717 n' <- case n of

718718 MN _ _ -> unique_hole n

test/dsl001/expected+4−4

@@ -1,13 +1,13 @@

1124

2212

33testFac : Int

4−testFac = PE_interp_f79b3e31 [] (PE_fromInteger_d6648df 4)

5−PE_interp_f79b3e31 : Env G -> Int -> Int

6−PE_interp_f79b3e31 (3arg) = \x =>

4+testFac = PE_interp_e04a79ff [] (PE_fromInteger_d6648df 4)

5+PE_interp_e04a79ff : Env G -> Int -> Int

6+PE_interp_e04a79ff (3arg) = \x =>

77 ifThenElse (PE_==_ba2f651f x

88 (PE_fromInteger_d6648df 0))

99 (Delay (PE_fromInteger_d6648df 1))

10− (Delay (PE_*_ba2f651f (PE_interp_f79b3e31 (x ::

10+ (Delay (PE_*_ba2f651f (PE_interp_e04a79ff (x ::

1111 (3arg))

1212 (PE_-_ba2f651f x

1313 (PE_fromInteger_d6648df 1)))

test/dsl001/input+1−1

@@ -1,2 +1,2 @@

11:printdef testFac

2−:printdef PE_interp_f79b3e31

2+:printdef PE_interp_e04a79ff

test/interactive010/expected+2−2

@@ -4,9 +4,9 @@ a is not an implicit argument of Prelude.Interfaces./

44Usage is :doc <functionname>

55Usage is :wc <functionname>

66Usage is :printdef <functionname>

7−pat {ty504} : Type toplevel.u. pat {__interface505} : Prelude.Interfaces.Fractional {ty504}. Prelude.Interfaces./ {ty504} {__interface505}

7+pat {ty503} : Type toplevel.u. pat {__interface504} : Prelude.Interfaces.Fractional {ty503}. Prelude.Interfaces./ {ty503} {__interface504}

9− : pty {ty504} : Type toplevel.u. pty {__interface505} : Prelude.Interfaces.Fractional {ty504}. {ty504} -> {ty504} -> {ty504}

9+ : pty {ty503} : Type toplevel.u. pty {__interface504} : Prelude.Interfaces.Fractional {ty503}. {ty503} -> {ty503} -> {ty503}

1010(input):1:1: error: expected: ":",

1111 dependent type signature,

1212 end of input