source: src/ERTLptr/ERTLtoERTLptr.ma @ 2566

Last change on this file since 2566 was 2566, checked in by piccolo, 7 years ago

ERTL to ERTLptr pass implemented up to a few things to be
left to the infrastructure (marked with PAOLO)

File size: 3.3 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "ERTL/ERTL.ma".
16include "ERTLptr/ERTLptr.ma".
17include "joint/TranslateUtils.ma".
18
19(* PAOLO: implement the b_graph_translate2 that expects functions that
20   return not (list instr * instr) but (list (label → instr) * instr) *)
21definition translate_step:
22 ∀globals.
23 label
24  →joint_step ERTL globals
25   →bind_seq_block ERTLptr globals (joint_step ERTLptr globals) ≝
26 λglobals.λl.λs.?.
27cases s
28[ #called #args #dest cases called
29  [ (*#_*) #id % %{[]} %1 [%1{id}] assumption
30  | (*#pc*) #dest1 %2 #reg %1 @(〈[?;?;?;?], ?〉)
31    [ @extension_seq @(LOW_ADDRESS reg ?(*pc*)) cases daemon
32    | @(PUSH … (Reg … reg))
33    | @extension_seq @(HIGH_ADDRESS reg ?(*pc*)) cases daemon
34    | @(PUSH … (Reg … reg))
35    | %1 [%2{dest1}] assumption
36    ]]
37| (*#_*) #reg #l %{[]} %2 assumption
38| (*#_*) #X %1 %{[]} %3 cases X
39  try (#a #b #c #d #e) try (#a #b #c #d) try (#a #b #c) try (#a #b) try #a
40  [%1|%2|%3|%4|%5|%6|%7|%8|%9|%10|%11|%12|%13|%14] try assumption
41  %1 @a ]
42qed.
43
44definition joint_fin_step_id: joint_fin_step ERTL → joint_fin_step ERTLptr.
45 * [#l %1 @l | %2 | #H #arg #arg' %3 assumption ]
46qed.
47
48(*CSC: cut&paste from RTLtoERTL up to ERTLptr :-( keep just one copy*)
49definition ertl_fresh_reg:
50 ∀globals.freshT ERTLptr globals register ≝
51  λglobals,def.
52    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
53    〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
54
55definition translate_internal :  ∀globals: list ident.
56  joint_closed_internal_function ERTL globals →
57  joint_closed_internal_function ERTLptr globals ≝
58  λglobals,int_fun.
59  (* initialize internal function *)
60  let init ≝ init_graph_if ERTLptr globals
61    (joint_if_luniverse … int_fun)
62    (joint_if_runiverse … int_fun)
63    (joint_if_result … int_fun)
64    (joint_if_params … int_fun)
65    (joint_if_locals … int_fun)
66    (joint_if_stacksize … int_fun)
67    (joint_if_entry … int_fun)
68    (joint_if_exit … int_fun) in
69  b_graph_translate …
70    (ertl_fresh_reg …)
71    init
72    (translate_step …)
73    (λ_.λstep.bret ?? 〈[],joint_fin_step_id step〉)
74    int_fun.
75cases daemon.
76qed.
77
78definition ertl_to_ertlptr: ertl_program → ertlptr_program ≝
79  λp.transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).
Note: See TracBrowser for help on using the repository browser.