diff --git a/Cargo.lock b/Cargo.lock index 0d757cb8..e35de384 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -30,9 +30,9 @@ checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa" [[package]] name = "base64" -version = "0.13.0" +version = "0.13.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "904dfeac50f3cdaba28fc6f57fdcddb75f49ed61346676a78c4ffe55877802fd" +checksum = "9e1b586273c5702936fe7b7d6896644d8be71e6314cfe09d3167c95f712589e8" [[package]] name = "bitflags" @@ -69,9 +69,9 @@ checksum = "ec8a7b6a70fde80372154c65702f00a0f56f3e1c36abbc6c440484be248856db" [[package]] name = "cc" -version = "1.0.73" +version = "1.0.76" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2fff2a6927b3bb87f9595d67196a70493f627687a71d87a0d692242c33f58c11" +checksum = "76a284da2e6fe2092f2353e51713435363112dfd60030e22add80be333fb928f" [[package]] name = "cfg-if" @@ -81,9 +81,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clap" -version = "3.2.22" +version = "3.2.23" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "86447ad904c7fb335a790c9d7fe3d0d971dc523b8ccd1561a520de9a85302750" +checksum = "71655c45cb9845d3270c9d6df84ebe72b4dad3c2ba3f7023ad47c144e4e473a5" dependencies = [ "atty", "bitflags", @@ -98,13 +98,13 @@ dependencies = [ [[package]] name = "clap" -version = "4.0.15" +version = "4.0.22" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6bf8832993da70a4c6d13c581f4463c2bdda27b9bf1c5498dc4365543abe6d6f" +checksum = "91b9970d7505127a162fdaa9b96428d28a479ba78c9ec7550a63a5d9863db682" dependencies = [ "atty", "bitflags", - "clap_derive 4.0.13", + "clap_derive 4.0.21", "clap_lex 0.3.0", "once_cell", "strsim", @@ -126,9 +126,9 @@ dependencies = [ [[package]] name = "clap_derive" -version = "4.0.13" +version = "4.0.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c42f169caba89a7d512b5418b09864543eeb4d497416c917d7137863bd2076ad" +checksum = "0177313f9f02afc995627906bbd8967e2be069f5261954222dac78290c2b9014" dependencies = [ "heck", "proc-macro-error", @@ -347,9 +347,9 @@ dependencies = [ [[package]] name = "h2" -version = "0.3.14" +version = "0.3.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5ca32592cf21ac7ccab1825cd87f6c9b3d9022c44d086172ed0966bec8af30be" +checksum = "5f9f29bc9dda355256b2916cf526ab02ce0aeaaaf2bad60d65ef3f12f11dd0f4" dependencies = [ "bytes", "fnv", @@ -431,7 +431,7 @@ version = "0.1.89" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e0581f8e42136b54e77d3180b6c871486ad2a2dca5e394daaa38fa3190dd00c9" dependencies = [ - "clap 3.2.22", + "clap 3.2.23", "highlight_error", "instant", "itertools", @@ -444,9 +444,9 @@ dependencies = [ [[package]] name = "hyper" -version = "0.14.20" +version = "0.14.23" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "02c929dc5c39e335a03c405292728118860721b10190d98c2a0f0efd5baafbac" +checksum = "034711faac9d2166cb1baf1a2fb0b60b1f277f8492fd72176c17f3515e1abd3c" dependencies = [ "bytes", "futures-channel", @@ -553,9 +553,9 @@ dependencies = [ [[package]] name = "ipnet" -version = "2.5.0" +version = "2.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "879d54834c8c76457ef4293a689b2a8c59b076067ad77b15efafbb05f92a592b" +checksum = "f88c5561171189e69df9d98bcf18fd5f9558300f7ea7b801eb8a0fd748bd8745" [[package]] name = "itertools" @@ -597,7 +597,7 @@ dependencies = [ name = "kind-cli" version = "0.3.0" dependencies = [ - "clap 4.0.15", + "clap 4.0.22", "kind-checker", "kind-driver", "kind-report", @@ -720,9 +720,9 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" [[package]] name = "libc" -version = "0.2.135" +version = "0.2.137" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "68783febc7782c6c5cb401fbda4de5a9898be1762314da0bb2c10ced61f18b0c" +checksum = "fc7fcc620a3bff7cdd7a365be3376c97191aeaccc2a603e600951e452615bf89" [[package]] name = "linked-hash-map" @@ -763,21 +763,21 @@ checksum = "2a60c7ce501c71e03a9c9c0d35b861413ae925bd979cc7a4e30d060069aaac8d" [[package]] name = "mio" -version = "0.8.4" +version = "0.8.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "57ee1c23c7c63b0c9250c339ffdc69255f110b298b901b9f6c82547b7b87caaf" +checksum = "e5d732bc30207a6423068df043e3d02e0735b155ad7ce1a6f76fe2baa5b158de" dependencies = [ "libc", "log", "wasi", - "windows-sys 0.36.1", + "windows-sys 0.42.0", ] [[package]] name = "native-tls" -version = "0.2.10" +version = "0.2.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fd7e2f3618557f980e0b17e8856252eee3c97fa12c54dff0ca290fb6266ca4a9" +checksum = "07226173c32f2926027b63cce4bcd8076c3552846cbe7925f3aaffeac0a3b92e" dependencies = [ "lazy_static", "libc", @@ -821,9 +821,9 @@ dependencies = [ [[package]] name = "num_cpus" -version = "1.13.1" +version = "1.14.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "19e64526ebdee182341572e50e9ad03965aa510cd94427a4549448f285e957a1" +checksum = "f6058e64324c71e02bc2b150e4f3bc8286db6c83092132ffa3f6b1eab0f9def5" dependencies = [ "hermit-abi", "libc", @@ -831,9 +831,9 @@ dependencies = [ [[package]] name = "once_cell" -version = "1.15.0" +version = "1.16.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e82dad04139b71a90c080c8463fe0dc7902db5192d939bd0950f074d014339e1" +checksum = "86f0b0d4bf799edbc74508c1e8bf170ff5f41238e5f8225603ca7caaae2b7860" [[package]] name = "openssl" @@ -869,9 +869,9 @@ checksum = "ff011a302c396a5197692431fc1948019154afc178baf7d8e37367442a4601cf" [[package]] name = "openssl-sys" -version = "0.9.76" +version = "0.9.77" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5230151e44c0f05157effb743e8d517472843121cf9243e8b81393edb5acd9ce" +checksum = "b03b84c3b2d099b81f0953422b4d4ad58761589d0229b5506356afca05a3670a" dependencies = [ "autocfg", "cc", @@ -882,9 +882,9 @@ dependencies = [ [[package]] name = "os_str_bytes" -version = "6.3.0" +version = "6.3.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9ff7415e9ae3fff1225851df9e0d9e4e5479f947619774677a63572e55e80eff" +checksum = "3baf96e39c5359d2eb0dd6ccb42c62b91d9678aa68160d261b9e0ccbf9e9dea9" [[package]] name = "parking_lot_core" @@ -919,9 +919,9 @@ checksum = "8b870d8c151b6f2fb93e84a13146138f05d02ed11c7e7c54f8826aaaf7c9f184" [[package]] name = "pkg-config" -version = "0.3.25" +version = "0.3.26" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1df8c4ec4b0627e53bdf214615ad287367e482558cf84b109250b37464dc03ae" +checksum = "6ac9a59f73473f1b8d852421e59e64809f025994837ef743615c6d0c5b305160" [[package]] name = "proc-macro-error" @@ -949,9 +949,9 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.46" +version = "1.0.47" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "94e2ef8dbfc347b10c094890f778ee2e36ca9bb4262e86dc99cd217e35f3470b" +checksum = "5ea3d908b0e36316caf9e9e2c4625cdde190a7e6f440d794667ed17a1855e725" dependencies = [ "unicode-ident", ] @@ -991,9 +991,9 @@ dependencies = [ [[package]] name = "regex" -version = "1.6.0" +version = "1.7.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4c4eb3267174b8c6c2f654116623910a0fef09c4753f8dd83db29c48a0df988b" +checksum = "e076559ef8e241f2ae3479e36f97bd5741c0330689e217ad51ce2c76808b868a" dependencies = [ "aho-corasick", "memchr", @@ -1002,9 +1002,9 @@ dependencies = [ [[package]] name = "regex-syntax" -version = "0.6.27" +version = "0.6.28" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a3f87b73ce11b1619a3c6332f45341e0047173771e8b8b73f87bfeefb7b56244" +checksum = "456c603be3e8d448b072f410900c09faf164fbce2d480456f50eea6e25f9c848" [[package]] name = "remove_dir_all" @@ -1108,9 +1108,9 @@ dependencies = [ [[package]] name = "serde" -version = "1.0.145" +version = "1.0.147" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "728eb6351430bccb993660dfffc5a72f91ccc1295abaa8ce19b27ebe4f75568b" +checksum = "d193d69bae983fc11a79df82342761dfbf28a99fc8d203dca4c3c1b590948965" [[package]] name = "serde_json" @@ -1178,9 +1178,9 @@ checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623" [[package]] name = "syn" -version = "1.0.102" +version = "1.0.103" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3fcd952facd492f9be3ef0d0b7032a6e442ee9b361d4acc2b1d0c4aaa5f613a1" +checksum = "a864042229133ada95abf3b54fdc62ef5ccabe9515b64717bcb9a1919e59445d" dependencies = [ "proc-macro2", "quote", @@ -1212,9 +1212,9 @@ dependencies = [ [[package]] name = "textwrap" -version = "0.15.1" +version = "0.16.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "949517c0cf1bf4ee812e2e07e08ab448e3ae0d23472aee8a06c985f0c8815b16" +checksum = "222a222a5bfe1bba4a77b45ec488a741b3cb8872e5e499451fd7d0129c9c7c3d" [[package]] name = "tinyvec" diff --git a/src/kind-checker/src/compiler/mod.rs b/src/kind-checker/src/compiler/mod.rs index e13452aa..483f3585 100644 --- a/src/kind-checker/src/compiler/mod.rs +++ b/src/kind-checker/src/compiler/mod.rs @@ -132,7 +132,8 @@ fn codegen_all_expr( match &expr.data { Typ => mk_quoted_ctr(eval_ctr(quote, TermTag::Typ), vec![span_to_num(expr.span)]), - U60 => mk_quoted_ctr(eval_ctr(quote, TermTag::U60), vec![span_to_num(expr.span)]), + NumType(desugared::NumType::U60) => mk_quoted_ctr(eval_ctr(quote, TermTag::U60), vec![span_to_num(expr.span)]), + NumType(desugared::NumType::U120) => todo!(), Var(ident) => { if quote && !lhs { set_origin(ident) @@ -240,10 +241,11 @@ fn codegen_all_expr( codegen_all_expr(lhs_rule, lhs, num, quote, expr), ], ), - Num(n) => mk_quoted_ctr( + Num(desugared::Num::U60(n)) => mk_quoted_ctr( eval_ctr(quote, TermTag::Num), vec![span_to_num(expr.span), mk_u60(*n)], ), + Num(desugared::Num::U120(n)) => todo!(), Binary(operator, left, right) => mk_quoted_ctr( eval_ctr(quote, TermTag::Binary), vec![ diff --git a/src/kind-checker/src/report.rs b/src/kind-checker/src/report.rs index 50ec5041..13c8b17e 100644 --- a/src/kind-checker/src/report.rs +++ b/src/kind-checker/src/report.rs @@ -149,7 +149,7 @@ fn parse_all_expr( )), "Kind.Quoted.hlp" => Ok(Expr::hlp(parse_orig(&args[0])?, Ident::generate("?"))), "Kind.Quoted.u60" => Ok(Expr::u60(parse_orig(&args[0])?)), - "Kind.Quoted.num" => Ok(Expr::num(parse_orig(&args[0])?, parse_num(&args[1])?)), + "Kind.Quoted.num" => Ok(Expr::num60(parse_orig(&args[0])?, parse_num(&args[1])?)), // TODO: do something about u120? "Kind.Quoted.op2" => Ok(Expr::binary( parse_orig(&args[0])?, parse_op(&args[1])?, diff --git a/src/kind-pass/src/desugar/expr.rs b/src/kind-pass/src/desugar/expr.rs index 3a1c6017..1b48ac1a 100644 --- a/src/kind-pass/src/desugar/expr.rs +++ b/src/kind-pass/src/desugar/expr.rs @@ -17,7 +17,8 @@ impl<'a> DesugarState<'a> { Literal::Type => desugared::Expr::typ(range), Literal::Help(name) => desugared::Expr::hlp(range, name.clone()), Literal::U60 => desugared::Expr::u60(range), - Literal::Number(num) => desugared::Expr::num(range, *num), + // TODO: Add u120 literals + Literal::Number(num) => desugared::Expr::num60(range, *num), Literal::String(string) => desugared::Expr::str(range, string.to_owned()), Literal::Char(_) => todo!(), } diff --git a/src/kind-pass/src/desugar/top_level.rs b/src/kind-pass/src/desugar/top_level.rs index e7f58750..375c9e73 100644 --- a/src/kind-pass/src/desugar/top_level.rs +++ b/src/kind-pass/src/desugar/top_level.rs @@ -304,7 +304,8 @@ impl<'a> DesugarState<'a> { desugared::Expr::var(name) } concrete::pat::PatKind::Var(ident) => desugared::Expr::var(ident.0.clone()), - concrete::pat::PatKind::Num(n) => desugared::Expr::num(pat.range, *n), + // TODO: Add u120 pattern literals + concrete::pat::PatKind::Num(n) => desugared::Expr::num60(pat.range, *n), concrete::pat::PatKind::Pair(fst, snd) => self.desugar_pair_pat(pat.range, fst, snd), concrete::pat::PatKind::List(ls) => self.desugar_list_pat(pat.range, ls), concrete::pat::PatKind::Str(string) => { diff --git a/src/kind-pass/src/erasure/mod.rs b/src/kind-pass/src/erasure/mod.rs index 16ea374d..7ec437a5 100644 --- a/src/kind-pass/src/erasure/mod.rs +++ b/src/kind-pass/src/erasure/mod.rs @@ -255,7 +255,7 @@ impl<'a> ErasureState<'a> { use kind_tree::desugared::ExprKind::*; match &expr.data { - Typ | U60 | Num(_) | Str(_) | Err => Box::new(expr.clone()), + Typ | NumType(_) | Num(_) | Str(_) | Err => Box::new(expr.clone()), Hole(_) | Hlp(_) => match &expr.span { kind_span::Span::Generated => Box::new(expr.clone()), kind_span::Span::Locatable(span) => { diff --git a/src/kind-target-hvm/src/lib.rs b/src/kind-target-hvm/src/lib.rs index 6c0e0fa8..577413eb 100644 --- a/src/kind-target-hvm/src/lib.rs +++ b/src/kind-target-hvm/src/lib.rs @@ -30,14 +30,16 @@ pub fn compile_term(expr: &desugared::Expr) -> Box { }), Ann(left, _) => compile_term(left), Sub(_, _, _, expr) => compile_term(expr), - Num(numb) => Box::new(Term::Num { numb: *numb }), + Num(desugared::Num::U60(numb)) => Box::new(Term::Num { numb: *numb }), + Num(_) => todo!(), Binary(op, l, r) => Box::new(Term::Ctr { name: op.to_string(), args: vec![compile_term(l), compile_term(r)], }), Hole(_) => unreachable!("Internal Error: 'Hole' cannot be a relevant term"), Typ => unreachable!("Internal Error: 'Typ' cannot be a relevant term"), - U60 => unreachable!("Internal Error: 'U60' cannot be a relevant term"), + NumType(desugared::NumType::U60) => unreachable!("Internal Error: 'U60' cannot be a relevant term"), + NumType(desugared::NumType::U120) => unreachable!("Internal Error: 'U120' cannot be a relevant term"), All(_, _, _) => unreachable!("Internal Error: 'All' cannot be a relevant term"), Str(_) => unreachable!("Internal Error: 'Str' cannot be a relevant term"), Hlp(_) => unreachable!("Internal Error: 'Hlp' cannot be a relevant term"), diff --git a/src/kind-tree/src/desugared/mod.rs b/src/kind-tree/src/desugared/mod.rs index 82d2d0c3..bb649cbe 100644 --- a/src/kind-tree/src/desugared/mod.rs +++ b/src/kind-tree/src/desugared/mod.rs @@ -39,10 +39,10 @@ pub enum ExprKind { Sub(Ident, usize, usize, Box), /// Type Literal Typ, - /// U60 Type - U60, - /// Number literal - Num(u64), + /// Primitive numeric types + NumType(NumType), + /// Primitive numeric values + Num(Num), /// Very special constructor :) Str(String), /// Binary operation (e.g. 2 + 3) @@ -158,14 +158,28 @@ impl Expr { pub fn u60(range: Range) -> Box { Box::new(Expr { span: Span::Locatable(range), - data: ExprKind::U60, + data: ExprKind::NumType(NumType::U60), }) } - pub fn num(range: Range, num: u64) -> Box { + pub fn u120(range: Range) -> Box { Box::new(Expr { span: Span::Locatable(range), - data: ExprKind::Num(num), + data: ExprKind::NumType(NumType::U120), + }) + } + + pub fn num60(range: Range, num: u64) -> Box { + Box::new(Expr { + span: Span::Locatable(range), + data: ExprKind::Num(Num::U60(num)), + }) + } + + pub fn num120(range: Range, num: u128) -> Box { + Box::new(Expr { + span: Span::Locatable(range), + data: ExprKind::Num(Num::U120(num)), }) } @@ -205,6 +219,18 @@ impl Expr { } } +#[derive(Clone, Debug, Hash, PartialEq, Eq)] +pub enum Num { + U60(u64), + U120(u128), +} + +#[derive(Clone, Debug, Hash, PartialEq, Eq)] +pub enum NumType { + U60, + U120 +} + /// An argument is a 'binding' of a name to a type /// it has some other options like /// eras: that express the erasure of this type when @@ -285,9 +311,11 @@ impl Display for Expr { use ExprKind::*; match &self.data { Typ => write!(f, "Type"), - U60 => write!(f, "U60"), + NumType(self::NumType::U60) => write!(f, "U60"), + NumType(self::NumType::U120) => write!(f, "U120"), Str(n) => write!(f, "\"{}\"", n), - Num(n) => write!(f, "{}", n), + Num(self::Num::U60(n)) => write!(f, "{}", n), + Num(self::Num::U120(n)) => write!(f, "{}u120", n), All(_, _, _) => write!(f, "({})", self.traverse_pi_types()), Var(name) => write!(f, "{}", name), Lambda(binder, body) => write!(f, "({} => {})", binder, body),