mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-09 04:59:31 -06:00
95 lines
2.3 KiB
Plaintext
95 lines
2.3 KiB
Plaintext
import prelude
|
|
|
|
data Cat : Type where {
|
|
Digit : Cat ;
|
|
Numeral : Cat ;
|
|
Sub10 : Cat ;
|
|
Sub100 : Cat ;
|
|
Sub1000 : Cat ;
|
|
Sub1000000 : Cat
|
|
} ;
|
|
|
|
data Tree : (_ : Cat)-> Type where {
|
|
n2 : Tree Digit ;
|
|
n3 : Tree Digit ;
|
|
n4 : Tree Digit ;
|
|
n5 : Tree Digit ;
|
|
n6 : Tree Digit ;
|
|
n7 : Tree Digit ;
|
|
n8 : Tree Digit ;
|
|
n9 : Tree Digit ;
|
|
num : (_ : Tree Sub1000000)-> Tree Numeral ;
|
|
pot0 : (_ : Tree Digit)-> Tree Sub10 ;
|
|
pot01 : Tree Sub10 ;
|
|
pot0as1 : (_ : Tree Sub10)-> Tree Sub100 ;
|
|
pot1 : (_ : Tree Digit)-> Tree Sub100 ;
|
|
pot110 : Tree Sub100 ;
|
|
pot111 : Tree Sub100 ;
|
|
pot1as2 : (_ : Tree Sub100)-> Tree Sub1000 ;
|
|
pot1plus : (_ : Tree Digit)-> (_ : Tree Sub10)-> Tree Sub100 ;
|
|
pot1to19 : (_ : Tree Digit)-> Tree Sub100 ;
|
|
pot2 : (_ : Tree Sub10)-> Tree Sub1000 ;
|
|
pot2as3 : (_ : Tree Sub1000)-> Tree Sub1000000 ;
|
|
pot2plus : (_ : Tree Sub10)-> (_ : Tree Sub100)-> Tree Sub1000 ;
|
|
pot3 : (_ : Tree Sub1000)-> Tree Sub1000000 ;
|
|
pot3plus : (_ : Tree Sub1000)-> (_ : Tree Sub1000)-> Tree Sub1000000
|
|
}
|
|
|
|
derive Compos Tree
|
|
|
|
|
|
data Binary_Cat : Type where {
|
|
Bin : Binary_Cat
|
|
} ;
|
|
data Binary_Tree : (_ : Binary_Cat)-> Type where {
|
|
End : Binary_Tree Bin ;
|
|
One : (_ : Binary_Tree Bin)-> Binary_Tree Bin ;
|
|
Zero : (_ : Binary_Tree Bin)-> Binary_Tree Bin
|
|
}
|
|
|
|
|
|
|
|
monoid_plus_Int : Monoid Integer
|
|
monoid_plus_Int = rec mzero = 0
|
|
mplus = (\x -> \y -> x + y)
|
|
|
|
|
|
num2int : Tree Numeral -> Integer
|
|
num2int = tree2int ?
|
|
|
|
tree2int : (C : Cat) -> Tree C -> Integer
|
|
tree2int _ n = case n of
|
|
n2 -> 2
|
|
n3 -> 3
|
|
n4 -> 4
|
|
n5 -> 5
|
|
n6 -> 6
|
|
n7 -> 7
|
|
n8 -> 8
|
|
n9 -> 9
|
|
pot01 -> 1
|
|
pot1 x -> 10 * tree2int ? x
|
|
pot110 -> 10
|
|
pot111 -> 11
|
|
pot1plus x y -> 10 * tree2int ? x + tree2int ? y
|
|
pot1to19 x -> 10 + tree2int ? x
|
|
pot2 x -> 100 * tree2int ? x
|
|
pot2as3 x -> 10 * tree2int ? x
|
|
pot2plus x y -> 100 * tree2int ? x + tree2int ? y
|
|
pot3 x -> 1000 * tree2int ? x
|
|
pot3plus x y -> 1000 * tree2int ? x + tree2int ? y
|
|
_ -> composFold ? ? compos_Tree ? monoid_plus_Int C tree2int n
|
|
|
|
int2bin : Integer -> Binary_Tree Bin
|
|
int2bin = int2bin_ End
|
|
|
|
int2bin_ : Binary_Tree Bin -> Integer -> Binary_Tree Bin
|
|
int2bin_ b 0 = b
|
|
int2bin_ b n = let d = if n % 2 == 0 then Zero else One
|
|
q = n / 2
|
|
in int2bin_ (d b) q
|
|
|
|
num2bin : Tree Numeral -> Binary_Tree Bin
|
|
num2bin n = int2bin (num2int n)
|
|
|