Changeset 757 for src/LIN


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

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

Location:
src/LIN
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • 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    | _ ⇒ [ ]
Note: See TracChangeset for help on using the changeset viewer.