edfe9c6 · Idris-dev · git.iko.soy

src/Core.hs+1−1

compare with master

unifiedsplit

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

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

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

200 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

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

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

204

src/Elaborate.hs+5

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

165 claim ty (RSet 0)

166 forall n (Var ty)

167

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+

168-- Some combinators on elaborations

173-- Some combinators on elaborations

169

174

170-- Sequencing

175-- Sequencing

src/ProofState.hs+9−1

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

186 return $ Bind x (Guess ty val) sc

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

188

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

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

190

191fill :: Raw -> RunTactic

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

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

252 showEnv env valty'))

253 return tm

254

255+-- shuffleHoles :: Term -> Term

256+-- shuffleHoles tm = shuffle [] tm

257+-- where

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

259+-- |

260+

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

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

256processTactic QED ps = case holes ps of

262processTactic QED ps = case holes ps of

257 [] -> do let tm = pterm ps

263 [] -> do let tm = pterm ps

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

297 updateSolved xs (Bind n b t)

303 updateSolved xs (Bind n b t)

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

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

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

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

306+ updateSolved xs (P _ n _)

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

300 updateSolved xs t = t

308 updateSolved xs t = t

301

309

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

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

src/ShellParser.hs+1

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

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

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

62 return (patvar n ty)

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

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

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

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

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

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

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