Documenting module Reductionops.Stack.

Also includes minor layout or code changes.

2 files changed, 44 insertions, 21 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 2a5de7ba74..cf5d4de40c 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -215,13 +215,13 @@ end =
 struct
   open EConstr
   type 'a app_node = int * 'a array * int
-  (* first releavnt position, arguments, last relevant position *)
+  (* first relevant position, arguments, last relevant position *)
 
   (*
-     Invariant that this module must ensure :
-     (behare of direct access to app_node by the rest of Reductionops)
+     Invariant that this module must ensure:
+     (beware of direct access to app_node by the rest of Reductionops)
      - in app_node (i,_,j) i <= j
-     - There is no array realocation (outside of debug printing)
+     - There is no array reallocation (outside of debug printing)
    *)
 
   let pr_app_node pr (i,a,j) =
@@ -292,7 +292,7 @@ struct
         Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
       | (Primitive(_,_,a1,_)::s1, Primitive(_,_,a2,_)::s2) ->
         Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
-      | ((Case _|Proj _|Fix _|Primitive _) :: _ | []) ,_ -> false in
+      | ((Case _ | Proj _ | Fix _ | Primitive _) :: _ | []) ,_ -> false in
     compare_rec 0 stk1 stk2
 
   exception IncompatibleFold2
@@ -333,26 +333,27 @@ struct
     append_app a s
 
   let rec args_size = function
-    | App (i,_,j)::s -> j + 1 - i + args_size s
-    | (Case _|Fix _|Proj _|Primitive _)::_ | [] -> 0
+    | App (i,_,j) :: s -> j + 1 - i + args_size s
+    | (Case _ | Fix _ | Proj _ | Primitive _) :: _ | [] -> 0
 
   let strip_app s =
     let rec aux out = function
       | ( App _ as e) :: s -> aux (e :: out) s
       | s -> List.rev out,s
     in aux [] s
+
   let strip_n_app n s =
     let rec aux n out = function
       | App (i,a,j) as e :: s ->
-         let nb = j  - i + 1 in
+         let nb = j - i + 1 in
          if n >= nb then
-           aux (n - nb) (e::out) s
+           aux (n - nb) (e :: out) s
          else
-           let p = i+n in
+           let p = i + n in
            Some (CList.rev
               (if Int.equal n 0 then out else App (i,a,p-1) :: out),
             a.(p),
-            if j > p then App(succ p,a,j)::s else s)
+            if j > p then App (succ p,a,j) :: s else s)
       | s -> None
     in aux n [] s
 
@@ -373,12 +374,11 @@ struct
         (Array.fold_right (fun x y -> x::y) a' args', s')
       | s -> ([],s) in
     let (out,s') = aux s in
-    let init = match s' with [] -> true | _ -> false in
-    Option.init init out
+    match s' with [] -> Some out | _ -> None
 
   let assign s p c =
     match strip_n_app p s with
-    | Some (pre,_,sk) -> pre @ (App (0,[|c|],0)::sk)
+    | Some (pre,_,sk) -> pre @ (App (0,[|c|],0) :: sk)
     | None -> assert false
 
   let tail n0 s0 =
@@ -386,12 +386,12 @@ struct
       if Int.equal n 0 then s else
         match s with
       | App (i,a,j) :: s ->
-         let nb = j  - i + 1 in
+         let nb = j - i + 1 in
          if n >= nb then
            aux (n - nb) s
          else
            let p = i+n in
-           if j >= p then App(p,a,j)::s else s
+           if j >= p then App (p,a,j) :: s else s
         | _ -> raise (Invalid_argument "Reductionops.Stack.tail")
     in aux n0 s0
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 7a840c5731..29b698f9d6 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -69,8 +69,6 @@ module Stack : sig
 
   val empty : 'a t
   val is_empty : 'a t -> bool
-  val append_app : 'a array -> 'a t -> 'a t
-  val decomp : 'a t -> ('a * 'a t) option
 
   val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t)
   [@@ocaml.deprecated "Use decomp_rev"]
@@ -85,26 +83,51 @@ module Stack : sig
   val fold2 : ('a -> constr -> constr -> 'a) -> 'a ->
     constr t -> constr t -> 'a
   val map : ('a -> 'a) -> 'a t -> 'a t
+
+  (** [append_app args sk] pushes array of arguments [args] on [sk] *)
+  val append_app : 'a array -> 'a t -> 'a t
+
+  (** [append_app_list args sk] pushes list of arguments [args] on [sk] *)
   val append_app_list : 'a list -> 'a t -> 'a t
 
-  (** if [strip_app s] = [(a,b)], then [s = a @ b] and [b] does not
-      start by App *)
+  (** if [strip_app sk] = [(sk1,sk2)], then [sk = sk1 @ sk2] with
+      [sk1] purely applicative and [sk2] does not start with an argument *)
   val strip_app : 'a t -> 'a t * 'a t
 
-  (** @return (the nth first elements, the (n+1)th element, the remaining stack)  *)
+  (** @return (the nth first elements, the (n+1)th element, the remaining stack)
+      if there enough of those *)
   val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option
 
+  (** [decomp sk] extracts the first argument of [sk] is there is some *)
+  val decomp : 'a t -> ('a * 'a t) option
+
   (** [decomp sk] extracts the first argument of reversed stack [sk] is there is some *)
   val decomp_rev : 'a t -> ('a * 'a t) option
 
+  (** [not_purely_applicative sk] *)
   val not_purely_applicative : 'a t -> bool
+
+  (** [list_of_app_stack sk] either returns [Some sk] turned into a list of
+      arguments if [sk] is purely applicative and [None] otherwise *)
   val list_of_app_stack : constr t -> constr list option
 
+  (** [assign sk n a] changes the [n]th argument of [sk] with [a], counting from 0
+      @raise an anomaly if there is less that [n] arguments available *)
   val assign : 'a t -> int -> 'a -> 'a t
+
+  (** [args_size sk] returns the number of arguments available at the
+      head of [sk] *)
   val args_size : 'a t -> int
+
+  (** [tail n sk] drops the [n] first arguments of [sk]
+      @raise [Invalid_argument] if there are not enough arguments *)
   val tail : int -> 'a t -> 'a t
+
+  (** [nth sk n] returns the [n]-th argument of [sk], counting from 0
+      @raise [Not_found] if there is no [n]th argument *)
   val nth : 'a t -> int -> 'a
 
+  (** [zip sigma t sk] *)
   val zip : evar_map -> constr * constr t -> constr
 end