diff options
| author | Pierre-Marie Pédrot | 2019-03-03 21:03:37 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-04 14:00:20 +0100 |
| commit | d72e5c154faeea1d55387bc8c039d97f63ebd1c4 (patch) | |
| tree | d7f3c292606e98d2c2891354398e8d406d4dc15c /pretyping/reductionops.mli | |
| parent | 6632739f853e42e5828fbf603f7a3089a00f33f7 (diff) | |
Change the representation of kernel case.
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index ae93eb48b4..e60def72f6 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -57,9 +57,12 @@ module Stack : sig val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t + type 'a case_stk = + case_info * EInstance.t * 'a array * 'a pcase_return * ('a, EInstance.t) pcase_invert * 'a pcase_branch array + type 'a member = | App of 'a app_node - | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array + | Case of 'a case_stk | Proj of Projection.t | Fix of ('a, 'a) pfixpoint * 'a t | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red |