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

feat(level): more judgements

Browse source
This commit is contained in:
Simon Cruanes 2023-03-01 22:36:56 -05:00
parent 2c435a5c18
commit 39aa3d7f64
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 21 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/core-logic/level.ml
View file

@ -183,7 +183,7 @@ let as_int self : _ option =
let is_int self : bool = Option.is_some (as_int self)
let leq_judge st l1 l2 : bool =
let judge_leq st l1 l2 : bool =
assert (store_id l1 = st.id);
assert (store_id l2 = st.id);
@ -232,5 +232,8 @@ let leq_judge st l1 l2 : bool =
let l2, n = as_offset l2 in
prove l1 l2 n
let eq_judge st l1 l2 : bool =
equal l1 l2 || (leq_judge st l1 l2 && leq_judge st l2 l1)
let judge_eq st l1 l2 : bool =
equal l1 l2 || (judge_leq st l1 l2 && judge_leq st l2 l1)
let judge_is_zero st l : bool = judge_leq st l (zero st)
let judge_is_nonzero st l : bool = judge_leq st (one st) l

21
src/core-logic/level.mli
View file

@ -40,12 +40,21 @@ val is_one : t -> bool
val is_int : t -> bool
val as_int : t -> int option
(** {2 Equivalence} *)
(** {2 Judgements}
val leq_judge : store -> t -> t -> bool
(** [leq_judge st l1 l2] is [true] if [l1] is proven to be lower
These are little proofs of some symbolic properties of levels, even
those which contain variables. *)
val judge_leq : store -> t -> t -> bool
(** [judge_leq st l1 l2] is [true] if [l1] is proven to be lower
or equal to [l2] *)
val eq_judge : store -> t -> t -> bool
(** [eq_judge st l1 l2] is [true] iff [leq_judge l1 l2]
and [leq_judge l2 l1] *)
val judge_eq : store -> t -> t -> bool
(** [judge_eq st l1 l2] is [true] iff [judge_leq l1 l2]
and [judge_leq l2 l1] *)
val judge_is_zero : store -> t -> bool
(** [judge_is_zero st l] is [true] iff [l <= 0] holds *)
val judge_is_nonzero : store -> t -> bool
(** [judge_is_nonzero st l] is [true] iff [1 <= l] holds *)