Re: [Caml-list] Request for hint/help in camlp4/5-ppx conversion of famous logic quotation code by Harrison

[Gabriel Scherer <gabriel.scherer@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 4492 bytes --]

Here is a transcript of using plain OCaml code instead of the extension:

(* mock parsers for testing; I'm sure the real definitions are more
interesting *)
let default_parser str = `Default str
let secondary_parser str = `Secondary str

(* do the same test as done by the syntax extension *)
let default_or_secondary_parser s =
    if String.sub s 0 1 = "|" && String.sub s (String.length s - 1) 1 = "|"
    then secondary_parser (String.sub s 1 (String.length s - 1))
    else default_parser s

(* convenient infix operator *)
let (!!) = default_or_secondary_parser

(* example use-cases from

https://github.com/logic-tools/sml-handbook/blob/master/code/OCaml/example.ml
 *)

let gold = !!{|p /\ q <=> ((p <=> q) <=> p \/ q)|} (* default parser *)
let test =
  ["fix1", !!{||--(imp(G,imp(Pr(G),S)))||};
   "fix2", !!{||--(imp(imp(Pr(G),S),G))||}];
(* the doubling of "|" in formulas above signals the secondary parser. *)

On Sun, Nov 4, 2018 at 7:00 PM Gabriel Scherer <gabriel.scherer@gmail.com>
wrote:

> It looks like what this syntax extension is doing is to rewrite fragments
> of the form
>
>   <<foo>>
>
> into
>
>   default_parser "foo"
>
> and
>
>   <<|foo|>>
>
> into
>
>   secondary_parser "foo".
>
> You should be able to translate examples from the book simply by doing
> this rewriting by hand. If the string/formula contains backslashes, it can
> be painful to properly escape them to follow the lexical conventions of
> OCaml double-quoted string literals, but you can use the new string literal
> {|foo|} to avoid escapes. For example, "a\\b" can be rewritten into {|a\b|}.
>
>
> On Sun, Nov 4, 2018 at 6:42 PM Rudi Cilibrasi <cilibrar@gmail.com> wrote:
>
>> Greetings ML friends,
>>
>> I have been gradually following the ML style languages a couple decades
>> with HOL/SML etc and recently got interested in the OCaml variation.
>>
>> I've been able to make simple OCaml programs for my research but am
>> hitting a steep learning curve trying to understand the differences
>> between the preprocessors camlp4, camlp5, and ppx. The documentation
>> is confusing to me at this point.
>>
>> I have been trying to compile the code from the famous and great book
>> on logic called "Handbook of Practical Logic and Automated Reasoning"
>> but it does not work for me under Ubuntu 18.04 using OCaml 4.05. I
>> have opam 1.2.2.  I am getting an "Unbound module Quotation" error
>> that Icannot solve and I suspect is related to old coding convention
>> for preprocessing.  Would anybody on the list be able to help me (perhaps
>> privately via email/github) to convert this small fragment to modern
>> PPX syntax so that we can "unlock" the rest of the code describing first
>> order logic?  I attach a transcript below trying to compile one of many
>> copies of the same code on github, this one from
>>
>> https://github.com/logic-tools/sml-handbook/tree/master/code/OCaml
>>
>> Any help or info you can provide to get unblocked would be appreciated.
>> Thank you in advance for your kind attention.
>>
>> Best regards,
>>
>> Rudi
>>
>> ----------------------------------------------------------------------------------------
>> ➜  sml-handbook git:(master) ✗ cd code/OCaml
>> ➜  OCaml git:(master) ✗ make
>> echo '#use "init.ml";;' >.ocamlinit; (sleep 3s; rm -f .ocamlinit) & ocaml
>>         OCaml version 4.05.0
>>
>> File "Quotexpander.ml", line 2, characters 5-72:
>> Warning 3: deprecated: Pervasives.&
>> Use (&&) instead.
>> File "Quotexpander.ml", line 7, characters 0-13:
>> Error: Unbound module Quotation
>> File "Quotexpander.ml", line 998, characters 7-9:
>> Unbound quotation: ""
>> Camlp5 parsing version 7.06
>>
>> #
>> ➜  OCaml git:(master) ✗ cat Quotexpander.ml
>> let quotexpander s =
>>   if String.sub s 0 1 = "|" & String.sub s (String.length s - 1) 1 = "|"
>> then
>>     "secondary_parser \""^
>>     (String.escaped (String.sub s 1 (String.length s - 2)))^"\""
>>   else "default_parser \""^(String.escaped s)^"\"";;
>>
>> Quotation.add "" (Quotation.ExStr (fun x -> quotexpander));;
>> ➜  OCaml git:(master) ✗ ocaml --version
>> The OCaml toplevel, version 4.05.0
>> ➜  OCaml git:(master) ✗ opam --version
>> 1.2.2
>> ➜  OCaml git:(master) ✗
>>
>>
>> --
>> Happy to Code with Integrity : Software Engineering Code of Ethics and
>> Professional Practice <http://www.acm.org/about/about/se-code>
>>
>

[-- Attachment #2: Type: text/html, Size: 6617 bytes --]