include "RTLabs/syntax.ma".
include "RTL/RTL.ma".
include "common/AssocList.ma".
include "common/Graphs.ma".

definition add_graph ≝
  λl: label.
  λstmt.
  λp.
  let rtl_if_luniverse' ≝ rtl_if_luniverse p in
  let rtl_if_runiverse' ≝ rtl_if_runiverse p in
  let rtl_if_sig' ≝ rtl_if_sig p in
  let rtl_if_result' ≝ rtl_if_result p in
  let rtl_if_params' ≝ rtl_if_params p in
  let rtl_if_locals' ≝ rtl_if_locals p in
  let rtl_if_stacksize' ≝ rtl_if_stacksize p in
  let rtl_if_graph' ≝ add ? ? (rtl_if_graph p) l stmt in
  let rtl_if_entry' ≝ rtl_if_entry p in
  let rtl_if_exit' ≝ rtl_if_exit p in
    mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse' rtl_if_sig'
                             rtl_if_params' rtl_if_params' rtl_if_locals'
                             rtl_if_stacksize' rtl_if_graph' rtl_if_entry'
                             rtl_if_exit'.
      
definition fresh_label ≝
  λdef.
    match fresh LabelTag (rtl_if_luniverse def) with
    [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ)
    | Error ⇒ None ?
    ].

axiom fresh_reg: rtl_internal_function → rtl_internal_function × register.

let rec fresh_regs (def: rtl_internal_function) (n: nat) on n ≝
  match n with
  [ O   ⇒ 〈def, [ ]〉
  | S n ⇒
    let 〈def, res〉 ≝ fresh_regs def n in
    let 〈def, r〉 ≝ fresh_reg def in
      〈def, r :: res〉
  ].

definition addr_regs ≝
  λregs.
  match regs with
  [ cons hd tl ⇒
    match tl with
    [ cons hd' tl' ⇒ Some (register × register) 〈hd, hd'〉
    | nil          ⇒ None (register × register)
    ]
  | nil ⇒ None (register × register)
  ].

inductive register_type: Type[0] ≝
  | register_int: register → register_type
  | register_ptr: register → register → register_type.

definition local_env ≝ assoc_list register register_type.

definition initialize_local_env_internal ≝
  λeq.
  λruniverse.
  λptrs.
  λlenv.
  λr.
    let fresh ≝ snd ? ? (fresh_reg runiverse) in
    let rt ≝
      match member ? eq r ptrs with
      [ true  ⇒ register_ptr r fresh
      | false ⇒ register_int r
      ]
    in
    assoc_list_add ? ? 〈r, rt〉 lenv.

definition initialize_local_env ≝
  λruniverse.
  λptrs.
  λregisters.
    foldl ? ? (initialize_local_env_internal (eq_identifier RegisterTag) runiverse ptrs) [ ] registers.

definition filter_and_to_list_local_env_internal ≝
  λlenv.
  λl.
  λr.
  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
  [ Some entry ⇒
    match entry with
    [ register_ptr r1 r2 ⇒ (l @ [ r1; r2 ])
    | register_int r ⇒ (l @ [ r ])
    ]
  | None       ⇒ [ ] (* dpm: should this be none? *)
  ].

definition filter_and_to_list_local_env ≝
  λlenv.
  λregisters.
    foldl ? ? (filter_and_to_list_local_env_internal lenv) [ ] registers.

definition list_of_register_type ≝
  λrt.
  match rt with
  [ register_ptr r1 r2 ⇒ [ r1; r2 ]
  | register_int r ⇒ [ r ]
  ].

definition find_and_list ≝
  λr.
  λlenv.
  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
  [ None      ⇒ [ ] (* dpm: should this be none? *)
  | Some lkup ⇒ list_of_register_type lkup
  ].

definition find_and_list_args ≝
  λargs.
  λlenv.
    map ? ? (λr. find_and_list r lenv) args.

definition find_and_addr ≝
  λr.
  λlenv.
  match find_and_list r lenv with
  [ cons hd tl ⇒
    match tl with
    [ cons hd' tl' ⇒ Some ? 〈hd, hd'〉
    | nil          ⇒ None ?
    ]
  | nil ⇒ None ? (* dpm: was assert false *)
  ].

definition rtl_args ≝
  λregs_list.
  λlenv.
    flatten ? (find_and_list_args regs_list lenv).

definition change_label ≝
  λlbl.
  λstmt: rtl_statement.
  match stmt with
  [ rtl_st_skip _ ⇒ rtl_st_skip lbl
  | rtl_st_cost cost_lbl _ ⇒ rtl_st_cost cost_lbl lbl
  | rtl_st_addr r1 r2 id _ ⇒ rtl_st_addr r1 r2 id lbl
  | rtl_st_stack_addr r1 r2 _ ⇒ rtl_st_stack_addr r1 r2 lbl
  | rtl_st_int r i _ ⇒ rtl_st_int r i lbl
  | rtl_st_move r1 r2 _ ⇒ rtl_st_move r1 r2 lbl
  | rtl_st_opaccs opaccs d s1 s2 _ ⇒ rtl_st_opaccs opaccs d s1 s2 lbl
  | rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl
  | rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl
  | rtl_st_clear_carry _ ⇒ rtl_st_clear_carry lbl
  | rtl_st_load d a1 a2 _ ⇒ rtl_st_load d a1 a2 lbl
  | rtl_st_store a1 a2 s _ ⇒ rtl_st_store a1 a2 s lbl
  | rtl_st_call_id f a r _ ⇒ rtl_st_call_id f a r lbl
  | rtl_st_call_ptr f1 f2 a r _ ⇒ rtl_st_call_ptr f1 f2 a r lbl
  | rtl_st_tailcall_id f a ⇒ rtl_st_tailcall_id f a
  | rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a
  | rtl_st_cond_acc r l1 l2 ⇒ rtl_st_cond_acc r l1 l2
  | rtl_st_return r ⇒ rtl_st_return r
  | _ ⇒ ?
  ].

let rec adds_graph (stmt_list: ?) (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function) ≝
  match stmt_list with
  [ nil ⇒ Some ? def
  | cons hd tl ⇒
    match tl with
    [ nil ⇒ Some ? (add_graph start_lbl (change_label dest_lbl hd) def)
    | cons hd' tl' ⇒
      let tmp_lbl ≝ fresh_label def in
      match tmp_lbl with
      [ None ⇒ None ?
      | Some tmp_lbl ⇒
        let stmt ≝ change_label tmp_lbl hd in
        let def ≝ add_graph start_lbl stmt def in
          adds_graph tl tmp_lbl dest_lbl def
      ]
    ]
  ].
  
(* dpm: had to lift this into option *)
let rec add_translates (translate_list: ?) (start_lbl: label) (dest_lbl: label)
                       (def: ?) on translate_list ≝
  match translate_list with
  [ nil ⇒ Some ? def
  | cons hd tl ⇒
    match tl with
    [ nil ⇒ hd start_lbl dest_lbl def
    | cons hd' tl' ⇒
      let tmp_lbl ≝ fresh_label def in
      match tmp_lbl with
      [ None ⇒ None ?
      | Some tmp_lbl ⇒
        match hd start_lbl tmp_lbl def with
        [ None ⇒ None ?
        | Some def ⇒ add_translates tl tmp_lbl dest_lbl def
        ]
      ]
    ]
  ].
  

(* dpm: horrendous, use dependent types.
  length destr = length srcrs *)
let rec translate_move (destrs: ?) (srcrs: ?) (start_lbl: label)
                       (dest_lbl: label) (def: ?) ≝
  match destrs with
  [ nil ⇒
    match srcrs with
    [ nil        ⇒ Some ? def
    | cons hd tl ⇒ None ?
    ]
  | cons hd tl ⇒
    match srcrs with
    [ nil        ⇒ None ?
    | cons hd' tl' ⇒
      match tl with
      [ nil            ⇒
        match tl' with
        (* one element lists *)
        [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_move hd hd' dest_lbl) def)
        | cons hd'' tl'' ⇒ None ?
        ]
      | cons hd'' tl'' ⇒
        match tl' with
        [ nil ⇒ None ?
        (* multielement lists *)
        | cons hd''' tl''' ⇒
          let tmp_lbl ≝ fresh_label def in
          match tmp_lbl with
          [ None ⇒ None ?
          | Some tmp_lbl ⇒
            let def ≝ add_graph start_lbl (rtl_st_move hd hd' tmp_lbl) def in
              translate_move tl tl' tmp_lbl dest_lbl def
          ]
        ]
      ]
    ]
  ].

definition translate_cst ≝
  λcst.
  λdestrs.
  λstart_lbl.
  λdest_lbl.
  λdef.
  match cst with
  [ cast_int i ⇒
    match destrs with
    [ nil ⇒ None ?
    | cons hd tl ⇒
      match tl with
      [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_int hd i dest_lbl) def)
      | cons hd' tl' ⇒ None ?
      ]
    ]
  | cast_addr_symbol id ⇒
    match destrs with
    [ nil ⇒ None ?
    | cons hd tl ⇒
      match tl with
      [ nil ⇒ None ?
      | cons hd' tl' ⇒
        Some ? (add_graph start_lbl (rtl_st_addr hd hd' id dest_lbl) def)
      ]
    ]
  | cast_stack_offset off ⇒
    match destrs with
    [ nil ⇒ None ?
    | cons hd tl ⇒
      match tl with
      [ nil ⇒ None ?
      | cons hd' tl' ⇒
        let 〈def, tmpr〉 ≝ fresh_reg def in
        adds_graph [
          rtl_st_stack_addr hd hd' start_lbl;
          rtl_st_int tmpr off start_lbl;
          rtl_st_op2 Add hd hd tmpr start_lbl;
          rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl;
          rtl_st_op2 Addc hd' hd' tmpr start_lbl
        ] start_lbl dest_lbl def
      ]
    ]
  | cast_float f ⇒ None ?
  ].

definition extract_singleton ≝
  λA: Type[0].
  λl: list A.
  match l with
  [ nil ⇒ None ?
  | cons hd tl ⇒
    match tl with
    [ nil ⇒ Some ? hd
    | cons hd tl ⇒ None ?
    ]
  ].

definition extract_pair ≝
  λA: Type[0].
  λl: list A.
  match l with
  [ nil ⇒ None ?
  | cons hd tl ⇒
    match tl with
    [ nil ⇒ None ?
    | cons hd' tl' ⇒
      match tl' with
      [ nil ⇒ Some ? 〈hd, hd'〉
      | cons hd'' tl'' ⇒ None ?
      ]
    ]
  ].

definition translate_op1 ≝
  λop1.
  λdestrs.
  λsrcrs.
  λstart_lbl.
  λdest_lbl.
  λdef.
  match op1 with
  [ op_cast8_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def
  | op_cast8_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def
  | op_cast16_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def
  | op_cast16_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def
  | op_neg_int ⇒
    let dstr ≝ extract_singleton ? destrs in
    let srcr ≝ extract_singleton ? srcrs in
    match dstr with
    [ None ⇒ None ?
    | Some dstr ⇒
      match srcr with
      [ None ⇒ None ?
      | Some srcr ⇒
        adds_graph [
          rtl_st_op1 Cmpl dstr srcr start_lbl;
          rtl_st_op1 Inc dstr dstr start_lbl
        ] start_lbl dest_lbl def
      ]
    ]
  | op_not_int ⇒
    let dstr ≝ extract_singleton ? destrs in
    let srcr ≝ extract_singleton ? srcrs in
    match dstr with
    [ None ⇒ None ?
    | Some dstr ⇒
      match srcr with
      [ None ⇒ None ?
      | Some srcr ⇒
        adds_graph [
          rtl_st_op1 Cmpl dstr srcr start_lbl
        ] start_lbl dest_lbl def
      ]
    ]
  | op_id ⇒ translate_move destrs srcrs start_lbl dest_lbl def
  | op_ptr_of_int ⇒
    let destr12 ≝ extract_pair ? destrs in
    let srcr ≝ extract_singleton ? srcrs in
    match destr12 with
    [ None ⇒ None ?
    | Some destr12 ⇒
      let 〈destr1, destr2〉 ≝ destr12 in
      match srcr with
      [ None ⇒ None ?
      | Some srcr ⇒
        adds_graph [
          rtl_st_move destr1 srcr dest_lbl;
          rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl
        ] start_lbl dest_lbl def
      ]
    ]
  | op_int_of_ptr ⇒
    let destr ≝ extract_singleton ? destrs in
    match destr with
    [ None ⇒ None ?
    | Some destr ⇒
      match srcrs with
      [ nil ⇒ None ?
      | cons srcr tl ⇒
        Some ? (add_graph start_lbl (rtl_st_move destr srcr dest_lbl) def)
      ]
    ]
  | op_not_bool ⇒
    let destr ≝ extract_singleton ? destrs in
    let srcrs ≝ extract_singleton ? srcrs in
    match destr with
    [ None ⇒ None ?
    | Some destr ⇒
      match srcrs with
      [ None ⇒ None ?
      | Some srcr ⇒
        let 〈def, tmpr〉 ≝ fresh_reg def in
        adds_graph [
          rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl;
          rtl_st_clear_carry start_lbl;
          rtl_st_op2 Sub destr tmpr srcr start_lbl;
          rtl_st_int destr (bitvector_of_nat ? 0) dest_lbl;
          rtl_st_op2 Addc destr destr destr start_lbl;
          rtl_st_int tmpr (bitvector_of_nat ? 1) dest_lbl;
          rtl_st_op2 Xor destr destr tmpr start_lbl
        ] start_lbl dest_lbl def
      ]
    ]
  | _ ⇒ None ? (* error float *)
  ].

definition translate_condptr ≝
  λr1.
  λr2.
  λstart_lbl: label.
  λlbl_true: label.
  λlbl_false: label.
  λdef.
  let 〈def, tmpr〉 ≝ fresh_reg def in
    adds_graph [
      rtl_st_op2 Or tmpr r1 r2 start_lbl;
      rtl_st_cond_acc tmpr lbl_true lbl_false
    ] start_lbl start_lbl def.

(*
let rec translate_op2 (op2: ?) (destrs: ?) (srcrs1: ?) (srcrs2: ?)
                      (start_lbl: label) (dest_lbl: label) (def: ?) on op2 ≝
  match op2 with
  [ op_add ⇒
    let destr ≝ extract_singleton ? destrs in
    let srcr1 ≝ extract_singleton ? srcrs1 in
    let srcr2 ≝ extract_singleton ? srcrs2 in
    match destr with
    [ None ⇒ None ?
    | Some destr ⇒
      match srcr1 with
      [ None ⇒ None ?
      | Some srcr1 ⇒
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          adds_graph [
            rtl_st_op2 Add destr srcr1 srcr2 start_lbl
          ] start_lbl dest_lbl def
        ]
      ]
    ]
  | op_sub ⇒
    let destr ≝ extract_singleton ? destrs in
    let srcr1 ≝ extract_singleton ? srcrs1 in
    let srcr2 ≝ extract_singleton ? srcrs2 in
    match destr with
    [ None ⇒ None ?
    | Some destr ⇒
      match srcr1 with
      [ None ⇒ None ?
      | Some srcr1 ⇒
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          adds_graph [
            rtl_st_clear_carry start_lbl;
            rtl_st_op2 Sub destr srcr1 srcr2 start_lbl
          ] start_lbl dest_lbl def
        ]
      ]
    ]
  | op_mul ⇒
    let destr ≝ extract_singleton ? destrs in
    let srcr1 ≝ extract_singleton ? srcrs1 in
    let srcr2 ≝ extract_singleton ? srcrs2 in
    match destr with
    [ None ⇒ None ?
    | Some destr ⇒
      match srcr1 with
      [ None ⇒ None ?
      | Some srcr1 ⇒
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          adds_graph [
            rtl_st_opaccs Mul destr srcr1 srcr2 start_lbl
          ] start_lbl dest_lbl def
        ]
      ]
    ]
  | op_div ⇒ None ? (* signed div not supported *)
  | op_divu ⇒
    let destr ≝ extract_singleton ? destrs in
    let srcr1 ≝ extract_singleton ? srcrs1 in
    let srcr2 ≝ extract_singleton ? srcrs2 in
    match destr with
    [ None ⇒ None ?
    | Some destr ⇒
      match srcr1 with
      [ None ⇒ None ?
      | Some srcr1 ⇒
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          adds_graph [
            rtl_st_opaccs Divu destr srcr1 srcr2 start_lbl
          ] start_lbl dest_lbl def
        ]
      ]
    ]
  | op_modu ⇒
    let destr ≝ extract_singleton ? destrs in
    let srcr1 ≝ extract_singleton ? srcrs1 in
    let srcr2 ≝ extract_singleton ? srcrs2 in
    match destr with
    [ None ⇒ None ?
    | Some destr ⇒
      match srcr1 with
      [ None ⇒ None ?
      | Some srcr1 ⇒
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          adds_graph [
            rtl_st_opaccs Modu destr srcr1 srcr2 start_lbl
          ] start_lbl dest_lbl def
        ]
      ]
    ]
  | op_mod ⇒ None ? (* signed mod not supported *)
  | op_and ⇒
    let destr ≝ extract_singleton ? destrs in
    let srcr1 ≝ extract_singleton ? srcrs1 in
    let srcr2 ≝ extract_singleton ? srcrs2 in
    match destr with
    [ None ⇒ None ?
    | Some destr ⇒
      match srcr1 with
      [ None ⇒ None ?
      | Some srcr1 ⇒
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          adds_graph [
            rtl_st_op2 And destr srcr1 srcr2 start_lbl
          ] start_lbl dest_lbl def
        ]
      ]
    ]
  | op_or ⇒
    let destr ≝ extract_singleton ? destrs in
    let srcr1 ≝ extract_singleton ? srcrs1 in
    let srcr2 ≝ extract_singleton ? srcrs2 in
    match destr with
    [ None ⇒ None ?
    | Some destr ⇒
      match srcr1 with
      [ None ⇒ None ?
      | Some srcr1 ⇒
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          adds_graph [
            rtl_st_op2 Or destr srcr1 srcr2 start_lbl
          ] start_lbl dest_lbl def
        ]
      ]
    ]
  | op_xor ⇒
    let destr ≝ extract_singleton ? destrs in
    let srcr1 ≝ extract_singleton ? srcrs1 in
    let srcr2 ≝ extract_singleton ? srcrs2 in
    match destr with
    [ None ⇒ None ?
    | Some destr ⇒
      match srcr1 with
      [ None ⇒ None ?
      | Some srcr1 ⇒
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          adds_graph [
            rtl_st_op2 Xor destr srcr1 srcr2 start_lbl
          ] start_lbl dest_lbl def
        ]
      ]
    ]
  | op_shru ⇒ None ? (* shifts not supported *)
  | op_shr ⇒ None ?
  | op_shl ⇒ None ?
  | op_addf ⇒ None ? (* floats not supported *)
  | op_subf ⇒ None ?
  | op_mulf ⇒ None ?
  | op_divf ⇒ None ?
  | op_cmpf _ ⇒ None ?
  | op_addp ⇒
    let destr12 ≝ extract_pair ? destrs in
    match destr12 with
    [ None         ⇒ None ?
    | Some destr12 ⇒
      let 〈destr1, destr2〉 ≝ destr12 in
      let srcr12 ≝ extract_pair ? srcrs1 in
      match srcr12 with
      [ None ⇒
        let srcr2 ≝ extract_singleton ? srcrs1 in
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          let srcr12 ≝ extract_pair ? srcrs2 in
          match srcr12 with
          [ None ⇒ None ?
          | Some srcr12 ⇒
            let 〈srcr11, srcr12〉 ≝ srcr12 in
            let 〈def, tmpr1〉 ≝ fresh_reg def in
            let 〈def, tmpr2〉 ≝ fresh_reg def in
              adds_graph [
                rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
                rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
                rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
                rtl_st_move destr1 tmpr1 start_lbl
              ] start_lbl dest_lbl def
          ]
        ]
      | Some srcr12 ⇒
        let 〈srcr11, srcr12〉 ≝ srcr12 in
        let srcr2 ≝ extract_singleton ? srcrs2 in
        match srcr2 with
        [ None       ⇒ None ?
        | Some srcr2 ⇒
          let 〈def, tmpr1〉 ≝ fresh_reg def in
          let 〈def, tmpr2〉 ≝ fresh_reg def in
            adds_graph [
              rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
              rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
              rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
              rtl_st_move destr1 tmpr1 start_lbl
            ] start_lbl dest_lbl def
        ]
      ]
    ]
  | op_subp ⇒
    let destr ≝ extract_singleton ? destrs in
    match destr with
    [ None ⇒
      let destr12 ≝ extract_pair ? destrs in
      match destr12 with
      [ None ⇒ None ?
      | Some destr12 ⇒
        let 〈destr1, destr2〉 ≝ destr12 in
        let srcr12 ≝ extract_pair ? srcrs1 in
        match srcr12 with
        [ None ⇒ None ?
        | Some srcr12 ⇒
          let 〈srcr11, srcr12〉 ≝ srcr12 in
          let srcr2 ≝ extract_singleton ? srcrs2 in
          match srcr2 with
          [ None ⇒ None ?
          | Some srcr2 ⇒
            adds_graph [
              rtl_st_clear_carry start_lbl;
              rtl_st_op2 Sub destr1 srcr11 srcr2 start_lbl;
              rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl;
              rtl_st_op2 Sub destr2 srcr12 destr2 start_lbl
            ] start_lbl dest_lbl def
          ]
        ] 
      ]
    | Some destr ⇒
      match srcrs1 with
      [ nil ⇒ None ?
      | cons srcr1 tl ⇒
        match srcrs2 with
        [ nil ⇒ None ?
        | cons srcr2 tl' ⇒
          let 〈def, tmpr1〉 ≝ fresh_reg def in
          let 〈def, tmpr2〉 ≝ fresh_reg def in
            adds_graph [
              rtl_st_op1 Cmpl tmpr1 srcr2 start_lbl;
              rtl_st_int tmpr2 (bitvector_of_nat ? 1) start_lbl;
              rtl_st_op2 Add tmpr1 tmpr1 tmpr2 start_lbl;
              rtl_st_op2 Add destr srcr1 tmpr1 start_lbl
            ] start_lbl dest_lbl def
        ]
      ]
    ]
  | op_cmp cmp ⇒
    match cmp with
    [ Compare_Equal ⇒
      add_translates [
        translate_op2 op_sub destrs srcrs1 srcrs2;
        translate_op1 op_not_bool destrs destrs
      ] start_lbl dest_lbl def
    | Compare_NotEqual ⇒
      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
    | _ ⇒ None ?
    ]
  | op_cmpu cmp ⇒
    match cmp with
    [ Compare_Equal ⇒
      add_translates [
        translate_op2 op_sub destrs srcrs1 srcrs2;
        translate_op1 op_not_bool destrs destrs
      ] start_lbl dest_lbl def
    | Compare_NotEqual ⇒
      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
    | Compare
    | _ ⇒ None ?
    ]
  | _ ⇒ ?
  ].

    | AST.Op_cmpu AST.Cmp_lt, [destr], [srcr1], [srcr2] ->
      let (def, tmpr) = fresh_reg def in
      adds_graph
	[RTL.St_clear_carry start_lbl ;
	 RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) ;
	 RTL.St_int (destr, 0, start_lbl) ;
	 RTL.St_op2 (I8051.Addc, destr, destr, destr, start_lbl)]
	start_lbl dest_lbl def

    | AST.Op_cmpu AST.Cmp_gt, _, _, _ ->
      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
	destrs srcrs2 srcrs1 start_lbl dest_lbl def

    | AST.Op_cmpu AST.Cmp_le, _, _, _ ->
      add_translates
	[translate_op2 (AST.Op_cmpu AST.Cmp_gt) destrs srcrs1 srcrs2 ;
	 translate_op1 AST.Op_notbool destrs destrs]
	start_lbl dest_lbl def

    | AST.Op_cmpu AST.Cmp_ge, _, _, _ ->
      add_translates
	[translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
	 translate_op1 AST.Op_notbool destrs destrs]
	start_lbl dest_lbl def

    | AST.Op_cmp cmp, _, _, _ ->
      let (def, tmprs1) = fresh_regs def (List.length srcrs1) in
      let (def, tmprs2) = fresh_regs def (List.length srcrs2) in
      add_translates
        [translate_cst (AST.Cst_int 128) tmprs1 ;
	 translate_cst (AST.Cst_int 128) tmprs2 ;
	 translate_op2 AST.Op_add tmprs1 srcrs1 tmprs1 ;
	 translate_op2 AST.Op_add tmprs2 srcrs2 tmprs2 ;
	 translate_op2 (AST.Op_cmpu cmp) destrs tmprs1 tmprs2] 
	start_lbl dest_lbl def

    | AST.Op_cmpp AST.Cmp_eq, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
      let (def, tmpr) = fresh_reg def in
      add_translates
	[translate_op2 (AST.Op_cmpu AST.Cmp_ne) [tmpr] [srcr11] [srcr21] ;
	 translate_op2 (AST.Op_cmpu AST.Cmp_ne) [destr] [srcr21] [srcr22] ;
	 translate_op2 AST.Op_or [destr] [destr] [tmpr] ;
	 adds_graph [RTL.St_int (tmpr, 1, start_lbl)] ;
	 translate_op2 AST.Op_xor [destr] [destr] [tmpr]]
	start_lbl dest_lbl def

    | AST.Op_cmpp AST.Cmp_lt, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
      let (def, tmpr1) = fresh_reg def in
      let (def, tmpr2) = fresh_reg def in
      add_translates
	[translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr12] [srcr22] ;
	 translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr12] [srcr22] ;
	 translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr11] [srcr21] ;
	 translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ;
	 translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]]
	start_lbl dest_lbl def

    | AST.Op_cmpp AST.Cmp_gt, _, _, _ ->
      translate_op2 (AST.Op_cmpp AST.Cmp_lt)
	destrs srcrs2 srcrs1 start_lbl dest_lbl def

    | AST.Op_cmpp AST.Cmp_le, _, _, _ ->
      add_translates
	[translate_op2 (AST.Op_cmpp AST.Cmp_gt) destrs srcrs1 srcrs2 ;
	 translate_op1 AST.Op_notbool destrs destrs]
	start_lbl dest_lbl def

    | AST.Op_cmpp AST.Cmp_ge, _, _, _ ->
      add_translates
	[translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
	 translate_op1 AST.Op_notbool destrs destrs]
	start_lbl dest_lbl def

    | _ -> assert false (* wrong number of arguments *)
*)

definition translate_condcst ≝
  λcst.
  λstart_lbl: label.
  λlbl_true: label.
  λlbl_false: label.
  λdef.
  match cst with
  [ cast_int i ⇒
    let 〈def, tmpr〉 ≝ fresh_reg def in
    adds_graph [
      rtl_st_int tmpr i start_lbl;
      rtl_st_cond_acc tmpr lbl_true lbl_false
    ] start_lbl start_lbl def
  | cast_addr_symbol x ⇒
    let 〈def, r1〉 ≝ fresh_reg def in
    let 〈def, r2〉 ≝ fresh_reg def in
    let lbl ≝ fresh_label def in
    match lbl with
    [ None ⇒ None ?
    | Some lbl ⇒
      let def ≝ add_graph start_lbl (rtl_st_addr r1 r2 x lbl) def in
        translate_condptr r1 r2 lbl lbl_true lbl_false def
    ]
  | cast_stack_offset off ⇒
    let 〈def, r1〉 ≝ fresh_reg def in
    let 〈def, r2〉 ≝ fresh_reg def in
    let tmp_lbl ≝ fresh_label def in
    match tmp_lbl with
    [ None ⇒ None ?
    | Some tmp_lbl ⇒
      let def ≝ translate_cst (cast_stack_offset off) [r1; r2] start_lbl tmp_lbl def in
      match def with
      [ None ⇒ None ?
      | Some def ⇒ translate_condptr r1 r2 tmp_lbl lbl_true lbl_false def
      ]
    ]
  | cast_float f ⇒ None ? (* error_float *)
  ].

definition size_of_op1_ret ≝
  λop.
  match op with
  [ op_cast8_unsigned ⇒ Some ? 1
  | op_cast8_signed ⇒ Some ? 1
  | op_cast16_unsigned ⇒ Some ? 1
  | op_cast16_signed ⇒ Some ? 1
  | op_neg_int ⇒ Some ? 1
  | op_not_int ⇒ Some ? 1
  | op_int_of_ptr ⇒ Some ? 1
  | op_ptr_of_int ⇒ Some ? 2
  | op_id ⇒ None ? (* invalid_argument *)
  | _ ⇒ None ? (* error_float *)
  ].

definition translate_cond1 ≝
  λop1.
  λsrcrs: list register.
  λstart_lbl: label.
  λlbl_true: label.
  λlbl_false: label.
  λdef.
  match op1 with
  [ op_id ⇒
    let srcr ≝ extract_singleton ? srcrs in
    match srcr with
    [ None ⇒
      let srcr12 ≝ extract_pair ? srcrs in
      match srcr12 with
      [ None ⇒ None ?
      | Some srcr12 ⇒
        let 〈srcr1, srcr2〉 ≝ srcr12 in
          translate_condptr srcr1 srcr2 start_lbl lbl_true lbl_false def
      ]
    | Some srcr ⇒
      adds_graph [
        rtl_st_cond_acc srcr lbl_true lbl_false
      ] start_lbl start_lbl def
    ]
  | _     ⇒
    let size ≝ size_of_op1_ret op1 in
    match size with
    [ None ⇒ None ?
    | Some size ⇒
      let 〈def, destrs〉 ≝ fresh_regs def size in
      let lbl ≝ fresh_label def in
      match lbl with
      [ None ⇒ None ?
      | Some lbl ⇒
        let def ≝ translate_op1 op1 destrs srcrs start_lbl lbl def in
        match def with
        [ None ⇒ None ?
        | Some def ⇒
          let destr ≝ extract_singleton ? destrs in
          match destr with
          [ None ⇒
            let destr12 ≝ extract_pair ? destrs in
            match destr12 with
            [ None ⇒ None ?
            | Some destr12 ⇒
              let 〈destr1, destr2〉 ≝ destr12 in
                translate_condptr destr1 destr2 start_lbl lbl_true lbl_false def
            ]
          | Some destr ⇒
            adds_graph [
              rtl_st_cond_acc destr lbl_true lbl_false
            ] start_lbl start_lbl def
          ]
        ]
      ]
    ]
  ].

definition size_of_op2_ret ≝
  λn: nat.
  λop2.
  match op2 with
  [ op_add ⇒ Some ? 1
  | op_sub ⇒ Some ? 1
  | op_mul ⇒ Some ? 1
  | op_div ⇒ Some ? 1
  | op_divu ⇒ Some ? 1
  | op_mod ⇒ Some ? 1
  | op_modu ⇒ Some ? 1
  | op_and ⇒ Some ? 1
  | op_or ⇒ Some ? 1
  | op_xor ⇒ Some ? 1
  | op_shl ⇒ Some ? 1
  | op_shr ⇒ Some ? 1
  | op_shru ⇒ Some ? 1
  | op_cmp _ ⇒ Some ? 1
  | op_cmpu _ ⇒ Some ? 1
  | op_cmpp _ ⇒ Some ? 1
  | op_addp ⇒ Some ? 2
  | op_subp ⇒
    if eq_nat n 4 then
      Some ? 1
    else
      Some ? 2
  | _ ⇒ None ? (* error_float *)
  ].

definition translate_cond2 ≝
  λop2.
  λsrcrs1: list register.
  λsrcrs2: list register.
  λstart_lbl: label.
  λlbl_true: label.
  λlbl_false: label.
  λdef.
  match op2 with
  [
  ]

let translate_cond2 op2 srcrs1 srcrs2 start_lbl lbl_true lbl_false def =
  match op2, srcrs1, srcrs2 with

    | AST.Op_cmp AST.Cmp_eq, [srcr1], [srcr2] ->
      let (def, tmpr) = fresh_reg def in
      adds_graph
	[RTL.St_clear_carry start_lbl ;
	 RTL.St_op2 (I8051.Sub, tmpr, srcr1, srcr2, start_lbl) ;
	 RTL.St_condacc (tmpr, lbl_false, lbl_true)]
	start_lbl start_lbl def

    | _, _, _ ->
      let n = (List.length srcrs1) + (List.length srcrs2) in
      let (def, destrs) = fresh_regs def (size_of_op2_ret n op2) in
      let lbl = fresh_label def in
      let def = translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def in
      translate_cond1 AST.Op_id destrs lbl lbl_true lbl_false def