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

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

[Rudi Cilibrasi]

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

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>

-- 
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list https://inbox.ocaml.org/caml-list
Forum: https://discuss.ocaml.org/
Bug reports: http://caml.inria.fr/bin/caml-bugs

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

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

[Gabriel Scherer]

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

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>
>

-- 
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list https://inbox.ocaml.org/caml-list
Forum: https://discuss.ocaml.org/
Bug reports: http://caml.inria.fr/bin/caml-bugs

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

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

[Gabriel Scherer]

[-- Attachment #1: Type: text/plain, Size: 4723 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>
>>
>

-- 
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list https://inbox.ocaml.org/caml-list
Forum: https://discuss.ocaml.org/
Bug reports: http://caml.inria.fr/bin/caml-bugs

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