dedukti 1.0.1 → 1.0.2
raw patch · 8 files changed
+1067/−14 lines, 8 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- Dedukti/Driver/Batch.hs +10/−10
- Dedukti/Module.hs +3/−3
- dedukti.cabal +6/−1
- doc/fdl.texi +506/−0
- doc/manual.texi.in +502/−0
- doc/mkfile +24/−0
- doc/references.texi +2/−0
- scripts/dkrun +14/−0
Dedukti/Driver/Batch.hs view
@@ -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
Dedukti/Module.hs view
@@ -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
dedukti.cabal view
@@ -1,5 +1,5 @@ name: dedukti-version: 1.0.1+version: 1.0.2 author: Mathieu Boespflug maintainer: Mathieu Boespflug <mboes@lix.polytechnique.fr> 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
+ doc/fdl.texi view
@@ -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:+
+ doc/manual.texi.in view
@@ -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
+ doc/mkfile view
@@ -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
+ doc/references.texi view
@@ -0,0 +1,2 @@+@item [DW99]+G. Dowek and B. Werner, ``Proof Normalization Modulo,'' @cite{Types for Proofs and Programs}, 1999, pp. 62-77.
+ scripts/dkrun view
@@ -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