git.iko.soy/Idris-dev
on master help sign in
Improved performance by not going through PQuote and doing less normalisation
d479f4aJan Bessai
samples/reflection.idr+4−6
compare with master
unifiedsplit
@@ -65,13 +65,11 @@ firstEq ((_, (Let _ y))::(_, (Let _ x))::(_, Let _ f)::Nil) _ = Exact (App (App
65firstEq ((y, Lam yt)::(x, Lam xt)::(_, Let _ f)::Nil) _ = Exact (App (App f (P (Bound) x xt)) (P Bound y yt))
65firstEq ((y, Lam yt)::(x, Lam xt)::(_, Let _ f)::Nil) _ = Exact (App (App f (P (Bound) x xt)) (P Bound y yt))
66firstEq xs _ = Exact (TConst (I 0))
66firstEq xs _ = Exact (TConst (I 0))
67
67
68−-- | Skip 3 arguments of the proof context and return the fourth one which
68+-- | Skip 1 argument of the proof context and return the second one which
69−-- has to be introduced.
70−-- Used for the tactical dispatch example, which will push dispatch,
69+-- has to be introduced. Used for the tactical dispatch example, which
71−-- its current proof context, the goal, and the result of dispatch applied to it
70+-- will push dispatch, as first env agrument.
72−-- first.
73innerTac : List (TTName, Binder TT) -> TT -> Tactic
71innerTac : List (TTName, Binder TT) -> TT -> Tactic
74−innerTac (_::_::_::_::(x, Lam xt)::_) _ = Exact (P Bound x xt)
72+innerTac (_::(x, Lam xt)::_) _ = Exact (P Bound x xt)
75
73
76-- | Returns the reflected representation of innerTac
74-- | Returns the reflected representation of innerTac
77innerTacTT : TT
75innerTacTT : TT
src/Idris/ElabTerm.hs+22−48
@@ -773,64 +773,38 @@ runTac autoSolve ist tac = do env <- get_env
773 runT Solve = solve
773 runT Solve = solve
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
777 tgoal <- goal -- store the goal
777 tgoal <- goal -- store the goal
778 attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...
778 attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...
779− valn <- unique_hole (MN 0 "tacval")
779+ script <- unique_hole (MN 0 "script")
780− claim valn (RBind (UN "__pi_arg")
780+ claim script scriptTy
781− (Pi (RApp listTy envTupleType))
782− (RBind (UN "__pi_arg1") (Pi (Var $ reflm "TT")) tacticTy))
783− tacn <- unique_hole (MN 0 "tacn" )
781+ scriptvar <- unique_hole (MN 0 "scriptvar" )
784− letbind tacn (RBind (UN "__pi_arg")
782+ letbind scriptvar scriptTy (Var script)
785− (Pi (RApp listTy envTupleType))
786− (RBind (UN "__pi_arg1") (Pi (Var $ reflm "TT")) tacticTy))
787− (Var valn)
788− focus valn
783+ focus script
789 elab ist toplevel False False (MN 0 "tac") tm
784 elab ist toplevel False False (MN 0 "tac") tm
790− (tm', ty') <- get_type_val (Var tacn)
791− ctxt <- get_context
792− env <- get_env
793− let tm'' = normalise ctxt env tm'
794− -- let x : List (TTName, Binder TT) = reflectEnv in ...
795− envval <- unique_hole (MN 0 "letval")
796− claim envval (RApp listTy envTupleType)
797− letn <- unique_hole (MN 0 "letvar")
798− letbind letn (RApp listTy envTupleType) (Var envval)
799− focus envval
800− env <- get_env
801− elab ist toplevel False False (MN 0 "tac") (PQuote (reflectEnv tenv))
802− (env', _) <- get_type_val (Var letn)
785+ (script', _) <- get_type_val (Var scriptvar)
803− ctxt <- get_context
786+ -- now that we have the script apply
804− env <- get_env
787+ -- it to the reflected goal and context
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'
818− -- let z : Tactic = f x g
819− restac <- unique_hole (MN 0 "letval")
788+ restac <- unique_hole (MN 0 "restac")
820 claim restac tacticTy
789 claim restac tacticTy
821− letn <- unique_hole (MN 0 "letvar")
822− letbind letn tacticTy (Var restac)
823 focus restac
790 focus restac
824− elab
825− ist toplevel False False (MN 0 "tac")
826− (PQuote (raw_apply (forget tm'') [forget env'', forget goal'']))
791+ fill (raw_apply (forget script')
827− (res, _) <- get_type_val (Var letn)
792+ [reflectEnv tenv, reflect tgoal])
793+ restac' <- get_guess
794+ solve
795+ -- normalise the result in order to
796+ -- reify it
828 ctxt <- get_context
797 ctxt <- get_context
829 env <- get_env
798 env <- get_env
830− let tactic = normalise ctxt env res
799+ let tactic = normalise ctxt env restac'
831 runReflected tactic
800 runReflected tactic
832 where tacticTy = Var (reflm "Tactic")
801 where tacticTy = Var (reflm "Tactic")
833 listTy = Var (NS (UN "List") ["List", "Prelude"])
802 listTy = Var (NS (UN "List") ["List", "Prelude"])
803+ scriptTy = (RBind (UN "__pi_arg")
804+ (Pi (RApp listTy envTupleType))
805+ (RBind (UN "__pi_arg1")
806+ (Pi (Var $ reflm "TT")) tacticTy))
807+
834 runT (Reflect v) = do attack -- let x = reflect v in ...
808 runT (Reflect v) = do attack -- let x = reflect v in ...
835 tyn <- unique_hole (MN 0 "letty")
809 tyn <- unique_hole (MN 0 "letty")
836 claim tyn RType
810 claim tyn RType