558d226 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Update elaborator for application of local variables

commit558d226cad3c1448d1dee073f87a51be20f2cd19 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 16 Jan 2012, 15:29 (15 years ago) parent22f40c1

3 files changed+9−6

compare with master

unifiedsplit

src/Core/ProofState.hs+5−4 src/Idris/AbsSyntax.hs+1−1 src/Idris/ElabTerm.hs+3−1

src/Core/ProofState.hs+5−4

@@ -460,14 +460,15 @@ processTactic Undo ps = case previous ps of

460460 Just pold -> return (pold, "")

461461processTactic EndUnify ps

462462 = let (h, ns) = unified ps

463− tm' = updateSolved ns (pterm ps)

464− probs' = updateProblems ns (problems ps) in

463+ ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns

464+ tm' = updateSolved ns' (pterm ps)

465+ probs' = updateProblems ns' (problems ps) in

465466 case probs' of

466467 [] -> return (ps { pterm = tm',

467468 unified = (h, []),

468− injective = map (tmap (updateSolved ns))

469+ injective = map (tmap (updateSolved ns'))

469470 (injective ps),

470− holes = holes ps \\ map fst ns }, "")

471+ holes = holes ps \\ map fst ns' }, "")

471472 errs@((_,_,_,err):_) -> tfail err

472473processTactic (Reorder n) ps

473474 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps

src/Idris/AbsSyntax.hs+1−1

@@ -1105,7 +1105,7 @@ aiFn ist fc f as

11051105 [(f',ns)] -> mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

11061106 [] -> if f `elem` idris_metavars ist

11071107 then PApp fc (PRef fc f) as

1108− else mkPApp fc 1 (PRef fc f) as

1108+ else mkPApp fc (length as) (PRef fc f) as

11091109 alts -> PAlternative $

11101110 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')

11111111 (insertImpl ns as)) alts

src/Idris/ElabTerm.hs+3−1

@@ -279,7 +279,9 @@ elab ist info pattern tcgen fn tm

279279 | otherwise = elabArg n t

280280 where elabArg n t

281281 = do hs <- get_holes

282− failed' <- case n `elem` hs of

282+ tm <- get_term

283+ failed' <- -- trace (show (n, t, hs, tm)) $

284+ case n `elem` hs of

283285 True ->

284286 if r

285287 then try (do focus n; elabE ina t; return failed)