Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (8 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN.ma

    r1378 r2286  
    22
    33inductive registers_move: Type[0] ≝
    4  | from_acc: Register → registers_move
    5  | to_acc: Register → registers_move.
     4 | from_acc: Register → unit → registers_move
     5 | to_acc: unit → Register → registers_move
     6 | int_to_reg : Register → beval → registers_move
     7 | int_to_acc : unit → beval → registers_move.
     8(* the last is redudant, but kept for notation's sake *)
    69
    7 definition ltl_lin_params__: params__ ≝
    8  mk_params__ unit unit unit unit registers_move Register nat unit False.
    9 definition ltl_lin_params0 : params0 ≝ mk_params0 ltl_lin_params__ unit unit.
    10 definition ltl_lin_params1 : params1 ≝ mk_params1 ltl_lin_params0 unit.
     10inductive ltl_lin_seq : Type[0] ≝
     11| SAVE_CARRY : ltl_lin_seq
     12| RESTORE_CARRY : ltl_lin_seq.
     13
     14definition LTL_LIN : unserialized_params ≝ mk_unserialized_params
     15    (* acc_a_reg ≝ *) unit
     16    (* acc_b_reg ≝ *) unit
     17    (* acc_a_arg ≝ *) unit
     18    (* acc_b_arg ≝ *) unit
     19    (* dpl_reg   ≝ *) unit
     20    (* dph_reg   ≝ *) unit
     21    (* dpl_arg   ≝ *) unit
     22    (* dph_arg   ≝ *) unit
     23    (* snd_arg   ≝ *) hdw_argument
     24    (* pair_move ≝ *) registers_move
     25    (* call_args ≝ *) ℕ
     26    (* call_dest ≝ *) unit
     27    (* ext_seq ≝ *) ltl_lin_seq
     28    (* ext_call ≝ *) void
     29    (* ext_tailcall ≝ *) void
     30    (* paramsT ≝ *) unit
     31    (* localsT ≝ *) void.
     32
     33interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)).
     34interpretation "move to acc" 'mov a b = (MOVE ?? (to_acc a b)).
     35interpretation "move int to reg" 'mov a b = (MOVE ?? (int_to_reg a b)).
     36interpretation "move int to acc" 'mov a b = (MOVE ?? (int_to_acc a b)).
Note: See TracChangeset for help on using the changeset viewer.