simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(core-logic): add builtin Proof type

Browse source 
not used yet
This commit is contained in:
Simon Cruanes 2022-10-12 12:22:04 -04:00
parent 7db5e1a902
commit 46c44648e1
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/core-logic/t_builtins.ml
View file

@ -1,7 +1,7 @@
open Types_ open Types_
open Term 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 let to_string = function
| C_bool -> "Bool" | C_bool -> "Bool"
@ -10,6 +10,7 @@ let to_string = function
| C_not -> "not" | C_not -> "not"
| C_true -> "true" | C_true -> "true"
| C_false -> "false" | C_false -> "false"
| C_proof -> "Proof"
| _ -> assert false | _ -> assert false
let of_string = function let of_string = function
@ -19,12 +20,14 @@ let of_string = function
| "not" -> Some C_not | "not" -> Some C_not
| "true" -> Some C_true | "true" -> Some C_true
| "false" -> Some C_false | "false" -> Some C_false
| "Proof" -> Some C_proof
| _ -> None | _ -> None
let ops : const_ops = let ops : const_ops =
let equal a b = let equal a b =
match a, b with match a, b with
| C_bool, C_bool | C_bool, C_bool
| C_proof, C_proof
| C_eq, C_eq | C_eq, C_eq
| C_ite, C_ite | C_ite, C_ite
| C_not, C_not | C_not, C_not
@ -41,6 +44,7 @@ let ops : const_ops =
| C_not -> CCHash.int 170 | C_not -> CCHash.int 170
| C_true -> CCHash.int 171 | C_true -> CCHash.int 171
| C_false -> CCHash.int 172 | C_false -> CCHash.int 172
| C_proof -> CCHash.int 173
| _ -> assert false | _ -> assert false
in in
@ -61,6 +65,7 @@ let const_decoders : Const.decoders =
] ]
let bool store = const store @@ Const.make C_bool ops ~ty:(type_ store) 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 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) let false_ store = const store @@ Const.make C_false ops ~ty:(bool store)

3
src/core-logic/t_builtins.mli
View file

@ -3,9 +3,10 @@
open Types_ open Types_
open Term 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 bool : store -> t
val proof : store -> t
val c_not : store -> t val c_not : store -> t
val c_eq : store -> t val c_eq : store -> t
val c_ite : store -> t val c_ite : store -> t