The heap predicates have a field that indicates which predicates are precise, and for those it splits up the arguments into inputs and outpus.
|
Module Type HeapPredicateKit (Import B : Base). |
|
(** Heap Predicates *) |
|
(* Predicate names. *) |
|
Parameter Inline 𝑯 : Set. |
|
(* Predicate field types. *) |
|
Parameter Inline 𝑯_Ty : 𝑯 -> Ctx Ty. |
|
(* Duplicable? *) |
|
#[export] Declare Instance 𝑯_is_dup : IsDuplicable 𝑯. |
|
|
|
#[export] Declare Instance 𝑯_eq_dec : EqDec 𝑯. |
|
|
|
Parameter 𝑯_precise : forall p : 𝑯, option (Precise 𝑯_Ty p). |
|
|
|
End HeapPredicateKit. |
I wonder why we went with that definition instead of defining inputs and outputs positions for all predicates uniformly. I think this would improve the code.
The heap predicates have a field that indicates which predicates are precise, and for those it splits up the arguments into inputs and outpus.
katamaran/theories/Syntax/Predicates.v
Lines 56 to 69 in b7d951c
I wonder why we went with that definition instead of defining inputs and outputs positions for all predicates uniformly. I think this would improve the code.