aqjune
April 16, 2024, 7:04pm
1
Hello all,
I have a question about a possible workaround for using camlp5 on UTop.
As an example, in HOL Light, a special quotation x
means an expression called ‘term’ type, and its camlp5 preprocesses it as parse_term "x"
. However, this preprocessing does not happen if I use UTop:
─( 11:13:52 )─< command 0 >───────────{ counter: 0 }─
utop # `1 + 2 = 3`;;
Error: Syntax error
Interestingly, if I store `1 + 2 = 3`;;
as a temporary file, say tmp.ml
, and load it using the #use
command, this works great.
─( 13:09:39 )─< command 1 >────────────{ counter: 0 }─
utop # #use "tmp.ml";;
- : term = `1 + 2 = 3`
Can UTop provide a flag that does this workaround, as a possible partial solution for supporting camlp5? I left an issue at A possible workaround for supporting camlp5 on UTop · Issue #485 · ocaml-community/utop · GitHub too.
Camlp5 has a pretty straightforward hook into the OCaml toplevel. A long time ago, I made changes to ocaml-mdx
to make Camlp5 work there. It was long enough ago that I forget whether the maintainers had figured it out independently but in any case it was a single-line change ( mdx/lib/top/mdx_top.ml at e2b6532d0bb34789aaff39429b1f8be3ae931333 · realworldocaml/mdx · GitHub ).
In any case, I suspect it should be straightforward to modify utop
to interact correctly with camlp5. I don’t use utop, but if you can look around in the sources and see if something looks like what I linked-to above, I can help you figure it out.
1 Like
aqjune
April 19, 2024, 3:00pm
3
Hi @Chet_Murthy , thanks for the pointer!
It appears UTop is calling UTop.parse_toplevel_phrase
:
Pparse.report_error Format.str_formatter error;
UTop.Error ([], "Error: " ^ Format.flush_str_formatter () ^ "\n"))
in
(result, Buffer.contents buf)
let parse_and_check input ~eos_is_error =
let buf = Buffer.create 32 in
let result =
UTop.collect_formatters buf [Format.err_formatter]
(fun () ->
match !UTop.parse_toplevel_phrase input eos_is_error with
| UTop.Error (locs, msg) ->
UTop.Error (convert_locs input locs, "Error: " ^ msg ^ "\n")
| UTop.Value phrase ->
try
let phrase = preprocess phrase in
match UTop.check_phrase phrase with
| None ->
UTop.Value phrase
| Some (locs, msg, lines) ->
UTop.Error (convert_loc_line input locs lines, msg)
I thought that if this invocation can be replaced with a wrapper of Toploop.parse_toplevel_phrase
then this would naturally support camlp5.
I looked deeper and the UTop.parse_toplevel_phrase
is defined using parse_default
and Parse.toplevel_phrase
:
But parse_default
is a somewhat long function, so it seems writing the wrapper is a non-trivial job. Hmm…
aqjune
April 19, 2024, 3:37pm
4
This one-line patch worked, actually:
diff --git a/src/lib/uTop.ml b/src/lib/uTop.ml
index 801fd29..ecb686e 100644
--- a/src/lib/uTop.ml
+++ b/src/lib/uTop.ml
@@ -305,7 +305,7 @@ let parse_default parse str eos_is_error =
| exn ->
Error ([], "Unknown parsing error (please report it to the utop project): " ^ Printexc.to_string exn)
-let parse_toplevel_phrase_default = parse_default Parse.toplevel_phrase
+let parse_toplevel_phrase_default = fun str -> parse_default !Toploop.parse_toplevel_phrase str
let parse_toplevel_phrase = ref parse_toplevel_phrase_default
let parse_use_file_default = parse_default Parse.use_file
I should test this more and create a pull request if it works ok.
Yep, that’s what I figured would work (or something like it). BTW, it’s worth checking if #use
works – the code path for that was different, IIRC (but I might be misremembering).
aqjune
April 23, 2024, 4:18am
6