source: src/ERTLptr/ERTLptr.ma @ 2645

Last change on this file since 2645 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.1 KB
Line 
1include "ERTL/ERTL.ma".
2
3inductive ertlptr_seq : Type[0] ≝
4  | ertlptr_ertl: ertl_seq → ertlptr_seq
5  | LOW_ADDRESS : register → label → ertlptr_seq
6  | HIGH_ADDRESS : register → label → ertlptr_seq.
7
8definition ERTLptr_uns ≝ mk_unserialized_params
9    (* acc_a_reg ≝ *) register
10    (* acc_b_reg ≝ *) register
11    (* acc_a_arg ≝ *) psd_argument
12    (* acc_b_arg ≝ *) psd_argument
13    (* dpl_reg   ≝ *) register
14    (* dph_reg   ≝ *) register
15    (* dpl_arg   ≝ *) psd_argument
16    (* dph_arg   ≝ *) psd_argument
17    (* snd_arg   ≝ *) psd_argument
18    (* pair_move ≝ *) (move_dst × move_src)
19    (* call_args ≝ *) ℕ
20    (* call_dest ≝ *) unit
21    (* ext_seq ≝ *) ertlptr_seq
22    (* ext_seq_labels ≝ *) (λ_.[])
23    (* has_tailcall ≝ *) false
24    (* paramsT ≝ *) ℕ.
25
26definition ERTLptr ≝ mk_graph_params ERTLptr_uns.
27definition ertlptr_program ≝ joint_program ERTLptr.
28 
29definition ertlptr_seq_joint ≝ extension_seq ERTLptr.
30coercion ertlptr_seq_to_joint_seq : ∀globals.∀s : ertlptr_seq.joint_seq ERTLptr globals ≝ ertlptr_seq_joint
31  on _s : ertlptr_seq to joint_seq ERTLptr ?.
32 
Note: See TracBrowser for help on using the repository browser.