git.iko.soy/Idris-dev
on master help sign in
A gadget or two
546e9f5Edwin Brady
src/Elaborate.hs+12
compare with master
unifiedsplit
@@ -36,6 +36,18 @@ processTactic' t = do (p, logs) <- get
36 put (p', logs ++ log)
36 put (p', logs ++ log)
37 return ()
37 return ()
38
38
39+-- Some handy gadgets for pulling out bits of state
40+
41+-- get the global context
42+get_context :: Elab Context
43+get_context = do (p, _) <- get
44+ return (context p)
45+
46+-- get the local context at the currently in focus hole
47+get_env :: Elab Env
48+get_env = do (p, _) <- get
49+ lift $ envAtFocus p
50+
39-- The primitives, from ProofState
51-- The primitives, from ProofState
40
52
41attack :: Elab ()
53attack :: Elab ()
src/ProofState.hs+10−4
@@ -4,7 +4,7 @@
4 proofs, and some high level commands for introducing new theorems,
4 proofs, and some high level commands for introducing new theorems,
5 evaluation/checking inside the proof system, etc. --}
5 evaluation/checking inside the proof system, etc. --}
6
6
7−module ProofState(ProofState(..), newProof,
7+module ProofState(ProofState(..), newProof, envAtFocus,
8 Tactic(..), processTactic) where
8 Tactic(..), processTactic) where
9
9
10import Typecheck
10import Typecheck
@@ -58,7 +58,7 @@ data TacticAction = AddGoal Name -- add a new goal, solve immediately
58instance Show ProofState where
58instance Show ProofState where
59 show (PS nm [] _ tm _ _ _) = show nm ++ ": no more goals"
59 show (PS nm [] _ tm _ _ _) = show nm ++ ": no more goals"
60 show (PS nm (h:hs) _ tm _ ctxt _)
60 show (PS nm (h:hs) _ tm _ ctxt _)
61− = let OK g = goal (Just h) tm ctxt
61+ = let OK g = goal (Just h) tm
62 wkenv = premises g in
62 wkenv = premises g in
63 showPs wkenv (reverse wkenv) ++ "\n" ++
63 showPs wkenv (reverse wkenv) ++ "\n" ++
64 "-------------------------------- (" ++ show nm ++
64 "-------------------------------- (" ++ show nm ++
@@ -105,8 +105,14 @@ type TState = (Int, [TacticAction])
105type RunTactic = Context -> Env -> Term -> StateT TState TC Term
105type RunTactic = Context -> Env -> Term -> StateT TState TC Term
106type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
106type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
107
107
108+envAtFocus :: ProofState -> TC Env
109+envAtFocus ps
110+ | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
111+ return (premises g)
112+ | otherwise = fail "No holes"
113+
108−goal :: Hole -> Term -> Context -> TC Goal
114+goal :: Hole -> Term -> TC Goal
109−goal h tm ctxt = g [] tm where
115+goal h tm = g [] tm where
110 g env (Bind n b sc) | hole b && same h n = return $ GD env b
116 g env (Bind n b sc) | hole b && same h n = return $ GD env b
111 | otherwise
117 | otherwise
112 = gb env b `mplus` g ((n, b):env) sc
118 = gb env b `mplus` g ((n, b):env) sc