From d72e5c154faeea1d55387bc8c039d97f63ebd1c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 3 Mar 2019 21:03:37 +0100
Subject: 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.
---
 checker/values.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'checker/values.ml')

diff --git a/checker/values.ml b/checker/values.ml
index 4e99d087df..b94173429d 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -147,7 +147,7 @@ let rec v_constr =
     [|v_puniverses v_cst|]; (* Const *)
     [|v_puniverses v_ind|]; (* Ind *)
     [|v_puniverses v_cons|]; (* Construct *)
-    [|v_caseinfo;v_constr;v_case_invert;v_constr;Array v_constr|]; (* Case *)
+    [|v_caseinfo;v_instance; Array v_constr; v_case_return; v_case_invert; v_constr; Array v_case_branch|]; (* Case *)
     [|v_fix|]; (* Fix *)
     [|v_cofix|]; (* CoFix *)
     [|v_proj;v_constr|]; (* Proj *)
@@ -162,6 +162,10 @@ and v_fix = Tuple ("pfixpoint", [|Tuple ("fix2",[|Array Int;Int|]);v_prec|])
 and v_cofix = Tuple ("pcofixpoint",[|Int;v_prec|])
 and v_case_invert = Sum ("case_inversion", 1, [|[|v_instance;Array v_constr|]|])
 
+and v_case_branch = Tuple ("case_branch", [|Array (v_binder_annot v_name); v_constr|])
+
+and v_case_return = Tuple ("case_return", [|Array (v_binder_annot v_name); v_constr|])
+
 let v_rdecl = v_sum "rel_declaration" 0
     [| [|v_binder_annot v_name; v_constr|];               (* LocalAssum *)
        [|v_binder_annot v_name; v_constr; v_constr|] |]   (* LocalDef *)
-- 
cgit v1.2.3


From 868b948f8a7bd583d467c5d02dfb34d328d53d37 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 11 Dec 2020 13:20:54 +0100
Subject: Remove redundant univ and parameter info from CaseInvert

---
 checker/values.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker/values.ml')

diff --git a/checker/values.ml b/checker/values.ml
index b94173429d..907f9f7e32 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -160,7 +160,7 @@ and v_prec = Tuple ("prec_declaration",
                     [|Array (v_binder_annot v_name); Array v_constr; Array v_constr|])
 and v_fix = Tuple ("pfixpoint", [|Tuple ("fix2",[|Array Int;Int|]);v_prec|])
 and v_cofix = Tuple ("pcofixpoint",[|Int;v_prec|])
-and v_case_invert = Sum ("case_inversion", 1, [|[|v_instance;Array v_constr|]|])
+and v_case_invert = Sum ("case_inversion", 1, [|[|Array v_constr|]|])
 
 and v_case_branch = Tuple ("case_branch", [|Array (v_binder_annot v_name); v_constr|])
 
-- 
cgit v1.2.3