Module `Locusops`

val or_var_map : ('a -> 'b) -> 'a Locus.or_var -> 'b Locus.or_var

val occurrences_map : ('a list -> 'b list) -> 'a Locus.occurrences_gen -> 'b Locus.occurrences_gen

Counting occurrences

type occurrences_count: A counter of occurrences associated to a list of occurrences

val initialize_occurrence_counter : Locus.occurrences -> occurrences_count: Initialize an occurrence_counter

val update_occurrence_counter : occurrences_count -> bool * occurrences_count: Increase the occurrence counter by one and tell if the current occurrence is selected

val check_used_occurrences : occurrences_count -> unit: Increase the occurrence counter and tell if the current occurrence is selected

val current_occurrence : occurrences_count -> int: Tell the value of the current occurrence

val occurrences_done : occurrences_count -> bool: Tell if there are no more occurrences to select and if the loop can be shortcut

val more_specific_occurrences : occurrences_count -> bool: Tell if there are no more occurrences to select (or unselect) and if an inner loop can be shortcut

Miscellaneous

val is_selected : int -> Locus.occurrences -> bool
val is_all_occurrences : 'a Locus.occurrences_gen -> bool
val error_invalid_occurrence : int list -> 'a

val allHypsAndConcl : 'a Locus.clause_expr
val allHyps : 'a Locus.clause_expr
val onConcl : 'a Locus.clause_expr
val nowhere : 'a Locus.clause_expr
val onHyp : 'a -> 'a Locus.clause_expr

val is_nowhere : 'a Locus.clause_expr -> bool

val simple_clause_of : (unit -> Names.Id.t list) -> Locus.clause -> Locus.simple_clause
val concrete_clause_of : (unit -> Names.Id.t list) -> Locus.clause -> Locus.concrete_clause

val occurrences_of_hyp : Names.Id.t -> Locus.clause -> Locus.occurrences * Locus.hyp_location_flag
val occurrences_of_goal : Locus.clause -> Locus.occurrences
val in_every_hyp : Locus.clause -> bool
val clause_with_generic_occurrences : 'a Locus.clause_expr -> bool
val clause_with_generic_context_selection : 'a Locus.clause_expr -> bool