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 98AC45D4 for ; Sun, 4 Nov 2018 17:52:08 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.54,465,1534802400"; d="scan'208,217";a="354054115" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 04 Nov 2018 18:51:42 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 6EF1482513; Sun, 4 Nov 2018 18:51:42 +0100 (CET) Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id CC74C824E4 for ; Sun, 4 Nov 2018 18:51:37 +0100 (CET) Authentication-Results: mail3-smtp-sop.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-f182.google.com IronPort-PHdr: =?us-ascii?q?9a23=3AG3ZXvhWo9yPrIPccObcUkeR4dUzV8LGtZVwlr6E/?= =?us-ascii?q?grcLSJyIuqrYbBSBt8tkgFKBZ4jH8fUM07OQ7/i/HzRYqb+681k6OKRWUBEEjc?= =?us-ascii?q?hE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRo?= =?us-ascii?q?LerpBIHSk9631+ev8JHPfglEnjWwba9wIRmssQndqtQdjJd/JKo21hbHuGZDdf?= =?us-ascii?q?5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXM?= =?us-ascii?q?TRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmij?= =?us-ascii?q?oINyQh/W7YhMx/jqJVrhyiqRJi3YDbfJqYO+Bicq7HZ94WWXZNU8RXWidcAo28?= =?us-ascii?q?dYwPD+8ZMOhZtYbyvEEOrRqgCgmoGejh1yNHhn/o0q0gzeshCxzN0QsvH90Uq3?= =?us-ascii?q?vUttT1O7kWUeyv16nH0TXDYO1M2Tjj8ojFaR8hofSWUrJxdcrd01UgFwTAjliJ?= =?us-ascii?q?r4HuIj2b1uMIs2eB7upgU/qihHQ7pAF0uDSvwd0siobRioIay1DE6SV5wJsuKt?= =?us-ascii?q?GiVEF7ZtukHINRtyGcNot2XtkuQ2RsuCs817YIuoa7cTAUxJg7wxPTcf+KfoiS?= =?us-ascii?q?7h79SuqdPy10iG9mdb6hgRu57FKuxffmVsau1VZHtipFncfItnAKzxHT79KISv?= =?us-ascii?q?p5/ku4wDaP1B3f5vhKIUwplqfXNYQtwrE3lpoUvkTDGjH5lF/qg6+Rc0Uo4umo?= =?us-ascii?q?6+L5bbX6vpKQKZN4hwXkPqktmsGzG/o0PhYQU2SB5Oix16Pv8VX8QLpQj/02lq?= =?us-ascii?q?fZsIrdJcQevqO5DBVa3Z056xa+ETim1M4UnWIbI1JFZh2HlZbmO0vVLfD3CPew?= =?us-ascii?q?mVWskDNxy//aOb3hB43BLmLfn7f5YbZ990lcxRIvwt9F4pJUDqgNIPbyWk/qqN?= =?us-ascii?q?zVFQQ5Mgyxw+b/EtpxzIIeWWSVAq+YKqzeq1GI5vh8a9WLMYQUvDf3MfE/z/Hr?= =?us-ascii?q?hH4931QaePqHx5wSPV+xFO5nLkHRWnHsj80MCy9esQM0Vu3njBuZWj5efXuod6?= =?us-ascii?q?057zA/TomhCNGQFciWnLWd0XLjTdVtbWdcBwXUSCa6R8C/Q/4JLRmqDIpkmz0A?= =?us-ascii?q?W6KmTtZ4hx6rvQ7+jbFgK7iNo3FKhdfYzNFwotbru1Qq7zUtVpaS1miMSyd/mW?= =?us-ascii?q?ZaH2ZrjpA6mlR0zxK46YY9g/FcEoYNtfZAUwN/LJ2FiuIjW4q0VQXGcdOEDl2h?= =?us-ascii?q?R4f+DA=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0D6AgCKMN9bh7beVdFjHgEGBwaBZYIqQ?= =?us-ascii?q?X8VE4N2gR2CXpAygg2OKokXgWYNI4FUgnECAgKDPhoHAQQ0FgEDAQECAQEBAQE?= =?us-ascii?q?TAQEBCA0JCCkjDII2IoJjAQQBIwQZARsRDAEDAQsGAwILMAcCAiEBAREBBQEcG?= =?us-ascii?q?QmDGAGBaAEDDQgPjHGQBzyLDHsWBQEXgncFgTEBgnYKGScNWoEdGgIGEotkgVg?= =?us-ascii?q?/gyV+gSgZAYEURQEBgS4BEgFMgleCVwKGVYIQJB+VNiYuBwKCFASEVoMkgxw5g?= =?us-ascii?q?yoYgiGOPz+MSYEEhhuDEA8hgTmBBXEzGiNQMYI7CYISGAIbgzeEIHSFPz4wi26?= =?us-ascii?q?CPgEB?= X-IPAS-Result: =?us-ascii?q?A0D6AgCKMN9bh7beVdFjHgEGBwaBZYIqQX8VE4N2gR2CXpA?= =?us-ascii?q?ygg2OKokXgWYNI4FUgnECAgKDPhoHAQQ0FgEDAQECAQEBAQETAQEBCA0JCCkjD?= =?us-ascii?q?II2IoJjAQQBIwQZARsRDAEDAQsGAwILMAcCAiEBAREBBQEcGQmDGAGBaAEDDQg?= =?us-ascii?q?PjHGQBzyLDHsWBQEXgncFgTEBgnYKGScNWoEdGgIGEotkgVg/gyV+gSgZAYEUR?= =?us-ascii?q?QEBgS4BEgFMgleCVwKGVYIQJB+VNiYuBwKCFASEVoMkgxw5gyoYgiGOPz+MSYE?= =?us-ascii?q?EhhuDEA8hgTmBBXEzGiNQMYI7CYISGAIbgzeEIHSFPz4wi26CPgEB?= X-IronPort-AV: E=Sophos;i="5.54,465,1534802400"; d="scan'208,217";a="284290820" Received: from mail-qk1-f182.google.com ([209.85.222.182]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 04 Nov 2018 18:51:36 +0100 Received: by mail-qk1-f182.google.com with SMTP id e4so11124605qkh.6 for ; Sun, 04 Nov 2018 09:51:36 -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=IoB5PjcdfKKW5hvbrgJdI1YKpxt7DAjtSbP2tY2cQYU=; b=BtgP+0aE7615jkze+KEh5AZxcvmEPOvdzg0c5nWh/UKXwQh5sWGLofHU3Cm+iVD/wT 3x32Rt0wN3pHpnD2QyREnUIcZWGMwGeF2yW9zdOB1mug2v7ktYGZWYZlOAEuEa3VoB3i nxsTbYmPkWURqI5gtFy8aJ4XQtBX4aWmX/9CU4lpdkyBAJAxT8PSjMagBj1eRfuusvuS nqHoBWSd4imtqlPNi5uYaD5O+QvGY67D+R2RPUi0bgdW0DQu5PB4bU9jZCg3myo72fOZ ZGVJXzSoiqiZB8neXndqgNF3vSAo6qut4qr/uo7/V2lgTa0AukJiOeCTHYThd1AXwnB2 RRAA== 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=IoB5PjcdfKKW5hvbrgJdI1YKpxt7DAjtSbP2tY2cQYU=; b=cmm0ubIkcfin7feKuDJyDRCIcgmViOL2JL9ciis7sgCeKoI3cnd4C99xH8+wKbq5dI QRFVwpxXImHeYLUPlwZm/5W4ep+7/e7e/cTOLn6qjLzA81lhN3b/4WxWZGvZUDgTueor ZLEsuvELUknilc2gmexmBf6FM5P+dXFQggILR1/mR55jbfOqjexuGoX1Mz6pE5cVM0Rv 56bzV8VD9pIw5GsI9Bel3030MbXW+nC4KnmC47pqyhXYTYI5/EbuTIbjTyp8BwQzyEa3 XGRATaN9bmOdB83vuYaboSNocHZ54YGsI4jl1IWBSRIsGf4r2UY6UoNk6XzNdmWWzz3P l3Fw== X-Gm-Message-State: AGRZ1gJPOqpeqQFYl37GvB0rSNFDm42VO5z22FfQD169RZ/ENy6guDaG /2eS89NUwKblqEehmdHtSMXuD0N9muxylgQKI9mSPQ== X-Google-Smtp-Source: AJdET5dQmoLCyHMY0O8LeWQo4z8Nq/LMm//Mv9jvzhsCCrHC/lHEnr2jjYirGRwfvy2jL5XRJS2j0isY325paWI7TUs= X-Received: by 2002:a37:a053:: with SMTP id j80mr17881852qke.356.1541353894951; Sun, 04 Nov 2018 09:51:34 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Gabriel Scherer Date: Sun, 4 Nov 2018 19:00:54 +0100 Message-ID: To: cilibrar@gmail.com Cc: caml users Content-Type: multipart/alternative; boundary="00000000000061c1d00579da6ba5" 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: 17117 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: --00000000000061c1d00579da6ba5 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 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 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= --00000000000061c1d00579da6ba5 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
It looks like what this syntax extension is doing is = to rewrite fragments of the form

=C2=A0 <<fo= o>>

into

=C2=A0 def= ault_parser "foo"

and

=C2=A0 <<|foo|>>

into

=C2=A0 secondary_parser "foo".

You should be able to translate examples from the book simply by doi= ng this rewriting by hand. If the string/formula contains backslashes, it c= an 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 i= nto {|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 s= tyle 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
betw= een the preprocessors camlp4, camlp5, and ppx. The documentation
= is confusing to me at this point.

I have been tryi= ng to compile the code from the famous and great book
on logic ca= lled "Handbook of Practical Logic and Automated Reasoning"
<= div>but 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 c= oding convention
for preprocessing.=C2=A0 Would anybody on the li= st be able to help me (perhaps
privately via email/github) to con= vert this small fragment to modern
PPX syntax so that we can &quo= t;unlock" 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

=

Any help or info you can pr= ovide to get unblocked would be appreciated.
Thank you in advance= for your kind attention.

Best regards,
=
Rudi
---------------------------------------------= -------------------------------------------
=E2=9E=9C=C2=A0 sml-h= andbook git:(master) =E2=9C=97 cd code/OCaml
=E2=9E=9C=C2=A0 OCam= l git:(master) =E2=9C=97 make
echo '#use "init.ml";;' >.ocamlinit; (sl= eep 3s; rm -f .ocamlinit) & ocaml
=C2=A0 =C2=A0 =C2=A0 =C2=A0= OCaml version 4.05.0

File "Quotexpander.ml&q= uot;, line 2, characters 5-72:
Warning 3: deprecated: Pervasives.= &
Use (&&) instead.
File "Quotexpander= .ml", line 7, characters 0-13:
Error: Unbound module Quotati= on
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 Quotexpande= r.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 &quo= t;|" 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)^"\"";;

= Quotation.add "" (Quotation.ExStr (fun x -> quotexpander));;
=E2=9E=9C=C2=A0 OCaml git:(master) =E2=9C=97 ocaml --version
=
The OCaml toplevel, version 4.05.0
=E2=9E=9C=C2=A0 OCaml git= :(master) =E2=9C=97 opam --version
1.2.2
=E2=9E=9C=C2= =A0 OCaml git:(master) =E2=9C=97=C2=A0


-= -
--00000000000061c1d00579da6ba5--