Commit 51d922ae authored by Armaël Guéneau's avatar Armaël Guéneau

Use [field] instead of its definition [nat] in type annotations

parent cfcd372f
......@@ -407,9 +407,9 @@ Global Opaque app_def curried.
is an association list from fields (natural numbers) to
dependent pairs (a value accompanied with its type). *)
Definition record_descr := list (nat * dynamic).
Definition record_descr := list (field * dynamic).
Definition record_repr_one (f:nat) A (v:A) (r:loc) : hprop :=
Definition record_repr_one (f:field) A (v:A) (r:loc) : hprop :=
heap_is_single r f v.
Fixpoint record_repr (L:record_descr) (r:loc) : hprop :=
......@@ -445,7 +445,7 @@ Definition app_record_new (L:record_descr) : ~~loc :=
Axiom record_get : func.
Axiom record_get_spec : forall (r:loc) (f:nat) A (v:A),
Axiom record_get_spec : forall (r:loc) (f:field) A (v:A),
app_keep record_get [r f]
(r ~> record_repr_one f v)
\[= v].
......@@ -454,7 +454,7 @@ Axiom record_get_spec : forall (r:loc) (f:nat) A (v:A),
Axiom record_set : func.
Axiom record_set_spec : forall (r:loc) (f:nat) A B (v:A) (w:B),
Axiom record_set_spec : forall (r:loc) (f:field) A B (v:A) (w:B),
app record_set [r f w]
(r ~> record_repr_one f v)
(# r ~> record_repr_one f w).
......@@ -562,7 +562,7 @@ Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f
(********************************************************************)
(* ** Computated derived specifications for [get] and [set] on records *)
Fixpoint record_get_compute_dyn (f:nat) (L:record_descr) : option dynamic :=
Fixpoint record_get_compute_dyn (f:field) (L:record_descr) : option dynamic :=
match L with
| nil => None
| (f',d')::T' =>
......@@ -571,7 +571,7 @@ Fixpoint record_get_compute_dyn (f:nat) (L:record_descr) : option dynamic :=
else record_get_compute_dyn f T'
end.
Definition record_get_compute_spec (f:nat) (L:record_descr) : option Prop :=
Definition record_get_compute_spec (f:field) (L:record_descr) : option Prop :=
match record_get_compute_dyn f L with
| None => None
| Some (dyn v) => Some (forall r,
......@@ -602,7 +602,7 @@ Proof using.
Qed. (* todo: could use xapply in this proof *)
Fixpoint record_set_compute_dyn (f:nat) (d:dynamic) (L:record_descr) : option record_descr :=
Fixpoint record_set_compute_dyn (f:field) (d:dynamic) (L:record_descr) : option record_descr :=
match L with
| nil => None
| (f',d')::T' =>
......@@ -614,7 +614,7 @@ Fixpoint record_set_compute_dyn (f:nat) (d:dynamic) (L:record_descr) : option re
end
end.
Definition record_set_compute_spec (f:nat) A (w:A) (L:record_descr) : option Prop :=
Definition record_set_compute_spec (f:field) A (w:A) (L:record_descr) : option Prop :=
match record_set_compute_dyn f (dyn w) L with
| None => None
| Some L' => Some (forall r,
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment