git.iko.soy/Idris-dev
on ccd64c7 help sign in
Idris-dev/src/ProofState.hs
61 lines 2.2 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
3module ProofState where
5import Typecheck
6import Evaluate
7import Core
8import Control.Monad.State
10data ProofState = PS { holes :: [Name], -- holes still to be solved
11 nextname :: Int, -- name supply
12 pterm :: Term -- current proof term
13 }
15data Goal = GD { premises :: Env,
16 goalType :: Term
17 }
19data TacticAction = AddGoal Name
21type Tactic = Context -> Env -> Term -> StateT [TacticAction] TC Term
22type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
24goal :: Hole -> Term -> Context -> TC Goal
25goal h tm ctxt = g [] tm where
26 g env (Bind n b sc) | hole b && same h n = return $ GD env (binderTy b)
27 | otherwise = gb env b `mplus` g ((n,b):env) sc
28 g env (App f t a) = g env f `mplus` g env t `mplus` g env a
29 g env t = Error "Can't find hole"
31 gb env (Let t v) = g env t `mplus` g env v
32 gb env (Guess t v) = g env t `mplus` g env v
33 gb env t = g env (binderTy t)
35tactic :: Hole -> Term -> Context -> Tactic -> StateT [TacticAction] TC Term
36tactic h tm ctxt f = atH [] tm where
37 atH env binder@(Bind n b sc)
38 | hole b && same h n = f ctxt env binder
39 | otherwise = do b' <- atHb env b
40 sc' <- atH ((n,b):env) sc
41 return (Bind n b' sc')
42 atH env (App f t a) = do f' <- atH env t; t' <- atH env t; a' <- atH env a
43 return (App f' t' a')
44 atH env t = do return t
46 atHb env (Let t v) = do t' <- atH env t
47 v' <- atH env v
48 return $ Let t' v'
49 atHb env (Guess t v) = do t' <- atH env t
50 v' <- atH env v
51 return $ Let t' v'
52 atHb env t = do ty' <- atH env (binderTy t)
53 return $ t { binderTy = ty' }
55same Nothing n = True
56same (Just x) n = x == n
58hole (Hole _) = True
59hole (Guess _ _) = True