git.iko.soy/Idris-dev
on master help sign in
Include reflection of the current goal in proofscript arguments
b65a0fbJan Bessai
effects/Effects.idr+8−8
compare with master
unifiedsplit
@@ -59,19 +59,19 @@ rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
59---- The Effect EDSL itself ----
59---- The Effect EDSL itself ----
60
60
61-- some proof automation
61-- some proof automation
62−findEffElem : Nat -> List (TTName, Binder TT) -> Tactic -- Nat is maximum search depth
62+findEffElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic -- Nat is maximum search depth
63−findEffElem O ctxt = Refine "Here" `Seq` Solve
63+findEffElem O ctxt goal = Refine "Here" `Seq` Solve
64−findEffElem (S n) ctxt = GoalType "EffElem"
64+findEffElem (S n) ctxt goal = GoalType "EffElem"
65 (Try (Refine "Here" `Seq` Solve)
65 (Try (Refine "Here" `Seq` Solve)
66− (Refine "There" `Seq` (Solve `Seq` findEffElem n ctxt)))
66+ (Refine "There" `Seq` (Solve `Seq` findEffElem n ctxt goal)))
67
67
68−findSubList : Nat -> List (TTName, Binder TT) -> Tactic
68+findSubList : Nat -> List (TTName, Binder TT) -> TT -> Tactic
69−findSubList O ctxt = Refine "SubNil" `Seq` Solve
69+findSubList O ctxt goal = Refine "SubNil" `Seq` Solve
70−findSubList (S n) ctxt
70+findSubList (S n) ctxt goal
71 = GoalType "SubList"
71 = GoalType "SubList"
72 (Try (Refine "subListId" `Seq` Solve)
72 (Try (Refine "subListId" `Seq` Solve)
73 ((Try (Refine "Keep" `Seq` Solve)
73 ((Try (Refine "Keep" `Seq` Solve)
74− (Refine "Drop" `Seq` Solve)) `Seq` findSubList n ctxt))
74+ (Refine "Drop" `Seq` Solve)) `Seq` findSubList n ctxt goal))
75
75
76updateResTy : (xs : List EFFECT) -> EffElem e a xs -> e a b t ->
76updateResTy : (xs : List EFFECT) -> EffElem e a xs -> e a b t ->
77 List EFFECT
77 List EFFECT
samples/reflection.idr+22−9
@@ -60,33 +60,46 @@ intEq x y = case x == y of
60
60
61-- | A tactic script to run intEq on two let-bound or introduced
61-- | A tactic script to run intEq on two let-bound or introduced
62-- arguments of the current (otherwise empty) proof context
62-- arguments of the current (otherwise empty) proof context
63−firstEq : List (TTName, Binder TT) -> Tactic
63+firstEq : List (TTName, Binder TT) -> TT -> Tactic
64−firstEq ((_, (Let _ y))::(_, (Let _ x))::(_, Let _ f)::Nil) = Exact (App (App f x) y)
64+firstEq ((_, (Let _ y))::(_, (Let _ x))::(_, Let _ f)::Nil) _ = Exact (App (App f x) y)
65−firstEq ((y, Lam yt)::(x, Lam xt)::(_, Let _ f)::Nil) = Exact (App (App f (P (Bound) x xt)) (P Bound y yt))
65+firstEq ((y, Lam yt)::(x, Lam xt)::(_, Let _ f)::Nil) _ = Exact (App (App f (P (Bound) x xt)) (P Bound y yt))
66−firstEq xs = Exact (TConst (I 0))
66+firstEq xs _ = Exact (TConst (I 0))
67
67
68-- | Skip 3 arguments of the proof context and return the fourth one which
68-- | Skip 3 arguments of the proof context and return the fourth one which
69-- has to be introduced.
69-- has to be introduced.
70-- Used for the tactical dispatch example, which will push dispatch,
70-- Used for the tactical dispatch example, which will push dispatch,
71−-- its current proof context and the result of dispatch applied to it
71+-- its current proof context, the goal, and the result of dispatch applied to it
72-- first.
72-- first.
73−innerTac : List (TTName, Binder TT) -> Tactic
73+innerTac : List (TTName, Binder TT) -> TT -> Tactic
74−innerTac (_::_::_::(x, Lam xt)::_) = Exact (P Bound x xt)
74+innerTac (_::_::_::_::(x, Lam xt)::_) _ = Exact (P Bound x xt)
75
75
76-- | Returns the reflected representation of innerTac
76-- | Returns the reflected representation of innerTac
77innerTacTT : TT
77innerTacTT : TT
78innerTacTT = ?innerTacTTPrf
78innerTacTT = ?innerTacTTPrf
79
79
80-- | Dispatch to the reflected rep. of innerTac
80-- | Dispatch to the reflected rep. of innerTac
81−dispatch : List (TTName, Binder TT) -> Tactic
81+dispatch : List (TTName, Binder TT) -> TT -> Tactic
82−dispatch xs = ApplyTactic (innerTacTT)
82+dispatch xs _ = ApplyTactic (innerTacTT)
83
83
84-- | Call dispatch which will then dispatch to innerTac.
84-- | Call dispatch which will then dispatch to innerTac.
85tacticalDispatch : Int -> Int
85tacticalDispatch : Int -> Int
86tacticalDispatch = ?tacticalDispatchPrf
86tacticalDispatch = ?tacticalDispatchPrf
87
87
88+-- | A tactic to get the representation of its goal
89+studyGoalTac : List (TTName, Binder TT) -> TT -> Tactic
90+studyGoalTac _ goal = Reflect goal
91+
92+-- | Returns the representation of its goal, TT
93+-- (so this is reflect on the type TT)
94+studyGoal : TT
95+studyGoal = ?studyGoalPrf
96+
88---------- Proofs ----------
97---------- Proofs ----------
89
98
99+ReflectionExamples.studyGoalPrf = proof {
100+ applyTactic studyGoalTac;
101+}
102+
90ReflectionExamples.envTuplePrf = proof {
103ReflectionExamples.envTuplePrf = proof {
91 let x = tupleType;
104 let x = tupleType;
92 fill x;
105 fill x;
src/Idris/ElabTerm.hs+23−6
@@ -774,13 +774,16 @@ runTac autoSolve ist tac = do env <- get_env
774 runT (Try l r) = do try' (runT l) (runT r) True
774 runT (Try l r) = do try' (runT l) (runT r) True
775 runT (TSeq l r) = do runT l; runT r
775 runT (TSeq l r) = do runT l; runT r
776 runT (ApplyTactic tm) = do tenv <- get_env -- store the environment before it is loaded with junk
776 runT (ApplyTactic tm) = do tenv <- get_env -- store the environment before it is loaded with junk
777+ tgoal <- goal -- store the goal
777− attack -- let f : List (TTName, Binder TT) -> Tactic = tm in ...
778+ attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...
778 valn <- unique_hole (MN 0 "tacval")
779 valn <- unique_hole (MN 0 "tacval")
779 claim valn (RBind (UN "__pi_arg")
780 claim valn (RBind (UN "__pi_arg")
780− (Pi (RApp listTy envTupleType)) tacticTy)
781+ (Pi (RApp listTy envTupleType))
782+ (RBind (UN "__pi_arg1") (Pi (Var $ reflm "TT")) tacticTy))
781− tacn <- unique_hole (MN 0 "tacn")
783+ tacn <- unique_hole (MN 0 "tacn" )
782 letbind tacn (RBind (UN "__pi_arg")
784 letbind tacn (RBind (UN "__pi_arg")
783− (Pi (RApp listTy envTupleType)) tacticTy)
785+ (Pi (RApp listTy envTupleType))
786+ (RBind (UN "__pi_arg1") (Pi (Var $ reflm "TT")) tacticTy))
784 (Var valn)
787 (Var valn)
785 focus valn
788 focus valn
786 elab ist toplevel False False (MN 0 "tac") tm
789 elab ist toplevel False False (MN 0 "tac") tm
@@ -800,13 +803,27 @@ runTac autoSolve ist tac = do env <- get_env
800 ctxt <- get_context
803 ctxt <- get_context
801 env <- get_env
804 env <- get_env
802 let env'' = normalise ctxt env env'
805 let env'' = normalise ctxt env env'
806+ -- let g : TT = reflect tgoal
807+ goalval <- unique_hole (MN 0 "letval")
808+ claim goalval (Var $ reflm "TT")
809+ letg <- unique_hole (MN 0 "letvar")
810+ letbind letg (Var $ reflm "TT") (Var goalval)
811+ focus goalval
812+ env <- get_env
813+ elab ist toplevel False False (MN 0 "tac") (PQuote (reflect tgoal))
814+ (goal', _) <- get_type_val (Var letg)
815+ ctxt <- get_context
816+ env <- get_env
817+ let goal'' = hnf ctxt env goal'
803− -- let z : Tactic = f x
818+ -- let z : Tactic = f x g
804 restac <- unique_hole (MN 0 "letval")
819 restac <- unique_hole (MN 0 "letval")
805 claim restac tacticTy
820 claim restac tacticTy
806 letn <- unique_hole (MN 0 "letvar")
821 letn <- unique_hole (MN 0 "letvar")
807 letbind letn tacticTy (Var restac)
822 letbind letn tacticTy (Var restac)
808 focus restac
823 focus restac
824+ elab
809− elab ist toplevel False False (MN 0 "tac") (PQuote (RApp (forget tm'') (forget env'')))
825+ ist toplevel False False (MN 0 "tac")
826+ (PQuote (raw_apply (forget tm'') [forget env'', forget goal'']))
810 (res, _) <- get_type_val (Var letn)
827 (res, _) <- get_type_val (Var letn)
811 ctxt <- get_context
828 ctxt <- get_context
812 env <- get_env
829 env <- get_env