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

Changes from working on my PC.

File:
1 edited

Legend:

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