diff --git a/Dedukti/Driver/Batch.hs b/Dedukti/Driver/Batch.hs --- a/Dedukti/Driver/Batch.hs +++ b/Dedukti/Driver/Batch.hs @@ -59,22 +59,22 @@ -- Now that we have the dependencies of the module, we can enounce a few -- build rules concerning the module. g mod ds compile = let capitalize x = toUpper (head x) : tail x - eu = srcPathFromModule mod - euo = objPathFromModule mod - eui = ifacePathFromModule mod + dk = srcPathFromModule mod + dko = objPathFromModule mod + dki = ifacePathFromModule mod hi = pathFromModule ".hi" mod chi = capitalize hi o = pathFromModule ".o" mod dephis = map (capitalize . pathFromModule ".hi") ds - in [ Rule eu [] Nothing cmp - , Rule euo [eu] (Just compile) cmp - , Rule eui [eu] (Just compile) cmp - , Rule hi (euo:eui:dephis) (Just $ task_hscomp euo) cmp - , Rule o (euo:eui:dephis) (Just $ task_hscomp euo) cmp + in [ Rule dk [] Nothing cmp + , Rule dko [dk] (Just compile) cmp + , Rule dki [dk] (Just compile) cmp + , Rule hi (dko:dki:dephis) (Just $ task_hscomp dko) cmp + , Rule o (dko:dki:dephis) (Just $ task_hscomp dko) cmp , Rule chi [hi] (Just $ task_himv hi chi) cmp ] - task_hscomp euo _ = do + task_hscomp dko _ = do hscomp <- parameter Config.hsCompiler - io . IO.testExitCode =<< command hscomp [ "-c", "-w", "-x", "hs", euo + io . IO.testExitCode =<< command hscomp [ "-c", "-w", "-x", "hs", dko , "-XOverloadedStrings" , "-XPatternGuards" ] -- GHC won't find the interface files if their names don't start with a diff --git a/Dedukti/Module.hs b/Dedukti/Module.hs --- a/Dedukti/Module.hs +++ b/Dedukti/Module.hs @@ -66,13 +66,13 @@ hierarchy . map (T.pack . check) . splitDirectories . dropExtension srcPathFromModule :: MName -> FilePath -srcPathFromModule = pathFromModule ".eu" +srcPathFromModule = pathFromModule ".dk" objPathFromModule :: MName -> FilePath -objPathFromModule = pathFromModule ".euo" +objPathFromModule = pathFromModule ".dko" ifacePathFromModule :: MName -> FilePath -ifacePathFromModule = pathFromModule ".eui" +ifacePathFromModule = pathFromModule ".dki" -- | The datatype of qualified names. data Qid = Qid { qid_qualifier :: !Hierarchy diff --git a/dedukti.cabal b/dedukti.cabal --- a/dedukti.cabal +++ b/dedukti.cabal @@ -1,5 +1,5 @@ name: dedukti -version: 1.0.1 +version: 1.0.2 author: Mathieu Boespflug maintainer: Mathieu Boespflug copyright: © 2009 CNRS - École Polytechnique - INRIA @@ -30,6 +30,11 @@ t/nat.dk t/peano.dk t/plus.dk +extra-source-files: doc/mkfile + doc/manual.texi.in + doc/fdl.texi + doc/references.texi + scripts/dkrun executable dedukti diff --git a/doc/fdl.texi b/doc/fdl.texi new file mode 100644 --- /dev/null +++ b/doc/fdl.texi @@ -0,0 +1,506 @@ +@c The GNU Free Documentation License. +@center Version 1.3, 3 November 2008 + +@c This file is intended to be included within another document, +@c hence no sectioning command or @node. + +@display +Copyright @copyright{} 2000, 2001, 2002, 2007, 2008 Free Software Foundation, Inc. +@uref{http://fsf.org/} + +Everyone is permitted to copy and distribute verbatim copies +of this license document, but changing it is not allowed. +@end display + +@enumerate 0 +@item +PREAMBLE + +The purpose of this License is to make a manual, textbook, or other +functional and useful document @dfn{free} in the sense of freedom: to +assure everyone the effective freedom to copy and redistribute it, +with or without modifying it, either commercially or noncommercially. +Secondarily, this License preserves for the author and publisher a way +to get credit for their work, while not being considered responsible +for modifications made by others. + +This License is a kind of ``copyleft'', which means that derivative +works of the document must themselves be free in the same sense. It +complements the GNU General Public License, which is a copyleft +license designed for free software. + +We have designed this License in order to use it for manuals for free +software, because free software needs free documentation: a free +program should come with manuals providing the same freedoms that the +software does. But this License is not limited to software manuals; +it can be used for any textual work, regardless of subject matter or +whether it is published as a printed book. We recommend this License +principally for works whose purpose is instruction or reference. + +@item +APPLICABILITY AND DEFINITIONS + +This License applies to any manual or other work, in any medium, that +contains a notice placed by the copyright holder saying it can be +distributed under the terms of this License. Such a notice grants a +world-wide, royalty-free license, unlimited in duration, to use that +work under the conditions stated herein. The ``Document'', below, +refers to any such manual or work. Any member of the public is a +licensee, and is addressed as ``you''. You accept the license if you +copy, modify or distribute the work in a way requiring permission +under copyright law. + +A ``Modified Version'' of the Document means any work containing the +Document or a portion of it, either copied verbatim, or with +modifications and/or translated into another language. + +A ``Secondary Section'' is a named appendix or a front-matter section +of the Document that deals exclusively with the relationship of the +publishers or authors of the Document to the Document's overall +subject (or to related matters) and contains nothing that could fall +directly within that overall subject. (Thus, if the Document is in +part a textbook of mathematics, a Secondary Section may not explain +any mathematics.) The relationship could be a matter of historical +connection with the subject or with related matters, or of legal, +commercial, philosophical, ethical or political position regarding +them. + +The ``Invariant Sections'' are certain Secondary Sections whose titles +are designated, as being those of Invariant Sections, in the notice +that says that the Document is released under this License. If a +section does not fit the above definition of Secondary then it is not +allowed to be designated as Invariant. The Document may contain zero +Invariant Sections. If the Document does not identify any Invariant +Sections then there are none. + +The ``Cover Texts'' are certain short passages of text that are listed, +as Front-Cover Texts or Back-Cover Texts, in the notice that says that +the Document is released under this License. A Front-Cover Text may +be at most 5 words, and a Back-Cover Text may be at most 25 words. + +A ``Transparent'' copy of the Document means a machine-readable copy, +represented in a format whose specification is available to the +general public, that is suitable for revising the document +straightforwardly with generic text editors or (for images composed of +pixels) generic paint programs or (for drawings) some widely available +drawing editor, and that is suitable for input to text formatters or +for automatic translation to a variety of formats suitable for input +to text formatters. A copy made in an otherwise Transparent file +format whose markup, or absence of markup, has been arranged to thwart +or discourage subsequent modification by readers is not Transparent. +An image format is not Transparent if used for any substantial amount +of text. A copy that is not ``Transparent'' is called ``Opaque''. + +Examples of suitable formats for Transparent copies include plain +@sc{ascii} without markup, Texinfo input format, La@TeX{} input +format, @acronym{SGML} or @acronym{XML} using a publicly available +@acronym{DTD}, and standard-conforming simple @acronym{HTML}, +PostScript or @acronym{PDF} designed for human modification. Examples +of transparent image formats include @acronym{PNG}, @acronym{XCF} and +@acronym{JPG}. Opaque formats include proprietary formats that can be +read and edited only by proprietary word processors, @acronym{SGML} or +@acronym{XML} for which the @acronym{DTD} and/or processing tools are +not generally available, and the machine-generated @acronym{HTML}, +PostScript or @acronym{PDF} produced by some word processors for +output purposes only. + +The ``Title Page'' means, for a printed book, the title page itself, +plus such following pages as are needed to hold, legibly, the material +this License requires to appear in the title page. For works in +formats which do not have any title page as such, ``Title Page'' means +the text near the most prominent appearance of the work's title, +preceding the beginning of the body of the text. + +The ``publisher'' means any person or entity that distributes copies +of the Document to the public. + +A section ``Entitled XYZ'' means a named subunit of the Document whose +title either is precisely XYZ or contains XYZ in parentheses following +text that translates XYZ in another language. (Here XYZ stands for a +specific section name mentioned below, such as ``Acknowledgements'', +``Dedications'', ``Endorsements'', or ``History''.) To ``Preserve the Title'' +of such a section when you modify the Document means that it remains a +section ``Entitled XYZ'' according to this definition. + +The Document may include Warranty Disclaimers next to the notice which +states that this License applies to the Document. These Warranty +Disclaimers are considered to be included by reference in this +License, but only as regards disclaiming warranties: any other +implication that these Warranty Disclaimers may have is void and has +no effect on the meaning of this License. + +@item +VERBATIM COPYING + +You may copy and distribute the Document in any medium, either +commercially or noncommercially, provided that this License, the +copyright notices, and the license notice saying this License applies +to the Document are reproduced in all copies, and that you add no other +conditions whatsoever to those of this License. You may not use +technical measures to obstruct or control the reading or further +copying of the copies you make or distribute. However, you may accept +compensation in exchange for copies. If you distribute a large enough +number of copies you must also follow the conditions in section 3. + +You may also lend copies, under the same conditions stated above, and +you may publicly display copies. + +@item +COPYING IN QUANTITY + +If you publish printed copies (or copies in media that commonly have +printed covers) of the Document, numbering more than 100, and the +Document's license notice requires Cover Texts, you must enclose the +copies in covers that carry, clearly and legibly, all these Cover +Texts: Front-Cover Texts on the front cover, and Back-Cover Texts on +the back cover. Both covers must also clearly and legibly identify +you as the publisher of these copies. The front cover must present +the full title with all words of the title equally prominent and +visible. You may add other material on the covers in addition. +Copying with changes limited to the covers, as long as they preserve +the title of the Document and satisfy these conditions, can be treated +as verbatim copying in other respects. + +If the required texts for either cover are too voluminous to fit +legibly, you should put the first ones listed (as many as fit +reasonably) on the actual cover, and continue the rest onto adjacent +pages. + +If you publish or distribute Opaque copies of the Document numbering +more than 100, you must either include a machine-readable Transparent +copy along with each Opaque copy, or state in or with each Opaque copy +a computer-network location from which the general network-using +public has access to download using public-standard network protocols +a complete Transparent copy of the Document, free of added material. +If you use the latter option, you must take reasonably prudent steps, +when you begin distribution of Opaque copies in quantity, to ensure +that this Transparent copy will remain thus accessible at the stated +location until at least one year after the last time you distribute an +Opaque copy (directly or through your agents or retailers) of that +edition to the public. + +It is requested, but not required, that you contact the authors of the +Document well before redistributing any large number of copies, to give +them a chance to provide you with an updated version of the Document. + +@item +MODIFICATIONS + +You may copy and distribute a Modified Version of the Document under +the conditions of sections 2 and 3 above, provided that you release +the Modified Version under precisely this License, with the Modified +Version filling the role of the Document, thus licensing distribution +and modification of the Modified Version to whoever possesses a copy +of it. In addition, you must do these things in the Modified Version: + +@enumerate A +@item +Use in the Title Page (and on the covers, if any) a title distinct +from that of the Document, and from those of previous versions +(which should, if there were any, be listed in the History section +of the Document). You may use the same title as a previous version +if the original publisher of that version gives permission. + +@item +List on the Title Page, as authors, one or more persons or entities +responsible for authorship of the modifications in the Modified +Version, together with at least five of the principal authors of the +Document (all of its principal authors, if it has fewer than five), +unless they release you from this requirement. + +@item +State on the Title page the name of the publisher of the +Modified Version, as the publisher. + +@item +Preserve all the copyright notices of the Document. + +@item +Add an appropriate copyright notice for your modifications +adjacent to the other copyright notices. + +@item +Include, immediately after the copyright notices, a license notice +giving the public permission to use the Modified Version under the +terms of this License, in the form shown in the Addendum below. + +@item +Preserve in that license notice the full lists of Invariant Sections +and required Cover Texts given in the Document's license notice. + +@item +Include an unaltered copy of this License. + +@item +Preserve the section Entitled ``History'', Preserve its Title, and add +to it an item stating at least the title, year, new authors, and +publisher of the Modified Version as given on the Title Page. If +there is no section Entitled ``History'' in the Document, create one +stating the title, year, authors, and publisher of the Document as +given on its Title Page, then add an item describing the Modified +Version as stated in the previous sentence. + +@item +Preserve the network location, if any, given in the Document for +public access to a Transparent copy of the Document, and likewise +the network locations given in the Document for previous versions +it was based on. These may be placed in the ``History'' section. +You may omit a network location for a work that was published at +least four years before the Document itself, or if the original +publisher of the version it refers to gives permission. + +@item +For any section Entitled ``Acknowledgements'' or ``Dedications'', Preserve +the Title of the section, and preserve in the section all the +substance and tone of each of the contributor acknowledgements and/or +dedications given therein. + +@item +Preserve all the Invariant Sections of the Document, +unaltered in their text and in their titles. Section numbers +or the equivalent are not considered part of the section titles. + +@item +Delete any section Entitled ``Endorsements''. Such a section +may not be included in the Modified Version. + +@item +Do not retitle any existing section to be Entitled ``Endorsements'' or +to conflict in title with any Invariant Section. + +@item +Preserve any Warranty Disclaimers. +@end enumerate + +If the Modified Version includes new front-matter sections or +appendices that qualify as Secondary Sections and contain no material +copied from the Document, you may at your option designate some or all +of these sections as invariant. To do this, add their titles to the +list of Invariant Sections in the Modified Version's license notice. +These titles must be distinct from any other section titles. + +You may add a section Entitled ``Endorsements'', provided it contains +nothing but endorsements of your Modified Version by various +parties---for example, statements of peer review or that the text has +been approved by an organization as the authoritative definition of a +standard. + +You may add a passage of up to five words as a Front-Cover Text, and a +passage of up to 25 words as a Back-Cover Text, to the end of the list +of Cover Texts in the Modified Version. Only one passage of +Front-Cover Text and one of Back-Cover Text may be added by (or +through arrangements made by) any one entity. If the Document already +includes a cover text for the same cover, previously added by you or +by arrangement made by the same entity you are acting on behalf of, +you may not add another; but you may replace the old one, on explicit +permission from the previous publisher that added the old one. + +The author(s) and publisher(s) of the Document do not by this License +give permission to use their names for publicity for or to assert or +imply endorsement of any Modified Version. + +@item +COMBINING DOCUMENTS + +You may combine the Document with other documents released under this +License, under the terms defined in section 4 above for modified +versions, provided that you include in the combination all of the +Invariant Sections of all of the original documents, unmodified, and +list them all as Invariant Sections of your combined work in its +license notice, and that you preserve all their Warranty Disclaimers. + +The combined work need only contain one copy of this License, and +multiple identical Invariant Sections may be replaced with a single +copy. If there are multiple Invariant Sections with the same name but +different contents, make the title of each such section unique by +adding at the end of it, in parentheses, the name of the original +author or publisher of that section if known, or else a unique number. +Make the same adjustment to the section titles in the list of +Invariant Sections in the license notice of the combined work. + +In the combination, you must combine any sections Entitled ``History'' +in the various original documents, forming one section Entitled +``History''; likewise combine any sections Entitled ``Acknowledgements'', +and any sections Entitled ``Dedications''. You must delete all +sections Entitled ``Endorsements.'' + +@item +COLLECTIONS OF DOCUMENTS + +You may make a collection consisting of the Document and other documents +released under this License, and replace the individual copies of this +License in the various documents with a single copy that is included in +the collection, provided that you follow the rules of this License for +verbatim copying of each of the documents in all other respects. + +You may extract a single document from such a collection, and distribute +it individually under this License, provided you insert a copy of this +License into the extracted document, and follow this License in all +other respects regarding verbatim copying of that document. + +@item +AGGREGATION WITH INDEPENDENT WORKS + +A compilation of the Document or its derivatives with other separate +and independent documents or works, in or on a volume of a storage or +distribution medium, is called an ``aggregate'' if the copyright +resulting from the compilation is not used to limit the legal rights +of the compilation's users beyond what the individual works permit. +When the Document is included in an aggregate, this License does not +apply to the other works in the aggregate which are not themselves +derivative works of the Document. + +If the Cover Text requirement of section 3 is applicable to these +copies of the Document, then if the Document is less than one half of +the entire aggregate, the Document's Cover Texts may be placed on +covers that bracket the Document within the aggregate, or the +electronic equivalent of covers if the Document is in electronic form. +Otherwise they must appear on printed covers that bracket the whole +aggregate. + +@item +TRANSLATION + +Translation is considered a kind of modification, so you may +distribute translations of the Document under the terms of section 4. +Replacing Invariant Sections with translations requires special +permission from their copyright holders, but you may include +translations of some or all Invariant Sections in addition to the +original versions of these Invariant Sections. You may include a +translation of this License, and all the license notices in the +Document, and any Warranty Disclaimers, provided that you also include +the original English version of this License and the original versions +of those notices and disclaimers. In case of a disagreement between +the translation and the original version of this License or a notice +or disclaimer, the original version will prevail. + +If a section in the Document is Entitled ``Acknowledgements'', +``Dedications'', or ``History'', the requirement (section 4) to Preserve +its Title (section 1) will typically require changing the actual +title. + +@item +TERMINATION + +You may not copy, modify, sublicense, or distribute the Document +except as expressly provided under this License. Any attempt +otherwise to copy, modify, sublicense, or distribute it is void, and +will automatically terminate your rights under this License. + +However, if you cease all violation of this License, then your license +from a particular copyright holder is reinstated (a) provisionally, +unless and until the copyright holder explicitly and finally +terminates your license, and (b) permanently, if the copyright holder +fails to notify you of the violation by some reasonable means prior to +60 days after the cessation. + +Moreover, your license from a particular copyright holder is +reinstated permanently if the copyright holder notifies you of the +violation by some reasonable means, this is the first time you have +received notice of violation of this License (for any work) from that +copyright holder, and you cure the violation prior to 30 days after +your receipt of the notice. + +Termination of your rights under this section does not terminate the +licenses of parties who have received copies or rights from you under +this License. If your rights have been terminated and not permanently +reinstated, receipt of a copy of some or all of the same material does +not give you any rights to use it. + +@item +FUTURE REVISIONS OF THIS LICENSE + +The Free Software Foundation may publish new, revised versions +of the GNU Free Documentation 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. See +@uref{http://www.gnu.org/copyleft/}. + +Each version of the License is given a distinguishing version number. +If the Document specifies that a particular numbered version of this +License ``or any later version'' applies to it, you have the option of +following the terms and conditions either of that specified version or +of any later version that has been published (not as a draft) by the +Free Software Foundation. If the Document does not specify a version +number of this License, you may choose any version ever published (not +as a draft) by the Free Software Foundation. If the Document +specifies that a proxy can decide which future versions of this +License can be used, that proxy's public statement of acceptance of a +version permanently authorizes you to choose that version for the +Document. + +@item +RELICENSING + +``Massive Multiauthor Collaboration Site'' (or ``MMC Site'') means any +World Wide Web server that publishes copyrightable works and also +provides prominent facilities for anybody to edit those works. A +public wiki that anybody can edit is an example of such a server. A +``Massive Multiauthor Collaboration'' (or ``MMC'') contained in the +site means any set of copyrightable works thus published on the MMC +site. + +``CC-BY-SA'' means the Creative Commons Attribution-Share Alike 3.0 +license published by Creative Commons Corporation, a not-for-profit +corporation with a principal place of business in San Francisco, +California, as well as future copyleft versions of that license +published by that same organization. + +``Incorporate'' means to publish or republish a Document, in whole or +in part, as part of another Document. + +An MMC is ``eligible for relicensing'' if it is licensed under this +License, and if all works that were first published under this License +somewhere other than this MMC, and subsequently incorporated in whole +or in part into the MMC, (1) had no cover texts or invariant sections, +and (2) were thus incorporated prior to November 1, 2008. + +The operator of an MMC Site may republish an MMC contained in the site +under CC-BY-SA on the same site at any time before August 1, 2009, +provided the MMC is eligible for relicensing. + +@end enumerate + +@page +@heading ADDENDUM: How to use this License for your documents + +To use this License in a document you have written, include a copy of +the License in the document and put the following copyright and +license notices just after the title page: + +@smallexample +@group + Copyright (C) @var{year} @var{your name}. + Permission is granted to copy, distribute and/or modify this document + under the terms of the GNU Free Documentation License, Version 1.3 + or any later version published by the Free Software Foundation; + with no Invariant Sections, no Front-Cover Texts, and no Back-Cover + Texts. A copy of the license is included in the section entitled ``GNU + Free Documentation License''. +@end group +@end smallexample + +If you have Invariant Sections, Front-Cover Texts and Back-Cover Texts, +replace the ``with@dots{}Texts.'' line with this: + +@smallexample +@group + with the Invariant Sections being @var{list their titles}, with + the Front-Cover Texts being @var{list}, and with the Back-Cover Texts + being @var{list}. +@end group +@end smallexample + +If you have Invariant Sections without Cover Texts, or some other +combination of the three, merge those two alternatives to suit the +situation. + +If your document contains nontrivial examples of program code, we +recommend releasing these examples in parallel under your choice of +free software license, such as the GNU General Public License, +to permit their use in free software. + +@c Local Variables: +@c ispell-local-pdict: "ispell-dict" +@c End: + diff --git a/doc/manual.texi.in b/doc/manual.texi.in new file mode 100644 --- /dev/null +++ b/doc/manual.texi.in @@ -0,0 +1,502 @@ +\input texinfo +@setfilename dedukti.info +@macro dkversion +esyscmd(awk '/^version:/{print $2}' ../dedukti.cabal)dnl +@end macro +@settitle Dedukti User's Guide, version @dkversion{} +@documentencoding UTF-8 +@afourpaper + +@copying +Copyright @copyright{} 2009 CNRS - École Polytechnique - INRIA. + +@quotation +Permission is granted to copy, distribute and/or modify this document +under the terms of the GNU Free Documentation License, Version 1.3 or +any later version published by the Free Software Foundation; with no +Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts. A +copy of the license is included in the section entitled ``Copying this +manual''. +@end quotation +@end copying + +@iftex +@macro lambdapi +@tex +$\\lambda\\Pi$% +@end tex +@end macro +@end iftex +@ifnottex +@macro lambdapi +λΠ +@end macro +@end ifnottex + +@defindex df + +@macro dindex {entry} +@dfindex \entry\ +@end macro + +@macro oindex {entry} +@dfindex Operator, @code{\entry\} +@end macro + +@synindex df cp +@syncodeindex fn cp + +@titlepage +@title Dedukti User's Guide +@subtitle Version @dkversion{} +@author Mathieu Boespflug (@email{mboes@@lix.polytechnique.fr}) +@page +@vskip 0pt plus 1filll +@insertcopying +@end titlepage + +@contents + +@node Top +@top The Dedukti proof checker + +This is the manual for Dedukti, version @dkversion{}. Dedukti is a proof checker +for the @lambdapi{}-calculus modulo. + +@menu +* Overview:: The general architecture. +* Installation:: How to install the Dedukti system. +* Dedukti syntax:: The input language for Dedukti. +* Invoking dedukti:: The compiler. +* Invoking dkrun:: Executing the proof checks. +* References:: Bibliographic references. +* Copying this manual:: How you can copy and share this manual. +* Index:: +@end menu + +@node Overview +@chapter Overview +@cindex architecture +@cindex overview +@cindex general usage + +@cindex @lambdapi{}-calculus modulo +The @lambdapi{}-calculus is a dependently typed lambda-calculus that +allows expressing proofs of minimal predicate logic through the +Brouwer-Heyting-Kolmogorov interpretation and the Curry-de Bruijn-Howard +correspondence. It can be extended in several ways to express proofs of +some theory. One way is to express the theory in Deduction modulo, i.e. +to orient the axioms as rewrite rules and to extend the +@lambdapi{}-calculus to express proofs in Deduction modulo. We get in +this way the @dfn{@lambdapi{}-calculus modulo}. + +Dedukti is a type checker for the @lambdapi{}-calculus modulo. + +The input is a series of source files that declare terms and define +rules. Checking these declarations with respect to the given rules is a +two step process. These source files are first compiled to object files. +The objects files for each source file are then linked together before +being executed to type check the rules and declarations of the input. + +As such the Dedukti system centers around two commands. @command{dedukti} +is the compiler that generates object files from source files +(@pxref{Invoking dedukti}). @command{dkrun} is the command that links all +object files together and executes the resulting program +(@pxref{Invoking dkrun}). + +@node Installation +@chapter Installation +@cindex configure +@cindex setup +@cindex install + +@cindex Cabal +@cindex Hackage +Dedukti uses the Cabal architecture for building and packaging +applications and libraries. + +@menu +* Local install:: Installing in your home directory. +* Global install:: Installing in the system directories. +* Building the documentation:: How to build the documentation. +@end menu + +@node Local install +@section Installing Dedukti locally + +If you have the @command{cabal} command part of the @code{cabal-install} +package, then you can obtain Dedukti from Hackage, configure and install +it all in one go: + +@example +$ cabal install dedukti --user +@end example + +@cindex Haskell Platform +@noindent +@code{cabal-install} is shipped as part of the Haskell +Platform@footnote{@uref{http://hackage.haskell.org/platform}}. +Alternatively, unpack the Dedukti source tarball and run + +@example +$ cabal configure --user +$ cabal build +$ cabal install +@end example + +You will have to satisfy dependencies by hand, if necessary. This will +install the Dedukti commands and other files under the Cabal hierarchy in +your home directory (typically @file{~/.cabal}). You will need to alter +your @env{PATH} appropriately to run these commands. + +@node Global install +@section Installing Dedukti globally + +If you have appropriate permissions, you can install Dedukti globally for +all users of the system. If you have the @command{cabal} command then +you can obtain Dedukti from Hackage, configure and install it all in one +go: + +@example +$ cabal install dedukti --global +@end example + +@noindent +Alternatively, unpack the Dedukti source tarball and run + +@example +$ cabal configure --global +$ cabal build +$ cabal install +@end example + +@node Building the documentation +@section Building the documentation + +If you prefer to have a local copy of this documentation, you can build +it from the @file{doc/} folder in the source distribution. The build +system is based on an @file{mkfile}, which plays the same role as +@command{make}'s @file{Makefile} but with a slightly different syntax +and simpler semantics. You can interpret @file{mkfile}'s using either +Plan 9's original mk +command@footnote{@uref{http://plan9.bell-labs.com/magic/man2html/1/mk}}, +or by using @command{hmk}, a Haskell clone of @command{mk} which is a +dependency of Dedukti. + +To build the pdf version of this manual: + +@example +$ cd doc +$ hmk pdf +@end example + +@noindent +To build the html version of this manual: + +@example +$ cd doc +$ hmk html +@end example + +The @command{hmk} command is part of the @file{hmk} Cabal package. It +may be found either somewhere in your global path, or in Cabal's user +folder, depending on the type of installation. You will also need a +POSIX compatible environment to build the documentation, including the +@command{m4} command to preprocess the texinfo source. + +@node Dedukti syntax +@chapter Dedukti syntax + +@menu +* Syntax overview:: An informal description of input files. +* Scoping rules:: The scope of declarations and rules. +* Grammar:: A formal specification of the syntax. +@end menu + +@node Syntax overview +@section A informal overview of the syntax + +@dindex module +@cindex top-level +@cindex source file +A Dedukti source file consists in a series of top-level declarations +rules, all terminated by a period. Each source file defines a +@dfn{module}. + +@subsection Declarations + +Declarations have the form + +@example +t : A. +@end example + +@noindent +where @code{t} is an identifier and @code{A} is a type. + +@anchor{Rules} +@subsection Rules + +@cindex rule environment +@cindex pattern +@dindex rule +@dindex rule head +@dindex head, of a rule +@cindex head constant +@oindex --> +Rules always start with an environment, followed by a head on the left +hand side and an expression on the right hand side of a long arrow. A +@dfn{rule head} consists of a head constant and zero or more patterns. +Here is an example: + +@example +S : nat. +O : nat. +[y : nat] plus O y --> y. +[x : nat, y : nat] plus (S x) y --> S (plus x y). +@end example + +@noindent +Two rules, each with two patterns in the head, are defined for the +constant @code{plus}. All variables in the pattern must appear in the +environment along with a type. All identifiers that are not mentioned in +the environment are considered constants, which must be in scope of +their declaration (@pxref{Scoping rules}). Here @code{O} and @code{S} +are constants declared earlier. The free variables in the right hand +side of the rule must be a subset of the pattern variables mentioned in +the left hand side. It is illegal to put variables in the rule +environment that are not also pattern variables in the left hand side of +the rule. + +A current limitation of the implementation imposes that rules for the +same head constant be defined contiguously and in the same module as the +declaration of the head constant. Another limitation is that all rules +must have same arity. That is, the head constant in each rule must be +followed by the same number of patterns. Both limitations may be lifted +in the future. + +@subsection Terms and types +@cindex term +@cindex sort +@cindex product +@cindex dependent product +@cindex variable + +@dindex term +@dindex type +@dindex dependent product +@dindex product +@dindex abstraction +@findex Type +@findex Kind +As in many dependently-typed languages, the @lambdapi{}-calculus modulo +unifies the syntax of terms and types. Nearly all terms have types and +those types are themselves terms. There are two special terms, +@code{Type} and @code{Kind}, which we refer to as @dfn{sorts}. In the +following, we will call @dfn{types} those terms whose type is a sort. + +A term is either a variable, an application of terms, and abstraction of +a variable over a term, a dependent product or a sort. +@dfn{Abstractions} are the regular lambda-abstractions of the +lambda-calculus with an extra type annotation on the bound variable. It +is written in Dedukti as in the following example: + +@oindex => +@example +x : A => t +@end example + +@noindent +where @code{x} is a variable, @code{A} is a type and @code{t} is a term. +Parentheses around the abstraction are optional. A product is written +similarly: + +@oindex -> +@example +x : A -> B +@end example + +@noindent +with @code{A} and @code{B} types. As a convenience, if the variable +@code{x} does not appear free in the type @code{B}, one may write + +@example +A -> B +@end example + +@dindex application +@noindent +instead. Finally @dfn{applications} are written as a simple +juxtaposition of terms, as in @code{t1 t2}. + +@cindex operator precedence +@cindex precedence +@cindex associativity +@quotation Note +Products bind more strongly than abstractions, so that @code{x : A -> B +=> t} is parsed as @code{x : (A -> B) => t}. Also, applications are +left-associative, while products are right-associative. This means that + +@example +((a b) c) d -> (e (f g) -> h) +@end example + +@noindent +is equivalent to + +@example +a b c d -> e (f g) -> h +@end example +@end quotation + +@node Scoping rules +@section Scoping rules +@cindex scoping +@cindex lexical scoping +@cindex rules, scope of +@cindex axioms, scope of + +An axiom declaration introduces the axiom into scope from the end of the +declaration to the end of the file. Binding constructs such as products +and abstractions introduce new variables whose scope encompasses the +entire binding construct, i.e.@: variables are lexically scoped. + +Rules may be defined anywhere within the scope of the head constant to +which it pertains and the scope of the constants appearing in the left +and right hand sides of the rule. As noted in @ref{Rules}, rules must be +defined in the same module as the declaration of the head constant. + +@node Grammar +@section The grammar of axioms and rules +@cindex grammar +@cindex syntax + +The concrete syntax for the @lambdapi{}-calculus modulo used by Dedukti +is given by the following grammar. + +@example +qid ::= id.id | id +toplevel ::= declaration toplevel + | rule toplevel + | eof +binding ::= id : term +declaration ::= id ":" term "." +domain ::= id ":" applicative + | applicative +sort ::= Type +term ::= domain "->" term + | domain "=>" term + | applicative +simple ::= sort + | qid + | "(" term ")" +applicative ::= simple + | applicative simple +rule ::= env term "-->" term +env ::= "[]" + | "[" env2 "]" +env2 ::= binding + | binding "," env2 +@end example + +@node Invoking dedukti +@chapter Invoking @command{dedukti} + +@menu +* One-shot mode:: Compiling one source file at a time. +* Batch mode:: Let Dedukti figure out what needs to be compiled. +@end menu + +@node One-shot mode +@section One-shot mode + +The simplest mode of operation is the one-shot mode. @command{dedukti} +will create a @file{.dko} file from the given source file. If the source +file refers to other modules, then compilation may only proceed if the +source files for those modules have also been compiled beforehand. + +A source file @file{a.dk} can be compiled as follows: + +@example +$ dedukti a.dk +@end example + +@noindent +Once a @file{.dko} file has been produced, one can further process this +file in order to obtain native object code. The @file{.dko} file is in +fact Haskell source code, so it can be compiled using the GHC Haskell +compiler. If this step is omitted, then the @file{.dko} file will be +converted to bytecode on the fly by @command{dkrun} when it is loaded. +Hence for better performance, it is better to compile all @file{.dko} +files with the GHC compiler, so that native code will be used when +checking each module, rather than bytecode. To have GHC called +automatically for you with the right flags, see @ref{Batch mode}. + +The @file{.dk} extension may be omitted. If @file{a.dk} mentions modules +@code{b} and @code{c} then files @file{b.dk} and @file{c.dk} need to be +compiled first. The next section details how to have @command{dedukti} +figure out dependencies and compile them in the right order +automatically. + +@node Batch mode +@section Batch mode + +Compile in batch mode by passing the @code{--make} flag to +@command{dedukti}. In this mode, dependencies of the file given in +argument will be compiled first, though after the dependencies of the +dependencies have been compiled, etc. Those dependencies that do not +need rebuilding, because their object file is up to date with respect to +the source file, will not be rebuilt. + +In addition, calling @command{dedukti} in batch mode will cause it to +invoke GHC on all compiled files, so as to produce native object code +for the module given as argument and its dependencies. Compiling to +native code often yields much better performance during checking. +@xref{Invoking dkrun}. + +@node Invoking dkrun +@chapter Invoking @command{dkrun} + +@command{dkrun} is a wrapper script that invokes @command{ghci} with the +appropriate flags on the Haskell source files (@file{.dko} files) given +as arguments. If object files exist for the given @file{.dko} files, +then these are loaded into memory and linked by the @command{ghci} +linker. Otherwise the files are compiled to slower, interpreted bytecode +by @command{ghci}. + +The first argument to @command{dkrun} is the @file{.dko} file +corresponding to the module one wants to proof check. If a module has +dependencies, then the Haskell source files corresponding to these +dependencies must be given as additional arguments to +@command{dkrun}@footnote{This is a limitation of the current +implementation and may be lifted at some point in the future.}. Say +@code{A} depends on @code{B} and @code{C}, @code{B} depends on @code{D}. +Then the following command proof checks @code{A}: + +@example +$ dkrun A.dko B.dko C.dko D.dko +@end example + + +@node References +@chapter References + +@enumerate + +@include references.texi + +@end enumerate + +@ifnottex +@node Copying this manual +@appendix Copying this manual + +@include fdl.texi +@end ifnottex + +@node Index +@unnumbered Index + +@printindex cp + +@bye diff --git a/doc/mkfile b/doc/mkfile new file mode 100644 --- /dev/null +++ b/doc/mkfile @@ -0,0 +1,24 @@ +%.html: %.texi.in + m4 $prereq | texi2html --split=chapter --prefix=$stem - + +%.pdf: %.texi.in + m4 $prereq > $stem.texi + texi2pdf -b $stem.texi; rm -f manual.texi + +%.info: %.texi.in + m4 $prereq | makeinfo - + +default:QV: + echo 'Please specify one of "html" or "pdf" as targets.' + exit 1 + +pdf:V: manual.pdf +html:V: manual.html +info:V: manual.info + +clean:V: + rm -f *.{aux,cp,cps,df,fn,ky,log,pg,toc,tp,vr} + rm -f *.info + rm -f *.html + rm -f *.pdf + rm -f manual.texi diff --git a/doc/references.texi b/doc/references.texi new file mode 100644 --- /dev/null +++ b/doc/references.texi @@ -0,0 +1,2 @@ +@item [DW99] +G. Dowek and B. Werner, ``Proof Normalization Modulo,'' @cite{Types for Proofs and Programs}, 1999, pp. 62-77. diff --git a/scripts/dkrun b/scripts/dkrun new file mode 100644 --- /dev/null +++ b/scripts/dkrun @@ -0,0 +1,14 @@ +#!/bin/sh + +if [ -z $* ] +then + echo "Usage: dkrun module.euo [DEPENDENCY]..." 1>&2 + echo " Where all dependent modules must be listed explicitly," 1>&2 + echo " after the module to typecheck." 1>&2 + exit 1 +fi + +main=$1 +shift 1 + +echo "do t <- Dedukti.Runtime.start; main; Dedukti.Runtime.stop t" | ghci -x hs -XOverloadedStrings -fglasgow-exts -w $* $main