From 79f6a1d8eb5aa3c1c426a2c6df19e9505b4836c3 Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm+hcompta@autogeree.net>
Date: Fri, 27 May 2016 04:21:06 +0200
Subject: [PATCH] =?utf8?q?D=C3=A9place=20hcompta-calculus=20vers=20lol-cal?=
=?utf8?q?culus=20et=20lol-typing?=
MIME-Version: 1.0
Content-Type: text/plain; charset=utf8
Content-Transfer-Encoding: 8bit
---
calculus/.gitignore | 4 -
calculus/COPYING | 674 -------
.../Abstraction/DeBruijn/Generalized.hs | 299 ---
calculus/Calculus/Lambda/Omega/Explicit.hs | 1723 -----------------
.../Omega/Explicit/REPL-with-stacktrace.sh | 9 -
.../Calculus/Lambda/Omega/Explicit/REPL.hs | 639 ------
.../Calculus/Lambda/Omega/Explicit/REPL.sh | 8 -
.../Calculus/Lambda/Omega/Explicit/Read.hs | 392 ----
.../Calculus/Lambda/Omega/Explicit/lib.cloe | 13 -
.../Lambda/Omega/Explicit/lib/Bool.cloe | 30 -
.../Lambda/Omega/Explicit/lib/Either.cloe | 40 -
.../Lambda/Omega/Explicit/lib/Eq.cloe | 36 -
.../Lambda/Omega/Explicit/lib/Function.cloe | 10 -
.../Lambda/Omega/Explicit/lib/Functor.cloe | 34 -
.../Lambda/Omega/Explicit/lib/IO.cloe | 36 -
.../Lambda/Omega/Explicit/lib/List.cloe | 74 -
.../Lambda/Omega/Explicit/lib/Maybe.cloe | 28 -
.../Lambda/Omega/Explicit/lib/Monad.cloe | 52 -
.../Lambda/Omega/Explicit/lib/Monoid.cloe | 42 -
.../Lambda/Omega/Explicit/lib/Nat.cloe | 19 -
.../Lambda/Omega/Explicit/lib/Ord.cloe | 51 -
.../Lambda/Omega/Explicit/lib/Pair.cloe | 23 -
calculus/Calculus/Lambda/Omega/Implicit.hs | 4 -
calculus/Control/Monad/Classes/EffectsFix.hs | 18 -
calculus/Control/Monad/Classes/Instance.hs | 23 -
calculus/Control/Monad/Classes/StateFix.hs | 132 --
.../Control/Monad/Classes/StateInstance.hs | 96 -
calculus/cabal.config | 2 -
calculus/hcompta-calculus.cabal | 137 --
29 files changed, 4648 deletions(-)
delete mode 100644 calculus/.gitignore
delete mode 100644 calculus/COPYING
delete mode 100644 calculus/Calculus/Abstraction/DeBruijn/Generalized.hs
delete mode 100644 calculus/Calculus/Lambda/Omega/Explicit.hs
delete mode 100755 calculus/Calculus/Lambda/Omega/Explicit/REPL-with-stacktrace.sh
delete mode 100644 calculus/Calculus/Lambda/Omega/Explicit/REPL.hs
delete mode 100755 calculus/Calculus/Lambda/Omega/Explicit/REPL.sh
delete mode 100644 calculus/Calculus/Lambda/Omega/Explicit/Read.hs
delete mode 100644 calculus/Calculus/Lambda/Omega/Explicit/lib.cloe
delete mode 100644 calculus/Calculus/Lambda/Omega/Explicit/lib/Bool.cloe
delete mode 100644 calculus/Calculus/Lambda/Omega/Explicit/lib/Either.cloe
delete mode 100644 calculus/Calculus/Lambda/Omega/Explicit/lib/Eq.cloe
delete mode 100644 calculus/Calculus/Lambda/Omega/Explicit/lib/Function.cloe
delete mode 100644 calculus/Calculus/Lambda/Omega/Explicit/lib/Functor.cloe
delete mode 100644 calculus/Calculus/Lambda/Omega/Explicit/lib/IO.cloe
delete mode 100644 calculus/Calculus/Lambda/Omega/Explicit/lib/List.cloe
delete mode 100644 calculus/Calculus/Lambda/Omega/Explicit/lib/Maybe.cloe
delete mode 100644 calculus/Calculus/Lambda/Omega/Explicit/lib/Monad.cloe
delete mode 100644 calculus/Calculus/Lambda/Omega/Explicit/lib/Monoid.cloe
delete mode 100644 calculus/Calculus/Lambda/Omega/Explicit/lib/Nat.cloe
delete mode 100644 calculus/Calculus/Lambda/Omega/Explicit/lib/Ord.cloe
delete mode 100644 calculus/Calculus/Lambda/Omega/Explicit/lib/Pair.cloe
delete mode 100644 calculus/Calculus/Lambda/Omega/Implicit.hs
delete mode 100644 calculus/Control/Monad/Classes/EffectsFix.hs
delete mode 100644 calculus/Control/Monad/Classes/Instance.hs
delete mode 100644 calculus/Control/Monad/Classes/StateFix.hs
delete mode 100644 calculus/Control/Monad/Classes/StateInstance.hs
delete mode 100644 calculus/cabal.config
delete mode 100644 calculus/hcompta-calculus.cabal
diff --git a/calculus/.gitignore b/calculus/.gitignore
deleted file mode 100644
index 4e7003c..0000000
--- a/calculus/.gitignore
+++ /dev/null
@@ -1,4 +0,0 @@
-.cabal-sandbox/
-cabal.sandbox.config
-dist/
-Calculus/Lambda/Omega/Explicit/REPL
diff --git a/calculus/COPYING b/calculus/COPYING
deleted file mode 100644
index 94a9ed0..0000000
--- a/calculus/COPYING
+++ /dev/null
@@ -1,674 +0,0 @@
- GNU GENERAL PUBLIC LICENSE
- Version 3, 29 June 2007
-
- Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>
- Everyone is permitted to copy and distribute verbatim copies
- of this license document, but changing it is not allowed.
-
- Preamble
-
- The GNU General Public License is a free, copyleft license for
-software and other kinds of works.
-
- The licenses for most software and other practical works are designed
-to take away your freedom to share and change the works. By contrast,
-the GNU General Public License is intended to guarantee your freedom to
-share and change all versions of a program--to make sure it remains free
-software for all its users. We, the Free Software Foundation, use the
-GNU General Public License for most of our software; it applies also to
-any other work released this way by its authors. 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
-them 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 prevent others from denying you
-these rights or asking you to surrender the rights. Therefore, you have
-certain responsibilities if you distribute copies of the software, or if
-you modify it: responsibilities to respect the freedom of others.
-
- For example, if you distribute copies of such a program, whether
-gratis or for a fee, you must pass on to the recipients the same
-freedoms that you received. 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.
-
- Developers that use the GNU GPL protect your rights with two steps:
-(1) assert copyright on the software, and (2) offer you this License
-giving you legal permission to copy, distribute and/or modify it.
-
- For the developers' and authors' protection, the GPL clearly explains
-that there is no warranty for this free software. For both users' and
-authors' sake, the GPL requires that modified versions be marked as
-changed, so that their problems will not be attributed erroneously to
-authors of previous versions.
-
- Some devices are designed to deny users access to install or run
-modified versions of the software inside them, although the manufacturer
-can do so. This is fundamentally incompatible with the aim of
-protecting users' freedom to change the software. The systematic
-pattern of such abuse occurs in the area of products for individuals to
-use, which is precisely where it is most unacceptable. Therefore, we
-have designed this version of the GPL to prohibit the practice for those
-products. If such problems arise substantially in other domains, we
-stand ready to extend this provision to those domains in future versions
-of the GPL, as needed to protect the freedom of users.
-
- Finally, every program is threatened constantly by software patents.
-States should not allow patents to restrict development and use of
-software on general-purpose computers, but in those that do, we wish to
-avoid the special danger that patents applied to a free program could
-make it effectively proprietary. To prevent this, the GPL assures that
-patents cannot be used to render the program non-free.
-
- The precise terms and conditions for copying, distribution and
-modification follow.
-
- TERMS AND CONDITIONS
-
- 0. Definitions.
-
- "This License" refers to version 3 of the GNU General Public License.
-
- "Copyright" also means copyright-like laws that apply to other kinds of
-works, such as semiconductor masks.
-
- "The Program" refers to any copyrightable work licensed under this
-License. Each licensee is addressed as "you". "Licensees" and
-"recipients" may be individuals or organizations.
-
- To "modify" a work means to copy from or adapt all or part of the work
-in a fashion requiring copyright permission, other than the making of an
-exact copy. The resulting work is called a "modified version" of the
-earlier work or a work "based on" the earlier work.
-
- A "covered work" means either the unmodified Program or a work based
-on the Program.
-
- To "propagate" a work means to do anything with it that, without
-permission, would make you directly or secondarily liable for
-infringement under applicable copyright law, except executing it on a
-computer or modifying a private copy. Propagation includes copying,
-distribution (with or without modification), making available to the
-public, and in some countries other activities as well.
-
- To "convey" a work means any kind of propagation that enables other
-parties to make or receive copies. Mere interaction with a user through
-a computer network, with no transfer of a copy, is not conveying.
-
- An interactive user interface displays "Appropriate Legal Notices"
-to the extent that it includes a convenient and prominently visible
-feature that (1) displays an appropriate copyright notice, and (2)
-tells the user that there is no warranty for the work (except to the
-extent that warranties are provided), that licensees may convey the
-work under this License, and how to view a copy of this License. If
-the interface presents a list of user commands or options, such as a
-menu, a prominent item in the list meets this criterion.
-
- 1. Source Code.
-
- The "source code" for a work means the preferred form of the work
-for making modifications to it. "Object code" means any non-source
-form of a work.
-
- A "Standard Interface" means an interface that either is an official
-standard defined by a recognized standards body, or, in the case of
-interfaces specified for a particular programming language, one that
-is widely used among developers working in that language.
-
- The "System Libraries" of an executable work include anything, other
-than the work as a whole, that (a) is included in the normal form of
-packaging a Major Component, but which is not part of that Major
-Component, and (b) serves only to enable use of the work with that
-Major Component, or to implement a Standard Interface for which an
-implementation is available to the public in source code form. A
-"Major Component", in this context, means a major essential component
-(kernel, window system, and so on) of the specific operating system
-(if any) on which the executable work runs, or a compiler used to
-produce the work, or an object code interpreter used to run it.
-
- The "Corresponding Source" for a work in object code form means all
-the source code needed to generate, install, and (for an executable
-work) run the object code and to modify the work, including scripts to
-control those activities. However, it does not include the work's
-System Libraries, or general-purpose tools or generally available free
-programs which are used unmodified in performing those activities but
-which are not part of the work. For example, Corresponding Source
-includes interface definition files associated with source files for
-the work, and the source code for shared libraries and dynamically
-linked subprograms that the work is specifically designed to require,
-such as by intimate data communication or control flow between those
-subprograms and other parts of the work.
-
- The Corresponding Source need not include anything that users
-can regenerate automatically from other parts of the Corresponding
-Source.
-
- The Corresponding Source for a work in source code form is that
-same work.
-
- 2. Basic Permissions.
-
- All rights granted under this License are granted for the term of
-copyright on the Program, and are irrevocable provided the stated
-conditions are met. This License explicitly affirms your unlimited
-permission to run the unmodified Program. The output from running a
-covered work is covered by this License only if the output, given its
-content, constitutes a covered work. This License acknowledges your
-rights of fair use or other equivalent, as provided by copyright law.
-
- You may make, run and propagate covered works that you do not
-convey, without conditions so long as your license otherwise remains
-in force. You may convey covered works to others for the sole purpose
-of having them make modifications exclusively for you, or provide you
-with facilities for running those works, provided that you comply with
-the terms of this License in conveying all material for which you do
-not control copyright. Those thus making or running the covered works
-for you must do so exclusively on your behalf, under your direction
-and control, on terms that prohibit them from making any copies of
-your copyrighted material outside their relationship with you.
-
- Conveying under any other circumstances is permitted solely under
-the conditions stated below. Sublicensing is not allowed; section 10
-makes it unnecessary.
-
- 3. Protecting Users' Legal Rights From Anti-Circumvention Law.
-
- No covered work shall be deemed part of an effective technological
-measure under any applicable law fulfilling obligations under article
-11 of the WIPO copyright treaty adopted on 20 December 1996, or
-similar laws prohibiting or restricting circumvention of such
-measures.
-
- When you convey a covered work, you waive any legal power to forbid
-circumvention of technological measures to the extent such circumvention
-is effected by exercising rights under this License with respect to
-the covered work, and you disclaim any intention to limit operation or
-modification of the work as a means of enforcing, against the work's
-users, your or third parties' legal rights to forbid circumvention of
-technological measures.
-
- 4. Conveying Verbatim Copies.
-
- You may convey 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;
-keep intact all notices stating that this License and any
-non-permissive terms added in accord with section 7 apply to the code;
-keep intact all notices of the absence of any warranty; and give all
-recipients a copy of this License along with the Program.
-
- You may charge any price or no price for each copy that you convey,
-and you may offer support or warranty protection for a fee.
-
- 5. Conveying Modified Source Versions.
-
- You may convey a work based on the Program, or the modifications to
-produce it from the Program, in the form of source code under the
-terms of section 4, provided that you also meet all of these conditions:
-
- a) The work must carry prominent notices stating that you modified
- it, and giving a relevant date.
-
- b) The work must carry prominent notices stating that it is
- released under this License and any conditions added under section
- 7. This requirement modifies the requirement in section 4 to
- "keep intact all notices".
-
- c) You must license the entire work, as a whole, under this
- License to anyone who comes into possession of a copy. This
- License will therefore apply, along with any applicable section 7
- additional terms, to the whole of the work, and all its parts,
- regardless of how they are packaged. This License gives no
- permission to license the work in any other way, but it does not
- invalidate such permission if you have separately received it.
-
- d) If the work has interactive user interfaces, each must display
- Appropriate Legal Notices; however, if the Program has interactive
- interfaces that do not display Appropriate Legal Notices, your
- work need not make them do so.
-
- A compilation of a covered work with other separate and independent
-works, which are not by their nature extensions of the covered work,
-and which are not combined with it such as to form a larger program,
-in or on a volume of a storage or distribution medium, is called an
-"aggregate" if the compilation and its resulting copyright are not
-used to limit the access or legal rights of the compilation's users
-beyond what the individual works permit. Inclusion of a covered work
-in an aggregate does not cause this License to apply to the other
-parts of the aggregate.
-
- 6. Conveying Non-Source Forms.
-
- You may convey a covered work in object code form under the terms
-of sections 4 and 5, provided that you also convey the
-machine-readable Corresponding Source under the terms of this License,
-in one of these ways:
-
- a) Convey the object code in, or embodied in, a physical product
- (including a physical distribution medium), accompanied by the
- Corresponding Source fixed on a durable physical medium
- customarily used for software interchange.
-
- b) Convey the object code in, or embodied in, a physical product
- (including a physical distribution medium), accompanied by a
- written offer, valid for at least three years and valid for as
- long as you offer spare parts or customer support for that product
- model, to give anyone who possesses the object code either (1) a
- copy of the Corresponding Source for all the software in the
- product that is covered by this License, on a durable physical
- medium customarily used for software interchange, for a price no
- more than your reasonable cost of physically performing this
- conveying of source, or (2) access to copy the
- Corresponding Source from a network server at no charge.
-
- c) Convey individual copies of the object code with a copy of the
- written offer to provide the Corresponding Source. This
- alternative is allowed only occasionally and noncommercially, and
- only if you received the object code with such an offer, in accord
- with subsection 6b.
-
- d) Convey the object code by offering access from a designated
- place (gratis or for a charge), and offer equivalent access to the
- Corresponding Source in the same way through the same place at no
- further charge. You need not require recipients to copy the
- Corresponding Source along with the object code. If the place to
- copy the object code is a network server, the Corresponding Source
- may be on a different server (operated by you or a third party)
- that supports equivalent copying facilities, provided you maintain
- clear directions next to the object code saying where to find the
- Corresponding Source. Regardless of what server hosts the
- Corresponding Source, you remain obligated to ensure that it is
- available for as long as needed to satisfy these requirements.
-
- e) Convey the object code using peer-to-peer transmission, provided
- you inform other peers where the object code and Corresponding
- Source of the work are being offered to the general public at no
- charge under subsection 6d.
-
- A separable portion of the object code, whose source code is excluded
-from the Corresponding Source as a System Library, need not be
-included in conveying the object code work.
-
- A "User Product" is either (1) a "consumer product", which means any
-tangible personal property which is normally used for personal, family,
-or household purposes, or (2) anything designed or sold for incorporation
-into a dwelling. In determining whether a product is a consumer product,
-doubtful cases shall be resolved in favor of coverage. For a particular
-product received by a particular user, "normally used" refers to a
-typical or common use of that class of product, regardless of the status
-of the particular user or of the way in which the particular user
-actually uses, or expects or is expected to use, the product. A product
-is a consumer product regardless of whether the product has substantial
-commercial, industrial or non-consumer uses, unless such uses represent
-the only significant mode of use of the product.
-
- "Installation Information" for a User Product means any methods,
-procedures, authorization keys, or other information required to install
-and execute modified versions of a covered work in that User Product from
-a modified version of its Corresponding Source. The information must
-suffice to ensure that the continued functioning of the modified object
-code is in no case prevented or interfered with solely because
-modification has been made.
-
- If you convey an object code work under this section in, or with, or
-specifically for use in, a User Product, and the conveying occurs as
-part of a transaction in which the right of possession and use of the
-User Product is transferred to the recipient in perpetuity or for a
-fixed term (regardless of how the transaction is characterized), the
-Corresponding Source conveyed under this section must be accompanied
-by the Installation Information. But this requirement does not apply
-if neither you nor any third party retains the ability to install
-modified object code on the User Product (for example, the work has
-been installed in ROM).
-
- The requirement to provide Installation Information does not include a
-requirement to continue to provide support service, warranty, or updates
-for a work that has been modified or installed by the recipient, or for
-the User Product in which it has been modified or installed. Access to a
-network may be denied when the modification itself materially and
-adversely affects the operation of the network or violates the rules and
-protocols for communication across the network.
-
- Corresponding Source conveyed, and Installation Information provided,
-in accord with this section must be in a format that is publicly
-documented (and with an implementation available to the public in
-source code form), and must require no special password or key for
-unpacking, reading or copying.
-
- 7. Additional Terms.
-
- "Additional permissions" are terms that supplement the terms of this
-License by making exceptions from one or more of its conditions.
-Additional permissions that are applicable to the entire Program shall
-be treated as though they were included in this License, to the extent
-that they are valid under applicable law. If additional permissions
-apply only to part of the Program, that part may be used separately
-under those permissions, but the entire Program remains governed by
-this License without regard to the additional permissions.
-
- When you convey a copy of a covered work, you may at your option
-remove any additional permissions from that copy, or from any part of
-it. (Additional permissions may be written to require their own
-removal in certain cases when you modify the work.) You may place
-additional permissions on material, added by you to a covered work,
-for which you have or can give appropriate copyright permission.
-
- Notwithstanding any other provision of this License, for material you
-add to a covered work, you may (if authorized by the copyright holders of
-that material) supplement the terms of this License with terms:
-
- a) Disclaiming warranty or limiting liability differently from the
- terms of sections 15 and 16 of this License; or
-
- b) Requiring preservation of specified reasonable legal notices or
- author attributions in that material or in the Appropriate Legal
- Notices displayed by works containing it; or
-
- c) Prohibiting misrepresentation of the origin of that material, or
- requiring that modified versions of such material be marked in
- reasonable ways as different from the original version; or
-
- d) Limiting the use for publicity purposes of names of licensors or
- authors of the material; or
-
- e) Declining to grant rights under trademark law for use of some
- trade names, trademarks, or service marks; or
-
- f) Requiring indemnification of licensors and authors of that
- material by anyone who conveys the material (or modified versions of
- it) with contractual assumptions of liability to the recipient, for
- any liability that these contractual assumptions directly impose on
- those licensors and authors.
-
- All other non-permissive additional terms are considered "further
-restrictions" within the meaning of section 10. If the Program as you
-received it, or any part of it, contains a notice stating that it is
-governed by this License along with a term that is a further
-restriction, you may remove that term. If a license document contains
-a further restriction but permits relicensing or conveying under this
-License, you may add to a covered work material governed by the terms
-of that license document, provided that the further restriction does
-not survive such relicensing or conveying.
-
- If you add terms to a covered work in accord with this section, you
-must place, in the relevant source files, a statement of the
-additional terms that apply to those files, or a notice indicating
-where to find the applicable terms.
-
- Additional terms, permissive or non-permissive, may be stated in the
-form of a separately written license, or stated as exceptions;
-the above requirements apply either way.
-
- 8. Termination.
-
- You may not propagate or modify a covered work except as expressly
-provided under this License. Any attempt otherwise to propagate or
-modify it is void, and will automatically terminate your rights under
-this License (including any patent licenses granted under the third
-paragraph of section 11).
-
- 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, you do not qualify to receive new licenses for the same
-material under section 10.
-
- 9. Acceptance Not Required for Having Copies.
-
- You are not required to accept this License in order to receive or
-run a copy of the Program. Ancillary propagation of a covered work
-occurring solely as a consequence of using peer-to-peer transmission
-to receive a copy likewise does not require acceptance. However,
-nothing other than this License grants you permission to propagate or
-modify any covered work. These actions infringe copyright if you do
-not accept this License. Therefore, by modifying or propagating a
-covered work, you indicate your acceptance of this License to do so.
-
- 10. Automatic Licensing of Downstream Recipients.
-
- Each time you convey a covered work, the recipient automatically
-receives a license from the original licensors, to run, modify and
-propagate that work, subject to this License. You are not responsible
-for enforcing compliance by third parties with this License.
-
- An "entity transaction" is a transaction transferring control of an
-organization, or substantially all assets of one, or subdividing an
-organization, or merging organizations. If propagation of a covered
-work results from an entity transaction, each party to that
-transaction who receives a copy of the work also receives whatever
-licenses to the work the party's predecessor in interest had or could
-give under the previous paragraph, plus a right to possession of the
-Corresponding Source of the work from the predecessor in interest, if
-the predecessor has it or can get it with reasonable efforts.
-
- You may not impose any further restrictions on the exercise of the
-rights granted or affirmed under this License. For example, you may
-not impose a license fee, royalty, or other charge for exercise of
-rights granted under this License, and you may not initiate litigation
-(including a cross-claim or counterclaim in a lawsuit) alleging that
-any patent claim is infringed by making, using, selling, offering for
-sale, or importing the Program or any portion of it.
-
- 11. Patents.
-
- A "contributor" is a copyright holder who authorizes use under this
-License of the Program or a work on which the Program is based. The
-work thus licensed is called the contributor's "contributor version".
-
- A contributor's "essential patent claims" are all patent claims
-owned or controlled by the contributor, whether already acquired or
-hereafter acquired, that would be infringed by some manner, permitted
-by this License, of making, using, or selling its contributor version,
-but do not include claims that would be infringed only as a
-consequence of further modification of the contributor version. For
-purposes of this definition, "control" includes the right to grant
-patent sublicenses in a manner consistent with the requirements of
-this License.
-
- Each contributor grants you a non-exclusive, worldwide, royalty-free
-patent license under the contributor's essential patent claims, to
-make, use, sell, offer for sale, import and otherwise run, modify and
-propagate the contents of its contributor version.
-
- In the following three paragraphs, a "patent license" is any express
-agreement or commitment, however denominated, not to enforce a patent
-(such as an express permission to practice a patent or covenant not to
-sue for patent infringement). To "grant" such a patent license to a
-party means to make such an agreement or commitment not to enforce a
-patent against the party.
-
- If you convey a covered work, knowingly relying on a patent license,
-and the Corresponding Source of the work is not available for anyone
-to copy, free of charge and under the terms of this License, through a
-publicly available network server or other readily accessible means,
-then you must either (1) cause the Corresponding Source to be so
-available, or (2) arrange to deprive yourself of the benefit of the
-patent license for this particular work, or (3) arrange, in a manner
-consistent with the requirements of this License, to extend the patent
-license to downstream recipients. "Knowingly relying" means you have
-actual knowledge that, but for the patent license, your conveying the
-covered work in a country, or your recipient's use of the covered work
-in a country, would infringe one or more identifiable patents in that
-country that you have reason to believe are valid.
-
- If, pursuant to or in connection with a single transaction or
-arrangement, you convey, or propagate by procuring conveyance of, a
-covered work, and grant a patent license to some of the parties
-receiving the covered work authorizing them to use, propagate, modify
-or convey a specific copy of the covered work, then the patent license
-you grant is automatically extended to all recipients of the covered
-work and works based on it.
-
- A patent license is "discriminatory" if it does not include within
-the scope of its coverage, prohibits the exercise of, or is
-conditioned on the non-exercise of one or more of the rights that are
-specifically granted under this License. You may not convey a covered
-work if you are a party to an arrangement with a third party that is
-in the business of distributing software, under which you make payment
-to the third party based on the extent of your activity of conveying
-the work, and under which the third party grants, to any of the
-parties who would receive the covered work from you, a discriminatory
-patent license (a) in connection with copies of the covered work
-conveyed by you (or copies made from those copies), or (b) primarily
-for and in connection with specific products or compilations that
-contain the covered work, unless you entered into that arrangement,
-or that patent license was granted, prior to 28 March 2007.
-
- Nothing in this License shall be construed as excluding or limiting
-any implied license or other defenses to infringement that may
-otherwise be available to you under applicable patent law.
-
- 12. No Surrender of Others' Freedom.
-
- If 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 convey a
-covered work so as to satisfy simultaneously your obligations under this
-License and any other pertinent obligations, then as a consequence you may
-not convey it at all. For example, if you agree to terms that obligate you
-to collect a royalty for further conveying from those to whom you convey
-the Program, the only way you could satisfy both those terms and this
-License would be to refrain entirely from conveying the Program.
-
- 13. Use with the GNU Affero General Public License.
-
- Notwithstanding any other provision of this License, you have
-permission to link or combine any covered work with a work licensed
-under version 3 of the GNU Affero General Public License into a single
-combined work, and to convey the resulting work. The terms of this
-License will continue to apply to the part which is the covered work,
-but the special requirements of the GNU Affero General Public License,
-section 13, concerning interaction through a network will apply to the
-combination as such.
-
- 14. Revised Versions of this License.
-
- The Free Software Foundation may publish revised and/or new versions of
-the GNU 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 that a certain numbered version of the GNU General
-Public License "or any later version" applies to it, you have the
-option of following the terms and conditions either of that numbered
-version or of any later version published by the Free Software
-Foundation. If the Program does not specify a version number of the
-GNU General Public License, you may choose any version ever published
-by the Free Software Foundation.
-
- If the Program specifies that a proxy can decide which future
-versions of the GNU General Public License can be used, that proxy's
-public statement of acceptance of a version permanently authorizes you
-to choose that version for the Program.
-
- Later license versions may give you additional or different
-permissions. However, no additional obligations are imposed on any
-author or copyright holder as a result of your choosing to follow a
-later version.
-
- 15. Disclaimer of Warranty.
-
- 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.
-
- 16. Limitation of Liability.
-
- IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
-WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS
-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.
-
- 17. Interpretation of Sections 15 and 16.
-
- If the disclaimer of warranty and limitation of liability provided
-above cannot be given local legal effect according to their terms,
-reviewing courts shall apply local law that most closely approximates
-an absolute waiver of all civil liability in connection with the
-Program, unless a warranty or assumption of liability accompanies a
-copy of the Program in return for a fee.
-
- 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
-state 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 3 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, see <http://www.gnu.org/licenses/>.
-
-Also add information on how to contact you by electronic and paper mail.
-
- If the program does terminal interaction, make it output a short
-notice like this when it starts in an interactive mode:
-
- <program> Copyright (C) <year> <name of author>
- This program 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, your program's commands
-might be different; for a GUI interface, you would use an "about box".
-
- You should also get your employer (if you work as a programmer) or school,
-if any, to sign a "copyright disclaimer" for the program, if necessary.
-For more information on this, and how to apply and follow the GNU GPL, see
-<http://www.gnu.org/licenses/>.
-
- The GNU 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. But first, please read
-<http://www.gnu.org/philosophy/why-not-lgpl.html>.
diff --git a/calculus/Calculus/Abstraction/DeBruijn/Generalized.hs b/calculus/Calculus/Abstraction/DeBruijn/Generalized.hs
deleted file mode 100644
index ce9da59..0000000
--- a/calculus/Calculus/Abstraction/DeBruijn/Generalized.hs
+++ /dev/null
@@ -1,299 +0,0 @@
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-{-# OPTIONS_GHC -fno-warn-tabs #-}
-module Calculus.Abstraction.DeBruijn.Generalized where
-
-import Control.Applicative (Applicative(..))
-import Control.Monad
-import Control.Monad.Trans.Class (MonadTrans(..))
-import Data.Bool (Bool(..))
-import Data.Eq (Eq(..))
-import Data.Foldable (Foldable(..))
-import Data.Function (($), (.))
-import Data.Function (on)
-import Data.Maybe (Maybe(..))
-import Data.Ord (Ord(..), Ordering(..))
-import Data.String (IsString(..), String)
-import Data.Text (Text)
-import Data.Text.Buildable (Buildable(..))
-import Data.Traversable (Traversable(..))
-import Prelude (Int)
-import Text.Show (Show(..), ShowS, showChar, showParen, showString)
-
--- * Type 'Abstraction'
--- | 'Abstraction' @bound@ @expr@ @var@:
--- encodes an 'abstract'-ion
--- over an expression of type @expr@,
--- by segretating its variables between:
---
--- * /bound variables/ of type: @bound@,
--- * and /unbound variables/ (aka. /free variables/) of type: @var@.
---
--- Note that /unbound variables/ may later themselves be made /bound variables/
--- of an enclosing 'Abstraction', effectively encoding
--- /DeBruijn indices/ using Haskellâs /data constructors/,
--- that is, not like in a /traditional DeBruijn indexing/:
--- where an integer is used in each /bound variable/
--- to indicate which one of its enclosing 'Abstraction's is bounding it,
--- but by the nesting of 'Var_Free' data constructors.
--- As a side note, this is also different from the /DeBruijn indexing/
--- encoded at Haskellâs /type level/ by using @GADTs@
--- (done for instance in https://hackage.haskell.org/package/glambda ).
---
--- Moreover, /unbound variables/ are wrapped within a second level of expression
--- in order to improve the time complexity of /traditional DeBruijn indexing/
--- when 'unabstract'-ing (aka. /instantiating/)
--- (see 'Var' and instance 'MonadTrans' of 'Abstraction').
---
--- 'Abstraction' enables:
---
--- * /locally-nameless/ variables (nameless in 'Var_Bound', named in the deepest 'Var_Free');
--- * substitution of /bound variables/ in an expression using /DeBruijn indices/
--- (hence enabling capture-avoiding /β-reduction/
--- and reducing /α-equivalence/ to a structural equality (==));
--- * shifting /DeBruijn indices/ within an expression without traversing it
--- (hence generalizing and speeding up /traditional DeBruijn indices/);
--- * simultaneous substitution of several /bound variables/
--- (hence enabling expressions implementing recursive-@let@).
---
--- __Ressources:__
---
--- * /Bound/, Edward Kmett, 19 August 2013,
--- https://www.schoolofhaskell.com/user/edwardk/bound
-newtype Abstraction bound expr var
- = Abstraction (expr (Var bound (expr var)))
- deriving (Foldable, Functor, Traversable)
-instance (Monad expr, Eq bound, Eq1 expr, Show bound)
- => Eq1 (Abstraction bound expr) where
- (==#) = (==#) `on` abstract_normalize
-instance (Monad expr, Eq bound, Eq1 expr, Eq var, Show var, Show bound)
- => Eq (Abstraction bound expr var) where
- (==) = (==#)
-instance (Monad expr, Ord bound, Ord1 expr, Show bound)
- => Ord1 (Abstraction bound expr) where
- compare1 = compare1 `on` abstract_normalize
-instance (Monad expr, Ord bound, Ord1 expr, Ord var, Show var, Show bound)
- => Ord (Abstraction bound expr var) where
- compare = compare1
-instance (Functor expr, Show bound, Show1 expr)
- => Show1 (Abstraction bound expr) where
- showsPrec1 d (Abstraction e) =
- showsUnaryWith "Abstraction" d $
- (Lift1 `fmap`) `fmap` e
-instance (Functor expr, Show bound, Show1 expr, Show var)
- => Show (Abstraction bound expr var) where
- showsPrec = showsPrec1
-instance Monad expr => Applicative (Abstraction bound expr) where
- pure = return
- (<*>) = ap
--- | A 'Monad' instance capturing the notion of /variable substitution/,
--- used by 'unabstract' to decrement the /DeBruijn indices/.
-instance Monad expr => Monad (Abstraction bound expr) where
- return = Abstraction . return . Var_Free . return
- Abstraction expr >>= f = Abstraction $ expr >>= \var ->
- case var of
- Var_Bound bound -> return (Var_Bound bound)
- Var_Free e -> e >>= (\(Abstraction ex) -> ex) . f
-instance MonadTrans (Abstraction bound) where
- lift = Abstraction . return . Var_Free
--- | 'Monad_Module_Left' instance capturing the notion
--- of /variable substitution/ with /capture-avoiding/.
-instance Monad_Module_Left (Abstraction bound) where
- l >>>= f = l >>= lift . f
-
--- | WARNING: 'abstract' 'fmap'-s the given expression,
--- thus repetitive 'abstract'-ings have a quadratic time-complexity.
-abstract
- :: Monad expr
- => (var -> Maybe bound)
- -> expr var
- -> Abstraction bound expr var
-abstract f = Abstraction . fmap (\var ->
- case f var of
- Nothing -> Var_Free (return var)
- Just b -> Var_Bound b)
-
-unabstract
- :: Monad expr
- => (bound -> expr var)
- -> Abstraction bound expr var
- -> expr var
-unabstract unbound (Abstraction ex) = ex >>= \var ->
- case var of
- Var_Bound b -> unbound b
- Var_Free v -> v
-
--- | @'abstract_normalize'@ normalize
--- the possible placements of 'Var_Free' in 'Abstraction'
--- by moving them all to the leaves of the 'abstract'-ed expression.
---
--- This gives /traditional DeBruijn indices/ for /bound variables/.
-abstract_normalize
- :: Monad expr
- => Abstraction bound expr var
- -> expr (Var bound var)
-abstract_normalize (Abstraction expr) = expr >>= \var ->
- case var of
- Var_Bound bound -> return $ Var_Bound bound
- Var_Free e -> Var_Free `fmap`{-on var of expr-} e
-
--- | Convert from /traditional DeBruijn indices/
--- to /generalized DeBruijn indices/,
--- by wrapping all the leaves within the 'Monad'
--- of the given expression.
---
--- This requires a full traversal of the given expression.
-abstract_generalize
- :: Monad expr
- => expr (Var bound var)
- -> Abstraction bound expr var
-abstract_generalize = Abstraction .
- ((return{-of expr-}
- `fmap`{-on var of Var-})
- `fmap`{-on var of expr-})
-
--- ** Class 'Monad_Module_Left'
--- | Like ('>>=') but whose 'Monad' is within a wrapping type @left@
--- (aka. /left module over a monad/).
---
--- __Laws:__
---
--- ('>>>=') should satisfy the following equations
--- in order to be used within a 'Monad' instance:
---
--- @
--- ('>>>=' 'return') = id
--- ('>>>=' (('>>=' g) . f)) = ('>>>=' f) . ('>>>=' g)
--- @
---
--- If @left@ has a 'MonadTrans' instance, then:
---
--- @
--- ('>>>=' f) = ('>>=' ('lift' . f))
--- @
---
--- which implies the above equations,
--- see 'MonadTrans' instance of ('Abstraction' @bound@).
---
--- __Uses:__
---
--- * Useful for expression constructors containing 'Abstraction' data.
---
--- __Ressources:__
---
--- * André Hirschowitz, Marco Maggesi, /Modules over monads and initial semantics/.
--- Information and Computation 208 (2010), pp. 545-564,
--- http://www.sciencedirect.com/science/article/pii/S0890540109002405
-class Monad_Module_Left left where
- (>>>=) :: Monad expr
- => left expr var
- -> (var -> expr bound)
- -> left expr bound
-infixl 1 >>>=
-
--- ** Type 'Var'
-
--- | 'Var' @bound@ @var@: a variable segregating between:
---
--- * 'Var_Bound', containing data of type @bound@,
--- considered /bound/ by the first enclosing 'Abstraction',
--- hence playing the role of a @Zero@ in /DeBruijn indexing/ terminology.
---
--- Note that the presence of this @bound@ enables the substitution
--- of a 'Var_Bound' by different values,
--- which is used to keep the 'Var_Name' given in the source code,
--- (note that it could also be used to implement a @recursive-let@).
---
--- * 'Var_Free', containing data of type @var@,
--- considered /free/ with respect to the first enclosing 'Abstraction',
--- hence playing the role of a @Succ@ in /DeBruijn indexing/ terminology.
---
--- Note that @var@ is not constrained to be itself a 'Var',
--- this in order to make it possible in 'Abstraction'
--- to insert @expr@ in between the @Succ@ nesting,
--- which optimizes the /DeBruijn indexing/ when 'unabstract'-ing,
--- by avoiding to traverse ('fmap') an @expr@ to @Succ@ its variables
--- (see instance 'MonadTrans' for 'Abstraction').
-data Var bound var
- = Var_Bound bound -- ^ @Zero@
- | Var_Free var -- ^ @Succ@
- deriving (Eq, Foldable, Functor, Ord, Show, Traversable)
-instance (Buildable bound, Buildable var) => Buildable (Var bound var) where
- build var =
- case var of
- Var_Bound b -> build b
- Var_Free f -> build f
-
--- | A convenient operator for 'abstract'-ing.
-(=?) :: Eq a => a -> a -> Maybe (Suggest a)
-(=?) x y = if x == y then Just (Suggest x) else Nothing
-
--- | A convenient type synonym for clarity.
-type Var_Name = Text
-
--- | A convenient class synonym for brievety.
-class (Show var, Buildable var) => Variable var
-instance Variable Var_Name
-instance (Variable bound, Variable var) => Variable (Var bound var)
-instance Variable var => Variable (Suggest var)
-
--- * Higher-order @Prelude@ classes
-
--- ** Class 'Eq1'
--- | Lift the 'Eq' class to unary type constructors,
--- to avoid the @UndecidableInstances@ language extension.
---
--- __Ressources:__
---
--- * /Simulating Quantified Class Constraints/, Valery Trifonov, 2003,
--- http://flint.cs.yale.edu/trifonov/papers/sqcc.pdf
--- * /prelude-extras/, Edward Kmett, 2011,
--- https://hackage.haskell.org/package/prelude-extras
--- * /base/ 'Data.Functor.Classes', Ross Paterson, 2013,
--- https://hackage.haskell.org/package/base/docs/Data-Functor-Classes.html
-class Eq1 f where
- (==#) :: (Eq a, Show a) => f a -> f a -> Bool
-
-class Eq1 f => Ord1 f where
- compare1 :: Ord a => f a -> f a -> Ordering
-
--- ** Class 'Show1'
--- | Lift the 'Show' class to unary type constructors,
--- to avoid the @UndecidableInstances@ language extension.
-class Show1 f where
- showsPrec1 :: Show a => Int -> f a -> ShowS
-
-showsUnaryWith :: (Show1 f, Show a) => String -> Int -> f a -> ShowS
-showsUnaryWith name d x =
- showParen (d > 10) $
- showString name . showChar ' ' . showsPrec1 11 x
-
--- ** Type 'Lift1'
--- | Lift the 'Lift' class to unary type constructors,
--- to avoid the @UndecidableInstances@ language extension.
-newtype Lift1 f a = Lift1 { lower1 :: f a }
- deriving (Functor, Foldable, Traversable, Eq1, Ord1, Show1)
-instance (Eq1 f, Eq a, Show a) => Eq (Lift1 f a) where (==) = (==#)
-instance (Ord1 f, Ord a, Show a) => Ord (Lift1 f a) where compare = compare1
-instance (Show1 f, Show a) => Show (Lift1 f a) where showsPrec = showsPrec1
-
--- ** Type 'Suggest'
-
--- | A convenient wrapper to include data ignored by /α-equivalence/.
-newtype Suggest n
- = Suggest n
- deriving (Functor, Show)
--- | Always return 'True', in order to be transparent for 'alpha_equiv'.
-instance Eq (Suggest n) where
- _ == _ = True
-instance Ord (Suggest n) where
- _ `compare` _ = EQ
-instance Buildable var
- => Buildable (Suggest var) where
- build (Suggest var) = build var
-instance IsString x => IsString (Suggest x) where
- fromString = Suggest . fromString
diff --git a/calculus/Calculus/Lambda/Omega/Explicit.hs b/calculus/Calculus/Lambda/Omega/Explicit.hs
deleted file mode 100644
index 0522115..0000000
--- a/calculus/Calculus/Lambda/Omega/Explicit.hs
+++ /dev/null
@@ -1,1723 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE EmptyDataDecls #-}
-{-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE NamedFieldPuns #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE ViewPatterns #-}
-{-# OPTIONS_GHC -fno-warn-tabs #-}
-module Calculus.Lambda.Omega.Explicit where
-
-import Control.Arrow
-import Control.Monad
-import qualified Data.Char as Char
-import Data.Function (on)
-import Data.Map.Strict (Map)
-import qualified Data.Map.Strict as Map
-import Data.Maybe (catMaybes)
-import Data.Maybe (fromJust)
-import Data.Monoid ((<>))
-import Data.Text (Text)
-import qualified Data.Text as Text
-import Data.Text.Buildable (Buildable(..))
-import qualified Data.Text.Lazy as TL
-import qualified Data.Text.Lazy.Builder as Builder
-import Data.Typeable as Typeable
-import Data.Bool
-import Data.Eq (Eq(..))
-import Data.Maybe (Maybe(..), maybe)
-import Data.Foldable (Foldable(..))
-import Data.Either (Either(..))
-import Data.List ((++))
-import Data.Monoid (Monoid(..))
-import Data.Function (($), (.), id, const, flip)
-import Data.String (String)
-import Data.Traversable (Traversable(..))
-import Data.Ord (Ord(..))
-import Control.Applicative (Applicative(..), (<$>))
-import Text.Show (Show(..), showParen, showString)
-import Prelude (Int, Integer, Num(..), error)
-import System.IO (IO)
-
--- import Debug.Trace
-
-import Calculus.Abstraction.DeBruijn.Generalized
-
--- * Type 'Term'
--- | 'Term' @var@ forms the main /Abstract Syntax Tree/
--- of the present /explicitely typed/ (aka. /Ã la Church/) /lambda-calculus/,
--- whose /term constructors/ are:
---
--- * 'TeTy_Var': for /term variable/ or /type variable/, see 'Abstraction'.
--- * 'TeTy_App': for /term application/ or /type application/, see 'normalize'.
--- * 'Term_Abst': for /term abstraction/ (aka. /λ-term/), see 'Abstraction'.
--- * 'Type_Abst': for /type abstraction/ (aka. /Î -type/, aka. /dependent product/), see 'sort_of_type_abst'.
--- * 'Type_Sort': for /sort constant/ of a /Pure Type System/ (aka. /PTS/), see 'sort_of_sort'.
--- * 'TeTy_Axiom': for /custom axiom/, see 'Axiomable'.
---
--- Note that 'Type' and 'Term' share this same data-type
--- (hence the varying prefixes of the Haskell /data constructors/),
--- which avoids duplication of code for their common operations.
---
--- Note that this Haskell type DOES NOT guarantee by itself
--- the /well-formedness/ of the 'Term' (or 'Type'),
--- for instance one can construct such @malformed_type@: @(* *)@:
---
--- @
--- > let star = 'Type_Sort' 'sort_star_mono'
--- > let malformed_type = 'TeTy_App' star star
--- > 'left' 'type_error_msg' '$' 'type_of' 'context' malformed_type
--- Left ('Type_Error_Msg_Not_a_function' ⦠)
--- @
---
--- Though an Haskell type could be crafted to get a stronger guarantee
--- over the /well-formedness/, it is not done here
--- for the following reasons :
---
--- 1. The /well-formedness/ alone is not really useful,
--- itâs the /well-typedness/ which matters,
--- and this depends upon a specific 'Context'.
---
--- 2. Guaranteeing a good combinaison of 'TeTy_App' with respect to 'Term_Abst' (or 'Type_Abst')
--- while using the 'Abstraction' approach could be done:
--- for instance by using @GADTs@ on 'Term'
--- to add an Haskell /type parameter/ @ty@ (aka. /index/)
--- constrained to @(i -> o)@, @i@ or @o@ depending on the /term constructors/,
--- and then by defining Haskell /type classes/
--- replicating: 'Functor', 'Foldable', 'Traversable', 'Monad' and 'Monad_Module_Left',
--- but working on /natural transformations/ (giving /indexed functors/, /indexed monads/, â¦),
--- however this yields to a significant increase in code complexity,
--- which is not really worth the resulting guarantee
--- (to my mind, here, simplicity has priority
--- over comprehensive automated checking,
--- especially since itâs a research project
--- where I don't fully know all what will be needed
--- and thus appreciate some level of flexibility).
---
--- So, with this actual 'Term' data-type:
--- 'type_of' MUST be used to check the /well-formedness/ along the /well-typedness/
--- of a 'Term' (or equivalently of a 'Type') with respect to a 'Context'.
-data Term var
- = TeTy_Var var
- | TeTy_App (Term var) (Term var)
- | Term_Abst (Suggest Var_Name) (Type var) (Abstraction (Suggest Var_Name) (Term) var)
- | Type_Abst (Suggest Var_Name) (Type var) (Abstraction (Suggest Var_Name) (Type) var)
- | Type_Sort Sort
- | forall ax .
- ( Axiomable (Axiom ax)
- , Typeable ax
- ) => TeTy_Axiom (Axiom ax)
- -- deriving (Eq, Show, Functor, Foldable, Traversable)
--- | 'Eq' instance ignores /bound variables/' 'Var_Name',
--- effectively testing for /α-equivalence/.
-instance (Eq var, Show var) => Eq (Term var) where
- TeTy_Var x == TeTy_Var y = x == y
- TeTy_App xf xa == TeTy_App yf ya = xf == yf && xa == ya
- Term_Abst _ xty xf == Term_Abst _ yty yf = xty == yty && xf == yf -- NOTE: ignore Var_Name
- Type_Abst _ xty xf == Type_Abst _ yty yf = xty == yty && xf == yf -- NOTE: ignore Var_Name
- Type_Sort x == Type_Sort y = x == y
- TeTy_Axiom x == TeTy_Axiom y = x `axiom_eq` y
- _ == _ = False
-deriving instance Show var => Show (Term var)
--- | A 'Functor' instance capturing the notion of /variable renaming/.
-deriving instance Functor Term
-deriving instance Foldable Term
-deriving instance Traversable Term
-deriving instance Typeable Term
-instance Show1 Term where showsPrec1 = showsPrec
-instance Eq1 Term where (==#) = (==)
-
-instance Applicative (Term) where
- pure = TeTy_Var
- (<*>) = ap
--- | A 'Monad' instance capturing the notion of /variable substitution/ with /capture-avoiding/.
-instance Monad (Term) where
- return = pure
- Type_Sort s >>= _ = Type_Sort s
- TeTy_Axiom a >>= _ = TeTy_Axiom a
- TeTy_Var v >>= go = go v
- TeTy_App f x >>= go = TeTy_App (f >>= go) (x >>= go)
- Term_Abst v f_in f >>= go = Term_Abst v (f_in >>= go) (f >>>= go)
- Type_Abst v f_in f >>= go = Type_Abst v (f_in >>= go) (f >>>= go)
-instance Buildable var => Buildable (Term var) where
- build = go False False
- where
- go :: forall v. (Buildable v)
- => Bool -> Bool
- -> Term v
- -> Builder.Builder
- go parenBind parenApp te =
- case te of
- Type_Sort s -> build s
- TeTy_Axiom ax -> build ax
- TeTy_Var v -> build v
- TeTy_App f x ->
- (if parenApp then "(" else "")
- <> go True False f <> " " <> go True True x
- <> (if parenApp then ")" else "")
- Term_Abst _ _ _ ->
- (if parenBind then "(" else "")
- <> "λ"{- <> "\\"-} <> go_abst parenBind parenApp te
- Type_Abst (Suggest x) f_in f_out ->
- (if parenBind then "(" else "")
- <> (if x == ""
- then go True False f_in
- else "â" <> "(" <> build x <> ":" <> go False False f_in <> ")" )
- <> " -> "
- <> go False False (abstract_normalize f_out)
- <> (if parenBind then ")" else "")
- go_abst :: forall v. (Buildable v)
- => Bool -> Bool
- -> Term v
- -> Builder.Builder
- go_abst parenBind parenApp te =
- case te of
- Term_Abst (Suggest x) f_in f ->
- let body = abstract_normalize f in
- case body of
- Term_Abst _ _ _ ->
- "(" <> go_var_def x <> ":" <> go False False f_in <> ")"
- <> " " <> go_abst parenBind parenApp body
- _ ->
- "(" <> go_var_def x <> ":" <> go False False f_in <> ")"
- <> " -> "
- <> go False False body
- <> (if parenBind then ")" else "")
- _ -> go parenBind parenApp te
- go_var_def x = if x == "" then "_" else build x
-
--- ** Type 'Sort'
--- | Four /PTS/ /sort constants/
--- are formed by combining
--- 'Type_Level' and 'Type_Morphism':
---
--- * @*m@: the 'Sort' to form the 'Type' of a monomorphic 'Term'.
--- * @*p@: the 'Sort' to form the 'Type' of a polymorphic 'Term'.
--- * @â¡m@: the 'Sort' to form the 'Type' of a monomorphic 'Type'.
--- * @â¡p@: the 'Sort' to form the 'Type' of a polymorphic 'Type'.
-type Sort = (Type_Level, Type_Morphism)
-instance Buildable Sort where
- build x = case x of
- (sort, morphism) -> build sort <> build morphism
-
--- | @*m@: the 'Sort' to form the 'Type' of a monomorphic 'Term'.
-sort_star_mono :: Sort
-sort_star_mono = (Type_Level_0, Type_Morphism_Mono)
-
--- | @*p@: the 'Sort' to form the 'Type' of a polymorphic 'Term'.
-sort_star_poly :: Sort
-sort_star_poly = (Type_Level_0, Type_Morphism_Poly)
-
--- *** Type 'Type_Level'
-data Type_Level
- = Type_Level_0 -- ^ aka. /@*@ (Star) sort constant/.
- | Type_Level_1 -- ^ aka. /@â¡@ (Box) sort constant/.
- deriving (Eq, Ord, Show)
-instance Buildable Type_Level where
- build x = case x of
- Type_Level_0 -> "*"
- Type_Level_1 -> "â¡"
-
--- *** Type 'Type_Morphism'
-data Type_Morphism
- = Type_Morphism_Mono
- | Type_Morphism_Poly
- deriving (Eq, Ord, Show)
-instance Buildable Type_Morphism where
- build x = case x of
- Type_Morphism_Mono -> "" -- "m"
- Type_Morphism_Poly -> "p"
-
--- | /PTS/ axioms for 'Sort':
---
--- * AXIOM: @⦠*m : â¡m@
--- * AXIOM: @⦠*p : â¡p@
-sort_of_sort :: Sort -> Either Type_Error_Msg Sort
-sort_of_sort (Type_Level_0, Type_Morphism_Mono)
- = return (Type_Level_1, Type_Morphism_Mono)
- -- AXIOM: @*m : â¡m@
- -- The type of MONOMORPHIC types of terms,
- -- is of type: the type of types of MONOMORPHIC types of terms
-sort_of_sort (Type_Level_0, Type_Morphism_Poly)
- = return (Type_Level_1, Type_Morphism_Poly)
- -- AXIOM: @*p : â¡p@
- -- The type of POLYMORPHIC types of terms,
- -- is of type: the type of types of POLYMORPHIC types of terms
-sort_of_sort s = Left $ Type_Error_Msg_No_sort_for_sort s
-
--- * Type 'Form'
-
--- | A record to keep a same 'Term' (or 'Type')
--- in several forms (and avoid to 'normalize' it multiple times).
-data Form var
- = Form
- { form_given :: Term var
- , form_normal :: Term var -- ^ 'normalize'-d version of 'form_given'.
- } deriving (Functor, Show)
-
--- | Return a 'Form' from a given 'Term'.
-form :: (Eq var, Ord var, Variable var, Typeable var) => Context var -> Term var -> Form var
-form ctx te = Form te (normalize ctx te)
-
--- | Reduce given 'Term' (or 'Type') to /normal form/ (NF)
--- by recursively performing /β-reduction/ and /η-reduction/.
---
--- Note that any well-typed 'Term' (i.e. for which 'type_of' returns a 'Type')
--- is /strongly normalizing/ (i.e. 'normalize' always returns,
--- and its returned 'Term' is unique up to /α-equivalence/).
-normalize :: (Eq var, Ord var, Variable var, Typeable var) => Context var -> Term var -> Term var
-normalize = go []
- where
- {-
- go_debug :: (Eq var, Ord var, Variable var, Typeable var)
- => [Term var]
- -> Context var
- -> Term var
- -> Term var
- go_debug args ctx te =
- go args ctx $
- trace ("normalize: "
- ++ "\n te = " ++ show te
- ++ "\n args = " ++ show args
- ) $ te
- -}
-
- go :: (Eq var, Ord var, Variable var, Typeable var)
- => [Term var]
- -> Context var
- -> Term var
- -> Term var
- go args ctx (TeTy_Var ((form_normal <$>) . context_item_term <=< context_lookup ctx -> Just te))
- -- NOTE: Replace variable mapped by the context
- = case args of
- [] -> te -- NOTE: no need to normalize again
- _ -> go args ctx te
- go args ctx (TeTy_App f x)
- -- NOTE: Normalize and collect applied arguments,
- -- this to normalize an argument only once for all patterns.
- = go (go [] ctx x : args) ctx f
- go [] ctx (Term_Abst x f_in f)
- -- NOTE: η-reduce: Term_Abst _ (TeTy_App f (TeTy_Var (Var_Bound _)) ==> f
- = (Term_Abst x (go [] ctx f_in) ||| id)
- (abst_eta_reduce ctx f)
- go (x:args) ctx (Term_Abst _ _ f)
- -- NOTE: β-reduce: TeTy_App (Term_Abst _ _ f) x ==> f x
- = go args ctx (const x `unabstract` f)
- go args ctx (Type_Abst x f_in f_out)
- -- NOTE: Recurse in Type_Abst fields
- = term_apps (Type_Abst x (go [] ctx f_in) (go_scope ctx f_out)) args
- go args ctx (TeTy_Axiom (flip (axiom_normalize ctx) args -> Just (r_te, r_args)))
- -- NOTE: Normalize axiom
- = go r_args ctx r_te
- go args _ctx te
- -- NOTE: Reapply remaining arguments, normalized
- = term_apps te args
-
- abst_eta_reduce
- :: (Eq var, Eq bound, Ord var, Ord bound, Variable var, Variable bound, Typeable var, Typeable bound)
- => Context var
- -> Abstraction bound (Term) var
- -> Either (Abstraction bound (Term) var) -- could not η-reduce
- (Term var) -- could η-reduce
- abst_eta_reduce ctx =
- (\abst_body ->
- let new_ctx = context_push_nothing ctx in
- case go [] new_ctx abst_body of
- te@(TeTy_App t (TeTy_Var (Var_Bound _{-Term_Abst's variable-}))) ->
- traverse (\var ->
- case var of
- Var_Free v -> Right v
- -- NOTE: decrement the DeBruijn indexing by one
- -- to reflect the removal of the Term_Abst.
- Var_Bound _ -> Left $ abstract_generalize te
- -- NOTE: cannot η-reduce because Term_Abst's variable
- -- is also used within t.
- ) t
- te -> Left $ abstract_generalize te
- ) .
- abstract_normalize
-
- go_scope
- :: (Eq var, Eq bound, Ord var, Ord bound, Variable var, Variable bound, Typeable var, Typeable bound)
- => Context var
- -> Abstraction bound (Term) var
- -> Abstraction bound (Term) var
- go_scope ctx =
- abstract_generalize .
- go [] (context_push_nothing ctx) .
- abstract_normalize
-
--- | Reduce given 'Term' to /Weak Head Normal Form/ (WHNF).
---
--- __Ressources:__
---
--- * https://wiki.haskell.org/Weak_head_normal_form
-whnf :: (Ord var, Variable var, Typeable var) => Context var -> Term var -> Term var
-whnf = go []
- where
- go :: (Ord var, Variable var, Typeable var) => [Term var] -> Context var -> Term var -> Term var
- go args ctx (TeTy_Var ((form_given <$>) .
- context_item_term <=< context_lookup ctx
- -> Just te))
- -- NOTE: Replace any variable mapped by the context
- = go args ctx te
- go args ctx (TeTy_App f a)
- -- NOTE: Collect applied arguments
- = go (a:args) ctx f
- go (x:args) ctx (Term_Abst _ _ f)
- -- NOTE: β-reduce: TeTy_App (Term_Abst _ _ f) x ==> f x
- = go args ctx (const x `unabstract` f)
- go args ctx (TeTy_Axiom (flip (axiom_normalize ctx) args -> Just (r_te, r_args)))
- -- NOTE: Normalize axiom
- -- TODO: maybe introduce an 'axiom_whnf' instead of 'axiom_normalize'
- = go r_args ctx r_te
- go args _ctx te
- -- NOTE: Reapply remaining arguments, normalized
- = term_apps te args
-
--- | Apply multiple 'Term's to a 'Term',
--- useful to reconstruct a 'Term' while normalizing (see 'normalize' or 'whnf').
-term_apps :: Term var -> [Term var] -> Term var
-term_apps = foldl TeTy_App
-
--- | /α-equivalence relation/, synonym of @(==)@.
---
--- Return 'True' iif. both given 'Term's are the same,
--- up to renaming the /bound variables/ it contains (see instance 'Eq' of 'Suggest').
-alpha_equiv :: (Eq var, Show var) => Term var -> Term var -> Bool
-alpha_equiv = (==)
-
--- | /αβη-equivalence relation/.
-equiv :: (Eq var, Ord var, Variable var, Typeable var) => Context var -> Term var -> Term var -> Bool
-equiv ctx = (==) `on` normalize ctx
-
--- * Type 'Type'
-
--- | 'Type' and 'Term' share the same data-type.
-type Type = Term
-
--- | Construct the 'Type' of the given 'Term',
--- effectively checking for the /well-formedness/
--- and /well-typedness/ of a 'Term' (or 'Type').
---
--- Note that a 'Type' is always to be considered
--- according to a given 'Context':
--- 'type_of' applied to the same 'Term'
--- but on different 'Context's
--- may return a different 'Type' or 'Type_Error'.
-type_of
- :: (Eq var, Ord var, Variable var, Typeable var)
- => Context var
- -> Term var
- -> Either Type_Error (Type var)
-type_of ctx term =
- case term of
- Type_Sort s -> (err +++ Type_Sort) $ sort_of_sort s
- TeTy_Var v ->
- case form_normal
- . context_item_type
- <$> context_lookup ctx v of
- Just ty -> return ty
- Nothing -> Left $ err $ Type_Error_Msg_Unbound_variable v
- TeTy_Axiom ax ->
- return $ axiom_type_of ctx ax
- TeTy_App f x -> do
- f_ty <- whnf ctx <$> type_of ctx f
- (f_in, f_out) <-
- case f_ty of
- Type_Abst _ i o -> return (i, o)
- _ -> Left $ err $ Type_Error_Msg_Not_a_function f f_ty
- x_ty <- type_of ctx x
- case equiv ctx x_ty f_in of
- True -> return $ const x `unabstract` f_out
- False -> Left $ err $ Type_Error_Msg_Function_argument_mismatch f_in x_ty
- Term_Abst (Suggest x) f_in f -> do
- _ <- type_of ctx f_in
- let new_ctx =
- if x == ""
- then context_push_nothing ctx
- else context_push_type ctx (Suggest x) f_in
- f_out <- type_of new_ctx (abstract_normalize f)
- let abst_ty = Type_Abst (Suggest x) f_in (abstract_generalize f_out)
- _ <- type_of ctx abst_ty
- return abst_ty
- Type_Abst (Suggest x) f_in f -> do
- f_in_ty <- type_of ctx f_in
- f_in_so <- case whnf ctx f_in_ty of
- Type_Sort s -> return s
- f_in_ty_whnf -> Left $ err $ Type_Error_Msg_Invalid_input_type f_in_ty_whnf
- let new_ctx =
- if x == ""
- then context_push_nothing ctx
- else context_push_type ctx (Suggest x) f_in
- f_out_ty <- type_of new_ctx (abstract_normalize f)
- f_out_so <- case whnf new_ctx f_out_ty of
- Type_Sort s -> return s
- f_out_ty_whnf -> Left $ Type_Error ctx term $
- Type_Error_Msg_Invalid_output_type f_out_ty_whnf (x, f_out_ty_whnf)
- (err +++ Type_Sort) $
- sort_of_type_abst f_in_so f_out_so
- where
- err = Type_Error ctx term
-
--- | Check that the given 'Term' has the given 'Type'.
-check
- :: (Eq var, Ord var, Variable var, Typeable var)
- => Context var
- -> Type var
- -> Term var
- -> Either (Type_Error) ()
-check ctx expect_ty te =
- type_of ctx te >>= \actual_ty ->
- if equiv ctx expect_ty actual_ty
- then Right ()
- else Left $ Type_Error
- { type_error_ctx = ctx
- , type_error_term = te
- , type_error_msg = Type_Error_Msg_Type_mismatch expect_ty actual_ty (normalize ctx expect_ty) (normalize ctx actual_ty)
- }
-
--- | Check that a 'Term' is closed, i.e. has no /unbound variables/.
-close :: Term Var_Name -> Either Type_Error (Term ())
-close te =
- traverse go te
- where
- go var = Left $
- Type_Error context te $
- Type_Error_Msg_Unbound_variable var
-
--- | Return the /unbound variables/ of given 'Term'.
-unbound_vars :: Ord var => Term var -> Map var ()
-unbound_vars = foldr (flip Map.insert ()) mempty
-
--- | /Dependent product/ rules: @s â t : u@, i.e.
--- "abstracting something of type @s@ out of something of type @t@ gives something of type @u@".
---
--- Given two 'Sort': @s@ and @t@, return a 'Sort': @u@,
--- when ('Type_Abst' @s@ @t@) is ruled legal
--- and has 'Type': 'Type_Sort' ('Sort' @u@).
---
--- The usual /PTS/ rules for /λÏ/
--- (or equivalently /Type Assignment Systems/ (TAS) rules for /System FÏ/)
--- are used here:
---
--- * RULE: @⦠* â * : *@, aka. /simple types/:
--- "abstracting a term out of a term is valid and gives a term",
--- as in /PTS λâ/ or /TAS F1/.
--- * RULE: @⦠⡠â * : *@, aka. /parametric polymorphism/:
--- "abstracting a type out of a term is valid and gives a term",
--- as in /PTS λ2/ or /TAS F2/ (aka. /System F/).
--- * RULE: @⦠⡠â â¡ : â¡@, aka. /constructors of types/:
--- "abstracting a type out of a type is valid and gives a type",
--- as in /PTS λÏ/ or /TAS FÏ/.
---
--- Note that the fourth usual rule is not ruled valid here:
---
--- * RULE: @⦠* â â¡ : â¡@, aka. /dependent types/:
--- "abstracting a term out of a type is valid and gives a type",
--- as in /PTS λPÏ/ or /TAS DFÏ/ (aka. /Calculus of constructions/).
---
--- However, to contain /impredicativity/ (see 'Axiom_MonoPoly')
--- the above /sort constants/ are split in two,
--- and the above rules adapted
--- to segregate between /monomorphic types/ (aka. /monotypes/)
--- and /polymorphic types/ (aka. /polytypes/):
---
--- * RULE: @⦠*m â *m : *m@, i.e. /simple types/, without /parametric polymorphism/.
--- * RULE: @⦠*m â *p : *p@, i.e. /simple types/, preserving /parametric polymorphism/ capture.
---
--- * RULE: @⦠*p â *m : *p@, i.e. /higher-rank polymorphism/, preserving /parametric polymorphism/ capture.
--- * RULE: @⦠*p â *p : *p@, i.e. /higher-rank polymorphism/, preserving /parametric polymorphism/ capture.
---
--- * RULE: @⦠â¡m â *m : *p@, i.e. /parametric polymorphism/, captured within @*p@ ('sort_star_poly').
--- * RULE: @⦠â¡m â *p : *p@, i.e. /parametric polymorphism/, preserving capture.
---
--- * RULE: @⦠â¡m â â¡m : â¡m@, i.e. /constructors of types/, without /parametric polymorphism/.
--- * RULE: @⦠â¡m â â¡p : â¡p@, i.e. /constructors of types/, preserving /parametric polymorphism/ capture.
---
--- Note that what is important here is
--- that there is no rule of the form: @⦠â¡p â _ : _@,
--- which forbids abstracting a /polymorphic type/ out of anything,
--- in particular the type @*p -> *m@ is forbidden,
--- though 'Axiom_MonoPoly'
--- is given to make it possible within it.
---
--- __Ressources:__
---
--- * /Henk: a typed intermediate language/,
--- Simon Peyton Jones, Erik Meijer, 20 May 1997,
--- https://research.microsoft.com/en-us/um/people/simonpj/papers/henk.ps.gz
-sort_of_type_abst
- :: Sort
- -> Sort
- -> Either Type_Error_Msg Sort
-
--- Simple types
-sort_of_type_abst
- (Type_Level_0, Type_Morphism_Mono)
- (Type_Level_0, m)
- = return (Type_Level_0, m)
- -- RULE: *m â *m : *m
- -- RULE: *m â *p : *p
- -- abstracting: a MONOMORPHIC term
- -- out of : a MONOMORPHIC (resp. POLYMORPHIC) term
- -- forms : a MONOMORPHIC (resp. POLYMORPHIC) term
-
--- Higher-rank
-sort_of_type_abst
- (Type_Level_0, Type_Morphism_Poly)
- (Type_Level_0, _)
- = return (Type_Level_0, Type_Morphism_Poly)
- -- RULE: *p â *m : *p
- -- RULE: *p â *p : *p
- -- abstracting: a POLYMORPHIC term
- -- out of : a term
- -- forms : a POLYMORPHIC term
-
--- Polymorphism
-sort_of_type_abst
- (Type_Level_1, Type_Morphism_Mono)
- (Type_Level_0, _)
- = return (Type_Level_0, Type_Morphism_Poly)
- -- RULE: â¡m â *m : *p
- -- RULE: â¡m â *p : *p
- -- abstracting: a MONOMORPHIC type of a term
- -- out of : a term
- -- forms : a POLYMORPHIC term
-
--- Type constructors
-sort_of_type_abst
- (Type_Level_1, Type_Morphism_Mono)
- (Type_Level_1, m)
- = return (Type_Level_1, m)
- -- RULE: â¡m â â¡m : â¡m
- -- RULE: â¡m â â¡p : â¡p
- -- abstracting: a MONOMORPHIC type of a term
- -- out of : a MONOMORPHIC (resp. POLYMORPHIC) type of a term
- -- forms : a MONOMORPHIC (resp. POLYMORPHIC) type of a term
- --
- -- NOTE: â¡m â â¡p : â¡p is useful for instance to build List_:
- -- let List_ : (A:*m) -> *p = \(A:*m) -> (R:*m) -> (A -> R -> R) -> R -> R
- -- let List : (A:*m) -> *m = \(A:*m) -> Monotype (List_ A)
-
--- Dependent types
-
-{-
-sort_of_type_abst
- (Type_Level_0, Type_Morphism_Mono)
- (Type_Level_1, m)
- = return (Type_Level_1, m)
- -- RULE: *m â â¡m : â¡m
- -- RULE: *m â â¡p : â¡p
- -- abstracting: a MONOMORPHIC term
- -- out of : a MONOMORPHIC (resp. POLYMORPHIC) type of a term
- -- forms : a MONOMORPHIC (resp. POLYMORPHIC) type of a term
-
-sort_of_type_abst
- (Type_Level_0, Type_Morphism_Poly)
- (Type_Level_1, _)
- = return (Type_Level_1, Type_Morphism_Poly)
- -- RULE: *p â â¡m : â¡p
- -- RULE: *p â â¡p : â¡p
- -- abstracting: a POLYMORPHIC term
- -- out of : a type of a term
- -- forms : a POLYMORPHIC type of a term
--}
-
-sort_of_type_abst
- s@(Type_Level_0, _)
- t@(Type_Level_1, _)
- = Left $ Type_Error_Msg_Illegal_type_abstraction s t
- -- RULE: * â â¡ : Illegal
- -- abstracting: a term
- -- out of : a type of a term
- -- is illegal
-
--- No impredicativity (only allowed through 'Axiom_MonoPoly')
-sort_of_type_abst
- s@(Type_Level_1, Type_Morphism_Poly)
- t@(_, _)
- = Left $ Type_Error_Msg_Illegal_type_abstraction s t
- -- RULE: â¡p â _ : Illegal
- -- abstracting: a POLYMORPHIC type of a term
- -- out of : anything
- -- is illegal
-
--- ** Type 'Type_Error'
-data Type_Error
- = forall var. (Ord var, Show var, Buildable var)
- => Type_Error
- { type_error_ctx :: Context var
- , type_error_term :: Term var
- , type_error_msg :: Type_Error_Msg
- }
-deriving instance Show Type_Error
-instance Buildable Type_Error where
- build (Type_Error ctx te msg) =
- "Error: Type_Error"
- <> "\n " <> build msg
- <> "\n Term:" <> " " <> build te
- <> (
- let vars =
- Map.keys $
- Map.intersection
- (unbound_vars te)
- (Map.fromList $ (, ()) <$> context_vars ctx) in
- case vars of
- [] -> "\n"
- _ -> "\n Context:\n" <> build ctx{context_vars=vars}
- )
-
--- ** Type 'Type_Error_Msg'
-data Type_Error_Msg
- = Type_Error_Msg_No_sort_for_sort Sort
- | Type_Error_Msg_Illegal_type_abstraction Sort Sort
- | forall var. Variable var => Type_Error_Msg_Invalid_input_type (Type var)
- | forall var. Variable var => Type_Error_Msg_Invalid_output_type (Type var) (Var_Name, Type var)
- | forall var. Variable var => Type_Error_Msg_Not_a_function (Term var) (Type var)
- | forall var. Variable var => Type_Error_Msg_Function_argument_mismatch (Type var) (Type var)
- | forall var. Variable var => Type_Error_Msg_Unbound_variable var
- | forall var. Variable var => Type_Error_Msg_Unbound_axiom var
- | forall var. Variable var => Type_Error_Msg_Type_mismatch (Type var) (Type var) (Type var) (Type var)
-deriving instance Show Type_Error_Msg
-instance Buildable Type_Error_Msg where
- build msg =
- case msg of
- Type_Error_Msg_No_sort_for_sort x ->
- "No_sort_for_sort: "
- <> build x
- Type_Error_Msg_Illegal_type_abstraction x y ->
- "Illegal_type_abstraction: "
- <> build x <> " -> " <> build y
- Type_Error_Msg_Invalid_input_type ty ->
- "Invalid_input_type: "
- <> build ty
- Type_Error_Msg_Invalid_output_type f_out (x, f_in) ->
- "Invalid_output_type: "
- <> build f_out <> "\n"
- <> " Input binding: "
- <> "(" <> build x <> " : " <> build f_in <> ")"
- Type_Error_Msg_Not_a_function f f_ty ->
- "Not_a_function: "
- <> build f
- <> " : "
- <> build f_ty
- Type_Error_Msg_Function_argument_mismatch f_in x_ty ->
- "Function_argument_mismatch: \n"
- <> " Function domain: " <> build f_in <> "\n"
- <> " Argument type: " <> build x_ty
- Type_Error_Msg_Unbound_variable var ->
- "Unbound_variable: "
- <> build var
- Type_Error_Msg_Unbound_axiom var ->
- "Unbound_axiom: "
- <> build var
- Type_Error_Msg_Type_mismatch x y nx ny ->
- "Type_mismatch: \n"
- <> " Expected type: " <> build x <> " == " <> build nx <> "\n"
- <> " Actual type: " <> build y <> " == " <> build ny
-
--- * Type 'Context'
-
--- | Map variables of type @var@
--- to their 'Type' and maybe also to their 'Term',
--- both in 'form_given' and 'form_normal'.
-data Context var
- = Context
- { context_vars :: [var]
- -- ^ used to dump the 'Context'
- , context_lookup :: var -> Maybe (Context_Item var)
- -- ^ used to query the 'Context'
- , context_lift :: Typeable var => Var_Name -> var
- -- ^ used to promote a ('Term' 'Var_Name') to ('Term' @var@)
- , context_unlift :: Typeable var => var -> Var_Name
- -- ^ used to unpromote ('Term' @var@) to ('Term' 'Var_Name')
- }
-data Context_Item var
- = Context_Item
- { context_item_term :: Maybe (Form var)
- , context_item_type :: Form var
- } deriving (Functor, Show)
-
-instance Show var => Show (Context var) where
- showsPrec n ctx@Context{context_vars=vars} =
- showParen (n > 10) $
- showString "Context " .
- showsPrec n ((\k ->
- (k, fromJust $ context_item_type
- <$> context_lookup ctx k))
- <$> vars) .
- showString " " .
- showsPrec n (catMaybes $ (\k ->
- (k,) . form_given <$>
- (context_item_term =<< context_lookup ctx k))
- <$> vars)
-instance Buildable var => Buildable (Context var) where
- build ctx@Context{context_vars=vars} =
- foldMap (\var ->
- " " <> build var
- <> maybe mempty (\ty -> " : " <> build (form_given ty))
- (context_item_type <$> context_lookup ctx var)
- {-
- <> maybe mempty (\te -> " = " <> build (form_given te))
- (context_item_term =<< context_lookup ctx var)
- -}
- <> "\n"
- ) vars
-
-context :: Context Var_Name
-context = Context [] (const Nothing) id id
-
-context_apply :: Context var -> Term var -> Term var
-context_apply ctx te =
- te >>= \var ->
- maybe (TeTy_Var var) id $ form_normal <$>
- (context_item_term =<< context_lookup ctx var)
-
-context_push_type
- :: (Eq var, Ord var, Variable var, Typeable var)
- => Context var
- -> bound
- -> Type var
- -> Context (Var bound var)
-context_push_type
- ctx@(Context keys lookup var_lift var_unlift)
- bound ty =
- Context
- { context_vars =
- Var_Bound bound :
- Var_Free `fmap` keys
- , context_lookup = \var ->
- (Var_Free `fmap`) `fmap`
- case var of
- Var_Bound _ ->
- Just $ Context_Item
- { context_item_term = Nothing
- , context_item_type = form ctx ty
- }
- Var_Free v -> lookup v
- , context_lift = Var_Free . var_lift
- , context_unlift = \var ->
- case var of
- Var_Bound _ -> error "context_push_type: context_unlift"
- Var_Free v -> var_unlift v
- }
-
-context_push_nothing
- :: (Show bound, Buildable (Context var), Typeable var, Typeable bound)
- => Context var
- -> Context (Var bound var)
-context_push_nothing
- (Context keys lookup var_lift var_unlift) =
- Context
- { context_vars = Var_Free `fmap` keys
- , context_lookup = \var ->
- (Var_Free `fmap`) `fmap`
- case var of
- Var_Bound _ -> Nothing
- Var_Free v -> lookup v
- , context_lift = Var_Free . var_lift
- , context_unlift = \var ->
- case var of
- -- DEBUG: Var_Bound (cast -> Just (Suggest b)) -> b
- -- DEBUG: Var_Bound (cast -> Just b) -> b
- Var_Bound b -> error $ "context_push_nothing: context_unlift: " ++ show b
- Var_Free v -> var_unlift v
- }
-
-context_from_env :: Env -> Context Var_Name
-context_from_env env =
- Context
- { context_vars = Map.keys env
- , context_lookup = \var ->
- (\item -> Context_Item
- { context_item_term = Just $ env_item_term item
- , context_item_type = env_item_type item
- }) <$> env_lookup env var
- , context_lift = id
- , context_unlift = id
- }
-
-context_relift :: forall from_var to_var.
- ( Typeable from_var
- , Typeable to_var )
- => Context from_var
- -> Type from_var
- -> Context to_var
- -> Type to_var
-context_relift from_ctx ty to_ctx =
- ( context_lift to_ctx
- . context_unlift from_ctx
- ) <$> ty
-
-{-
-context_from_list :: Eq var => [(var, Type var)] -> Context var
-context_from_list l =
- Context
- { context_vars = fst <$> l
- , context_lookup_type = \var -> List.lookup var l
- }
-
--- | Return /free term variables/ of an 'Abstraction'-ed 'Term'.
-ftv
- :: Abstraction bound (Term) var
- -> Term (Var bound var)
-ftv = abstract_normalize
--}
-
--- * Type 'Env'
-type Env
- = Map Var_Name Env_Item
-data Env_Item
- = Env_Item
- { env_item_term :: Form Var_Name
- , env_item_type :: Form Var_Name
- }
-env_item
- :: Context Var_Name
- -> Term Var_Name
- -> Type Var_Name
- -> Env_Item
-env_item ctx te ty =
- Env_Item
- { env_item_term = form ctx te
- , env_item_type = form ctx ty
- }
-
-env_lookup :: Env -> Var_Name -> Maybe (Env_Item)
-env_lookup env var = Map.lookup var env
-
-env_insert :: Var_Name -> Term Var_Name -> Type Var_Name -> Env -> Env
-env_insert var te ty env =
- let ctx = context_from_env env in
- Map.insert var (env_item ctx te ty) env
-
--- * Type 'Axiom'
-
-data family Axiom r
--- deriving instance Typeable Axiom
-
-axiom_cast :: (Typeable a, Typeable b) => Axiom a -> Maybe (Axiom b)
-axiom_cast = cast
-
--- ** Type 'Axioms'
--- | 'Axioms' are made of 'Axiom's injected in regular 'Env_Item's,
--- see 'env_item_from_axiom'.
-type Axioms = Env
-
-env_item_from_axiom
- :: ( Axiomable (Axiom ax)
- , Typeable ax )
- => Context Var_Name -> Axiom ax -> Env_Item
-env_item_from_axiom ctx ax =
- Env_Item
- { env_item_term = form ctx $ TeTy_Axiom ax
- , env_item_type = form ctx $ axiom_type_of ctx ax
- }
-
--- ** Class 'Axiomable'
-
--- class (Eq ax, Show ax, Buildable ax, Typeable ax) => Axiomable_Type_Of ax where
--- class (Eq ax, Show ax, Buildable ax, Typeable ax) => Axiomable_Normalize ax where
--- class (Eq ax, Show ax, Buildable ax, Typeable ax) => Axiomable_Eq ax where
-
--- | Instances of this class are 'Axiom's injectable in 'TeTy_Axiom', that is:
---
--- * they have a 'Type', given by 'axiom_type_of',
--- * and they can perform an optional reduction
--- within 'normalize' or 'whnf', given by 'axiom_normalize'.
-class
- ( Eq ax, Show ax, Buildable ax, Typeable ax
- -- , Axiomable_Type_Of ax
- -- , Axiomable_Normalize ax
- -- , Axiomable_Eq ax
- ) => Axiomable ax where
- axiom_type_of
- :: forall var. Typeable var
- => Context var -> ax -> Type var
- -- ^ Return the 'Type' of the given 'Axiomable' instance.
- axiom_normalize
- :: forall var. (Typeable var, Ord var, Variable var)
- => Context var -> ax -> [Term var] -> Maybe (Term var, [Term var])
- -- ^ Custom-'normalize': given a typing 'Context',
- -- an 'Axiomable' instance
- -- and a list of arguments, return:
- --
- -- * 'Nothing': if the axiom performs no reduction,
- -- * 'Just': with the reducted 'Term' and the arguments not used by the reduction.
- --
- -- Default: @\\_ctx _ax _args -> Nothing@
- axiom_normalize _ctx _ax _args = Nothing
- axiom_eq :: ax -> (forall ax'. Axiomable ax' => ax' -> Bool)
- -- ^ Custom-bipolymorphic-@(==)@:
- -- given an 'Axiomable' instance
- -- return a function to test if any
- -- other 'Axiomable' instance
- -- is equal to the first instance given.
- --
- -- Default: @maybe False (x ==) (cast y)@
- axiom_eq x y = maybe False (x ==) (cast y)
-
--- ** Class 'Axiom_Type'
-
--- | A class to embed an Haskell-type within an 'Axiom'.
-class Axiom_Type h where
- axiom_type :: Axiom h
- -- ^ Construct (implicitely) an Haskell-term representing
- -- the Haskell-type @h@.
- axiom_Type :: Axiom h -> Type Var_Name
- -- ^ Return a 'Type' representing the Haskell-type @h@,
- -- given through its representation as an Haskell-term
- -- (which is an 'Axiom' and thus has itself a 'Type',
- -- given by its 'axiom_type_of').
-
-axiom_term
- :: (Axiom_Type h, Typeable h)
- => h -> Axiom (Axiom_Term h)
-axiom_term (x::h) =
- Axiom_Term x $ \ctx ->
- context_lift ctx <$> axiom_Type (axiom_type::Axiom h)
-
--- ** Type 'Axiom_Type_Assume'
--- | An instance to use 'Type' as an 'Axiom'.
-data Axiom_Type_Assume
-newtype instance Axiom (Axiom_Type_Assume)
- = Axiom_Type_Assume (Type Var_Name)
- deriving (Eq, Show)
-instance Buildable (Axiom Axiom_Type_Assume) where
- build (Axiom_Type_Assume ty) = "(_:" <> build ty <> ")"
-instance Axiomable (Axiom Axiom_Type_Assume) where
- axiom_type_of ctx (Axiom_Type_Assume ty) =
- context_lift ctx <$> ty
-
--- ** Type 'Axiom_MonoPoly'
--- | Non-'Sort' constants for /boxed parametric polymorphism/.
---
--- Used to embed /polymorphic types/ into first-class /monomorphic types/
--- via explicit injection ('Axiom_Term_MonoPoly_Box') and projection ('Axiom_Term_MonoPoly_UnBox') functions.
---
--- Special treatment of 'Axiom_MonoPoly' constructors is done in 'normalize' and 'whnf'
--- to remove adjacent pairs of 'Axiom_Term_MonoPoly_Box' / 'Axiom_Term_MonoPoly_UnBox'
--- or 'Axiom_Term_MonoPoly_UnBox' / 'Axiom_Term_MonoPoly_Box'.
---
--- __Ressources:__
---
--- * /Recasting MLF/, Didier Le Botlan, Didier Rémy, June 2009,
--- https://hal.inria.fr/inria-00156628
-data Axiom_MonoPoly
-data instance Axiom Axiom_MonoPoly
- = Axiom_Type_MonoPoly
- | Axiom_Term_MonoPoly_Box
- | Axiom_Term_MonoPoly_UnBox
- deriving (Eq, Ord, Show)
-instance Buildable (Axiom Axiom_MonoPoly) where
- build ax = case ax of
- Axiom_Type_MonoPoly -> "Monotype"
- Axiom_Term_MonoPoly_Box -> "monotype"
- Axiom_Term_MonoPoly_UnBox -> "polytype"
-instance Axiomable (Axiom Axiom_MonoPoly) where
- axiom_type_of ctx ax =
- case ax of
- Axiom_Type_MonoPoly ->
- -- Monotype : *p -> *m
- Type_Abst "" (Type_Sort sort_star_poly) $
- (const Nothing `abstract`) $
- Type_Sort sort_star_mono
- Axiom_Term_MonoPoly_Box ->
- -- monotype : (Polytype : *p) -> Polytype -> Monotype Polytype
- (context_lift ctx <$>) $
- Type_Abst "Polytype" (Type_Sort sort_star_poly) $
- (("Polytype" =?) `abstract`) $
- Type_Abst "" (TeTy_Var "Polytype") $
- (("" =?) `abstract`) $
- TeTy_App
- (TeTy_Axiom $ Axiom_Type_MonoPoly)
- (TeTy_Var "Polytype")
- Axiom_Term_MonoPoly_UnBox ->
- -- polytype : (Polytype : *p) -> Monotype Polytype -> Polytype
- (context_lift ctx <$>) $
- Type_Abst "Polytype" (Type_Sort sort_star_poly) $
- (("Polytype" =?) `abstract`) $
- Type_Abst ""
- (TeTy_App
- (TeTy_Axiom $ Axiom_Type_MonoPoly)
- (TeTy_Var "Polytype")) $
- (("" =?) `abstract`) $
- TeTy_Var "Polytype"
- axiom_normalize _ctx
- Axiom_Term_MonoPoly_UnBox
- (_ty:TeTy_App (TeTy_App (TeTy_Axiom (axiom_cast -> Just Axiom_Term_MonoPoly_Box)) _ty') te:args)
- -- NOTE: Remove adjacent Axiom_Term_MonoPoly_UnBox / Axiom_Term_MonoPoly_Box
- = Just (te, args)
- axiom_normalize _ctx
- Axiom_Term_MonoPoly_Box
- (_ty:TeTy_App (TeTy_App (TeTy_Axiom (axiom_cast -> Just Axiom_Term_MonoPoly_UnBox)) _ty') te:args)
- -- NOTE: Remove adjacent Axiom_Term_MonoPoly_Box / Axiom_Term_MonoPoly_UnBox
- = Just (te, args)
- axiom_normalize _ctx _ax _args = Nothing
-
--- | /PTS/ axioms for 'Axiom_MonoPoly':
---
--- * AXIOM: @⦠Monotype : *p -> *m@
--- * AXIOM: @⦠monotype : (Polytype : *p) -> Polytype -> Monotype Polytype@
--- * AXIOM: @⦠polytype : (Polytype : *p) -> Monotype Polytype -> Polytype@
-axioms_monopoly :: Axioms
-axioms_monopoly =
- Map.fromList $
- [ ("Monotype", item Axiom_Type_MonoPoly)
- , ("monotype", item Axiom_Term_MonoPoly_Box)
- , ("polytype", item Axiom_Term_MonoPoly_UnBox)
- ]
- where
- item = env_item_from_axiom ctx
- ctx = context_from_env mempty
-
--- ** Type 'Axiom_Term'
-
--- | Embed an Haskell-term of Haskell-type @h@ within an 'Axiom'
-data Axiom_Term h
-data instance Axiom (Axiom_Term h)
- = Typeable h
- => Axiom_Term h
- (forall var. Typeable var => Context var -> Type var)
- deriving (Typeable)
-
--- Instance 'Axiom' 'Integer'
-data instance Axiom Integer
- = Axiom_Type_Integer
- deriving (Eq, Ord, Show)
-instance Buildable (Axiom Integer) where
- build Axiom_Type_Integer = "Int"
-instance Axiomable (Axiom Integer) where
- axiom_type_of _ctx Axiom_Type_Integer =
- Type_Sort (Type_Level_0, Type_Morphism_Mono)
-
-instance Axiom_Type Integer where
- axiom_type = Axiom_Type_Integer
- axiom_Type = TeTy_Axiom
-instance Eq (Axiom (Axiom_Term Integer)) where
- Axiom_Term x _ == Axiom_Term y _ = x == y
-instance Ord (Axiom (Axiom_Term Integer)) where
- Axiom_Term x _ `compare` Axiom_Term y _ = x `compare` y
-instance Show (Axiom (Axiom_Term Integer)) where
- showsPrec n (Axiom_Term te ty) =
- showParen (n > 10) $
- showString "Axiom_Term " .
- showsPrec n te .
- showString " " .
- showsPrec n (ty context)
-instance Buildable (Axiom (Axiom_Term Integer)) where
- build (Axiom_Term i _ty) = build i
-instance Axiomable (Axiom (Axiom_Term Integer)) where
- axiom_type_of _ctx (Axiom_Term _ _ty) =
- TeTy_Axiom Axiom_Type_Integer
-
--- Instance 'Axiom' '()'
-data instance Axiom ()
- = Axiom_Type_Unit
- deriving (Eq, Ord, Show)
-instance Buildable (Axiom ()) where
- build (Axiom_Type_Unit) = "()"
-instance Axiomable (Axiom ()) where
- axiom_type_of _ctx Axiom_Type_Unit =
- Type_Sort (Type_Level_0, Type_Morphism_Mono)
-
-instance Axiom_Type () where
- axiom_type = Axiom_Type_Unit
- axiom_Type = TeTy_Axiom
-instance Eq (Axiom (Axiom_Term ())) where
- Axiom_Term x _ == Axiom_Term y _ = x == y
-instance Ord (Axiom (Axiom_Term ())) where
- Axiom_Term x _ `compare` Axiom_Term y _ = x `compare` y
-instance Show (Axiom (Axiom_Term ())) where
- showsPrec n (Axiom_Term te ty) =
- showParen (n > 10) $
- showString "Axiom_Term " .
- showsPrec n te .
- showString " " .
- showsPrec n (ty context)
-instance Buildable (Axiom (Axiom_Term ())) where
- build (Axiom_Term _te _ty) = "()"
-instance Axiomable (Axiom (Axiom_Term ())) where
- axiom_type_of _ctx (Axiom_Term _te _ty) =
- TeTy_Axiom Axiom_Type_Unit
-
--- Instance 'Axiom' 'Text'
-data instance Axiom Text
- = Axiom_Type_Text
- deriving (Eq, Ord, Show)
-instance Buildable (Axiom Text) where
- build (Axiom_Type_Text) = "Text"
-instance Axiomable (Axiom Text) where
- axiom_type_of _ctx Axiom_Type_Text =
- Type_Sort (Type_Level_0, Type_Morphism_Mono)
-
-instance Axiom_Type Text where
- axiom_type = Axiom_Type_Text
- axiom_Type = TeTy_Axiom
-instance Eq (Axiom (Axiom_Term Text)) where
- Axiom_Term x _ == Axiom_Term y _ = x == y
-instance Ord (Axiom (Axiom_Term Text)) where
- Axiom_Term x _ `compare` Axiom_Term y _ = x `compare` y
-instance Show (Axiom (Axiom_Term Text)) where
- showsPrec n (Axiom_Term te ty) =
- showParen (n > 10) $
- showString "Axiom_Term " .
- showsPrec n te .
- showString " " .
- showsPrec n (ty context)
-instance Buildable (Axiom (Axiom_Term Text)) where
- build (Axiom_Term t _) = build $ show t
-instance Axiomable (Axiom (Axiom_Term Text)) where
- axiom_type_of _ctx (Axiom_Term _te _ty) =
- TeTy_Axiom Axiom_Type_Text
-
--- Instance 'Axiom' type variable
-
--- ** Type 'Axiom_Type_Var'
-
--- | Singleton type, whose constructors
--- are bijectively mapped to Haskell types
--- of kind 'Type_Var'.
-data Axiom_Type_Var (v::Type_Var) where
- Axiom_Type_Var_Zero :: Axiom_Type_Var 'Type_Var_Zero
- Axiom_Type_Var_Succ :: Axiom_Type_Var v -> Axiom_Type_Var ('Type_Var_Succ v)
-deriving instance Eq (Axiom_Type_Var v)
-deriving instance Ord (Axiom_Type_Var v)
-deriving instance Show (Axiom_Type_Var v)
-deriving instance Typeable Axiom_Type_Var
-instance Buildable (Axiom_Type_Var v) where
- build v = build $ type_var_string v
-
--- *** Type 'Type_Var'
-
--- | Natural numbers (aka. /Peano numbers/)
--- promoted by @DataKinds@ to Haskell type-level.
-data Type_Var
- = Type_Var_Zero
- | Type_Var_Succ Type_Var
- deriving (Eq, Ord, Show, Typeable)
-
-type A = Axiom_Type_Var 'Type_Var_Zero
-type B = Axiom_Type_Var ('Type_Var_Succ 'Type_Var_Zero)
-type C = Axiom_Type_Var ('Type_Var_Succ ('Type_Var_Succ 'Type_Var_Zero))
--- ^ â¦aliases only for the first few 'Axiom_Type_Var' used: extend on need.
-
--- | Return the Haskell term-level 'Int' encoded by the given Haskell type-level @(v :: 'Type_Var')@.
-type_var_int :: Axiom_Type_Var v -> Int
-type_var_int v =
- case v of
- Axiom_Type_Var_Zero -> 0
- Axiom_Type_Var_Succ n -> 1 + type_var_int n
-
--- | Return a readable 'String' encoding the given Haskell type-level @(v :: 'Type_Var')@.
---
--- First 26 variables give: @\"A"@ to @\"Z"@,
--- and followings give: @(\"A" ++ show n)@, where @n@ is a positive 'Int' starting at @0@.
-type_var_string :: Axiom_Type_Var v -> String
-type_var_string v =
- case type_var_int v of
- x | 0 <= x && x < 26 -> [Char.chr (Char.ord 'A' + x)]
- x -> 'A' : show (x - 26)
-
--- *** Class 'Type_Var_Implicit'
-class Type_Var_Implicit (v::Type_Var) where
- type_var :: Axiom_Type_Var v
-instance Type_Var_Implicit 'Type_Var_Zero where
- type_var = Axiom_Type_Var_Zero
-instance Type_Var_Implicit v => Type_Var_Implicit ('Type_Var_Succ v) where
- type_var = Axiom_Type_Var_Succ type_var
-
-data instance Axiom (Axiom_Type_Var (v::Type_Var))
- = Axiom_Type_Var (Axiom_Type_Var v)
- deriving (Eq, Ord, Show)
-instance Buildable (Axiom (Axiom_Type_Var (v::Type_Var))) where
- build (Axiom_Type_Var v) = build v
-instance (Typeable v) => Axiomable (Axiom (Axiom_Type_Var (v::Type_Var))) where
- axiom_type_of _ctx (Axiom_Type_Var _v) =
- Type_Sort (Type_Level_0, Type_Morphism_Mono)
-instance Type_Var_Implicit v => Axiom_Type (Axiom_Type_Var (v::Type_Var)) where
- axiom_type = Axiom_Type_Var (type_var::Axiom_Type_Var v)
- axiom_Type (Axiom_Type_Var v) = TeTy_Var $ Text.pack $ type_var_string v
-
-instance Eq (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
- Axiom_Term x _ == Axiom_Term y _ = x == y
-instance Ord (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
- Axiom_Term x _ `compare` Axiom_Term y _ = x `compare` y
-instance Show (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
- showsPrec n (Axiom_Term v ty) =
- showParen (n > 10) $
- showString "Axiom_Term " .
- (showParen (n > 10) $
- showString "Axiom_Type_Var " .
- showsPrec n v) .
- showString " " .
- (showParen (n > 10) $
- showString " " .
- showsPrec n (ty context))
-instance Buildable (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
- build (Axiom_Term v _ty) = build v
-instance Typeable v => Axiomable (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
- axiom_type_of ctx (Axiom_Term _ ty) = ty ctx
-
--- Instance 'Axiom' '->'
-data instance Axiom (i -> o)
- = Axiom_Term_Abst (Axiom i) (Axiom o)
-deriving instance (Eq (Axiom i), Eq (Axiom o)) => Eq (Axiom (i -> o))
-deriving instance (Ord (Axiom i), Ord (Axiom o)) => Ord (Axiom (i -> o))
-deriving instance (Show (Axiom i), Show (Axiom o)) => Show (Axiom (i -> o))
-instance (Buildable (Axiom i), Buildable (Axiom o)) => Buildable (Axiom (i -> o)) where
- build (Axiom_Term_Abst i o) =
- "(" <> build i <> " -> " <> build o <> ")"
-instance
- ( Typeable i
- , Typeable o
- , Eq (Axiom i)
- , Show (Axiom i)
- , Buildable (Axiom i)
- , Eq (Axiom o)
- , Show (Axiom o)
- , Buildable (Axiom o)
- -- , Axiomable (Axiom i)
- -- , Axiomable (Axiom o)
- ) => Axiomable (Axiom (i -> o)) where
- axiom_type_of _ctx (Axiom_Term_Abst _i _o) =
- Type_Sort (Type_Level_0, Type_Morphism_Mono)
-
-instance (Axiom_Type i, Axiom_Type o) => Axiom_Type (i -> o) where
- axiom_type =
- Axiom_Term_Abst
- axiom_type
- axiom_type
- axiom_Type (Axiom_Term_Abst i o) =
- Type_Abst ""
- (axiom_Type i) $
- (const Nothing `abstract`) $
- (axiom_Type o)
-instance Eq (Axiom (Axiom_Term (i -> o))) where
- (==) = error "Eq Axiom: (==) on functions"
-instance Ord (Axiom (Axiom_Term (i -> o))) where
- compare = error "Eq Axiom: compare on functions"
-instance
- {-( Buildable (Axiom (i -> o))
- ) =>-} Show (Axiom (Axiom_Term (i -> o))) where
- showsPrec n (Axiom_Term _ ty) =
- showParen (n > 10) $
- showString "Axiom_Term " .
- showString "(_:" .
- showString (
- Text.unpack $
- TL.toStrict $
- Builder.toLazyText $
- build (ty context)
- ) .
- showString ")"
-instance
- {-( Buildable (Axiom i)
- , Buildable (Axiom o)
- ) =>-} Buildable (Axiom (Axiom_Term (i -> o))) where
- build (Axiom_Term _o ty) =
- "(_:" <> build (ty context) <> ")"
-
-instance
- ( Typeable (Term var)
- , Typeable o
- , Axiomable (Axiom (Axiom_Term o))
- -- , Axiomable (Axiom (Term var))
- -- , Axiomable (Axiom o)
- -- , Buildable (Axiom (Term var))
- -- , Show (Axiom (Axiom_Term (Term var)))
- -- , Show (Axiom (Axiom_Term o))
- ) => Axiomable (Axiom (Axiom_Term (Term var -> o))) where
- axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
- axiom_normalize (ctx::Context var_)
- {-ax@-}(Axiom_Term (cast -> Just (o::Term var_ -> o)) o_ty)
- (arg:args) =
- {-
- trace ("axiom_normalize (i -> o): Term"
- ++ "\n ax=" ++
- (Text.unpack $
- TL.toStrict $
- Builder.toLazyText $
- build (ax))
- ++ "\n ax=" ++ show ax
- ++ "\n ty(ax)=" ++ show (typeOf ax)
- ++ "\n arg=" ++ show (context_unlift ctx <$> arg)
- ++ "\n args=" ++ show ((context_unlift ctx <$>) <$> args)
- ++ "\n o=" ++ show (Axiom_Term (o arg) o_ty)
- ) $
- -}
- case type_of ctx arg of
- Right i_ty ->
- case o_ty ctx of
- Type_Abst _ _o_in o_out ->
- let oi = o arg in
- let oi_ty = const i_ty `unabstract` o_out in
- Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
- _ -> Nothing
- _ -> Nothing
- axiom_normalize _ctx _ax _args = Nothing
-
-instance
- ( Typeable (Term var -> io)
- , Typeable o
- , Typeable io
- , Axiomable (Axiom (Axiom_Term o))
- -- , Axiomable (Axiom (Term var -> io))
- -- , Axiomable (Axiom o)
- -- , Show (Axiom (Axiom_Term (Term var -> io)))
- -- , Show (Axiom (Axiom_Term o))
- ) => Axiomable (Axiom (Axiom_Term ((Term var -> io) -> o))) where
- axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
- axiom_normalize
- (ctx::Context var_)
- {-ax@-}(Axiom_Term (cast -> Just (o::(Term var_ -> io) -> o)) o_ty)
- (arg@(Term_Abst _arg_v _arg_f_in arg_f):args) =
- case type_of ctx arg of
- Right i_ty ->
- case o_ty ctx of
- Type_Abst _ _o_in o_out ->
- {-
- trace ("axiom_normalize (i -> o): Term ->"
- ++ "\n ax=" ++
- (Text.unpack $
- TL.toStrict $
- Builder.toLazyText $
- build (ax))
- ++ "\n ax=" ++ show ax
- ++ "\n args=" ++ show ((context_unlift ctx <$>) <$> args)
- ++ "\n ty(args)=" ++ show (typeOf <$> args)
- ++ "\n ty(ax)=" ++ show (typeOf ax)
- ++ "\n i~" ++ show (typeOf (undefined::Term var -> io))
- ++ "\n o~" ++ show (typeOf (undefined::o))
- ++ "\n i=" ++ show (typeOf i)
- ) $
- -}
- let i te =
- case normalize ctx (const te `unabstract` arg_f) of
- TeTy_Axiom (axiom_cast -> Just (Axiom_Term io _io_ty)) -> io
- _ -> error "axiom_normalize: Axiom_Term ((Term var -> io) -> o): cannot extract io"
- in
- let oi = o i in
- let oi_ty = const i_ty `unabstract` o_out in
- Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
- _ -> Nothing
- _ -> Nothing
- axiom_normalize ctx
- (Axiom_Term o o_ty)
- (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
- =
- case o_ty ctx of
- Type_Abst _ _o_in o_out ->
- let oi = o i in
- let oi_ty = const (i_ty ctx) `unabstract` o_out in
- {-
- trace ("axiom_normalize (i -> o): Term var -> io"
- ++ (
- Text.unpack $
- TL.toStrict $
- Builder.toLazyText $
- build (context_unlift ctx <$> oi_ty))
- ) $
- -}
- Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
- _ -> Nothing
- axiom_normalize _ctx _ax _args = Nothing
-
-instance
- ( Typeable (Axiom_Type_Var v -> io)
- , Typeable o
- , Axiomable (Axiom (Axiom_Type_Var v -> io))
- , Axiomable (Axiom o)
- , Axiomable (Axiom (Axiom_Term o))
- , Show (Axiom (Axiom_Term (Axiom_Type_Var v -> io)))
- , Show (Axiom (Axiom_Term o))
- ) => Axiomable (Axiom (Axiom_Term ((Axiom_Type_Var v -> io) -> o))) where
- axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
-
-instance
- ( Typeable Integer
- , Typeable o
- , Axiomable (Axiom Integer)
- , Axiomable (Axiom o)
- , Axiomable (Axiom (Axiom_Term o))
- , Show (Axiom (Axiom_Term Integer))
- , Show (Axiom (Axiom_Term o))
- ) => Axiomable (Axiom (Axiom_Term (Integer -> o))) where
- axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
- axiom_normalize ctx
- (Axiom_Term o o_ty)
- (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
- =
- case o_ty ctx of
- Type_Abst _ _o_in o_out ->
- let oi = o i in
- let oi_ty = const (i_ty ctx) `unabstract` o_out in
- {-
- trace ("axiom_normalize (i -> o): "
- ++ (
- Text.unpack $
- TL.toStrict $
- Builder.toLazyText $
- build (context_unlift ctx <$> oi_ty))
- ) $
- -}
- Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
- _ -> Nothing
- axiom_normalize _ctx _ax _args = Nothing
-
-instance
- ( Typeable Text
- , Typeable o
- , Axiomable (Axiom Text)
- , Axiomable (Axiom o)
- , Axiomable (Axiom (Axiom_Term o))
- , Show (Axiom (Axiom_Term Text))
- , Show (Axiom (Axiom_Term o))
- ) => Axiomable (Axiom (Axiom_Term (Text -> o))) where
- axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
- axiom_normalize ctx
- (Axiom_Term o o_ty)
- (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
- =
- case o_ty ctx of
- Type_Abst _ _o_in o_out ->
- let oi = o i in
- let oi_ty = const (i_ty ctx) `unabstract` o_out in
- {-
- trace ("axiom_normalize (i -> o): "
- ++ (
- Text.unpack $
- TL.toStrict $
- Builder.toLazyText $
- build (context_unlift ctx <$> oi_ty))
- ) $
- -}
- Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
- _ -> Nothing
- axiom_normalize _ctx _ax _args = Nothing
-
-instance
- ( Typeable (Axiom_Type_Var v)
- , Typeable o
- , Axiomable (Axiom (Axiom_Type_Var v))
- , Axiomable (Axiom o)
- , Axiomable (Axiom (Axiom_Term o))
- , Show (Axiom (Axiom_Term (Axiom_Type_Var v)))
- , Show (Axiom (Axiom_Term o))
- ) => Axiomable (Axiom (Axiom_Term (Axiom_Type_Var v -> o))) where
- axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
- axiom_normalize ctx
- (Axiom_Term o o_ty)
- (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
- =
- case o_ty ctx of
- Type_Abst _ _o_in o_out ->
- let oi = o i in
- let oi_ty = const (i_ty ctx) `unabstract` o_out in
- {-
- trace ("axiom_normalize (i -> o): "
- ++ (
- Text.unpack $
- TL.toStrict $
- Builder.toLazyText $
- build (context_unlift ctx <$> oi_ty))
- ) $
- -}
- Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
- _ -> Nothing
- axiom_normalize _ctx _ax _args = Nothing
-
-instance
- ( Typeable (IO a)
- , Typeable o
- , Typeable a
- , Axiomable (Axiom (Axiom_Term o))
- , Show (Axiom (Axiom_Term (IO a)))
- , Show (Axiom (Axiom_Term o))
- -- , Axiomable (Axiom (IO a))
- -- , Axiomable (Axiom o)
- ) => Axiomable (Axiom (Axiom_Term (IO a -> o))) where
- axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
- axiom_normalize ctx
- (Axiom_Term o o_ty)
- (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
- =
- case o_ty ctx of
- Type_Abst _ _o_in o_out ->
- let oi = o i in
- let oi_ty = const (i_ty ctx) `unabstract` o_out in
- {-
- trace ("axiom_normalize (Axiom_Term ((IO a) -> o)): "
- ++ (
- Text.unpack $
- TL.toStrict $
- Builder.toLazyText $
- build (context_unlift ctx <$> oi_ty))
- ) $
- -}
- Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
- _ -> Nothing
- axiom_normalize (ctx::Context var)
- (Axiom_Term o o_ty)
- (TeTy_Axiom (axiom_cast -> Just (Axiom_Term (i::IO (Term var)) i_ty)):args)
- =
- case o_ty ctx of
- Type_Abst _ _o_in o_out ->
- let oi = o $
- (\te ->
- case normalize ctx te of
- TeTy_Axiom (axiom_cast -> Just (Axiom_Term io _io_ty)) -> io
- _ -> error "axiom_normalize: Axiom_Term ((Term var -> io) -> o): cannot extract io"
- ) <$> i in
- let oi_ty = const (i_ty ctx) `unabstract` o_out in
- Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
- _ -> Nothing
- axiom_normalize _ctx _ax _args = Nothing
-
--- ** Type 'Axiom_Type_Abst'
-
--- | Encode a @forall a.@ within an 'Axiom'.
-data Axiom_Type_Abst
-data instance Axiom (Axiom_Type_Abst)
- = Axiom_Type_Abst
- { axiom_type_abst_Var ::
- (Suggest Var_Name)
- -- ^ A name for the variable inhabiting the abstracting 'Type'.
- , axiom_type_abst_Term ::
- (Type Var_Name -> Term Var_Name)
- -- ^ The abstracted 'Term', abstracted by a 'Type'.
- , axiom_type_abst_Type ::
- (Abstraction (Suggest Var_Name) Type Var_Name)
- -- ^ The 'Type' of the abstracted 'Term'
- -- (not exactly a 'Type', but just enough to build it with 'Type_Abst').
- }
- deriving (Typeable)
-instance Eq (Axiom (Axiom_Type_Abst)) where
- Axiom_Type_Abst{} == Axiom_Type_Abst{} =
- error "Eq Axiom_Type_Abst" -- maybe False (x ==) (cast y)
-instance Show (Axiom (Axiom_Type_Abst)) where
- show (Axiom_Type_Abst{}) = "Axiom_Type_Abst"
-instance Buildable (Axiom (Axiom_Type_Abst)) where
- build ax = "(_:" <> (build $ axiom_type_of context ax) <> ")"
-instance Axiomable (Axiom (Axiom_Type_Abst)) where
- axiom_type_of ctx (Axiom_Type_Abst v _o ty) =
- Type_Abst v
- (Type_Sort (Type_Level_0, Type_Morphism_Mono)) $
- (context_lift ctx <$> ty)
- axiom_normalize ctx
- {-ax@-}(Axiom_Type_Abst _ o ty)
- (arg:args)
- =
- let a = context_unlift ctx <$> arg in
- let ty_a = const a `unabstract` ty in
- let r = o $ ty_a in
- {-
- trace ("axiom_normalize: Axiom_Type_Abst:"
- ++ "\n a=" ++
- (Text.unpack $
- TL.toStrict $
- Builder.toLazyText $
- build (a)
- )
- ++ "\n ty=" ++
- (Text.unpack $
- TL.toStrict $
- Builder.toLazyText $
- build (axiom_type_of context ax)
- )
- ++ "\n ty_a=" ++
- (Text.unpack $
- TL.toStrict $
- Builder.toLazyText $
- build (ty_a)
- )
- ++ "\n r=" ++
- (show r
- )
- ) $
- -}
- Just (context_lift ctx <$> r, args)
- axiom_normalize _ctx _ax _args = Nothing
-
--- Instance 'Axiom' 'IO'
-data instance Axiom (IO a)
- = Axiom_Type_IO
- deriving (Eq, Ord, Show)
-instance Buildable (Axiom (IO a)) where
- build _ = "IO"
-instance (Typeable a) => Axiomable (Axiom (IO a)) where
- axiom_type_of _ctx ax =
- case ax of
- Axiom_Type_IO ->
- -- IO : * -> *
- Type_Abst "" (Type_Sort sort_star_mono) $
- (const Nothing `abstract`) $
- Type_Sort sort_star_mono
- axiom_eq x y =
- maybe (
- case
- ( Typeable.splitTyConApp (typeOf x)
- , Typeable.splitTyConApp (typeOf y)
- ) of
- ( (xc,[(Typeable.typeRepTyCon -> xc')])
- , (yc,[(Typeable.typeRepTyCon -> yc')])
- ) | xc == yc && xc' == yc' -> True
- _ ->
- error $ "Eq: Axiomable (Axiom (IO a)): "
- ++ "\n x : " ++ show (Typeable.splitTyConApp (typeOf x))
- ++ "\n y : " ++ show (Typeable.splitTyConApp (typeOf y))
- ) (x ==) (cast y)
-
-instance
- ( Typeable a
- , Axiom_Type a
- ) => Axiom_Type (IO a) where
- axiom_type = Axiom_Type_IO
- axiom_Type (Axiom_Type_IO) =
- TeTy_App
- (TeTy_Axiom (Axiom_Type_IO::Axiom (IO a)))
- (axiom_Type (axiom_type::Axiom a))
-
-instance Eq (Axiom (Axiom_Term (IO a))) where
- (==) = error "Eq Axiom: (==) on IO"
-instance Ord (Axiom (Axiom_Term (IO a))) where
- compare = error "Eq Axiom: compare on IO"
-instance
- {-( Buildable (Axiom a)
- ) =>-} Show (Axiom (Axiom_Term (IO a))) where
- showsPrec n (Axiom_Term _te ty) =
- showParen (n > 10) $
- showString "Axiom_Term " .
- showString "(_:" .
- showString (
- Text.unpack $
- TL.toStrict $
- Builder.toLazyText $
- build $ (ty context)
- ) .
- showString ")"
-instance
- {-( Buildable (Axiom a)
- ) =>-} Buildable (Axiom (Axiom_Term (IO a))) where
- build (Axiom_Term _a ty) =
- "(_:" <> build (ty context) <> ")"
-instance
- ( Typeable a
- -- , Buildable (Axiom a)
- -- , Axiomable (Axiom a)
- -- , Axiomable (Axiom (Axiom_Term a))
- ) => Axiomable (Axiom (Axiom_Term (IO a))) where
- axiom_type_of ctx (Axiom_Term _a ty) = ty ctx
diff --git a/calculus/Calculus/Lambda/Omega/Explicit/REPL-with-stacktrace.sh b/calculus/Calculus/Lambda/Omega/Explicit/REPL-with-stacktrace.sh
deleted file mode 100755
index 3a02ec2..0000000
--- a/calculus/Calculus/Lambda/Omega/Explicit/REPL-with-stacktrace.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/bin/sh -eux
-
-ghc \
- -main-is Calculus.Lambda.Omega.Explicit.REPL \
- -prof -fprof-auto -fprof-cafs \
- ${GHC_FLAGS-} \
- Calculus/Lambda/Omega/Explicit/REPL.hs
-
-Calculus/Lambda/Omega/Explicit/REPL +RTS -xc "$@"
diff --git a/calculus/Calculus/Lambda/Omega/Explicit/REPL.hs b/calculus/Calculus/Lambda/Omega/Explicit/REPL.hs
deleted file mode 100644
index 42375bb..0000000
--- a/calculus/Calculus/Lambda/Omega/Explicit/REPL.hs
+++ /dev/null
@@ -1,639 +0,0 @@
-{-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE NamedFieldPuns #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE ViewPatterns #-}
-{-# OPTIONS_GHC -fno-warn-tabs #-}
-module Calculus.Lambda.Omega.Explicit.REPL where
-
-import Control.Applicative (Applicative(..), (<$>))
-import Control.Exception
-import Control.Monad
-import Control.Monad.State
-import Data.Bool
-import qualified Data.Char as Char
-import Data.Either (Either(..))
-import Data.Eq (Eq(..))
-import Data.Foldable (Foldable(..))
-import Data.Function (($), (.), const, flip)
-import Data.Functor.Identity
-import Data.List ((++), break, concat, dropWhile, last, reverse)
-import Data.List (isPrefixOf, find)
-import qualified Data.List as List
-import Data.Map.Strict (Map)
-import qualified Data.Map.Strict as Map
-import Data.Maybe (Maybe(..))
-import Data.Monoid ((<>))
-import Data.Monoid (Monoid(..))
-import Data.Ord (Ord(..))
-import Data.String (String)
-import Data.Text (Text)
-import qualified Data.Text as Text
-import Data.Text.Buildable (Buildable(..))
-import qualified Data.Text.Lazy as TL
-import qualified Data.Text.Lazy.Builder as Builder
-import Data.Tuple (fst)
-import Data.Typeable as Typeable
-import Prelude (Integer, Num(..), div, error)
-import System.Console.Haskeline
-import System.Directory
-import System.FilePath
-import System.IO (IO, readFile)
-import qualified Text.Parsec as R
-import Text.Show (Show(..))
-
--- import Debug.Trace
-
-import Calculus.Abstraction.DeBruijn.Generalized
-import Calculus.Lambda.Omega.Explicit
-import Calculus.Lambda.Omega.Explicit.Read
-
--- * Type 'REPL'
-
--- | /Read Eval Print Loop/ monad.
-newtype REPL a
- = REPL
- { unREPL :: StateT REPL_State (InputT IO) a }
- deriving ( Functor
- , Applicative
- , Monad
- , MonadIO
- , MonadState REPL_State )
-
-data REPL_State
- = REPL_State
- { repl_state_env :: Env
- , repl_state_load_dir :: FilePath
- , repl_state_load_done :: Map FilePath ()
- }
-
-main :: IO ()
-main = do
- cwd <- getCurrentDirectory
- runInputT defaultSettings $
- evalStateT (unREPL main_loop) $
- REPL_State
- { repl_state_env = prelude axioms
- , repl_state_load_dir = cwd
- , repl_state_load_done = mempty
- }
- where
- main_loop :: REPL ()
- main_loop = do
- let prompt = "> "
- line <- repl_read_command prompt
- case slice <$> line of
- Just (cmd, input) | (not (length cmd > 1 && cmd `isPrefixOf` "quit")) ->
- dispatch cmd input
- _ -> return ()
- main_loop
-
-slice :: String -> (String, String)
-slice (':':str) = break Char.isSpace str
-slice str = ("", str)
-
-
--- ** I/O
-print :: Buildable a => a -> TL.Text
-print = Builder.toLazyText . build
-
-repl_write_string_ln :: String -> REPL ()
-repl_write_string_ln = REPL . lift . outputStrLn
-
-repl_write_string :: String -> REPL ()
-repl_write_string = REPL . lift . outputStr
-
-repl_show :: Show a => a -> REPL ()
-repl_show = repl_write_string_ln . show
-
-repl_print :: Buildable a => a -> REPL ()
-repl_print = repl_write_string . TL.unpack . print
-
-repl_print_ln :: Buildable a => a -> REPL ()
-repl_print_ln = repl_write_string_ln . TL.unpack . print
-
-repl_read :: Parser Identity x -> String -> (x -> REPL ()) -> REPL ()
-repl_read _p [] _k = return ()
-repl_read p s k =
- case runIdentity $ read p s of
- Right x -> k x
- Left err -> do
- repl_write_string_ln "Parsing error:"
- repl_show err
- repl_write_string " Command_Input: "
- repl_write_string_ln s
-
--- ** Commands
-repl_read_command :: String -> REPL (Maybe String)
-repl_read_command prompt = do
- line <- REPL . lift $ getInputLine prompt
- case line of
- Just s@(':':_) -> return $ Just s
- Just l@(_:_) | last l == ' ' -> parse_block l
- Just s -> return $ Just s
- Nothing -> return Nothing
- where
- parse_block :: String -> REPL (Maybe String)
- parse_block s = do
- line <- REPL . lift $ getInputLine ""
- case line of
- Just l@(_:_) | last l == ' ' -> parse_block (s ++ '\n' : l)
- _ -> return $ Just s
-
-type Command_Name = String
-type Command = Command_Input -> IO Command_Output
-
-command :: Command_Name -> Command
-command "" = command "let"
-command cmd =
- case find (\p -> cmd `isPrefixOf` fst p) commands of
- Nothing -> (\_ -> return $ Left $ Error_Command cmd)
- Just (_, c) -> c
- where
- commands :: [(String, Command)]
- commands =
- [ ("assume", command_assume) -- Type -> IO ()
- , ("code" , command_code) -- Var -> Term
- , ("dump" , command_dump) -- Term -> Text
- , ("equiv", command_equiv) -- Term -> Term -> Bool
- -- , ("echo" , command_echo) -- Term -> Term
- , ("let" , command_let) -- Var -> Term -> IO ()
- , ("load" , command_load) -- FilePath -> IO ()
- , ("nf" , command_normalize normalize) -- Term -> Term
- , ("nf_dump", command_normalize_dump normalize) -- Term -> Term
- , ("reset", command_reset) -- () -> IO ()
- , ("type" , command_type) -- Term -> Type
- , ("type_dump", command_type_dump) -- Term -> Text
- , ("whnf" , command_normalize whnf) -- Term -> Term
- ]
-command_run :: Command_Name -> Command
-command_run cmd (Command_Input i st) = do
- command cmd $
- Command_Input (strip_spaces i) st
- where
- strip_spaces =
- reverse . dropWhile Char.isSpace .
- reverse . dropWhile Char.isSpace
-
-dispatch :: Command_Name -> String -> REPL ()
-dispatch cmd i = do
- st <- get
- output <- liftIO $ command_run cmd (Command_Input i st)
- case output of
- Left (err::Error) ->
- repl_print err
- Right (Command_Result msg new_st) -> do
- case TL.unpack $ print msg of
- [] -> return ()
- o -> repl_write_string_ln o
- put new_st
-
-data Command_Input
- = Command_Input String REPL_State
-type Command_Output
- = Either Error Command_Result
-data Error
- = Error_Parse String R.ParseError
- | Error_Type Type_Error
- | Error_Let Var_Name Type_Error
- | Error_Code Var_Name
- | Error_Command Command_Name
- | Error_IO IOException
- | Error_Load FilePath Error
- deriving (Show)
-instance Buildable Error where
- build err =
- case err of
- Error_Parse s e -> "Error: parsing: " <> build s <> "\n" <> build (show e) <> "\n"
- Error_Type e -> build e
- Error_Let var e -> "Error: in let: " <> build var <> "\n " <> build e
- Error_Code var -> "Error: no such variable in environment: " <> build var
- Error_Command cmd -> "Error: unrecognized command: " <> build cmd <> "\n"
- Error_IO e -> "Error: " <> build (show e) <> "\n"
- Error_Load file e ->
- "Error: loading: " <> build file <> "\n"
- <> build e
-data Command_Result
- = forall msg.
- ( Buildable msg
- ) => Command_Result msg REPL_State
-
-command_assume :: Command
-command_assume (Command_Input str st) =
- return $
- let ctx = context_from_env $ repl_state_env st in
- case runIdentity $ read parse_assume str of
- Left err -> Left $ Error_Parse str err
- Right (v, ty) ->
- case type_of ctx ty of
- Left err -> Left $ Error_Type err
- Right _ty_ty -> Right $
- Command_Result (""::Text) $
- st{repl_state_env = env_insert v
- (TeTy_Axiom (Axiom_Type_Assume ty)) ty $
- repl_state_env st
- }
-
-command_code :: Command
-command_code (Command_Input str st) =
- return $
- let env = repl_state_env st in
- case runIdentity $ read parse_var_name str of
- Left err -> Left $ Error_Parse str err
- Right var ->
- case Map.lookup var env of
- Nothing -> Left $ Error_Code var
- Just item -> Right $ Command_Result
- (form_given $ env_item_term item)
- st
-
-command_dump :: Command
-command_dump (Command_Input str st) =
- return $
- case runIdentity $ read parse_term str of
- Left err -> Left $ Error_Parse str err
- Right te -> Right $ Command_Result (show te) st
-
-command_let :: Command
-command_let (Command_Input [] st) =
- return $ Right $ Command_Result (""::Text) st
-command_let (Command_Input str st) =
- let toks_or_err = runIdentity $ lex lex_all str in
- case toks_or_err of
- Left err -> return $ Left $ Error_Parse str err
- Right [] -> return $ Right $ Command_Result (""::Text) st
- Right toks ->
- case runIdentity $ parse parse_let_or_term toks of
- Left err -> return $ Left $ Error_Parse str err
- Right let_or_term -> do
- let ctx = context_from_env $ repl_state_env st
- case let_or_term of
- Left (v, mty, te) ->
- let ety = case mty of
- Nothing -> type_of ctx te
- Just ty -> do
- _ty_ty <- type_of ctx ty
- const ty <$> check ctx (context_apply ctx ty) te
- in
- return $
- case ety of
- Left err -> Left $ Error_Let v err
- Right ty -> do
- Right $ Command_Result (build v <> " : " <> build ty) $
- st{repl_state_env = env_insert v te ty $ repl_state_env st}
- Right let_te ->
- case type_of ctx let_te of
- Left err -> return $ Left $ Error_Type err
- Right _ty ->
- let norm_te = normalize ctx let_te in
- case norm_te of
- TeTy_Axiom (axiom_cast -> Just (Axiom_Term (io::IO (Term Var_Name)) _o_ty)) -> do
- io_te <- io
- return $ Right $ Command_Result io_te st
- _ ->
- return $ Right $ Command_Result norm_te st
-
-command_load :: Command
-command_load (Command_Input file input_st) = do
- err_or_io <- try $ do
- path <- canonicalizePath (repl_state_load_dir input_st </> file)
- content <- readFile path
- return (path, content)
- case err_or_io of
- Left (err::IOException) -> return $ Left $ Error_IO err
- Right (modul, content) -> do
- case Map.lookup modul $ repl_state_load_done input_st of
- Just _ -> return $ Right $
- Command_Result ("Module already loaded: " ++ modul) input_st
- _ ->
- case runIdentity $ R.runParserT (parse_commands <* R.eof) () modul content of
- Left err -> return $ Left $ Error_Load modul $ Error_Parse content err
- Right cmds -> do
- let old_dir = repl_state_load_dir input_st
- err_or_st <-
- foldM (\err_or_st (cmd, i) ->
- case err_or_st of
- Left _ -> return $ err_or_st
- Right (Command_Result last_msg last_st) -> do
- o <- command_run cmd (Command_Input i last_st)
- case o of
- Left _ -> return o
- Right (Command_Result msg running_st) ->
- return $ Right $
- Command_Result (build last_msg <> "\n" <> build msg) running_st
- )
- (Right $ Command_Result ("Loading: " <> modul)
- input_st{repl_state_load_dir = takeDirectory modul})
- ({-trace ("cmds: " ++ show cmds)-} cmds)
- return $
- case err_or_st of
- Left err -> Left $ Error_Load modul $ err
- Right (Command_Result msg result_st) ->
- Right $ Command_Result msg $ result_st
- { repl_state_load_dir = old_dir
- , repl_state_load_done =
- Map.insert modul () $
- repl_state_load_done result_st
- }
-
-command_normalize
- :: (Context Var_Name -> Term Var_Name -> Term Var_Name)
- -> Command
-command_normalize norm (Command_Input str st) = do
- let ctx = context_from_env $ repl_state_env st
- case runIdentity $ read parse_term str of
- Left err -> return $ Left $ Error_Parse str err
- Right (te::Term Var_Name) ->
- let n_te = norm ctx te in
- case n_te of
- TeTy_Axiom (axiom_cast -> Just (Axiom_Term (o::IO (Term Var_Name)) _o_ty)) -> do
- r <- o
- return $ Right $ Command_Result r st
- TeTy_Axiom (axiom_cast -> Just (Axiom_Term (o::IO Text) _o_ty)) -> do
- r <- o
- return $ Right $ Command_Result r st
- _ ->
- return $ Right $ Command_Result n_te st
-
-command_equiv :: Command
-command_equiv (Command_Input str st) = do
- let ctx = context_from_env $ repl_state_env st
- return $
- case runIdentity $ read ((,) <$> parse_term <* (parse_token Token_Equal >> parse_token Token_Equal) <*> parse_term) str of
- Left err -> Left $ Error_Parse str err
- Right (x_te, y_te) -> Right $
- Command_Result (if equiv ctx x_te y_te then "True" else "False"::Text) st
-
-command_normalize_dump
- :: (Context Var_Name -> Term Var_Name -> Term Var_Name)
- -> Command
-command_normalize_dump norm (Command_Input str st) = do
- let ctx = context_from_env $ repl_state_env st
- return $
- case runIdentity $ read parse_term str of
- Left err -> Left $ Error_Parse str err
- Right te -> Right $ Command_Result (show $ norm ctx te) st
-
-command_reset :: Command
-command_reset (Command_Input _ st) =
- return $ Right $
- Command_Result (""::Text) st{repl_state_env = mempty}
-
-command_type :: Command
-command_type (Command_Input [] st) = do
- let env = repl_state_env st
- return $
- Right $ Command_Result
- (
- foldr (flip (<>)) "" $
- List.intersperse "\n" $
- (\(name, item) ->
- build name <> " : "
- <> build (form_given $ env_item_type item))
- <$> (Map.toList env)
- )
- st
-command_type (Command_Input str st) = do
- let ctx = context_from_env $ repl_state_env st
- return $
- case runIdentity $ read parse_term str of
- Left err -> Left $ Error_Parse str err
- Right te ->
- case type_of ctx te of
- Left err -> Left $ Error_Type err
- Right ty -> Right $ Command_Result (normalize ctx ty) st
-
-command_type_dump :: Command
-command_type_dump (Command_Input [] st) = do
- let env = repl_state_env st
- return $
- Right $ Command_Result
- (
- foldr (flip (<>)) "" $
- List.intersperse "\n" $
- (\(name, item) ->
- build name <> " : "
- <> build (show $ form_given $ env_item_type item))
- <$> (Map.toList env)
- )
- st
-command_type_dump (Command_Input str st) = do
- let ctx = context_from_env $ repl_state_env st
- return $
- case runIdentity $ read parse_term str of
- Left err -> Left $ Error_Parse str err
- Right te ->
- case type_of ctx te of
- Left err -> Left $ Error_Type err
- Right ty -> Right $ Command_Result (show $ normalize ctx ty) st
-
-{-
-command_echo :: String -> REPL ()
-command_echo str =
- repl_read parse_term str repl_print_ln
--}
-
--- * Builtins
-
-builtin :: Axioms -> [Text] -> Env
-builtin =
- foldl $ \env str ->
- let ctx = context_from_env env in
- read_string parse_let str $ \(v, mty, te) ->
- let ety = case mty of
- Just ty -> do
- _ty_ty <- type_of ctx ty
- const ty <$> check ctx (context_apply ctx ty) te
- Nothing -> type_of ctx te in
- case ety of
- Left err -> error $ show err
- Right ty -> env_insert v te ty env
- where
- read_string p s k =
- case runIdentity $ read p s of
- Right x -> k x
- Left err -> error $
- "Parsing_error:\n" ++ show err
- ++ " Input: " ++ Text.unpack s
-
-axioms :: Axioms
-axioms =
- (axioms_monopoly <>) $
- (Map.fromList axioms_io <>) $
- (Map.fromList axioms_int <>) $
- (Map.fromList axioms_text <>) $
- Map.fromList
- [ ("Unit", item $ Axiom_Type_Unit)
- ]
- where
- item :: (Axiomable (Axiom ax), Typeable ax) => Axiom ax -> Env_Item
- item = env_item_from_axiom context
- {-
- axioms_arr =
- [ -- ("Arr", item $ Axiom_Term_Abst)
- ]
- -}
- axioms_text =
- [ ("Text" , item $ Axiom_Type_Text)
- , ("text_empty", item $ axiom_term (""::Text))
- , ("text_hello", item $ axiom_term ("Hello World!"::Text))
- ]
- axioms_int =
- [ ("Int" , item $ Axiom_Type_Integer)
- , ("int_zero" , item $ axiom_term (0::Integer))
- , ("int_one" , item $ axiom_term (1::Integer))
- , ("int_add" , item $ axiom_term ((+)::Integer -> Integer -> Integer))
- , ("int_neg" , item $ axiom_term (negate::Integer -> Integer))
- , ("int_sub" , item $ axiom_term ((-)::Integer -> Integer -> Integer))
- , ("int_mul" , item $ axiom_term ((*)::Integer -> Integer -> Integer))
- , ("int_div" , item $ axiom_term (div::Integer -> Integer -> Integer))
- ]
- axioms_io =
- [ ("IO" , item $ (Axiom_Type_IO::Axiom (IO A)))
- , ("return_io", item $ return_io)
- , ("bind_io" , item $ bind_io)
- , ("join_io" , item $ join_io)
- -- , ("return_io_text", item $ axiom_term $ (return::Text -> IO Text))
- -- , ("return_io_int", item $ Axiom_Term $ (return::Int -> IO Int))
- ]
- where
- -- | @return_io : â(A:*) -> A -> IO A@
- return_io :: Axiom (Axiom_Type_Abst)
- return_io =
- Axiom_Type_Abst "A" (TeTy_Axiom . ax_te) ax_ty
- where
- ax_te :: Type Var_Name
- -> Axiom (Axiom_Term (Term Var_Name -> IO (Term Var_Name)))
- ax_te ty = Axiom_Term return (\ctx -> context_lift ctx <$> ty)
- ax_ty :: Abstraction (Suggest Var_Name) Type Var_Name
- ax_ty =
- (("A" =?) `abstract`) $
- axiom_type_of context $
- axiom_term (return::A -> IO A)
-
- -- | @bind_io : â(A:*) -> â(B:*) -> IO A -> (A -> IO B) -> IO B@
- bind_io :: Axiom Axiom_Type_Abst
- bind_io = ax1_te
- where
- ax1_te :: Axiom Axiom_Type_Abst
- ax1_te =
- Axiom_Type_Abst "A"
- (\(Type_Abst _ _ ty_a_abst) ->
- TeTy_Axiom $
- Axiom_Type_Abst "B"
- (TeTy_Axiom . ax0_te)
- ty_a_abst)
- ax1_ty
- ax1_ty =
- (("A" =?) `abstract`) $
- Type_Abst "B"
- (Type_Sort (Type_Level_0, Type_Morphism_Mono)) $
- ax0_ty
-
- ax0_te
- :: Type Var_Name
- -> Axiom (Axiom_Term
- ( IO (Term Var_Name)
- -> (Term Var_Name -> IO (Term Var_Name))
- -> IO (Term Var_Name)
- ))
- ax0_te ty =
- Axiom_Term (>>=) (\ctx -> context_lift ctx <$> ty)
- ax0_ty =
- (("B" =?) `abstract`) $
- axiom_type_of context $
- axiom_term ((>>=)::IO A -> (A -> IO B) -> IO B)
-
- -- | @join_io : â(A:*) -> IO (IO A) -> IO A@
- join_io :: Axiom Axiom_Type_Abst
- join_io = ax1_te
- where
- ax1_te :: Axiom Axiom_Type_Abst
- ax1_te =
- Axiom_Type_Abst "A"
- (\ty_a ->
- TeTy_Axiom $
- Axiom_Term
- (join::IO (IO (Term Var_Name)) -> IO (Term Var_Name))
- (\ctx -> context_lift ctx <$> ty_a))
- ax1_ty
- ax1_ty =
- (("A" =?) `abstract`) $
- axiom_type_of context $
- axiom_term (join::IO (IO A) -> IO A)
-
-prelude :: Axioms -> Env
-prelude axs =
- builtin axs $ concat $ (Text.unlines <$>) <$>
- [ prelude_bool
- , prelude_either
- ]
- where
- prelude_bool :: [[Text]]
- prelude_bool =
- [ ["Bool_Polytype : *p = (R:*) -> R -> R -> R"]
- , ["Bool : *m = Monotype Bool_Polytype"]
- , ["True : Bool = monotype Bool_Polytype (λ(R:*) (True:R) (False:R) -> True)"]
- , ["False : Bool = monotype Bool_Polytype (λ(R:*) (True:R) (False:R) -> False)"]
- , [ "eq (x:Bool) (y:Bool) : Bool"
- , " = monotype Bool_Polytype"
- , " (λ(R:*) (True:R) (False:R) ->"
- , " polytype Bool_Polytype x R"
- , " (polytype Bool_Polytype y R True False)"
- , " (polytype Bool_Polytype y R False True)"
- , " )"
- ]
- , [ "and (x:Bool) (y:Bool) : Bool"
- , " = monotype Bool_Polytype"
- , " (λ(R:*) (True:R) (False:R) ->"
- , " polytype Bool_Polytype x R"
- , " (polytype Bool_Polytype y R True False)"
- , " (polytype Bool_Polytype y R False False)"
- , " )"
- ]
- , [ "or (x:Bool) (y:Bool) : Bool"
- , " = monotype Bool_Polytype"
- , " (λ(R:*) (True:R) (False:R) ->"
- , " polytype Bool_Polytype x R"
- , " (polytype Bool_Polytype y R True True)"
- , " (polytype Bool_Polytype y R True False)"
- , " )"
- ]
- , [ "xor (x:Bool) (y:Bool) : Bool"
- , " = monotype Bool_Polytype"
- , " (λ(R:*) (True:R) (False:R) ->"
- , " polytype Bool_Polytype x R"
- , " (polytype Bool_Polytype y R False True)"
- , " (polytype Bool_Polytype y R True False)"
- , " )"
- ]
- , [ "not (x:Bool) : Bool"
- , " = monotype Bool_Polytype"
- , " (λ(R:*) (True:R) (False:R) ->"
- , " polytype Bool_Polytype x R False True)"
- ]
- ]
- prelude_either :: [[Text]]
- prelude_either =
- [ ["Either_Polytype (A:*) (B:*) : *p = (R:*) -> (A -> R) -> (B -> R) -> R"]
- , ["Either (A:*) (B:*) : *m = Monotype (Either_Polytype A B)"]
- , [ "Left (A:*) (B:*) (x:A)"
- , " : Either A B"
- , " = monotype (Either_Polytype A B)"
- , " (λ(R:*) (Left:A -> R) (Right:B -> R) -> Left x)"
- ]
- , [ "Right (A:*) (B:*) (x:B)"
- , " : Either A B"
- , " = monotype (Either_Polytype A B)"
- , " (λ(R:*) (Left:A -> R) (Right:B -> R) -> Right x)"
- ]
- , [ "either (A:*) (B:*) (R:*) (l:A -> R) (r:B -> R) (e:Either A B) : R"
- , " = polytype (Either_Polytype A B) e R l r"
- ]
- ]
diff --git a/calculus/Calculus/Lambda/Omega/Explicit/REPL.sh b/calculus/Calculus/Lambda/Omega/Explicit/REPL.sh
deleted file mode 100755
index 63d5a83..0000000
--- a/calculus/Calculus/Lambda/Omega/Explicit/REPL.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-#!/bin/sh -eux
-
-ghc \
- -main-is Calculus.Lambda.Omega.Explicit.REPL \
- ${GHC_FLAGS-} \
- Calculus/Lambda/Omega/Explicit/REPL.hs
-
-Calculus/Lambda/Omega/Explicit/REPL "$@"
diff --git a/calculus/Calculus/Lambda/Omega/Explicit/Read.hs b/calculus/Calculus/Lambda/Omega/Explicit/Read.hs
deleted file mode 100644
index 4463ea1..0000000
--- a/calculus/Calculus/Lambda/Omega/Explicit/Read.hs
+++ /dev/null
@@ -1,392 +0,0 @@
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE TupleSections #-}
-{-# OPTIONS_GHC -fno-warn-tabs #-}
-module Calculus.Lambda.Omega.Explicit.Read where
-
-import Control.Applicative (Alternative(..), Applicative(..), (<$>), (<$))
-import qualified Control.Applicative as Applicative
-import Control.Monad
-import Data.Bool
-import Data.Char (Char)
-import qualified Data.Char as Char
-import Data.Either (Either(..))
-import Data.Eq (Eq(..))
-import Data.Foldable (Foldable(..))
-import Data.Function (($), (.), flip)
-import qualified Data.List as List
-import Data.Maybe (Maybe(..))
-import Data.Maybe (catMaybes)
-import Data.Text (Text)
-import Data.String (String)
-import qualified Data.Text as Text
-import Text.Parsec ((<?>))
-import qualified Text.Parsec as R
-import Text.Show (Show(..))
-
--- import Debug.Trace
-
-import Calculus.Abstraction.DeBruijn.Generalized
-import Calculus.Lambda.Omega.Explicit
-
--- * Type 'Lexer'
-type Lexer s m a
- = R.Stream s m Char
- => R.ParsecT s Lexer_State m a
-type Lexer_State = ()
-
--- ** Type 'Token'
--- | A lexed token.
-data Token
- = Token_Arrow
- | Token_Type_0
- | Token_Equal
- | Token_Colon
- | Token_Lambda
- | Token_Name Text
- | Token_Paren_Close
- | Token_Paren_Open
- | Token_Pi
- deriving (Eq, Show)
-
--- | A lexed token with location information attached
-data Lexed_Token
- = Lexed_Token Token R.SourcePos
- deriving (Show)
-
--- | Remove location information from a 'Lexed_Token'
-lexed_token :: Lexed_Token -> Token
-lexed_token (Lexed_Token tok _) = tok
-
-lex
- :: R.Stream s m Char
- => Lexer s m a
- -> s -> m (Either R.ParseError a)
-lex l = R.runParserT l () ""
-
-lex_all :: Lexer s m [Lexed_Token]
-lex_all =
- catMaybes
- <$> R.many lex_token_or_whitespace
- <* R.eof
-
--- | Lex either one token or some whitespace
-lex_token_or_whitespace :: Lexer s m (Maybe Lexed_Token)
-lex_token_or_whitespace =
- (<|>)
- (Nothing <$ R.try lex_whitespace)
- (Just <$> lex_token)
-
-lex_whitespace :: Lexer s m ()
-lex_whitespace =
- R.choice
- [ () <$ Applicative.some R.space
- , lex_comment_block
- , lex_comment_line
- ]
-
--- | Lex a @{- ... -}@ comment (perhaps nested).
-lex_comment_block :: Lexer s m ()
-lex_comment_block = R.try (R.string "{-") *> lex_comment_body
-
--- | Lex a block comment, without the opening.
-lex_comment_body :: Lexer s m ()
-lex_comment_body =
- R.choice
- [ lex_comment_block *> lex_comment_body
- , R.try (R.string "-}") *> return ()
- , R.anyChar *> lex_comment_body
- ]
-
-lex_comment_line :: Lexer s m ()
-lex_comment_line =
- R.try (R.string "--")
- *> R.manyTill R.anyChar (R.eof <|> (() <$ R.newline))
- *> return ()
-
-lex_token :: Lexer s m Lexed_Token
-lex_token =
- Lexed_Token
- <$> R.choice
- [ lex_symbol
- , lex_word
- -- , Token_Int . fromInteger <$> R.natural R.haskell
- ]
- <*> R.getPosition
-
--- | Lex one non-alphanumeric token
-lex_symbol :: Lexer s m Token
-lex_symbol = R.choice
- [ Token_Arrow <$ (R.try (R.string "->") <|> R.string "â")
- , Token_Colon <$ R.char ':'
- , Token_Equal <$ R.char '='
- , Token_Lambda <$ (R.char '\\' <|> R.char 'λ')
- , Token_Type_0 <$ R.char '*'
- , Token_Paren_Close <$ R.char ')'
- , Token_Paren_Open <$ R.char '('
- , Token_Pi <$ (R.string "\\/" <|> R.string "Î " <|> R.string "â")
- ]
-
-lex_word :: Lexer s m Token
-lex_word = tokenify <$> lex_name
- where
- tokenify name = Token_Name (Text.pack name)
-
-lex_name :: Lexer s m String
-lex_name = (:)
- <$> (R.letter <|> R.char '_')
- <*> (R.many (R.alphaNum <|> R.char '_'))
-
--- * Type 'Parser'
-type Parser m a
- = R.Stream [Lexed_Token] m Lexed_Token
- => R.ParsecT [Lexed_Token] Parser_State m a
-type Parser_State = ()
-
-read
- :: (R.Stream s m Char, Monad m)
- => Parser m a -> s -> m (Either R.ParseError a)
-read p s = do
- toks <- lex lex_all s
- case toks of
- Left err -> return $ Left err
- Right ts -> parse p ts
-
-parse
- :: R.Stream [Lexed_Token] m Lexed_Token
- => Parser m a
- -> [Lexed_Token]
- -> m (Either R.ParseError a)
-parse p = R.runParserT (p <* R.eof) () ""
-
--- | Like 'R.updatePosChar' but working on 'Lexed_Token'.
-updatePosToken
- :: R.SourcePos -- ^ position of the current token
- -> Lexed_Token -- ^ current token
- -> [Lexed_Token] -- ^ remaining tokens
- -> R.SourcePos -- ^ position of the next token
-updatePosToken pos _ [] = pos
-updatePosToken _ _ (Lexed_Token _ pos : _) = pos
-
--- | Parse a nullary token.
-parse_token
- :: Token -> Parser m ()
-parse_token t =
- R.tokenPrim
- show updatePosToken
- (guard . (t ==) . lexed_token)
-
--- | Parse an unary token.
-parse_token_1
- :: (Token -> Maybe a)
- -> Parser m a
-parse_token_1 untoken =
- R.tokenPrim
- show updatePosToken
- (untoken . lexed_token)
-
--- | 'parse_term' @::=@ 'parse_term_abst' @|@ 'parse_type_abst'
-parse_term :: Parser m (Term Var_Name)
-parse_term =
- R.try parse_term_abst
- <|> parse_type_abst
- <?> "term"
-
-parse_sort :: Parser m (Type Var_Name)
-parse_sort =
- Type_Sort . (Type_Level_0,)
- <$ parse_token Token_Type_0
- <*> R.option Type_Morphism_Mono
- (parse_token_1 $ \tok -> case tok of
- Token_Name "m" -> Just Type_Morphism_Mono
- Token_Name "p" -> Just Type_Morphism_Poly
- _ -> Nothing)
- <?> "sort"
-
-parse_var_name :: Parser m Var_Name
-parse_var_name =
- parse_token_1 (\tok ->
- case tok of
- Token_Name "_" -> Nothing
- Token_Name n -> Just n
- _ -> Nothing)
- <?> "variable-name"
-
-parse_var_def :: Parser m Var_Name
-parse_var_def =
- parse_token_1 (\tok ->
- case tok of
- Token_Name "_" -> Just ""
- Token_Name n -> Just n
- _ -> Nothing)
- <?> "variable-definition"
-
-parse_var :: Parser m (Term Var_Name)
-parse_var =
- TeTy_Var
- <$> parse_var_name
- <?> "variable"
-
--- | 'parse_app' @::=@ 'parse_atom'@+@
-parse_app :: Parser m (Term Var_Name)
-parse_app =
- List.foldl1 TeTy_App
- <$> R.many1 (R.try parse_atom)
- <?> "application"
-
--- | 'parse_atom' @::=@ 'parse_sort' @|@ 'parse_var' @|@ @"("@ 'parse_term @")"@
-parse_atom :: Parser m (Term Var_Name)
-parse_atom =
- R.try parse_sort
- <|> R.try parse_var
- <|> R.between
- (parse_token Token_Paren_Open)
- (parse_token Token_Paren_Close)
- parse_term
- <?> "atom"
-
--- | 'parse_term_abst' @::=@ @"\"@ 'parse_term_abst_decl'@+@ @"->"@ 'parse_term'
-parse_term_abst :: Parser m (Term Var_Name)
-parse_term_abst =
- (flip $ foldr (\(x, f_in) t ->
- Term_Abst (Suggest x) f_in ((x =?) `abstract` t)))
- <$ parse_token Token_Lambda
- <*> R.many1 parse_term_abst_decl
- <* parse_token Token_Arrow
- <*> parse_term
- <?> "term_abst"
-
--- | 'parse_term_abst_decl' @::=@ @"("@ 'parse_var_def' @":"@ 'parse_type' @")"@
-parse_term_abst_decl :: Parser m (Var_Name, Type Var_Name)
-parse_term_abst_decl =
- (,)
- <$ parse_token Token_Paren_Open
- <*> parse_var_def
- <* parse_token Token_Colon
- <*> parse_type
- <* parse_token Token_Paren_Close
- <?> "term_abst_decl"
-
--- | 'parse_type_abst_decl' @::=@ @"("@ @(@ 'parse_var_def' @":"@ @)?@ 'parse_type' @")"@
-parse_type_abst_decl :: Parser m (Var_Name, Type Var_Name)
-parse_type_abst_decl =
- (,)
- <$ parse_token Token_Paren_Open
- <*> R.option "" (R.try parse_var_def <* parse_token Token_Colon)
- <*> parse_type
- <* parse_token Token_Paren_Close
- <?> "type_abst_decl"
-
--- | 'parse_type_abst' @::=@ @(@ 'parse_app' @|@ 'parse_type_abst_decl' @)@ @"->"@ 'parse_type_abst' @|@ 'parse_app'
-parse_type_abst :: Parser m (Term Var_Name)
-parse_type_abst =
- (R.try
- ((\(x, f_in) f_out ->
- Type_Abst (Suggest x) f_in ((x =?) `abstract` f_out))
- <$> (
- (R.try (("",) <$> parse_app))
- <|>
- (R.option () (parse_token Token_Pi)
- *> parse_type_abst_decl)
- )
- <* parse_token Token_Arrow
- <*> parse_type_abst))
- <|> parse_app
- <?> "type_abst"
-
--- | 'parse_type' @::=@ 'parse_term'
-parse_type :: Parser m (Term Var_Name)
-parse_type =
- parse_term <?> "type"
-
-parse_let_or_term :: Parser m (Either (Var_Name, Maybe (Type Var_Name), Term Var_Name) (Term Var_Name))
-parse_let_or_term =
- R.option
- Right
- (R.try ((\name args maybe_ty te ->
- Left
- ( name
- , (\ty -> foldr (\(x, x_ty) t ->
- Type_Abst (Suggest x) x_ty ((x =?) `abstract` t)) ty args
- ) <$> maybe_ty
- , foldr (\(x, x_ty) t ->
- Term_Abst (Suggest x) x_ty ((x =?) `abstract` t)) te args
- )
- )<$> parse_var_name
- <*> R.many parse_term_abst_decl
- <*> (<|>)
- (R.try (Just
- <$ parse_token Token_Colon
- <*> parse_type))
- (pure Nothing)
- <* parse_token Token_Equal
- ))
- <*> parse_term
-
--- | 'parse_let' @::=@ 'parse_var_name' @(@'parse_term_abst_decl'@)*@ @"="@ 'parse_term'
-parse_let :: Parser m (Var_Name, Maybe (Type Var_Name), Term Var_Name)
-parse_let =
- (\name args maybe_ty te ->
- ( name
- , (\ty -> foldr (\(x, x_ty) t ->
- Type_Abst (Suggest x) x_ty ((x =?) `abstract` t)) ty args
- ) <$> maybe_ty
- , foldr (\(x, x_ty) t ->
- Term_Abst (Suggest x) x_ty ((x =?) `abstract` t)) te args
- )
- )<$> parse_var_name
- <*> R.many parse_term_abst_decl
- <*> (<|>)
- (R.try (Just
- <$ parse_token Token_Colon
- <*> parse_type))
- (pure Nothing)
- <* parse_token Token_Equal
- <*> parse_term
- <?> "let"
-
--- | 'parse_assume' @::=@ 'parse_var_name' @":"@ 'parse_type'
-parse_assume :: Parser m (Var_Name, Type Var_Name)
-parse_assume =
- (,)
- <$> parse_var_name
- <* parse_token Token_Colon
- <*> parse_type
- <?> "axiom"
-
-parse_command
- :: R.Stream s m Char
- => R.ParsecT s () m (String, String)
-parse_command =
- (,)
- <$> (R.option "" (R.try (
- R.char ':'
- *> R.many (R.satisfy Char.isLetter <|> R.char '_')
- <* (R.option () $ void $ R.many (void $ R.char ' '))
- )))
- <*> R.many (R.try (
- (<|>)
- (R.try R.newline <* R.lookAhead (R.char ' ' <|> R.char '\t'))
- (R.satisfy is_horizontal)
- ))
- where
- is_horizontal c = case c of {'\n' -> False; '\r' -> False; _ -> True}
-
-parse_commands
- :: R.Stream s m Char
- => R.ParsecT s () m [(String, String)]
-parse_commands =
- R.many $ do
- _ <- R.many $ do
- _ <- R.many (R.satisfy is_horizontal_space)
- R.newline
- (c, s) <- parse_command
- _ <- R.many1 $ do
- _ <- R.try (R.many (R.satisfy is_horizontal_space))
- R.newline
- return (c,s)
- where
- is_horizontal_space c = case c of {' ' -> True; '\t' -> True; _ -> False}
-
diff --git a/calculus/Calculus/Lambda/Omega/Explicit/lib.cloe b/calculus/Calculus/Lambda/Omega/Explicit/lib.cloe
deleted file mode 100644
index 049d2e3..0000000
--- a/calculus/Calculus/Lambda/Omega/Explicit/lib.cloe
+++ /dev/null
@@ -1,13 +0,0 @@
-:load lib/Bool.cloe
-:load lib/Either.cloe
-:load lib/Eq.cloe
-:load lib/Function.cloe
-:load lib/Functor.cloe
-:load lib/IO.cloe
-:load lib/List.cloe
-:load lib/Maybe.cloe
-:load lib/Monad.cloe
-:load lib/Monoid.cloe
-:load lib/Nat.cloe
-:load lib/Ord.cloe
-:load lib/Pair.cloe
diff --git a/calculus/Calculus/Lambda/Omega/Explicit/lib/Bool.cloe b/calculus/Calculus/Lambda/Omega/Explicit/lib/Bool.cloe
deleted file mode 100644
index 9eb6613..0000000
--- a/calculus/Calculus/Lambda/Omega/Explicit/lib/Bool.cloe
+++ /dev/null
@@ -1,30 +0,0 @@
-Bool_Polytype : *p = (Data:*) -> Data -> Data -> Data
-Bool : *m = Monotype Bool_Polytype
-True : Bool = monotype Bool_Polytype (λ(Data:*) (True:Data) (False:Data) -> True)
-False : Bool = monotype Bool_Polytype (λ(Data:*) (True:Data) (False:Data) -> False)
-
-and (x:Bool) (y:Bool) : Bool
- = monotype Bool_Polytype
- (λ(Data:*) (True:Data) (False:Data) ->
- polytype Bool_Polytype x Data
- (polytype Bool_Polytype y Data True False)
- (polytype Bool_Polytype y Data False False)
- )
-or (x:Bool) (y:Bool) : Bool
- = monotype Bool_Polytype
- (λ(Data:*) (True:Data) (False:Data) ->
- polytype Bool_Polytype x Data
- (polytype Bool_Polytype y Data True True)
- (polytype Bool_Polytype y Data True False)
- )
-xor (x:Bool) (y:Bool) : Bool
- = monotype Bool_Polytype
- (λ(Data:*) (True:Data) (False:Data) ->
- polytype Bool_Polytype x Data
- (polytype Bool_Polytype y Data False True)
- (polytype Bool_Polytype y Data True False)
- )
-not (x:Bool) : Bool
- = monotype Bool_Polytype
- (λ(Data:*) (True:Data) (False:Data) ->
- polytype Bool_Polytype x Data False True)
diff --git a/calculus/Calculus/Lambda/Omega/Explicit/lib/Either.cloe b/calculus/Calculus/Lambda/Omega/Explicit/lib/Either.cloe
deleted file mode 100644
index 5842004..0000000
--- a/calculus/Calculus/Lambda/Omega/Explicit/lib/Either.cloe
+++ /dev/null
@@ -1,40 +0,0 @@
-Either_Polytype (L:*) (R:*) : *p
- = (Data:*) -> (L -> Data) -> (R -> Data) -> Data
-Either (L:*) (R:*) : *m
- = Monotype (Either_Polytype L R)
-Left (L:*) (R:*) (l:L) : Either L R
- = monotype (Either_Polytype L R)
- (λ(Data:*) (Left:L -> Data) (Right:R -> Data) -> Left l)
-Right (L:*) (R:*) (r:R) : Either L R
- = monotype (Either_Polytype L R)
- (λ(Data:*) (Left:L -> Data) (Right:R -> Data) -> Right r)
-
-left (L:*) (R:*) (l:L)
- : Either L R
- = monotype (Either_Polytype L R)
- (λ(Data:*) (Left:L -> Data) (Right:R -> Data) -> Left l)
-right (L:*) (R:*) (r:R)
- : Either L R
- = monotype (Either_Polytype L R)
- (λ(Data:*) (Left:L -> Data) (Right:R -> Data) -> Right r)
-either
- (L:*) (R:*) (Data:*)
- (l:L -> Data)
- (r:R -> Data)
- (e:Either L R)
- : Data
- = polytype (Either_Polytype L R) e Data l r
-
-:load Monad.cloe
-Monad_return_Either (L:*) (X:*)
- : Monad_Return (Either L) X
- = Right L X
-Monad_bind_Either (L:*) (X:*) (Y:*)
- : Monad_Bind (Either L) X Y
- = λ(mx:Either L X) (my:X -> Either L Y) ->
- either L X (Either L Y) (Left L Y) my mx
-Monad_Either (L:*)
- : Monad (Either L)
- = monad (Either L)
- (Monad_return_Either L)
- (Monad_bind_Either L)
diff --git a/calculus/Calculus/Lambda/Omega/Explicit/lib/Eq.cloe b/calculus/Calculus/Lambda/Omega/Explicit/lib/Eq.cloe
deleted file mode 100644
index ee5ca15..0000000
--- a/calculus/Calculus/Lambda/Omega/Explicit/lib/Eq.cloe
+++ /dev/null
@@ -1,36 +0,0 @@
-:load Bool.cloe
-
-Eq_Equal
- (X:*)
- = X -> X -> Bool
-
-Eq_Class
- (X:*) (Data:*)
- = (equal:Eq_Equal X)
- -> Data
-Eq_Polytype
- (X:*) : *p
- = (Data:*) -> Eq_Class X Data -> Data
-Eq
- (X:*) : *m
- = Monotype (Eq_Polytype X)
-
-eq
- (X:*)
- (equal:Eq_Equal X)
- : Eq X
- = monotype (Eq_Polytype X)
- (λ(Data:*) (eq_class:Eq_Class X Data) -> eq_class equal)
-unEq
- (X:*) (Data:*)
- (eq_class:Eq_Class X Data)
- (eq:Eq X)
- : Data
- = polytype (Eq_Polytype X) eq Data eq_class
-
-Eq_equal
- (X:*) (eq:Eq X)
- : Eq_Equal X
- = unEq X (Eq_Equal X)
- (λ(equal:Eq_Equal X) -> equal)
- eq
diff --git a/calculus/Calculus/Lambda/Omega/Explicit/lib/Function.cloe b/calculus/Calculus/Lambda/Omega/Explicit/lib/Function.cloe
deleted file mode 100644
index b486be6..0000000
--- a/calculus/Calculus/Lambda/Omega/Explicit/lib/Function.cloe
+++ /dev/null
@@ -1,10 +0,0 @@
-id (X:*) (x:X) : X = x
-
-const (X:*) (Y:*) (x:X) (y:Y) : X = x
-
-o
- (X:*) (Y:*) (Z:*)
- (f:Y -> Z)
- (g:X -> Y)
- : X -> Z
- = λ(x:X) -> f (g x)
diff --git a/calculus/Calculus/Lambda/Omega/Explicit/lib/Functor.cloe b/calculus/Calculus/Lambda/Omega/Explicit/lib/Functor.cloe
deleted file mode 100644
index 6efc0cb..0000000
--- a/calculus/Calculus/Lambda/Omega/Explicit/lib/Functor.cloe
+++ /dev/null
@@ -1,34 +0,0 @@
-Functor_Fmap
- (F:* -> *) (X:*) (Y:*)
- = (X -> Y) -> F X -> F Y
-
-Functor_Class
- (F:* -> *) (Data:*)
- = (fmap:â(X:*) -> â(Y:*) -> Functor_Fmap F X Y)
- -> Data
-Functor_Polytype
- (F:* -> *) : *p
- = (Data:*) -> Functor_Class F Data -> Data
-Functor
- (F:* -> *) : *m
- = Monotype (Functor_Polytype F)
-
-functor
- (F:* -> *)
- (fmap:â(X:*) -> â(Y:*) -> Functor_Fmap F X Y)
- : Functor F
- = monotype (Functor_Polytype F)
- (λ(Data:*) (functor_class:Functor_Class F Data) -> functor_class fmap)
-unFunctor
- (F:* -> *) (Data:*)
- (functor_class:Functor_Class F Data)
- (functor:Functor F)
- : Data
- = polytype (Functor_Polytype F) functor Data functor_class
-
-Functor_fmap
- (F:* -> *) (functor:Functor F) (X:*) (Y:*)
- : Functor_Fmap F X Y
- = unFunctor F (Functor_Fmap F X Y)
- (λ(fmap:â(X:*) -> â(Y:*) -> Functor_Fmap F X Y) -> fmap X Y)
- functor
diff --git a/calculus/Calculus/Lambda/Omega/Explicit/lib/IO.cloe b/calculus/Calculus/Lambda/Omega/Explicit/lib/IO.cloe
deleted file mode 100644
index a8b6358..0000000
--- a/calculus/Calculus/Lambda/Omega/Explicit/lib/IO.cloe
+++ /dev/null
@@ -1,36 +0,0 @@
-:load Pair.cloe
-
-:assume World : *
-IO_Polytype (X:*) : *p
- = (Data:*) -> (data:(p:World -> Pair World X) -> Data) -> Data
-IO (X:*) = Monotype (IO_Polytype X)
-
-:load Monad.cloe
-Monad_return_IO (X:*)
- : Monad_Return IO X
- = λ(x:X) ->
- monotype (IO_Polytype X)
- (λ(Data:*) (data:(World -> Pair World X) -> Data) ->
- data (λ(w:World) -> pair World X w x))
-Monad_bind_IO (X:*) (Y:*)
- : Monad_Bind IO X Y
- = λ(mx:IO X) (my:X -> IO Y) ->
- monotype (IO_Polytype Y)
- (λ(Data:*) (oy:(World -> Pair World Y) -> Data) ->
- polytype (IO_Polytype X) mx Data (λ(px:World -> Pair World X) ->
- oy (λ(w:World) ->
- uncurry World X (Pair World Y)
- (λ(w:World) (x:X) ->
- polytype (IO_Polytype Y) (my x) (Pair World Y) (λ(py:World -> Pair World Y) ->
- py w
- )
- )
- (px w)
- )
- )
- )
-Monad_List
- : Monad IO
- = monad IO
- Monad_return_IO
- Monad_bind_IO
diff --git a/calculus/Calculus/Lambda/Omega/Explicit/lib/List.cloe b/calculus/Calculus/Lambda/Omega/Explicit/lib/List.cloe
deleted file mode 100644
index 8c8c4c6..0000000
--- a/calculus/Calculus/Lambda/Omega/Explicit/lib/List.cloe
+++ /dev/null
@@ -1,74 +0,0 @@
-List_Polytype (X:*) : *p
- = (Data:*) -> (Cons:X -> Data -> Data) -> (Nil:Data) -> Data
-List (X:*) : *m
- = Monotype (List_Polytype X)
-List_foldr (X:*) (L:List X) (Data:*)
- = polytype (List_Polytype X) L Data
-List_Nil (X:*) : List X
- = monotype (List_Polytype X)
- (λ(Data:*) (Cons:X -> Data -> Data) (Nil:Data) -> Nil)
-List_Cons_right (X:*) (x:X) (xs:List X)
- : List X
- = monotype (List_Polytype X) (λ(Data:*) (Cons:X -> Data -> Data) (Nil:Data) ->
- polytype (List_Polytype X) xs Data Cons (Cons x Nil))
-List_Cons_left (X:*) (x:X) (xs:List X)
- : List X
- = monotype (List_Polytype X) (λ(Data:*) (Cons:X -> Data -> Data) (Nil:Data) ->
- Cons x (polytype (List_Polytype X) xs Data Cons Nil))
-List_Cons
- : (X:*m) -> (x:X) -> (xs:List X) -> List X
- = List_Cons_left
-
-:load Functor.cloe
-Functor_fmap_List (X:*) (Y:*)
- : Functor_Fmap List X Y
- = λ(y:X -> Y) (xs:List X) ->
- monotype (List_Polytype Y) (λ(Data:*) (Cons:Y -> Data -> Data) ->
- polytype (List_Polytype X) xs Data
- (λ(x:X) -> Cons (y x)))
-Functor_fmap_List_using_foldr (X:*) (Y:*)
- : Functor_Fmap List X Y
- = λ(y:X -> Y) (xs:List X) ->
- List_foldr X xs (List Y) (λ(x:X) ->
- List_Cons_left Y (y x)) (List_Nil Y)
-
-:load Monoid.cloe
-Monoid_mempty_List (X:*)
- : Monoid_Mempty (List X)
- = List_Nil X
-Monoid_mappend_List (X:*)
- : Monoid_Mappend (List X)
- = λ(xs:List X) (ys:List X) ->
- monotype (List_Polytype X)
- (λ(Data:*) (Cons:X -> Data -> Data) (Nil:Data) ->
- polytype (List_Polytype X) xs Data
- Cons
- (polytype (List_Polytype X) ys Data Cons Nil))
-Monoid_mappend_List_using_foldr (X:*)
- : Monoid_Mappend (List X)
- = λ(xs:List X) (ys:List X) ->
- List_foldr X xs (List X) (List_Cons X) ys
-
-:load Monad.cloe
-Monad_return_List (X:*)
- : Monad_Return List X
- = λ(x:X) -> List_Cons X x (List_Nil X)
-Monad_bind_List (X:*) (Y:*)
- : Monad_Bind List X Y
- = λ(xs:List X) (ys:X -> List Y) ->
- List_foldr X xs (List Y)
- (λ(x:X) -> Monoid_mappend_List Y (ys x))
- (Monoid_mempty_List Y)
-Monad_join_List (X:*)
- : Monad_Join List X
- = λ(xss:List (List X)) ->
- monotype (List_Polytype X)
- (λ(Data:*) (Cons:X -> Data -> Data) (Nil:Data) ->
- polytype (List_Polytype (List X)) xss Data
- (λ(xs:List X) -> polytype (List_Polytype X) xs Data Cons)
- Nil)
-Monad_List
- : Monad List
- = monad List
- Monad_return_List
- Monad_bind_List
diff --git a/calculus/Calculus/Lambda/Omega/Explicit/lib/Maybe.cloe b/calculus/Calculus/Lambda/Omega/Explicit/lib/Maybe.cloe
deleted file mode 100644
index 71b81fc..0000000
--- a/calculus/Calculus/Lambda/Omega/Explicit/lib/Maybe.cloe
+++ /dev/null
@@ -1,28 +0,0 @@
-Maybe_Polytype (X:*) : *p
- = (Data:*) -> Data -> (X -> Data) -> Data
-Maybe (X:*) : *m
- = Monotype (Maybe_Polytype X)
-Nothing (X:*) : Maybe X
- = monotype (Maybe_Polytype X)
- (λ(Data:*) (Nothing:Data) (Just:X -> Data) -> Nothing)
-Just (X:*) (x:X) : Maybe X
- = monotype (Maybe_Polytype X)
- (λ(Data:*) (Nothing:Data) (Just:X -> Data) -> Just x)
-maybe (X:*) (Data:*) (nothing:Data) (just:X -> Data) (m:Maybe X) : Data
- = polytype (Maybe_Polytype X) m Data nothing just
-
-:load Monad.cloe
-Monad_return_Maybe
- (X:*)
- : Monad_Return Maybe X
- = Just X
-Monad_bind_Maybe
- (X:*) (Y:*)
- : Monad_Bind Maybe X Y
- = λ(mx:Maybe X) (my:X -> Maybe Y) ->
- maybe X (Maybe Y) (Nothing Y) my mx
-Monad_Maybe
- : Monad Maybe
- = monad Maybe
- Monad_return_Maybe
- Monad_bind_Maybe
diff --git a/calculus/Calculus/Lambda/Omega/Explicit/lib/Monad.cloe b/calculus/Calculus/Lambda/Omega/Explicit/lib/Monad.cloe
deleted file mode 100644
index 1faf0d9..0000000
--- a/calculus/Calculus/Lambda/Omega/Explicit/lib/Monad.cloe
+++ /dev/null
@@ -1,52 +0,0 @@
-Monad_Return (M:* -> *) (X:*) = X -> M X
-Monad_Join (M:* -> *) (X:*) = M (M X) -> M X
-Monad_Bind (M:* -> *) (X:*) (Y:*) = M X -> (X -> M Y) -> M Y
-
-Monad_Class
- (M:* -> *) (Data:*)
- = (return:â(X:*) -> Monad_Return M X)
- -> (bind:â(X:*) -> â(Y:*) -> Monad_Bind M X Y)
- -> Data
-Monad_Polytype
- (M:* -> *) : *p
- = (Data:*) -> Monad_Class M Data -> Data
-Monad
- (M:* -> *) : *m
- = Monotype (Monad_Polytype M)
-
-monad
- (M:* -> *)
- (return:â(X:*) -> Monad_Return M X)
- (bind:â(X:*) -> â(Y:*) -> Monad_Bind M X Y)
- : Monad M
- = monotype (Monad_Polytype M)
- (λ(Data:*) (monad_class:Monad_Class M Data) ->
- monad_class return bind)
-unMonad
- (M:* -> *) (Data:*)
- (monad_class:Monad_Class M Data)
- (monad:Monad M)
- : Data
- = polytype (Monad_Polytype M) monad Data monad_class
-
-Monad_return
- (M:* -> *) (monad:Monad M) (X:*)
- : Monad_Return M X
- = unMonad M (Monad_Return M X)
- (λ(return:â(X:*) -> Monad_Return M X)
- (bind:â(X:*) -> â(Y:*) -> Monad_Bind M X Y)
- -> return X
- ) monad
-Monad_bind
- (M:* -> *) (monad:Monad M) (X:*) (Y:*)
- : Monad_Bind M X Y
- = unMonad M (Monad_Bind M X Y)
- (λ(return:â(X:*) -> Monad_Return M X)
- (bind:â(X:*) -> â(Y:*) -> Monad_Bind M X Y)
- -> bind X Y
- ) monad
-Monad_join
- (M:* -> *) (monad:Monad M) (X:*)
- : Monad_Join M X
- = λ(m:M (M X)) ->
- Monad_bind M monad (M X) X m (λ(x:M X) -> x)
diff --git a/calculus/Calculus/Lambda/Omega/Explicit/lib/Monoid.cloe b/calculus/Calculus/Lambda/Omega/Explicit/lib/Monoid.cloe
deleted file mode 100644
index 340698f..0000000
--- a/calculus/Calculus/Lambda/Omega/Explicit/lib/Monoid.cloe
+++ /dev/null
@@ -1,42 +0,0 @@
-Monoid_Mempty (M:*) = M
-Monoid_Mappend (M:*) = M -> M -> M
-
-Monoid_Class
- (M:*) (Data:*)
- = (mempty:Monoid_Mempty M)
- -> (mappend:Monoid_Mappend M)
- -> Data
-Monoid_Polytype
- (M:*) : *p
- = (Data:*) -> Monoid_Class M Data -> Data
-Monoid
- (M:*) : *m
- = Monotype (Monoid_Polytype M)
-
-monoid
- (M:*)
- (mempty:Monoid_Mempty M)
- (mappend:Monoid_Mappend M)
- : Monoid M
- = monotype (Monoid_Polytype M)
- (λ(Data:*) (monoid_class:Monoid_Class M Data) ->
- monoid_class mempty mappend)
-unMonoid
- (M:*) (Data:*)
- (monoid_class:Monoid_Class M Data)
- (monoid:Monoid M)
- : Data
- = polytype (Monoid_Polytype M) monoid Data monoid_class
-
-Monoid_mempty
- (M:*) (monoid:Monoid M)
- : Monoid_Mempty M
- = unMonoid M (Monoid_Mempty M)
- (λ(mempty:Monoid_Mempty M) (mappend:Monoid_Mappend M) -> mempty)
- monoid
-Monoid_mappend
- (M:*) (monoid:Monoid M)
- : Monoid_Mappend M
- = unMonoid M (Monoid_Mappend M)
- (λ(mempty:Monoid_Mempty M) (mappend:Monoid_Mappend M) -> mappend)
- monoid
diff --git a/calculus/Calculus/Lambda/Omega/Explicit/lib/Nat.cloe b/calculus/Calculus/Lambda/Omega/Explicit/lib/Nat.cloe
deleted file mode 100644
index fce00b6..0000000
--- a/calculus/Calculus/Lambda/Omega/Explicit/lib/Nat.cloe
+++ /dev/null
@@ -1,19 +0,0 @@
-Nat_Polytype : *p
- = (Data:*) -> (Succ:Data -> Data) -> (Zero:Data) -> Data
-Nat : *m = Monotype Nat_Polytype
-zero : Nat = (monotype Nat_Polytype) (λ(Data:*) (Succ:Data -> Data) (Zero:Data) -> Zero)
-succ (n:Nat) : Nat
- = monotype Nat_Polytype
- (λ(Data:*) (Succ:Data -> Data) (Zero:Data) ->
- Succ (polytype Nat_Polytype n Data Succ Zero))
-one : Nat = succ zero
-two : Nat = succ one
-three : Nat = succ two
-plus (n:Nat) (m:Nat) : Nat
- = monotype Nat_Polytype
- (λ(Data:*) (Succ:Data -> Data) (Zero:Data) ->
- polytype Nat_Polytype n Data Succ (polytype Nat_Polytype m Data Succ Zero))
-mult (n:Nat) (m:Nat) : Nat
- = monotype Nat_Polytype
- (λ(Data:*) (Succ:Data -> Data) (Zero:Data) ->
- polytype Nat_Polytype n Data (polytype Nat_Polytype m Data Succ) Zero)
diff --git a/calculus/Calculus/Lambda/Omega/Explicit/lib/Ord.cloe b/calculus/Calculus/Lambda/Omega/Explicit/lib/Ord.cloe
deleted file mode 100644
index 0279109..0000000
--- a/calculus/Calculus/Lambda/Omega/Explicit/lib/Ord.cloe
+++ /dev/null
@@ -1,51 +0,0 @@
-Ordering_Polytype : *p
- = (Data:*) -> (Lt:Data) -> (Eq:Data) -> (Gt:Data) -> Data
-Ordering : *m = Monotype Ordering_Polytype
-
-Ord_Lt : Ordering = monotype Ordering_Polytype (λ(Data:*) (Lt:Data) (Eq:Data) (Gt:Data) -> Lt)
-Ord_Eq : Ordering = monotype Ordering_Polytype (λ(Data:*) (Lt:Data) (Eq:Data) (Gt:Data) -> Eq)
-Ord_Gt : Ordering = monotype Ordering_Polytype (λ(Data:*) (Lt:Data) (Eq:Data) (Gt:Data) -> Gt)
-
-:load Eq.cloe
-
-Ord_Compare (X:*) = X -> X -> Ordering
-
-Ord_Class
- (X:*) (Data:*)
- = (eq:Eq X)
- -> (compare:Ord_Compare X)
- -> Data
-Ord_Polytype
- (X:*) : *p
- = (Data:*) -> Ord_Class X Data -> Data
-Ord
- (X:*) : *m
- = Monotype (Ord_Polytype X)
-
-ord
- (X:*)
- (eq:Eq X)
- (compare:Ord_Compare X)
- : Ord X
- = monotype (Ord_Polytype X)
- (λ(Data:*) (ord_class:Ord_Class X Data) ->
- ord_class eq compare)
-unOrd
- (X:*) (Data:*)
- (ord_class:Ord_Class X Data)
- (ord:Ord X)
- : Data
- = polytype (Ord_Polytype X) ord Data ord_class
-
-Ord_eq
- (X:*) (ord:Ord X)
- : Eq X
- = unOrd X (Eq X)
- (λ(eq:Eq X) (compare:Ord_Compare X) -> eq)
- ord
-Ord_compare
- (X:*) (ord:Ord X)
- : Ord_Compare X
- = unOrd X (Ord_Compare X)
- (λ(eq:Eq X) (compare:Ord_Compare X) -> compare)
- ord
diff --git a/calculus/Calculus/Lambda/Omega/Explicit/lib/Pair.cloe b/calculus/Calculus/Lambda/Omega/Explicit/lib/Pair.cloe
deleted file mode 100644
index 6eac7c6..0000000
--- a/calculus/Calculus/Lambda/Omega/Explicit/lib/Pair.cloe
+++ /dev/null
@@ -1,23 +0,0 @@
-Pair_Polytype (X:*) (Y:*) : *p = (Data:*) -> (X -> Y -> Data) -> Data
-Pair (X:*) (Y:*) : *m = Monotype (Pair_Polytype X Y)
-pair (X:*) (Y:*) (x:X) (y:Y) : Pair X Y
- = monotype (Pair_Polytype X Y)
- (λ(Data:*) (f:X -> Y -> Data) -> f x y)
-
-uncurry (X:*) (Y:*) (Data:*) (r:X -> Y -> Data) (p:Pair X Y) : Data
- = polytype (Pair_Polytype X Y)
- p Data r
-curry (X:*) (Y:*) (Data:*) (r:Pair X Y -> Data) (x:X) (y:Y)
- = r (pair X Y x y)
-
-fst (X:*) (Y:*) (p:Pair X Y) : X
- = uncurry X Y X (λ(x:X) (y:Y) -> x) p
-snd (X:*) (Y:*) (p:Pair X Y) : Y
- = uncurry X Y Y (λ(x:X) (y:Y) -> y) p
-repair (X:*) (Y:*) (p:Pair X Y) : Pair X Y
- = pair X Y (fst X Y p) (snd X Y p)
-
-first (X:*) (Y:*) (Z:*) (f:X -> Z) (p:Pair X Y) : Pair Z Y
- = uncurry X Y (Pair Z Y) (λ(x:X) (y:Y) -> pair Z Y (f x) y) p
-second (X:*) (Y:*) (Z:*) (f:Y -> Z) (p:Pair X Y) : Pair X Z
- = uncurry X Y (Pair X Z) (λ(x:X) (y:Y) -> pair X Z x (f y)) p
diff --git a/calculus/Calculus/Lambda/Omega/Implicit.hs b/calculus/Calculus/Lambda/Omega/Implicit.hs
deleted file mode 100644
index ec8b698..0000000
--- a/calculus/Calculus/Lambda/Omega/Implicit.hs
+++ /dev/null
@@ -1,4 +0,0 @@
-module Calculus.Lambda.Omega.Implicit where
-
-
-
diff --git a/calculus/Control/Monad/Classes/EffectsFix.hs b/calculus/Control/Monad/Classes/EffectsFix.hs
deleted file mode 100644
index 9456f9b..0000000
--- a/calculus/Control/Monad/Classes/EffectsFix.hs
+++ /dev/null
@@ -1,18 +0,0 @@
-{-# LANGUAGE EmptyDataDecls #-}
-{-# LANGUAGE KindSignatures #-}
-module Control.Monad.Classes.EffectsFix where
--- | Effects whose state is parameterized by the 'Monad' stack.
-
--- * Types of effects
-
--- | Writer effect
-data EffWriterFix (w :: {-m-}(* -> *) -> *)
-
--- | Reader effect
-data EffReaderFix (e :: {-m-}(* -> *) -> *)
-
--- | Local state change effect
-data EffLocalFix (e :: {-m-}(* -> *) -> *)
-
--- | State effect
-data EffStateFix (s :: {-m-}(* -> *) -> *)
diff --git a/calculus/Control/Monad/Classes/Instance.hs b/calculus/Control/Monad/Classes/Instance.hs
deleted file mode 100644
index 7bfdea5..0000000
--- a/calculus/Control/Monad/Classes/Instance.hs
+++ /dev/null
@@ -1,23 +0,0 @@
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE TypeFamilies #-}
-module Control.Monad.Classes.Instance where
-import Data.Bool (Bool(..))
-import GHC.Prim (Constraint)
-
--- | A data type to existentially wrap a value of type @ty@,
--- when it is an instance of the type class @cl@.
-data Instance (cl:: * -> Constraint)
- = forall ty. cl ty => Instance ty
-
--- | An open type family to know (at the type level) whether a type @ty@
--- has an instance of the type class @cl@.
---
--- NOTE: currently, users have to manually define type family instances of 'Class'
--- to indicate to the compiler which type support which type class.
--- It is definitively redundant to have to define
--- both a type class instance and a type family instance,
--- but I cannot find a way to automatically synchronize
--- the compiler's knowledge between these two levels.
-type family Class (cl:: * -> Constraint) (ty:: *) :: Bool
diff --git a/calculus/Control/Monad/Classes/StateFix.hs b/calculus/Control/Monad/Classes/StateFix.hs
deleted file mode 100644
index 8d60005..0000000
--- a/calculus/Control/Monad/Classes/StateFix.hs
+++ /dev/null
@@ -1,132 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE EmptyDataDecls #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE MagicHash #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-module Control.Monad.Classes.StateFix where
--- | 'MonadState' whose state is parameterized by the 'Monad' stack.
-
-import Control.Applicative (Applicative(..))
-import Control.Monad
-import Control.Monad.Classes
-import Control.Monad.Classes.EffectsFix
-import Control.Monad.Trans.Class
-import qualified Control.Monad.Trans.State.Lazy as SL
--- import qualified Control.Monad.Trans.State.Strict as SS -- TODO: when needed :)
-import Data.Bool (Bool(..))
-import Data.Function ((.))
-import Data.Functor.Identity (Identity)
-import GHC.Prim (Proxy#, proxy#)
-import Prelude (seq)
-
--- * Type 'StateLazyFixT'
-
-data StateLazyFixT
- (st::{-StateLazyFixT st m-}(* -> *) -> *)
- (m::{-a-}* -> *)
- (a:: *)
- = StateLazyFixT
- { unStateLazyFixT :: SL.StateT (st (StateLazyFixT st m)) m a }
- deriving (Functor)
-instance Monad m => Applicative (StateLazyFixT st m) where
- pure = return
- (<*>) = ap
-instance Monad m => Monad (StateLazyFixT st m) where
- return = StateLazyFixT . return
- m >>= f = StateLazyFixT (unStateLazyFixT m >>= unStateLazyFixT . f)
-instance MonadTrans (StateLazyFixT st) where
- lift = StateLazyFixT . lift
-
--- ** Type 'StateLazyFix'
-type StateLazyFix st
- = StateLazyFixT st Identity
-
--- * Type family 'StateFixCanDo'
-
-type instance CanDo (StateLazyFixT s m) eff
- = StateFixCanDo s eff
-
-type family StateFixCanDo s eff where
- StateFixCanDo s (EffStateFix s) = 'True
- StateFixCanDo s (EffReaderFix s) = 'True
- StateFixCanDo s (EffLocalFix s) = 'True
- StateFixCanDo s (EffWriterFix s) = 'True
- StateFixCanDo s eff = 'False
-
--- * Class 'MonadStateFixN'
-
-class Monad m => MonadStateFixN (n :: Peano) s m where
- stateFixN :: Proxy# n -> (s m -> (a, s m)) -> m a
-
--- | Warning: only work when 'StateLazyFixT'
--- is the outermost 'Monad' (i.e. when @n@ @~@ 'Zero'),
--- because the state is paramaterized by this 'Monad'.
-instance Monad m => MonadStateFixN 'Zero s (StateLazyFixT s m) where
- stateFixN _ = StateLazyFixT . SL.state
-
--- ** Type 'MonadStateFixN'
-
--- | The @'MonadStateFix' s m@ constraint asserts that @m@ is a 'Monad' stack
--- that supports state operations on type @s@
-type MonadStateFix (s::(* -> *) -> *) m
- = MonadStateFixN (Find (EffStateFix s) m) s m
-
--- | Construct a state 'Monad' computation from a function
-stateFix
- :: forall s m a. (MonadStateFix s m)
- => (s m -> (a, s m)) -> m a
-stateFix = stateFixN (proxy# :: Proxy# (Find (EffStateFix s) m))
-
--- | @'put' s@ sets the state within the 'Monad' to @s@
-putFix :: MonadStateFix s m => s m -> m ()
-putFix s = stateFix (\_ -> ((), s))
-
--- | Fetch the current value of the state within the 'Monad'
-getFix :: MonadStateFix s m => m (s m)
-getFix = stateFix (\s -> (s, s))
-
--- | Gets specific component of the state,
--- using a projection function supplied.
-getsFix :: MonadStateFix s m => (s m -> a) -> m a
-getsFix f = do
- s <- getFix
- return (f s)
-
--- | Maps an old state to a new state inside a state 'Monad' layer
-modifyFix :: MonadStateFix s m => (s m -> s m) -> m ()
-modifyFix f = stateFix (\s -> ((), f s))
-
--- | A variant of 'modify' in which the computation
--- is strict in the new state.
-modifyFix' :: MonadStateFix s m => (s m -> s m) -> m ()
-modifyFix' f = stateFix (\s -> let s' = f s in s' `seq` ((), s'))
-
--- Return the 'Monad' parameter and the state.
-runStateLazyFix
- :: st (StateLazyFixT st m)
- -> StateLazyFixT st m a
- -> m (a, st (StateLazyFixT st m))
-runStateLazyFix s m = SL.runStateT (unStateLazyFixT m) s
-
--- Return the 'Monad' parameter.
-evalStateLazyFix
- :: Monad m
- => st (StateLazyFixT st m)
- -> StateLazyFixT st m a
- -> m a
-evalStateLazyFix s m = SL.evalStateT (unStateLazyFixT m) s
-
--- Return the state.
-execStateLazyFix
- :: Monad m
- => st (StateLazyFixT st m)
- -> StateLazyFixT st m a
- -> m (st (StateLazyFixT st m))
-execStateLazyFix s m = SL.execStateT (unStateLazyFixT m) s
diff --git a/calculus/Control/Monad/Classes/StateInstance.hs b/calculus/Control/Monad/Classes/StateInstance.hs
deleted file mode 100644
index 74bc1c4..0000000
--- a/calculus/Control/Monad/Classes/StateInstance.hs
+++ /dev/null
@@ -1,96 +0,0 @@
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE MagicHash #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-} -- NOTE: for CansMonadStateInstance
-module Control.Monad.Classes.StateInstance where
--- | Collect in a 'Monad' stack, the states of 'MC.MonadState' 'Monad'
--- which are instances of a given type class.
-
-import Control.Monad
-import qualified Control.Monad.Classes as MC
-import Control.Monad.Classes.Instance
-import Control.Monad.Trans.Class
-import qualified Control.Monad.Trans.State.Lazy as SL
-import qualified Control.Monad.Trans.State.Strict as SS
-import Data.Bool (Bool(..))
-import GHC.Prim (Proxy#, proxy#, Constraint)
-
--- * Class 'MonadStateInstance'
-
--- ** Type family 'CanMonadStateInstance'
-
--- | An close type family to know whether a 'Monad' @m@
--- support an effect 'eff' whose state is an instance of the type class @cl@.
---
--- NOTE: the closeness enables to define 'Class' instances
--- only for the states of the 'Monad's in a 'Monad' stack
--- which support the effects 'MC.EffState' or 'MC.EffReader'.
-type family CanMonadStateInstance (cl:: * -> Constraint) (m:: * -> *) (eff:: k) :: Bool where
- CanMonadStateInstance cl (SL.StateT s m) (MC.EffState _s) = Class cl s
- CanMonadStateInstance cl (SS.StateT s m) (MC.EffState _s) = Class cl s
- -- CanMonadStateInstance cl (SL.StateT s m) (MC.EffReader _s) = Class cl s
- -- CanMonadStateInstance cl (SS.StateT s m) (MC.EffReader _s) = Class cl s
- CanMonadStateInstance cl s eff = 'False
-
--- ** Type family 'CansMonadStateInstance'
-
--- | A close type family to know which 'Monad's in a 'Monad' stack @stack@
--- support an effect 'eff' whose state is an instance of the type class @cl@.
-type family CansMonadStateInstance (cl:: * -> Constraint) (eff :: k) (stack :: * -> *) :: [Bool] where
- CansMonadStateInstance cl eff (t m) = CanMonadStateInstance cl (t m) eff ': CansMonadStateInstance cl eff m
- CansMonadStateInstance cl eff m = CanMonadStateInstance cl m eff ': '[]
-
--- | A type synonym to constrain a 'Monad' @m@
--- to support an 'MC.EffState' whose state is an instance of the type class @cl@.
-type MonadStateInstance cl m
- = MonadStateInstanceN cl (CansMonadStateInstance cl (MC.EffState ()) m) m
-
-getInstance :: forall cl m. MonadStateInstance cl m => m [Instance cl]
-getInstance = getInstanceN (proxy# :: Proxy# (CansMonadStateInstance cl (MC.EffState ()) m))
-
--- ** Class 'MonadStateInstanceN'
-
--- | A type class to recurse over the 'Monad' stack
--- to collect the states which are instance of the type class @cl@.
-class Monad m => MonadStateInstanceN cl (cans::[Bool]) m where
- getInstanceN :: Proxy# cans -> m [Instance cl]
-
--- | Collect the lazy 'SL.StateT', and recurse.
-instance (cl s, Monad m, MonadStateInstanceN cl cans m)
- => MonadStateInstanceN cl ('True ': cans) (SL.StateT s m) where
- getInstanceN _ = do
- s <- SL.get
- ss <- lift (getInstanceN (proxy# :: Proxy# cans))
- return (Instance s : ss)
-
--- | Collect the strict 'SS.StateT', and recurse.
-instance (cl s, Monad m, MonadStateInstanceN cl cans m)
- => MonadStateInstanceN cl ('True ': cans) (SS.StateT s m) where
- getInstanceN _ = do
- s <- SS.get
- ss <- lift (getInstanceN (proxy# :: Proxy# cans))
- return (Instance s : ss)
-
--- | Recurse the 'Monad' stack, passing over 'Monad' @t m@
--- such that 'CanMonadStateInstance' @cl@ @t m@ @MC.EffState ()@ @~@ 'False'.
-instance
- ( Monad m
- , Monad (t m)
- , MonadTrans t
- , MonadStateInstanceN cl cans m
- ) => MonadStateInstanceN cl ('False ': cans) (t m) where
- getInstanceN _ = lift (getInstanceN (proxy# :: Proxy# cans))
-
--- | Terminating instance, when the deepest 'Monad' on the stack
--- is such that 'CanMonadStateInstance' @cl@ @t m@ @MC.EffState ()@ @~@ 'False':
--- then there is no need to recurse,
--- and thus no 'MonadStateInstanceN' @cl@ @[]@ @m@ constraint to impose.
-instance Monad m => MonadStateInstanceN cl ('False ': '[]) m where
- getInstanceN _ = return []
diff --git a/calculus/cabal.config b/calculus/cabal.config
deleted file mode 100644
index 9d7340b..0000000
--- a/calculus/cabal.config
+++ /dev/null
@@ -1,2 +0,0 @@
-haddock
- html-location: http://hackage.haskell.org/packages/archive/$pkg/latest/doc/html
diff --git a/calculus/hcompta-calculus.cabal b/calculus/hcompta-calculus.cabal
deleted file mode 100644
index 490e28e..0000000
--- a/calculus/hcompta-calculus.cabal
+++ /dev/null
@@ -1,137 +0,0 @@
-author: Julien Moutinho <julm+hcompta@autogeree.net>
-bug-reports: http://doc.autogeree.net/hcompta/bugs
-build-type: Simple
-cabal-version: >= 1.8
-category: Finance
--- data-dir: data
--- data-files:
-description: Accounting calculus.
-extra-source-files: Test.hs
-extra-tmp-files:
-homepage: http://doc.autogeree.net/coop/hcompta
-license: GPL
-license-file: COPYING
-maintainer: Julien Moutinho <julm+hcompta@autogeree.net>
-name: hcompta-calculus
-stability: experimental
-synopsis: Accounting calculus based upon a typed lambda-calculus.
-tested-with: GHC==7.8.4
-version: 0.0.0
-
-source-repository head
- location: git://git.autogeree.net/hcompta
- type: git
-
-Flag dev
- Default: False
- Description: Turn on development settings.
-
-Flag dump
- Default: False
- Description: Dump some intermediate files.
- Manual: True
-
-Flag exe
- Description: Build only executable.
- Default: False
-
-Flag lib
- Description: Build only library.
- Default: False
-
-Flag prof
- Default: False
- Description: Turn on profiling settings.
-
-Flag threaded
- Default: True
- Description: Enable threads.
- Manual: True
-
-Library
- extensions: NoImplicitPrelude
- ghc-options: -Wall -fno-warn-tabs
- if flag(dev)
- cpp-options: -DDEVELOPMENT
- ghc-options:
- -- -ddump-splices
- -- -fno-warn-unused-do-bind -fno-warn-name-shadowing -fno-warn-missing-signatures
- -- -fno-warn-type-defaults -fno-warn-orphans
- else
- ghc-options: -O2
- if flag(dump)
- ghc-options: -ddump-simpl -ddump-stg -ddump-to-file
- if flag(exe)
- Buildable: False
- if flag(prof)
- cpp-options: -DPROFILING
- ghc-options: -O2 -fprof-auto
- -- default-language: Haskell2010
- exposed-modules:
- Calculus.Abstraction.DeBruijn.Generalized
- Calculus.Lambda.Omega.Explicit
- Calculus.Lambda.Omega.Explicit.Read
- Calculus.Lambda.Omega.Implicit
- Control.Monad.Classes.EffectsFix
- Control.Monad.Classes.StateFix
- Control.Monad.Classes.Instance
- Control.Monad.Classes.StateInstance
- build-depends:
- base >= 4.6 && < 5
- , array
- , containers >= 0.5 && < 0.6
- , deepseq >= 1.4 && < 1.5
- , directory
- , filepath
- , ghc-prim
- -- , mtl >= 2.0
- , monad-classes >= 0.3.1.1
- , parsec >= 3.1.2 && < 4
- , peano
- , semigroups
- , strict
- , test-framework
- , test-framework-hunit
- , text
- , text-format
- , time
- , transformers >= 0.4 && < 0.5
-
-Executable hcompta-calculus-explicit
- extensions: NoImplicitPrelude
- ghc-options: -Wall -fno-warn-tabs
- -main-is Calculus.Lambda.Omega.Explicit.REPL
- if flag(threaded)
- ghc-options: -threaded -rtsopts -with-rtsopts=-N
- if flag(dev)
- cpp-options: -DDEVELOPMENT
- ghc-options:
- else
- ghc-options: -O2
- if flag(prof)
- cpp-options: -DPROFILING
- ghc-options: -fprof-auto
- if flag(lib)
- Buildable: False
- exposed-modules:
- main-is: Calculus/Lambda/Omega/Explicit/REPL.hs
- hs-source-dirs: .
- build-depends:
- base >= 4.6 && < 5
- , ansi-terminal >= 0.4 && < 0.7
- , bytestring
- , containers >= 0.5 && < 0.6
- , Decimal
- , deepseq
- , directory
- , filepath
- , haskeline >= 0.7 && < 0.8
- , hcompta-calculus
- , mtl >= 2.0
- , parsec
- , semigroups
- , strict
- , text
- , text-format
- , time
- , transformers >= 0.4 && < 0.5
--
2.47.2