Changeset 699 for src/LIN/LIN.ma


Ignore:
Timestamp:
Mar 18, 2011, 2:53:25 PM (9 years ago)
Author:
mulligan
Message:

More or less finished formalisation of LIN.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN.ma

    r698 r699  
    44include "ASM/I8051.ma".
    55include "common/AST.ma".
    6 include "utilities/StringTools.ma".
    76
    87alias id "ASMOp1" = "cic:/matita/cerco/ASM/I8051/Op1.ind(1,0,0)".
    98alias id "ASMOp2" = "cic:/matita/cerco/ASM/I8051/Op2.ind(1,0,0)".
    109
     10(* dpm: should go to standard library *)
    1111let rec member (i: Identifier) (eq_i: Identifier → Identifier → bool)
    12                (g: list (Identifier × nat)) on g: Prop ≝
     12               (g: list Identifier) on g: Prop ≝
    1313  match g with
    1414  [ nil ⇒ False
    1515  | cons hd tl ⇒
    16       bool_to_Prop (eq_i (fst ? ? hd) i) ∨ member i eq_i tl
     16      bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
    1717  ].
    1818
    19 inductive LINStatement (globals: list (Identifier × nat)): Type[0] ≝
     19inductive LINStatement (globals: list Identifier): Type[0] ≝
    2020  | LIN_St_Goto: Identifier → LINStatement globals
    2121  | LIN_St_Label: Identifier → LINStatement globals
    2222  | LIN_St_Comment: String → LINStatement globals
    23   | LIN_St_CostLabel: CostLabel → LINStatement globals
     23  | LIN_St_CostLabel: Identifier → LINStatement globals
    2424  | LIN_St_Int: Register → Byte → LINStatement globals
    2525  | LIN_St_Pop: LINStatement globals
     
    4040definition LINInternalFunction ≝ λglobals. list (LINStatement globals).
    4141
    42 inductive LINFunctionDefinition (globals: list (Identifier × nat)): Type[0] ≝
     42inductive LINFunctionDefinition (globals: list Identifier): Type[0] ≝
    4343  LIN_Fu_Internal: LINInternalFunction globals → LINFunctionDefinition globals
    4444| LIN_Fu_External: ExternalFunction → LINFunctionDefinition globals.
    4545
    46 record LINProgram (globals: list (Identifier × nat)): Type[0] ≝
     46record LINProgram: Type[0] ≝
    4747{
    4848  LIN_Pr_vars: list (Identifier × nat);
    49   LIN_Pr_funs: list (Identifier × (LINFunctionDefinition globals));
     49  LIN_Pr_funs: list (Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) LIN_Pr_vars)));
    5050  LIN_Pr_main: option Identifier
    5151}.
     52
     53definition LIN_Pr_vars:
     54    LINProgram → list (Identifier × nat).
     55  # r
     56  cases r
     57  # H1 # H2 #H3
     58  @ H1
     59qed.
     60
     61definition LIN_Pr_funs:
     62  ∀p: LINProgram.
     63    list (Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) (LIN_Pr_vars p)))).
     64  # r
     65  cases r
     66  # H1 # H2 #H3
     67  @ H2
     68qed.
Note: See TracChangeset for help on using the changeset viewer.