Changeset 683


Ignore:
Timestamp:
Mar 15, 2011, 2:47:34 PM (9 years ago)
Author:
mulligan
Message:

Changes from working on my PC.

Location:
Deliverables/D4.2-4.3
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.2-4.3/ASM/I8051.ma

    r491 r683  
    108108    let r_as_nat ≝ nat_of_register r in
    109109    let s_as_nat ≝ nat_of_register s in
    110       if eqb r_as_nat s_as_nat then
    111         Compare_Equal
    112       else if ltb r_as_nat s_as_nat then
    113         Compare_Less
    114       else
    115         Compare_Greater.
     110      match eqb r_as_nat s_as_nat with
     111      [ true ⇒ Compare_Equal
     112      | false ⇒
     113        match ltb r_as_nat s_as_nat with
     114        [ true ⇒ Compare_Less
     115        | false ⇒ Compare_Greater
     116        ]
     117      ].
    116118
    117119definition eq_register: Register → Register → bool ≝
  • Deliverables/D4.2-4.3/LIN/LIN.ma

    r491 r683  
    99alias id "ASMOp2" = "cic:/matita/cerco-intermediate-languages/ASM/I8051/Op2.ind(1,0,0)".
    1010
    11 inductive LINStatement: Type[0] ≝
    12   | LIN_St_Goto: Label → LINStatement
    13   | LIN_St_Label: Label → LINStatement
    14   | LIN_St_Comment: String → LINStatement
    15   | LIN_St_CostLabel: CostLabel → LINStatement
    16   | LIN_St_Int: Register → Byte → LINStatement
    17   | LIN_St_Pop: LINStatement
    18   | LIN_St_Push: LINStatement
    19   | LIN_St_Address: Identifier → LINStatement
    20   | LIN_St_FromAcc: Register → LINStatement
    21   | LIN_St_ToAcc: Register → LINStatement
    22   | LIN_St_OpAccs: OpAccs → LINStatement
    23   | LIN_St_Op1: ASMOp1 → LINStatement
    24   | LIN_St_Op2: ASMOp2 → Register → LINStatement
    25   | LIN_St_ClearCarry: LINStatement
    26   | LIN_St_Load: LINStatement
    27   | LIN_St_Store: LINStatement
    28   | LIN_St_CallId: Identifier → LINStatement
    29   | LIN_St_CondAcc: Label → LINStatement
    30   | LIN_St_Return: LINStatement.
     11let rec member (i: Identifier) (eq_i: Identifier → Identifier → bool)
     12               (g: list (Identifier × nat)) on g: Prop ≝
     13  match g with
     14  [ nil ⇒ False
     15  | cons hd tl ⇒
     16    let 〈id, n〉 ≝ hd in
     17    match eq_i i id with
     18    [ true ⇒ True
     19    | false ⇒ member i eq_i tl
     20    ]
     21  ].
     22
     23inductive LINStatement (globals: list (Identifier × nat)): Type[0] ≝
     24  | LIN_St_Goto: Label → LINStatement globals
     25  | LIN_St_Label: Label → LINStatement globals
     26  | LIN_St_Comment: String → LINStatement globals
     27  | LIN_St_CostLabel: CostLabel → LINStatement globals
     28  | LIN_St_Int: Register → Byte → LINStatement globals
     29  | LIN_St_Pop: LINStatement globals
     30  | LIN_St_Push: LINStatement globals
     31  | LIN_St_Address: ∀i: Identifier. (member i (eq_bv ?) globals) → LINStatement globals
     32  | LIN_St_FromAcc: Register → LINStatement globals
     33  | LIN_St_ToAcc: Register → LINStatement globals
     34  | LIN_St_OpAccs: OpAccs → LINStatement globals
     35  | LIN_St_Op1: ASMOp1 → LINStatement globals
     36  | LIN_St_Op2: ASMOp2 → Register → LINStatement globals
     37  | LIN_St_ClearCarry: LINStatement globals
     38  | LIN_St_Load: LINStatement globals
     39  | LIN_St_Store: LINStatement globals
     40  | LIN_St_CallId: Identifier → LINStatement globals
     41  | LIN_St_CondAcc: Label → LINStatement globals
     42  | LIN_St_Return: LINStatement globals.
    3143 
    32 definition LINInternalFunction ≝ list LINStatement.
     44definition LINInternalFunction ≝ λglobals. list (LINStatement globals).
    3345
    34 inductive LINFunctionDefinition: Type[0] ≝
    35   LIN_Fu_Internal: LINInternalFunction → LINFunctionDefinition
    36 | LIN_Fu_External: ExternalFunction → LINFunctionDefinition.
     46inductive LINFunctionDefinition (globals: list (Identifier × nat)): Type[0] ≝
     47  LIN_Fu_Internal: LINInternalFunction globals → LINFunctionDefinition globals
     48| LIN_Fu_External: ExternalFunction → LINFunctionDefinition globals.
    3749
    38 record LINProgram: Type[0] ≝
     50record LINProgram (globals: list (Identifier × nat)): Type[0] ≝
    3951{
    4052  LIN_Pr_vars: list (Identifier × nat);
    41   LIN_Pr_funs: list (Identifier × LINFunctionDefinition);
     53  LIN_Pr_funs: list (Identifier × (LINFunctionDefinition globals));
    4254  LIN_Pr_main: option Identifier
    4355}.
  • Deliverables/D4.2-4.3/LIN/LinToAsm.ma

    r491 r683  
    44
    55definition statement_labels ≝
    6   λs: LINStatement.
     6  λg: list (Identifier × nat).
     7  λs: LINStatement g.
    78  match s with
    89  [ LIN_St_Goto lbl ⇒ set_insert ? lbl (set_empty ?)
     
    1314  ].
    1415
    15 definition function_labels_internal: BitVectorTrieSet 8 → LINStatement → BitVectorTrieSet 8 ≝
     16definition function_labels_internal ≝
     17  λglobals: list (Identifier × nat).
    1618  λlabels: BitVectorTrieSet 8.
    17   λstatement: LINStatement.
    18     set_union ? labels (statement_labels statement).
     19  λstatement: LINStatement globals.
     20    set_union ? labels (statement_labels globals statement).
    1921
    2022(* dpm: A = Identifier *)
    21 definition function_labels: ∀A. ∀f. BitVectorTrieSet 8 ≝
     23definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet 8 ≝
    2224  λA: Type[0].
    23   λf: A × LINFunctionDefinition.
     25  λglobals: list (Identifier × nat).
     26  λf: A × (LINFunctionDefinition globals).
    2427  let 〈ignore, fun_def〉 ≝ f in
    2528  match fun_def return λ_. BitVectorTrieSet 8 with
    2629  [ LIN_Fu_Internal stmts ⇒
    27       foldl ? ? function_labels_internal (set_empty 8) stmts
     30      foldl ? ? (function_labels_internal globals) (set_empty 8) stmts
    2831  | LIN_Fu_External _ ⇒ set_empty ?
    2932  ].
    3033 
    31 definition program_labels_internal: ∀A. ∀labels. ∀funct. BitVectorTrieSet 8 ≝
     34definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet 8 ≝
    3235  λA: Type[0].
     36  λglobals: list (Identifier × nat).
    3337  λlabels: BitVectorTrieSet 8.
    34   λfunct: A × LINFunctionDefinition.
    35     set_union ? labels (function_labels ? funct).
     38  λfunct: A × (LINFunctionDefinition globals).
     39    set_union ? labels (function_labels ? globals funct).
    3640   
    3741definition program_labels ≝
     42  λglobals: list (Identifier × nat).
    3843  λprogram.
    39     foldl ? ? (program_labels_internal ?) (set_empty 8) (LIN_Pr_funs program).
     44    foldl ? ? (program_labels_internal ? globals)
     45              (set_empty 8) (LIN_Pr_funs globals program).
    4046   
    4147definition data_of_int ≝ λbv. DATA bv.
     
    4652
    4753definition translate_statements ≝
    48   λglobal_addresses.
    49   λlin_statement.
     54  λglobals: list (Identifier × nat).
     55  λlin_statement: LINStatement globals.
    5056  match lin_statement with
    51   [ LIN_St_Goto lbl ⇒ [ Jmp lbl ]
    52   | LIN_St_Label lbl ⇒ [ Label lbl ]
    53   | LIN_St_Comment _ ⇒ [ ]
    54   | LIN_St_CostLabel lbl ⇒ [ Cost lbl ]
    55   | LIN_St_Pop ⇒ [ Instruction (POP ? accumulator_address) ]
    56   | LIN_St_Push ⇒ [ Instruction (PUSH ? accumulator_address) ]
    57   | LIN_St_ClearCarry ⇒ [ Instruction (CLR ? CARRY) ]
    58   | LIN_St_Return ⇒ [ Instruction (RET ?) ]
    59   | LIN_St_CallId f ⇒ [ Call f ]
     57  [ LIN_St_Goto lbl ⇒ Some ? [ Jmp lbl ]
     58  | LIN_St_Label lbl ⇒ Some ? [ Label lbl ]
     59  | LIN_St_Comment _ ⇒ Some ? [ ]
     60  | LIN_St_CostLabel lbl ⇒ Some ? [ Cost lbl ]
     61  | LIN_St_Pop ⇒ Some ? [ Instruction (POP ? accumulator_address) ]
     62  | LIN_St_Push ⇒ Some ? [ Instruction (PUSH ? accumulator_address) ]
     63  | LIN_St_ClearCarry ⇒ Some ? [ Instruction (CLR ? CARRY) ]
     64  | LIN_St_Return ⇒ Some ? [ Instruction (RET ?) ]
     65  | LIN_St_CallId f ⇒ Some ? [ Call f ]
    6066  | LIN_St_OpAccs accs ⇒
    6167    match accs with
    62     [ Mul ⇒ [ Instruction (MUL ? ACC_A ACC_B) ]
    63     | Divu ⇒ [ Instruction (DIV ? ACC_A ACC_B) ]
     68    [ Mul ⇒ Some ? [ Instruction (MUL ? ACC_A ACC_B) ]
     69    | Divu ⇒ Some ? [ Instruction (DIV ? ACC_A ACC_B) ]
    6470    | Modu ⇒ ?
    6571    ]
    6672  | LIN_St_Op1 op1 ⇒
    6773    match op1 with
    68     [ Cmpl ⇒ [ Instruction (CPL ? ACC_A) ]
    69     | Inc ⇒ [ Instruction (INC ? ACC_A) ]
     74    [ Cmpl ⇒ Some ? [ Instruction (CPL ? ACC_A) ]
     75    | Inc ⇒ Some ? [ Instruction (INC ? ACC_A) ]
    7076    ]
    7177  | LIN_St_Op2 op2 reg ⇒
    7278    match op2 with
    73     [ Add ⇒ [ Instruction (ADD ? ACC_A (register_address reg)) ]
    74     | Addc ⇒ [ Instruction (ADDC ? ACC_A (register_address reg)) ]
    75     | Sub ⇒ [ Instruction (SUBB ? ACC_A (register_address reg)) ]
    76     | And ⇒ [ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, (register_address reg)〉))) ]
    77     | Or ⇒ [ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, (register_address reg)〉))) ]
    78     | Xor ⇒ [ Instruction (XRL ? (inl ? ? 〈ACC_A, (register_address reg)〉)) ]
     79    [ Add ⇒ Some ? [ Instruction (ADD ? ACC_A (register_address reg)) ]
     80    | Addc ⇒ Some ? [ Instruction (ADDC ? ACC_A (register_address reg)) ]
     81    | Sub ⇒ Some ? [ Instruction (SUBB ? ACC_A (register_address reg)) ]
     82    | And ⇒ Some ? [ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, (register_address reg)〉))) ]
     83    | Or ⇒ Some ? [ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, (register_address reg)〉))) ]
     84    | Xor ⇒ Some ? [ Instruction (XRL ? (inl ? ? 〈ACC_A, (register_address reg)〉)) ]
    7985    ]
    8086  | LIN_St_Int reg byte ⇒
    81     let reg ≝ register_address reg in
    82       match reg return λx. bool_to_Prop (is_in … [[ acc_a;
     87    let reg' ≝ register_address reg in
     88      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    8389                                                    register;
    8490                                                    direct ]] x) → ? with
    8591      [ REGISTER _ ⇒ λreg: True.
    86         [ Instruction (MOV ? (inr ? ? 〈register, (data_of_int byte)〉)) ]
     92        Some ? [ Instruction (MOV ? (inl ? ? 〈register, (data_of_int byte)〉)) ]
     93      | _ ⇒ ?
     94      ] (subaddressing_modein … reg')
     95  | _ ⇒ ?
     96  ].
     97
    8798      | DIRECT _ ⇒ λdirect: True.
    88         [ Instruction (MOV ? (inr ? ? (inr ? ? 〈register, (data_of_int byte)〉))) ]
     99        Some ? [ Instruction (MOV ? (inr ? ? (inr ? ? 〈register, (data_of_int byte)〉))) ]
    89100      | ACC_A ⇒ λacc_a: True.
    90         [ Instruction (MOV ? (inl ? ? 〈ACC_A, (data_of_int byte)〉)) ]
     101        Some ? [ Instruction (MOV ? (inl ? ? 〈ACC_A, (data_of_int byte)〉)) ]
    91102      | _ ⇒ λother: False. ⊥
    92       ] (subaddressing_modein … reg)
    93   | LIN_St_FromAcc reg ⇒ [ Instruction (MOV ? (inr ? ? 〈(register_address reg), ACC_A〉)) ]
    94   | LIN_St_ToAcc reg ⇒ [ Instruction (MOV ? (inl ? ? 〈ACC_A, (register_address reg)〉)) ]
    95   | LIN_St_Address addr ⇒
    96     let lookup ≝ association ? ? global_addresses addr in
    97       [ Instruction (MOV ? (inr ? ? (inr ? ? 〈DPTR, (data16_of_int lookup)〉))) ]
    98   | LIN_St_Load ⇒ [ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) ]
    99   | LIN_St_Store ⇒ [ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) ]
     103      ] (subaddressing_modein … reg')
     104
     105  | LIN_St_FromAcc reg ⇒ ? (*
     106    let reg' ≝ register_address reg in
     107      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     108                                                    register;
     109                                                    direct ]] x) → ? with
     110      [ REGISTER _ ⇒ λreg: True.
     111        Some ? [ Instruction (MOV ? (inr ? ? 〈reg', ACC_A〉)) ]
     112      | DIRECT _ ⇒ λdirect: True.
     113        Some ? [ Instruction (MOV ? (inr ? ? 〈reg', ACC_A〉)) ]
     114      | ACC_A ⇒ λacc_a: True.
     115        Some ? [ Instruction (MOV ? (inr ? ? 〈reg', ACC_A〉)) ]
     116      | _ ⇒ λother: False. ⊥
     117      ] (subaddressing_modein … reg') *)
     118  | LIN_St_ToAcc reg ⇒ ? (*
     119    let reg' ≝ register_address reg in
     120      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     121                                                    register;
     122                                                    direct ]] x) → ? with
     123      [ REGISTER _ ⇒ λreg: True.
     124        Some ? [ Instruction (MOV ? (inr ? ? 〈ACC_A, reg'〉)) ]
     125      | DIRECT _ ⇒ λdirect: True.
     126        Some ? [ Instruction (MOV ? (inr ? ? 〈ACC_A, reg'〉)) ]
     127      | ACC_A ⇒ λacc_a: True.
     128        Some ? [ Instruction (MOV ? (inr ? ? 〈ACC_A, reg'〉)) ]
     129      | _ ⇒ λother: False. ⊥
     130      ] (subaddressing_modein … reg') *)
     131  | LIN_St_Address addr ⇒ ? (*
     132    let look ≝ association ? ? eq_v addr global_addresses in
     133    match look with
     134    [ None ⇒ None
     135    | Some look' ⇒
     136      Some ? [ Instruction (MOV ? (inr ? ? (inr ? ? 〈DPTR, (data16_of_int look')〉))) ]
     137    ] *)
     138  | LIN_St_Load ⇒ Some ? [ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) ]
     139  | LIN_St_Store ⇒ Some ? [ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) ]
    100140  | LIN_St_CondAcc lbl ⇒ ?
    101141  ].
Note: See TracChangeset for help on using the changeset viewer.