Skip to content

Commit

Permalink
Merge pull request #261 from zickgraf/master
Browse files Browse the repository at this point in the history
  • Loading branch information
zickgraf authored Sep 25, 2024
2 parents f391737 + d4168de commit d7f04f7
Show file tree
Hide file tree
Showing 2 changed files with 53 additions and 13 deletions.
2 changes: 1 addition & 1 deletion PackageInfo.g
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ SetPackageInfo( rec(

PackageName := "FinSetsForCAP",
Subtitle := "The elementary topos of (skeletal) finite sets",
Version := "2024.08-01",
Version := "2024.09-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",
Expand Down
64 changes: 52 additions & 12 deletions gap/SkeletalFinSets.gi
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,12 @@ InstallMethod( SkeletalCategoryOfFiniteSets,

FunctionWithNamedArguments(
[
[ "FinalizeCategory", true ],
[ "no_precompiled_code", false ],
[ "overhead", true ],
],
function ( CAP_NAMED_ARGUMENTS )
local cat;
local cat, expected_weight;

cat := CreateCapCategoryWithDataTypes(
"SkeletalFinSets", IsSkeletalCategoryOfFiniteSets,
Expand Down Expand Up @@ -58,7 +59,44 @@ InstallMethod( SkeletalCategoryOfFiniteSets,

fi;

Finalize( cat );
if CAP_NAMED_ARGUMENTS.FinalizeCategory then

Finalize( cat );

# check weights of operations using other primitive operations
if CAP_NAMED_ARGUMENTS.no_precompiled_code then

##
expected_weight := 1 + Sum( [ [ "ExponentialOnObjects", 1 ],
[ "ExactCoverWithGlobalElements", 1 ],
[ "PreComposeList", 2 ],
[ "CartesianLambdaElimination", 2 ],
[ "DirectProductToExponentialRightAdjunctMorphismWithGivenExponential", 2 ] ],
e -> e[2] * CurrentOperationWeight( cat!.derivations_weight_list, e[1] ) );

if CurrentOperationWeight( cat!.derivations_weight_list, "ExponentialOnMorphismsWithGivenExponentials" ) <> expected_weight then

# COVERAGE_IGNORE_NEXT_LINE
Print( "WARNING: please update the weight of ExponentialOnMorphismsWithGivenExponentials in SkeletalFinSetsForCAP to ", String( expected_weight ), "\n" );

fi;

##
expected_weight := 1 + Sum( [ [ "ExponentialOnObjects", 1 ],
[ "ExactCoverWithGlobalElements", 1 ],
[ "CartesianLambdaElimination", 2 ] ],
e -> e[2] * CurrentOperationWeight( cat!.derivations_weight_list, e[1] ) );

if CurrentOperationWeight( cat!.derivations_weight_list, "MorphismsOfExternalHom" ) <> expected_weight then

# COVERAGE_IGNORE_NEXT_LINE
Print( "WARNING: please update the weight of MorphismsOfExternalHom in SkeletalFinSetsForCAP to ", String( expected_weight ), "\n" );

fi;

fi;

fi;

return cat;

Expand Down Expand Up @@ -914,12 +952,13 @@ AddExponentialOnMorphismsWithGivenExponentials( SkeletalFinSets,
range_beta ) ) )[1 + 0] ),
T );

end, 1 + Sum( [ [ "ExponentialOnObjects", 1 ],
[ "ExactCoverWithGlobalElements", 1 ],
[ "PreComposeList", 2 ],
[ "CartesianLambdaElimination", 2 ],
[ "DirectProductToExponentialRightAdjunctMorphismWithGivenExponential", 2 ] ],
e -> e[2] * CurrentOperationWeight( SkeletalFinSets!.derivations_weight_list, e[1] ) ) );
end, 1403 ); # weight = 1 + Sum(
# [ [ "ExponentialOnObjects", 1 ],
# [ "ExactCoverWithGlobalElements", 1 ],
# [ "PreComposeList", 2 ],
# [ "CartesianLambdaElimination", 2 ],
# [ "DirectProductToExponentialRightAdjunctMorphismWithGivenExponential", 2 ] ],
# e -> e[2] * CurrentOperationWeight( SkeletalFinSets!.derivations_weight_list, e[1] ) )

## Bᴸ × L → B
AddCartesianLeftEvaluationMorphismWithGivenSource( SkeletalFinSets,
Expand Down Expand Up @@ -1018,10 +1057,11 @@ AddMorphismsOfExternalHom( SkeletalFinSets,
B,
mor ) );

end, 1 + Sum( [ [ "ExponentialOnObjects", 1 ],
[ "ExactCoverWithGlobalElements", 1 ],
[ "CartesianLambdaElimination", 2 ] ],
e -> e[2] * CurrentOperationWeight( SkeletalFinSets!.derivations_weight_list, e[1] ) ) );
end, 401 ); # weight = 1 + Sum( [
# [ "ExponentialOnObjects", 1 ],
# [ "ExactCoverWithGlobalElements", 1 ],
# [ "CartesianLambdaElimination", 2 ] ],
# e -> e[2] * CurrentOperationWeight( SkeletalFinSets!.derivations_weight_list, e[1] ) ) );

end );

Expand Down

0 comments on commit d7f04f7

Please sign in to comment.