CristalCaveGem » LustreC

                        'configure.ac'

                      ],

                      {

                        '_AM_MAKEFILE_INCLUDE' => 1,

                        'AM_PROG_F77_C_O' => 1,

                        'AM_GNU_GETTEXT_INTL_SUBDIR' => 1,

                        'LT_INIT' => 1,

                        'AC_CONFIG_FILES' => 1,

                        'AC_FC_FREEFORM' => 1,

                        'AC_CONFIG_LINKS' => 1,

                        'AC_FC_SRCEXT' => 1,

                        'AM_MAKEFILE_INCLUDE' => 1,

                        'AM_INIT_AUTOMAKE' => 1,

                        'AC_CANONICAL_SYSTEM' => 1,

                        'AH_OUTPUT' => 1,

                        'AC_CONFIG_AUX_DIR' => 1,

                      }

                    ], 'Autom4te::Request' )

           );

    )

    dependencies

let translate fmt basename prog machines=

  (* We print typedef *)

  print_type_definitions fmt;

  main_print machines fmt

(* Local Variables: *)

*)

let pp_assign m pp_var fmt var_name value =

  let self = m.mname.node_id in

    (pp_horn_val ~is_lhs:true self pp_var) var_name

    (pp_value_suffix self pp_var) value

(* In case of no reset call, we define mid_mem = current_mem *)

let pp_no_reset machines m fmt i =

  let (n,_) = List.assoc i m.minstances in

  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in

    rename_machine_list

      (concat m.mname.node_id i)

      (rename_mid_list (full_memory_vars machines target_machine))

    fprintf fmt "(= %a %a)"

      (pp_horn_var m) mhd

      (pp_horn_var m) chd

  | _ -> (

    fprintf fmt "@[<v 0>(and @[<v 0>";

      fprintf fmt "(= %a %a)@ "

      (pp_horn_var m) mhd

      (pp_horn_var m) chd

let pp_instance_reset machines m fmt i =

  let (n,_) = List.assoc i m.minstances in

  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in

  fprintf fmt "(%a @[<v 0>%a)@]"

    pp_machine_reset_name (node_name n)

    (

      (rename_machine_list

	 (concat m.mname.node_id i)

	 (rename_current_list (full_memory_vars machines target_machine))

      @

	(rename_machine_list

	   (concat m.mname.node_id i)

      if not (List.mem i reset_instances) then

	(* If not, declare mem_m = mem_c *)

	pp_no_reset machines m fmt i;

      let mems = full_memory_vars machines target_machine in

      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in

      let mid_mems = rename_mems rename_mid_list in

	fprintf fmt "@[<v 5>(and ";

	fprintf fmt "(= %a (ite %a %a %a))"

	  (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *)

	  (pp_horn_val self (pp_horn_var m)) i1

	  (pp_horn_val self (pp_horn_var m)) i2

	;

	  (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)

	  (Utils.pp_final_char_if_non_empty "@ " outputs)

	  (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems)

      end

    end

  with Not_found -> ( (* stateless node instance *)

      (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))

      (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)

  )

(* Print the instruction and update the set of reset instances *)

let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list =

  match instr with

       statement. *)

    let self = m.mname.node_id in

    let pp_branch fmt (tag, instrs) =

	(*"@[<v 3>(=> (= %a %s)@ "*)  (* Issues with some versions of Z3. It

					  seems that => within Horn predicate

					  may cause trouble. I have hard time

      () (* rs *)

    in

    pp_conj pp_branch fmt hl;

  let ppi rs fmt i = pp_machine_instr machines rs m fmt i in

  match instrs with

  | _::_ ->

    fprintf fmt "(and @[<v 0>";

      let rs = ppi rs fmt i in

      fprintf fmt "@ ";

      rs

    )

    in

    fprintf fmt "@])";

    rs

  fprintf fmt "@[<v 5>(and @ ";

  (* print "x_m = x_c" for each local memory *)

    fprintf fmt "(= %a %a)"

      (pp_horn_var m) (rename_mid v)

      (pp_horn_var m) (rename_current v)

  *)

  (Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) ->

    let name = node_name n in

      fprintf fmt "(= %s._arrow._first_m true)"

    ) else (

	name

	(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))

    )

   )) fmt m.minstances;

  else

    begin

      fprintf fmt "; %s@." m.mname.node_id;

      (* Printing variables *)

      Utils.fprintf_list ~sep:"@." pp_decl_var fmt

	(

	  (* Rule for reset *)

	  fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."

	    pp_machine_reset_name m.mname.node_id

	    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m);

		pp_machine_step_name m.mname.node_id

		(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);

	    end

	    begin

	      let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in

	      (* print_string pp_val; *)

	      fprintf fmt "; with Assertions @.";

	      (*Rule for step*)

	      fprintf fmt "@[<v 2>(rule (=> @ (and @ ";

	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);

		pp_machine_step_name m.mname.node_id

		(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);

	    end

	end

    end

(* Local Variables: *)

(* compile-command:"make -C ../../.." *)

(* End: *)

  "assumes", ASSUMES;

  "exists", EXISTS;

  "forall", FORALL;

  ]

}

  "assert", ASSERT;

  "lib", LIB;

  "prototype", PROTOTYPE;

]

let include_path =

if (!include_dir != ".") then Version.prefix ^ !include_dir

else Version.include_path

let salsa_enabled = ref true

let set_mpfr prec =

  if prec > 0 then (

    mpfr := true;

  )

  else

    failwith "mpfr requires a positive integer"

let options =

[ "-d", Arg.Set_string dest_dir,

"uses the specified directory \x1b[4mdir\x1b[0m as root for generated/imported object and C files <default: .>";

    "-print_clocks", Arg.Set print_clocks, "prints node clocks";

    "-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";

    "-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>";

    "-version", Arg.Unit print_version, " displays the version";]

let plugin_opt (name, activate, options) =

  ( "-" ^ name , Arg.Unit activate, "activate plugin " ^ name ) ::

    (List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options)

let get_witness_dir filename =

  (* Make sure the directory exists *)

%token PRE ARROW

%token EOF

%token REQUIRES ENSURES OBSERVER

%token EXISTS FORALL

%nonassoc prec_exists prec_forall

| IDENT COL expr SCOL lustre_annot_list { ([$1],$3)::$5 }

| INVARIANT COL expr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }

| OBSERVER COL expr SCOL lustre_annot_list { (["observer"],$3)::$5 }

kwd:

DIV { [] }

%token MINUS PLUS UMINUS

%token PRE ARROW

%token REQUIRES ENSURES OBSERVER

%token EXISTS FORALL

%token PROTOTYPE LIB

%token EOF

| IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 }

| INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }

| OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 }

kwd:

DIV { [] }

let pp_quantifiers fmt (q, vars) =

  match q with

let rec pp_struct_const_field fmt (label, c) =

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

  match c with

    | Const_int i -> pp_print_int fmt i

    | Const_real (c, e, s) -> pp_print_string fmt s (*if e = 0 then pp_print_int fmt c else if e < 0 then Format.fprintf fmt "%ie%i" c (-e) else Format.fprintf fmt "%ie-%i" c e *)

let rec pp_expr fmt expr =

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

      match expr.expr_desc with

    | Expr_const c -> pp_const fmt c

    | Expr_ident id -> Format.fprintf fmt "%s" id

    | 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) -> fprintf fmt "%a when %s(%s)" pp_expr e l id

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

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

    )

and pp_app fmt id e r =

  match r with

  | None -> pp_call fmt id e

and pp_call fmt id e =

  match id, e.expr_desc with

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

    pp_expr e.eexpr_qfexpr

and pp_expr_annot fmt expr_ann =

  let pp_annot fmt (kwds, ee) =

      pp_eexpr ee

  in

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

(*

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

*)

  begin

    fprintf fmt "%s%s: %a%a" (if id.var_dec_const then "const " else "") id.var_id Types.print_node_ty id.var_type Clocks.print_ck_suffix id.var_clock;

    match id.var_dec_value with

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

    pp_eq_lhs eq.eq_lhs

    pp_expr eq.eq_rhs

    (Utils.fprintf_list ~sep:"@," pp_unless) handler.hand_unless

    (fun fmt locals ->

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

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

	  locals)

    handler.hand_locals

let rec pp_var_struct_type_field fmt (label, tdesc) =

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

and pp_var_type_dec_desc fmt tdesc =

  | Tydec_any -> fprintf fmt "<any>"

  | Tydec_int -> fprintf fmt "int"

  | Tydec_real -> fprintf fmt "real"

  fprintf fmt "@[<hov 2>(*@@ ";

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

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

      name

      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes

      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "ensures %a;" pp_eexpr r)) ensures

let pp_asserts fmt asserts =

  | _::_ -> (

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

    let expr = assert_.assert_expr in

  )

  | _ -> ()

fprintf fmt "@[<v 0>%a%t%s %s (%a) returns (%a)@.%a%alet@.@[<h 2>   @ @[<v>%a@ %a@ %a@]@ @]@.tel@]@."

  (fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec

  (fun fmt -> match nd.node_spec with None -> () | Some _ -> Format.fprintf fmt "@.")

  pp_node_args nd.node_outputs

  (fun fmt locals ->

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

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

      locals

  ) nd.node_locals

  (fun fmt checks ->

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

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

      checks

  ) nd.node_checks

  pp_asserts nd.node_asserts

(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)

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

    (if ind.nodei_stateless then "function" else "node")

    ind.nodei_id

let pp_const_decl fmt cdecl =

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

  fprintf_list ~sep:"@ " pp_const_decl fmt clist

let pp_decl fmt decl =

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

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

  fprintf_list ~sep:"@ " pp_decl fmt prog

let pp_short_decl fmt decl =

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

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

  match decl.top_decl_desc with

  | ImportedNode ind -> fprintf fmt "%a;@ " pp_imported_node ind

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

  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. *)@.@.";

let pp_offset fmt offset =

  match offset with