type value = [
    | `Unit
    | `Pair of value * value
    | `Inl of value
    | `Inr of value ]

type u = [`Unit]

type valrt = [ `Inl of u
             | `Inr of [ `Inl of u
                       | `Inr of [`Inl of u]]]

let none   : valrt = `Inl `Unit
let medium : valrt = `Inr (`Inl `Unit)
let all    : valrt = `Inr (`Inr (`Inl `Unit))

let plus (x : valrt) (y : valrt) =
  match x with
    | `Inl _ -> y (* x = none *)
    | `Inr x1 ->
        match x1 with
          | `Inl _ -> (* x = medium *)
              (match y with
                 | `Inl _ -> medium (* y = none *)
                 | `Inr _ -> all (* y = medium or none *))
          | `Inr _ -> all (* x = all *)

let mult (x : valrt) (y : valrt) =
  match x with
    | `Inl _ -> none (* x = none *)
    | `Inr x1 ->
        match x1 with
          | `Inl _ -> (* x = medim *)
              (match y with
                 | `Inl _ -> none (* y = none *)
                 | `Inr _ -> medium )
          | `Inr _ -> y

let split (`Pair (x, y)) = (x, y)

type direction = [`Inl of u | `Inr of u]

let towards : direction = `Inl `Unit
let away : direction = `Inr `Unit

type surface =
    [`Pair of direction * [`Pair of valrt * [`Pair of valrt * valrt]]]

let d (s : surface) =
  let (l, r) = split s in l

let r (s : surface) =
  let (_, r) = split s in
  let (l, _) = split r in l

let t (s : surface) =
  let (_, r) = split s in
  let (_, r1) = split r in
  let (l, _) = split r1 in l

let e (s : surface) =
  let (_, r) = split s in
  let (_, r1) = split r in
  let (_, r2) = split r1 in r2

type 'a vlist = [`Inl of [`Pair of 'a * 'b] | `Inr of [`Unit]] as 'b

let rec rev_append (ln : 'a vlist) (lw : 'a vlist) : 'a vlist =
  match ln with
    | `Inl i ->
        let (e, qln) = split i in
        let lw1 = `Inl (`Pair (e, lw)) in
          rev_append qln lw1
    | `Inr _ -> lw

let rev l =
  let nil = `Inr `Unit in
    rev_append l nil

type info_list_elem =
    [`Pair of surface (* Si *) * [`Pair of valrt (* li *) * valrt (* ri *)]]
type info_list = info_list_elem vlist

let compute_val s e12 =
  let (e1, e2) = split e12 in
  let es = e s
  and ts = t s
  and rs = r s in
  let v1 = mult rs e1
  and v2 = mult ts e2 in
  let v3 = plus v1 v2 in
    plus es v3

let rec update_ri rim1 (s : info_list) : info_list =
  match s with
    | `Inr _ -> `Inr `Unit
    | `Inl i ->
        let v, qs = split i in
        let si, lri = split v in
        let li, ri = split lri in
        let ri1 =
          match d si with
            | `Inr _ (* away *) ->
                let arg = `Pair (li, rim1) in
                  compute_val si arg
            | `Inl _ (* towards *) ->
                rim1
        in
        let lri1 = `Pair (li, ri1) in
        let v1 = `Pair (si, lri1) in
        let qs1 = update_ri ri1 qs in
          `Inl (`Pair (v1, qs1))

type arg_update_li = [`Pair of valrt (* lip1 *) * surface (* sip1 *)]

let rec update_li (w : arg_update_li) (revs : info_list) : info_list =
  match revs with
    | `Inr _ -> `Inr `Unit
    | `Inl i ->
        let lip1, sip1 = split w in
        let v, qrevs = split i in
        let si, lri = split v in
        let li, ri = split lri in
        let li1 =
          match d sip1 with
            | `Inl _ (* towards *) ->
                let arg = `Pair (ri, lip1) in
                  compute_val sip1 arg
            | `Inr _ (* away *) ->
                lip1
        in
        let lri1 = `Pair (li1, ri) in
        let v1 = `Pair (si, lri1) in
        let w1 = `Pair (li1, si) in
        let qrevs1 = update_li w1 qrevs in
          `Inl (`Pair (v1, qrevs1))

(* The computation of Li uses S(i+1) and is not defined on Ln *)
let start_update_li (revs : info_list) : info_list =
  match revs with
    | `Inr _ -> `Inr `Unit
    | `Inl i ->
        let v, qrevs' = split i in
        let si, _ = split v in
        let arg_update = `Pair (none (* = Ln *), si) in
        let qrevs'' = update_li arg_update qrevs' in
          `Inl (`Pair (v, qrevs''))

let update (s : info_list) : info_list =
  let s' = update_ri none s in
  let revs' = rev s' in
  let revs'' = start_update_li revs' in
  let s'' = rev revs'' in
    s''

type boolean = [ `Inl of u | `Inr of u]

let tr : boolean = `Inl `Unit
let fal : boolean = `Inr `Unit

let rec equal_valrt (x : valrt) (y : valrt) : boolean =
  match x with
    | `Inl _ ->
        (match y with
           | `Inl _ -> tr
           | `Inr _ -> fal)
    | `Inr v ->
        (match y with
           | `Inl _ -> tr
           | `Inr v' -> equal_valrt (v :> valrt) (v' :> valrt))

let equal_info_list_elem (x : info_list_elem) (y : info_list_elem) : boolean =
  let (sx, vx) = split x in
  let (sy, vy) = split y in
  let (lix, rix) = split vx in
  let (liy, riy) = split vy in
    match equal_valrt lix liy with
      | `Inl _ -> (* true *)
          equal_valrt rix riy
      | `Inr _ -> (* false *) fal

(* Give me some dependent types ! *)
let rec equal_info_list (l1 : info_list) (l2 : info_list) : boolean =
  match l1 with
    | `Inl v1 ->
        (match l2 with
          | `Inl v2 ->
              let (v1, q1) = split v1 in
              let (v2, q2) = split v2 in
                (match equal_info_list_elem v1 v2 with
                   | `Inl _ -> equal_info_list q1 q2
                   | `Inr _ -> fal)
          | `Inr _ -> assert false)
    | `Inr _ -> tr (* both lists are empty *)

let rec iterate (s : info_list) : info_list =
  let s' = update s in
    match equal_info_list s s' with
      | `Inl _ -> s
      | `Inr _ -> iterate s'

let rec add_lri (l: surface vlist) : info_list =
  match l with
    | `Inl i ->
        let (s, q) = split i in
        let q1 = add_lri q in
          `Inl (`Pair (`Pair (s, `Pair (none, none)), q1))
    | `Inr _  -> `Inr `Unit

let get_l0 (s: info_list) : valrt =
  match s with
    | `Inl i1 ->
        let (v1, _) = split i1 in
        let (s1, lr1) = split v1 in
        let (l1, r1) = split lr1 in
          (match d s1 with
             | `Inl _ (* towards *) ->
                 let arg = `Pair (none (* = R0 *), l1) in
                   compute_val s1 arg
             | `Inr _ (* away *) ->
                 l1)
    | `Inr _ -> none (* n = 0, result is Ln *)

let main (s: surface vlist) : valrt =
  let l = add_lri s in
  let l1 = iterate l in
    get_l0 l1

(**** TESTS, NOT TO BE TRANSLATED *)

(*
let test_rev =
  rev (`Inl (`Pair (1, `Inl (`Pair (2, `Inl (`Pair (3, `Inr `Unit)))))))
*)

let s (d, r, t, e) : surface = `Pair (d, `Pair (r, `Pair (t, e)))

let nil : 'a vlist = `Inr `Unit
let cons (e : 'a) (l : 'a vlist) : 'a vlist =
  `Inl (`Pair (e, l))

let med = medium

let s = List.map s [
away, all, none, none;
towards, none, none, med;
away, all, all, med;
towards, all, none, none;
away, none, med, none;
towards, med, all, none;
(*away, med, med, med;
towards, med, med, all;
away, none, all, none;
towards, none, none, all;*)
]

let rec list_to_vlist : 'a list -> 'a vlist = function
  | e :: q -> cons e (list_to_vlist q)
  | [] -> `Inr `Unit

let s = list_to_vlist s

let rec print_valrt : valrt -> unit = function
  | `Inl `Unit -> print_string "none"
  | `Inr (`Inl `Unit) -> print_string "medium"
  | `Inr (`Inr (`Inl `Unit)) -> print_string "all"

let rec print_list_val : info_list -> unit = function
  | `Inl (`Pair (`Pair (_, `Pair (li, ri)), q)) ->
      print_string "L: ";
      print_valrt li;
      print_string "  R: ";
      print_valrt ri;
      print_string "\n";
      print_list_val q
  | `Inr `Unit -> ()

let main_test (s: surface vlist) =
  let l = add_lri s in
  let l1 = iterate l in
    get_l0 l1, l1

let _ =
  let e, l = main_test s in
    print_string "L0: ";
    print_valrt e;
    print_string "  R0: ";
    print_valrt none;
    print_string "\n";
    print_list_val l

This document was generated using caml2html