mirror of
https://github.com/dart-lang/sdk
synced 2024-09-16 04:06:59 +00:00
ed0590b532
- Fix force_options so it doesn't take so long to run - Fix property get typechecking so it forces getters to be synchronized with methods. - Simplify member_env. Bug: Change-Id: I3e2a0710c7fde950e7573ba6216820907b9ae374 Reviewed-on: https://dart-review.googlesource.com/9040 Reviewed-by: Dmitry Stefantsov <dmitryas@google.com>
76 lines
2.8 KiB
Coq
76 lines
2.8 KiB
Coq
(* Copyright (c) 2017, the Dart project authors. Please see the AUTHORS file
|
|
* for details. All rights reserved. Use of this source code is governed by a
|
|
* BSD-style license that can be found in the LICENSE file. *)
|
|
|
|
Require Import Common.
|
|
Require Export CpdtTactics.
|
|
|
|
Import OptionMonad.
|
|
|
|
Ltac extract E x y := set (x := E); assert (y : E = x); [auto|rewrite y in *].
|
|
|
|
Ltac force_expr E H :=
|
|
let v1 := fresh in
|
|
let v2 := fresh in
|
|
extract E v1 v2; destruct v1; [idtac|simpl in H; contradict H; congruence].
|
|
|
|
Lemma bind_some : forall A B x f, @opt_bind A B (Some x) f = f x.
|
|
Proof.
|
|
auto.
|
|
Qed.
|
|
|
|
Lemma simpl_if : forall A (e1 e2 : A), (if true then e1 else e2) = e1.
|
|
auto.
|
|
Qed.
|
|
|
|
(* remember (expression_type CE (NatMap.add v s TE) arg) as EXP. *)
|
|
(* destruct EXP; [rewrite bind_some in H1|simpl in H1; contradict H1; congruence]. *)
|
|
Ltac force_option :=
|
|
match goal with
|
|
| [ H : (opt_bind ?y (fun x => ?z)) = Some ?w |- _ ] =>
|
|
force_expr y H; rewrite bind_some in H
|
|
| [ H : (if ?cond then ?x else None) = Some ?w |- _ ] =>
|
|
force_expr cond H; rewrite simpl_if in H
|
|
| [ H : (match ?x with _ => _ end) = Some ?w |- _ ] =>
|
|
force_expr x H
|
|
end.
|
|
|
|
Ltac force_options := repeat force_option.
|
|
|
|
Inductive ltac_no_arg : Set :=
|
|
| Ltac_No_Arg : ltac_no_arg.
|
|
|
|
Ltac extract_head_2 term H varid eqid :=
|
|
match type of H with
|
|
| context[term ?X] => extract_head_2 (term X) H varid eqid
|
|
| context[term] => remember term as varid eqn:eqid
|
|
end.
|
|
|
|
Ltac extract_head_1 term H varid := let eqid := fresh varid "Eq" in extract_head_2 term H varid eqid.
|
|
Ltac extract_head_0 term H := let varid := fresh H in extract_head_1 term H varid.
|
|
|
|
Ltac extract_head_goal_2 term varid eqid :=
|
|
match goal with
|
|
| [ |- context[term ?X] ] => extract_head_goal_2 (term X) varid eqid
|
|
| [ |- context[term] ] => remember term as varid eqn:eqid
|
|
end.
|
|
|
|
Ltac extract_head_goal_1 term varid := let eqid := fresh varid "Eq" in extract_head_goal_2 term varid eqid.
|
|
Ltac extract_head_goal_0 term := let varid := fresh "G" in extract_head_goal_1 term varid.
|
|
|
|
Tactic Notation "extract_head" constr(term) "in" constr(H) := extract_head_0 term H.
|
|
Tactic Notation "extract_head" constr(term) "in" constr(H) "as" ident(name) := extract_head_1 term H name.
|
|
Tactic Notation "extract_head" constr(term) "in" constr(H) "as" ident(name) "," ident(name2) := extract_head_2 term H name name2.
|
|
|
|
Tactic Notation "extract_head" constr(term) := extract_head_goal_0 term.
|
|
Tactic Notation "extract_head" constr(term) "as" ident(name) := extract_head_goal_1 term name.
|
|
Tactic Notation "extract_head" constr(term) "as" ident(name) "," ident(name2) := extract_head_goal_2 term name name2.
|
|
|
|
Ltac continue_with H :=
|
|
match type of H with
|
|
| ?X -> ?Y =>
|
|
let K := fresh H in
|
|
let H' := fresh H in
|
|
assert (X) as K; [idtac|pose proof (H K) as H']
|
|
end.
|