The Coq Proof Assistant

# Library Ltac2.Array

Require Import Ltac2.Init.
Require Ltac2.Int.
Require Ltac2.Control.
Require Ltac2.Bool.
Require Ltac2.Message.
Ltac2 @external empty : 'a array := "coq-core.plugins.ltac2" "array_empty".
Ltac2 @external make : int -> 'a -> 'a array := "coq-core.plugins.ltac2" "array_make".
Ltac2 @external length : 'a array -> int := "coq-core.plugins.ltac2" "array_length".
Ltac2 @external get : 'a array -> int -> 'a := "coq-core.plugins.ltac2" "array_get".
Ltac2 @external set : 'a array -> int -> 'a -> unit := "coq-core.plugins.ltac2" "array_set".
Ltac2 @external lowlevel_blit : 'a array -> int -> 'a array -> int -> int -> unit := "coq-core.plugins.ltac2" "array_blit".
Ltac2 @external lowlevel_fill : 'a array -> int -> int -> 'a -> unit := "coq-core.plugins.ltac2" "array_fill".
Ltac2 @external concat : ('a array) list -> 'a array := "coq-core.plugins.ltac2" "array_concat".
Ltac2 lowlevel_sub (arr : 'a array) (start : int) (len : int) :=
let l := length arr in
match Int.equal l 0 with
| true => empty
| false =>
let newarr:=make len (get arr 0) in
lowlevel_blit arr start newarr 0 len;
newarr
end.
Ltac2 init (l : int) (f : int->'a) :=
let rec init_aux (dst : 'a array) (pos : int) (len : int) (f : int->'a) :=
match Int.equal len 0 with
| true => ()
| false =>
set dst pos (f pos);
init_aux dst (Int.add pos 1) (Int.sub len 1) f
end
in
match Int.le l 0 with
| true => empty
| false =>
let arr:=make l (f 0) in
init_aux arr 1 (Int.sub l 1) f;
arr
end.
Ltac2 make_matrix (sx : int) (sy : int) (v : 'a) :=
let init1 _ := v in
let initr _ := init sy init1 in
init sx initr.
Ltac2 copy a := lowlevel_sub a 0 (length a).
Ltac2 append (a1 : 'a array) (a2 : 'a array) :=
match Int.equal (length a1) 0 with
| true => copy a2
| false => match Int.equal (length a2) 0 with
| true => copy a1
| false =>
let newarr:=make (Int.add (length a1) (length a2)) (get a1 0) in
lowlevel_blit a1 0 newarr 0 (length a1);
lowlevel_blit a2 0 newarr (length a1) (length a2);
newarr
end
end.
Ltac2 sub (a : 'a array) (ofs : int) (len : int) :=
Control.assert_valid_argument "Array.sub ofs<0" (Int.ge ofs 0);
Control.assert_valid_argument "Array.sub len<0" (Int.ge len 0);
Control.assert_bounds "Array.sub" (Int.le ofs (Int.sub (length a) len));
lowlevel_sub a ofs len.
Ltac2 fill (a : 'a array) (ofs : int) (len : int) (v : 'a) :=
Control.assert_valid_argument "Array.fill ofs<0" (Int.ge ofs 0);
Control.assert_valid_argument "Array.fill len<0" (Int.ge len 0);
Control.assert_bounds "Array.fill" (Int.le ofs (Int.sub (length a) len));
lowlevel_fill a ofs len v.
Ltac2 blit (a1 : 'a array) (ofs1 : int) (a2 : 'a array) (ofs2 : int) (len : int) :=
Control.assert_valid_argument "Array.blit ofs1<0" (Int.ge ofs1 0);
Control.assert_valid_argument "Array.blit ofs2<0" (Int.ge ofs2 0);
Control.assert_valid_argument "Array.blit len<0" (Int.ge len 0);
Control.assert_bounds "Array.blit ofs1+len>len a1" (Int.le ofs1 (Int.sub (length a1) len));
Control.assert_bounds "Array.blit ofs2+len>len a2" (Int.le ofs2 (Int.sub (length a2) len));
lowlevel_blit a1 ofs1 a2 ofs2 len.
Ltac2 rec iter_aux (f : 'a -> unit) (a : 'a array) (pos : int) (len : int) :=
match Int.equal len 0 with
| true => ()
| false => f (get a pos); iter_aux f a (Int.add pos 1) (Int.sub len 1)
end.
Ltac2 iter (f : 'a -> unit) (a : 'a array) := iter_aux f a 0 (length a).
Ltac2 rec iter2_aux (f : 'a -> 'b -> unit) (a : 'a array) (b : 'b array) (pos : int) (len : int) :=
match Int.equal len 0 with
| true => ()
| false => f (get a pos) (get b pos); iter2_aux f a b (Int.add pos 1) (Int.sub len 1)
end.
Ltac2 rec iter2 (f : 'a -> 'b -> unit) (a : 'a array) (b : 'b array) :=
Control.assert_valid_argument "Array.iter2" (Int.equal (length a) (length b));
iter2_aux f a b 0 (length a).
Ltac2 map (f : 'a -> 'b) (a : 'a array) :=
init (length a) (fun i => f (get a i)).
Ltac2 map2 (f : 'a -> 'b -> 'c) (a : 'a array) (b : 'b array) :=
Control.assert_valid_argument "Array.map2" (Int.equal (length a) (length b));
init (length a) (fun i => f (get a i) (get b i)).
Ltac2 rec iteri_aux (f : int -> 'a -> unit) (a : 'a array) (pos : int) (len : int) :=
match Int.equal len 0 with
| true => ()
| false => f pos (get a pos); iteri_aux f a (Int.add pos 1) (Int.sub len 1)
end.
Ltac2 iteri (f : int -> 'a -> unit) (a : 'a array) := iteri_aux f a 0 (length a).
Ltac2 mapi (f : int -> 'a -> 'b) (a : 'a array) :=
init (length a) (fun i => f i (get a i)).
Ltac2 rec to_list_aux (a : 'a array) (pos : int) (len : int) :=
match Int.equal len 0 with
| true => []
| false => get a pos :: to_list_aux a (Int.add pos 1) (Int.sub len 1)
end.
Ltac2 to_list (a : 'a array) := to_list_aux a 0 (length a).
Ltac2 rec of_list_aux (ls : 'a list) (dst : 'a array) (pos : int) :=
match ls with
| [] => ()
| hd::tl =>
set dst pos hd;
of_list_aux tl dst (Int.add pos 1)
end.
Ltac2 of_list (ls : 'a list) :=
let rec list_length (ls : 'a list) :=
match ls with
| [] => 0
| _ :: tl => Int.add 1 (list_length tl)
end in
match ls with
| [] => empty
| hd :: _ =>
let anew := make (list_length ls) hd in
of_list_aux ls anew 0;
anew
end.
Ltac2 rec fold_left_aux (f : 'a -> 'b -> 'a) (x : 'a) (a : 'b array) (pos : int) (len : int) :=
match Int.equal len 0 with
| true => x
| false => fold_left_aux f (f x (get a pos)) a (Int.add pos 1) (Int.sub len 1)
end.
Ltac2 fold_left (f : 'a -> 'b -> 'a) (x : 'a) (a : 'b array) : 'a :=
fold_left_aux f x a 0 (length a).
Ltac2 rec fold_right_aux (f : 'a -> 'b -> 'b) (a : 'a array) (x : 'b) (pos : int) (len : int) :=
match Int.equal len 0 with
| true => x
| false => fold_right_aux f a (f (get a pos) x) (Int.sub pos 1) (Int.sub len 1)
end.
Ltac2 fold_right (f : 'a -> 'b -> 'b) (a : 'a array) (x : 'b) : 'b :=
fold_right_aux f a x (Int.sub (length a) 1) (length a).
Ltac2 rec exist_aux (p : 'a -> bool) (a : 'a array) (pos : int) (len : int) :=
match Int.equal len 0 with
| true => false
| false => match p (get a pos) with
| true => true
| false => exist_aux p a (Int.add pos 1) (Int.sub len 1)
end
end.
Ltac2 exist (p : 'a -> bool) (a : 'a array) := exist_aux p a 0 (length a).
Ltac2 rec for_all_aux (p : 'a -> bool) (a : 'a array) (pos : int) (len : int) :=
match Int.equal len 0 with
| true => true
| false => match p (get a pos) with
| true => for_all_aux p a (Int.add pos 1) (Int.sub len 1)
| false => false
end
end.
Ltac2 for_all (p : 'a -> bool) (a : 'a array) := for_all_aux p a 0 (length a).
Ltac2 mem (eq : 'a -> 'a -> bool) (x : 'a) (a : 'a array) :=
exist (eq x) a.
Ltac2 rec for_all2_aux (p : 'a -> 'b -> bool) (a : 'a array) (b : 'b array) (pos : int) (len : int) :=
if Int.equal len 0
then true
else if p (get a pos) (get b pos)
then for_all2_aux p a b (Int.add pos 1) (Int.sub len 1)
else false.
Ltac2 for_all2 p a b :=
let lena := length a in
let lenb := length b in
if Int.equal lena lenb
then for_all2_aux p a b 0 lena
else Control.throw_invalid_argument "Array.for_all2".
Ltac2 equal p a b :=
let lena := length a in
let lenb := length b in
if Int.equal lena lenb
then for_all2_aux p a b 0 lena
else false.
Ltac2 rev (ar : 'a array) : 'a array :=
let len := length ar in
init len (fun i => get ar (Int.sub (Int.sub len i) 1)).