Revision 518951ed
Added by Pierre-Loïc Garoche over 5 years ago
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
Seal export lustre