diff options
author | Jason Gross <jgross@mit.edu> | 2017-11-07 14:34:07 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-11-07 14:34:07 -0500 |
commit | 6a9fcb91e1e7ae45ede6626bd60592a7cd53a5b0 (patch) | |
tree | 6f8974aee0bc48229714d80cb19a1af5db3b6393 /src/Specific | |
parent | 3f3f454c314a5c71cba88ee2d8fc5968f85a5b36 (diff) |
Move SideConditionFramework
Diffstat (limited to 'src/Specific')
-rw-r--r-- | src/Specific/Framework/SideConditionFramework.v | 53 |
1 files changed, 0 insertions, 53 deletions
diff --git a/src/Specific/Framework/SideConditionFramework.v b/src/Specific/Framework/SideConditionFramework.v deleted file mode 100644 index 86bd21860..000000000 --- a/src/Specific/Framework/SideConditionFramework.v +++ /dev/null @@ -1,53 +0,0 @@ -Import EqNotations. -Require Import Crypto.Util.Decidable. - -Definition vm_decide_package (P : Prop) := P. -Definition cbv_minus_then_vm_decide_package {T} (ident : T) (P : Prop) := P. -Definition vm_compute_reflexivity_package (P : Prop) := P. -Record evar_package {T} (v : T) := - { val : T; - evar_package_pf : val = v }. -Arguments val {T v} _. -Arguments evar_package_pf {T v} _. -Record evard_package {s d} (v : s) := - { vald : d; - evard_package_pfT : s = d; - evard_package_pf : vald = rew evard_package_pfT in v }. -Arguments vald {s d v} _. -Arguments evard_package_pfT {s d v} _. -Arguments evard_package_pf {s d v} _. -Inductive cast_bias := LHS | RHS. -Definition vm_compute_evar_package_gen {bias : cast_bias} {T} (v : T) := - @evar_package T v. -Notation vm_compute_evar_package_vm_small := (@vm_compute_evar_package_gen LHS). -Notation vm_compute_evar_package_vm_large := (@vm_compute_evar_package_gen RHS). -Notation vm_compute_evar_package := vm_compute_evar_package_vm_small. -Definition vm_cast_evar_package {s} (v : s) d := @evard_package s d v. -Definition cast_evar_package {s} (v : s) d := @evard_package s d v. - -Module Internal. - Ltac autosolve else_tac := - lazymatch goal with - | [ |- vm_decide_package ?P ] => cbv beta delta [vm_decide_package]; vm_decide - | [ |- cbv_minus_then_vm_decide_package ?ident ?P ] => cbv -[ident]; vm_decide - | [ |- vm_compute_reflexivity_package ?P ] => vm_compute; reflexivity - | [ |- vm_compute_evar_package_vm_small ?v ] - => let v' := (eval vm_compute in v) in - (exists v'); abstract vm_cast_no_check (eq_refl v') - | [ |- vm_compute_evar_package_vm_large ?v ] - => let v' := (eval vm_compute in v) in - (exists v'); abstract vm_cast_no_check (eq_refl v) - | [ |- vm_cast_evar_package ?v ?d ] - => simple refine {| vald := (v <: d) |}; - [ vm_compute; reflexivity - | let lhs := lazymatch goal with |- ?lhs = _ => lhs end in - abstract exact_no_check (eq_refl lhs) ] - | [ |- cast_evar_package (s:=?s) ?v ?d ] - => exact (@Build_evard_package - s d v - v eq_refl eq_refl) - | _ => else_tac () - end. -End Internal. - -Ltac autosolve := Internal.autosolve. |