Changeset 722 for src/LIN/LIN.ma


Ignore:
Timestamp:
Mar 29, 2011, 6:32:47 PM (9 years ago)
Author:
mulligan
Message:

Committing changes from today. Several files do not typecheck.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN.ma

    r714 r722  
    88alias id "ASMOp2" = "cic:/matita/cerco/ASM/I8051/Op2.ind(1,0,0)".
    99
    10 inductive LINStatement (globals: list Identifier): Type[0] ≝
    11   | LIN_St_Goto: Identifier → LINStatement globals
    12   | LIN_St_Label: Identifier → LINStatement globals
    13   | LIN_St_Comment: String → LINStatement globals
    14   | LIN_St_CostLabel: Identifier → LINStatement globals
    15   | LIN_St_Int: Register → Byte → LINStatement globals
    16   | LIN_St_Pop: LINStatement globals
    17   | LIN_St_Push: LINStatement globals
    18   | LIN_St_Address: ∀i: Identifier. (member i (eq_bv ?) globals) → LINStatement globals
    19   | LIN_St_FromAcc: Register → LINStatement globals
    20   | LIN_St_ToAcc: Register → LINStatement globals
    21   | LIN_St_OpAccs: OpAccs → LINStatement globals
    22   | LIN_St_Op1: ASMOp1 → LINStatement globals
    23   | LIN_St_Op2: ASMOp2 → Register → LINStatement globals
    24   | LIN_St_ClearCarry: LINStatement globals
    25   | LIN_St_Load: LINStatement globals
    26   | LIN_St_Store: LINStatement globals
    27   | LIN_St_CallId: Identifier → LINStatement globals
    28   | LIN_St_CondAcc: Identifier → LINStatement globals
    29   | LIN_St_Return: LINStatement globals.
     10inductive JointInstruction (globals: list Identifier): Type[0] ≝
     11  | Joint_Instr_Goto: Identifier → JointInstruction globals
     12  | Joint_Instr_Comment: String → JointInstruction globals
     13  | Joint_Instr_CostLabel: Identifier → JointInstruction globals
     14  | Joint_Instr_Int: Register → Byte → JointInstruction globals
     15  | Joint_Instr_Pop: JointInstruction globals
     16  | Joint_Instr_Push: JointInstruction globals
     17  | Joint_Instr_Address: ∀i: Identifier. (member i (eq_bv ?) globals) → JointInstruction globals
     18  | Joint_Instr_FromAcc: Register → JointInstruction globals
     19  | Joint_Instr_ToAcc: Register → JointInstruction globals
     20  | Joint_Instr_OpAccs: OpAccs → JointInstruction globals
     21  | Joint_Instr_Op1: Op1 → JointInstruction globals
     22  | Joint_Instr_Op2: Op2 → Register → JointInstruction globals
     23  | Joint_Instr_ClearCarry: JointInstruction globals
     24  | Joint_Instr_Load: JointInstruction globals
     25  | Joint_Instr_Store: JointInstruction globals
     26  | Joint_Instr_CallId: Identifier → JointInstruction globals
     27  | Joint_Instr_CondAcc: Identifier → JointInstruction globals.
     28
     29inductive JointStatement (A: Type[0]) (globals: list Identifier): Type[0] ≝
     30  | LIN_St_Sequential: JointInstruction globals → A → JointStatement A globals
     31  | LIN_St_Return: JointStatement A globals.
     32 
     33definition LINStatement ≝
     34  λglobals.
     35    option Identifier × (JointStatement unit globals).
    3036 
    3137definition LINInternalFunction ≝ λglobals. list (LINStatement globals).
Note: See TracChangeset for help on using the changeset viewer.