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