bd744f1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Propagate function name to tactics

Handy for knowing where we are in proof search, for example

commitbd744f17530509b1106e288e5dbe989fc9ded436 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 28 Feb 2014, 18:16 (13 years ago) parentc37de47

6 files changed+20−21

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/DeepSeq.hs+2−2 src/Idris/ElabTerm.hs+9−9 src/Idris/ParseExpr.hs+1−2 src/Idris/Prover.hs+5−5 src/Idris/REPL.hs+2−2

src/Idris/AbsSyntaxTree.hs+1−1

@@ -694,7 +694,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

694694 | MatchRefine Name

695695 | LetTac Name t | LetTacTy Name t t

696696 | Exact t | Compute | Trivial | TCInstance

697− | ProofSearch (Maybe Name) Name [Name]

697+ | ProofSearch (Maybe Name) [Name]

698698 | Solve

699699 | Attack

700700 | ProofState | ProofTerm | Undo

src/Idris/DeepSeq.hs+2−2

@@ -205,8 +205,8 @@ instance (NFData t) => NFData (PTactic' t) where

205205 rnf (Exact x1) = rnf x1 `seq` ()

206206 rnf Compute = ()

207207 rnf Trivial = ()

208− rnf (ProofSearch x1 x2 x3)

209− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

208+ rnf (ProofSearch x1 x2)

209+ = rnf x1 `seq` rnf x2 `seq` ()

210210 rnf Solve = ()

211211 rnf Attack = ()

212212 rnf ProofState = ()

src/Idris/ElabTerm.hs+9−9

@@ -538,9 +538,9 @@ elab ist info pattern opts fn tm

538538 mkN n = case namespace info of

539539 Just xs@(_:_) -> sNS n xs

540540 _ -> n

541− elab' ina (PProof ts) = do compute; mapM_ (runTac True ist) ts

541+ elab' ina (PProof ts) = do compute; mapM_ (runTac True ist fn) ts

542542 elab' ina (PTactics ts)

543− | not pattern = do mapM_ (runTac False ist) ts

543+ | not pattern = do mapM_ (runTac False ist fn) ts

544544 | otherwise = elab' ina Placeholder

545545 elab' ina (PElabError e) = fail (pshow ist e)

546546 elab' ina (PRewrite fc r sc newg)

@@ -950,8 +950,8 @@ collectDeferred top t = return t

950950-- Running tactics directly

951951-- if a tactic adds unification problems, return an error

952952

953−runTac :: Bool -> IState -> PTactic -> ElabD ()

954−runTac autoSolve ist tac

953+runTac :: Bool -> IState -> Name -> PTactic -> ElabD ()

954+runTac autoSolve ist fn tac

955955 = do env <- get_env

956956 g <- goal

957957 if autoSolve

@@ -1065,8 +1065,8 @@ runTac autoSolve ist tac

10651065 runT Compute = compute

10661066 runT Trivial = do trivial' ist; when autoSolve solveAll

10671067 runT TCInstance = runT (Exact (PResolveTC emptyFC))

1068− runT (ProofSearch top n hints)

1069− = do proofSearch' ist top n hints; when autoSolve solveAll

1068+ runT (ProofSearch top hints)

1069+ = do proofSearch' ist top fn hints; when autoSolve solveAll

10701070 runT (Focus n) = focus n

10711071 runT Solve = solve

10721072 runT (Try l r) = do try' (runT l) (runT r) True

@@ -1145,7 +1145,7 @@ runTac autoSolve ist tac

11451145 ctxt <- get_context

11461146 env <- get_env

11471147 let value' = hnf ctxt env value

1148− runTac autoSolve ist (Exact $ PQuote (reflect value'))

1148+ runTac autoSolve ist fn (Exact $ PQuote (reflect value'))

11491149 runT (Fill v) = do attack -- let x = fill x in ...

11501150 tyn <- getNameFrom (sMN 0 "letty")

11511151 claim tyn RType

@@ -1160,7 +1160,7 @@ runTac autoSolve ist tac

11601160 env <- get_env

11611161 let value' = normalise ctxt env value

11621162 rawValue <- reifyRaw value'

1163− runTac autoSolve ist (Exact $ PQuote rawValue)

1163+ runTac autoSolve ist fn (Exact $ PQuote rawValue)

11641164 runT (GoalType n tac) = do g <- goal

11651165 case unApply g of

11661166 (P _ n' _, _) ->

@@ -1173,7 +1173,7 @@ runTac autoSolve ist tac

11731173 runT x = fail $ "Not implemented " ++ show x

11741174

11751175 runReflected t = do t' <- reify ist t

1176− runTac autoSolve ist t'

1176+ runTac autoSolve ist fn t'

11771177

11781178-- | Prefix a name with the "Language.Reflection" namespace

11791179reflm :: String -> Name

src/Idris/ParseExpr.hs+1−2

@@ -1165,8 +1165,7 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (

11651165 return $ TSeq t (mergeSeq ts)

11661166 <|> do reserved "compute"; return Compute

11671167 <|> do reserved "trivial"; return Trivial

1168− <|> do reserved "search"; n <- (indentPropHolds gtProp *> fnName)

1169− return (ProofSearch Nothing n [])

1168+ <|> do reserved "search"; return (ProofSearch Nothing [])

11701169 <|> do reserved "instance"; return TCInstance

11711170 <|> do reserved "solve"; return Solve

11721171 <|> do reserved "attack"; return Attack

src/Idris/Prover.hs+5−5

@@ -59,7 +59,7 @@ prove :: Context -> Bool -> Name -> Type -> Idris ()

5959prove ctxt lit n ty

6060 = do let ps = initElaborator n ctxt ty

6161 ideslavePutSExp "start-proof-mode" n

62− (tm, prf) <- ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing

62+ (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing

6363 iLOG $ "Adding " ++ show tm

6464 iputStrLn $ showProof lit n prf

6565 i <- getIState

@@ -161,8 +161,8 @@ receiveInput e =

161161 Just (Interpret cmd) -> return (Just cmd)

162162 Nothing -> return Nothing

163163

164−ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])

165−ploop d prompt prf e h

164+ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])

165+ploop fn d prompt prf e h

166166 = do i <- getIState

167167 when d $ dumpState i (proof e)

168168 (x, h') <-

@@ -260,7 +260,7 @@ ploop d prompt prf e h

260260 return (False, e, False, prf))

261261 (\err -> do putIState ist ; ierror err)

262262 Success tac -> do (_, e) <- elabStep e saveState

263− (_, st) <- elabStep e (runTac True i tac)

263+ (_, st) <- elabStep e (runTac True i fn tac)

264264-- trace (show (problems (proof st))) $

265265 iPrintResult ""

266266 return (True, st, False, prf ++ [step]))

@@ -269,5 +269,5 @@ ploop d prompt prf e h

269269 ideslavePutSExp "write-proof-state" (prf', length prf')

270270 if done then do (tm, _) <- elabStep st get_term

271271 return (tm, prf')

272− else ploop d prompt prf' st h'

272+ else ploop fn d prompt prf' st h'

273273 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env

src/Idris/REPL.hs+2−2

@@ -724,8 +724,8 @@ process h fn (DoProofSearch updatefile l n hints)

724724 Just (t, e, False) -> (t, e, False)

725725 _ -> (Nothing, 0, True)

726726 let fc = fileFC fn

727− let body t = PProof [Try (TSeq Intros (ProofSearch t n hints))

728− (ProofSearch t n hints)]

727+ let body t = PProof [Try (TSeq Intros (ProofSearch t hints))

728+ (ProofSearch t hints)]

729729 let def = PClause fc mn (PRef fc mn) [] (body top) []

730730 newmv <- idrisCatch

731731 (do elabDecl' EAll toplevel (PClauses fc [] mn [def])