Commit e80bd62d authored by charguer's avatar charguer

primitives_cleanup

parent 9f3d73ac
(************************************************************)
(** Arrays *)
(** The model of an imperative array is a sequence, represented as a list *)
Definition array (A:Type) := list A.
Parameter ArrayOf : forall a A (T:htype A a) (M:array A) (l:loc), hprop.
Notation "'Array'" := (ArrayOf Id).
Require Import LibBag.
Parameter caml_array_make_spec : forall a,
Spec caml_array_make (n:int) (v:a) |R>>
n >= 0 ->
R \[] (fun l => Hexists M, l ~> Array M \* \[M = make n v]).
(* Note: zmake is the make function for lists with an argument in Z *)
Parameter caml_array_make_spec_direct : forall a,
Spec caml_array_make (n:int) (v:a) |R>>
R \[] (fun l => l ~> Array (make n v)).
(* todo: prove as a derived lemma *)
Parameter caml_array_get_spec : forall a,
Spec caml_array_get (l:loc) (i:int) |R>>
forall `{Inhab a} (t:list a), index t i ->
keep R (l ~> Array t) (fun x => \[x = t[i]]).
Parameter caml_array_set_spec : forall a,
Spec caml_array_set (l:loc) (i:int) (v:a) |R>>
forall (t:list a), index t i ->
R (l ~> Array t) (# l ~> Array (t[i:=v])).
Parameter caml_array_length_spec : forall a,
Spec caml_array_length (l:loc) |R>> forall (t:array a),
keep R (l ~> Array t) (fun x => \[x = length t]).
Hint Extern 1 (RegisterSpec caml_array_make) => Provide caml_array_make_spec.
Hint Extern 1 (RegisterSpec caml_array_get) => Provide caml_array_get_spec.
Hint Extern 1 (RegisterSpec caml_array_set) => Provide caml_array_set_spec.
Hint Extern 1 (RegisterSpec caml_array_length) => Provide caml_array_length_spec.
(* -- with credits ---*)
Set Implicit Arguments.
Require Export LibInt LibListZ CFSpec CFPrint CFPrimSpec.
Generalizable Variables a A.
Parameter array_make_cst : nat.
Parameter ml_array_make_spec_direct : forall a,
Spec ml_array_make (n:int) (v:a) |R>>
R (\$ (abs n * array_make_cst))
(fun l => l ~> Array (make n v)).
Parameter ml_array_make_spec : forall a,
Spec ml_array_make (n:int) (v:a) |R>>
n >= 0 ->
R (\$ (abs n * array_make_cst))
(fun l => Hexists M, l ~> Array M \* \[M = make n v]).
Hint Extern 1 (RegisterSpecCredits ml_array_make) => Provide ml_array_make_spec.
(************************************************************)
(** Lists *)
Parameter caml_list_iter_spec : forall a,
Spec caml_list_iter f l |R>> forall (I:list a->hprop),
(forall x t, (App f x;) (I (x::t)) (# I t)) ->
R (I l) (# I nil).
Hint Extern 1 (RegisterSpec caml_list_iter) => Provide caml_list_iter_spec.
(*
(************************************************************)
(** Stacks *)
Module Stack_ml.
Definition t (A:Type) := loc.
End Stack_ml.
Parameter caml_stack_create : func.
Parameter caml_stack_is_empty : func.
Parameter caml_stack_push : func.
Parameter caml_stack_pop : func.
*)
(*------------------------------------------------------------------*)
(* ** Lists *)
Fixpoint List A a (T:A->a->hprop) (L:list A) (l:list a) : hprop :=
match L,l with
| nil, nil => \[l = nil] (* %todo: True*)
| X::L', x::l' => x ~> T X \* l' ~> List T L'
| _,_=> \[False]
end.
Lemma focus_nil : forall A a (T:A->a->hprop),
\[] ==> nil ~> List T nil.
Proof. intros. simpl. hdata_simpl. hsimpl~. Qed.
Lemma unfocus_nil : forall a (l:list a) A (T:A->a->hprop),
l ~> List T nil ==> \[l = nil].
Proof. intros. simpl. hdata_simpl. destruct l. auto. hsimpl. Qed.
Lemma unfocus_nil' : forall A (L:list A) a (T:A->a->hprop),
nil ~> List T L ==> \[L = nil].
Proof.
intros. destruct L.
simpl. hdata_simpl. hsimpl~.
simpl. hdata_simpl. hsimpl.
Qed.
Lemma focus_cons : forall a (l:list a) A (X:A) (L':list A) (T:A->a->hprop),
(l ~> List T (X::L')) ==>
Hexists x l', (x ~> T X) \* (l' ~> List T L') \* \[l = x::l'].
Proof.
intros. simpl. hdata_simpl. destruct l as [|x l'].
hsimpl.
hsimpl~ x l'.
Qed.
Lemma focus_cons' : forall a (x:a) (l:list a) A (L:list A) (T:A->a->hprop),
(x::l) ~> List T L ==>
Hexists X L', \[L = X::L'] \* (x ~> T X) \* (l ~> List T L').
Proof. intros. destruct L; simpl; hdata_simpl; hsimpl~. Qed.
Lemma unfocus_cons : forall a (x:a) (l:list a) A (X:A) (L:list A) (T:A->a->hprop),
(x ~> T X) \* (l ~> List T L) ==>
((x::l) ~> List T (X::L)).
Proof. intros. simpl. hdata_simpl. hsimpl. Qed.
Global Opaque List.
(* should export Primitives.mli *)
(************************************************************)
(** Type conversion *)
external magic : 'a -> 'b = "%magic"
(************************************************************)
(** Physical equality *)
let (!==) x y =
external physical_eq : 'a -> 'a -> bool = "%physical_eq"
let ( == ) = physical_eq
let physical_neq x y =
not (x == y)
let ( !== ) = physical_neq
(************************************************************)
(** Comparison *)
let compare_eq : 'a -> 'a -> bool = "%compare_eq"
let compare_neq : 'a -> 'a -> bool = "%compare_neq"
let compare_lt : 'a -> 'a -> bool = "%compare_lt"
let compare_gt : 'a -> 'a -> bool = "%compare_gt"
let compare_le : 'a -> 'a -> bool = "%compare_le"
let compare_ge : 'a -> 'a -> bool = "%compare_ge"
let ( = ) = compare_eq
let ( <> ) = compare_neq
let ( < ) = compare_lt
let ( > ) = compare_gt
let ( <= ) = compare_le
let ( >= ) = compare_ge
let min x y =
if x <= y then x else y
......@@ -19,6 +43,16 @@ let max x y =
if x >= y then x else y
(************************************************************)
(** Boolean *)
external bool_and : bool -> bool -> bool = "%bool_and"
external bool_or : bool -> bool -> bool = "%bool_or"
let ( && ) = bool_and
let ( || ) = bool_or
(************************************************************)
(** References *)
......@@ -27,12 +61,16 @@ type 'a ref = { mutable contents : 'a }
let ref x =
{ contents = x }
let (!) r =
let get r =
r.contents
let (:=) r x =
let (!) = get
let set r x =
r.contents <- x
let (:=) = set
let incr r =
r := !r + 1
......@@ -59,7 +97,21 @@ let not x =
(************************************************************)
(** Arithmetic *)
(** Integer *)
external int_neg : int -> int = "%int_neg"
external int_add : int -> int -> int = "%int_add"
external int_sub : int -> int -> int = "%int_sub"
external int_mul : int -> int -> int = "%int_mul"
external int_div : int -> int -> int = "%int_div"
external int_mod : int -> int -> int = "%int_mod"
let ( ~- ) = int_neg
let ( + ) = int_add
let ( - ) = int_sub
let ( * ) = int_mul
let ( / ) = int_div
let ( mod ) = int_mod
let succ n =
n + 1
......@@ -86,3 +138,14 @@ let snd (x,y) =
let ignore x =
()
(************************************************************)
(** Arrays *)
external array_make : int -> 'a -> 'a array = "%array_make"
external array_length : 'a array -> int = "%array_length"
external array_get : 'a array -> int -> 'a = "%array_get"
external array_set : 'a array -> int -> 'a -> unit = "%array_set"
Set Implicit Arguments.
Require Export CFLib
LibListZ LibMap LibInt.
Generalizable Variables a A.
Global Opaque heap_is_empty hdata heap_is_single heap_is_empty_st.
(* todo: check needed *)
Global Opaque Zplus. (* todo: move *)
Transparent hdata. (* todo: should use hdata_simpl instead *)
(********************************************************************)
(* Z *)
Notation "'Zmod'" := Z.modulo.
Notation "'Zdiv'" := Z.div.
Require Import LibSet.
Open Scope container_scope.
(*------------------------------------------------------------------*)
(* ** Tuple 2 *)
Definition Tup2 A1 A2 a1 a2 (T1:A1->a1->hprop) (T2:A2->a2->hprop) P p :=
let '(X1,X2) := P in let '(x1,x2) := p in x1 ~> T1 X1 \* x2 ~> T2 X2.
Lemma focus_tup2 : forall a1 a2 (p:a1*a2) A1 A2 (T1:htype A1 a1) (T2:htype A2 a2) V1 V2,
p ~> Tup2 T1 T2 (V1,V2) ==> let '(x1,x2) := p in x1 ~> T1 V1 \* x2 ~> T2 V2.
Proof. auto. Qed.
Lemma unfocus_tup2 : forall a1 (x1:a1) a2 (x2:a2) A1 A2 (T1:htype A1 a1) (T2:htype A2 a2) V1 V2,
x1 ~> T1 V1 \* x2 ~> T2 V2 ==> (x1,x2) ~> Tup2 T1 T2 (V1,V2).
Proof. intros. unfold Tup2. hdata_simpl. auto. Qed.
Global Opaque Tup2.
(*------------------------------------------------------------------*)
(* ** Tuple 3 *)
Definition Tup3 A1 A2 A3 a1 a2 a3 (T1:A1->a1->hprop) (T2:A2->a2->hprop) (T3:A3->a3->hprop) P p :=
let '(X1,X2,X3) := P in let '(x1,x2,x3) := p in x1 ~> T1 X1 \* x2 ~> T2 X2 \* x3 ~> T3 X3.
Lemma focus_tup3 : forall a1 a2 a3 (p:a1*a2*a3) A1 A2 A3 (T1:htype A1 a1) (T2:htype A2 a2) (T3:A3->a3->hprop) V1 V2 V3,
p ~> Tup3 T1 T2 T3 (V1,V2,V3) ==> let '(x1,x2,x3) := p in x1 ~> T1 V1 \* x2 ~> T2 V2 \* x3 ~> T3 V3.
Proof. auto. Qed.
Lemma unfocus_tup3 : forall a1 (x1:a1) a2 (x2:a2) a3 (x3:a3) A1 A2 A3 (T1:htype A1 a1) (T2:htype A2 a2) (T3:A3->a3->hprop) V1 V2 V3,
x1 ~> T1 V1 \* x2 ~> T2 V2 \* x3 ~> T3 V3 ==> (x1,x2,x3) ~> Tup3 T1 T2 T3 (V1,V2,V3).
Proof. intros. unfold Tup3. hdata_simpl. auto. Qed.
Global Opaque Tup3.
(************************************************************)
(** Locations *)
Parameter caml_phy_eq_spec : Spec caml_phy_eq x y |R>>
pure R (= (x '= y :> loc)).
Parameter caml_phy_neq_spec : Spec caml_phy_neq x y |R>>
pure R (= (x '<> y :> loc)).
Hint Extern 1 (RegisterSpec caml_phy_eq) => Provide caml_phy_eq_spec.
Hint Extern 1 (RegisterSpec caml_phy_neq) => Provide caml_phy_neq_spec.
(************************************************************)
(** Boolean *)
Parameter caml_eqb_int_spec : Spec caml_eqb (x:int) (y:int) |R>>
pure R (= (x '= y)).
Parameter caml_and_spec : Spec caml_and x y |R>>
pure R (= (x && y)).
Parameter caml_or_spec : Spec caml_or x y |R>>
pure R (= (x || y)).
Hint Extern 1 (RegisterSpec caml_eqb) => Provide caml_eqb_int_spec.
Hint Extern 1 (RegisterSpec caml_and) => Provide caml_and_spec.
Hint Extern 1 (RegisterSpec caml_and) => Provide caml_or_spec.
(************************************************************)
(** Arithmetic *)
Parameter caml_plus_spec : Spec caml_plus x y |R>>
pure R (= (x + y)%Z).
Parameter caml_minus_spec : Spec caml_minus x y |R>>
pure R (= (x - y)%Z).
Parameter caml_div_spec : Spec caml_div x y |R>>
(y <> 0) ->
R \[] (fun z => \[z = Zdiv x y]).
Parameter caml_mod_spec : Spec caml_mod x y |R>>
(y <> 0) ->
R \[] (fun z => \[z = Zmod x y]).
Parameter caml_leq_spec : Spec caml_leq x y |R>>
pure R (= (x <= y)%I).
Parameter caml_geq_spec : Spec caml_geq x y |R>>
pure R (= (x >= y)%I).
Parameter caml_lt_spec : Spec caml_lt x y |R>>
pure R (= (x < y)%I).
Parameter caml_gt_spec : Spec caml_gt x y |R>>
pure R (= (x > y)%I).
Hint Extern 1 (RegisterSpec caml_plus) => Provide caml_plus_spec.
Hint Extern 1 (RegisterSpec caml_minus) => Provide caml_minus_spec.
Hint Extern 1 (RegisterSpec caml_div) => Provide caml_div_spec.
Hint Extern 1 (RegisterSpec caml_mod) => Provide caml_mod_spec.
Hint Extern 1 (RegisterSpec caml_leq) => Provide caml_leq_spec.
Hint Extern 1 (RegisterSpec caml_geq) => Provide caml_geq_spec.
Hint Extern 1 (RegisterSpec caml_lt) => Provide caml_lt_spec.
Hint Extern 1 (RegisterSpec caml_gt) => Provide caml_gt_spec.
(************************************************************)
(** Stream *)
(* TODO *)
Definition stream := list.
Definition stream_cell := list.
(********************************************************************)
(** IO manipulations
Parameter Channel : forall (L:list dynamic) (l:loc), hprop.
Notation "l ~>> L" := (l ~> Channel L)
(at level 32, no associativity).
Parameter caml_read_int_spec :
Spec caml_read_int () |R>> forall L (n:int),
R (stdin ~>> (dyn n::L)) (fun x => \[x = n] \* stdin ~>> L).
Parameter caml_print_int_spec :
Spec caml_print_int (n:int) |R>> forall L,
R (stdout ~>> L) (# stdout ~>> L & (dyn n)).
Hint Extern 1 (RegisterSpec caml_read_int) => Provide caml_read_int_spec.
Hint Extern 1 (RegisterSpec caml_print_int) => Provide caml_print_int_spec.
(* Tools for stdio *)
Definition list_dyn A (L:list A) :=
LibList.map dyn L.
Lemma list_dyn_nil : forall A,
list_dyn (@nil A) = nil.
Proof. auto. Qed.
Lemma list_dyn_cons : forall A X (L:list A),
list_dyn (X::L) = (dyn X)::(list_dyn L).
Proof. auto. Qed.
Lemma list_dyn_last : forall A X (L:list A),
list_dyn (L&X) = (list_dyn L) & (dyn X).
Proof. intros. unfold list_dyn. rew_list~. Qed.
Hint Rewrite list_dyn_nil list_dyn_cons list_dyn_last: rew_app.
Hint Rewrite list_dyn_nil list_dyn_cons list_dyn_last : rew_map.
Hint Rewrite list_dyn_nil list_dyn_cons list_dyn_last: rew_list.
*)
\ No newline at end of file
(*------------------------------------------------------------------*)
(* ** References *)
Definition Ref a A (T:htype A a) (V:A) (l:loc) :=
Hexists v, heap_is_single l v \* v ~> T V.
Instance Ref_Heapdata : forall a A (T:htype A a),
(Heapdata (@Ref a A T)).
Proof using.
intros. applys Heapdata_prove. intros x X1 X2.
unfold Ref. hdata_simpl. hextract as x1 x2.
hchange (@star_is_single_same_loc x). hsimpl.
Qed.
Open Local Scope heap_scope_advanced.
Notation "'~~>' v" := (~> Ref (@Id _) v)
(at level 32, no associativity) : heap_scope_advanced.
(*
Notation "l '~~>' v" := (l ~> Ref (@Id _) v)
(at level 32, no associativity) : heap_scope.
*)
Notation "l '~~>' v" := (hdata (@Ref _ _ (@Id _) v) l)
(at level 32, no associativity) : heap_scope.
Lemma focus_ref : forall (l:loc) a A (T:htype A a) V,
l ~> Ref T V ==> Hexists v, l ~~> v \* v ~> T V.
Proof. intros. unfold Ref, hdata. unfold Id. hsimpl~. Qed.
Lemma unfocus_ref : forall (l:loc) a (v:a) A (T:htype A a) V,
l ~~> v \* v ~> T V ==> l ~> Ref T V.
Proof. intros. unfold Ref. hdata_simpl. hsimpl. subst~. Qed.
Lemma heap_is_single_impl_null : forall (l:loc) A (v:A),
heap_is_single l v ==> heap_is_single l v \* \[l <> null].
Proof.
intros. intros h Hh. forwards*: heap_is_single_null. exists___*.
Qed.
Lemma focus_ref_null : forall a A (T:htype A a) V,
null ~> Ref T V ==> \[False].
Proof.
intros. unfold Ref, hdata. hextract as v.
hchanges (@heap_is_single_impl_null null).
Qed.
Global Opaque Ref.
Implicit Arguments focus_ref [a A].
Implicit Arguments unfocus_ref [a A].
(* does not really work? *)
Notation "l '~~>' v" := (hdata (@Ref _ _ (@Id _) v) l)
(at level 32, no associativity).
(************************************************************)
(** References *)
Parameter caml_ref_spec : forall a,
Spec caml_ref (v:a) |R>>
R \[] (~~> v).
Parameter caml_get_spec : forall a,
Spec caml_get (l:loc) |R>>
forall (v:a), keep R (l ~~> v) (fun x => \[x = v]).
Parameter caml_set_spec : forall a,
Spec caml_set (l:loc) (v:a) |R>>
forall (v':a), R (l ~> Ref Id v') (# l ~> Ref Id v).
Parameter caml_sset_spec : forall a a',
Spec caml_sset (l:loc) (v:a) |R>>
forall (v':a'), R (l ~~> v') (# l ~~> v).
Parameter caml_incr_spec :
Spec caml_incr (l:loc) |R>>
forall n, R (l ~~> n) (# l ~~> (n+1)).
Parameter caml_decr_spec :
Spec caml_decr (l:loc) |R>>
forall n, R (l ~~> n) (# l ~~> (n-1)).
Parameter caml_free_spec :
Spec caml_free (l:loc) |R>>
forall A (v:A), R (l ~> Ref Id v) (# \[]).
Hint Extern 1 (RegisterSpec caml_ref) => Provide caml_ref_spec.
Hint Extern 1 (RegisterSpec caml_get) => Provide caml_get_spec.
Hint Extern 1 (RegisterSpec caml_set) => Provide caml_set_spec.
Hint Extern 1 (RegisterSpec caml_sset) => Provide caml_sset_spec.
Hint Extern 1 (RegisterSpec caml_incr) => Provide caml_incr_spec.
Hint Extern 1 (RegisterSpec caml_decr) => Provide caml_decr_spec.
Hint Extern 1 (RegisterSpec caml_free) => Provide caml_free_spec.
(************************************************************)
(** Group of References *)
Parameter caml_ref_spec_group : forall a,
Spec caml_ref (v:a) |R>> forall (M:map loc a),
R (Group (Ref Id) M) (fun (l:loc) =>
Group (Ref Id) (M[l:=v]) \* \[l \notindom M]).
Lemma caml_get_spec_group : forall a,
Spec caml_get (l:loc) |R>> forall (M:map loc a),
forall `{Inhab a}, l \indom M ->
keep R (Group (Ref Id) M) (fun x => \[x = M[l]]).
Proof.
intros. xweaken. intros l R LR HR M IA IlM. simpls.
rewrite~ (Group_rem l M). xapply (HR (M[l])); hsimpl~.
Qed.
Lemma caml_set_spec_group : forall a,
Spec caml_set (l:loc) (v:a) |R>> forall (M:map loc a),
forall `{Inhab a}, l \indom M ->
R (Group (Ref Id) M) (# Group (Ref Id) (M[l:=v])).
Proof.
intros. xweaken. intros l v R LR HR M IA IlM. simpls.
rewrite~ (Group_rem l M).
xapply (HR (M[l])). hsimpl.
intros _. hchanges~ (Group_add' l M).
Qed.
(************************************************************)
(** Pairs *)
Parameter caml_fst_spec : forall a1 a2,
Spec caml_fst (p:a1*a2) |R>>
pure R (= fst p).
Parameter caml_snd_spec : forall a1 a2,
Spec caml_snd (p:a1*a2) |R>>
pure R (= snd p).
Hint Extern 1 (RegisterSpec caml_fst) => Provide caml_fst_spec.
Hint Extern 1 (RegisterSpec caml_snd) => Provide caml_snd_spec.
......@@ -8,18 +8,18 @@ external magic : 'a -> 'b = "%magic"
(************************************************************)
(** Physical equality *)
external ( == ) : 'a -> 'a -> bool = "%phy_eq"
external physical_eq : 'a -> 'a -> bool = "%physical_eq"