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

11 files changed, 34 insertions, 65 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 2e74b809f..d45e6b9b3 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -28,6 +28,8 @@ open Nametab
 open Notation
 open Reserve
 open Detyping
+open Misctypes
+open Decl_kinds
 (*i*)
 
 (* Translation from glob_constr to front constr *)
@@ -218,7 +220,7 @@ let rec check_same_type ty1 ty2 =
   | CHole _, CHole _ -> ()
   | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> ()
   | CSort(_,s1), CSort(_,s2) when s1=s2 -> ()
-  | CCast(_,a1,CastConv (_,b1)), CCast(_,a2, CastConv(_,b2)) ->
+  | CCast(_,a1,(CastConv b1|CastVM b1)), CCast(_,a2,(CastConv b2|CastVM b2)) ->
       check_same_type a1 a2;
       check_same_type b1 b2
   | CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) ->
@@ -644,7 +646,8 @@ let extern_optimal_prim_token scopes r r' =
 (* mapping glob_constr to constr_expr                                    *)
 
 let extern_glob_sort = function
-  | GProp _ as s -> s
+  | GProp -> GProp
+  | GSet -> GSet
   | GType (Some _) as s when !print_universes -> s
   | GType _ -> GType None
 
@@ -811,10 +814,9 @@ let rec extern inctx scopes vars r =
 
   | GHole (loc,e) -> CHole (loc, Some e)
 
-  | GCast (loc,c, CastConv (k,t)) ->
-      CCast (loc,sub_extern true scopes vars c, CastConv (k,extern_typ scopes vars t))
-  | GCast (loc,c, CastCoerce) ->
-      CCast (loc,sub_extern true scopes vars c, CastCoerce)
+  | GCast (loc,c, c') ->
+      CCast (loc,sub_extern true scopes vars c,
+	     Miscops.map_cast_type (extern_typ scopes vars) c')
 
 and extern_typ (_,scopes) =
   extern true (Some Notation.type_scope,scopes)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index c112506ab..21c33f3f3 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -18,6 +18,7 @@ open Glob_term
 open Pattern
 open Topconstr
 open Notation
+open Misctypes
 
 val check_same_type : constr_expr -> constr_expr -> unit
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index af48a37c9..4467cf9f2 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -23,6 +23,8 @@ open Topconstr
 open Nametab
 open Notation
 open Inductiveops
+open Misctypes
+open Decl_kinds
 
 (** constr_expr -> glob_constr translation:
     - it adds holes for implicit arguments
@@ -1516,10 +1518,8 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	GEvar (loc, n, Option.map (List.map (intern env)) l)
     | CSort (loc, s) ->
 	GSort(loc,s)
-    | CCast (loc, c1, CastConv (k, c2)) ->
-	GCast (loc,intern env c1, CastConv (k, intern_type env c2))
-    | CCast (loc, c1, CastCoerce) ->
-	GCast (loc,intern env c1, CastCoerce)
+    | CCast (loc, c1, c2) ->
+	GCast (loc,intern env c1, Miscops.map_cast_type (intern_type env) c2)
 
   and intern_type env = intern (set_type_scope env)
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 7d0009021..b1bc63658 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -17,6 +17,8 @@ open Pattern
 open Topconstr
 open Termops
 open Pretyping
+open Misctypes
+open Decl_kinds
 
 (** Translation from front abstract syntax of term to untyped terms (glob_constr) *)
 
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 0d640640b..3597879de 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -16,6 +16,7 @@ open Glob_term
 open Topconstr
 open Term
 open Evd
+open Misctypes
 
 type argument_type =
   (* Basic types *)
@@ -43,11 +44,6 @@ type argument_type =
   | PairArgType of argument_type * argument_type
   | ExtraArgType of string
 
-type 'a and_short_name = 'a * identifier located option
-type 'a or_by_notation =
-  | AN of 'a
-  | ByNotation of (loc * string * Notation.delimiters option)
-
 let loc_of_or_by_notation f = function
   | AN c -> f c
   | ByNotation (loc,s,_) -> loc
@@ -68,16 +64,6 @@ type rlevel
 type glevel
 type tlevel
 
-type intro_pattern_expr =
-  | IntroOrAndPattern of or_and_intro_pattern_expr
-  | IntroWildcard
-  | IntroRewrite of bool
-  | IntroIdentifier of identifier
-  | IntroFresh of identifier
-  | IntroForthcoming of bool
-  | IntroAnonymous
-and or_and_intro_pattern_expr = (loc * intro_pattern_expr) list list
-
 let rec pr_intro_pattern (_,pat) = match pat with
   | IntroOrAndPattern pll -> pr_or_and_intro_pattern pll
   | IntroWildcard -> str "_"
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 540fc400c..0368e99e0 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -16,12 +16,7 @@ open Pattern
 open Topconstr
 open Term
 open Evd
-
-type 'a and_short_name = 'a * identifier located option
-
-type 'a or_by_notation =
-  | AN of 'a
-  | ByNotation of (loc * string * Notation.delimiters option)
+open Misctypes
 
 val loc_of_or_by_notation : ('a -> loc) -> 'a or_by_notation -> loc
 
@@ -37,16 +32,6 @@ type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
 
 type 'a with_ebindings = 'a * open_constr bindings
 
-type intro_pattern_expr =
-  | IntroOrAndPattern of or_and_intro_pattern_expr
-  | IntroWildcard
-  | IntroRewrite of bool
-  | IntroIdentifier of identifier
-  | IntroFresh of identifier
-  | IntroForthcoming of bool
-  | IntroAnonymous
-and or_and_intro_pattern_expr = (loc * intro_pattern_expr) list list
-
 val pr_intro_pattern : intro_pattern_expr located -> Pp.std_ppcmds
 val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds
 
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index e92699f64..3384d79a5 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -25,6 +25,7 @@ open Typeclasses_errors
 open Pp
 open Libobject
 open Nameops
+open Misctypes
 (*i*)
 
 let generalizable_table = ref Idpred.empty
@@ -182,7 +183,7 @@ let generalizable_vars_of_glob_constr ?(bound=Idset.empty) ?(allowed=Idset.empty
 	in
 	array_fold_left_i vars_fix vs idl
     | GCast (loc,c,k) -> let v = vars bound vs c in
-	(match k with CastConv (_,t) -> vars bound v t | _ -> v)
+	(match k with CastConv t | CastVM t -> vars bound v t | _ -> v)
     | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
 
   and vars_pattern bound vs (loc,idl,p,c) =
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 043c255a4..66efe5982 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -17,7 +17,7 @@ open Errors
 open Util
 open Names
 open Libnames
-open Genarg
+open Misctypes
 open Syntax_def
 open Topconstr
 
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 0c7bc6157..b4e121b4b 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -9,7 +9,7 @@
 open Pp
 open Names
 open Libnames
-open Genarg
+open Misctypes
 
 (** [locate_global_with_alias] locates global reference possibly following
    a notation if this notation has a role of aliasing; raise Not_found
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 1a86170f3..d3773305a 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -16,6 +16,8 @@ open Libnames
 open Glob_term
 open Term
 open Mod_subst
+open Misctypes
+open Decl_kinds
 (*i*)
 
 (**********************************************************************)
@@ -148,10 +150,7 @@ let glob_constr_of_aconstr_with_binders loc g f e = function
 	  (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
       let e',idl = array_fold_map (to_id g) e idl in
       GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
-  | ACast (c,k) -> GCast (loc,f e c,
-			  match k with
-			    | CastConv (k,t) -> CastConv (k,f e t)
-			    | CastCoerce -> CastCoerce)
+  | ACast (c,k) -> GCast (loc,f e c, Miscops.map_cast_type (f e) k)
   | ASort x -> GSort (loc,x)
   | AHole x  -> GHole (loc,x)
   | APatVar n -> GPatVar (loc,(false,n))
@@ -315,9 +314,7 @@ let aconstr_and_vars_of_glob_constr a =
 	   error "Binders marked as implicit not allowed in notations.";
 	 add_name found na; (na,Option.map aux oc,aux b))) dll in
       ARec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
-  | GCast (_,c,k) -> ACast (aux c,
-			    match k with CastConv (k,t) -> CastConv (k,aux t)
-			      | CastCoerce -> CastCoerce)
+  | GCast (_,c,k) -> ACast (aux c,Miscops.map_cast_type aux k)
   | GSort (_,s) -> ASort s
   | GHole (_,w) -> AHole w
   | GRef (_,r) -> ARef r
@@ -495,16 +492,9 @@ let rec subst_aconstr subst bound raw =
 	  |Evar_kinds.ImpossibleCase |Evar_kinds.MatchingVar _) -> raw
 
   | ACast (r1,k) ->
-      match k with
-	  CastConv (k, r2) ->
-	    let r1' = subst_aconstr subst bound r1
-	    and r2' = subst_aconstr subst bound r2 in
-	      if r1' == r1 && r2' == r2 then raw else
-		ACast (r1',CastConv (k,r2'))
-	| CastCoerce ->
-	    let r1' = subst_aconstr subst bound r1 in
-	      if r1' == r1 then raw else
-		ACast (r1',CastCoerce)
+      let r1' = subst_aconstr subst bound r1 in
+      let k' = Miscops.smartmap_cast_type (subst_aconstr subst bound) k in
+      if r1' == r1 && k' == k then raw else ACast(r1',k')
 
 let subst_interpretation subst (metas,pat) =
   let bound = List.map fst metas in
@@ -728,7 +718,8 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
       let alp,sigma = array_fold_right2 (fun id1 id2 alsig ->
 	match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in
       array_fold_left2 (match_in u alp metas) sigma bl1 bl2
-  | GCast(_,c1, CastConv(_,t1)), ACast(c2, CastConv (_,t2)) ->
+  | GCast(_,c1,CastConv t1), ACast (c2,CastConv t2)
+  | GCast(_,c1,CastVM t1), ACast (c2,CastVM t2) ->
       match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2
   | GCast(_,c1, CastCoerce), ACast(c2, CastCoerce) ->
       match_in u alp metas sigma c1 c2
@@ -1079,7 +1070,7 @@ let fold_constr_expr_with_binders g f n acc = function
   | CApp (loc,(_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
   | CProdN (_,l,b) | CLambdaN (_,l,b) -> fold_constr_expr_binders g f n acc b l
   | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],default_binder_kind,a]
-  | CCast (loc,a,CastConv(_,b)) -> f n (f n acc a) b
+  | CCast (loc,a,(CastConv b|CastVM b)) -> f n (f n acc a) b
   | CCast (loc,a,CastCoerce) -> f n acc a
   | CNotation (_,_,(l,ll,bll)) ->
       (* The following is an approximation: we don't know exactly if
@@ -1236,8 +1227,7 @@ let map_constr_expr_with_binders g f e = function
   | CLambdaN (loc,bl,b) ->
       let (e,bl) = map_binders f g e bl in CLambdaN (loc,bl,f e b)
   | CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b)
-  | CCast (loc,a,CastConv (k,b)) -> CCast (loc,f e a,CastConv(k, f e b))
-  | CCast (loc,a,CastCoerce) -> CCast (loc,f e a,CastCoerce)
+  | CCast (loc,a,c) -> CCast (loc,f e a, Miscops.map_cast_type (f e) c)
   | CNotation (loc,n,(l,ll,bll)) ->
       (* This is an approximation because we don't know what binds what *)
       CNotation (loc,n,(List.map (f e) l,List.map (List.map (f e)) ll,
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 48871432e..101c39eea 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -13,6 +13,8 @@ open Libnames
 open Glob_term
 open Term
 open Mod_subst
+open Misctypes
+open Decl_kinds
 
 (** Topconstr: definitions of [aconstr] et [constr_expr] *)