locus.mli for occurrences+clauses, misctypes.mli for various little things

 Corresponding operations in locusops.ml and miscops.ml

 The type of occurrences is now a clear algebraic one instead of
 a bool*list hard to understand.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 81 insertions, 0 deletions

diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
new file mode 100644
index 000000000..5f136c536
--- /dev/null
+++ b/pretyping/locusops.ml
@@ -0,0 +1,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        *)
+(************************************************************************)
+
+open Names
+open Misctypes
+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 (List.mem occ l)
+  | OnlyOccurrences l -> 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 }
+
+
+(** 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