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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Locus
(** Utilities on occurrences *)
let occurrences_map f = function
| OnlyOccurrences l ->
let l' = f l in
if l' = [] then NoOccurrences else OnlyOccurrences l'
| AllOccurrencesBut l ->
let l' = f l in
if l' = [] then AllOccurrences else AllOccurrencesBut l'
| (NoOccurrences|AllOccurrences) as o -> o
let convert_occs = function
| AllOccurrences -> (false,[])
| AllOccurrencesBut l -> (false,l)
| NoOccurrences -> (true,[])
| OnlyOccurrences l -> (true,l)
let is_selected occ = function
| AllOccurrences -> true
| AllOccurrencesBut l -> not (Int.List.mem occ l)
| OnlyOccurrences l -> Int.List.mem occ l
| NoOccurrences -> false
(** Usual clauses *)
let allHypsAndConcl = { onhyps=None; concl_occs=AllOccurrences }
let allHyps = { onhyps=None; concl_occs=NoOccurrences }
let onConcl = { onhyps=Some[]; concl_occs=AllOccurrences }
let nowhere = { onhyps=Some[]; concl_occs=NoOccurrences }
let onHyp h =
{ onhyps=Some[(AllOccurrences,h),InHyp]; concl_occs=NoOccurrences }
let is_nowhere = function
| { onhyps=Some[]; concl_occs=NoOccurrences } -> true
| _ -> false
(** Clause conversion functions, parametrized by a hyp enumeration function *)
(** From [clause] to [simple_clause] *)
let simple_clause_of enum_hyps cl =
let error_occurrences () =
Errors.error "This tactic does not support occurrences selection" in
let error_body_selection () =
Errors.error "This tactic does not support body selection" in
let hyps =
match cl.onhyps with
| None ->
List.map Option.make (enum_hyps ())
| Some l ->
List.map (fun ((occs,id),w) ->
if occs <> AllOccurrences then error_occurrences ();
if w = InHypValueOnly then error_body_selection ();
Some id) l in
if cl.concl_occs = NoOccurrences then hyps
else
if cl.concl_occs <> AllOccurrences then error_occurrences ()
else None :: hyps
(** From [clause] to [concrete_clause] *)
let concrete_clause_of enum_hyps cl =
let hyps =
match cl.onhyps with
| None ->
let f id = OnHyp (id,AllOccurrences,InHyp) in
List.map f (enum_hyps ())
| Some l ->
List.map (fun ((occs,id),w) -> OnHyp (id,occs,w)) l in
if cl.concl_occs = NoOccurrences then hyps
else
OnConcl cl.concl_occs :: hyps
(** Miscellaneous functions *)
let out_arg = function
| Misctypes.ArgVar _ -> Errors.anomaly (Pp.str "Unevaluated or_var variable")
| Misctypes.ArgArg x -> x
let occurrences_of_hyp id cls =
let rec hyp_occ = function
[] -> NoOccurrences, InHyp
| ((occs,id'),hl)::_ when Names.Id.equal id id' ->
occurrences_map (List.map out_arg) occs, hl
| _::l -> hyp_occ l in
match cls.onhyps with
None -> AllOccurrences,InHyp
| Some l -> hyp_occ l
let occurrences_of_goal cls =
occurrences_map (List.map out_arg) cls.concl_occs
let in_every_hyp cls = Option.is_empty cls.onhyps
let clause_with_generic_occurrences cls =
let hyps = match cls.onhyps with
| None -> true
| Some hyps ->
List.for_all
(function ((AllOccurrences,_),_) -> true | _ -> false) hyps in
let concl = match cls.concl_occs with
| AllOccurrences | NoOccurrences -> true
| _ -> false in
hyps && concl
let clause_with_generic_context_selection cls =
let hyps = match cls.onhyps with
| None -> true
| Some hyps ->
List.for_all
(function ((AllOccurrences,_),InHyp) -> true | _ -> false) hyps in
let concl = match cls.concl_occs with
| AllOccurrences | NoOccurrences -> true
| _ -> false in
hyps && concl
|
