From 09746cda2d48517ec5d296f67a6ff4c825f81e68 Mon Sep 17 00:00:00 2001 From: Mohamed Barakat Date: Wed, 7 Jun 2023 16:59:07 +0200 Subject: [PATCH] outsourced a derivation of IsHomSetInhabited from Toposes to FinSetsForCAP --- PackageInfo.g | 2 +- ...SkeletalFinSetsWithMorphismsGivenByLists.g | 1 + gap/CompilerLogic.gi | 9 ++++++ gap/SkeletalFinSets.gi | 29 ++++++++++++++----- ...etsWithMorphismsGivenByListsPrecompiled.gi | 2 +- 5 files changed, 33 insertions(+), 10 deletions(-) diff --git a/PackageInfo.g b/PackageInfo.g index 868f91d..f314a9f 100644 --- a/PackageInfo.g +++ b/PackageInfo.g @@ -10,7 +10,7 @@ SetPackageInfo( rec( PackageName := "FinSetsForCAP", Subtitle := "The elementary topos of (skeletal) finite sets", -Version := "2023.06-05", +Version := "2023.06-06", 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", diff --git a/examples/PrecompileCategoryOfSkeletalFinSetsWithMorphismsGivenByLists.g b/examples/PrecompileCategoryOfSkeletalFinSetsWithMorphismsGivenByLists.g index a473ffc..df2e007 100644 --- a/examples/PrecompileCategoryOfSkeletalFinSetsWithMorphismsGivenByLists.g +++ b/examples/PrecompileCategoryOfSkeletalFinSetsWithMorphismsGivenByLists.g @@ -24,6 +24,7 @@ primitive_operations := category_constructor( : no_precompiled_code := true ) );; list_of_operations := SortedList( Concatenation( primitive_operations, [ + "IsHomSetInhabited", "TruthMorphismOfImplies", #"HasPushoutComplement", "PushoutComplement", diff --git a/gap/CompilerLogic.gi b/gap/CompilerLogic.gi index 22011ba..de3af4a 100644 --- a/gap/CompilerLogic.gi +++ b/gap/CompilerLogic.gi @@ -431,6 +431,15 @@ CapJitAddLogicTemplate( ) ); +CapJitAddLogicTemplate( + rec( + variable_names := [ "number1", "number2" ], + variable_filters := [ IsBigInt, IsBigInt ], + src_template := "not number2 ^ number1 = 0", + dst_template := "number1 = 0 or not number2 = 0", + ) +); + CapJitAddLogicTemplate( rec( variable_names := [ "entry", "func" ], diff --git a/gap/SkeletalFinSets.gi b/gap/SkeletalFinSets.gi index f5708fd..97fe945 100644 --- a/gap/SkeletalFinSets.gi +++ b/gap/SkeletalFinSets.gi @@ -331,14 +331,6 @@ AddIsEqualForMorphisms( SkeletalFinSets, end ); -## -AddIsHomSetInhabited( SkeletalFinSets, - function ( cat, A, B ) - - return IsInitial( cat, A ) or not IsInitial( cat, B ); - -end ); - ## AddIdentityMorphism( SkeletalFinSets, function ( cat, n ) @@ -985,6 +977,27 @@ end, 1 + Sum( [ [ "ExponentialOnObjects", 1 ], end ); +## +AddDerivationToCAP( IsHomSetInhabited, + "IsHomSetInhabited using IsInitial when the range category of the homomorphism structure is the skeletal category of finite sets", + [ [ HomomorphismStructureOnObjects, 1 ], + [ IsInitial, 1, RangeCategoryOfHomomorphismStructure ] ], + + function ( cat, a, b ) + local range_cat; + + range_cat := RangeCategoryOfHomomorphismStructure( cat ); + + return not IsInitial( range_cat, + HomomorphismStructureOnObjects( cat, a, b ) ); + +end : CategoryGetters := rec( range_cat := RangeCategoryOfHomomorphismStructure ), +CategoryFilter := + function ( cat ) + return HasRangeCategoryOfHomomorphismStructure( cat ) and + IsCategoryOfSkeletalFinSets( RangeCategoryOfHomomorphismStructure( cat ) ); +end ); + ## InstallMethod( String, "for a CAP skeletal finite set", diff --git a/gap/precompiled_categories/CategoryOfSkeletalFinSetsWithMorphismsGivenByListsPrecompiled.gi b/gap/precompiled_categories/CategoryOfSkeletalFinSetsWithMorphismsGivenByListsPrecompiled.gi index 10db28c..e4b4f3c 100644 --- a/gap/precompiled_categories/CategoryOfSkeletalFinSetsWithMorphismsGivenByListsPrecompiled.gi +++ b/gap/precompiled_categories/CategoryOfSkeletalFinSetsWithMorphismsGivenByListsPrecompiled.gi @@ -449,7 +449,7 @@ function ( cat_1, arg2_1, arg3_1 ) end ######## - , 100 ); + , 202 : IsPrecompiledDerivation := true ); ## AddIsInitial( cat,