@@ -5,14 +5,18 @@ module ProofState where
55import Typecheck
66import Evaluate
77import Core
8+
89import Control.Monad.State
10+import Control.Applicative
11+import Data.List
912
1013data ProofState = PS { thname :: Name,
1114 holes :: [Name], -- holes still to be solved
1215 nextname :: Int, -- name supply
1316 pterm :: Term, -- current proof term
17+ ptype :: Type, -- original goal
1418 context :: Context,
15− complete :: Bool
19+ done :: Bool
1620 }
1721
1822data Goal = GD { premises :: Env,
@@ -26,35 +30,59 @@ data Command = Theorem Name Raw
2630
2731data Tactic = Attack
2832 | Claim Name Raw
29− | Try Raw
33+ | Fill Raw
3034 | Regret
3135 | Solve
36+ | Intro Name
37+ | ProofState
3238 | QED
3339
40+data TacticAction = AddGoal Name
41+ | Solved Name
42+ | Log String
43+
44+-- Some utilites on proof and tactic states
45+
3446instance 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" ++
47+ show (PS nm [] _ tm _ _ _) = show nm ++ ": no more goals"
48+ show (PS nm (h:hs) _ tm _ ctxt _)
49+ = let OK g = goal (Just h) tm ctxt
50+ wkenv = weakenEnv (premises g) in
51+ showPs wkenv (reverse wkenv) ++ "\n" ++
3952 "-------------------------------- (" ++ show nm ++
4053 ") -------\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)
54+ show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
55+ where showPs env [] = ""
56+ showPs env ((n, b):bs)
57+ = " " ++ show n ++ " : " ++ showEnv env (binderTy b) ++
58+ "\n" ++ showPs env bs
59+ showG ps (Guess t v) = showEnv ps t ++ " =?= " ++ showEnv ps v
60+ showG ps b = showEnv ps (binderTy b)
61+
62+same Nothing n = True
63+same (Just x) n = x == n
64+
65+hole (Hole _) = True
66+hole (Guess _ _) = True
67+hole _ = False
4768
4869holeName i = MN i "hole"
4970
71+getName :: Monad m => String -> StateT TState m Name
72+getName tag = do (n, ts) <- get
73+ put (n+1, ts)
74+ return $ MN n tag
75+
76+action :: Monad m => TacticAction -> StateT TState m ()
77+action a = do (n, ts) <- get
78+ put (n, a:ts)
79+
5080newProof :: Name -> Context -> Type -> ProofState
5181newProof n ctxt ty = let h = holeName 0 in
52− PS n [h] 1 (Bind h (Hole ty) (V 0)) ctxt False
53−
54−data TacticAction = AddGoal Name
55− | Log String
82+ PS n [h] 1 (Bind h (Hole ty) (V 0)) ty ctxt False
5683
57−type RunTactic = Context -> Env -> Term -> StateT [TacticAction] TC Term
84+type TState = (Int, [TacticAction])
85+type RunTactic = Context -> Env -> Term -> StateT TState TC Term
5886type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
5987
6088goal :: Hole -> Term -> Context -> TC Goal
@@ -68,34 +96,30 @@ goal h tm ctxt = g [] tm where
6896 gb env (Guess t v) = g env t `mplus` g env v
6997 gb env t = g env (binderTy t)
7098
71−tactic :: Hole -> Term -> Context -> RunTactic -> StateT [TacticAction] TC Term
72−tactic h tm ctxt f = atH [] tm where
99+tactic :: Hole -> ProofState -> Context -> RunTactic -> StateT TState TC ProofState
100+tactic h ps ctxt f = do let tm = pterm ps
101+ tm' <- atH [] tm
102+ return (ps { pterm = tm' })
103+ where
73104 atH env binder@(Bind n b sc)
74− | hole b && same h n = f ctxt env binder
75− | otherwise = do b' <- atHb env b
76− sc' <- atH ((n,b):env) sc
77− return (Bind n b' sc')
78− atH env (App f t a) = do f' <- atH env t; t' <- atH env t; a' <- atH env a
79− return (App f' t' a')
80− atH env t = do return t
105+ | hole b && same h n = f ctxt (weakenEnv env) binder
106+ | otherwise = pure Bind <*> pure n <*> atHb env b <*> atH ((n,b):env) sc
107+ atH env (App f t a) = pure App <*> atH env f <*> atH env t <*> atH env a
108+ atH env t = return t
81109
82− atHb env (Let t v) = do t' <- atH env t
83− v' <- atH env v
84− return $ Let t' v'
85− atHb env (Guess t v) = do t' <- atH env t
86− v' <- atH env v
87− return $ Let t' v'
110+ atHb env (Let t v) = pure Let <*> atH env t <*> atH env v
111+ atHb env (Guess t v) = pure Guess <*> atH env t <*> atH env v
88112 atHb env t = do ty' <- atH env (binderTy t)
89113 return $ t { binderTy = ty' }
90−
91−same Nothing n = True
92−same (Just x) n = x == n
93−
94−hole (Hole _) = True
95−hole (Guess _ _) = True
96114
97115attack :: RunTactic
98−attack = undefined
116+attack ctxt env (Bind x (Hole t) sc)
117+ = do h <- getName "hole"
118+ action (AddGoal h)
119+ return $ Bind x (Guess t (newtm h)) sc
120+ where
121+ newtm h = Bind h (Hole t) (V 0)
122+attack ctxt env _ = fail "Not an attackable hole"
99123
100124claim :: Name -> Raw -> RunTactic
101125claim = undefined
@@ -104,27 +128,55 @@ regret :: RunTactic
104128regret = undefined
105129
106130fill :: Raw -> RunTactic -- Try
107−fill = undefined
131+fill guess ctxt env (Bind x (Hole ty) sc) =
132+ do (val, valty) <- lift $ check ctxt env guess
133+ lift $ converts ctxt env valty ty
134+ return $ Bind x (Guess ty val) sc
135+fill _ _ _ _ = fail "Can't fill here."
108136
109137solve :: RunTactic
110−solve = undefined
138+solve ctxt env (Bind x (Guess ty val) sc)
139+ | pureTerm val = do action (Solved x)
140+ return $ Bind x (Let ty val) sc
141+ | otherwise = fail "I see a hole in your solution."
142+solve _ _ _ = fail "Not a guess."
143+
144+intro :: Name -> RunTactic
145+intro n ctxt env (Bind x (Hole t) (V 0)) =
146+ do let t' = normalise ctxt env t
147+ case t' of
148+ Bind y (Pi s) t -> return $ Bind n (Lam s) (Bind x (Hole t) (V 0))
149+ _ -> fail "Nothing to introduce"
150+intro ctxt env _ _ = fail "Can't introduce here."
111151
112152processTactic :: Tactic -> ProofState -> TC (ProofState, String)
113153processTactic QED ps = case holes ps of
114− [] -> return (ps { complete = True }, "QED")
115− _ -> Error "Still holes to fill"
154+ [] -> return (ps { done = True }, "Proof complete.")
155+ _ -> Error "Still holes to fill."
156+processTactic ProofState ps = return (ps, show (pterm ps))
116157processTactic 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)
158+ [] -> Error "Nothing to fill in."
159+ (h:_) -> do let n = nextname ps
160+ (ps',(n', actions)) <- runStateT (process t h ps) (n, [])
161+ return (ps' { nextname = n',
162+ holes = goals (holes ps') actions },
163+ logs actions)
120164 where logs [] = ""
121165 logs (Log x : xs) = x ++ "\n" ++ logs xs
122166 logs (_ : xs) = logs xs
123167
124−process :: Tactic -> Name -> ProofState -> StateT [TacticAction] TC ProofState
125−process (Try x) h ps = undefined
126−
168+ goals g [] = g
169+ goals g (AddGoal n : xs) = goals (n : g) xs
170+ goals g (Solved n : xs) = goals (g \\ [n]) xs
171+ goals g (_ : xs) = goals g xs
127172
128−
129173
174+process :: Tactic -> Name -> ProofState -> StateT TState TC ProofState
175+process t h ps = tactic (Just h) ps (context ps) (mktac t)
176+ where mktac Attack = attack
177+ mktac (Claim n r) = claim n r
178+ mktac (Fill r) = fill r
179+ mktac Regret = regret
180+ mktac Solve = solve
181+ mktac (Intro n) = intro n
130182