2196023 · Idris-dev · git.iko.soy

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

compare with master

unifiedsplit

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

463equiv tm = processTactic' (Equiv tm)

464

465-- | 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

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

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

469patvar n = do env <- get_env

470 hs <- get_holes

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

472− else do n' <- case n of

472+ else do n' <- case hs of

473− UN _ -> return $! n

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

474− MN _ _ -> unique_hole n

474+ else unique_hole n

475− NS _ _ -> return $! n

475+ _ -> unique_hole n

476− x -> return $! n

477− processTactic' (PatVar n')

476+ processTactic' (PatVar n)

478

477

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

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

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

479-- 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

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

171 (updsubst n v t', True)

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

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

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

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

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

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

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

176− else (tm, False)

176+ else (tm, False)

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

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

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

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

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

705 solve

706 highlightSource nfc (AnnBoundName n False)

707 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")

709 addAutoBind p n

710 addPSname n -- okay for proof search

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

712 solve

713 highlightSource nfc (AnnBoundName n False)

714 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")

716 claim tyn RType

717 n' <- case n of

718 MN _ _ -> unique_hole n

test/dsl001/expected+4−4

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

124

212

3testFac : Int

4−testFac = PE_interp_f79b3e31 [] (PE_fromInteger_d6648df 4)

4+testFac = PE_interp_e04a79ff [] (PE_fromInteger_d6648df 4)

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

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

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

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

7 ifThenElse (PE_==_ba2f651f x

8 (PE_fromInteger_d6648df 0))

9 (Delay (PE_fromInteger_d6648df 1))

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

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

11 (3arg))

12 (PE_-_ba2f651f x

13 (PE_fromInteger_d6648df 1)))

test/dsl001/input+1−1

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

1: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./

4Usage is :doc <functionname>

5Usage is :wc <functionname>

6Usage 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}

8

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}

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

11 dependent type signature,

12 end of input