git.iko.soy/Idris-dev
on bb6bba2 help sign in
Idris-dev/src/ProofState.hs
182 lines 6.5 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 | Intro Name
37 | ProofState
38 | QED
40data TacticAction = AddGoal Name
41 | Solved Name
42 | Log String
44-- Some utilites on proof and tactic states
46instance Show ProofState where
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" ++
52 "-------------------------------- (" ++ show nm ++
53 ") -------\n" ++
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)
62same Nothing n = True
63same (Just x) n = x == n
65hole (Hole _) = True
66hole (Guess _ _) = True
67hole _ = False
69holeName i = MN i "hole"
71getName :: Monad m => String -> StateT TState m Name
72getName tag = do (n, ts) <- get
73 put (n+1, ts)
74 return $ MN n tag
76action :: Monad m => TacticAction -> StateT TState m ()
77action a = do (n, ts) <- get
78 put (n, a:ts)
80newProof :: Name -> Context -> Type -> ProofState
81newProof n ctxt ty = let h = holeName 0 in
82 PS n [h] 1 (Bind h (Hole ty) (V 0)) ty ctxt False
84type TState = (Int, [TacticAction])
85type RunTactic = Context -> Env -> Term -> StateT TState TC Term
86type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
88goal :: Hole -> Term -> Context -> TC Goal
89goal h tm ctxt = g [] tm where
90 g env (Bind n b sc) | hole b && same h n = return $ GD env b
91 | otherwise = gb env b `mplus` g ((n,b):env) sc
92 g env (App f t a) = g env f `mplus` g env t `mplus` g env a
93 g env t = Error "Can't find hole"
95 gb env (Let t v) = g env t `mplus` g env v
96 gb env (Guess t v) = g env t `mplus` g env v
97 gb env t = g env (binderTy t)
99tactic :: Hole -> ProofState -> Context -> RunTactic -> StateT TState TC ProofState
100tactic h ps ctxt f = do let tm = pterm ps
101 tm' <- atH [] tm
102 return (ps { pterm = tm' })
103 where
104 atH env binder@(Bind n b sc)
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
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
112 atHb env t = do ty' <- atH env (binderTy t)
113 return $ t { binderTy = ty' }
115attack :: RunTactic
116attack 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)
122attack ctxt env _ = fail "Not an attackable hole"
124claim :: Name -> Raw -> RunTactic
125claim = undefined
127regret :: RunTactic
128regret = undefined
130fill :: Raw -> RunTactic -- Try
131fill 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
135fill _ _ _ _ = fail "Can't fill here."
137solve :: RunTactic
138solve 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."
142solve _ _ _ = fail "Not a guess."
144intro :: Name -> RunTactic
145intro 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"
150intro ctxt env _ _ = fail "Can't introduce here."
152processTactic :: Tactic -> ProofState -> TC (ProofState, String)
153processTactic QED ps = case holes ps of
154 [] -> return (ps { done = True }, "Proof complete.")
155 _ -> Error "Still holes to fill."
156processTactic ProofState ps = return (ps, show (pterm ps))
157processTactic t ps = case holes ps of
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)
164 where logs [] = ""
165 logs (Log x : xs) = x ++ "\n" ++ logs xs
166 logs (_ : xs) = logs xs
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
174process :: Tactic -> Name -> ProofState -> StateT TState TC ProofState
175process 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