source: src/LIN/joint_LTL_LIN.ma @ 2760

Last change on this file since 2760 was 2645, checked in by sacerdot, 7 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 1.5 KB
Line 
1include "joint/Joint.ma".
2
3inductive registers_move: Type[0] ≝
4 | from_acc: Register → unit → registers_move
5 | to_acc: unit → Register → registers_move
6 | int_to_reg : Register → Byte → registers_move
7 | int_to_acc : unit → Byte → registers_move.
8(* the last is redudant, but kept for notation's sake *)
9
10inductive ltl_lin_seq : Type[0] ≝
11| SAVE_CARRY : ltl_lin_seq
12| RESTORE_CARRY : ltl_lin_seq
13| LOW_ADDRESS : Register → label → ltl_lin_seq
14| HIGH_ADDRESS : Register → label → ltl_lin_seq.
15
16definition ltl_lin_seq_labels ≝ λs.match s with
17[ LOW_ADDRESS _ lbl ⇒ [ lbl ]
18| HIGH_ADDRESS _ lbl ⇒ [ lbl ]
19| _ ⇒ [ ]
20].
21
22definition LTL_LIN : unserialized_params ≝ mk_unserialized_params
23    (* acc_a_reg ≝ *) unit
24    (* acc_b_reg ≝ *) unit
25    (* acc_a_arg ≝ *) unit
26    (* acc_b_arg ≝ *) unit
27    (* dpl_reg   ≝ *) unit
28    (* dph_reg   ≝ *) unit
29    (* dpl_arg   ≝ *) unit
30    (* dph_arg   ≝ *) unit
31    (* snd_arg   ≝ *) hdw_argument
32    (* pair_move ≝ *) registers_move
33    (* call_args ≝ *) ℕ
34    (* call_dest ≝ *) unit
35    (* ext_seq ≝ *) ltl_lin_seq
36    (* ext_seq_labels ≝ *) ltl_lin_seq_labels
37    (* has_tailcalls ≝ *) false
38    (* paramsT ≝ *) unit.
39
40interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)).
41interpretation "move to acc" 'mov a b = (MOVE ?? (to_acc a b)).
42interpretation "move int to reg" 'mov a b = (MOVE ?? (int_to_reg a b)).
43interpretation "move int to acc" 'mov a b = (MOVE ?? (int_to_acc a b)).
Note: See TracBrowser for help on using the repository browser.