Revision 23ce017b
Added by Pierre-Loïc Garoche over 6 years ago
| src/algebraicLoop.ml | ||
|---|---|---|
| 2 | 2 |
each node is mapped to its own cycles |
| 3 | 3 |
each cycle is tentatively solved by inlining one of its component |
| 4 | 4 |
|
| 5 |
When done, a report is generated |
|
| 5 |
When done, a report is generated.
|
|
| 6 | 6 |
|
| 7 | 7 |
- for each initial AL, the cycle is presented |
| 8 | 8 |
- either it is solvable and we provide the set of inlines that solves it |
| 9 | 9 |
- or it is not and we write the AL as unsolvable by inlining |
| 10 | 10 |
|
| 11 | 11 |
If the option solve_al is activated, the resulting partially inlined prog is |
| 12 |
propagated fur future processing |
|
| 13 |
Otherwise the program stops |
|
| 12 |
propagated fur future processing Otherwise the compilation stops |
|
| 14 | 13 |
*) |
| 15 | 14 |
open LustreSpec |
| 16 | 15 |
open Corelang |
| ... | ... | |
| 18 | 17 |
open Format |
| 19 | 18 |
|
| 20 | 19 |
(* An single algebraic loop is defined (partition, node calls, inlined, status) |
| 21 |
ie the list of variables in the loop, ident list |
|
| 22 |
the possible functions identifier to inline, and whether they have been inlined yet (ident * tag * bool) list |
|
| 23 |
and a status whether the inlining is enough bool |
|
| 20 |
ie |
|
| 21 |
|
|
| 22 |
1. the list of variables in the loop, ident list |
|
| 23 |
|
|
| 24 |
2.the possible functions identifier to inline, and whether they have been |
|
| 25 |
inlined yet (ident * tag * bool) list and |
|
| 26 |
|
|
| 27 |
3. a status whether the inlining is enough bool |
|
| 24 | 28 |
*) |
| 25 |
type algebraic_loop = (ident list * (ident * expr * bool) list * bool) |
|
| 29 |
|
|
| 30 |
type call = ident * expr * eq (* fun id, expression, and containing equation *) |
|
| 31 |
|
|
| 32 |
type algebraic_loop = ident list * (call * bool) list * bool |
|
| 26 | 33 |
|
| 27 | 34 |
exception Error of (node_desc * (algebraic_loop list)) list |
| 28 | 35 |
|
| ... | ... | |
| 33 | 40 |
|
| 34 | 41 |
(* We iter over calls in node defs. If the call defined on of the variable in |
| 35 | 42 |
the cycle, we store it for future possible inline. *) |
| 36 |
let resolve node partition = |
|
| 43 |
let resolve node partition : call list =
|
|
| 37 | 44 |
let partition = ISet.of_list partition in |
| 38 | 45 |
(* Preprocessing calls: associate to each of them the eq.lhs associated *) |
| 39 | 46 |
let eqs = get_node_eqs node in |
| ... | ... | |
| 47 | 54 |
| Expr_appl(fun_id, _, _) -> fun_id |
| 48 | 55 |
| _ -> assert false |
| 49 | 56 |
in |
| 50 |
eq, expr, fun_name
|
|
| 57 |
fun_name, expr, eq
|
|
| 51 | 58 |
) calls_expr in |
| 52 | 59 |
List.fold_left ( |
| 53 |
fun accu ((eq, _, _) as call) ->
|
|
| 60 |
fun accu ((_, _, eq) as call) ->
|
|
| 54 | 61 |
let shared_vars = ISet.inter (ISet.of_list eq.eq_lhs) partition in |
| 55 | 62 |
if not (ISet.is_empty shared_vars) then |
| 56 | 63 |
(* We have a match: keep the eq and the expr to inline *) |
| ... | ... | |
| 69 | 76 |
Format.fprintf fmt "inlining: %a" Printers.pp_node_eq eq |
| 70 | 77 |
) fmt resolution |
| 71 | 78 |
|
| 72 |
let al_is_solved al = true |
|
| 73 |
|
|
| 74 |
(********************) |
|
| 79 |
let al_is_solved (_, (vars, calls, status)) = status |
|
| 80 |
|
|
| 81 |
(**********************************************************************) |
|
| 82 |
(* Functions to access or toggle the local inlining feature of a call *) |
|
| 83 |
(* expression *) |
|
| 84 |
(**********************************************************************) |
|
| 75 | 85 |
|
| 76 | 86 |
let inline_annotation loc = |
| 77 | 87 |
Inliner.keyword, |
Also available in: Unified diff
Ongoing work