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

Add a demo for recursive record definitions

parent 4bf63199
......@@ -795,6 +795,19 @@ type ('a,'b) recordb =
-- else would need to prefix all fields with the type... *)
(********************************************************************)
(* ** Recursive definitions are supported for heap-allocated records *)
type 'a node = {
mutable data : 'a;
mutable prev : 'a node;
mutable next : 'a node;
}
let create_cyclic_node (data: 'a): 'a node =
let rec node = { data; prev = node; next = node } in
node
(********************************************************************)
(* ** Type mutual *)
......
......@@ -1353,6 +1353,15 @@ Qed.
Definition Sitems A (L:list A) r :=
Hexists n, r ~> `{ nb' := n; items' := L } \* \[ n = LibListZ.length L ].
(********************************************************************)
(* ** Recursive records definitions *)
Lemma create_cyclic_node_spec : forall (A:Type) (data:A),
app create_cyclic_node [data]
PRE \[]
POST (fun (r: loc) => r ~> `{ data' := data; prev' := r; next' := r }).
Proof using. xcf_go~. Qed.
(*
Section ProjLemma.
Variables (B:Type) (A1 : Type).
......
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