CristalCaveGem » LustreC

(********************************************************************)

(*                                                                  *)

(*  The LustreC compiler toolset   /  The LustreC Development Team  *)

(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)

(*                                                                  *)

(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)

(*  under the terms of the GNU Lesser General Public License        *)

(*  version 2.1.                                                    *)

(*                                                                  *)

(********************************************************************)

open Utils

  [ "initial" ]

let kind2_protect id =

  if List.mem id kind2_language_cst then

    "_KIND2_PROTECT_" ^ id

  else

    id

   following the C convention for multiple lines macro *)

let pp_as_c_macro pp_fun fmt v =

  let macro_newline () =

    begin

      formatter_out_funs.out_string "\\" 0 1;

      formatter_out_funs.out_newline ()

    end in

  fprintf fmt "%a : %a;" pp_print_string label pp_var_type_dec_desc tdesc

and pp_var_type_dec_desc fmt tdesc =

  match tdesc with 

  | Tydec_any -> fprintf fmt "<any>"

  | Tydec_const t -> fprintf fmt "%s" t

  | Tydec_enum id_list -> fprintf fmt "enum {%a }" (fprintf_list ~sep:", " pp_print_string) id_list

  | Tydec_struct f_list -> fprintf fmt "struct {%a }" (fprintf_list ~sep:" " pp_var_struct_type_field) f_list

  | Tydec_array (s, t) -> fprintf fmt "%a^%a" pp_var_type_dec_desc t Dimension.pp_dimension s

let pp_var_type_dec fmt ty =

  pp_var_type_dec_desc fmt ty.ty_dec_desc

  fprintf fmt "%s" (if !Options.kind2_print then kind2_protect id.var_id else id.var_id) 

  if !Options.print_dec_types then

    pp_var_type_dec fmt id.var_dec_type

  else

    Types.print_node_ty fmt id.var_type

let pp_var_clock fmt id = Clocks.print_ck_suffix fmt id.var_clock

  fprintf fmt "%s%s: %a"

    (if id.var_dec_const then "const " else "")

  fprintf_list ~sep:"; " pp_var fmt vars

  match q with

    | Exists -> fprintf fmt "exists %a" pp_vars vars 

  fprintf fmt "%a = %a;" pp_print_string label pp_const c

and pp_const fmt c = 

    | Const_int i -> pp_print_int fmt i

    | Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:" " pp_struct_const_field) fl

    (* used only for annotations *)

  match kwds with

  | [] -> assert false

  | _ -> fprintf fmt "/%a/" (fprintf_list ~sep:"/" pp_print_string) kwds

  if l = "true" then 

    fprintf fmt "%s" id

  else if l = "false" then

    fprintf fmt "not(%s)" id

  else

    fprintf fmt "(%s=%s)" l id

  (match expr.expr_annot with 

   | Some ann -> fprintf fmt "@[(%a %t)@]" pp_expr_annot ann)

      let pp fmt = 

         fprintf fmt "%s"

           (if !Options.kind2_print then kind2_protect id else id)

      | Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d

      | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d

      | Expr_tuple el -> fprintf fmt "(%a)" pp_tuple 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) -> fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2

      | Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2

      | Expr_pre e -> fprintf fmt "pre %a" pp_expr e

      | Expr_when (e, id, l) ->

         if !Options.kind2_print then

           fprintf fmt "%a when %a" pp_expr e pp_kind2_when (l, id)

      | Expr_merge (id, hl) -> 

         fprintf fmt "merge %s %a" id pp_handlers hl

      | Expr_appl (id, e, r) -> pp_app fmt id e r

      if false (* extra debug *)

      then

        Format.fprintf fmt "%t: %a" pp Types.print_ty expr.expr_type 

      else

        pp fmt

and pp_handler fmt (t, h) =

and pp_handlers fmt hl =

and pp_app fmt id e r =

       not (List.mem id Basic_library.internal_funs) then

    (* We only translate calls to nodes in kind2. The other may be

      let rec un_when_ed_expr e =

        match e.expr_desc with

          Expr_when (e,i,l) -> (Some (i,l)), e

        | Expr_tuple el -> (

          let un_when_ed_el = List.map un_when_ed_expr el in

          if List.length un_when_ed_el < 1 then

            assert false; (* tuple should have at least one element*)

          let init_when =

            fst (List.hd un_when_ed_el)

          in

          let common_when =

            List.fold_left (fun accu (new_opt,_) ->

                match accu, new_opt with

                | Some c1, Some c2 ->

                   if c1 = c2 then

                     Some c1

                   else

                     assert false  (* should not be clocked *)

                | None, None -> None

                | _ -> assert false (* If this is not even, there

                                       should be a clocking problem*)

              ) init_when (List.tl un_when_ed_el)

          in

          match common_when with

          | None -> None, e

          | Some _ -> common_when, { e with expr_desc =

                                              Expr_tuple (List.map snd un_when_ed_el) } 

        )

        | _ -> None, e

      in

      let when_expr, unwhen_ed_e = un_when_ed_expr e in

      match r, when_expr with

      | None, None -> pp_call fmt id e

      | None, Some w ->

         fprintf fmt "(activate %s every (%a)) (%a)"

           id

           pp_kind2_when w

           pp_expr e

      | Some r, None ->

         fprintf fmt "(restart %s every (%a)) (%a)"

           id

           pp_expr r

           pp_expr e

      | Some r, Some w ->

         fprintf fmt "(activate %s every (%a) restart every (%a)) (%a)"

           id

           pp_kind2_when w

           pp_expr r

           pp_expr e

    )

    match r with

    | None -> pp_call fmt id e

    | Some c ->

       fprintf fmt "%t every (%a)" (fun fmt -> pp_call fmt id e) pp_expr c 

  )

  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

  | "impl", 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

and pp_eexpr fmt e =

  fprintf fmt "%a%t %a"

    (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers

    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")

    pp_expr e.eexpr_qfexpr

    (* (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers *)

    (* (fun fmt -> match e.eexpr_quantifiers *)

    (*             with [] -> () *)

    (*                | _ -> fprintf fmt ";") *)

    pp_expr e.eexpr_qfexpr

and pp_s_function fmt expr_ann =

  let pp_annot fmt (kwds, ee) =

                  | [] -> assert false

                  | [x] -> pp_print_string fmt x

                  | _ -> fprintf fmt "%a" (fprintf_list ~sep:"/" pp_print_string) kwds)

      pp_sf_value ee

  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots

and pp_expr_annot fmt expr_ann =

  let pp_annot fmt (kwds, ee) =

  in

  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots

let pp_asserts fmt asserts =

  match asserts with 

  | _::_ -> (

    fprintf fmt "(* Asserts definitions *)@ ";

    fprintf_list ~sep:"@ " (fun fmt assert_ -> 

      let expr = assert_.assert_expr in

      fprintf fmt "assert %a;" pp_expr expr 

    ) fmt asserts 

  )

  | _ -> ()

let pp_node_var fmt id = fprintf fmt "%s%s: %a(%a)%a" (if id.var_dec_const then "const " else "") id.var_id print_dec_ty id.var_dec_type.ty_dec_desc Types.print_ty id.var_type Clocks.print_ck_suffix id.var_clock

*)

let pp_node_var fmt id =

  begin

      (if id.var_dec_const then "const " else "")

      pp_var_clock id;

    | None -> () 

    | Some v -> fprintf fmt " = %a" pp_expr v

  end 

  fprintf fmt "%a = %a;" 

    pp_eq_lhs eq.eq_lhs

    pp_expr eq.eq_rhs

let pp_unless fmt (_, expr, restart, st) =

    pp_restart restart

    st

let pp_until fmt (_, expr, restart, st) =

    pp_restart restart

    st

let rec pp_handler fmt handler =

    (fun fmt -> if not ([] = handler.hand_unless) then fprintf fmt "@ ")

      match locals with [] -> () | _ ->

    handler.hand_locals

and pp_node_stmt fmt stmt =

  match stmt with

  | Eq eq -> pp_node_eq fmt eq

  | Aut aut -> pp_node_aut fmt aut

and pp_node_stmts fmt stmts = fprintf_list ~sep:"@ " pp_node_stmt fmt stmts

and pp_node_aut fmt aut =

    (Utils.fprintf_list ~sep:"@ " pp_handler) aut.aut_handlers

and pp_node_eqs fmt eqs = fprintf_list ~sep:"@ " pp_node_eq fmt eqs

let pp_typedec fmt ty =

(* let rec pp_var_type fmt ty =  *)

(*   fprintf fmt "%a" (match ty.tdesc with  *)

(*     | Tvar | Tarrow | Tlink | Tunivar -> assert false *)

(*     | Tint -> pp_print_string fmt "int" *)

(*     | Treal -> pp_print_string fmt "real" *)

(*     | Tbool -> pp_print_string fmt "bool" *)

(*     | Trat -> pp_print_string fmt "rat" *)

(*     | Tclock -> pp_print_string fmt "clock"  *)

(*     | Ttuple tel -> fprintf_list ~sep:" * " pp_var_type fmt tel *)

(*   ) *)

 *   match q with

 *     | Forall -> fprintf fmt "forall %a" pp_vars vars 

 *     | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars  *)

    (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers

    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")

    pp_expr e.eexpr_qfexpr

let pp_spec_eq fmt eq = 

  fprintf fmt "var %a : %a = %a;" 

    pp_eq_lhs eq.eq_lhs

    Types.print_node_ty eq.eq_rhs.expr_type

    pp_expr eq.eq_rhs

let pp_spec_stmt fmt stmt =

  match stmt with

  | Eq eq -> pp_spec_eq fmt eq

  | Aut aut -> assert false (* Not supported yet *)

     variables. We adapt the call to produce the appropriate output. *)

    ) fmt spec.consts;

  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt s -> pp_spec_stmt fmt s) fmt spec.stmts;

  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "assume %a;" pp_eexpr r) fmt spec.assume;

      (fprintf_list ~eol:"" ~sep:"@ " (fun fmt r -> fprintf fmt "ensure %a;" pp_eexpr r)) mode.ensure

      import.import_nodeid

      pp_expr import.outputs

let node_as_contract nd =

  | None | Some (NodeSpec _) -> raise (Invalid_argument "Not a contract")

  | Some (Contract c) -> (

       consts, an unprocessed one could. So we conservatively merge

       elements, to enable printing unprocessed contracts *)

    let consts, locals = List.partition(fun v -> v.var_dec_const) nd.node_locals in

      locals = locals @ c.locals;

      stmts = nd.node_stmts @ c.stmts;

  )

(* Printing top contract as comments in regular output and as contract

   in kind2 *)

  fprintf fmt "@[<v 2>%scontract %s(%a) returns (%a);@ "

    (if !Options.kind2_print then "" else "(*@")

    pp_node_args nd.node_outputs;

  fprintf fmt "@[<v 2>let@ ";

  (if !Options.kind2_print then "" else "*)")

  match spec with

  | Contract c -> (* should have been processed by now *)

     fprintf fmt "@]*)@ "

  | NodeSpec name -> (* Pushing stmts in contract. We update the

                      original information with the computed one in

                      nd. *)

     let pp_l = fprintf_list ~sep:"," pp_var_name in

       pp_l inl

       pp_l outl

  fprintf fmt "%s" (if nd.node_dec_stateless then "function" else "node")

  fprintf fmt "@[<v 0>";

  (* Prototype *)

    pp_node_vs_function nd

    pp_node_args nd.node_inputs

    pp_node_args nd.node_outputs;

  (* Contracts *)

  fprintf fmt "%a" (fun fmt locals ->

      match locals with [] -> () | _ ->

                                    fprintf fmt "@[<v 4>var %a@]@ " 

                                      (fprintf_list ~sep:"@ " 

	                                 (fun fmt v -> fprintf fmt "%a;" pp_node_var v))

                                      locals

    ) nd.node_locals;

  (* Checks *)

  fprintf fmt "%a"

    (fun fmt checks ->

      match checks with [] -> () | _ ->

                                    fprintf fmt "@[<v 4>check@ %a@]@ " 

                                      (fprintf_list ~sep:"@ " 

	                                 (fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))

                                      checks

    ) nd.node_checks;

  (* Body *)

  fprintf fmt "let@[<h 2>   @ @[<v>";

  (* Annotations *)

  fprintf fmt "%a@ " (fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot;

  (* Statements *)

  fprintf fmt "%a@ " pp_node_stmts nd.node_stmts;

  (* Asserts *)    

  fprintf fmt "%a" pp_asserts nd.node_asserts;

  (* closing boxes body (2)  and node (1) *) 

  fprintf fmt "@]@]@ tel@]@ "

  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 -> pp_contract fmt nd 

  | _ -> assert false

  (* Prototype *)

  fprintf fmt  "%s @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "

    pp_node_args ind.nodei_inputs

  (* Contracts *)

  fprintf fmt "%a%t"

  fprintf fmt "@]@ "

  fprintf fmt "%s = %a;" cdecl.const_id pp_const cdecl.const_value

let pp_const_decl_list fmt clist = 

  fprintf_list ~sep:"@ " pp_const_decl fmt clist

  match decl.top_decl_desc with

     fprintf fmt "(* imported %a; *)" pp_imported_node ind

  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s

     introduces a cyclic dependance *)

  let open_decl, prog =

    List.partition (fun decl -> match decl.top_decl_desc with Open _ -> true | _ -> false) prog

  in

  let type_decl, prog =

  in

  match decl.top_decl_desc with

                 pp_node_vs_function nd

                 nd.node_id

  | TypeDef tdef -> fprintf fmt "type %s;@ " tdef.tydef_id

let pp_prog_short = pp_prog pp_short_decl

let pp_prog = pp_prog pp_decl

  match decl.top_decl_desc with

  | Const c -> fprintf fmt "const %a@ " pp_const_decl c

  | TypeDef tdef -> fprintf fmt "%a@ " pp_typedef tdef

  | Node _ -> assert false

  fprintf fmt "(* Generated Lustre Interface file from %s.lus *)@ " basename;

  fprintf fmt "(* by Lustre-C compiler version %s, %a *)@ " Version.number pp_date (Unix.gmtime (Unix.time ()));

  fprintf fmt "(* Feel free to mask some of the definitions by removing them from this file. *)@ @ ";

  List.iter (fprintf fmt "%a@ " pp_lusi) prog;

let pp_offset fmt offset =

  match offset with

  | Index i -> fprintf fmt "[%a]" Dimension.pp_dimension i

  | Field f -> fprintf fmt ".%s" f