edfe9c6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added pattern arguments; bug fixes

commitedfe9c688ffce001d1ed34160bfed40c95f7761c authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 29 Sep 2011, 10:06 (15 years ago) parentee3dbaa

4 files changed+16−2

compare with master

unifiedsplit

src/Core.hs+1−1 src/Elaborate.hs+5 src/ProofState.hs+9−1 src/ShellParser.hs+1

src/Core.hs+1−1

@@ -198,7 +198,7 @@ showEnv' env t dbg = se 10 env t where

198198 sb env n (Lam t) = showb env "\\ " " => " n t

199199 sb env n (Hole t) = showb env "? " ". " n t

200200 sb env n (Pi t) = showb env "(" ") -> " n t

201− sb env n (PVar t) = showb env "! " ". " n t

201+ sb env n (PVar t) = showb env "pat " ". " n t

202202 sb env n (Let t v) = showbv env "let " " in " n t v

203203 sb env n (Guess t v) = showbv env "?? " " in " n t v

204204

src/Elaborate.hs+5

@@ -165,6 +165,11 @@ arg n tyhole = do ty <- unique_hole tyhole

165165 claim ty (RSet 0)

166166 forall n (Var ty)

167167

168+patarg :: Name -> Name -> Elab ()

169+patarg n tyhole = do ty <- unique_hole tyhole

170+ claim ty (RSet 0)

171+ patvar n (Var ty)

172+

168173-- Some combinators on elaborations

169174

170175-- Sequencing

src/ProofState.hs+9−1

@@ -186,7 +186,7 @@ exact guess ctxt env (Bind x (Hole ty) sc) =

186186 return $ Bind x (Guess ty val) sc

187187exact _ _ _ _ = fail "Can't fill here."

188188

189−-- As fill, but attempts to solve other goals by unification

189+-- As exact, but attempts to solve other goals by unification

190190

191191fill :: Raw -> RunTactic

192192fill guess ctxt env (Bind x (Hole ty) sc) =

@@ -252,6 +252,12 @@ eval_in t ctxt env tm =

252252 showEnv env valty'))

253253 return tm

254254

255+-- shuffleHoles :: Term -> Term

256+-- shuffleHoles tm = shuffle [] tm

257+-- where

258+-- shuffle ns (Bind n b sc)

259+-- |

260+

255261processTactic :: Tactic -> ProofState -> TC (ProofState, String)

256262processTactic QED ps = case holes ps of

257263 [] -> do let tm = pterm ps

@@ -297,6 +303,8 @@ processTactic t ps

297303 updateSolved xs (Bind n b t)

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

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

306+ updateSolved xs (P _ n _)

307+ | Just v <- lookup n xs = v

300308 updateSolved xs t = t

301309

302310process :: Tactic -> Name -> ProofState -> StateT TState TC ProofState

src/ShellParser.hs+1

@@ -60,6 +60,7 @@ pTactic = do reserved "attack"; return attack

6060 <|> do reserved "arg"; n <- iName; t <- iName; return (arg n t)

6161 <|> do reserved "patvar"; n <- iName; lchar ':'; ty <- pTerm

6262 return (patvar n ty)

63+ <|> do reserved "patarg"; n <- iName; t <- iName; return (patarg n t)

6364 <|> do reserved "eval"; t <- pTerm; return (eval_in t)

6465 <|> do reserved "check"; t <- pTerm; return (check_in t)

6566 <|> do reserved "focus"; n <- iName; return (focus n)