diff options
| author | Pierre-Marie Pédrot | 2020-07-06 16:18:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-07-06 16:18:33 +0200 |
| commit | 8907a5b7d2b91bff0b573956a05e4679b5238161 (patch) | |
| tree | 2fff532e687a8e82543044352aeaf3168434aac1 /kernel/vconv.ml | |
| parent | 3244b9c6e4159042bae0cd2ad48aba77928d7b2d (diff) | |
| parent | 0ea2d0ff4ed84e1cc544c958b8f6e98f6ba2e9b6 (diff) | |
Merge PR #11604: Primitive persistent arrays
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
Ack-by: proux01
Ack-by: silene
Diffstat (limited to 'kernel/vconv.ml')
| -rw-r--r-- | kernel/vconv.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 3563407f7e..f78f0d4d1e 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -76,6 +76,11 @@ and conv_whd env pb k whd1 whd2 cu = | Vfloat64 f1, Vfloat64 f2 -> if Float64.(equal (of_float f1) (of_float f2)) then cu else raise NotConvertible + | Varray t1, Varray t2 -> + if t1 == t2 then cu else + let n = Parray.length_int t1 in + if not (Int.equal n (Parray.length_int t2)) then raise NotConvertible; + Parray.fold_left2 (fun cu v1 v2 -> conv_val env CONV k v1 v2 cu) cu t1 t2 | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) -> conv_atom env pb k a1 stk1 a2 stk2 cu | Vfun _, _ | _, Vfun _ -> @@ -83,7 +88,7 @@ and conv_whd env pb k whd1 whd2 cu = conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ | Vint64 _, _ - | Vfloat64 _, _ | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible + | Vfloat64 _, _ | Varray _, _ | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible and conv_atom env pb k a1 stk1 a2 stk2 cu = |