git.iko.soy/Idris-dev
on master help sign in
Improved performance by not going through PQuote and doing less normalisation
commitd479f4acaa46e2cb1650f8de153f2076c75f3f7b authorJan Bessai <Jan.Bessai@tu-dortmund.de> dateMon 25 Mar 2013, 19:57 (14 years ago) parentb65a0fb
2 files changed+26−54
compare with master
unifiedsplit
samples/reflection.idr+4−6 src/Idris/ElabTerm.hs+22−48
samples/reflection.idr+4−6
@@ -65,13 +65,11 @@ firstEq ((_, (Let _ y))::(_, (Let _ x))::(_, Let _ f)::Nil) _ = Exact (App (App
6565firstEq ((y, Lam yt)::(x, Lam xt)::(_, Let _ f)::Nil) _ = Exact (App (App f (P (Bound) x xt)) (P Bound y yt))
6666firstEq xs _ = Exact (TConst (I 0))
6767
68−-- | Skip 3 arguments of the proof context and return the fourth one which
69−-- has to be introduced.
70−-- Used for the tactical dispatch example, which will push dispatch,
71−-- its current proof context, the goal, and the result of dispatch applied to it
72−-- first.
68+-- | Skip 1 argument of the proof context and return the second one which
69+-- has to be introduced. Used for the tactical dispatch example, which
70+-- will push dispatch, as first env agrument.
7371innerTac : 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)
7573
7674-- | Returns the reflected representation of innerTac
7775innerTacTT : TT
src/Idris/ElabTerm.hs+22−48
@@ -773,64 +773,38 @@ runTac autoSolve ist tac = do env <- get_env
773773 runT Solve = solve
774774 runT (Try l r) = do try' (runT l) (runT r) True
775775 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
777777 tgoal <- goal -- store the goal
778778 attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...
779− valn <- unique_hole (MN 0 "tacval")
780− claim valn (RBind (UN "__pi_arg")
781− (Pi (RApp listTy envTupleType))
782− (RBind (UN "__pi_arg1") (Pi (Var $ reflm "TT")) tacticTy))
783− tacn <- unique_hole (MN 0 "tacn" )
784− letbind tacn (RBind (UN "__pi_arg")
785− (Pi (RApp listTy envTupleType))
786− (RBind (UN "__pi_arg1") (Pi (Var $ reflm "TT")) tacticTy))
787− (Var valn)
788− focus valn
779+ script <- unique_hole (MN 0 "script")
780+ claim script scriptTy
781+ scriptvar <- unique_hole (MN 0 "scriptvar" )
782+ letbind scriptvar scriptTy (Var script)
783+ focus script
789784 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)
803− ctxt <- get_context
804− env <- get_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'
818− -- let z : Tactic = f x g
819− restac <- unique_hole (MN 0 "letval")
785+ (script', _) <- get_type_val (Var scriptvar)
786+ -- now that we have the script apply
787+ -- it to the reflected goal and context
788+ restac <- unique_hole (MN 0 "restac")
820789 claim restac tacticTy
821− letn <- unique_hole (MN 0 "letvar")
822− letbind letn tacticTy (Var restac)
823790 focus restac
824− elab
825− ist toplevel False False (MN 0 "tac")
826− (PQuote (raw_apply (forget tm'') [forget env'', forget goal'']))
827− (res, _) <- get_type_val (Var letn)
791+ fill (raw_apply (forget script')
792+ [reflectEnv tenv, reflect tgoal])
793+ restac' <- get_guess
794+ solve
795+ -- normalise the result in order to
796+ -- reify it
828797 ctxt <- get_context
829798 env <- get_env
830− let tactic = normalise ctxt env res
799+ let tactic = normalise ctxt env restac'
831800 runReflected tactic
832801 where tacticTy = Var (reflm "Tactic")
833802 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+
834808 runT (Reflect v) = do attack -- let x = reflect v in ...
835809 tyn <- unique_hole (MN 0 "letty")
836810 claim tyn RType