git.iko.soy/Idris-dev
on master help sign in
Tactics can now complete basic proofs
bb6bba2Edwin Brady
src/Core.hs+71−21
compare with master
unifiedsplit
@@ -87,28 +87,74 @@ type Type = Term
87
87
88type Env = EnvTT Name
88type Env = EnvTT Name
89
89
90+-- an environment with de Bruijn indices 'normalised' so that they all refer to
91+-- this environment
92+
93+newtype WkEnvTT n = Wk (EnvTT n)
94+type WkEnv = WkEnvTT Name
95+
90instance Show n => Show (TT n) where
96instance Show n => Show (TT n) where
97+ show t = showEnv [] t
98+
99+showEnv env t = showEnv' env t False
100+showEnvDbg env t = showEnv' env t True
101+
91− show t = se 10 [] t where
102+showEnv' env t dbg = se 10 env t where
92− se p env (P _ n _) = show n
103+ se p env (P _ n _) = show n
93− se p env (V i) | i < length env = show $ fst $ env!!i
104+ se p env (V i) | i < length env = (show $ fst $ env!!i) ++
105+ if dbg then "{" ++ show i ++ "}" else ""
94− | otherwise = "!!V " ++ show i ++ "!!"
106+ | otherwise = "!!V " ++ show i ++ "!!"
95− se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc
107+ se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc
96− se p env (App f t a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a
108+ se p env (App f t a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a
97− se p env (Set i) = "Set" ++ show i
109+ se p env (Set i) = "Set" ++ show i
98−
110+
99− sb env n (Lam t) = showb env "\\ " " => " n t
111+ sb env n (Lam t) = showb env "\\ " " => " n t
100− sb env n (Hole t) = showb env "? " ". " n t
112+ sb env n (Hole t) = showb env "? " ". " n t
101− sb env n (Pi t) = showb env "forall " " -> " n t
113+ sb env n (Pi t) = showb env "forall " " -> " n t
102− sb env n (PVar t) = showb env "! " ". " n t
114+ sb env n (PVar t) = showb env "! " ". " n t
103− sb env n (Let t v) = showbv env "let " " in " n t v
115+ sb env n (Let t v) = showbv env "let " " in " n t v
104− sb env n (Guess t v) = showbv env "?? " " in " n t v
116+ sb env n (Guess t v) = showbv env "?? " " in " n t v
105−
117+
106− showb env op sc n t = op ++ show n ++ " : " ++ se 10 env t ++ sc
118+ showb env op sc n t = op ++ show n ++ " : " ++ se 10 env t ++ sc
107− showbv env op sc n t v = op ++ show n ++ " : " ++ se 10 env t ++ " = " ++
119+ showbv env op sc n t v = op ++ show n ++ " : " ++ se 10 env t ++ " = " ++
108− se 10 env v ++ sc
120+ se 10 env v ++ sc
109−
121+
110− bracket outer inner str | inner > outer = "(" ++ str ++ ")"
122+ bracket outer inner str | inner > outer = "(" ++ str ++ ")"
111− | otherwise = str
123+ | otherwise = str
124+
125+-- Check whether a term has any holes in it - impure if so
126+
127+pureTerm :: TT n -> Bool
128+pureTerm (App f t a) = pureTerm f && pureTerm t && pureTerm a
129+pureTerm (Bind n b sc) = pureBinder b && pureTerm sc where
130+ pureBinder (Hole _) = False
131+ pureBinder (Guess _ _) = False
132+ pureBinder (Let t v) = pureTerm t && pureTerm v
133+ pureBinder t = pureTerm (binderTy t)
134+pureTerm _ = True
135+
136+-- weaken a term by adding i to each de Bruijn index (i.e. lift it over i bindings)
137+
138+weakenTm :: Int -> TT n -> TT n
139+weakenTm i t = wk i 0 t
140+ where wk i min (V x) | x >= min = V (i + x)
141+ wk i m (App f t a) = App (wk i m f) (wk i m t) (wk i m a)
142+ wk i m (Bind x b sc) = Bind x (wkb i m b) (wk i (m + 1) sc)
143+ wk i m t = t
144+ wkb i m (Let t v) = Let (wk i m t) (wk i m v)
145+ wkb i m (Guess t v) = Guess (wk i m t) (wk i m v)
146+ wkb i m t = t { binderTy = wk i m (binderTy t) }
147+
148+-- weaken an environment so that all the de Bruijn indices are correct according
149+-- to the latest bound variable
150+
151+weakenEnv :: Show n => EnvTT n -> EnvTT n
152+weakenEnv env = wk (length env - 1) env
153+ where wk i [] = []
154+ wk i ((n, b) : bs) = (n, weakenTmB i b) : wk (i - 1) bs
155+ weakenTmB i (Let t v) = Let (weakenTm i t) (weakenTm i v)
156+ weakenTmB i (Guess t v) = Guess (weakenTm i t) (weakenTm i v)
157+ weakenTmB i t = t { binderTy = weakenTm i (binderTy t) }
112
158
113-- WELL TYPED TERMS AS HOAS -------------------------------------------------
159-- WELL TYPED TERMS AS HOAS -------------------------------------------------
114
160
@@ -149,6 +195,10 @@ type Context = [(Name, Def)]
149
195
150emptyContext = []
196emptyContext = []
151
197
198+addToCtxt :: Name -> Term -> Type -> Context -> Context
199+addToCtxt n tm ty ctxt = (n, Function (Fun ty (hoas [] ty)
200+ tm (hoas [] tm))) : ctxt
201+
152lookupTy :: Name -> Context -> Maybe Type
202lookupTy :: Name -> Context -> Maybe Type
153lookupTy n ctxt = do def <- lookup n ctxt
203lookupTy n ctxt = do def <- lookup n ctxt
154 case def of
204 case def of
src/ProofShell.hs+16−3
@@ -24,10 +24,23 @@ processCommand (Theorem n ty) state
24 OK (gl, Set _) -> (state { prf = Just (newProof n (ctxt state) gl) }, "")
24 OK (gl, Set _) -> (state { prf = Just (newProof n (ctxt state) gl) }, "")
25 OK _ -> (state, "Goal is not a type")
25 OK _ -> (state, "Goal is not a type")
26 err -> (state, show err)
26 err -> (state, show err)
27−processCommand Quit state = (state { exitNow = True }, "Bye bye")
27+processCommand Quit state = (state { exitNow = True }, "Bye bye")
28−processCommand (Tac t) state
28+processCommand (Eval t) state =
29+ case check (ctxt state) [] t of
30+ OK (val, _) ->
31+ let nf = normalise (ctxt state) [] val in
32+ (state, show nf)
33+ err -> (state, show err)
34+processCommand (Tac t) state
29 | Just ps <- prf state = case processTactic t ps of
35 | Just ps <- prf state = case processTactic t ps of
36+ OK (ps', resp) ->
37+ if (not (done ps'))
30− OK (ps', resp) -> (state { prf = Just ps' }, resp)
38+ then (state { prf = Just ps' }, resp)
39+ else (state { prf = Nothing,
40+ ctxt = addToCtxt (thname ps')
41+ (pterm ps')
42+ (ptype ps')
43+ (context ps') }, resp)
31 err -> (state, show err)
44 err -> (state, show err)
32 | otherwise = (state, "No proof in progress")
45 | otherwise = (state, "No proof in progress")
33
46
src/ProofState.hs+102−50
@@ -5,14 +5,18 @@ module ProofState where
5import Typecheck
5import Typecheck
6import Evaluate
6import Evaluate
7import Core
7import Core
8+
8import Control.Monad.State
9import Control.Monad.State
10+import Control.Applicative
11+import Data.List
9
12
10data ProofState = PS { thname :: Name,
13data ProofState = PS { thname :: Name,
11 holes :: [Name], -- holes still to be solved
14 holes :: [Name], -- holes still to be solved
12 nextname :: Int, -- name supply
15 nextname :: Int, -- name supply
13 pterm :: Term, -- current proof term
16 pterm :: Term, -- current proof term
17+ ptype :: Type, -- original goal
14 context :: Context,
18 context :: Context,
15− complete :: Bool
19+ done :: Bool
16 }
20 }
17
21
18data Goal = GD { premises :: Env,
22data Goal = GD { premises :: Env,
@@ -26,35 +30,59 @@ data Command = Theorem Name Raw
26
30
27data Tactic = Attack
31data Tactic = Attack
28 | Claim Name Raw
32 | Claim Name Raw
29− | Try Raw
33+ | Fill Raw
30 | Regret
34 | Regret
31 | Solve
35 | Solve
36+ | Intro Name
37+ | ProofState
32 | QED
38 | QED
33
39
40+data TacticAction = AddGoal Name
41+ | Solved Name
42+ | Log String
43+
44+-- Some utilites on proof and tactic states
45+
34instance Show ProofState where
46instance Show ProofState where
35− show (PS nm [] _ tm _ _) = show nm ++ ": no more goals"
47+ show (PS nm [] _ tm _ _ _) = show nm ++ ": no more goals"
36− show (PS nm (h:hs) _ tm ctxt _)
48+ show (PS nm (h:hs) _ tm _ ctxt _)
37− = let OK g = goal (Just h) tm ctxt in
49+ = let OK g = goal (Just h) tm ctxt
38− showEnv (premises g) ++ "\n" ++
50+ wkenv = weakenEnv (premises g) in
51+ showPs wkenv (reverse wkenv) ++ "\n" ++
39 "-------------------------------- (" ++ show nm ++
52 "-------------------------------- (" ++ show nm ++
40 ") -------\n" ++
53 ") -------\n" ++
41− show h ++ " : " ++ showG (goalType g) ++ "\n"
54+ show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
42− where showEnv [] = ""
55+ where showPs env [] = ""
56+ showPs env ((n, b):bs)
43− showEnv ((n, b):bs) = " " ++ show n ++ " : " ++ show (binderTy b) ++ "\n" ++
57+ = " " ++ show n ++ " : " ++ showEnv env (binderTy b) ++
44− showEnv bs
58+ "\n" ++ showPs env bs
45− showG (Guess t v) = show t ++ " =?= " ++ show v
59+ showG ps (Guess t v) = showEnv ps t ++ " =?= " ++ showEnv ps v
46− showG b = show (binderTy b)
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
47
68
48holeName i = MN i "hole"
69holeName i = MN i "hole"
49
70
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+
50newProof :: Name -> Context -> Type -> ProofState
80newProof :: Name -> Context -> Type -> ProofState
51newProof n ctxt ty = let h = holeName 0 in
81newProof n ctxt ty = let h = holeName 0 in
52− PS n [h] 1 (Bind h (Hole ty) (V 0)) ctxt False
82+ PS n [h] 1 (Bind h (Hole ty) (V 0)) ty ctxt False
53−
54−data TacticAction = AddGoal Name
55− | Log String
56
83
84+type TState = (Int, [TacticAction])
57−type RunTactic = Context -> Env -> Term -> StateT [TacticAction] TC Term
85+type RunTactic = Context -> Env -> Term -> StateT TState TC Term
58type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
86type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
59
87
60goal :: Hole -> Term -> Context -> TC Goal
88goal :: Hole -> Term -> Context -> TC Goal
@@ -68,34 +96,30 @@ goal h tm ctxt = g [] tm where
68 gb env (Guess t v) = g env t `mplus` g env v
96 gb env (Guess t v) = g env t `mplus` g env v
69 gb env t = g env (binderTy t)
97 gb env t = g env (binderTy t)
70
98
71−tactic :: Hole -> Term -> Context -> RunTactic -> StateT [TacticAction] TC Term
99+tactic :: Hole -> ProofState -> Context -> RunTactic -> StateT TState TC ProofState
72−tactic h tm ctxt f = atH [] tm where
100+tactic h ps ctxt f = do let tm = pterm ps
101+ tm' <- atH [] tm
102+ return (ps { pterm = tm' })
103+ where
73 atH env binder@(Bind n b sc)
104 atH env binder@(Bind n b sc)
74− | hole b && same h n = f ctxt env binder
105+ | hole b && same h n = f ctxt (weakenEnv env) binder
75− | otherwise = do b' <- atHb env b
106+ | otherwise = pure Bind <*> pure n <*> atHb env b <*> atH ((n,b):env) sc
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
107+ atH env (App f t a) = pure App <*> atH env f <*> atH env t <*> atH env a
79− return (App f' t' a')
80− atH env t = do return t
108+ atH env t = return t
81
109
82− atHb env (Let t v) = do t' <- atH env t
110+ atHb env (Let t v) = pure Let <*> atH env t <*> atH env v
83− v' <- atH env v
84− return $ Let t' v'
85− atHb env (Guess t v) = do t' <- atH env t
111+ atHb env (Guess t v) = pure Guess <*> atH env t <*> atH env v
86− v' <- atH env v
87− return $ Let t' v'
88 atHb env t = do ty' <- atH env (binderTy t)
112 atHb env t = do ty' <- atH env (binderTy t)
89 return $ t { binderTy = ty' }
113 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
96
114
97attack :: RunTactic
115attack :: 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"
99
123
100claim :: Name -> Raw -> RunTactic
124claim :: Name -> Raw -> RunTactic
101claim = undefined
125claim = undefined
@@ -104,27 +128,55 @@ regret :: RunTactic
104regret = undefined
128regret = undefined
105
129
106fill :: Raw -> RunTactic -- Try
130fill :: 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."
108
136
109solve :: RunTactic
137solve :: 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."
111
151
112processTactic :: Tactic -> ProofState -> TC (ProofState, String)
152processTactic :: Tactic -> ProofState -> TC (ProofState, String)
113processTactic QED ps = case holes ps of
153processTactic QED ps = case holes ps of
114− [] -> return (ps { complete = True }, "QED")
154+ [] -> return (ps { done = True }, "Proof complete.")
115− _ -> Error "Still holes to fill"
155+ _ -> Error "Still holes to fill."
156+processTactic ProofState ps = return (ps, show (pterm ps))
116processTactic t ps = case holes ps of
157processTactic t ps = case holes ps of
117− [] -> Error "Nothing to fill in"
158+ [] -> Error "Nothing to fill in."
159+ (h:_) -> do let n = nextname ps
118− (h:_) -> do (ps', actions) <- runStateT (process t h ps) []
160+ (ps',(n', actions)) <- runStateT (process t h ps) (n, [])
161+ return (ps' { nextname = n',
162+ holes = goals (holes ps') actions },
119− return (ps', logs actions)
163+ logs actions)
120 where logs [] = ""
164 where logs [] = ""
121 logs (Log x : xs) = x ++ "\n" ++ logs xs
165 logs (Log x : xs) = x ++ "\n" ++ logs xs
122 logs (_ : xs) = logs xs
166 logs (_ : xs) = logs xs
123
167
124−process :: Tactic -> Name -> ProofState -> StateT [TacticAction] TC ProofState
168+ goals g [] = g
125−process (Try x) h ps = undefined
169+ goals g (AddGoal n : xs) = goals (n : g) xs
126−
170+ goals g (Solved n : xs) = goals (g \\ [n]) xs
171+ goals g (_ : xs) = goals g xs
127
172
128−
129
173
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
130
182
src/ShellParser.hs+10−5
@@ -35,8 +35,8 @@ parseCommand = parse pCommand "(input)"
35parseTactic = parse (pTactic >>= return . Tac) "(input)"
35parseTactic = parse (pTactic >>= return . Tac) "(input)"
36
36
37pCommand :: Parser Command
37pCommand :: Parser Command
38−pCommand = do reserved "theorem"; n <- identifier; lchar ':'; ty <- pTerm
38+pCommand = do reserved "theorem"; n <- iname; lchar ':'; ty <- pTerm
39− return (Theorem (UN [n]) ty)
39+ return (Theorem n ty)
40 <|> do reserved "eval"; tm <- pTerm
40 <|> do reserved "eval"; tm <- pTerm
41 return (Eval tm)
41 return (Eval tm)
42 <|> do reserved "quit";
42 <|> do reserved "quit";
@@ -44,9 +44,14 @@ pCommand = do reserved "theorem"; n <- identifier; lchar ':'; ty <- pTerm
44
44
45pTactic :: Parser Tactic
45pTactic :: Parser Tactic
46pTactic = do reserved "attack"; return Attack
46pTactic = do reserved "attack"; return Attack
47− <|> do reserved "claim"; n <- identifier; lchar ':'; ty <- pTerm
47+ <|> do reserved "claim"; n <- iname; lchar ':'; ty <- pTerm
48− return (Claim (UN [n]) ty)
48+ return (Claim n ty)
49− <|> do reserved "try"; tm <- pTerm; return (Try tm)
49+ <|> do reserved "fill"; tm <- pTerm; return (Fill tm)
50 <|> do reserved "regret"; return Regret
50 <|> do reserved "regret"; return Regret
51 <|> do reserved "solve"; return Solve
51 <|> do reserved "solve"; return Solve
52+ <|> do reserved "intro"; n <- iname; return (Intro n)
53+ <|> do reserved "state"; return ProofState
52 <|> do reserved "qed"; return QED
54 <|> do reserved "qed"; return QED
55+
56+iname :: Parser Name
57+iname = identifier >>= (\n -> return (UN [n]))
src/Typecheck.hs+2−1
@@ -1,4 +1,4 @@
1−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
1+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor #-}
2
2
3module Typecheck where
3module Typecheck where
4
4
@@ -10,6 +10,7 @@ import Evaluate
10
10
11data TC a = OK a
11data TC a = OK a
12 | Error String -- TMP! Make this an informative data structure
12 | Error String -- TMP! Make this an informative data structure
13+ deriving (Eq, Functor)
13
14
14instance Show a => Show (TC a) where
15instance Show a => Show (TC a) where
15 show (OK x) = show x
16 show (OK x) = show x