(* type u = [()] *)

(* type valrt = [Inl of u |
             Inr of [Inl of u |
                      Inr of [Inl of u]]]    *)

value fst x = let (y, _) = x in y;
value snd x = let (_, y) = x in y;

value plus x y =
  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 *) ] ];

value mult x y =
  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 ] ];

(* type direction = [Inl of u | Inr of u] *)

(* type surface =
    [Pair of direction * [Pair of valrt * [Pair of valrt * valrt]]]    *)

value r s = fst (snd s);

value t s = fst (snd (snd s));

value e s = snd (snd (snd s));

(* type 'a vlist = ([Inl of [Pair of 'a * 'b] | Inr of [()]] as 'b) *)

value rec revAppend ln lw =
  match ln with
    [ Inl i ->
        let (e, qln) = i in
        let lw1 = Inl (e, lw) in
          revAppend qln lw1
    | Inr _ -> lw ];

value rev l =
  let nil = Inr () in
    revAppend l nil;

(* type infoListElem = *)
    (* [Pair of surface |+ Si +| * [Pair of valrt |+ li +| * valrt |+ ri +|]] *)
(* type infoList = infoListElem vlist *)

value computeVal s e12 =
  let (e1, e2) = e12 in
  let es = e s in
  let ts = t s in
  let rs = r s in
  let v1 = mult rs e1 in
  let v2 = mult ts e2 in
  let v3 = plus v1 v2 in
    plus es v3;

value computeValAway si arg =
  match fst si with
  [ Away -> computeVal si arg
  | Towards -> snd arg ];

value rec updateRi rim1 s =
  match s with
    [ Inr _ -> Inr ()
    | Inl i ->
        let (v, qs) = i in
        let (si, lri) = v in
        let (li, ri) = lri in
        let ri1 = computeValAway si (li, rim1) in
        let lri1 = (li, ri1) in
        let v1 = (si, lri1) in
        let qs1 = updateRi ri1 qs in
          Inl (v1, qs1) ];

(* type argUpdateLi = [Pair of valrt |+ lip1 +| * surface |+ sip1 +|] *)

value computeValTowards sip1 arg =
  match fst sip1 with
  [ Towards -> computeVal sip1 arg
  | Away -> snd arg ];

value rec updateLi w revs =
  match revs with
    [ Inr _ -> Inr ()
    | Inl i ->
        let (lip1, sip1) = w in
        let (v, qrevs) = i in
        let (si, lri) = v in
        let (li, ri) = lri in
        let li1 = computeValTowards sip1 (ri, lip1) in
        let lri1 = (li1, ri) in
        let v1 = (si, lri1) in
        let w1 = (li1, si) in
        let qrevs1 = updateLi w1 qrevs in
          Inl (v1, qrevs1) ];

(* The computation of Li uses S(i+1) and is not defined on Ln *)
value startUpdateLi revs =
  match revs with
    [ Inr _ -> Inr ()
    | Inl i ->
        let (v, qrevs') = i in
        let (si, _) = v in
        let argUpdate = (None (* = Ln *), si) in
        let qrevs'' = updateLi argUpdate qrevs' in
          Inl (v, qrevs'') ];

value update s =
  let s' = updateRi None s in
  let revs' = rev s' in
  let revs'' = startUpdateLi revs' in
  let s'' = rev revs'' in
    s'';

(*
value rec equalValrt x y =
  match x with
    [ Inl _ ->
        match y with
        [ Inl _ -> True
        | Inr _ -> False ]
    | Inr v ->
        match y with
        [ Inl _ -> True
        | Inr v' -> equalValrt v v' ] ];

value equalInfoListElem x y =
  let (sx, vx) = x in
  let (sy, vy) = y in
  let (lix, rix) = vx in
  let (liy, riy) = vy in
    match equalValrt lix liy with
      [ True -> equalValrt rix riy
      | False -> False ];
*)

(*
(* Give me some dependent types ! *)
value rec equalInfoList l1 l2 =
  match l1 with
    [ Inl v1 ->
        match l2 with
        [ Inl v2 ->
            let (v1, q1) = v1 in
            let (v2, q2) = v2 in
              match equalInfoListElem v1 v2 with
              [ Inl _ -> equalInfoList q1 q2
              | Inr _ -> False]
        | Inr _ -> Error ]
    | Inr _ -> True (* both lists are empty *) ];
*)

(*
value rec iterate s =
      let s' = update s in
        update s';
*)
(*
  let s' = update s in
    match equalInfoList s s' with
      [ Inl _ -> s
      | Inr _ -> iterate s' ];
*)

value rec addLri l =
  match l with
    [ Inl i ->
        let (s, q) = i in
        let q1 = addLri q in
          Inl ((s, (None, None)), q1)
    | Inr _  -> Inr () ];

value getL0 s =
  match s with
    [ Inl i1 ->
        let (v1, _) = i1 in
        let (s1, lr1) = v1 in
        let (l1, r1) = lr1 in
          match fst s1 with
          [ Towards ->
                 let arg = (None (* = R0 *), l1) in
                   computeVal s1 arg
          | Away ->
                 l1 ]
    | Inr _ -> None (* n = 0, result is Ln *) ];

value main s =
  let l = addLri s in
  let l1 = update l in
  let l2 = update l1 in
    getL0 l2;