Commit 94f15fa7 authored by Michael Sammler's avatar Michael Sammler
Browse files

add generated postfix to rules

parent 7e5afceb
Pipeline #43921 failed with stage
in 17 minutes and 7 seconds
......@@ -70,18 +70,18 @@ Section spec.
{| rmovable 'r := movable_eq _ _ (btree_t_unfold r) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance btree_t_simplify_hyp_place_inst l_ β_ (r : btree_rfmt) :
Global Instance btree_t_simplify_hyp_place_inst_generated l_ β_ (r : btree_rfmt) :
SimplifyHypPlace l_ β_ (r @ btree_t)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (btree_t_unfold _)).
Global Instance btree_t_simplify_goal_place_inst l_ β_ (r : btree_rfmt) :
Global Instance btree_t_simplify_goal_place_inst_generated l_ β_ (r : btree_rfmt) :
SimplifyGoalPlace l_ β_ (r @ btree_t)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (btree_t_unfold _)).
Global Program Instance btree_t_simplify_hyp_val_inst v_ (r : btree_rfmt) :
Global Program Instance btree_t_simplify_hyp_val_inst_generated v_ (r : btree_rfmt) :
SimplifyHypVal v_ (r @ btree_t)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (btree_t_unfold _) T _).
Next Obligation. done. Qed.
Global Program Instance btree_t_simplify_goal_val_inst v_ (r : btree_rfmt) :
Global Program Instance btree_t_simplify_goal_val_inst_generated v_ (r : btree_rfmt) :
SimplifyGoalVal v_ (r @ btree_t)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (btree_t_unfold _) T _).
Next Obligation. done. Qed.
......
......@@ -53,18 +53,18 @@ Section spec.
{| rmovable 'f := movable_eq _ _ (flags_unfold f) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance flags_simplify_hyp_place_inst l_ β_ (f : Flags) :
Global Instance flags_simplify_hyp_place_inst_generated l_ β_ (f : Flags) :
SimplifyHypPlace l_ β_ (f @ flags)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (flags_unfold _)).
Global Instance flags_simplify_goal_place_inst l_ β_ (f : Flags) :
Global Instance flags_simplify_goal_place_inst_generated l_ β_ (f : Flags) :
SimplifyGoalPlace l_ β_ (f @ flags)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (flags_unfold _)).
Global Program Instance flags_simplify_hyp_val_inst v_ (f : Flags) :
Global Program Instance flags_simplify_hyp_val_inst_generated v_ (f : Flags) :
SimplifyHypVal v_ (f @ flags)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (flags_unfold _) T _).
Next Obligation. done. Qed.
Global Program Instance flags_simplify_goal_val_inst v_ (f : Flags) :
Global Program Instance flags_simplify_goal_val_inst_generated v_ (f : Flags) :
SimplifyGoalVal v_ (f @ flags)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (flags_unfold _) T _).
Next Obligation. done. Qed.
......
......@@ -72,18 +72,18 @@ Section spec.
{| rmovable '(n1, n2, n3) := movable_eq _ _ (lock_test_unfold n1 n2 n3) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance lock_test_simplify_hyp_place_inst l_ β_ (n1 : Z) (n2 : Z) (n3 : Z) :
Global Instance lock_test_simplify_hyp_place_inst_generated l_ β_ (n1 : Z) (n2 : Z) (n3 : Z) :
SimplifyHypPlace l_ β_ ((n1, n2, n3) @ lock_test)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (lock_test_unfold _ _ _)).
Global Instance lock_test_simplify_goal_place_inst l_ β_ (n1 : Z) (n2 : Z) (n3 : Z) :
Global Instance lock_test_simplify_goal_place_inst_generated l_ β_ (n1 : Z) (n2 : Z) (n3 : Z) :
SimplifyGoalPlace l_ β_ ((n1, n2, n3) @ lock_test)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (lock_test_unfold _ _ _)).
Global Program Instance lock_test_simplify_hyp_val_inst v_ (n1 : Z) (n2 : Z) (n3 : Z) :
Global Program Instance lock_test_simplify_hyp_val_inst_generated v_ (n1 : Z) (n2 : Z) (n3 : Z) :
SimplifyHypVal v_ ((n1, n2, n3) @ lock_test)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (lock_test_unfold _ _ _) T _).
Next Obligation. done. Qed.
Global Program Instance lock_test_simplify_goal_val_inst v_ (n1 : Z) (n2 : Z) (n3 : Z) :
Global Program Instance lock_test_simplify_goal_val_inst_generated v_ (n1 : Z) (n2 : Z) (n3 : Z) :
SimplifyGoalVal v_ ((n1, n2, n3) @ lock_test)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (lock_test_unfold _ _ _) T _).
Next Obligation. done. Qed.
......
......@@ -41,18 +41,18 @@ Section spec.
{| rmovable 'len := movable_eq _ _ (freelist_t_unfold entry_size len) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance freelist_t_simplify_hyp_place_inst l_ β_ (entry_size : nat) (len : nat) :
Global Instance freelist_t_simplify_hyp_place_inst_generated l_ β_ (entry_size : nat) (len : nat) :
SimplifyHypPlace l_ β_ (len @ freelist_t entry_size)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (freelist_t_unfold _ _)).
Global Instance freelist_t_simplify_goal_place_inst l_ β_ (entry_size : nat) (len : nat) :
Global Instance freelist_t_simplify_goal_place_inst_generated l_ β_ (entry_size : nat) (len : nat) :
SimplifyGoalPlace l_ β_ (len @ freelist_t entry_size)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (freelist_t_unfold _ _)).
Global Program Instance freelist_t_simplify_hyp_val_inst v_ (entry_size : nat) (len : nat) :
Global Program Instance freelist_t_simplify_hyp_val_inst_generated v_ (entry_size : nat) (len : nat) :
SimplifyHypVal v_ (len @ freelist_t entry_size)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (freelist_t_unfold _ _) T _).
Next Obligation. done. Qed.
Global Program Instance freelist_t_simplify_goal_val_inst v_ (entry_size : nat) (len : nat) :
Global Program Instance freelist_t_simplify_goal_val_inst_generated v_ (entry_size : nat) (len : nat) :
SimplifyGoalVal v_ (len @ freelist_t entry_size)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (freelist_t_unfold _ _) T _).
Next Obligation. done. Qed.
......@@ -106,18 +106,18 @@ Section spec.
{| rmovable 'len := movable_eq _ _ (slab_unfold entry_size len) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance slab_simplify_hyp_place_inst l_ β_ (entry_size : nat) (len : nat) :
Global Instance slab_simplify_hyp_place_inst_generated l_ β_ (entry_size : nat) (len : nat) :
SimplifyHypPlace l_ β_ (len @ slab entry_size)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (slab_unfold _ _)).
Global Instance slab_simplify_goal_place_inst l_ β_ (entry_size : nat) (len : nat) :
Global Instance slab_simplify_goal_place_inst_generated l_ β_ (entry_size : nat) (len : nat) :
SimplifyGoalPlace l_ β_ (len @ slab entry_size)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (slab_unfold _ _)).
Global Program Instance slab_simplify_hyp_val_inst v_ (entry_size : nat) (len : nat) :
Global Program Instance slab_simplify_hyp_val_inst_generated v_ (entry_size : nat) (len : nat) :
SimplifyHypVal v_ (len @ slab entry_size)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (slab_unfold _ _) T _).
Next Obligation. done. Qed.
Global Program Instance slab_simplify_goal_val_inst v_ (entry_size : nat) (len : nat) :
Global Program Instance slab_simplify_goal_val_inst_generated v_ (entry_size : nat) (len : nat) :
SimplifyGoalVal v_ (len @ slab entry_size)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (slab_unfold _ _) T _).
Next Obligation. done. Qed.
......
......@@ -59,18 +59,18 @@ Section spec.
{| rmovable 'len := movable_eq _ _ (mpool_chunk_t_unfold entry_size len) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance mpool_chunk_t_simplify_hyp_place_inst l_ β_ (entry_size : nat) (len : nat) :
Global Instance mpool_chunk_t_simplify_hyp_place_inst_generated l_ β_ (entry_size : nat) (len : nat) :
SimplifyHypPlace l_ β_ (len @ mpool_chunk_t entry_size)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (mpool_chunk_t_unfold _ _)).
Global Instance mpool_chunk_t_simplify_goal_place_inst l_ β_ (entry_size : nat) (len : nat) :
Global Instance mpool_chunk_t_simplify_goal_place_inst_generated l_ β_ (entry_size : nat) (len : nat) :
SimplifyGoalPlace l_ β_ (len @ mpool_chunk_t entry_size)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (mpool_chunk_t_unfold _ _)).
Global Program Instance mpool_chunk_t_simplify_hyp_val_inst v_ (entry_size : nat) (len : nat) :
Global Program Instance mpool_chunk_t_simplify_hyp_val_inst_generated v_ (entry_size : nat) (len : nat) :
SimplifyHypVal v_ (len @ mpool_chunk_t entry_size)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (mpool_chunk_t_unfold _ _) T _).
Next Obligation. done. Qed.
Global Program Instance mpool_chunk_t_simplify_goal_val_inst v_ (entry_size : nat) (len : nat) :
Global Program Instance mpool_chunk_t_simplify_goal_val_inst_generated v_ (entry_size : nat) (len : nat) :
SimplifyGoalVal v_ (len @ mpool_chunk_t entry_size)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (mpool_chunk_t_unfold _ _) T _).
Next Obligation. done. Qed.
......@@ -110,18 +110,18 @@ Section spec.
{| rmovable 'len := movable_eq _ _ (mpool_entry_t_unfold entry_size len) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance mpool_entry_t_simplify_hyp_place_inst l_ β_ (entry_size : nat) (len : nat) :
Global Instance mpool_entry_t_simplify_hyp_place_inst_generated l_ β_ (entry_size : nat) (len : nat) :
SimplifyHypPlace l_ β_ (len @ mpool_entry_t entry_size)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (mpool_entry_t_unfold _ _)).
Global Instance mpool_entry_t_simplify_goal_place_inst l_ β_ (entry_size : nat) (len : nat) :
Global Instance mpool_entry_t_simplify_goal_place_inst_generated l_ β_ (entry_size : nat) (len : nat) :
SimplifyGoalPlace l_ β_ (len @ mpool_entry_t entry_size)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (mpool_entry_t_unfold _ _)).
Global Program Instance mpool_entry_t_simplify_hyp_val_inst v_ (entry_size : nat) (len : nat) :
Global Program Instance mpool_entry_t_simplify_hyp_val_inst_generated v_ (entry_size : nat) (len : nat) :
SimplifyHypVal v_ (len @ mpool_entry_t entry_size)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (mpool_entry_t_unfold _ _) T _).
Next Obligation. done. Qed.
Global Program Instance mpool_entry_t_simplify_goal_val_inst v_ (entry_size : nat) (len : nat) :
Global Program Instance mpool_entry_t_simplify_goal_val_inst_generated v_ (entry_size : nat) (len : nat) :
SimplifyGoalVal v_ (len @ mpool_entry_t entry_size)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (mpool_entry_t_unfold _ _) T _).
Next Obligation. done. Qed.
......@@ -195,18 +195,18 @@ Section spec.
{| rmovable 'entries := movable_eq _ _ (mpool_unfold entry_size entries) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance mpool_simplify_hyp_place_inst l_ β_ (entry_size : nat) (entries : nat) :
Global Instance mpool_simplify_hyp_place_inst_generated l_ β_ (entry_size : nat) (entries : nat) :
SimplifyHypPlace l_ β_ (entries @ mpool entry_size)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (mpool_unfold _ _)).
Global Instance mpool_simplify_goal_place_inst l_ β_ (entry_size : nat) (entries : nat) :
Global Instance mpool_simplify_goal_place_inst_generated l_ β_ (entry_size : nat) (entries : nat) :
SimplifyGoalPlace l_ β_ (entries @ mpool entry_size)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (mpool_unfold _ _)).
Global Program Instance mpool_simplify_hyp_val_inst v_ (entry_size : nat) (entries : nat) :
Global Program Instance mpool_simplify_hyp_val_inst_generated v_ (entry_size : nat) (entries : nat) :
SimplifyHypVal v_ (entries @ mpool entry_size)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (mpool_unfold _ _) T _).
Next Obligation. done. Qed.
Global Program Instance mpool_simplify_goal_val_inst v_ (entry_size : nat) (entries : nat) :
Global Program Instance mpool_simplify_goal_val_inst_generated v_ (entry_size : nat) (entries : nat) :
SimplifyGoalVal v_ (entries @ mpool entry_size)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (mpool_unfold _ _) T _).
Next Obligation. done. Qed.
......
......@@ -39,18 +39,18 @@ Section spec.
{| rmovable 'n := movable_eq _ _ (mpool_entry_unfold n) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance mpool_entry_simplify_hyp_place_inst l_ β_ (n : nat) :
Global Instance mpool_entry_simplify_hyp_place_inst_generated l_ β_ (n : nat) :
SimplifyHypPlace l_ β_ (n @ mpool_entry)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (mpool_entry_unfold _)).
Global Instance mpool_entry_simplify_goal_place_inst l_ β_ (n : nat) :
Global Instance mpool_entry_simplify_goal_place_inst_generated l_ β_ (n : nat) :
SimplifyGoalPlace l_ β_ (n @ mpool_entry)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (mpool_entry_unfold _)).
Global Program Instance mpool_entry_simplify_hyp_val_inst v_ (n : nat) :
Global Program Instance mpool_entry_simplify_hyp_val_inst_generated v_ (n : nat) :
SimplifyHypVal v_ (n @ mpool_entry)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (mpool_entry_unfold _) T _).
Next Obligation. done. Qed.
Global Program Instance mpool_entry_simplify_goal_val_inst v_ (n : nat) :
Global Program Instance mpool_entry_simplify_goal_val_inst_generated v_ (n : nat) :
SimplifyGoalVal v_ (n @ mpool_entry)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (mpool_entry_unfold _) T _).
Next Obligation. done. Qed.
......@@ -84,18 +84,18 @@ Section spec.
{| rmovable 'n := movable_eq _ _ (mpool_unfold n) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance mpool_simplify_hyp_place_inst l_ β_ (n : nat) :
Global Instance mpool_simplify_hyp_place_inst_generated l_ β_ (n : nat) :
SimplifyHypPlace l_ β_ (n @ mpool)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (mpool_unfold _)).
Global Instance mpool_simplify_goal_place_inst l_ β_ (n : nat) :
Global Instance mpool_simplify_goal_place_inst_generated l_ β_ (n : nat) :
SimplifyGoalPlace l_ β_ (n @ mpool)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (mpool_unfold _)).
Global Program Instance mpool_simplify_hyp_val_inst v_ (n : nat) :
Global Program Instance mpool_simplify_hyp_val_inst_generated v_ (n : nat) :
SimplifyHypVal v_ (n @ mpool)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (mpool_unfold _) T _).
Next Obligation. done. Qed.
Global Program Instance mpool_simplify_goal_val_inst v_ (n : nat) :
Global Program Instance mpool_simplify_goal_val_inst_generated v_ (n : nat) :
SimplifyGoalVal v_ (n @ mpool)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (mpool_unfold _) T _).
Next Obligation. done. Qed.
......
......@@ -109,18 +109,18 @@ Section spec.
{| rmovable '(mp, items, count) := movable_eq _ _ (fixed_size_map_unfold mp items count) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance fixed_size_map_simplify_hyp_place_inst l_ β_ (mp : gmap Z type) (items : list item_ref) (count : nat) :
Global Instance fixed_size_map_simplify_hyp_place_inst_generated l_ β_ (mp : gmap Z type) (items : list item_ref) (count : nat) :
SimplifyHypPlace l_ β_ ((mp, items, count) @ fixed_size_map)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (fixed_size_map_unfold _ _ _)).
Global Instance fixed_size_map_simplify_goal_place_inst l_ β_ (mp : gmap Z type) (items : list item_ref) (count : nat) :
Global Instance fixed_size_map_simplify_goal_place_inst_generated l_ β_ (mp : gmap Z type) (items : list item_ref) (count : nat) :
SimplifyGoalPlace l_ β_ ((mp, items, count) @ fixed_size_map)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (fixed_size_map_unfold _ _ _)).
Global Program Instance fixed_size_map_simplify_hyp_val_inst v_ (mp : gmap Z type) (items : list item_ref) (count : nat) :
Global Program Instance fixed_size_map_simplify_hyp_val_inst_generated v_ (mp : gmap Z type) (items : list item_ref) (count : nat) :
SimplifyHypVal v_ ((mp, items, count) @ fixed_size_map)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (fixed_size_map_unfold _ _ _) T _).
Next Obligation. done. Qed.
Global Program Instance fixed_size_map_simplify_goal_val_inst v_ (mp : gmap Z type) (items : list item_ref) (count : nat) :
Global Program Instance fixed_size_map_simplify_goal_val_inst_generated v_ (mp : gmap Z type) (items : list item_ref) (count : nat) :
SimplifyGoalVal v_ ((mp, items, count) @ fixed_size_map)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (fixed_size_map_unfold _ _ _) T _).
Next Obligation. done. Qed.
......
......@@ -50,18 +50,18 @@ Section spec.
{| rmovable 'a := movable_eq _ _ (mem_t_unfold a) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance mem_t_simplify_hyp_place_inst l_ β_ (a : nat) :
Global Instance mem_t_simplify_hyp_place_inst_generated l_ β_ (a : nat) :
SimplifyHypPlace l_ β_ (a @ mem_t)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (mem_t_unfold _)).
Global Instance mem_t_simplify_goal_place_inst l_ β_ (a : nat) :
Global Instance mem_t_simplify_goal_place_inst_generated l_ β_ (a : nat) :
SimplifyGoalPlace l_ β_ (a @ mem_t)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (mem_t_unfold _)).
Global Program Instance mem_t_simplify_hyp_val_inst v_ (a : nat) :
Global Program Instance mem_t_simplify_hyp_val_inst_generated v_ (a : nat) :
SimplifyHypVal v_ (a @ mem_t)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (mem_t_unfold _) T _).
Next Obligation. done. Qed.
Global Program Instance mem_t_simplify_goal_val_inst v_ (a : nat) :
Global Program Instance mem_t_simplify_goal_val_inst_generated v_ (a : nat) :
SimplifyGoalVal v_ (a @ mem_t)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (mem_t_unfold _) T _).
Next Obligation. done. Qed.
......
......@@ -60,18 +60,18 @@ Section spec.
{| rmovable 's := movable_eq _ _ (chunks_t_unfold s) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance chunks_t_simplify_hyp_place_inst l_ β_ (s : gmultiset nat) :
Global Instance chunks_t_simplify_hyp_place_inst_generated l_ β_ (s : gmultiset nat) :
SimplifyHypPlace l_ β_ (s @ chunks_t)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (chunks_t_unfold _)).
Global Instance chunks_t_simplify_goal_place_inst l_ β_ (s : gmultiset nat) :
Global Instance chunks_t_simplify_goal_place_inst_generated l_ β_ (s : gmultiset nat) :
SimplifyGoalPlace l_ β_ (s @ chunks_t)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (chunks_t_unfold _)).
Global Program Instance chunks_t_simplify_hyp_val_inst v_ (s : gmultiset nat) :
Global Program Instance chunks_t_simplify_hyp_val_inst_generated v_ (s : gmultiset nat) :
SimplifyHypVal v_ (s @ chunks_t)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (chunks_t_unfold _) T _).
Next Obligation. done. Qed.
Global Program Instance chunks_t_simplify_goal_val_inst v_ (s : gmultiset nat) :
Global Program Instance chunks_t_simplify_goal_val_inst_generated v_ (s : gmultiset nat) :
SimplifyGoalVal v_ (s @ chunks_t)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (chunks_t_unfold _) T _).
Next Obligation. done. Qed.
......
......@@ -47,18 +47,18 @@ Section spec.
{| rmovable 'ty := movable_eq _ _ (queue_elem_unfold cont ty) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance queue_elem_simplify_hyp_place_inst l_ β_ (cont : type) (ty : type) :
Global Instance queue_elem_simplify_hyp_place_inst_generated l_ β_ (cont : type) (ty : type) :
SimplifyHypPlace l_ β_ (ty @ queue_elem cont)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (queue_elem_unfold _ _)).
Global Instance queue_elem_simplify_goal_place_inst l_ β_ (cont : type) (ty : type) :
Global Instance queue_elem_simplify_goal_place_inst_generated l_ β_ (cont : type) (ty : type) :
SimplifyGoalPlace l_ β_ (ty @ queue_elem cont)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (queue_elem_unfold _ _)).
Global Program Instance queue_elem_simplify_hyp_val_inst v_ (cont : type) (ty : type) :
Global Program Instance queue_elem_simplify_hyp_val_inst_generated v_ (cont : type) (ty : type) :
SimplifyHypVal v_ (ty @ queue_elem cont)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (queue_elem_unfold _ _) T _).
Next Obligation. done. Qed.
Global Program Instance queue_elem_simplify_goal_val_inst v_ (cont : type) (ty : type) :
Global Program Instance queue_elem_simplify_goal_val_inst_generated v_ (cont : type) (ty : type) :
SimplifyGoalVal v_ (ty @ queue_elem cont)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (queue_elem_unfold _ _) T _).
Next Obligation. done. Qed.
......@@ -98,18 +98,18 @@ Section spec.
{| rmovable 'tys := movable_eq _ _ (queue_unfold tys) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance queue_simplify_hyp_place_inst l_ β_ (tys : list type) :
Global Instance queue_simplify_hyp_place_inst_generated l_ β_ (tys : list type) :
SimplifyHypPlace l_ β_ (tys @ queue)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (queue_unfold _)).
Global Instance queue_simplify_goal_place_inst l_ β_ (tys : list type) :
Global Instance queue_simplify_goal_place_inst_generated l_ β_ (tys : list type) :
SimplifyGoalPlace l_ β_ (tys @ queue)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (queue_unfold _)).
Global Program Instance queue_simplify_hyp_val_inst v_ (tys : list type) :
Global Program Instance queue_simplify_hyp_val_inst_generated v_ (tys : list type) :
SimplifyHypVal v_ (tys @ queue)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (queue_unfold _) T _).
Next Obligation. done. Qed.
Global Program Instance queue_simplify_goal_val_inst v_ (tys : list type) :
Global Program Instance queue_simplify_goal_val_inst_generated v_ (tys : list type) :
SimplifyGoalVal v_ (tys @ queue)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (queue_unfold _) T _).
Next Obligation. done. Qed.
......
......@@ -49,18 +49,18 @@ Section spec.
{| rmovable 'l := movable_eq _ _ (list_t_unfold l) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance list_t_simplify_hyp_place_inst l_ β_ (l : list type) :
Global Instance list_t_simplify_hyp_place_inst_generated l_ β_ (l : list type) :
SimplifyHypPlace l_ β_ (l @ list_t)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (list_t_unfold _)).
Global Instance list_t_simplify_goal_place_inst l_ β_ (l : list type) :
Global Instance list_t_simplify_goal_place_inst_generated l_ β_ (l : list type) :
SimplifyGoalPlace l_ β_ (l @ list_t)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (list_t_unfold _)).
Global Program Instance list_t_simplify_hyp_val_inst v_ (l : list type) :
Global Program Instance list_t_simplify_hyp_val_inst_generated v_ (l : list type) :
SimplifyHypVal v_ (l @ list_t)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (list_t_unfold _) T _).
Next Obligation. done. Qed.
Global Program Instance list_t_simplify_goal_val_inst v_ (l : list type) :
Global Program Instance list_t_simplify_goal_val_inst_generated v_ (l : list type) :
SimplifyGoalVal v_ (l @ list_t)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (list_t_unfold _) T _).
Next Obligation. done. Qed.
......
......@@ -826,7 +826,7 @@ let pp_spec : string -> import list -> string list -> typedef list ->
(* Generation of the global instances. *)
let pp_instance_place inst_name type_name =
pp "@;Global Instance %s_%s_inst l_ β_ %a%a:@;" id inst_name
pp "@;Global Instance %s_%s_inst_generated l_ β_ %a%a:@;" id inst_name
pp_params params pp_params annot.st_refined_by;
pp " %s l_ β_ (%a @@ %a)%%I (Some 100%%N) :=@;" type_name
(pp_as_tuple pp_str) ref_names (pp_id_args false id) par_names;
......@@ -835,7 +835,7 @@ let pp_spec : string -> import list -> string list -> typedef list ->
List.iter (fun _ -> pp " _") ref_names; pp "))."
in
let pp_instance_val inst_name type_name =
pp "@;Global Program Instance %s_%s_inst v_ %a%a:@;" id inst_name
pp "@;Global Program Instance %s_%s_inst_generated v_ %a%a:@;" id inst_name
pp_params params pp_params annot.st_refined_by;
pp " %s v_ (%a @@ %a)%%I (Some 100%%N) :=@;" type_name
(pp_as_tuple pp_str) ref_names (pp_id_args false id) par_names;
......
......@@ -49,18 +49,18 @@ Section spec.
{| rmovable 'xs := movable_eq _ _ (list_t_unfold xs) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance list_t_simplify_hyp_place_inst l_ β_ (xs : list Z) :
Global Instance list_t_simplify_hyp_place_inst_generated l_ β_ (xs : list Z) :
SimplifyHypPlace l_ β_ (xs @ list_t)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (list_t_unfold _)).
Global Instance list_t_simplify_goal_place_inst l_ β_ (xs : list Z) :
Global Instance list_t_simplify_goal_place_inst_generated l_ β_ (xs : list Z) :
SimplifyGoalPlace l_ β_ (xs @ list_t)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (list_t_unfold _)).
Global Program Instance list_t_simplify_hyp_val_inst v_ (xs : list Z) :
Global Program Instance list_t_simplify_hyp_val_inst_generated v_ (xs : list Z) :
SimplifyHypVal v_ (xs @ list_t)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (list_t_unfold _) T _).
Next Obligation. done. Qed.
Global Program Instance list_t_simplify_goal_val_inst v_ (xs : list Z) :
Global Program Instance list_t_simplify_goal_val_inst_generated v_ (xs : list Z) :
SimplifyGoalVal v_ (xs @ list_t)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (list_t_unfold _) T _).
Next Obligation. done. Qed.
......
......@@ -53,18 +53,18 @@ Section spec.
{| rmovable 'l := movable_eq _ _ (list_t_unfold l) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance list_t_simplify_hyp_place_inst l_ β_ (l : list type) :
Global Instance list_t_simplify_hyp_place_inst_generated l_ β_ (l : list type) :
SimplifyHypPlace l_ β_ (l @ list_t)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (list_t_unfold _)).
Global Instance list_t_simplify_goal_place_inst l_ β_ (l : list type) :
Global Instance list_t_simplify_goal_place_inst_generated l_ β_ (l : list type) :
SimplifyGoalPlace l_ β_ (l @ list_t)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (list_t_unfold _)).
Global Program Instance list_t_simplify_hyp_val_inst v_ (l : list type) :
Global Program Instance list_t_simplify_hyp_val_inst_generated v_ (l : list type) :
SimplifyHypVal v_ (l @ list_t)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (list_t_unfold _) T _).
Next Obligation. done. Qed.
Global Program Instance list_t_simplify_goal_val_inst v_ (l : list type) :
Global Program Instance list_t_simplify_goal_val_inst_generated v_ (l : list type) :
SimplifyGoalVal v_ (l @ list_t)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (list_t_unfold _) T _).
Next Obligation. done. Qed.
......
......@@ -59,18 +59,18 @@ Section spec.
{| rmovable 'sizes := movable_eq _ _ (alloc_entry_t_unfold sizes) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance alloc_entry_t_simplify_hyp_place_inst l_ β_ (sizes : list nat) :
Global Instance alloc_entry_t_simplify_hyp_place_inst_generated l_ β_ (sizes : list nat) :
SimplifyHypPlace l_ β_ (sizes @ alloc_entry_t)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (alloc_entry_t_unfold _)).
Global Instance alloc_entry_t_simplify_goal_place_inst l_ β_ (sizes : list nat) :
Global Instance alloc_entry_t_simplify_goal_place_inst_generated l_ β_ (sizes : list nat) :
SimplifyGoalPlace l_ β_ (sizes @ alloc_entry_t)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (alloc_entry_t_unfold _)).
Global Program Instance alloc_entry_t_simplify_hyp_val_inst v_ (sizes : list nat) :
Global Program Instance alloc_entry_t_simplify_hyp_val_inst_generated v_ (sizes : list nat) :
SimplifyHypVal v_ (sizes @ alloc_entry_t)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (alloc_entry_t_unfold _) T _).
Next Obligation. done. Qed.
Global Program Instance alloc_entry_t_simplify_goal_val_inst v_ (sizes : list nat) :
Global Program Instance alloc_entry_t_simplify_goal_val_inst_generated v_ (sizes : list nat) :
SimplifyGoalVal v_ (sizes @ alloc_entry_t)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (alloc_entry_t_unfold _) T _).
Next Obligation. done. Qed.
......@@ -108,18 +108,18 @@ Section spec.
{| rmovable 'n := movable_eq _ _ (alloc_state_unfold n) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance alloc_state_simplify_hyp_place_inst l_ β_ (n : unit) :
Global Instance alloc_state_simplify_hyp_place_inst_generated l_ β_ (n : unit) :
SimplifyHypPlace l_ β_ (n @ alloc_state)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (alloc_state_unfold _)).
Global Instance alloc_state_simplify_goal_place_inst l_ β_ (n : unit) :
Global Instance alloc_state_simplify_goal_place_inst_generated l_ β_ (n : unit) :
SimplifyGoalPlace l_ β_ (n @ alloc_state)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (alloc_state_unfold _)).
Global Program Instance alloc_state_simplify_hyp_val_inst v_ (n : unit) :
Global Program Instance alloc_state_simplify_hyp_val_inst_generated v_ (n : unit) :
SimplifyHypVal v_ (n @ alloc_state)%I (Some 100%N) :=