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 /interp/constrintern.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 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d95554de56..987aa63392 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -772,7 +772,7 @@ let rec adjust_env env = function | NCast (c,_) -> adjust_env env c | NApp _ -> restart_no_binders env | NVar _ | NRef _ | NHole _ | NCases _ | NLetTuple _ | NIf _ - | NRec _ | NSort _ | NInt _ | NFloat _ + | NRec _ | NSort _ | NInt _ | NFloat _ | NArray _ | NList _ | NBinderList _ -> env (* to be safe, but restart should be ok *) let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = @@ -2204,6 +2204,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CCast (c1, c2) -> DAst.make ?loc @@ GCast (intern env c1, map_cast_type (intern_type (slide_binders env)) c2) + | CArray(u,t,def,ty) -> + DAst.make ?loc @@ GArray(u, Array.map (intern env) t, intern env def, intern env ty) ) and intern_type env = intern (set_type_scope env) |