--- /dev/null
+*~
+*.cmi
+*.cmo
+*.cmx
+*.cma
+*.cmxa
+*.o
+
+.depend
+Goalfile
+Makefile
+config.log
+
+/aclocal.m4
+/autom4te.cache/
+/configure
+/config.h
+/config.h.in
+/config.status
+/install-sh
+/parsing/goals
+/parsing/lexer.ml
+/parsing/parser.conflicts
+/parsing/parser.ml
+/parsing/parser.mli
+/parsing/stamp-parser
+/stamp-h
--- /dev/null
+ GNU GENERAL PUBLIC LICENSE
+ Version 2, June 1991
+
+ Copyright (C) 1989, 1991 Free Software Foundation, Inc.,
+ 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+ Preamble
+
+ The licenses for most software are designed to take away your
+freedom to share and change it. By contrast, the GNU General Public
+License is intended to guarantee your freedom to share and change free
+software--to make sure the software is free for all its users. This
+General Public License applies to most of the Free Software
+Foundation's software and to any other program whose authors commit to
+using it. (Some other Free Software Foundation software is covered by
+the GNU Lesser General Public License instead.) You can apply it to
+your programs, too.
+
+ When we speak of free software, we are referring to freedom, not
+price. Our General Public Licenses are designed to make sure that you
+have the freedom to distribute copies of free software (and charge for
+this service if you wish), that you receive source code or can get it
+if you want it, that you can change the software or use pieces of it
+in new free programs; and that you know you can do these things.
+
+ To protect your rights, we need to make restrictions that forbid
+anyone to deny you these rights or to ask you to surrender the rights.
+These restrictions translate to certain responsibilities for you if you
+distribute copies of the software, or if you modify it.
+
+ For example, if you distribute copies of such a program, whether
+gratis or for a fee, you must give the recipients all the rights that
+you have. You must make sure that they, too, receive or can get the
+source code. And you must show them these terms so they know their
+rights.
+
+ We protect your rights with two steps: (1) copyright the software, and
+(2) offer you this license which gives you legal permission to copy,
+distribute and/or modify the software.
+
+ Also, for each author's protection and ours, we want to make certain
+that everyone understands that there is no warranty for this free
+software. If the software is modified by someone else and passed on, we
+want its recipients to know that what they have is not the original, so
+that any problems introduced by others will not reflect on the original
+authors' reputations.
+
+ Finally, any free program is threatened constantly by software
+patents. We wish to avoid the danger that redistributors of a free
+program will individually obtain patent licenses, in effect making the
+program proprietary. To prevent this, we have made it clear that any
+patent must be licensed for everyone's free use or not licensed at all.
+
+ The precise terms and conditions for copying, distribution and
+modification follow.
+
+ GNU GENERAL PUBLIC LICENSE
+ TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
+
+ 0. This License applies to any program or other work which contains
+a notice placed by the copyright holder saying it may be distributed
+under the terms of this General Public License. The "Program", below,
+refers to any such program or work, and a "work based on the Program"
+means either the Program or any derivative work under copyright law:
+that is to say, a work containing the Program or a portion of it,
+either verbatim or with modifications and/or translated into another
+language. (Hereinafter, translation is included without limitation in
+the term "modification".) Each licensee is addressed as "you".
+
+Activities other than copying, distribution and modification are not
+covered by this License; they are outside its scope. The act of
+running the Program is not restricted, and the output from the Program
+is covered only if its contents constitute a work based on the
+Program (independent of having been made by running the Program).
+Whether that is true depends on what the Program does.
+
+ 1. You may copy and distribute verbatim copies of the Program's
+source code as you receive it, in any medium, provided that you
+conspicuously and appropriately publish on each copy an appropriate
+copyright notice and disclaimer of warranty; keep intact all the
+notices that refer to this License and to the absence of any warranty;
+and give any other recipients of the Program a copy of this License
+along with the Program.
+
+You may charge a fee for the physical act of transferring a copy, and
+you may at your option offer warranty protection in exchange for a fee.
+
+ 2. You may modify your copy or copies of the Program or any portion
+of it, thus forming a work based on the Program, and copy and
+distribute such modifications or work under the terms of Section 1
+above, provided that you also meet all of these conditions:
+
+ a) You must cause the modified files to carry prominent notices
+ stating that you changed the files and the date of any change.
+
+ b) You must cause any work that you distribute or publish, that in
+ whole or in part contains or is derived from the Program or any
+ part thereof, to be licensed as a whole at no charge to all third
+ parties under the terms of this License.
+
+ c) If the modified program normally reads commands interactively
+ when run, you must cause it, when started running for such
+ interactive use in the most ordinary way, to print or display an
+ announcement including an appropriate copyright notice and a
+ notice that there is no warranty (or else, saying that you provide
+ a warranty) and that users may redistribute the program under
+ these conditions, and telling the user how to view a copy of this
+ License. (Exception: if the Program itself is interactive but
+ does not normally print such an announcement, your work based on
+ the Program is not required to print an announcement.)
+
+These requirements apply to the modified work as a whole. If
+identifiable sections of that work are not derived from the Program,
+and can be reasonably considered independent and separate works in
+themselves, then this License, and its terms, do not apply to those
+sections when you distribute them as separate works. But when you
+distribute the same sections as part of a whole which is a work based
+on the Program, the distribution of the whole must be on the terms of
+this License, whose permissions for other licensees extend to the
+entire whole, and thus to each and every part regardless of who wrote it.
+
+Thus, it is not the intent of this section to claim rights or contest
+your rights to work written entirely by you; rather, the intent is to
+exercise the right to control the distribution of derivative or
+collective works based on the Program.
+
+In addition, mere aggregation of another work not based on the Program
+with the Program (or with a work based on the Program) on a volume of
+a storage or distribution medium does not bring the other work under
+the scope of this License.
+
+ 3. You may copy and distribute the Program (or a work based on it,
+under Section 2) in object code or executable form under the terms of
+Sections 1 and 2 above provided that you also do one of the following:
+
+ a) Accompany it with the complete corresponding machine-readable
+ source code, which must be distributed under the terms of Sections
+ 1 and 2 above on a medium customarily used for software interchange; or,
+
+ b) Accompany it with a written offer, valid for at least three
+ years, to give any third party, for a charge no more than your
+ cost of physically performing source distribution, a complete
+ machine-readable copy of the corresponding source code, to be
+ distributed under the terms of Sections 1 and 2 above on a medium
+ customarily used for software interchange; or,
+
+ c) Accompany it with the information you received as to the offer
+ to distribute corresponding source code. (This alternative is
+ allowed only for noncommercial distribution and only if you
+ received the program in object code or executable form with such
+ an offer, in accord with Subsection b above.)
+
+The source code for a work means the preferred form of the work for
+making modifications to it. For an executable work, complete source
+code means all the source code for all modules it contains, plus any
+associated interface definition files, plus the scripts used to
+control compilation and installation of the executable. However, as a
+special exception, the source code distributed need not include
+anything that is normally distributed (in either source or binary
+form) with the major components (compiler, kernel, and so on) of the
+operating system on which the executable runs, unless that component
+itself accompanies the executable.
+
+If distribution of executable or object code is made by offering
+access to copy from a designated place, then offering equivalent
+access to copy the source code from the same place counts as
+distribution of the source code, even though third parties are not
+compelled to copy the source along with the object code.
+
+ 4. You may not copy, modify, sublicense, or distribute the Program
+except as expressly provided under this License. Any attempt
+otherwise to copy, modify, sublicense or distribute the Program is
+void, and will automatically terminate your rights under this License.
+However, parties who have received copies, or rights, from you under
+this License will not have their licenses terminated so long as such
+parties remain in full compliance.
+
+ 5. You are not required to accept this License, since you have not
+signed it. However, nothing else grants you permission to modify or
+distribute the Program or its derivative works. These actions are
+prohibited by law if you do not accept this License. Therefore, by
+modifying or distributing the Program (or any work based on the
+Program), you indicate your acceptance of this License to do so, and
+all its terms and conditions for copying, distributing or modifying
+the Program or works based on it.
+
+ 6. Each time you redistribute the Program (or any work based on the
+Program), the recipient automatically receives a license from the
+original licensor to copy, distribute or modify the Program subject to
+these terms and conditions. You may not impose any further
+restrictions on the recipients' exercise of the rights granted herein.
+You are not responsible for enforcing compliance by third parties to
+this License.
+
+ 7. If, as a consequence of a court judgment or allegation of patent
+infringement or for any other reason (not limited to patent issues),
+conditions are imposed on you (whether by court order, agreement or
+otherwise) that contradict the conditions of this License, they do not
+excuse you from the conditions of this License. If you cannot
+distribute so as to satisfy simultaneously your obligations under this
+License and any other pertinent obligations, then as a consequence you
+may not distribute the Program at all. For example, if a patent
+license would not permit royalty-free redistribution of the Program by
+all those who receive copies directly or indirectly through you, then
+the only way you could satisfy both it and this License would be to
+refrain entirely from distribution of the Program.
+
+If any portion of this section is held invalid or unenforceable under
+any particular circumstance, the balance of the section is intended to
+apply and the section as a whole is intended to apply in other
+circumstances.
+
+It is not the purpose of this section to induce you to infringe any
+patents or other property right claims or to contest validity of any
+such claims; this section has the sole purpose of protecting the
+integrity of the free software distribution system, which is
+implemented by public license practices. Many people have made
+generous contributions to the wide range of software distributed
+through that system in reliance on consistent application of that
+system; it is up to the author/donor to decide if he or she is willing
+to distribute software through any other system and a licensee cannot
+impose that choice.
+
+This section is intended to make thoroughly clear what is believed to
+be a consequence of the rest of this License.
+
+ 8. If the distribution and/or use of the Program is restricted in
+certain countries either by patents or by copyrighted interfaces, the
+original copyright holder who places the Program under this License
+may add an explicit geographical distribution limitation excluding
+those countries, so that distribution is permitted only in or among
+countries not thus excluded. In such case, this License incorporates
+the limitation as if written in the body of this License.
+
+ 9. The Free Software Foundation may publish revised and/or new versions
+of the General Public License from time to time. Such new versions will
+be similar in spirit to the present version, but may differ in detail to
+address new problems or concerns.
+
+Each version is given a distinguishing version number. If the Program
+specifies a version number of this License which applies to it and "any
+later version", you have the option of following the terms and conditions
+either of that version or of any later version published by the Free
+Software Foundation. If the Program does not specify a version number of
+this License, you may choose any version ever published by the Free Software
+Foundation.
+
+ 10. If you wish to incorporate parts of the Program into other free
+programs whose distribution conditions are different, write to the author
+to ask for permission. For software which is copyrighted by the Free
+Software Foundation, write to the Free Software Foundation; we sometimes
+make exceptions for this. Our decision will be guided by the two goals
+of preserving the free status of all derivatives of our free software and
+of promoting the sharing and reuse of software generally.
+
+ NO WARRANTY
+
+ 11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY
+FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN
+OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES
+PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED
+OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
+MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS
+TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE
+PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING,
+REPAIR OR CORRECTION.
+
+ 12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR
+REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES,
+INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING
+OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED
+TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY
+YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER
+PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGES.
+
+ END OF TERMS AND CONDITIONS
+
+ How to Apply These Terms to Your New Programs
+
+ If you develop a new program, and you want it to be of the greatest
+possible use to the public, the best way to achieve this is to make it
+free software which everyone can redistribute and change under these terms.
+
+ To do so, attach the following notices to the program. It is safest
+to attach them to the start of each source file to most effectively
+convey the exclusion of warranty; and each file should have at least
+the "copyright" line and a pointer to where the full notice is found.
+
+ <one line to give the program's name and a brief idea of what it does.>
+ Copyright (C) <year> <name of author>
+
+ This program is free software; you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation; either version 2 of the License, or
+ (at your option) any later version.
+
+ This program is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ GNU General Public License for more details.
+
+ You should have received a copy of the GNU General Public License along
+ with this program; if not, write to the Free Software Foundation, Inc.,
+ 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+
+Also add information on how to contact you by electronic and paper mail.
+
+If the program is interactive, make it output a short notice like this
+when it starts in an interactive mode:
+
+ Gnomovision version 69, Copyright (C) year name of author
+ Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'.
+ This is free software, and you are welcome to redistribute it
+ under certain conditions; type `show c' for details.
+
+The hypothetical commands `show w' and `show c' should show the appropriate
+parts of the General Public License. Of course, the commands you use may
+be called something other than `show w' and `show c'; they could even be
+mouse-clicks or menu items--whatever suits your program.
+
+You should also get your employer (if you work as a programmer) or your
+school, if any, to sign a "copyright disclaimer" for the program, if
+necessary. Here is a sample; alter the names:
+
+ Yoyodyne, Inc., hereby disclaims all copyright interest in the program
+ `Gnomovision' (which makes passes at compilers) written by James Hacker.
+
+ <signature of Ty Coon>, 1 April 1989
+ Ty Coon, President of Vice
+
+This General Public License does not permit incorporating your program into
+proprietary programs. If your program is a subroutine library, you may
+consider it more useful to permit linking proprietary applications with the
+library. If this is what you want to do, use the GNU Lesser General
+Public License instead of this License.
--- /dev/null
+# Goalfile parser
+# Copyright (C) 2019 Richard W.M. Jones
+# Copyright (C) 2019 Red Hat Inc.
+#
+# This program is free software; you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License along
+# with this program; if not, write to the Free Software Foundation, Inc.,
+# 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+
--- /dev/null
+# Goalfile parser
+# Copyright (C) 2019 Richard W.M. Jones
+# Copyright (C) 2019 Red Hat Inc.
+#
+# This program is free software; you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License along
+# with this program; if not, write to the Free Software Foundation, Inc.,
+# 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+
+SUBDIRS = parsing
+
+all clean depend install:
+ $(MAKE) -C parsing $@
+
+config.h: stamp-h
+stamp-h: config.h.in config.status
+ ./config.status config.h
+ touch $@
+
+Makefile: Makefile.in config.status
+ ./config.status Makefile
+
+$(srcdir)/configure: configure.ac aclocal.m4
+ cd '$(srcdir)' && autoconf
+
+$(srcdir)/config.h.in: stamp-h.in
+$(srcdir)/stamp-h.in: configure.ac aclocal.m4
+ cd '$(srcdir)' && autoheader
+ echo timestamp > '$(srcdir)/stamp-h.in'
+
+config.status: configure
+ ./config.status --recheck
--- /dev/null
+autoreconf -i
+
+# Although we don't use automake, we have to run this in order to
+# create or regenerate install-sh (PR automake/546).
+automake --add-missing >/dev/null 2>&1 ||:
+
+./configure "$@"
--- /dev/null
+# Goals
+# Copyright (C) 2019 Richard W.M. Jones
+# Copyright (C) 2019 Red Hat Inc.
+#
+# This program is free software; you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License along
+# with this program; if not, write to the Free Software Foundation, Inc.,
+# 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+
+AC_INIT([goals], [0.1])
+AC_CONFIG_MACRO_DIR([m4])
+
+AC_PROG_INSTALL
+
+dnl Check for basic C environment.
+AC_PROG_CC_STDC
+AC_PROG_INSTALL
+AC_PROG_CPP
+
+AC_C_PROTOTYPES
+test "x$U" != "x" && AC_MSG_ERROR([Compiler not ANSI compliant])
+
+dnl Check for basic OCaml environment and findlib.
+AC_PROG_OCAML
+if test "x$OCAMLC" = "xno"; then
+ AC_MSG_ERROR([OCaml compiler is required])
+fi
+
+dnl Check for required programs.
+AC_PROG_FINDLIB
+if test "x$OCAMLFIND" = "xno"; then
+ AC_MSG_ERROR([OCaml findlib is required])
+fi
+AC_PROG_OCAMLLEX
+if test "x$OCAMLLEX" = "xno"; then
+ AC_MSG_ERROR([OCaml ocamllex lexical generator tool is required])
+fi
+
+AC_CHECK_PROG(MENHIR, [menhir], [menhir], [
+ AC_MSG_ERROR([OCaml menhir parser generator is required])
+])
+
+dnl Produce output files.
+AC_CONFIG_HEADERS([config.h])
+AC_CONFIG_FILES([stamp-h], [echo timestamp > stamp-h])
+AC_CONFIG_FILES([Goalfile Makefile
+ parsing/Goalfile parsing/Makefile])
+
+AC_OUTPUT
--- /dev/null
+dnl autoconf macros for OCaml
+dnl
+dnl Copyright © 2009 Richard W.M. Jones
+dnl Copyright © 2009 Stefano Zacchiroli
+dnl Copyright © 2000-2005 Olivier Andrieu
+dnl Copyright © 2000-2005 Jean-Christophe Filliâtre
+dnl Copyright © 2000-2005 Georges Mariano
+dnl
+dnl For documentation, please read the ocaml.m4 man page.
+
+AC_DEFUN([AC_PROG_OCAML],
+[dnl
+ # checking for ocamlc
+ AC_CHECK_TOOL([OCAMLC],[ocamlc],[no])
+
+ if test "$OCAMLC" != "no"; then
+ OCAMLVERSION=`$OCAMLC -v | sed -n -e 's|.*version* *\(.*\)$|\1|p'`
+ AC_MSG_RESULT([OCaml version is $OCAMLVERSION])
+ OCAMLLIB=`$OCAMLC -where 2>/dev/null || $OCAMLC -v|tail -1|cut -d ' ' -f 4`
+ AC_MSG_RESULT([OCaml library path is $OCAMLLIB])
+
+ AC_SUBST([OCAMLVERSION])
+ AC_SUBST([OCAMLLIB])
+
+ # checking for ocamlopt
+ AC_CHECK_TOOL([OCAMLOPT],[ocamlopt],[no])
+ OCAMLBEST=byte
+ if test "$OCAMLOPT" = "no"; then
+ AC_MSG_WARN([Cannot find ocamlopt; bytecode compilation only.])
+ else
+ TMPVERSION=`$OCAMLOPT -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
+ if test "$TMPVERSION" != "$OCAMLVERSION" ; then
+ AC_MSG_RESULT([versions differs from ocamlc; ocamlopt discarded.])
+ OCAMLOPT=no
+ else
+ OCAMLBEST=opt
+ fi
+ fi
+
+ AC_SUBST([OCAMLBEST])
+
+ # checking for ocamlc.opt
+ AC_CHECK_TOOL([OCAMLCDOTOPT],[ocamlc.opt],[no])
+ if test "$OCAMLCDOTOPT" != "no"; then
+ TMPVERSION=`$OCAMLCDOTOPT -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
+ if test "$TMPVERSION" != "$OCAMLVERSION" ; then
+ AC_MSG_RESULT([versions differs from ocamlc; ocamlc.opt discarded.])
+ else
+ OCAMLC=$OCAMLCDOTOPT
+ fi
+ fi
+
+ # checking for ocamlopt.opt
+ if test "$OCAMLOPT" != "no" ; then
+ AC_CHECK_TOOL([OCAMLOPTDOTOPT],[ocamlopt.opt],[no])
+ if test "$OCAMLOPTDOTOPT" != "no"; then
+ TMPVERSION=`$OCAMLOPTDOTOPT -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
+ if test "$TMPVERSION" != "$OCAMLVERSION" ; then
+ AC_MSG_RESULT([version differs from ocamlc; ocamlopt.opt discarded.])
+ else
+ OCAMLOPT=$OCAMLOPTDOTOPT
+ fi
+ fi
+ fi
+
+ AC_SUBST([OCAMLOPT])
+ fi
+
+ AC_SUBST([OCAMLC])
+
+ # checking for ocamldep
+ AC_CHECK_TOOL([OCAMLDEP],[ocamldep],[no])
+
+ # checking for ocamlmktop
+ AC_CHECK_TOOL([OCAMLMKTOP],[ocamlmktop],[no])
+
+ # checking for ocamlmklib
+ AC_CHECK_TOOL([OCAMLMKLIB],[ocamlmklib],[no])
+
+ # checking for ocamldoc
+ AC_CHECK_TOOL([OCAMLDOC],[ocamldoc],[no])
+
+ # checking for ocamlbuild
+ AC_CHECK_TOOL([OCAMLBUILD],[ocamlbuild],[no])
+])
+
+
+AC_DEFUN([AC_PROG_OCAMLLEX],
+[dnl
+ # checking for ocamllex
+ AC_CHECK_TOOL([OCAMLLEX],[ocamllex],[no])
+ if test "$OCAMLLEX" != "no"; then
+ AC_CHECK_TOOL([OCAMLLEXDOTOPT],[ocamllex.opt],[no])
+ if test "$OCAMLLEXDOTOPT" != "no"; then
+ OCAMLLEX=$OCAMLLEXDOTOPT
+ fi
+ fi
+ AC_SUBST([OCAMLLEX])
+])
+
+AC_DEFUN([AC_PROG_OCAMLYACC],
+[dnl
+ AC_CHECK_TOOL([OCAMLYACC],[ocamlyacc],[no])
+ AC_SUBST([OCAMLYACC])
+])
+
+
+AC_DEFUN([AC_PROG_CAMLP4],
+[dnl
+ AC_REQUIRE([AC_PROG_OCAML])dnl
+
+ # checking for camlp4
+ AC_CHECK_TOOL([CAMLP4],[camlp4],[no])
+ if test "$CAMLP4" != "no"; then
+ TMPVERSION=`$CAMLP4 -v 2>&1| sed -n -e 's|.*version *\(.*\)$|\1|p'`
+ if test "$TMPVERSION" != "$OCAMLVERSION" ; then
+ AC_MSG_RESULT([versions differs from ocamlc])
+ CAMLP4=no
+ fi
+ fi
+ AC_SUBST([CAMLP4])
+
+ # checking for companion tools
+ AC_CHECK_TOOL([CAMLP4BOOT],[camlp4boot],[no])
+ AC_CHECK_TOOL([CAMLP4O],[camlp4o],[no])
+ AC_CHECK_TOOL([CAMLP4OF],[camlp4of],[no])
+ AC_CHECK_TOOL([CAMLP4OOF],[camlp4oof],[no])
+ AC_CHECK_TOOL([CAMLP4ORF],[camlp4orf],[no])
+ AC_CHECK_TOOL([CAMLP4PROF],[camlp4prof],[no])
+ AC_CHECK_TOOL([CAMLP4R],[camlp4r],[no])
+ AC_CHECK_TOOL([CAMLP4RF],[camlp4rf],[no])
+ AC_SUBST([CAMLP4BOOT])
+ AC_SUBST([CAMLP4O])
+ AC_SUBST([CAMLP4OF])
+ AC_SUBST([CAMLP4OOF])
+ AC_SUBST([CAMLP4ORF])
+ AC_SUBST([CAMLP4PROF])
+ AC_SUBST([CAMLP4R])
+ AC_SUBST([CAMLP4RF])
+])
+
+
+AC_DEFUN([AC_PROG_FINDLIB],
+[dnl
+ AC_REQUIRE([AC_PROG_OCAML])dnl
+
+ # checking for ocamlfind
+ AC_CHECK_TOOL([OCAMLFIND],[ocamlfind],[no])
+ AC_SUBST([OCAMLFIND])
+])
+
+
+dnl Thanks to Jim Meyering for working this next bit out for us.
+dnl XXX We should define AS_TR_SH if it's not defined already
+dnl (eg. for old autoconf).
+AC_DEFUN([AC_CHECK_OCAML_PKG],
+[dnl
+ AC_REQUIRE([AC_PROG_FINDLIB])dnl
+
+ AC_MSG_CHECKING([for OCaml findlib package $1])
+
+ unset found
+ unset pkg
+ found=no
+ for pkg in $1 $2 ; do
+ if $OCAMLFIND query $pkg >/dev/null 2>/dev/null; then
+ AC_MSG_RESULT([found])
+ AS_TR_SH([OCAML_PKG_$1])=$pkg
+ found=yes
+ break
+ fi
+ done
+ if test "$found" = "no" ; then
+ AC_MSG_RESULT([not found])
+ AS_TR_SH([OCAML_PKG_$1])=no
+ fi
+
+ AC_SUBST(AS_TR_SH([OCAML_PKG_$1]))
+])
+
+
+AC_DEFUN([AC_CHECK_OCAML_MODULE],
+[dnl
+ AC_MSG_CHECKING([for OCaml module $2])
+
+ cat > conftest.ml <<EOF
+open $3
+EOF
+ unset found
+ for $1 in $$1 $4 ; do
+ if $OCAMLC -c -I "$$1" conftest.ml >&5 2>&5 ; then
+ found=yes
+ break
+ fi
+ done
+
+ if test "$found" ; then
+ AC_MSG_RESULT([$$1])
+ else
+ AC_MSG_RESULT([not found])
+ $1=no
+ fi
+ AC_SUBST([$1])
+])
+
+
+dnl XXX Cross-compiling
+AC_DEFUN([AC_CHECK_OCAML_WORD_SIZE],
+[dnl
+ AC_MSG_CHECKING([for OCaml compiler word size])
+ cat > conftest.ml <<EOF
+ print_endline (string_of_int Sys.word_size)
+ EOF
+ OCAML_WORD_SIZE=`ocaml conftest.ml`
+ AC_MSG_RESULT([$OCAML_WORD_SIZE])
+ AC_SUBST([OCAML_WORD_SIZE])
+])
--- /dev/null
+# Goalfile parser
+# Copyright (C) 2019 Richard W.M. Jones
+# Copyright (C) 2019 Red Hat Inc.
+#
+# This program is free software; you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License along
+# with this program; if not, write to the Free Software Foundation, Inc.,
+# 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+
+let objects = ["ast.cmx", "parser.cmx", "lexer.cmx", "main.cmx"]
+
+goal all = : file("goals")
+
+goal clean = {
+ rm -f *~
+ rm -f *.cmi *.cmo *.cmx *.o
+ rm -f parser.ml parser.mli lexer.ml parser.conflicts
+ rm -f goals
+}
+
+file("goals"): objects {
+ @OCAMLFIND@ opt %^ -o %@
+}
+
+let OCAMLFLAGS = "-g -safe-string -warn-error CDEFLMPSUVYZX+52-3"
+
+goal compile_cmi (name) = "%name.cmi": "%name.mli" {
+ @OCAMLFIND@ c %OCAMLFLAGS -c %< -o %@
+}
+goal compile_cmo (name) = "%name.cmo": "%name.ml" {
+ @OCAMLFIND@ c %OCAMLFLAGS -c %< -o %@
+}
+goal compile_cmx (name) = "%name.cmx": "%name.ml" {
+ @OCAMLFIND@ opt %OCAMLFLAGS -c %< -o %@
+}
+
+"parser.ml", "parser.mli": "parser.mly" {
+ @MENHIR@ --explain %<
+}
+
+"lexer.ml": "lexer.mll", "lexer.cmi", "parser.ml" {
+ @OCAMLLEX@ %<
+}
+
+# depend: .depend
+
+# .depend: parser.mly lexer.mll *.mli
+# rm -f $@ $@-t
+# @MENHIR@ --depend parser.mly > $@-t
+# ocamldep lexer.mll *.mli >> $@-t
+# mv $@-t $@
+
+# -include .depend
+
+# .PHONY: all clean depend
--- /dev/null
+# Goalfile parser
+# Copyright (C) 2019 Richard W.M. Jones
+# Copyright (C) 2019 Red Hat Inc.
+#
+# This program is free software; you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License along
+# with this program; if not, write to the Free Software Foundation, Inc.,
+# 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+
+OBJECTS = ast.cmx parser.cmx lexer.cmx main.cmx
+
+all: goals
+
+clean:
+ rm -f *~
+ rm -f *.cmi *.cmo *.cmx *.o
+ rm -f parser.ml parser.mli lexer.ml parser.conflicts stamp-parser
+ rm -f goals
+
+goals: $(OBJECTS)
+ @OCAMLFIND@ opt $^ -o $@
+
+OCAMLFLAGS = -g -safe-string -warn-error CDEFLMPSUVYZX+52-3
+
+%.cmi: %.mli
+ @OCAMLFIND@ c $(OCAMLFLAGS) -c $< -o $@
+%.cmo: %.ml
+ @OCAMLFIND@ c $(OCAMLFLAGS) -c $< -o $@
+%.cmx: %.ml
+ @OCAMLFIND@ opt $(OCAMLFLAGS) -c $< -o $@
+
+parser.ml parser.mli: stamp-parser
+stamp-parser: parser.mly
+ @MENHIR@ --explain $<
+ touch $@
+
+lexer.ml: lexer.mll lexer.cmi parser.ml
+ @OCAMLLEX@ $<
+
+depend: .depend
+
+.depend: parser.mly lexer.mll *.mli
+ rm -f $@ $@-t
+ @MENHIR@ --depend parser.mly > $@-t
+ ocamldep lexer.mll *.ml *.mli >> $@-t
+ mv $@-t $@
+
+-include .depend
+
+Makefile: Makefile.in ../config.status
+ ../config.status Makefile
+
+.PHONY: all clean depend
+
+# Doesn't build all *.cmi files before *.cmo/cmx files:
+#.NOTPARALLEL:
--- /dev/null
+(* Goalfile Abstract Syntax Tree
+ * Copyright (C) 2019 Richard W.M. Jones
+ * Copyright (C) 2019 Red Hat Inc.
+ *
+ * This program is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation; either version 2 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License along
+ * with this program; if not, write to the Free Software Foundation, Inc.,
+ * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+ *)
+
+open Printf
+
+type file = stmt list
+and stmt =
+ | Let of id * expr
+ | Goal of id * id list * pattern list * expr list * code option
+and pattern =
+ | PTactic of id * substs list
+ | PVarSubst of id
+and expr =
+ | ECall of id * expr list
+ | EVar of id
+ | EString of substs
+ | EList of expr list
+and id = string
+and code = substs
+and substs = subst list
+and subst =
+ | SString of string
+ | SVar of id
+
+module Substs = struct
+ type t = {
+ mutable elems : subst list; (* built in reverse order *)
+ curr : Buffer.t; (* current string *)
+ }
+
+ let create () = { elems = []; curr = Buffer.create 13 }
+
+ let finalize t =
+ if Buffer.length t.curr > 0 then
+ t.elems <- SString (Buffer.contents t.curr) :: t.elems;
+ Buffer.clear t.curr
+
+ let get t = finalize t; List.rev t.elems
+
+ let add_char { curr } = Buffer.add_char curr
+ let add_string { curr} = Buffer.add_string curr
+ let add_var t id = finalize t; t.elems <- SVar id :: t.elems
+end
+
+let iter_with_commas
+ : out_channel -> (out_channel -> 'a -> unit) -> 'a list -> unit =
+ fun fp f xs ->
+ let comma = ref false in
+ List.iter (
+ fun x ->
+ if !comma then fprintf fp ", ";
+ comma := true;
+ f fp x
+ ) xs
+
+let rec print_file fp file =
+ List.iter (print_stmt fp) file
+
+and print_stmt fp = function
+ | Let (name, expr) ->
+ fprintf fp "let %s = " name;
+ print_expr fp expr;
+ fprintf fp "\n"
+ | Goal (name, params, patterns, exprs, code) ->
+ fprintf fp "goal %s (%s) =\n" name (String.concat ", " params);
+ fprintf fp " ";
+ iter_with_commas fp print_pattern patterns;
+ fprintf fp " : ";
+ iter_with_commas fp print_expr exprs;
+ (match code with
+ | None -> ()
+ | Some code ->
+ fprintf fp " {\n";
+ print_code fp code;
+ fprintf fp "\n }"
+ );
+ fprintf fp "\n"
+
+and print_pattern fp = function
+ | PTactic (name, params) ->
+ fprintf fp "%s (" name;
+ iter_with_commas fp print_substs params;
+ fprintf fp ")"
+ | PVarSubst id -> print_id fp id
+
+and print_expr fp = function
+ | ECall (name, params) ->
+ fprintf fp "%s (" name;
+ iter_with_commas fp print_expr params;
+ fprintf fp ")"
+ | EVar var -> print_id fp var
+ | EString s -> print_substs fp s;
+ | EList xs ->
+ fprintf fp "[";
+ iter_with_commas fp print_expr xs;
+ fprintf fp "]"
+
+and print_id = output_string
+
+and print_substs fp xs =
+ let xs =
+ List.map (
+ function
+ | SString s -> sprintf "%S" s
+ | SVar id -> id
+ ) xs in
+ fprintf fp "%s" (String.concat "+" xs)
+
+and print_code fp xs =
+ List.iter (
+ function
+ | SString s -> fprintf fp "%s" s
+ | SVar id -> fprintf fp "%%%s" id
+ ) xs
--- /dev/null
+(* Goalfile Abstract Syntax Tree
+ * Copyright (C) 2019 Richard W.M. Jones
+ * Copyright (C) 2019 Red Hat Inc.
+ *
+ * This program is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation; either version 2 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License along
+ * with this program; if not, write to the Free Software Foundation, Inc.,
+ * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+ *)
+
+type file = stmt list
+and stmt =
+ (* let id = expr *)
+ | Let of id * expr
+ (* goal id (params) = patterns : exprs = code *)
+ | Goal of id * id list * pattern list * expr list * code option
+and pattern =
+ (* match tactic such as file ("filename") *)
+ | PTactic of id * substs list
+ (* match named variable, which must be a string or list *)
+ | PVarSubst of id
+and expr =
+ (* goalname (params), tactic (params) etc. *)
+ | ECall of id * expr list
+ (* variable *)
+ | EVar of id
+ (* string with %-substitutions *)
+ | EString of substs
+ (* list *)
+ | EList of expr list
+and id = string
+and code = substs
+and substs = subst list
+and subst =
+ (* String literal part. *)
+ | SString of string
+ (* %-substitution. *)
+ | SVar of id
+
+(* This is used for incrementally building Ast.substs in the parser. *)
+module Substs : sig
+ type t
+ val create : unit -> t
+ val get : t -> substs
+ val add_char : t -> char -> unit
+ val add_string : t -> string -> unit
+ val add_var : t -> string -> unit
+end
+
+val print_file : out_channel -> file -> unit
--- /dev/null
+(* Goalfile lexer
+ * Copyright (C) 2019 Richard W.M. Jones
+ * Copyright (C) 2019 Red Hat Inc.
+ *
+ * This program is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation; either version 2 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License along
+ * with this program; if not, write to the Free Software Foundation, Inc.,
+ * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+ *)
+
+exception SyntaxError of string
+
+val read : Lexing.lexbuf -> Parser.token
--- /dev/null
+(* Goalfile lexer
+ * Copyright (C) 2019 Richard W.M. Jones
+ * Copyright (C) 2019 Red Hat Inc.
+ *
+ * This program is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation; either version 2 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License along
+ * with this program; if not, write to the Free Software Foundation, Inc.,
+ * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+ *)
+
+{
+open Lexing
+open Parser
+
+open Printf
+
+exception SyntaxError of string
+
+let new_line lexbuf =
+ let pos = lexbuf.lex_curr_p in
+ lexbuf.lex_curr_p <-
+ { pos with pos_bol = lexbuf.lex_curr_pos; pos_lnum = pos.pos_lnum + 1 }
+}
+
+let white = [' ' '\t']+
+let newline = '\r' | '\n' | "\r\n"
+let comment = '#' (_#'\n')*
+let id = ['a'-'z' 'A'-'Z' '_'] ['a'-'z' 'A'-'Z' '0'-'9' '_']*
+
+rule read =
+ parse
+ | white
+ | comment { read lexbuf }
+ | newline { new_line lexbuf; read lexbuf }
+ | "," { COMMA }
+ | ":" { COLON }
+ | "=" { EQUALS }
+ | "(" { LEFT_PAREN }
+ | ")" { RIGHT_PAREN }
+ | "[" { LEFT_ARRAY }
+ | "]" { RIGHT_ARRAY }
+ | '"' { read_string (Ast.Substs.create ()) lexbuf }
+ | "{" { read_code (Ast.Substs.create ()) (ref 1) lexbuf }
+ | "goal" { GOAL }
+ | "let" { LET }
+ | id { ID (Lexing.lexeme lexbuf) }
+ | _ { raise (SyntaxError ("unexpected character: " ^
+ Lexing.lexeme lexbuf)) }
+ | eof { EOF }
+
+(* Parse "STRING" literal with %-substitutions. *)
+and read_string buf =
+ parse
+ | '\\' '"'
+ { Ast.Substs.add_char buf '"'; read_string buf lexbuf }
+ | '\\' 'a'
+ { Ast.Substs.add_char buf '\007'; read_string buf lexbuf }
+ | '\\' 'b'
+ { Ast.Substs.add_char buf '\008'; read_string buf lexbuf }
+ | '\\' 't'
+ { Ast.Substs.add_char buf '\009'; read_string buf lexbuf }
+ | '\\' 'n'
+ { Ast.Substs.add_char buf '\010'; read_string buf lexbuf }
+ | '\\' 'v'
+ { Ast.Substs.add_char buf '\011'; read_string buf lexbuf }
+ | '\\' 'f'
+ { Ast.Substs.add_char buf '\012'; read_string buf lexbuf }
+ | '\\' 'r'
+ { Ast.Substs.add_char buf '\013'; read_string buf lexbuf }
+ | '\\' '\\'
+ { Ast.Substs.add_char buf '\\'; read_string buf lexbuf }
+ | '"' { STRING (Ast.Substs.get buf) }
+ | newline { Ast.Substs.add_char buf '\n';
+ new_line lexbuf; read_string buf lexbuf }
+ | '%' '%' { Ast.Substs.add_char buf '%'; read_string buf lexbuf }
+ | '%' id { let id = Lexing.lexeme lexbuf in
+ let len = String.length id in
+ Ast.Substs.add_var buf (String.sub id 1 (len-1));
+ read_string buf lexbuf }
+ | '%' _ { raise (SyntaxError ("illegal character in %-substitution: " ^
+ Lexing.lexeme lexbuf)) }
+ | [^ '"' '\\' '\r' '\n' '%' ]+
+ { Ast.Substs.add_string buf (Lexing.lexeme lexbuf);
+ read_string buf lexbuf }
+ | _ { raise (SyntaxError ("illegal character in string: " ^
+ Lexing.lexeme lexbuf)) }
+ | eof { raise (SyntaxError ("unterminated string")) }
+
+(* Parse { CODE } literal with %-substitutions.
+ *
+ * Note the range of %-substitutions possible is larger than
+ * for strings.
+ *)
+and read_code buf level =
+ parse
+ | '{' { incr level; read_code buf level lexbuf }
+ | '}' { decr level;
+ if !level = 0 then CODE (Ast.Substs.get buf)
+ else (
+ Ast.Substs.add_char buf '}';
+ read_code buf level lexbuf
+ ) }
+ | newline { Ast.Substs.add_char buf '\n';
+ new_line lexbuf; read_code buf level lexbuf }
+ | '%' '%' { Ast.Substs.add_char buf '%'; read_code buf level lexbuf }
+ | '%' '@' { Ast.Substs.add_var buf "@"; read_code buf level lexbuf }
+ | '%' '<' { Ast.Substs.add_var buf "<"; read_code buf level lexbuf }
+ | '%' '^' { Ast.Substs.add_var buf "^"; read_code buf level lexbuf }
+ | '%' id { let id = Lexing.lexeme lexbuf in
+ let len = String.length id in
+ Ast.Substs.add_var buf (String.sub id 1 (len-1));
+ read_code buf level lexbuf }
+ | '%' _ { raise (SyntaxError ("illegal character in %-substitution: " ^
+ Lexing.lexeme lexbuf)) }
+ | [^ '{' '}' '\r' '\n' '%' ]+
+ { Ast.Substs.add_string buf (Lexing.lexeme lexbuf);
+ read_code buf level lexbuf }
+ | _ { raise (SyntaxError ("illegal character in code section: " ^
+ Lexing.lexeme lexbuf)) }
+ | eof { raise (SyntaxError ("unterminated code section")) }
--- /dev/null
+(* Goalfile parser
+ * Copyright (C) 2019 Richard W.M. Jones
+ * Copyright (C) 2019 Red Hat Inc.
+ *
+ * This program is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation; either version 2 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License along
+ * with this program; if not, write to the Free Software Foundation, Inc.,
+ * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+ *)
+
+open Lexer
+open Lexing
+
+open Printf
+
+let parse lexbuf =
+ let print_position fp lexbuf =
+ let pos = lexbuf.lex_curr_p in
+ fprintf fp "%s:%d:%d"
+ pos.pos_fname pos.pos_lnum (pos.pos_cnum - pos.pos_bol)
+ in
+
+ try Parser.file Lexer.read lexbuf
+ with
+ | SyntaxError msg ->
+ eprintf "%a: %s\n" print_position lexbuf msg;
+ exit 1
+ | Parser.Error ->
+ eprintf "%a: parse error\n" print_position lexbuf;
+ exit 1
+
+let () =
+ let filename = "Goalfile" in
+ let fp = open_in filename in
+ let lexbuf = Lexing.from_channel fp in
+ lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = filename };
+ let file : Ast.file = parse lexbuf in
+ close_in fp;
+
+ Ast.print_file stdout file
--- /dev/null
+(* Goalfile parser
+ * Copyright (C) 2019 Richard W.M. Jones
+ * Copyright (C) 2019 Red Hat Inc.
+ *
+ * This program is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation; either version 2 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License along
+ * with this program; if not, write to the Free Software Foundation, Inc.,
+ * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+ *)
+
+%{
+open Printf
+%}
+
+(* Tokens. *)
+%token <Ast.substs> CODE
+%token COLON
+%token COMMA
+%token <string> ID
+%token EQUALS
+%token EOF
+%token GOAL
+%token LEFT_ARRAY
+%token LEFT_PAREN
+%token LET
+%token RIGHT_ARRAY
+%token RIGHT_PAREN
+%token <Ast.substs> STRING
+
+%type <Ast.expr> expr
+%type <Ast.stmt> stmt
+
+(* Start non-terminal. *)
+%start <Ast.file> file
+%%
+
+file:
+ | stmts EOF { $1 }
+ ;
+
+stmts:
+ | list(stmt) { $1 }
+ ;
+stmt:
+ | option(goal_stmt) patterns COLON barelist option(CODE)
+ { let name, params =
+ match $1 with
+ | None ->
+ let pos = $startpos in
+ sprintf "_goal@%d" pos.pos_lnum, []
+ | Some x -> x in
+ Ast.Goal (name, params, $2, $4, $5)
+ }
+ | goal_stmt CODE
+ {
+ let name, params = $1 in
+ Ast.Goal (name, params, [], [], Some $2)
+ }
+ | LET ID EQUALS expr { Ast.Let ($2, $4) }
+ ;
+
+goal_stmt:
+ | GOAL ID option(param_decl) EQUALS
+ { $2, match $3 with None -> [] | Some ps -> ps }
+ ;
+param_decl:
+ | LEFT_PAREN separated_list(COMMA, ID) RIGHT_PAREN { $2 }
+ ;
+
+patterns:
+ | separated_list(COMMA, pattern) { $1 }
+ ;
+pattern:
+ | STRING { Ast.PTactic ("file", [$1]) }
+ | ID pattern_params { Ast.PTactic ($1, $2) }
+ | ID { Ast.PVarSubst $1 }
+ ;
+pattern_params:
+ | LEFT_PAREN separated_list(COMMA, pattern_param) RIGHT_PAREN { $2 }
+ ;
+pattern_param:
+ | STRING { $1 }
+ ;
+
+expr:
+ | ID params { Ast.ECall ($1, $2) }
+ | ID { Ast.EVar $1 (* This might be replaced with ECall later. *) }
+ | STRING { Ast.EString $1 }
+ | LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList $2 }
+ ;
+barelist:
+ | separated_list(COMMA, expr) { $1 }
+ ;
+params:
+ | LEFT_PAREN separated_list(COMMA, expr) RIGHT_PAREN { $2 }
+ ;
git.annexia.org / goals.git / commitdiff