sig
type abstract = Existing of int | Fresh of Agent.t
type 'a port = 'a * int
type 'a arrow =
ToNode of 'a Navigation.port
| ToNothing
| ToInternal of int
type 'a step = 'a Navigation.port * 'a Navigation.arrow
type 'a t = 'a Navigation.step list
val print :
Signature.s ->
(int -> int) ->
Format.formatter -> Navigation.abstract Navigation.t -> unit
val step_to_yojson :
Navigation.abstract Navigation.step -> Yojson.Basic.json
val step_of_yojson :
Yojson.Basic.json -> Navigation.abstract Navigation.step
val to_yojson : Navigation.abstract Navigation.t -> Yojson.Basic.json
val of_yojson : Yojson.Basic.json -> Navigation.abstract Navigation.t
val rename :
Renaming.t ->
Navigation.abstract Navigation.t ->
Renaming.t * Navigation.abstract Navigation.t
val compatible_fresh_point :
Navigation.abstract Navigation.step ->
Agent.t ->
int -> Navigation.abstract Navigation.arrow -> Renaming.t option
val is_subnavigation :
Renaming.t ->
Navigation.abstract Navigation.t ->
Navigation.abstract Navigation.t ->
(Renaming.t * Navigation.abstract Navigation.t) option
val check_edge : Edges.t -> Navigation.abstract Navigation.step -> bool
val injection_for_one_more_edge :
?root:Agent.t ->
Renaming.t ->
Edges.t -> Navigation.abstract Navigation.step -> Renaming.t option
val imperative_edge_is_valid :
?root:Agent.t ->
Renaming.t -> Edges.t -> Navigation.abstract Navigation.step -> bool
val concretize :
Agent.t ->
Edges.t -> Navigation.abstract Navigation.t -> int Navigation.t option
end