From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTPS id F229A5D4 for ; Sun, 4 Nov 2018 17:57:29 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.54,465,1534802400"; d="scan'208,217";a="354054459" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 04 Nov 2018 18:57:28 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 0B17D824F7; Sun, 4 Nov 2018 18:57:29 +0100 (CET) Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 77456824E4 for ; Sun, 4 Nov 2018 18:57:25 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gabriel.scherer@gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer@gmail.com; spf=None smtp.helo=postmaster@mail-qk1-f196.google.com IronPort-PHdr: =?us-ascii?q?9a23=3Aop9S2RdtUYleF2sTz2pE2eYQlGMj4u6mDksu8pMi?= =?us-ascii?q?zoh2WeGdxcS6Yh7h7PlgxGXEQZ/co6odzbaO7Oa4ASQp2tWoiDg6aptCVhsI24?= =?us-ascii?q?09vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7?= =?us-ascii?q?Ovr6GpLIj8Swyuu+54Dfbx9HiTahY75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYe?= =?us-ascii?q?RWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZ?= =?us-ascii?q?TAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hy?= =?us-ascii?q?cdLzM2/2/Xhc5wgqxVoxyvugJxzJLPbY6PKPZzZLnQcc8GSWdDWMtaSixPApm7?= =?us-ascii?q?b4sKF+cPPPxXoJLnp1sPsxS+ARSnCv7zxT9ImHD2x7M10/48GgzB0wwvBckBsG?= =?us-ascii?q?7VrNrrMKceS/u1w7XIzTrddfNZxy395ZPHchAku/6MXLZwfdDNxkkoEgPIl1Od?= =?us-ascii?q?opHrMTOS0+QCqWmb7+x4WO21l2Enrht9oj+1xscjkoXJiYMVykzE9SVk24k5P8?= =?us-ascii?q?G3SEl+YdK8EZtQsSCaN5dsTsMnR2FlvjsxxL4euZOjYiQG1JAqywTcZvGHaYSE?= =?us-ascii?q?/AzvWPiLLTtlgH9oebSyjAuo/0e60O3zTMy03U5KriVbltnMsWgA1xnJ5ciGTv?= =?us-ascii?q?tx516h2TWS2wzK5OFIPEQ5mKvBJ54uxb4wkZUTsUDdESPshEr2i6qWel0l+uiu?= =?us-ascii?q?9evnfq3rqoGAO4JwkA3zMaQjltahDegmLAQCRXWX9OC92bH7+E32WrRKjvk4kq?= =?us-ascii?q?nDt5DaINwWpqGjDABOyIYj6giwDzO83NQDgXYHLExKeAiZgIjzIFzOL/X4Au2+?= =?us-ascii?q?g1Soijtk2/fGPrj5DpXXMnfDiKvhfap660NE1AU819Vf55ZNBrEFIfLzQVPxuc?= =?us-ascii?q?fDDh45Ngy02/zoBM981oMYQ2KPA7WWPLncsV+StaoTJLyHZYsUsiz0MdAq4vfv?= =?us-ascii?q?iTkynlpOU7Ou2M44YXqiH/lia36SYXf2j81JRWgDtBA/Qeisk1aCXCRefV69Wq?= =?us-ascii?q?s94ncwD4fwXtSLfZyknLHUhHTzJZZRfG0TUgndQ0etTJ2NXrI3UAzXJ8ZgljIe?= =?us-ascii?q?Ur34Et0u0BivsEnxzL81d7OIqB1djorq0Z1O38OWjQs7rGUmAMGU0mXLRGZxzD?= =?us-ascii?q?tRGm0GmZtnqEk48W+tlKh1h/sCS45W7vJNFx45bNvSlr0kTd/1XQ3Fc5GCT1P0?= =?us-ascii?q?Gtg=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0ChAgCmMt9bf8TeVdFjHAEBAQQBAQcEA?= =?us-ascii?q?QGBZYIqQX8VE4N2gR2CXpAygg2OKokXgWYNJYFSgnECAgKDPhoHAQQ0FgEDAQE?= =?us-ascii?q?CAQEBAQETAQEJCwsIGwwlDII2IoJjAQUjBBkBGxEMAQMBCwYDAgsNIwcCAiEBA?= =?us-ascii?q?REBBQEcGQmDGYFoAQMVD4xvkAc8iwx7FgUBF4J3BYExAYJ2ChknDVqBHRoCBhK?= =?us-ascii?q?LZIFYP4MlfoEoGQGBFEUBAYEuARIBTIJXglcChlWCECQflTYmLgcCghQEhFaDJ?= =?us-ascii?q?IMcOYMqGIIhjj8/jEmBBIYbgxAPIYE5gQVxMxojUDGCOwmCEhgdgzeEIHSFPz4?= =?us-ascii?q?wi26CPgEB?= X-IPAS-Result: =?us-ascii?q?A0ChAgCmMt9bf8TeVdFjHAEBAQQBAQcEAQGBZYIqQX8VE4N?= =?us-ascii?q?2gR2CXpAygg2OKokXgWYNJYFSgnECAgKDPhoHAQQ0FgEDAQECAQEBAQETAQEJC?= =?us-ascii?q?wsIGwwlDII2IoJjAQUjBBkBGxEMAQMBCwYDAgsNIwcCAiEBAREBBQEcGQmDGYF?= =?us-ascii?q?oAQMVD4xvkAc8iwx7FgUBF4J3BYExAYJ2ChknDVqBHRoCBhKLZIFYP4MlfoEoG?= =?us-ascii?q?QGBFEUBAYEuARIBTIJXglcChlWCECQflTYmLgcCghQEhFaDJIMcOYMqGIIhjj8?= =?us-ascii?q?/jEmBBIYbgxAPIYE5gQVxMxojUDGCOwmCEhgdgzeEIHSFPz4wi26CPgEB?= X-IronPort-AV: E=Sophos;i="5.54,465,1534802400"; d="scan'208,217";a="354054457" Received: from mail-qk1-f196.google.com ([209.85.222.196]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 04 Nov 2018 18:57:23 +0100 Received: by mail-qk1-f196.google.com with SMTP id o89so11198733qko.0 for ; Sun, 04 Nov 2018 09:57:23 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=QALaYWsaKTflXcnnvMCEF8pVI8Z+0PZofTF74gs0ltI=; b=lwEUNxba75wLgMq7p5zo4jorQat0uG0tLYlEoNHC3/roiDMHpzMcl3bTms1e+OJ615 nlkqNbVi+oUWavgvUpvbXsbw4Nxm+MouR5FHIbhhEJmva2SswrRqes8DRoCX5fDub5BR acfF29lPqF9KL/AtWWs3+EgsS8GxGslAJ+XWjjwh7R1TX1N/u3vzWnOSqxikVCSENPqS KcLqzdUYLrFF9D1zUEm85s912+vJ0gRFke5wV+lGwXCIGJHJuln3QUgnJwTj5Bpsn5b8 EZFt25ZFoiwz/u6tVyBLQ4oajy0BLiKd9GeYyQpHsOBmNIE+NqCHM/DbxReQN2m+iPx5 qFmQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc; bh=QALaYWsaKTflXcnnvMCEF8pVI8Z+0PZofTF74gs0ltI=; b=HPrRnpoVP3nORqCboEUDM4VPVt6wEfoMX7pf6ocUgksUawRUpD+UywzuCNeqrYmnME O11z5otrn0Go9e8snDmb3Tn15h80TW33cbkGaoqWTf3kWk6cCFOFjApqFr+USe+2yNuk 66Nj1k6caVaBTs5fa6Ba+HD6kWc1OHB/GLsKFKSnSOit4bUz6gj+bCuIeiUtPBE2CU9G HBH3+zoM6ix5e/T3yhKyrd+cpjNMOiB6tg4j2Jr9hzFLJ25vP6vbhJL7x4IwfYfsaVzb tIqSEsbPLq3Yq3yfpeoVY3xb+7maTx1treV8mKUKEzcAMKo9rgjIGnP3jzGMHEh8spcg VhwQ== X-Gm-Message-State: AGRZ1gJ2Jc8dWUUcyPwYIPWwDY3MTtiNMAEp9Z/x+cBi5MLqXmMkXzI0 tFIYYxT2R8FSNSF4EujaXuUlWhgXApd3bFMb5UE= X-Google-Smtp-Source: AJdET5dyZJYaPdyFdvge7jHMVZrej/48TAhkb62Jrnl7VWKxPzdrddE3NNjscw7klbkWwjFWWvTgrZOMcbIlre3Yg/E= X-Received: by 2002:a0c:89e9:: with SMTP id 38mr18727612qvs.31.1541354242506; Sun, 04 Nov 2018 09:57:22 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Gabriel Scherer Date: Sun, 4 Nov 2018 19:06:42 +0100 Message-ID: To: cilibrar@gmail.com Cc: caml users Content-Type: multipart/alternative; boundary="00000000000019057c0579da803e" Subject: Re: [Caml-list] Request for hint/help in camlp4/5-ppx conversion of famous logic quotation code by Harrison Reply-To: Gabriel Scherer X-Loop: caml-list@inria.fr X-Sequence: 17118 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: --00000000000019057c0579da803e Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 =3D `Default str let secondary_parser str =3D `Secondary str (* do the same test as done by the syntax extension *) let default_or_secondary_parser s =3D if String.sub s 0 1 =3D "|" && String.sub s (String.length s - 1) 1 =3D= "|" then secondary_parser (String.sub s 1 (String.length s - 1)) else default_parser s (* convenient infix operator *) let (!!) =3D default_or_secondary_parser (* example use-cases from https://github.com/logic-tools/sml-handbook/blob/master/code/OCaml/example.= ml *) let gold =3D !!{|p /\ q <=3D> ((p <=3D> q) <=3D> p \/ q)|} (* default parse= r *) let test =3D ["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 wrote: > It looks like what this syntax extension is doing is to rewrite fragments > of the form > > <> > > 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 liter= al > {|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 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 >> >> ------------------------------------------------------------------------= ---------------- >> =E2=9E=9C sml-handbook git:(master) =E2=9C=97 cd code/OCaml >> =E2=9E=9C OCaml git:(master) =E2=9C=97 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 >> >> # >> =E2=9E=9C OCaml git:(master) =E2=9C=97 cat Quotexpander.ml >> let quotexpander s =3D >> if String.sub s 0 1 =3D "|" & String.sub s (String.length s - 1) 1 =3D= "|" >> 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));; >> =E2=9E=9C OCaml git:(master) =E2=9C=97 ocaml --version >> The OCaml toplevel, version 4.05.0 >> =E2=9E=9C OCaml git:(master) =E2=9C=97 opam --version >> 1.2.2 >> =E2=9E=9C OCaml git:(master) =E2=9C=97 >> >> >> -- >> Happy to Code with Integrity : Software Engineering Code of Ethics and >> Professional Practice >> > --=20 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= --00000000000019057c0579da803e Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Here is a transcript of using plain = OCaml code instead of the extension:

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

(* do the same test as done by the syntax extension *)=
let default_or_secondary_parser s =3D
=C2=A0=C2=A0=C2=A0 if String.s= ub s 0 1 =3D "|" && String.sub s (String.length s - 1) 1 = =3D "|"
=C2=A0=C2=A0=C2=A0 then secondary_parser (String.sub s= 1 (String.length s - 1))
=C2=A0=C2=A0=C2=A0 else default_parser s
(* convenient infix operator *)
let (!!) =3D default_or_secondary_pars= er

(* example use-cases from
=C2=A0=C2=A0 https://= github.com/logic-tools/sml-handbook/blob/master/code/OCaml/example.ml=C2=A0*)

let gold =3D !!{|p /\ q <=3D> ((p <=3D> q) &l= t;=3D> p \/ q)|} (* default parser *)
let test =3D
=C2=A0 ["f= ix1", !!{||--(imp(G,imp(Pr(G),S)))||};=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0
=C2=A0=C2=A0 "fix2", !!{||--(imp(imp(Pr(G),S),G)= )||}];
(* the doubling of "|" in formulas above sig= nals the secondary parser. *)

On Sun, Nov 4, 2018 at 7:00 PM Gabriel Scherer <= gabriel.scherer@gmail.com&= gt; wrote:
It= looks like what this syntax extension is doing is to rewrite fragments of = the form

=C2=A0 <<foo>>

=
into

=C2=A0 default_parser "foo&qu= ot;

and

=C2=A0 <<|f= oo|>>

into

=C2=A0 s= econdary_parser "foo".

You should be abl= e to translate examples from the book simply by doing this rewriting by han= d. If the string/formula contains backslashes, it can be painful to properl= y escape them to follow the lexical conventions of OCaml double-quoted stri= ng literals, but you can use the new string literal {|foo|} to avoid escape= s. For example, "a\\b" can be rewritten into {|a\b|}.
<= br>

On Sun, Nov = 4, 2018 at 6:42 PM Rudi Cilibrasi <cilibrar@gmail.com> wrote:
Greetings ML frien= ds,

I have been gradually following the ML style l= anguages a couple decades
with HOL/SML etc and recently got inter= ested in the OCaml variation.

I've been able t= o make simple OCaml programs for my research but am
hitting a ste= ep learning curve trying to understand the differences
between th= e preprocessors camlp4, camlp5, and ppx. The documentation
is con= fusing to me at this point.

I have been trying to = compile the code from the famous and great book
on logic called &= quot;Handbook of Practical Logic and Automated Reasoning"
bu= t it does not work for me under Ubuntu 18.04 using OCaml 4.05. I
= have opam 1.2.2.=C2=A0 I am getting an "Unbound module Quotation"= error
that Icannot solve and I suspect is related to old coding = convention
for preprocessing.=C2=A0 Would anybody on the list be = able to help me (perhaps
privately via email/github) to convert t= his small fragment to modern
PPX syntax so that we can "unlo= ck" the rest of the code describing first=C2=A0
order logic?= =C2=A0 I attach a transcript below trying to compile one of many
= copies of the same code on github, this one from

<= a href=3D"https://github.com/logic-tools/sml-handbook/tree/master/code/OCam= l" target=3D"_blank">https://github.com/logic-tools/sml-handbook/tree/maste= r/code/OCaml

Any help or info you can provide = to get unblocked would be appreciated.
Thank you in advance for y= our kind attention.

Best regards,

Rudi
---------------------------------------------------= -------------------------------------
=E2=9E=9C=C2=A0 sml-handboo= k git:(master) =E2=9C=97 cd code/OCaml
=E2=9E=9C=C2=A0 OCaml git:= (master) =E2=9C=97 make
echo '#use "init.ml";;' >.ocamlinit; (sleep 3s= ; rm -f .ocamlinit) & ocaml
=C2=A0 =C2=A0 =C2=A0 =C2=A0 OCaml= version 4.05.0

File "Quotexpander.ml", = line 2, characters 5-72:
Warning 3: deprecated: Pervasives.&<= /div>
Use (&&) instead.
File "Quotexpander.ml&qu= ot;, line 7, characters 0-13:
Error: Unbound module Quotation
File "Quotexpander.ml", line 998, characters 7-9:
Unbound quotation: ""
Camlp5 parsing version 7.06

#=C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0
=E2=9E=9C=C2=A0 OCaml git:(master) =E2=9C=97 cat Quotexpander.ml=C2= =A0
let quotexpander s =3D
=C2=A0 if String.sub s 0 1 = =3D "|" & String.sub s (String.length s - 1) 1 =3D "|&qu= ot; then
=C2=A0 =C2=A0 "secondary_parser \""^
=C2=A0 =C2=A0 (String.escaped (String.sub s 1 (String.length s - 2)))= ^"\""
=C2=A0 else "default_parser \"&quo= t;^(String.escaped s)^"\"";;

Quotat= ion.add "" (Quotation.ExStr (fun x -> quotexpander));;
=E2=9E=9C=C2=A0 OCaml git:(master) =E2=9C=97 ocaml --version
T= he OCaml toplevel, version 4.05.0
=E2=9E=9C=C2=A0 OCaml git:(mast= er) =E2=9C=97 opam --version
1.2.2
=E2=9E=9C=C2=A0 OCam= l git:(master) =E2=9C=97=C2=A0


--
--00000000000019057c0579da803e--