Project

General

Profile

« Previous | Next » 

Revision 518951ed

Added by Pierre-Loïc Garoche over 2 years ago

Seal export lustre

View differences:

src/tools/seal/seal_verifier.ml
3 3
open Seal_utils
4 4

  
5 5
let active = ref false
6
let seal_export = ref None
6 7

  
8
let set_export s = match s with
9
  | "lustre" | "lus" | "m" | "matlab" -> seal_export := Some s
10
  | _ -> (Format.eprintf "Unrecognized seal export: %s@.@?" s; exit 1)
7 11
(* TODO
8 12

  
9 13
   - build the output function: for the moment we slice the node with
......
97 101
      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@ "
98 102
        pp_res  sw_sys
99 103
    );
100
  let new_node = Seal_export.to_lustre m sw_init sw_sys init_out update_out in  
101
  Format.eprintf "%a@." Printers.pp_node new_node;
102
  let output_file = !Options.dest_dir ^ "/" ^ basename ^ "_seal.lus" in
103
  Format.eprintf "%s@." output_file;
104
  let new_top = Corelang.mktop_decl Location.dummy_loc output_file false (Node new_node) in
105

  
106
  let out = open_out output_file in
107
  let fmt = Format.formatter_of_out_channel out in
108
  Format.fprintf fmt "%a@." 
109
    Printers.pp_prog  (prog@[new_top]);
104
  let _ = match !seal_export with
105
    | Some "lustre" | Some "lus" ->
106
       Seal_export.to_lustre basename prog m sw_init sw_sys init_out update_out  
107
    | Some "matlab" | Some "m" -> assert false (* TODO *)
108
    | Some _ -> assert false 
109
    | None -> ()
110
  in
110 111
  ()
111 112
  
112 113
module Verifier =
113 114
  (struct
114 115
    include VerifierType.Default
115 116
    let name = "seal"
116
    let options = []
117
    let options = ["-export", Arg.String set_export, "seal export option (lustre, matlab)"]
117 118
    let activate () =
118 119
      active := true;
119 120
      Options.global_inline := true

Also available in: Unified diff