From 46c44648e1f5db5960a5d83c2d0cc7be242170ad Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Wed, 12 Oct 2022 12:22:04 -0400
Subject: [PATCH] feat(core-logic): add builtin `Proof` type

not used yet
---
 src/core-logic/t_builtins.ml  | 7 ++++++-
 src/core-logic/t_builtins.mli | 3 ++-
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/core-logic/t_builtins.ml b/src/core-logic/t_builtins.ml
index 95cf4834..c103f540 100644
--- a/src/core-logic/t_builtins.ml
+++ b/src/core-logic/t_builtins.ml
@@ -1,7 +1,7 @@
 open Types_
 open Term
 
-type const_view += C_bool | C_eq | C_ite | C_not | C_true | C_false
+type const_view += C_bool | C_eq | C_ite | C_not | C_true | C_false | C_proof
 
 let to_string = function
   | C_bool -> "Bool"
@@ -10,6 +10,7 @@ let to_string = function
   | C_not -> "not"
   | C_true -> "true"
   | C_false -> "false"
+  | C_proof -> "Proof"
   | _ -> assert false
 
 let of_string = function
@@ -19,12 +20,14 @@ let of_string = function
   | "not" -> Some C_not
   | "true" -> Some C_true
   | "false" -> Some C_false
+  | "Proof" -> Some C_proof
   | _ -> None
 
 let ops : const_ops =
   let equal a b =
     match a, b with
     | C_bool, C_bool
+    | C_proof, C_proof
     | C_eq, C_eq
     | C_ite, C_ite
     | C_not, C_not
@@ -41,6 +44,7 @@ let ops : const_ops =
     | C_not -> CCHash.int 170
     | C_true -> CCHash.int 171
     | C_false -> CCHash.int 172
+    | C_proof -> CCHash.int 173
     | _ -> assert false
   in
 
@@ -61,6 +65,7 @@ let const_decoders : Const.decoders =
   ]
 
 let bool store = const store @@ Const.make C_bool ops ~ty:(type_ store)
+let proof store = const store @@ Const.make C_proof ops ~ty:(type_ store)
 let true_ store = const store @@ Const.make C_true ops ~ty:(bool store)
 let false_ store = const store @@ Const.make C_false ops ~ty:(bool store)
 
diff --git a/src/core-logic/t_builtins.mli b/src/core-logic/t_builtins.mli
index eb45adf2..7f16873c 100644
--- a/src/core-logic/t_builtins.mli
+++ b/src/core-logic/t_builtins.mli
@@ -3,9 +3,10 @@
 open Types_
 open Term
 
-type const_view += C_bool | C_eq | C_ite | C_not | C_true | C_false
+type const_view += C_bool | C_eq | C_ite | C_not | C_true | C_false | C_proof
 
 val bool : store -> t
+val proof : store -> t
 val c_not : store -> t
 val c_eq : store -> t
 val c_ite : store -> t