Merge PR #11896: Use lists instead of arrays in evar instances.

Ack-by: SkySkimmer
Reviewed-by: maximedenes

7 files changed, 33 insertions, 38 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 4508633858..ca681e58f8 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -355,7 +355,7 @@ let iter_with_full_binders sigma g f n c =
   | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
   | LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c
   | App (c,l) -> f n c; Array.Fun1.iter f n l
-  | Evar (_,l) -> Array.Fun1.iter f n l
+  | Evar (_,l) -> List.iter (fun c -> f n c) l
   | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
   | Proj (p,c) -> f n c
   | Fix (_,(lna,tl,bl)) ->
@@ -717,7 +717,7 @@ let val_of_named_context e = val_of_named_context (cast_named_context unsafe_eq
 let named_context_of_val e = cast_named_context (sym unsafe_eq) (named_context_of_val e)
 
 let of_existential : Constr.existential -> existential =
-  let gen : type a b. (a,b) eq -> 'c * b array -> 'c * a array = fun Refl x -> x in
+  let gen : type a b. (a,b) eq -> 'c * b list -> 'c * a list = fun Refl x -> x in
   gen unsafe_eq
 
 let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e)
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index fdcdfe11f4..5fcadfcef7 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -200,7 +200,7 @@ let make_pure_subst evi args =
       match args with
         | a::rest -> (rest, (NamedDecl.get_id decl, a)::l)
         | _ -> anomaly (Pp.str "Instance does not match its signature."))
-    (evar_filtered_context evi) (Array.rev_to_list args,[]))
+    (evar_filtered_context evi) (List.rev args,[]))
 
 (*------------------------------------*
  * functional operations on evar sets *
@@ -448,7 +448,7 @@ let new_evar_instance ?src ?filter ?abstract_arguments ?candidates ?naming ?type
   assert (not !Flags.debug ||
             List.distinct (ids_of_named_context (named_context_of_val sign)));
   let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate ?principal typ in
-  evd, mkEvar (newevk,Array.of_list instance)
+  evd, mkEvar (newevk, instance)
 
 let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ =
   let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
@@ -506,7 +506,7 @@ let generalize_evar_over_rels sigma (ev,args) =
   List.fold_left2
     (fun (c,inst as x) a d ->
       if isRel sigma a then (mkNamedProd_or_LetIn d c,a::inst) else x)
-     (evi.evar_concl,[]) (Array.to_list args) sign
+     (evi.evar_concl,[]) args sign
 
 (************************************)
 (* Removing a dependency in an evar *)
@@ -594,7 +594,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
                   (* No dependency at all, we can keep this ev's context hyp *)
                     (ri, true::filter)
                   with Depends id -> (Id.Map.add (NamedDecl.get_id h) id ri, false::filter))
-                ctxt (Array.to_list l) (Id.Map.empty,[]) in
+                ctxt l (Id.Map.empty,[]) in
             (* Check if some rid to clear in the context of ev has dependencies
                in the type of ev and adjust the source of the dependency *)
             let _nconcl =
@@ -736,7 +736,7 @@ let undefined_evars_of_term evd t =
     match EConstr.kind evd c with
       | Evar (n, l) ->
         let acc = Evar.Set.add n acc in
-        Array.fold_left evrec acc l
+        List.fold_left evrec acc l
       | _ -> EConstr.fold evd evrec acc c
   in
   evrec Evar.Set.empty t
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 1dec63aaf0..b5c7ccb283 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -88,7 +88,7 @@ val new_evar_instance :
  named_context_val -> evar_map -> types ->
   constr list -> evar_map * constr
 
-val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list
+val make_pure_subst : evar_info -> 'a list -> (Id.t * 'a) list
 
 val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option
 
diff --git a/engine/evd.ml b/engine/evd.ml
index 65fe261ff4..5642145f6d 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -233,32 +233,27 @@ exception NotInstantiatedEvar
 (* Note: let-in contributes to the instance *)
 
 let evar_instance_array test_id info args =
-  let len = Array.length args in
-  let rec instrec filter ctxt i = match filter, ctxt with
-  | [], [] ->
-    if Int.equal i len then []
-    else instance_mismatch ()
-  | false :: filter, _ :: ctxt ->
-    instrec filter ctxt i
-  | true :: filter, d :: ctxt ->
-    if i < len then
-      let c = Array.unsafe_get args i in
-      if test_id d c then instrec filter ctxt (succ i)
-      else (NamedDecl.get_id d, c) :: instrec filter ctxt (succ i)
-    else instance_mismatch ()
+  let rec instrec filter ctxt args = match filter, ctxt, args with
+  | [], [], [] -> []
+  | false :: filter, _ :: ctxt, args ->
+    instrec filter ctxt args
+  | true :: filter, d :: ctxt, c :: args ->
+    if test_id d c then instrec filter ctxt args
+    else (NamedDecl.get_id d, c) :: instrec filter ctxt args
   | _ -> instance_mismatch ()
   in
   match Filter.repr (evar_filter info) with
   | None ->
-     let map i d =
-      if (i < len) then
-        let c = Array.unsafe_get args i in
-        if test_id d c then None else Some (NamedDecl.get_id d, c)
-      else instance_mismatch ()
+    let rec instance ctxt args = match ctxt, args with
+    | [], [] -> []
+    | d :: ctxt, c :: args ->
+      if test_id d c then instance ctxt args
+      else (NamedDecl.get_id d, c) :: instance ctxt args
+    | _ -> instance_mismatch ()
     in
-    List.map_filter_i map (evar_context info)
+    instance (evar_context info) args
   | Some filter ->
-    instrec filter (evar_context info) 0
+    instrec filter (evar_context info) args
 
 let make_evar_instance_array info args =
   evar_instance_array (NamedDecl.get_id %> isVarId) info args
@@ -794,7 +789,7 @@ let restrict evk filter ?candidates ?src evd =
   | _ -> Evar.Set.add evk evd.last_mods in
   let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
   let ctxt = Filter.filter_list filter (evar_context evar_info) in
-  let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in
+  let id_inst = List.map (NamedDecl.get_id %> mkVar) ctxt in
   let body = mkEvar(evk',id_inst) in
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   let evar_flags = declare_restricted_evar evd.evar_flags evk evk' in
@@ -1405,7 +1400,7 @@ let evars_of_term evd c =
   let rec evrec acc c =
     let c = MiniEConstr.whd_evar evd c in
     match kind c with
-    | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
+    | Evar (n, l) -> Evar.Set.add n (List.fold_left evrec acc l)
     | _ -> Constr.fold evrec acc c
   in
   evrec Evar.Set.empty c
@@ -1413,7 +1408,7 @@ let evars_of_term evd c =
 let evar_nodes_of_term c =
   let rec evrec acc c =
     match kind c with
-    | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
+    | Evar (n, l) -> Evar.Set.add n (List.fold_left evrec acc l)
     | _ -> Constr.fold evrec acc c
   in
   evrec Evar.Set.empty c
diff --git a/engine/evd.mli b/engine/evd.mli
index bbdb63a467..c6c4a71b22 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -247,9 +247,9 @@ val existential_opt_value : evar_map -> econstr pexistential -> econstr option
 val existential_opt_value0 : evar_map -> existential -> constr option
 
 val evar_instance_array : (Constr.named_declaration -> 'a -> bool) -> evar_info ->
-  'a array -> (Id.t * 'a) list
+  'a list -> (Id.t * 'a) list
 
-val instantiate_evar_array : evar_info -> econstr -> econstr array -> econstr
+val instantiate_evar_array : evar_info -> econstr -> econstr list -> econstr
 
 val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool ->
   evar_map ->  evar_map -> evar_map
diff --git a/engine/termops.ml b/engine/termops.ml
index 16f2a87c1e..6d779e6a35 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -636,8 +636,8 @@ let map_constr_with_binders_left_to_right sigma g f l c =
       if b' == b then c
       else mkProj (p, b')
   | Evar (e,al) ->
-    let al' = Array.map_left (f l) al in
-      if Array.for_all2 (==) al' al then c
+    let al' = List.map_left (f l) al in
+      if List.for_all2 (==) al' al then c
       else mkEvar (e, al')
   | Case (ci,p,b,bl) ->
       (* In v8 concrete syntax, predicate is after the term to match! *)
@@ -707,8 +707,8 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
       let c' = f l c in
         if c' == c then cstr else mkProj (p, c')
   | Evar (e,al) ->
-      let al' = Array.map (f l) al in
-      if Array.for_all2 (==) al al' then cstr else mkEvar (e, al')
+      let al' = List.map (f l) al in
+      if List.for_all2 (==) al al' then cstr else mkEvar (e, al')
   | Case (ci,p,c,bl) when userview ->
       let p' = map_return_predicate_with_full_binders sigma g f l ci p in
       let c' = f l c in
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index 6000650ad9..a691239ee2 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -131,7 +131,7 @@ let nf_evars_and_universes_opt_subst f subst =
   let rec aux c =
     match kind c with
     | Evar (evk, args) ->
-      let args = Array.map aux args in
+      let args = List.map aux args in
       (match try f (evk, args) with Not_found -> None with
       | None -> mkEvar (evk, args)
       | Some c -> aux c)