ott1

Overview

Ott version 0.34 distribution of Mon Dec 30 10:12:45 GMT 2024

usage: ott <options> <filename1> .. <filenamen>

-i <filename>

Input file (can be used multiple times)

-o <filename>

Output file (can be used multiple times)

-writesys <filename>

Output system definition

-readsys <filename>

Input system definition

-tex_filter <src><dst>

Files to TeX filter

-coq_filter <src><dst>

Files to Coq filter

-hol_filter <src><dst>

Files to HOL filter

-lem_filter <src><dst>

Files to HOL filter

-isa_filter <src><dst>

Files to Isabelle filter

-ocaml_filter <src><dst>

Files to OCaml filter

-merge <false>

merge grammar and definition rules

-parse <string>

Test parse symterm,eg ":nontermroot: term"

-fast_parse <false>

do not parse :rulename: pseudoterminals

-signal_parse_errors <false>

return >0 if there are bad defns

-picky_multiple_parses <false>

Picky about multiple parses

-quotient_rules <true>

Quotient rules, as per {{ quotient-with ntr }} homs

-generate_aux_rules <true>

Generate auxiliary rules or constructor arguments from {{ aux ... }} homs

-aux_style_rules <true>

Auxiliary rules (true) vs constructor arguments (false)

-output_source_locations <0>

Include source location info in output (0=none, 1=drules, 2=grammar+drules)

-colour <true>

Use (vt220) colour for ASCII pretty print

-show_sort <false>

Show ASCII pretty print of syntax

-show_defns <false>

Show ASCII pretty print defns

-tex_show_meta <true>

Include meta prods and rules in TeX output

-tex_show_categories <false>

Signal production flags in TeX output

-tex_suppress_category <[]>

Suppress productions and rules with this category in TeX output

-tex_suppress_ntr <[]>

Suppress nonterminal root in TeX output

-tex_colour <true>

Colour parse errors in TeX output

-tex_wrap <true>

Wrap TeX output in document pre/postamble

-tex_name_prefix <string>

Prefix for tex commands (default "ott")

-isabelle_primrec <true>

Use "primrec" instead of "fun" for functions

-isabelle_inductive <true>

Use "inductive" instead of "inductive_set" for relations

-isa_syntax <false>

Use fancy syntax in Isabelle output

-isa_generate_lemmas <false>

Lemmas for collapsed functions in Isabelle

-coq_avoid <1>

coq type-name avoidance (0=nothing, 1=avoid, 2=secondaryify)

-coq_expand_list_types <false>

Expand list types in Coq output

-coq_lngen <false>

lngen compatibility

-coq_names_in_rules <true>

Copy user names in rule definitions

-coq_use_filter_fn <false>

Use list_filter instead of list_minus2 in substitutions

-ocaml_include_terminals <false>

Include terminals in OCaml output (experimental!)

-ocaml_pp

<target.ml filename> generate OCaml AST pretty printer files (experimental!) (also included in .mly target)

-ocaml_pp_ast_module

override default OCaml module name for AST module (experimental!)

-ocaml_pp_json <false>

Include JSON output in pretty printer (experimental)

-pp_grammar

(debug) print term grammar

-dot <filename>

(debug) dot graph of syntax dependencies

-alltt <filename>

(debug) alltt output of single source file

-sort <true>

(debug) do topological sort

-process_defns <true>

(debug) process inductive reln definitions

-showraw <false>

(debug) show raw grammar

-ugly <false>

(debug) use ugly ASCII output

-no_rbcatn <true>

(debug) remove relevant bind clauses

-lem_debug

(debug) print lem debug locations

-help

Display this list of options

--help

Display this list of options