refactor(Typology/Numeral): split numeral object from WALS survey

Linglib.lean

@@ -229,7 +229,8 @@ import Linglib.Typology.Directives
 import Linglib.Typology.Indefinite
 import Linglib.Typology.Profile
 import Linglib.Typology.Universal
-import Linglib.Typology.Numerals
+import Linglib.Typology.Numeral.Basic
+import Linglib.Typology.Numeral.WALS
 import Linglib.Typology.Plurals
 import Linglib.Typology.PolarityMarking
 import Linglib.Typology.Possession

Linglib/Fragments/Arabic/ModernStandard/Numerals.lean

@@ -1,4 +1,4 @@
-import Linglib.Typology.Numerals
+import Linglib.Typology.Numeral.WALS
 
 /-!
 # Modern Standard Arabic Numeral Profile (WALS Chs 53–56, 131)
@@ -9,7 +9,7 @@ per Ryding ch 15 (pp. 329–365).
 
 ## What's encoded vs documented
 
-The substrate `Typology.NumeralProfile` records a small set of
+The substrate `Numeral.Profile` records a small set of
 typological dimensions (ordinal-formation strategy, distributive
 marking, classifier presence, conjunction–quantifier identity, plural
 marking, base). The arithmetically richer phenomena MSA is famous for
@@ -46,15 +46,13 @@ namespace Fragments.Arabic.ModernStandard
     classifiers. *wa-* 'and' and *kull* 'all/every' are morphologically
     distinct. Dual + plural marking on counted nouns is obligatory.
     Decimal base (Ryding §15.1). -/
-def numeralProfile : Typology.NumeralProfile :=
-  { language := "Arabic (Modern Standard)"
-  , iso := "arb"
-  , ordinal := .firstSuppletion
-  , distributive := .markedByReduplication
-  , classifier := .absent
-  , conjQuant := .differentiation
-  , region := .westAsia
-  , pluralMarking := .obligatory
-  , numeralBase := some .decimal }
+def numeralProfile : Numeral.Profile :=
+  -- MSA (iso `arb`) is absent from WALS Chs 53/131; curated values kept for
+  -- those. Ch 54 defaults to `noDistributive`, matching the docstring (the
+  -- reduplication is intensifying, not a productive distributive).
+  { Numeral.Profile.fromWALS "Arabic (Modern Standard)" "arb"
+      (region := .westAsia) (pluralMarking := .obligatory) with
+    ordinal := .firstSuppletion
+    numeralBase := some .decimal }
 
 end Fragments.Arabic.ModernStandard

Linglib/Fragments/Bengali/Numerals.lean

@@ -1,4 +1,4 @@
-import Linglib.Typology.Numerals
+import Linglib.Typology.Numeral.WALS
 
 /-!
 # Bengali numeral profile (WALS Chs 53–56, 131)
@@ -11,15 +11,10 @@ namespace Fragments.Bengali
     suppletive. Distributive by reduplication. Optional classifiers (*tin-ta
     boi* 'three-CL book', but bare *tin boi* also grammatical). *Ebong* (and)
     differs from *sob* (all). Optional plural; decimal base. -/
-def numeralProfile : Typology.NumeralProfile :=
-  { language := "Bengali"
-  , iso := "ben"
-  , ordinal := .firstSuppletion
-  , distributive := .markedByReduplication
-  , classifier := .optional
-  , conjQuant := .differentiation
-  , region := .southAsia
-  , pluralMarking := .optional
-  , numeralBase := some .decimal }
+def numeralProfile : Numeral.Profile :=
+  -- Bengali (iso `ben`) is absent from WALS Ch 131; decimal base is curated.
+  { Numeral.Profile.fromWALS "Bengali" "ben" (region := .southAsia)
+      (pluralMarking := .optional) with
+    numeralBase := some .decimal }
 
 end Fragments.Bengali

Linglib/Fragments/Burmese/Numerals.lean

@@ -1,4 +1,4 @@
-import Linglib.Typology.Numerals
+import Linglib.Typology.Numeral.WALS
 
 /-!
 # Burmese numeral profile (WALS Chs 53–56, 131)
@@ -11,15 +11,7 @@ namespace Fragments.Burmese
     Pali; modern ordinals use *tha-* prefix); various pattern. Numeral
     classifiers obligatory (*lu thon yauk* 'person three CL'). No
     morphological distributive. No grammatical plural; decimal base. -/
-def numeralProfile : Typology.NumeralProfile :=
-  { language := "Burmese"
-  , iso := "mya"
-  , ordinal := .various
-  , distributive := .noDistributive
-  , classifier := .obligatory
-  , conjQuant := .differentiation
-  , region := .southeastAsia
-  , pluralMarking := .none
-  , numeralBase := some .decimal }
+def numeralProfile : Numeral.Profile :=
+  Numeral.Profile.fromWALS "Burmese" "mya" (region := .southeastAsia) (pluralMarking := .none)
 
 end Fragments.Burmese

Linglib/Fragments/English/Numerals.lean

@@ -1,4 +1,4 @@
-import Linglib.Typology.Numerals
+import Linglib.Typology.Numeral.WALS
 
 /-!
 # English numeral profile (WALS Chs 53–56, 131)
@@ -11,15 +11,7 @@ namespace Fragments.English
     suffix). No morphological distributive numerals (*two-each*), no numeral
     classifiers, conjunction *and* differs from universal *all*. Obligatory
     plural on nouns; decimal base. -/
-def numeralProfile : Typology.NumeralProfile :=
-  { language := "English"
-  , iso := "eng"
-  , ordinal := .firstSecondSuppletion
-  , distributive := .noDistributive
-  , classifier := .absent
-  , conjQuant := .differentiation
-  , region := .europe
-  , pluralMarking := .obligatory
-  , numeralBase := some .decimal }
+def numeralProfile : Numeral.Profile :=
+  Numeral.Profile.fromWALS "English" "eng" (region := .europe) (pluralMarking := .obligatory)
 
 end Fragments.English

Linglib/Fragments/Finnish/Numerals.lean

@@ -1,4 +1,4 @@
-import Linglib.Typology.Numerals
+import Linglib.Typology.Numeral.WALS
 
 /-!
 # Finnish numeral profile (WALS Chs 53–56, 131)
@@ -11,15 +11,7 @@ namespace Fragments.Finnish
     'different', higher ordinals regular with *-(n)s* suffix (*kolmas* 'third').
     No morphological distributive. No classifiers. *Ja* (and) differs from
     *kaikki* (all). Obligatory plural with *-t*; decimal base. -/
-def numeralProfile : Typology.NumeralProfile :=
-  { language := "Finnish"
-  , iso := "fin"
-  , ordinal := .firstSecondSuppletion
-  , distributive := .noDistributive
-  , classifier := .absent
-  , conjQuant := .differentiation
-  , region := .europe
-  , pluralMarking := .obligatory
-  , numeralBase := some .decimal }
+def numeralProfile : Numeral.Profile :=
+  Numeral.Profile.fromWALS "Finnish" "fin" (region := .europe) (pluralMarking := .obligatory)
 
 end Fragments.Finnish

Linglib/Fragments/Georgian/Numerals.lean

@@ -1,4 +1,4 @@
-import Linglib.Typology.Numerals
+import Linglib.Typology.Numeral.WALS
 
 /-!
 # Georgian numeral profile (WALS Chs 53–56, 131)
@@ -12,15 +12,7 @@ namespace Fragments.Georgian
     suffix *-agan* (*or-agan* 'two each'). No numeral classifiers. *Da* (and)
     differs from *q'vela* (all). Obligatory plural; hybrid vigesimal-decimal
     base. -/
-def numeralProfile : Typology.NumeralProfile :=
-  { language := "Georgian"
-  , iso := "kat"
-  , ordinal := .firstSuppletion
-  , distributive := .markedBySuffix
-  , classifier := .absent
-  , conjQuant := .differentiation
-  , region := .westAsia
-  , pluralMarking := .obligatory
-  , numeralBase := some .hybridVigesimalDecimal }
+def numeralProfile : Numeral.Profile :=
+  Numeral.Profile.fromWALS "Georgian" "kat" (region := .westAsia) (pluralMarking := .obligatory)
 
 end Fragments.Georgian

Linglib/Fragments/Hindi/Numerals.lean

@@ -1,4 +1,4 @@
-import Linglib.Typology.Numerals
+import Linglib.Typology.Numeral.WALS
 
 /-!
 # Hindi numeral profile (WALS Chs 53–56, 131)
@@ -11,15 +11,7 @@ namespace Fragments.Hindi
     suppletive, higher ordinals regular with *-vam* suffix. Distributive by
     reduplication (*do-do* 'two-two'). No numeral classifiers. *Aur* (and)
     differs from *sab* (all). Obligatory plural; decimal base. -/
-def numeralProfile : Typology.NumeralProfile :=
-  { language := "Hindi"
-  , iso := "hin"
-  , ordinal := .firstSecondSuppletion
-  , distributive := .markedByReduplication
-  , classifier := .absent
-  , conjQuant := .differentiation
-  , region := .southAsia
-  , pluralMarking := .obligatory
-  , numeralBase := some .decimal }
+def numeralProfile : Numeral.Profile :=
+  Numeral.Profile.fromWALS "Hindi" "hin" (region := .southAsia) (pluralMarking := .obligatory)
 
 end Fragments.Hindi

Linglib/Fragments/Hungarian/Numerals.lean

@@ -1,4 +1,4 @@
-import Linglib.Typology.Numerals
+import Linglib.Typology.Numeral.WALS
 
 /-!
 # Hungarian numeral profile (WALS Chs 53–56, 131)
@@ -12,15 +12,7 @@ namespace Fragments.Hungarian
     reduplication (*ket-ket* 'two-two'). No numeral classifiers. *És* (and)
     differs from *minden* (all/every). Obligatory plural with *-k*;
     decimal base. -/
-def numeralProfile : Typology.NumeralProfile :=
-  { language := "Hungarian"
-  , iso := "hun"
-  , ordinal := .firstSuppletion
-  , distributive := .markedByReduplication
-  , classifier := .absent
-  , conjQuant := .differentiation
-  , region := .europe
-  , pluralMarking := .obligatory
-  , numeralBase := some .decimal }
+def numeralProfile : Numeral.Profile :=
+  Numeral.Profile.fromWALS "Hungarian" "hun" (region := .europe) (pluralMarking := .obligatory)
 
 end Fragments.Hungarian

Linglib/Fragments/Indonesian/Numerals.lean

@@ -1,4 +1,4 @@
-import Linglib.Typology.Numerals
+import Linglib.Typology.Numeral.WALS
 
 /-!
 # Indonesian numeral profile (WALS Chs 53–56, 131)
@@ -12,15 +12,7 @@ namespace Fragments.Indonesian
     morphological distributive. Obligatory numeral classifiers (*tiga orang
     murid* 'three CL student'). *Dan* (and) differs from *semua* (all).
     Optional plural by reduplication; decimal base. -/
-def numeralProfile : Typology.NumeralProfile :=
-  { language := "Indonesian"
-  , iso := "ind"
-  , ordinal := .various
-  , distributive := .noDistributive
-  , classifier := .obligatory
-  , conjQuant := .differentiation
-  , region := .southeastAsia
-  , pluralMarking := .optional
-  , numeralBase := some .decimal }
+def numeralProfile : Numeral.Profile :=
+  Numeral.Profile.fromWALS "Indonesian" "ind" (region := .southeastAsia) (pluralMarking := .optional)
 
 end Fragments.Indonesian

Linglib/Fragments/Japanese/Numerals.lean

@@ -1,4 +1,4 @@
-import Linglib.Typology.Numerals
+import Linglib.Typology.Numeral.WALS
 
 /-!
 # Japanese numeral profile (WALS Chs 53–56, 131)
@@ -12,15 +12,7 @@ namespace Fragments.Japanese
     (*hitori-hitori* 'one by one'). Obligatory numeral classifiers (*san-nin*
     'three-CL.person'). Conjunction *to* differs from universal *subete*. No
     grammatical plural on common nouns; decimal base. -/
-def numeralProfile : Typology.NumeralProfile :=
-  { language := "Japanese"
-  , iso := "jpn"
-  , ordinal := .allFromCardinals
-  , distributive := .markedByReduplication
-  , classifier := .obligatory
-  , conjQuant := .differentiation
-  , region := .eastAsia
-  , pluralMarking := .none
-  , numeralBase := some .decimal }
+def numeralProfile : Numeral.Profile :=
+  Numeral.Profile.fromWALS "Japanese" "jpn" (region := .eastAsia) (pluralMarking := .none)
 
 end Fragments.Japanese

Linglib/Fragments/Korean/Numerals.lean

@@ -1,4 +1,4 @@
-import Linglib.Typology.Numerals
+import Linglib.Typology.Numeral.WALS
 
 /-!
 # Korean numeral profile (WALS Chs 53–56, 131)
@@ -7,20 +7,15 @@ import Linglib.Typology.Numerals
 
 namespace Fragments.Korean
 
-/-- Korean: ordinals use native numerals + *-jjae* suffix (*cheot-jjae* 'first'
-    partially suppletive). Distributive by suffix *-ssik* (*du-ssik* 'two
-    each'). Optional numeral classifiers (*se myeong-ui haksaeng* 'three CL
-    student'). *Gwa*/*wa* (and) differs from *modu* (all). Optional plural
-    with *-deul*; decimal base. -/
-def numeralProfile : Typology.NumeralProfile :=
-  { language := "Korean"
-  , iso := "kor"
-  , ordinal := .firstSuppletion
-  , distributive := .markedBySuffix
-  , classifier := .optional
-  , conjQuant := .differentiation
-  , region := .eastAsia
-  , pluralMarking := .optional
-  , numeralBase := some .decimal }
+/-- Korean. Coded after @cite{wals-2013}: WALS 53A codes Korean
+    "one-th, two-th, three-th" (Sino-Korean *je-* + cardinal, fully regular) →
+    `allFromCardinals`; the native paradigm's *cheot-jjae* 'first' suppletion is
+    a secondary system not picked up by the WALS coding. WALS 55A codes numeral
+    classifiers Obligatory (counting requires a classifier: *haksaeng se myeong*
+    'three CL student'). Distributive by suffix *-ssik* (*du-ssik* 'two each',
+    WALS 54A). *Gwa*/*wa* (and) differs from *modu* (all). Optional plural with
+    *-deul*; decimal base (WALS 131A). -/
+def numeralProfile : Numeral.Profile :=
+  Numeral.Profile.fromWALS "Korean" "kor" (region := .eastAsia) (pluralMarking := .optional)
 
 end Fragments.Korean

Linglib/Fragments/Mandarin/Numerals.lean

@@ -1,4 +1,4 @@
-import Linglib.Typology.Numerals
+import Linglib.Typology.Numeral.WALS
 
 /-!
 # Mandarin numeral profile (WALS Chs 53–56, 131)
@@ -12,15 +12,7 @@ namespace Fragments.Mandarin
     Obligatory numeral classifiers (*san ge ren* 'three CL person'). Conjunction
     *he* and universal *dou* are distinct morphemes. No grammatical plural on
     common nouns; decimal base. -/
-def numeralProfile : Typology.NumeralProfile :=
-  { language := "Mandarin"
-  , iso := "cmn"
-  , ordinal := .allFromCardinals
-  , distributive := .noDistributive
-  , classifier := .obligatory
-  , conjQuant := .differentiation
-  , region := .eastAsia
-  , pluralMarking := .none
-  , numeralBase := some .decimal }
+def numeralProfile : Numeral.Profile :=
+  Numeral.Profile.fromWALS "Mandarin" "cmn" (region := .eastAsia) (pluralMarking := .none)
 
 end Fragments.Mandarin

Linglib/Fragments/Mayan/Tseltal/Numerals.lean

@@ -1,4 +1,4 @@
-import Linglib.Typology.Numerals
+import Linglib.Typology.Numeral.WALS
 
 /-!
 # Tseltal numeral profile (WALS Chs 53–56, 131)
@@ -11,15 +11,12 @@ namespace Fragments.Mayan.Tseltal
     classifiers obligatory (distinct from Mayan noun classifiers). No
     morphological distributive. Conjunction and universal quantifier are
     differentiated. No obligatory plural on nouns; vigesimal base. -/
-def numeralProfile : Typology.NumeralProfile :=
-  { language := "Tseltal"
-  , iso := "tzh"
-  , ordinal := .noOrdinals
-  , distributive := .noDistributive
-  , classifier := .obligatory
-  , conjQuant := .differentiation
-  , region := .mesoamerica
-  , pluralMarking := .none
-  , numeralBase := some .vigesimal }
+def numeralProfile : Numeral.Profile :=
+  -- Tseltal (iso `tzh`) is in WALS only for Ch 55 (classifiers); ordinal and
+  -- base are curated (absent from Chs 53/131).
+  { Numeral.Profile.fromWALS "Tseltal" "tzh" (region := .mesoamerica)
+      (pluralMarking := .none) with
+    ordinal := .noOrdinals
+    numeralBase := some .vigesimal }
 
 end Fragments.Mayan.Tseltal

Linglib/Fragments/Slavic/Russian/Numerals.lean

@@ -1,4 +1,4 @@
-import Linglib.Typology.Numerals
+import Linglib.Typology.Numeral.WALS
 
 /-!
 # Russian numeral profile (WALS Chs 53–56, 131)
@@ -12,15 +12,7 @@ namespace Fragments.Slavic.Russian
     'fourth'). No morphological distributive (uses prepositional phrase
     *po + dative*). No numeral classifiers. *I* (and) differs from *vse*
     (all). Obligatory plural; decimal base. -/
-def numeralProfile : Typology.NumeralProfile :=
-  { language := "Russian"
-  , iso := "rus"
-  , ordinal := .firstSecondSuppletion
-  , distributive := .noDistributive
-  , classifier := .absent
-  , conjQuant := .differentiation
-  , region := .europe
-  , pluralMarking := .obligatory
-  , numeralBase := some .decimal }
+def numeralProfile : Numeral.Profile :=
+  Numeral.Profile.fromWALS "Russian" "rus" (region := .europe) (pluralMarking := .obligatory)
 
 end Fragments.Slavic.Russian