From 45e14bdb854fe5da40c2ed1d9ca575ae8d435d36 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Sep 2018 18:55:30 +0200
Subject: 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.
---
 kernel/cClosure.ml          |  4 ++--
 kernel/clambda.ml           |  5 +----
 kernel/constr.ml            | 44 ++++++++++++++++++++++++++++----------------
 kernel/constr.mli           |  6 +++---
 kernel/inferCumulativity.ml |  5 ++++-
 kernel/mod_subst.ml         |  2 +-
 kernel/nativelambda.ml      |  2 +-
 kernel/reduction.ml         | 13 ++++++++++---
 8 files changed, 50 insertions(+), 31 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index c31cdae6f5..de02882370 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -613,7 +613,7 @@ let rec to_constr lfts v =
                     subst_constr subs f)
     | FEvar ((ev,args),env) ->
       let subs = comp_subs lfts env in
-        mkEvar(ev,Array.map (fun a -> subst_constr subs a) args)
+        mkEvar(ev,List.map (fun a -> subst_constr subs a) args)
     | FLIFT (k,a) -> to_constr (el_shft k lfts) a
 
     | FInt i ->
@@ -1408,7 +1408,7 @@ and norm_head info tab m =
             Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
           mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
       | FEvar((i,args),env) ->
-          mkEvar(i, Array.map (fun a -> kl info tab (mk_clos env a)) args)
+          mkEvar(i, List.map (fun a -> kl info tab (mk_clos env a)) args)
       | FProj (p,c) ->
           mkProj (p, kl info tab c)
       | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FConstruct _
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 8c7aa6b17a..65de52c0f6 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -670,7 +670,7 @@ let rec lambda_of_constr env c =
   match Constr.kind c with
   | Meta _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr: Meta")
   | Evar (evk, args) ->
-    let args = lambda_of_args env 0 args in
+    let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in
     Levar (evk, args)
 
   | Cast (c, _, _) -> lambda_of_constr env c
@@ -799,9 +799,6 @@ and lambda_of_args env start args =
       (fun i -> lambda_of_constr env args.(start + i))
   else empty_args
 
-
-
-
 (*********************************)
 let dump_lambda = ref false
 
diff --git a/kernel/constr.ml b/kernel/constr.ml
index ade03fdf93..703e3616a0 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -71,7 +71,7 @@ type case_info =
 
 (* [constr array] is an instance matching definitional [named_context] in
    the same order (i.e. last argument first) *)
-type 'constr pexistential = existential_key * 'constr array
+type 'constr pexistential = existential_key * 'constr list
 type ('constr, 'types) prec_declaration =
     Name.t binder_annot array * 'types array * 'constr array
 type ('constr, 'types) pfixpoint =
@@ -110,7 +110,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
 type t = (t, t, Sorts.t, Instance.t) kind_of_term
 type constr = t
 
-type existential = existential_key * constr array
+type existential = existential_key * constr list
 
 type types = constr
 
@@ -470,7 +470,7 @@ let fold f acc c = match kind c with
   | LetIn (_,b,t,c) -> f (f (f acc b) t) c
   | App (c,l) -> Array.fold_left f (f acc c) l
   | Proj (_p,c) -> f acc c
-  | Evar (_,l) -> Array.fold_left f acc l
+  | Evar (_,l) -> List.fold_left f acc l
   | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
   | Fix (_,(_lna,tl,bl)) ->
     Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
@@ -490,7 +490,7 @@ let iter f c = match kind c with
   | LetIn (_,b,t,c) -> f b; f t; f c
   | App (c,l) -> f c; Array.iter f l
   | Proj (_p,c) -> f c
-  | Evar (_,l) -> Array.iter f l
+  | Evar (_,l) -> List.iter f l
   | Case (_,p,c,bl) -> f p; f c; Array.iter f bl
   | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
   | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
@@ -509,7 +509,7 @@ let iter_with_binders g f n c = match kind c with
   | Lambda (_,t,c) -> f n t; f (g n) c
   | LetIn (_,b,t,c) -> f n b; f n t; f (g 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 (_,(_,tl,bl)) ->
@@ -536,7 +536,7 @@ let fold_constr_with_binders g f n acc c =
   | LetIn (_na,b,t,c) -> f (g  n) (f n (f n acc b) t) c
   | App (c,l) -> Array.fold_left (f n) (f n acc c) l
   | Proj (_p,c) -> f n acc c
-  | Evar (_,l) -> Array.fold_left (f n) acc l
+  | Evar (_,l) -> List.fold_left (f n) acc l
   | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
   | Fix (_,(_,tl,bl)) ->
       let n' = iterate g (Array.length tl) n in
@@ -657,7 +657,7 @@ let map_gen userview f c = match kind c with
       if t' == t then c
       else mkProj (p, t')
   | Evar (e,l) ->
-      let l' = Array.Smart.map f l in
+      let l' = List.Smart.map f l in
       if l'==l then c
       else mkEvar (e, l')
   | Case (ci,p,b,bl) when userview ->
@@ -722,7 +722,8 @@ let fold_map f accu c = match kind c with
       if t' == t then accu, c
       else accu, mkProj (p, t')
   | Evar (e,l) ->
-      let accu, l' = Array.Smart.fold_left_map f accu l in
+    (* Doesn't matter, we should not hashcons evars anyways *)
+      let accu, l' = List.fold_left_map f accu l in
       if l'==l then accu, c
       else accu, mkEvar (e, l')
   | Case (ci,p,b,bl) ->
@@ -782,7 +783,7 @@ let map_with_binders g f l c0 = match kind c0 with
     if t' == t then c0
     else mkProj (p, t')
   | Evar (e, al) ->
-    let al' = Array.Fun1.Smart.map f l al in
+    let al' = List.Smart.map (fun c -> f l c) al in
     if al' == al then c0
     else mkEvar (e, al')
   | Case (ci, p, c, bl) ->
@@ -834,7 +835,7 @@ let fold_with_full_binders g f n acc c =
   | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
   | App (c,l) -> Array.fold_left (f n) (f n acc c) l
   | Proj (_,c) -> f n acc c
-  | Evar (_,l) -> Array.fold_left (f n) acc l
+  | Evar (_,l) -> List.fold_left (f n) acc l
   | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
   | Fix (_,(lna,tl,bl)) ->
       let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
@@ -880,7 +881,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
     Int.equal len (Array.length l2) &&
     leq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2
   | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq 0 c1 c2
-  | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal (eq 0) l1 l2
+  | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && List.equal (eq 0) l1 l2
   | Const (c1,u1), Const (c2,u2) ->
     (* The args length currently isn't used but may as well pass it. *)
     Constant.equal c1 c2 && leq_universes (GlobRef.ConstRef c1) nargs u1 u2
@@ -1039,7 +1040,7 @@ let constr_ord_int f t1 t2 =
     | Meta m1, Meta m2 -> Int.compare m1 m2
     | Meta _, _ -> -1 | _, Meta _ -> 1
     | Evar (e1,l1), Evar (e2,l2) ->
-        (Evar.compare =? (Array.compare f)) e1 e2 l1 l2
+        (Evar.compare =? (List.compare f)) e1 e2 l1 l2
     | Evar _, _ -> -1 | _, Evar _ -> 1
     | Sort s1, Sort s2 -> Sorts.compare s1 s2
     | Sort _, _ -> -1 | _, Sort _ -> 1
@@ -1141,7 +1142,7 @@ let hasheq t1 t2 =
       n1 == n2 && b1 == b2 && t1 == t2 && c1 == c2
     | App (c1,l1), App (c2,l2) -> c1 == c2 && array_eqeq l1 l2
     | Proj (p1,c1), Proj(p2,c2) -> p1 == p2 && c1 == c2
-    | Evar (e1,l1), Evar (e2,l2) -> e1 == e2 && array_eqeq l1 l2
+    | Evar (e1,l1), Evar (e2,l2) -> e1 == e2 && List.equal (==) l1 l2
     | Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2
     | Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2
     | Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && u1 == u2
@@ -1221,7 +1222,7 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
         let l, hl = hash_term_array l in
         (App (c,l), combinesmall 7 (combine hl hc))
       | Evar (e,l) ->
-        let l, hl = hash_term_array l in
+        let l, hl = hash_list_array l in
         (Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl))
       | Const (c,u) ->
         let c' = sh_con c in
@@ -1289,6 +1290,14 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
     let h = !accu land 0x3FFFFFFF in
     (HashsetTermArray.repr h t term_array_table, h)
 
+  and hash_list_array l =
+    let fold accu c =
+      let c, h = sh_rec c in
+      (combine accu h, c)
+    in
+    let h, l = List.fold_left_map fold 0 l in
+    (l, h land 0x3FFFFFFF)
+
   in
   (* Make sure our statically allocated Rels (1 to 16) are considered
      as canonical, and hence hash-consed to themselves *)
@@ -1316,7 +1325,7 @@ let rec hash t =
     | App (c,l) ->
       combinesmall 7 (combine (hash_term_array l) (hash c))
     | Evar (e,l) ->
-      combinesmall 8 (combine (Evar.hash e) (hash_term_array l))
+      combinesmall 8 (combine (Evar.hash e) (hash_term_list l))
     | Const (c,u) ->
       combinesmall 9 (combine (Constant.hash c) (Instance.hash u))
     | Ind (ind,u) ->
@@ -1339,6 +1348,9 @@ let rec hash t =
 and hash_term_array t =
   Array.fold_left (fun acc t -> combine acc (hash t)) 0 t
 
+and hash_term_list t =
+  List.fold_left (fun acc t -> combine (hash t) acc) 0 t
+
 module CaseinfoHash =
 struct
   type t = case_info
@@ -1458,7 +1470,7 @@ let rec debug_print c =
        prlist_with_sep spc debug_print (Array.to_list l) ++ str")")
   | Evar (e,l) -> hov 1
       (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++
-       prlist_with_sep spc debug_print (Array.to_list l) ++str"}")
+       prlist_with_sep spc debug_print l ++str"}")
   | Const (c,u) -> str"Cst(" ++ pr_puniverses (Constant.debug_print c) u ++ str")"
   | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i) u ++ str")"
   | Construct (((sp,i),j),u) ->
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 16919b705a..00051d7551 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -83,7 +83,7 @@ val mkFloat : Float64.t -> constr
 val mkMeta : metavariable -> constr
 
 (** Constructs an existential variable *)
-type existential = Evar.t * constr array
+type existential = Evar.t * constr list
 val mkEvar : existential -> constr
 
 (** Construct a sort *)
@@ -203,9 +203,9 @@ val mkCoFix : cofixpoint -> constr
 
 (** {6 Concrete type for making pattern-matching. } *)
 
-(** [constr array] is an instance matching definitional [named_context] in
+(** [constr list] is an instance matching definitional [named_context] in
    the same order (i.e. last argument first) *)
-type 'constr pexistential = Evar.t * 'constr array
+type 'constr pexistential = Evar.t * 'constr list
 
 type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Rel       of int                                  (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *)
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index f987164d52..662ad550b8 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -99,7 +99,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
     end
   | FEvar ((_,args),e) ->
     let variances = infer_stack infos variances stk in
-    infer_vect infos variances (Array.map (mk_clos e) args)
+    infer_list infos variances (List.map (mk_clos e) args)
   | FRel _ -> infer_stack infos variances stk
   | FInt _ -> infer_stack infos variances stk
   | FFloat _ -> infer_stack infos variances stk
@@ -168,6 +168,9 @@ and infer_stack infos variances (stk:CClosure.stack) =
 and infer_vect infos variances v =
   Array.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v
 
+and infer_list infos variances v =
+  List.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v
+
 let infer_term cv_pb env variances c =
   let open CClosure in
   let infos = (create_clos_infos all env, create_tab ()) in
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index aa513c1536..317141e324 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -405,7 +405,7 @@ let rec map_kn f f' c =
             if (ct'== ct && l'==l) then c
             else mkApp (ct',l')
       | Evar (e,l) ->
-          let l' = Array.Smart.map func l in
+          let l' = List.Smart.map func l in
             if (l'==l) then c
             else mkEvar (e,l')
       | Fix (ln,(lna,tl,bl)) ->
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 9ed0f6f411..02ee501f5f 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -474,7 +474,7 @@ let rec lambda_of_constr cache env sigma c =
   | Evar (evk,args as ev) ->
      (match evar_value sigma ev with
      | None ->
-        let args = Array.map (lambda_of_constr cache env sigma) args in
+        let args = Array.map_of_list (fun c -> lambda_of_constr cache env sigma c) args in
         Levar(evk, args)
      | Some t -> lambda_of_constr cache env sigma t)
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 7574d7b21e..4ff90dd70d 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -367,9 +367,9 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           let el1 = el_stack lft1 v1 in
           let el2 = el_stack lft2 v2 in
           let cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in
-          convert_vect l2r infos el1 el2
-            (Array.map (mk_clos env1) args1)
-            (Array.map (mk_clos env2) args2) cuniv
+          convert_list l2r infos el1 el2
+            (List.map (mk_clos env1) args1)
+            (List.map (mk_clos env2) args2) cuniv
         else raise NotConvertible
 
     (* 2 index known to be bound to no constant *)
@@ -702,6 +702,13 @@ and convert_branches l2r infos ci e1 e2 lft1 lft2 br1 br2 cuniv =
   in
   Array.fold_right3 fold ci.ci_cstr_nargs br1 br2 cuniv
 
+and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with
+| [], [] -> cuniv
+| c1 :: v1, c2 :: v2 ->
+  let cuniv = ccnv CONV l2r infos lft1 lft2 c1 c2 cuniv in
+  convert_list l2r infos lft1 lft2 v1 v2 cuniv
+| _, _ -> raise NotConvertible
+
 let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
   let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
   let infos = create_clos_infos ~evars reds env in
-- 
cgit v1.2.3