Glob_term now mli-only, operations now in Glob_ops

Stuff about reductions now in genredexpr.mli, operations in redops.ml

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

12 files changed, 139 insertions, 271 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7019495afb..4b7f9187fd 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -23,6 +23,7 @@ open Reductionops
 open Typeops
 open Type_errors
 open Glob_term
+open Glob_ops
 open Retyping
 open Pretype_errors
 open Evarutil
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 832d32086d..c1e0d123db 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -18,6 +18,7 @@ open Inductiveops
 open Environ
 open Sign
 open Glob_term
+open Glob_ops
 open Nameops
 open Termops
 open Namegen
diff --git a/pretyping/glob_term.ml b/pretyping/glob_ops.ml
index 466e73b8ea..7a48ee9de2 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_ops.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i*)
 open Errors
 open Pp
 open Util
@@ -18,58 +17,14 @@ open Nametab
 open Decl_kinds
 open Misctypes
 open Locus
-(*i*)
+open Glob_term
 
 (* Untyped intermediate terms, after ASTs and before constr. *)
 
-(* locs here refers to the ident's location, not whole pat *)
-(* the last argument of PatCstr is a possible alias ident for the pattern *)
-type cases_pattern =
-  | PatVar of loc * name
-  | PatCstr of loc * constructor * cases_pattern list * name
-
 let cases_pattern_loc = function
     PatVar(loc,_) -> loc
   | PatCstr(loc,_,_,_) -> loc
 
-type glob_constr =
-  | GRef of (loc * global_reference)
-  | GVar of (loc * identifier)
-  | GEvar of loc * existential_key * glob_constr list option
-  | GPatVar of loc * (bool * patvar) (* Used for patterns only *)
-  | GApp of loc * glob_constr * glob_constr list
-  | GLambda of loc * name * binding_kind * glob_constr * glob_constr
-  | GProd of loc * name * binding_kind * glob_constr * glob_constr
-  | GLetIn of loc * name * glob_constr * glob_constr
-  | GCases of loc * case_style * glob_constr option * tomatch_tuples * cases_clauses
-  | GLetTuple of loc * name list * (name * glob_constr option) *
-      glob_constr * glob_constr
-  | GIf of loc * glob_constr * (name * glob_constr option) * glob_constr * glob_constr
-  | GRec of loc * fix_kind * identifier array * glob_decl list array *
-      glob_constr array * glob_constr array
-  | GSort of loc * glob_sort
-  | GHole of (loc * Evar_kinds.t)
-  | GCast of loc * glob_constr * glob_constr cast_type
-
-and glob_decl = name * binding_kind * glob_constr option * glob_constr
-
-and fix_recursion_order = GStructRec | GWfRec of glob_constr | GMeasureRec of glob_constr * glob_constr option
-
-and fix_kind =
-  | GFix of ((int option * fix_recursion_order) array * int)
-  | GCoFix of int
-
-and predicate_pattern =
-    name * (loc * inductive * name list) option
-
-and tomatch_tuple = (glob_constr * predicate_pattern)
-
-and tomatch_tuples = tomatch_tuple list
-
-and cases_clause = (loc * identifier list * cases_pattern list * glob_constr)
-
-and cases_clauses = cases_clause list
-
 let cases_predicate_names tml =
   List.flatten (List.map (function
     | (tm,(na,None)) -> [na]
@@ -80,37 +35,37 @@ let mkGApp loc p t =
   | GApp (loc,f,l) -> GApp (loc,f,l@[t])
   | _ -> GApp (loc,p,[t])
 
-let map_glob_decl_left_to_right f (na,k,obd,ty) = 
+let map_glob_decl_left_to_right f (na,k,obd,ty) =
   let comp1 = Option.map f obd in
   let comp2 = f ty in
   (na,k,comp1,comp2)
 
 let map_glob_constr_left_to_right f = function
-  | GApp (loc,g,args) -> 
-      let comp1 = f g in 
-      let comp2 = Util.list_map_left f args in 
+  | GApp (loc,g,args) ->
+      let comp1 = f g in
+      let comp2 = Util.list_map_left f args in
       GApp (loc,comp1,comp2)
-  | GLambda (loc,na,bk,ty,c) -> 
-      let comp1 = f ty in 
-      let comp2 = f c in 
+  | GLambda (loc,na,bk,ty,c) ->
+      let comp1 = f ty in
+      let comp2 = f c in
       GLambda (loc,na,bk,comp1,comp2)
-  | GProd (loc,na,bk,ty,c) -> 
-      let comp1 = f ty in 
-      let comp2 = f c in 
+  | GProd (loc,na,bk,ty,c) ->
+      let comp1 = f ty in
+      let comp2 = f c in
       GProd (loc,na,bk,comp1,comp2)
-  | GLetIn (loc,na,b,c) -> 
-      let comp1 = f b in 
-      let comp2 = f c in 
+  | GLetIn (loc,na,b,c) ->
+      let comp1 = f b in
+      let comp2 = f c in
       GLetIn (loc,na,comp1,comp2)
   | GCases (loc,sty,rtntypopt,tml,pl) ->
-      let comp1 = Option.map f rtntypopt in 
+      let comp1 = Option.map f rtntypopt in
       let comp2 = Util.list_map_left (fun (tm,x) -> (f tm,x)) tml in
       let comp3 = Util.list_map_left (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl in
       GCases (loc,sty,comp1,comp2,comp3)
   | GLetTuple (loc,nal,(na,po),b,c) ->
       let comp1 = Option.map f po in
       let comp2 = f b in
-      let comp3 = f c in 
+      let comp3 = f c in
       GLetTuple (loc,nal,(na,comp1),comp2,comp3)
   | GIf (loc,c,(na,po),b1,b2) ->
       let comp1 = Option.map f po in
@@ -122,7 +77,7 @@ let map_glob_constr_left_to_right f = function
       let comp2 = Array.map f tyl in
       let comp3 = Array.map f bv in
       GRec (loc,fk,idl,comp1,comp2,comp3)
-  | GCast (loc,c,k) -> 
+  | GCast (loc,c,k) ->
       let comp1 = f c in
       let comp2 = Miscops.map_cast_type f k in
       GCast (loc,comp1,comp2)
@@ -130,43 +85,6 @@ let map_glob_constr_left_to_right f = function
 
 let map_glob_constr = map_glob_constr_left_to_right
 
-(*
-let name_app f e = function
-  | Name id -> let (id, e) = f id e in (Name id, e)
-  | Anonymous -> Anonymous, e
-
-let fold_ident g idl e =
-  let (idl,e) =
-    Array.fold_right
-      (fun id (idl,e) -> let id,e = g id e in (id::idl,e)) idl ([],e)
-  in (Array.of_list idl,e)
-
-let map_glob_constr_with_binders_loc loc g f e = function
-  | GVar (_,id) -> GVar (loc,id)
-  | GApp (_,a,args) -> GApp (loc,f e a, List.map (f e) args)
-  | GLambda (_,na,ty,c) ->
-      let na,e = name_app g e na in GLambda (loc,na,f e ty,f e c)
-  | GProd (_,na,ty,c) ->
-      let na,e = name_app g e na in GProd (loc,na,f e ty,f e c)
-  | GLetIn (_,na,b,c) ->
-      let na,e = name_app g e na in GLetIn (loc,na,f e b,f e c)
-  | GCases (_,tyopt,tml,pl) ->
-      (* We don't modify pattern variable since we don't traverse patterns *)
-      let g' id e = snd (g id e) in
-      let h (_,idl,p,c) = (loc,idl,p,f (List.fold_right g' idl e) c) in
-      GCases
-	(loc,Option.map (f e) tyopt,List.map (f e) tml, List.map h pl)
-  | GRec (_,fk,idl,tyl,bv) ->
-      let idl',e' = fold_ident g idl e in
-      GRec (loc,fk,idl',Array.map (f e) tyl,Array.map (f e') bv)
-  | GCast (_,c,t) -> GCast (loc,f e c,f e t)
-  | GSort (_,x) -> GSort (loc,x)
-  | GHole (_,x)  -> GHole (loc,x)
-  | GRef (_,x) -> GRef (loc,x)
-  | GEvar (_,x,l) -> GEvar (loc,x,l)
-  | GPatVar (_,x) -> GPatVar (loc,x)
-*)
-
 let fold_glob_constr f acc =
   let rec fold acc = function
   | GVar _ -> acc
@@ -347,35 +265,3 @@ let glob_constr_of_closed_cases_pattern = function
       na,glob_constr_of_closed_cases_pattern_aux (PatCstr (loc,cstr,l,Anonymous))
   | _ ->
       raise Not_found
-
-(**********************************************************************)
-(* Reduction expressions                                              *)
-
-type 'a glob_red_flag = {
-  rBeta : bool;
-  rIota : bool;
-  rZeta : bool;
-  rDelta : bool; (* true = delta all but rConst; false = delta only on rConst*)
-  rConst : 'a list
-}
-
-let all_flags =
-  {rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []}
-
-type ('a,'b,'c) red_expr_gen =
-  | Red of bool
-  | Hnf
-  | Simpl of 'c with_occurrences option
-  | Cbv of 'b glob_red_flag
-  | Lazy of 'b glob_red_flag
-  | Unfold of 'b with_occurrences list
-  | Fold of 'a list
-  | Pattern of 'a with_occurrences list
-  | ExtraRedExpr of string
-  | CbvVm of 'c with_occurrences option
-
-type ('a,'b,'c) may_eval =
-  | ConstrTerm of 'a
-  | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
-  | ConstrContext of (loc * identifier) * 'a
-  | ConstrTypeOf of 'a
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
new file mode 100644
index 0000000000..19d003a92c
--- /dev/null
+++ b/pretyping/glob_ops.mli
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*  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 Errors
+open Pp
+open Util
+open Names
+open Sign
+open Term
+open Libnames
+open Nametab
+open Decl_kinds
+open Misctypes
+open Locus
+open Glob_term
+
+(** Operations on [glob_constr] *)
+
+val cases_pattern_loc : cases_pattern -> loc
+
+val cases_predicate_names : tomatch_tuples -> name list
+
+(** Apply one argument to a glob_constr *)
+val mkGApp : loc -> glob_constr -> glob_constr -> glob_constr
+
+val map_glob_constr :
+  (glob_constr -> glob_constr) -> glob_constr -> glob_constr
+
+(** Ensure traversal from left to right *)
+val map_glob_constr_left_to_right :
+  (glob_constr -> glob_constr) -> glob_constr -> glob_constr
+
+val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
+val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
+val occur_glob_constr : identifier -> glob_constr -> bool
+val free_glob_vars : glob_constr -> identifier list
+val loc_of_glob_constr : glob_constr -> loc
+
+(** Conversion from glob_constr to cases pattern, if possible
+
+    Take the current alias as parameter,
+    @raise Not_found if translation is impossible *)
+val cases_pattern_of_glob_constr : name -> glob_constr -> cases_pattern
+
+val glob_constr_of_closed_cases_pattern : cases_pattern -> name * glob_constr
diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli
deleted file mode 100644
index f654925ef8..0000000000
--- a/pretyping/glob_term.mli
+++ /dev/null
@@ -1,138 +0,0 @@
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
-
-(**Untyped intermediate terms, after constr_expr and before constr
-
-   Resolution of names, insertion of implicit arguments placeholder,
-   and notations are done, but coercions, inference of implicit
-   arguments and pattern-matching compilation are not. *)
-
-open Errors
-open Pp
-open Names
-open Sign
-open Term
-open Libnames
-open Nametab
-open Decl_kinds
-open Misctypes
-open Locus
-
-(**  The kind of patterns that occurs in "match ... with ... end"
-
-     locs here refers to the ident's location, not whole pat *)
-type cases_pattern =
-  | PatVar of loc * name
-  | PatCstr of loc * constructor * cases_pattern list * name
-      (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *)
-
-val cases_pattern_loc : cases_pattern -> loc
-
-type glob_constr =
-  | GRef of (loc * global_reference)
-  | GVar of (loc * identifier)
-  | GEvar of loc * existential_key * glob_constr list option
-  | GPatVar of loc * (bool * patvar) (** Used for patterns only *)
-  | GApp of loc * glob_constr * glob_constr list
-  | GLambda of loc * name * binding_kind *  glob_constr * glob_constr
-  | GProd of loc * name * binding_kind * glob_constr * glob_constr
-  | GLetIn of loc * name * glob_constr * glob_constr
-  | GCases of loc * case_style * glob_constr option * tomatch_tuples * cases_clauses
-      (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in 
-	  [MatchStyle]) *)
-
-  | GLetTuple of loc * name list * (name * glob_constr option) *
-      glob_constr * glob_constr
-  | GIf of loc * glob_constr * (name * glob_constr option) * glob_constr * glob_constr
-  | GRec of loc * fix_kind * identifier array * glob_decl list array *
-      glob_constr array * glob_constr array
-  | GSort of loc * glob_sort
-  | GHole of (loc * Evar_kinds.t)
-  | GCast of loc * glob_constr * glob_constr cast_type
-
-and glob_decl = name * binding_kind * glob_constr option * glob_constr
-
-and fix_recursion_order = GStructRec | GWfRec of glob_constr | GMeasureRec of glob_constr * glob_constr option
-
-and fix_kind =
-  | GFix of ((int option * fix_recursion_order) array * int)
-  | GCoFix of int
-
-and predicate_pattern =
-    name * (loc * inductive * name list) option
-      (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *)
-
-and tomatch_tuple = (glob_constr * predicate_pattern)
-
-and tomatch_tuples = tomatch_tuple list
-
-and cases_clause = (loc * identifier list * cases_pattern list * glob_constr)
-(** [(p,il,cl,t)] = "|'cl' => 't'" where FV(t) \subset il *)
-
-and cases_clauses = cases_clause list
-
-val cases_predicate_names : tomatch_tuples -> name list
-
-(* Apply one argument to a glob_constr *)
-val mkGApp : loc -> glob_constr -> glob_constr -> glob_constr
-
-val map_glob_constr : (glob_constr -> glob_constr) -> glob_constr -> glob_constr
-
-(* Ensure traversal from left to right *)
-val map_glob_constr_left_to_right :
-  (glob_constr -> glob_constr) -> glob_constr -> glob_constr
-
-(*
-val map_glob_constr_with_binders_loc : loc ->
-  (identifier -> 'a -> identifier * 'a) ->
-  ('a -> glob_constr -> glob_constr) -> 'a -> glob_constr -> glob_constr
-*)
-
-val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
-val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
-val occur_glob_constr : identifier -> glob_constr -> bool
-val free_glob_vars : glob_constr -> identifier list
-val loc_of_glob_constr : glob_constr -> loc
-
-(** Conversion from glob_constr to cases pattern, if possible
-    
-    Take the current alias as parameter, 
-    @raise Not_found if translation is impossible *)
-val cases_pattern_of_glob_constr : name -> glob_constr -> cases_pattern
-
-val glob_constr_of_closed_cases_pattern : cases_pattern -> name * glob_constr
-
-(** {6 Reduction expressions} *)
-
-type 'a glob_red_flag = {
-  rBeta : bool;
-  rIota : bool;
-  rZeta : bool;
-  rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*)
-  rConst : 'a list
-}
-
-val all_flags : 'a glob_red_flag
-
-type ('a,'b,'c) red_expr_gen =
-  | Red of bool
-  | Hnf
-  | Simpl of 'c with_occurrences option
-  | Cbv of 'b glob_red_flag
-  | Lazy of 'b glob_red_flag
-  | Unfold of 'b with_occurrences list
-  | Fold of 'a list
-  | Pattern of 'a with_occurrences list
-  | ExtraRedExpr of string
-  | CbvVm of 'c with_occurrences option
-
-type ('a,'b,'c) may_eval =
-  | ConstrTerm of 'a
-  | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
-  | ConstrContext of (loc * identifier) * 'a
-  | ConstrTypeOf of 'a
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 2528d57f30..0f659f1b65 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -10,6 +10,8 @@ open Misctypes
 open Pp
 open Nameops
 
+(** Mapping [cast_type] *)
+
 let map_cast_type f = function
   | CastConv a -> CastConv (f a)
   | CastVM a -> CastVM (f a)
@@ -41,3 +43,11 @@ and pr_or_and_intro_pattern = function
       str "[" ++
       hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
       ++ str "]"
+
+(** Printing of [move_location] *)
+
+let pr_move_location pr_id = function
+  | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id
+  | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
+  | MoveFirst -> str " at top"
+  | MoveLast -> str " at bottom"
diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli
index b8f6f68606..123d307de9 100644
--- a/pretyping/miscops.mli
+++ b/pretyping/miscops.mli
@@ -8,11 +8,17 @@
 
 open Misctypes
 
-val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type
+(** Mapping [cast_type] *)
 
+val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type
 val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type
 
 (** Printing of [intro_pattern] *)
 
 val pr_intro_pattern : intro_pattern_expr Pp.located -> Pp.std_ppcmds
 val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds
+
+(** Printing of [move_location] *)
+
+val pr_move_location :
+  ('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index ef81aa4d32..08e5ac75c9 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -13,6 +13,7 @@ open Libnames
 open Nameops
 open Term
 open Glob_term
+open Glob_ops
 open Environ
 open Nametab
 open Pp
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 82f030ae09..b241336e77 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -42,6 +42,7 @@ open Recordops
 open Evarutil
 open Pretype_errors
 open Glob_term
+open Glob_ops
 open Evarconv
 open Pattern
 open Misctypes
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index e520602db2..fca2d714f8 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -15,7 +15,8 @@ Evarconv
 Arguments_renaming
 Typing
 Miscops
-Glob_term
+Glob_ops
+Redops
 Pattern
 Matching
 Tacred
diff --git a/pretyping/redops.ml b/pretyping/redops.ml
new file mode 100644
index 0000000000..53ac6e6c87
--- /dev/null
+++ b/pretyping/redops.ml
@@ -0,0 +1,36 @@
+(************************************************************************)
+(*  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 Genredexpr
+
+let make_red_flag l =
+  let rec add_flag red = function
+    | [] -> red
+    | FBeta :: lf -> add_flag { red with rBeta = true } lf
+    | FIota :: lf -> add_flag { red with rIota = true } lf
+    | FZeta :: lf -> add_flag { red with rZeta = true } lf
+    | FConst l :: lf ->
+	if red.rDelta then
+	  Errors.error
+	    "Cannot set both constants to unfold and constants not to unfold";
+        add_flag { red with rConst = Util.list_union red.rConst l } lf
+    | FDeltaBut l :: lf ->
+	if red.rConst <> [] & not red.rDelta then
+	  Errors.error
+	    "Cannot set both constants to unfold and constants not to unfold";
+        add_flag
+	  { red with rConst = Util.list_union red.rConst l; rDelta = true }
+	  lf
+  in
+  add_flag
+    {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []}
+    l
+
+
+let all_flags =
+  {rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []}
diff --git a/pretyping/redops.mli b/pretyping/redops.mli
new file mode 100644
index 0000000000..b555970984
--- /dev/null
+++ b/pretyping/redops.mli
@@ -0,0 +1,13 @@
+(************************************************************************)
+(*  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 Genredexpr
+
+val make_red_flag : 'a red_atom list -> 'a glob_red_flag
+
+val all_flags : 'a glob_red_flag