Changeset 757 for src


Ignore:
Timestamp:
Apr 18, 2011, 12:30:53 PM (10 years ago)
Author:
mulligan
Message:

Lots more fixing to get both front and backends using same conventions and types.

Location:
src
Files:
15 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/ASM.ma

    r722 r757  
    2222| ADDR16: Word → addressing_mode.
    2323
     24(* dpm: renamed register to registr to avoid clash with brian's types *)
    2425inductive addressing_mode_tag : Type[0] ≝
    2526  direct: addressing_mode_tag
    2627| indirect: addressing_mode_tag
    2728| ext_indirect: addressing_mode_tag
    28 | register: addressing_mode_tag
     29| registr: addressing_mode_tag
    2930| acc_a: addressing_mode_tag
    3031| acc_b: addressing_mode_tag
    … …  
    4950      | indirect ⇒ match b with [ indirect ⇒ true | _ ⇒ false ]
    5051      | ext_indirect ⇒ match b with [ ext_indirect ⇒ true | _ ⇒ false ]
    51       | register ⇒ match b with [ register ⇒ true | _ ⇒ false ]
     52      | registr ⇒ match b with [ registr ⇒ true | _ ⇒ false ]
    5253      | acc_a ⇒ match b with [ acc_a ⇒ true | _ ⇒ false ]
    5354      | acc_b ⇒ match b with [ acc_b ⇒ true | _ ⇒ false ]
    … …  
    7374   | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ]
    7475   | ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true | _ ⇒ false ]
    75    | register ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ]
     76   | registr ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ]
    7677   | acc_a ⇒ match A with [ ACC_A ⇒ true | _ ⇒ false ]
    7778   | acc_b ⇒ match A with [ ACC_B ⇒ true | _ ⇒ false ]
    … …  
    120121| JNZ: A → jump A
    121122| CJNE:
    122    [[acc_a]] × [[direct; data]] ⊎ [[register; indirect]] × [[data]] → A → jump A
    123 | DJNZ: [[register ; direct]] → A → jump A.
     123   [[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → jump A
     124| DJNZ: [[registr ; direct]] → A → jump A.
    124125
    125126inductive preinstruction (A: Type[0]) : Type[0] ≝
    126   ADD: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
    127 | ADDC: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
    128 | SUBB: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
    129 | INC: [[ acc_a ; register ; direct ; indirect ; dptr ]] → preinstruction A
    130 | DEC: [[ acc_a ; register ; direct ; indirect ]] → preinstruction A
     127  ADD: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
     128| ADDC: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
     129| SUBB: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
     130| INC: [[ acc_a ; registr ; direct ; indirect ; dptr ]] → preinstruction A
     131| DEC: [[ acc_a ; registr ; direct ; indirect ]] → preinstruction A
    131132| MUL: [[acc_a]] → [[acc_b]] → preinstruction A
    132133| DIV: [[acc_a]] → [[acc_b]] → preinstruction A
    … …  
    135136 (* logical operations *)
    136137| ANL:
    137    [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎
     138   [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
    138139   [[direct]] × [[ acc_a ; data ]] ⊎
    139140   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
    140141| ORL:
    141    [[acc_a]] × [[ register ; data ; direct ; indirect ]] ⊎
     142   [[acc_a]] × [[ registr ; data ; direct ; indirect ]] ⊎
    142143   [[direct]] × [[ acc_a ; data ]] ⊎
    143144   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
    144145| XRL:
    145    [[acc_a]] × [[ data ; register ; direct ; indirect ]] ⊎
     146   [[acc_a]] × [[ data ; registr ; direct ; indirect ]] ⊎
    146147   [[direct]] × [[ acc_a ; data ]] → preinstruction A
    147148| CLR: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
    … …  
    155156 (* data transfer *)
    156157| MOV:
    157     [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎
    158     [[ register ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
    159     [[direct]] × [[ acc_a ; register ; direct ; indirect ; data ]] ⊎
     158    [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
     159    [[ registr ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
     160    [[direct]] × [[ acc_a ; registr ; direct ; indirect ; data ]] ⊎
    160161    [[dptr]] × [[data16]] ⊎
    161162    [[carry]] × [[bit_addr]] ⊎
    … …  
    168169| PUSH: [[direct]] → preinstruction A
    169170| POP: [[direct]] → preinstruction A
    170 | XCH: [[acc_a]] → [[ register ; direct ; indirect ]] → preinstruction A
     171| XCH: [[acc_a]] → [[ registr ; direct ; indirect ]] → preinstruction A
    171172| XCHD: [[acc_a]] → [[indirect]] → preinstruction A
    172173

  • src/ASM/Assembly.ma

    r719 r757  
    1515      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    1616  | ADD addr1 addr2 ⇒
    17      match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
     17     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    1818      [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
    1919      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
    … …  
    2222      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    2323  | ADDC addr1 addr2 ⇒
    24      match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
     24     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    2525      [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ]
    2626      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
    … …  
    3838      [ inl addrs ⇒ match addrs with
    3939         [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    40            match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
     40           match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    4141            [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
    4242            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
    … …  
    8080     [ ([[true; true; false; true; false; true; false; false]]) ]
    8181  | DEC addr ⇒
    82      match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect]] x) → ? with
     82     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect]] x) → ? with
    8383      [ ACC_A ⇒ λ_.
    8484         [ ([[false; false; false; true; false; true; false; false]]) ]
    … …  
    9999           [ RELATIVE b2 ⇒ λ_. b2
    100100           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
    101          match addr1 return λx. bool_to_Prop (is_in ? [[register;direct]] x) → ? with
     101         match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with
    102102          [ REGISTER r ⇒ λ_.
    103103             [ ([[true; true; false; true; true]]) @@ r ; b2 ]
    … …  
    170170               [ DATA b2 ⇒ λ_. b2
    171171               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
    172              match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → list Byte with
     172             match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with
    173173              [ REGISTER r⇒ λ_.
    174174                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
    … …  
    177177              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) ]]
    178178  | INC addr ⇒
    179      match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;dptr]] x) → ? with
     179     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with
    180180      [ ACC_A ⇒ λ_.
    181181         [ ([[false;false;false;false;false;true;false;false]]) ]         
    … …  
    214214                     match addrs with
    215215                      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    216                          match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
     216                         match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    217217                          [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
    218218                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
    … …  
    221221                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    222222                      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    223                          match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → ? with
     223                         match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → ? with
    224224                          [ REGISTER r ⇒ λ_.
    225225                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
    … …  
    240240                       [ DIRECT b1 ⇒ λ_. b1
    241241                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
    242                      match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;data]] x) → ? with
     242                     match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;data]] x) → ? with
    243243                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
    244244                      | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
    … …  
    295295         match addrs with
    296296          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    297              match addr2 return λx. bool_to_Prop (is_in ? [[register;data;direct;indirect]] x) → ? with
     297             match addr2 return λx. bool_to_Prop (is_in ? [[registr;data;direct;indirect]] x) → ? with
    298298             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
    299299             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
    … …  
    354354      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    355355  | SUBB addr1 addr2 ⇒
    356      match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
     356     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    357357      [ REGISTER r ⇒ λ_.
    358358         [ ([[true;false;false;true;true]]) @@ r ]
    … …  
    367367     [ ([[true;true;false;false;false;true;false;false]]) ]
    368368  | XCH addr1 addr2 ⇒
    369      match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect]] x) → ? with
     369     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect]] x) → ? with
    370370      [ REGISTER r ⇒ λ_.
    371371         [ ([[true;true;false;false;true]]) @@ r ]
    … …  
    383383     match addrs with
    384384      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    385          match addr2 return λx. bool_to_Prop (is_in ? [[data;register;direct;indirect]] x) → ? with
     385         match addr2 return λx. bool_to_Prop (is_in ? [[data;registr;direct;indirect]] x) → ? with
    386386          [ REGISTER r ⇒ λ_.
    387387             [ ([[false;true;true;false;true]]) @@ r ]

  • src/ASM/I8051.ma

    r746 r757  
    140140definition RegisterSPH ≝ Register07.
    141141
    142 definition register_address: Register → [[ acc_a; direct; register ]] ≝
     142definition register_address: Register → [[ acc_a; direct; registr ]] ≝
    143143  λr: Register.
    144144    match r with

  • src/ASM/Interpret.ma

    r712 r757  
    156156
    157157include alias "arithmetics/nat.ma".
     158include alias "ASM/BitVectorTrie.ma".
    158159
    159160definition execute_1: Status → Status ≝
    … …  
    172173            let ov_flag ≝ get_index' ? 2 ? flags in
    173174            let s ≝ set_arg_8 s ACC_A result in
    174               set_flags s cy_flag (Some Bit ac_flag) ov_flag   
     175              set_flags s cy_flag (Some Bit ac_flag) ov_flag
    175176        | ADDC addr1 addr2 ⇒
    176177            let old_cy_flag ≝ get_cy_flag s in
    … …  
    240241        | INC addr ⇒
    241242            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
    242                                                            register;
     243                                                           registr;
    243244                                                           direct;
    244245                                                           indirect;
    … …  
    427428            | _ ⇒ λother: False. ⊥
    428429            ] (subaddressing_modein … addr)
    429         | MOVC addr1 addr2 ⇒
    430           match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
    431             [ ACC_DPTR ⇒ λacc_dptr: True.
    432               let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
    433               let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
    434               let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
    435               let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
    436                 set_8051_sfr s SFR_ACC_A result
    437             | ACC_PC ⇒ λacc_pc: True.
    438               let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
    439               let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat 16 1) in
    440               (* DPM: Under specified: does the carry from PC incrementation affect the *)
    441               (*      addition of the PC with the DPTR? At the moment, no.              *)
    442               let s ≝ set_program_counter s inc_pc in
    443               let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
    444               let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
    445                 set_8051_sfr s SFR_ACC_A result
    446             | _ ⇒ λother: False. ⊥
    447             ] (subaddressing_modein … addr2)
    448430        | MOVX addr ⇒
    449431          (* DPM: only copies --- doesn't affect I/O *)
    … …  
    631613                ] (subaddressing_modein … addr2)
    632614            ]
     615        | MOVC addr1 addr2 ⇒
     616          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
     617            [ ACC_DPTR ⇒ λacc_dptr: True.
     618              let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
     619              let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
     620              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
     621              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
     622                set_8051_sfr s SFR_ACC_A result
     623            | ACC_PC ⇒ λacc_pc: True.
     624              let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
     625              let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat 16 1) in
     626              (* DPM: Under specified: does the carry from PC incrementation affect the *)
     627              (*      addition of the PC with the DPTR? At the moment, no.              *)
     628              let s ≝ set_program_counter s inc_pc in
     629              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
     630              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
     631                set_8051_sfr s SFR_ACC_A result
     632            | _ ⇒ λother: False. ⊥
     633            ] (subaddressing_modein … addr2)
    633634        | NOP ⇒ s
    634635        ]

  • src/ASM/Status.ma

    r705 r757  
    755755      ] (subaddressing_modein … a).
    756756     
    757 definition get_arg_8: Status → bool → [[ direct ; indirect ; register ;
     757definition get_arg_8: Status → bool → [[ direct ; indirect ; registr ;
    758758                                          acc_a ; acc_b ; data ; acc_dptr ;
    759759                                          acc_pc ; ext_indirect ;
    760760                                          ext_indirect_dptr ]] → Byte ≝
    761761  λs, l, a.
    762     match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ;
     762    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
    763763                                                acc_a ; acc_b ; data ; acc_dptr ;
    764764                                                acc_pc ; ext_indirect ;
    … …  
    820820qed.
    821821
    822 definition set_arg_8: Status → [[ direct ; indirect ; register ;
     822definition set_arg_8: Status → [[ direct ; indirect ; registr ;
    823823                                   acc_a ; acc_b ; ext_indirect ;
    824824                                   ext_indirect_dptr ]] → Byte → Status ≝
    825825  λs, a, v.
    826     match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ;
     826    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
    827827                                                acc_a ; acc_b ; ext_indirect ;
    828828                                                ext_indirect_dptr ]] x) → ? with

  • src/ERTL/ERTLToLTL.ma

    r753 r757  
    33 
    44axiom translate_ERTL_func:
    5   ∀globals: list Identifier.
    6     list (Identifier × ERTLFunction) → list (Identifier × (LTLFunctionDefinition globals)).
     5  ∀globals: list ident.
     6    list (ident × ertl_function) → list (ident × (ltl_function_definition globals)).
    77 
    8 definition translate: ∀e: ERTLProgram. LTLProgram (ERTL_Pr_Vars e) ≝
     8definition translate: ∀e: ertl_program. ltl_program (ertl_pr_vars e) ≝
    99  λp.
    10     let globals ≝ map ? ? \fst (ERTL_Pr_Vars p) in
    11     let ltl_pr_funcs ≝ map ? ? ? (ERTL_Pr_Funcs p) in
    12       mk_LTLProgram (ERTL_Pr_Vars p) ltl_pr_funcs (ERTL_Pr_Main p).
     10    let globals ≝ map ? ? \fst (ertl_pr_vars p) in
     11    let ltl_pr_funcs ≝ map ? ? ? (ertl_pr_funcs p) in
     12      mk_ltl_program (ertl_pr_vars p) ltl_pr_funcs (ertl_pr_main p).
    1313    # H1
    14     @ (translate_ERTL_func globals) in ⊢ (? × %) (* dpm here *)
     14    @ (translate_ertl_func globals) in ⊢ (? × %) (* dpm here *)

  • src/LIN/JointLTLLIN.ma

    r733 r757  
    11include "ASM/String.ma".
    22include "ASM/I8051.ma".
     3include "common/CostLabel.ma".
    34include "common/AST.ma".
     5include "common/Registers.ma".
    46
    5 inductive JointInstruction (globals: list Identifier): Type[0] ≝
    6   | Joint_Instr_Comment: String → JointInstruction globals
    7   | Joint_Instr_CostLabel: Identifier → JointInstruction globals
    8   | Joint_Instr_Int: Register → Byte → JointInstruction globals
    9   | Joint_Instr_Pop: JointInstruction globals
    10   | Joint_Instr_Push: JointInstruction globals
    11   | Joint_Instr_Address: ∀i: Identifier. (member i (eq_bv ?) globals) → JointInstruction globals
    12   | Joint_Instr_FromAcc: Register → JointInstruction globals
    13   | Joint_Instr_ToAcc: Register → JointInstruction globals
    14   | Joint_Instr_OpAccs: OpAccs → JointInstruction globals
    15   | Joint_Instr_Op1: Op1 → JointInstruction globals
    16   | Joint_Instr_Op2: Op2 → Register → JointInstruction globals
    17   | Joint_Instr_ClearCarry: JointInstruction globals
    18   | Joint_Instr_Load: JointInstruction globals
    19   | Joint_Instr_Store: JointInstruction globals
    20   | Joint_Instr_CallId: Identifier → JointInstruction globals
    21   | Joint_Instr_CondAcc: Identifier → JointInstruction globals.
     7inductive joint_instruction (globals: list ident): Type[0] ≝
     8  | joint_instr_comment: String → joint_instruction globals
     9  | joint_instr_cost_label: costlabel → joint_instruction globals
     10  | joint_instr_int: register → Byte → joint_instruction globals
     11  | joint_instr_pop: joint_instruction globals
     12  | joint_instr_push: joint_instruction globals
     13  | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → joint_instruction globals
     14  | joint_instr_from_acc: register → joint_instruction globals
     15  | joint_instr_to_acc: register → joint_instruction globals
     16  | joint_instr_opaccs: OpAccs → joint_instruction globals
     17  | joint_instr_op1: Op1 → joint_instruction globals
     18  | joint_instr_op2: Op2 → register → joint_instruction globals
     19  | joint_instr_clear_carry: joint_instruction globals
     20  | joint_instr_load: joint_instruction globals
     21  | joint_instr_store: joint_instruction globals
     22  | joint_instr_call_id: ident → joint_instruction globals
     23  | joint_instr_cond_acc: ident → joint_instruction globals.
    2224
    23 inductive JointStatement (A: Type[0]) (globals: list Identifier): Type[0] ≝
    24   | Joint_St_Sequential: JointInstruction globals → A → JointStatement A globals
    25   | Joint_St_Goto: Identifier → JointStatement A globals
    26   | Joint_St_Return: JointStatement A globals.
     25inductive joint_statement (A: Type[0]) (globals: list ident): Type[0] ≝
     26  | joint_st_sequential: joint_instruction globals → A → joint_statement A globals
     27  | joint_st_goto: ident → joint_statement A globals
     28  | joint_st_return: joint_statement A globals.

  • src/LIN/LIN.ma

    r723 r757  
    11include "LIN/JointLTLLIN.ma".
    22 
    3 definition PreLINStatement ≝ JointStatement unit.
     3definition pre_lin_statement ≝ joint_statement unit.
    44
    5 definition LINStatement ≝
     5definition lin_statement ≝
    66  λglobals.
    7     option Identifier × (PreLINStatement globals).
     7    option ident × (pre_lin_statement globals).
    88
    9 definition WellFormedP ≝
     9definition well_formed_P ≝
    1010  λA, B: Type[0].
    1111  λcode: list (option A × B).
    … …  
    1919    ].
    2020   
    21 inductive LINFunctionDefinition (globals: list Identifier): Type[0] ≝
    22   LIN_Fu_Internal: ∀code: list (LINStatement globals). WellFormedP ? ? code → LINFunctionDefinition globals
    23 | LIN_Fu_External: ExternalFunction → LINFunctionDefinition globals.
     21inductive lin_function_definition (globals: list ident): Type[0] ≝
     22  lin_fu_internal: ∀code: list (lin_statement globals). well_formed_P ? ? code → lin_function_definition globals
     23| lin_fu_external: external_function → lin_function_definition globals.
    2424
    25 record LINProgram: Type[0] ≝
     25record lin_program: Type[0] ≝
    2626{
    27   LIN_Pr_vars: list (Identifier × nat);
    28   LIN_Pr_funs: list (Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) LIN_Pr_vars)));
    29   LIN_Pr_main: option Identifier
     27  lin_pr_vars: list (ident × nat);
     28  lin_pr_funcs: list (ident × (lin_function_definition (map ? ? (fst ? ?) lin_pr_vars)));
     29  lin_pr_main: option ident
    3030}.
    3131
    32 definition LIN_Pr_vars:
    33     LINProgram → list (Identifier × nat).
     32definition lin_pr_vars:
     33    lin_program → list (ident × nat).
    3434  # r
    3535  cases r
    … …  
    3838qed.
    3939
    40 definition LIN_Pr_funs:
    41   ∀p: LINProgram.
    42     list (Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) (LIN_Pr_vars p)))).
     40definition lin_pr_funcs:
     41  ∀p: lin_program.
     42    list (ident × (lin_function_definition (map ? ? (fst ? ?) (lin_pr_vars p)))).
    4343  # r
    4444  cases r

  • src/LIN/LINToASM.ma

    r734 r757  
    44include "LIN/LIN.ma".
    55 
    6 let rec association (i: Identifier) (l: list (Identifier × nat))
    7                     on l: member i (eq_bv ?) (map ? ? (fst ? ?) l) → nat ≝
    8   match l return λl. member i (eq_bv ?) (map ? ? (fst ? ?) l) → nat with
     6let rec association (i: ident) (l: list (ident × nat))
     7                    on l: member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat ≝
     8  match l return λl. member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat with
    99  [ nil ⇒ λabsd. ?
    1010  | cons hd tl ⇒
    11     λprf: member i (eq_bv ?) (map ? ? (fst ? ?) (cons ? hd tl)).
    12       (match eq_bv ? (\fst hd) i return λb. eq_bv ? (\fst hd) i = b → nat with
     11    λprf: member i (eq_identifier ?) (map ? ? (fst ? ?) (cons ? hd tl)).
     12      (match eq_identifier ? (\fst hd) i return λb. eq_identifier ? (\fst hd) i = b → nat with
    1313      [ true ⇒ λeq_prf. \snd hd
    1414      | false ⇒ λeq_prf. association i tl ?
    15       ]) (refl ? (eq_bv ? (\fst hd) i))
     15      ]) (refl ? (eq_identifier ? (\fst hd) i))
    1616  ].
    1717  [ cases absd
    … …  
    2727
    2828definition statement_labels ≝
    29   λg: list Identifier.
    30   λs: LINStatement g.
     29  λg: list ident.
     30  λs: lin_statement g.
    3131  let 〈label, instr〉 ≝ s in
    3232  let generated ≝
    3333    match instr with
    34     [ Joint_St_Sequential instr' _ ⇒
     34    [ joint_st_sequential instr' _ ⇒
    3535        match instr' with
    36         [ Joint_Instr_CostLabel lbl ⇒ set_insert ? lbl (set_empty ?)
    37         | Joint_Instr_CondAcc lbl ⇒ set_insert ? lbl (set_empty ?)
     36        [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     37        | joint_instr_cond_acc lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    3838        | _ ⇒ set_empty ?
    3939        ]
    40     | Joint_St_Goto lbl ⇒ set_insert ? lbl (set_empty ?)
    41     | Joint_St_Return ⇒ set_empty ?
     40    | joint_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     41    | joint_st_return ⇒ set_empty ?
    4242    ] in
    4343  match label with
    4444  [ None ⇒ generated
    45   | Some lbl ⇒ set_insert ? lbl generated
     45  | Some lbl ⇒ set_insert ? (word_of_identifier ? lbl) generated
    4646  ].
    4747
    4848definition function_labels_internal ≝
    49   λglobals: list Identifier.
     49  λglobals: list ident.
    5050  λlabels: BitVectorTrieSet ?.
    51   λstatement: LINStatement globals.
     51  λstatement: lin_statement globals.
    5252    set_union ? labels (statement_labels globals statement).
    5353
    … …  
    5555definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝
    5656  λA: Type[0].
    57   λglobals: list Identifier.
    58   λf: A × (LINFunctionDefinition globals).
     57  λglobals: list ident.
     58  λf: A × (lin_function_definition globals).
    5959  let 〈ignore, fun_def〉 ≝ f in
    6060  match fun_def return λ_. BitVectorTrieSet ? with
    61   [ LIN_Fu_Internal stmts proof ⇒
     61  [ lin_fu_internal stmts proof ⇒
    6262      foldl ? ? (function_labels_internal globals) (set_empty ?) stmts
    63   | LIN_Fu_External _ ⇒ set_empty ?
     63  | lin_fu_external _ ⇒ set_empty ?
    6464  ].
    6565 
    6666definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet ? ≝
    6767  λA: Type[0].
    68   λglobals: list Identifier.
     68  λglobals: list ident.
    6969  λlabels: BitVectorTrieSet ?.
    70   λfunct: A × (LINFunctionDefinition globals).
     70  λfunct: A × (lin_function_definition globals).
    7171    set_union ? labels (function_labels ? globals funct).
    7272   
    7373definition program_labels ≝
    7474  λprogram.
    75     foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) (LIN_Pr_vars program)))
    76               (set_empty ?) (LIN_Pr_funs program).
     75    foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) (lin_pr_vars program)))
     76              (set_empty ?) (lin_pr_funcs program).
    7777   
    7878definition data_of_int ≝ λbv. DATA bv.
    … …  
    8383
    8484definition translate_statements ≝
    85   λglobals: list (Identifier × nat).
    86   λglobals_old: list Identifier.
    87   λprf: ∀i: Identifier. member i (eq_bv ?) globals_old → member i (eq_bv ?) (map ? ? (fst ? ?) globals).
    88   λstatement: PreLINStatement globals_old.
     85  λglobals: list (ident × nat).
     86  λglobals_old: list ident.
     87  λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals).
     88  λstatement: pre_lin_statement globals_old.
    8989  match statement with
    90   [ Joint_St_Return ⇒ Instruction (RET ?)
    91   | Joint_St_Goto lbl ⇒ Jmp lbl
    92   | Joint_St_Sequential instr _ ⇒
     90  [ joint_st_return ⇒ Instruction (RET ?)
     91  | joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
     92  | joint_st_sequential instr _ ⇒
    9393    match instr with
    94     [ Joint_Instr_Comment comment ⇒ Comment comment
    95     | Joint_Instr_CostLabel lbl ⇒ Cost lbl
    96     | Joint_Instr_Pop ⇒ Instruction (POP ? accumulator_address)
    97     | Joint_Instr_Push ⇒ Instruction (PUSH ? accumulator_address)
    98     | Joint_Instr_ClearCarry ⇒ Instruction (CLR ? CARRY)
    99     | Joint_Instr_CallId f ⇒ Call f
    100     | Joint_Instr_OpAccs accs ⇒
     94    [ joint_instr_comment comment ⇒ Comment comment
     95    | joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl)
     96    | joint_instr_pop ⇒ Instruction (POP ? accumulator_address)
     97    | joint_instr_push ⇒ Instruction (PUSH ? accumulator_address)
     98    | joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY)
     99    | joint_instr_call_id f ⇒ Call (word_of_identifier ? f)
     100    | joint_instr_opaccs accs ⇒
    101101      match accs with
    102102      [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
    … …  
    104104      | Modu ⇒ ?
    105105      ]
    106     | Joint_Instr_Op1 op1 ⇒
     106    | joint_instr_op1 op1 ⇒
    107107      match op1 with
    108108      [ Cmpl ⇒ Instruction (CPL ? ACC_A)
    109109      | Inc ⇒ Instruction (INC ? ACC_A)
    110110      ]
    111     | Joint_Instr_Op2 op2 reg ⇒
     111    | joint_instr_op2 op2 reg ⇒
    112112      match op2 with
    113113      [ Add ⇒
    114         let reg' ≝ register_address reg in
    115         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    116                                                        direct;
    117                                                        register ]] x) → ? with
     114        let reg' ≝ register_address (Register_of_register reg) in
     115        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     116                                                       direct;
     117                                                       registr ]] x) → ? with
    118118        [ ACC_A ⇒ λacc_a: True.
    119119          Instruction (ADD ? ACC_A accumulator_address)
    … …  
    125125        ] (subaddressing_modein … reg')
    126126      | Addc ⇒
    127         let reg' ≝ register_address reg in
    128         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    129                                                        direct;
    130                                                        register ]] x) → ? with
     127        let reg' ≝ register_address (Register_of_register reg) in
     128        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     129                                                       direct;
     130                                                       registr ]] x) → ? with
    131131        [ ACC_A ⇒ λacc_a: True.
    132132          Instruction (ADDC ? ACC_A accumulator_address)
    … …  
    138138        ] (subaddressing_modein … reg')
    139139      | Sub ⇒
    140         let reg' ≝ register_address reg in
    141         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    142                                                        direct;
    143                                                        register ]] x) → ? with
     140        let reg' ≝ register_address (Register_of_register reg) in
     141        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     142                                                       direct;
     143                                                       registr ]] x) → ? with
    144144        [ ACC_A ⇒ λacc_a: True.
    145145          Instruction (SUBB ? ACC_A accumulator_address)
    … …  
    151151        ] (subaddressing_modein … reg')
    152152      | And ⇒
    153         let reg' ≝ register_address reg in
    154         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    155                                                        direct;
    156                                                        register ]] x) → ? with
     153        let reg' ≝ register_address (Register_of_register reg) in
     154        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     155                                                       direct;
     156                                                       registr ]] x) → ? with
    157157        [ ACC_A ⇒ λacc_a: True.
    158158          Instruction (NOP ?)
    … …  
    164164        ] (subaddressing_modein … reg')
    165165      | Or ⇒
    166         let reg' ≝ register_address reg in
    167         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    168                                                        direct;
    169                                                        register ]] x) → ? with
     166        let reg' ≝ register_address (Register_of_register reg) in
     167        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     168                                                       direct;
     169                                                       registr ]] x) → ? with
    170170        [ ACC_A ⇒ λacc_a: True.
    171171          Instruction (NOP ?)
    … …  
    177177        ] (subaddressing_modein … reg')
    178178      | Xor ⇒
    179         let reg' ≝ register_address reg in
    180         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    181                                                        direct;
    182                                                        register ]] x) → ? with
     179        let reg' ≝ register_address (Register_of_register reg) in
     180        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     181                                                       direct;
     182                                                       registr ]] x) → ? with
    183183        [ ACC_A ⇒ λacc_a: True.
    184184          Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
    … …  
    190190        ] (subaddressing_modein … reg')
    191191      ]
    192     | Joint_Instr_Int reg byte ⇒
    193       let reg' ≝ register_address reg in
    194         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    195                                                        direct;
    196                                                        register ]] x) → ? with
     192    | joint_instr_int reg byte ⇒
     193      let reg' ≝ register_address (Register_of_register reg) in
     194        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     195                                                       direct;
     196                                                       registr ]] x) → ? with
    197197        [ REGISTER r ⇒ λregister7: True.
    198198          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉))))))
    … …  
    203203        | _ ⇒ λother: False. ⊥
    204204        ] (subaddressing_modein … reg')
    205     | Joint_Instr_FromAcc reg ⇒
    206       let reg' ≝ register_address reg in
    207         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    208                                                        direct;
    209                                                        register ]] x) → ? with
     205    | joint_instr_from_acc reg ⇒
     206      let reg' ≝ register_address (Register_of_register reg) in
     207        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     208                                                       direct;
     209                                                       registr ]] x) → ? with
    210210        [ REGISTER r ⇒ λregister8: True.
    211211          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
    … …  
    216216        | _ ⇒ λother: False. ⊥
    217217        ] (subaddressing_modein … reg')
    218     | Joint_Instr_ToAcc reg ⇒
    219       let reg' ≝ register_address reg in
    220         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    221                                                        direct;
    222                                                        register ]] x) → ? with
     218    | joint_instr_to_acc reg ⇒
     219      let reg' ≝ register_address (Register_of_register reg) in
     220        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     221                                                       direct;
     222                                                       registr ]] x) → ? with
    223223        [ REGISTER r ⇒ λregister9: True.
    224224          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
    … …  
    229229        | _ ⇒ λother: False. ⊥
    230230        ] (subaddressing_modein … reg')
    231     | Joint_Instr_Load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
    232     | Joint_Instr_Store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    233     | Joint_Instr_Address addr proof ⇒
     231    | joint_instr_load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
     232    | joint_instr_store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
     233    | joint_instr_address addr proof ⇒
    234234      let look ≝ association addr globals (prf ? proof) in
    235235        Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
    236     | Joint_Instr_CondAcc lbl ⇒
     236    | joint_instr_cond_acc lbl ⇒
    237237      (* dpm: this should be handled in translate_code! *)
    238       WithLabel (JNZ ? lbl)
     238      WithLabel (JNZ ? (word_of_identifier ? lbl))
    239239    ]
    240240  ].
    … …  
    248248  λglobals_old.
    249249  λprf.
    250   λstatement: LINStatement globals_old.
     250  λstatement: lin_statement globals_old.
    251251    〈\fst statement, translate_statements globals globals_old prf (\snd statement)〉.
    252252
    253253definition translate_code ≝
    254   λglobals: list (Identifier × nat).
    255   λglobals_old: list Identifier.
     254  λglobals: list (ident × nat).
     255  λglobals_old: list ident.
    256256  λprf.
    257   λcode: list (LINStatement globals_old).
     257  λcode: list (lin_statement globals_old).
    258258    map ? ? (build_translated_statement globals globals_old prf) code.
    259259   
    260260lemma translate_code_preserves_WellFormedP:
    261261  ∀globals, globals_old, prf, code.
    262     WellFormedP ? ? code → WellFormedP ? ? (translate_code globals globals_old prf code).
     262    well_formed_P ? ? code → well_formed_P ? ? (translate_code globals globals_old prf code).
    263263  #G #GO #P #C
    264264  elim C
    … …  
    279279    let 〈id, def〉 ≝ id_def in
    280280    match def with
    281     [ LIN_Fu_Internal code proof ⇒
    282       match translate_code globals globals_old prf code return λtranscode. WellFormedP ? ? transcode → list labelled_instruction with
     281    [ lin_fu_internal code proof ⇒
     282      match translate_code globals globals_old prf code return λtranscode. well_formed_P ? ? transcode → list labelled_instruction with
    283283      [ nil ⇒ λprf2. ⊥
    284       | cons hd tl ⇒ λ_. 〈Some ? id, \snd hd〉 :: tl
     284      | cons hd tl ⇒ λ_.
     285        let rest ≝ 〈Some ? id, \snd hd〉 :: tl in
     286          map ? ? (
     287            λr.
     288            match fst ? ? r with
     289            [ Some id' ⇒ 〈Some ? (word_of_identifier ? id'), snd ? ? r〉
     290            | None ⇒ 〈None ?, \snd r〉
     291            ]) rest
    285292      ] (translate_code_preserves_WellFormedP globals globals_old prf code proof)
    286293    | _ ⇒ [ ]

  • src/LTL/LTL.ma

    r753 r757  
    11include "common/Graphs.ma".
    22include "utilities/IdentifierTools.ma".
    3 
    43include "LIN/LIN.ma".
    54
    6 definition LTLStatement ≝ JointStatement Identifier.
     5definition ltl_statement ≝ joint_statement ident.
    76 
    8 definition LTLStatementGraph ≝ λglobals. graph (LTLStatement globals).
     7definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
    98 
    10 record LTLInternalFunction (globals: list Identifier): Type[0] ≝
     9record ltl_internal_function (globals: list ident): Type[0] ≝
    1110{
    12   LTL_IF_LUniverse: Universe;
    13   LTL_IF_StackSize: nat;
    14   LTL_IF_Graph: LTLStatementGraph globals;
    15   LTL_IF_Entry: label;
    16   LTL_IF_Exit: label
     11  ltl_if_luniverse: universe LabelTag;
     12  ltl_if_runiverse: universe RegisterTag;
     13  ltl_if_StackSize: nat;
     14  ltl_if_Graph: ltl_statement_graph globals;
     15  ltl_if_Entry: label;
     16  ltl_if_Exit: label
    1717}.
    1818
    19 inductive LTLFunctionDefinition (globals: list Identifier): Type[0] ≝
    20   | LTL_Fu_InternalFunction: LTLInternalFunction globals → LTLFunctionDefinition globals
    21   | LTL_Fu_ExternalFunction: ExternalFunction → LTLFunctionDefinition globals.
     19inductive ltl_function_definition (globals: list ident): Type[0] ≝
     20  | ltl_fu_internal_function: ltl_internal_function globals → ltl_function_definition globals
     21  | ltl_fu_external_function: external_function → ltl_function_definition globals.
    2222 
    23 record LTLProgram (globals: list (Identifier × nat)): Type[0] ≝
     23record ltl_program (globals: list (ident × nat)): Type[0] ≝
    2424{
    25   LTL_Pr_Funs: list (Identifier × (LTLFunctionDefinition (map ? ? \fst globals)));
    26   LTL_Pr_Main: option Identifier
     25  ltl_pr_funcs: list (ident × (ltl_function_definition (map ? ? \fst globals)));
     26  ltl_pr_main: option ident
    2727}.

  • src/LTL/LTLToLIN.ma

    r753 r757  
    66axiom LTLTag: String.
    77
    8 definition translate_statement: ∀globals. LTLStatement globals → PreLINStatement globals ≝
    9   λglobals: list Identifier.
    10   λs: LTLStatement globals.
     8definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝
     9  λglobals: list ident.
     10  λs: ltl_statement globals.
    1111    match s with
    12     [ Joint_St_Return ⇒ Joint_St_Return ? globals
    13     | Joint_St_Sequential instr _ ⇒ Joint_St_Sequential ? globals instr it
    14     | Joint_St_Goto lbl ⇒ Joint_St_Goto ? globals lbl
     12    [ joint_st_return ⇒ joint_st_return ? globals
     13    | joint_st_sequential instr _ ⇒ joint_st_sequential ? globals instr it
     14    | joint_st_goto lbl ⇒ joint_st_goto ? globals lbl
    1515    ].
    1616   
    17 definition require: Identifier → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
    18   λl: Identifier.
     17definition require: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
     18  λl: ident.
    1919  λg: BitVectorTrieSet 16.
    2020    set_insert ? l g.
    2121   
    22 definition mark: Identifier → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
    23   λl: Identifier.
     22definition mark: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
     23  λl: ident.
    2424  λg: BitVectorTrieSet 16.
    2525    set_insert ? l g.
    2626   
    27 definition marked: Identifier → BitVectorTrieSet 16 → bool ≝
    28   λl: Identifier.
     27definition marked: ident → BitVectorTrieSet 16 → bool ≝
     28  λl: ident.
    2929  λg: BitVectorTrieSet 16.
    3030    set_member ? l g.
    … …  
    3232definition graph_lookup ≝
    3333  λglobals.
    34   λl: Identifier.
    35   λg: LTLStatementGraph globals.
     34  λl: ident.
     35  λg: ltl_statement_graph globals.
    3636    lookup LabelTag (LTLStatement globals) g (an_identifier LabelTag l).
    3737   
    … …  
    5858   visit globals g required visited generated l2 n.
    5959
    60 let rec visit (globals: list Identifier) (g: LTLStatementGraph globals)
     60let rec visit (globals: list ident) (g: ltl_statement_graph globals)
    6161              (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
    62               (generated: list (PreLINStatement globals)) (l: Identifier) (n: nat) on n: BitVectorTrieSet 16 × (list (PreLINStatement globals)) ≝
     62              (generated: list (pre_lin_statement globals)) (l: ident) (n: nat) on n: BitVectorTrieSet 16 × (list (PreLINStatement globals)) ≝
    6363  match n with
    6464  [ O ⇒ 〈required, generated〉
    … …  
    7171      let generated'' ≝ translated_statement :: generated in
    7272      match statement with
    73       [ Joint_St_Sequential instr l2 ⇒
     73      [ joint_st_sequential instr l2 ⇒
    7474        match instr with
    75         [ Joint_Instr_CondAcc l1 ⇒
     75        [ joint_instr_cond_acc l1 ⇒
    7676            let required' ≝
    7777              if marked l2 visited' then
    … …  
    101101            visit globals g required' visited' generated'' l2 n'
    102102        ]
    103       | Joint_St_Goto lbl ⇒
     103      | joint_st_goto lbl ⇒
    104104        let required' ≝
    105105          if marked lbl visited' then
    … …  
    111111        else
    112112          visit globals g required' visited' generated'' lbl n'
    113       | Joint_St_Return ⇒ 〈required, generated''〉 (* dpm: correct? *)
     113      | joint_st_Return ⇒ 〈required, generated''〉 (* dpm: correct? *)
    114114      ]
    115115    ]

  • src/common/AST.ma

    r747 r757  
    497497
    498498(* dpm: should go to standard library *)
    499 let rec member (i: Identifier) (eq_i: Identifier → Identifier → bool)
    500                (g: list Identifier) on g: Prop ≝
     499let rec member (i: ident) (eq_i: ident → ident → bool)
     500               (g: list ident) on g: Prop ≝
    501501  match g with
    502502  [ nil ⇒ False

  • src/common/CostLabel.ma

    r747 r757  
    77(* For use in importing programs in intermediate languages. *)
    88definition costlabel_of_nat : nat → costlabel ≝ identifier_of_nat ?.
     9
     10(* dpm: fix identifier/costlabel mismatch *)
     11axiom Identifier_of_costlabel: costlabel → Identifier.

  • src/common/Identifiers.ma

    r753 r757  
    2424      OK ? 〈an_identifier tag (next_identifier ? g), mk_universe tag gen〉.
    2525// qed.
     26
     27definition eq_identifier ≝
     28  λt.
     29  λl, r: identifier t.
     30  match l with
     31  [ an_identifier l' ⇒
     32    match r with
     33    [ an_identifier r' ⇒
     34      eq_bv ? l' r'
     35    ]
     36  ].
     37   
     38   
     39definition word_of_identifier ≝
     40  λt.
     41  λl: identifier t.
     42  match l with   
     43  [ an_identifier l' ⇒ l'
     44  ].
    2645
    2746definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).

  • src/common/Registers.ma

    r738 r757  
    66include "ASM/BitVectorTrie.ma".
    77include "common/Identifiers.ma".
     8include "ASM/I8051.ma".
    89
    910axiom RegisterTag : String.
    … …  
    1415
    1516definition register_env ≝ identifier_map RegisterTag.
     17
     18(* dpm: fix the Register/register mismatch *)
     19axiom Register_of_register: register → Register.
Note: See TracChangeset for help on using the changeset viewer.