12f9368 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

apply and prepare_apply elaborations

12f9368Edwin Brady15 years ago

src/Core.hs+14

compare with master

unifiedsplit

@@ -79,6 +79,10 @@ data Binder b = Lam { binderTy :: b }

79 | PVar { binderTy :: b }

80 deriving (Show, Eq, Functor)

82+raw_apply :: Raw -> [Raw] -> Raw

83+raw_apply f [] = f

84+raw_apply f (a : as) = raw_apply (RApp f a) as

85+

82data RawFun = RawFun { rtype :: Raw,

86data RawFun = RawFun { rtype :: Raw,

83 rval :: Raw

87 rval :: Raw

84 }

88 }

@@ -144,6 +148,16 @@ unApply t = ua [] t where

144 ua args (App f a) = ua (a:args) f

148 ua args (App f a) = ua (a:args) f

145 ua args t = (t, reverse args)

149 ua args t = (t, reverse args)

146

150

151+forget :: TT Name -> Raw

152+forget tm = fe [] tm

153+ where

154+ fe env (P _ n _) = Var n

155+ fe env (V i) = Var (env !! i)

156+ fe env (Bind n b sc) = RBind n (fmap (fe env) b)

157+ (fe (n:env) sc)

158+ fe env (App f a) = RApp (fe env f) (fe env a)

159+ fe env (Set i) = RSet i

160+

147type Term = TT Name

161type Term = TT Name

148type Type = Term

162type Type = Term

149

163

src/Elaborate.hs+59

@@ -13,8 +13,11 @@ module Elaborate(module Elaborate, module ProofState) where

13import ProofState

14import Core

15import Evaluate

16+import Typecheck

17import Control.Monad.State

18import Control.Monad.State

19+import Data.Char

20+import Debug.Trace

19-- I don't really want this here, but it's useful for the test shell

22-- I don't really want this here, but it's useful for the test shell

20data Command = Theorem Name Raw

23data Command = Theorem Name Raw

@@ -48,6 +51,39 @@ get_env :: Elab Env

48get_env = do (p, _) <- get

51get_env = do (p, _) <- get

49 lift $ envAtFocus p

52 lift $ envAtFocus p

54+-- get the current goal type

55+goal :: Elab Type

56+goal = do (p, _) <- get

57+ lift $ goalAtFocus p

58+

59+-- typecheck locally

60+get_type :: Raw -> Elab Type

61+get_type tm = do ctxt <- get_context

62+ env <- get_env

63+ (val, ty) <- lift $ check ctxt env tm

64+ return (vToP ty)

65+

66+-- given a desired hole name, return a unique hole name

67+unique_hole :: Name -> Elab Name

68+unique_hole n = do env <- get_env

69+ return (uniq n (map fst env))

70+ where

71+ uniq n hs | n `elem` hs = uniq (next n) hs

72+ | otherwise = n

73+

74+next (MN i n) = MN (i+1) n

75+next (UN (x:xs)) = let (num', nm') = span isDigit (reverse x)

76+ nm = reverse nm'

77+ num = readN (reverse num') in

78+ UN ((nm ++ show (num+1)) : xs)

79+ where

80+ readN "" = 0

81+ readN x = read x

82+

83+log :: String -> Elab ()

84+log str = do (p, logs) <- get

85+ put (p, logs ++ str ++ "\n")

86+

51-- The primitives, from ProofState

87-- The primitives, from ProofState

53attack :: Elab ()

89attack :: Elab ()

@@ -86,12 +122,35 @@ forall n t = processTactic' (Forall n t)

86focus :: Name -> Elab ()

122focus :: Name -> Elab ()

87focus n = processTactic' (Focus n)

123focus n = processTactic' (Focus n)

124

125+movelast :: Name -> Elab ()

126+movelast n = processTactic' (MoveLast n)

127+

89proofstate :: Elab ()

128proofstate :: Elab ()

90proofstate = processTactic' ProofState

129proofstate = processTactic' ProofState

130

92qed :: Elab ()

131qed :: Elab ()

93qed = processTactic' QED

132qed = processTactic' QED

133

134+prepare_apply :: Raw -> [Bool] -> Elab [Name]

135+prepare_apply fn imps =

136+ do ty <- get_type fn

137+ let claims = getArgs ty imps

138+ mapM doClaim claims

139+ where

140+ getArgs (Bind n (Pi t) sc) (i : is) = (n, t, i):getArgs sc is

141+ getArgs t i = []

142+

143+ doClaim (n', t, i) =

144+ do n <- unique_hole n'

145+ claim n (forget t)

146+ when i (movelast n)

147+ return n

148+

149+apply :: Raw -> [Bool] -> Elab ()

150+apply fn imps =

151+ do args <- prepare_apply fn imps

152+ unify_fill (raw_apply fn (map Var args))

153+

95-- Some combinators on elaborations

154-- Some combinators on elaborations

155

97-- Sequencing

156-- Sequencing

src/ProofState.hs+16−3

@@ -4,7 +4,7 @@

4 proofs, and some high level commands for introducing new theorems,

5 evaluation/checking inside the proof system, etc. --}

7−module ProofState(ProofState(..), newProof, envAtFocus,

7+module ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,

8 Tactic(..), processTactic) where

10import Typecheck

@@ -42,13 +42,14 @@ data Tactic = Attack

42 | Intro Name

43 | Forall Name Raw

44 | Focus Name

45+ | MoveLast Name

45 | ProofState

46 | ProofState

46 | QED

47 | QED

47−-- Next: add 'EvalHere' and 'CheckHere' tactics

49data TacticAction = AddGoal Name -- add a new goal, solve immediately

50 | NextGoal Name -- add a new goal, solve it after current one

51 | FocusGoal Name -- focus on this goal next

52+ | MoveGoal Name -- move this goal to the end of the hole queue

52 | Solved Name

53 | Solved Name

53 | AlsoSolved Name Term -- goals solved by unification

54 | AlsoSolved Name Term -- goals solved by unification

54 | Log String

55 | Log String

@@ -111,6 +112,11 @@ envAtFocus ps

111 return (premises g)

112 return (premises g)

112 | otherwise = fail "No holes"

113 | otherwise = fail "No holes"

113

114

115+goalAtFocus :: ProofState -> TC Type

116+goalAtFocus ps

117+ | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)

118+ return (binderTy (goalType g))

119+

114goal :: Hole -> Term -> TC Goal

120goal :: Hole -> Term -> TC Goal

115goal h tm = g [] tm where

121goal h tm = g [] tm where

116 g env (Bind n b sc) | hole b && same h n = return $ GD env b

122 g env (Bind n b sc) | hole b && same h n = return $ GD env b

@@ -160,6 +166,10 @@ focus :: Name -> RunTactic

160focus n ctxt env t = do action (FocusGoal n)

166focus n ctxt env t = do action (FocusGoal n)

161 return t

167 return t

162

168

169+movelast :: Name -> RunTactic

170+movelast n ctxt env t = do action (MoveGoal n)

171+ return t

172+

163-- Hmmm. YAGNI?

173-- Hmmm. YAGNI?

164regret :: RunTactic

174regret :: RunTactic

165regret = undefined

175regret = undefined

@@ -257,6 +267,7 @@ processTactic t ps

257 goals g (AddGoal n : xs) = goals (n : g) xs

267 goals g (AddGoal n : xs) = goals (n : g) xs

258 goals (g:gs) (NextGoal n : xs) = goals (g : n : gs) xs

268 goals (g:gs) (NextGoal n : xs) = goals (g : n : gs) xs

259 goals g (FocusGoal n : xs) = goals (n : (g \\ [n])) xs

269 goals g (FocusGoal n : xs) = goals (n : (g \\ [n])) xs

270+ goals g (MoveGoal n : xs) = goals ((g \\ [n]) ++ [n]) xs

260 goals g (Solved n : xs) = goals (g \\ [n]) xs

271 goals g (Solved n : xs) = goals (g \\ [n]) xs

261 goals g (AlsoSolved n tm : xs) = goals (g \\ [n]) xs

272 goals g (AlsoSolved n tm : xs) = goals (g \\ [n]) xs

262 goals g (_ : xs) = goals g xs

273 goals g (_ : xs) = goals g xs

@@ -265,8 +276,9 @@ processTactic t ps

265 getSolved (AlsoSolved n tm : xs) = (n, tm) : getSolved xs

276 getSolved (AlsoSolved n tm : xs) = (n, tm) : getSolved xs

266 getSolved (_ : xs) = getSolved xs

277 getSolved (_ : xs) = getSolved xs

267

278

268− updateSolved xs (Bind n b t)

279+ updateSolved xs (Bind n b@(Hole _) t)

269 | Just v <- lookup n xs = Bind n (Let (binderTy b) v) (updateSolved xs t)

280 | Just v <- lookup n xs = Bind n (Let (binderTy b) v) (updateSolved xs t)

281+ updateSolved xs (Bind n b t)

270 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)

282 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)

271 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)

283 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)

272 updateSolved xs t = t

284 updateSolved xs t = t

@@ -285,3 +297,4 @@ process t h ps = tactic (Just h) ps (context ps) (mktac t)

285 mktac (CheckIn r) = check_in r

297 mktac (CheckIn r) = check_in r

286 mktac (EvalIn r) = eval_in r

298 mktac (EvalIn r) = eval_in r

287 mktac (Focus n) = focus n

299 mktac (Focus n) = focus n

300+ mktac (MoveLast n) = movelast n

src/ShellParser.hs+5

@@ -50,6 +50,8 @@ pTactic = do reserved "attack"; return attack

50 <|> do reserved "regret"; return regret

51 <|> do reserved "fill"; tm <- pTerm; return (fill tm)

52 <|> do reserved "unify"; tm <- pTerm; return (unify_fill tm)

53+ <|> do reserved "apply"; tm <- pTerm; args <- many pArgType;

54+ return (apply tm args)

53 <|> do reserved "solve"; return solve

55 <|> do reserved "solve"; return solve

54 <|> do reserved "compute"; return compute

56 <|> do reserved "compute"; return compute

55 <|> do reserved "intro"; n <- iName; return (intro n)

57 <|> do reserved "intro"; n <- iName; return (intro n)

@@ -61,4 +63,7 @@ pTactic = do reserved "attack"; return attack

61 <|> do reserved "state"; return proofstate

63 <|> do reserved "state"; return proofstate

62 <|> do reserved "qed"; return qed

64 <|> do reserved "qed"; return qed

66+pArgType :: Parser Bool

67+pArgType = do lchar '_'; return True -- implicit (machine fills in)

68+ <|> do lchar '?'; return False -- user fills in