Top

This has been processed with:

## Code refinement

(code in `tests`

`/`

`natlist`

`.`

`ml`

, run with `./`

`ocamlorn`

` `

`tests`

`/`

`natlist`

`.`

`ml`

)
We start with the following code operating on natural numbers:

type nat =
| Z
| S of nat |

let rec add m n = match m with
| Z -> n
| S m' -> S (add m' n) |

We declare a datatype of lists, and an ornamentation relation:

type 'a list =
| Nil
| Cons of 'a * 'a list |

type ornament 'a natlist : nat => 'a list with
| Z => Nil
| S n => Cons (_,n) when n : 'a natlist |

We then request an ornament at this type:

let _append = lifting add : _ natlist -> _ natlist -> _ natlist |

The system outputs a version of `append`

with a hole:

let rec _append m n = match m with
| Nil -> n
| Cons(_, m') -> Cons(#2, _append m' n) |

We can provide a patch to fill the hole, using the variables named in the original code, and the patch identifier given in the incomplete term:

let append = lifting add : _ natlist -> _ natlist -> _ natlist with
#2 <- match m with Cons (a, _) -> a |

We then obtain an implementation of `append`

:

let rec append m n = match m with
| Nil -> n
| Cons(a, m') -> Cons(a, append m' n) |