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

git.iko.soy/Idris-dev

on master help sign in

Fix scope/matching issues in proof scripts

29c02f4Edwin Brady12 years ago

src/Idris/AbsSyntax.hs+3−3

compare with master

unifiedsplit

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

1399 ai qq env ds (PApp fc f as)

1400 = let f' = ai qq env ds f

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

1402− mkPApp fc 1 f' as'

1402+ mkPApp fc 1 f' as'

1403 ai qq env ds (PCase fc c os)

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

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

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

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

1425 PGoal fc r' n sc'

1426 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)

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

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

1428+ -- properly known in ElabTerm.runTac

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

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

1431 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

806 do ty <- goal

807 env <- get_env

808 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]

810 case tyh of

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

812 -> return (PAlternative False tries)

813 _ -> return t

814 where

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

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

816+ mkDelay env t

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

817+ = let fc = fileFC "Delay" in

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

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

818− [pexp t])

819+ [pexp t])

819

820

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

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

821 -- they can go in the branches separately.

822 -- they can go in the branches separately.

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

831 (PCoerced tm, _) -> tm

832 (PCoerced tm, _) -> tm

832 (_, []) -> t

833 (_, []) -> t

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

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

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

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

835 return t'

836 return t'

836 where

837 where

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

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

839+ addImplBound ist (map fst env)

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

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

839

841

840 -- | Elaborate the arguments to a function

842 -- | Elaborate the arguments to a function

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

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

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

1101runTac autoSolve ist fn tac

1103runTac autoSolve ist fn tac

1102 = do env <- get_env

1104 = do env <- get_env

1103 g <- goal

1105 g <- goal

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

1104 if autoSolve

1107 if autoSolve

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

1108+ then runT tac'

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

1109+ else no_errors (runT tac')

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

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

1108 where

1111 where

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

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

src/Idris/Prover.hs+2

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

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

101 Error a -> ierror a

102 where eCheck = do res <- e

103+ matchProblems True

104+ unifyProblems

103 probs' <- get_probs

105 probs' <- get_probs

104 case probs' of

106 case probs' of

105 [] -> do tm <- get_term

107 [] -> do tm <- get_term