summaryrefslogtreecommitdiff
path: root/theories/Lists/ListTactics.v
blob: 5de2780a80131c8ed94874aad115c29faf1a94c0 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*i $Id: ListTactics.v 13323 2010-07-24 15:57:30Z herbelin $ i*)

Require Import BinPos.
Require Import List.

Ltac list_fold_right fcons fnil l :=
  match l with
  | ?x :: ?tl => fcons x ltac:(list_fold_right fcons fnil tl)
  | nil => fnil
  end.

(* A variant of list_fold_right, to prevent the match of list_fold_right
   from catching errors raised by fcons. *)
Ltac lazy_list_fold_right fcons fnil l :=
  let f :=
    match l with
    | ?x :: ?tl =>
         fun _ =>
         fcons x ltac:(fun _ => lazy_list_fold_right fcons fnil tl)
    | nil => fun _ => fnil()
    end in
  f().

Ltac list_fold_left fcons fnil l :=
  match l with
  | ?x :: ?tl => list_fold_left fcons ltac:(fcons x fnil) tl
  | nil => fnil
  end.

Ltac list_iter f l :=
  match l with
  | ?x :: ?tl => f x; list_iter f tl
  | nil => idtac
  end.

Ltac list_iter_gen seq f l :=
  match l with
  | ?x :: ?tl =>
      let t1 _ := f x in
      let t2 _ := list_iter_gen seq f tl in
      seq t1 t2
  | nil => idtac
  end.

Ltac AddFvTail a l :=
 match l with
 | nil      => constr:(a::nil)
 | a :: _   => l
 | ?x :: ?l => let l' := AddFvTail a l in constr:(x::l')
 end.

Ltac Find_at a l :=
 let rec find n l :=
   match l with
   | nil     => fail 100 "anomaly: Find_at"
   | a :: _  => eval compute in n
   | _ :: ?l => find (Psucc n) l
   end
 in find 1%positive l.

Ltac check_is_list t :=
  match t with
  | _ :: ?l => check_is_list l
  | nil     => idtac
  | _       => fail 100 "anomaly: failed to build a canonical list"
  end.

Ltac check_fv l :=
  check_is_list l;
  match type of l with
  | list _ => idtac
  | _      => fail 100 "anomaly: built an ill-typed list"
  end.