ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-11 03:34:13 +03:00
Code Issues Projects Releases Wiki Activity

Include reflection of the current goal in proofscript arguments

Browse Source
This commit is contained in:
Jan Bessai 2013-03-25 10:05:59 +01:00
parent 8ce17c634a
commit b65a0fbbfa
3 changed files with 53 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
effects/Effects.idr
View File

@ -59,19 +59,19 @@ rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
---- The Effect EDSL itself ----
-- some proof automation
findEffElem : Nat -> List (TTName, Binder TT) -> Tactic -- Nat is maximum search depth
findEffElem O ctxt = Refine "Here" `Seq` Solve
findEffElem (S n) ctxt = GoalType "EffElem"
findEffElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic -- Nat is maximum search depth
findEffElem O ctxt goal = Refine "Here" `Seq` Solve
findEffElem (S n) ctxt goal = GoalType "EffElem"
(Try (Refine "Here" `Seq` Solve)
(Refine "There" `Seq` (Solve `Seq` findEffElem n ctxt)))
(Refine "There" `Seq` (Solve `Seq` findEffElem n ctxt goal)))
findSubList : Nat -> List (TTName, Binder TT) -> Tactic
findSubList O ctxt = Refine "SubNil" `Seq` Solve
findSubList (S n) ctxt
findSubList : Nat -> List (TTName, Binder TT) -> TT -> Tactic
findSubList O ctxt goal = Refine "SubNil" `Seq` Solve
findSubList (S n) ctxt goal
= GoalType "SubList"
(Try (Refine "subListId" `Seq` Solve)
((Try (Refine "Keep" `Seq` Solve)
(Refine "Drop" `Seq` Solve)) `Seq` findSubList n ctxt))
(Refine "Drop" `Seq` Solve)) `Seq` findSubList n ctxt goal))
updateResTy : (xs : List EFFECT) -> EffElem e a xs -> e a b t ->
List EFFECT

31
samples/reflection.idr
View File

@ -60,33 +60,46 @@ intEq x y = case x == y of
-- | A tactic script to run intEq on two let-bound or introduced
-- arguments of the current (otherwise empty) proof context
firstEq : List (TTName, Binder TT) -> Tactic
firstEq ((_, (Let _ y))::(_, (Let _ x))::(_, Let _ f)::Nil) = Exact (App (App f x) y)
firstEq ((y, Lam yt)::(x, Lam xt)::(_, Let _ f)::Nil) = Exact (App (App f (P (Bound) x xt)) (P Bound y yt))
firstEq xs = Exact (TConst (I 0))
firstEq : List (TTName, Binder TT) -> TT -> Tactic
firstEq ((_, (Let _ y))::(_, (Let _ x))::(_, Let _ f)::Nil) _ = Exact (App (App f x) y)
firstEq ((y, Lam yt)::(x, Lam xt)::(_, Let _ f)::Nil) _ = Exact (App (App f (P (Bound) x xt)) (P Bound y yt))
firstEq xs _ = Exact (TConst (I 0))
-- | Skip 3 arguments of the proof context and return the fourth one which
-- has to be introduced.
-- Used for the tactical dispatch example, which will push dispatch,
-- its current proof context and the result of dispatch applied to it
-- its current proof context, the goal, and the result of dispatch applied to it
-- first.
innerTac : List (TTName, Binder TT) -> Tactic
innerTac (_::_::_::(x, Lam xt)::_) = Exact (P Bound x xt)
innerTac : List (TTName, Binder TT) -> TT -> Tactic
innerTac (_::_::_::_::(x, Lam xt)::_) _ = Exact (P Bound x xt)
-- | Returns the reflected representation of innerTac
innerTacTT : TT
innerTacTT = ?innerTacTTPrf
-- | Dispatch to the reflected rep. of innerTac
dispatch : List (TTName, Binder TT) -> Tactic
dispatch xs = ApplyTactic (innerTacTT)
dispatch : List (TTName, Binder TT) -> TT -> Tactic
dispatch xs _ = ApplyTactic (innerTacTT)
-- | Call dispatch which will then dispatch to innerTac.
tacticalDispatch : Int -> Int
tacticalDispatch = ?tacticalDispatchPrf
-- | A tactic to get the representation of its goal
studyGoalTac : List (TTName, Binder TT) -> TT -> Tactic
studyGoalTac _ goal = Reflect goal
-- | Returns the representation of its goal, TT
-- (so this is reflect on the type TT)
studyGoal : TT
studyGoal = ?studyGoalPrf
---------- Proofs ----------
ReflectionExamples.studyGoalPrf = proof {
applyTactic studyGoalTac;
}
ReflectionExamples.envTuplePrf = proof {
let x = tupleType;
fill x;

29
src/Idris/ElabTerm.hs
View File

@ -774,13 +774,16 @@ runTac autoSolve ist tac = do env <- get_env
runT (Try l r) = do try' (runT l) (runT r) True
runT (TSeq l r) = do runT l; runT r
runT (ApplyTactic tm) = do tenv <- get_env -- store the environment before it is loaded with junk
attack -- let f : List (TTName, Binder TT) -> Tactic = tm in ...
tgoal <- goal -- store the goal
attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...
valn <- unique_hole (MN 0 "tacval")
claim valn (RBind (UN "__pi_arg")
(Pi (RApp listTy envTupleType)) tacticTy)
tacn <- unique_hole (MN 0 "tacn")
(Pi (RApp listTy envTupleType))
(RBind (UN "__pi_arg1") (Pi (Var $ reflm "TT")) tacticTy))
tacn <- unique_hole (MN 0 "tacn" )
letbind tacn (RBind (UN "__pi_arg")
(Pi (RApp listTy envTupleType)) tacticTy)
(Pi (RApp listTy envTupleType))
(RBind (UN "__pi_arg1") (Pi (Var $ reflm "TT")) tacticTy))
(Var valn)
focus valn
elab ist toplevel False False (MN 0 "tac") tm
@ -800,13 +803,27 @@ runTac autoSolve ist tac = do env <- get_env
ctxt <- get_context
env <- get_env
let env'' = normalise ctxt env env'
-- let z : Tactic = f x
-- let g : TT = reflect tgoal
goalval <- unique_hole (MN 0 "letval")
claim goalval (Var $ reflm "TT")
letg <- unique_hole (MN 0 "letvar")
letbind letg (Var $ reflm "TT") (Var goalval)
focus goalval
env <- get_env
elab ist toplevel False False (MN 0 "tac") (PQuote (reflect tgoal))
(goal', _) <- get_type_val (Var letg)
ctxt <- get_context
env <- get_env
let goal'' = hnf ctxt env goal'
-- let z : Tactic = f x g
restac <- unique_hole (MN 0 "letval")
claim restac tacticTy
letn <- unique_hole (MN 0 "letvar")
letbind letn tacticTy (Var restac)
focus restac
elab ist toplevel False False (MN 0 "tac") (PQuote (RApp (forget tm'') (forget env'')))
elab
ist toplevel False False (MN 0 "tac")
(PQuote (raw_apply (forget tm'') [forget env'', forget goal'']))
(res, _) <- get_type_val (Var letn)
ctxt <- get_context
env <- get_env