CristalCaveGem » LustreC

(* Loading Lus/Lusi file and filling type tables with parsed

let parse filename extension =

  let f_in = open_in filename in

  let lexbuf = Lexing.from_channel f_in in

  let prog = 

      match extension with

        ".lusi" ->

        Log.report ~level:1

          (fun fmt -> fprintf fmt ".. parsing header file %s@ " filename);

        Parse.header Parser_lustre.header Lexer_lustre.token lexbuf 

      | ".lus" ->

         Log.report ~level:1 

           (fun fmt -> fprintf fmt ".. parsing source file %s@ " filename);

         Parse.prog Parser_lustre.prog Lexer_lustre.token lexbuf

      | _ -> assert false

       Parse.report_error err;

       raise exc

        Error.pp_error_msg err

        Location.pp_loc loc;

  in

  close_in f_in;

  prog

  let lusic_ext = ".lusic" in

    if (* Generating the lusic file *)

      extension = ".lusi" (* because input is a lusi *)

      || (extension = ".lus" &&

            not (Sys.file_exists header_name))

           (* or because it is a lus but not lusic exists *)

      || (let lusic = Lusic.read_lusic destname lusic_ext in

          not lusic.Lusic.from_lusi)

         (* or the lusic exists but is not generated from a lusi, hence it

            has te be regenerated *)

    then

	Lusic.write_lusic

          (extension = ".lusi") (* is it a lusi file ? *)

          (if extension = ".lusi" then prog else Lusic.extract_header dirname basename prog)

          destname

          lusic_ext;

        let _ =

          match !Options.output with

          | "C" -> C_backend_lusic.print_lusic_to_h destname lusic_ext

          | _ -> ()

        in

        ()

      end

    else (* Lusic exists and is usable. Checking compatibility *)

      begin

	Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);

        let lusic = Lusic.read_lusic destname lusic_ext in

        Lusic.check_obsolete lusic destname;

	let header = lusic.Lusic.contents in

	let (declared_types_env, declared_clocks_env) = Modules.get_envs_from_top_decls header in

	check_compatibility

	  (prog, computed_types_env, computed_clocks_env)

	  (header, declared_types_env, declared_clocks_env)

let stage1 params prog dirname basename extension =

  let prog, dependencies, (typ_env, clk_env) = Modules.load ~is_header:(extension = ".lusi") prog in

  (* If compiling a lusi, generate the lusic. If this is a lus file, Check the existence of a lusi (Lustre Interface file) *)

  compile_source_to_header

    prog !Global.type_env !Global.clock_env dirname basename extension;

let stage3 prog machine_code dependencies basename extension =

  match !Options.output, extension with

    "C", ".lus" -> 

     begin

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

       C_backend.translate_to_c

	 (* alloc_header_file source_lib_file source_main_file makefile_file *)

	 basename prog machine_code dependencies

     end

  |  "C", _ -> 

      	Log.report ~level:1 (fun fmt -> fprintf fmt ".. no C code generation for lusi@,");

  | "java", _ ->

  | "horn", _ ->

  | "lustre", _ ->

       let source_file = destname ^ ".lustrec" ^ extension  in (* Could be changed *)

       Log.report ~level:1 (fun fmt -> fprintf fmt ".. exporting processed file as %s@," source_file);

  | "emf", _ ->

let rec compile dirname basename extension =

  let prog = parse source_name extension in

    if !Options.mpfr &&

         extension = ".lus" (* trying to avoid the injection of the module for lusi files *) 

    then

      Compiler_stages.stage1 params prog dirname basename extension

  Compiler_stages.stage3 prog machine_code dependencies basename extension;

  | ".lusi"  

  | ".lus"   -> compile dirname basename extension

  let prog = parse source_name extension in

  let prog, dependencies = Compiler_stages.stage1 params prog dirname basename extension in

  let prog = parse source_name extension in

      Compiler_stages.stage1 params prog dirname basename extension

         if Filename.check_suffix basename ".lus" then

           let include_src = Compiler_common.parse basename ".lus" in

           load_rec ~is_header:false accu include_src

         else

           raise (Error (decl.top_decl_loc, LoadError("include requires a lustre file")))

  eprintf "Syntax error: %a@.%a@."

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 *)

    fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt v ->

    fprintf fmt "const %a = %t;"

      (fun fmt -> match v.var_dec_value with None -> assert false | Some e -> pp_expr fmt e)

    ) 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 "guarantees %a;" pp_eexpr r) fmt spec.guarantees;

  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt mode ->

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

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

  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt import ->

  ) fmt spec.imports

let pp_spec_as_comment fmt spec =

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

  pp_spec fmt spec;

  fprintf fmt "@]*)@ "

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

  fprintf fmt "@[<v 0>";

  (* Prototype *)

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

    pp_node_args ind.nodei_outputs;

  (* Contracts *)

  fprintf fmt "%a%t"

    (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt s | _ -> ()) ind.nodei_spec

    (fun fmt -> match ind.nodei_spec with None -> () | Some _ -> fprintf fmt "@ ");

  fprintf fmt "@]@ "

     let prog, deps = Compiler_stages.stage1 params prog "" "" ".lus" in

(* TODO general remark: expect in the add_vdelc, it seems to me that

   all the pairs (env, vd_env) should be replace with just env, since

   vd_env is never used and the env element is always extract with a

   fst *)

    let type_spec env spec =

      let vd_env = spec.consts @ spec.locals in

      check_vd_env vd_env;

      let env = type_var_decl_list ((* this argument seems useless to me, cf TODO at top of the file*) vd_env) env vd_env in

      (* typing stmts *)

      let eqs = List.map (fun s -> match s with Eq eq -> eq | _ -> assert false) spec.stmts  in

      let undefined_vars_init =

        List.fold_left

          (fun uvs v -> ISet.add v.var_id uvs)

          ISet.empty spec.locals

      in

      let _ =

        List.fold_left

          (type_eq (env, vd_env) (false (*is_main*)))

          undefined_vars_init

          eqs

      in

      (match nd.node_spec with None -> () | Some spec -> ignore (type_spec new_env spec));

      let delta_env = type_var_decl_list vd_env env nd.nodei_inputs in

      let delta_env = type_var_decl_list vd_env delta_env nd.nodei_outputs in

      let new_env = Env.overwrite env delta_env in

      (* Typing spec *)

      (match nd.nodei_spec with None -> () | Some spec -> ignore (type_spec new_env spec)); 

let fprintf_list ?(eol:('a, formatter, unit) Pervasives.format = "") ~sep:sep f fmt l =

  let rec aux fmt = function

  | x::r -> Format.fprintf fmt "%a%(%)%a" f x sep aux r

  in

  match l with

  | [] -> ()

  | _ -> (

    aux fmt l;

    Format.fprintf fmt "%(%)" eol

  )