Previous  Up  Next

Module Position

module Position: sig .. end

Positions in terms, clauses...


type t =
| Stop
| Type of t (*
Switch to type
*)
| Left of t (*
Left term in curried application
*)
| Right of t (*
Right term in curried application, and subterm of binder
*)
| Head of t (*
Head of uncurried term
*)
| Arg of int * t (*
argument term in uncurried term, or in multiset
*)
| Body of t (*
Body of binder
*)
A position is a path in a tree
type position = t 
val stop : t
val left : t -> t
val right : t -> t
val type_ : t -> t
val left : t -> t
val right : t -> t
val head : t -> t
val arg : int -> t -> t
val opp : t -> t
Opposite position, when it makes sense (left/right)
val rev : t -> t
Reverse the position
val append : t -> t -> t
Append two positions
val compare : t -> t -> int
val eq : t -> t -> bool
val hash : t -> int
include Interfaces.PRINT

Position builder


module Build: sig .. end