546e9f5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

A gadget or two

commit546e9f5b1429df0ffc11e3df77511d34c0eb4c80 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 27 Sep 2011, 19:18 (15 years ago) parent5ee3376

2 files changed+22−4

compare with master

unifiedsplit

src/Elaborate.hs+12 src/ProofState.hs+10−4

src/Elaborate.hs+12

@@ -36,6 +36,18 @@ processTactic' t = do (p, logs) <- get

3636 put (p', logs ++ log)

3737 return ()

3838

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+

3951-- The primitives, from ProofState

4052

4153attack :: Elab ()

src/ProofState.hs+10−4

@@ -4,7 +4,7 @@

44 proofs, and some high level commands for introducing new theorems,

55 evaluation/checking inside the proof system, etc. --}

7−module ProofState(ProofState(..), newProof,

7+module ProofState(ProofState(..), newProof, envAtFocus,

88 Tactic(..), processTactic) where

1010import Typecheck

@@ -58,7 +58,7 @@ data TacticAction = AddGoal Name -- add a new goal, solve immediately

5858instance Show ProofState where

5959 show (PS nm [] _ tm _ _ _) = show nm ++ ": no more goals"

6060 show (PS nm (h:hs) _ tm _ ctxt _)

61− = let OK g = goal (Just h) tm ctxt

61+ = let OK g = goal (Just h) tm

6262 wkenv = premises g in

6363 showPs wkenv (reverse wkenv) ++ "\n" ++

6464 "-------------------------------- (" ++ show nm ++

@@ -105,8 +105,14 @@ type TState = (Int, [TacticAction])

105105type RunTactic = Context -> Env -> Term -> StateT TState TC Term

106106type Hole = Maybe Name -- Nothing = default hole, first in list in proof state

107107

108−goal :: Hole -> Term -> Context -> TC Goal

109−goal h tm ctxt = g [] tm where

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+

114+goal :: Hole -> Term -> TC Goal

115+goal h tm = g [] tm where

110116 g env (Bind n b sc) | hole b && same h n = return $ GD env b

111117 | otherwise

112118 = gb env b `mplus` g ((n, b):env) sc