Changeset 723 for src/LIN/LIN.ma


Ignore:
Timestamp:
Mar 30, 2011, 12:34:25 PM (10 years ago)
Author:
mulligan
Message:

Added dependent type internalising the invariant that LIN function bodies are non-empty and do not start with a label.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN.ma

    r722 r723  
    1 include "arithmetics/nat.ma".
    2 include "ASM/String.ma".
     1include "LIN/JointLTLLIN.ma".
     2 
     3definition PreLINStatement ≝ JointStatement unit.
    34
    4 include "ASM/I8051.ma".
    5 include "common/AST.ma".
    6 
    7 alias id "ASMOp1" = "cic:/matita/cerco/ASM/I8051/Op1.ind(1,0,0)".
    8 alias id "ASMOp2" = "cic:/matita/cerco/ASM/I8051/Op2.ind(1,0,0)".
    9 
    10 inductive 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 
    29 inductive 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  
    335definition LINStatement ≝
    346  λglobals.
    35     option Identifier × (JointStatement unit globals).
    36  
    37 definition LINInternalFunction ≝ λglobals. list (LINStatement globals).
     7    option Identifier × (PreLINStatement globals).
    388
     9definition WellFormedP ≝
     10  λA, B: Type[0].
     11  λcode: list (option A × B).
     12    match code with
     13    [ nil ⇒ False
     14    | cons hd tl ⇒
     15      match \fst hd with
     16      [ Some lbl ⇒ False
     17      | None ⇒ True
     18      ]
     19    ].
     20   
    3921inductive LINFunctionDefinition (globals: list Identifier): Type[0] ≝
    40   LIN_Fu_Internal: LINInternalFunction globals → LINFunctionDefinition globals
     22  LIN_Fu_Internal: ∀code: list (LINStatement globals). WellFormedP ? ? code → LINFunctionDefinition globals
    4123| LIN_Fu_External: ExternalFunction → LINFunctionDefinition globals.
    4224
Note: See TracChangeset for help on using the changeset viewer.