Add an experimental transpiler to Velus (`-velus` flag)

src/compiler_stages.ml

@@ -127,6 +127,7 @@ let stage1 params prog dirname basename extension =
   (* Clock calculus *)
   Global.clock_env := clock_decls !Global.clock_env prog;
 
+
   (* Registering and checking machine types *)
   if Machine_types.is_active then Machine_types.load prog;
 
@@ -182,6 +183,12 @@ let stage1 params prog dirname basename extension =
   (* (\* Registering and checking machine types *\) *)
   (* Machine_types.load prog; *)
 
+  (* Dump Velus output *)
+  (if !Options.velus_print then
+     let basename = Filename.basename basename in
+     let velus_file = basename ^ ".velus.lus" in
+     Utils.Format.with_out_file velus_file (fun fmt -> Velus_printer.pp_prog fmt prog));
+
   (* Normalization phase *)
   Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. normalization@ ");
   let prog = Normalization.normalize_prog params prog in

src/options.ml

@@ -82,6 +82,7 @@ let al_nb_max = ref 15
 
 (* Printer options *)
 let kind2_print = ref false
+let velus_print = ref false
 
 (* C main options *)
 let c_main_options = ref false

src/options.mli

 val kind2_print : bool ref
+val velus_print : bool ref
 val mpfr : bool ref
 val print_dec_types : bool ref
 val verbose_level : int ref

src/options_management.ml

@@ -104,7 +104,8 @@ let common_options =
     ( "-algebraic-loop-max",
       Arg.Set_int al_nb_max,
       "try to solve \x1b[4mnb\x1b[0m number of algebraic loops  <default: 15>" );
-    "-kind2", Arg.Set kind2_print, "active kind2 output";
+    "-kind2", Arg.Set kind2_print, "enable kind2 output";
+    "-velus", Arg.Set velus_print, "enable Velus output";
     ( "-verbose",
       Arg.Set_int verbose_level,
       "changes verbose \x1b[4mlevel\x1b[0m <default: 1>" );

src/velus_printer.ml

+open Lustre_types
+open Utils
+open Format
+
+let error msg =
+  eprintf "Velus output Error: %s@ " msg;
+  exit 1
+
+let warning msg =
+  eprintf "Velus output Warning: %s@ " msg
+
+let error_ns msg =
+  error (msg ^ " are not supported by Velus")
+
+let warning_ig msg =
+  error (msg ^ " are ignored")
+
+let pp_var_type fmt id =
+  let b = !Options.kind2_print in
+  Options.kind2_print := true;
+  Types.pp_node_ty fmt id.var_type;
+  Options.kind2_print := b
+
+let rec print_carrier fmt cr =
+  let open Clocks in
+  match cr.carrier_desc with
+  | Carry_const id ->
+    fprintf fmt "%s" id
+  | Carry_name
+  | Carry_var ->
+    assert false
+  | Carry_link cr' ->
+    print_carrier fmt cr'
+
+let pp_var_clock fmt id =
+  let open Clocks in
+  let rec pp_suffix fmt ck =
+    match ck.cdesc with
+    | Carrow _ | Ctuple _ | Cvar | Cunivar ->
+      ()
+    | Con (ck, c, "true") ->
+      fprintf fmt "%a when %a" pp_suffix ck print_carrier c
+    | Con (ck, c, "false") ->
+      fprintf fmt "%a when not %a" pp_suffix ck print_carrier c
+    | Con _ ->
+      error_ns "Generalized clocks"
+    | Clink ck' ->
+      pp_suffix fmt ck'
+    | Ccarrying (_, ck') ->
+      fprintf fmt "%a" pp_suffix ck'
+  in
+  pp_suffix fmt id.var_clock
+
+let pp_node_var fmt id =
+  if id.var_dec_const then warning_ig "Constant parameters";
+  if Option.is_some id.var_dec_value then warning_ig "Parameter initializations";
+  fprintf
+    fmt
+    "%s: %a%a"
+    id.var_id
+    pp_var_type
+    id
+    pp_var_clock
+    id
+
+let pp_const fmt c =
+  match c with
+  | Const_int i ->
+    pp_print_int fmt i
+  | Const_real r ->
+    Real.pp fmt r
+  | Const_tag t ->
+    pp_print_string fmt t
+  | Const_array _ ->
+    error_ns "Arrays"
+  | Const_struct _ ->
+    error_ns "Structures"
+  (* used only for annotations *)
+  | Const_string _
+  | Const_modeid _ ->
+    warning_ig "Annotations"
+
+let zero expr = expr
+
+let rec pp_expr fmt expr =
+  if Option.is_some expr.expr_annot then warning_ig "Expression annotations";
+  let rec pp fmt e = match e with
+    | Expr_const c ->
+      pp_const fmt c
+    | Expr_ident id ->
+      pp_print_string fmt id
+    | Expr_array _
+    | Expr_access _
+    | Expr_power _ ->
+      error_ns "Arrays"
+    | Expr_tuple el ->
+      fprintf fmt "%a" (pp_print_parenthesized pp_expr) el
+    | Expr_ite (c, t, e) ->
+      fprintf
+        fmt
+        "@[<hov 1>(if %a then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]@])"
+        pp_expr
+        c
+        pp_expr
+        t
+        pp_expr
+        e
+    | Expr_arrow (e1, e2) ->
+      begin match e2.expr_desc with
+        | Expr_pre _ ->
+          warning "-> pre's are replaced by fby's";
+          pp fmt (Expr_fby (e1, e2))
+        | _ -> fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2
+      end
+    | Expr_fby (e1, e2) ->
+      begin match e2.expr_desc with
+        | Expr_pre e2 ->
+          pp fmt (Expr_fby (e1, e2))
+        | _ -> fprintf fmt "%a fby (%a)" pp_expr e1 pp_expr e2
+      end
+    | Expr_pre e ->
+      warning "pre's are replaced by fby's";
+      pp fmt (Expr_fby (zero e, e))
+    | Expr_when (e, id, "true") ->
+      fprintf fmt "(%a) when %s" pp_expr e id
+    | Expr_when (e, id, "false") ->
+      fprintf fmt "(%a) when not %s" pp_expr e id
+    | Expr_when _ ->
+      error_ns "Generalized clocks"
+    | Expr_merge (id, hl) ->
+      fprintf fmt "merge %s %a" id pp_handlers hl
+    | Expr_appl (id, e, r) ->
+      pp_app fmt id e r
+  in
+  fprintf fmt "%a" pp expr.expr_desc
+
+and pp_handler fmt (t, h) = fprintf fmt "(%s -> %a)" t pp_expr h
+
+and pp_handlers fmt hl = pp_print_list pp_handler fmt hl
+
+and pp_app fmt id e r =
+  match r with
+  | None ->
+    pp_call fmt id e
+  | Some c ->
+    fprintf str_formatter "(restart %s every %a)" id pp_expr c;
+    pp_call fmt (flush_str_formatter ()) e
+
+and pp_call fmt id e =
+  match id, e.expr_desc with
+  | "+", Expr_tuple [ e1; e2 ] ->
+    fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2
+  | "uminus", _ ->
+    fprintf fmt "(- %a)" pp_expr e
+  | "-", Expr_tuple [ e1; e2 ] ->
+    fprintf fmt "(%a - %a)" pp_expr e1 pp_expr e2
+  | "*", Expr_tuple [ e1; e2 ] ->
+    fprintf fmt "(%a * %a)" pp_expr e1 pp_expr e2
+  | "/", Expr_tuple [ e1; e2 ] ->
+    fprintf fmt "(%a / %a)" pp_expr e1 pp_expr e2
+  | "mod", Expr_tuple [ e1; e2 ] ->
+    fprintf fmt "(%a mod %a)" pp_expr e1 pp_expr e2
+  | "&&", Expr_tuple [ e1; e2 ] ->
+    fprintf fmt "(%a and %a)" pp_expr e1 pp_expr e2
+  | "||", Expr_tuple [ e1; e2 ] ->
+    fprintf fmt "(%a or %a)" pp_expr e1 pp_expr e2
+  | "xor", Expr_tuple [ e1; e2 ] ->
+    fprintf fmt "(%a xor %a)" pp_expr e1 pp_expr e2
+  | "<", Expr_tuple [ e1; e2 ] ->
+    fprintf fmt "(%a < %a)" pp_expr e1 pp_expr e2
+  | "<=", Expr_tuple [ e1; e2 ] ->
+    fprintf fmt "(%a <= %a)" pp_expr e1 pp_expr e2
+  | ">", Expr_tuple [ e1; e2 ] ->
+    fprintf fmt "(%a > %a)" pp_expr e1 pp_expr e2
+  | ">=", Expr_tuple [ e1; e2 ] ->
+    fprintf fmt "(%a >= %a)" pp_expr e1 pp_expr e2
+  | "!=", Expr_tuple [ e1; e2 ] ->
+    fprintf fmt "(%a <> %a)" pp_expr e1 pp_expr e2
+  | "=", Expr_tuple [ e1; e2 ] ->
+    fprintf fmt "(%a = %a)" pp_expr e1 pp_expr e2
+  | "not", _ ->
+    fprintf fmt "(not %a)" pp_expr e
+  | _, Expr_tuple _ ->
+    fprintf fmt "%s %a" id pp_expr e
+  | _ ->
+    fprintf fmt "%s (%a)" id pp_expr e
+
+let pp_eq_lhs = pp_comma_list pp_print_string
+
+let pp_node_eq fmt eq =
+  fprintf fmt "%a = %a;" pp_eq_lhs eq.eq_lhs pp_expr eq.eq_rhs
+
+let pp_node_stmt fmt stmt =
+  match stmt with
+  | Eq eq -> pp_node_eq fmt eq
+  | Aut _ -> error_ns "Automata"
+
+let pp_node_stmts fmt stmts =
+  pp_print_list
+    ~pp_open_box:pp_open_vbox0
+    ~pp_sep:pp_print_cut
+    pp_node_stmt
+    fmt
+    stmts
+
+let pp_node_args = pp_print_list ~pp_sep:pp_print_semicolon pp_node_var
+
+let pp_node fmt nd =
+  (* Prototype *)
+  fprintf
+    fmt
+    "node @[<hov>%s (%a)@ returns (%a)@]@ "
+    nd.node_id
+    pp_node_args
+    nd.node_inputs
+    pp_node_args
+    nd.node_outputs;
+  (* Contracts *)
+  if Option.is_some nd.node_spec then warning_ig "Contracts";
+  (* Locals *)
+  fprintf
+    fmt
+    "%a"
+    (pp_print_list
+       ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 4)
+       ~pp_prologue:(fun fmt () -> pp_print_string fmt "var ")
+       ~pp_epilogue:pp_print_cut
+       ~pp_eol:pp_print_semicolon
+       ~pp_sep:pp_print_semicolon
+       pp_node_var)
+    (List.map fst nd.node_locals);
+  (* Checks *)
+  if nd.node_checks <> [] then warning_ig "Node checks";
+  (* Body *)
+  (* Annotations *)
+  if nd.node_annot <> [] then warning_ig "Node annotations";
+  (* Asserts *)
+  if nd.node_asserts <> [] then warning_ig "Node asserts";
+  (* Statements *)
+  fprintf fmt "@[<v 2>let@ %a@]@ tel"
+    pp_node_stmts nd.node_stmts
+
+let pp_node fmt nd =
+  match nd.node_spec, nd.node_iscontract with
+  | None, false | Some (NodeSpec _), false ->
+    pp_node fmt nd
+  | Some (Contract _), false ->
+    pp_node fmt nd (* may happen early in the compil process *)
+  | Some (Contract _), true ->
+    warning_ig "Contract nodes"
+  | _ ->
+    assert false
+
+let pp_decl fmt decl =
+  match decl.top_decl_desc with
+  | Node nd ->
+    fprintf fmt "%a" pp_node nd
+  | TypeDef _ ->
+    error_ns "Type definitions"
+  | ImportedNode _ ->
+    error_ns "Imported nodes"
+  | Const _ ->
+    error_ns "Top-level constants"
+  | Open _ ->
+    error_ns "Open directives"
+  | Include _ ->
+    error_ns "Include directives"
+
+let pp_prog fmt prog =
+  fprintf fmt "%a@."
+  (pp_print_list
+    ~pp_open_box:pp_open_vbox0
+    ~pp_sep:pp_print_cutcut
+    pp_decl)
+  prog