29c02f4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix scope/matching issues in proof scripts

Need to treat appeals to tactics as independent calls to the elaborator, with known current scope, so don't add implicits until just before invoking the tactic, and add a final unify/match step to collect any missing implicits.

commit29c02f48afa7f20fd050868c5939eaaadca58472 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 12 Jul 2014, 14:03 (12 years ago) parent8ed343b

3 files changed+18−13

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+3−3 src/Idris/ElabTerm.hs+13−10 src/Idris/Prover.hs+2

src/Idris/AbsSyntax.hs+3−3

@@ -1399,7 +1399,7 @@ addImpl' inpat env infns ist ptm

13991399 ai qq env ds (PApp fc f as)

14001400 = let f' = ai qq env ds f

14011401 as' = map (fmap (ai qq env ds)) as in

1402− mkPApp fc 1 f' as'

1402+ mkPApp fc 1 f' as'

14031403 ai qq env ds (PCase fc c os)

14041404 = let c' = ai qq env ds c in

14051405 -- leave os alone, because they get lifted into a new pattern match

@@ -1424,8 +1424,8 @@ addImpl' inpat env infns ist ptm

14241424 sc' = ai qq ((n, Nothing):env) ds sc in

14251425 PGoal fc r' n sc'

14261426 ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)

1427− ai qq env ds (PProof ts) = PProof (map (fmap (ai qq env ds)) ts)

1428− ai qq env ds (PTactics ts) = PTactics (map (fmap (ai qq env ds)) ts)

1427+ -- Don't do PProof or PTactics since implicits get added when scope is

1428+ -- properly known in ElabTerm.runTac

14291429 ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)

14301430 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)

14311431 ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)

src/Idris/ElabTerm.hs+13−10

@@ -806,16 +806,17 @@ elab ist info emode opts fn tm

806806 do ty <- goal

807807 env <- get_env

808808 let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)

809− let tries = if pattern then [t, mkDelay t] else [mkDelay t, t]

809+ let tries = if pattern then [t, mkDelay env t] else [mkDelay env t, t]

810810 case tyh of

811811 P _ (UN l) _ | l == txt "Lazy'"

812812 -> return (PAlternative False tries)

813813 _ -> return t

814814 where

815− mkDelay (PAlternative b xs) = PAlternative b (map mkDelay xs)

816− mkDelay t = let fc = fileFC "Delay" in

817− addImpl ist (PApp fc (PRef fc (sUN "Delay"))

818− [pexp t])

815+ mkDelay env (PAlternative b xs) = PAlternative b (map (mkDelay env) xs)

816+ mkDelay env t

817+ = let fc = fileFC "Delay" in

818+ addImplBound ist (map fst env) (PApp fc (PRef fc (sUN "Delay"))

819+ [pexp t])

819820

820821 -- case is tricky enough without implicit coercions! If they are needed,

821822 -- they can go in the branches separately.

@@ -831,11 +832,12 @@ elab ist info emode opts fn tm

831832 (PCoerced tm, _) -> tm

832833 (_, []) -> t

833834 (_, cs) -> PAlternative False [t ,

834− PAlternative True (map (mkCoerce t) cs)]

835+ PAlternative True (map (mkCoerce env t) cs)]

835836 return t'

836837 where

837− mkCoerce t n = let fc = fileFC "Coercion" in -- line never appears!

838− addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)])

838+ mkCoerce env t n = let fc = fileFC "Coercion" in -- line never appears!

839+ addImplBound ist (map fst env)

840+ (PApp fc (PRef fc n) [pexp (PCoerced t)])

839841

840842 -- | Elaborate the arguments to a function

841843 elabArgs :: IState -- ^ The current Idris state

@@ -1101,9 +1103,10 @@ runTac :: Bool -> IState -> Name -> PTactic -> ElabD ()

11011103runTac autoSolve ist fn tac

11021104 = do env <- get_env

11031105 g <- goal

1106+ let tac' = fmap (addImplBound ist (map fst env)) tac

11041107 if autoSolve

1105− then runT (fmap (addImplBound ist (map fst env)) tac)

1106− else no_errors (runT (fmap (addImplBound ist (map fst env)) tac))

1108+ then runT tac'

1109+ else no_errors (runT tac')

11071110 (Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))

11081111 where

11091112 runT (Intro []) = do g <- goal

src/Idris/Prover.hs+2

@@ -100,6 +100,8 @@ elabStep st e = case runStateT eCheck st of

100100 OK (a, st') -> return (a, st')

101101 Error a -> ierror a

102102 where eCheck = do res <- e

103+ matchProblems True

104+ unifyProblems

103105 probs' <- get_probs

104106 case probs' of

105107 [] -> do tm <- get_term