Commit 3b419e11 authored by Jean-Christophe's avatar Jean-Christophe
Browse files

new program example relabel in progress

parent 959edfa9
module Relabel
use import list.Mem
use import list.Append
type tree 'a =
| Leaf 'a
| Node (tree 'a) (tree 'a)
logic labels (t : tree 'a) : list 'a = match t with
| Leaf x -> Cons x Nil
| Node l r -> labels l ++ labels r
end
lemma labels_Leaf :
forall x y : 'a. mem x (labels (Leaf y)) <-> x=y
lemma labels_Node :
forall x : 'a, l r : tree 'a.
mem x (labels (Node l r)) <-> mem x (labels l) or mem x (labels r)
inductive same_shape (t1 : tree 'a) (t2 : tree 'b) =
| same_shape_Leaf :
forall x1 : 'a, x2 : 'b.
same_shape (Leaf x1) (Leaf x2)
| same_shape_Node :
forall l1 r1 : tree 'a, l2 r2 : tree 'b.
same_shape l1 l2 -> same_shape r1 r2 ->
same_shape (Node l1 r1) (Node l2 r2)
inductive distinct (l : list 'a) =
| distinct_zero : distinct (Nil : list 'a)
| distinct_one : forall x:'a. distinct (Cons x Nil)
use import int.Int
use import module stdlib.Ref
parameter r : ref int
let fresh () = {} r := !r + 1; !r { r = old r + 1 and result = r }
let rec relabel (t : tree 'a) : tree int =
{}
match t with
| Leaf _ -> Leaf (fresh ())
| Node l r -> Node (relabel l) (relabel r)
end
{ (* same_shape t result and distinct (labels result) and *)
(forall x:int. mem x (labels result) -> old r < x <= r) }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/relabel.gui"
End:
*)
module P module P
use import int.Int use import int.Int
use import module stdlib.Ref
type t 'a = { a : int; mutable b : int; } parameter r : ref int
parameter fresh : unit -> {} unit writes r { r = old r + 1 }
let rec f () =
{}
if any bool then
fresh ()
else begin
f (); f ()
end
{ r > old r }
end end
......
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