From 94e38fbc7fbe0a249f78e5c0635913e4870244f5 Mon Sep 17 00:00:00 2001 From: Masahiro Sakai Date: Sun, 19 Dec 2010 23:07:04 +0900 Subject: [PATCH] importing from PTQ 0.0.5 --- COPYING | 510 ++++++++++++++++++++++++++++++++ PTQ.cabal | 71 +++++ README | 41 +++ Setup.lhs | 4 + cgi/index.html | 14 + cgi/main.html | 49 +++ misc/Test.hs | 50 ++++ misc/Test2.agda | 99 +++++++ misc/Test3.hs | 53 ++++ src/CGI.hs | 139 +++++++++ src/CGIMain.hs | 31 ++ src/Context.hs | 99 +++++++ src/IL.hs | 319 ++++++++++++++++++++ src/MP.hs | 50 ++++ src/Main.hs | 44 +++ src/P.hs | 213 +++++++++++++ src/PDict.hs | 79 +++++ src/Parser.hs | 723 +++++++++++++++++++++++++++++++++++++++++++++ src/ParserTest.hs | 37 +++ src/Report.hs | 51 ++++ src/ReportHTML.hs | 76 +++++ src/Translation.hs | 184 ++++++++++++ src/URLEncoding.hs | 37 +++ src/Version.hs | 4 + 24 files changed, 2977 insertions(+) create mode 100644 COPYING create mode 100644 PTQ.cabal create mode 100644 README create mode 100755 Setup.lhs create mode 100644 cgi/index.html create mode 100644 cgi/main.html create mode 100644 misc/Test.hs create mode 100644 misc/Test2.agda create mode 100644 misc/Test3.hs create mode 100644 src/CGI.hs create mode 100644 src/CGIMain.hs create mode 100644 src/Context.hs create mode 100644 src/IL.hs create mode 100644 src/MP.hs create mode 100644 src/Main.hs create mode 100644 src/P.hs create mode 100644 src/PDict.hs create mode 100644 src/Parser.hs create mode 100644 src/ParserTest.hs create mode 100644 src/Report.hs create mode 100644 src/ReportHTML.hs create mode 100644 src/Translation.hs create mode 100644 src/URLEncoding.hs create mode 100644 src/Version.hs diff --git a/COPYING b/COPYING new file mode 100644 index 0000000..cf9b6b9 --- /dev/null +++ b/COPYING @@ -0,0 +1,510 @@ + + GNU LESSER GENERAL PUBLIC LICENSE + Version 2.1, February 1999 + + Copyright (C) 1991, 1999 Free Software Foundation, Inc. + 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + +[This is the first released version of the Lesser GPL. It also counts + as the successor of the GNU Library Public License, version 2, hence + the version number 2.1.] + + Preamble + + The licenses for most software are designed to take away your +freedom to share and change it. By contrast, the GNU General Public +Licenses are intended to guarantee your freedom to share and change +free software--to make sure the software is free for all its users. + + This license, the Lesser General Public License, applies to some +specially designated software packages--typically libraries--of the +Free Software Foundation and other authors who decide to use it. You +can use it too, but we suggest you first think carefully about whether +this license or the ordinary General Public License is the better +strategy to use in any particular case, based on the explanations +below. + + When we speak of free software, we are referring to freedom of use, +not price. Our General Public Licenses are designed to make sure that +you have the freedom to distribute copies of free software (and charge +for this service if you wish); that you receive source code or can get +it if you want it; that you can change the software and use pieces of +it in new free programs; and that you are informed that you can do +these things. + + To protect your rights, we need to make restrictions that forbid +distributors to deny you these rights or to ask you to surrender these +rights. These restrictions translate to certain responsibilities for +you if you distribute copies of the library or if you modify it. + + For example, if you distribute copies of the library, whether gratis +or for a fee, you must give the recipients all the rights that we gave +you. You must make sure that they, too, receive or can get the source +code. If you link other code with the library, you must provide +complete object files to the recipients, so that they can relink them +with the library after making changes to the library and recompiling +it. And you must show them these terms so they know their rights. + + We protect your rights with a two-step method: (1) we copyright the +library, and (2) we offer you this license, which gives you legal +permission to copy, distribute and/or modify the library. + + To protect each distributor, we want to make it very clear that +there is no warranty for the free library. Also, if the library is +modified by someone else and passed on, the recipients should know +that what they have is not the original version, so that the original +author's reputation will not be affected by problems that might be +introduced by others. +^L + Finally, software patents pose a constant threat to the existence of +any free program. We wish to make sure that a company cannot +effectively restrict the users of a free program by obtaining a +restrictive license from a patent holder. Therefore, we insist that +any patent license obtained for a version of the library must be +consistent with the full freedom of use specified in this license. + + Most GNU software, including some libraries, is covered by the +ordinary GNU General Public License. This license, the GNU Lesser +General Public License, applies to certain designated libraries, and +is quite different from the ordinary General Public License. We use +this license for certain libraries in order to permit linking those +libraries into non-free programs. + + When a program is linked with a library, whether statically or using +a shared library, the combination of the two is legally speaking a +combined work, a derivative of the original library. The ordinary +General Public License therefore permits such linking only if the +entire combination fits its criteria of freedom. The Lesser General +Public License permits more lax criteria for linking other code with +the library. + + We call this license the "Lesser" General Public License because it +does Less to protect the user's freedom than the ordinary General +Public License. It also provides other free software developers Less +of an advantage over competing non-free programs. These disadvantages +are the reason we use the ordinary General Public License for many +libraries. However, the Lesser license provides advantages in certain +special circumstances. + + For example, on rare occasions, there may be a special need to +encourage the widest possible use of a certain library, so that it +becomes a de-facto standard. To achieve this, non-free programs must +be allowed to use the library. A more frequent case is that a free +library does the same job as widely used non-free libraries. In this +case, there is little to gain by limiting the free library to free +software only, so we use the Lesser General Public License. + + In other cases, permission to use a particular library in non-free +programs enables a greater number of people to use a large body of +free software. For example, permission to use the GNU C Library in +non-free programs enables many more people to use the whole GNU +operating system, as well as its variant, the GNU/Linux operating +system. + + Although the Lesser General Public License is Less protective of the +users' freedom, it does ensure that the user of a program that is +linked with the Library has the freedom and the wherewithal to run +that program using a modified version of the Library. + + The precise terms and conditions for copying, distribution and +modification follow. Pay close attention to the difference between a +"work based on the library" and a "work that uses the library". The +former contains code derived from the library, whereas the latter must +be combined with the library in order to run. +^L + GNU LESSER GENERAL PUBLIC LICENSE + TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION + + 0. This License Agreement applies to any software library or other +program which contains a notice placed by the copyright holder or +other authorized party saying it may be distributed under the terms of +this Lesser General Public License (also called "this License"). +Each licensee is addressed as "you". + + A "library" means a collection of software functions and/or data +prepared so as to be conveniently linked with application programs +(which use some of those functions and data) to form executables. + + The "Library", below, refers to any such software library or work +which has been distributed under these terms. A "work based on the +Library" means either the Library or any derivative work under +copyright law: that is to say, a work containing the Library or a +portion of it, either verbatim or with modifications and/or translated +straightforwardly into another language. (Hereinafter, translation is +included without limitation in the term "modification".) + + "Source code" for a work means the preferred form of the work for +making modifications to it. For a library, complete source code means +all the source code for all modules it contains, plus any associated +interface definition files, plus the scripts used to control +compilation and installation of the library. + + Activities other than copying, distribution and modification are not +covered by this License; they are outside its scope. The act of +running a program using the Library is not restricted, and output from +such a program is covered only if its contents constitute a work based +on the Library (independent of the use of the Library in a tool for +writing it). Whether that is true depends on what the Library does +and what the program that uses the Library does. + + 1. You may copy and distribute verbatim copies of the Library's +complete source code as you receive it, in any medium, provided that +you conspicuously and appropriately publish on each copy an +appropriate copyright notice and disclaimer of warranty; keep intact +all the notices that refer to this License and to the absence of any +warranty; and distribute a copy of this License along with the +Library. + + You may charge a fee for the physical act of transferring a copy, +and you may at your option offer warranty protection in exchange for a +fee. + + 2. You may modify your copy or copies of the Library or any portion +of it, thus forming a work based on the Library, and copy and +distribute such modifications or work under the terms of Section 1 +above, provided that you also meet all of these conditions: + + a) The modified work must itself be a software library. + + b) You must cause the files modified to carry prominent notices + stating that you changed the files and the date of any change. + + c) You must cause the whole of the work to be licensed at no + charge to all third parties under the terms of this License. + + d) If a facility in the modified Library refers to a function or a + table of data to be supplied by an application program that uses + the facility, other than as an argument passed when the facility + is invoked, then you must make a good faith effort to ensure that, + in the event an application does not supply such function or + table, the facility still operates, and performs whatever part of + its purpose remains meaningful. + + (For example, a function in a library to compute square roots has + a purpose that is entirely well-defined independent of the + application. Therefore, Subsection 2d requires that any + application-supplied function or table used by this function must + be optional: if the application does not supply it, the square + root function must still compute square roots.) + +These requirements apply to the modified work as a whole. If +identifiable sections of that work are not derived from the Library, +and can be reasonably considered independent and separate works in +themselves, then this License, and its terms, do not apply to those +sections when you distribute them as separate works. But when you +distribute the same sections as part of a whole which is a work based +on the Library, the distribution of the whole must be on the terms of +this License, whose permissions for other licensees extend to the +entire whole, and thus to each and every part regardless of who wrote +it. + +Thus, it is not the intent of this section to claim rights or contest +your rights to work written entirely by you; rather, the intent is to +exercise the right to control the distribution of derivative or +collective works based on the Library. + +In addition, mere aggregation of another work not based on the Library +with the Library (or with a work based on the Library) on a volume of +a storage or distribution medium does not bring the other work under +the scope of this License. + + 3. You may opt to apply the terms of the ordinary GNU General Public +License instead of this License to a given copy of the Library. To do +this, you must alter all the notices that refer to this License, so +that they refer to the ordinary GNU General Public License, version 2, +instead of to this License. (If a newer version than version 2 of the +ordinary GNU General Public License has appeared, then you can specify +that version instead if you wish.) Do not make any other change in +these notices. +^L + Once this change is made in a given copy, it is irreversible for +that copy, so the ordinary GNU General Public License applies to all +subsequent copies and derivative works made from that copy. + + This option is useful when you wish to copy part of the code of +the Library into a program that is not a library. + + 4. You may copy and distribute the Library (or a portion or +derivative of it, under Section 2) in object code or executable form +under the terms of Sections 1 and 2 above provided that you accompany +it with the complete corresponding machine-readable source code, which +must be distributed under the terms of Sections 1 and 2 above on a +medium customarily used for software interchange. + + If distribution of object code is made by offering access to copy +from a designated place, then offering equivalent access to copy the +source code from the same place satisfies the requirement to +distribute the source code, even though third parties are not +compelled to copy the source along with the object code. + + 5. A program that contains no derivative of any portion of the +Library, but is designed to work with the Library by being compiled or +linked with it, is called a "work that uses the Library". Such a +work, in isolation, is not a derivative work of the Library, and +therefore falls outside the scope of this License. + + However, linking a "work that uses the Library" with the Library +creates an executable that is a derivative of the Library (because it +contains portions of the Library), rather than a "work that uses the +library". The executable is therefore covered by this License. +Section 6 states terms for distribution of such executables. + + When a "work that uses the Library" uses material from a header file +that is part of the Library, the object code for the work may be a +derivative work of the Library even though the source code is not. +Whether this is true is especially significant if the work can be +linked without the Library, or if the work is itself a library. The +threshold for this to be true is not precisely defined by law. + + If such an object file uses only numerical parameters, data +structure layouts and accessors, and small macros and small inline +functions (ten lines or less in length), then the use of the object +file is unrestricted, regardless of whether it is legally a derivative +work. (Executables containing this object code plus portions of the +Library will still fall under Section 6.) + + Otherwise, if the work is a derivative of the Library, you may +distribute the object code for the work under the terms of Section 6. +Any executables containing that work also fall under Section 6, +whether or not they are linked directly with the Library itself. +^L + 6. As an exception to the Sections above, you may also combine or +link a "work that uses the Library" with the Library to produce a +work containing portions of the Library, and distribute that work +under terms of your choice, provided that the terms permit +modification of the work for the customer's own use and reverse +engineering for debugging such modifications. + + You must give prominent notice with each copy of the work that the +Library is used in it and that the Library and its use are covered by +this License. You must supply a copy of this License. If the work +during execution displays copyright notices, you must include the +copyright notice for the Library among them, as well as a reference +directing the user to the copy of this License. Also, you must do one +of these things: + + a) Accompany the work with the complete corresponding + machine-readable source code for the Library including whatever + changes were used in the work (which must be distributed under + Sections 1 and 2 above); and, if the work is an executable linked + with the Library, with the complete machine-readable "work that + uses the Library", as object code and/or source code, so that the + user can modify the Library and then relink to produce a modified + executable containing the modified Library. (It is understood + that the user who changes the contents of definitions files in the + Library will not necessarily be able to recompile the application + to use the modified definitions.) + + b) Use a suitable shared library mechanism for linking with the + Library. A suitable mechanism is one that (1) uses at run time a + copy of the library already present on the user's computer system, + rather than copying library functions into the executable, and (2) + will operate properly with a modified version of the library, if + the user installs one, as long as the modified version is + interface-compatible with the version that the work was made with. + + c) Accompany the work with a written offer, valid for at least + three years, to give the same user the materials specified in + Subsection 6a, above, for a charge no more than the cost of + performing this distribution. + + d) If distribution of the work is made by offering access to copy + from a designated place, offer equivalent access to copy the above + specified materials from the same place. + + e) Verify that the user has already received a copy of these + materials or that you have already sent this user a copy. + + For an executable, the required form of the "work that uses the +Library" must include any data and utility programs needed for +reproducing the executable from it. However, as a special exception, +the materials to be distributed need not include anything that is +normally distributed (in either source or binary form) with the major +components (compiler, kernel, and so on) of the operating system on +which the executable runs, unless that component itself accompanies +the executable. + + It may happen that this requirement contradicts the license +restrictions of other proprietary libraries that do not normally +accompany the operating system. Such a contradiction means you cannot +use both them and the Library together in an executable that you +distribute. +^L + 7. You may place library facilities that are a work based on the +Library side-by-side in a single library together with other library +facilities not covered by this License, and distribute such a combined +library, provided that the separate distribution of the work based on +the Library and of the other library facilities is otherwise +permitted, and provided that you do these two things: + + a) Accompany the combined library with a copy of the same work + based on the Library, uncombined with any other library + facilities. This must be distributed under the terms of the + Sections above. + + b) Give prominent notice with the combined library of the fact + that part of it is a work based on the Library, and explaining + where to find the accompanying uncombined form of the same work. + + 8. You may not copy, modify, sublicense, link with, or distribute +the Library except as expressly provided under this License. Any +attempt otherwise to copy, modify, sublicense, link with, or +distribute the Library is void, and will automatically terminate your +rights under this License. However, parties who have received copies, +or rights, from you under this License will not have their licenses +terminated so long as such parties remain in full compliance. + + 9. You are not required to accept this License, since you have not +signed it. However, nothing else grants you permission to modify or +distribute the Library or its derivative works. These actions are +prohibited by law if you do not accept this License. Therefore, by +modifying or distributing the Library (or any work based on the +Library), you indicate your acceptance of this License to do so, and +all its terms and conditions for copying, distributing or modifying +the Library or works based on it. + + 10. Each time you redistribute the Library (or any work based on the +Library), the recipient automatically receives a license from the +original licensor to copy, distribute, link with or modify the Library +subject to these terms and conditions. You may not impose any further +restrictions on the recipients' exercise of the rights granted herein. +You are not responsible for enforcing compliance by third parties with +this License. +^L + 11. If, as a consequence of a court judgment or allegation of patent +infringement or for any other reason (not limited to patent issues), +conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot +distribute so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you +may not distribute the Library at all. For example, if a patent +license would not permit royalty-free redistribution of the Library by +all those who receive copies directly or indirectly through you, then +the only way you could satisfy both it and this License would be to +refrain entirely from distribution of the Library. + +If any portion of this section is held invalid or unenforceable under +any particular circumstance, the balance of the section is intended to +apply, and the section as a whole is intended to apply in other +circumstances. + +It is not the purpose of this section to induce you to infringe any +patents or other property right claims or to contest validity of any +such claims; this section has the sole purpose of protecting the +integrity of the free software distribution system which is +implemented by public license practices. Many people have made +generous contributions to the wide range of software distributed +through that system in reliance on consistent application of that +system; it is up to the author/donor to decide if he or she is willing +to distribute software through any other system and a licensee cannot +impose that choice. + +This section is intended to make thoroughly clear what is believed to +be a consequence of the rest of this License. + + 12. If the distribution and/or use of the Library is restricted in +certain countries either by patents or by copyrighted interfaces, the +original copyright holder who places the Library under this License +may add an explicit geographical distribution limitation excluding those +countries, so that distribution is permitted only in or among +countries not thus excluded. In such case, this License incorporates +the limitation as if written in the body of this License. + + 13. The Free Software Foundation may publish revised and/or new +versions of the Lesser 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 Library +specifies a version number of this License which applies to it and +"any later version", you have the option of following the terms and +conditions either of that version or of any later version published by +the Free Software Foundation. If the Library does not specify a +license version number, you may choose any version ever published by +the Free Software Foundation. +^L + 14. If you wish to incorporate parts of the Library into other free +programs whose distribution conditions are incompatible with these, +write to the author to ask for permission. For software which is +copyrighted by the Free Software Foundation, write to the Free +Software Foundation; we sometimes make exceptions for this. Our +decision will be guided by the two goals of preserving the free status +of all derivatives of our free software and of promoting the sharing +and reuse of software generally. + + NO WARRANTY + + 15. BECAUSE THE LIBRARY IS LICENSED FREE OF CHARGE, THERE IS NO +WARRANTY FOR THE LIBRARY, TO THE EXTENT PERMITTED BY APPLICABLE LAW. +EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR +OTHER PARTIES PROVIDE THE LIBRARY "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 +LIBRARY IS WITH YOU. SHOULD THE LIBRARY PROVE DEFECTIVE, YOU ASSUME +THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION. + + 16. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN +WRITING WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY +AND/OR REDISTRIBUTE THE LIBRARY 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 +LIBRARY (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 LIBRARY TO OPERATE WITH ANY OTHER SOFTWARE), EVEN IF +SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH +DAMAGES. + + END OF TERMS AND CONDITIONS +^L + How to Apply These Terms to Your New Libraries + + If you develop a new library, and you want it to be of the greatest +possible use to the public, we recommend making it free software that +everyone can redistribute and change. You can do so by permitting +redistribution under these terms (or, alternatively, under the terms +of the ordinary General Public License). + + To apply these terms, attach the following notices to the library. +It is safest to attach them to the start of each source file to most +effectively convey the exclusion of warranty; and each file should +have at least the "copyright" line and a pointer to where the full +notice is found. + + + + Copyright (C) + + This library is free software; you can redistribute it and/or + modify it under the terms of the GNU Lesser General Public + License as published by the Free Software Foundation; either + version 2.1 of the License, or (at your option) any later version. + + This library 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 + Lesser General Public License for more details. + + You should have received a copy of the GNU Lesser General Public + License along with this library; if not, write to the Free Software + Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA + +Also add information on how to contact you by electronic and paper mail. + +You should also get your employer (if you work as a programmer) or +your school, if any, to sign a "copyright disclaimer" for the library, +if necessary. Here is a sample; alter the names: + + Yoyodyne, Inc., hereby disclaims all copyright interest in the + library `Frob' (a library for tweaking knobs) written by James + Random Hacker. + + , 1 April 1990 + Ty Coon, President of Vice + +That's all there is to it! + + diff --git a/PTQ.cabal b/PTQ.cabal new file mode 100644 index 0000000..b167797 --- /dev/null +++ b/PTQ.cabal @@ -0,0 +1,71 @@ +Name: PTQ +Version: 0.0.5 +License: LGPL +License-File: COPYING +Author: Masahiro Sakai +Maintainer: Masahiro Sakai +Homepage: http://www.tom.sfc.keio.ac.jp/~sakai/hiki/?hsPTQ +Category: Natural Language Processing +Build-Type: Simple +Synopsis: An implementation of Montague's PTQ. +Description: An implementation of Montague's PTQ (Proper Treatment of Quantification). It translates simple plain English sentences into formulas of intentional logic. +Cabal-Version: >= 1.2.3 +Stability: experimental +Extra-Source-Files: + README, COPYING + src/Context.hs, src/MP.hs, src/PDict.hs, src/ParserTest.hs, + misc/Test.hs, misc/Test2.agda, misc/Test3.hs +Data-Files: cgi/index.html, cgi/main.html + +Flag UTF8Terminal + Description: Use UTF-8 for terminal I/O + Default: False + +Flag UTF8CGI + Description: Use UTF-8 for HTTP contents + Default: True + +Executable ptq + Main-Is: Main.hs + Hs-Source-Dirs: src + Other-Modules: + IL + P + Translation + Parser + Report + Version + Extensions: + EmptyDataDecls + GADTs + MultiParamTypeClasses + TypeOperators + TypeSynonymInstances + Build-Depends: base >=4 && <5, haskell98, mtl, containers + if flag(UTF8Terminal) + CPP-Options: "-DUSE_UTF8" + Build-Depends: utf8-string + +Executable ptq.cgi + Main-Is: CGIMain.hs + Hs-Source-Dirs: src + Other-Modules: + IL + P + Translation + Parser + Version + ReportHTML + CGI + URLEncoding + Extensions: + EmptyDataDecls + GADTs + MultiParamTypeClasses + TypeOperators + TypeSynonymInstances + CPP + Build-Depends: base >=4 && <5, haskell98, mtl, containers, network, xml + if flag(UTF8CGI) + CPP-Options: "-DUSE_UTF8" + Build-Depends: utf8-string diff --git a/README b/README new file mode 100644 index 0000000..9319ba7 --- /dev/null +++ b/README @@ -0,0 +1,41 @@ += An implementation of Montague's PTQ in Haskell + +== Build and Install + +You'll need GHC 6.7 or later. + + % runhaskell Setup.lhs configure + % runhaskell Setup.lhs build + % runhaskell Setup.lhs install + +== Usage of interactive shell ptq + + % ptq + PTQ> John seeks a unicorn. + Parsed: + F4 john (F5 seek (F2 a unicorn)) + + Translation: + (\x0. x0 {john}) (Int (seek (Int ((\x0. \x1. exists x2. x0 {x2} && x1 {x2}) (Int unicorn))))) + + Translation (simplified): + seek (Int (\x0. exists x1. unicorn x1 && x0 {x1})) john + + ------------------------------------------------------ + + Parsed: + F10 0 (F2 a unicorn) (F4 john (F5 seek (He 0))) + + Translation: + (\x0. \x1. exists x2. x0 {x2} && x1 {x2}) (Int unicorn) (Int (\x0. (\x1. x1 {john}) (Int (seek (Int (\x1. x1 {x0})))))) + + Translation (simplified): + exists x0. unicorn x0 && seek (Int (\x1. x1 {x0})) john + PTQ> quit + % + +== CGI interface + +By locating ptq.cgi, cgi/index.html and cgi/main.html to the place +where CGI is executable, you can try it on the web. +Demo site runs at . diff --git a/Setup.lhs b/Setup.lhs new file mode 100755 index 0000000..6ad1835 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,4 @@ +#! /usr/bin/env runhaskell + +> import Distribution.Simple +> main = defaultMain diff --git a/cgi/index.html b/cgi/index.html new file mode 100644 index 0000000..2d7f7e9 --- /dev/null +++ b/cgi/index.html @@ -0,0 +1,14 @@ + + + + +Demo page of PTQ + + + + + +<a href="main.html">No frame version</a> + + + diff --git a/cgi/main.html b/cgi/main.html new file mode 100644 index 0000000..fab66e3 --- /dev/null +++ b/cgi/main.html @@ -0,0 +1,49 @@ + + + + +Demo page of PTQ + + + +

Demo page of PTQ

+ +

+

+ + +
+

+ +

+

+Sample: +
+

+ + diff --git a/misc/Test.hs b/misc/Test.hs new file mode 100644 index 0000000..1d43354 --- /dev/null +++ b/misc/Test.hs @@ -0,0 +1,50 @@ +{-# OPTIONS_GHC -fglasgow-exts #-} + +{-# OPTIONS_GHC -fallow-undecidable-instances #-} +-- coverage condition を満たしていないインスタンス宣言があるため + +----------------------------------------------------------------------------- +-- Expr.hs + +-- Benetteの意味タイプ +data E -- 個体 +data Prop -- 本来はtと書かれるけど、小文字が使えないので +data S a +-- 関数型はHaskellの -> をそのまま使う + +infixl 9 :@ + +-- 意味タイプがtである式 +data Expr t where + FVar :: Name -> Expr t + BVar :: !Int -> Expr t + Lam :: Name -> Scope b -> Expr (a -> b) + Forall :: Name -> Scope Prop -> Expr Prop + Exists :: Name -> Scope Prop -> Expr Prop + (:@) :: Expr (a -> b) -> Expr a -> Expr b + C :: C t -> Expr t + +type Name = String +newtype Scope t = Sc (Expr t) + +data C t where + John' :: C E + Mary' :: C E + Bill' :: C E + Int :: C (a -> S a) + +abstract :: Name -> Expr t -> Scope t +abstract name expr = Sc (h 0 expr) + where + h outer (FVar name') | name==name' = BVar 0 + | otherwise = FVar name' + h outer (BVar index) = BVar index + +-- instantiate :: Expr u -> Scope t -> Expr t + +----------------------------------------------------------------------------- + +-- import Expr.hs + + +----------------------------------------------------------------------------- diff --git a/misc/Test2.agda b/misc/Test2.agda new file mode 100644 index 0000000..7a77ac1 --- /dev/null +++ b/misc/Test2.agda @@ -0,0 +1,99 @@ +postulate s :: Set +postulate e :: Set +postulate t :: Set +postulate ext :: (a::Set) |-> (s -> a) -> a +postulate int :: (a::Set) |-> a -> (s -> a) +postulate box :: t -> t +postulate id :: e -> e -> t +postulate and :: t -> t -> t +postulate or :: t -> t -> t +postulate imply :: t -> t -> t +postulate equiv :: t -> t -> t +postulate not :: t -> t +postulate forall :: (e -> t) -> t +postulate exists :: (e -> t) -> t +postulate H :: t -> t +postulate F :: t -> t + +CN :: Set +CN = e -> t + +IV :: Set +IV = e -> t + +(/) :: Set -> Set -> Set +a / b = (s -> b) -> a + +(//) :: Set -> Set -> Set +a // b = (s -> b) -> a + +T = t / IV +TV = IV / T +IAV = IV / IV + +Det = T / CN +DTV = TV / T +TTV = TV / T +PP = IV / TV +Adj :: Set +Adj = e -> t + +be :: TV +be p x = ext p (int (\(y::e) -> id x y)) + +necessarily :: t / t +necessarily p = box (ext p) + +postulate j :: e +postulate m :: e +postulate b :: e +postulate n :: e + +John :: T +John P = ext P j + +Mary :: T +Mary P = ext P m + +Bill :: T +Bill P = ext P b + +ninty :: T +ninty P = ext P n + +a :: Det +a p q = exists (\(x::e) -> and (ext p x) (ext q x)) + +the :: Det +the p q = exists (\(y::e) -> + forall (\(x::e) -> and (equiv (ext p x) (id x y)) (ext q x))) + +every :: Det +every p q = forall (\(x::e) -> imply (ext p x) (ext q x)) + +no :: Det +no p q = forall (\(x::e) -> not (and (ext p x) (ext q x))) + +be' :: IV / Adj +be' P x = ext P x + +by :: PP / T +by P R x = ext P (int (\(y::e) -> ext R (int (\(Q::s -> e -> t) -> ext Q x)) y)) + +-- NG +by' :: PP / T +by' P R x = ext P (int (\(y::e) -> int R {! !} {! !} {! !} {! !})) +-- λP λR λx P{^ (λy [^R(y, ^(λP P{x}))])} + +bar :: ((R::{! !}) -> (h::{! !}) -> {! !}) / T +bar = \(P::s->T) -> \(R::{! !}) -> \(x::e) -> + ext P (int (\(y::e) -> {! !})) + +{- +Q : s -> e -> x + +int (\Q -> ext Q x) +-} + +F25 :: TV -> Adj +F25 delta x = exists (\(y::e) -> H (delta (int (\(P::s->e->t) -> ext P x)) y)) diff --git a/misc/Test3.hs b/misc/Test3.hs new file mode 100644 index 0000000..89dea12 --- /dev/null +++ b/misc/Test3.hs @@ -0,0 +1,53 @@ +{-# OPTIONS_GHC -fallow-undecidable-instances #-} +-- coverage condition を満たしていないインスタンス宣言があるため + +----------------------------------------------------------------------------- + +data Prop +data S +data E + +infixl 9 :@ + +data Expr t where + BVar :: Int -> Expr t + FVar :: String -> Expr t + (:@) :: Expr (a->b) -> Expr a -> Expr b + Lam :: Expr b -> Expr (a->b) + Int :: Expr a -> Expr (S->a) + Ext :: Expr (S->a) -> Expr a + +----------------------------------------------------------------------------- + +infixl 1 :/ + +data Sen +data IV +data CN +data (:/) a b + +type T = Sen :/ IV +type TV = IV :/ T +type IAV = IV :/ IV + +data P c where + F :: CatToType b u => P (a :/ b) -> P b -> P a + +class CatToType c t | c -> t +instance CatToType Sen Prop +instance CatToType IV (E->Prop) +instance CatToType CN (E->Prop) +instance (CatToType a t, CatToType b u) => CatToType (a :/ b) ((S->u)->t) + +translate :: CatToType c t => P c -> Expr t +translate (F fun arg) = translate fun :@ Int (translate arg) + +----------------------------------------------------------------------------- + +{- +class Assoc a b | a -> b +instance Assoc Int Int + +f :: Assoc Int b => Int -> b +f x = x +-} diff --git a/src/CGI.hs b/src/CGI.hs new file mode 100644 index 0000000..a5f6451 --- /dev/null +++ b/src/CGI.hs @@ -0,0 +1,139 @@ +----------------------------------------------------------------------------- +-- | +-- Module : CGI +-- Copyright : Copyright (c) 2005,2006 Minero Aoki +-- License : LGPL (see COPYING) +-- +-- Maintainer: masahiro.sakai@gmail.com +-- Stability : experimental +-- Portability : non-portable + +{-# LANGUAGE CPP #-} + +-- +-- $Id: CGI.hs,v 1.2 2006/05/14 17:29:22 aamine Exp $ +-- +-- Copyright (c) 2005,2006 Minero Aoki +-- +-- This program is free software. +-- You can distribute/modify this program under the terms of +-- the GNU LGPL, Lesser General Public License version 2.1. +-- For details of the GNU LGPL, see the file "COPYING". +-- + +module CGI + (runCGI, + HTTPRequest, varExist, lookupVar, lookupVars, + HTTPResponse(..), httpResponseToString, textContentType) where + +import URLEncoding +import Data.Maybe +import Control.Monad +import System.IO +import System.Environment +#ifdef USE_UTF8 +import qualified Codec.Binary.UTF8.String as UTF8 +#endif + +runCGI :: (HTTPRequest -> IO HTTPResponse) -> IO () +runCGI f = do hSetBinaryMode stdin True + hSetBinaryMode stdout True + input <- getContents + env <- cgiEnvs + res <- f (parseCGIRequest env input) + putStr (httpResponseToString' res) + +cgiEnvs = return . catMaybes =<< mapM mGetEnvPair names + where + mGetEnvPair :: String -> IO (Maybe (String, String)) + mGetEnvPair name = catch (return . Just . (,) name =<< getEnv name) + (const $ return Nothing) + + names = [ "SERVER_NAME", "SERVER_PORT", + "SERVER_SOFTWARE", "SERVER_PROTOCOL", + "GATEWAY_INTERFACE", "SCRIPT_NAME", "REQUEST_METHOD", + "PATH_INFO", "PATH_TRANSLATED", + "CONTENT_TYPE", "CONTENT_LENGTH", "QUERY_STRING", + "HTTP_COOKIE", "HTTP_ACCEPT", + "REMOTE_HOST", "REMOTE_ADDR", "REMOTE_USER", + "AUTH_TYPE", "HTTPS" ] + +data HTTPRequest = HTTPRequest { params :: [(String, String)] } + +parseCGIRequest env input = + case method of + "GET" -> parseGET env + "POST" -> parsePOST env input + _ -> parseUnknown + where + method = getenv "REQUEST_METHOD" env + + getenv key env = fromMaybe "" $ lookup key env + + parseGET env = HTTPRequest (parseQueryString $ getenv "QUERY_STRING" env) + + parsePOST env input = HTTPRequest (parseQueryString $ input) + + -- FIXME + parseUnknown = HTTPRequest [] + + parseQueryString = map splitKV . splitQueryString + + splitQueryString = splitBy (\c -> c == ';' || c == '&') + + splitKV kv = case break (== '=') kv of + (k, ('=':v)) -> (decodeWord k, decodeWord v) + (k, "") -> (decodeWord k, "") + + decodeWord = urldecode . decodePlus + + decodePlus = map (\c -> if c == '+' then ' ' else c) + +splitBy :: (Char -> Bool) -> String -> [String] +splitBy _ [] = [] +splitBy f str = word : splitBy f cont + where + (word, cont') = break f str + cont = case cont' of + [] -> "" + (c:cs) -> cs + +varExist :: String -> HTTPRequest -> Bool +varExist key = isJust . lookupVar key + +lookupVar :: String -> HTTPRequest -> Maybe String +lookupVar key = lookup key . params + +lookupVars :: String -> HTTPRequest -> [String] +lookupVars key = lookupAll key . params + +lookupAll :: Eq a => a -> [(a,b)] -> [b] +lookupAll key = map snd . filter ((== key) . fst) + +data HTTPResponse = HTTPResponse { + resContentType :: String, + resBody :: String +} + +instance Show HTTPResponse where + show = httpResponseToString + +httpResponseToString (HTTPResponse ctype body) = + concat [ "Content-Type: ", ctype, "\r\n", + "Content-Length: ", show (length body), "\r\n", + "\r\n", + body ] + +#ifdef USE_UTF8 +httpResponseToString' (HTTPResponse ctype body) = + concat [ "Content-Type: ", ctype, "\r\n", + "Content-Length: ", show (length body'), "\r\n", + "\r\n", + body' ] + where + body' = UTF8.encodeString body +#else +httpResponseToString' = httpResponseToString +#endif + +textContentType typ encoding = concat [typ, "; charset=\"", encoding, "\""] diff --git a/src/CGIMain.hs b/src/CGIMain.hs new file mode 100644 index 0000000..781b914 --- /dev/null +++ b/src/CGIMain.hs @@ -0,0 +1,31 @@ +----------------------------------------------------------------------------- +-- | +-- Module : CGIMain +-- Copyright : (c) Masahiro Sakai 2007-2009 +-- License : BSD3-style (see LICENSE) +-- +-- Maintainer: masahiro.sakai@gmail.com +-- Stability : experimental +-- Portability : portable + +module Main where + +import ReportHTML +import CGI +import Control.Concurrent + +-- 1秒以内に処理が終わらなかったら、そのままプロセスを終了 +main :: IO () +main = + do th <- myThreadId + forkIO $ threadDelay (1*1000*1000) >> killThread th + runCGI appMain + +appMain :: HTTPRequest -> IO HTTPResponse +appMain req = return $ + case lookupVar "s" req of + Nothing -> + HTTPResponse (textContentType "text/plain" "us-ascii") "(no input)\n" + Just s -> + --HTTPResponse (textContentType "text/plain" "utf-8") (report s) + HTTPResponse (textContentType "text/html" "utf-8") (report s) diff --git a/src/Context.hs b/src/Context.hs new file mode 100644 index 0000000..62aa006 --- /dev/null +++ b/src/Context.hs @@ -0,0 +1,99 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Context +-- Copyright : (c) Masahiro Sakai 2007-2009 +-- License : BSD3-style (see LICENSE) +-- +-- Maintainer: masahiro.sakai@gmail.com +-- Stability : experimental +-- Portability : non-portable + +class Context a + +data Empty +instance Context Empty + +infixl 9 :* +infixl 9 :@ + +data (:*) c a +instance Context c => Context (c :* a) + +class Append c d e | c d -> e +instance Append c Empty c +instance Append c d e => Append c (d :* a) (e :* a) + +data BVar ctx a where + B0 :: BVar (c :* a) a + BS :: BVar c a -> BVar (c :* b) a + +data Expr c t where + B :: BVar c t -> Expr c t + (:@) :: Expr c (a->b) -> Expr c a -> Expr c b + Lam :: Expr (c :* a) b -> Expr c (a->b) + +type Name = String + +{- +inst :: Expr (c :* a) b -> Expr c a -> Expr c b +inst (B v) x = case v of + B0 -> x + BS v -> B v +inst (a :@ b) x = inst a x :@ inst b x +inst (Lam a) x = + case x of + B B0 -> + B (BS v) -> +-} + +{- +f :: forall c d a. Expr c a -> (forall a. BVar c a -> Expr d a) -> Expr d a +f x g = + case x of + a :@ b -> f a g :@ f b g + B x -> g x + Lam y -> Lam (f y g') + where g' :: forall b z. BVar (c :* z) b -> Expr (d :* z) b + g' B0 = B B0 + g' (BS x) = let foo :: Expr d b + foo = g x + bar :: Expr (d :* z) b + bar = shift foo + in bar +-} + +shift' :: forall c d e e' u t. + (Append c d e, Append (c :* u) d e') => + (forall t. BVar e t -> BVar e' t) -> + Expr e t -> Expr e' t +shift' v (a :@ b) = shift' v a :@ shift' v b +shift' v (B x) = B (v x) +shift' v (Lam x) = Lam (shift' v' x) + where v' B0 = B0 + v' (BS x) = BS (v x) + +shift0 :: Expr c t -> Expr (c :* u) t +shift0 (a :@ b) = shift0 a :@ shift0 b +shift0 (B x) = B (v0 x) +shift0 (Lam x) = Lam (shift1 x) + +v0 :: BVar c t -> BVar (c :* u) t +v0 = BS + +shift1 :: Expr (c :* a) t -> Expr (c :* u :* a) t +shift1 (a :@ b) = shift1 a :@ shift1 b +shift1 (B x) = B (v1 x) +shift1 (Lam x) = Lam (shift2 x) + +v1 :: BVar (c :* a) t -> BVar (c :* u :* a) t +v1 B0 = B0 +v1 (BS x) = BS (v0 x) + +shift2 :: Expr (c :* a :* b) t -> Expr (c :* u :* a :* b) t +shift2 (a :@ b) = shift2 a :@ shift2 b +shift2 (B x) = B (v2 x) +shift2 (Lam x) = undefined + +v2 :: BVar (c :* a :* b) t -> BVar (c :* u :* a :* b) t +v2 B0 = B0 +v2 (BS x) = BS (v1 x) diff --git a/src/IL.hs b/src/IL.hs new file mode 100644 index 0000000..ddccb3e --- /dev/null +++ b/src/IL.hs @@ -0,0 +1,319 @@ +----------------------------------------------------------------------------- +-- | +-- Module : IL +-- Copyright : (c) Masahiro Sakai 2007-2009 +-- License : BSD3-style (see LICENSE) +-- +-- Maintainer: masahiro.sakai@gmail.com +-- Stability : experimental +-- Portability : non-portable + +{-# LANGUAGE CPP #-} +module IL + ( Type (..) + , renderType + , Op1 (..) + , Op2 (..) + , Binder (..) + , Expr (..) + , Scope (..) + , Name + , lambda + , forall + , exists + , int + , ext + , (<@>) + , abstract + , instantiate + , normalize + , renderExpr + , typeCheck + ) where + +import Control.Monad.RWS +import Data.List +import Data.Monoid +import Data.Function + +-- -------------------------------------------------------------------------- + +infixr 0 :-> + +data Type + = Prop + | E + | S Type + | (:->) Type Type + deriving (Eq, Ord) + +instance Show Type where +#ifdef USE_UTF8 + showsPrec = renderType True +#else + showsPrec = renderType False +#endif + +renderType :: Bool -> Int -> Type -> ShowS +renderType unicode = f + where + f _ Prop = showString "t" + f _ E = showString "e" + f d (S t) = showParen (d > 0) $ showString "s" . arr . f 0 t + f d (t1 :-> t2) = showParen (d > 0) $ f 1 t1 . arr . f 0 t2 + arr = if unicode then showString "→" else showString "->" + +-- -------------------------------------------------------------------------- + +infixl 9 :@ + +data Expr + = FVar Name -- 自由変数 + | BVar !Int -- 束縛変数 + | Expr :@ Expr -- 関数適用 + | Const Name -- 定数 (≒自由変数) + | Op1 !Op1 Expr -- 前置演算子 + | Op2 !Op2 Expr Expr -- 中置演算子 + | Bind !Binder Type Scope -- 変数束縛 + +data Op1 = Not | Box | F | H | Int | Ext deriving (Eq,Ord,Show) +data Op2 = And | Or | Imply | Equiv | Id deriving (Eq,Ord,Show) +data Binder = Lambda | Forall | Exists deriving (Eq,Ord,Show) + +newtype Scope = Sc Expr deriving Show +type Name = (String, Type) + +instance Show Expr where +#ifdef USE_UTF8 + showsPrec = renderExpr True False +#else + showsPrec = renderExpr False False +#endif + +lambda :: Name -> Expr -> Expr +lambda name expr = Bind Lambda (snd name) (abstract name expr) + +forall :: Name -> Expr -> Expr +forall name expr = Bind Forall (snd name) (abstract name expr) + +exists :: Name -> Expr -> Expr +exists name expr = Bind Exists (snd name) (abstract name expr) + +int :: Expr -> Expr +int = Op1 Int + +ext :: Expr -> Expr +ext = Op1 Ext + +-- 「a{b}」を「a <@> b」と表記 +infixl 9 <@> +(<@>) :: Expr -> Expr -> Expr +fun <@> arg = ext fun :@ arg + +varChange :: (Int -> Name -> Expr) -> (Int -> Int -> Expr) -> Expr -> Expr +varChange f g = h 0 + where + h :: Int -> Expr -> Expr + h outer (FVar name) = f outer name + h outer (BVar index) = g outer index + h outer (Bind q t (Sc body)) = Bind q t (Sc (h (outer+1) body)) + h outer (fun :@ arg) = h outer fun :@ h outer arg + h _ (Const s) = Const s + h outer (Op1 op a) = Op1 op (h outer a) + h outer (Op2 op a b) = Op2 op (h outer a) (h outer b) + +abstract :: Name -> Expr -> Scope +abstract name expr = Sc (varChange f g expr) + where + f outer name' | name==name' = BVar outer + | otherwise = FVar name' + g outer index | index>=outer = BVar (index+1) + | otherwise = BVar index + +instantiate :: Expr -> Scope -> Expr +instantiate image (Sc body) = varChange f g body + where + f _ name = FVar name + g outer index | index==outer = varShift outer image + | index>outer = BVar (index-1) + | otherwise = BVar index + +-- 外を指している変数のインデックスをずらす +varShift :: Int -> Expr -> Expr +varShift 0 = id +varShift n = varChange f g + where + f _ name = FVar name + g outer index | index>=outer = BVar (index+n) + | otherwise = BVar index + +normalize :: Expr -> Expr +normalize (Bind Lambda t (Sc body)) = + case normalize body of + f :@ BVar 0 | not (0 `elem` bvs f) -> varShift (-1) f -- η-conversion + body' -> Bind Lambda t (Sc body') +normalize (Bind q t (Sc body)) = Bind q t (Sc (normalize body)) +normalize (fun :@ arg) = + case normalize fun of + Bind Lambda t body -> normalize (instantiate arg' body) -- β-reduction + fun' -> fun' :@ arg' + where arg' = normalize arg +normalize (Op1 Ext a) = + case normalize a of + Op1 Int b -> b + a' -> Op1 Ext a' +normalize (Op1 op a) = Op1 op (normalize a) +normalize (Op2 op a b) = Op2 op (normalize a) (normalize b) +normalize x = x + +bvs :: Expr -> [Int] +bvs (FVar _) = [] +bvs (BVar n) = [n] +bvs (f :@ x) = bvs f ++ bvs x +bvs (Const _) = [] +bvs (Op1 _ e) = bvs e +bvs (Op2 _ e1 e2) = bvs e1 ++ bvs e2 +bvs (Bind _ _ (Sc e)) = [n - 1 | n <- bvs e, n /= 0] + +-- -------------------------------------------------------------------------- + +type RenderM = RWS [Name] () Int + +renderExpr :: Bool -> Bool -> Int -> Expr -> ShowS +renderExpr unicode uncurrying d e = + case runRWS (h d e) [] 0 of + (a, _, _) -> a + where + h d e = case e of + FVar name -> return $ showString (fst name) + BVar index -> do + vs <- ask + return $ showString $ fst (vs !! index) + Bind q _ _ -> f d q e + a :@ b | uncurrying -> f a [b] + where + f (e1 :@ e2) xs = f e1 (e2:xs) + f e xs = uncurriedApp e xs + Op1 Ext a :@ b -> do + a' <- h (app_prec+1) a + b' <- h 0 b + return $ showParen (d > app_prec) + $ a' . showString " {" . b' . showChar '}' + a :@ b -> do + a' <- h app_prec a + b' <- h (app_prec+1) b + return $ showParen (d > app_prec) $ a' . showChar ' ' . b' + Const s -> return $ showString (fst s) + Op1 op a -> do + t <- h (prec+1) a + return $ showParen (d > prec) + $ showString s . t + where + s = case op of + Not -> if unicode then "¬" else "not " -- ¬ (U+00AC) + Box -> if unicode then "◻" else "[]" -- ◻ (U+25FB) が正しそうだが □ (U+25A1) を使うのが無難か? + F -> "F " + H -> "H " + Int -> if unicode then "˄" else "Int " -- ˄ (U+02C4) + Ext -> if unicode then "˅" else "Ext " -- ˅ (U+02C5) + prec = case op of + Int | unicode -> app_prec + 1 + Ext | unicode -> app_prec + 1 + _ -> app_prec + Op2 op a b -> do + a' <- h (l prec) a + b' <- h (r prec) b + return $ showParen (d > prec) + $ a' . showChar ' ' . showString s . showChar ' ' . b' + where + (s,prec,l,r) = + case op of + And -> (if unicode then "∧" else "&&", 4, id, id) -- ∧ (U+2227) + Or -> (if unicode then "∨" else "||", 3, id, id) -- ∨ (U+2228) + Imply -> (if unicode then "→" else "->", 1, (+1), id) -- → (U+2192) + Equiv -> (if unicode then "↔" else "<->", 1, (+1), (+1)) -- ↔ (U+2194) + Id -> ("=", 5, (+1), (+1)) + + f :: Int -> Binder -> Expr -> RenderM ShowS + f d b e = do + (xs, s) <- go e + let b' = case b of + Lambda -> if unicode then "λ" else "\\" -- λ (U+03BB) + Forall -> if unicode then "∀" else "forall " -- ∀ (U+2200) + Exists -> if unicode then "∃" else "exists " -- ∃ (U+2203) + ys :: [(Type, [String])] + ys = [(snd (head ys), map fst ys) | ys <- groupBy ((==) `on` snd) xs] + ws :: [String] + ws = [intercalate ", " zs ++ " : "++ renderType unicode 0 t "" | (t, zs) <- ys] + return $ showParen (d > 0) $ + showString b' . showString (intercalate ", " ws) . showString ". " . s + where + go :: Expr -> RenderM ([Name], ShowS) + go (Bind b' t (Sc body)) | b==b' = do + x <- gensym t + (xs, s) <- local (x:) $ go body + return (x:xs, s) + go e = do + s <- h 0 e + return ([], s) + + uncurriedApp :: Expr -> [Expr] -> RenderM ShowS + uncurriedApp e xs = do + bs <- mapM (liftM Endo . h 0) $ reverse xs + let cs = appEndo $ mconcat $ intersperse (Endo (showString ", ")) bs + case e of + Op1 Ext e2 -> do + a <- h (app_prec+1) e2 + return $ showParen (d > app_prec) + $ a . showString "{" . cs . showChar '}' + _ -> do + a <- h (app_prec+1) e + return $ showParen (d > app_prec) + $ a . showString "(" . cs . showChar ')' + +app_prec :: Int +app_prec = 10 + +gensym :: Type -> RenderM Name +gensym t = do + i <- get + put (i+1) + return ("x"++show i, t) + +-- --------------------------------------------------------------------------- + +typeCheck ::[Type] -> Expr -> Maybe Type +typeCheck = f + where + f _ (FVar (_,t)) = return t + f env (BVar n) = return (env !! n) + f env (e1 :@ e2) = do + (t1 :-> t2) <- f env e1 + t3 <- f env e2 + guard $ t1 == t3 + return t2 + f env (Const (_,t)) = return t + f env (Op1 Ext e) = do + S t <- f env e + return t + f env (Op1 Int e) = do + t <- f env e + return (S t) + f env (Op1 op e) = do + Prop <- f env e + return Prop + f env (Op2 Id e1 e2) = do + t1 <- f env e1 + t2 <- f env e2 + guard $ t1 == t2 + return Prop + f env (Op2 op e1 e2) = do + Prop <- f env e1 + Prop <- f env e2 + return Prop + f env (Bind Lambda t (Sc e)) = do + t2 <- f (t:env) e + return (t :-> t2) + f env (Bind b t (Sc e)) = do + Prop <- f (t:env) e + return Prop diff --git a/src/MP.hs b/src/MP.hs new file mode 100644 index 0000000..7712338 --- /dev/null +++ b/src/MP.hs @@ -0,0 +1,50 @@ +----------------------------------------------------------------------------- +-- | +-- Module : MP +-- Copyright : (c) Masahiro Sakai 2007-2009 +-- License : BSD3-style (see LICENSE) +-- +-- Maintainer: masahiro.sakai@gmail.com +-- Stability : experimental +-- Portability : portable + +module MP + ( applyMP + ) + where +import P +import IL +import Translation (catToType) + +applyMP :: Expr -> Expr +-- MP1 +-- MP4 +applyMP (Const tv) | fst tv `elem` ["find","lose","eat","love"] = + lambda p $ lambda x $ + FVar p <@> (int $ lambda y $ int (Const tv') <@> FVar y :@ FVar x) + where + tv' = (fst tv ++ "*", E :-> E :-> Prop) + p = ("p", S ((S (E :-> Prop)) :-> Prop)) + x = ("x", E) + y = ("y", E) +-- MP8 +applyMP (Const ("in",_)) = + lambda p $ lambda pp $ lambda x $ + FVar p <@> (int $ lambda y $ int (Const in') <@> FVar y :@ FVar pp :@ FVar x) + where + in' = ("in*", E :-> (S (E :-> Prop)) :-> E :-> Prop) + p = ("p", S ((S (E :-> Prop)) :-> Prop)) + pp = ("P", S (E :-> Prop)) + x = ("x", E) + y = ("y", E) +-- MP9 +applyMP (Const ("seek",_)) = lambda p $ Const try' :@ int (find' :@ FVar p) + where + try' = ("try", catToType (IV :// IV)) + find' = applyMP (Const ("find", catToType (cat :: Cat TV))) + p = ("P", S ((S (E :-> Prop)) :-> Prop)) +applyMP (Bind q t (Sc body)) = Bind q t (Sc (applyMP body)) +applyMP (fun :@ arg) = applyMP fun :@ applyMP arg +applyMP (Op1 op a) = Op1 op (applyMP a) +applyMP (Op2 op a b) = Op2 op (applyMP a) (applyMP b) +applyMP x = x diff --git a/src/Main.hs b/src/Main.hs new file mode 100644 index 0000000..6cfe128 --- /dev/null +++ b/src/Main.hs @@ -0,0 +1,44 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Main +-- Copyright : (c) Masahiro Sakai 2007-2009 +-- License : BSD3-style (see LICENSE) +-- +-- Maintainer: masahiro.sakai@gmail.com +-- Stability : experimental +-- Portability : non-portable + +{-# LANGUAGE CPP #-} +module Main where +import Report +import Version +#ifdef USE_UTF8 +import Prelude hiding (putStr, putStrLn, getLine) +import System.IO (stdout, hSetBuffering, BufferMode (..)) +import System.IO.UTF8 +#else +import System.IO +#endif + +main :: IO () +main = do + putStrLn banner + hSetBuffering stdout NoBuffering + loop + +banner :: String +banner = unlines + [ "PTQ version " ++ versionStr + , "" + , "Type :quit to quit" + ] + +loop :: IO () +loop = do + putStr "PTQ> " + s <- getLine + case s of + ":quit" -> return () + _ -> do + putStr (report s) + loop diff --git a/src/P.hs b/src/P.hs new file mode 100644 index 0000000..e7ad3b0 --- /dev/null +++ b/src/P.hs @@ -0,0 +1,213 @@ +----------------------------------------------------------------------------- +-- | +-- Module : P +-- Copyright : (c) Masahiro Sakai 2007-2009 +-- License : BSD3-style (see LICENSE) +-- +-- Maintainer: masahiro.sakai@gmail.com +-- Stability : experimental +-- Portability : non-portable + +{-# LANGUAGE TypeOperators, GADTs, EmptyDataDecls, MultiParamTypeClasses + , TypeSynonymInstances #-} + +module P + ( Sen + , IV + , CN + , Adj + , (:/) + , (://) + , Cat (..) + , CatType (..) + , T + , TV + , IAV + , Det + , DTV + , TTV + , PP + , PronounNo + , P (..) + , PAny (..) + , F5 + , F6 + , F8 + , F9 + , F10 + , catOf + ) where + +----------------------------------------------------------------------------- + +infixl 1 :/ +infixl 1 :// + +-- 型レベルでの範疇の表現 +data Sen -- 文。本来はtと書かれるけど小文字が使えないので +data IV -- 動詞句, 自動詞: walk +data CN -- 普通名詞(句): man +data Adj -- 形容詞? (定義が載っていなかった) +data (:/) a b +data (://) a b + +-- 範疇を型レベルだけでなく値レベルでも表現 +data Cat a where + Sen :: Cat Sen + IV :: Cat IV + CN :: Cat CN + Adj :: Cat Adj + (:/) :: Cat a -> Cat b -> Cat (a :/ b) + (://) :: Cat a -> Cat b -> Cat (a :// b) + +class CatType a where + cat :: Cat a +instance CatType Sen where + cat = Sen +instance CatType IV where + cat = IV +instance CatType CN where + cat = CN +instance CatType Adj where + cat = Adj +instance (CatType a, CatType b) => CatType (a :/ b) where + cat = cat :/ cat +instance (CatType a, CatType b) => CatType (a :// b) where + cat = cat :// cat + +instance Show (Cat a) where + showsPrec _ Sen = showString "t" + showsPrec _ IV = showString "IV" + showsPrec _ CN = showString "CN" + showsPrec _ Adj = showString "Adj" + showsPrec d (a :/ b) = showParen (d > 0) $ showsPrec 1 a . showString " / " . showsPrec 1 b + showsPrec d (a :// b) = showParen (d > 0) $ showsPrec 1 a . showString " // " . showsPrec 1 b + +type T = Sen :/ IV -- 名詞句, 固有名詞: John, he +type TV = IV :/ T -- 他動詞(句): find +type IAV = IV :/ IV -- 動詞句修飾の副詞(句): slowly + +-- FIXME: 定義が載っていなかった範疇 +type Det = T :/ CN -- 冠詞 +type DTV = TV :/ T -- ditransitive verb : 名詞句を２つ取る他動詞 +type TTV = TV :/ T -- to transitive verb : DTVと名詞句の順序が逆? +type PP = IV :/ TV -- prepositional phrase?: by John + +----------------------------------------------------------------------------- + +type PronounNo = Int + +-- 範疇がcである表現 +data P c where + -- 基本表現 + B :: Cat c -> String -> P c + He :: PronounNo -> P T + + -- 統語規則 + -- F1はないのね + F2 :: P Det -> P CN -> P T + F3 :: PronounNo -> P CN -> P Sen -> P CN + F4 :: P T -> P IV -> P Sen + F5 :: F5 c => P (c :/ T) -> P T -> P c + F6 :: F6 c a => P (c :/ a) -> P a -> P c + F7 :: P IAV -> P IV -> P IV + F8 :: F8 c => P c -> P c -> P c -- and + F9 :: F9 c => P c -> P c -> P c -- or + F10 :: F10 c => PronounNo -> P T -> P c -> P c -- 文の中への量化 + F11 :: P T -> P IV -> P Sen + F12 :: P T -> P IV -> P Sen + F13 :: P T -> P IV -> P Sen + F14 :: P T -> P IV -> P Sen + F15 :: P T -> P IV -> P Sen + F16 :: P (IV :/ Sen) -> P Sen -> P IV + F17 :: P (IV :// IV) -> P IV -> P IV + -- F18はないのね + F19 :: P TV -> P IV + F20 :: P DTV -> P T -> P TV + F21 :: P DTV -> P T -> P TV + F22 :: P DTV -> P TTV + F23 :: P PP -> P TV -> P IV + F24 :: P (PP :/ T) -> P T -> P PP + F25 :: P TV -> P Adj + +data PAny where + PAny :: CatType c => P c -> PAny + +class CatType c => F5 c +instance F5 IV -- T5 +instance F5 IAV -- T6 + +class (CatType c, CatType a) => F6 c a +instance F6 Sen Sen -- T9 +instance F6 IV Adj -- T18 + +class CatType c => F8 c +instance F8 Sen +instance F8 IV + +class CatType c => F9 c +instance F9 Sen +instance F9 IV +instance F9 T + +class CatType c => F10 c +instance F10 Sen +instance F10 CN +instance F10 IV + +catOf :: CatType c => P c -> Cat c +catOf _ = cat + +----------------------------------------------------------------------------- + +-- Ughhh!! +instance Show (P c) where + showsPrec _ (B _ s) = showString s + showsPrec d (He n) = c1 d "He" n + showsPrec d (F2 x y) = c2 d "F2" x y + showsPrec d (F3 n x y) = c3 d "F3" n x y + showsPrec d (F4 x y) = c2 d "F4" x y + showsPrec d (F5 x y) = c2 d "F5" x y + showsPrec d (F6 x y) = c2 d "F6" x y + showsPrec d (F7 x y) = c2 d "F7" x y + showsPrec d (F8 x y) = c2 d "F8" x y + showsPrec d (F9 x y) = c2 d "F9" x y + showsPrec d (F10 n x y) = c3 d "F10" n x y + showsPrec d (F11 x y) = c2 d "F11" x y + showsPrec d (F12 x y) = c2 d "F12" x y + showsPrec d (F13 x y) = c2 d "F13" x y + showsPrec d (F14 x y) = c2 d "F14" x y + showsPrec d (F15 x y) = c2 d "F15" x y + showsPrec d (F16 x y) = c2 d "F16" x y + showsPrec d (F17 x y) = c2 d "F17" x y + showsPrec d (F19 x) = c1 d "F19" x + showsPrec d (F20 x y) = c2 d "F20" x y + showsPrec d (F21 x y) = c2 d "F21" x y + showsPrec d (F22 x) = c1 d "F22" x + showsPrec d (F23 x y) = c2 d "F23" x y + showsPrec d (F24 x y) = c2 d "F24" x y + showsPrec d (F25 x) = c1 d "F25" x + +instance Show PAny where + showsPrec d (PAny p) = c1 d "PAny" p + +c1 :: (Show x) => Int -> String -> x -> ShowS +c1 d con x = + showParen (d > app_prec) $ + showString con + . showChar ' ' . showsPrec (app_prec+1) x +c2 :: (Show x, Show y) => Int -> String -> x -> y -> ShowS +c2 d con x y = + showParen (d > app_prec) $ + showString con + . showChar ' ' . showsPrec (app_prec+1) x + . showChar ' ' . showsPrec (app_prec+1) y +c3 :: (Show x, Show y, Show z) => Int -> String -> x -> y -> z -> ShowS +c3 d con x y z = + showParen (d > app_prec) $ + showString con + . showChar ' ' . showsPrec (app_prec+1) x + . showChar ' ' . showsPrec (app_prec+1) y + . showChar ' ' . showsPrec (app_prec+1) z +app_prec :: Int +app_prec = 10 diff --git a/src/PDict.hs b/src/PDict.hs new file mode 100644 index 0000000..1db3c1a --- /dev/null +++ b/src/PDict.hs @@ -0,0 +1,79 @@ +----------------------------------------------------------------------------- +-- | +-- Module : PDict +-- Copyright : (c) Masahiro Sakai 2007-2009 +-- License : BSD3-style (see LICENSE) +-- +-- Maintainer: masahiro.sakai@gmail.com +-- Stability : experimental +-- Portability : portable + +module PDict where + +import P + +----------------------------------------------------------------------------- + +john, mary, bill, ninety :: P T +john = B cat_T "john" +mary = B cat_T "mary" +bill = B cat_T "bill" +ninety = B cat_T "ninety" + +run, walk, talk, rise, change :: P IV +run = B cat_IV "run" +walk = B cat_IV "walk" +talk = B cat_IV "talk" +rise = B cat_IV "rise" +change = B cat_IV "change" + +find, lose, eat, love, date, seek, coneiveg :: P TV +find = B cat_TV "find" +lose = B cat_TV "lose" +eat = B cat_TV "eat" +love = B cat_TV "love" +date = B cat_TV "date" +seek = B cat_TV "seek" +coneiveg = B cat_TV "coneiveg" + +man, woman, park, fish, pen, unicorn, price, temperature :: P CN +man = B cat_CN "man" +woman = B cat_CN "woman" +park = B cat_CN "park" +fish = B cat_CN "fish" +pen = B cat_CN "pen" +unicorn = B cat_CN "unicorn" +price = B cat_CN "price" +temperature = B cat_CN "temperature" + +slowly :: P IAV +slowly = B cat_IAV "slowly" + +believe, assert :: P (IV :/ Sen) +believe = B (cat_IV :/ cat_Sen) "beleave" +assert = B (cat_IV :/ cat_Sen) "assert" + +asleep :: P Adj +asleep = B cat_Adj "asleep" + +try', wish :: P (IV :// IV) +try' = B (cat_IV :// cat_IV) "try" +wish = B (cat_IV :// cat_IV) "wish" + +in', about :: P (IAV :/ T) +in' = B (cat_IAV :/ cat_T) "in" +about = B (cat_IAV :/ cat_T) "about" + +a, every :: P Det +a = B cat_Det "a" +every = B cat_Det "every" + +necessarily :: P (Sen :/ Sen) +necessarily = B (cat_Sen :/ cat_Sen) "necessarily" + +class Be c where + be :: P c +instance Be TV where + be = B cat_TV "be" +instance Be (IV :/ Adj) where + be = B (cat_IV :/ cat_Adj) "be" diff --git a/src/Parser.hs b/src/Parser.hs new file mode 100644 index 0000000..089374c --- /dev/null +++ b/src/Parser.hs @@ -0,0 +1,723 @@ +---------------------------------------------------------------------------- +-- | +-- Module : Parser +-- Copyright : (c) Masahiro Sakai 2007-2009 +-- License : BSD3-style (see LICENSE) +-- +-- Maintainer: masahiro.sakai@gmail.com +-- Stability : experimental +-- Portability : non-portable + +{-# LANGUAGE TypeOperators #-} +module Parser (parse, parseAny) where + +import Data.Char +import Control.Monad +import qualified Data.IntSet as IS + +import P + +----------------------------------------------------------------------------- +-- パーサのコア部分 + +type Token = String + +newtype Parser a + = Parser + { runParser :: Env -> State -> [Token] -> [(a, State, [Token])] + } + +instance Monad Parser where + return x = Parser $ \_ s ts -> [(x,s,ts)] + m >>= f = Parser $ \env s ts -> + do (v,s',ts') <- runParser m env s ts + runParser (f v) env s' ts' + +instance MonadPlus Parser where + mzero = Parser $ \_ _ _ -> [] + mplus x y = Parser $ \env s ts -> + runParser x env s ts ++ runParser y env s ts + +infixr 0 <|> +(<|>) :: Parser a -> Parser a -> Parser a +(<|>) = mplus + +anyToken :: Parser Token +anyToken = Parser g + where g _ _ [] = [] + g _ s (t:ts) = [(t, s, ts)] + +lookAhead :: Parser Token +lookAhead = Parser g + where g _ _ [] = [] + g _ s (t:ts) = [(t, s, t:ts)] + +----------------------------------------------------------------------------- +-- 環境 + +data Env + = Env + { s3env :: S3Env + } + +initialEnv :: Env +initialEnv = Env{ s3env = initialS3Env } + +local :: (Env -> Env) -> Parser a -> Parser a +local f (Parser g) = Parser g' + where g' env s ts = g (f env) s ts + +ask :: Parser Env +ask = Parser g + where g env s ts = [(env,s,ts)] + +----------------------------------------------------------------------------- +-- 状態 + +data State + = State + { gensymState :: PronounNo + , f10State :: F10State + } +initialState :: State +initialState = State{ gensymState = 0, f10State = initialF10State } + +get :: Parser State +get = Parser g + where g _ s xs = [(s,s,xs)] + +put :: State -> Parser () +put s = Parser g + where g _ _ xs = [((),s,xs)] + +----------------------------------------------------------------------------- +-- S3Env + +type S3Env = [(PronounNo,Gender)] -- S3規則で使うためのデータ +initialS3Env :: S3Env +initialS3Env = [] + +localS3 :: (S3Env -> S3Env) -> Parser a -> Parser a +localS3 f = local (\env@Env{ s3env = x } -> env{ s3env = f x }) + +askS3 :: Parser S3Env +askS3 = liftM s3env ask + +----------------------------------------------------------------------------- +-- Counter + +gensym :: Parser PronounNo +gensym = + do s@State{ gensymState = i } <- get + put s{ gensymState = i+1 } + return i + +----------------------------------------------------------------------------- +-- F10のための処理 + +-- DVarStateみたいな名前にした方が良いか +type F10Entry = (PronounNo, Gender, P T, IS.IntSet) +type F10State = [F10Entry] -- F10で使うためのデータ +initialF10State :: F10State +initialF10State = [] + +getF10State :: Parser F10State +getF10State = + do State{ f10State = s } <- get + return s + +putF10State :: F10State -> Parser () +putF10State s = + do x <- get + put x{ f10State = s } + +asPronoun :: Gender -> P T -> Parser (P T) +asPronoun g t = + do n <- gensym + s <- getF10State + putF10State ((n,g,t,fvs t) : s) + return (He n) + +mayF10s :: F10 c => Parser (P c) -> Parser (P c) +mayF10s p = liftM fst $ mayF10s' $ p >>= \x -> return (x,()) + +mayF10s' :: F10 c => Parser (P c, a) -> Parser (P c, a) +mayF10s' p = + do s <- getF10State + putF10State [] + (x,a) <- localS3 ([(n,g) | (n,g,_,_)<-s]++) p + x' <- introF10s x + s' <- getF10State + putF10State (s'++s) + return (x',a) + +introF10 :: F10 c => P c -> Parser (P c) +introF10 x = + do (n, _, alpha, _) <- takeF10Entry + return (F10 n alpha x) + +introF10s :: F10 c => P c -> Parser (P c) +introF10s x = (introF10 x >>= introF10s) <|> return x + +-- F10に変換可能なエントリを取り出す +takeF10Entry :: Parser F10Entry +takeF10Entry = + do s <- getF10State + (e@(n,_,_,_), s') <- msum $ map return $ pick s + noDanglingRef n + putF10State s' + return e + +pick :: [a] -> [(a,[a])] +pick [] = [] +pick (x:xs) = (x,xs) : [(y,x:ys) | (y,ys) <- pick xs] + +-- nへの参照が残っていないことを保障 +noDanglingRef :: PronounNo -> Parser () +noDanglingRef n = + do s <- getF10State + guard $ and [not (IS.member n vs) | (_,_,_,vs) <- s] + +----------------------------------------------------------------------------- +-- パーサのユーティリティ + +token :: Token -> Parser Token +token x = + do y <- anyToken + guard $ x==y + return y + +many, many1 :: Parser a -> Parser [a] +many p = many1 p <|> return [] +many1 p = + do x <- p + xs <- many p + return (x:xs) + +chainr1 :: Parser a -> Parser (a->a->a) -> Parser a +chainr1 p q = + do x <- p + f <- do{ op <- q; y <- chainr1 p q; return (`op` y) } <|> return id + return (f x) + +----------------------------------------------------------------------------- +-- API + +parse :: String -> [P Sen] +parse = parse' p_t + +parseAny :: String -> [PAny] +parseAny s = concat $ + [ f p_Det, f (liftM fst p_CN), f p_IAV_T, f p_t_t, f p_t, f p_Adj, f p_PP + , f p_IAV, f p_PP_T, f (p_T [Subject, Object]) ] ++ + [ concat [ f (p_IV x), f (p_TV x), f (p_IV__IV x), f (p_DTV x), f (p_IV_t x) + , f (p_IV_Adj x)] | x <- vfs ] + where + f :: CatType a => Parser (P a) -> [PAny] + f p = map PAny (parse' p s) + vfs :: [VerbForm] + vfs = [VFOrig, VFPastParticiple] ++ [f True | f <- [VFPresent, VFFuture, VFPerfect]] + -- 否定形の動詞それ自体はPで表現できないのでパース出来ない + +parse' :: Parser (P a) -> String -> [P a] +parse' p s = [x | (x, State{ f10State = [] }, []) <- runParser p initialEnv initialState ts] + where ts = tokenize s + +tokenize :: String -> [Token] +tokenize = expandAbbr . words . map toLower . filter ('.'/=) + +expandAbbr :: [String] -> [String] +expandAbbr = concatMap f + where f "doesn't" = ["does", "not"] + f "won't" = ["will", "not"] + f "hasn't" = ["has", "not"] + f "isn't" = ["is", "not"] + f x = [x] + +----------------------------------------------------------------------------- +-- 各範疇のパーサ + +p_Det :: Parser (P Det) +p_Det = + do x@(B _ s) <- s1_Det + let x' = if s=="an" then B (cat :: Cat Det) "a" else x -- XXX + -- FIXME: anの場合には次の語が母音で始まるかチェック + return $ x' + +p_CN :: Parser (P CN, Gender) +p_CN = mayF10s' $ -- S15 + do (zeta,g) <- s1_CN + zeta <- s3s g zeta + return (zeta,g) + +-- FIXME: 全ての組み合わせを網羅している? +p_T :: [Case] -> Parser (P T) +p_T cs = chainr1 (p <|> he_n cs) f9 -- S13 + where p = do (x,g) <- s1_T <|> s2 + return x <|> asPronoun g x + +-- He_n +he_n :: [Case] -> Parser (P T) +he_n cs = + do g <- mplus + (if Subject `elem` cs + then msum [ token "he" >> return Masculine + , token "she" >> return Feminine + , token "it" >> return Neuter + ] + else mzero) + (if Object `elem` cs + then msum [ token "him" >> return Masculine + , token "her" >> return Feminine + , token "it" >> return Neuter + ] + else mzero) + xs <- getF10State + ys <- askS3 + let ns = [(n,g') | (n, g', _, _) <- xs] ++ ys + msum [ return (He n) | (n,g') <- ns, g==g' ] + +-- FIXME: 全ての組み合わせを網羅している? +p_IV :: VerbForm -> Parser (P IV) +p_IV vf = mayF10s q -- S16 + where p = do x <- s1_IV vf + <|> s5 vf + <|> s7 vf + <|> s8 vf + <|> s18 vf + <|> s19 vf + <|> s23 vf + liftM (foldl (flip F7) x) (many p_IAV) -- S10 + q = chainr1 p (f8 <|> f9) -- S12a, S12b + +p_TV :: VerbForm -> Parser (P TV) +p_TV vf = s1_TV vf <|> s20 vf <|> s21 vf + +p_IAV_T :: Parser (P (IAV :/ T)) +p_IAV_T = s1_IAV_T + +p_IV__IV :: VerbForm -> Parser (P (IV :// IV)) +p_IV__IV = s1_IV__IV + +p_t_t :: Parser (P (Sen :/ Sen)) +p_t_t = s1_t_t + +-- FIXME: 全ての組み合わせを網羅している? +p_t :: Parser (P Sen) +p_t = mayF10s $ -- S14 + chainr1 (s9 <|> s4_or_s17) (f8 <|> f9) -- S11a, S11b + +p_IV_t :: VerbForm -> Parser (P (IV :/ Sen)) +p_IV_t = s1_IV_t + +p_IV_Adj :: VerbForm -> Parser (P (IV :/ Adj)) +p_IV_Adj vf = s1_IV_Adj vf + +p_Adj :: Parser (P Adj) +p_Adj = s1_Adj <|> s25 + +-- FIXME +p_DTV :: VerbForm -> Parser (P DTV) +p_DTV vf = mzero -- ??? + +p_PP :: Parser (P PP) +p_PP = s24 + +p_IAV :: Parser (P IAV) +p_IAV = s1_IAV <|> s6 + +p_PP_T :: Parser (P (PP :/ T)) +p_PP_T = s1_PP_T + +----------------------------------------------------------------------------- +-- 動詞の辞書 + +-- (原形, 三人称単数現在形, 過去分詞) +type VerbEntry = (String, String, String) + +verb_be :: VerbEntry +verb_be = ("be", "is", "been") + +{-# INLINE regularVerb #-} +regularVerb :: String -> VerbEntry +regularVerb s = (s, present, past_participle) + where + rs = reverse s + present = + case rs of + 's':'s':_ -> s ++ "es" + 'h':'c':_ -> s ++ "es" + 'h':'s':_ -> s ++ "es" + 'x':_ -> s ++ "es" + 'y':s' -> reverse s' ++ "ies" + _ -> s ++ "s" + past_participle = + case rs of + 'e':_ -> s ++ "d" + 'y':s' -> reverse s' ++ "ied" + _ -> s ++ "ed" + +dict_IV :: [VerbEntry] +dict_IV = + [ regularVerb "walk" + , regularVerb "talk" + , regularVerb "change" + , ("run", "runs", "ran") + , ("rise", "rises", "rosen") + ] + +dict_TV :: [VerbEntry] +dict_TV = + [ ("find", "finds", "found") + , ("lose", "loses", "lost") + , ("eat", "eats", "eaten") + , ("seek", "seeks", "sought") + , regularVerb "love" + , regularVerb "date" + --, "coneive" -- FIXME: conceiveの間違い? + , verb_be + ] + +dict_IV_t :: [VerbEntry] +dict_IV_t = + [ regularVerb "believe" + , regularVerb "assert" + ] + +dict_IV__IV :: [VerbEntry] +dict_IV__IV = + [ regularVerb "try" + , regularVerb "wish" + ] + +dict_IV_Adj :: [VerbEntry] +dict_IV_Adj = [verb_be] + +-- DTVをTTVに変換することは出来るから、giveの範疇はDTVだろうな。多分。 +dict_DTV :: [VerbEntry] +dict_DTV = + [ ("give", "gives", "given") + ] + +----------------------------------------------------------------------------- +-- 動詞のパーサ + +data VerbForm + = VFOrig -- 原形 + | VFPastParticiple -- 過去分詞 + | VFPresent !Bool -- 三人称単数現在形とその否定形 + | VFFuture !Bool -- 三人称単数未来系とその否定形 + | VFPerfect !Bool -- 三人称単数現在完了系とその否定形 + +{-# INLINE verbParser #-} +verbParser :: CatType c => [VerbEntry] -> VerbForm -> Parser (P c) +verbParser dict vf = + do s <- verbParser' dict vf + return (B cat s) + +-- FIXME: 後で整理する +{-# INLINE verbParser' #-} +verbParser' :: [VerbEntry] -> VerbForm -> Parser String +verbParser' dict (VFPresent False) = + mplus (do token "does" + token "not" + x <- verbParser' dict VFOrig + guard (x/="be") + return x) + (do x <- verbParser' dict (VFPresent True) + guard (x=="be") + token "not" + return x) +verbParser' dict (VFFuture b) = + do token "will" + unless b $ token "not" >> return () + verbParser' dict VFOrig +verbParser' dict (VFPerfect b) = + do token "has" + unless b $ token "not" >> return () + verbParser' dict VFPastParticiple +verbParser' dict vf = + do x <- anyToken + msum [ return o + | (o, present, pastparticiple) <- dict + , case vf of + VFOrig -> o==x + VFPastParticiple -> pastparticiple==x + VFPresent True -> present==x + _ -> False -- shouldn't happen + ] + +----------------------------------------------------------------------------- +-- 名詞の辞書とパーサ + +data Case = Subject | Object deriving (Show,Eq,Ord) + +data Gender = Masculine | Feminine | Neuter deriving (Show,Eq,Ord) +type NounEntry = (String, Gender) + +dict_T :: [NounEntry] +dict_T = + [ ("john" , Masculine) + , ("mary" , Feminine) + , ("bill" , Masculine) + , ("ninety" , Neuter) + ] + +dict_CN :: [NounEntry] +dict_CN = + [ ("man" , Masculine) + , ("woman" , Feminine) + , ("park" , Neuter) + , ("fish" , Neuter) + , ("pen" , Neuter) + , ("unicorn" , Neuter) + , ("price" , Neuter) + , ("temperature" , Neuter) + ] + +{-# INLINE nounParser #-} +nounParser :: CatType c => [NounEntry] -> Parser (P c, Gender) +nounParser dict = + do x <- anyToken + case lookup x dict of + Nothing -> mzero + Just g -> return (B cat x, g) + +----------------------------------------------------------------------------- +-- それ以外の基本表現の辞書とパーサ + +dict_IAV :: [String] +dict_IAV = + [ "rapidly" + , "slowly" + , "voluntarily" + , "allegedly" + ] + +dict_t_t :: [String] +dict_t_t = ["necessarily"] + +dict_IAV_T :: [String] +dict_IAV_T = ["in", "about"] + +dict_Adj :: [String] +dict_Adj = ["asleep"] + +dict_Det :: [String] +dict_Det = ["a", "an", "the", "every", "no"] + +dict_PP_T :: [String] +dict_PP_T = ["by"] + +{-# INLINE dictParser #-} +dictParser :: CatType c => [String] -> Parser (P c) +dictParser dict = + do x <- anyToken + guard $ x `elem` dict + return $ B cat x + +----------------------------------------------------------------------------- +-- 各統語規則のパーサ + +s1_IV :: VerbForm -> Parser (P IV) +s1_IV = verbParser dict_IV + +s1_TV :: VerbForm -> Parser (P TV) +s1_TV = verbParser dict_TV + +s1_IV_t :: VerbForm -> Parser (P (IV :/ Sen)) +s1_IV_t = verbParser dict_IV_t + +s1_IV__IV :: VerbForm -> Parser (P (IV :// IV)) +s1_IV__IV = verbParser dict_IV__IV + +s1_IV_Adj :: VerbForm -> Parser (P (IV :/ Adj)) +s1_IV_Adj = verbParser dict_IV_Adj + +s1_T :: Parser (P T, Gender) +s1_T = nounParser dict_T + +s1_CN :: Parser (P CN, Gender) +s1_CN = nounParser dict_CN + +s1_IAV :: Parser (P IAV) +s1_IAV = dictParser dict_IAV + +s1_t_t :: Parser (P (Sen :/ Sen)) +s1_t_t = dictParser dict_t_t + +s1_IAV_T :: Parser (P (IAV :/ T)) +s1_IAV_T = dictParser dict_IAV_T + +s1_Adj :: Parser (P Adj) +s1_Adj = dictParser dict_Adj + +s1_Det :: Parser (P Det) +s1_Det = dictParser dict_Det + +s1_PP_T :: Parser (P (PP :/ T)) +s1_PP_T = dictParser dict_PP_T + +s2 :: Parser (P T, Gender) +s2 = + do delta <- p_Det + -- w <- lookAhead + (zeta,g) <- p_CN + return (F2 delta zeta, g) + +s3s :: Gender -> P CN -> Parser (P CN) +s3s g zeta = (s3_postfix g zeta >>= s3s g) <|> return zeta + +s3_postfix :: Gender -> P CN -> Parser (P CN) +s3_postfix g zeta = + do token "such" + token "that" + n <- gensym + phi <- localS3 ((n,g):) p_t + guard $ IS.member n (fvs phi) -- XXX: He n が現れていることを検査。 + noDanglingRef n -- nを参照している参照が残っていないことを保障 + return (F3 n zeta phi) + +s4_or_s17 :: Parser (P Sen) +s4_or_s17 = + do alpha <- p_T [Subject] + msum [ do delta <- p_IV (VFPresent True) + return (F4 alpha delta) -- 三人称単数現在形 (S4) + , do delta <- p_IV (VFPresent False) + return (F11 alpha delta) -- 三人称単数現在の否定形 (S17) + , do delta <- p_IV (VFFuture True) + return (F12 alpha delta) -- 三人称単数未来形 (S17) + , do delta <- p_IV (VFFuture False) + return (F13 alpha delta) -- 三人称単数未来の否定形 (S17) + , do delta <- p_IV (VFPerfect True) + return (F14 alpha delta) -- 三人称単数現在完了形 (S17) + , do delta <- p_IV (VFPerfect False) + return (F15 alpha delta) -- 三人称単数現在完了の否定形 (S17) + ] + +s5 :: VerbForm -> Parser (P IV) +s5 vf = + do delta <- p_TV vf + beta <- p_T [Object] + return (F5 delta beta) + +s6 :: Parser (P IAV) +s6 = + do delta <- p_IAV_T + beta <- p_T [Object] + return (F5 delta beta) + +s7 :: VerbForm -> Parser (P IV) +s7 vf = + do delta <- p_IV_t vf + token "that" + phi <- p_t + return (F16 delta phi) + +s8 :: VerbForm -> Parser (P IV) +s8 vf = + do delta <- p_IV__IV vf + token "to" + beta <- p_IV VFOrig + return (F17 delta beta) + +s9 :: Parser (P Sen) +s9 = + do delta <- p_t_t + beta <- p_t + return (F6 delta beta) + +-- S10 は他のパーサの中に組み込んでしまっている +-- S11a, S11b, S12a, S12b, S13 は他のパーサの中に組み込んでしまっている +-- S14, S15, S16 は他のパーサの中に組み込んでしまっている + +f8 :: F8 c => Parser (P c -> P c -> P c) +f8 = token "and" >> return F8 + +f9 :: F9 c => Parser (P c -> P c -> P c) +f9 = token "or" >> return F9 + +-- S17はS4のパーサの中に組み込んでしまっている + +-- 講義資料でF9と書いてある??? +s18 :: VerbForm -> Parser (P IV) +s18 vf = + do alpha <- p_IV_Adj vf + beta <- p_Adj + return (F6 alpha beta) + +s19 :: VerbForm -> Parser (P IV) +s19 vf = liftM F19 (p_TV vf) + +-- FIXME: S20とS21のどちらかはTTVでは? +-- S20の方か? + +-- ???: x が DTV ならば、x to him は TV +s20 :: VerbForm -> Parser (P TV) +s20 vf = + do delta <- p_DTV vf + token "to" + beta <- p_T [Object] + return (F20 delta beta) + +s21 :: VerbForm -> Parser (P TV) +s21 vf = + do delta <- p_DTV vf + beta <- p_T [Object] + return (F21 delta beta) + +-- FIXME: この規則はどこからも使われていないけど良いのだろうか? +s22 :: VerbForm -> Parser (P TTV) +s22 vf = liftM F22 (p_DTV vf) + +-- FIXME: αが-enならばというのは何を指している? +-- δ が been, rosen, eaten であること? +s23 :: VerbForm -> Parser (P IV) +s23 vf = + do verbParser' [verb_be] vf + delta <- p_TV VFPastParticiple + alpha <- p_PP + return (F23 alpha delta) + +-- FIXME: αが-enならばというのは何を指している? +-- β≠he_n の間違いか? +s24 :: Parser (P PP) +s24 = + do alpha <- p_PP_T + beta <- p_T [Object] + return (F24 alpha beta) + +s25 :: Parser (P Adj) +s25 = + do delta <- p_TV VFPastParticiple + return (F25 delta) + +----------------------------------------------------------------------------- + +-- He n で表される「自由変数」の集合 +fvs :: P c -> IS.IntSet +fvs (B _ _) = IS.empty +fvs (He n) = IS.singleton n +fvs (F2 x y) = IS.union (fvs x) (fvs y) +fvs (F3 n x y) = IS.delete n $ IS.union (fvs x) (fvs y) +fvs (F4 x y) = IS.union (fvs x) (fvs y) +fvs (F5 x y) = IS.union (fvs x) (fvs y) +fvs (F6 x y) = IS.union (fvs x) (fvs y) +fvs (F7 x y) = IS.union (fvs x) (fvs y) +fvs (F8 x y) = IS.union (fvs x) (fvs y) +fvs (F9 x y) = IS.union (fvs x) (fvs y) +fvs (F10 n x y) = IS.delete n $ IS.union (fvs x) (fvs y) +fvs (F11 x y) = IS.union (fvs x) (fvs y) +fvs (F12 x y) = IS.union (fvs x) (fvs y) +fvs (F13 x y) = IS.union (fvs x) (fvs y) +fvs (F14 x y) = IS.union (fvs x) (fvs y) +fvs (F15 x y) = IS.union (fvs x) (fvs y) +fvs (F16 x y) = IS.union (fvs x) (fvs y) +fvs (F17 x y) = IS.union (fvs x) (fvs y) +fvs (F19 x) = fvs x +fvs (F20 x y) = IS.union (fvs x) (fvs y) +fvs (F21 x y) = IS.union (fvs x) (fvs y) +fvs (F22 x) = fvs x +fvs (F23 x y) = IS.union (fvs x) (fvs y) +fvs (F24 x y) = IS.union (fvs x) (fvs y) +fvs (F25 x) = fvs x diff --git a/src/ParserTest.hs b/src/ParserTest.hs new file mode 100644 index 0000000..788df14 --- /dev/null +++ b/src/ParserTest.hs @@ -0,0 +1,37 @@ +----------------------------------------------------------------------------- +-- | +-- Module : PTest +-- Copyright : (c) Masahiro Sakai 2007-2009 +-- License : BSD3-style (see LICENSE) +-- +-- Maintainer: masahiro.sakai@gmail.com +-- Stability : experimental +-- Portability : non-portable + +import Report + +test :: String -> IO () +test = putStr . report + +----------------------------------------------------------------------------- + +ex4_1 = "John seeks a unicorn." +-- ex4_2 +ex4_3 = "John finds a unicorn." +ex4_4 = "Necessarily John walks." +ex4_5 = "John is Bill." +ex4_6 = "John is a unicorn." + +ex_1 = "John believes that a unicorn talks." +ex_2 = "Every woman loves a unicorn." +ex_3 = "Every woman loves John." +ex_4 = "A unicorn walks and it talks." +ex_5 = "Every unicorn such that it walks talks." +ex_6 = "John walks slowly." +ex_7 = "John walks in a park." +ex_8 = "John wishes to find a unicorn and eat it." +ex_9 = "A man or a woman is asleep." +ex_10 = "A man is asleep or a woman is asleep." +ex_11 = "A man or a woman loves every unicorn." +ex_12 = "A man loves every unicorn or a woman loves every unicorn." +ex_13 = "Every unicorn walks or talks." diff --git a/src/Report.hs b/src/Report.hs new file mode 100644 index 0000000..71140db --- /dev/null +++ b/src/Report.hs @@ -0,0 +1,51 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Report +-- Copyright : (c) Masahiro Sakai 2007-2009 +-- License : BSD3-style (see LICENSE) +-- +-- Maintainer: masahiro.sakai@gmail.com +-- Stability : experimental +-- Portability : portable + +module Report (report) where +import IL +import P +import Parser +import MP +import Translation +import Data.List (intersperse) + +report :: String -> String +report s = unlines $ + case parseAny s of + [] -> ["(parse error)"] + ps -> concat $ intersperse ["",sep,""] (map f ps) + +f :: PAny -> [String] +f (PAny p) = + [ "Parsed:" + , " " ++ show p + , " : " ++ show c + , "" + , "Translation:" + , " " ++ show e + , " : " ++ show t + , "" + , "Translation (simplified):" + , " " ++ show e' + , " : " ++ show t + , "" + , "Translation (MP applied):" + , " " ++ show e'' + , " : " ++ show t + ] + where + e = translate p + e' = normalize e + e'' = normalize $ applyMP $ e' + c = catOf p + t = catToType c + +sep :: String +sep = "------------------------------------------------------" diff --git a/src/ReportHTML.hs b/src/ReportHTML.hs new file mode 100644 index 0000000..e88c85c --- /dev/null +++ b/src/ReportHTML.hs @@ -0,0 +1,76 @@ +----------------------------------------------------------------------------- +-- | +-- Module : ReportHTML +-- Copyright : (c) Masahiro Sakai 2009 +-- License : BSD3-style (see LICENSE) +-- +-- Maintainer: masahiro.sakai@gmail.com +-- Stability : experimental +-- Portability : portable + +module ReportHTML (report) where +import IL +import P +import Parser +import MP +import Translation +import Data.List (intersperse) +import Text.XML.Light + +report :: String -> String +report s = showTopElement $ html [hd (title ("Result of \"" ++ s ++ "\"")), body b] + where + b = case parseAny s of + [] -> [p "(parse error)"] + ps -> intersperse sep (map f ps) + +f :: PAny -> Element +f (PAny p) = dl + [ dt "Parsed" + , dd (show p ++ " : " ++ show c) + , dt "Translation" + , dd (show e ++ " : " ++ show t) + , dt "Translation (simplified)" + , dd (show e' ++ " : " ++ show t) + , dt "Translation (MP applied)" + , dd (show e'' ++ " : " ++ show t) + ] + where + e = translate p + e' = normalize e + e'' = normalize $ applyMP $ e' + c = catOf p + t = catToType c + +html :: Node t => t -> Element +html c = add_attr (Attr xmlns ns) $ node QName{ qName = "html", qURI = Just ns, qPrefix = Nothing } c + +xmlns :: QName +xmlns = QName{ qName = "xmlns", qURI = Nothing, qPrefix = Nothing} + +ns :: String +ns = "http://www.w3.org/1999/xhtml" + +hd :: Node t => t -> Element +hd = node QName{ qName = "head", qURI = Just ns, qPrefix = Nothing } + +title :: Node t => t -> Element +title = node QName{ qName = "title", qURI = Just ns, qPrefix = Nothing } + +body :: Node t => t -> Element +body = node QName{ qName = "body", qURI = Just ns, qPrefix = Nothing } + +p :: Node t => t -> Element +p = node QName{ qName = "p", qURI = Just ns, qPrefix = Nothing } + +dl :: Node t => t -> Element +dl = node QName{ qName = "dl", qURI = Just ns, qPrefix = Nothing } + +dt :: Node t => t -> Element +dt = node QName{ qName = "dt", qURI = Just ns, qPrefix = Nothing } + +dd :: Node t => t -> Element +dd = node QName{ qName = "dd", qURI = Just ns, qPrefix = Nothing } + +sep :: Element +sep = node QName{ qName = "hr", qURI = Just ns, qPrefix = Nothing } () diff --git a/src/Translation.hs b/src/Translation.hs new file mode 100644 index 0000000..5770274 --- /dev/null +++ b/src/Translation.hs @@ -0,0 +1,184 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Translation +-- Copyright : (c) Masahiro Sakai 2007-2009 +-- License : BSD3-style (see LICENSE) +-- +-- Maintainer: masahiro.sakai@gmail.com +-- Stability : experimental +-- Portability : non-portable + +{-# LANGUAGE TypeOperators, GADTs, TypeSynonymInstances, ScopedTypeVariables #-} + +module Translation (translate, catToType) where + +import IL +import P + +----------------------------------------------------------------------------- + +{- +-- 範疇から型への対応 +type family Translate x +type instance Translate Sen = Prop +type instance Translate IV = E -> Prop +type instance Translate CN = E -> Prop +type instance Translate Adj = E -> Prop +type instance Translate (a :/ b) = ((S -> Translate b) -> Translate a) +type instance Translate (a :// b) = ((S -> Translate b) -> Translate a) +-} + +catToType :: Cat c -> Type +catToType Sen = Prop +catToType IV = E :-> Prop +catToType CN = E :-> Prop +catToType Adj = E :-> Prop -- これで本当にあっている? +catToType (a :/ b) = (S (catToType b)) :-> catToType a +catToType (a :// b) = (S (catToType b)) :-> catToType a + +----------------------------------------------------------------------------- + +translate :: forall c. P c -> Expr +--- 1. αがgの定義域にあれば，α は，g(α) に翻訳される． +-- 最後に +--- 2. be → λp.λx. p{f^λy.[x = y]}. +--- ここで，変数pのタイプは>, t>>. +translate (B (IV :/ (Sen :/ IV)){- TV -} "be") = + lambda p $ lambda x $ + FVar p <@> int (lambda y $ Op2 Id (FVar x) (FVar y)) + where + p = ("p", S (S (E :-> Prop) :-> Prop)) + x = ("x", E) + y = ("y", E) +--- 3. necessarily → λp[□ext p]. ここで，p のタイプはとする． +translate (B (Sen :/ Sen) "necessarily") = lambda p $ Op1 Box (ext (FVar p)) + where + p = ("p", S Prop) +--- 4. j, m, b はタイプがe の定数記号，変数P のタイプは>とする． +translate (B (Sen :/ IV){- T -} x) = lambda p $ FVar p <@> Const (x, E) + where + p = ("p", S (catToType IV)) +--- 5. he_n → λP. P {x_n}．x_ はタイプe の変数． +translate (He n) = lambda p $ FVar p <@> FVar (xn n) + where + p = ("p", S (E :-> Prop)) +translate (F2 delta zeta) = trApp delta zeta -- T2 +translate (F3 n zeta phi) = -- T3 + lambda (xn n) $ Op2 And (translate zeta :@ FVar (xn n)) (translate phi) +translate (F4 alpha delta) = trApp alpha delta -- T4 +translate (F5 delta beta) = trApp delta beta -- T5 +-- T6 (T5と同じなので省略) +translate (F16 delta phi) = trApp delta phi -- T7 +translate (F17 delta beta) = trApp' delta beta -- T8 +translate (F6 delta beta) = trApp delta beta -- T9 +translate (F7 delta beta) = trApp delta beta -- T10 +translate (F8 phi psi) = + case cat :: Cat c of + Sen -> Op2 And (translate phi) (translate psi) -- T11a + IV -> lambda x $ Op2 And (translate phi :@ FVar x) (translate psi :@ FVar x) -- T12a + where + x = ("x", E) +translate (F9 phi psi) = + case cat :: Cat c of + Sen -> Op2 Or (translate phi) (translate psi) -- T11b + IV -> lambda x $ Op2 Or (translate phi :@ FVar x) (translate psi :@ FVar x) -- T12b + where x = ("x", E) + Sen :/ IV -> lambda p $ Op2 Or (translate phi :@ FVar p) (translate psi :@ FVar p) -- T13 + where p = ("P", S (E :-> Prop)) +-- T14 (講義資料はx_nになるべきところがxになっている) +translate (F10 n alpha phi) = + case cat :: Cat c of + Sen -> translate alpha :@ (int $ lambda (xn n) (translate phi)) -- T14 + CN -> lambda y $ translate alpha :@ int (lambda (xn n) (translate phi :@ FVar y)) -- T15 + IV -> lambda y $ translate alpha :@ int (lambda (xn n) (translate phi :@ FVar y)) -- T16 + where + y = ("y", E) +-- T17 +translate (F11 alpha delta) = Op1 Not $ trApp alpha delta +translate (F12 alpha delta) = Op1 F $ trApp alpha delta +translate (F13 alpha delta) = Op1 Not $ Op1 F $ trApp alpha delta +translate (F14 alpha delta) = Op1 H $ trApp alpha delta +translate (F15 alpha delta) = Op1 Not $ Op1 H $ trApp alpha delta +-- T18 (beの扱い以外はT9と同じ) +translate (B (IV :/ Adj) "be") = lambda p $ lambda x $ FVar p <@> FVar x + where + p = ("P", S (E :-> Prop)) + x = ("x", E) +-- T19 +translate (F19 delta) = + lambda x $ exists y $ + translate delta :@ int (lambda p (FVar p <@> FVar y)) :@ FVar x + where + x = ("x", E) + p = ("P", S (E :-> Prop)) + y = ("y", E) +translate (F20 delta beta) = trApp delta beta -- T20 +translate (F21 delta beta) = trApp delta beta -- T21 (講義資料ではF20を誤って使っている) +-- T22 +translate (F22 delta) = + lambda p $ lambda q $ lambda x $ + translate delta :@ FVar q :@ FVar p :@ FVar x + where + p = ("P", S (catToType (cat :: Cat T))) + q = ("Q", S (catToType (cat :: Cat T))) + x = ("x", E) +translate (F23 alpha delta) = trApp alpha delta -- T23 +translate (F24 alpha beta) = trApp alpha beta -- T24 +-- 講義資料のByの解釈は誤り? (型が一致しない) +translate (B (IV :/ (IV :/ (Sen :/ IV)) :/ (Sen :/ IV)){- PP/T -} "by") = + lambda p $ lambda r $ lambda x $ + FVar p <@> + (int $ lambda y $ FVar r <@> int (lambda q $ FVar q <@> FVar x) :@ FVar y) + where + p = ("P", S (catToType (Sen :/ IV))) + r = ("R", S (catToType (IV :/ (Sen :/ IV)))) + x = ("x", E) + y = ("y", E) + q = ("Q", S (catToType IV)) +-- T25 +translate (F25 delta) = + lambda x $ exists y $ Op1 H $ + translate delta :@ + int (lambda p $ FVar p <@> FVar x) :@ + (FVar y) + where + x = ("x", E) + y = ("y", E) + p = ("P", S (catToType IV)) + +-- Det +translate (B (Sen :/ IV :/ CN) s) = + case s of + "a" -> + lambda p $ lambda q $ exists x $ + Op2 And (FVar p <@> FVar x) (FVar q <@> FVar x) + "the" -> + lambda p $ lambda q $ exists y $ + Op2 And + (forall x $ Op2 Equiv (FVar p <@> FVar x) (Op2 Id (FVar x) (FVar y))) + (FVar q <@> FVar y) + "every" -> + lambda p $ lambda q $ forall x $ + Op2 Imply (FVar p <@> FVar x) (FVar q <@> FVar x) + "no" -> + lambda p $ lambda q $ forall x $ + Op1 Not (Op2 And (FVar p <@> FVar x) (FVar q <@> FVar x)) + _ -> Const (s, catToType (cat :: Cat Det)) + where + p = ("p", S (E :-> Prop)) + q = ("q", S (E :-> Prop)) + x = ("x", E) + y = ("y", E) + +-- それ以外 +translate (B c x) = Const (x, catToType c) + +-- ユーティリティ +trApp :: P (b :/ a) -> P a -> Expr +trApp f a = translate f :@ (int (translate a)) +trApp' :: P (b :// a) -> P a -> Expr +trApp' f a = translate f :@ (int (translate a)) + +xn :: Int -> Name +xn n = ("he_"++show n, E) + diff --git a/src/URLEncoding.hs b/src/URLEncoding.hs new file mode 100644 index 0000000..1e87b17 --- /dev/null +++ b/src/URLEncoding.hs @@ -0,0 +1,37 @@ +----------------------------------------------------------------------------- +-- | +-- Module : URLEncoding +-- Copyright : Copyright (c) 2005,2006 Minero Aoki +-- License : LGPL (see COPYING) +-- +-- Maintainer: masahiro.sakai@gmail.com +-- Stability : experimental +-- Portability : non-portable + +{-# LANGUAGE CPP #-} +-- +-- $Id: URLEncoding.hs,v 1.2 2006/04/05 17:55:14 aamine Exp $ +-- +-- Copyright (c) 2005,2006 Minero Aoki +-- +-- This program is free software. +-- You can distribute/modify this program under the terms of +-- the GNU LGPL, Lesser General Public License version 2.1. +-- For details of the GNU LGPL, see the file "COPYING". +-- + +module URLEncoding (urlencode, urldecode) where + +#if __GLASGOW_HASKELL__ > 602 +import Network.URI (escapeURIString, unEscapeString) +#else +import Network.URI (escapeString, unEscapeString) +#endif +import Data.Char (isAlphaNum) + +#if __GLASGOW_HASKELL__ > 602 +urlencode = escapeURIString (isAlphaNum) +#else +urlencode str = escapeString str (isAlphaNum) +#endif +urldecode = unEscapeString diff --git a/src/Version.hs b/src/Version.hs new file mode 100644 index 0000000..bffdb64 --- /dev/null +++ b/src/Version.hs @@ -0,0 +1,4 @@ +module Version where + +versionStr :: String +versionStr = "0.0.5"