source: src/ERTL/ERTL.ma @ 2652

Last change on this file since 2652 was 2645, checked in by sacerdot, 8 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: 2.9 KB
Line 
1include "joint/Joint.ma".
2
3inductive move_dst: Type[0] ≝
4  | PSD: register → move_dst
5  | HDW: Register → move_dst.
6
7definition move_src ≝ argument move_dst.
8
9definition move_src_from_dst : move_dst → move_src ≝ Reg move_dst.
10coercion move_dst_to_src : ∀r : move_dst.move_src ≝ move_src_from_dst on _r : move_dst to move_src.
11
12definition psd_argument_move_src : psd_argument → move_src ≝
13  λarg.match arg with
14  [ Imm b ⇒ Imm ? b
15  | Reg r ⇒ Reg ? (PSD r)
16  ].
17coercion psd_argument_to_move_src : ∀a:psd_argument.move_src ≝
18  psd_argument_move_src on _a : psd_argument to move_src.
19
20inductive ertl_seq : Type[0] ≝
21  | ertl_new_frame: ertl_seq
22  | ertl_del_frame: ertl_seq
23  | ertl_frame_size: register → ertl_seq.
24
25definition ERTL_uns ≝ mk_unserialized_params
26    (* acc_a_reg ≝ *) register
27    (* acc_b_reg ≝ *) register
28    (* acc_a_arg ≝ *) psd_argument
29    (* acc_b_arg ≝ *) psd_argument
30    (* dpl_reg   ≝ *) register
31    (* dph_reg   ≝ *) register
32    (* dpl_arg   ≝ *) psd_argument
33    (* dph_arg   ≝ *) psd_argument
34    (* snd_arg   ≝ *) psd_argument
35    (* pair_move ≝ *) (move_dst × move_src)
36    (* call_args ≝ *) ℕ
37    (* call_dest ≝ *) unit
38    (* ext_seq ≝ *) ertl_seq
39    (* ext_seq_labels ≝ *) (λ_.[])
40    (* has_tailcall ≝ *) false
41    (* paramsT ≝ *) ℕ.
42
43definition ERTL ≝ mk_graph_params ERTL_uns.
44definition ertl_program ≝ joint_program ERTL.
45
46interpretation "move" 'mov r a = (MOVE ?? (mk_Prod move_dst move_src r a)).
47
48(* aid unification *)
49unification hint 0 ≔
50(*---------------*) ⊢
51pair_move ERTL ≡ move_dst × move_src.
52unification hint 0 ≔
53(*---------------*) ⊢
54acc_a_reg ERTL ≡ register.
55unification hint 0 ≔
56(*---------------*) ⊢
57acc_b_reg ERTL ≡ register.
58unification hint 0 ≔
59(*---------------*) ⊢
60acc_a_arg ERTL ≡ psd_argument.
61unification hint 0 ≔
62(*---------------*) ⊢
63acc_b_arg ERTL ≡ psd_argument.
64unification hint 0 ≔
65(*---------------*) ⊢
66dpl_reg ERTL ≡ register.
67unification hint 0 ≔
68(*---------------*) ⊢
69dph_reg ERTL ≡ register.
70unification hint 0 ≔
71(*---------------*) ⊢
72dpl_arg ERTL ≡ psd_argument.
73unification hint 0 ≔
74(*---------------*) ⊢
75dph_arg ERTL ≡ psd_argument.
76unification hint 0 ≔
77(*---------------*) ⊢
78snd_arg ERTL ≡ psd_argument.
79unification hint 0 ≔
80(*---------------*) ⊢
81call_args ERTL ≡ ℕ.
82unification hint 0 ≔
83(*---------------*) ⊢
84call_dest ERTL ≡ unit.
85
86unification hint 0 ≔
87(*---------------*) ⊢
88ext_seq ERTL ≡ ertl_seq.
89
90coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ERTL ≝
91  psd_argument_from_reg
92  on _r : register to snd_arg ERTL.
93coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ERTL ≝
94  psd_argument_from_byte
95  on _b : Byte to snd_arg ERTL.
96 
97definition ertl_seq_joint ≝ extension_seq ERTL.
98coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ERTL globals ≝ ertl_seq_joint
99  on _s : ertl_seq to joint_seq ERTL ?.
Note: See TracBrowser for help on using the repository browser.