git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1973 from david-christiansen/wip/tactical

Updates to new-style tactics

commit97bc9dfc0ceee3f8e5d3ab54da53f3dab5803ded authorDavid Christiansen <david@davidchristiansen.dk> dateMon 2 Mar 2015, 22:58 (12 years ago) parent3233dd1a1c42ad
10 files changed+279−65
compare with master
unifiedsplit
idris.cabal+3 libs/prelude/Language/Reflection.idr+181−33 libs/prelude/Language/Reflection/Tactical.idr+21 src/Idris/Core/Elaborate.hs−7 src/Idris/ElabTerm.hs+40−23 src/Idris/ParseExpr.hs+3−1 src/Idris/ParseHelpers.hs+1−1 test/tactics001/Tactics.idr+27 test/tactics001/expected test/tactics001/run+3
idris.cabal+3
@@ -548,6 +548,9 @@ Extra-source-files:
548548 test/sugar005/*.idr
549549 test/sugar005/expected
550550
551+ test/tactics001/run
552+ test/tactics001/*.idr
553+ test/tactics001/expected
551554
552555 test/totality001/run
553556 test/totality001/*.idr
libs/prelude/Language/Reflection.idr+181−33
@@ -267,108 +267,193 @@ data Tactic =
267267%name Tactic tac, tac'
268268
269269
270−||| Things with a canonical representation in the TT datatype.
270+||| Things with a canonical representation as a reflected term.
271271|||
272272||| This type class is intended to be used during proof automation and the
273273||| construction of custom tactics.
274274|||
275275||| @ a the type to be quoted
276−class Quotable a where
276+||| @ t the type to quote it to (typically `TT` or `Raw`)
277+class Quotable a t where
277278 ||| A representation of the type `a`.
278279 |||
279280 ||| This is to enable quoting polymorphic datatypes
280− quotedTy : TT
281+ quotedTy : t
281282
282283 ||| Quote a particular element of `a`.
283284 |||
284285 ||| Each equation should look something like ```quote (Foo x y) = `(Foo ~(quote x) ~(quote y))```
285− quote : a -> TT
286+ quote : a -> t
286287
287−instance Quotable Nat where
288+instance Quotable Nat TT where
288289 quotedTy = `(Nat)
289290
290291 quote Z = `(Z)
291292 quote (S k) = `(S ~(quote k))
292293
293−instance Quotable Int where
294+instance Quotable Nat Raw where
295+ quotedTy = `(Nat)
296+
297+ quote Z = `(Z)
298+ quote (S k) = `(S ~(quote k))
299+
300+instance Quotable Int TT where
294301 quotedTy = `(Int)
295302 quote x = TConst (I x)
296303
297−instance Quotable Float where
304+instance Quotable Int Raw where
305+ quotedTy = `(Int)
306+ quote x = RConstant (I x)
307+
308+instance Quotable Float TT where
298309 quotedTy = `(Float)
299310 quote x = TConst (Fl x)
300311
301−instance Quotable Char where
312+instance Quotable Float Raw where
313+ quotedTy = `(Float)
314+ quote x = RConstant (Fl x)
315+
316+instance Quotable Char TT where
302317 quotedTy = `(Char)
303318 quote x = TConst (Ch x)
304319
305−instance Quotable Bits8 where
320+instance Quotable Char Raw where
321+ quotedTy = `(Char)
322+ quote x = RConstant (Ch x)
323+
324+instance Quotable Bits8 TT where
306325 quotedTy = `(Bits8)
307326 quote x = TConst (B8 x)
308327
309−instance Quotable Bits16 where
328+instance Quotable Bits8 Raw where
329+ quotedTy = `(Bits8)
330+ quote x = RConstant (B8 x)
331+
332+instance Quotable Bits16 TT where
310333 quotedTy = `(Bits16)
311334 quote x = TConst (B16 x)
312335
313−instance Quotable Bits32 where
336+instance Quotable Bits16 Raw where
337+ quotedTy = `(Bits16)
338+ quote x = RConstant (B16 x)
339+
340+instance Quotable Bits32 TT where
314341 quotedTy = `(Bits32)
315342 quote x = TConst (B32 x)
316343
317−instance Quotable Bits64 where
344+instance Quotable Bits32 Raw where
345+ quotedTy = `(Bits32)
346+ quote x = RConstant (B32 x)
347+
348+instance Quotable Bits64 TT where
318349 quotedTy = `(Bits64)
319350 quote x = TConst (B64 x)
320351
321−instance Quotable Integer where
352+instance Quotable Bits64 Raw where
353+ quotedTy = `(Bits64)
354+ quote x = RConstant (B64 x)
355+
356+instance Quotable Integer TT where
322357 quotedTy = `(Integer)
323358 quote x = TConst (BI x)
324359
325−instance Quotable Bits8x16 where
360+instance Quotable Integer Raw where
361+ quotedTy = `(Integer)
362+ quote x = RConstant (BI x)
363+
364+instance Quotable Bits8x16 TT where
326365 quotedTy = `(Bits8x16)
327366 quote x = TConst (B8V x)
328367
329−instance Quotable Bits16x8 where
368+instance Quotable Bits8x16 Raw where
369+ quotedTy = `(Bits8x16)
370+ quote x = RConstant (B8V x)
371+
372+instance Quotable Bits16x8 TT where
330373 quotedTy = `(Bits16x8)
331374 quote x = TConst (B16V x)
332375
333−instance Quotable Bits32x4 where
376+instance Quotable Bits16x8 Raw where
377+ quotedTy = `(Bits16x8)
378+ quote x = RConstant (B16V x)
379+
380+instance Quotable Bits32x4 TT where
334381 quotedTy = `(Bits32x4)
335382 quote x = TConst (B32V x)
336383
337−instance Quotable Bits64x2 where
384+instance Quotable Bits32x4 Raw where
385+ quotedTy = `(Bits32x4)
386+ quote x = RConstant (B32V x)
387+
388+instance Quotable Bits64x2 TT where
338389 quotedTy = `(Bits64x2)
339390 quote x = TConst (B64V x)
340391
341−instance Quotable String where
392+instance Quotable Bits64x2 Raw where
393+ quotedTy = `(Bits64x2)
394+ quote x = RConstant (B64V x)
395+
396+instance Quotable String TT where
342397 quotedTy = `(String)
343398 quote x = TConst (Str x)
344399
345−instance Quotable NameType where
400+instance Quotable String Raw where
401+ quotedTy = `(String)
402+ quote x = RConstant (Str x)
403+
404+instance Quotable NameType TT where
346405 quotedTy = `(NameType)
347406 quote Bound = `(Bound)
348407 quote Ref = `(Ref)
349408 quote (DCon x y) = `(DCon ~(quote x) ~(quote y))
350409 quote (TCon x y) = `(TCon ~(quote x) ~(quote y))
351410
352−instance Quotable a => Quotable (List a) where
411+instance Quotable NameType Raw where
412+ quotedTy = `(NameType)
413+ quote Bound = `(Bound)
414+ quote Ref = `(Ref)
415+ quote (DCon x y) = `(DCon ~(quote {t=Raw} x) ~(quote {t=Raw} y))
416+ quote (TCon x y) = `(TCon ~(quote {t=Raw} x) ~(quote {t=Raw} y))
417+
418+instance Quotable a TT => Quotable (List a) TT where
353419 quotedTy = `(List ~(quotedTy {a=a}))
354420 quote [] = `(List.Nil {a=~quotedTy})
355421 quote (x :: xs) = `(List.(::) {a=~quotedTy} ~(quote x) ~(quote xs))
356422
357−instance Quotable TTName where
423+instance Quotable a Raw => Quotable (List a) Raw where
424+ quotedTy = `(List ~(quotedTy {a=a}))
425+ quote [] = `(List.Nil {a=~quotedTy})
426+ quote (x :: xs) = `(List.(::) {a=~quotedTy} ~(quote x) ~(quote xs))
427+
428+instance Quotable TTName TT where
358429 quotedTy = `(TTName)
359430 quote (UN x) = `(UN ~(quote x))
360431 quote (NS n xs) = `(NS ~(quote n) ~(quote xs))
361432 quote (MN x y) = `(MN ~(quote x) ~(quote y))
362433 quote NErased = `(NErased)
363434
364−instance Quotable NativeTy where
435+instance Quotable TTName Raw where
436+ quotedTy = `(TTName)
437+ quote (UN x) = `(UN ~(quote {t=Raw} x))
438+ quote (NS n xs) = `(NS ~(quote {t=Raw} n) ~(quote {t=Raw} xs))
439+ quote (MN x y) = `(MN ~(quote {t=Raw} x) ~(quote {t=Raw} y))
440+ quote NErased = `(NErased)
441+
442+instance Quotable NativeTy TT where
443+ quotedTy = `(NativeTy)
444+ quote IT8 = `(Reflection.IT8)
445+ quote IT16 = `(Reflection.IT16)
446+ quote IT32 = `(Reflection.IT32)
447+ quote IT64 = `(Reflection.IT64)
448+
449+instance Quotable NativeTy Raw where
365450 quotedTy = `(NativeTy)
366451 quote IT8 = `(Reflection.IT8)
367452 quote IT16 = `(Reflection.IT16)
368453 quote IT32 = `(Reflection.IT32)
369454 quote IT64 = `(Reflection.IT64)
370455
371−instance Quotable Reflection.IntTy where
456+instance Quotable Reflection.IntTy TT where
372457 quotedTy = `(Reflection.IntTy)
373458 quote (ITFixed x) = `(ITFixed ~(quote x))
374459 quote ITNative = `(Reflection.ITNative)
@@ -376,12 +461,25 @@ instance Quotable Reflection.IntTy where
376461 quote ITChar = `(Reflection.ITChar)
377462 quote (ITVec x y) = `(ITVec ~(quote x) ~(quote y))
378463
379−instance Quotable ArithTy where
464+instance Quotable Reflection.IntTy Raw where
465+ quotedTy = `(Reflection.IntTy)
466+ quote (ITFixed x) = `(ITFixed ~(quote {t=Raw} x))
467+ quote ITNative = `(Reflection.ITNative)
468+ quote ITBig = `(ITBig)
469+ quote ITChar = `(Reflection.ITChar)
470+ quote (ITVec x y) = `(ITVec ~(quote {t=Raw} x) ~(quote {t=Raw} y))
471+
472+instance Quotable ArithTy TT where
380473 quotedTy = `(ArithTy)
381474 quote (ATInt x) = `(ATInt ~(quote x))
382475 quote ATFloat = `(ATFloat)
383476
384−instance Quotable Const where
477+instance Quotable ArithTy Raw where
478+ quotedTy = `(ArithTy)
479+ quote (ATInt x) = `(ATInt ~(quote {t=Raw} x))
480+ quote ATFloat = `(ATFloat)
481+
482+instance Quotable Const TT where
385483 quotedTy = `(Const)
386484 quote (I x) = `(I ~(quote x))
387485 quote (BI x) = `(BI ~(quote x))
@@ -406,19 +504,55 @@ instance Quotable Const where
406504 quote WorldType = `(WorldType)
407505 quote TheWorld = `(TheWorld)
408506
409−instance Quotable TTUExp where
507+instance Quotable Const Raw where
508+ quotedTy = `(Const)
509+ quote (I x) = `(I ~(quote {t=Raw} x))
510+ quote (BI x) = `(BI ~(quote {t=Raw} x))
511+ quote (Fl x) = `(Fl ~(quote {t=Raw} x))
512+ quote (Ch x) = `(Ch ~(quote {t=Raw} x))
513+ quote (Str x) = `(Str ~(quote {t=Raw} x))
514+ quote (B8 x) = `(B8 ~(quote {t=Raw} x))
515+ quote (B16 x) = `(B16 ~(quote {t=Raw} x))
516+ quote (B32 x) = `(B32 ~(quote {t=Raw} x))
517+ quote (B64 x) = `(B64 ~(quote {t=Raw} x))
518+ quote (B8V xs) = `(B8V ~(quote {t=Raw} xs))
519+ quote (B16V xs) = `(B16V ~(quote {t=Raw} xs))
520+ quote (B32V xs) = `(B32V ~(quote {t=Raw} xs))
521+ quote (B64V xs) = `(B64V ~(quote {t=Raw} xs))
522+ quote (AType x) = `(AType ~(quote {t=Raw} x))
523+ quote StrType = `(StrType)
524+ quote PtrType = `(PtrType)
525+ quote ManagedPtrType = `(ManagedPtrType)
526+ quote BufferType = `(BufferType)
527+ quote VoidType = `(VoidType)
528+ quote Forgot = `(Forgot)
529+ quote WorldType = `(WorldType)
530+ quote TheWorld = `(TheWorld)
531+
532+instance Quotable TTUExp TT where
410533 quotedTy = `(TTUExp)
411534 quote (UVar x) = `(UVar ~(quote x))
412535 quote (UVal x) = `(UVal ~(quote x))
413536
414−instance Quotable Universe where
537+instance Quotable TTUExp Raw where
538+ quotedTy = `(TTUExp)
539+ quote (UVar x) = `(UVar ~(quote {t=Raw} x))
540+ quote (UVal x) = `(UVal ~(quote {t=Raw} x))
541+
542+instance Quotable Universe TT where
543+ quotedTy = `(Universe)
544+ quote Reflection.NullType = `(NullType)
545+ quote Reflection.UniqueType = `(UniqueType)
546+ quote Reflection.AllTypes = `(AllTypes)
547+
548+instance Quotable Universe Raw where
415549 quotedTy = `(Universe)
416550 quote Reflection.NullType = `(NullType)
417551 quote Reflection.UniqueType = `(UniqueType)
418552 quote Reflection.AllTypes = `(AllTypes)
419553
420554mutual
421− instance Quotable TT where
555+ instance Quotable TT TT where
422556 quotedTy = `(TT)
423557 quote (P nt n tm) = `(P ~(quote nt) ~(quote n) ~(quote tm))
424558 quote (V x) = `(V ~(quote x))
@@ -431,7 +565,7 @@ mutual
431565 quote (TType uexp) = `(TType ~(quote uexp))
432566 quote (UType u) = `(UType ~(quote u))
433567
434− instance Quotable (Binder TT) where
568+ instance Quotable (Binder TT) TT where
435569 quotedTy = `(Binder TT)
436570 quote (Lam x) = `(Lam {a=TT} ~(assert_total (quote x)))
437571 quote (Pi x k) = `(Pi {a=TT} ~(assert_total (quote x))
@@ -448,7 +582,7 @@ mutual
448582 quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x)))
449583
450584
451−instance Quotable ErrorReportPart where
585+instance Quotable ErrorReportPart TT where
452586 quotedTy = `(ErrorReportPart)
453587 quote (TextPart x) = `(TextPart ~(quote x))
454588 quote (NamePart n) = `(NamePart ~(quote n))
@@ -476,15 +610,15 @@ mutual
476610 quoteRawBinder (PVar x) = `(PVar {a=Raw} ~(quoteRaw x))
477611 quoteRawBinder (PVTy x) = `(PVTy {a=Raw} ~(quoteRaw x))
478612
479−instance Quotable Raw where
613+instance Quotable Raw TT where
480614 quotedTy = `(Raw)
481615 quote = quoteRaw
482616
483−instance Quotable (Binder Raw) where
617+instance Quotable (Binder Raw) TT where
484618 quotedTy = `(Binder Raw)
485619 quote = quoteRawBinder
486620
487−instance Quotable Tactic where
621+instance Quotable Tactic TT where
488622 quotedTy = `(Tactic)
489623 quote (Try tac tac') = `(Try ~(quote tac) ~(quote tac'))
490624 quote (GoalType x tac) = `(GoalType ~(quote x) ~(quote tac))
@@ -514,3 +648,17 @@ instance Quotable Tactic where
514648 quote (Fail xs) = `(Fail ~(quote xs))
515649 quote SourceFC = `(SourceFC)
516650
651+
652+instance Quotable SourceLocation TT where
653+ quotedTy = `(SourceLocation)
654+ quote (FileLoc fn (sl, sc) (el, ec)) =
655+ `(FileLoc ~(quote fn)
656+ (~(quote sl), ~(quote sc))
657+ (~(quote el), ~(quote ec)))
658+
659+instance Quotable SourceLocation Raw where
660+ quotedTy = `(SourceLocation)
661+ quote (FileLoc fn (sl, sc) (el, ec)) =
662+ `(FileLoc ~(quote {t=Raw} fn)
663+ (~(quote {t=Raw} sl), ~(quote {t=Raw} sc))
664+ (~(quote {t=Raw} el), ~(quote {t=Raw} ec)))
libs/prelude/Language/Reflection/Tactical.idr+21
@@ -22,6 +22,8 @@ data Tactical : Type -> Type where
2222 prim__Holes : Tactical (List TTName)
2323 prim__Guess : Tactical (Maybe TT)
2424
25+ prim__SourceLocation : Tactical SourceLocation
26+
2527 prim__Forget : TT -> Tactical Raw
2628
2729 prim__Gensym : String -> Tactical TTName
@@ -32,7 +34,10 @@ data Tactical : Type -> Type where
3234 prim__Unfocus : TTName -> Tactical ()
3335 prim__Attack : Tactical ()
3436
37+ prim__Rewrite : Raw -> Tactical ()
38+
3539 prim__Claim : TTName -> Raw -> Tactical ()
40+ prim__Intro : Maybe TTName -> Tactical ()
3641
3742-------------
3843-- Public API
@@ -93,3 +98,19 @@ attack = prim__Attack
9398
9499claim : TTName -> Raw -> Tactical ()
95100claim n ty = prim__Claim n ty
101+
102+intro : Maybe TTName -> Tactical ()
103+intro n = prim__Intro n
104+
105+||| Find out the present source context for the tactic script
106+getSourceLocation : Tactical SourceLocation
107+getSourceLocation = prim__SourceLocation
108+
109+||| Attempt to solve the current goal with the source code location
110+sourceLocation : Tactical ()
111+sourceLocation = do loc <- getSourceLocation
112+ fill (quote loc)
113+ solve
114+
115+rewriteWith : Raw -> Tactical ()
116+rewriteWith rule = prim__Rewrite rule
src/Idris/Core/Elaborate.hs−7
@@ -28,13 +28,6 @@ import Debug.Trace
2828
2929import Util.Pretty hiding (fill)
3030
31−-- I don't really want this here, but it's useful for the test shell
32−data Command = Theorem Name Raw
33− | Eval Raw
34− | Quit
35− | Print Name
36− | Tac (Elab ())
37−
3831data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))
3932 deriving Show
4033
src/Idris/ElabTerm.hs+40−23
@@ -1066,7 +1066,7 @@ elab ist info emode opts fn tm
10661066 delayElab $ do focus h
10671067 dotterm
10681068 elab' ina fc t
1069− elab' ina _ (PRunTactics fc tm) =
1069+ elab' ina fc (PRunTactics fc' tm) =
10701070 do attack
10711071 n <- getNameFrom (sMN 0 "tacticScript")
10721072 n' <- getNameFrom (sMN 0 "tacticExpr")
@@ -1075,10 +1075,10 @@ elab ist info emode opts fn tm
10751075 movelast n
10761076 letbind n' scriptTy (Var n)
10771077 focus n
1078− elab' ina (Just fc) tm
1078+ elab' ina (Just fc') tm
10791079 env <- get_env
10801080 ctxt <- get_context
1081− runTactical fc ctxt env (P Bound n' Erased)
1081+ runTactical (maybe fc' id fc) ctxt env (P Bound n' Erased)
10821082 solve
10831083 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
10841084
@@ -1508,7 +1508,7 @@ case_ ind autoSolve ist fn tm = do
15081508runTactical :: FC -> Context -> Env -> Term -> ElabD ()
15091509runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
15101510 where
1511− eval = normaliseAll ctxt env
1511+ eval = normaliseAll ctxt env . finalise
15121512 tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]
15131513 returnUnit = fmap fst $ get_type_val (Var unitCon)
15141514
@@ -1540,6 +1540,9 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
15401540 else fmap fst . get_type_val $
15411541 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
15421542 (Var (reflm "TT"))
1543+ | n == tacN "prim__SourceLocation", [] <- args
1544+ = fmap fst . get_type_val $
1545+ reflectFC fc
15431546 | n == tacN "prim__Env", [] <- args
15441547 = do env <- get_env
15451548 fmap fst . get_type_val $ reflectEnv env
@@ -1547,7 +1550,7 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
15471550 = do parts <- reifyReportParts (eval errs)
15481551 lift . tfail $ ReflectionError [parts] (Msg "")
15491552 | n == tacN "prim__PureTactical", [_a, tm] <- args
1550− = return tm
1553+ = return tm
15511554 | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args
15521555 = do let first' = eval first
15531556 res <- runTacTm first'
@@ -1575,6 +1578,10 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
15751578 | n == tacN "prim__Attack", [] <- args
15761579 = do attack
15771580 returnUnit
1581+ | n == tacN "prim__Rewrite", [rule] <- args
1582+ = do r <- reifyRaw rule
1583+ rewrite r
1584+ returnUnit
15781585 | n == tacN "prim__Focus", [what] <- args
15791586 = do n' <- reifyTTName what
15801587 focus n'
@@ -1583,6 +1590,12 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
15831590 = do n' <- reifyTTName what
15841591 movelast n'
15851592 returnUnit
1593+ | n == tacN "prim__Intro", [mn] <- args
1594+ = do n <- case fromTTMaybe mn of
1595+ Nothing -> return Nothing
1596+ Just name -> fmap Just $ reifyTTName name
1597+ intro n
1598+ returnUnit
15861599 runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x
15871600
15881601-- Running tactics directly
@@ -1829,22 +1842,7 @@ runTac autoSolve ist perhapsFC fn tac
18291842 case perhapsFC of
18301843 Nothing -> lift . tfail $ Msg "There is no source location available."
18311844 Just fc ->
1832− do let intTy = RConstant (AType (ATInt ITNative))
1833− fill $ raw_apply (Var (reflm "FileLoc"))
1834− [ RConstant (Str (fc_fname fc))
1835− , raw_apply (Var pairCon) $
1836− [intTy, intTy] ++
1837− map (RConstant . I)
1838− [ fst (fc_start fc)
1839− , snd (fc_start fc)
1840− ]
1841− , raw_apply (Var pairCon) $
1842− [intTy, intTy] ++
1843− map (RConstant . I)
1844− [ fst (fc_end fc)
1845− , snd (fc_end fc)
1846− ]
1847− ]
1845+ do fill $ reflectFC fc
18481846 solve
18491847 runT x = fail $ "Not implemented " ++ show x
18501848
@@ -1966,7 +1964,7 @@ reifyRaw t@(App _ _)
19661964 | (P _ f _, args) <- unApply t = reifyRawApp f args
19671965reifyRaw t@(P _ n _)
19681966 | n == reflm "RType" = return $ RType
1969−reifyRaw t = fail ("Unknown reflection raw term: " ++ show t)
1967+reifyRaw t = fail ("Unknown reflection raw term in reifyRaw: " ++ show t)
19701968
19711969reifyRawApp :: Name -> [Term] -> ElabD Raw
19721970reifyRawApp t [n]
@@ -1982,7 +1980,7 @@ reifyRawApp t [t']
19821980 | t == reflm "RForce" = liftM RForce (reifyRaw t')
19831981reifyRawApp t [c]
19841982 | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)
1985−reifyRawApp t args = fail ("Unknown reflection raw term: " ++ show (t, args))
1983+reifyRawApp t args = fail ("Unknown reflection raw term in reifyRawApp: " ++ show (t, args))
19861984
19871985reifyTTName :: Term -> ElabD Name
19881986reifyTTName t
@@ -2617,6 +2615,25 @@ reflectErr (LoadingFailed str err) =
26172615 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
26182616reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
26192617
2618+-- | Reflect a file context
2619+reflectFC :: FC -> Raw
2620+reflectFC fc = raw_apply (Var (reflm "FileLoc"))
2621+ [ RConstant (Str (fc_fname fc))
2622+ , raw_apply (Var pairCon) $
2623+ [intTy, intTy] ++
2624+ map (RConstant . I)
2625+ [ fst (fc_start fc)
2626+ , snd (fc_start fc)
2627+ ]
2628+ , raw_apply (Var pairCon) $
2629+ [intTy, intTy] ++
2630+ map (RConstant . I)
2631+ [ fst (fc_end fc)
2632+ , snd (fc_end fc)
2633+ ]
2634+ ]
2635+ where intTy = RConstant (AType (ATInt ITNative))
2636+
26202637elaboratingArgErr :: [(Name, Name)] -> Err -> Err
26212638elaboratingArgErr [] err = err
26222639elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)
src/Idris/ParseExpr.hs+3−1
@@ -878,7 +878,9 @@ pi syn =
878878 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)) <|> (do
879879 try (lchar '{' *> reserved "default")
880880 when (st == Static) $ fail "default tactic constraints can not be static"
881− script <- simpleExpr syn
881+ ist <- get
882+ script' <- simpleExpr syn
883+ let script = debindApp syn . desugar syn ist $ script'
882884 xt <- typeDeclList syn
883885 lchar '}'
884886 symbol "->"
src/Idris/ParseHelpers.hs+1−1
@@ -326,7 +326,7 @@ commentMarkers :: [String]
326326commentMarkers = [ "--", "|||" ]
327327
328328invalidOperators :: [String]
329−invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\"]
329+invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%"]
330330
331331-- | Parses an operator
332332operator :: MonadicParsing m => m String
test/tactics001/Tactics.idrnew file+27
@@ -0,0 +1,27 @@
1+module Tactics
2+
3+import Language.Reflection.Tactical
4+
5+%default total
6+
7+-- Test that basic proofs with new-style tactics work
8+
9+||| Construct a Refl at some particular type for some particular term
10+||| @ t the type
11+||| @ x the term for equality to be reflexive at
12+refl : (t, x : Raw) -> Raw
13+refl t x = RApp (RApp (Var (UN "Refl")) t) x
14+
15+plusZeroRightNeutralNew : (n : Nat) -> plus n 0 = n
16+plusZeroRightNeutralNew Z = Refl
17+plusZeroRightNeutralNew (S k) =
18+ %runTactics (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var "k"))
19+ fill $ refl `(Nat : Type) `(S ~(Var (UN "k")))
20+ solve)
21+
22+plusSuccRightSuccNew : (j, k : Nat) -> plus j (S k) = S (plus j k)
23+plusSuccRightSuccNew Z k = Refl
24+plusSuccRightSuccNew (S j) k =
25+ %runTactics (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))
26+ fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))
27+ solve)
test/tactics001/expectednew file

No changes to the content.

test/tactics001/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ --check Tactics.idr
3+rm -f *.ibc