 ### Change the ;; notation for Seq and use ;;;, so that it stays compatible with...

`Change the ;; notation for Seq and use ;;;, so that it stays compatible with stdpp/iris. This is temporary, until we find a better solution.`
parent e241b995
 ... ... @@ -187,7 +187,7 @@ Definition val_swap := ValFun 'p 'q := Let 'x := val_get 'p in Let 'y := val_get 'q in val_set 'p 'y ;; val_set 'p 'y ;;; val_set 'q 'x. Lemma rule_swap_neq : forall p q v w, ... ... @@ -213,7 +213,7 @@ Qed. Definition val_succ_using_incr := ValFun 'n := Let 'p := val_ref 'n in val_incr 'p ;; val_incr 'p ;;; Let 'x := val_get 'p in 'x. ... ... @@ -239,7 +239,7 @@ Qed. Definition val_incr_twice := ValFun 'p := val_incr 'p ;; val_incr 'p ;;; val_incr 'p. Lemma rule_incr_twice : forall p n, ... ... @@ -288,7 +288,7 @@ Definition val_example_one_ref := ValFun 'n := Let 'k := 'n '+ 1 in Let 'i := 'ref 'k in val_incr 'i ;; val_incr 'i ;;; '!'i. Lemma rule_example_one_ref : forall n, ... ... @@ -322,12 +322,12 @@ Definition val_example_two_ref := ValFun 'n := Let 'i := 'ref 0 in Let 'r := 'ref 'n in val_decr 'r ;; val_incr 'i ;; val_decr 'r ;;; val_incr 'i ;;; Let 'i1 := '!'i in Let 'r1 := '!'r in Let 's := 'i1 '+ 'r1 in 'r ':= 's ;; 'r ':= 's ;;; Let 'i2 := '!'i in Let 'r2 := '!'r in 'i2 '+ 'r2. ... ...
 ... ... @@ -84,7 +84,7 @@ Qed. Definition val_twice : val := ValFun 'f := 'f '() ;; 'f '() ;;; 'f '(). Lemma Rule_twice : forall (f:func) (H H':hprop) `{EB:Enc B} (Q:B->hprop), ... ... @@ -188,7 +188,7 @@ Qed. Definition val_mkcounter : val := ValFun 'u := Let 'p := val_ref 0 in (Fun 'v := val_incr 'p ;; val_get 'p). (Fun 'v := val_incr 'p ;;; val_get 'p). (* ---------------------------------------------------------------------- *) ... ...
 ... ... @@ -210,8 +210,8 @@ Definition val_new_cell : val := val_new_record 2%nat. Definition val_new_cell := ValFun 'x 'y := Let 'p := val_alloc 2 in val_set_item 'p 'x;; val_set_left 'p 'y;; val_set_item 'p 'x;;; val_set_left 'p 'y;;; 'p. *) ... ... @@ -258,9 +258,9 @@ Definition val_transfer := 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 'p1 'b2 ;;; val_set_hd 'b1 'x2 ;;; val_set_tl 'b1 'n2 ;;; val_set_tl 'p2 'f2 End. ... ... @@ -409,7 +409,7 @@ Definition val_mlist_iter : val := ValFix 'g 'f 'p := If_ 'p '<> null Then Let 'x := val_get_hd 'p in 'f 'x ;; 'f 'x ;;; Let 'q := val_get_tl 'p in 'g 'f 'q End. ... ... @@ -474,7 +474,7 @@ Definition val_mlist_length_using_iter : val := ValFun 'p := Let 'r := val_ref 0 in LetFun 'f 'x := val_incr 'r in val_mlist_iter 'f 'p ;; val_mlist_iter 'f 'p ;;; val_get 'r. Lemma Rule_mlist_length_using_iter : forall A `{EA:Enc A} (L:list A) (p:loc), ... ... @@ -501,11 +501,11 @@ Definition val_mlist_length_loop : val := Let 'n := val_ref 0 in While (Let 'p := val_get 'r in 'p '<> null) Do val_incr 'n ;; val_incr 'n ;;; Let 'p := val_get 'r in Let 'q := val_get_tl 'p in val_set 'r 'q Done ;; Done ;;; val_get 'n. Lemma Rule_mlist_length_loop : forall A `{EA:Enc A} (L:list A) (p:loc), ... ... @@ -544,7 +544,7 @@ Definition val_mlist_incr : val := If_ 'p '<> null Then ( Let 'x := val_get_hd 'p in Let 'y := 'x '+ 1 in val_set_hd 'p 'y;; val_set_hd 'p 'y;;; Let 'q := val_get_tl 'p in 'f 'q ) End. ... ... @@ -574,11 +574,11 @@ Definition val_mlist_in_place_rev : val := 'p '<> null) Do Let 'p := val_get 'r in Let 'q := val_get_tl 'p in val_set 'r 'q ;; val_set 'r 'q ;;; Let 't := val_get 's in val_set_tl 'p 't ;; val_set_tl 'p 't ;;; val_set 's 'p Done ;; Done ;;; val_get 's. Lemma Rule_mlist_in_place_rev : forall A `{EA:Enc A} (L:list A) (p:loc), ... ... @@ -616,7 +616,7 @@ Definition val_mlist_cps_append : val := If_ val_eq 'p null Then ( 'k 'q ) Else ( LetFun 'k2 'r := (val_set_tl 'p 'r ;; 'k 'p) in LetFun 'k2 'r := (val_set_tl 'p 'r ;;; 'k 'p) in Let 't := val_get_tl 'p in 'f 't 'q 'k2 ). ... ...
 ... ... @@ -152,8 +152,8 @@ Hint Extern 1 (Register_spec val_set_tl) => Provide rule_set_tl. Definition val_new_cell := ValFun 'x 'y := Let 'p := val_alloc 2 in val_set_hd 'p 'x;; val_set_tl 'p 'y;; val_set_hd 'p 'x;;; val_set_tl 'p 'y;;; 'p. Lemma rule_alloc_cell : ... ... @@ -442,11 +442,11 @@ Definition val_mlist_length_loop : val := Let 'n := val_ref 0 in While (Let 'p := val_get 'r in 'p '<> null) Do val_incr 'n ;; val_incr 'n ;;; Let 'p := val_get 'r in Let 'q := val_get_tl 'p in val_set 'r 'q Done ;; Done ;;; val_get 'n. Lemma rule_mlist_length_loop : forall L p, ... ...
 ... ... @@ -78,8 +78,8 @@ Definition val_push_back := 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_hd 'q 'v ;;; val_set_tl 'q 'r ;;; val_set_tl 'p 'r. Lemma rule_push_back : forall L v p, ... ... @@ -121,7 +121,7 @@ Definition val_pop_front := 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;; val_set_hd 'p 'r;;; 'x. Lemma rule_pop_front : forall L v p, ... ... @@ -160,9 +160,9 @@ Definition val_transfer := 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 'p1 'b2 ;;; val_set_hd 'b1 'x2 ;;; val_set_tl 'b1 'n2 ;;; val_set_tl 'p2 'f2 End. ... ...
 ... ... @@ -181,9 +181,9 @@ Definition val_new_node := val_new_record 3%nat. Definition val_new_node := 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;; val_set_item 'p 'x;;; val_set_left 'p 'y;;; val_set_right 'p 'z;;; 'p. *) ... ...
 ... ... @@ -397,7 +397,7 @@ Definition val_compress := LetFix 'f 'x := If_ 'x '<> 'z Then Let 'y := val_array_get 'p 'x in val_array_set 'p 'x 'z ;; val_array_set 'p 'x 'z ;;; 'f 'y End in 'f 'x. ... ... @@ -448,7 +448,7 @@ Hint Extern 1 (Register_spec val_compress) => Provide rule_compress. Definition val_find := ValFun 'p 'x := Let 'r := val_root 'p 'x in val_compress 'p 'x 'r ;; val_compress 'p 'x 'r ;;; 'r. Lemma rule_find : forall n R p x, ... ...
 ... ... @@ -323,7 +323,7 @@ Qed. Definition val_incr_twice := ValFun 'p := val_incr 'p ;; val_incr 'p ;;; val_incr 'p. (* EXERCISE: specify and verify [val_incr_twice] *) ... ... @@ -394,7 +394,7 @@ Definition val_example_one_ref := ValFun 'n := Let 'k := 'n '+ 1 in Let 'i := 'ref 'k in val_incr 'i ;; val_incr 'i ;;; '!'i. Lemma rule_val_example_one_ref : forall n, ... ... @@ -496,8 +496,8 @@ Definition val_push_back := 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_hd 'q 'v ;;; val_set_tl 'q 'r ;;; val_set_tl 'p 'r. Lemma rule_push_back : forall L v p, ... ... @@ -519,7 +519,7 @@ Definition val_pop_front := 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;; val_set_hd 'p 'r;;; 'x. Lemma rule_pop_front : forall L v p, ... ... @@ -718,9 +718,9 @@ Definition val_transfer := 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 'p1 'b2 ;;; val_set_hd 'b1 'x2 ;;; val_set_tl 'b1 'n2 ;;; val_set_tl 'p2 'f2 End. (* /SOLUTION *) ... ...
 ... ... @@ -264,10 +264,10 @@ Notation "'`If' v 'Then' F1 'Else' F2" := (local (cf_if_val v F1 F2)) (at level 69) : charac. Notation "'`Seq' F1 ;; F2" := Notation "'`Seq' F1 ;;; F2" := (local (cf_seq F1 F2)) (at level 68, right associativity, format "'[v' '`Seq' '[' F1 ']' ;; '/' '[' F2 ']' ']'") : charac. format "'[v' '`Seq' '[' F1 ']' ;;; '/' '[' F2 ']' ']'") : charac. Notation "'`Let' x ':=' F1 'in' F2" := (local (cf_let F1 (fun x => F2))) ... ...
 ... ... @@ -312,10 +312,10 @@ Notation "'`If' v 'Then' F1 'Else' F2" := (Local (Cf_if_val v F1 F2)) (at level 69) : charac. Notation "'`Seq' F1 ;; F2" := Notation "'`Seq' F1 ;;; F2" := (Local (Cf_seq F1 F2)) (at level 68, right associativity, format "'[v' '`Seq' '[' F1 ']' ;; '/' '[' F2 ']' ']'") : charac. format "'[v' '`Seq' '[' F1 ']' ;;; '/' '[' F2 ']' ']'") : charac. Notation "'``Let' x ':=' F1 'in' F2" := (Local (Cf_let_typed F1 (fun x => F2))) ... ...
 ... ... @@ -174,7 +174,7 @@ Qed. The initial goal is [S a H Q]. An assumption is provided to unfold the loop: [forall i H' Q', (If_ i <= b Then (Seq_ F ;; S (i+1)) Else (Ret tt)) H' Q' -> S i H' Q']. (If_ i <= b Then (Seq_ F ;;; S (i+1)) Else (Ret tt)) H' Q' -> S i H' Q']. After [xfor], the typical proof pattern is to generalize the goal by calling [assert (forall X i, i <= b -> S i (Hof i X) (Qof i X))], ... ... @@ -541,10 +541,10 @@ Notation "'`If' v 'Then' F1 'Else' F2" := (Cf_if_val v F1 F2) (at level 69) : charac. Notation "'`Seq' F1 ;; F2" := Notation "'`Seq' F1 ;;; F2" := (Cf_seq F1 F2) (at level 68, right associativity, format "'[v' '`Seq' '[' F1 ']' ;; '/' '[' F2 ']' ']'") : charac. format "'[v' '`Seq' '[' F1 ']' ;;; '/' '[' F2 ']' ']'") : charac. Notation "'`Let' x ':=' F1 'in' F2" := (Cf_let_typed F1 (fun x => F2)) ... ... @@ -578,10 +578,10 @@ Notation "'`If' v 'Then' F1 'Else' F2" := (Cf_if_val v F1 F2) (at level 69) : charac2. Notation "'`Seq' F1 ;; F2" := Notation "'`Seq' F1 ;;; F2" := (Cf_seq F1 F2) (at level 68, right associativity, format "'[v' '`Seq' '[' F1 ']' ;; '/' '[' F2 ']' ']'") : charac2. format "'[v' '`Seq' '[' F1 ']' ;;; '/' '[' F2 ']' ']'") : charac2. Notation "'`Let' x ':=' F1 'in' F2" := (Cf_let_typed F1 (fun x => F2)) ... ... @@ -616,10 +616,10 @@ Notation "'`If' v 'Then' F1 'Else' F2" := (Local (Cf_if_val v F1 F2)) (at level 69) : charac. Notation "'`Seq' F1 ;; F2" := Notation "'`Seq' F1 ;;; F2" := (Local (Cf_seq F1 F2)) (at level 68, right associativity, format "'[v' '`Seq' '[' F1 ']' ;; '/' '[' F2 ']' ']'") : charac. format "'[v' '`Seq' '[' F1 ']' ;;; '/' '[' F2 ']' ']'") : charac. Notation "'``Let' x ':=' F1 'in' F2" := (Local (Cf_let_typed F1 (fun x => F2))) ... ... @@ -735,7 +735,7 @@ 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). (Fun V := val_incr P ;;; val_get P). (* ---------------------------------------------------------------------- *) ... ...
 ... ... @@ -387,10 +387,10 @@ Notation "'Let' 'Rec' f x ':=' t1 'in' t2" := (at level 69, f at level 0, x at level 0, right associativity, format "'[v' '[' 'Let' 'Rec' f x ':=' t1 'in' ']' '/' '[' t2 ']' ']'") : trm_scope. Notation "t1 ;; t2" := Notation "t1 ;;; t2" := (trm_seq t1 t2) (at level 68, right associativity, only parsing, format "'[v' '[' t1 ']' ;; '/' '[' t2 ']' ']'") : trm_scope. format "'[v' '[' t1 ']' ;;; '/' '[' t2 ']' ']'") : trm_scope. Notation "'Fix' f x ':=' t" := (trm_fix f x t) ... ...
 ... ... @@ -328,7 +328,7 @@ Definition val_array_make : val := Let 'b := 'n '- 1 in For 'i := 0 To 'b Do (* todo: allow inlining of B *) Array' 'p`['i] `<- 'v Done;; Done;;; 'p. Lemma rule_array_make : forall n v, ... ...
 ... ... @@ -448,8 +448,8 @@ End Alloc_to_Record. Definition val_new_record_2 := ValFun 'x 'y := Let 'p := val_alloc 2 in val_set_field 0%nat 'p 'x;; val_set_field 1%nat 'p 'y;; val_set_field 0%nat 'p 'x;;; val_set_field 1%nat 'p 'y;;; 'p. Lemma Rule_new_record_2 : forall `{EA1:Enc A1} `{EA2:Enc A2} (v1:A1) (v2:A2), ... ... @@ -472,7 +472,7 @@ Definition val_new_record (n:nat) := let P : var := nat_to_var n in val_funs xs ( Let P := val_alloc n in LibList.fold_right (fun f t => val_set_field (f:field) P (nat_to_var f);; t) (trm_var P) fs). LibList.fold_right (fun f t => val_set_field (f:field) P (nat_to_var f);;; t) (trm_var P) fs). Lemma Subst_new_record_aux : forall (n':nat) fs xs Vs (i n:nat) (p:loc), n' = length Vs -> ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!