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

git.iko.soy/Idris-dev

Added rewrite tactic

commit58bd7c4287513913d55a0ea3f7a84595fd33b78b authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 31 Oct 2011, 13:50 (15 years ago) parent6cc3c32

7 files changed+56−4

compare with master

unifiedsplit

lib/builtins.idr+4 src/Core/Elaborate.hs+6−1 src/Core/ProofState.hs+27 src/Idris/AbsSyntax.hs+1−1 src/Idris/ElabDecls.hs+12 src/Idris/Parser.hs+3 src/Idris/Prover.hs+3−2

lib/builtins.idr+4

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

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

88getSigVal (Exists a v) = v;

10+-- For rewrite tactic

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

12+replace refl prf = prf;

13+

1014lazy : a -> a;

1115lazy x = x; -- compiled specially

1216

src/Core/Elaborate.hs+6−1

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

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

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

184184

185+rewrite :: Raw -> Elab ()

186+rewrite tm = processTactic' (Rewrite tm)

187+

185188patvar :: Name -> Elab ()

186189patvar n = processTactic' (PatVar n)

187190

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

242245 fill (raw_apply fn (map Var args))

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

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

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

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

249+ -- so do nothing

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

246251 ES p s prev <- get

247252 let (n, hs) = unified p

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

src/Core/ProofState.hs+27

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

5050 | Intro Name

5151 | Forall Name Raw

5252 | LetBind Name Raw Raw

53+ | Rewrite Raw

5354 | PatVar Name

5455 | PatBind Name

5556 | Focus Name

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

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

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

282283

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+

283309patbind :: Name -> RunTactic

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

285311 do let t' = normalise ctxt env t

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

390416 mktac (Intro n) = intro n

391417 mktac (Forall n t) = forall n t

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

419+ mktac (Rewrite t) = rewrite t

393420 mktac (PatVar n) = patvar n

394421 mktac (PatBind n) = patbind n

395422 mktac (CheckIn r) = check_in r

src/Idris/AbsSyntax.hs+1−1

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

219219 deriving Eq

220220

221221data PTactic = Intro [Name] | Focus Name

222− | Refine Name [Bool]

222+ | Refine Name [Bool] | Rewrite PTerm

223223 | Exact PTerm

224224 | Solve

225225 | Attack

src/Idris/ElabDecls.hs+12

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

428428 solveAll

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

430430 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)

431443runTac (Focus n) = focus n

432444runTac Solve = solve

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

src/Idris/Parser.hs+3

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

601601 Nothing -> []

602602 Just args -> map isImp args

603603 return $ Refine n imps

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

605+ i <- getState

606+ return $ Rewrite (desugar syn i t)

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

605608 return $ Focus n

606609 <|> 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 _ _)

6161 tshow t = show (delab ist t)

6262

6363 showPs [] = ""

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

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

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

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

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

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

6768 showPs ((n, b) : bs)

6869 = " " ++ show n ++ " : " ++

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