58bd7c4 · Idris-dev · git.iko.soy

lib/builtins.idr+4

compare with master

unifiedsplit

@@ -7,6 +7,10 @@ getSigIdx (Exists a v) = a;

7getSigVal : {P : a -> Set} -> (s : Sigma a P) -> P (getSigIdx s);

8getSigVal (Exists a v) = v;

9

10+-- For rewrite tactic

11+replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Set} -> x = y -> P x -> P y;

12+replace refl prf = prf;

13+

10lazy : a -> a;

14lazy : a -> a;

11lazy x = x; -- compiled specially

15lazy x = x; -- compiled specially

12

16

src/Core/Elaborate.hs+6−1

@@ -182,6 +182,9 @@ forall n t = processTactic' (Forall n t)

182letbind :: Name -> Raw -> Raw -> Elab ()

183letbind n t v = processTactic' (LetBind n t v)

184

185+rewrite :: Raw -> Elab ()

186+rewrite tm = processTactic' (Rewrite tm)

187+

185patvar :: Name -> Elab ()

188patvar :: Name -> Elab ()

186patvar n = processTactic' (PatVar n)

189patvar n = processTactic' (PatVar n)

187

190

@@ -242,7 +245,9 @@ apply fn imps =

242 fill (raw_apply fn (map Var args))

245 fill (raw_apply fn (map Var args))

243 -- *Don't* solve the arguments we're specifying by hand.

246 -- *Don't* solve the arguments we're specifying by hand.

244 -- (remove from unified list before calling end_unify)

247 -- (remove from unified list before calling end_unify)

248+ -- HMMM: Actually, if we get it wrong, the typechecker will complain!

249+ -- so do nothing

245− let dontunify = map fst (filter (not.snd) (zip args imps))

250+ let dontunify = [] -- map fst (filter (not.snd) (zip args imps))

246 ES p s prev <- get

251 ES p s prev <- get

247 let (n, hs) = unified p

252 let (n, hs) = unified p

248 let unify = (n, filter (\ (n, t) -> not (n `elem` dontunify)) hs)

253 let unify = (n, filter (\ (n, t) -> not (n `elem` dontunify)) hs)

src/Core/ProofState.hs+27

@@ -50,6 +50,7 @@ data Tactic = Attack

50 | Intro Name

51 | Forall Name Raw

52 | LetBind Name Raw Raw

53+ | Rewrite Raw

53 | PatVar Name

54 | PatVar Name

54 | PatBind Name

55 | PatBind Name

55 | Focus Name

56 | Focus Name

@@ -280,6 +281,31 @@ letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

280 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))

281 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))

281letbind n ty val ctxt env _ = fail "Can't let bind here"

282letbind n ty val ctxt env _ = fail "Can't let bind here"

282

283

284+rewrite :: Raw -> RunTactic

285+rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =

286+ do (tmv, tmt) <- lift $ check ctxt env tm

287+ case unApply tmt of

288+ (P _ (UN ["="]) _, [lt,rt,l,r]) ->

289+ do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)

290+ let newt = mkP l r l t

291+ return (Bind x (Hole newt)

292+ (mkApp (P Ref (UN ["replace"]) (Set 0))

293+ [lt, l, r, p, tmv, xp]))

294+ -- fail $ "Rewrite " ++ show l ++ " to " ++ show r ++ " in " ++

295+ -- show t ++ " with " ++ show (p, newt) ++ " not done yet"

296+ _ -> fail "Not an equality type"

297+ where

298+ -- to make the P for rewrite, replace syntactic occurrences of l in ty with

299+ -- and x, and put \x : lt in front

300+ mkP lt l r ty | l == ty = lt

301+ mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f

302+ a' = if (r /= a) then mkP lt l r a else a in

303+ App f' a'

304+ mkP lt l r x = x

305+

306+ rname = MN 0 "replaced"

307+rewrite _ _ _ _ = fail "Can't rewrite here"

308+

283patbind :: Name -> RunTactic

309patbind :: Name -> RunTactic

284patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

310patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

285 do let t' = normalise ctxt env t

311 do let t' = normalise ctxt env t

@@ -390,6 +416,7 @@ process t h = tactic (Just h) (mktac t)

390 mktac (Intro n) = intro n

416 mktac (Intro n) = intro n

391 mktac (Forall n t) = forall n t

417 mktac (Forall n t) = forall n t

392 mktac (LetBind n t v) = letbind n t v

418 mktac (LetBind n t v) = letbind n t v

419+ mktac (Rewrite t) = rewrite t

393 mktac (PatVar n) = patvar n

420 mktac (PatVar n) = patvar n

394 mktac (PatBind n) = patbind n

421 mktac (PatBind n) = patbind n

395 mktac (CheckIn r) = check_in r

422 mktac (CheckIn r) = check_in r

src/Idris/AbsSyntax.hs+1−1

@@ -219,7 +219,7 @@ data PTerm = PQuote Raw

219 deriving Eq

220

221data PTactic = Intro [Name] | Focus Name

222− | Refine Name [Bool]

222+ | Refine Name [Bool] | Rewrite PTerm

223 | Exact PTerm

224 | Solve

225 | Attack

src/Idris/ElabDecls.hs+12

@@ -428,6 +428,18 @@ runTac (Exact tm) = do elab toplevel False tm

428 solveAll

429runTac (Refine fn imps) = do ns <- apply (Var fn) imps

430 solveAll

431+runTac (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

432+ = do attack; -- (h:_) <- get_holes

433+ tyn <- unique_hole (MN 0 "rty")

434+ -- start_unify h

435+ claim tyn (RSet 0)

436+ valn <- unique_hole (MN 0 "rval")

437+ claim valn (Var tyn)

438+ letn <- unique_hole (MN 0 "rewrite_rule")

439+ letbind letn (Var tyn) (Var valn)

440+ focus valn

441+ elab toplevel False tm

442+ rewrite (Var letn)

431runTac (Focus n) = focus n

443runTac (Focus n) = focus n

432runTac Solve = solve

444runTac Solve = solve

433runTac x = fail $ "Not implemented " ++ show x

445runTac x = fail $ "Not implemented " ++ show x

src/Idris/Parser.hs+3

@@ -601,6 +601,9 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

601 Nothing -> []

602 Just args -> map isImp args

603 return $ Refine n imps

604+ <|> do reserved "rewrite"; t <- pExpr syn;

605+ i <- getState

606+ return $ Rewrite (desugar syn i t)

604 <|> do reserved "focus"; n <- pName

607 <|> do reserved "focus"; n <- pName

605 return $ Focus n

608 return $ Focus n

606 <|> do reserved "exact"; t <- pExpr syn;

609 <|> do reserved "exact"; t <- pExpr syn;

src/Idris/Prover.hs+3−2

@@ -61,9 +61,10 @@ dumpState ist ps@(PS nm (h:hs) _ tm _ _ i _ cyxy _ _)

61 tshow t = show (delab ist t)

62

63 showPs [] = ""

64+ showPs ((MN _ "rewrite_rule", _) : bs) = showPs bs

64 showPs ((n, Let t v) : bs)

65 showPs ((n, Let t v) : bs)

65− = " " ++ show n ++ " : " ++

66+ = " " ++ show n ++ " = " ++ tshow v ++ " : " ++

66− tshow t ++ " = " ++ tshow v ++ "\n" ++ showPs bs

67+ tshow t ++ "\n" ++ showPs bs

67 showPs ((n, b) : bs)

68 showPs ((n, b) : bs)

68 = " " ++ show n ++ " : " ++

69 = " " ++ show n ++ " : " ++

69 tshow (binderTy b) ++ "\n" ++ showPs bs

70 tshow (binderTy b) ++ "\n" ++ showPs bs