extensions by Codex

This commit is contained in:
Krasimir Angelov
2026-09-28 20:45:48 +02:00
parent 2d6beba1e6
commit 70ebabfba8
25 changed files with 1095 additions and 653 deletions
+63 -111
View File
@@ -1,117 +1,69 @@
concrete NumeralGla of Numeral = CatGla [Numeral,Digits] **
concrete NumeralGla of Numeral = CatGla [Numeral,Digits,Decimal] **
open Prelude, ResGla in {
{-
lincat
Digit = LinNumeral ; -- 2..9
Sub10, -- 1..9
Sub100, -- 1..99
Sub1000, -- 1..999
Sub1000000, -- 1..999999
Sub1000000000, -- 1..999999999
Sub1000000000000 -- 1..999999999999
= LinNumeral ;
-- param CardOrd defined in ResGla
-- type LinNumeral -""-
lincat
Digit, Sub10, Sub100, Sub1000, Sub1000000,
Sub1000000000, Sub1000000000000, Dig = LinNumeral ;
lin
num x = x ;
n2 = mkNumeral "dhà" "dàrna" ;
n3 = mkNumeral "trì" "treas" ;
n4 = mkNumeral "ceithir" "ceathramh" ;
n5 = mkNumeral "còig" "còigeamh" ;
n6 = mkNumeral "sia" "siathamh" ;
n7 = mkNumeral "seachd" "seachdamh" ;
n8 = mkNumeral "ochd" "ochdamh" ;
n9 = mkNumeral "naoi" "naoidheamh" ;
pot01 = one ;
pot0 d = d ;
pot0as1 n = n ;
pot110 = mkNumeral "deich" "deicheamh" ;
pot111 = mkNumeral "aon deug" "aonamh deug" ;
pot1to19 d = join "deug" d ;
pot1 d = join "deich" d ;
pot1plus d e = plus (join "deich" d) e ;
pot1as2 n = n ;
pot21 = mkNumeral "ceud" "ceudamh" ;
pot2 d = join "ceud" d ;
pot2plus d e = plus (join "ceud" d) e ;
pot2as3 n = n ;
pot31 = mkNumeral "mìle" "mìleamh" ;
pot3 d = join "mìle" d ;
pot3plus d e = plus (join "mìle" d) e ;
pot3as4 n = n ;
pot3decimal d = mkNumeral (d.s ++ "mìle") (d.s ++ "mìleamh") ;
pot41 = mkNumeral "millean" "milleanamh" ;
pot4 d = join "millean" d ;
pot4plus d e = plus (join "millean" d) e ;
pot4as5 n = n ;
pot4decimal d = mkNumeral (d.s ++ "millean") (d.s ++ "milleanamh") ;
pot51 = mkNumeral "billean" "billeanamh" ;
pot5 d = join "billean" d ;
pot5plus d e = plus (join "billean" d) e ;
pot5decimal d = mkNumeral (d.s ++ "billean") (d.s ++ "billeanamh") ;
lin
-- : Sub1000000 -> Numeral ; -- 123456 [coercion to top category]
num x = x ;
IDig d = d ;
IIDig d ds = {
s = table {NCard => d.s ! NCard ++ BIND ++ ds.s ! NCard ; NOrd => d.s ! NCard ++ BIND ++ ds.s ! NOrd} ;
n = Pl
} ;
D_0 = digit "0" ; D_1 = digit "1" ; D_2 = digit "2" ; D_3 = digit "3" ;
D_4 = digit "4" ; D_5 = digit "5" ; D_6 = digit "6" ; D_7 = digit "7" ;
D_8 = digit "8" ; D_9 = digit "9" ;
PosDecimal ds = {s = ds.s ! NCard} ;
NegDecimal ds = {s = "-" ++ BIND ++ ds.s ! NCard} ;
IFrac d x = {s = d.s ++ "." ++ x.s ! NCard} ;
-- : Digit ;
n2 = mkNumeral "two" ;
n3 = mkNumeral "three" ;
n4 = mkNumeral "four" ;
n5 = mkNumeral "five" ;
n6 = mkNumeral "six" ;
n7 = mkNumeral "seven" ;
n8 = mkNumeral "eight" ;
n9 = mkNumeral "nine" ;
-- : Sub10 ; -- 1
-- pot01 =
-- : Digit -> Sub10 ; -- d * 1
pot0 d = d ;
-- : Sub100 ; -- 10
-- pot110 = mkNum "ten" ;
-- : Sub100 ; -- 11
-- pot111 = mkNum "eleven" ;
-- : Digit -> Sub100 ; -- 10 + d
-- pot1to19 d =
-- : Sub10 -> Sub100 ; -- coercion of 1..9
pot0as1 n = n ;
-- : Digit -> Sub100 ; -- d * 10
-- pot1 d =
-- : Digit -> Sub10 -> Sub100 ; -- d * 10 + n
-- pot1plus d e =
-- : Sub100 -> Sub1000 ; -- coercion of 1..99
pot1as2 n = n ;
-- : Sub10 -> Sub1000 ; -- m * 100
-- pot2 d =
-- : Sub10 -> Sub100 -> Sub1000 ; -- m * 100 + n
-- pot2plus d e =
-- : Sub1000 -> Sub1000000 ; -- coercion of 1..999
pot2as3 n = n ;
-- : Sub1000 -> Sub1000000 ; -- m * 1000
-- pot3 d =
-- : Sub1000 -> Sub1000 -> Sub1000000 ; -- m * 1000 + n
-- pot3plus d e =
--------------------------------------------------------------------------------
-- Numerals as sequences of digits have a separate, simpler grammar
--
lincat
Dig = LinDig ; -- single digit 0..9
lin
-- : Dig -> Digits ; -- 8
IDig d = d ;
-- : Dig -> Digits -> Digits ; -- 876
IIDig d e = {
s = table {
NCard => glue (d.s ! NCard) (e.s ! NCard) ;
NOrd => glue (d.s ! NCard) (e.s ! NOrd)
} ;
n = Pl ;
} ;
-- : Dig ;
D_0 = mkDig "0" ;
D_1 = mkDig "1" ;
D_2 = mkDig "2" ;
D_3 = mkDig "3" ;
D_4 = mkDig "4" ;
D_5 = mkDig "5" ;
D_6 = mkDig "6" ;
D_7 = mkDig "7" ;
D_8 = mkDig "8" ;
D_9 = mkDig "9" ;
oper
LinDig : Type = {s : CardOrd => Str ; n : Number} ;
mkDig : Str -> LinDig = \s -> {
s = table {
NCard => s ;
NOrd => s + "th"
} ;
n = Pl ; -- TODO: handle number 1
} ;
-}
oper
one : LinNumeral = {s = table {NCard => "aon" ; NOrd => "ciad"} ; n = Sg} ;
digit : Str -> LinNumeral = \x -> {s = table {NCard => x ; NOrd => x} ; n = Pl} ;
join : Str -> LinNumeral -> LinNumeral = \unit,n -> {
s = table {NCard => n.s ! NCard ++ unit ; NOrd => n.s ! NCard ++ unit} ; n = Pl
} ;
plus : LinNumeral -> LinNumeral -> LinNumeral = \x,y -> {
s = table {NCard => x.s ! NCard ++ "'s" ++ y.s ! NCard ;
NOrd => x.s ! NCard ++ "'s" ++ y.s ! NOrd} ;
n = Pl
} ;
}