Commit 7de702ec authored by charguer's avatar charguer

newvars_ok

parent e8de79e4
......@@ -24,11 +24,10 @@ Implicit Types n : int.
(* From LambdaStruct
Definition val_incr :=
Vars P, N, M in
ValFun P :=
Let N := val_get P in
Let M := val_add N 1 in
val_set P M.
ValFun 'p :=
Let 'n := val_get 'p in
Let 'm := val_add 'n 1 in
val_set 'p 'm.
*)
(* ---------------------------------------------------------------------- *)
......@@ -182,12 +181,11 @@ Proof using. intros. xapps. hsimpl~. Qed.
(** Swap function *)
Definition val_swap :=
Vars P, Q, X, Y in
ValFun P Q :=
Let X := val_get P in
Let Y := val_get Q in
val_set P Y ;;
val_set Q X.
ValFun 'p 'q :=
Let 'x := val_get 'p in
Let 'y := val_get 'q in
val_set 'p 'y ;;
val_set 'q 'x.
Lemma rule_swap_neq : forall p q v w,
triple (val_swap p q)
......@@ -210,12 +208,11 @@ Qed.
(** Succ function using incr *)
Definition val_succ_using_incr :=
Vars N, P, X in
ValFun N :=
Let P := val_ref N in
val_incr P ;;
Let X := val_get P in
X.
ValFun 'n :=
Let 'p := val_ref 'n in
val_incr 'p ;;
Let 'x := val_get 'p in
'x.
Lemma rule_succ_using_incr : forall n,
triple (val_succ_using_incr n)
......
......@@ -21,8 +21,7 @@ Implicit Types n : int.
(* * Apply function *)
Definition val_apply : val :=
Vars F, X in
ValFun F X := (F X).
ValFun 'f 'x := ('f 'x).
Lemma Rule_apply : forall (f:func) `{EA:Enc A} (x:A),
forall (H:hprop) `{EB:Enc B} (Q:B->hprop),
......@@ -47,11 +46,10 @@ Proof using. intros. xpull ;=> M. applys~ Rule_apply. Qed.
(* * RefApply function *)
Definition val_refapply : val :=
Vars F, R, X, Y in
ValFun F R :=
Let X := val_get R in
Let Y := F X in
val_set R Y.
ValFun 'f 'r :=
Let 'x := val_get 'r in
Let 'y := 'f 'x in
val_set 'r 'y.
Lemma Rule_refapply_pure : forall (f:func) `{EA:Enc A} (r:loc) (x:A),
forall `{EB:Enc B} (P:A->B->Prop),
......@@ -85,10 +83,9 @@ Qed.
(* * Twice function *)
Definition val_twice : val :=
Vars F in
ValFun F :=
F '() ;;
F '().
ValFun 'f :=
'f '() ;;
'f '().
Lemma Rule_twice : forall (f:func) (H H':hprop) `{EB:Enc B} (Q:B->hprop),
Triple (f `tt) H (fun (_:unit) => H') ->
......@@ -103,18 +100,17 @@ Qed.
(* * Repeat function *)
Definition val_repeat : val :=
Vars N, F, I in
ValFun N F :=
For I := 1 To N Do
F '()
ValFun 'n 'f :=
For 'i := 1 To 'n Do
'f '()
Done.
Axiom xfor_inv_lemma : forall (I:int->hprop),
forall (a:int) (b:int) (F:int->Formula) H H',
(a <= b+1) ->
(H ==> I a \* H') ->
(forall i, a <= i <= b -> '(F i) (I i) (fun (_:unit) => I(i+1))) ->
'(Cf_for a b F) H (fun (_:unit) => I (b+1) \* H').
(forall i, a <= i <= b -> ^(F i) (I i) (fun (_:unit) => I(i+1))) ->
^(Cf_for a b F) H (fun (_:unit) => I (b+1) \* H').
......@@ -190,10 +186,9 @@ Qed.
(** Implementation *)
Definition val_mkcounter : val :=
Vars U, V, P, G in
ValFun U :=
Let P := val_ref 0 in
(Fun V := val_incr P ;; val_get P).
ValFun 'u :=
Let 'p := val_ref 0 in
(Fun 'v := val_incr 'p ;; val_get 'p).
(* ---------------------------------------------------------------------- *)
......@@ -215,11 +210,10 @@ Hint Extern 1 (Register_Spec val_mkcounter) => Provide Rule_mkcounter.
(** Demo *)
Definition trm_test_mkcounter : trm :=
Vars C, M, N in
Let C := val_mkcounter '() in
Let N := C '() in
Let M := C '() in
val_add N M.
Let 'c := val_mkcounter '() in
Let 'n := 'c '() in
Let 'm := 'c '() in
val_add 'n 'm.
Lemma rule_test_mkcounter :
Triple trm_test_mkcounter
......
......@@ -203,17 +203,16 @@ End SegProperties.
(* ---------------------------------------------------------------------- *)
(* ** Node allocation *)
Definition val_new_cell := val_new_record 2%nat.
Definition val_new_cell : val := val_new_record 2%nat.
(** Above equivalent to :
Definition val_new_cell :=
Vars X, Y, P in
ValFun X Y :=
Let P := val_alloc 2 in
val_set_item P X;;
val_set_left P Y;;
P.
ValFun 'x 'y :=
Let 'p := val_alloc 2 in
val_set_item 'p 'x;;
val_set_left 'p 'y;;
'p.
*)
Lemma Rule_new_cell : forall `{EA:Enc A} (x:A) (q:loc),
......@@ -224,17 +223,19 @@ Proof using. xrule_new_record. Qed.
Hint Extern 1 (Register_Spec val_new_cell) => Provide Rule_new_cell.
Opaque val_new_cell.
(* ---------------------------------------------------------------------- *)
(* ** List copy *)
Definition val_mlist_copy :=
Vars F, X, P, P1, P1' in
ValFix F P :=
If_ val_eq P null Then null Else (
Let X := val_get_hd P in
Let P1 := val_get_tl P in
Let P1' := F P1 in
val_new_cell X P1'
ValFix 'f 'p :=
If_ val_eq 'p null Then null Else (
Let 'x := val_get_hd 'p in
Let 'p1 := val_get_tl 'p in
Let 'p2 := 'f 'p1 in
val_new_cell 'x 'p2
).
Lemma Rule_mlist_copy : forall p (L:list int),
......@@ -246,10 +247,13 @@ Proof using.
xapps~. xif ;=> C.
{ xval. subst p. rewrite MList_null_eq. hsimpl~. }
{ xchanges~ (MList_not_null_inv_cons p) ;=> x p1 T1 E. subst.
xapps. xapps. xapp~ as p1'. xapp.
xapps. xapps. xapp~ as p1'.
(* TODO URGENT xapp.
(* todo: xapp should look for hyp *)
intros p'. do 2 rewrite MList_cons_eq. hsimpl. }
Qed.
*)
Admitted.
Hint Extern 1 (Register_Spec val_mlist_copy) => Provide Rule_mlist_copy.
......@@ -259,12 +263,11 @@ Hint Extern 1 (Register_Spec val_mlist_copy) => Provide Rule_mlist_copy.
(* * Length of a mutable list *)
Definition val_mlist_length : val :=
Vars F, P, Q, N in
ValFix F P :=
If_ val_neq P null Then (
Let Q := val_get_tl P in
Let N := F Q in
val_add N 1
ValFix 'f 'p :=
If_ val_neq 'p null Then (
Let 'q := val_get_tl 'p in
Let 'n := 'f 'q in
val_add 'n 1
) Else (
0
).
......@@ -288,15 +291,14 @@ Qed.
(* * Out-of-place append of two mutable lists *)
Definition val_mlist_append : val :=
Vars F, P1, P2, X, P1', P' in
ValFix F P1 P2 :=
If_ val_eq P1 null Then (
val_mlist_copy P2
ValFix 'f 'p1 'p2 :=
If_ val_eq 'p1 null Then (
val_mlist_copy 'p2
) Else (
Let X := val_get_hd P1 in
Let P1' := val_get_tl P1 in
Let P' := F P1' P2 in
val_new_cell X P'
Let 'x := val_get_hd 'p1 in
Let 'c1 := val_get_tl 'p1 in
Let 'p := 'f 'c1 'p2 in
val_new_cell 'x 'p
).
Lemma Rule_mlist_append : forall (L1 L2:list int) (p1 p2:loc),
......@@ -350,13 +352,12 @@ Qed.
(* * Iter *)
Definition val_mlist_iter : val :=
Vars G, F, P, Q, X in
ValFix G F P :=
If_ val_neq P null Then
Let X := val_get_hd P in
F X ;;
Let Q := val_get_tl P in
G F Q
ValFix 'g 'f 'p :=
If_ val_neq 'p null Then
Let 'x := val_get_hd 'p in
'f 'x ;;
Let 'q := val_get_tl 'p in
'g 'f 'q
End.
Lemma Rule_mlist_iter : forall `{EA:Enc A} (I:list A->hprop) (L:list A) (f:func) (p:loc),
......@@ -416,12 +417,11 @@ Qed.
(* * Length of a mutable list using iter *)
Definition val_mlist_length_using_iter : val :=
Vars F, R, X, P in
ValFun P :=
Let R := val_ref 0 in
LetFun F X := val_incr R in
val_mlist_iter F P ;;
val_get R.
ValFun 'p :=
Let 'r := val_ref 0 in
LetFun 'f 'x := val_incr 'r in
val_mlist_iter 'f 'p ;;
val_get 'r.
Lemma Rule_mlist_length_using_iter : forall A `{EA:Enc A} (L:list A) (p:loc),
Triple (val_mlist_length_using_iter `p)
......@@ -442,18 +442,17 @@ Qed.
(* * Length of a mutable list using a loop *)
Definition val_mlist_length_loop : val :=
Vars P0, R, P, Q, N in
ValFun P0 :=
Let R := val_ref P0 in
Let N := val_ref 0 in
While (Let P := val_get R in
val_neq P null) Do
val_incr N ;;
Let P := val_get R in
Let Q := val_get_tl P in
val_set R Q
ValFun 'p1 :=
Let 'r := val_ref 'p1 in
Let 'n := val_ref 0 in
While (Let 'p := val_get 'r in
val_neq 'p null) Do
val_incr 'n ;;
Let 'p := val_get 'r in
Let 'q := val_get_tl 'p in
val_set 'r 'q
Done ;;
val_get N.
val_get 'n.
Lemma Rule_mlist_length_loop : forall A `{EA:Enc A} (L:list A) (p:loc),
Triple (val_mlist_length_loop `p)
......@@ -463,7 +462,7 @@ Proof using.
xcf. xapp ;=> r. xapp ;=> n.
{ xwhile as R.
cuts K: (forall (nacc:int),
'R (r ~~> p \* p ~> MList L \* n ~~> nacc)
^R (r ~~> p \* p ~> MList L \* n ~~> nacc)
(fun (_:unit) => p ~> MList L \* n ~~> (nacc + length L))).
{ xapplys* K. }
gen p. induction_wf: list_sub_wf L; intros. applys (rm HR).
......@@ -487,14 +486,13 @@ Qed.
(* * Length of a mutable list *)
Definition val_mlist_incr : val :=
Vars F, P, Q, X, Y in
ValFix F P :=
If_ val_neq P null Then (
Let X := val_get_hd P in
Let Y := val_add X 1 in
val_set_hd P Y;;
Let Q := val_get_tl P in
F Q
ValFix 'f 'p :=
If_ val_neq 'p null Then (
Let 'x := val_get_hd 'p in
Let 'y := val_add 'x 1 in
val_set_hd 'p 'y;;
Let 'q := val_get_tl 'p in
'f 'q
) End.
Lemma Rule_mlist_incr : forall (L:list int) (p:loc),
......@@ -515,20 +513,19 @@ Qed.
(* * In-place list reversal *)
Definition val_mlist_in_place_rev : val :=
Vars P0, RP, P, Q, RS, S in
ValFun P0 :=
Let RP := val_ref P0 in
Let RS := val_ref null in
While (Let P := val_get RP in
val_neq P null) Do
Let P := val_get RP in
Let Q := val_get_tl P in
val_set RP Q ;;
Let S := val_get RS in
val_set_tl P S ;;
val_set RS P
ValFun 'p1 :=
Let 'r := val_ref 'p1 in
Let 's := val_ref null in
While (Let 'p := val_get 'r in
val_neq 'p null) Do
Let 'p := val_get 'r in
Let 'q := val_get_tl 'p in
val_set 'r 'q ;;
Let 't := val_get 's in
val_set_tl 'p 't ;;
val_set 's 'p
Done ;;
val_get RS.
val_get 's.
Lemma Rule_mlist_in_place_rev : forall A `{EA:Enc A} (L:list A) (p:loc),
Triple (val_mlist_in_place_rev `p)
......@@ -561,14 +558,13 @@ Qed.
(* * CPS append *)
Definition val_mlist_cps_append : val :=
Vars F, P, Q, K, K', R, T in
ValFix F P Q K :=
If_ val_eq P null Then (
K Q
ValFix 'f 'p 'q 'k :=
If_ val_eq 'p null Then (
'k 'q
) Else (
LetFun K' R := (val_set_tl P R ;; K P) in
Let T := val_get_tl P in
F T Q K'
LetFun 'k2 'r := (val_set_tl 'p 'r ;; 'k 'p) in
Let 't := val_get_tl 'p in
'f 't 'q 'k2
).
Lemma Rule_mlist_cps_append : forall A `{EA:Enc A} (L M:list A) (p q:loc) (k:func),
......
......@@ -149,12 +149,11 @@ Hint Extern 1 (Register_spec val_set_tl) => Provide rule_set_tl.
(** Allocation of list cells *)
Definition val_new_cell :=
Vars X, Y, P in
ValFun X Y :=
Let P := val_alloc 2 in
val_set_hd P X;;
val_set_tl P Y;;
P.
ValFun 'x 'y :=
Let 'p := val_alloc 2 in
val_set_hd 'p 'x;;
val_set_tl 'p 'y;;
'p.
Lemma rule_alloc_cell :
triple (val_alloc 2)
......@@ -315,12 +314,11 @@ Global Opaque MList.
(** Implementation *)
Definition val_mlist_length : val :=
Vars F, P, Q, N in
ValFix F P :=
If_ val_neq P null Then (
Let Q := val_get_tl P in
Let N := F Q in
val_add N 1
ValFix 'f 'p :=
If_ val_neq 'p null Then (
Let 'q := val_get_tl 'p in
Let 'n := 'f 'q in
val_add 'n 1
) Else (
0
).
......@@ -438,18 +436,17 @@ Qed.
(** Implementation *)
Definition val_mlist_length_loop : val :=
Vars P0, R, P, Q, N in
ValFun P0 :=
Let R := val_ref P0 in
Let N := val_ref 0 in
While (Let P := val_get R in
val_neq P null) Do
val_incr N ;;
Let P := val_get R in
Let Q := val_get_tl P in
val_set R Q
ValFun 'p1 :=
Let 'r := val_ref 'p1 in
Let 'n := val_ref 0 in
While (Let 'p := val_get 'r in
val_neq 'p null) Do
val_incr 'n ;;
Let 'p := val_get 'r in
Let 'q := val_get_tl 'p in
val_set 'r 'q
Done ;;
val_get N.
val_get 'n.
Lemma rule_mlist_length_loop : forall L p,
triple (val_mlist_length_loop p)
......@@ -579,10 +576,9 @@ Definition MQueue (L:list val) (p:loc) :=
MCell pf pb p \* MListSeg pb L pf \* MCell vx vy pb.
Definition val_create :=
Vars R, V in
ValFun V :=
Let R := val_alloc 2 in
val_new_cell R R.
ValFun 'v :=
Let 'r := val_alloc 2 in
val_new_cell 'r 'r.
Lemma rule_create :
triple (val_create val_unit)
......@@ -600,11 +596,10 @@ Qed.
(** Is empty *)
Definition val_is_empty :=
Vars P, X, Y in
ValFun P :=
Let X := val_get_hd P in
Let Y := val_get_tl P in
val_eq X Y.
ValFun 'p :=
Let 'x := val_get_hd 'p in
Let 'y := val_get_tl 'p in
val_eq 'x 'y.
Lemma rule_is_empty : forall p L,
triple (val_is_empty p)
......@@ -625,13 +620,12 @@ Hint Extern 1 (Register_spec val_is_empty) => Provide rule_is_empty.
(** Push back *)
Definition val_push_back :=
Vars V, P, Q, R in
ValFun V P :=
Let Q := val_get_tl P in
Let R := val_alloc 2 in
val_set_hd Q V ;;
val_set_tl Q R ;;
val_set_tl P R.
ValFun 'v 'p :=
Let 'q := val_get_tl 'p in
Let 'r := val_alloc 2 in
val_set_hd 'q 'v ;;
val_set_tl 'q 'r ;;
val_set_tl 'p 'r.
Lemma rule_push_back : forall v p L,
triple (val_push_back v p)
......@@ -648,11 +642,10 @@ Qed.
(** Push front *)
Definition val_push_front :=
Vars V, P, Q, R in
ValFun V P :=
Let Q := val_get_hd P in
Let R := val_new_cell V Q in
val_set_hd P R.
ValFun 'v 'p :=
Let 'q := val_get_hd 'p in
Let 'r := val_new_cell 'v 'q in
val_set_hd 'p 'r.
Lemma rule_push_front : forall v p L,
triple (val_push_front v p)
......@@ -669,13 +662,12 @@ Qed.
(** Pop front *)
Definition val_pop_front :=
Vars V, P, Q, R, X in
ValFun V P :=
Let Q := val_get_hd P in
Let X := val_get_hd Q in
Let R := val_get_tl Q in
val_set_hd P R;;
X.
ValFun 'v 'p :=
Let 'q := val_get_hd 'p in
Let 'x := val_get_hd 'q in
Let 'r := val_get_tl 'q in
val_set_hd 'p 'r;;
'x.
Lemma rule_pop_front : forall v p L,
L <> nil ->
......@@ -694,21 +686,18 @@ Qed.
(** Transfer *)
Definition val_transfer :=
Vars P1, F1, B1, X1, N1 in
Vars P2, F2, B2, X2, N2 from 5%nat in
Vars E2 from 10%nat in
ValFun P1 P2 :=
Let E2 := val_is_empty P2 in
If_ val_not E2 Then
Let B1 := val_get_tl P1 in
Let F2 := val_get_hd P2 in
Let X2 := val_get_hd F2 in
Let N2 := val_get_tl F2 in
Let B2 := val_get_tl P2 in
val_set_tl P1 B2 ;;
val_set_hd B1 X2 ;;
val_set_tl B1 N2 ;;
val_set_tl P2 F2
ValFun 'p1 'p2 :=
Let 'e2 := val_is_empty 'p2 in
If_ val_not 'e2 Then
Let 'b1 := val_get_tl 'p1 in
Let 'f2 := val_get_hd 'p2 in
Let 'x2 := val_get_hd 'f2 in
Let 'n2 := val_get_tl 'f2 in
Let 'b2 := val_get_tl 'p2 in
val_set_tl 'p1 'b2 ;;
val_set_hd 'b1 'x2 ;;
val_set_tl 'b1 'n2 ;;
val_set_tl 'p2 'f2
End.
Lemma rule_transfer : forall p1 p2 L1 L2,
......
......@@ -179,13 +179,12 @@ Definition val_new_node := val_new_record 3%nat.
(** Above equivalent to :
Definition val_new_node :=
Vars X, Y, Z, P in
ValFun X Y Z :=
Let P := val_alloc 3 in
val_set_item P X;;
val_set_left P Y;;
val_set_right P Z;;
P.
ValFun 'x 'y 'z :=
Let 'p := val_alloc 3 in
val_set_item 'p 'x;;
val_set_left 'p 'y;;
val_set_right 'p 'z;;
'p.
*)
Lemma Rule_new_node : forall x p1 p2,
......@@ -201,15 +200,14 @@ Hint Extern 1 (Register_Spec val_new_node) => Provide Rule_new_node.
(* ** Tree copy *)
Definition val_tree_copy :=
Vars F, X, P1, P2, Q1, Q2, P in
ValFix F P :=
If_ val_eq P null Then null Else (
Let X := val_get_item P in
Let P1 := val_get_left P in
Let P2 := val_get_right P in
Let Q1 := F P1 in
Let Q2 := F P2 in
val_new_node X Q1 Q2
ValFix 'f 'p :=
If_ val_eq 'p null Then null Else (
Let 'x := val_get_item 'p in
Let 'p1 := val_get_left 'p in
Let 'p2 := val_get_right 'p in
Let 'q1 := 'f 'p1 in
Let 'q2 := 'f 'p2 in
val_new_node 'x 'q1 'q2
).
Hint Constructors tree_sub.
......@@ -223,10 +221,15 @@ Proof using.
xapps~. xif ;=> C.
{ xval. subst p. rewrite MTree_null_eq. hsimpl~. }
{ xchanges~ (MTree_not_null_inv_node p) ;=> x p1 p2 T1 T2 E. subst.
xapps. xapps. xapps. xapp~ IH as p1'. xapp~ IH as p2'. xapp.
xapps. xapps. xapps. xapp~ IH as p1'. xapp~ IH as p2'.
(* TODO URGENT: requires fixing records
xapp.
(* todo: xapp should look for hyp *)
intros p'. do 2 rewrite MTree_node_eq. hsimpl. }
Qed.
*)