CristalCaveGem » LustreC

  List.fold_left 

    (fun env (op, op_type) -> TE.add_value env op op_type)

    TE.initial

    [

       "+", (static_op type_bin_poly_op);

      "uminus", (static_op type_unary_poly_op); 

      "-", (static_op type_bin_poly_op); 

      "*", (static_op type_bin_poly_op);

      "/", (static_op type_bin_poly_op);

      "mod", (static_op type_bin_int_op);

      "&&", (static_op type_bin_bool_op);

      "||", (static_op type_bin_bool_op);

      "xor", (static_op type_bin_bool_op);

      "impl", (static_op type_bin_bool_op);

      "<", (static_op type_bin_comp_op);

      "<=", (static_op type_bin_comp_op);

      ">", (static_op type_bin_comp_op);

      ">=", (static_op type_bin_comp_op);

      "!=", (static_op type_bin_comp_op);

      "=", (static_op type_bin_comp_op);

      "not", (static_op type_unary_bool_op)

]

  let defs = [ 

    "uminus", (function [Dint a] -> Dint (-a)           | _ -> assert false);

    "not", (function [Dbool b] -> Dbool (not b)         | _ -> assert false);

    "+", (function [Dint a; Dint b] -> Dint (a+b)       | _ -> assert false);

    "-", (function [Dint a; Dint b] -> Dint (a-b)       | _ -> assert false);

    "*", (function [Dint a; Dint b] -> Dint (a*b)       | _ -> assert false);

    "/", (function [Dint a; Dint b] -> Dint (a/b)       | _ -> assert false);

    "mod", (function [Dint a; Dint b] -> Dint (a mod b) | _ -> assert false);

    "&&", (function [Dbool a; Dbool b] -> Dbool (a&&b)  | _ -> assert false);

    "||", (function [Dbool a; Dbool b] -> Dbool (a||b)  | _ -> assert false);

    "xor", (function [Dbool a; Dbool b] -> Dbool (a<>b) | _ -> assert false);

    "impl", (function [Dbool a; Dbool b] -> Dbool (a<=b)| _ -> assert false);

    "<", (function [Dint a; Dint b] -> Dbool (a<b)      | _ -> assert false);

    ">", (function [Dint a; Dint b] -> Dbool (a>b)      | _ -> assert false);

    "<=", (function [Dint a; Dint b] -> Dbool (a<=b)    | _ -> assert false);

    ">=", (function [Dint a; Dint b] -> Dbool (a>=b)    | _ -> assert false);

    "!=", (function [a; b] -> Dbool (a<>b)              | _ -> assert false);

    "=", (function [a; b] -> Dbool (a=b)                | _ -> assert false);

  ]

  in

  List.fold_left 

    (fun env (op, op_eval) -> VE.add_value env op op_eval)

    VE.initial

    defs

(* Removed because of "open" constructs. No more extern functions *)

(*

      *)

let print_prototype fmt decl =

  match decl.top_decl_desc with

  | Open m -> fprintf fmt "#include \"%s.h\"@," m

  | _ -> () (* We don't do anything here *)

let print_makefile basename nodename fmt =

  fprintf fmt "GCC=gcc@.";

  fprintf fmt "INC=/usr/local/include/lustrec@.";

  fprintf fmt "@.";

  fprintf fmt "main:@.";

  fprintf fmt "\t${GCC} -I${INC} -I. -c %s.c@." basename;    

  fprintf fmt "\t${GCC} -I${INC} -c ${INC}/io_frontend.c@.";    

  fprintf fmt "\t${GCC} -I${INC} -c ${INC}/StdLibrary.c@.";

  fprintf fmt "\t${GCC} -o %s_%s io_frontend.o StdLibrary.o -lm %s.o@." basename nodename basename

let translate_to_c header_fmt source_fmt makefile_fmt spec_fmt_opt basename prog machines =

  let main_include, main_print, main_makefile =

      | "" -> (fun _ -> ()), (fun _ -> ()), (fun _ -> ())

	| None -> eprintf "Unable to find a main node named %s@.@?" main_node; (fun _ -> ()), (fun _ -> ()), (fun _ -> ())

	| Some m -> print_main_header, print_main_fun machines m, print_makefile basename !Options.main_node

  main_print source_fmt;

  (* Generating Makefile *)

  main_makefile makefile_fmt    

  | Open _ ->

  List.fold_left (fun e decl -> clock_top_decl e decl) env decls

let check_env_compat declared computed =

  Env.iter declared (fun k decl_clock_k -> 

    let computed_c = Env.lookup_value computed k in

    try_unify decl_clock_k computed_c Location.dummy_loc

  ) 

  | Open of string

	| Node _ | ImportedNode _ | ImportedFun _ | Open _ -> consts  

	| Consts _ | ImportedNode _ | ImportedFun _ | Open _ -> nodes  

  | Consts _ | Open _ -> ()

    Utils.reset_names ();

    fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock

  | ImportedFun _ | Consts _ | Open _ -> ()

  | Open of string

let iter env f = IMap.iter f env

  "open", OPEN;

let type_decls env decls =  

  report ~level:1 (fun fmt -> fprintf fmt ".. typing@,@?");

  let new_env = 

    begin

      try

	Typing.type_prog env decls

    (*Typing.uneval_prog_generics prog*)

      with (Types.Error (loc,err)) as exc ->

	Format.eprintf "Typing error at loc %a: %a@]@."

	  Location.pp_loc loc

	  Types.pp_error err;

	raise exc

    end 

  in

  if !Options.print_types then

    report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,@?" Corelang.pp_prog_type decls);

  new_env

let clock_decls env decls = 

  report ~level:1 (fun fmt -> fprintf fmt ".. clock calculus@,@?");

  let new_env =

    begin

      try

	Clock_calculus.clock_prog env decls

      with (Clocks.Error (loc,err)) as exc ->

	Location.print loc;

	eprintf "Clock calculus error at loc %a: %a@]@." Location.pp_loc loc Clocks.pp_error err;

	raise exc

    end

  in

  if !Options.print_clocks then

    report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,@?" Corelang.pp_prog_clock decls);

  new_env

(* Loading Lusi file and filing type tables with parsed

   functions/nodes *)

let load_lusi filename =

  Location.input_name := filename;

  let lexbuf = Lexing.from_channel (open_in filename) in

  Location.init lexbuf filename;

  (* Parsing *)

  report ~level:1 (fun fmt -> fprintf fmt "@[<v>.. parsing header file %s@,@?" filename);

  let header = 

    try

      Parse.prog Parser_lustre.header Lexer_lustre.token lexbuf

    with (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc -> 

      Parse.report_error err;

      raise exc

  in

  let new_tenv = type_decls Basic_library.type_env header in   (* Typing *)

  let new_cenv: Clocks.clock_expr Utils.IMap.t = clock_decls Basic_library.clock_env header in   (* Clock calculus *)

  header, new_tenv, new_cenv

  (* Loading the input file *)

  report ~level:1 

    (fun fmt -> fprintf fmt "@[<v>.. parsing file %s@,@?" source_name);

  (* Extracting dependencies *)

  report ~level:1 (fun fmt -> fprintf fmt ".. extracting dependencies@,@?");

  let dependencies = 

      (fun d accu -> match d.Corelang.top_decl_desc with 

      | Corelang.Open s -> s::accu 

      | _ -> accu) 

  let type_env, clock_env =

    List.fold_left (fun (type_env, clock_env) s -> 

      try

	let basename = s ^ ".lusi" in 

	report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>Library %s@ " s);

	let _, lusi_type_env, lusi_clock_env = load_lusi basename in 

	report ~level:1 (fun fmt -> fprintf fmt "@]@,@?");

	Env.overwrite type_env lusi_type_env,

	Env.overwrite clock_env lusi_clock_env      

      with Sys_error msg -> (

	Format.eprintf "Failure: impossible to load library %s.@.%s@." s msg;

	exit 1

      )

    )  (Basic_library.type_env, Basic_library.clock_env) dependencies

  in

  let computed_types_env = type_decls type_env prog in

  let computed_clocks_env = clock_decls clock_env prog in

  (*

    if(!Options.delay_calculus)

    then

    report ~level:1 (fun fmt -> fprintf fmt ".. initialisation analysis@?");

    try

    Delay_calculus.delay_prog Basic_library.delay_env prog

    with (Delay.Error (loc,err)) as exc ->

    Location.print loc;

    eprintf "%a" Delay.pp_error err;

    Utils.track_exception ();

    raise exc

  *)

    (* Causality analysis *)

  (* Checking the existence of a lusi (Lustre Interface file) *)

  let lusi_name = basename ^ ".lusi" in

  let _ = 

    try 

      let _ = open_in lusi_name in

      let _, declared_types_env, declared_clocks_env = load_lusi lusi_name in

      (* checking type compatibilty with computed types*)

      Typing.check_env_compat declared_types_env computed_types_env;

      (* checking clocks compatibilty with computed clocks*)

      Clock_calculus.check_env_compat declared_clocks_env computed_clocks_env;

    with Sys_error _ -> ( 

      (* Printing lusi file is necessary *)

      report ~level:1 

	(fun fmt -> 

	  fprintf fmt 

	    ".. generating lustre interface file %s@,@?" lusi_name);

      let lusi_out = open_out lusi_name in

      let lusi_fmt = formatter_of_out_channel lusi_out in

      Printers.pp_lusi_header lusi_fmt source_name normalized_prog

    )

    | (Types.Error (loc,err)) as exc ->

      Format.eprintf "Type mismatch between computed type and declared type in lustre interface file: %a@]@."

	Types.pp_error err;

      raise exc

  in

      report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);

      let source_out = open_out source_file in

      let source_fmt = formatter_of_out_channel source_out in

      report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");

      Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)

    let makefile_file = basename ^ ".makefile" in (* Could be changed *)

    let makefile_out = open_out makefile_file in

    let makefile_fmt = formatter_of_out_channel makefile_out in

    C_backend.translate_to_c header_fmt source_fmt makefile_fmt spec_fmt_opt basename normalized_prog machine_code;

  | Open _ | ImportedNode _ | ImportedFun _ | Consts _ -> decl

%token STATELESS ASSERT OPEN QUOTE FUNCTION

%start header

%type <Corelang.top_decl list> header

header:

    typ_def_list top_decl_header_list EOF {$1;(List.rev $2)}

top_decl_header_list:

  top_decl_header {[$1]}

| top_decl_header_list top_decl_header {$2::$1}

top_decl_header:

| NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR stateless_opt SCOL

                            {nodei_id = $2;

                             nodei_inputs = List.rev $4;

			     nodei_stateless = $12;

    Hashtbl.add node_table $2 nd; nd}

| nodespec_list NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR stateless_opt SCOL

                            {nodei_id = $3;

                             nodei_inputs = List.rev $5;

			     nodei_stateless = $13;

    Hashtbl.add node_table $3 nd; nd}

| FUNCTION IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL

                             nodei_outputs = List.rev $9;

| nodespec_list FUNCTION IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL

                             nodei_outputs = List.rev $10;

top_decl:

| CONST cdecl_list { mktop_decl (Consts (List.rev $2)) }

| NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL 

    {let eqs, asserts, annots = $15 in

     let nd = mktop_decl (Node

                            {node_id = $2;

                             node_type = Types.new_var ();

                             node_clock = Clocks.new_var true;

                             node_inputs = List.rev $4;

                             node_outputs = List.rev $9;

                             node_locals = List.rev $13;

			     node_gencalls = [];

			     node_checks = [];

			     node_asserts = asserts; 

                             node_eqs = eqs;

			     node_spec = None;

			     node_annot = match annots with [] -> None | _ -> Some annots})

    in

    Hashtbl.add node_table $2 nd; nd}

| nodespec_list NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL 

    {let eqs, asserts, annots = $16 in

     let nd = mktop_decl (Node

                            {node_id = $3;

                             node_type = Types.new_var ();

                             node_clock = Clocks.new_var true;

                             node_inputs = List.rev $5;

                             node_outputs = List.rev $10;

                             node_locals = List.rev $14;

			     node_gencalls = [];

			     node_checks = [];

			     node_asserts = asserts; 

                             node_eqs = eqs;

			     node_spec = Some $1;

			     node_annot = match annots with [] -> None | _ -> Some annots})

    in

    Hashtbl.add node_table $3 nd; nd}

| OPEN QUOTE IDENT QUOTE { mktop_decl (Open $3) }

  | Open s -> fprintf fmt "open \"%s\"" s

  | Open s -> fprintf fmt "open \"%s\"" s

let pp_lusi fmt decl = 

  match decl.top_decl_desc with

  | Node nd ->  

    fprintf fmt 

      "@[<v>node %s (%a) returns (%a);@ @]@ "

      nd.node_id

      pp_node_args nd.node_inputs

      pp_node_args nd.node_outputs

  | ImportedNode _ | ImportedFun _ | Consts _ | Open _ -> ()

let pp_lusi_header fmt filename prog =

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

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

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

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

    (* application of non internal function is not legal in a constant

       expression *)

    | Some (x, l) -> 

      check_constant expr.expr_loc const false;

      let expr_x = expr_of_ident x expr.expr_loc in	

      let typ_l = 

	Type_predef.type_clock 

	  (type_const expr.expr_loc (Const_tag l)) in

      type_subtyping_arg env in_main ~sub:false const expr_x typ_l);

  | Open _  -> env

  List.fold_left type_top_decl env decls

  | Open _  -> ()

let check_env_compat declared computed =

  Env.iter declared (fun k decl_type_k -> 

    let computed_t = Env.lookup_value computed k in

    try_unify decl_type_k computed_t Location.dummy_loc

  ) 

let pp_date fmt tm =

  Format.fprintf fmt "%i/%i/%i, %i:%i:%i"

    (tm.Unix.tm_year + 1900)

    tm.Unix.tm_mon

    tm.Unix.tm_mday

    tm.Unix.tm_hour

    tm.Unix.tm_min

    tm.Unix.tm_sec

LUSTREC="../../_build/src/lustrec"

	$LUSTREC -d build -verbose 0 $opts -node $main ../$file;

	$LUSTREC -d build -verbose 0 $opts ../$file