LocusLocus : positions in hypotheses and goals.
'a or_var represents either a value of type 'a or a variable.
type 'a occurrences_gen = | AllOccurrences | |
| AtLeastOneOccurrence | |
| AllOccurrencesBut of 'a list | (* The list should be non-empty. *) |
| NoOccurrences | |
| OnlyOccurrences of 'a list | (* The list should be non-empty. *) |
Occurences in a hypothesis or conclusion.
type occurrences_expr = int or_var occurrences_gentype 'a with_occurrences_expr = occurrences_expr * 'atype occurrences = int occurrences_gentype 'a with_occurrences = occurrences * 'aIn a hypothesis, occurrences can refer to the body (if any), to the type, or to both.
type 'a hyp_location_expr = 'a with_occurrences_expr * hyp_location_flagA clause_expr (and its instance clause) denotes occurrences and hypotheses in a goal in an abstract way; in particular, it can refer to the set of all hypotheses independently of the effective contents of the current goal.
Concerning the field onhyps:
None means *on every hypothesis*.Some hyps means on hypotheses belonging to hyps.type clause = Names.Id.t clause_exprtype clause_atom = | OnHyp of Names.Id.t * occurrences_expr * hyp_location_flag |
| OnConcl of occurrences_expr |
clause_atom refers either to:
type concrete_clause = clause_atom listA concrete_clause is a collection of occurrences in hypotheses and in the conclusion.
type hyp_location = Names.Id.t * hyp_location_flagA hyp_location is a hypothesis together with a location in this hypothesis (body, type, or both).
type goal_location = hyp_location optionA goal_location is either:
None).type simple_clause = Names.Id.t option listA simple_clause is a set of hypotheses, possibly extended with the conclusion (conclusion is represented by None).