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 /checker/values.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 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/checker/values.ml b/checker/values.ml index 178a3d8624..38cb243f80 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -152,7 +152,8 @@ let rec v_constr = [|v_cofix|]; (* CoFix *) [|v_proj;v_constr|]; (* Proj *) [|v_uint63|]; (* Int *) - [|Float64|] (* Int *) + [|Float64|]; (* Float *) + [|v_instance;Array v_constr;v_constr;v_constr|] (* Array *) |]) and v_prec = Tuple ("prec_declaration", @@ -235,7 +236,7 @@ let v_template_universes = v_tuple "template_universes" [|List(Opt v_level);v_context_set|] let v_primitive = - v_enum "primitive" 44 (* Number of "Primitive" in Int63.v and PrimFloat.v *) + v_enum "primitive" 50 (* Number of "Primitive" in Int63.v and PrimFloat.v *) let v_cst_def = v_sum "constant_def" 0 @@ -259,8 +260,11 @@ let v_cb = v_tuple "constant_body" v_bool; v_typing_flags|] +let v_nested = v_sum "nested" 0 + [|[|v_ind|] (* NestedInd *);[|v_cst|] (* NestedPrimitive *)|] + let v_recarg = v_sum "recarg" 1 (* Norec *) - [|[|v_ind|] (* Mrec *);[|v_ind|] (* Imbr *)|] + [|[|v_ind|] (* Mrec *);[|v_nested|] (* Nested *)|] let rec v_wfp = Sum ("wf_paths",0, [|[|Int;Int|]; (* Rtree.Param *) @@ -317,7 +321,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body" let v_prim_ind = v_enum "prim_ind" 6 (* Number of "Register ... as kernel.ind_..." in Int63.v and PrimFloat.v *) -let v_prim_type = v_enum "prim_type" 2 +let v_prim_type = v_enum "prim_type" 3 (* Number of constructors of prim_type in "kernel/cPrimitives.ml" *) let v_retro_action = |