Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/backends/backends.ml
2 2
let join_guards = ref true
3 3

  
4 4
let setup () =
5
  if !Options.output = "emf" then begin
5
  if !Options.output = "emf" then (
6 6
    (* Not merging branches *)
7 7
    join_guards := false;
8 8
    (* In case of a default "int" type, substitute it with the legal int32 value *)
9
    if !Options.int_type = "int" then Options.int_type := "int32"
10
  end;
11
  if !Options.optimization < 0 then
12
    join_guards := false
9
    if !Options.int_type = "int" then Options.int_type := "int32");
10
  if !Options.optimization < 0 then join_guards := false
13 11

  
14
let is_functional () = 
12
let is_functional () =
15 13
  match !Options.output with
16
  | "horn" | "lustre" | "acsl" | "emf" -> true
17
  | _ -> false
14
  | "horn" | "lustre" | "acsl" | "emf" ->
15
    true
16
  | _ ->
17
    false
18 18

  
19
                             
20 19
(* Special treatment of arrows in lustre backend. We want to keep them *)
21
let unfold_arrow () =
22
  match !Options.output with
23
  | "lustre" -> false
24
  | _ -> true
20
let unfold_arrow () = match !Options.output with "lustre" -> false | _ -> true
25 21

  
26 22
(* Forcing ite normalization *)
27
let alias_ite () =
28
  match !Options.output with
29
  | "emf" -> true
30
  | _ -> false
23
let alias_ite () = match !Options.output with "emf" -> true | _ -> false
31 24

  
32 25
(* Forcing basic functions normalization *)
33 26
let alias_internal_fun () =
34
  match !Options.output with
35
  | "emf" -> true
36
  | _ -> false
27
  match !Options.output with "emf" -> true | _ -> false
37 28

  
38
let get_normalization_params () = {
29
let get_normalization_params () =
30
  {
39 31
    Normalization.unfold_arrow_active = unfold_arrow ();
40 32
    force_alias_ite = alias_ite ();
41 33
    force_alias_internal_fun = alias_internal_fun ();
42 34
  }
43 35

  
44

  
45 36
(* Local Variables: *)
46 37
(* compile-command: "make -k -C .." *)
47 38
(* End: *)

Also available in: Unified diff