git.iko.soy/Idris-dev
on 4c68b68 help sign in
Idris-dev/src/ProofState.hs
199 lines 7.1 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
3module ProofState where
5import Typecheck
6import Evaluate
7import Core
9import Control.Monad.State
10import Control.Applicative
11import Data.List
13data ProofState = PS { thname :: Name,
14 holes :: [Name], -- holes still to be solved
15 nextname :: Int, -- name supply
16 pterm :: Term, -- current proof term
17 ptype :: Type, -- original goal
18 context :: Context,
19 done :: Bool
20 }
22data Goal = GD { premises :: Env,
23 goalType :: Binder Term
24 }
26data Command = Theorem Name Raw
27 | Eval Raw
28 | Quit
29 | Tac Tactic
31data Tactic = Attack
32 | Claim Name Raw
33 | Fill Raw
34 | Regret
35 | Solve
36 | EvalIn Raw
37 | CheckIn Raw
38 | Intro Name
39 | ProofState
40 | QED
41-- Next: add 'EvalHere' and 'CheckHere' tactics
43data TacticAction = AddGoal Name
44 | Solved Name
45 | Log String
47-- Some utilites on proof and tactic states
49instance Show ProofState where
50 show (PS nm [] _ tm _ _ _) = show nm ++ ": no more goals"
51 show (PS nm (h:hs) _ tm _ ctxt _)
52 = let OK g = goal (Just h) tm ctxt
53 wkenv = weakenEnv (premises g) in
54 showPs wkenv (reverse wkenv) ++ "\n" ++
55 "-------------------------------- (" ++ show nm ++
56 ") -------\n" ++
57 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
58 where showPs env [] = ""
59 showPs env ((n, b):bs)
60 = " " ++ show n ++ " : " ++ showEnv env (binderTy b) ++
61 "\n" ++ showPs env bs
62 showG ps (Guess t v) = showEnv ps t ++ " =?= " ++ showEnv ps v
63 showG ps b = showEnv ps (binderTy b)
65same Nothing n = True
66same (Just x) n = x == n
68hole (Hole _) = True
69hole (Guess _ _) = True
70hole _ = False
72holeName i = MN i "hole"
74getName :: Monad m => String -> StateT TState m Name
75getName tag = do (n, ts) <- get
76 put (n+1, ts)
77 return $ MN n tag
79action :: Monad m => TacticAction -> StateT TState m ()
80action a = do (n, ts) <- get
81 put (n, a:ts)
83newProof :: Name -> Context -> Type -> ProofState
84newProof n ctxt ty = let h = holeName 0 in
85 PS n [h] 1 (Bind h (Hole ty) (V 0)) ty ctxt False
87type TState = (Int, [TacticAction])
88type RunTactic = Context -> Env -> Term -> StateT TState TC Term
89type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
91goal :: Hole -> Term -> Context -> TC Goal
92goal h tm ctxt = g [] tm where
93 g env (Bind n b sc) | hole b && same h n = return $ GD env b
94 | otherwise = gb env b `mplus` g ((n,b):env) sc
95 g env (App f a) = g env f `mplus` g env a
96 g env t = Error "Can't find hole"
98 gb env (Let t v) = g env t `mplus` g env v
99 gb env (Guess t v) = g env t `mplus` g env v
100 gb env t = g env (binderTy t)
102tactic :: Hole -> ProofState -> Context -> RunTactic -> StateT TState TC ProofState
103tactic h ps ctxt f = do let tm = pterm ps
104 tm' <- atH [] tm
105 return (ps { pterm = tm' })
106 where
107 atH env binder@(Bind n b sc)
108 | hole b && same h n = f ctxt (weakenEnv env) binder
109 | otherwise = pure Bind <*> pure n <*> atHb env b <*> atH ((n,b):env) sc
110 atH env (App f a) = pure App <*> atH env f <*> atH env a
111 atH env t = return t
113 atHb env (Let t v) = pure Let <*> atH env t <*> atH env v
114 atHb env (Guess t v) = pure Guess <*> atH env t <*> atH env v
115 atHb env t = do ty' <- atH env (binderTy t)
116 return $ t { binderTy = ty' }
118attack :: RunTactic
119attack ctxt env (Bind x (Hole t) sc)
120 = do h <- getName "hole"
121 action (AddGoal h)
122 return $ Bind x (Guess t (newtm h)) sc
123 where
124 newtm h = Bind h (Hole t) (V 0)
125attack ctxt env _ = fail "Not an attackable hole"
127claim :: Name -> Raw -> RunTactic
128claim = undefined
130regret :: RunTactic
131regret = undefined
133fill :: Raw -> RunTactic -- Try
134fill guess ctxt env (Bind x (Hole ty) sc) =
135 do (val, valty) <- lift $ check ctxt env guess
136 lift $ converts ctxt env valty ty
137 return $ Bind x (Guess ty val) sc
138fill _ _ _ _ = fail "Can't fill here."
140solve :: RunTactic
141solve ctxt env (Bind x (Guess ty val) sc)
142 | pureTerm val = do action (Solved x)
143 return $ Bind x (Let ty val) sc
144 | otherwise = fail "I see a hole in your solution."
145solve _ _ _ = fail "Not a guess."
147intro :: Name -> RunTactic
148intro n ctxt env (Bind x (Hole t) (V 0)) =
149 do let t' = normalise ctxt env t
150 case t' of
151 Bind y (Pi s) t -> return $ Bind n (Lam s) (Bind x (Hole t) (V 0))
152 _ -> fail "Nothing to introduce"
153intro ctxt env _ _ = fail "Can't introduce here."
155check_in :: Raw -> RunTactic
156check_in t ctxt env tm =
157 do (val, valty) <- lift $ check ctxt env t
158 action (Log (showEnv env val ++ " : " ++ showEnv env valty))
159 return tm
161eval_in :: Raw -> RunTactic
162eval_in t ctxt env tm =
163 do (val, valty) <- lift $ check ctxt env t
164 action (Log (showEnv env (normalise ctxt env val) ++ " : " ++ showEnv env valty))
165 return tm
168processTactic :: Tactic -> ProofState -> TC (ProofState, String)
169processTactic QED ps = case holes ps of
170 [] -> return (ps { done = True }, "Proof complete.")
171 _ -> Error "Still holes to fill."
172processTactic ProofState ps = return (ps, show (pterm ps))
173processTactic t ps = case holes ps of
174 [] -> Error "Nothing to fill in."
175 (h:_) -> do let n = nextname ps
176 (ps',(n', actions)) <- runStateT (process t h ps) (n, [])
177 return (ps' { nextname = n',
178 holes = goals (holes ps') actions },
179 logs actions)
180 where logs [] = ""
181 logs (Log x : xs) = x ++ "\n" ++ logs xs
182 logs (_ : xs) = logs xs
184 goals g [] = g
185 goals g (AddGoal n : xs) = goals (n : g) xs
186 goals g (Solved n : xs) = goals (g \\ [n]) xs
187 goals g (_ : xs) = goals g xs
190process :: Tactic -> Name -> ProofState -> StateT TState TC ProofState
191process t h ps = tactic (Just h) ps (context ps) (mktac t)
192 where mktac Attack = attack
193 mktac (Claim n r) = claim n r
194 mktac (Fill r) = fill r
195 mktac Regret = regret
196 mktac Solve = solve
197 mktac (Intro n) = intro n
198 mktac (CheckIn r) = check_in r
199 mktac (EvalIn r) = eval_in r