git.iko.soy/Idris-dev
on master help sign in
Builds on ubuntu haskell platform
aa85339Edwin Brady
src/Core/ProofShell.hs+4−3
compare with master
unifiedsplit
@@ -1,4 +1,4 @@
1−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
1+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}
2
2
3module Core.ProofShell where
3module Core.ProofShell where
4
4
@@ -11,13 +11,14 @@ import Core.Elaborate
11import Control.Monad.State
11import Control.Monad.State
12import System.Console.Readline
12import System.Console.Readline
13
13
14+data ShellState = ShellState
14−data ShellState = State { ctxt :: Context,
15+ { ctxt :: Context,
15 prf :: Maybe ProofState,
16 prf :: Maybe ProofState,
16 deferred :: [(Name, ProofState)],
17 deferred :: [(Name, ProofState)],
17 exitNow :: Bool
18 exitNow :: Bool
18 }
19 }
19
20
20−initState c = State c Nothing [] False
21+initState c = ShellState c Nothing [] False
21
22
22processCommand :: Command -> ShellState -> (ShellState, String)
23processCommand :: Command -> ShellState -> (ShellState, String)
23processCommand (Theorem n ty) state
24processCommand (Theorem n ty) state
src/Core/ProofState.hs+5−5
@@ -1,4 +1,4 @@
1−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
1+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}
2
2
3{- Implements a proof state, some primitive tactics for manipulating
3{- Implements a proof state, some primitive tactics for manipulating
4 proofs, and some high level commands for introducing new theorems,
4 proofs, and some high level commands for introducing new theorems,
@@ -144,12 +144,12 @@ tactic h f = do ps <- get
144 atH c env binder@(Bind n b sc)
144 atH c env binder@(Bind n b sc)
145 | hole b && same h n = f c env binder
145 | hole b && same h n = f c env binder
146 | otherwise
146 | otherwise
147− = pure Bind <*> pure n <*> atHb c env b <*> atH c ((n,b) : env) sc
147+ = liftM2 (Bind n) (atHb c env b) (atH c ((n, b) : env) sc)
148− atH c env (App f a) = pure App <*> atH c env f <*> atH c env a
148+ atH c env (App f a) = liftM2 App (atH c env f) (atH c env a)
149 atH c env t = return t
149 atH c env t = return t
150
150
151− atHb c env (Let t v) = pure Let <*> atH c env t <*> atH c env v
151+ atHb c env (Let t v) = liftM2 Let (atH c env t) (atH c env v)
152− atHb c env (Guess t v) = pure Guess <*> atH c env t <*> atH c env v
152+ atHb c env (Guess t v) = liftM2 Guess (atH c env t) (atH c env v)
153 atHb c env t = do ty' <- atH c env (binderTy t)
153 atHb c env t = do ty' <- atH c env (binderTy t)
154 return $ t { binderTy = ty' }
154 return $ t { binderTy = ty' }
155
155