From 79613858d9c11a60397de48925f5199d93696f74 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lb@leliobrun.net>
Date: Tue, 9 May 2023 19:42:31 +0900
Subject: [PATCH] Add an experimental transpiler to Velus (`-velus` flag)
---
src/compiler_stages.ml | 7 +
src/options.ml | 1 +
src/options.mli | 1 +
src/options_management.ml | 3 +-
src/velus_printer.ml | 275 ++++++++++++++++++++++++++++++++++++++
5 files changed, 286 insertions(+), 1 deletion(-)
create mode 100644 src/velus_printer.ml
diff --git a/src/compiler_stages.ml b/src/compiler_stages.ml
index 83aa2755..e95db55b 100644
--- a/src/compiler_stages.ml
+++ b/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
diff --git a/src/options.ml b/src/options.ml
index a490d19a..664ff625 100644
--- a/src/options.ml
+++ b/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
diff --git a/src/options.mli b/src/options.mli
index 145646b1..981b26fd 100644
--- a/src/options.mli
+++ b/src/options.mli
@@ -1,4 +1,5 @@
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
diff --git a/src/options_management.ml b/src/options_management.ml
index 5fab157e..65a9afce 100644
--- a/src/options_management.ml
+++ b/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>" );
diff --git a/src/velus_printer.ml b/src/velus_printer.ml
new file mode 100644
index 00000000..9cc5466f
--- /dev/null
+++ b/src/velus_printer.ml
@@ -0,0 +1,275 @@
+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
--
GitLab