This file implements utilities for dealing with $property and $counterexample pragmas.
val find_properties :
'a Ast_defs.ast ->
(string * string * Ast.l * 'a Ast.val_spec) Ast_util.Bindings.tfind_properties defs returns a mapping from ids to of 4-tuples of the form (prop_type, command, loc, val_spec), which contains the information from any pragmas of the form
$prop_type command ... val <val_spec>
where prop_type is either "counterexample" or "property" and the location loc is the location that was attached to the pragma
val rewrite : Type_check.tannot Ast_defs.ast -> Type_check.tannot Ast_defs.astFor a property
$prop_type val f : forall X, C. T -> bool
find the function body for id:
function f(args) = exp
and rewrite the function body to
function f(args) = if constraint(not(C)) then true else exp
The reason we do this is that the type information in T constrained by C might be lost when translating to Jib, as Jib types are simpler and less precise. If we then do random test generation/proving we want to ensure that inputs outside the constraints of the function are ignored.
val string_of_event : event -> stringmodule Event : sig ... endval default_query : queryval parse_pragma : Parse_ast.l -> string -> pragma