Top

This file has been processed with:

ocamlorn --library stdlib.mli \ --library natlist.in.ml --input natlist.in.ml --lifting natlist.lif.ml \ > natlist.out.ml

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(#3, _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 patch #3[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)