Changeset 714


Ignore:
Timestamp:
Mar 29, 2011, 12:24:45 PM (9 years ago)
Author:
mulligan
Message:

Work on translation from LTL to LIN.

Location:
src
Files:
1 added
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r698 r714  
    9696  | VCons m he (tl: Vector addressing_mode_tag m) ⇒
    9797     is_a he A ∨ is_in ? tl A ].
    98 
    99 definition bool_to_Prop ≝
    100  λb. match b with [ true ⇒ True | false ⇒ False ].
    10198
    10299record subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
  • src/LIN/LIN.ma

    r699 r714  
    77alias id "ASMOp1" = "cic:/matita/cerco/ASM/I8051/Op1.ind(1,0,0)".
    88alias id "ASMOp2" = "cic:/matita/cerco/ASM/I8051/Op2.ind(1,0,0)".
    9 
    10 (* dpm: should go to standard library *)
    11 let rec member (i: Identifier) (eq_i: Identifier → Identifier → bool)
    12                (g: list Identifier) on g: Prop ≝
    13   match g with
    14   [ nil ⇒ False
    15   | cons hd tl ⇒
    16       bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
    17   ].
    189
    1910inductive LINStatement (globals: list Identifier): Type[0] ≝
  • src/LTL/LTL.ma

    r713 r714  
    1414  | LTL_St_Pop: label → LTLStatement globals
    1515  | LTL_St_Push: label → LTLStatement globals
    16   | LTL_St_Address: Identifier → label → LTLStatement globals
     16  | LTL_St_Address: ∀i: Identifier. (member i (eq_bv ?) globals) → Identifier → label → LTLStatement globals
    1717  | LTL_St_FromAcc: Register → label → LTLStatement globals
    1818  | LTL_St_ToAcc: Register → label → LTLStatement globals
  • src/common/AST.ma

    r699 r714  
    77definition Identifier ≝ Byte.
    88definition Immediate ≝ nat.
     9
     10definition bool_to_Prop ≝
     11 λb. match b with [ true ⇒ True | false ⇒ False ].
     12
     13(* dpm: should go to standard library *)
     14let rec member (i: Identifier) (eq_i: Identifier → Identifier → bool)
     15               (g: list Identifier) on g: Prop ≝
     16  match g with
     17  [ nil ⇒ False
     18  | cons hd tl ⇒
     19      bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
     20  ].
    921
    1022inductive Compare: Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.