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) |