From cd6db46a88eb192b7370308489cd4e2b719df342 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 22 May 2019 17:13:24 -0400 Subject: [Ltac2] Add util files for Bool, List, Option Most functions are taken either from the Coq standard library or the OCaml standard library. One (`enumerate`) is taken from Python. Most names are chosen according to OCaml conventions (as Coq does not have exceptions, and so the OCaml naming conventions already distinguish between option and exception). Since `exists` is a keyword, we use the Coq name `existsb` instead. We generally favor Coq argument ordering when there is a conflict between Coq and OCaml. Note that `seq` matches neither Coq nor OCaml; it takes a `step` argument for how much to increment by on each step. Sorting functions are mostly taken from Coq's mergesort library; it might make sense to replace them with OCaml's versions for efficiency? --- user-contrib/Ltac2/Bool.v | 63 +++++ user-contrib/Ltac2/Init.v | 3 + user-contrib/Ltac2/Int.v | 15 ++ user-contrib/Ltac2/List.v | 606 ++++++++++++++++++++++++++++++++++++++++++++ user-contrib/Ltac2/Option.v | 27 ++ 5 files changed, 714 insertions(+) create mode 100644 user-contrib/Ltac2/Bool.v create mode 100644 user-contrib/Ltac2/List.v create mode 100644 user-contrib/Ltac2/Option.v diff --git a/user-contrib/Ltac2/Bool.v b/user-contrib/Ltac2/Bool.v new file mode 100644 index 0000000000..413746acbd --- /dev/null +++ b/user-contrib/Ltac2/Bool.v @@ -0,0 +1,63 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* y + | false => false + end. + +Ltac2 orb x y := + match x with + | true => true + | false => y + end. + +Ltac2 implb x y := + match x with + | true => y + | false => true + end. + +Ltac2 negb x := + match x with + | true => false + | false => true + end. + +Ltac2 xorb x y := + match x with + | true + => match y with + | true => false + | false => true + end + | false + => match y with + | true => true + | false => false + end + end. + +Ltac2 eqb x y := + match x with + | true + => match y with + | true => true + | false => false + end + | false + => match y with + | true => false + | false => true + end + end. diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v index dc1690bdfb..c47aa82b05 100644 --- a/user-contrib/Ltac2/Init.v +++ b/user-contrib/Ltac2/Init.v @@ -66,5 +66,8 @@ Ltac2 Type exn ::= [ Not_found ]. Ltac2 Type exn ::= [ Match_failure ]. (** Used to signal a pattern didn't match a term. *) +Ltac2 Type exn ::= [ Invalid_argument (message option) ]. +(** Used to signal that an invalid argument was passed to a tactic. *) + Ltac2 Type exn ::= [ Tactic_failure (message option) ]. (** Generic error for tactic failure. *) diff --git a/user-contrib/Ltac2/Int.v b/user-contrib/Ltac2/Int.v index 0a90d757b6..d88f8a70f3 100644 --- a/user-contrib/Ltac2/Int.v +++ b/user-contrib/Ltac2/Int.v @@ -16,3 +16,18 @@ Ltac2 @ external add : int -> int -> int := "ltac2" "int_add". Ltac2 @ external sub : int -> int -> int := "ltac2" "int_sub". Ltac2 @ external mul : int -> int -> int := "ltac2" "int_mul". Ltac2 @ external neg : int -> int := "ltac2" "int_neg". + +Ltac2 lt (x : int) (y : int) := equal (compare x y) -1. +Ltac2 gt (x : int) (y : int) := equal (compare x y) 1. +Ltac2 le (x : int) (y : int) := + (* we might use [lt x (add y 1)], but that has the wrong behavior on MAX_INT *) + match equal x y with + | true => true + | false => lt x y + end. +Ltac2 ge (x : int) (y : int) := + (* we might use [lt (add x 1) y], but that has the wrong behavior on MAX_INT *) + match equal x y with + | true => true + | false => gt x y + end. diff --git a/user-contrib/Ltac2/List.v b/user-contrib/Ltac2/List.v new file mode 100644 index 0000000000..10bef5a9bf --- /dev/null +++ b/user-contrib/Ltac2/List.v @@ -0,0 +1,606 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* 0 + | _ :: xs => Int.add 1 (length xs) + end. + +Ltac2 rec compare_lengths (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] + => match ls2 with + | [] => 0 + | _ :: _ => -1 + end + | _ :: ls1 + => match ls2 with + | [] => 1 + | _ :: ls2 => compare_lengths ls1 ls2 + end + end. + +Ltac2 rec compare_length_with (ls : 'a list) (n : int) := + match Int.lt n 0 with + | true => 1 + | false + => match ls with + | [] => Int.compare 0 n + | _ :: ls => compare_length_with ls (Int.sub n 1) + end + end. + +Ltac2 cons (x : 'a) (xs : 'a list) := + x :: xs. + +Ltac2 hd_opt (ls : 'a list) := + match ls with + | [] => None + | x :: xs => Some x + end. + +Ltac2 hd_default (default : 'a) (ls : 'a list) := + match hd_opt ls with + | Some v => v + | None => default + end. + +Ltac2 hd (ls : 'a list) := + match ls with + | [] => Control.zero (Tactic_failure (Some (Message.of_string "hd"))) + | x :: xs => x + end. + +Ltac2 tl (ls : 'a list) := + match ls with + | [] => [] + | x :: xs => xs + end. + +Ltac2 rec last_opt (ls : 'a list) := + match ls with + | [] => None + | x :: xs + => match xs with + | [] => Some x + | _ :: _ => last_opt xs + end + end. + +Ltac2 last_default (default : 'a) (ls : 'a list) := + match last_opt ls with + | None => default + | Some v => v + end. + +Ltac2 last (ls : 'a list) := + match last_opt ls with + | None => Control.zero (Tactic_failure (Some (Message.of_string "last"))) + | Some v => v + end. + +Ltac2 rec removelast (ls : 'a list) := + match ls with + | [] => [] + | x :: xs + => match xs with + | [] => [] + | _ :: _ => x :: removelast xs + end + end. + +Ltac2 rec nth_opt_aux (ls : 'a list) (n : int) := + match ls with + | [] => None + | x :: xs + => match Int.equal n 0 with + | true => Some x + | false => nth_opt_aux xs (Int.sub n 1) + end + end. + +Ltac2 nth_opt (ls : 'a list) (n : int) := + match Int.lt n 0 with + | true => Control.zero (Invalid_argument (Some (Message.of_string "List.nth"))) + | false => nth_opt_aux ls n + end. + +Ltac2 nth_default (default : 'a) (ls : 'a list) (n : int) := + match nth_opt ls n with + | Some v => v + | None => default + end. + +Ltac2 nth (ls : 'a list) (n : int) := + match nth_opt ls n with + | Some v => v + | None => Control.zero Out_of_bounds + end. + +Ltac2 rec rev_append (l1 : 'a list) (l2 : 'a list) := + match l1 with + | [] => l2 + | a :: l => rev_append l (a :: l2) + end. + +Ltac2 rev l := rev_append l []. + +Ltac2 rec append ls1 ls2 := + match ls1 with + | [] => ls2 + | x :: xs => x :: append xs ls2 + end. + +Ltac2 app ls1 ls2 := append ls1 ls2. + +Ltac2 rec concat (ls : 'a list list) := + match ls with + | [] => [] + | x :: xs => app x (concat xs) + end. +Ltac2 flatten (ls : 'a list list) := concat ls. + +Ltac2 rec iter (f : 'a -> unit) (ls : 'a list) := + match ls with + | [] => () + | l :: ls => f l; iter f ls + end. + +Ltac2 rec iteri_aux (i : int) (f : int -> 'a -> unit) (ls : 'a list) := + match ls with + | [] => () + | l :: ls => f i l; iteri_aux (Int.add i 1) f ls + end. + +Ltac2 iteri (f : int -> 'a -> unit) (ls : 'a list) := + iteri_aux 0 f ls. + +Ltac2 rec map (f : 'a -> 'b) (ls : 'a list) := + match ls with + | [] => [] + | l :: ls => f l :: map f ls + end. + +Ltac2 rec mapi_aux (i : int) (f : int -> 'a -> 'b) (ls : 'a list) := + match ls with + | [] => [] + | l :: ls => f i l :: mapi_aux (Int.add i 1) f ls + end. + +Ltac2 mapi (f : int -> 'a -> 'b) (ls : 'a list) := + mapi_aux 0 f ls. + +Ltac2 rec flat_map (f : 'a -> 'b list) (xs : 'a list) := + match xs with + | [] => [] + | x :: xs => append (f x) (flat_map f xs) + end. + +(* from the OCaml std lib *) +Ltac2 rev_map (f : 'a -> 'b) (ls : 'a list) := + let rec rmap_f accu ls := + match ls with + | [] => accu + | a::l => rmap_f (f a :: accu) l + end in + rmap_f [] ls. + +Ltac2 rec fold_right (f : 'a -> 'b -> 'b) (a : 'b) (ls : 'a list) := + match ls with + | [] => a + | l :: ls => f l (fold_right f a ls) + end. + +Ltac2 rec fold_left (f : 'a -> 'b -> 'a) (xs : 'b list) (a : 'a) := + match xs with + | [] => a + | x :: xs => fold_left f xs (f a x) + end. + +Ltac2 rec iter2 (f : 'a -> 'b -> unit) (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] + => match ls2 with + | [] => () + | _ :: _ => Control.zero (Invalid_argument (Some (Message.of_string "List.iter2"))) + end + | l1 :: ls1 + => match ls2 with + | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.iter2"))) + | l2 :: ls2 + => f l1 l2; iter2 f ls1 ls2 + end + end. + +Ltac2 rec map2 (f : 'a -> 'b -> 'c) (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] + => match ls2 with + | [] => [] + | _ :: _ => Control.zero (Invalid_argument (Some (Message.of_string "List.map2"))) + end + | l1 :: ls1 + => match ls2 with + | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.map2"))) + | l2 :: ls2 + => f l1 l2 :: map2 f ls1 ls2 + end + end. + +(* from the OCaml std lib *) +Ltac2 rev_map2 (f : 'a -> 'b -> 'c) (ls1 : 'a list) (ls2 : 'b list) := + let rec rmap2_f accu ls1 ls2 := + match ls1 with + | [] + => match ls2 with + | [] => accu + | _ :: _ => Control.zero (Invalid_argument (Some (Message.of_string "List.rev_map2"))) + end + | l1 :: ls1 + => match ls2 with + | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.rev_map2"))) + | l2 :: ls2 + => rmap2_f (f l1 l2 :: accu) ls1 ls2 + end + end in + rmap2_f [] ls1 ls2. + +Ltac2 rec fold_right2 (f : 'a -> 'b -> 'c -> 'c) (a : 'c) (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] + => match ls2 with + | [] => a + | _ :: _ => Control.zero (Invalid_argument (Some (Message.of_string "List.fold_right2"))) + end + | l1 :: ls1 + => match ls2 with + | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.fold_right2"))) + | l2 :: ls2 + => f l1 l2 (fold_right2 f a ls1 ls2) + end + end. + +Ltac2 rec fold_left2 (f : 'a -> 'b -> 'c -> 'a) (ls1 : 'b list) (ls2 : 'c list) (a : 'a) := + match ls1 with + | [] + => match ls2 with + | [] => a + | _ :: _ => Control.zero (Invalid_argument (Some (Message.of_string "List.fold_left2"))) + end + | l1 :: ls1 + => match ls2 with + | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.fold_left2"))) + | l2 :: ls2 + => fold_left2 f ls1 ls2 (f a l1 l2) + end + end. + +Ltac2 rec for_all f ls := + match ls with + | [] => true + | x :: xs => match f x with + | true => for_all f xs + | false => false + end + end. + +(* we would call this [exists] a la OCaml's [List.exists], but that's a syntax error, so instead we name it after Coq's [existsb] *) +Ltac2 rec existsb f ls := + match ls with + | [] => false + | x :: xs => match f x with + | true => true + | false => existsb f xs + end + end. +Ltac2 forallb f ls := for_all f ls. + +Ltac2 rec for_all2_aux f f_x f_y xs ys := + match xs with + | [] => for_all f_y ys + | x :: xs' + => match ys with + | [] => for_all f_x xs + | y :: ys' + => match f x y with + | true => for_all2_aux f f_x f_y xs' ys' + | false => false + end + end + end. +Ltac2 for_all2 f xs ys := + let on_different_lengths () := + Control.zero (Invalid_argument (Some (Message.of_string "List.for_all2"))) in + for_all2_aux + f (fun _ => on_different_lengths ()) (fun _ => on_different_lengths ()) + xs ys. +Ltac2 forallb2 f xs ys := for_all2 f xs ys. +Ltac2 rec exists2_aux f f_x f_y xs ys := + match xs with + | [] => existsb f_y ys + | x :: xs' + => match ys with + | [] => existsb f_x xs + | y :: ys' + => match f x y with + | true => true + | false => exists2_aux f f_x f_y xs' ys' + end + end + end. +Ltac2 existsb2 f xs ys := + let on_different_lengths () := + Control.zero (Invalid_argument (Some (Message.of_string "List.existsb2"))) in + exists2_aux + f (fun _ => on_different_lengths ()) (fun _ => on_different_lengths ()) + xs ys. + +Ltac2 rec find_opt f xs := + match xs with + | [] => None + | x :: xs => match f x with + | true => Some x + | false => find_opt f xs + end + end. +Ltac2 rec find f xs := + match find_opt f xs with + | Some v => v + | None => Control.zero Not_found + end. +Ltac2 rec find_rev_opt f xs := + match xs with + | [] => None + | x :: xs => match find_rev_opt f xs with + | Some v => Some v + | None => match f x with + | true => Some x + | false => None + end + end + end. +Ltac2 find_rev f xs := + match find_rev_opt f xs with + | Some v => v + | None => Control.zero Not_found + end. + +Ltac2 mem (eq : 'a -> 'a -> bool) (a : 'a) (ls : 'a list) := + match find_opt (eq a) ls with + | Some _ => true + | None => false + end. + +Ltac2 rec filter f xs := + match xs with + | [] => [] + | x :: xs + => match f x with + | true => x :: filter f xs + | false => filter f xs + end + end. +Ltac2 rec filter_out f xs := + filter (fun x => Bool.negb (f x)) xs. + +Ltac2 find_all (f : 'a -> bool) (ls : 'a list) := filter f ls. + +Ltac2 remove (eqb : 'a -> 'a -> bool) (x : 'a) (ls : 'a list) := + filter_out (eqb x) ls. + +Ltac2 count_occ (eqb : 'a -> 'a -> bool) (x : 'a) (ls : 'a list) := + length (filter (eqb x) ls). + +(* from the Coq stdlib *) +Ltac2 rec list_power (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] => [] :: [] + | x :: t + => flat_map (fun f => map (fun y => (x, y) :: f) ls2) + (list_power t ls2) + end. + +Ltac2 rec partition (f : 'a -> bool) (l : 'a list) := + match l with + | [] => ([], []) + | x :: tl + => let (g, d) := partition f tl in + match f x with + | true => ((x::g), d) + | false => (g, (x::d)) + end + end. + +(* from the Coq stdlib *) +(** [list_prod] has the same signature as [combine], but unlike + [combine], it adds every possible pairs, not only those at the + same position. *) + +Ltac2 rec list_prod (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] => [] + | x :: t + => app (map (fun y => (x, y)) ls2) (list_prod t ls2) + end. + +Ltac2 rec firstn (n : int) (ls : 'a list) := + match Int.lt n 0 with + | true => Control.zero (Invalid_argument (Some (Message.of_string "List.firstn"))) + | false + => match Int.equal n 0 with + | true => [] + | false + => match ls with + | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.firstn"))) + | x :: xs + => x :: firstn (Int.sub n 1) xs + end + end + end. + +Ltac2 rec skipn (n : int) (ls : 'a list) := + match Int.lt n 0 with + | true => Control.zero (Invalid_argument (Some (Message.of_string "List.skipn"))) + | false + => match Int.equal n 0 with + | true => ls + | false + => match ls with + | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.skipn"))) + | x :: xs + => skipn (Int.sub n 1) xs + end + end + end. + +Ltac2 rec nodup (eqb : 'a -> 'a -> bool) (ls : 'a list) := + match ls with + | [] => [] + | x :: xs + => match mem eqb x xs with + | true => nodup eqb xs + | false => x :: nodup eqb xs + end + end. + +(* seq start 1 last = start :: start + 1 :: ... :: (last - 1) *) +Ltac2 rec seq (start : int) (step : int) (last : int) := + match Int.lt (Int.sub last start) step with + | true + => [] + | false + => start :: seq (Int.add start step) step last + end. + +Ltac2 init (len : int) (f : int -> 'a) := + match Int.lt len 0 with + | true => Control.zero (Invalid_argument (Some (Message.of_string "List.init"))) + | false => map f (seq 0 1 len) + end. + +Ltac2 repeat (x : 'a) (n : 'int) := + init n (fun _ => x). + +Ltac2 assoc (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) := + let eq_key kv := let (k', _) := kv in eqk k k' in + let (_, v) := find eq_key l in + v. + +Ltac2 assoc_opt (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) := + let eq_key kv := let (k', _) := kv in eqk k k' in + match find_opt eq_key l with + | Some kv => let (_, v) := kv in Some v + | None => None + end. + +Ltac2 mem_assoc (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) := + let eq_key kv := let (k', _) := kv in eqk k k' in + existsb eq_key l. + +Ltac2 remove_assoc (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) := + let eq_key kv := let (k', _) := kv in eqk k k' in + filter_out eq_key l. + + +Ltac2 rec split (ls : ('a * 'b) list) := + match ls with + | [] => ([], []) + | xy :: tl + => let (x, y) := xy in + let (left, right) := split tl in + ((x::left), (y::right)) + end. +Ltac2 rec combine (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] + => match ls2 with + | [] => [] + | _ :: _ => Control.zero (Invalid_argument (Some (Message.of_string "List.combine"))) + end + | x :: xs + => match ls2 with + | y :: ys + => (x, y) :: combine xs ys + | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.combine"))) + end + end. + +Ltac2 enumerate (ls : 'a list) := + combine (seq 0 1 (length ls)) ls. + +(* from Coq stdlib *) +Ltac2 rec merge (cmp : 'a -> 'a -> int) (l1 : 'a list) (l2 : 'b list) := + let rec merge_aux l2 := + match l1 with + | [] => l2 + | a1 :: l1' + => match l2 with + | [] => l1 + | a2 :: l2' + => match Int.le (cmp a1 a2) 0 with + | true => a1 :: merge cmp l1' l2 + | false => a2 :: merge_aux l2' + end + end + end in + merge_aux l2. + +Ltac2 rec merge_list_to_stack cmp stack l := + match stack with + | [] => [Some l] + | l' :: stack' + => match l' with + | None => Some l :: stack' + | Some l' + => None :: merge_list_to_stack cmp stack' (merge cmp l' l) + end + end. + +Ltac2 rec merge_stack cmp stack := + match stack with + | [] => [] + | l :: stack' + => match l with + | None => merge_stack cmp stack' + | Some l => merge cmp l (merge_stack cmp stack') + end + end. + +Ltac2 rec iter_merge cmp stack l := + match l with + | [] => merge_stack cmp stack + | a::l' => iter_merge cmp (merge_list_to_stack cmp stack [a]) l' + end. + +Ltac2 sort cmp l := iter_merge cmp [] l. + +(* TODO: maybe replace this with a faster implementation *) +Ltac2 sort_uniq (cmp : 'a -> 'a -> int) (l : 'a list) := + let rec uniq l := + match l with + | [] => [] + | x1 :: xs + => match xs with + | [] => x1 :: xs + | x2 :: _ + => match Int.equal (cmp x1 x2) 0 with + | true => uniq xs + | false => x1 :: uniq xs + end + end + end in + uniq (sort cmp l). diff --git a/user-contrib/Ltac2/Option.v b/user-contrib/Ltac2/Option.v new file mode 100644 index 0000000000..0f09a0cc48 --- /dev/null +++ b/user-contrib/Ltac2/Option.v @@ -0,0 +1,27 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* 'b) (x : 'a option) := + match x with + | Some x => Some (f x) + | None => None + end. + +Ltac2 bind (x : 'a option) (f : 'a -> 'b option) := + match x with + | Some x => f x + | None => None + end. + +Ltac2 ret (x : 'a) := Some x. + +Ltac2 lift (f : 'a -> 'b) (x : 'a option) := map f x. -- cgit v1.2.3