Commit 8d660e91 by Janno

### Do not always call vm_compute for `change_dep`.

```The calls to `vm_change_dep` were put in without properly benchmarking
them. They do not correspond to the original ltac code, which uses just
`change`.```
parent eda63869
 ... ... @@ -261,7 +261,7 @@ Definition solve_closed : tactic := mmatch P in Prop as P' return M (P' *m _) with | [#] Closed | X e =n> e' <- W.of_expr e; TT.vm_change_dep (fun e => Closed X e) (W.to_expr e') ( TT.change_dep (fun e => Closed X e) (W.to_expr e') ( TT.apply (W.is_closed_correct _ _) <**> (TT.vm_compute <**> TT.change True (TT.apply I)) ... ... @@ -285,7 +285,7 @@ Definition solve_into_val : tactic := mmatch P in Prop as P' return M (P' *m _) with | [#] IntoVal | e v =n> e' <- W.of_expr e; TT.vm_change_dep (fun e => to_val e = Some v) (W.to_expr e') ( TT.change_dep (fun e => to_val e = Some v) (W.to_expr e') ( TT.apply (W.to_val_Some _ _) <**> TT.reflexivity (*TT.by' ( simpl &> T.unfold W.to_expr &> T.reflexivity ... ... @@ -308,7 +308,7 @@ Definition solve_as_val : tactic := mmatch P in Prop as P' return M (P' *m _) with | [#] AsVal | e =n> e' <- W.of_expr e; TT.vm_change_dep (fun e => is_Some (to_val e)) (W.to_expr e') ( TT.change_dep (fun e => is_Some (to_val e)) (W.to_expr e') ( (TT.apply (@W.to_val_is_Some e') <**> ( dec <- M.solve_typeclass_or_fail _; ... ... @@ -334,7 +334,7 @@ Definition solve_atomic : tactic := mmatch P in Prop as P' return M (P' *m _) with | [#] @Atomic heap_lang | s e =u> e' <- W.of_expr e; TT.vm_change_dep (Atomic s) (W.to_expr e') ( TT.change_dep (Atomic s) (W.to_expr e') ( TT.apply (W.is_atomic_correct _ _) <**> (TT.vm_change_dep (fun P => P) True (TT.vm_compute <**> TT.apply I)) ) ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!