@@ -7,23 +7,59 @@ import Evaluate
77import Core
88import Control.Monad.State
99
10−data ProofState = PS { holes :: [Name], -- holes still to be solved
11− nextname :: Int, -- name supply
12− pterm :: Term -- current proof term
10+data ProofState = PS { thname :: Name,
11+ holes :: [Name], -- holes still to be solved
12+ nextname :: Int, -- name supply
13+ pterm :: Term, -- current proof term
14+ context :: Context,
15+ complete :: Bool
1316 }
1417
1518data Goal = GD { premises :: Env,
16− goalType :: Term
19+ goalType :: Binder Term
1720 }
1821
22+data Command = Theorem Name Raw
23+ | Eval Raw
24+ | Quit
25+ | Tac Tactic
26+
27+data Tactic = Attack
28+ | Claim Name Raw
29+ | Try Raw
30+ | Regret
31+ | Solve
32+ | QED
33+
34+instance Show ProofState where
35+ show (PS nm [] _ tm _ _) = show nm ++ ": no more goals"
36+ show (PS nm (h:hs) _ tm ctxt _)
37+ = let OK g = goal (Just h) tm ctxt in
38+ showEnv (premises g) ++ "\n" ++
39+ "-------------------------------- (" ++ show nm ++
40+ ") -------\n" ++
41+ show h ++ " : " ++ showG (goalType g) ++ "\n"
42+ where showEnv [] = ""
43+ showEnv ((n, b):bs) = " " ++ show n ++ " : " ++ show (binderTy b) ++ "\n" ++
44+ showEnv bs
45+ showG (Guess t v) = show t ++ " =?= " ++ show v
46+ showG b = show (binderTy b)
47+
48+holeName i = MN i "hole"
49+
50+newProof :: Name -> Context -> Type -> ProofState
51+newProof n ctxt ty = let h = holeName 0 in
52+ PS n [h] 1 (Bind h (Hole ty) (V 0)) ctxt False
53+
1954data TacticAction = AddGoal Name
20−
21−type Tactic = Context -> Env -> Term -> StateT [TacticAction] TC Term
55+ | Log String
56+
57+type RunTactic = Context -> Env -> Term -> StateT [TacticAction] TC Term
2258type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
2359
2460goal :: Hole -> Term -> Context -> TC Goal
2561goal h tm ctxt = g [] tm where
26− g env (Bind n b sc) | hole b && same h n = return $ GD env (binderTy b)
62+ g env (Bind n b sc) | hole b && same h n = return $ GD env b
2763 | otherwise = gb env b `mplus` g ((n,b):env) sc
2864 g env (App f t a) = g env f `mplus` g env t `mplus` g env a
2965 g env t = Error "Can't find hole"
@@ -32,7 +68,7 @@ goal h tm ctxt = g [] tm where
3268 gb env (Guess t v) = g env t `mplus` g env v
3369 gb env t = g env (binderTy t)
3470
35−tactic :: Hole -> Term -> Context -> Tactic -> StateT [TacticAction] TC Term
71+tactic :: Hole -> Term -> Context -> RunTactic -> StateT [TacticAction] TC Term
3672tactic h tm ctxt f = atH [] tm where
3773 atH env binder@(Bind n b sc)
3874 | hole b && same h n = f ctxt env binder
@@ -58,4 +94,37 @@ same (Just x) n = x == n
5894hole (Hole _) = True
5995hole (Guess _ _) = True
6096
97+attack :: RunTactic
98+attack = undefined
99+
100+claim :: Name -> Raw -> RunTactic
101+claim = undefined
102+
103+regret :: RunTactic
104+regret = undefined
105+
106+fill :: Raw -> RunTactic -- Try
107+fill = undefined
108+
109+solve :: RunTactic
110+solve = undefined
111+
112+processTactic :: Tactic -> ProofState -> TC (ProofState, String)
113+processTactic QED ps = case holes ps of
114+ [] -> return (ps { complete = True }, "QED")
115+ _ -> Error "Still holes to fill"
116+processTactic t ps = case holes ps of
117+ [] -> Error "Nothing to fill in"
118+ (h:_) -> do (ps', actions) <- runStateT (process t h ps) []
119+ return (ps', logs actions)
120+ where logs [] = ""
121+ logs (Log x : xs) = x ++ "\n" ++ logs xs
122+ logs (_ : xs) = logs xs
123+
124+process :: Tactic -> Name -> ProofState -> StateT [TacticAction] TC ProofState
125+process (Try x) h ps = undefined
126+
127+
128+
129+
61130