(* 'a option is an ornament of bool *)
type bool = True | False
type 'a option = Some of 'a | None

let is_some = fun ['a] (x : 'a option) => match x with
  | Some(y) => True
  | None => False
 end

let forall 'a ornament is_some ['a] : 'a option -> bool

(* Dummy implementation of key and compare *)
type key = Key
let rec compare : key -> key -> int = compare

(* Implementation of sets *)
type set = Empty | Node of key * set * set

let empty = Empty
let rec find : key -> set -> bool = fun (k : key) (s : set) =>
  match s with
    | Empty => False
    | Node(k',l,r) =>
       if eq (compare k k') 0 then True
       else if gt (compare k k') 0 then find k l
       else find k r
  end 

(* Maps are an ornament of sets *)
type 'a map = MEmpty | MNode of key * 'a * 'a map * 'a map

let rec keys : forall 'a. 'a map -> set = fun ['a] (m : 'a map) =>
  match m with
    | MEmpty => Empty
    | MNode(k,v,l,r) => Node(k,keys ['a] l,keys ['a] r)
  end 

let forall 'a ornament keys ['a] : 'a map -> set

(* Code generation *)
let ornament mempty from empty with forall +'a. {keys ['a]}
let ornament mfind from find with forall +'a. [key]  -> {keys ['a]} -> {is_some ['a]}