PTQ (empty) → 0.0.4
raw patch · 22 files changed
+2746/−0 lines, 22 filesdep +basedep +containersdep +haskell98setup-changed
Dependencies added: base, containers, haskell98, mtl, network, utf8-string
Files
- COPYING +510/−0
- PTQ.cabal +71/−0
- README +42/−0
- Setup.lhs +4/−0
- cgi/index.html +14/−0
- cgi/main.html +49/−0
- misc/Test.hs +50/−0
- misc/Test2.agda +99/−0
- misc/Test3.hs +53/−0
- src/CGI.hs +139/−0
- src/CGIMain.hs +29/−0
- src/Context.hs +99/−0
- src/Expr.hs +246/−0
- src/MP.hs +34/−0
- src/Main.hs +36/−0
- src/P.hs +206/−0
- src/PDict.hs +79/−0
- src/Parser.hs +722/−0
- src/ParserTest.hs +37/−0
- src/Report.hs +45/−0
- src/Translation.hs +145/−0
- src/URLEncoding.hs +37/−0
+ COPYING view
@@ -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.+++ <one line to give the library's name and a brief idea of what it does.>+ Copyright (C) <year> <name of author>++ 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.++ <signature of Ty Coon>, 1 April 1990+ Ty Coon, President of Vice++That's all there is to it!++
+ PTQ.cabal view
@@ -0,0 +1,71 @@+Name: PTQ+Version: 0.0.4+License: LGPL+License-File: COPYING+Author: Masahiro Sakai+Maintainer: Masahiro Sakai <masahiro.sakai AT gmail.com>+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:+ Expr+ P+ Translation+ Parser+ Report+ Extensions:+ EmptyDataDecls+ GADTs+ MultiParamTypeClasses+ TypeOperators+ TypeSynonymInstances+ GeneralizedNewtypeDeriving+ 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:+ Expr+ P+ Translation+ Parser+ Report+ CGI+ URLEncoding+ Extensions:+ EmptyDataDecls+ GADTs+ MultiParamTypeClasses+ TypeOperators+ TypeSynonymInstances+ GeneralizedNewtypeDeriving+ CPP+ Build-Depends: base >=4 && <5, haskell98, mtl, containers, network+ if flag(UTF8CGI)+ CPP-Options: "-DUSE_UTF8"+ Build-Depends: utf8-string
+ README view
@@ -0,0 +1,42 @@+= 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+ %++== Simple 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.++Currenly it also runs at ((<URL:http://www.tom.sfc.keio.ac.jp/~sakai/hsPTQ/>)).
+ Setup.lhs view
@@ -0,0 +1,4 @@+#! /usr/bin/env runhaskell + +> import Distribution.Simple +> main = defaultMain
+ cgi/index.html view
@@ -0,0 +1,14 @@+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Frameset//EN">+<html>+<head>+<meta http-equiv="Content-Type" content="text/html; charset=utf-8">+<title>Demo page of PTQ</title>+</head>+<frameset rows="30%,*">+<frame src="main.html">+<frame name="result">+<noframes>+<a href="main.html">No frame version</a>+</noframes>+</frameset>+</html>
+ cgi/main.html view
@@ -0,0 +1,49 @@+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">+<html>+<head>+<meta http-equiv="Content-Type" content="text/html; charset=utf-8">+<title>Demo page of PTQ</title>+</head>++<body>+<h1>Demo page of <a href="http://www.tom.sfc.keio.ac.jp/~sakai/hiki/?hsPTQ" target="_top">PTQ</a></h1>++<p>+<form method="get" action="ptq.cgi" accept-charset="utf-8 us-ascii" target="result">+<input type="text" name="s" value="" size="100" />+<input type="submit" value="Translate!" />+</form>+</p>++<p>+<form method="get" action="ptq.cgi" accept-charset="utf-8 us-ascii" target="result">+Sample: <select name="s">+<option>John seeks a unicorn.</option>+<option>John finds a unicorn.</option>+<option>Necessarily John walks.</option>+<option>John is Bill.</option>+<option>John is a unicorn.</option>+<option>John believes that a unicorn talks.</option>+<option>Every woman loves a unicorn.</option>+<option>Every woman loves John.</option>+<option>A unicorn walks and it talks.</option>+<option>Every unicorn such that it walks talks.</option>+<option>John walks slowly.</option>+<option>John walks in a park.</option>+<option>John wishes to find a unicorn and eat it.</optoin>+<option>A man or a woman is asleep.</option>+<option>A man is asleep or a woman is asleep.</option>+<option>A man or a woman loves every unicorn.</option>+<option>A man loves every unicorn or a woman loves every unicorn.</option>+<option>Every unicorn walks or talks.</option>+<!-- ここまでは講義資料に載っていたもの -->+<option>John has sought a unicorn.</option>+<option>John will seek a unicorn.</option>+<option>A unicorn is eaten by John.</option>+<option>Every unicorn is not a man.</option>+<option>Every man loves a woman such that she loves him.</option>+</select> <input type="submit" value="Translate!" />+</form>+</p>++</body> </html>
+ misc/Test.hs view
@@ -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+++-----------------------------------------------------------------------------
+ misc/Test2.agda view
@@ -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))
+ misc/Test3.hs view
@@ -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+-}
+ src/CGI.hs view
@@ -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, "\""]
+ src/CGIMain.hs view
@@ -0,0 +1,29 @@+-----------------------------------------------------------------------------+-- |+-- 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 Report+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)
+ src/Context.hs view
@@ -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)
+ src/Expr.hs view
@@ -0,0 +1,246 @@+-----------------------------------------------------------------------------+-- |+-- Module : Expr+-- Copyright : (c) Masahiro Sakai 2007-2009+-- License : BSD3-style (see LICENSE)+-- +-- Maintainer: masahiro.sakai@gmail.com+-- Stability : experimental+-- Portability : non-portable++{-# LANGUAGE CPP, GeneralizedNewtypeDeriving #-}+module Expr+ ( Op1 (..)+ , Op2 (..)+ , Binder (..)+ , Expr (..)+ , Scope (..)+ , Name+ , lambda+ , forall+ , exists+ , int+ , ext+ , (<@>)+ , abstract+ , instantiate+ , normalize+ , RenderM+ , runRenderM+ , renderExpr+ , renderExprU+ ) where++import Control.Monad.RWS+import Data.List++-----------------------------------------------------------------------------++data Op1 = Not | Box | F | H | Int | Ext deriving (Eq,Show)+data Op2 = And | Or | Imply | Equiv | Id deriving (Eq,Show)+data Binder = Lambda | Forall | Exists deriving (Eq,Show)++infixl 9 :@++data Expr+ = FVar Name -- 自由変数+ | BVar !Int -- 束縛変数+ | Expr :@ Expr -- 関数適用+ | Const String -- 定数 (≒自由変数)+ | Op1 !Op1 Expr -- 前置演算子+ | Op2 !Op2 Expr Expr -- 中置演算子+ | Bind !Binder Scope -- 変数束縛++instance Show Expr where+#ifdef USE_UTF8+ showsPrec d x = runRenderM (renderExprU d x)+#else+ showsPrec d x = runRenderM (renderExpr d x)+#endif++newtype Scope = Sc Expr deriving Show+type Name = String++-----------------------------------------------------------------------------++lambda :: Name -> Expr -> Expr+lambda name expr = Bind Lambda (abstract name expr)++forall :: Name -> Expr -> Expr+forall name expr = Bind Forall (abstract name expr)++exists :: Name -> Expr -> Expr+exists name expr = Bind Exists (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 (Sc body)) = Bind q (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 (Sc body)) =+ case normalize body of+ f :@ BVar 0 | not (0 `elem` bvs f) -> varShift (-1) f -- η-conversion+ body -> Bind Lambda (Sc body)+normalize (Bind q (Sc body)) = Bind q (Sc (normalize body))+normalize (fun :@ arg) =+ case normalize fun of+ Bind Lambda 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 b (Sc e)) = [n - 1 | n <- bvs e, n /= 0]++-----------------------------------------------------------------------------++newtype RenderM a = RenderM (RWS [Name] () Int a)+ deriving (Monad, MonadReader [Name])++runRenderM :: RenderM a -> a+runRenderM (RenderM m) = + case runRWS m [] 0 of+ (a, _, _) -> a++render :: Bool -> Int -> Expr -> RenderM ShowS+render u = h+ where+ h d e = case e of+ FVar name -> return $ showString name+ BVar index -> do+ vs <- ask+ return $ showString (vs !! index)+ Bind q _ -> f d q e+ 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 s+ Op1 op a -> do+ t <- h (prec+1) a+ return $ showParen (d > prec)+ $ showString s . t+ where+ s = case op of+ Not -> if u then "¬" else "not " -- ¬ (U+00AC)+ Box -> if u then "◻" else "[]" -- ◻ (U+25FB) が正しそうだが □ (U+25A1) を使うのが無難か?+ F -> "F "+ H -> "H "+ Int -> if u then "˄" else "Int " -- ˄ (U+02C4)+ Ext -> if u then "˅" else "Ext " -- ˅ (U+02C5)+ prec = case op of+ Int | u -> app_prec + 1+ Ext | u -> 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 u then "∧" else "&&", 4, id, id) -- ∧ (U+2227)+ Or -> (if u then "∨" else "||", 3, id, id) -- ∨ (U+2228)+ Imply -> (if u then "→" else "->", 1, (+1), id) -- → (U+2192)+ Equiv -> (if u then "↔" else "<->", 1, (+1), (+1)) -- ↔ (U+2194)+ Id -> ("=", 2, (+1), (+1))++ f :: Int -> Binder -> Expr -> RenderM ShowS+ f d b e = do+ (xs, s) <- go e+ return $ showParen (d > 0) $+ showString (g b) . showString (intercalate " " xs) . showString ". " . s+ where+ go :: Expr -> RenderM ([Name], ShowS)+ go (Bind b' (Sc body)) | b==b' = do+ x <- gensym + (xs, s) <- local (x:) $ go body+ return (x:xs, s)+ go e = do+ s <- h 0 e+ return ([], s)++ g :: Binder -> String+ g Lambda = if u then "λ" else "\\" -- λ (U+03BB)+ g Forall = if u then "∀" else "forall " -- ∀ (U+2200)+ g Exists = if u then "∃" else "exists " -- ∃ (U+2203)+++renderExpr :: Int -> Expr -> RenderM ShowS+renderExpr = render False++renderExprU :: Int -> Expr -> RenderM ShowS+renderExprU = render True++app_prec :: Int+app_prec = 10++gensym :: RenderM Name+gensym = RenderM $ do + i <- get+ put (i+1)+ return ("x"++show i)
+ src/MP.hs view
@@ -0,0 +1,34 @@+-----------------------------------------------------------------------------+-- |+-- 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 Expr++applyMP :: Expr -> Expr+-- MP1+-- MP4+applyMP (Const tv) | tv `elem` ["find","lose","eat","love"] =+ lambda "p" $ lambda "x" $+ FVar "p" <@> (int $ lambda "y" $ Const tv :@ int (lambda "P" $ FVar "P" <@> FVar "y") :@ FVar "x")+-- MP8+applyMP (Const "in") =+ lambda "p" $ lambda "P" $ lambda "x" $+ FVar "p" <@> (int $ lambda "y" $ Const "in" :@ int (lambda "z" $ FVar "z" <@> FVar "y") :@ FVar "P" :@ FVar "x")+-- MP9+applyMP (Const "seek") = lambda "P" $ Const "try" :@ int (find' :@ FVar "P")+ where find' = applyMP (Const "find")+applyMP (Bind q (Sc body)) = Bind q (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
+ src/Main.hs view
@@ -0,0 +1,36 @@+-----------------------------------------------------------------------------+-- |+-- 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+#ifdef USE_UTF8+import Prelude hiding (putStr, getLine)+import System.IO hiding (putStr, getLine)+import System.IO.UTF8+#else+import System.IO+#endif++main :: IO ()+main =+ do -- FIXME: バナーを表示+ hSetBuffering stdout NoBuffering+ loop++loop :: IO ()+loop = + do putStr "PTQ> "+ s <- getLine+ case s of+ "quit" -> return ()+ _ -> do + putStr (report s)+ loop
+ src/P.hs view
@@ -0,0 +1,206 @@+-----------------------------------------------------------------------------+-- |+-- 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 (..)+ , cat_Sen+ , cat_IV+ , cat_CN+ , cat_Adj+ , T+ , TV+ , IAV+ , cat_T+ , cat_TV+ , cat_IAV+ , Det+ , DTV+ , TTV+ , PP+ , cat_Det+ , cat_DTV+ , cat_PP+ , PronounNo+ , P (..)+ , PAny (..)+ , F5+ , F6+ , F8 (..)+ , F9 (..)+ , F10 (..)+ ) where+import Expr++-----------------------------------------------------------------------------++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)+cat_Sen = Sen+cat_IV = IV+cat_CN = CN+cat_Adj = Adj++type T = Sen :/ IV -- 名詞句, 固有名詞: John, he+type TV = IV :/ T -- 他動詞(句): find+type IAV = IV :/ IV -- 動詞句修飾の副詞(句): slowly+cat_T = cat_Sen :/ cat_IV+cat_TV = cat_IV :/ cat_T+cat_IAV = cat_IV :/ cat_IV++-- 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+cat_Det = cat_T :/ cat_CN+cat_DTV = cat_TV :/ cat_T+cat_PP = cat_IV :/ cat_TV++-----------------------------------------------------------------------------++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 :: P a -> PAny++class F5 c +instance F5 IV -- T5+instance F5 IAV -- T6++class F6 c a+instance F6 Sen Sen -- T9+instance F6 IV Adj -- T18++class F8 c where f8 :: Cat c+instance F8 Sen where f8 = cat_Sen+instance F8 IV where f8 = cat_IV++class F9 c where f9 :: Cat c+instance F9 Sen where f9 = cat_Sen+instance F9 IV where f9 = cat_IV+instance F9 T where f9 = cat_T++class F10 c where f10 :: Cat c+instance F10 Sen where f10 = cat_Sen+instance F10 CN where f10 = cat_CN+instance F10 IV where f10 = cat_IV++-----------------------------------------------------------------------------++-- 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
+ src/PDict.hs view
@@ -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"
+ src/Parser.hs view
@@ -0,0 +1,722 @@+----------------------------------------------------------------------------+-- |+-- 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 hiding (f8,f9,f10)++-----------------------------------------------------------------------------+-- パーサのコア部分++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 x) | x <- [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 :: 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_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 c = chainr1 (p <|> he_n c) 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 c =+ do g <- case c of+ Subject -> + msum [ token "he" >> return Masculine+ , token "she" >> return Feminine+ , token "it" >> return Neuter+ ]+ Object ->+ msum [ token "him" >> return Masculine+ , token "her" >> return Feminine+ , token "it" >> return Neuter+ ]+ 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 :: Cat c -> [VerbEntry] -> VerbForm -> Parser (P c)+verbParser cat 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 :: Cat c -> [NounEntry] -> Parser (P c, Gender)+nounParser c dict =+ do x <- anyToken+ case lookup x dict of+ Nothing -> mzero+ Just g -> return (B c 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 :: Cat c -> [String] -> Parser (P c)+dictParser cat dict =+ do x <- anyToken+ guard $ x `elem` dict+ return $ B cat x++-----------------------------------------------------------------------------+-- 各統語規則のパーサ++s1_IV :: VerbForm -> Parser (P IV)+s1_IV = verbParser cat_IV dict_IV++s1_TV :: VerbForm -> Parser (P TV)+s1_TV = verbParser cat_TV dict_TV++s1_IV_t :: VerbForm -> Parser (P (IV :/ Sen))+s1_IV_t = verbParser (cat_IV :/ cat_Sen) dict_IV_t++s1_IV__IV :: VerbForm -> Parser (P (IV :// IV))+s1_IV__IV = verbParser (cat_IV :// cat_IV) dict_IV__IV++s1_IV_Adj :: VerbForm -> Parser (P (IV :/ Adj))+s1_IV_Adj = verbParser (cat_IV :/ cat_Adj) dict_IV_Adj++s1_T :: Parser (P T, Gender)+s1_T = nounParser cat_T dict_T++s1_CN :: Parser (P CN, Gender)+s1_CN = nounParser cat_CN dict_CN++s1_IAV :: Parser (P IAV)+s1_IAV = dictParser cat_IAV dict_IAV++s1_t_t :: Parser (P (Sen :/ Sen)) +s1_t_t = dictParser (cat_Sen :/ cat_Sen) dict_t_t++s1_IAV_T :: Parser (P (IAV :/ T))+s1_IAV_T = dictParser (cat_IAV :/ cat_T) dict_IAV_T++s1_Adj :: Parser (P Adj)+s1_Adj = dictParser cat_Adj dict_Adj++s1_Det :: Parser (P Det)+s1_Det = dictParser cat_Det dict_Det++s1_PP_T :: Parser (P (PP :/ T))+s1_PP_T = dictParser (cat_PP :/ cat_T) 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
+ src/ParserTest.hs view
@@ -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."
+ src/Report.hs view
@@ -0,0 +1,45 @@+-----------------------------------------------------------------------------+-- |+-- 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 Expr+import P+import Parser+import MP+import Translation+import 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+ , ""+ , "Translation:"+ , " " ++ show e+ , ""+ , "Translation (simplified):"+ , " " ++ show e'+ , ""+ , "Translation (MP applied):"+ , " " ++ show e''+ ]+ where+ e = translate p+ e' = normalize e+ e'' = normalize $ applyMP $ e'++sep :: String+sep = "------------------------------------------------------"
+ src/Translation.hs view
@@ -0,0 +1,145 @@+-----------------------------------------------------------------------------+-- |+-- 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) where++import Expr+import P++-----------------------------------------------------------------------------+-- Exprも型付きにしたいなぁ++{-+data E -- e+data S -- s+data Prop -- t+-- 関数型はHaskellの -> をそのまま使う++-- 範疇から型への対応+type family Translate x+type instance Translate Sen = Prop+type instance Translate IV = E -> Prop+type instance Translate CN = E -> Prop+type instance Translate (a :/ b) = ((S -> Translate b) -> Translate a)+type instance Translate (a :// b) = ((S -> Translate b) -> Translate a)+-}++-----------------------------------------------------------------------------++translate :: forall c. P c -> Expr+--- 1. αがgの定義域にあれば，α は，g(α) に翻訳される．+-- 最後に+--- 2. be → λp.λx. p{f^λy.[x = y]}.+--- ここで，変数pのタイプは<s, <<s, <e, t>>, t>>.+translate (B (IV :/ (Sen :/ IV)){- TV -} "be") =+ lambda "p" $ lambda "x" $ + FVar "p" <@>+ int (lambda "y" $ Op2 Id (FVar "x") (FVar "y"))+--- 3. necessarily → λp[□ext p]. ここで，p のタイプは<s, t>とする．+translate (B (Sen :/ Sen) "necessarily") = lambda "p" $ Op1 Box (ext (FVar "p"))+--- 4. j, m, b はタイプがe の定数記号，変数P のタイプは<s, <e, t>>とする．+translate (B (Sen :/ IV){- T -} x) = lambda "p" $ FVar "p" <@> Const x+--- 5. he_n → λP. P {x_n}．x_ はタイプe の変数．+translate (He n) = lambda "p" $ FVar "p" <@> FVar (xn n)++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 f8 :: 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+translate (F9 phi psi) =+ case f9 :: 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+ Sen :/ IV -> lambda "P" $ Op2 Or (translate phi :@ FVar "P") (translate psi :@ FVar "P") -- T13+-- T14 (講義資料はx_nになるべきところがxになっている)+translate (F10 n alpha phi) =+ case f10 :: 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+-- 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"+-- T19+translate (F19 delta) =+ lambda "x" $ exists "y" $+ translate delta :@+ int (lambda "P" (FVar "P" <@> FVar "y")) :@+ FVar "x"+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"+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")+-- T25+translate (F25 delta) =+ lambda "x" $ exists "y" $ Op1 H $+ translate delta :@+ int (lambda "P" $ FVar "P" <@> FVar "x") :@+ (FVar "y")++-- 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" $ forall "x" $+ Op2 And+ (Op2 Equiv (FVar "p" <@> FVar "x") (Op2 Id (FVar "x") (FVar "y")))+ (FVar "q" <@> FVar "x")+ "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++-- それ以外+translate (B _ x) = Const x++-- ユーティリティ+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+
+ src/URLEncoding.hs view
@@ -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