ONijn is an OCaml module of Nijn. It is intended to be used as a tool to generate Coq termination certification scripts from the output of termination tools.

The public API consists of three modules: `Syntax`

, `Coq`

, and `Parser`

.

`Syntax`

Provides submodules for syntactic constructions. It contains representations for Types, Terms, Polynomials, and rewriting rules.

`Coq`

Provides interfacing to generate strings that are valid coq constructions. For more details, check the`Coq.Grammar`

and`Coq.Proof_script`

modules.

`Parser`

Provides abstract interfacing for creating parsers of file formats accepted by**ONijn**.

In order to certify terminaion of a rewriting system, one must first represent the certificate (stating the termination property) in a way that **onijn** understands it.

The rewriting formalism of accepted by **onijn** is AFS (Algebraic Functional Systems).

```
answer := YES | NO | MAYBE
sort, fn, var := ['a'-'z' 'A'-'Z'] ['a'-'z' 'A'-'Z' '0'-'9']*
type := sort | type -> type
term := var | fn | term term | /\var.term
rewrite_rule := term => term
```

Where `answer`

represents the termination status given by a termination tool. In the construct for `sort`

, `fn`

, and `var`

, the regex expression `['a'-'z' 'A'-'Z'] ['a'-'z' 'A'-'Z' '0'-'9']*`

stating the string format accepted as names for sorts, function symbols, and variables, respectively.

In algebraic functional systems, type declarations and types are not the same. The `type`

construct defines the usual simple types. Expressions in `type`

are parsed assuming that `=>`

is right-associative, as usual.

We can already represent signature and rewriting systems. Let us take the `map`

TRS as exemple.

```
map F nil => nil
map F (hd :: tl) => F(hd) :: (map F tl)
```

In **onijn** format this system is represented as:

```
Signature: [
cons : a -> list -> list ;
map : list -> (a -> a) -> list ;
nil : list
]
Rules: [
map nil F => nil ;
map (cons X Y) G => cons (G X) (map Y G)
]
```

We represent polynomials with the grammar below:

```
var := ['a'-'z' 'A'-'Z'] ['a'-'z' 'A'-'Z' '0'-'9']*
poly := n | var | var(poly) | poly + poly | poly * poly
poly_fun := Lam[var_1; ...; var_n] . poly
poly_int := J(fn) = poly_fun
```

Continuing with the map example, we represet an interpretation for it in **onijn** as follows:

```
Interpretation: [
J(cons) = Lam[y0;y1].3 + 2*y1;
J(map) = Lam[y0;G1].3*y0 + 3*y0*G1(y0);
J(nil) = 3
]
```

An **onijn** file must end with a list of rules that can be oriented with the given interpretation.

```
Removed: [
map nil F => nil ;
map (cons X Y) G => cons (G X) (map Y G)
]
```

Putting everything together we get a file `map_trs.onijn`

as follows:

```
(** This is a comment. It will be ignored by onijn. **)
YES
Signature: [
cons : a -> list -> list ;
map : list -> (a -> a) -> list ;
nil : list
]
Rules: [
map nil F => nil ;
map (cons X Y) G => cons (G X) (map Y G)
]
Interpretation: [
J(cons) = Lam[y0;y1].3 + 2*y1 ;
J(map) = Lam[y0;G1].3*y0 + 3*y0*G1(y0) ;
J(nil) = 3
]
Removed: [
map nil F => nil ;
map (cons X Y) G => cons (G X) (map Y G)
]
```