Changeset 1161 for src/ERTL/ERTL.ma


Ignore:
Timestamp:
Aug 31, 2011, 6:24:03 PM (9 years ago)
Author:
mulligan
Message:

changes from today: merged ertl, ltl and lin into one datatype to simplify semantics

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1138 r1161  
    11include "ASM/I8051.ma".
     2include "LIN/JointLTLLIN.ma".
    23include "utilities/BitVectorTrieSet.ma".
    34include "utilities/IdentifierTools.ma".
     
    89definition registers ≝ list register.
    910
     11definition pre_ertl_statement ≝
     12  λglobals: list ident.
     13  joint_statement label globals register
     14                  register register register
     15                  register (Register × Register).
     16                 
     17inductive ertl_statement (globals: list ident): Type[0] ≝
     18  | ertl_st_lift_pre: pre_ertl_statement globals → ertl_statement globals
     19  | ertl_st_new_frame: label → ertl_statement globals
     20  | ertl_st_del_frame: label → ertl_statement globals
     21  | ertl_st_frame_size: register → label → ertl_statement globals
     22  | ertl_st_move: register → register → label → ertl_statement globals
     23  | ertl_st_get_hdw: register → Register → label → ertl_statement globals
     24  | ertl_st_set_hdw: Register → register → label → ertl_statement globals.
     25
     26(*
    1027inductive ertl_statement: Type[0] ≝
    1128  | ertl_st_skip: label → ertl_statement
     
    2138  | ertl_st_push: register → label → ertl_statement
    2239  | ertl_st_addr: register → register → ident → label → ertl_statement
    23 (* XXX: changed from O'Caml
    24   | ertl_st_addr_h: register → ident → label → ertl_statement
    25   | ertl_st_addr_l: register → ident → label → ertl_statement
    26 *)
    2740  | ertl_st_int: register → Byte → label → ertl_statement
    2841  | ertl_st_move: register → register → label → ertl_statement
    2942  | ertl_st_opaccs: OpAccs → register → register → register → register → label → ertl_statement
    30 (* XXX: changed from O'Caml
    31   | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
    32   | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
    33 *)
    3443  | ertl_st_op1: Op1 → register → register → label → ertl_statement
    3544  | ertl_st_op2: Op2 → register → register → register → label → ertl_statement
     
    4150  | ertl_st_cond: register → label → label → ertl_statement
    4251  | ertl_st_return: ertl_statement.
     52*)
    4353
    44 definition ertl_statement_graph ≝ graph ertl_statement.
     54definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals).
    4555
    46 record ertl_internal_function: Type[0] ≝
     56record ertl_internal_function (globals: list ident): Type[0] ≝
    4757{
    4858  ertl_if_luniverse: universe LabelTag;
     
    5161  ertl_if_locals: registers;
    5262  ertl_if_stacksize: nat;
    53   ertl_if_graph: ertl_statement_graph;
     63  ertl_if_graph: ertl_statement_graph globals;
    5464  ertl_if_entry: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?;
    5565  ertl_if_exit: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?
    5666}.
    5767
    58 definition ertl_function ≝ fundef ertl_internal_function.
     68definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals).
    5969 
    60 record ertl_program: Type[0] ≝
     70record ertl_program (globals: list ident): Type[0] ≝
    6171{
    6272  ertl_pr_vars: list (ident × nat);
    63   ertl_pr_funcs: list (ident × ertl_function);
     73  ertl_pr_funcs: list (ident × (ertl_function globals));
    6474  ertl_pr_main: option ident
    6575}.
     76
     77
     78(* XXX: changed from O'Caml
     79  | ertl_st_addr_h: register → ident → label → ertl_statement
     80  | ertl_st_addr_l: register → ident → label → ertl_statement
     81*)
     82
     83(* XXX: changed from O'Caml
     84  | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
     85  | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
     86*)
Note: See TracChangeset for help on using the changeset viewer.