Use lists instead of arrays in evar instances.

This corresponds more naturally to the use we make of them, as we don't need
fast indexation but we instead keep pushing terms on top of them.

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)