Something went wrong. Try again.
The Monad language. Dependent types, functional programming compiled with LLVM. Hobby project. monad-lang.org
dependent-types language compiler programming-language functional-programming
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646/// Number types and operations// I8#[native i8_add]def I8.add (a b : I8) : I8#[native i8_sub]pub def I8.sub (a b : I8) : I8#[native i8_mul]def I8.mul (a b : I8) : I8#[native i8_div]def I8.div (a b : I8) : I8#[native i8_eq]pub def I8.beq (a b : I8) : Bool#[native i8_lt]def I8.lt (a b : I8) : Bool#[native i8_gt]pub def I8.gt (a b : I8) : Bool#[native i8_to_string]pub def I8.to_string (a : I8) : Stringinstance Add I8 { def add (a b : I8) : I8 := I8.add a b}pub instance Sub I8 { def sub (a b : I8) : I8 := I8.sub a b}instance HMul I8 I8 I8 { def mul (a b : I8) : I8 := I8.mul a b}instance Div I8 { def div (a b : I8) : I8 := I8.div a b}pub instance BEq I8 { def beq (a b : I8) : Bool := I8.beq a b}pub instance BOrd I8 { def lt (a b : I8) : Bool := I8.lt a b def gt (a b : I8) : Bool := I8.gt a b}pub instance ToString I8 { def to_string (a : I8) : String := I8.to_string a}// I16#[native i16_add]def I16.add (a b : I16) : I16#[native i16_sub]pub def I16.sub (a b : I16) : I16#[native i16_mul]def I16.mul (a b : I16) : I16#[native i16_div]def I16.div (a b : I16) : I16#[native i16_eq]pub def I16.beq (a b : I16) : Bool#[native i16_lt]def I16.lt (a b : I16) : Bool#[native i16_gt]pub def I16.gt (a b : I16) : Bool#[native i16_to_string]pub def I16.to_string (a : I16) : Stringinstance Add I16 { def add (a b : I16) : I16 := I16.add a b}pub instance Sub I16 { def sub (a b : I16) : I16 := I16.sub a b}instance HMul I16 I16 I16 { def mul (a b : I16) : I16 := I16.mul a b}instance Div I16 { def div (a b : I16) : I16 := I16.div a b}pub instance BEq I16 { def beq (a b : I16) : Bool := I16.beq a b}pub instance BOrd I16 { def lt (a b : I16) : Bool := I16.lt a b def gt (a b : I16) : Bool := I16.gt a b}pub instance ToString I16 { def to_string (a : I16) : String := I16.to_string a}// I32#[native i32_add]def I32.add (a b : I32) : I32#[native i32_sub]pub def I32.sub (a b : I32) : I32#[native i32_mul]def I32.mul (a b : I32) : I32#[native i32_div]def I32.div (a b : I32) : I32#[native i32_eq]pub def I32.beq (a b : I32) : Bool#[native i32_lt]def I32.lt (a b : I32) : Bool#[native i32_gt]pub def I32.gt (a b : I32) : Bool#[native i32_to_string]pub def I32.to_string (a : I32) : String#[native i32_to_i64]pub def I32.to_i64 (a : I32) : I64instance Add I32 { def add (a b : I32) : I32 := I32.add a b}pub instance Sub I32 { def sub (a b : I32) : I32 := I32.sub a b}instance HMul I32 I32 I32 { def mul (a b : I32) : I32 := I32.mul a b}instance Div I32 { def div (a b : I32) : I32 := I32.div a b}pub instance BEq I32 { def beq (a b : I32) : Bool := I32.beq a b}pub instance BOrd I32 { def lt (a b : I32) : Bool := I32.lt a b def gt (a b : I32) : Bool := I32.gt a b}pub instance ToString I32 { def to_string (a : I32) : String := I32.to_string a}// I64#[native i64_add]def I64.add (a b : I64) : I64#[native i64_sub]pub def I64.sub (a b : I64) : I64#[native i64_mul]def I64.mul (a b : I64) : I64#[native i64_div]def I64.div (a b : I64) : I64#[native i64_lt]def I64.lt (a b : I64) : Bool#[native i64_gt]pub def I64.gt (a b : I64) : Bool#[native i64_to_u64]def I64.to_u64 (a : I64) : U64/// For FFI calls that take a C `int` (`SSL_set_fd` in motes/tls takes/// the socket's descriptor). Identity at the payload level; no/// truncation is applied, matching the reference's `int_to_int`.#[native i64_to_i32]pub def I64.to_i32 (a : I64) : I32#[native i64_to_u32]def I64.to_u32 (a : I64) : U32#[native i64_eq]pub def I64.beq (a b : I64) : Bool#[native i64_to_string]pub def I64.to_string (a : I64) : String/// Arithmetic negation. Canonical home for what `lang/json.mo` and/// `lang/toml.mo` each had as their own `neg_i64`/`Toml.neg_i64`/// (duplicated only because top-level names are not file-scoped).def I64.neg (n : I64) : I64 := 0 - ninstance Add I64 { def add (a b : I64) : I64 := I64.add a b}pub instance Sub I64 { // `I64.sub`, NOT `a - b`: `infix (-) := Sub.sub` (init/prelude.mo), so // spelling this with the operator makes it call itself. def sub (a b : I64) : I64 := I64.sub a b}instance HMul I64 I64 I64 { def mul (a b : I64) : I64 := I64.mul a b}instance Div I64 { def div (a b : I64) : I64 := I64.div a b}pub instance BEq I64 { def beq (a b : I64) : Bool := I64.beq a b}pub instance BOrd I64 { def lt (a b : I64) : Bool := I64.lt a b def gt (a b : I64) : Bool := I64.gt a b}pub instance ToString I64 { def to_string (a : I64) : String := I64.to_string a}instance Hashable I64 { def hash (a : I64) : U64 := I64.to_u64 a}// U8#[native u8_add]def U8.add (a b : U8) : U8#[native u8_sub]pub def U8.sub (a b : U8) : U8#[native u8_mul]def U8.mul (a b : U8) : U8#[native u8_div]def U8.div (a b : U8) : U8#[native u8_eq]pub def U8.beq (a b : U8) : Bool#[native u8_to_u64]def U8.to_u64 (a : U8) : U64#[native u8_to_u32]def U8.to_u32 (a : U8) : U32#[native u8_lt]def U8.lt (a b : U8) : Bool#[native u8_gt]pub def U8.gt (a b : U8) : Bool#[native u8_to_string]pub def U8.to_string (a : U8) : Stringinstance Add U8 { def add (a b : U8) : U8 := U8.add a b}pub instance Sub U8 { def sub (a b : U8) : U8 := U8.sub a b}instance HMul U8 U8 U8 { def mul (a b : U8) : U8 := U8.mul a b}instance Div U8 { def div (a b : U8) : U8 := U8.div a b}pub instance BEq U8 { def beq (a b : U8) : Bool := U8.beq a b}pub instance BOrd U8 { def lt (a b : U8) : Bool := U8.lt a b def gt (a b : U8) : Bool := U8.gt a b}pub instance ToString U8 { def to_string (a : U8) : String := U8.to_string a}// U16#[native u16_add]def U16.add (a b : U16) : U16#[native u16_sub]pub def U16.sub (a b : U16) : U16#[native u16_mul]def U16.mul (a b : U16) : U16#[native u16_div]def U16.div (a b : U16) : U16#[native u16_eq]pub def U16.beq (a b : U16) : Bool#[native u16_lt]def U16.lt (a b : U16) : Bool#[native u16_gt]pub def U16.gt (a b : U16) : Bool#[native u16_to_string]pub def U16.to_string (a : U16) : Stringinstance Add U16 { def add (a b : U16) : U16 := U16.add a b}pub instance Sub U16 { def sub (a b : U16) : U16 := U16.sub a b}instance HMul U16 U16 U16 { def mul (a b : U16) : U16 := U16.mul a b}instance Div U16 { def div (a b : U16) : U16 := U16.div a b}pub instance BEq U16 { def beq (a b : U16) : Bool := U16.beq a b}pub instance BOrd U16 { def lt (a b : U16) : Bool := U16.lt a b def gt (a b : U16) : Bool := U16.gt a b}pub instance ToString U16 { def to_string (a : U16) : String := U16.to_string a}// U32#[native u32_add]def U32.add (a b : U32) : U32#[native u32_sub]pub def U32.sub (a b : U32) : U32#[native u32_mul]def U32.mul (a b : U32) : U32#[native u32_div]def U32.div (a b : U32) : U32#[native u32_eq]pub def U32.beq (a b : U32) : Bool#[native u32_lt]def U32.lt (a b : U32) : Bool#[native u32_gt]pub def U32.gt (a b : U32) : Bool#[native u32_to_string]pub def U32.to_string (a : U32) : Stringinstance Add U32 { def add (a b : U32) : U32 := U32.add a b}pub instance Sub U32 { def sub (a b : U32) : U32 := U32.sub a b}instance HMul U32 U32 U32 { def mul (a b : U32) : U32 := U32.mul a b}instance Div U32 { def div (a b : U32) : U32 := U32.div a b}pub instance BEq U32 { def beq (a b : U32) : Bool := U32.beq a b}pub instance BOrd U32 { def lt (a b : U32) : Bool := U32.lt a b def gt (a b : U32) : Bool := U32.gt a b}pub instance ToString U32 { def to_string (a : U32) : String := U32.to_string a}#[native u32_and]def U32.and (a b : U32) : U32#[native u32_or]def U32.or (a b : U32) : U32#[native u32_xor]def U32.xor (a b : U32) : U32#[native u32_shl]def U32.shl (a b : U32) : U32#[native u32_shr]def U32.shr (a b : U32) : U32#[native u32_to_u8]def U32.to_u8 (a : U32) : U8def U32.not (a : U32) : U32 := U32.xor a 0xFFFFFFFFu32def U32.rotr (a n : U32) : U32 := U32.or (U32.shr a n) (U32.shl a (U32.sub 32u32 n))// U64#[native u64_add]def U64.add (a b : U64) : U64#[native u64_sub]pub def U64.sub (a b : U64) : U64#[native u64_mul]def U64.mul (a b : U64) : U64#[native u64_div]def U64.div (a b : U64) : U64#[native u64_mod]def U64.mod (a b : U64) : U64#[native u64_xor]def U64.xor (a b : U64) : U64#[native u64_eq]pub def U64.beq (a b : U64) : Bool#[native u64_lt]def U64.lt (a b : U64) : Bool#[native u64_gt]pub def U64.gt (a b : U64) : Bool#[native u64_to_string]pub def U64.to_string (a : U64) : Stringinstance Add U64 { def add (a b : U64) : U64 := U64.add a b}pub instance Sub U64 { def sub (a b : U64) : U64 := U64.sub a b}instance HMul U64 U64 U64 { def mul (a b : U64) : U64 := U64.mul a b}instance Div U64 { def div (a b : U64) : U64 := U64.div a b}instance Hashable U64 { def hash (a : U64) : U64 := a}pub instance BEq U64 { def beq (a b : U64) : Bool := U64.beq a b}pub instance BOrd U64 { def lt (a b : U64) : Bool := U64.lt a b def gt (a b : U64) : Bool := U64.gt a b}pub instance ToString U64 { def to_string (a : U64) : String := U64.to_string a}// F32#[native f32_add]def F32.add (a b : F32) : F32#[native f32_sub]pub def F32.sub (a b : F32) : F32#[native f32_mul]def F32.mul (a b : F32) : F32#[native f32_div]def F32.div (a b : F32) : F32#[native f32_eq]pub def F32.beq (a b : F32) : Bool#[native f32_lt]def F32.lt (a b : F32) : Bool#[native f32_gt]pub def F32.gt (a b : F32) : Bool#[native f32_to_string]pub def F32.to_string (a : F32) : Stringinstance Add F32 { def add (a b : F32) : F32 := F32.add a b}pub instance Sub F32 { def sub (a b : F32) : F32 := F32.sub a b}instance HMul F32 F32 F32 { def mul (a b : F32) : F32 := F32.mul a b}instance Div F32 { def div (a b : F32) : F32 := F32.div a b}pub instance BEq F32 { def beq (a b : F32) : Bool := F32.beq a b}pub instance BOrd F32 { def lt (a b : F32) : Bool := F32.lt a b def gt (a b : F32) : Bool := F32.gt a b}pub instance ToString F32 { def to_string (a : F32) : String := F32.to_string a}// F64#[native f64_add]def F64.add (a b : F64) : F64#[native f64_sub]pub def F64.sub (a b : F64) : F64#[native f64_mul]def F64.mul (a b : F64) : F64#[native f64_div]def F64.div (a b : F64) : F64#[native f64_eq]pub def F64.beq (a b : F64) : Bool#[native f64_lt]def F64.lt (a b : F64) : Bool#[native f64_gt]pub def F64.gt (a b : F64) : Bool#[native f64_to_string]pub def F64.to_string (a : F64) : String/// Text -> the double's own bit pattern: the decimal parser this backend/// needs to lower a FLOAT LITERAL, since `Literal.flt` carries a/// literal's source text rather than a value (`lang/types.mo`: there is/// no native bridge from a decimal string to a float bit pattern on the/// self-hosted side, which is why the literal keeps its text at all)./// `lang/codegen/emit.mo`'s `compile_lit_ir` calls this to turn `5.0`/// into the constant it emits, so the route is the ordinary one:/// a `#[native]` def, wired like the rest of this family.////// `I64`, not `F64`, because the result IS the bit pattern and an `F64`/// is nothing else here -- a codegen caller wants it as the integer it/// has to emit, with no further conversion in between. The C side is/// `strtod` (`runtime/src/runtime.c`) and the Rust host's equivalent is/// `f64::from_str` (`core/src/core_native.rs`), which agree on every/// spelling the number parser can produce; text that parses to nothing/// gives 0.0 rather than failing, so a malformed literal is a wrong/// constant instead of a compiler crash.#[native f64_of_string]pub def F64.bits_of_string (text : String) : I64instance Add F64 { def add (a b : F64) : F64 := F64.add a b}pub instance Sub F64 { def sub (a b : F64) : F64 := F64.sub a b}instance HMul F64 F64 F64 { def mul (a b : F64) : F64 := F64.mul a b}instance Div F64 { def div (a b : F64) : F64 := F64.div a b}pub instance BEq F64 { def beq (a b : F64) : Bool := F64.beq a b}pub instance BOrd F64 { def lt (a b : F64) : Bool := F64.lt a b def gt (a b : F64) : Bool := F64.gt a b}pub instance ToString F64 { def to_string (a : F64) : String := F64.to_string a}def nat_to_i64 (n : Nat) : I64 := match n { zero => 0, succ m => I64.add 1 (nat_to_i64 m) }pub def Nat.to_string (n : Nat) : String := I64.to_string (nat_to_i64 n)