diff options
| author | Maxime Dénès | 2020-02-03 18:19:42 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2020-07-06 11:22:43 +0200 |
| commit | 0ea2d0ff4ed84e1cc544c958b8f6e98f6ba2e9b6 (patch) | |
| tree | fbad060c3c2e29e81751dea414c898b5cb0fa22d /pretyping/vnorm.ml | |
| parent | cf388fdb679adb88a7e8b3122f65377552d2fb94 (diff) | |
Primitive persistent arrays
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Diffstat (limited to 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index efe1efd74e..b3f577b684 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -170,6 +170,7 @@ and nf_whd env sigma whd typ = mkApp(capp,args) | Vint64 i -> i |> Uint63.of_int64 |> mkInt | Vfloat64 f -> f |> Float64.of_float |> mkFloat + | Varray t -> nf_array env sigma t typ | Vatom_stk(Aid idkey, stk) -> constr_type_of_idkey env sigma idkey stk | Vatom_stk(Aind ((mi,i) as ind), stk) -> @@ -399,6 +400,14 @@ and nf_cofix env sigma cf = let cfb = Util.Array.map2 (fun v t -> nf_val env sigma v t) vb cft in mkCoFix (init,(names,cft,cfb)) +and nf_array env sigma t typ = + let ty, allargs = decompose_appvect (whd_all env typ) in + let typ_elem = allargs.(0) in + let t, vdef = Parray.to_array t in + let t = Array.map (fun v -> nf_val env sigma v typ_elem) t in + let u = snd (destConst ty) in + mkArray(u, t, nf_val env sigma vdef typ_elem, typ_elem) + let cbv_vm env sigma c t = if Termops.occur_meta sigma c then CErrors.user_err Pp.(str "vm_compute does not support metas."); |