git.iko.soy/Idris-dev
on master help sign in
Propagate function name to tactics
bd744f1Edwin Brady
src/Idris/AbsSyntaxTree.hs+1−1
compare with master
unifiedsplit
@@ -694,7 +694,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name
694 | MatchRefine Name
694 | MatchRefine Name
695 | LetTac Name t | LetTacTy Name t t
695 | LetTac Name t | LetTacTy Name t t
696 | Exact t | Compute | Trivial | TCInstance
696 | Exact t | Compute | Trivial | TCInstance
697− | ProofSearch (Maybe Name) Name [Name]
697+ | ProofSearch (Maybe Name) [Name]
698 | Solve
698 | Solve
699 | Attack
699 | Attack
700 | ProofState | ProofTerm | Undo
700 | ProofState | ProofTerm | Undo
src/Idris/DeepSeq.hs+2−2
@@ -205,8 +205,8 @@ instance (NFData t) => NFData (PTactic' t) where
205 rnf (Exact x1) = rnf x1 `seq` ()
205 rnf (Exact x1) = rnf x1 `seq` ()
206 rnf Compute = ()
206 rnf Compute = ()
207 rnf Trivial = ()
207 rnf Trivial = ()
208− rnf (ProofSearch x1 x2 x3)
208+ rnf (ProofSearch x1 x2)
209− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
209+ = rnf x1 `seq` rnf x2 `seq` ()
210 rnf Solve = ()
210 rnf Solve = ()
211 rnf Attack = ()
211 rnf Attack = ()
212 rnf ProofState = ()
212 rnf ProofState = ()
src/Idris/ElabTerm.hs+9−9
@@ -538,9 +538,9 @@ elab ist info pattern opts fn tm
538 mkN n = case namespace info of
538 mkN n = case namespace info of
539 Just xs@(_:_) -> sNS n xs
539 Just xs@(_:_) -> sNS n xs
540 _ -> n
540 _ -> 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
542 elab' ina (PTactics ts)
542 elab' ina (PTactics ts)
543− | not pattern = do mapM_ (runTac False ist) ts
543+ | not pattern = do mapM_ (runTac False ist fn) ts
544 | otherwise = elab' ina Placeholder
544 | otherwise = elab' ina Placeholder
545 elab' ina (PElabError e) = fail (pshow ist e)
545 elab' ina (PElabError e) = fail (pshow ist e)
546 elab' ina (PRewrite fc r sc newg)
546 elab' ina (PRewrite fc r sc newg)
@@ -950,8 +950,8 @@ collectDeferred top t = return t
950-- Running tactics directly
950-- Running tactics directly
951-- if a tactic adds unification problems, return an error
951-- if a tactic adds unification problems, return an error
952
952
953−runTac :: Bool -> IState -> PTactic -> ElabD ()
953+runTac :: Bool -> IState -> Name -> PTactic -> ElabD ()
954−runTac autoSolve ist tac
954+runTac autoSolve ist fn tac
955 = do env <- get_env
955 = do env <- get_env
956 g <- goal
956 g <- goal
957 if autoSolve
957 if autoSolve
@@ -1065,8 +1065,8 @@ runTac autoSolve ist tac
1065 runT Compute = compute
1065 runT Compute = compute
1066 runT Trivial = do trivial' ist; when autoSolve solveAll
1066 runT Trivial = do trivial' ist; when autoSolve solveAll
1067 runT TCInstance = runT (Exact (PResolveTC emptyFC))
1067 runT TCInstance = runT (Exact (PResolveTC emptyFC))
1068− runT (ProofSearch top n hints)
1068+ runT (ProofSearch top hints)
1069− = do proofSearch' ist top n hints; when autoSolve solveAll
1069+ = do proofSearch' ist top fn hints; when autoSolve solveAll
1070 runT (Focus n) = focus n
1070 runT (Focus n) = focus n
1071 runT Solve = solve
1071 runT Solve = solve
1072 runT (Try l r) = do try' (runT l) (runT r) True
1072 runT (Try l r) = do try' (runT l) (runT r) True
@@ -1145,7 +1145,7 @@ runTac autoSolve ist tac
1145 ctxt <- get_context
1145 ctxt <- get_context
1146 env <- get_env
1146 env <- get_env
1147 let value' = hnf ctxt env value
1147 let value' = hnf ctxt env value
1148− runTac autoSolve ist (Exact $ PQuote (reflect value'))
1148+ runTac autoSolve ist fn (Exact $ PQuote (reflect value'))
1149 runT (Fill v) = do attack -- let x = fill x in ...
1149 runT (Fill v) = do attack -- let x = fill x in ...
1150 tyn <- getNameFrom (sMN 0 "letty")
1150 tyn <- getNameFrom (sMN 0 "letty")
1151 claim tyn RType
1151 claim tyn RType
@@ -1160,7 +1160,7 @@ runTac autoSolve ist tac
1160 env <- get_env
1160 env <- get_env
1161 let value' = normalise ctxt env value
1161 let value' = normalise ctxt env value
1162 rawValue <- reifyRaw value'
1162 rawValue <- reifyRaw value'
1163− runTac autoSolve ist (Exact $ PQuote rawValue)
1163+ runTac autoSolve ist fn (Exact $ PQuote rawValue)
1164 runT (GoalType n tac) = do g <- goal
1164 runT (GoalType n tac) = do g <- goal
1165 case unApply g of
1165 case unApply g of
1166 (P _ n' _, _) ->
1166 (P _ n' _, _) ->
@@ -1173,7 +1173,7 @@ runTac autoSolve ist tac
1173 runT x = fail $ "Not implemented " ++ show x
1173 runT x = fail $ "Not implemented " ++ show x
1174
1174
1175 runReflected t = do t' <- reify ist t
1175 runReflected t = do t' <- reify ist t
1176− runTac autoSolve ist t'
1176+ runTac autoSolve ist fn t'
1177
1177
1178-- | Prefix a name with the "Language.Reflection" namespace
1178-- | Prefix a name with the "Language.Reflection" namespace
1179reflm :: String -> Name
1179reflm :: String -> Name
src/Idris/ParseExpr.hs+1−2
@@ -1165,8 +1165,7 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (
1165 return $ TSeq t (mergeSeq ts)
1165 return $ TSeq t (mergeSeq ts)
1166 <|> do reserved "compute"; return Compute
1166 <|> do reserved "compute"; return Compute
1167 <|> do reserved "trivial"; return Trivial
1167 <|> 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 [])
1170 <|> do reserved "instance"; return TCInstance
1169 <|> do reserved "instance"; return TCInstance
1171 <|> do reserved "solve"; return Solve
1170 <|> do reserved "solve"; return Solve
1172 <|> do reserved "attack"; return Attack
1171 <|> do reserved "attack"; return Attack
src/Idris/Prover.hs+5−5
@@ -59,7 +59,7 @@ prove :: Context -> Bool -> Name -> Type -> Idris ()
59prove ctxt lit n ty
59prove ctxt lit n ty
60 = do let ps = initElaborator n ctxt ty
60 = do let ps = initElaborator n ctxt ty
61 ideslavePutSExp "start-proof-mode" n
61 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
63 iLOG $ "Adding " ++ show tm
63 iLOG $ "Adding " ++ show tm
64 iputStrLn $ showProof lit n prf
64 iputStrLn $ showProof lit n prf
65 i <- getIState
65 i <- getIState
@@ -161,8 +161,8 @@ receiveInput e =
161 Just (Interpret cmd) -> return (Just cmd)
161 Just (Interpret cmd) -> return (Just cmd)
162 Nothing -> return Nothing
162 Nothing -> return Nothing
163
163
164−ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
164+ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
165−ploop d prompt prf e h
165+ploop fn d prompt prf e h
166 = do i <- getIState
166 = do i <- getIState
167 when d $ dumpState i (proof e)
167 when d $ dumpState i (proof e)
168 (x, h') <-
168 (x, h') <-
@@ -260,7 +260,7 @@ ploop d prompt prf e h
260 return (False, e, False, prf))
260 return (False, e, False, prf))
261 (\err -> do putIState ist ; ierror err)
261 (\err -> do putIState ist ; ierror err)
262 Success tac -> do (_, e) <- elabStep e saveState
262 Success tac -> do (_, e) <- elabStep e saveState
263− (_, st) <- elabStep e (runTac True i tac)
263+ (_, st) <- elabStep e (runTac True i fn tac)
264-- trace (show (problems (proof st))) $
264-- trace (show (problems (proof st))) $
265 iPrintResult ""
265 iPrintResult ""
266 return (True, st, False, prf ++ [step]))
266 return (True, st, False, prf ++ [step]))
@@ -269,5 +269,5 @@ ploop d prompt prf e h
269 ideslavePutSExp "write-proof-state" (prf', length prf')
269 ideslavePutSExp "write-proof-state" (prf', length prf')
270 if done then do (tm, _) <- elabStep st get_term
270 if done then do (tm, _) <- elabStep st get_term
271 return (tm, prf')
271 return (tm, prf')
272− else ploop d prompt prf' st h'
272+ else ploop fn d prompt prf' st h'
273 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
273 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)
724 Just (t, e, False) -> (t, e, False)
724 Just (t, e, False) -> (t, e, False)
725 _ -> (Nothing, 0, True)
725 _ -> (Nothing, 0, True)
726 let fc = fileFC fn
726 let fc = fileFC fn
727− let body t = PProof [Try (TSeq Intros (ProofSearch t n hints))
727+ let body t = PProof [Try (TSeq Intros (ProofSearch t hints))
728− (ProofSearch t n hints)]
728+ (ProofSearch t hints)]
729 let def = PClause fc mn (PRef fc mn) [] (body top) []
729 let def = PClause fc mn (PRef fc mn) [] (body top) []
730 newmv <- idrisCatch
730 newmv <- idrisCatch
731 (do elabDecl' EAll toplevel (PClauses fc [] mn [def])
731 (do elabDecl' EAll toplevel (PClauses fc [] mn [def])