Commit 9f3d73ac authored by charguer's avatar charguer

primitives

parent 58cfc3c9
let make = Primitives.array_make
let length = Primitives.array_length
let get = Primitives.array_get
let set = Primitives.array_set
let init n f =
assert (n >= 0);
if n = 0 then [||] else begin
let res = create n (f 0) in
for i = 1 to pred n do
unsafe_set res i (f i)
done;
res
end
(* Remark: might be optimized by using a sub-array to avoid initialization *)
let fill a start nb v =
assert (not (start < 0 || nb < 0 || start > length a - nb));
for i = start to pred (start + nb) do
a.(i) <- v;
done
let blit a1 start1 a2 start2 nb =
assert (not (nb < 0 || start1 < 0 || start1 > length a1 - nb
|| start2 < 0 || start2 > length a2 - nb));
for i = 0 to pred nb do
a2.(start2 + i) <- a1.(start1 + i);
done
let append a1 a2 =
let n1 = length a1 in
let n2 = length a2 in
if n1 = 0 && n2 = 0 then [||] else begin
let d = (if n1 <> 0 then a1.(0) else a2.(0)) in
let a = make (n1+n2) d in
for i = 0 to pred n1 do
a.(i) <- a1.(i);
done;
for i = 0 to pred n2 do
a.(n1+i) <- a2.(i)
done;
end
(* Remark: might be optimized by using a sub-array to avoid initialization *)
let iter f a =
for i = 0 to pred (length a) do
f a.(i)
done
let iteri f a =
for i = 0 to pred (length a) do
f i a.(i)
done
let map f a =
let n = length a in
if n = 0 then [||] else begin
let r = make n (f a.(0)) in
for i = 1 to pred n do
r.(i) <- f a.(i);
done;
r
end
(* Remark: might be optimized by using a sub-array to avoid initialization *)
let mapi f a =
let n = length a in
if n = 0 then [||] else begin
let r = make n (f 0 a.(0)) in
for i = 1 to pred n do
r.(i) <- f i a.(i);
done;
r
end
(* Remark: might be optimized by using a sub-array to avoid initialization *)
let fold_left f x a =
let r = ref x in
for i = 0 to pred (length a) do
r := f !r a.(i)
done;
!r
let fold_right f a x =
let r = ref x in
for i = pred (length a) downto 0 do
r := f a.(i) !r
done;
!r
(* INCLUDE?
let hd = function
| [] -> assert false
| a::l -> a
let tl = function
| [] -> assert false
| a::l -> l
*)
let length l =
let rec aux len = function
| [] -> len
| a::l -> length_aux (len + 1) l
in
aux 0 l
let nth l n =
assert (n >= 0);
let rec aux l n =
match l with
| [] -> assert false
| a::l -> if n = 0 then a else aux l (n - 1)
in
aux l n
let append l1 l2 =
let rec aux = function
| [] -> l2
| a::l -> a::(aux l)
in
aux l1
let (@) = append
let rec rev_append l1 l2 =
match l1 with
| [] -> l2
| a :: l -> rev_append l (a :: l2)
let rev l =
rev_append l []
let rec concat = function
| [] -> []
| l::r -> l @ flatten r
let rec iter f = function
| [] -> ()
| a::l -> f a; iter f l
let iteri f l =
let rec aux i = function
| [] -> ()
| a::l -> f i a; aux (i + 1) l
in
aux 0 l
let rec map f = function
| [] -> []
| a::l ->
let r = f a in
r :: map f l
let mapi f l =
let rec aux i = function
| [] -> []
| a::l ->
let r = f i a in
r :: aux (i + 1) l
in
mapi 0 f l
(* USEFUL?
let rev_map f l =
let rec rmap_f acc = function
| [] -> acc
| a::l -> rmap_f (f a :: acc) l
in
rmap_f [] l
*)
let rec fold_left f acc l =
match l with
| [] -> acc
| a::l -> fold_left f (f acc a) l
let rec fold_right f l acc =
match l with
| [] -> acc
| a::l -> f a (fold_right f l acc)
let rec for_all p = function
| [] -> true
| a::l -> p a && for_all p l
let rec exists p = function
| [] -> false
| a::l -> p a || exists p l
exception Find_not_found
let rec find p = function
| [] -> raise Find_not_found
| a::l -> if p a then a else find p l
let filter p l =
let rec aux acc = function
| [] -> rev acc
| a::l -> if p a then aux (a::acc) l else find acc l
in
aux [] l
let partition p l =
let rec aux yes no = function
| [] -> (rev yes, rev no)
| x :: l ->
if p x
then aux (x :: yes) no l
else aux yes (x :: no) l
in
aux [] [] l
let rec split = function
| [] -> ([], [])
| (x,y)::l ->
let (rx, ry) = split l in
(x::rx, y::ry)
let rec combine l1 l2 =
match (l1, l2) with
| ([], []) -> []
| (a1::l1, a2::l2) -> (a1, a2) :: (combine l1 l2)
| (_, _) -> assert false
let take n l =
assert (n >= 0);
let rec aux n l =
if n = 0 then [] else begin
match l with
| [] -> assert false
| a::l -> a::(aux (n-1) l) in
end
in
aux n l
let drop n l =
assert (n >= 0);
let rec aux n l =
if n = 0 then l else begin
match l with
| [] -> assert false
| a::l -> aux (n-1) l in
end
in
aux n l
let split_at n l =
assert (n >= 0);
let rec aux n l =
if n = 0 then ([], l) else begin
match l with
| [] -> assert false
| a::l ->
let (l1,l2) = aux (n-1) l in
(a::l1,l2)
end
in
aux n l
(************************************************************)
(* LATER move into List2 module
let rec for_all2 p l1 l2 =
match (l1, l2) with
([], []) -> true
| (a1::l1, a2::l2) -> p a1 a2 && for_all2 p l1 l2
| (_, _) -> invalid_arg "List.for_all2"
let rec exists2 p l1 l2 =
match (l1, l2) with
([], []) -> false
| (a1::l1, a2::l2) -> p a1 a2 || exists2 p l1 l2
| (_, _) -> invalid_arg "List.exists2"
let rec map2 f l1 l2 =
match (l1, l2) with
([], []) -> []
| (a1::l1, a2::l2) -> let r = f a1 a2 in r :: map2 f l1 l2
| (_, _) -> invalid_arg "List.map2"
let rev_map2 f l1 l2 =
let rec rmap2_f acc l1 l2 =
match (l1, l2) with
| ([], []) -> acc
| (a1::l1, a2::l2) -> rmap2_f (f a1 a2 :: acc) l1 l2
| (_, _) -> invalid_arg "List.rev_map2"
in
rmap2_f [] l1 l2
;;
let rec iter2 f l1 l2 =
match (l1, l2) with
([], []) -> ()
| (a1::l1, a2::l2) -> f a1 a2; iter2 f l1 l2
| (_, _) -> invalid_arg "List.iter2"
let rec fold_left2 f acc l1 l2 =
match (l1, l2) with
([], []) -> acc
| (a1::l1, a2::l2) -> fold_left2 f (f acc a1 a2) l1 l2
| (_, _) -> invalid_arg "List.fold_left2"
let rec fold_right2 f l1 l2 acc =
match (l1, l2) with
([], []) -> acc
| (a1::l1, a2::l2) -> f a1 a2 (fold_right2 f l1 l2 acc)
| (_, _) -> invalid_arg "List.fold_right2"
*)
(************************************************************)
(** LATER, into some other file Stacks *)
(*
Module Stack_ml.
Definition t (A:Type) := loc.
End Stack_ml.
Parameter ml_stack_create : func.
Parameter ml_stack_is_empty : func.
Parameter ml_stack_push : func.
Parameter ml_stack_pop : func.
*)
(* should export Primitives.mli *)
(************************************************************)
(** Physical equality *)
let (!==) x y =
not (x == y)
(************************************************************)
(** Comparison *)
let min x y =
if x <= y then x else y
let max x y =
if x >= y then x else y
(************************************************************)
(** References *)
type 'a ref = { mutable contents : 'a }
let ref x =
{ contents = x }
let (!) r =
r.contents
let (:=) r x =
r.contents <- x
let incr r =
r := !r + 1
let decr r =
r := !r - 1
(** [ref_free r] is a logical free operation, useful for translating
to languages without garbage collection *)
let ref_free r =
()
(** [ref_unsafe_set r x] allows to modifies the contents of a reference *)
let ref_unsafe_set r x =
r.contents <- (magic x)
(************************************************************)
(** Boolean *)
let not x =
if x then false else true
(************************************************************)
(** Arithmetic *)
let succ n =
n + 1
let pred n =
n - 1
let abs x =
if x >= 0 then x else -x
(************************************************************)
(** Pairs *)
let fst (x,y) =
x
let snd (x,y) =
y
(************************************************************)
(** Unit *)
let ignore x =
()
(************************************************************)
(** Type conversion *)
external magic : 'a -> 'b = "%magic"
(************************************************************)
(** Physical equality *)
external ( == ) : 'a -> 'a -> bool = "%phy_eq"
(************************************************************)
(** Comparison *)
external ( = ) : 'a -> 'a -> bool = "%equal"
external ( <> ) : 'a -> 'a -> bool = "%notequal"
external ( < ) : 'a -> 'a -> bool = "%lessthan"
external ( > ) : 'a -> 'a -> bool = "%greaterthan"
external ( <= ) : 'a -> 'a -> bool = "%lessequal"
external ( >= ) : 'a -> 'a -> bool = "%greaterequal"
(************************************************************)
(** Boolean *)
external ( && ) : bool -> bool -> bool = "%bool_and"
external ( || ) : bool -> bool -> bool = "%bool_or"
(************************************************************)
(** Integer *)
external ( ~- ) : int -> int = "%int_neg"
external ( + ) : int -> int -> int = "%int_add"
external ( - ) : int -> int -> int = "%int_sub"
external ( * ) : int -> int -> int = "%int_mul"
external ( / ) : int -> int -> int = "%int_div"
external ( mod ) : int -> int -> int = "%int_mod"
(************************************************************)
(** 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"
(************************************************************)
(** IO *)
(*
Parameter stdin : loc.
Parameter stdout : loc.
Parameter ml_read_int : func.
Parameter ml_print_int : func.
*)
(************************************************************)
(** Type conversion *)
val magic : 'a -> 'b
(************************************************************)
(** Physical equality *)
val ( == ) : 'a -> 'a -> bool
(************************************************************)
(** Comparison *)
val ( = ) : 'a -> 'a -> bool
val ( <> ) : 'a -> 'a -> bool
val ( < ) : 'a -> 'a -> bool
val ( > ) : 'a -> 'a -> bool
val ( <= ) : 'a -> 'a -> bool
val ( >= ) : 'a -> 'a -> bool
(************************************************************)
(** Boolean *)
val ( && ) : bool -> bool -> bool
val ( || ) : bool -> bool -> bool
(************************************************************)
(** Integer *)
val ( ~- ) : int -> int
val ( + ) : int -> int -> int
val ( - ) : int -> int -> int
val ( * ) : int -> int -> int
val ( / ) : int -> int -> int
val ( mod ) : int -> int -> int
(************************************************************)
(** Arrays *)
val array_make : int -> 'a -> 'a array
val array_length : 'a array -> int
val array_get : 'a array -> int -> 'a
val array_set : 'a array -> int -> 'a -> unit
This diff is collapsed.
......@@ -2367,23 +2367,6 @@ Definition weakenable B (F:~~B) :=
(*------------------------------------------------------------------*)
(* ** Properties of [local] *)
(** A definition whose head is [local] satisfies [is_local] *)
Lemma local_is_local : forall B (F:~~B),
is_local (local F).
Proof using. intros. unfolds. rewrite~ local_local. Qed.
Hint Resolve local_is_local.
(** A introduction rule to establish [is_local] *)
Lemma is_local_prove : forall B (F:~~B),
(forall H Q, F H Q <-> local F H Q) -> is_local F.
Proof using.
intros. unfold is_local. apply func_ext_2.
intros. applys prop_ext. applys H.
Qed.
(** The [local] operator can be freely erased from a conclusion *)
Lemma local_erase : forall B (F:~~B),
......@@ -2411,6 +2394,23 @@ Proof using.
apply~ local_erase.
Qed.
(** A definition whose head is [local] satisfies [is_local] *)
Lemma local_is_local : forall B (F:~~B),
is_local (local F).
Proof using. intros. unfolds. rewrite~ local_local. Qed.
Hint Resolve local_is_local.
(** A introduction rule to establish [is_local] *)
Lemma is_local_prove : forall B (F:~~B),
(forall H Q, F H Q <-> local F H Q) -> is_local F.
Proof using.
intros. unfold is_local. apply func_ext_2.
intros. applys prop_ext. applys H.
Qed.
(** Weaken and frame and gc property [local] *)
Lemma local_wgframe : forall B (F:~~B) H H1 H2 Q1 Q,
......@@ -2438,7 +2438,15 @@ Proof using.
hchange WQ. hsimpl.
Qed.
(** Weakening from [local] *)
(** Frame property from [local] *)
Lemma local_frame : forall H' B H Q (F:~~B),
is_local F ->
F H Q ->
F (H \* H') (Q \*+ H').
Proof using. intros. apply* local_wframe. Qed.
(** Weakening on pre and post from [local] *)
Lemma local_weaken : forall B H' Q' (F:~~B) H Q,
is_local F ->
......@@ -2450,10 +2458,51 @@ Proof using.
intros. eapply local_wframe with (H2 := \[]); eauto; rew_heap~.
Qed.
(* DEPRECATED
Lemma local_weaken' : forall B (F:~~B),
is_local F -> weakenable F.
Proof using. intros_all. apply* local_weaken. Qed.
(* todo: use only one lemma from the two above *)
*)
(** Garbage collection on precondition from [local] *)
Lemma local_gc_pre : forall HG H' B (F:~~B) H Q,
is_local F ->
H ==> HG \* H' ->
F H' Q ->
F H Q.
Proof using.
introv L M W. rewrite L. introv Ph.
exists H' HG Q. splits.
rewrite star_comm. apply~ M.
auto.
hsimpl.
Qed.
(** Weakening on pre and post with gc from [local] *)
Lemma local_weaken_gc : forall B H' Q' (F:~~B) H Q,
is_local F ->