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 From 313518aab118dfdd6f559b5a0fc431e4e6740fdd Mon Sep 17 00:00:00 2001 From: Michael Soegtrop Date: Sun, 16 Jun 2019 09:48:20 +0200 Subject: - added OCaml copyright header to List.v (if for no other reason than out of courtesy) - index errors (negative or out of bounds) generally throw (panic) - hd, last, find backtrack, because here backtracking can actually be useful added a _throw variant to these functions which panics This emaphasizes the difference between backtracking and throwing exceptions, which doesn't exist in OCaml. - simplified the implementation of for_all2 and exist2 (ok, that is a matter of taste ...) - added assertions which combine a boolean match with a throw. This makes the code more readable and makes it easier to have more specific error messages. - added a lastn function - gave Out_of_bounds a message argument (there is no good reason why invalid_argument has one and this not) All other exceptions without message argument are quite specific to certain functions (like Not_Found) --- user-contrib/Ltac2/Control.v | 26 ++++++ user-contrib/Ltac2/Init.v | 2 +- user-contrib/Ltac2/List.v | 192 +++++++++++++++++++++++++------------------ 3 files changed, 140 insertions(+), 80 deletions(-) mode change 100644 => 100755 user-contrib/Ltac2/Init.v diff --git a/user-contrib/Ltac2/Control.v b/user-contrib/Ltac2/Control.v index 071c2ea8ce..6068dd20cb 100644 --- a/user-contrib/Ltac2/Control.v +++ b/user-contrib/Ltac2/Control.v @@ -7,6 +7,7 @@ (************************************************************************) Require Import Ltac2.Init. +Require Ltac2.Message. (** Panic *) @@ -74,3 +75,28 @@ Ltac2 @ external abstract : ident option -> (unit -> unit) -> unit := "ltac2" "a Ltac2 @ external check_interrupt : unit -> unit := "ltac2" "check_interrupt". (** For internal use. *) + +(** Assertions throwing exceptions and short form throws *) + +Ltac2 throw_invalid_argument (msg : string) := + Control.throw (Invalid_argument (Some (Message.of_string msg))). + +Ltac2 throw_out_of_bounds (msg : string) := + Control.throw (Out_of_bounds (Some (Message.of_string msg))). + +Ltac2 assert_valid_argument (msg : string) (test : bool) := + match test with + | true => () + | false => throw_invalid_argument msg + end. + +Ltac2 assert_bounds (msg : string) (test : bool) := + match test with + | true => () + | false => throw_out_of_bounds msg + end. + +(** Short form backtracks *) + +Ltac2 backtrack_tactic_failure (msg : string) := + Control.zero (Tactic_failure (Some (Message.of_string msg))). diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v old mode 100644 new mode 100755 index c47aa82b05..5c51c798c1 --- a/user-contrib/Ltac2/Init.v +++ b/user-contrib/Ltac2/Init.v @@ -51,7 +51,7 @@ Ltac2 Type err. Ltac2 Type exn ::= [ Internal (err) ]. (** Wrapper around the errors raised by Coq implementation. *) -Ltac2 Type exn ::= [ Out_of_bounds ]. +Ltac2 Type exn ::= [ Out_of_bounds (message option) ]. (** Used for bound checking, e.g. with String and Array. *) Ltac2 Type exn ::= [ Not_focussed ]. diff --git a/user-contrib/Ltac2/List.v b/user-contrib/Ltac2/List.v index 10bef5a9bf..07505d7d54 100644 --- a/user-contrib/Ltac2/List.v +++ b/user-contrib/Ltac2/List.v @@ -8,6 +8,23 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(* The interface is an extended version of OCaml stdlib/list.ml. *) + +(**************************************************************************) +(* *) +(* OCaml *) +(* *) +(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *) +(* *) +(* Copyright 1996 Institut National de Recherche en Informatique et *) +(* en Automatique. *) +(* *) +(* All rights reserved. This file is distributed under the terms of *) +(* the GNU Lesser General Public License version 2.1, with the *) +(* special exception on linking described in the file LICENSE. *) +(* *) +(**************************************************************************) + Require Import Ltac2.Init. Require Ltac2.Int. Require Ltac2.Control. @@ -47,6 +64,10 @@ Ltac2 rec compare_length_with (ls : 'a list) (n : int) := Ltac2 cons (x : 'a) (xs : 'a list) := x :: xs. +(* Since Ltac-2 distinguishes between backtracking and fatal exceptions, + we provide option and default variants of functions which throw in the + OCaml stdlib. *) + Ltac2 hd_opt (ls : 'a list) := match ls with | [] => None @@ -59,9 +80,15 @@ Ltac2 hd_default (default : 'a) (ls : 'a list) := | None => default end. +Ltac2 hd_throw (ls : 'a list) := + match ls with + | [] => Control.throw_invalid_argument "List.hd" + | x :: xs => x + end. + Ltac2 hd (ls : 'a list) := match ls with - | [] => Control.zero (Tactic_failure (Some (Message.of_string "hd"))) + | [] => Control.backtrack_tactic_failure "List.hd" | x :: xs => x end. @@ -87,9 +114,15 @@ Ltac2 last_default (default : 'a) (ls : 'a list) := | Some v => v end. +Ltac2 last_throw (ls : 'a list) := + match last_opt ls with + | None => Control.throw_invalid_argument "List.last" + | Some v => v + end. + Ltac2 last (ls : 'a list) := match last_opt ls with - | None => Control.zero (Tactic_failure (Some (Message.of_string "last"))) + | None => Control.backtrack_tactic_failure "List.last" | Some v => v end. @@ -114,10 +147,8 @@ Ltac2 rec nth_opt_aux (ls : 'a list) (n : int) := 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. + Control.assert_valid_argument "List.nth" (Int.ge n 0); + nth_opt_aux ls n. Ltac2 nth_default (default : 'a) (ls : 'a list) (n : int) := match nth_opt ls n with @@ -128,7 +159,7 @@ Ltac2 nth_default (default : 'a) (ls : 'a list) (n : int) := Ltac2 nth (ls : 'a list) (n : int) := match nth_opt ls n with | Some v => v - | None => Control.zero Out_of_bounds + | None => Control.throw_out_of_bounds "List.nth" end. Ltac2 rec rev_append (l1 : 'a list) (l2 : 'a list) := @@ -145,13 +176,12 @@ Ltac2 rec append ls1 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) + | x :: xs => append x (concat xs) end. + Ltac2 flatten (ls : 'a list list) := concat ls. Ltac2 rec iter (f : 'a -> unit) (ls : 'a list) := @@ -216,11 +246,11 @@ Ltac2 rec iter2 (f : 'a -> 'b -> unit) (ls1 : 'a list) (ls2 : 'b list) := | [] => match ls2 with | [] => () - | _ :: _ => Control.zero (Invalid_argument (Some (Message.of_string "List.iter2"))) + | _ :: _ => Control.throw_invalid_argument "List.iter2" end | l1 :: ls1 => match ls2 with - | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.iter2"))) + | [] => Control.throw_invalid_argument "List.iter2" | l2 :: ls2 => f l1 l2; iter2 f ls1 ls2 end @@ -231,11 +261,11 @@ Ltac2 rec map2 (f : 'a -> 'b -> 'c) (ls1 : 'a list) (ls2 : 'b list) := | [] => match ls2 with | [] => [] - | _ :: _ => Control.zero (Invalid_argument (Some (Message.of_string "List.map2"))) + | _ :: _ => Control.throw_invalid_argument "List.map2" end | l1 :: ls1 => match ls2 with - | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.map2"))) + | [] => Control.throw_invalid_argument "List.map2" | l2 :: ls2 => f l1 l2 :: map2 f ls1 ls2 end @@ -248,11 +278,11 @@ Ltac2 rev_map2 (f : 'a -> 'b -> 'c) (ls1 : 'a list) (ls2 : 'b list) := | [] => match ls2 with | [] => accu - | _ :: _ => Control.zero (Invalid_argument (Some (Message.of_string "List.rev_map2"))) + | _ :: _ => Control.throw_invalid_argument "List.rev_map2" end | l1 :: ls1 => match ls2 with - | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.rev_map2"))) + | [] => Control.throw_invalid_argument "List.rev_map2" | l2 :: ls2 => rmap2_f (f l1 l2 :: accu) ls1 ls2 end @@ -264,11 +294,11 @@ Ltac2 rec fold_right2 (f : 'a -> 'b -> 'c -> 'c) (a : 'c) (ls1 : 'a list) (ls2 : | [] => match ls2 with | [] => a - | _ :: _ => Control.zero (Invalid_argument (Some (Message.of_string "List.fold_right2"))) + | _ :: _ => Control.throw_invalid_argument "List.fold_right2" end | l1 :: ls1 => match ls2 with - | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.fold_right2"))) + | [] => Control.throw_invalid_argument "List.fold_right2" | l2 :: ls2 => f l1 l2 (fold_right2 f a ls1 ls2) end @@ -279,11 +309,11 @@ Ltac2 rec fold_left2 (f : 'a -> 'b -> 'c -> 'a) (ls1 : 'b list) (ls2 : 'c list) | [] => match ls2 with | [] => a - | _ :: _ => Control.zero (Invalid_argument (Some (Message.of_string "List.fold_left2"))) + | _ :: _ => Control.throw_invalid_argument "List.fold_left2" end | l1 :: ls1 => match ls2 with - | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.fold_left2"))) + | [] => Control.throw_invalid_argument "List.fold_left2" | l2 :: ls2 => fold_left2 f ls1 ls2 (f a l1 l2) end @@ -298,56 +328,49 @@ Ltac2 rec for_all f ls := 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 := +(* we would call this [exists] a la OCaml's [List.exists], but that's a syntax error, so instead we name it exist *) +Ltac2 rec exist f ls := match ls with | [] => false | x :: xs => match f x with | true => true - | false => existsb f xs + | false => exist f xs end end. -Ltac2 forallb f ls := for_all f ls. -Ltac2 rec for_all2_aux f f_x f_y xs ys := +Ltac2 rec for_all2 f xs ys := match xs with - | [] => for_all f_y ys + | [] => match ys with + | [] => true + | y :: ys' => Control.throw_invalid_argument "List.for_all2" + end | x :: xs' => match ys with - | [] => for_all f_x xs + | [] => Control.throw_invalid_argument "List.for_all2" | y :: ys' => match f x y with - | true => for_all2_aux f f_x f_y xs' ys' + | true => for_all2 f 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 := + +Ltac2 rec exist2 f xs ys := match xs with - | [] => existsb f_y ys + | [] => match ys with + | [] => false + | y :: ys' => Control.throw_invalid_argument "List.exist2" + end | x :: xs' => match ys with - | [] => existsb f_x xs + | [] => Control.throw_invalid_argument "List.exist2" | y :: ys' => match f x y with | true => true - | false => exists2_aux f f_x f_y xs' ys' + | false => exist2 f 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 @@ -357,11 +380,19 @@ Ltac2 rec find_opt f xs := | false => find_opt f xs end end. -Ltac2 rec find f xs := + +Ltac2 find_throw f xs := + match find_opt f xs with + | Some v => v + | None => Control.throw Not_found + end. + +Ltac2 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 @@ -373,6 +404,13 @@ Ltac2 rec find_rev_opt f xs := end end end. + +Ltac2 find_rev_throw f xs := + match find_rev_opt f xs with + | Some v => v + | None => Control.throw Not_found + end. + Ltac2 find_rev f xs := match find_rev_opt f xs with | Some v => v @@ -380,10 +418,7 @@ Ltac2 find_rev f xs := end. Ltac2 mem (eq : 'a -> 'a -> bool) (a : 'a) (ls : 'a list) := - match find_opt (eq a) ls with - | Some _ => true - | None => false - end. + exist (eq a) ls. Ltac2 rec filter f xs := match xs with @@ -394,6 +429,7 @@ Ltac2 rec filter f xs := | false => filter f xs end end. + Ltac2 rec filter_out f xs := filter (fun x => Bool.negb (f x)) xs. @@ -434,39 +470,39 @@ 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) + => append (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"))) + Control.assert_valid_argument "List.firstn" (Int.ge n 0); + match Int.equal n 0 with + | true => [] | 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 + => match ls with + | [] => Control.throw_out_of_bounds "List.firstn" + | x :: xs + => x :: firstn (Int.sub n 1) xs 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"))) + Control.assert_valid_argument "List.skipn" (Int.ge n 0); + match Int.equal n 0 with + | true => ls | 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 + => match ls with + | [] => Control.throw_out_of_bounds "List.skipn" + | x :: xs + => skipn (Int.sub n 1) xs end end. +Ltac2 lastn (n : int) (ls : 'a list) := + let l := length ls in + Control.assert_valid_argument "List.lastn" (Int.ge n 0); + Control.assert_bounds "List.lastn" (Int.le n l); + skipn (Int.sub l n). + Ltac2 rec nodup (eqb : 'a -> 'a -> bool) (ls : 'a list) := match ls with | [] => [] @@ -487,10 +523,8 @@ Ltac2 rec seq (start : int) (step : int) (last : int) := 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. + Control.assert_valid_argument "List.init" (Int.ge len 0); + map f (seq 0 1 len). Ltac2 repeat (x : 'a) (n : 'int) := init n (fun _ => x). @@ -509,13 +543,12 @@ Ltac2 assoc_opt (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) := 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. + exist 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 | [] => ([], []) @@ -524,18 +557,19 @@ Ltac2 rec split (ls : ('a * 'b) list) := 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"))) + | _ :: _ => Control.throw_invalid_argument "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"))) + | [] => Control.throw_invalid_argument "List.combine" end end. -- cgit v1.2.3 From 01d0b60694e3b4ee810bdde7115b40e49355ac24 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop Date: Tue, 18 Jun 2019 21:01:27 +0200 Subject: Removed "b" from function names in Bool.v Changed year in headers --- user-contrib/Ltac2/Bool.v | 14 +++++++------- user-contrib/Ltac2/List.v | 4 ++-- user-contrib/Ltac2/Option.v | 2 +- 3 files changed, 10 insertions(+), 10 deletions(-) mode change 100644 => 100755 user-contrib/Ltac2/Bool.v diff --git a/user-contrib/Ltac2/Bool.v b/user-contrib/Ltac2/Bool.v old mode 100644 new mode 100755 index 413746acbd..d808436e13 --- a/user-contrib/Ltac2/Bool.v +++ b/user-contrib/Ltac2/Bool.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* y | false => false end. -Ltac2 orb x y := +Ltac2 or x y := match x with | true => true | false => y end. -Ltac2 implb x y := +Ltac2 impl x y := match x with | true => y | false => true end. -Ltac2 negb x := +Ltac2 neg x := match x with | true => false | false => true end. -Ltac2 xorb x y := +Ltac2 xor x y := match x with | true => match y with @@ -48,7 +48,7 @@ Ltac2 xorb x y := end end. -Ltac2 eqb x y := +Ltac2 eq x y := match x with | true => match y with diff --git a/user-contrib/Ltac2/List.v b/user-contrib/Ltac2/List.v index 07505d7d54..3783618cb1 100644 --- a/user-contrib/Ltac2/List.v +++ b/user-contrib/Ltac2/List.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* Bool.negb (f x)) xs. + filter (fun x => Bool.neg (f x)) xs. Ltac2 find_all (f : 'a -> bool) (ls : 'a list) := filter f ls. diff --git a/user-contrib/Ltac2/Option.v b/user-contrib/Ltac2/Option.v index 0f09a0cc48..af0b7c28ca 100644 --- a/user-contrib/Ltac2/Option.v +++ b/user-contrib/Ltac2/Option.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* Some x end. -Ltac2 hd_default (default : 'a) (ls : 'a list) := - match hd_opt ls with - | Some v => v - | None => default - end. - -Ltac2 hd_throw (ls : 'a list) := - match ls with - | [] => Control.throw_invalid_argument "List.hd" - | x :: xs => x - end. - Ltac2 hd (ls : 'a list) := match ls with - | [] => Control.backtrack_tactic_failure "List.hd" + | [] => Control.throw_invalid_argument "List.hd" | x :: xs => x end. @@ -108,21 +96,9 @@ Ltac2 rec last_opt (ls : 'a list) := end end. -Ltac2 last_default (default : 'a) (ls : 'a list) := - match last_opt ls with - | None => default - | Some v => v - end. - -Ltac2 last_throw (ls : 'a list) := - match last_opt ls with - | None => Control.throw_invalid_argument "List.last" - | Some v => v - end. - Ltac2 last (ls : 'a list) := match last_opt ls with - | None => Control.backtrack_tactic_failure "List.last" + | None => Control.throw_invalid_argument "List.last" | Some v => v end. @@ -150,12 +126,6 @@ Ltac2 nth_opt (ls : 'a list) (n : int) := Control.assert_valid_argument "List.nth" (Int.ge n 0); nth_opt_aux ls n. -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 @@ -381,16 +351,10 @@ Ltac2 rec find_opt f xs := end end. -Ltac2 find_throw f xs := - match find_opt f xs with - | Some v => v - | None => Control.throw Not_found - end. - Ltac2 find f xs := match find_opt f xs with | Some v => v - | None => Control.zero Not_found + | None => Control.throw Not_found end. Ltac2 rec find_rev_opt f xs := @@ -405,16 +369,10 @@ Ltac2 rec find_rev_opt f xs := end end. -Ltac2 find_rev_throw f xs := - match find_rev_opt f xs with - | Some v => v - | None => Control.throw Not_found - end. - Ltac2 find_rev f xs := match find_rev_opt f xs with | Some v => v - | None => Control.zero Not_found + | None => Control.throw Not_found end. Ltac2 mem (eq : 'a -> 'a -> bool) (a : 'a) (ls : 'a list) := diff --git a/user-contrib/Ltac2/Option.v b/user-contrib/Ltac2/Option.v index af0b7c28ca..584d84ddb5 100644 --- a/user-contrib/Ltac2/Option.v +++ b/user-contrib/Ltac2/Option.v @@ -8,14 +8,47 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(* Some of the below functions are inspired by ocaml-extlib *) + Require Import Ltac2.Init. +Require Import Ltac2.Control. -Ltac2 map (f : 'a -> 'b) (x : 'a option) := - match x with - | Some x => Some (f x) +Ltac2 may (f : 'a -> unit) (ov : 'a option) := + match ov with + | Some v => f v + | None => () + end. + +Ltac2 map (f : 'a -> 'b) (ov : 'a option) := + match ov with + | Some v => Some (f v) | None => None end. +Ltac2 default (def : 'a) (ov : 'a option) := + match ov with + | Some v => v + | None => def + end. + +Ltac2 map_default (f : 'a -> 'b) (def : 'b) (ov : 'a option) := + match ov with + | Some v => f v + | None => def + end. + +Ltac2 get (ov : 'a option) := + match ov with + | Some v => v + | None => Control.throw No_value + end. + +Ltac2 get_bt (ov : 'a option) := + match ov with + | Some v => v + | None => Control.zero No_value + end. + Ltac2 bind (x : 'a option) (f : 'a -> 'b option) := match x with | Some x => f x -- cgit v1.2.3