CristalCaveGem » LustreC

let load_file f =

  let ic = open_in f in

  let n = in_channel_length ic in

  let s = String.create n in

  really_input ic s 0 n;

  close_in ic;

  (s)

let print_dep fmt prog =

  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. extracting Horn libraries@,");

  fprintf fmt "; Statically linked libraries@";

  let dependencies = Corelang.get_dependencies prog in

  List.iter

    (fun dep ->

      let (local, s) = Corelang.dependency_of_top dep in

      let basename = ((if local then !Options.dest_dir else !Options.include_dir)) ^ s ^ ".smt2" in

      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@[<v 0> Horn Library %s@," basename);

      let horn = load_file basename in

      fprintf fmt "@.%s@." horn;

    )

    dependencies

let check_sfunction mannot =

 (*Check if its an sfunction*)

  match mannot with

    [] -> false

  | [x] ->

     begin

       match x.annots with

         [] -> false

        |[(key,va)] ->

          begin

            match key with

              [] -> false

            | [x]  -> x == "c_code" || x =="matlab"

            | _ -> false

          end

        |(_,_)::_ -> false

     end

  | _::_ -> false

let translate fmt basename prog machines=

  print_dep fmt prog; (*print static library e.g. math*)

  (*List.iter (print_machine machines fmt) (List.rev machines);*)

  List.iter(fun m ->

      let is_sfunction = check_sfunction m.mannot in

      if is_sfunction then(

        Log.report ~level:1 (fun fmt -> fprintf fmt ".. detected sfunction: %s@," m.mname.node_id);

        print_sfunction machines fmt m

      ) else (

         print_machine machines fmt m)

         )

           (List.rev machines);