diff --git a/src/haz3lformatter/Formatter.re b/src/haz3lformatter/Formatter.re new file mode 100644 index 000000000..a60c4a693 --- /dev/null +++ b/src/haz3lformatter/Formatter.re @@ -0,0 +1,11 @@ +open Haz3lcore; +let format = (~inline: bool, s: string): string => { + let seg = + ExpToSegment.exp_to_segment( + ~settings=ExpToSegment.Settings.of_core(~inline, CoreSettings.on), + MakeTerm.from_zip_for_sem(Option.get(Printer.zipper_of_string(s))). + term, + ); + let zipper = Zipper.unzip(seg); + Printer.zipper_to_string(~holes=Some("?"), zipper); +}; diff --git a/src/haz3lformatter/FormatterMain.re b/src/haz3lformatter/FormatterMain.re new file mode 100644 index 000000000..726084b4e --- /dev/null +++ b/src/haz3lformatter/FormatterMain.re @@ -0,0 +1,3 @@ +open Haz3lformatter; + +print_endline(Formatter.format(~inline=false, In_channel.input_all(stdin))); diff --git a/test/Test_Formatter.re b/test/Test_Formatter.re new file mode 100644 index 000000000..86e697e3b --- /dev/null +++ b/test/Test_Formatter.re @@ -0,0 +1,27 @@ + +open Alcotest; +open Haz3lcore; +open Haz3lformatter; + +let parse_exp = (s: string) => + MakeTerm.from_zip_for_sem(Option.get(Printer.zipper_of_string(s))).term; +let serialize = (exp: Exp.t): string => { + let seg = + ExpToSegment.exp_to_segment( + ~settings=ExpToSegment.Settings.of_core(~inline=true, CoreSettings.on), + exp, + ); + let zipper = Zipper.unzip(seg); + Printer.zipper_to_string(~holes=Some("?"), zipper); +}; + +let tests = [ + test_case("Incomplete Function Definition", `Quick, () => { + check( + string, + "let = fun x -> in ", + "let ? = (fun x -> ?) in ?", + Formatter.format(~inline=true, "let = fun x -> in "), + ) + }), +]; diff --git a/test/haz3ltest.re b/test/haz3ltest.re index 9eed7a992..dea6b375e 100644 --- a/test/haz3ltest.re +++ b/test/haz3ltest.re @@ -10,6 +10,7 @@ let (suite, _) = ("Evaluator", Test_Evaluator.tests), ("MakeTerm", Test_MakeTerm.tests), ("ExpToSegment", Test_ExpToSegment.tests), + ("Formatter", Test_Formatter.tests), ], ); Junit.to_file(Junit.make([suite]), "junit_tests.xml");