Commit 274c256e authored by charguer's avatar charguer

string vars

parent caf53b92
......@@ -13,6 +13,7 @@ License: MIT.
Set Implicit Arguments.
From TLC Require Export LibCore.
From Sep Require Export LambdaCF LambdaSepLifted.
Import LibList.
Generalizable Variables A B.
Open Scope charac.
......
......@@ -12,8 +12,9 @@ License: MIT.
*)
Set Implicit Arguments.
From TLC Require Export LibCore.
From TLC Require Export LibString LibCore.
From Sep Require Export Fmap TLCbuffer.
Open Scope string_scope.
(* ********************************************************************** *)
......@@ -22,12 +23,12 @@ From Sep Require Export Fmap TLCbuffer.
(* ---------------------------------------------------------------------- *)
(** Representation of variables and locations *)
Definition var := nat.
Definition var := string.
Definition loc := nat.
Definition null : loc := 0%nat.
Definition field := nat.
Definition eq_var_dec := Nat.eq_dec.
Definition eq_var_dec := String.string_dec.
Global Opaque field var loc.
......@@ -262,12 +263,12 @@ Notation "'If_' t0 'Then' t1 'End'" :=
Notation "'Let' x ':=' t1 'in' t2" :=
(trm_let x t1 t2)
(at level 69, x ident, right associativity,
(at level 69, x at level 0, right associativity,
format "'[v' '[' 'Let' x ':=' t1 'in' ']' '/' '[' t2 ']' ']'") : trm_scope.
Notation "'Let' 'Rec' f x ':=' t1 'in' t2" :=
(trm_let f (trm_fix f x t1) t2)
(at level 69, f ident, x ident, right associativity,
(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" :=
......@@ -277,75 +278,75 @@ Notation "t1 ;; t2" :=
Notation "'Fix' f x ':=' t" :=
(trm_fix f x t)
(at level 69, f ident, x ident) : trm_scope.
(at level 69, f at level 0, x at level 0) : trm_scope.
Notation "'Fix' f x1 x2 ':=' t" :=
(trm_fix f x1 (trm_fun x2 t))
(at level 69, f ident, x1 ident, x2 ident) : trm_scope.
(at level 69, f at level 0, x1 at level 0, x2 at level 0) : trm_scope.
Notation "'Fix' f x1 x2 x3 ':=' t" :=
(trm_fix f x1 (trm_fun x2 (trm_fun x3 t)))
(at level 69, f ident, x1 ident, x2 ident, x3 ident) : trm_scope.
(at level 69, f at level 0, x1 at level 0, x2 at level 0, x3 at level 0) : trm_scope.
Notation "'ValFix' f x ':=' t" :=
(val_fix f x t)
(at level 69, f ident, x ident) : trm_scope.
(at level 69, f at level 0, x at level 0) : trm_scope.
Notation "'ValFix' f x1 x2 ':=' t" :=
(val_fix f x1 (trm_fun x2 t))
(at level 69, f ident, x1 ident, x2 ident) : trm_scope.
(at level 69, f at level 0, x1 at level 0, x2 at level 0) : trm_scope.
Notation "'ValFix' f x1 x2 x3 ':=' t" :=
(val_fix f x1 (trm_fun x2 (trm_fun x3 t)))
(at level 69, f ident, x1 ident, x2 ident, x3 ident) : trm_scope.
(at level 69, f at level 0, x1 at level 0, x2 at level 0, x3 at level 0) : trm_scope.
Notation "'Fun' x1 ':=' t" :=
(trm_fun x1 t)
(at level 69, x1 ident) : trm_scope.
(at level 69, x1 at level 0) : trm_scope.
Notation "'Fun' x1 x2 ':=' t" :=
(trm_fun x1 (trm_fun x2 t))
(at level 69, x1 ident, x2 ident) : trm_scope.
(at level 69, x1 at level 0, x2 at level 0) : trm_scope.
Notation "'Fun' x1 x2 x3 ':=' t" :=
(trm_fun x1 (trm_fun x2 (trm_fun x3 t)))
(at level 69, x1 ident, x2 ident, x3 ident) : trm_scope.
(at level 69, x1 at level 0, x2 at level 0, x3 at level 0) : trm_scope.
Notation "'ValFun' x1 ':=' t" :=
(val_fun x1 t)
(at level 69, x1 ident) : trm_scope.
(at level 69, x1 at level 0) : trm_scope.
Notation "'ValFun' x1 x2 ':=' t" :=
(val_fun x1 (trm_fun x2 t))
(at level 69, x1 ident, x2 ident) : trm_scope.
(at level 69, x1 at level 0, x2 at level 0) : trm_scope.
Notation "'ValFun' x1 x2 x3 ':=' t" :=
(val_fun x1 (trm_fun x2 (trm_fun x3 t)))
(at level 69, x1 ident, x2 ident, x3 ident) : trm_scope.
(at level 69, x1 at level 0, x2 at level 0, x3 at level 0) : trm_scope.
Notation "'LetFun' f x1 ':=' t1 'in' t2" :=
(trm_let f (trm_fun x1 t1) t2)
(at level 69, f ident, x1 ident) : trm_scope.
(at level 69, f at level 0, x1 at level 0) : trm_scope.
Notation "'LetFun' f x1 x2 ':=' t1 'in' t2" :=
(trm_let f (trm_fun x1 (trm_fun x2 t1)) t2)
(at level 69, f ident, x1 ident, x2 ident) : trm_scope.
(at level 69, f at level 0, x1 at level 0, x2 at level 0) : trm_scope.
Notation "'LetFun' f x1 x2 x3 ':=' t1 'in' t2" :=
(trm_let f (trm_fun x1 (trm_fun x2 (trm_fun x3 t1))) t2)
(at level 69, f ident, x1 ident, x2 ident, x3 ident) : trm_scope.
(at level 69, f at level 0, x1 at level 0, x2 at level 0, x3 at level 0) : trm_scope.
Notation "'LetFix' f x1 ':=' t1 'in' t2" :=
(trm_let f (trm_fix f x1 t1) t2)
(at level 69, f ident, x1 ident) : trm_scope.
(at level 69, f at level 0, x1 at level 0) : trm_scope.
Notation "'LetFix' f x1 x2 ':=' t1 'in' t2" :=
(trm_let f (trm_fix f x1 (trm_fun x2 t1)) t2)
(at level 69, f ident, x1 ident, x2 ident) : trm_scope.
(at level 69, f at level 0, x1 at level 0, x2 at level 0) : trm_scope.
Notation "'LetFix' f x1 x2 x3 ':=' t1 'in' t2" :=
(trm_let f (trm_fix f x1 (trm_fun x2 (trm_fun x3 t1))) t2)
(at level 69, f ident, x1 ident, x2 ident, x3 ident) : trm_scope.
(at level 69, f at level 0, x1 at level 0, x2 at level 0, x3 at level 0) : trm_scope.
Notation "'While' t1 'Do' t2 'Done'" :=
(trm_while t1 t2)
......@@ -355,7 +356,7 @@ Notation "'While' t1 'Do' t2 'Done'" :=
Notation "'For' x ':=' t1 'To' t2 'Do' t3 'Done'" :=
(trm_for x t1 t2 t3)
(at level 69, x ident, (* t1 at level 0, t2 at level 0, *)
(at level 69, x at level 0, (* t1 at level 0, t2 at level 0, *)
format "'[v' 'For' x ':=' t1 'To' t2 'Do' '/' '[' t3 ']' '/' 'Done' ']'")
: trm_scope.
......@@ -366,6 +367,7 @@ Notation "'For' x ':=' t1 'To' t2 'Do' t3 'Done'" :=
(* TODO: check if it is possible to use a recursive notation *)
(* DEPRECATED
Notation "'Vars' X1 'from' n 'in' t" :=
(let X1 : var := n%nat in t)
(at level 69, X1 ident).
......@@ -444,6 +446,7 @@ Notation "'Vars' X1 , X2 , X3 , X4 , X5 , X6 , X7 'in' t" :=
let X6 : var := 5%nat in
let X7 : var := 6%nat in t)
(at level 69, X1 ident, X2 ident, X3 ident, X4 ident, X5 ident, X6 ident, X7 ident).
*)
(* ********************************************************************** *)
......@@ -815,6 +818,22 @@ Proof using. intros. rew_nary. Abort.
(* ---------------------------------------------------------------------- *)
(* ** Sequence of consecutive variables *)
(* TODO: generalize to lists *)
Definition nats := list nat.
Fixpoint nat_fresh (y:nat) (xs:nats) : bool :=
match xs with
| nil => true
| x::xs' => if eq_nat_dec x y then false else nat_fresh y xs'
end.
Fixpoint nat_distinct (xs:nats) : bool :=
match xs with
| nil => true
| x::xs' => nat_fresh x xs' && nat_distinct xs'
end.
(** [nat_seq i n] generates a list of variables [x1;x2;..;xn]
with [x1=i] and [xn=i+n-1]. Such lists are useful for
generic programming. *)
......@@ -830,7 +849,7 @@ Implicit Types start nb : nat.
Lemma var_fresh_nat_seq_lt : forall x start nb,
(x < start)%nat ->
var_fresh x (nat_seq start nb).
nat_fresh x (nat_seq start nb).
Proof using.
intros. gen start. induction nb; intros.
{ auto. }
......@@ -839,7 +858,7 @@ Qed.
Lemma var_fresh_nat_seq_ge : forall x start nb,
(x >= start+nb)%nat ->
var_fresh x (nat_seq start nb).
nat_fresh x (nat_seq start nb).
Proof using.
intros. gen start. induction nb; intros.
{ auto. }
......@@ -847,7 +866,7 @@ Proof using.
Qed.
Lemma var_distinct_nat_seq : forall start nb,
var_distinct (nat_seq start nb).
nat_distinct (nat_seq start nb).
Proof using.
intros. gen start. induction nb; intros.
{ auto. }
......@@ -863,6 +882,7 @@ Proof using.
{ auto. } { rew_list. rewrite~ IHnb. }
Qed.
(* TODO: convert nat to var
Lemma var_funs_nat_seq : forall start nb,
(nb > 0%nat)%nat ->
var_funs nb (nat_seq start nb).
......@@ -872,6 +892,7 @@ Proof using.
{ applys length_nat_seq. }
{ destruct nb. { false. math. } { simpl. auto_false. } }
Qed.
*)
End Nat_seq.
......
......@@ -21,11 +21,12 @@ Open Scope fmap_scope.
Ltac auto_star ::= jauto.
Implicit Types f : var.
Implicit Types v w : val.
Implicit Types t : trm.
Implicit Types n : int.
Implicit Types l : loc.
Implicit Types f : field.
Implicit Types k : field.
(* ********************************************************************** *)
......@@ -287,22 +288,22 @@ Qed.
(** Definition of the heap predicate describing a single record field,
written [l `.` f ~> v]. *)
Definition hfield (l:loc) (f:field) (v:val) : hprop :=
(l+f)%nat ~~~> v \* \[ l <> null ].
Definition hfield (l:loc) (k:field) (v:val) : hprop :=
(l+k)%nat ~~~> v \* \[ l <> null ].
Notation "l `.` f '~~~>' v" := (hfield l f v)
(at level 32, f at level 0, no associativity,
format "l `.` f '~~~>' v") : heap_scope.
Notation "l `.` k '~~~>' v" := (hfield l k v)
(at level 32, k at level 0, no associativity,
format "l `.` k '~~~>' v") : heap_scope.
Lemma hstar_hfield_same_loc_disjoint : forall l f v1 v2,
(l`.`f ~~~> v1) \* (l`.`f ~~~> v2) ==> \[False].
Lemma hstar_hfield_same_loc_disjoint : forall l k v1 v2,
(l`.`k ~~~> v1) \* (l`.`k ~~~> v2) ==> \[False].
Proof using.
intros. unfold hfield. hpull ;=> N1 N2.
applys hstar_hsingle_same_loc_disjoint.
Qed.
Lemma hfield_not_null : forall l f v,
(l`.`f ~~~> v) ==> (l`.`f ~~~> v) \* \[l <> null].
Lemma hfield_not_null : forall l k v,
(l`.`k ~~~> v) ==> (l`.`k ~~~> v) \* \[l <> null].
Proof using.
intros. subst. unfold hfield. hchanges~ hsingle_not_null.
Qed.
......@@ -310,16 +311,16 @@ Qed.
Arguments hfield_not_null : clear implicits.
Lemma hfield_eq_fun_hsingle :
hfield = (fun l f v => ((l+f)%nat ~~~> v) \* \[l <> null]).
hfield = (fun l k v => ((l+k)%nat ~~~> v) \* \[l <> null]).
Proof using. intros. auto. Qed.
Lemma hfield_to_hsingle : forall l f v,
(l`.`f ~~~> v) ==> ((l+f)%nat ~~~> v) \* \[l <> null].
Lemma hfield_to_hsingle : forall l k v,
(l`.`k ~~~> v) ==> ((l+k)%nat ~~~> v) \* \[l <> null].
Proof using. intros. auto. Qed.
Lemma hsingle_to_hfield : forall l f v,
Lemma hsingle_to_hfield : forall l k v,
l <> null ->
((l+f)%nat ~~~> v) ==> l`.`f ~~~> v.
((l+k)%nat ~~~> v) ==> l`.`k ~~~> v.
Proof using. intros. unfold hfield. hsimpl~. Qed.
Arguments hsingle_to_hfield : clear implicits.
......@@ -398,9 +399,9 @@ Lemma Alloc_split_eq : forall k1 (k:nat) p,
(k1 <= k)%nat ->
Alloc k p = Alloc k1 p \* Alloc (k-k1)%nat (p + k1)%nat.
Proof using.
Transparent loc.
Transparent loc field. unfold field.
intros k1 k. gen k1. induction k; introv N.
{ math_rewrite (k1 = 0%nat). rew_Alloc. rew_heap~. }
{math_rewrite (k1 = 0%nat). rew_Alloc. rew_heap~. }
{ destruct k1 as [|k1']; rew_nat.
{ rew_Alloc. rew_heap~. }
{ rew_Alloc. rewrite (IHk k1'); [|math]. rew_heap~. } }
......
......@@ -16,6 +16,7 @@ License: MIT.
Set Implicit Arguments.
From TLC Require Import LibCore.
From Sep Require Import LambdaSep.
Import LibList.
Generalizable Variables A B.
Open Scope trm_scope.
......
......@@ -22,19 +22,30 @@ Local Open Scope fmap_scope.
Implicit Types t : trm.
Implicit Types v : val.
Implicit Types f : field.
Implicit Types f : var.
Implicit Types k : field.
Implicit Type l p q : loc.
Implicit Types n : int.
Notation "'B'" := ("B":var) : var_scope.
Notation "'I'" := ("I":var) : var_scope.
Notation "'N'" := ("N":var) : var_scope.
Notation "'M'" := ("M":var) : var_scope.
Notation "'P'" := ("P":var) : var_scope.
Notation "'Q'" := ("Q":var) : var_scope.
Notation "'V'" := ("V":var) : var_scope.
Notation "'X'" := ("X":var) : var_scope.
Local Open Scope var_scope.
(* ********************************************************************** *)
(* * Derived basic functions *)
(* ---------------------------------------------------------------------- *)
(** Increment function *)
Definition val_incr :=
Vars P, N, M in
ValFun P :=
Let N := val_get P in
Let M := val_add N 1 in
......@@ -57,7 +68,6 @@ Hint Extern 1 (Register_spec val_incr) => Provide rule_incr.
(** Negation *)
Definition val_not :=
Vars N in
ValFun N := If_ val_eq N true Then false Else true.
Lemma rule_not : forall (b:bool),
......@@ -77,7 +87,6 @@ Hint Extern 1 (Register_spec val_not) => Provide rule_not.
(** Disequality test *)
Definition val_neq :=
Vars M, N, X in
ValFun M N :=
Let X := val_eq M N in
val_not X.
......@@ -99,44 +108,42 @@ Hint Extern 1 (Register_spec val_neq) => Provide rule_neq.
(* ---------------------------------------------------------------------- *)
(** Read to a record field *)
Definition val_get_field (f:field) :=
Vars P, Q in
Definition val_get_field (k:field) :=
ValFun P :=
Let Q := val_ptr_add P (nat_to_Z f) in
Let Q := val_ptr_add P (nat_to_Z k) in
val_get Q.
Lemma rule_get_field : forall l f v,
triple ((val_get_field f) l)
(l `.` f ~~~> v)
(fun r => \[r = v] \* (l `.` f ~~~> v)).
Lemma rule_get_field : forall l k v,
triple ((val_get_field k) l)
(l `.` k ~~~> v)
(fun r => \[r = v] \* (l `.` k ~~~> v)).
Proof using.
intros. applys rule_app_fun. reflexivity. simpl.
applys rule_let. { xapplys rule_ptr_add_nat. }
intros r. simpl. xpull. intro_subst.
rewrite hfield_eq_fun_hsingle.
xpull ;=> N. xapplys~ rule_get.
xpull ;=> HN. xapplys~ rule_get.
Qed.
(* ---------------------------------------------------------------------- *)
(** Write to a record field *)
Definition val_set_field (f:field) :=
Vars P, Q, V in
Definition val_set_field (k:field) :=
ValFun P V :=
Let Q := val_ptr_add P (nat_to_Z f) in
Let Q := val_ptr_add P (nat_to_Z k) in
val_set Q V.
Lemma rule_set_field : forall v' l f v,
triple ((val_set_field f) l v)
(l `.` f ~~~> v')
(fun r => \[r = val_unit] \* (l `.` f ~~~> v)).
Lemma rule_set_field : forall v' l k v,
triple ((val_set_field k) l v)
(l `.` k ~~~> v')
(fun r => \[r = val_unit] \* (l `.` k ~~~> v)).
Proof using.
intros. applys rule_app_fun2. reflexivity. auto. simpl.
applys rule_let. { xapplys rule_ptr_add_nat. }
intros r. simpl. xpull. intro_subst.
rewrite hfield_eq_fun_hsingle.
xpull ;=> N. xapplys~ rule_set.
xpull ;=> HN. xapplys~ rule_set.
Qed.
Arguments rule_set_field : clear implicits.
......@@ -186,14 +193,14 @@ Lemma Array_middle_eq : forall n p L,
Array L1 p \* (abs(p+n) ~~~> x) \* Array L2 (p + length L1 + 1)%nat.
Proof using.
(* TODO: simplify the Z/nat math, by using a result from LibListZ directly *)
introv N. applys himpl_antisym.
{ forwards (L1&x&L2&E&M): list_middle_inv (abs n) L.
introv HN. applys himpl_antisym.
{ forwards (L1&x&L2&E&HM): list_middle_inv (abs n) L.
asserts (N1&N2): (0 <= abs n /\ (abs n < length L)%Z).
{ split; rewrite abs_nonneg; math. } math.
lets M': eq_int_of_eq_nat M. rewrite abs_nonneg in M'; [|math].
lets M': eq_int_of_eq_nat HM. rewrite abs_nonneg in M'; [|math].
hsimpl~ (>> L1 x L2). subst L. rewrite Array_concat_eq, Array_cons_eq.
rew_nat. hsimpl. rewrite M. rewrite~ abs_nat_plus_nonneg. math. }
{ hpull ;=> L1 x L2 M E. subst n.
rew_nat. hsimpl. rewrite HM. rewrite~ abs_nat_plus_nonneg. math. }
{ hpull ;=> L1 x L2 HM E. subst n.
subst L. rewrite Array_concat_eq, Array_cons_eq.
rew_nat. hsimpl. applys_eq himpl_refl 1. fequals.
rewrite abs_nat_plus_nonneg; [|math]. rewrite~ abs_nat. }
......@@ -224,7 +231,7 @@ Lemma rule_alloc_array : forall n,
(fun r => Hexists (p:loc) (L:list val), \[r = val_loc p] \*
\[length L = n :> int] \* Array L p).
Proof using.
introv N. xapp. math.
introv HN. xapp. math.
intros r. hpull ;=> l (E&Nl). subst r.
hchange Array_of_Alloc. hpull ;=> L HL.
hsimpl~. rewrite HL. rewrite~ abs_nonneg.
......@@ -242,7 +249,6 @@ Implicit Types i ofs len : int.
(** Array get *)
Definition val_array_get : val :=
Vars P, I, N in
ValFun P I :=
Let N := val_ptr_add P I in
val_get N.
......@@ -253,7 +259,7 @@ Lemma rule_array_get : forall p i L,
(Array L p)
(fun r => \[r = L[i]] \* Array L p).
Proof using.
introv N. rewrite index_eq_inbound in N.
introv HN. rewrite index_eq_inbound in HN.
xcf. xapps. { math. }
rewrites (>> Array_middle_eq i). { math. }
xpull ;=> L1 x L2 EL HL.
......@@ -272,7 +278,6 @@ Notation "'Array'' p `[ i ]" := (trm_app (trm_app (trm_val val_array_get) p) i)
(** Array set *)
Definition val_array_set : val :=
Vars P, I, X, N in
ValFun P I X :=
Let N := val_ptr_add P I in
val_set N X.
......@@ -283,7 +288,7 @@ Lemma rule_array_set : forall p i v L,
(Array L p)
(fun r => \[r = val_unit] \* Array (L[i:=v]) p).
Proof using.
introv N. rewrite index_eq_inbound in N.
introv HN. rewrite index_eq_inbound in HN.
xcf. xapps. { math. }
rewrites (>> Array_middle_eq i). { math. }
xpull ;=> L1 x L2 EL HL.
......@@ -304,7 +309,6 @@ Notation "'Array'' p `[ i ] `<- x" := (trm_app (trm_app (trm_app (trm_val val_ar
(** Array make *)
Definition val_array_make : val :=
Vars N, V, P, B, I in
ValFun N V :=
Let P := val_alloc N in
Let B := val_sub N 1 in
......@@ -319,16 +323,16 @@ Lemma rule_array_make : forall n v,
\[]
(fun r => Hexists p L, \[r = val_loc p] \* \[L = make n v] \* Array L p).
Proof using.
introv N. xcf. xapp~ rule_alloc_array ;=> r p L Er EL. subst r.
introv HN. xcf. xapp~ rule_alloc_array ;=> r p L Er EL. subst r.
xapps. xseq.
{ (* todo: xfor tactic *)
applys local_erase. esplit; esplit; splits; [reflexivity|reflexivity|].
intros S LS EF M. subst EF. simpl in M.
intros S LS EF HM. subst EF. simpl in HM.
cuts G: (forall i L', i >= 0 -> length L' = n-i ->
S i (Array ((make i v)++L') p) (fun r => \[r = '()] \* (Array (make n v) p))).
{ applys_eq (>> G L) 2. math. math. rewrite make_zero. rew_list~. }
intros i. induction_wf IH: (upto n) i. intros L' Ei EL'.
applys (rm M). case_if.
applys (rm HM). case_if.
{ xapp~. { rewrite index_eq_inbound. rew_list. rewrite length_make; math. }
destruct L' as [|x L']. { false. rew_list in EL'. math. }
rewrite~ update_middle; [| rewrite length_make; math ].
......
......@@ -451,6 +451,8 @@ Qed.
(* ---------------------------------------------------------------------- *)
(* ** Specification for allocation of records of arbitrary arity *)
(* TODO: convert nat to var
Definition val_new_record (n:nat) :=
let xs := nat_seq 0%nat n in
let P : var := n%nat in
......@@ -568,6 +570,7 @@ Ltac xrule_new_record_core tt :=
Tactic Notation "xrule_new_record" :=
xrule_new_record_core tt.
*)
(* ********************************************************************** *)
(* * Lifted access rules for arrays *)
......
......@@ -110,10 +110,10 @@ Lemma List_combine_eq : forall A B (L1:list A) (L2:list B),
length L1 = length L2 ->
List.combine L1 L2 = LibList.combine L1 L2.
Proof using.
introv E. gen L2. induction L1 as [|x1 L1']; intros.
introv E. gen L2.
induction L1 as [|x1 L1']; intros; destruct L2 as [|x2 L2']; tryfalse.
{ auto. }
{ destruct L2 as [|x2 L2']. { false. }
rew_list in E. simpl. fequals~. }
{ rew_list in E. simpl. fequals~. }
Qed.
(* todo: reformulate without arguments *)
......
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