@@ -373,6 +373,82 @@ impl Aspect {
373373 _ => AspectCategory :: Other ,
374374 }
375375 }
376+
377+ /// Get snake_case slug for use in dotted domain keys.
378+ pub fn slug ( & self ) -> & ' static str {
379+ match self {
380+ Aspect :: PropositionalLogic => "propositional_logic" ,
381+ Aspect :: PredicateLogic => "predicate_logic" ,
382+ Aspect :: ModalLogic => "modal_logic" ,
383+ Aspect :: TemporalLogic => "temporal_logic" ,
384+ Aspect :: HigherOrderLogic => "higher_order_logic" ,
385+ Aspect :: IntuitionisticLogic => "intuitionistic_logic" ,
386+ Aspect :: ClassicalLogic => "classical_logic" ,
387+ Aspect :: NaturalNumbers => "natural_numbers" ,
388+ Aspect :: Integers => "integers" ,
389+ Aspect :: Rationals => "rationals" ,
390+ Aspect :: Reals => "reals" ,
391+ Aspect :: Complex => "complex" ,
392+ Aspect :: NumberTheory => "number_theory" ,
393+ Aspect :: Arithmetic => "arithmetic" ,
394+ Aspect :: Groups => "groups" ,
395+ Aspect :: Rings => "rings" ,
396+ Aspect :: Fields => "fields" ,
397+ Aspect :: VectorSpaces => "vector_spaces" ,
398+ Aspect :: Modules => "modules" ,
399+ Aspect :: Lattices => "lattices" ,
400+ Aspect :: CategoryTheory => "category_theory" ,
401+ Aspect :: UniversalAlgebra => "universal_algebra" ,
402+ Aspect :: Limits => "limits" ,
403+ Aspect :: Continuity => "continuity" ,
404+ Aspect :: Derivatives => "derivatives" ,
405+ Aspect :: Integrals => "integrals" ,
406+ Aspect :: Sequences => "sequences" ,
407+ Aspect :: MeasureTheory => "measure_theory" ,
408+ Aspect :: FunctionalAnalysis => "functional_analysis" ,
409+ Aspect :: MetricSpaces => "metric_spaces" ,
410+ Aspect :: TopologicalSpaces => "topological_spaces" ,
411+ Aspect :: Compactness => "compactness" ,
412+ Aspect :: Connectedness => "connectedness" ,
413+ Aspect :: TopologicalContinuity => "topological_continuity" ,
414+ Aspect :: SetOperations => "set_operations" ,
415+ Aspect :: Cardinality => "cardinality" ,
416+ Aspect :: Ordinals => "ordinals" ,
417+ Aspect :: AxiomOfChoice => "axiom_of_choice" ,
418+ Aspect :: ZFC => "zfc" ,
419+ Aspect :: DependentTypes => "dependent_types" ,
420+ Aspect :: Universes => "universes" ,
421+ Aspect :: InductiveTypes => "inductive_types" ,
422+ Aspect :: CoinductiveTypes => "coinductive_types" ,
423+ Aspect :: Polymorphism => "polymorphism" ,
424+ Aspect :: TypeEquivalence => "type_equivalence" ,
425+ Aspect :: Algorithms => "algorithms" ,
426+ Aspect :: Complexity => "complexity" ,
427+ Aspect :: FormalVerification => "formal_verification" ,
428+ Aspect :: ProgramSemantics => "program_semantics" ,
429+ Aspect :: Concurrency => "concurrency" ,
430+ Aspect :: Cryptography => "cryptography" ,
431+ Aspect :: Automata => "automata" ,
432+ Aspect :: LambdaCalculus => "lambda_calculus" ,
433+ Aspect :: Induction => "induction" ,
434+ Aspect :: Coinduction => "coinduction" ,
435+ Aspect :: Recursion => "recursion" ,
436+ Aspect :: CaseAnalysis => "case_analysis" ,
437+ Aspect :: Contradiction => "contradiction" ,
438+ Aspect :: DirectProof => "direct_proof" ,
439+ Aspect :: Combinatorics => "combinatorics" ,
440+ Aspect :: GraphTheory => "graph_theory" ,
441+ Aspect :: Probability => "probability" ,
442+ Aspect :: GameTheory => "game_theory" ,
443+ Aspect :: Geometry => "geometry" ,
444+ Aspect :: AbstractNonsense => "abstract_nonsense" ,
445+ }
446+ }
447+
448+ /// Canonical dotted domain key: `"category.aspect"` (e.g. `"arithmetic.natural_numbers"`).
449+ pub fn dotted_key ( & self ) -> String {
450+ format ! ( "{}.{}" , self . category( ) . slug( ) , self . slug( ) )
451+ }
376452}
377453
378454impl fmt:: Display for Aspect {
@@ -396,6 +472,24 @@ pub enum AspectCategory {
396472 Other ,
397473}
398474
475+ impl AspectCategory {
476+ /// Get snake_case slug for use in dotted domain keys.
477+ pub fn slug ( & self ) -> & ' static str {
478+ match self {
479+ AspectCategory :: Logic => "logic" ,
480+ AspectCategory :: Arithmetic => "arithmetic" ,
481+ AspectCategory :: Algebra => "algebra" ,
482+ AspectCategory :: Analysis => "analysis" ,
483+ AspectCategory :: Topology => "topology" ,
484+ AspectCategory :: SetTheory => "set_theory" ,
485+ AspectCategory :: TypeTheory => "type_theory" ,
486+ AspectCategory :: ComputerScience => "computer_science" ,
487+ AspectCategory :: ProofTechniques => "proof_techniques" ,
488+ AspectCategory :: Other => "other" ,
489+ }
490+ }
491+ }
492+
399493/// Features extracted from a theorem for aspect classification
400494#[ derive( Debug , Clone , Default ) ]
401495pub struct TheoremFeatures {
@@ -1149,4 +1243,109 @@ mod tests {
11491243
11501244 assert ! ( aspects. contains( & Aspect :: Induction ) ) ;
11511245 }
1246+
1247+ #[ test]
1248+ fn test_dotted_key_eponymous_category ( ) {
1249+ assert_eq ! ( Aspect :: Arithmetic . dotted_key( ) , "arithmetic.arithmetic" ) ;
1250+ }
1251+
1252+ #[ test]
1253+ fn test_dotted_key_natural_numbers ( ) {
1254+ assert_eq ! ( Aspect :: NaturalNumbers . dotted_key( ) , "arithmetic.natural_numbers" ) ;
1255+ }
1256+
1257+ #[ test]
1258+ fn test_dotted_key_groups ( ) {
1259+ assert_eq ! ( Aspect :: Groups . dotted_key( ) , "algebra.groups" ) ;
1260+ }
1261+
1262+ #[ test]
1263+ fn test_dotted_key_propositional_logic ( ) {
1264+ assert_eq ! ( Aspect :: PropositionalLogic . dotted_key( ) , "logic.propositional_logic" ) ;
1265+ }
1266+
1267+ #[ test]
1268+ fn test_dotted_key_zfc ( ) {
1269+ assert_eq ! ( Aspect :: ZFC . dotted_key( ) , "set_theory.zfc" ) ;
1270+ }
1271+
1272+ #[ test]
1273+ fn test_all_variants_have_exactly_one_dot ( ) {
1274+ let all_aspects = [
1275+ Aspect :: PropositionalLogic ,
1276+ Aspect :: PredicateLogic ,
1277+ Aspect :: ModalLogic ,
1278+ Aspect :: TemporalLogic ,
1279+ Aspect :: HigherOrderLogic ,
1280+ Aspect :: IntuitionisticLogic ,
1281+ Aspect :: ClassicalLogic ,
1282+ Aspect :: NaturalNumbers ,
1283+ Aspect :: Integers ,
1284+ Aspect :: Rationals ,
1285+ Aspect :: Reals ,
1286+ Aspect :: Complex ,
1287+ Aspect :: NumberTheory ,
1288+ Aspect :: Arithmetic ,
1289+ Aspect :: Groups ,
1290+ Aspect :: Rings ,
1291+ Aspect :: Fields ,
1292+ Aspect :: VectorSpaces ,
1293+ Aspect :: Modules ,
1294+ Aspect :: Lattices ,
1295+ Aspect :: CategoryTheory ,
1296+ Aspect :: UniversalAlgebra ,
1297+ Aspect :: Limits ,
1298+ Aspect :: Continuity ,
1299+ Aspect :: Derivatives ,
1300+ Aspect :: Integrals ,
1301+ Aspect :: Sequences ,
1302+ Aspect :: MeasureTheory ,
1303+ Aspect :: FunctionalAnalysis ,
1304+ Aspect :: MetricSpaces ,
1305+ Aspect :: TopologicalSpaces ,
1306+ Aspect :: Compactness ,
1307+ Aspect :: Connectedness ,
1308+ Aspect :: TopologicalContinuity ,
1309+ Aspect :: SetOperations ,
1310+ Aspect :: Cardinality ,
1311+ Aspect :: Ordinals ,
1312+ Aspect :: AxiomOfChoice ,
1313+ Aspect :: ZFC ,
1314+ Aspect :: DependentTypes ,
1315+ Aspect :: Universes ,
1316+ Aspect :: InductiveTypes ,
1317+ Aspect :: CoinductiveTypes ,
1318+ Aspect :: Polymorphism ,
1319+ Aspect :: TypeEquivalence ,
1320+ Aspect :: Algorithms ,
1321+ Aspect :: Complexity ,
1322+ Aspect :: FormalVerification ,
1323+ Aspect :: ProgramSemantics ,
1324+ Aspect :: Concurrency ,
1325+ Aspect :: Cryptography ,
1326+ Aspect :: Automata ,
1327+ Aspect :: LambdaCalculus ,
1328+ Aspect :: Induction ,
1329+ Aspect :: Coinduction ,
1330+ Aspect :: Recursion ,
1331+ Aspect :: CaseAnalysis ,
1332+ Aspect :: Contradiction ,
1333+ Aspect :: DirectProof ,
1334+ Aspect :: Combinatorics ,
1335+ Aspect :: GraphTheory ,
1336+ Aspect :: Probability ,
1337+ Aspect :: GameTheory ,
1338+ Aspect :: Geometry ,
1339+ Aspect :: AbstractNonsense ,
1340+ ] ;
1341+ for aspect in & all_aspects {
1342+ let key = aspect. dotted_key ( ) ;
1343+ let dot_count = key. chars ( ) . filter ( |& c| c == '.' ) . count ( ) ;
1344+ assert_eq ! (
1345+ dot_count, 1 ,
1346+ "Expected exactly one dot in dotted_key for {:?}, got: {}" ,
1347+ aspect, key
1348+ ) ;
1349+ }
1350+ }
11521351}
0 commit comments