From c1d2a9b5b0e766121e210ca159a80860e8be87a7 Mon Sep 17 00:00:00 2001 From: Fabian Zickgraf Date: Tue, 1 Aug 2023 12:20:46 +0200 Subject: [PATCH 1/4] Remove DeductiveSystemForCAP --- DeductiveSystemForCAP/.gitignore | 34 - DeductiveSystemForCAP/LICENSE | 339 ----- DeductiveSystemForCAP/PackageInfo.g | 102 -- DeductiveSystemForCAP/README.md | 32 - DeductiveSystemForCAP/doc/Doc.autodoc | 1 - DeductiveSystemForCAP/doc/clean | 2 - DeductiveSystemForCAP/examples/LogicExample.g | 40 - .../examples/LogicKaiserslautern.g | 47 - .../examples/ModulesOverPolynomialRing.g | 45 - .../examples/SpectralSequenceKaiserslautern.g | 75 - ...pectralSequenceKaiserslauternWithCospans.g | 65 - ...nceKaiserslauternWithCospansToDoListTest.g | 69 - DeductiveSystemForCAP/examples/VectorSpaces.g | 1029 ------------- .../examples/deductive_generalized.g | 66 - DeductiveSystemForCAP/gap/DeductiveSystem.gd | 105 -- DeductiveSystemForCAP/gap/DeductiveSystem.gi | 1323 ----------------- .../gap/LogicForDeductiveSystem.gd | 33 - .../gap/LogicForDeductiveSystem.gi | 623 -------- DeductiveSystemForCAP/init.g | 3 - DeductiveSystemForCAP/makedoc.g | 31 - .../makedoc_with_overfull_hbox_warnings.g | 42 - DeductiveSystemForCAP/makefile | 57 - DeductiveSystemForCAP/read.g | 4 - DeductiveSystemForCAP/tst/100_LoadPackage.tst | 15 - DeductiveSystemForCAP/tst/testall.g | 35 - README.md | 8 - dev/codecov.yml | 5 +- dev/make_dist.sh | 5 - dev/simulate_dist.sh | 5 - dev/upload_codecov.sh | 4 - makefile | 15 +- 31 files changed, 4 insertions(+), 4255 deletions(-) delete mode 100644 DeductiveSystemForCAP/.gitignore delete mode 100644 DeductiveSystemForCAP/LICENSE delete mode 100644 DeductiveSystemForCAP/PackageInfo.g delete mode 100644 DeductiveSystemForCAP/README.md delete mode 100644 DeductiveSystemForCAP/doc/Doc.autodoc delete mode 100755 DeductiveSystemForCAP/doc/clean delete mode 100644 DeductiveSystemForCAP/examples/LogicExample.g delete mode 100644 DeductiveSystemForCAP/examples/LogicKaiserslautern.g delete mode 100644 DeductiveSystemForCAP/examples/ModulesOverPolynomialRing.g delete mode 100644 DeductiveSystemForCAP/examples/SpectralSequenceKaiserslautern.g delete mode 100644 DeductiveSystemForCAP/examples/SpectralSequenceKaiserslauternWithCospans.g delete mode 100644 DeductiveSystemForCAP/examples/SpectralSequenceKaiserslauternWithCospansToDoListTest.g delete mode 100644 DeductiveSystemForCAP/examples/VectorSpaces.g delete mode 100644 DeductiveSystemForCAP/examples/deductive_generalized.g delete mode 100644 DeductiveSystemForCAP/gap/DeductiveSystem.gd delete mode 100644 DeductiveSystemForCAP/gap/DeductiveSystem.gi delete mode 100644 DeductiveSystemForCAP/gap/LogicForDeductiveSystem.gd delete mode 100644 DeductiveSystemForCAP/gap/LogicForDeductiveSystem.gi delete mode 100644 DeductiveSystemForCAP/init.g delete mode 100644 DeductiveSystemForCAP/makedoc.g delete mode 100644 DeductiveSystemForCAP/makedoc_with_overfull_hbox_warnings.g delete mode 100644 DeductiveSystemForCAP/makefile delete mode 100644 DeductiveSystemForCAP/read.g delete mode 100644 DeductiveSystemForCAP/tst/100_LoadPackage.tst delete mode 100644 DeductiveSystemForCAP/tst/testall.g diff --git a/DeductiveSystemForCAP/.gitignore b/DeductiveSystemForCAP/.gitignore deleted file mode 100644 index 9231374e12..0000000000 --- a/DeductiveSystemForCAP/.gitignore +++ /dev/null @@ -1,34 +0,0 @@ -/doc/chap*.html -/doc/chap*.txt -/doc/*.css -/doc/*.js -/doc/chooser.html -/doc/*.aux -/doc/*.bbl -/doc/*.blg -/doc/*.brf -/doc/*.idx -/doc/*.ilg -/doc/*.ind -/doc/*.lab -/doc/*.log -/doc/*.out -/doc/*.pnr -/doc/*.six -/doc/*.tex -/doc/*.toc -/doc/manual.pdf -/doc/_*.xml - -/bin/ -/gen/ -/Makefile - -/tmp/ -/gh-pages/ - -/coverage.json -/doc/*.xml -/doc_tmp/ -/stats -/tst/deductivesystemforcap*.tst diff --git a/DeductiveSystemForCAP/LICENSE b/DeductiveSystemForCAP/LICENSE deleted file mode 100644 index d159169d10..0000000000 --- a/DeductiveSystemForCAP/LICENSE +++ /dev/null @@ -1,339 +0,0 @@ - GNU GENERAL PUBLIC LICENSE - Version 2, June 1991 - - Copyright (C) 1989, 1991 Free Software Foundation, Inc., - 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA - Everyone is permitted to copy and distribute verbatim copies - of this license document, but changing it is not allowed. - - Preamble - - The licenses for most software are designed to take away your -freedom to share and change it. By contrast, the GNU General Public -License is intended to guarantee your freedom to share and change free -software--to make sure the software is free for all its users. This -General Public License applies to most of the Free Software -Foundation's software and to any other program whose authors commit to -using it. (Some other Free Software Foundation software is covered by -the GNU Lesser General Public License instead.) You can apply it to -your programs, too. - - When we speak of free software, we are referring to freedom, not -price. Our General Public Licenses are designed to make sure that you -have the freedom to distribute copies of free software (and charge for -this service if you wish), that you receive source code or can get it -if you want it, that you can change the software or use pieces of it -in new free programs; and that you know you can do these things. - - To protect your rights, we need to make restrictions that forbid -anyone to deny you these rights or to ask you to surrender the rights. -These restrictions translate to certain responsibilities for you if you -distribute copies of the software, or if you modify it. - - For example, if you distribute copies of such a program, whether -gratis or for a fee, you must give the recipients all the rights that -you have. You must make sure that they, too, receive or can get the -source code. And you must show them these terms so they know their -rights. - - We protect your rights with two steps: (1) copyright the software, and -(2) offer you this license which gives you legal permission to copy, -distribute and/or modify the software. - - Also, for each author's protection and ours, we want to make certain -that everyone understands that there is no warranty for this free -software. If the software is modified by someone else and passed on, we -want its recipients to know that what they have is not the original, so -that any problems introduced by others will not reflect on the original -authors' reputations. - - Finally, any free program is threatened constantly by software -patents. We wish to avoid the danger that redistributors of a free -program will individually obtain patent licenses, in effect making the -program proprietary. To prevent this, we have made it clear that any -patent must be licensed for everyone's free use or not licensed at all. - - The precise terms and conditions for copying, distribution and -modification follow. - - GNU GENERAL PUBLIC LICENSE - TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION - - 0. This License applies to any program or other work which contains -a notice placed by the copyright holder saying it may be distributed -under the terms of this General Public License. The "Program", below, -refers to any such program or work, and a "work based on the Program" -means either the Program or any derivative work under copyright law: -that is to say, a work containing the Program or a portion of it, -either verbatim or with modifications and/or translated into another -language. (Hereinafter, translation is included without limitation in -the term "modification".) Each licensee is addressed as "you". - -Activities other than copying, distribution and modification are not -covered by this License; they are outside its scope. The act of -running the Program is not restricted, and the output from the Program -is covered only if its contents constitute a work based on the -Program (independent of having been made by running the Program). -Whether that is true depends on what the Program does. - - 1. You may copy and distribute verbatim copies of the Program's -source code as you receive it, in any medium, provided that you -conspicuously and appropriately publish on each copy an appropriate -copyright notice and disclaimer of warranty; keep intact all the -notices that refer to this License and to the absence of any warranty; -and give any other recipients of the Program a copy of this License -along with the Program. - -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 Program or any portion -of it, thus forming a work based on the Program, 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) You must cause the modified files to carry prominent notices - stating that you changed the files and the date of any change. - - b) You must cause any work that you distribute or publish, that in - whole or in part contains or is derived from the Program or any - part thereof, to be licensed as a whole at no charge to all third - parties under the terms of this License. - - c) If the modified program normally reads commands interactively - when run, you must cause it, when started running for such - interactive use in the most ordinary way, to print or display an - announcement including an appropriate copyright notice and a - notice that there is no warranty (or else, saying that you provide - a warranty) and that users may redistribute the program under - these conditions, and telling the user how to view a copy of this - License. (Exception: if the Program itself is interactive but - does not normally print such an announcement, your work based on - the Program is not required to print an announcement.) - -These requirements apply to the modified work as a whole. If -identifiable sections of that work are not derived from the Program, -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 Program, 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 Program. - -In addition, mere aggregation of another work not based on the Program -with the Program (or with a work based on the Program) on a volume of -a storage or distribution medium does not bring the other work under -the scope of this License. - - 3. You may copy and distribute the Program (or a work based on it, -under Section 2) in object code or executable form under the terms of -Sections 1 and 2 above provided that you also do one of the following: - - a) 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; or, - - b) Accompany it with a written offer, valid for at least three - years, to give any third party, for a charge no more than your - cost of physically performing source distribution, a complete - machine-readable copy of the corresponding source code, to be - distributed under the terms of Sections 1 and 2 above on a medium - customarily used for software interchange; or, - - c) Accompany it with the information you received as to the offer - to distribute corresponding source code. (This alternative is - allowed only for noncommercial distribution and only if you - received the program in object code or executable form with such - an offer, in accord with Subsection b above.) - -The source code for a work means the preferred form of the work for -making modifications to it. For an executable work, 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 executable. However, as a -special exception, the source code 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. - -If distribution of executable or 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 counts as -distribution of the source code, even though third parties are not -compelled to copy the source along with the object code. - - 4. You may not copy, modify, sublicense, or distribute the Program -except as expressly provided under this License. Any attempt -otherwise to copy, modify, sublicense or distribute the Program 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. - - 5. 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 Program or its derivative works. These actions are -prohibited by law if you do not accept this License. Therefore, by -modifying or distributing the Program (or any work based on the -Program), you indicate your acceptance of this License to do so, and -all its terms and conditions for copying, distributing or modifying -the Program or works based on it. - - 6. Each time you redistribute the Program (or any work based on the -Program), the recipient automatically receives a license from the -original licensor to copy, distribute or modify the Program 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 to -this License. - - 7. 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 Program at all. For example, if a patent -license would not permit royalty-free redistribution of the Program 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 Program. - -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. - - 8. If the distribution and/or use of the Program is restricted in -certain countries either by patents or by copyrighted interfaces, the -original copyright holder who places the Program 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. - - 9. The Free Software Foundation may publish revised and/or new versions -of the General Public License from time to time. Such new versions will -be similar in spirit to the present version, but may differ in detail to -address new problems or concerns. - -Each version is given a distinguishing version number. If the Program -specifies 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 Program does not specify a version number of -this License, you may choose any version ever published by the Free Software -Foundation. - - 10. If you wish to incorporate parts of the Program into other free -programs whose distribution conditions are different, 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 - - 11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY -FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN -OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES -PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED -OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF -MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS -TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE -PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, -REPAIR OR CORRECTION. - - 12. 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 PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, -INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING -OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED -TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY -YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER -PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE -POSSIBILITY OF SUCH DAMAGES. - - END OF TERMS AND CONDITIONS - - How to Apply These Terms to Your New Programs - - If you develop a new program, and you want it to be of the greatest -possible use to the public, the best way to achieve this is to make it -free software which everyone can redistribute and change under these terms. - - To do so, attach the following notices to the program. It is safest -to attach them to the start of each source file to most effectively -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 program is free software; you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation; either version 2 of the License, or - (at your option) any later version. - - This program is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License along - with this program; if not, write to the Free Software Foundation, Inc., - 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. - -Also add information on how to contact you by electronic and paper mail. - -If the program is interactive, make it output a short notice like this -when it starts in an interactive mode: - - Gnomovision version 69, Copyright (C) year name of author - Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'. - This is free software, and you are welcome to redistribute it - under certain conditions; type `show c' for details. - -The hypothetical commands `show w' and `show c' should show the appropriate -parts of the General Public License. Of course, the commands you use may -be called something other than `show w' and `show c'; they could even be -mouse-clicks or menu items--whatever suits your program. - -You should also get your employer (if you work as a programmer) or your -school, if any, to sign a "copyright disclaimer" for the program, if -necessary. Here is a sample; alter the names: - - Yoyodyne, Inc., hereby disclaims all copyright interest in the program - `Gnomovision' (which makes passes at compilers) written by James Hacker. - - , 1 April 1989 - Ty Coon, President of Vice - -This General Public License does not permit incorporating your program into -proprietary programs. If your program is a subroutine library, you may -consider it more useful to permit linking proprietary applications with the -library. If this is what you want to do, use the GNU Lesser General -Public License instead of this License. diff --git a/DeductiveSystemForCAP/PackageInfo.g b/DeductiveSystemForCAP/PackageInfo.g deleted file mode 100644 index e29fa660bd..0000000000 --- a/DeductiveSystemForCAP/PackageInfo.g +++ /dev/null @@ -1,102 +0,0 @@ -# SPDX-License-Identifier: GPL-2.0-or-later -# DeductiveSystemForCAP: Deductive system for CAP -# -# This file contains package meta data. For additional information on -# the meaning and correct usage of these fields, please consult the -# manual of the "Example" package as well as the comments in its -# PackageInfo.g file. -# -SetPackageInfo( rec( - -PackageName := "DeductiveSystemForCAP", -Subtitle := "Deductive system for CAP", -Version := "2023.03-03", -Date := (function ( ) if IsBound( GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE ) then return GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE; else return Concatenation( ~.Version{[ 1 .. 4 ]}, "-", ~.Version{[ 6, 7 ]}, "-01" ); fi; end)( ), -License := "GPL-2.0-or-later", - -Persons := [ - rec( - IsAuthor := true, - IsMaintainer := true, - FirstNames := "Sebastian", - LastName := "Gutsche", - WWWHome := "http://wwwb.math.rwth-aachen.de/~gutsche/", - Email := "gutsche@mathematik.uni-kl.de", - PostalAddress := Concatenation( - "Department of Mathematics\n", - "University of Kaiserslautern\n", - "67653 Kaiserslautern\n", - "Germany" ), - Place := "Kaiserslautern", - Institution := "University of Kaiserslautern", - ), - rec( - IsAuthor := true, - IsMaintainer := true, - FirstNames := "Sebastian", - LastName := "Posur", - WWWHome := "https://sebastianpos.github.io", - Email := "sposur@momo.math.rwth-aachen.de", - PostalAddress := Concatenation( - "Sebastian Posur\n", - "Lehrstuhl B fuer Mathematik, RWTH Aachen\n", - "Templergraben 64\n", - "52062 Aachen\n", - "Germany" ), - Place := "Aachen", - Institution := "RWTH Aachen University", - ), -], - -# BEGIN URLS -SourceRepository := rec( - Type := "git", - URL := "https://github.com/homalg-project/CAP_project", -), -IssueTrackerURL := Concatenation( ~.SourceRepository.URL, "/issues" ), -PackageWWWHome := "https://homalg-project.github.io/pkg/DeductiveSystemForCAP", -PackageInfoURL := "https://homalg-project.github.io/CAP_project/DeductiveSystemForCAP/PackageInfo.g", -README_URL := "https://homalg-project.github.io/CAP_project/DeductiveSystemForCAP/README.md", -ArchiveURL := Concatenation( "https://github.com/homalg-project/CAP_project/releases/download/DeductiveSystemForCAP-", ~.Version, "/DeductiveSystemForCAP-", ~.Version ), -# END URLS - -ArchiveFormats := ".tar.gz .zip", - -## Status information. Currently the following cases are recognized: -## "accepted" for successfully refereed packages -## "submitted" for packages submitted for the refereeing -## "deposited" for packages for which the GAP developers agreed -## to distribute them with the core GAP system -## "dev" for development versions of packages -## "other" for all other packages -## -Status := "dev", - -AbstractHTML := "", - -PackageDoc := rec( - BookName := "DeductiveSystemForCAP", - ArchiveURLSubset := ["doc"], - HTMLStart := "doc/chap0.html", - PDFFile := "doc/manual.pdf", - SixFile := "doc/manual.six", - LongTitle := "Deductive system for CAP", -), - -Dependencies := rec( - GAP := ">= 4.12.1", - NeededOtherPackages := [ [ "GAPDoc", ">= 1.5" ], - [ "CAP", ">= 2022.03-01" ] ], - SuggestedOtherPackages := [ ], - ExternalConditions := [ ], -), - -AvailabilityTest := function() - return true; - end, - -TestFile := "tst/testall.g", - -#Keywords := [ "TODO" ], - -)); diff --git a/DeductiveSystemForCAP/README.md b/DeductiveSystemForCAP/README.md deleted file mode 100644 index 4a1859400e..0000000000 --- a/DeductiveSystemForCAP/README.md +++ /dev/null @@ -1,32 +0,0 @@ - -# DeductiveSystemForCAP [![View code][code-img]][code-url] - -### Deductive system for CAP - -| Documentation | Latest Release | Build Status of [CAP_project](/../../) | Code Coverage | -| ------------- | -------------- | ------------ | ------------- | -| [![HTML stable documentation][html-img]][html-url] [![PDF stable documentation][pdf-img]][pdf-url] | [![version][version-img]][version-url] [![date][date-img]][date-url] | [![Build Status][tests-img]][tests-url] | [![Code Coverage][codecov-img]][codecov-url] | - - - -[html-img]: https://img.shields.io/badge/🔗%20HTML-stable-blue.svg -[html-url]: https://homalg-project.github.io/CAP_project/DeductiveSystemForCAP/doc/chap0_mj.html - -[pdf-img]: https://img.shields.io/badge/🔗%20PDF-stable-blue.svg -[pdf-url]: https://homalg-project.github.io/CAP_project/DeductiveSystemForCAP/download_pdf.html - -[version-img]: https://img.shields.io/endpoint?url=https://homalg-project.github.io/CAP_project/DeductiveSystemForCAP/badge_version.json&label=🔗%20version&color=yellow -[version-url]: https://homalg-project.github.io/CAP_project/DeductiveSystemForCAP/view_release.html - -[date-img]: https://img.shields.io/endpoint?url=https://homalg-project.github.io/CAP_project/DeductiveSystemForCAP/badge_date.json&label=🔗%20released%20on&color=yellow -[date-url]: https://homalg-project.github.io/CAP_project/DeductiveSystemForCAP/view_release.html - -[tests-img]: https://github.com/homalg-project/CAP_project/actions/workflows/Tests.yml/badge.svg?branch=master -[tests-url]: https://github.com/homalg-project/CAP_project/actions/workflows/Tests.yml?query=branch%3Amaster - -[codecov-img]: https://codecov.io/gh/homalg-project/CAP_project/branch/master/graph/badge.svg?flag=DeductiveSystemForCAP -[codecov-url]: https://app.codecov.io/gh/homalg-project/CAP_project/tree/master/DeductiveSystemForCAP - -[code-img]: https://img.shields.io/badge/-View%20code-blue?logo=github -[code-url]: https://github.com/homalg-project/CAP_project/tree/master/DeductiveSystemForCAP#top - diff --git a/DeductiveSystemForCAP/doc/Doc.autodoc b/DeductiveSystemForCAP/doc/Doc.autodoc deleted file mode 100644 index 1df78e94d6..0000000000 --- a/DeductiveSystemForCAP/doc/Doc.autodoc +++ /dev/null @@ -1 +0,0 @@ -@Chapter Deduction system diff --git a/DeductiveSystemForCAP/doc/clean b/DeductiveSystemForCAP/doc/clean deleted file mode 100755 index ffe1f90868..0000000000 --- a/DeductiveSystemForCAP/doc/clean +++ /dev/null @@ -1,2 +0,0 @@ -#!/bin/sh -rm -f *.{aux,bbl,blg,brf,css,html,idx,ilg,ind,js,lab,log,out,pdf,pnr,six,tex,toc,txt,xml,xml.bib} diff --git a/DeductiveSystemForCAP/examples/LogicExample.g b/DeductiveSystemForCAP/examples/LogicExample.g deleted file mode 100644 index 531bc529a6..0000000000 --- a/DeductiveSystemForCAP/examples/LogicExample.g +++ /dev/null @@ -1,40 +0,0 @@ -## Create the category of rational vector spaces - -if not IsBound( VectorSpacesConstructorsLoaded ) then - - ReadPackage( "CAP", "examples/VectorSpacesConstructors.g" );; - -fi; - -vecspaces := CreateCapCategory( "vecspaces" ); -vecspaces!.category_as_first_argument := false; -ReadPackage( "CAP", "examples/VectorSpacesAllMethods.g" ); - -## create example input - -A := QVectorSpace( 2 ); -B := QVectorSpace( 2 ); -alpha := VectorSpaceMorphism( A, [ [ 1, 1 ], [ 1, -1 ] ], A ); -A := InDeductiveSystem( A ); -B := InDeductiveSystem( B ); -alpha := InDeductiveSystem( alpha ); - -## operations - -# k := KernelEmbedding( alpha ); - -k := alpha; - -P := DirectProduct( A, A ); - -pi := ProjectionInFactorOfDirectProduct( [ A, A ], 1 ); - -F := FiberProduct( k, pi ); - -pr := ProjectionInFactor( F, 2 ); - -k2 := KernelObject( pr ); - -P2 := DirectProduct( k2, k2, k2 ); - -HasIsZero( P2 ); diff --git a/DeductiveSystemForCAP/examples/LogicKaiserslautern.g b/DeductiveSystemForCAP/examples/LogicKaiserslautern.g deleted file mode 100644 index ccc21749db..0000000000 --- a/DeductiveSystemForCAP/examples/LogicKaiserslautern.g +++ /dev/null @@ -1,47 +0,0 @@ -LoadPackage( "ModulePresentationsForCAP" ); - -LoadPackage( "RingsForHomalg" ); - -Q := HomalgFieldOfRationalsInSingular( ); - -R := Q * "x,y"; - -F := FreeLeftPresentation( 1, R ); - -alpha1 := PresentationMorphism( F, HomalgMatrix( "[ [ x ] ]", R ), F ); - -alpha2 := PresentationMorphism( F, HomalgMatrix( "[ [ y ] ]", R ), F ); - -## Initializing the deductive system - -# alpha1 := InDeductiveSystem( alpha1_eval ); -# -# alpha2 := InDeductiveSystem( alpha2_eval ); - -## Formal computation - -P := FiberProduct( alpha1, alpha2 ); - -pi1 := ProjectionInFactorOfFiberProduct( [ alpha1, alpha2 ], 1 ); - -composite := PreCompose( pi1, alpha1 ); - -PrintHistory( composite ); - -HasIsMonomorphism( composite ); - -IsMonomorphism( alpha1 ); - -IsMonomorphism( alpha2 ); - -HasEvaluation( composite ); - -HasIsMonomorphism( composite ); - -IsMonomorphism( composite ); - -HasEvaluation( composite ); - -Evaluation( composite ); - -HasEvaluation( composite ); diff --git a/DeductiveSystemForCAP/examples/ModulesOverPolynomialRing.g b/DeductiveSystemForCAP/examples/ModulesOverPolynomialRing.g deleted file mode 100644 index 3e10035b0f..0000000000 --- a/DeductiveSystemForCAP/examples/ModulesOverPolynomialRing.g +++ /dev/null @@ -1,45 +0,0 @@ -LoadPackage( "ModulePresentationsForCAP" ); - -LoadPackage( "RingsForHomalg" ); - -## Initialisation - -Q := HomalgFieldOfRationalsInSingular( ); - -R := Q * "x,y"; - -# R := R / "y - x - 1"; - -F := FreeLeftPresentation( 1, R ); - -I1 := AsLeftPresentation( HomalgMatrix( [ [ "x" ] ], R ) ); - -I2 := AsLeftPresentation( HomalgMatrix( [ [ "y" ] ], R ) ); - -eps1 := PresentationMorphism( F, HomalgMatrix( [ [ 1 ] ], R ), I1 ); - -eps2 := PresentationMorphism( F, HomalgMatrix( [ [ 1 ] ], R ), I2 ); - -F := InDeductiveSystem( F ); - -I1 := InDeductiveSystem( I1 ); - -I2 := InDeductiveSystem( I2 ); - -eps1 := InDeductiveSystem( eps1 ); - -eps2 := InDeductiveSystem( eps2 ); - -## Computation - -kernelemb1 := KernelEmbedding( eps1 ); - -kernelemb2 := KernelEmbedding( eps2 ); - -P := FiberProduct( kernelemb1, kernelemb2 ); - -pi1 := ProjectionInFactorOfFiberProduct( [ kernelemb1, kernelemb2 ], 1 ); - -composite := PreCompose( pi1, kernelemb1 ); - -e := Evaluation( composite ); diff --git a/DeductiveSystemForCAP/examples/SpectralSequenceKaiserslautern.g b/DeductiveSystemForCAP/examples/SpectralSequenceKaiserslautern.g deleted file mode 100644 index 85079435d3..0000000000 --- a/DeductiveSystemForCAP/examples/SpectralSequenceKaiserslautern.g +++ /dev/null @@ -1,75 +0,0 @@ -LoadPackage( "ModulePresentationsForCAP" ); -LoadPackage( "GeneralizedMorphismsForCAP" ); -LoadPackage( "RingsForHomalg" ); - -## Initialisation - -ZZ := HomalgRingOfIntegersInSingular( ); - -C1_eval := FreeLeftPresentation( 1, ZZ ); -C1 := InDeductiveSystem( C1_eval ); - -C2_eval := FreeLeftPresentation( 2, ZZ ); -C2 := InDeductiveSystem( C2_eval ); - -C3_eval := FreeLeftPresentation( 3, ZZ ); -C3 := InDeductiveSystem( C3_eval ); - -C4_eval := FreeLeftPresentation( 3, ZZ ); -C4 := InDeductiveSystem( C4_eval ); - -C5_eval := FreeLeftPresentation( 2, ZZ ); -C5 := InDeductiveSystem( C5_eval ); - -C6_eval := FreeLeftPresentation( 1, ZZ ); -C6 := InDeductiveSystem( C6_eval ); - -delta1_eval := PresentationMorphism( C1_eval, HomalgMatrix( [ [ 1, 0 ] ], ZZ ), C2_eval ); -delta1 := InDeductiveSystem( delta1_eval ); - -delta2_eval := PresentationMorphism( C3_eval, HomalgMatrix( [ [ 0, 0 ], [ 1, 0 ], [ 0, 1 ] ], ZZ ), C2_eval ); -delta2 := InDeductiveSystem( delta2_eval ); - -delta3_eval := PresentationMorphism( C3_eval, HomalgMatrix( [ [ 1, 0, 0 ], [ 0, 1, 0 ], [ 0, 0, 1 ] ], ZZ ), C4_eval ); -delta3 := InDeductiveSystem( delta3_eval ); - -delta4_eval := PresentationMorphism( C5_eval, HomalgMatrix( [ [ 1, 0, 0 ], [ 0, 1, 0 ] ], ZZ ), C4_eval ); -delta4 := InDeductiveSystem( delta4_eval ); - -delta5_eval := PresentationMorphism( C5_eval, HomalgMatrix( [ [ 0 ], [ 1 ] ], ZZ ), C6_eval ); -delta5 := InDeductiveSystem( delta5_eval ); - - -SetIsAbelianCategory( CapCategory( delta1 ), true ); - - -delta1_generalized := AsGeneralizedMorphism( delta1 ); - -delta2_generalized := AsGeneralizedMorphism( delta2 ); - -delta3_generalized := AsGeneralizedMorphism( delta3 ); - -delta4_generalized := AsGeneralizedMorphism( delta4 ); - -delta5_generalized := AsGeneralizedMorphism( delta5 ); - - -connecting_morphism := delta1_generalized; - -connecting_morphism := PreCompose( connecting_morphism, PseudoInverse( delta2_generalized ) ); - -connecting_morphism := PreCompose( connecting_morphism, delta3_generalized ); - -connecting_morphism := PreCompose( connecting_morphism, PseudoInverse( delta4_generalized ) ); - -connecting_morphism := PreCompose( connecting_morphism, delta5_generalized ); - -c := AssociatedMorphism( connecting_morphism ); - -c_eval := Evaluation( c ); - -c_eval_less_generators := ApplyFunctor( FunctorLessGeneratorsLeft( ZZ ), c_eval ); - -Display( UnderlyingMatrix( c_eval_less_generators ) ); - - diff --git a/DeductiveSystemForCAP/examples/SpectralSequenceKaiserslauternWithCospans.g b/DeductiveSystemForCAP/examples/SpectralSequenceKaiserslauternWithCospans.g deleted file mode 100644 index 8adc3c504f..0000000000 --- a/DeductiveSystemForCAP/examples/SpectralSequenceKaiserslauternWithCospans.g +++ /dev/null @@ -1,65 +0,0 @@ -LoadPackage( "ModulePresentationsForCAP" ); -LoadPackage( "GeneralizedMorphismsForCAP" ); -LoadPackage( "RingsForHomalg" ); - -## Initialisation - -ZZ := HomalgRingOfIntegersInSingular( ); - -C1_eval := FreeLeftPresentation( 1, ZZ ); -C1 := InDeductiveSystem( C1_eval ); - -C2_eval := FreeLeftPresentation( 2, ZZ ); -C2 := InDeductiveSystem( C2_eval ); - -C3_eval := FreeLeftPresentation( 3, ZZ ); -C3 := InDeductiveSystem( C3_eval ); - -C4_eval := FreeLeftPresentation( 3, ZZ ); -C4 := InDeductiveSystem( C4_eval ); - -C5_eval := FreeLeftPresentation( 2, ZZ ); -C5 := InDeductiveSystem( C5_eval ); - -C6_eval := FreeLeftPresentation( 1, ZZ ); -C6 := InDeductiveSystem( C6_eval ); - -delta1_eval := PresentationMorphism( C1_eval, HomalgMatrix( [ [ 1, 0 ] ], ZZ ), C2_eval ); -delta1 := InDeductiveSystem( delta1_eval ); - -delta2_eval := PresentationMorphism( C3_eval, HomalgMatrix( [ [ 0, 0 ], [ 1, 0 ], [ 0, 1 ] ], ZZ ), C2_eval ); -delta2 := InDeductiveSystem( delta2_eval ); - -delta3_eval := PresentationMorphism( C3_eval, HomalgMatrix( [ [ 1, 0, 0 ], [ 0, 1, 0 ], [ 0, 0, 1 ] ], ZZ ), C4_eval ); -delta3 := InDeductiveSystem( delta3_eval ); - -delta4_eval := PresentationMorphism( C5_eval, HomalgMatrix( [ [ 1, 0, 0 ], [ 0, 1, 0 ] ], ZZ ), C4_eval ); -delta4 := InDeductiveSystem( delta4_eval ); - -delta5_eval := PresentationMorphism( C5_eval, HomalgMatrix( [ [ 0 ], [ 1 ] ], ZZ ), C6_eval ); -delta5 := InDeductiveSystem( delta5_eval ); - - -SetIsAbelianCategory( CapCategory( delta1 ), true ); - - -cospan1 := GeneralizedMorphismWithRangeAid( delta1, delta2 ); - -cospan2 := GeneralizedMorphismWithRangeAid( delta3, delta4 ); - -delta5_generalized := AsGeneralizedMorphism( delta5 ); - -connecting_morphism := PreCompose( cospan1, cospan2 ); - -connecting_morphism := PreCompose( connecting_morphism, delta5_generalized ); - -c := AssociatedMorphism( connecting_morphism ); - -c_eval := Evaluation( c ); - -c_eval_less_generators := ApplyFunctor( FunctorLessGeneratorsLeft( ZZ ), c_eval ); - -Display( UnderlyingMatrix( c_eval_less_generators ) ); - -QUIT; - diff --git a/DeductiveSystemForCAP/examples/SpectralSequenceKaiserslauternWithCospansToDoListTest.g b/DeductiveSystemForCAP/examples/SpectralSequenceKaiserslauternWithCospansToDoListTest.g deleted file mode 100644 index 93b6d63ac6..0000000000 --- a/DeductiveSystemForCAP/examples/SpectralSequenceKaiserslauternWithCospansToDoListTest.g +++ /dev/null @@ -1,69 +0,0 @@ -LoadPackage( "ToolsForHomalg" ); - -ShowToDoListInfo( ); - -LoadPackage( "ModulePresentationsForCAP" ); -LoadPackage( "GeneralizedMorphismsForCAP" ); -LoadPackage( "RingsForHomalg" ); - -## Initialisation - -ZZ := HomalgRingOfIntegersInSingular( ); - -C1_eval := FreeLeftPresentation( 1, ZZ ); -C1 := InDeductiveSystem( C1_eval ); - -C2_eval := FreeLeftPresentation( 2, ZZ ); -C2 := InDeductiveSystem( C2_eval ); - -C3_eval := FreeLeftPresentation( 3, ZZ ); -C3 := InDeductiveSystem( C3_eval ); - -C4_eval := FreeLeftPresentation( 3, ZZ ); -C4 := InDeductiveSystem( C4_eval ); - -C5_eval := FreeLeftPresentation( 2, ZZ ); -C5 := InDeductiveSystem( C5_eval ); - -C6_eval := FreeLeftPresentation( 1, ZZ ); -C6 := InDeductiveSystem( C6_eval ); - -delta1_eval := PresentationMorphism( C1_eval, HomalgMatrix( [ [ 1, 0 ] ], ZZ ), C2_eval ); -delta1 := InDeductiveSystem( delta1_eval ); - -delta2_eval := PresentationMorphism( C3_eval, HomalgMatrix( [ [ 0, 0 ], [ 1, 0 ], [ 0, 1 ] ], ZZ ), C2_eval ); -delta2 := InDeductiveSystem( delta2_eval ); - -delta3_eval := PresentationMorphism( C3_eval, HomalgMatrix( [ [ 1, 0, 0 ], [ 0, 1, 0 ], [ 0, 0, 1 ] ], ZZ ), C4_eval ); -delta3 := InDeductiveSystem( delta3_eval ); - -delta4_eval := PresentationMorphism( C5_eval, HomalgMatrix( [ [ 1, 0, 0 ], [ 0, 1, 0 ] ], ZZ ), C4_eval ); -delta4 := InDeductiveSystem( delta4_eval ); - -delta5_eval := PresentationMorphism( C5_eval, HomalgMatrix( [ [ 0 ], [ 1 ] ], ZZ ), C6_eval ); -delta5 := InDeductiveSystem( delta5_eval ); - - -SetIsAbelianCategory( CapCategory( delta1 ), true ); - - -cospan1 := GeneralizedMorphismWithRangeAid( delta1, delta2 ); - -cospan2 := GeneralizedMorphismWithRangeAid( delta3, delta4 ); - -delta5_generalized := AsGeneralizedMorphism( delta5 ); - -connecting_morphism := PreCompose( cospan1, cospan2 ); - -connecting_morphism := PreCompose( connecting_morphism, delta5_generalized ); - -c := AssociatedMorphism( connecting_morphism ); - -c_eval := Evaluation( c ); - -c_eval_less_generators := ApplyFunctor( FunctorLessGeneratorsLeft( ZZ ), c_eval ); - -Display( UnderlyingMatrix( c_eval_less_generators ) ); - -QUIT; - diff --git a/DeductiveSystemForCAP/examples/VectorSpaces.g b/DeductiveSystemForCAP/examples/VectorSpaces.g deleted file mode 100644 index b48b905dbb..0000000000 --- a/DeductiveSystemForCAP/examples/VectorSpaces.g +++ /dev/null @@ -1,1029 +0,0 @@ - -LoadPackage( "CAP" ); - -LoadPackage( "DeductiveSystemForCAP" ); - -LoadPackage( "MatricesForHomalg" ); - -LoadPackage( "GaussForHomalg" ); - -#ProfileFunctionsInGlobalVariables( true ); -#ProfileOperationsAndMethods( true ); -#ProfileGlobalFunctions( true ); - -ProfileMethods( IsEqualForCache ); - -################################### -## -## Types and Representations -## -################################### - -DeclareRepresentation( "IsHomalgRationalVectorSpaceRep", - IsCapCategoryObjectRep, - [ ] ); - -BindGlobal( "TheTypeOfHomalgRationalVectorSpaces", - NewType( TheFamilyOfCapCategoryObjects, - IsHomalgRationalVectorSpaceRep ) ); - -DeclareRepresentation( "IsHomalgRationalVectorSpaceMorphismRep", - IsCapCategoryMorphismRep, - [ ] ); - -BindGlobal( "TheTypeOfHomalgRationalVectorSpaceMorphism", - NewType( TheFamilyOfCapCategoryMorphisms, - IsHomalgRationalVectorSpaceMorphismRep ) ); - -################################### -## -## Attributes -## -################################### - -DeclareAttribute( "Dimension", - IsHomalgRationalVectorSpaceRep ); - -####################################### -## -## Operations -## -####################################### - -DeclareOperation( "QVectorSpace", - [ IsInt ] ); - -DeclareOperation( "VectorSpaceMorphism", - [ IsHomalgRationalVectorSpaceRep, IsObject, IsHomalgRationalVectorSpaceRep ] ); - -vecspaces := CreateCapCategory( "VectorSpaces" ); - -vecspaces!.category_as_first_argument := false; - -SetIsAbelianCategory( vecspaces, true ); - -VECTORSPACES_FIELD := HomalgFieldOfRationals( ); - -####################################### -## -## Categorical Implementations -## -####################################### - -## -InstallMethod( QVectorSpace, - [ IsInt ], - - function( dim ) - local space; - - space := ObjectifyWithAttributes( rec( ), TheTypeOfHomalgRationalVectorSpaces, - Dimension, dim - ); - - # is this the right place? - Add( vecspaces, space ); - - return space; - -end ); - -## -InstallMethod( VectorSpaceMorphism, - [ IsHomalgRationalVectorSpaceRep, IsObject, IsHomalgRationalVectorSpaceRep ], - - function( source, matrix, range ) - local morphism, objectified_morphism; - - if not IsHomalgMatrix( matrix ) then - - morphism := HomalgMatrix( matrix, Dimension( source ), Dimension( range ), VECTORSPACES_FIELD ); - - else - - morphism := matrix; - - fi; - - morphism := rec( morphism := morphism ); - - objectified_morphism := ObjectifyWithAttributes( morphism, TheTypeOfHomalgRationalVectorSpaceMorphism, - Source, source, - Range, range - ); - - Add( vecspaces, objectified_morphism ); - - return objectified_morphism; - -end ); - -AddIsEqualForMorphisms( vecspaces, - - function( a, b ) - - return a!.morphism = b!.morphism; - -end ); - -AddIsCongruentForMorphisms( vecspaces, - - function( a, b ) - - return a!.morphism = b!.morphism; - -end ); - -AddIsZeroForMorphisms( vecspaces, - - function( a ) - - return IsZero( a!.morphism ); - -end ); - -AddAdditionForMorphisms( vecspaces, - - function( a, b ) - - return VectorSpaceMorphism( Source( a ), a!.morphism + b!.morphism, Range( a ) ); - -end ); - -AddAdditiveInverseForMorphisms( vecspaces, - - function( a ) - - return VectorSpaceMorphism( Source( a ), - a!.morphism, Range( a ) ); - -end ); - -AddZeroMorphism( vecspaces, - - function( a, b ) - - return VectorSpaceMorphism( a, HomalgZeroMatrix( Dimension( a ), Dimension( b ), VECTORSPACES_FIELD ), b ); - -end ); - -## -AddIdentityMorphism( vecspaces, - - function( obj ) - - return VectorSpaceMorphism( obj, HomalgIdentityMatrix( Dimension( obj ), VECTORSPACES_FIELD ), obj ); - -end ); - -## -AddPreCompose( vecspaces, - - function( mor_left, mor_right ) - local composition; - - composition := mor_left!.morphism * mor_right!.morphism; - - return VectorSpaceMorphism( Source( mor_left ), composition, Range( mor_right ) ); - -end ); - -## -AddZeroObject( vecspaces, - - function( ) - - return QVectorSpace( 0 ); - -end ); - -## -AddLiftAlongMonomorphism( vecspaces, - - function( monomorphism, test_morphism ) - - return VectorSpaceMorphism( Source( test_morphism ), RightDivide( test_morphism!.morphism, monomorphism!.morphism ), Source( monomorphism ) ); - -end ); - -## -AddColiftAlongEpimorphism( vecspaces, - - function( epimorphism, test_morphism ) - - return VectorSpaceMorphism( Range( epimorphism ), LeftDivide( epimorphism!.morphism, test_morphism!.morphism ), Range( test_morphism ) ); - -end ); - -## -AddKernelObject( vecspaces, - - function( morphism ) - local homalg_matrix; - - homalg_matrix := morphism!.morphism; - - return QVectorSpace( NrRows( homalg_matrix ) - RowRankOfMatrix( homalg_matrix ) ); - -end ); - -## -AddKernelEmbedding( vecspaces, - - function( morphism ) - local kernel_emb, kernel_obj; - - kernel_emb := SyzygiesOfRows( morphism!.morphism ); - - kernel_obj := QVectorSpace( NrRows( kernel_emb ) ); - - return VectorSpaceMorphism( kernel_obj, kernel_emb, Source( morphism ) ); - -end ); - -## -AddKernelEmbeddingWithGivenKernelObject( vecspaces, - - function( morphism, kernel ) - local kernel_emb; - - kernel_emb := SyzygiesOfRows( morphism!.morphism ); - - return VectorSpaceMorphism( kernel, kernel_emb, Source( morphism ) ); - -end ); - -## -AddCokernelObject( vecspaces, - - function( morphism ) - local homalg_matrix; - - homalg_matrix := morphism!.morphism; - - return QVectorSpace( NrColumns( homalg_matrix ) - RowRankOfMatrix( homalg_matrix ) ); - -end ); - - -## -AddCokernelProjection( vecspaces, - - function( morphism ) - local cokernel_proj, cokernel_obj; - - cokernel_proj := SyzygiesOfColumns( morphism!.morphism ); - - cokernel_obj := QVectorSpace( NrColumns( cokernel_proj ) ); - - return VectorSpaceMorphism( Range( morphism ), cokernel_proj, cokernel_obj ); - -end ); - -## -AddCokernelProjectionWithGivenCokernelObject( vecspaces, - - function( morphism, cokernel ) - local cokernel_proj; - - cokernel_proj := SyzygiesOfColumns( morphism!.morphism ); - - return VectorSpaceMorphism( Range( morphism ), cokernel_proj, cokernel ); - -end ); - -# ## -# AddCoproduct( vecspaces, -# -# function( object_product_list ) -# local dim; -# -# dim := Sum( List( object_product_list, c -> Dimension( c ) ) ); -# -# return QVectorSpace( dim ); -# -# end ); - -## -## the user may assume that Length( object_product_list ) > 1 -AddInjectionOfCofactorOfDirectSum( vecspaces, - - function( object_product_list, injection_number ) - local components, dim, dim_pre, dim_post, dim_cofactor, coproduct, number_of_objects, injection_of_cofactor; - - components := object_product_list; - - number_of_objects := Length( components ); - - dim := Sum( components, c -> Dimension( c ) ); - - dim_pre := Sum( components{ [ 1 .. injection_number - 1 ] }, c -> Dimension( c ) ); - - dim_post := Sum( components{ [ injection_number + 1 .. number_of_objects ] }, c -> Dimension( c ) ); - - dim_cofactor := Dimension( object_product_list[ injection_number ] ); - - coproduct := QVectorSpace( dim ); - - injection_of_cofactor := HomalgZeroMatrix( dim_cofactor, dim_pre ,VECTORSPACES_FIELD ); - - injection_of_cofactor := UnionOfColumns( injection_of_cofactor, - HomalgIdentityMatrix( dim_cofactor, VECTORSPACES_FIELD ) ); - - injection_of_cofactor := UnionOfColumns( injection_of_cofactor, - HomalgZeroMatrix( dim_cofactor, dim_post, VECTORSPACES_FIELD ) ); - - return VectorSpaceMorphism( object_product_list[ injection_number ], injection_of_cofactor, coproduct ); - -end ); - -## -## the user may assume that Length( object_product_list ) > 1 -AddInjectionOfCofactorOfDirectSumWithGivenDirectSum( vecspaces, - - function( object_product_list, injection_number, coproduct ) - local components, dim_pre, dim_post, dim_cofactor, number_of_objects, injection_of_cofactor; - - components := object_product_list; - - number_of_objects := Length( object_product_list ); - - dim_pre := Sum( components{ [ 1 .. injection_number - 1 ] }, c -> Dimension( c ) ); - - dim_post := Sum( components{ [ injection_number + 1 .. number_of_objects ] }, c -> Dimension( c ) ); - - dim_cofactor := Dimension( object_product_list[ injection_number ] ); - - injection_of_cofactor := HomalgZeroMatrix( dim_cofactor, dim_pre ,VECTORSPACES_FIELD ); - - injection_of_cofactor := UnionOfColumns( injection_of_cofactor, - HomalgIdentityMatrix( dim_cofactor, VECTORSPACES_FIELD ) ); - - injection_of_cofactor := UnionOfColumns( injection_of_cofactor, - HomalgZeroMatrix( dim_cofactor, dim_post, VECTORSPACES_FIELD ) ); - - return VectorSpaceMorphism( object_product_list[ injection_number ], injection_of_cofactor, coproduct ); - -end ); - -## -AddUniversalMorphismFromDirectSum( vecspaces, - - function( diagram, test_object, sink ) - local dim, coproduct, components, universal_morphism, morphism; - - components := sink; - - dim := Sum( components, c -> Dimension( Source( c ) ) ); - - coproduct := QVectorSpace( dim ); - - universal_morphism := sink[1]!.morphism; - - for morphism in components{ [ 2 .. Length( components ) ] } do - - universal_morphism := UnionOfRows( universal_morphism, morphism!.morphism ); - - od; - - return VectorSpaceMorphism( coproduct, universal_morphism, Range( sink[1] ) ); - -end ); - -## -AddUniversalMorphismFromDirectSumWithGivenDirectSum( vecspaces, - - function( diagram, test_object, sink, coproduct ) - local components, universal_morphism, morphism; - - components := sink; - - universal_morphism := sink[1]!.morphism; - - for morphism in components{ [ 2 .. Length( components ) ] } do - - universal_morphism := UnionOfRows( universal_morphism, morphism!.morphism ); - - od; - - return VectorSpaceMorphism( coproduct, universal_morphism, Range( sink[1] ) ); - -end ); - -## -AddDirectSum( vecspaces, - - function( object_product_list ) - local dim; - - dim := Sum( List( object_product_list, c -> Dimension( c ) ) ); - - return QVectorSpace( dim ); - -end ); - -# ## -# AddDirectProduct( vecspaces, -# -# function( object_product_list ) -# local dim; -# -# dim := Sum( List( object_product_list, c -> Dimension( c ) ) ); -# -# return QVectorSpace( dim ); -# -# end ); - -# -# the user may assume that Length( object_product_list ) > 1 -AddProjectionInFactorOfDirectSum( vecspaces, - - function( object_product_list, projection_number ) - local components, dim, dim_pre, dim_post, dim_factor, direct_product, number_of_objects, projection_in_factor; - - components := object_product_list; - - number_of_objects := Length( components ); - - dim := Sum( components, c -> Dimension( c ) ); - - dim_pre := Sum( components{ [ 1 .. projection_number - 1 ] }, c -> Dimension( c ) ); - - dim_post := Sum( components{ [ projection_number + 1 .. number_of_objects ] }, c -> Dimension( c ) ); - - dim_factor := Dimension( object_product_list[ projection_number ] ); - - direct_product := QVectorSpace( dim ); - - projection_in_factor := HomalgZeroMatrix( dim_pre, dim_factor, VECTORSPACES_FIELD ); - - projection_in_factor := UnionOfRows( projection_in_factor, - HomalgIdentityMatrix( dim_factor, VECTORSPACES_FIELD ) ); - - projection_in_factor := UnionOfRows( projection_in_factor, - HomalgZeroMatrix( dim_post, dim_factor, VECTORSPACES_FIELD ) ); - - return VectorSpaceMorphism( direct_product, projection_in_factor, object_product_list[ projection_number ] ); - -end ); - -## -## the user may assume that Length( object_product_list ) > 1 -AddProjectionInFactorOfDirectSumWithGivenDirectSum( vecspaces, - - function( object_product_list, projection_number, direct_product ) - local components, dim_pre, dim_post, dim_factor, number_of_objects, projection_in_factor; - - components := object_product_list; - - number_of_objects := Length( components ); - - dim_pre := Sum( components{ [ 1 .. projection_number - 1 ] }, c -> Dimension( c ) ); - - dim_post := Sum( components{ [ projection_number + 1 .. number_of_objects ] }, c -> Dimension( c ) ); - - dim_factor := Dimension( object_product_list[ projection_number ] ); - - projection_in_factor := HomalgZeroMatrix( dim_pre, dim_factor, VECTORSPACES_FIELD ); - - projection_in_factor := UnionOfRows( projection_in_factor, - HomalgIdentityMatrix( dim_factor, VECTORSPACES_FIELD ) ); - - projection_in_factor := UnionOfRows( projection_in_factor, - HomalgZeroMatrix( dim_post, dim_factor, VECTORSPACES_FIELD ) ); - - return VectorSpaceMorphism( direct_product, projection_in_factor, object_product_list[ projection_number ] ); - -end ); - -AddUniversalMorphismIntoDirectSum( vecspaces, - - function( diagram, test_object, sink ) - local dim, direct_product, components, universal_morphism, morphism; - - components := sink; - - dim := Sum( components, c -> Dimension( Range( c ) ) ); - - direct_product := QVectorSpace( dim ); - - universal_morphism := sink[1]!.morphism; - - for morphism in components{ [ 2 .. Length( components ) ] } do - - universal_morphism := UnionOfColumns( universal_morphism, morphism!.morphism ); - - od; - - return VectorSpaceMorphism( Source( sink[1] ), universal_morphism, direct_product ); - -end ); - -AddUniversalMorphismIntoDirectSumWithGivenDirectSum( vecspaces, - - function( diagram, test_object, sink, direct_product ) - local components, universal_morphism, morphism; - - components := sink; - - universal_morphism := sink[1]!.morphism; - - for morphism in components{ [ 2 .. Length( components ) ] } do - - universal_morphism := UnionOfColumns( universal_morphism, morphism!.morphism ); - - od; - - return VectorSpaceMorphism( Source( sink[1] ), universal_morphism, direct_product ); - -end ); - -## -AddUniversalMorphismIntoZeroObject( vecspaces, - - function( sink ) - local morphism; - - morphism := VectorSpaceMorphism( sink, HomalgZeroMatrix( Dimension( sink ), 0, VECTORSPACES_FIELD ), QVectorSpace( 0 ) ); - - return morphism; - -end ); - -## -AddUniversalMorphismIntoZeroObjectWithGivenZeroObject( vecspaces, - - function( sink, terminal_object ) - local morphism; - - morphism := VectorSpaceMorphism( sink, HomalgZeroMatrix( Dimension( sink ), 0, VECTORSPACES_FIELD ), terminal_object ); - - return morphism; - -end ); - -## -AddZeroObject( vecspaces, - - function( ) - - return QVectorSpace( 0 ); - -end ); - -## -AddUniversalMorphismFromZeroObject( vecspaces, - - function( source ) - local morphism; - - morphism := VectorSpaceMorphism( QVectorSpace( 0 ), HomalgZeroMatrix( 0, Dimension( source ), VECTORSPACES_FIELD ), source ); - - return morphism; - -end ); - -## -AddUniversalMorphismFromZeroObjectWithGivenZeroObject( vecspaces, - - function( source, initial_object ) - local morphism; - - morphism := VectorSpaceMorphism( initial_object, HomalgZeroMatrix( 0, Dimension( source ), VECTORSPACES_FIELD ), source ); - - return morphism; - -end ); - -## -AddIsWellDefinedForObjects( vecspaces, - - function( vectorspace ) - - return IsHomalgRationalVectorSpaceRep( vectorspace ) and Dimension( vectorspace ) >= 0; - -end ); - -## -AddIsWellDefinedForMorphisms( vecspaces, - - function( morphism ) - local matrix; - - if not IsHomalgRationalVectorSpaceMorphismRep( morphism ) then - return false; - fi; - - matrix := morphism!.morphism; - - return IsHomalgMatrix( matrix ) - and NrRows( matrix ) = Dimension( Source( morphism ) ) - and NrColumns( matrix ) = Dimension( Range( morphism ) ); - -end ); -# -# AddIsZeroForObjects( vecspaces, -# -# function( obj ) -# -# return Dimension( obj ) = 0; -# -# end ); -# -# AddIsMonomorphism( vecspaces, -# -# function( morphism ) -# -# return RowRankOfMatrix( morphism!.morphism ) = Dimension( Source( morphism ) ); -# -# end ); -# -# AddIsEpimorphism( vecspaces, -# -# function( morphism ) -# -# return ColumnRankOfMatrix( morphism!.morphism ) = Dimension( Range( morphism ) ); -# -# end ); -# -# AddIsIsomorphism( vecspaces, -# -# function( morphism ) -# -# return Dimension( Range( morphism ) ) = Dimension( Source( morphism ) ) -# and ColumnRankOfMatrix( morphism!.morphism ) = Dimension( Range( morphism ) ); -# -# end ); - -# ## -# AddImageObject( vecspaces, -# -# function( morphism ) -# -# return QVectorSpace( RowRankOfMatrix( morphism!.morphism ) ); -# -# end ); - -AddIsEqualForObjects( vecspaces, - - function( vecspace_1, vecspace_2 ) - - return Dimension( vecspace_1 ) = Dimension( vecspace_2 ); - -end ); - -Finalize( vecspaces ); - -####################################### -## -## View and Display -## -####################################### - -InstallMethod( ViewString, - [ IsHomalgRationalVectorSpaceRep ], - - function( obj ) - - return Concatenation( "" ); - -end ); - -InstallMethod( ViewString, - [ IsHomalgRationalVectorSpaceMorphismRep ], - - function( obj ) - - return Concatenation( "A rational vector space homomorphism with matrix: \n", StringDisplay( obj!.morphism ) ); - -end ); - -####################################### -## -## Test -## -####################################### - -T := QVectorSpace( 2 ); - -B := QVectorSpace( 2 ); - -A := QVectorSpace( 1 ); - -C := QVectorSpace( 3 ); - -D := QVectorSpace( 1 ); - -f := VectorSpaceMorphism( B, [ [ 1 ], [ 1 ] ], A ); - -g := VectorSpaceMorphism( C, [ [ 1 ], [ -1 ], [ 1 ] ], A ); - -t1 := VectorSpaceMorphism( D, [ [ 1, 1 ] ], B ); - -t2 := VectorSpaceMorphism( D, [ [ 1, 0, 1 ] ], C ); - -# KernelLift Test: -tau := VectorSpaceMorphism( T, [ [ 1, 1 ], [ 1, 1 ] ], B ); - -theta := VectorSpaceMorphism( A, [ [ 2, -2 ] ], T ); - -# KernelLift( tau, theta ); -# -# # Inverse Test -# alpha := VectorSpaceMorphism( T, [ [ 1, 2 ], [ 3, 4 ] ], B ); -# -# Inverse( alpha ); -# -# #CokernelColift Test: -# tau2 := VectorSpaceMorphism( B, [ [ 1, 1 ], [ 1, 1 ] ], T ); -# -# CokernelColift( theta, tau2 ); - -# Universal morphism of direct product - -alpha := VectorSpaceMorphism( T, [ [ 3 ], [ 4 ] ], A ); - -beta := VectorSpaceMorphism( T, [ [ 1, 1 ], [ 1, 1 ] ], B ); - -gamma := VectorSpaceMorphism( T, [ [ 1, 2 ], [ 3, 4 ] ], B ); - -####################################### -## -## Snake-Lemma test -## -####################################### - -eta := VectorSpaceMorphism( T, [ [ 1, 1 ], [ 2, 2 ] ], T ); - -eta := InDeductiveSystem( eta ); - -SetIsAbelianCategory( CapCategory( eta ), true ); - -####################################### -## -## Functorial methods tests -## -####################################### - -A := QVectorSpace( 2 ); - -A_p := QVectorSpace( 2 ); - -B := QVectorSpace( 2 ); - -B_p := QVectorSpace( 2 ); - -alpha := VectorSpaceMorphism( A, [ [ 0, 0 ], [ 0, 1 ] ], B ); - -alpha_p := VectorSpaceMorphism( A_p, [ [ 0, 0 ], [ 0, 1 ] ], B_p ); - -mu := VectorSpaceMorphism( A, [ [ 1, 0 ], [ 0, 0 ] ], A_p ); - -nu := VectorSpaceMorphism( B, [ [ 1, 0 ], [ 0, 0 ] ], B_p ); - -# KernelObjectFunctorial( mu, alpha, nu ); - -####################################### -## -## Functors -## -####################################### - -Tensor_Product_For_VecSpaces := CapFunctor( "Tensor_Product_For_VecSpaces", Product( vecspaces, vecspaces ), vecspaces ); - -AddObjectFunction( Tensor_Product_For_VecSpaces, - - function( vecspace_pair ) - - return QVectorSpace( Dimension( vecspace_pair[ 1 ] ) * Dimension( vecspace_pair[ 2 ] ) ); - -end ); - -AddMorphismFunction( Tensor_Product_For_VecSpaces, - - function( new_source, morphism, new_range ) - - return VectorSpaceMorphism( new_source, KroneckerMat( morphism[ 1 ]!.morphism, morphism[ 2 ]!.morphism ), new_range ); - -end ); - -Change_Components := CapFunctor( "change_components", Product( vecspaces, vecspaces ), Product( vecspaces, vecspaces ) ); - -AddObjectFunction( Change_Components, - - function( vecspace_pair ) - - return Product( vecspace_pair[ 2 ], vecspace_pair[ 1 ] ); - -end ); - -AddMorphismFunction( Change_Components, - - function( new_source, morphism_pair, new_range ) - - return Product( morphism_pair[ 2 ], morphism_pair[ 1 ] ); - -end ); - -#################################### -## -## Generalized morphisms -## -#################################### - -## use tau as associated morphism - -# tau_source_aid := VectorSpaceMorphism( Source( tau ), [ [ 1, 1, 0 ], [ 0, 1, 1 ] ], QVectorSpace( 3 ) ); -# -# tau_range_aid := VectorSpaceMorphism( QVectorSpace( 3 ), [ [ 1, 0 ], [ 1, 1 ], [ 0, 1 ] ], Range( tau ) ); -# -# GeneralizedMorphism( tau_source_aid, tau, tau_range_aid ); -# -# ## -# -# BB := QVectorSpace( 3 ); -# -# factor := VectorSpaceMorphism( BB, [ [ 1, -1 ], [ 3, 7 ], [ 21, 4 ] ], QVectorSpace( 2 ) ); -# -# sub := VectorSpaceMorphism( QVectorSpace( 2 ), [ [ 1, -1, 2 ], [ 3, -1, 11 ] ], BB ); -# -# # factor := VectorSpaceMorphism( BB, [ [ 1 ], [ 3 ], [ 21 ] ], QVectorSpace( 1 ) ); -# # -# # sub := VectorSpaceMorphism( QVectorSpace( 2 ), [ [ 1, -1, 2 ], [ 3, -1, 11 ] ], BB ); -# -# # factor := VectorSpaceMorphism( BB, [ ], QVectorSpace( 0 ) ); -# # -# # sub := VectorSpaceMorphism( QVectorSpace( 2 ), [ [ 1, -1, 2 ], [ 3, -1, 11 ] ], BB ); -# -# # factor := VectorSpaceMorphism( BB, [ [ 1 ], [ 3 ], [ 21 ] ], QVectorSpace( 1 ) ); -# # -# # sub := VectorSpaceMorphism( QVectorSpace( 0 ), [ ], BB ); -# -# phi_tilde_associated := VectorSpaceMorphism( A, [ [ 1, 2, 0 ] ], C ); -# -# phi_tilde_source_aid := VectorSpaceMorphism( A, [ [ 1, 2 ] ], B ); -# -# phi_tilde := GeneralizedMorphismWithSourceAid( phi_tilde_source_aid, phi_tilde_associated ); -# -# psi_tilde_associated := IdentityMorphism( B ); -# -# psi_tilde_source_aid := VectorSpaceMorphism( B, [ [ 1, 0, 0 ] ,[ 0, 1, 0 ] ], C ); -# -# psi_tilde := GeneralizedMorphismWithSourceAid( psi_tilde_source_aid, psi_tilde_associated ); -# -# PreCompose( phi_tilde, psi_tilde ); -# -# phi2_tilde_associated := VectorSpaceMorphism( A, [ [ 1, 5 ] ], B ); -# -# phi2_tilde_range_aid := VectorSpaceMorphism( C, [ [ 1, 0 ], [ 0, 1 ], [ 1, 1 ] ], B ); -# -# phi2_tilde := GeneralizedMorphismWithRangeAid( phi2_tilde_associated, phi2_tilde_range_aid ); -# -# psi2_tilde_associated := VectorSpaceMorphism( C, [ [ 1 ], [ 3 ], [ 4 ] ], A ); -# -# psi2_tilde_range_aid := VectorSpaceMorphism( B, [ [ 1 ], [ 1 ] ], A ); -# -# psi2_tilde := GeneralizedMorphismWithRangeAid( psi2_tilde_associated, psi2_tilde_range_aid ); -# -# composition := PreCompose( phi2_tilde, psi2_tilde ); - -# phi3_associated := VectorSpaceMorphism( B, [ [ 1, 0 ], [ 0, 1 ] ], B ); -# -# phi3_range_aid := VectorSpaceMorphism( C, [ [ 1, 0 ], [ 0, 1 ], [ 0, 0 ] ], B ); -# -# psi3_associated := VectorSpaceMorphism( B, [ [ 1, 0 ], [ 0, 1 ] ], B ); -# -# psi3_source_aid := VectorSpaceMorphism( B, [ [ 0,1,0],[0,0,1]], C ); -# -# phi3 := GeneralizedMorphismWithRangeAid( phi3_associated, phi3_range_aid ); -# -# psi3 := GeneralizedMorphismWithSourceAid( psi3_source_aid, psi3_associated ); -# -# PreCompose( phi3, psi3 ); - -#################################### -## -## Natural transformation -## -#################################### - -## -identity_functor := IdentityMorphism( AsCatObject( vecspaces ) ); - -## -zero_object := CapFunctor( "Zero functor of VectorSpaces", vecspaces, vecspaces ); - -AddObjectFunction( zero_object, - - function( obj ) - - return ZeroObject( obj ); - -end ); - -AddMorphismFunction( zero_object, - - function( zero1, morphism, zero2 ) - - return VectorSpaceMorphism( zero1, [ ], zero2 ); - -end ); - -id_to_zero := NaturalTransformation( "One to zero in VectorSpaces", identity_functor, zero_object ); - -# psi3 := GeneralizedMorphismWithSourceAid( psi3_source_aid, psi3_associated ); -# -# PreCompose( phi3, psi3 ); - -AddNaturalTransformationFunction( id_to_zero, - - function( one_obj, obj, zero ) - - return MorphismIntoZeroObject( obj ); - -end ); - -## -double_functor := CapFunctor( "Double of Vecspaces", vecspaces, vecspaces ); - -AddObjectFunction( double_functor, - - function( obj ) - - return QVectorSpace( 2 * Dimension( obj ) ); - -end ); - -AddMorphismFunction( double_functor, - - function( new_source, mor, new_range ) - local matr, matr1; - - matr := EntriesOfHomalgMatrixAsListList( mor!.morphism ); - - matr := Concatenation( List( matr, i -> Concatenation( i, ListWithIdenticalEntries( Length( i ), 0 ) ) ), - List( matr, i -> Concatenation( ListWithIdenticalEntries( Length( i ), 0 ), i ) ) ); - - return VectorSpaceMorphism( new_source, matr, new_range ); - -end ); - -id_to_double := NaturalTransformation( "Id to double in vecspaces", identity_functor, double_functor ); - -AddNaturalTransformationFunction( id_to_double, - - function( new_source, obj, new_range ) - local dim, matr; - - dim := Dimension( obj ); - - matr := IdentityMat( dim ); - - matr := List( matr, i -> Concatenation( i, i ) ); - - return VectorSpaceMorphism( new_source, matr, new_range ); - -end ); - -double_swap_components := NaturalTransformation( "double swap components", double_functor, double_functor ); - -AddNaturalTransformationFunction( double_swap_components, - - function( doubled_source, obj, doubled_range ) - local zero_morphism, one_morphism; - - zero_morphism := ZeroMorphism( obj, obj ); - - one_morphism := IdentityMorphism( obj ); - - return MorphismBetweenDirectSums( [ [ zero_morphism, one_morphism ], [ one_morphism, zero_morphism ] ] ); - -end ); - -composition_of_double_swap_components := VerticalPreCompose( double_swap_components, double_swap_components ); - -ApplyNaturalTransformation( composition_of_double_swap_components, A ); - -# theorem_string := "\alpha:Mor, \beta:Mor ~|~ \IsMonomorphism( \alpha ) \vdash \IsMonomorphism( \ProjectionInFactorOfFiberProduct( [ \alpha, \beta ], 2 ) )"; -# -# ADD_THEOREM_TO_CATEGORY( vecspaces, PARSE_THEOREM_FROM_LATEX( theorem_string ) ); - -# @Theorem -# A | ( For all x in A : IsZero( x ) = true ) => IsZero( DirectProduct( A ) ) = true. -# A:\Obj ~|~ \IsZero( A ) \vdash \IsInjective( A ) -# @EndTheorem -# @Proof -# bla bla bla bla -# # @EndProof -# -# eval_rule := rec( command := "PreCompose", -# commands_to_check := [ [ [ 1 ], "UniversalMorphismIntoFiberProduct" ], -# [ [ 2 ], "ProjectionInFactorOfFiberProduct" ] ], -# cells_to_check := [ [ [ 1, 1, 1 ], [ 2, 1, 1 ] ], -# [ [ 1, 1, 2 ], [ 2, 1, 2 ] ], -# [ [ 2, 2 ], 2 ] -# ], -# part_to_replace := [ 1, 2, 1 ], -# ## TODO: -# part_for_is_well_defined := [ [ "IsCongruentForMorphisms", [ [ "PreCompose", [ [ 1, 2, 1 ], [ 1, 1, 1 ] ] ], [ "PreCompose", [ [ 1, 2, 2 ], [ 1, 1, 2 ] ] ] ] ] ] ); -# -# eval_rule := REMOVE_CHARACTERS_FROM_LATEX( "A, B:Obj, tau_A, tau_B:Mor |~ &()vdash &Precompose(InjectionOfCofactorOfCoproduct( [A, B], 1 ),&UniversalMorphismFromCoproduct( [A,B], [tau_A, tau_B] ) ) = tau_A" ); diff --git a/DeductiveSystemForCAP/examples/deductive_generalized.g b/DeductiveSystemForCAP/examples/deductive_generalized.g deleted file mode 100644 index 747a4831a7..0000000000 --- a/DeductiveSystemForCAP/examples/deductive_generalized.g +++ /dev/null @@ -1,66 +0,0 @@ -if not IsBound( VectorSpacesConstructorsLoaded ) then - - ReadPackage( "CAP", "examples/VectorSpacesConstructors.g" );; - -fi; -vecspaces := CreateCapCategory( "VectorSpacesForGeneralizedMorphismsTest" ); -#! VectorSpacesForGeneralizedMorphismsTest -vecspaces!.category_as_first_argument := false;; -ReadPackage( "CAP", "examples/VectorSpacesAllMethods.g" ); -#! true -A := QVectorSpace( 3 ); -#! -Asub := QVectorSpace( 2 ); -#! -B := QVectorSpace( 3 ); -#! -Bfac := QVectorSpace( 1 ); -#! -Bsub := QVectorSpace( 2 ); -#! -C := QVectorSpace( 3 ); -#! -Cfac := QVectorSpace( 1 ); -#! -Asub_into_A := VectorSpaceMorphism( Asub, [ [ 1, 0, 0 ], [ 0, 1, 0 ] ], A ); -#! A rational vector space homomorphism with matrix: -#! [ [ 1, 0, 0 ], -#! [ 0, 1, 0 ] ] -#! -Asub_to_Bfac := VectorSpaceMorphism( Asub, [ [ 1 ], [ 1 ] ], Bfac ); -#! A rational vector space homomorphism with matrix: -#! [ [ 1 ], -#! [ 1 ] ] -#! -B_onto_Bfac := VectorSpaceMorphism( B, [ [ 1 ], [ 1 ], [ 1 ] ], Bfac ); -#! A rational vector space homomorphism with matrix: -#! [ [ 1 ], -#! [ 1 ], -#! [ 1 ] ] -#! -Bsub_into_B := VectorSpaceMorphism( Bsub, [ [ 2, 2, 0 ], [ 0, 2, 2 ] ], B ); -#! A rational vector space homomorphism with matrix: -#! [ [ 2, 2, 0 ], -#! [ 0, 2, 2 ] ] -#! -Bsub_to_Cfac := VectorSpaceMorphism( Bsub, [ [ 3 ], [ 0 ] ], Cfac ); -#! A rational vector space homomorphism with matrix: -#! [ [ 3 ], -#! [ 0 ] ] -#! -C_onto_Cfac := VectorSpaceMorphism( C, [ [ 1 ], [ 2 ], [ 3 ] ], Cfac ); -Asub_into_A := InDeductiveSystem( Asub_into_A ); -Asub_to_Bfac := InDeductiveSystem( Asub_to_Bfac ); -B_onto_Bfac := InDeductiveSystem( B_onto_Bfac ); -Bsub_into_B := InDeductiveSystem( Bsub_into_B ); -Bsub_to_Cfac := InDeductiveSystem( Bsub_to_Cfac ); -C_onto_Cfac := InDeductiveSystem( C_onto_Cfac ); -SetIsAbelianCategory( CapCategory( C_onto_Cfac ), true ); -generalized_morphism1 := GeneralizedMorphism( Asub_into_A, Asub_to_Bfac, B_onto_Bfac ); -#! -generalized_morphism2 := GeneralizedMorphism( Bsub_into_B, Bsub_to_Cfac, C_onto_Cfac ); -generalized_morphism1 := InDeductiveSystem( generalized_morphism1 ); -generalized_morphism2 := InDeductiveSystem( generalized_morphism2 ); -p := PreCompose( generalized_morphism1, generalized_morphism2 ); - - diff --git a/DeductiveSystemForCAP/gap/DeductiveSystem.gd b/DeductiveSystemForCAP/gap/DeductiveSystem.gd deleted file mode 100644 index 82ce42ede1..0000000000 --- a/DeductiveSystemForCAP/gap/DeductiveSystem.gd +++ /dev/null @@ -1,105 +0,0 @@ -# SPDX-License-Identifier: GPL-2.0-or-later -# DeductiveSystemForCAP: Deductive system for CAP -# -# Declarations -# - -#! @Chapter Deduction system - -DeclareGlobalVariable( "DEDUCTIVE_SYSTEM_OPTIONS" ); - -DeclareGlobalVariable( "CATEGORIES_FAMILY_PROPERTIES" ); - -InstallValue( CATEGORIES_FAMILY_PROPERTIES, - - rec( ) ); - -DeclareGlobalFunction( "DeclareFamilyProperty" ); - -DeclareCategory( "IsDeductiveSystemCell", - IsCapCategoryCell ); - -DeclareCategory( "IsDeductiveSystemObject", - IsDeductiveSystemCell and IsCapCategoryObject ); - -DeclareCategory( "IsDeductiveSystemMorphism", - IsDeductiveSystemCell and IsCapCategoryMorphism ); - -DeclareCategory( "IsDeductiveSystemTwoCell", - IsDeductiveSystemCell and IsCapCategoryTwoCell ); - -DeclareGlobalFunction( "INSTALL_PROPERTIES_FOR_DEDUCTIVE_SYSTEM" ); - -DeclareGlobalFunction( "ADDS_FOR_DEDUCTIVE_SYSTEM" ); - -DeclareGlobalFunction( "RESOLVE_HISTORY" ); - -DeclareGlobalFunction( "RECURSIVE_EVAL" ); - -DeclareGlobalFunction( "HistoryToString" ); - -DeclareGlobalFunction( "PRINT_HISTORY_RECURSIVE" ); - -DeclareGlobalFunction( "PrintHistoryClean" ); - -DeclareGlobalFunction( "PrintHistory" ); - -##################################### -## -## Constructor -## -##################################### - -DeclareAttribute( "DeductiveSystem", - IsCapCategory ); - -DeclareAttribute( "InDeductiveSystem", - IsCapCategoryObject ); - -DeclareOperation( "DeductiveSystemObject", - [ IsCapCategory ] ); - -DeclareOperation( "DeductiveSystemObject", - [ IsString, IsList ] ); - -DeclareAttribute( "InDeductiveSystem", - IsCapCategoryMorphism ); - -DeclareOperation( "DeductiveSystemMorphism", - [ IsDeductiveSystemObject, IsString, IsList, IsDeductiveSystemObject ] ); - -DeclareOperation( "DeductiveSystemMorphism", - [ IsDeductiveSystemObject, IsDeductiveSystemObject ] ); - -##################################### -## -## Special Add -## -##################################### - -##################################### -## -## Attributes -## -##################################### - -DeclareAttribute( "History", - IsDeductiveSystemCell, "mutable" ); - -DeclareOperation( "Evaluation", - [ IsDeductiveSystemCell ] ); - -DeclareOperation( "HasEvaluation", - [ IsDeductiveSystemCell ] ); - -DeclareOperation( "SetEvaluation", - [ IsDeductiveSystemCell, IsCapCategoryCell ] ); - -##################################### -## -## Attributes for all cells -## -##################################### - -DeclareAttribute( "ChecksFromLogic", - IsCapCategoryCell, "mutable" ); diff --git a/DeductiveSystemForCAP/gap/DeductiveSystem.gi b/DeductiveSystemForCAP/gap/DeductiveSystem.gi deleted file mode 100644 index 5836d4599e..0000000000 --- a/DeductiveSystemForCAP/gap/DeductiveSystem.gi +++ /dev/null @@ -1,1323 +0,0 @@ -# SPDX-License-Identifier: GPL-2.0-or-later -# DeductiveSystemForCAP: Deductive system for CAP -# -# Implementations -# - -#################################### -## -## Option records and functions -## -#################################### - -InstallValue( DEDUCTIVE_SYSTEM_OPTIONS, - rec( resolve_variable_names := false ) ); - -#################################### -## -## Auxiliary functions -## -#################################### - -InstallGlobalFunction( RESOLVE_HISTORY, - - function( list ) - local new_list, i; - - new_list := [ ]; - - for i in list do - - if IsDeductiveSystemCell( i ) then - - Add( new_list, History( i ) ); - - elif IsList( i ) then - - Add( new_list, List( i, History ) ); - - else - - Add( new_list, i ); - - fi; - - od; - - return new_list; - -end ); - -########################################## -## -## Family property -## -########################################## - -# see commit 3864a12e3182aa81977836d7946e9a57e05df1c9 for how this was used previously -InstallGlobalFunction( DeclareFamilyProperty, - - function( arg ) - local name, filter, family, cell_type, reinstall; - - if Length( arg ) < 2 or Length( arg ) > 4 then - - Error( "usage DeclareFamilyProperty( name, filter[, family, type of cell ] )" ); - - fi; - - name := arg[ 1 ]; - - filter := arg[ 2 ]; - - if not IsBound( arg[ 3 ] ) then - - family := "general"; - - elif IsBound( arg[ 3 ] ) and LowercaseString( arg[ 3 ] ) in [ "object", "morphism", "twocell" ] then - - arg[ 4 ] := arg[ 3 ]; - - family := "general"; - - else - - family := LowercaseString( arg[ 3 ] ); - - fi; - - if Length( arg ) > 3 then - - cell_type := LowercaseString( arg[ 4 ] ); - - else - - Error( "the case `cell` is not supported anymore" ); - - fi; - - if not cell_type in [ "object", "morphism", "twocell" ] then - - Error( "cell must be object, morphism, or twocell" ); - - fi; - - if not IsBound( CATEGORIES_FAMILY_PROPERTIES.( family ) ) then - - CATEGORIES_FAMILY_PROPERTIES.( family ) := rec( ); - - fi; - - if not IsBound( CATEGORIES_FAMILY_PROPERTIES.( family ).( cell_type ) ) then - - CATEGORIES_FAMILY_PROPERTIES.( family ).( cell_type ) := [ ]; - - fi; - - reinstall := ValueOption( "reinstall" ); - - if reinstall <> false then - - reinstall := true; - - fi; - - Add( CATEGORIES_FAMILY_PROPERTIES.( family ).( cell_type ), [ name, reinstall ] ); - - DeclareProperty( name, filter ); - -end ); - -#################################### -## -## Reps and types -## -#################################### - -DeclareRepresentation( "IsDeductiveSystemObjectRep", - IsCapCategoryObjectRep and IsDeductiveSystemObject, - [ ] ); - -BindGlobal( "TheTypeOfDeductiveSystemObject", - NewType( TheFamilyOfCapCategoryObjects, - IsDeductiveSystemObjectRep ) ); - -DeclareRepresentation( "IsDeductiveSystemMorphismRep", - IsCapCategoryMorphismRep and IsDeductiveSystemMorphism, - [ ] ); - -BindGlobal( "TheTypeOfDeductiveSystemMorphism", - NewType( TheFamilyOfCapCategoryMorphisms, - IsDeductiveSystemMorphismRep ) ); - -DeclareRepresentation( "IsDeductiveSystemTwoCellRep", - IsCapCategoryTwoCellRep and IsDeductiveSystemTwoCell, - [ ] ); - -BindGlobal( "TheTypeOfDeductiveTwoCell", - NewType( TheFamilyOfCapCategoryTwoCells, - IsDeductiveSystemTwoCellRep ) ); - -#################################### -## -## Add methods -## -#################################### - -InstallGlobalFunction( ADDS_FOR_DEDUCTIVE_SYSTEM, - - function( deductive_system, category ) - - AddPreCompose( deductive_system, - - function( cat, left_morphism, right_morphism ) - - return DeductiveSystemMorphism( Source( left_morphism ), "PreCompose", [ left_morphism, right_morphism ], Range( right_morphism ) ); - - end ); - - AddIdentityMorphism( deductive_system, - - function( cat, object ) - - return DeductiveSystemMorphism( object, "IdentityMorphism", [ object ], object ); - - end ); - - AddInverseForMorphisms( deductive_system, - - function( cat, morphism ) - - return DeductiveSystemMorphism( Range( morphism ), "Inverse", [ morphism ], Source( morphism ) ); - - end ); - - AddLiftAlongMonomorphism( deductive_system, - - function( cat, monomorphism, test_morphism ) - - return DeductiveSystemMorphism( Source( test_morphism ), "LiftAlongMonomorphism", [ monomorphism, test_morphism ], Source( monomorphism ) ); - - end ); - - AddColiftAlongEpimorphism( deductive_system, - - function( cat, epimorphism, test_morphism ) - - return DeductiveSystemMorphism( Range( epimorphism ), "ColiftAlongEpimorphism", [ epimorphism, test_morphism ], Range( test_morphism ) ); - - end ); - - AddIsMonomorphism( deductive_system, - - function( cat, morphism ) - - return IsMonomorphism( Evaluation( morphism ) ); - - end ); - - AddIsEpimorphism( deductive_system, - - function( cat, morphism ) - - return IsEpimorphism( Evaluation( morphism ) ); - - end ); - - AddIsIsomorphism( deductive_system, - - function( cat, morphism ) - - return IsIsomorphism( Evaluation( morphism ) ); - - end ); - - AddIsDominating( deductive_system, - - function( cat, subobject1, subobject2 ) - - return IsDominating( Evaluation( subobject1 ), Evaluation( subobject2 ) ); - - end ); - - AddIsCodominating( deductive_system, - - function( cat, factorobject1, factorobject2 ) - - return IsCodominating( Evaluation( factorobject1 ), Evaluation( factorobject2 ) ); - - end ); - - AddIsCongruentForMorphisms( deductive_system, - - function( cat, morphism1, morphism2 ) - - return IsCongruentForMorphisms( Evaluation( morphism1 ), Evaluation( morphism2 ) ); - - end ); - - AddIsZeroForMorphisms( deductive_system, - - function( cat, morphism ) - - return IsZero( Evaluation( morphism ) ); - - end ); - - AddAdditionForMorphisms( deductive_system, - - function( cat, morphism1, morphism2 ) - - return DeductiveSystemMorphism( Source( morphism1 ), "\+", [ morphism1, morphism2 ], Range( morphism1 ) ); - - end ); - - AddAdditiveInverseForMorphisms( deductive_system, - - function( cat, morphism ) - - return DeductiveSystemMorphism( Source( morphism ), "AdditiveInverse", [ morphism ], Range( morphism ) ); - - end ); - - AddZeroMorphism( deductive_system, - - function( cat, source, range ) - - return DeductiveSystemMorphism( source, "ZeroMorphism", [ source, range ], range ); - - end ); - - ## HOLE: Well defined - - AddKernelObject( deductive_system, - - function( cat, morphism ) - - return DeductiveSystemObject( "KernelObject", [ morphism ] ); - - end ); - - AddKernelEmbedding( deductive_system, - - function( cat, morphism ) - - return DeductiveSystemMorphism( KernelObject( morphism ), "KernelEmbedding", [ morphism ], Source( morphism ) ); - - end ); - - AddKernelEmbeddingWithGivenKernelObject( deductive_system, - - function( cat, morphism, kernel ) - - return DeductiveSystemMorphism( kernel, "KernelEmbedding", [ morphism ], Source( morphism ) ); - - end ); - - AddKernelLift( deductive_system, - - function( cat, morphism, test_object, test_morphism ) - - return DeductiveSystemMorphism( Source( test_morphism ), "KernelLift", [ morphism, test_object, test_morphism ], KernelObject( morphism ) ); - - end ); - - AddKernelLiftWithGivenKernelObject( deductive_system, - - function( cat, morphism, test_object, test_morphism, kernel ) - - return DeductiveSystemMorphism( Source( test_morphism ), "KernelLift", [ morphism, test_object, test_morphism ], kernel ); - - end ); - - AddCokernelObject( deductive_system, - - function( cat, morphism ) - - return DeductiveSystemObject( "CokernelObject", [ morphism ] ); - - end ); - - AddCokernelProjection( deductive_system, - - function( cat, morphism ) - - return DeductiveSystemMorphism( Range( morphism ), "CokernelProjection", [ morphism ], CokernelObject( morphism ) ); - - end ); - - AddCokernelProjectionWithGivenCokernelObject( deductive_system, - - function( cat, morphism, cokernel ) - - return DeductiveSystemMorphism( Range( morphism ), "CokernelProjection", [ morphism ], cokernel ); - - end ); - - AddCokernelColift( deductive_system, - - function( cat, morphism, test_object, test_morphism ) - - return DeductiveSystemMorphism( CokernelObject( morphism ), "CokernelColift", [ morphism, test_object, test_morphism ], Range( test_morphism ) ); - - end ); - - AddCokernelColiftWithGivenCokernelObject( deductive_system, - - function( cat, morphism, test_object, test_morphism, cokernel ) - - return DeductiveSystemMorphism( cokernel, "CokernelColift", [ morphism, test_object, test_morphism ], Range( test_morphism ) ); - - end ); - - AddZeroObject( deductive_system, - - function( cat ) - - return DeductiveSystemObject( "ZeroObject", [ category ] ); - - end ); - - AddTerminalObject( deductive_system, - - function( cat ) - - return DeductiveSystemObject( "TerminalObject", [ category ] ); - - end ); - - AddUniversalMorphismIntoTerminalObject( deductive_system, - - function( cat, object ) - - return DeductiveSystemMorphism( object, "UniversalMorphismIntoTerminalObject", [ object ], TerminalObject( deductive_system ) ); - - end ); - - AddUniversalMorphismIntoTerminalObjectWithGivenTerminalObject( deductive_system, - - function( cat, object, terminal_object ) - - return DeductiveSystemMorphism( object, "UniversalMorphismIntoTerminalObject", [ object ], terminal_object ); - - end ); - - AddInitialObject( deductive_system, - - function( cat ) - - return DeductiveSystemObject( "InitialObject", [ category ] ); - - end ); - - AddUniversalMorphismFromInitialObject( deductive_system, - - function( cat, object ) - - return DeductiveSystemMorphism( InitialObject( object ), "UniversalMorphismFromInitialObject", [ object ], object ); - - end ); - - AddUniversalMorphismFromInitialObjectWithGivenInitialObject( deductive_system, - - function( cat, object, initial_object ) - - return DeductiveSystemMorphism( initial_object, "UniversalMorphismFromInitialObject", [ object ], object ); - - end ); - - AddDirectSum( deductive_system, - - function( cat, object_product_list ) - - return DeductiveSystemObject( "DirectSum", [ object_product_list ] ); - - end ); - - AddCoproduct( deductive_system, - - function( cat, object_product_list ) - - return DeductiveSystemObject( "Coproduct", [ object_product_list ] ); - - end ); - - AddInjectionOfCofactorOfCoproduct( deductive_system, - - function( cat, object_product_list, injection_number ) - local coproduct; - - coproduct := Coproduct( object_product_list ); - - return DeductiveSystemMorphism( object_product_list[ injection_number ], "InjectionOfCofactorOfCoproduct", [ object_product_list, injection_number ], coproduct ); - - end ); - - AddInjectionOfCofactorOfCoproductWithGivenCoproduct( deductive_system, - - function( cat, object_product_list, injection_number, coproduct ) - - return DeductiveSystemMorphism( object_product_list[ injection_number ], "InjectionOfCofactorOfCoproduct", [ object_product_list, injection_number ], coproduct ); - - end ); - - AddUniversalMorphismFromCoproduct( deductive_system, - - function( cat, diagram, test_object, sink ) - local coproduct; - - coproduct := Coproduct( List( sink, Source ) ); - - return DeductiveSystemMorphism( coproduct, "UniversalMorphismFromCoproduct", [ diagram, test_object, sink ], Source( sink[ 1 ] ) ); - - end ); - - AddUniversalMorphismFromCoproductWithGivenCoproduct( deductive_system, - - function( cat, diagram, test_object, sink, coproduct ) - - return DeductiveSystemMorphism( coproduct, "UniversalMorphismFromCoproduct", [ diagram, test_object, sink ], Source( sink[ 1 ] ) ); - - end ); - - AddDirectProduct( deductive_system, - - function( cat, object_product_list ) - - return DeductiveSystemObject( "DirectProduct", [ object_product_list ] ); - - end ); - - AddProjectionInFactorOfDirectProduct( deductive_system, - - function( cat, object_product_list, projection_number ) - local direct_product; - - direct_product := DirectProduct( object_product_list ); - - return DeductiveSystemMorphism( direct_product, "ProjectionInFactorOfDirectProduct", [ object_product_list, projection_number ], object_product_list[ projection_number ] ); - - end ); - - AddProjectionInFactorOfDirectProductWithGivenDirectProduct( deductive_system, - - function( cat, object_product_list, projection_number, direct_product ) - - return DeductiveSystemMorphism( direct_product, "ProjectionInFactorOfDirectProduct", [ object_product_list, projection_number ], object_product_list[ projection_number ] ); - - end ); - - AddUniversalMorphismIntoDirectProduct( deductive_system, - - function( cat, diagram, test_object, source ) - local direct_product; - - direct_product := DirectProduct( List( source, Range ) ); - - return DeductiveSystemMorphism( Source( source[ 1 ] ), "UniversalMorphismIntoDirectProduct", [ diagram, test_object, source ], direct_product ); - - end ); - - AddUniversalMorphismIntoDirectProductWithGivenDirectProduct( deductive_system, - - function( cat, diagram, test_object, source, direct_product ) - - return DeductiveSystemMorphism( Source( source[ 1 ] ), "UniversalMorphismIntoDirectProduct", [ diagram, test_object, source ], direct_product ); - - end ); - - AddFiberProduct( deductive_system, - - function( cat, diagram ) - - return DeductiveSystemObject( "FiberProduct", [ diagram ] ); - - end ); - - AddProjectionInFactorOfFiberProduct( deductive_system, - - function( cat, diagram, projection_number ) - local pullback; - - pullback := FiberProduct( diagram ); - - return DeductiveSystemMorphism( pullback, "ProjectionInFactorOfFiberProduct", [ diagram, projection_number ], Source( diagram[ projection_number ] ) ); - - end ); - - AddProjectionInFactorOfFiberProductWithGivenFiberProduct( deductive_system, - - function( cat, diagram, projection_number, pullback ) - - return DeductiveSystemMorphism( pullback, "ProjectionInFactorOfFiberProduct", [ diagram, projection_number ], Source( diagram[ projection_number ] ) ); - - end ); - - AddUniversalMorphismIntoFiberProduct( deductive_system, - - function( cat, diagram, test_object, source ) - local pullback; - - pullback := FiberProduct( diagram ); - - return DeductiveSystemMorphism( Source( source[ 1 ] ), "UniversalMorphismIntoFiberProduct", [ diagram, test_object, source ], pullback ); - - end ); - - AddUniversalMorphismIntoFiberProductWithGivenFiberProduct( deductive_system, - - function( cat, diagram, test_object, source, pullback ) - - return DeductiveSystemMorphism( Source( source[ 1 ] ), "UniversalMorphismIntoFiberProduct", [ diagram, test_object, source ], pullback ); - - end ); - - AddPushout( deductive_system, - - function( cat, diagram ) - - return DeductiveSystemObject( "Pushout", [ diagram ] ); - - end ); - - AddInjectionOfCofactorOfPushout( deductive_system, - - function( cat, diagram, injection_number ) - local pushout; - - pushout := Pushout( diagram ); - - return DeductiveSystemMorphism( Range( diagram[ injection_number ] ), "InjectionOfCofactorOfPushout", [ diagram, injection_number ], pushout ); - - end ); - - AddInjectionOfCofactorOfPushoutWithGivenPushout( deductive_system, - - function( cat, diagram, injection_number, pushout ) - - return DeductiveSystemMorphism( Range( diagram[ injection_number ] ), "InjectionOfCofactorOfPushout", [ diagram, injection_number ], pushout ); - - end ); - - AddUniversalMorphismFromPushout( deductive_system, - - function( cat, diagram, test_object, sink ) - local pushout; - - pushout := Pushout( diagram ); - - return DeductiveSystemMorphism( pushout, "UniversalMorphismFromPushout", [ diagram, test_object, sink ], Range( sink[ 1 ] ) ); - - end ); - - AddUniversalMorphismFromPushoutWithGivenPushout( deductive_system, - - function( cat, diagram, test_object, sink, pushout ) - - return DeductiveSystemMorphism( pushout, "UniversalMorphismFromPushout", [ diagram, test_object, sink ], Range( sink[ 1 ] ) ); - - end ); - - AddImageObject( deductive_system, - - function( cat, morphism ) - - return DeductiveSystemObject( "ImageObject", [ morphism ] ); - - end ); - - AddImageEmbedding( deductive_system, - - function( cat, morphism ) - local image_object; - - image_object := ImageObject( morphism ); - - return DeductiveSystemMorphism( image_object, "ImageEmbedding", [ morphism ], Range( morphism ) ); - - end ); - - AddImageEmbeddingWithGivenImageObject( deductive_system, - - function( cat, morphism, image_object ) - - return DeductiveSystemMorphism( image_object, "ImageEmbedding", [ morphism ], Range( morphism ) ); - - end ); - - AddCoastrictionToImage( deductive_system, - - function( cat, morphism ) - local image_object; - - image_object := ImageObject( morphism ); - - return DeductiveSystemMorphism( Source( morphism ), "CoastrictionToImage", [ morphism ], image_object ); - - end ); - - AddCoastrictionToImageWithGivenImageObject( deductive_system, - - function( cat, morphism, image_object ) - - return DeductiveSystemMorphism( Source( morphism ), "CoastrictionToImage", [ morphism ], image_object ); - - end ); - - AddUniversalMorphismFromImage( deductive_system, - - function( cat, morphism, test_factorization ) - local image_object; - - image_object := ImageObject( morphism ); - - return DeductiveSystemMorphism( image_object, "UniversalMorphismFromImage", [ morphism, test_factorization ], Source( test_factorization[1] ) ); - end ); - - AddUniversalMorphismFromImageWithGivenImageObject( deductive_system, - - function( cat, morphism, test_factorization, image_object ) - - return DeductiveSystemMorphism( image_object, "UniversalMorphismFromImage", [ morphism, test_factorization ], Source( test_factorization[1] ) ); - end ); - -end ); - -#################################### -## -## Constructors -## -#################################### - -InstallMethod( DeductiveSystem, - [ IsCapCategory ], - - function( category ) - local deductive_system; - - deductive_system := CreateCapCategory( Concatenation( "Deduction system of ", Name( category ) ) ); - - deductive_system!.category_as_first_argument := true; - - SetTheoremRecord( deductive_system, TheoremRecord( category ) ); - - SetUnderlyingCategory( deductive_system, category ); - - INSTALL_PROPERTIES_FOR_DEDUCTIVE_SYSTEM( deductive_system, category ); - - ADDS_FOR_DEDUCTIVE_SYSTEM( deductive_system, category ); - - INSTALL_LOGICAL_IMPLICATIONS_HELPER_EVAL_RULES( category, deductive_system, "IsCapCategory" ); - - return deductive_system; - -end ); - -BindGlobal( "INSTALL_PROPERTIES_FOR_DEDUCTIVE_SYSTEM_INSTALL_HELPER", - - function( name, filter ) - - InstallMethod( name, - [ filter ], - - function( cell ) - - return name( Evaluation( cell ) ); - - end ); - -end ); - -InstallGlobalFunction( INSTALL_PROPERTIES_FOR_DEDUCTIVE_SYSTEM, - - function( deductive_category, category ) - local families, family, type, filter, filter_getter, property, type_list; - - families := category!.families; - - deductive_category!.properties_to_propagate := rec( cell := [ ], object := [ ], morphism := [ ], twocell := [ ] ); - - for family in families do - - if IsBound( CATEGORIES_FAMILY_PROPERTIES.( family ) ) then - - for type in [ 1 .. 4 ] do - - filter := [ "IsDeductiveSystemCell", "IsDeductiveSystemObject", "IsDeductiveSystemMorphism", "IsDeductiveSystemTwoCell" ]; - - filter := filter[ type ]; - - filter_getter := [ CellFilter, ObjectFilter, MorphismFilter, TwoCellFilter ]; - - filter_getter := filter_getter[ type ]; - - type_list := [ "cell", "object", "morphism", "twocell" ]; - - type := type_list[ type ]; - - if IsBound( CATEGORIES_FAMILY_PROPERTIES.( family ).( type ) ) then - - for property in CATEGORIES_FAMILY_PROPERTIES.( family ).( type ) do - - Add( deductive_category!.properties_to_propagate.( type ), property[ 1 ] ); - - if property[ 2 ] = true then - - DeclareProperty( property[ 1 ], ValueGlobal( filter ) and filter_getter( deductive_category ) ); - - fi; - - property := ValueGlobal( property[ 1 ] ); - - INSTALL_PROPERTIES_FOR_DEDUCTIVE_SYSTEM_INSTALL_HELPER( property, ValueGlobal( filter ) and filter_getter( deductive_category ) ); - - od; - - fi; - - od; - - fi; - - od; - -end ); - -## -InstallMethod( InDeductiveSystem, - [ IsCapCategoryObject ], - - function( object ) - local deductive_object, deductive_system, property, entry; - - deductive_object := ObjectifyWithAttributes( rec( ), TheTypeOfDeductiveSystemObject ); - - SetEvaluation( deductive_object, object ); - - SetHistory( deductive_object, deductive_object ); - - deductive_system := DeductiveSystem( CapCategory( object ) ); - - Add( deductive_system, deductive_object ); - - for property in Concatenation( deductive_system!.properties_to_propagate.cell, deductive_system!.properties_to_propagate.object ) do - - AddToToDoList( ToDoListEntryForEqualAttributes( object, property, deductive_object, property ) ); - - od; - - return deductive_object; - -end ); - -## -InstallMethod( DeductiveSystemObject, - [ IsString, IsList ], - - function( func, argument_list ) - local deductive_object, resolved_history; - -# resolved_history := RESOLVE_HISTORY( argument_list ); - - deductive_object := ObjectifyWithAttributes( rec( ), TheTypeOfDeductiveSystemObject, - History, rec( command := func, arguments := argument_list ) ); - - INSTALL_TODO_FOR_LOGICAL_THEOREMS( func, argument_list, deductive_object ); - - return deductive_object; - -end ); - -## -InstallMethod( DeductiveSystemObject, - [ IsCapCategory ], - - function( category ) - local deductive_system, deductive_object; - - deductive_system := DeductiveSystem( category ); - - deductive_object := ObjectifyWithAttributes( rec( ), TheTypeOfDeductiveSystemObject ); - - SetHistory( deductive_object, deductive_object ); - - Add( deductive_system, deductive_object ); - - return deductive_object; - -end ); - - -## -InstallMethod( InDeductiveSystem, - [ IsCapCategoryMorphism ], - - function( morphism ) - local deductive_morphism, source, range, property, deductive_system; - - source := InDeductiveSystem( Source( morphism ) ); - - range := InDeductiveSystem( Range( morphism ) ); - - deductive_morphism := ObjectifyWithAttributes( rec( ), TheTypeOfDeductiveSystemMorphism, - Source, source, - Range, range ); - - SetEvaluation( deductive_morphism, morphism ); - - SetHistory( deductive_morphism, deductive_morphism ); - - deductive_system := DeductiveSystem( CapCategory( morphism ) ); - - Add( deductive_system, deductive_morphism ); - - INSTALL_TODO_FOR_LOGICAL_THEOREMS( "Source", [ deductive_morphism ], source ); - - INSTALL_TODO_FOR_LOGICAL_THEOREMS( "Range", [ deductive_morphism ], range ); - - for property in Concatenation( deductive_system!.properties_to_propagate.cell, deductive_system!.properties_to_propagate.morphism ) do - - AddToToDoList( ToDoListEntryForEqualAttributes( morphism, property, deductive_morphism, property ) ); - - od; - - return deductive_morphism; - -end ); - -## -InstallMethod( DeductiveSystemMorphism, - [ IsDeductiveSystemObject, IsString, IsList, IsDeductiveSystemObject ], - - function( source, func, argument_list, range ) - local deductive_morphism, resolved_history; - -# resolved_history := RESOLVE_HISTORY( argument_list ); - - deductive_morphism := ObjectifyWithAttributes( rec( ), TheTypeOfDeductiveSystemMorphism, - History, rec( command := func, arguments := argument_list ), - Source, source, - Range, range ); - - INSTALL_TODO_FOR_LOGICAL_THEOREMS( func, argument_list, deductive_morphism ); - - ## CHECK THIS - INSTALL_TODO_FOR_LOGICAL_THEOREMS( "Source", [ deductive_morphism ], source, CapCategory( source ) ); - - INSTALL_TODO_FOR_LOGICAL_THEOREMS( "Range", [ deductive_morphism ], range, CapCategory( range ) ); - - return deductive_morphism; - -end ); - -## -InstallMethod( DeductiveSystemMorphism, - [ IsDeductiveSystemObject, IsDeductiveSystemObject ], - - function( source, range ) - local deductive_system, deductive_morphism; - - deductive_morphism := ObjectifyWithAttributes( rec( ), TheTypeOfDeductiveSystemMorphism, - Source, source, - Range, range ); - - SetHistory( deductive_morphism, deductive_morphism ); - - Add( CapCategory( source ), deductive_morphism ); - - INSTALL_TODO_FOR_LOGICAL_THEOREMS( "Source", [ deductive_morphism ], source, CapCategory( source ) ); - - INSTALL_TODO_FOR_LOGICAL_THEOREMS( "Range", [ deductive_morphism ], range, CapCategory( range ) ); - - return deductive_morphism; - -end ); - -################################# -## -## Eval -## -################################# - -BindGlobal( "APPLY_LOGIC_TO_HISTORY", - - function( history ) - - return [ history, [ ] ]; - -end ); - -## FIXME: This can be done more efficient, but not today. -InstallGlobalFunction( RECURSIVE_EVAL, - - function( list ) - - if IsDeductiveSystemCell( list ) then - - if IsDeductiveSystemCell( History( list ) ) and not HasEvaluation( list ) then - - Error( "cannot evaluate object since leaves in history do not have evaluation.\n If you continue from here, your results will be wrong." ); - - fi; - - return Evaluation( list ); - - elif IsRecord( list ) then - - return CallFuncList( ValueGlobal( list!.command ), List( list!.arguments, RECURSIVE_EVAL ) ); - - elif IsList( list ) then - - return List( list, RECURSIVE_EVAL ); - - fi; - - return list; - -end ); - -## -InstallMethod( Evaluation, - [ IsDeductiveSystemCell ], - - function( cell ) - local history, new_history, checks, eval, property, property_list, deductive_system; - - if IsBound( cell!.eval ) and IsBoundElmWPObj( cell!.eval, 1 ) then - - return ElmWPObj( cell!.eval, 1 ); - - fi; - - history := History( cell ); - - if IsBound( UnderlyingCategory( CapCategory( cell ) )!.eval_rules ) then - - new_history := APPLY_JUDGEMENT_TO_HISTORY_RECURSIVE( history, UnderlyingCategory( CapCategory( cell ) )!.eval_rules ); - - else - - new_history := fail; - - fi; - - if new_history <> fail then - - checks := new_history!.part_for_is_well_defined; - - new_history := new_history!.new_history; - - else - - checks := [ ]; - - new_history := history; - - fi; - - SetHistory( cell, new_history ); - - SetChecksFromLogic( cell, checks ); - - eval := RECURSIVE_EVAL( new_history ); - - cell!.eval := WeakPointerObj( [ eval ] ); - - deductive_system := CapCategory( cell ); - - if IsDeductiveSystemMorphism( cell ) then - - property_list := deductive_system!.properties_to_propagate.morphism; - - elif IsDeductiveSystemObject( cell ) then - - property_list := deductive_system!.properties_to_propagate.object; - - else - - property_list := [ ]; - - fi; - - for property in Concatenation( deductive_system!.properties_to_propagate.cell, property_list ) do - - AddToToDoList( ToDoListEntryForEqualAttributes( cell, property, eval, property ) ); - - od; - - return eval; - -end ); - -InstallMethod( HasEvaluation, - [ IsDeductiveSystemCell ], - - function( cell ) - - return IsBound( cell!.eval ) and IsBoundElmWPObj( cell!.eval, 1 ); - -end ); - -InstallMethod( SetEvaluation, - [ IsDeductiveSystemCell, IsCapCategoryCell ], - - function( cell, value ) - - cell!.eval := WeakPointerObj( [ value ] ); - -end ); - -################################# -## -## Special Adds -## -################################# - -# InstallMethod( Add, -# [ IsCapCategory, IsDeductiveSystemObject ], -# -# function( deductive_system, object ) -# local property; -# -# if HasEvaluation( object ) then -# -# TryNextMethod(); -# -# fi; -# -# AddToToDoList( ToDoListEntryToMaintainEqualAttributes( [ [ object, "HasEvaluation", ] ], [ object, [ Eval, object ] ], Concatenation( deductive_system!.properties_to_propagate.cell, deductive_system!.properties_to_propagate.object ) ) ); -# -# TryNextMethod(); -# -# end ); -# -# InstallMethod( Add, -# [ IsCapCategory, IsDeductiveSystemMorphism ], -# -# function( deductive_system, morphism ) -# local property; -# -# if HasEval( morphism ) then -# -# TryNextMethod(); -# -# fi; -# -# AddToToDoList( ToDoListEntryToMaintainEqualAttributes( [ [ morphism, "Eval" ] ], [ morphism, [ Eval, morphism ] ], Concatenation( deductive_system!.properties_to_propagate.cell, deductive_system!.properties_to_propagate.morphism ) ) ); -# -# TryNextMethod(); -# -# end ); - -################################# -## -## View -## -################################# - -InstallMethod( ViewString, - [ IsDeductiveSystemObject ], - - function( cell ) - - return Concatenation( "<", String( cell ), ">" ); - -end ); - -InstallMethod( String, - [ IsDeductiveSystemObject ], - - function( cell ) - - return Concatenation( "An unevaluated object in " , Name( CapCategory( cell ) ) ); - -end ); - -InstallMethod( ViewString, - [ IsDeductiveSystemMorphism ], - - function( cell ) - - return Concatenation( "<", String( cell ), ">" ); - -end ); - -InstallMethod( String, - [ IsDeductiveSystemMorphism ], - - function( cell ) - - return Concatenation( "An unevaluated morphism in " , Name( CapCategory( cell ) ) ); - -end ); - -## Those two methods can cause errors. -InstallMethod( ViewString, - [ IsDeductiveSystemCell ], - 1000000, ##FIXME!!!! - - function( cell ) - - if HasEvaluation( cell ) then - - return Concatenation( "" ); - - else - - TryNextMethod(); - - fi; - -end ); - -## -InstallMethod( String, - [ IsDeductiveSystemCell ], - 1000000, - - function( cell ) - - if HasEvaluation( cell ) then - - return Concatenation( "Deductive system hull of ", String( cell ) ); - - fi; - - TryNextMethod(); - -end ); - -##################################### -## -## Print history -## -##################################### - -## -InstallGlobalFunction( "HistoryToString", - - function( history ) - local string, resolve_variable_names, gvars; - - resolve_variable_names := ValueOption( "ResolveVariableNames" ); - - if IsRecord( history ) then - - return Concatenation( history!.command, "( ", JoinStringsWithSeparator( List( history!.arguments, HistoryToString ), "," ), " )" ); - - elif IsList( history ) then - - string := List( history, HistoryToString ); - - string := JoinStringsWithSeparator( string, ", " ); - - return Concatenation( "[ ", string, " ]" ); - - elif IsCapCategoryCell( history ) and resolve_variable_names = true then - - gvars := NamesGVars( ); - - for string in gvars do - - if IsBoundGlobal( string ) and IsIdenticalObj( ValueGlobal( string ), history ) and not string in [ "last", "last2", "last3" ] then - - return string; - - fi; - - od; - - fi; - - return String( history ); - -end ); - -## -InstallGlobalFunction( PRINT_HISTORY_RECURSIVE, - - function( history ) - local string, resolve_variable_names, gvars; - - resolve_variable_names := ValueOption( "ResolveVariableNames" ); - - if IsCapCategoryCell( history ) and IsRecord( History( history ) ) then - - history := History( history ); - - fi; - - if IsRecord( history ) then - - string := List( history!.arguments, PRINT_HISTORY_RECURSIVE ); - - string := List( string, i -> ReplacedString( i, "\n", "\n* " ) ); - - string := List( string, i -> Concatenation( "** ", i, "\n" ) ); - - string := JoinStringsWithSeparator( string, "" ); - - string := Concatenation( history!.command, "(\n", string, ")" ); - - return string; - - elif IsList( history ) then - - string := List( history, PRINT_HISTORY_RECURSIVE ); - - string := List( string, i -> ReplacedString( i, "\n", "\n* " ) ); - - string := List( string, i -> Concatenation( "** ", i, "\n" ) ); - - string := JoinStringsWithSeparator( string, "" ); - - string := Concatenation( "[\n", string, "]" ); - - return string; - - elif IsCapCategoryCell( history ) and resolve_variable_names = true then - - gvars := NamesUserGVars( ); - - for string in gvars do - - if IsBoundGlobal( string ) and IsIdenticalObj( ValueGlobal( string ), history ) and not string in [ "last", "last2", "last3" ] then - - return string; - - fi; - - od; - - fi; - -# InfoOfObject( history ); - - return String( history ); - -end ); - -InstallGlobalFunction( PrintHistoryClean, - - function( history ) - - if IsCapCategoryCell( history ) then - - Print( PRINT_HISTORY_RECURSIVE( History( history ) ) ); - - else - - Print( PRINT_HISTORY_RECURSIVE( history ) ); - - fi; - -end ); - -InstallGlobalFunction( PrintHistory, - - function( history ) - - PrintHistoryClean( history : ResolveVariableNames := true ); - -end ); - diff --git a/DeductiveSystemForCAP/gap/LogicForDeductiveSystem.gd b/DeductiveSystemForCAP/gap/LogicForDeductiveSystem.gd deleted file mode 100644 index e43f49bc27..0000000000 --- a/DeductiveSystemForCAP/gap/LogicForDeductiveSystem.gd +++ /dev/null @@ -1,33 +0,0 @@ -# SPDX-License-Identifier: GPL-2.0-or-later -# DeductiveSystemForCAP: Deductive system for CAP -# -# Declarations -# - -#! @Chapter Deduction system - -## Global files and add functions - -DeclareGlobalFunction( "INSTALL_LOGICAL_IMPLICATIONS_HELPER_EVAL_RULES" ); - -DeclareAttribute( "INSTALL_LOGICAL_IMPLICATIONS", - IsCapCategory ); - -## Theorems - -## True methods - -## Eval rules - -DeclareGlobalFunction( "FIX_WELL_DEFINED_PART" ); - -DeclareGlobalFunction( "IS_EQUAL_FOR_SUBTREES_RECURSIVE" ); - -DeclareGlobalFunction( "APPLY_JUDGEMENT_TO_HISTORY_RECURSIVE" ); - -DeclareGlobalFunction( "CHECK_CORRECT_COMMAND_HISTORY_RECURSIVE" ); - -DeclareGlobalFunction( "SANITIZE_SOURCE_PART_WITH_EVERYTHING_GIVEN_RECURSIVE" ); - -DeclareFilter( "EvalCanComputePredicates" ); - diff --git a/DeductiveSystemForCAP/gap/LogicForDeductiveSystem.gi b/DeductiveSystemForCAP/gap/LogicForDeductiveSystem.gi deleted file mode 100644 index be598f05d1..0000000000 --- a/DeductiveSystemForCAP/gap/LogicForDeductiveSystem.gi +++ /dev/null @@ -1,623 +0,0 @@ -# SPDX-License-Identifier: GPL-2.0-or-later -# DeductiveSystemForCAP: Deductive system for CAP -# -# Implementations -# - -## RETHINK THIS WHOLE STRUCTURE - -######################################## -## -## Global logic files -## -######################################## - -InstallGlobalFunction( INSTALL_LOGICAL_IMPLICATIONS_HELPER_EVAL_RULES, - - function( category, deductive_category, current_filter ) - local i, theorem_list, current_theorem; - - category!.logical_implication_files.EvalRules.general_rules_already_read := true; - - for i in category!.logical_implication_files.EvalRules.( current_filter ) do - - theorem_list := READ_EVAL_RULE_FILE( i ); - - for current_theorem in theorem_list do - - ADD_EVAL_RULES_TO_CATEGORY( category, current_theorem ); - - od; - - od; - -end ); - -InstallImmediateMethod( INSTALL_LOGICAL_IMPLICATIONS, - IsCapCategory and HasDeductiveSystem and IsEnrichedOverCommutativeRegularSemigroup, - 0, - - function( category ) - - INSTALL_LOGICAL_IMPLICATIONS_HELPER_EVAL_RULES( category, DeductiveSystem( category ), "IsEnrichedOverCommutativeRegularSemigroup" ); - - TryNextMethod( ); - -end ); - -InstallImmediateMethod( INSTALL_LOGICAL_IMPLICATIONS, - IsCapCategory and HasDeductiveSystem and IsAdditiveCategory, - 0, - - function( category ) - - INSTALL_LOGICAL_IMPLICATIONS_HELPER_EVAL_RULES( category, DeductiveSystem( category ), "IsAdditiveCategory" ); - - TryNextMethod( ); - -end ); - -InstallImmediateMethod( INSTALL_LOGICAL_IMPLICATIONS, - IsCapCategory and HasDeductiveSystem and IsPreAbelianCategory, - 0, - - function( category ) - - INSTALL_LOGICAL_IMPLICATIONS_HELPER_EVAL_RULES( category, DeductiveSystem( category ), "IsPreAbelianCategory" ); - - TryNextMethod( ); - -end ); - -InstallImmediateMethod( INSTALL_LOGICAL_IMPLICATIONS, - IsCapCategory and HasDeductiveSystem and IsAbelianCategory, - 0, - - function( category ) - - INSTALL_LOGICAL_IMPLICATIONS_HELPER_EVAL_RULES( category, DeductiveSystem( category ), "IsAbelianCategory" ); - - TryNextMethod( ); - -end ); - -InstallImmediateMethod( INSTALL_LOGICAL_IMPLICATIONS, - IsCapCategory and HasDeductiveSystem and IsAbCategory, - 0, - - function( category ) - - INSTALL_LOGICAL_IMPLICATIONS_HELPER_EVAL_RULES( category, DeductiveSystem( category ), "IsAbCategory" ); - - TryNextMethod( ); - -end ); - -################################### -## -## Eval rule part -## -################################### - -## -BindGlobal( "GET_CORRECT_SUBTREE_ENTRY", - - function( tree, subtree_index_list ) - local i; - - for i in subtree_index_list do - - if IsRecord( tree ) then - - tree := tree!.arguments[ i ]; - - elif IsList( tree ) then - - tree := tree[ i ]; - - else - - return fail; - - fi; - - od; - - return tree; - -end ); - -## -InstallGlobalFunction( IS_EQUAL_FOR_SUBTREES_RECURSIVE, - - function( subtree1, subtree2 ) - local i; - - if IsRecord( subtree1 ) and IsRecord( subtree2 ) then - - return subtree1!.command = subtree2!.command and IS_EQUAL_FOR_SUBTREES_RECURSIVE( subtree1!.arguments, subtree2!.arguments ); - - elif IsList( subtree1 ) and IsList( subtree2 ) then - - if not Length( subtree1 ) = Length( subtree2 ) then - - return false; - - fi; - - return ForAll( [ 1 .. Length( subtree1 ) ], i -> IS_EQUAL_FOR_SUBTREES_RECURSIVE( subtree1[ i ], subtree2[ i ] ) ); - - else - - return IsIdenticalObj( subtree1, subtree2 ); - - fi; - - return false; - -end ); - -## -BindGlobal( "IS_EQUAL_FOR_SUBTREES", - - function( arg ) - local first_subtree, i; - - if Length( arg ) < 2 then - - return true; - - fi; - - first_subtree := arg[ 1 ]; - - for i in [ 2 .. Length( arg ) ] do - - if IS_EQUAL_FOR_SUBTREES_RECURSIVE( first_subtree, arg[ i ] ) = false then - - return false; - - fi; - - od; - - return true; - -end ); - -## -InstallGlobalFunction( FIX_WELL_DEFINED_PART, - - function( well_defined_part, history ) - local current_well_defined_part; - - if IsString( well_defined_part ) then - - return well_defined_part; - - fi; - - if IsList( well_defined_part ) and ForAll( well_defined_part, IsInt ) then - - return GET_CORRECT_SUBTREE_ENTRY( history, well_defined_part ); - - fi; - - if IsList( well_defined_part ) then - - return List( well_defined_part, i -> FIX_WELL_DEFINED_PART( i, history ) ); - - fi; - - return well_defined_part; - -end ); - -## -InstallGlobalFunction( CHECK_CORRECT_COMMAND_HISTORY_RECURSIVE, - - function( history, command_tree ) - local object_history; - - if command_tree = fail then - - return true; - - fi; - - if IsCapCategoryCell( history ) then - - history := History( history ); - - if not IsRecord( history ) then - - return false; - - else - - return CHECK_CORRECT_COMMAND_HISTORY_RECURSIVE( history, command_tree ); - - fi; - - fi; - - if IsList( history ) and IsList( command_tree ) then - - if Length( history ) = Length( command_tree ) then - - return ForAll( [ 1 .. Length( history ) ], i -> CHECK_CORRECT_COMMAND_HISTORY_RECURSIVE( history[ i ], command_tree[ i ] ) ); - - fi; - - fi; - - if IsRecord( history ) and IsRecord( command_tree ) then - - return history!.command = command_tree!.command and CHECK_CORRECT_COMMAND_HISTORY_RECURSIVE( history!.arguments, command_tree!.arguments ); - - fi; - - return false; - -end ); - -BindGlobal( "GET_FULL_POSITION", - - function( position, variable_name_record ) - local new_position, i; - - new_position := ShallowCopy( position ); - - for i in [ 1 .. Length( new_position ) ] do - - if IsString( new_position[ i ] ) then - - new_position[ i ] := variable_name_record.( new_position[ i ] ); - - fi; - - od; - - return new_position; - -end ); - -BindGlobal( "GET_VARIABLE_FROM_POSITION", - - function( history, position ) - local variable, i; - - variable := history; - - for i in position do - - if IsCapCategoryCell( variable ) then - - variable := History( variable ); - - fi; - - if IsRecord( variable ) then - - variable := variable!.arguments[ i ]; - - continue; - - elif IsList( variable ) then - - variable := variable[ i ]; - - continue; - - fi; - - od; - - return variable; - -end ); - -## -BindGlobal( "FILL_VARIABLE_NAME_RECORD", - - function( history, variable_name_record ) - local filled_variable_record, name, current_position, current_variable, i; - - filled_variable_record := StructuralCopy( variable_name_record ); - - for name in RecNames( filled_variable_record ) do - - current_position := filled_variable_record.( name ); - - current_variable := GET_VARIABLE_FROM_POSITION( history, current_position ); - - filled_variable_record.( name ) := current_variable; - - od; - - return filled_variable_record; - -end ); - -## -BindGlobal( "CHECK_VARIABLE_PAIRS", - - function( history, variable_name_pairs, variable_name_record ) - local current_list, position_index, current_first_object, current_object; - - for current_list in variable_name_pairs do - - if Length( current_list ) < 2 then - - continue; - - fi; - - current_first_object := current_list[ 1 ]; - - current_first_object := GET_VARIABLE_FROM_POSITION( history, GET_FULL_POSITION( current_first_object, variable_name_record ) ); - - for position_index in [ 2 .. Length( current_list ) ] do - - current_object := GET_VARIABLE_FROM_POSITION( history, GET_FULL_POSITION( current_list[ position_index ], variable_name_record ) ); - - if not current_object = current_first_object then - - return false; - - fi; - - od; - - od; - - return true; - -end ); - -BindGlobal( "GET_VARIABLE_BY_NAME", - - function( name, variable_name_record ) - local name_and_index, variable; - - if IS_LIST_WITH_INDEX( name ) then - - name_and_index := SPLIT_INTO_LIST_NAME_AND_INDEX( name ); - - variable := variable_name_record.( name_and_index[ 1 ] ); - - if STRING_REPRESENTS_INTEGER( name_and_index[ 2 ] ) then - - variable := variable[ Int_SAVE( name_and_index[ 2 ] ) ]; - - else - - variable := variable[ variable_name_record.( name_and_index[ 2 ] ) ]; - - fi; - - else - - variable := variable_name_record.( name ); - - fi; - - return variable; - -end ); - -InstallGlobalFunction( SANITIZE_SOURCE_PART_WITH_EVERYTHING_GIVEN_RECURSIVE, - - function( source_rec, variable_name_rec ) - local new_rec, new_name; - - if IsRecord( source_rec ) then - - new_rec := rec( command := source_rec!.command ); - - new_rec.arguments := List( source_rec.arguments, i -> SANITIZE_SOURCE_PART_WITH_EVERYTHING_GIVEN_RECURSIVE( i, variable_name_rec ) ); - - return new_rec; - - elif IsInt( source_rec ) then - - return source_rec; - - elif IsString( source_rec ) then - - return GET_VARIABLE_BY_NAME( source_rec, variable_name_rec ); - - fi; - -end ); - -BindGlobal( "SANITIZE_SOURCE_PART", - - function( source_rec, history, variable_name_record ) - local new_source_rec, bound_variable_name, bound_variable_list, i, new_source_list; - - new_source_rec := StructuralCopy( source_rec ); - - if source_rec!.bound_variable = fail then - - bound_variable_name := "xXx_my_super_crazy_dummy_variable_name_ausrufezeichen_xXx"; - - bound_variable_list := [ 1 ]; - - else - - bound_variable_name := source_rec!.bound_variable_name; - - if IsBound( source_rec!.bound_variable_name ) then - - bound_variable_list := variable_name_record.( source_rec.bound_variable_name ); - - else - - bound_variable_list := source_rec.bound_variable_list_boundaries; - - for i in [ 1, 2 ] do - - if IsInt( bound_variable_list[ i ] ) then - - continue; - - fi; - - if PositionSublist( bound_variable_list[ i ], "Length(" ) <> fail then - - bound_variable_list[ i ] := bound_variable_list[ i ]{[ PositionSublist( bound_variable_list[ i ], "Length(" ) + 7 .. Length( bound_variable_list[ i ] ) - 1 ]}; - - bound_variable_list[ i ] := Length( variable_name_record.( bound_variable_list[ i ] ) ); - - else - - bound_variable_list[ i ] := variable_name_record.( bound_variable_list[ i ] ); - - fi; - - od; - - bound_variable_list := [ bound_variable_list[ 1 ] .. bound_variable_list[ 2 ] ]; - - fi; - - fi; - - new_source_list := [ ]; - - for i in bound_variable_list do - - variable_name_record.( bound_variable_name ) := i; - - Add( new_source_list, SANITIZE_SOURCE_PART_WITH_EVERYTHING_GIVEN_RECURSIVE( source_rec, variable_name_record ) ); - - od; - - return new_source_list; - -end ); - - -## -InstallGlobalFunction( APPLY_JUDGEMENT_TO_HISTORY_RECURSIVE, - - function( history, rules ) - local return_rec, command, current_rules, rule_to_apply, command_to_check, - command_from_history, to_be_applied, rule_applied, object_to_check, resolved_objects, i, - replaced_history, part_for_well_defined, new_return, arguments, command_check, variable_name_record, - variable_check; - - if IsCapCategoryCell( history ) then - - history := History( history ); - - if not IsRecord( history ) then - - return fail; - - fi; - - fi; - - return_rec := rec( ); - - command := history!.command; - - if not IsBound( rules.( command ) ) then - - return fail; - - fi; - - current_rules := rules.( command ); - - rule_applied := false; - - for rule_to_apply in current_rules do - - command_check := CHECK_CORRECT_COMMAND_HISTORY_RECURSIVE( history, rule_to_apply!.command_tree ); - - if command_check = false then - - continue; - - fi; - - variable_name_record := FILL_VARIABLE_NAME_RECORD( history, rule_to_apply!.variable_record ); - - variable_check := CHECK_VARIABLE_PAIRS( history, rule_to_apply!.equal_variable_positions, variable_name_record ); - - if variable_check = false then - - continue; - - fi; - - ## if we get here, we have found a rule to apply - - replaced_history := GET_VARIABLE_FROM_POSITION( history, GET_FULL_POSITION( rule_to_apply!.replace, variable_name_record ) ); - - part_for_well_defined := rule_to_apply!.source_list; - - part_for_well_defined := List( part_for_well_defined, i -> SANITIZE_SOURCE_PART( i, history, variable_name_record ) ); - - part_for_well_defined := Flat( part_for_well_defined ); - - rule_applied := true; - - break; - - od; - - if rule_applied = true then - - new_return := APPLY_JUDGEMENT_TO_HISTORY_RECURSIVE( replaced_history, rules ); - - if new_return = fail then - - return rec( new_history := replaced_history, part_for_is_well_defined := part_for_well_defined ); - - else - - new_return!.part_for_is_well_defined := Concatenation( new_return!.part_for_is_well_defined, part_for_well_defined ); - - return new_return; - - fi; - - fi; - - for arguments in [ 1 .. Length( history!.arguments ) ] do - - new_return := APPLY_JUDGEMENT_TO_HISTORY_RECURSIVE( history!.arguments[ arguments ], rules ); - - if new_return <> fail then - - history := StructuralCopy( history ); - - history!.arguments[ arguments ] := new_return!.new_history; - - part_for_well_defined := new_return!.part_for_is_well_defined; - - new_return := APPLY_JUDGEMENT_TO_HISTORY_RECURSIVE( history, rules ); - - if new_return = fail then - - return rec( new_history := history, part_for_is_well_defined := part_for_well_defined ); - - else - - return rec( new_history := new_return!.new_history, part_for_is_well_defined := Concatenation( part_for_well_defined, new_return!.part_for_is_well_defined ) ); - - fi; - - fi; - - od; - - return fail; - -end ); - - diff --git a/DeductiveSystemForCAP/init.g b/DeductiveSystemForCAP/init.g deleted file mode 100644 index acbb644f11..0000000000 --- a/DeductiveSystemForCAP/init.g +++ /dev/null @@ -1,3 +0,0 @@ -ReadPackage( "DeductiveSystemForCAP", "gap/DeductiveSystem.gd"); - -ReadPackage( "DeductiveSystemForCAP", "gap/LogicForDeductiveSystem.gd"); diff --git a/DeductiveSystemForCAP/makedoc.g b/DeductiveSystemForCAP/makedoc.g deleted file mode 100644 index a1511563fc..0000000000 --- a/DeductiveSystemForCAP/makedoc.g +++ /dev/null @@ -1,31 +0,0 @@ -# SPDX-License-Identifier: GPL-2.0-or-later -# DeductiveSystemForCAP: Deductive system for CAP -# -# This file is a script which compiles the package manual. -# -if fail = LoadPackage( "AutoDoc", "2019.05.20" ) then - - Error( "AutoDoc version 2019.05.20 or newer is required." ); - -fi; - -AutoDoc( rec( - autodoc := rec( - files := [ "doc/Doc.autodoc" ], - scan_dirs := [ "doc", "gap", "examples", "examples/doc" ], - ), - extract_examples := rec( - units := "Single", - ), - gapdoc := rec( - LaTeXOptions := rec( - LateExtraPreamble := """ - """, - ), - ), - scaffold := rec( - entities := [ "homalg", "CAP" ], - ), -) ); - -QUIT; diff --git a/DeductiveSystemForCAP/makedoc_with_overfull_hbox_warnings.g b/DeductiveSystemForCAP/makedoc_with_overfull_hbox_warnings.g deleted file mode 100644 index b46c34d894..0000000000 --- a/DeductiveSystemForCAP/makedoc_with_overfull_hbox_warnings.g +++ /dev/null @@ -1,42 +0,0 @@ -# SPDX-License-Identifier: GPL-2.0-or-later -# DeductiveSystemForCAP: Deductive system for CAP -# -# This file is a script which compiles the package manual and prints overfull hbox warnings. -# -if fail = LoadPackage( "AutoDoc", "2019.05.20" ) then - - Error( "AutoDoc version 2019.05.20 or newer is required." ); - -fi; - -AutoDoc( rec( - dir := "doc_tmp/", - autodoc := rec( - files := [ "doc/Doc.autodoc" ], - scan_dirs := [ "doc", "gap", "examples", "examples/doc" ], - ), - gapdoc := rec( - LaTeXOptions := rec( - LateExtraPreamble := """ - % Many thanks to https://tex.stackexchange.com/questions/22466/how-to-convince-fancyvrb-to-give-overfull-warnings/534486#534486 - \makeatletter - \def\FV@ListProcessLine#1{% - \hbox to \hsize{% - \kern\leftmargin - \hbox to \linewidth{% - \FV@LeftListNumber - \FV@LeftListFrame - \FancyVerbFormatLine{#1}\hfil % change \hss to \hfil - \FV@RightListFrame - \FV@RightListNumber}% - \hss}} - \makeatother - """, - ), - ), - scaffold := rec( - entities := [ "homalg", "CAP" ], - ), -) ); - -QUIT; diff --git a/DeductiveSystemForCAP/makefile b/DeductiveSystemForCAP/makefile deleted file mode 100644 index 91e943aadc..0000000000 --- a/DeductiveSystemForCAP/makefile +++ /dev/null @@ -1,57 +0,0 @@ -# make sure gap --quitonbreak fails even if it is part of a pipe -SHELL=/bin/bash -o pipefail - -all: doc test - -doc: doc/manual.six - -doc/manual.six: makedoc.g \ - PackageInfo.g \ - $(wildcard doc/*.autodoc gap/*.gd gap/*.gi examples/*.g examples/*/*.g) - gap --quitonbreak makedoc.g - -clean: - (cd doc ; ./clean) - -test: doc - gap tst/testall.g - -test-basic-spacing: - # exit code 1 means no match, which is what we want here (exit code 2 signals an error) - grep -RPl "\t" examples/ gap/; test $$? -eq 1 || (echo "Tabs found" && exit 1) - grep -RPl "\r" examples/ gap/; test $$? -eq 1 || (echo "Windows line-endings found" && exit 1) - grep -RPzL "\n\z" examples/ gap/ | grep ""; test $$? -eq 1 || (echo "File with no newline at end of file found" && exit 1) - -test-doc: doc - cp -aT doc/ doc_tmp/ - cd doc_tmp && ./clean - gap --quitonbreak makedoc_with_overfull_hbox_warnings.g | perl -pe 'END { exit $$status } $$status=1 if /#W/;' - -test-with-coverage: doc - gap --quitonbreak --cover stats tst/testall.g - gap --quitonbreak --norepl -c 'LoadPackage("profiling"); OutputJsonCoverage("stats", "coverage.json");' - -test-spacing: - # exit code 1 means no match, which is what we want here (exit code 2 signals an error) - grep -R "[^ [\"] " gap/*.gi; test $$? -eq 1 || (echo "Duplicate spaces found" && exit 1) - grep -RE '[^ ] +$$' gap/*; test $$? -eq 1 || (echo "Trailing whitespace found" && exit 1) - for filename in gap/*; do \ - echo $$filename; \ - gap --quitonbreak --norepl --banner -c "LoadPackage(\"DeductiveSystemForCAP\"); SizeScreen([4096]); func := ReadAsFunction(\"$$filename\"); FileString(\"gap_spacing\", DisplayString(func));"; \ - # In a perfect world, the DisplayString of a function would exactly match our code. However, our line breaks and indentation might differ from the GAP ones, \ - # so we remove all indentation, line breaks, and empty lines, and afterwards insert line breaks at semicolons again for better readability. \ - cat "gap_spacing" | tail -n +2 | head -n -2 | sed 's/\[ \]/[ ]/g' | sed 's/( )/( )/g' | sed 's/( :/( :/g' | sed 's/ *$$//' | sed 's/^ *//' | grep -v "^$$" | tr "\n" " " | sed 's/;/;\n/g' > modified_gap_spacing; \ - cat "$$filename" | grep -v "^ *[#]" | sed 's/^ *//' | grep -v "^$$" | tr "\n" " " | sed "s/;/;\n/g" > modified_custom_spacing; \ - # Our code might still differ from the GAP code, for example because of additional brackets. \ - # Thus, we diff the code once as expected and once ignoring all space. Diffing the two diffs then shows lines which only differ by spacing. \ - diff modified_gap_spacing modified_custom_spacing > spacing_diff; \ - diff modified_gap_spacing modified_custom_spacing --ignore-all-space --ignore-space-change --ignore-trailing-space --ignore-blank-lines > spacing_diff_no_blanks; \ - diff spacing_diff_no_blanks spacing_diff || exit; \ - done - rm gap_spacing - rm modified_gap_spacing - rm modified_custom_spacing - rm spacing_diff - rm spacing_diff_no_blanks - -ci-test: test-basic-spacing test-with-coverage diff --git a/DeductiveSystemForCAP/read.g b/DeductiveSystemForCAP/read.g deleted file mode 100644 index 5b246dcb92..0000000000 --- a/DeductiveSystemForCAP/read.g +++ /dev/null @@ -1,4 +0,0 @@ -ReadPackage( "DeductiveSystemForCAP", "gap/DeductiveSystem.gi"); - -ReadPackage( "DeductiveSystemForCAP", "gap/LogicForDeductiveSystem.gi"); - diff --git a/DeductiveSystemForCAP/tst/100_LoadPackage.tst b/DeductiveSystemForCAP/tst/100_LoadPackage.tst deleted file mode 100644 index 0d945e51b4..0000000000 --- a/DeductiveSystemForCAP/tst/100_LoadPackage.tst +++ /dev/null @@ -1,15 +0,0 @@ -# SPDX-License-Identifier: GPL-2.0-or-later -# DeductiveSystemForCAP: Deductive system for CAP -# -# This file tests if the package can be loaded without errors or warnings. -# -# do not load suggested dependencies automatically -gap> PushOptions( rec( OnlyNeeded := true ) ); -gap> package_loading_info_level := InfoLevel( InfoPackageLoading );; -gap> SetInfoLevel( InfoPackageLoading, PACKAGE_ERROR );; -gap> LoadPackage( "DeductiveSystemForCAP", false ); -true -gap> SetInfoLevel( InfoPackageLoading, PACKAGE_INFO );; -gap> LoadPackage( "DeductiveSystemForCAP" ); -true -gap> SetInfoLevel( InfoPackageLoading, package_loading_info_level );; diff --git a/DeductiveSystemForCAP/tst/testall.g b/DeductiveSystemForCAP/tst/testall.g deleted file mode 100644 index 40ff96c257..0000000000 --- a/DeductiveSystemForCAP/tst/testall.g +++ /dev/null @@ -1,35 +0,0 @@ -# SPDX-License-Identifier: GPL-2.0-or-later -# DeductiveSystemForCAP: Deductive system for CAP -# -# This file runs package tests. It is also referenced in the package -# metadata in PackageInfo.g. -# -options := rec( - exitGAP := true, - testOptions := rec( - compareFunction := "uptowhitespace", - ), -); - -# reverse RecNames 50% of the time to detect code relying on the order of RecNames -if Random( RandomSource( IsMersenneTwister, NanosecondsSinceEpoch( ) ), [ false, true ] ) then - - Display( "Executing with reversed RecNames" ); - - MakeReadWriteGlobal( "RecNames" ); - - old_RecNames := RecNames; - - RecNames := record -> Reversed( old_RecNames( record ) ); - - MakeReadOnlyGlobal( "RecNames" ); - -else - - Display( "Executing with non-reversed RecNames" ); - -fi; - -TestDirectory( DirectoriesPackageLibrary( "DeductiveSystemForCAP", "tst" ), options ); - -FORCE_QUIT_GAP( 1 ); # if we ever get here, there was an error diff --git a/README.md b/README.md index 8f250281bb..af4078652b 100644 --- a/README.md +++ b/README.md @@ -27,7 +27,6 @@ Please take a look at our [manual](https://github.com/homalg-project/CAP_project | [CartesianCategories](CartesianCategories#readme) | Cartesian and cocartesian categories and various subdoctrines | [![HTML stable documentation][html-CartesianCategories-img]][html-CartesianCategories-url] [![PDF stable documentation][pdf-CartesianCategories-img]][pdf-CartesianCategories-url] | | [CompilerForCAP](CompilerForCAP#readme) | Speed up computations in CAP categories | [![HTML stable documentation][html-CompilerForCAP-img]][html-CompilerForCAP-url] [![PDF stable documentation][pdf-CompilerForCAP-img]][pdf-CompilerForCAP-url] | | [ComplexesAndFilteredObjectsForCAP](ComplexesAndFilteredObjectsForCAP#readme) | Implementation of complexes, cocomplexes and filtered objects for CAP | [![HTML stable documentation][html-ComplexesAndFilteredObjectsForCAP-img]][html-ComplexesAndFilteredObjectsForCAP-url] [![PDF stable documentation][pdf-ComplexesAndFilteredObjectsForCAP-img]][pdf-ComplexesAndFilteredObjectsForCAP-url] | -| [DeductiveSystemForCAP](DeductiveSystemForCAP#readme) | Deductive system for CAP | [![HTML stable documentation][html-DeductiveSystemForCAP-img]][html-DeductiveSystemForCAP-url] [![PDF stable documentation][pdf-DeductiveSystemForCAP-img]][pdf-DeductiveSystemForCAP-url] | | [FreydCategoriesForCAP](FreydCategoriesForCAP#readme) | Freyd categories - Formal (co)kernels for additive categories | [![HTML stable documentation][html-FreydCategoriesForCAP-img]][html-FreydCategoriesForCAP-url] [![PDF stable documentation][pdf-FreydCategoriesForCAP-img]][pdf-FreydCategoriesForCAP-url] | | [GeneralizedMorphismsForCAP](GeneralizedMorphismsForCAP#readme) | Implementations of generalized morphisms for the CAP project | [![HTML stable documentation][html-GeneralizedMorphismsForCAP-img]][html-GeneralizedMorphismsForCAP-url] [![PDF stable documentation][pdf-GeneralizedMorphismsForCAP-img]][pdf-GeneralizedMorphismsForCAP-url] | | [GradedModulePresentationsForCAP](GradedModulePresentationsForCAP#readme) | Presentations for graded modules | [![HTML stable documentation][html-GradedModulePresentationsForCAP-img]][html-GradedModulePresentationsForCAP-url] [![PDF stable documentation][pdf-GradedModulePresentationsForCAP-img]][pdf-GradedModulePresentationsForCAP-url] | @@ -82,13 +81,6 @@ Please take a look at our [manual](https://github.com/homalg-project/CAP_project [pdf-ComplexesAndFilteredObjectsForCAP-url]: https://homalg-project.github.io/CAP_project/ComplexesAndFilteredObjectsForCAP/download_pdf.html -[html-DeductiveSystemForCAP-img]: https://img.shields.io/badge/🔗%20HTML-stable-blue.svg -[html-DeductiveSystemForCAP-url]: https://homalg-project.github.io/CAP_project/DeductiveSystemForCAP/doc/chap0_mj.html - -[pdf-DeductiveSystemForCAP-img]: https://img.shields.io/badge/🔗%20PDF-stable-blue.svg -[pdf-DeductiveSystemForCAP-url]: https://homalg-project.github.io/CAP_project/DeductiveSystemForCAP/download_pdf.html - - [html-FreydCategoriesForCAP-img]: https://img.shields.io/badge/🔗%20HTML-stable-blue.svg [html-FreydCategoriesForCAP-url]: https://homalg-project.github.io/CAP_project/FreydCategoriesForCAP/doc/chap0_mj.html diff --git a/dev/codecov.yml b/dev/codecov.yml index 27aa8cc0e9..5d78868819 100644 --- a/dev/codecov.yml +++ b/dev/codecov.yml @@ -2,7 +2,7 @@ codecov: disable_default_path_fixes: true require_ci_to_pass: false comment: - after_n_builds: 18 + after_n_builds: 17 flags: CAP: paths: @@ -22,9 +22,6 @@ flags: ComplexesAndFilteredObjectsForCAP: paths: - "ComplexesAndFilteredObjectsForCAP/" - DeductiveSystemForCAP: - paths: - - "DeductiveSystemForCAP/" FreydCategoriesForCAP: paths: - "FreydCategoriesForCAP/" diff --git a/dev/make_dist.sh b/dev/make_dist.sh index e0444c2e12..8843ee79d0 100755 --- a/dev/make_dist.sh +++ b/dev/make_dist.sh @@ -32,11 +32,6 @@ echo "Release ComplexesAndFilteredObjectsForCAP" GAP_PKG_RELEASE_DATE=$(date -I) ./dev/release-gap-package --skip-existing-release --srcdir "$PWD/ComplexesAndFilteredObjectsForCAP" --webdir "$PWD/gh-pages/ComplexesAndFilteredObjectsForCAP" --update-script "$PWD/gh-pages/update.g" --release-script "$PWD/dev/.release" echo "" -# DeductiveSystemForCAP -echo "Release DeductiveSystemForCAP" -GAP_PKG_RELEASE_DATE=$(date -I) ./dev/release-gap-package --skip-existing-release --srcdir "$PWD/DeductiveSystemForCAP" --webdir "$PWD/gh-pages/DeductiveSystemForCAP" --update-script "$PWD/gh-pages/update.g" --release-script "$PWD/dev/.release" -echo "" - # FreydCategoriesForCAP echo "Release FreydCategoriesForCAP" GAP_PKG_RELEASE_DATE=$(date -I) ./dev/release-gap-package --skip-existing-release --srcdir "$PWD/FreydCategoriesForCAP" --webdir "$PWD/gh-pages/FreydCategoriesForCAP" --update-script "$PWD/gh-pages/update.g" --release-script "$PWD/dev/.release" diff --git a/dev/simulate_dist.sh b/dev/simulate_dist.sh index ac1de61e62..d093655b9a 100755 --- a/dev/simulate_dist.sh +++ b/dev/simulate_dist.sh @@ -32,11 +32,6 @@ echo "Simulate release of ComplexesAndFilteredObjectsForCAP" GAP_PKG_RELEASE_DATE=$(date -I) ./dev/release-gap-package --srcdir "$PWD/ComplexesAndFilteredObjectsForCAP" --webdir "$PWD/gh-pages/ComplexesAndFilteredObjectsForCAP" --update-script "$PWD/gh-pages/update.g" --release-script "$PWD/dev/.release" --only-tarball echo "" -# DeductiveSystemForCAP -echo "Simulate release of DeductiveSystemForCAP" -GAP_PKG_RELEASE_DATE=$(date -I) ./dev/release-gap-package --srcdir "$PWD/DeductiveSystemForCAP" --webdir "$PWD/gh-pages/DeductiveSystemForCAP" --update-script "$PWD/gh-pages/update.g" --release-script "$PWD/dev/.release" --only-tarball -echo "" - # FreydCategoriesForCAP echo "Simulate release of FreydCategoriesForCAP" GAP_PKG_RELEASE_DATE=$(date -I) ./dev/release-gap-package --srcdir "$PWD/FreydCategoriesForCAP" --webdir "$PWD/gh-pages/FreydCategoriesForCAP" --update-script "$PWD/gh-pages/update.g" --release-script "$PWD/dev/.release" --only-tarball diff --git a/dev/upload_codecov.sh b/dev/upload_codecov.sh index a4bb9ef884..dec4e661f2 100755 --- a/dev/upload_codecov.sh +++ b/dev/upload_codecov.sh @@ -47,10 +47,6 @@ while ! ./codecov -Z -v -s ../ -F ComplexesAndFilteredObjectsForCAP; do echo "Codecov upload failed, retrying in 60s" sleep 60 done -while ! ./codecov -Z -v -s ../ -F DeductiveSystemForCAP; do - echo "Codecov upload failed, retrying in 60s" - sleep 60 -done while ! ./codecov -Z -v -s ../ -F FreydCategoriesForCAP; do echo "Codecov upload failed, retrying in 60s" sleep 60 diff --git a/makefile b/makefile index 81d65d8f64..fac7ad6731 100644 --- a/makefile +++ b/makefile @@ -4,7 +4,7 @@ ci-test: ci-test_all_packages # BEGIN PACKAGE JANITOR ################################ -doc: doc_CAP doc_ActionsForCAP doc_AttributeCategoryForCAP doc_CartesianCategories doc_CompilerForCAP doc_ComplexesAndFilteredObjectsForCAP doc_DeductiveSystemForCAP doc_FreydCategoriesForCAP doc_GeneralizedMorphismsForCAP doc_GradedModulePresentationsForCAP doc_GroupRepresentationsForCAP doc_HomologicalAlgebraForCAP doc_InternalExteriorAlgebraForCAP doc_LinearAlgebraForCAP doc_ModulePresentationsForCAP doc_ModulesOverLocalRingsForCAP doc_MonoidalCategories doc_ToricSheaves +doc: doc_CAP doc_ActionsForCAP doc_AttributeCategoryForCAP doc_CartesianCategories doc_CompilerForCAP doc_ComplexesAndFilteredObjectsForCAP doc_FreydCategoriesForCAP doc_GeneralizedMorphismsForCAP doc_GradedModulePresentationsForCAP doc_GroupRepresentationsForCAP doc_HomologicalAlgebraForCAP doc_InternalExteriorAlgebraForCAP doc_LinearAlgebraForCAP doc_ModulePresentationsForCAP doc_ModulesOverLocalRingsForCAP doc_MonoidalCategories doc_ToricSheaves doc_CAP: $(MAKE) -C CAP doc @@ -24,9 +24,6 @@ doc_CompilerForCAP: doc_ComplexesAndFilteredObjectsForCAP: $(MAKE) -C ComplexesAndFilteredObjectsForCAP doc -doc_DeductiveSystemForCAP: - $(MAKE) -C DeductiveSystemForCAP doc - doc_FreydCategoriesForCAP: $(MAKE) -C FreydCategoriesForCAP doc @@ -61,7 +58,7 @@ doc_ToricSheaves: $(MAKE) -C ToricSheaves doc ################################ -test: doc test_CAP test_ActionsForCAP test_AttributeCategoryForCAP test_CartesianCategories test_CompilerForCAP test_ComplexesAndFilteredObjectsForCAP test_DeductiveSystemForCAP test_FreydCategoriesForCAP test_GeneralizedMorphismsForCAP test_GradedModulePresentationsForCAP test_GroupRepresentationsForCAP test_HomologicalAlgebraForCAP test_InternalExteriorAlgebraForCAP test_LinearAlgebraForCAP test_ModulePresentationsForCAP test_ModulesOverLocalRingsForCAP test_MonoidalCategories test_ToricSheaves +test: doc test_CAP test_ActionsForCAP test_AttributeCategoryForCAP test_CartesianCategories test_CompilerForCAP test_ComplexesAndFilteredObjectsForCAP test_FreydCategoriesForCAP test_GeneralizedMorphismsForCAP test_GradedModulePresentationsForCAP test_GroupRepresentationsForCAP test_HomologicalAlgebraForCAP test_InternalExteriorAlgebraForCAP test_LinearAlgebraForCAP test_ModulePresentationsForCAP test_ModulesOverLocalRingsForCAP test_MonoidalCategories test_ToricSheaves test_CAP: $(MAKE) -C CAP test @@ -81,9 +78,6 @@ test_CompilerForCAP: test_ComplexesAndFilteredObjectsForCAP: $(MAKE) -C ComplexesAndFilteredObjectsForCAP test -test_DeductiveSystemForCAP: - $(MAKE) -C DeductiveSystemForCAP test - test_FreydCategoriesForCAP: $(MAKE) -C FreydCategoriesForCAP test @@ -118,7 +112,7 @@ test_ToricSheaves: $(MAKE) -C ToricSheaves test ################################ -ci-test_all_packages: ci-test_CAP ci-test_ActionsForCAP ci-test_AttributeCategoryForCAP ci-test_CartesianCategories ci-test_CompilerForCAP ci-test_ComplexesAndFilteredObjectsForCAP ci-test_DeductiveSystemForCAP ci-test_FreydCategoriesForCAP ci-test_GeneralizedMorphismsForCAP ci-test_GradedModulePresentationsForCAP ci-test_GroupRepresentationsForCAP ci-test_HomologicalAlgebraForCAP ci-test_InternalExteriorAlgebraForCAP ci-test_LinearAlgebraForCAP ci-test_ModulePresentationsForCAP ci-test_ModulesOverLocalRingsForCAP ci-test_MonoidalCategories ci-test_ToricSheaves +ci-test_all_packages: ci-test_CAP ci-test_ActionsForCAP ci-test_AttributeCategoryForCAP ci-test_CartesianCategories ci-test_CompilerForCAP ci-test_ComplexesAndFilteredObjectsForCAP ci-test_FreydCategoriesForCAP ci-test_GeneralizedMorphismsForCAP ci-test_GradedModulePresentationsForCAP ci-test_GroupRepresentationsForCAP ci-test_HomologicalAlgebraForCAP ci-test_InternalExteriorAlgebraForCAP ci-test_LinearAlgebraForCAP ci-test_ModulePresentationsForCAP ci-test_ModulesOverLocalRingsForCAP ci-test_MonoidalCategories ci-test_ToricSheaves ci-test_CAP: $(MAKE) -C CAP ci-test @@ -138,9 +132,6 @@ ci-test_CompilerForCAP: ci-test_ComplexesAndFilteredObjectsForCAP: $(MAKE) -C ComplexesAndFilteredObjectsForCAP ci-test -ci-test_DeductiveSystemForCAP: - $(MAKE) -C DeductiveSystemForCAP ci-test - ci-test_FreydCategoriesForCAP: $(MAKE) -C FreydCategoriesForCAP ci-test From 4e6b39c636acdba9794eabe806da35ed6accb997 Mon Sep 17 00:00:00 2001 From: Fabian Zickgraf Date: Tue, 1 Aug 2023 12:20:54 +0200 Subject: [PATCH 2/4] Remove obsolete attribute --- CAP/gap/LogicForCAP.gd | 3 --- 1 file changed, 3 deletions(-) diff --git a/CAP/gap/LogicForCAP.gd b/CAP/gap/LogicForCAP.gd index 505ba8e28e..40d61ab8aa 100644 --- a/CAP/gap/LogicForCAP.gd +++ b/CAP/gap/LogicForCAP.gd @@ -52,6 +52,3 @@ DeclareGlobalFunction( "ADD_EVAL_RULES_TO_CATEGORY" ); ############################# DeclareGlobalFunction( "INSTALL_LOGICAL_IMPLICATIONS_HELPER" ); - -DeclareAttribute( "CAP_CATEGORY_SOURCE_RANGE_THEOREM_INSTALL_HELPER", - IsCapCategoryMorphism ); From 2ea57bbe25d40a5561943c094b683a62bd8d0e9d Mon Sep 17 00:00:00 2001 From: Fabian Zickgraf Date: Tue, 1 Aug 2023 12:21:23 +0200 Subject: [PATCH 3/4] Compute `property_of` from the existing information --- CAP/gap/MethodRecord.gi | 68 ++++++++++++++++++----------------------- 1 file changed, 29 insertions(+), 39 deletions(-) diff --git a/CAP/gap/MethodRecord.gi b/CAP/gap/MethodRecord.gi index 207a4f85ac..4ad86dd298 100644 --- a/CAP/gap/MethodRecord.gi +++ b/CAP/gap/MethodRecord.gi @@ -57,7 +57,6 @@ BindGlobal( "CAP_INTERNAL_VALID_METHOD_NAME_RECORD_COMPONENTS", # additional components which are deprecated or undocumented BindGlobal( "CAP_INTERNAL_LEGACY_METHOD_NAME_RECORD_COMPONENTS", [ - "property_of", "is_merely_set_theoretic", "is_reflected_by_faithful_functor", ] @@ -1243,7 +1242,6 @@ IsZeroForMorphisms := rec( filter_list := [ "category", "morphism" ], return_type := "bool", dual_operation := "IsZeroForMorphisms", - property_of := "morphism", is_reflected_by_faithful_functor := true, compatible_with_congruence_of_morphisms := true, ), @@ -2504,44 +2502,43 @@ IsZeroForObjects := rec( filter_list := [ "category", "object" ], return_type := "bool", dual_operation := "IsZeroForObjects", - property_of := "object" ), +), IsMonomorphism := rec( filter_list := [ "category", "morphism" ], return_type := "bool", dual_operation := "IsEpimorphism", - property_of := "morphism", - is_reflected_by_faithful_functor := true ), + is_reflected_by_faithful_functor := true, +), IsEpimorphism := rec( filter_list := [ "category", "morphism" ], return_type := "bool", dual_operation := "IsMonomorphism", - property_of := "morphism", - is_reflected_by_faithful_functor := true ), + is_reflected_by_faithful_functor := true, +), IsIsomorphism := rec( filter_list := [ "category", "morphism" ], dual_operation := "IsIsomorphism", return_type := "bool", - property_of := "morphism" ), +), IsEndomorphism := rec( filter_list := [ "category", "morphism" ], return_type := "bool", dual_operation := "IsEndomorphism", - property_of := "morphism" ), +), IsAutomorphism := rec( filter_list := [ "category", "morphism" ], return_type := "bool", dual_operation := "IsAutomorphism", - property_of := "morphism" ), +), IsOne := rec( filter_list := [ "category", "morphism" ], return_type := "bool", - property_of := "morphism", dual_operation := "IsOne", pre_function := function( cat, morphism ) @@ -2552,19 +2549,20 @@ IsOne := rec( fi; return [ true ]; - end ), + end, +), IsSplitMonomorphism := rec( filter_list := [ "category", "morphism" ], return_type := "bool", dual_operation := "IsSplitEpimorphism", - property_of := "morphism" ), +), IsSplitEpimorphism := rec( filter_list := [ "category", "morphism" ], return_type := "bool", dual_operation := "IsSplitMonomorphism", - property_of := "morphism" ), +), IsIdempotent := rec( pre_function := function( cat, morphism ) @@ -2582,49 +2580,49 @@ IsIdempotent := rec( filter_list := [ "category", "morphism" ], return_type := "bool", dual_operation := "IsIdempotent", - property_of := "morphism" ), +), IsBijectiveObject := rec( filter_list := [ "category", "object" ], return_type := "bool", dual_operation := "IsBijectiveObject", - property_of := "object" ), +), IsProjective := rec( filter_list := [ "category", "object" ], return_type := "bool", dual_operation := "IsInjective", - property_of := "object" ), +), IsInjective := rec( filter_list := [ "category", "object" ], return_type := "bool", dual_operation := "IsProjective", - property_of := "object" ), +), IsTerminal := rec( filter_list := [ "category", "object" ], return_type := "bool", dual_operation := "IsInitial", - property_of := "object" ), +), IsInitial := rec( filter_list := [ "category", "object" ], return_type := "bool", dual_operation := "IsTerminal", - property_of := "object" ), +), IsEqualToIdentityMorphism := rec( filter_list := [ "category", "morphism" ], return_type := "bool", dual_operation := "IsEqualToIdentityMorphism", - property_of := "morphism" ), +), IsEqualToZeroMorphism := rec( filter_list := [ "category", "morphism" ], return_type := "bool", dual_operation := "IsEqualToZeroMorphism", - property_of := "morphism" ), +), CoastrictionToImage := rec( filter_list := [ "category", "morphism" ], @@ -4746,7 +4744,11 @@ InstallValue( CAP_INTERNAL_FIND_OPPOSITE_PROPERTY_PAIRS_IN_METHOD_NAME_RECORD, current_rec := method_name_record.( current_recname ); - if not IsBound( current_rec.property_of ) then + if not (current_rec.return_type = "bool" and Length( current_rec.filter_list ) = 2) then + continue; + fi; + + if current_recname in [ "IsWellDefinedForObjects", "IsWellDefinedForMorphisms", "IsWellDefinedForTwoCells" ] then continue; fi; @@ -4761,25 +4763,13 @@ InstallValue( CAP_INTERNAL_FIND_OPPOSITE_PROPERTY_PAIRS_IN_METHOD_NAME_RECORD, fi; - if method_name_record.( current_recname ).property_of = "object" then - - if not current_entry in CAP_INTERNAL_OPPOSITE_PROPERTY_PAIRS_FOR_OBJECTS then - - Add( CAP_INTERNAL_OPPOSITE_PROPERTY_PAIRS_FOR_OBJECTS, current_entry ); - - fi; - - elif method_name_record.( current_recname ).property_of = "morphism" then + if current_rec.filter_list[2] = "object" then - if not current_entry in CAP_INTERNAL_OPPOSITE_PROPERTY_PAIRS_FOR_MORPHISMS then - - Add( CAP_INTERNAL_OPPOSITE_PROPERTY_PAIRS_FOR_MORPHISMS, current_entry ); - - fi; + AddSet( CAP_INTERNAL_OPPOSITE_PROPERTY_PAIRS_FOR_OBJECTS, current_entry ); - else + elif current_rec.filter_list[2] = "morphism" then - Error( "this should never happen" ); + AddSet( CAP_INTERNAL_OPPOSITE_PROPERTY_PAIRS_FOR_MORPHISMS, current_entry ); fi; From f3ab77da4d02b5a408c2f0bf38777fe10aa10339 Mon Sep 17 00:00:00 2001 From: Fabian Zickgraf Date: Tue, 1 Aug 2023 12:23:35 +0200 Subject: [PATCH 4/4] Bump version --- CAP/PackageInfo.g | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CAP/PackageInfo.g b/CAP/PackageInfo.g index fb54060bbb..cf32d36d07 100644 --- a/CAP/PackageInfo.g +++ b/CAP/PackageInfo.g @@ -10,7 +10,7 @@ SetPackageInfo( rec( PackageName := "CAP", Subtitle := "Categories, Algorithms, Programming", -Version := "2023.07-10", +Version := "2023.08-01", Date := (function ( ) if IsBound( GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE ) then return GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE; else return Concatenation( ~.Version{[ 1 .. 4 ]}, "-", ~.Version{[ 6, 7 ]}, "-01" ); fi; end)( ), License := "GPL-2.0-or-later",