Commit 20d1eda3 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

whyml: let the whyml-exp format use the library .mlw files

parent e8b1ab5e
......@@ -23,6 +23,8 @@ open Util
open Mlw_module
open Mlw_typing
let debug = Debug.register_flag "whyml_print_modules"
let read_channel env path file c =
let lb = Lexing.from_channel c in
Loc.set_file file lb;
......@@ -33,11 +35,25 @@ let read_channel env path file c =
let mm, tm =
List.fold_left (add_theory_module env path) (Mstr.empty, Mstr.empty) ml
Mstr.iter (fun _ m ->
if Debug.test_flag debug then Mstr.iter (fun _ m ->
Format.fprintf Format.err_formatter
"@[<hov 2>module %a@\n%a@]@\nend@." Pretty.print_th m.mod_theory
(Pp.print_list Pp.newline2 Mlw_pretty.print_pdecl) m.mod_decls;
Format.pp_print_newline Format.err_formatter ()) mm;
mm, tm
(* TODO: remove this function once whyml becomes the default *)
let read_channel =
let one_time_hack = ref true in
fun env path file c ->
let env =
if !one_time_hack then begin
one_time_hack := false;
let genv = Env.env_of_library env in
Env.register_format "whyml-library" ["mlw"] read_channel genv
else env
read_channel env path file c
let library_of_env = Env.register_format "whyml-exp" ["mlx"] read_channel
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment