Changeset 2286 for src/LIN/LINToASM.ma


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (8 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r1995 r2286  
    22include "utilities/BitVectorTrieSet.ma".
    33include "LIN/LIN.ma".
     4include "ASM/ASM.ma".
     5
     6definition register_address: Register → [[ acc_a; direct; registr ]] ≝
     7  λr: Register.
     8    match r with
     9    [ Register00 ⇒ REGISTER [[ false; false; false ]]
     10    | Register01 ⇒ REGISTER [[ false; false; true ]]
     11    | Register02 ⇒ REGISTER [[ false; true; false ]]
     12    | Register03 ⇒ REGISTER [[ false; true; true ]]
     13    | Register04 ⇒ REGISTER [[ true; false; false ]]
     14    | Register05 ⇒ REGISTER [[ true; false; true ]]
     15    | Register06 ⇒ REGISTER [[ true; true; false ]]
     16    | Register07 ⇒ REGISTER [[ true; true; true ]]
     17    | RegisterA ⇒ ACC_A
     18    | RegisterB ⇒ DIRECT (bitvector_of_nat 8 240)
     19    | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82)
     20    | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83)
     21    | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r))
     22    ]. @I qed.
     23
     24(* TODO:
     25  this should translate back end immediates (which rely on beval) to ASM
     26  byte immediates. How should it work? surely needs arguments for instantiation
     27  of blocks. If it's too much a fuss, we can go back to byte immediates in the
     28  back end. *)
     29definition asm_byte_of_beval : beval → Byte ≝
     30  λb.match b with
     31    [ BVByte b ⇒ b
     32    | BVundef ⇒ (* any will do *) zero_byte
     33    | BVnonzero ⇒ (* any will do *) maximum 7 @@ [[ true ]]
     34    | BVnull _ ⇒ zero_byte (* is it correct? *)
     35    | BVptr b p o ⇒ ?
     36    ].
     37  cases daemon qed.
     38
     39definition arg_address : hdw_argument → [[ acc_a ; direct ; registr ; data ]] ≝
     40  λa.match a with
     41  [ Reg r ⇒ register_address r
     42  | Imm bv ⇒ DATA (asm_byte_of_beval bv)
     43  ].
     44  cases a #x [2: normalize //] normalize nodelta
     45  elim (register_address ?) #rslt @is_in_subvector_is_in_supervector @I
     46qed.
    447
    548let rec association (i: ident) (l: list (ident × nat))
     
    2568qed.
    2669
     70definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).
     71 
    2772definition statement_labels ≝
    2873  λg: list ident.
     
    3378    [ sequential instr' _ ⇒
    3479      match instr' with
    35       [ COST_LABEL lbl ⇒ { (toASM_ident ? lbl) }
     80      [ step_seq instr'' ⇒
     81        match instr'' with
     82        [ COST_LABEL lbl ⇒ { (toASM_ident ? lbl) }
     83        | _ ⇒ ∅
     84        ]
    3685      | COND acc_a_reg lbl ⇒ { (toASM_ident ? lbl) }
     86      ]
     87    | final instr' ⇒
     88      match instr' with
     89      [ GOTO lbl ⇒ {(toASM_ident ? lbl)}
    3790      | _ ⇒ ∅
    3891      ]
    39     | RETURN ⇒ ∅
    40     | GOTO lbl ⇒ {(toASM_ident ? lbl)} ]
     92    ]
    4193  in
    4294  match label with
     
    55107  λA: Type[0].
    56108  λglobals: list ident.
    57   λf: A × (lin_function globals).
     109  λf: A × (joint_function LIN globals).
    58110  let 〈ignore, fun_def〉 ≝ f in
    59111  match fun_def return λ_. identifier_set ? with
     
    67119  λglobals: list ident.
    68120  λlabels: identifier_set ?.
    69   λfunct: A × (lin_function globals).
     121  λfunct: A × (joint_function LIN globals).
    70122    labels ∪ (function_labels ? globals funct).
    71123
     
    80132definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
    81133
     134(* TODO: check and change to free bit *)
     135definition asm_other_bit ≝ BIT_ADDR (zero_byte).
     136
    82137definition translate_statements ≝
    83138  λglobals: list (ident × nat).
    84139  λglobals_old: list ident.
    85140  λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals).
    86   λstatement: pre_lin_statement globals_old.
     141  λstatement: joint_statement LIN globals_old.
    87142  match statement with
    88   [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl)
    89   | RETURN ⇒ Instruction (RET ?)
     143  [ final instr ⇒
     144    match instr with
     145    [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl)
     146    | RETURN ⇒ Instruction (RET ?)
     147    | tailcall abs ⇒ match abs in void with [ ]
     148    ]
    90149  | sequential instr _ ⇒
    91150      match instr with
    92       [ extension ext ⇒ ⊥
    93       | COMMENT comment ⇒ Comment comment
    94       | COST_LABEL lbl ⇒ Cost lbl
    95       | POP _ ⇒ Instruction (POP ? accumulator_address)
    96       | PUSH _ ⇒ Instruction (PUSH ? accumulator_address)
    97       | CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)
    98       | CALL_ID f _ _ ⇒ Call (toASM_ident ? f)
    99       | OPACCS accs _ _ _ _ ⇒
    100         match accs with
    101         [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
    102         | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
    103         ]
    104       | OP1 op1 _ _ ⇒
    105         match op1 with
    106         [ Cmpl ⇒ Instruction (CPL ? ACC_A)
    107         | Inc ⇒ Instruction (INC ? ACC_A)
    108         | Rl ⇒ Instruction (RL ? ACC_A)
    109         ]
    110       | OP2 op2 _ _ reg ⇒
    111         match op2 with
    112         [ Add ⇒
    113           let reg' ≝ register_address reg in
    114           match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    115                                                          direct;
    116                                                          registr ]] x) → ? with
    117           [ ACC_A ⇒ λacc_a: True.
    118             Instruction (ADD ? ACC_A accumulator_address)
    119           | DIRECT d ⇒ λdirect1: True.
    120             Instruction (ADD ? ACC_A (DIRECT d))
    121           | REGISTER r ⇒ λregister1: True.
    122             Instruction (ADD ? ACC_A (REGISTER r))
    123           | _ ⇒ λother: False. ⊥
    124           ] (subaddressing_modein … reg')
    125         | Addc ⇒
    126           let reg' ≝ register_address reg in
    127           match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    128                                                          direct;
    129                                                          registr ]] x) → ? with
    130           [ ACC_A ⇒ λacc_a: True.
    131             Instruction (ADDC ? ACC_A accumulator_address)
    132           | DIRECT d ⇒ λdirect2: True.
    133             Instruction (ADDC ? ACC_A (DIRECT d))
    134           | REGISTER r ⇒ λregister2: True.
    135             Instruction (ADDC ? ACC_A (REGISTER r))
    136           | _ ⇒ λother: False. ⊥
    137           ] (subaddressing_modein … reg')
    138         | Sub ⇒
    139           let reg' ≝ register_address reg in
    140           match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    141                                                          direct;
    142                                                          registr ]] x) → ? with
    143           [ ACC_A ⇒ λacc_a: True.
    144             Instruction (SUBB ? ACC_A accumulator_address)
    145           | DIRECT d ⇒ λdirect3: True.
    146             Instruction (SUBB ? ACC_A (DIRECT d))
    147           | REGISTER r ⇒ λregister3: True.
    148             Instruction (SUBB ? ACC_A (REGISTER r))
    149           | _ ⇒ λother: False. ⊥
    150           ] (subaddressing_modein … reg')
    151         | And ⇒
    152           let reg' ≝ register_address reg in
    153           match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    154                                                          direct;
    155                                                          registr ]] x) → ? with
    156           [ ACC_A ⇒ λacc_a: True.
    157             Instruction (NOP ?)
    158           | DIRECT d ⇒ λdirect4: True.
    159             Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
    160           | REGISTER r ⇒ λregister4: True.
    161             Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
    162           | _ ⇒ λother: False. ⊥
    163           ] (subaddressing_modein … reg')
    164         | Or ⇒
    165           let reg' ≝ register_address reg in
    166           match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    167                                                          direct;
    168                                                          registr ]] x) → ? with
    169           [ ACC_A ⇒ λacc_a: True.
    170             Instruction (NOP ?)
    171           | DIRECT d ⇒ λdirect5: True.
    172             Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
    173           | REGISTER r ⇒ λregister5: True.
    174             Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
    175           | _ ⇒ λother: False. ⊥
    176           ] (subaddressing_modein … reg')
    177         | Xor ⇒
    178           let reg' ≝ register_address reg in
    179           match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    180                                                          direct;
    181                                                          registr ]] x) → ? with
    182           [ ACC_A ⇒ λacc_a: True.
    183             Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
    184           | DIRECT d ⇒ λdirect6: True.
    185             Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
    186           | REGISTER r ⇒ λregister6: True.
    187             Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
    188           | _ ⇒ λother: False. ⊥
    189           ] (subaddressing_modein … reg')
    190         ]
    191       | INT reg byte ⇒
    192         let reg' ≝ register_address reg in
    193           match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    194                                                          direct;
    195                                                          registr ]] x) → ? with
    196           [ REGISTER r ⇒ λregister7: True.
    197             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉))))))
    198           | ACC_A ⇒ λacc: True.
    199             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉))))))
    200           | DIRECT d ⇒ λdirect7: True.
    201             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉)))))
    202           | _ ⇒ λother: False. ⊥
    203           ] (subaddressing_modein … reg')
    204       | MOVE regs ⇒
    205          match regs with
    206           [ from_acc reg ⇒
     151      [ step_seq instr' ⇒
     152        match instr' with
     153        [ extension_seq ext ⇒
     154          match ext with
     155          [ SAVE_CARRY ⇒
     156            Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉))
     157          | RESTORE_CARRY ⇒
     158            Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉)))
     159          ]
     160        | COMMENT comment ⇒ Comment comment
     161        | COST_LABEL lbl ⇒ Cost lbl
     162        | POP _ ⇒ Instruction (POP ? accumulator_address)
     163        | PUSH _ ⇒ Instruction (PUSH ? accumulator_address)
     164        | CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)
     165        | CALL_ID f _ _ ⇒ Call (toASM_ident ? f)
     166        | extension_call abs ⇒ match abs in void with [ ]
     167        | OPACCS accs _ _ _ _ ⇒
     168          match accs with
     169          [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
     170          | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
     171          ]
     172        | OP1 op1 _ _ ⇒
     173          match op1 with
     174          [ Cmpl ⇒ Instruction (CPL ? ACC_A)
     175          | Inc ⇒ Instruction (INC ? ACC_A)
     176          | Rl ⇒ Instruction (RL ? ACC_A)
     177          ]
     178        | OP2 op2 _ _ reg ⇒
     179          match op2 with
     180          [ Add ⇒
     181            let reg' ≝ arg_address reg in
     182            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     183                                                           direct;
     184                                                           registr;
     185                                                           data ]] x) → ? with
     186            [ ACC_A ⇒ λacc_a: True.
     187              Instruction (ADD ? ACC_A accumulator_address)
     188            | DIRECT d ⇒ λdirect1: True.
     189              Instruction (ADD ? ACC_A (DIRECT d))
     190            | REGISTER r ⇒ λregister1: True.
     191              Instruction (ADD ? ACC_A (REGISTER r))
     192            | DATA b ⇒ λdata : True.
     193              Instruction (ADD ? ACC_A (DATA b))
     194            | _ ⇒ Ⓧ
     195            ] (subaddressing_modein … reg')
     196          | Addc ⇒
     197            let reg' ≝ arg_address reg in
     198            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     199                                                           direct;
     200                                                           registr;
     201                                                           data ]] x) → ? with
     202            [ ACC_A ⇒ λacc_a: True.
     203              Instruction (ADDC ? ACC_A accumulator_address)
     204            | DIRECT d ⇒ λdirect2: True.
     205              Instruction (ADDC ? ACC_A (DIRECT d))
     206            | REGISTER r ⇒ λregister2: True.
     207              Instruction (ADDC ? ACC_A (REGISTER r))
     208            | DATA b ⇒ λdata : True.
     209              Instruction (ADDC ? ACC_A (DATA b))
     210            | _ ⇒ Ⓧ
     211            ] (subaddressing_modein … reg')
     212          | Sub ⇒
     213            let reg' ≝ arg_address reg in
     214            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     215                                                           direct;
     216                                                           registr;
     217                                                           data ]] x) → ? with
     218            [ ACC_A ⇒ λacc_a: True.
     219              Instruction (SUBB ? ACC_A accumulator_address)
     220            | DIRECT d ⇒ λdirect3: True.
     221              Instruction (SUBB ? ACC_A (DIRECT d))
     222            | REGISTER r ⇒ λregister3: True.
     223              Instruction (SUBB ? ACC_A (REGISTER r))
     224            | DATA b ⇒ λdata : True.
     225              Instruction (SUBB ? ACC_A (DATA b))
     226            | _ ⇒ Ⓧ
     227            ] (subaddressing_modein … reg')
     228          | And ⇒
     229            let reg' ≝ arg_address reg in
     230            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     231                                                           direct;
     232                                                           registr;
     233                                                           data ]] x) → ? with
     234            [ ACC_A ⇒ λacc_a: True.
     235              Instruction (NOP ?)
     236            | DIRECT d ⇒ λdirect4: True.
     237              Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
     238            | REGISTER r ⇒ λregister4: True.
     239              Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
     240            | DATA b ⇒ λdata : True.
     241              Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
     242            | _ ⇒ Ⓧ
     243            ] (subaddressing_modein … reg')
     244          | Or ⇒
     245            let reg' ≝ arg_address reg in
     246            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     247                                                           direct;
     248                                                           registr ; data ]] x) → ? with
     249            [ ACC_A ⇒ λacc_a: True.
     250              Instruction (NOP ?)
     251            | DIRECT d ⇒ λdirect5: True.
     252              Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
     253            | REGISTER r ⇒ λregister5: True.
     254              Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
     255            | DATA b ⇒ λdata : True.
     256              Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
     257            | _ ⇒ Ⓧ
     258            ] (subaddressing_modein … reg')
     259          | Xor ⇒
     260            let reg' ≝ arg_address reg in
     261            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     262                                                           direct;
     263                                                           registr ; data ]] x) → ? with
     264            [ ACC_A ⇒ λacc_a: True.
     265              Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
     266            | DIRECT d ⇒ λdirect6: True.
     267              Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
     268            | REGISTER r ⇒ λregister6: True.
     269              Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
     270            | DATA b ⇒ λdata : True.
     271              Instruction (XRL ? (inl ? ? 〈ACC_A, DATA b〉))
     272            | _ ⇒ Ⓧ
     273            ] (subaddressing_modein … reg')
     274          ]
     275        | LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
     276        | STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
     277        | ADDRESS addr proof _ _ ⇒
     278          let look ≝ association addr globals (prf ? proof) in
     279            Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
     280        | SET_CARRY ⇒
     281          Instruction (SETB ? CARRY)
     282        | MOVE regs ⇒
     283          match regs with
     284          [ to_acc _ reg ⇒
     285             let reg' ≝ register_address reg in
     286               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     287                                                              direct;
     288                                                              registr ]] x) → ? with
     289               [ REGISTER r ⇒ λregister9: True.
     290                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
     291               | DIRECT d ⇒ λdirect9: True.
     292                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
     293               | ACC_A ⇒ λacc_a: True.
     294                 Instruction (NOP ?)
     295               | _ ⇒ λother: False. ⊥
     296               ] (subaddressing_modein … reg')
     297          | from_acc reg _ ⇒
    207298             let reg' ≝ register_address reg in
    208299               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     
    217308               | _ ⇒ λother: False. ⊥
    218309               ] (subaddressing_modein … reg')
    219           | to_acc reg ⇒
    220              let reg' ≝ register_address reg in
    221                match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    222                                                               direct;
    223                                                               registr ]] x) → ? with
    224                [ REGISTER r ⇒ λregister9: True.
    225                  Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
    226                | DIRECT d ⇒ λdirect9: True.
    227                  Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
    228                | ACC_A ⇒ λacc_a: True.
    229                  Instruction (NOP ?)
    230                | _ ⇒ λother: False. ⊥
    231                ] (subaddressing_modein … reg')]
    232       | LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
    233       | STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    234       | ADDRESS addr proof _ _ ⇒
    235         let look ≝ association addr globals (prf ? proof) in
    236           Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
     310          | int_to_reg reg bv ⇒
     311            let b ≝ asm_byte_of_beval bv in
     312            let reg' ≝ register_address reg in
     313              match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     314                                                             direct;
     315                                                             registr ]] x) → ? with
     316              [ REGISTER r ⇒ λregister7: True.
     317                Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, DATA b〉))))))
     318              | ACC_A ⇒ λacc: True.
     319                Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
     320              | DIRECT d ⇒ λdirect7: True.
     321                Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, DATA b〉)))))
     322              | _ ⇒ λother: False. ⊥
     323              ] (subaddressing_modein … reg')
     324          | int_to_acc _ bv ⇒
     325            let b ≝ asm_byte_of_beval bv in
     326            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
     327          ]
     328        ]
    237329      | COND _ lbl ⇒
    238330        (* dpm: this should be handled in translate_code! *)
    239331        Instruction (JNZ ? (toASM_ident ? lbl))
    240       | SET_CARRY ⇒
    241         Instruction (SETB ? CARRY)
    242332      ]
    243333    ].
     
    272362    match def with
    273363    [ Internal int ⇒
    274       let code ≝ joint_if_code … (lin_params globals_old) int in
     364      let code ≝ joint_if_code LIN globals_old int in
    275365      match translate_code globals globals_old prf code with
    276366      [ nil ⇒ ⊥
     
    293383let rec flatten_fun_defs
    294384  (globals: list (ident × nat)) (globals_old: list ident) (prf: ?) (initial_pc: nat)
    295     (the_list: list ((identifier SymbolTag) × (fundef (joint_internal_function globals_old (lin_params globals_old)))))
     385    (the_list: list ((identifier SymbolTag) × (fundef (joint_internal_function LIN globals_old))))
    296386      on the_list: ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) ≝
    297387  match the_list return λx. ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) with
Note: See TracChangeset for help on using the changeset viewer.