Changeset 1164


Ignore:
Timestamp:
Sep 1, 2011, 4:53:01 PM (8 years ago)
Author:
mulligan
Message:

ltl to lin working again, more changes to joint syntax

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/JointLTLLIN.ma

    r1163 r1164  
    66include "common/Registers.ma".
    77
     8inductive registers_move: Type[0] ≝
     9  | from_acc: Register → registers_move
     10  | to_acc: Register → registers_move.
     11
    812inductive joint_instruction
    9   (globals: list ident) (acc_a_reg: Type[0]) (acc_b_reg: Type[0])
    10   (dpl_reg: Type[0]) (dph_reg: Type[0]) (pair_reg: Type[0]) (generic_reg: Type[0]): Type[0] ≝
    11   | joint_instr_comment: String → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
    12   | joint_instr_cost_label: costlabel → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
    13   | joint_instr_int: generic_reg → Byte → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
    14   | joint_instr_move: pair_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
    15   | joint_instr_pop: acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
    16   | joint_instr_push: acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
    17   | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg → dph_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
    18   | joint_instr_opaccs: OpAccs → acc_a_reg → acc_b_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
    19   | joint_instr_op1: Op1 → acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
    20   | joint_instr_op2: Op2 → acc_a_reg → generic_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
    21   | joint_instr_clear_carry: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
    22   | joint_instr_set_carry: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
    23   | joint_instr_load: acc_a_reg → dpl_reg → dph_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
    24   | joint_instr_store: dpl_reg → dph_reg → acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
    25   | joint_instr_call_id: ident → nat → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
    26   | joint_instr_cond: acc_a_reg → label → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg.
     13  (acc_a_reg: Type[0]) (acc_b_reg: Type[0]) (dpl_reg: Type[0])
     14  (dph_reg: Type[0]) (pair_reg: Type[0]) (generic_reg: Type[0]) (globals: list ident): Type[0] ≝
     15  | joint_instr_comment: String → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
     16  | joint_instr_cost_label: costlabel → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
     17  | joint_instr_int: generic_reg → Byte → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
     18  | joint_instr_move: pair_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
     19  | joint_instr_pop: acc_a_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
     20  | joint_instr_push: acc_a_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
     21  | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg → dph_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
     22  | joint_instr_opaccs: OpAccs → acc_a_reg → acc_b_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
     23  | joint_instr_op1: Op1 → acc_a_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
     24  | joint_instr_op2: Op2 → acc_a_reg → generic_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
     25  | joint_instr_clear_carry: joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
     26  | joint_instr_set_carry: joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
     27  | joint_instr_load: acc_a_reg → dpl_reg → dph_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
     28  | joint_instr_store: dpl_reg → dph_reg → acc_a_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
     29  | joint_instr_call_id: ident → nat → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
     30  | joint_instr_cond: acc_a_reg → label → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals.
    2731
    2832inductive joint_statement
    29   (A: Type[0]) (globals: list ident) (acc_a_reg: Type[0]) (acc_b_reg: Type[0])
    30   (dpl_reg: Type[0]) (dph_reg: Type[0]) (pair_reg: Type[0]) (generic_reg: Type[0]): Type[0] ≝
    31   | joint_st_sequential: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg → A → joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
    32   | joint_st_goto: label → joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
    33   | joint_st_return: joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg.
     33  (A: Type[0]) (acc_a_reg: Type[0]) (acc_b_reg: Type[0]) (dpl_reg: Type[0])
     34  (dph_reg: Type[0]) (pair_reg: Type[0]) (generic_reg: Type[0]) (globals: list ident): Type[0] ≝
     35  | joint_st_sequential: joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals → A → joint_statement A acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
     36  | joint_st_goto: label → joint_statement A acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
     37  | joint_st_return: joint_statement A acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals.
  • src/LIN/LIN.ma

    r1163 r1164  
    22 
    33definition pre_lin_statement ≝
    4   λglobals.
    5   joint_statement unit globals Register Register
     4  joint_statement unit Register Register
    65                  Register Register Register
    7                   (Register × Register).
     6                  registers_move.
    87
    98definition lin_statement ≝
  • src/LTL/LTL.ma

    r1163 r1164  
    44
    55definition ltl_statement ≝
    6   λglobals.
    7     joint_statement label globals Register
     6    joint_statement label Register Register
    87                    Register Register Register
    9                     Register (Register × Register).
     8                    registers_move.
    109 
    1110definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
  • src/LTL/LTLToLIN.ma

    r1149 r1164  
    1010  λs: ltl_statement globals.
    1111    match s with
    12     [ joint_st_return ⇒ joint_st_return ? globals
    13     | joint_st_sequential instr _ ⇒ joint_st_sequential ? globals instr it
    14     | joint_st_goto l ⇒ joint_st_goto ? globals l
     12    [ joint_st_return ⇒ joint_st_return globals
     13    | joint_st_sequential instr _ ⇒ joint_st_sequential globals instr it
     14    | joint_st_goto l ⇒ joint_st_goto globals l
    1515    ].
    1616   
     
    5656    BitVectorTrieSet 16 × (list (pre_lin_statement globals)).
    5757  if marked l2 visited then
    58     〈require l2 required, (joint_st_goto ? globals l2) :: generated〉
     58    〈require l2 required, (joint_st_goto globals l2) :: generated〉
    5959  else
    6060   visit globals g required visited generated l2 n.
     
    8080      [ joint_st_sequential instr l2 ⇒
    8181        match instr with
    82         [ joint_instr_cond_acc l1 ⇒
     82        [ joint_instr_cond acc_a_reg l1 ⇒
    8383              let required' ≝
    8484                if marked l2 visited' then
     
    104104                required in
    105105            if marked l2 visited' then
    106               〈required', joint_st_goto ? globals l2 :: generated''〉
     106              〈required', joint_st_goto globals l2 :: generated''〉
    107107            else
    108108              visit globals g required' visited' generated'' l2 n'
     
    117117       in
    118118         if marked l visited' then
    119            〈required', joint_st_goto ? globals l :: generated''〉
     119           〈required', joint_st_goto globals l :: generated''〉
    120120         else
    121121           visit globals g required' visited' generated'' l n'
Note: See TracChangeset for help on using the changeset viewer.