module Target: sig .. end
Datatype and Function for Targets
type
| |
Target_hol |
| |
Target_ocaml |
| |
Target_isa |
| |
Target_coq |
| |
Target_tex |
| |
Target_html |
| |
Target_lem |
A datatype for Targets. In contrast to the one in
ast.ml this one does not carry white-space information.
type
target for the typechecked ast is either a real target as in the AST or
the identity target
val ast_target_to_target : Ast.target -> non_ident_target
ast_target_to_target t converts an ast-target to a
target. This essentially means dropping the white-space information.
val target_to_ast_target : non_ident_target -> Ast.target
target_to_ast_target t converts a target t to an
ast_target. This essentially means adding empty white-space information.
val ast_target_compare : Ast.target -> Ast.target -> int
ast_target_compare is a comparison function for ast-targets.
val target_compare : non_ident_target -> non_ident_target -> int
target_compare is a comparison function for targets.
module Targetmap: sig .. end
target keyed finite maps
module Targetset: Set.S with type elt = non_ident_target
target sets
val all_targets_list : non_ident_target list
A list of all the targets.
val all_targets : Targetset.t
The set of all the targets.
val all_targets_non_explicit : Targetset.t
The set of targets used when negating or no mentioning explicit targets. Targets like Lem are excluded by default.
val non_ident_target_to_string : non_ident_target -> string
non_ident_target_to_string t returns a string description of a target t.
val target_to_string : target -> string
target_to_string t_opt returns a string description of a target.
If some target is given, it does the same as target_to_string. Otherwise,
it returns a string description of the identity backend.
val non_ident_target_to_mname : non_ident_target -> Name.t
non_ident_target_to_mname t returns a name for a target. It is similar to
non_ident_target_to_string t. However, it returns capitalised versions.
val target_to_output : Ast.target -> Output.t
target_to_output t returns output for a target t.
val is_human_target : target -> bool
is_human_target targ checks whether targ is a target intended to be read by humans
and therefore needs preserving the original structure very closely. Examples for such targets are
the tex-, html- and identity-targets.
val dest_human_target : target -> non_ident_target option
dest_human_target targ destructs targ to get the non-identity target. If it s a human-target,
None is returned, otherwise the non-identity target.