git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1973 from david-christiansen/wip/tactical
97bc9dfDavid Christiansen
idris.cabal+3
compare with master
unifiedsplit
@@ -548,6 +548,9 @@ Extra-source-files:
548 test/sugar005/*.idr
548 test/sugar005/*.idr
549 test/sugar005/expected
549 test/sugar005/expected
550
550
551+ test/tactics001/run
552+ test/tactics001/*.idr
553+ test/tactics001/expected
551
554
552 test/totality001/run
555 test/totality001/run
553 test/totality001/*.idr
556 test/totality001/*.idr
libs/prelude/Language/Reflection.idr+181−33
@@ -267,108 +267,193 @@ data Tactic =
267%name Tactic tac, tac'
267%name Tactic tac, tac'
268
268
269
269
270−||| Things with a canonical representation in the TT datatype.
270+||| Things with a canonical representation as a reflected term.
271|||
271|||
272||| This type class is intended to be used during proof automation and the
272||| This type class is intended to be used during proof automation and the
273||| construction of custom tactics.
273||| construction of custom tactics.
274|||
274|||
275||| @ a the type to be quoted
275||| @ a the type to be quoted
276+||| @ t the type to quote it to (typically `TT` or `Raw`)
276−class Quotable a where
277+class Quotable a t where
277 ||| A representation of the type `a`.
278 ||| A representation of the type `a`.
278 |||
279 |||
279 ||| This is to enable quoting polymorphic datatypes
280 ||| This is to enable quoting polymorphic datatypes
280− quotedTy : TT
281+ quotedTy : t
281
282
282 ||| Quote a particular element of `a`.
283 ||| Quote a particular element of `a`.
283 |||
284 |||
284 ||| Each equation should look something like ```quote (Foo x y) = `(Foo ~(quote x) ~(quote y))```
285 ||| Each equation should look something like ```quote (Foo x y) = `(Foo ~(quote x) ~(quote y))```
285− quote : a -> TT
286+ quote : a -> t
286
287
287−instance Quotable Nat where
288+instance Quotable Nat TT where
288 quotedTy = `(Nat)
289 quotedTy = `(Nat)
289
290
290 quote Z = `(Z)
291 quote Z = `(Z)
291 quote (S k) = `(S ~(quote k))
292 quote (S k) = `(S ~(quote k))
292
293
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
294 quotedTy = `(Int)
301 quotedTy = `(Int)
295 quote x = TConst (I x)
302 quote x = TConst (I x)
296
303
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
298 quotedTy = `(Float)
309 quotedTy = `(Float)
299 quote x = TConst (Fl x)
310 quote x = TConst (Fl x)
300
311
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
302 quotedTy = `(Char)
317 quotedTy = `(Char)
303 quote x = TConst (Ch x)
318 quote x = TConst (Ch x)
304
319
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
306 quotedTy = `(Bits8)
325 quotedTy = `(Bits8)
307 quote x = TConst (B8 x)
326 quote x = TConst (B8 x)
308
327
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
310 quotedTy = `(Bits16)
333 quotedTy = `(Bits16)
311 quote x = TConst (B16 x)
334 quote x = TConst (B16 x)
312
335
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
314 quotedTy = `(Bits32)
341 quotedTy = `(Bits32)
315 quote x = TConst (B32 x)
342 quote x = TConst (B32 x)
316
343
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
318 quotedTy = `(Bits64)
349 quotedTy = `(Bits64)
319 quote x = TConst (B64 x)
350 quote x = TConst (B64 x)
320
351
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
322 quotedTy = `(Integer)
357 quotedTy = `(Integer)
323 quote x = TConst (BI x)
358 quote x = TConst (BI x)
324
359
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
326 quotedTy = `(Bits8x16)
365 quotedTy = `(Bits8x16)
327 quote x = TConst (B8V x)
366 quote x = TConst (B8V x)
328
367
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
330 quotedTy = `(Bits16x8)
373 quotedTy = `(Bits16x8)
331 quote x = TConst (B16V x)
374 quote x = TConst (B16V x)
332
375
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
334 quotedTy = `(Bits32x4)
381 quotedTy = `(Bits32x4)
335 quote x = TConst (B32V x)
382 quote x = TConst (B32V x)
336
383
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
338 quotedTy = `(Bits64x2)
389 quotedTy = `(Bits64x2)
339 quote x = TConst (B64V x)
390 quote x = TConst (B64V x)
340
391
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
342 quotedTy = `(String)
397 quotedTy = `(String)
343 quote x = TConst (Str x)
398 quote x = TConst (Str x)
344
399
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
346 quotedTy = `(NameType)
405 quotedTy = `(NameType)
347 quote Bound = `(Bound)
406 quote Bound = `(Bound)
348 quote Ref = `(Ref)
407 quote Ref = `(Ref)
349 quote (DCon x y) = `(DCon ~(quote x) ~(quote y))
408 quote (DCon x y) = `(DCon ~(quote x) ~(quote y))
350 quote (TCon x y) = `(TCon ~(quote x) ~(quote y))
409 quote (TCon x y) = `(TCon ~(quote x) ~(quote y))
351
410
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+
352−instance Quotable a => Quotable (List a) where
418+instance Quotable a TT => Quotable (List a) TT where
353 quotedTy = `(List ~(quotedTy {a=a}))
419 quotedTy = `(List ~(quotedTy {a=a}))
354 quote [] = `(List.Nil {a=~quotedTy})
420 quote [] = `(List.Nil {a=~quotedTy})
355 quote (x :: xs) = `(List.(::) {a=~quotedTy} ~(quote x) ~(quote xs))
421 quote (x :: xs) = `(List.(::) {a=~quotedTy} ~(quote x) ~(quote xs))
356
422
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
358 quotedTy = `(TTName)
429 quotedTy = `(TTName)
359 quote (UN x) = `(UN ~(quote x))
430 quote (UN x) = `(UN ~(quote x))
360 quote (NS n xs) = `(NS ~(quote n) ~(quote xs))
431 quote (NS n xs) = `(NS ~(quote n) ~(quote xs))
361 quote (MN x y) = `(MN ~(quote x) ~(quote y))
432 quote (MN x y) = `(MN ~(quote x) ~(quote y))
362 quote NErased = `(NErased)
433 quote NErased = `(NErased)
363
434
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
365 quotedTy = `(NativeTy)
450 quotedTy = `(NativeTy)
366 quote IT8 = `(Reflection.IT8)
451 quote IT8 = `(Reflection.IT8)
367 quote IT16 = `(Reflection.IT16)
452 quote IT16 = `(Reflection.IT16)
368 quote IT32 = `(Reflection.IT32)
453 quote IT32 = `(Reflection.IT32)
369 quote IT64 = `(Reflection.IT64)
454 quote IT64 = `(Reflection.IT64)
370
455
371−instance Quotable Reflection.IntTy where
456+instance Quotable Reflection.IntTy TT where
372 quotedTy = `(Reflection.IntTy)
457 quotedTy = `(Reflection.IntTy)
373 quote (ITFixed x) = `(ITFixed ~(quote x))
458 quote (ITFixed x) = `(ITFixed ~(quote x))
374 quote ITNative = `(Reflection.ITNative)
459 quote ITNative = `(Reflection.ITNative)
@@ -376,12 +461,25 @@ instance Quotable Reflection.IntTy where
376 quote ITChar = `(Reflection.ITChar)
461 quote ITChar = `(Reflection.ITChar)
377 quote (ITVec x y) = `(ITVec ~(quote x) ~(quote y))
462 quote (ITVec x y) = `(ITVec ~(quote x) ~(quote y))
378
463
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
380 quotedTy = `(ArithTy)
473 quotedTy = `(ArithTy)
381 quote (ATInt x) = `(ATInt ~(quote x))
474 quote (ATInt x) = `(ATInt ~(quote x))
382 quote ATFloat = `(ATFloat)
475 quote ATFloat = `(ATFloat)
383
476
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
385 quotedTy = `(Const)
483 quotedTy = `(Const)
386 quote (I x) = `(I ~(quote x))
484 quote (I x) = `(I ~(quote x))
387 quote (BI x) = `(BI ~(quote x))
485 quote (BI x) = `(BI ~(quote x))
@@ -406,19 +504,55 @@ instance Quotable Const where
406 quote WorldType = `(WorldType)
504 quote WorldType = `(WorldType)
407 quote TheWorld = `(TheWorld)
505 quote TheWorld = `(TheWorld)
408
506
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
410 quotedTy = `(TTUExp)
533 quotedTy = `(TTUExp)
411 quote (UVar x) = `(UVar ~(quote x))
534 quote (UVar x) = `(UVar ~(quote x))
412 quote (UVal x) = `(UVal ~(quote x))
535 quote (UVal x) = `(UVal ~(quote x))
413
536
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
415 quotedTy = `(Universe)
549 quotedTy = `(Universe)
416 quote Reflection.NullType = `(NullType)
550 quote Reflection.NullType = `(NullType)
417 quote Reflection.UniqueType = `(UniqueType)
551 quote Reflection.UniqueType = `(UniqueType)
418 quote Reflection.AllTypes = `(AllTypes)
552 quote Reflection.AllTypes = `(AllTypes)
419
553
420mutual
554mutual
421− instance Quotable TT where
555+ instance Quotable TT TT where
422 quotedTy = `(TT)
556 quotedTy = `(TT)
423 quote (P nt n tm) = `(P ~(quote nt) ~(quote n) ~(quote tm))
557 quote (P nt n tm) = `(P ~(quote nt) ~(quote n) ~(quote tm))
424 quote (V x) = `(V ~(quote x))
558 quote (V x) = `(V ~(quote x))
@@ -431,7 +565,7 @@ mutual
431 quote (TType uexp) = `(TType ~(quote uexp))
565 quote (TType uexp) = `(TType ~(quote uexp))
432 quote (UType u) = `(UType ~(quote u))
566 quote (UType u) = `(UType ~(quote u))
433
567
434− instance Quotable (Binder TT) where
568+ instance Quotable (Binder TT) TT where
435 quotedTy = `(Binder TT)
569 quotedTy = `(Binder TT)
436 quote (Lam x) = `(Lam {a=TT} ~(assert_total (quote x)))
570 quote (Lam x) = `(Lam {a=TT} ~(assert_total (quote x)))
437 quote (Pi x k) = `(Pi {a=TT} ~(assert_total (quote x))
571 quote (Pi x k) = `(Pi {a=TT} ~(assert_total (quote x))
@@ -448,7 +582,7 @@ mutual
448 quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x)))
582 quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x)))
449
583
450
584
451−instance Quotable ErrorReportPart where
585+instance Quotable ErrorReportPart TT where
452 quotedTy = `(ErrorReportPart)
586 quotedTy = `(ErrorReportPart)
453 quote (TextPart x) = `(TextPart ~(quote x))
587 quote (TextPart x) = `(TextPart ~(quote x))
454 quote (NamePart n) = `(NamePart ~(quote n))
588 quote (NamePart n) = `(NamePart ~(quote n))
@@ -476,15 +610,15 @@ mutual
476 quoteRawBinder (PVar x) = `(PVar {a=Raw} ~(quoteRaw x))
610 quoteRawBinder (PVar x) = `(PVar {a=Raw} ~(quoteRaw x))
477 quoteRawBinder (PVTy x) = `(PVTy {a=Raw} ~(quoteRaw x))
611 quoteRawBinder (PVTy x) = `(PVTy {a=Raw} ~(quoteRaw x))
478
612
479−instance Quotable Raw where
613+instance Quotable Raw TT where
480 quotedTy = `(Raw)
614 quotedTy = `(Raw)
481 quote = quoteRaw
615 quote = quoteRaw
482
616
483−instance Quotable (Binder Raw) where
617+instance Quotable (Binder Raw) TT where
484 quotedTy = `(Binder Raw)
618 quotedTy = `(Binder Raw)
485 quote = quoteRawBinder
619 quote = quoteRawBinder
486
620
487−instance Quotable Tactic where
621+instance Quotable Tactic TT where
488 quotedTy = `(Tactic)
622 quotedTy = `(Tactic)
489 quote (Try tac tac') = `(Try ~(quote tac) ~(quote tac'))
623 quote (Try tac tac') = `(Try ~(quote tac) ~(quote tac'))
490 quote (GoalType x tac) = `(GoalType ~(quote x) ~(quote tac))
624 quote (GoalType x tac) = `(GoalType ~(quote x) ~(quote tac))
@@ -514,3 +648,17 @@ instance Quotable Tactic where
514 quote (Fail xs) = `(Fail ~(quote xs))
648 quote (Fail xs) = `(Fail ~(quote xs))
515 quote SourceFC = `(SourceFC)
649 quote SourceFC = `(SourceFC)
516
650
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
22 prim__Holes : Tactical (List TTName)
22 prim__Holes : Tactical (List TTName)
23 prim__Guess : Tactical (Maybe TT)
23 prim__Guess : Tactical (Maybe TT)
24
24
25+ prim__SourceLocation : Tactical SourceLocation
26+
25 prim__Forget : TT -> Tactical Raw
27 prim__Forget : TT -> Tactical Raw
26
28
27 prim__Gensym : String -> Tactical TTName
29 prim__Gensym : String -> Tactical TTName
@@ -32,7 +34,10 @@ data Tactical : Type -> Type where
32 prim__Unfocus : TTName -> Tactical ()
34 prim__Unfocus : TTName -> Tactical ()
33 prim__Attack : Tactical ()
35 prim__Attack : Tactical ()
34
36
37+ prim__Rewrite : Raw -> Tactical ()
38+
35 prim__Claim : TTName -> Raw -> Tactical ()
39 prim__Claim : TTName -> Raw -> Tactical ()
40+ prim__Intro : Maybe TTName -> Tactical ()
36
41
37-------------
42-------------
38-- Public API
43-- Public API
@@ -93,3 +98,19 @@ attack = prim__Attack
93
98
94claim : TTName -> Raw -> Tactical ()
99claim : TTName -> Raw -> Tactical ()
95claim n ty = prim__Claim n ty
100claim 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
28
28
29import Util.Pretty hiding (fill)
29import Util.Pretty hiding (fill)
30
30
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−
38data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))
31data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))
39 deriving Show
32 deriving Show
40
33
src/Idris/ElabTerm.hs+40−23
@@ -1066,7 +1066,7 @@ elab ist info emode opts fn tm
1066 delayElab $ do focus h
1066 delayElab $ do focus h
1067 dotterm
1067 dotterm
1068 elab' ina fc t
1068 elab' ina fc t
1069− elab' ina _ (PRunTactics fc tm) =
1069+ elab' ina fc (PRunTactics fc' tm) =
1070 do attack
1070 do attack
1071 n <- getNameFrom (sMN 0 "tacticScript")
1071 n <- getNameFrom (sMN 0 "tacticScript")
1072 n' <- getNameFrom (sMN 0 "tacticExpr")
1072 n' <- getNameFrom (sMN 0 "tacticExpr")
@@ -1075,10 +1075,10 @@ elab ist info emode opts fn tm
1075 movelast n
1075 movelast n
1076 letbind n' scriptTy (Var n)
1076 letbind n' scriptTy (Var n)
1077 focus n
1077 focus n
1078− elab' ina (Just fc) tm
1078+ elab' ina (Just fc') tm
1079 env <- get_env
1079 env <- get_env
1080 ctxt <- get_context
1080 ctxt <- get_context
1081− runTactical fc ctxt env (P Bound n' Erased)
1081+ runTactical (maybe fc' id fc) ctxt env (P Bound n' Erased)
1082 solve
1082 solve
1083 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
1083 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
1084
1084
@@ -1508,7 +1508,7 @@ case_ ind autoSolve ist fn tm = do
1508runTactical :: FC -> Context -> Env -> Term -> ElabD ()
1508runTactical :: FC -> Context -> Env -> Term -> ElabD ()
1509runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
1509runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
1510 where
1510 where
1511− eval = normaliseAll ctxt env
1511+ eval = normaliseAll ctxt env . finalise
1512 tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]
1512 tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]
1513 returnUnit = fmap fst $ get_type_val (Var unitCon)
1513 returnUnit = fmap fst $ get_type_val (Var unitCon)
1514
1514
@@ -1540,6 +1540,9 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
1540 else fmap fst . get_type_val $
1540 else fmap fst . get_type_val $
1541 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1541 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1542 (Var (reflm "TT"))
1542 (Var (reflm "TT"))
1543+ | n == tacN "prim__SourceLocation", [] <- args
1544+ = fmap fst . get_type_val $
1545+ reflectFC fc
1543 | n == tacN "prim__Env", [] <- args
1546 | n == tacN "prim__Env", [] <- args
1544 = do env <- get_env
1547 = do env <- get_env
1545 fmap fst . get_type_val $ reflectEnv env
1548 fmap fst . get_type_val $ reflectEnv env
@@ -1547,7 +1550,7 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
1547 = do parts <- reifyReportParts (eval errs)
1550 = do parts <- reifyReportParts (eval errs)
1548 lift . tfail $ ReflectionError [parts] (Msg "")
1551 lift . tfail $ ReflectionError [parts] (Msg "")
1549 | n == tacN "prim__PureTactical", [_a, tm] <- args
1552 | n == tacN "prim__PureTactical", [_a, tm] <- args
1550− = return tm
1553+ = return tm
1551 | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args
1554 | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args
1552 = do let first' = eval first
1555 = do let first' = eval first
1553 res <- runTacTm first'
1556 res <- runTacTm first'
@@ -1575,6 +1578,10 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
1575 | n == tacN "prim__Attack", [] <- args
1578 | n == tacN "prim__Attack", [] <- args
1576 = do attack
1579 = do attack
1577 returnUnit
1580 returnUnit
1581+ | n == tacN "prim__Rewrite", [rule] <- args
1582+ = do r <- reifyRaw rule
1583+ rewrite r
1584+ returnUnit
1578 | n == tacN "prim__Focus", [what] <- args
1585 | n == tacN "prim__Focus", [what] <- args
1579 = do n' <- reifyTTName what
1586 = do n' <- reifyTTName what
1580 focus n'
1587 focus n'
@@ -1583,6 +1590,12 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
1583 = do n' <- reifyTTName what
1590 = do n' <- reifyTTName what
1584 movelast n'
1591 movelast n'
1585 returnUnit
1592 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
1586 runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x
1599 runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x
1587
1600
1588-- Running tactics directly
1601-- Running tactics directly
@@ -1829,22 +1842,7 @@ runTac autoSolve ist perhapsFC fn tac
1829 case perhapsFC of
1842 case perhapsFC of
1830 Nothing -> lift . tfail $ Msg "There is no source location available."
1843 Nothing -> lift . tfail $ Msg "There is no source location available."
1831 Just fc ->
1844 Just fc ->
1832− do let intTy = RConstant (AType (ATInt ITNative))
1845+ do fill $ reflectFC fc
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− ]
1848 solve
1846 solve
1849 runT x = fail $ "Not implemented " ++ show x
1847 runT x = fail $ "Not implemented " ++ show x
1850
1848
@@ -1966,7 +1964,7 @@ reifyRaw t@(App _ _)
1966 | (P _ f _, args) <- unApply t = reifyRawApp f args
1964 | (P _ f _, args) <- unApply t = reifyRawApp f args
1967reifyRaw t@(P _ n _)
1965reifyRaw t@(P _ n _)
1968 | n == reflm "RType" = return $ RType
1966 | 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)
1970
1968
1971reifyRawApp :: Name -> [Term] -> ElabD Raw
1969reifyRawApp :: Name -> [Term] -> ElabD Raw
1972reifyRawApp t [n]
1970reifyRawApp t [n]
@@ -1982,7 +1980,7 @@ reifyRawApp t [t']
1982 | t == reflm "RForce" = liftM RForce (reifyRaw t')
1980 | t == reflm "RForce" = liftM RForce (reifyRaw t')
1983reifyRawApp t [c]
1981reifyRawApp t [c]
1984 | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)
1982 | 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))
1986
1984
1987reifyTTName :: Term -> ElabD Name
1985reifyTTName :: Term -> ElabD Name
1988reifyTTName t
1986reifyTTName t
@@ -2617,6 +2615,25 @@ reflectErr (LoadingFailed str err) =
2617 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
2615 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
2618reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
2616reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
2619
2617
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+
2620elaboratingArgErr :: [(Name, Name)] -> Err -> Err
2637elaboratingArgErr :: [(Name, Name)] -> Err -> Err
2621elaboratingArgErr [] err = err
2638elaboratingArgErr [] err = err
2622elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)
2639elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)
src/Idris/ParseExpr.hs+3−1
@@ -878,7 +878,9 @@ pi syn =
878 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)) <|> (do
878 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)) <|> (do
879 try (lchar '{' *> reserved "default")
879 try (lchar '{' *> reserved "default")
880 when (st == Static) $ fail "default tactic constraints can not be static"
880 when (st == Static) $ fail "default tactic constraints can not be static"
881+ ist <- get
881− script <- simpleExpr syn
882+ script' <- simpleExpr syn
883+ let script = debindApp syn . desugar syn ist $ script'
882 xt <- typeDeclList syn
884 xt <- typeDeclList syn
883 lchar '}'
885 lchar '}'
884 symbol "->"
886 symbol "->"
src/Idris/ParseHelpers.hs+1−1
@@ -326,7 +326,7 @@ commentMarkers :: [String]
326commentMarkers = [ "--", "|||" ]
326commentMarkers = [ "--", "|||" ]
327
327
328invalidOperators :: [String]
328invalidOperators :: [String]
329−invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\"]
329+invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%"]
330
330
331-- | Parses an operator
331-- | Parses an operator
332operator :: MonadicParsing m => m String
332operator :: 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