From b06ae1e3c5360d6f4aad6baf140800ec3057cdb9 Mon Sep 17 00:00:00 2001 From: Karl Meakin Date: Sun, 12 Feb 2023 02:39:27 +0000 Subject: [PATCH] Allow synth_binop to infer the expected rhs type from the operator and lhs type --- fathom/src/surface/elaboration.rs | 279 ++++++++++++++++-------------- tests/succeed/binops/synth.fathom | 144 +++++++++++---- tests/succeed/binops/synth.snap | 105 +++++++++-- 3 files changed, 345 insertions(+), 183 deletions(-) diff --git a/fathom/src/surface/elaboration.rs b/fathom/src/surface/elaboration.rs index cf4a19466..1fdbf0850 100644 --- a/fathom/src/surface/elaboration.rs +++ b/fathom/src/surface/elaboration.rs @@ -1856,134 +1856,162 @@ impl<'arena> Context<'arena> { // de-sugar into function application let (lhs_expr, lhs_type) = self.synth_and_insert_implicit_apps(lhs); - let (rhs_expr, rhs_type) = self.synth_and_insert_implicit_apps(rhs); let lhs_type = self.elim_env().force(&lhs_type); - let rhs_type = self.elim_env().force(&rhs_type); - let operand_types = Option::zip(lhs_type.match_prim_spine(), rhs_type.match_prim_spine()); - - let (fun, body_type) = match (op, operand_types) { - (Mul(_), Some(((U8Type, []), (U8Type, [])))) => (U8Mul, U8Type), - (Mul(_), Some(((U16Type, []), (U16Type, [])))) => (U16Mul, U16Type), - (Mul(_), Some(((U32Type, []), (U32Type, [])))) => (U32Mul, U32Type), - (Mul(_), Some(((U64Type, []), (U64Type, [])))) => (U64Mul, U64Type), - - (Mul(_), Some(((S8Type, []), (S8Type, [])))) => (S8Mul, S8Type), - (Mul(_), Some(((S16Type, []), (S16Type, [])))) => (S16Mul, S16Type), - (Mul(_), Some(((S32Type, []), (S32Type, [])))) => (S32Mul, S32Type), - (Mul(_), Some(((S64Type, []), (S64Type, [])))) => (S64Mul, S64Type), - - (Div(_), Some(((U8Type, []), (U8Type, [])))) => (U8Div, U8Type), - (Div(_), Some(((U16Type, []), (U16Type, [])))) => (U16Div, U16Type), - (Div(_), Some(((U32Type, []), (U32Type, [])))) => (U32Div, U32Type), - (Div(_), Some(((U64Type, []), (U64Type, [])))) => (U64Div, U64Type), - - (Div(_), Some(((S8Type, []), (S8Type, [])))) => (S8Div, S8Type), - (Div(_), Some(((S16Type, []), (S16Type, [])))) => (S16Div, S16Type), - (Div(_), Some(((S32Type, []), (S32Type, [])))) => (S32Div, S32Type), - (Div(_), Some(((S64Type, []), (S64Type, [])))) => (S64Div, S64Type), - - (Add(_), Some(((U8Type, []), (U8Type, [])))) => (U8Add, U8Type), - (Add(_), Some(((U16Type, []), (U16Type, [])))) => (U16Add, U16Type), - (Add(_), Some(((U32Type, []), (U32Type, [])))) => (U32Add, U32Type), - (Add(_), Some(((U64Type, []), (U64Type, [])))) => (U64Add, U64Type), - - (Add(_), Some(((S8Type, []), (S8Type, [])))) => (S8Add, S8Type), - (Add(_), Some(((S16Type, []), (S16Type, [])))) => (S16Add, S16Type), - (Add(_), Some(((S32Type, []), (S32Type, [])))) => (S32Add, S32Type), - (Add(_), Some(((S64Type, []), (S64Type, [])))) => (S64Add, S64Type), - - (Add(_), Some(((PosType, []), (U8Type, [])))) => (PosAddU8, PosType), - (Add(_), Some(((PosType, []), (U16Type, [])))) => (PosAddU16, PosType), - (Add(_), Some(((PosType, []), (U32Type, [])))) => (PosAddU32, PosType), - (Add(_), Some(((PosType, []), (U64Type, [])))) => (PosAddU64, PosType), - - (Sub(_), Some(((U8Type, []), (U8Type, [])))) => (U8Sub, U8Type), - (Sub(_), Some(((U16Type, []), (U16Type, [])))) => (U16Sub, U16Type), - (Sub(_), Some(((U32Type, []), (U32Type, [])))) => (U32Sub, U32Type), - (Sub(_), Some(((U64Type, []), (U64Type, [])))) => (U64Sub, U64Type), - - (Sub(_), Some(((S8Type, []), (S8Type, [])))) => (S8Sub, S8Type), - (Sub(_), Some(((S16Type, []), (S16Type, [])))) => (S16Sub, S16Type), - (Sub(_), Some(((S32Type, []), (S32Type, [])))) => (S32Sub, S32Type), - (Sub(_), Some(((S64Type, []), (S64Type, [])))) => (S64Sub, S64Type), - - (Eq(_), Some(((BoolType, []), (BoolType, [])))) => (BoolEq, BoolType), - (Neq(_), Some(((BoolType, []), (BoolType, [])))) => (BoolNeq, BoolType), - - (Eq(_), Some(((U8Type, []), (U8Type, [])))) => (U8Eq, BoolType), - (Eq(_), Some(((U16Type, []), (U16Type, [])))) => (U16Eq, BoolType), - (Eq(_), Some(((U32Type, []), (U32Type, [])))) => (U32Eq, BoolType), - (Eq(_), Some(((U64Type, []), (U64Type, [])))) => (U64Eq, BoolType), - - (Eq(_), Some(((S8Type, []), (S8Type, [])))) => (S8Eq, BoolType), - (Eq(_), Some(((S16Type, []), (S16Type, [])))) => (S16Eq, BoolType), - (Eq(_), Some(((S32Type, []), (S32Type, [])))) => (S32Eq, BoolType), - (Eq(_), Some(((S64Type, []), (S64Type, [])))) => (S64Eq, BoolType), - - (Neq(_), Some(((U8Type, []), (U8Type, [])))) => (U8Neq, BoolType), - (Neq(_), Some(((U16Type, []), (U16Type, [])))) => (U16Neq, BoolType), - (Neq(_), Some(((U32Type, []), (U32Type, [])))) => (U32Neq, BoolType), - (Neq(_), Some(((U64Type, []), (U64Type, [])))) => (U64Neq, BoolType), - - (Neq(_), Some(((S8Type, []), (S8Type, [])))) => (S8Neq, BoolType), - (Neq(_), Some(((S16Type, []), (S16Type, [])))) => (S16Neq, BoolType), - (Neq(_), Some(((S32Type, []), (S32Type, [])))) => (S32Neq, BoolType), - (Neq(_), Some(((S64Type, []), (S64Type, [])))) => (S64Neq, BoolType), - - (Lt(_), Some(((U8Type, []), (U8Type, [])))) => (U8Lt, BoolType), - (Lt(_), Some(((U16Type, []), (U16Type, [])))) => (U16Lt, BoolType), - (Lt(_), Some(((U32Type, []), (U32Type, [])))) => (U32Lt, BoolType), - (Lt(_), Some(((U64Type, []), (U64Type, [])))) => (U64Lt, BoolType), - - (Lt(_), Some(((S8Type, []), (S8Type, [])))) => (S8Lt, BoolType), - (Lt(_), Some(((S16Type, []), (S16Type, [])))) => (S16Lt, BoolType), - (Lt(_), Some(((S32Type, []), (S32Type, [])))) => (S32Lt, BoolType), - (Lt(_), Some(((S64Type, []), (S64Type, [])))) => (S64Lt, BoolType), - - (Lte(_), Some(((U8Type, []), (U8Type, [])))) => (U8Lte, BoolType), - (Lte(_), Some(((U16Type, []), (U16Type, [])))) => (U16Lte, BoolType), - (Lte(_), Some(((U32Type, []), (U32Type, [])))) => (U32Lte, BoolType), - (Lte(_), Some(((U64Type, []), (U64Type, [])))) => (U64Lte, BoolType), - - (Lte(_), Some(((S8Type, []), (S8Type, [])))) => (S8Lte, BoolType), - (Lte(_), Some(((S16Type, []), (S16Type, [])))) => (S16Lte, BoolType), - (Lte(_), Some(((S32Type, []), (S32Type, [])))) => (S32Lte, BoolType), - (Lte(_), Some(((S64Type, []), (S64Type, [])))) => (S64Lte, BoolType), - - (Gt(_), Some(((U8Type, []), (U8Type, [])))) => (U8Gt, BoolType), - (Gt(_), Some(((U16Type, []), (U16Type, [])))) => (U16Gt, BoolType), - (Gt(_), Some(((U32Type, []), (U32Type, [])))) => (U32Gt, BoolType), - (Gt(_), Some(((U64Type, []), (U64Type, [])))) => (U64Gt, BoolType), - - (Gt(_), Some(((S8Type, []), (S8Type, [])))) => (S8Gt, BoolType), - (Gt(_), Some(((S16Type, []), (S16Type, [])))) => (S16Gt, BoolType), - (Gt(_), Some(((S32Type, []), (S32Type, [])))) => (S32Gt, BoolType), - (Gt(_), Some(((S64Type, []), (S64Type, [])))) => (S64Gt, BoolType), - - (Gte(_), Some(((U8Type, []), (U8Type, [])))) => (U8Gte, BoolType), - (Gte(_), Some(((U16Type, []), (U16Type, [])))) => (U16Gte, BoolType), - (Gte(_), Some(((U32Type, []), (U32Type, [])))) => (U32Gte, BoolType), - (Gte(_), Some(((U64Type, []), (U64Type, [])))) => (U64Gte, BoolType), - - (Gte(_), Some(((S8Type, []), (S8Type, [])))) => (S8Gte, BoolType), - (Gte(_), Some(((S16Type, []), (S16Type, [])))) => (S16Gte, BoolType), - (Gte(_), Some(((S32Type, []), (S32Type, [])))) => (S32Gte, BoolType), - (Gte(_), Some(((S64Type, []), (S64Type, [])))) => (S64Gte, BoolType), + + let lhs_prim = lhs_type.match_prim_spine(); + let (prim, rhs_prim_type, ret_prim_type) = match (op, lhs_prim) { + (Add(_), Some((U8Type, []))) => (U8Add, U8Type, U8Type), + (Add(_), Some((U16Type, []))) => (U16Add, U16Type, U16Type), + (Add(_), Some((U32Type, []))) => (U32Add, U32Type, U32Type), + (Add(_), Some((U64Type, []))) => (U64Add, U64Type, U64Type), + + (Add(_), Some((S8Type, []))) => (S8Add, S8Type, S8Type), + (Add(_), Some((S16Type, []))) => (S16Add, S16Type, S16Type), + (Add(_), Some((S32Type, []))) => (S32Add, S32Type, S32Type), + (Add(_), Some((S64Type, []))) => (S64Add, S64Type, S64Type), + + (Sub(_), Some((U8Type, []))) => (U8Sub, U8Type, U8Type), + (Sub(_), Some((U16Type, []))) => (U16Sub, U16Type, U16Type), + (Sub(_), Some((U32Type, []))) => (U32Sub, U32Type, U32Type), + (Sub(_), Some((U64Type, []))) => (U64Sub, U64Type, U64Type), + + (Sub(_), Some((S8Type, []))) => (S8Sub, S8Type, S8Type), + (Sub(_), Some((S16Type, []))) => (S16Sub, S16Type, S16Type), + (Sub(_), Some((S32Type, []))) => (S32Sub, S32Type, S32Type), + (Sub(_), Some((S64Type, []))) => (S64Sub, S64Type, S64Type), + + (Mul(_), Some((U8Type, []))) => (U8Mul, U8Type, U8Type), + (Mul(_), Some((U16Type, []))) => (U16Mul, U16Type, U16Type), + (Mul(_), Some((U32Type, []))) => (U32Mul, U32Type, U32Type), + (Mul(_), Some((U64Type, []))) => (U64Mul, U64Type, U64Type), + + (Mul(_), Some((S8Type, []))) => (S8Mul, S8Type, S8Type), + (Mul(_), Some((S16Type, []))) => (S16Mul, S16Type, S16Type), + (Mul(_), Some((S32Type, []))) => (S32Mul, S32Type, S32Type), + (Mul(_), Some((S64Type, []))) => (S64Mul, S64Type, S64Type), + + (Div(_), Some((U8Type, []))) => (U8Div, U8Type, U8Type), + (Div(_), Some((U16Type, []))) => (U16Div, U16Type, U16Type), + (Div(_), Some((U32Type, []))) => (U32Div, U32Type, U32Type), + (Div(_), Some((U64Type, []))) => (U64Div, U64Type, U64Type), + + (Div(_), Some((S8Type, []))) => (S8Div, S8Type, S8Type), + (Div(_), Some((S16Type, []))) => (S16Div, S16Type, S16Type), + (Div(_), Some((S32Type, []))) => (S32Div, S32Type, S32Type), + (Div(_), Some((S64Type, []))) => (S64Div, S64Type, S64Type), + + (Eq(_), Some((BoolType, []))) => (BoolEq, BoolType, BoolType), + (Neq(_), Some((BoolType, []))) => (BoolNeq, BoolType, BoolType), + + (Eq(_), Some((U8Type, []))) => (U8Eq, U8Type, BoolType), + (Eq(_), Some((U16Type, []))) => (U16Eq, U16Type, BoolType), + (Eq(_), Some((U32Type, []))) => (U32Eq, U32Type, BoolType), + (Eq(_), Some((U64Type, []))) => (U64Eq, U64Type, BoolType), + + (Eq(_), Some((S8Type, []))) => (S8Eq, S8Type, BoolType), + (Eq(_), Some((S16Type, []))) => (S16Eq, S16Type, BoolType), + (Eq(_), Some((S32Type, []))) => (S32Eq, S32Type, BoolType), + (Eq(_), Some((S64Type, []))) => (S64Eq, S64Type, BoolType), + + (Neq(_), Some((U8Type, []))) => (U8Neq, U8Type, BoolType), + (Neq(_), Some((U16Type, []))) => (U16Neq, U16Type, BoolType), + (Neq(_), Some((U32Type, []))) => (U32Neq, U32Type, BoolType), + (Neq(_), Some((U64Type, []))) => (U64Neq, U64Type, BoolType), + + (Neq(_), Some((S8Type, []))) => (S8Neq, S8Type, BoolType), + (Neq(_), Some((S16Type, []))) => (S16Neq, S16Type, BoolType), + (Neq(_), Some((S32Type, []))) => (S32Neq, S32Type, BoolType), + (Neq(_), Some((S64Type, []))) => (S64Neq, S64Type, BoolType), + + (Lt(_), Some((U8Type, []))) => (U8Lt, U8Type, BoolType), + (Lt(_), Some((U16Type, []))) => (U16Lt, U16Type, BoolType), + (Lt(_), Some((U32Type, []))) => (U32Lt, U32Type, BoolType), + (Lt(_), Some((U64Type, []))) => (U64Lt, U64Type, BoolType), + + (Lt(_), Some((S8Type, []))) => (S8Lt, S8Type, BoolType), + (Lt(_), Some((S16Type, []))) => (S16Lt, S16Type, BoolType), + (Lt(_), Some((S32Type, []))) => (S32Lt, S32Type, BoolType), + (Lt(_), Some((S64Type, []))) => (S64Lt, S64Type, BoolType), + + (Lte(_), Some((U8Type, []))) => (U8Lte, U8Type, BoolType), + (Lte(_), Some((U16Type, []))) => (U16Lte, U16Type, BoolType), + (Lte(_), Some((U32Type, []))) => (U32Lte, U32Type, BoolType), + (Lte(_), Some((U64Type, []))) => (U64Lte, U64Type, BoolType), + + (Lte(_), Some((S8Type, []))) => (S8Lte, S8Type, BoolType), + (Lte(_), Some((S16Type, []))) => (S16Lte, S16Type, BoolType), + (Lte(_), Some((S32Type, []))) => (S32Lte, S32Type, BoolType), + (Lte(_), Some((S64Type, []))) => (S64Lte, S64Type, BoolType), + + (Gt(_), Some((U8Type, []))) => (U8Gt, U8Type, BoolType), + (Gt(_), Some((U16Type, []))) => (U16Gt, U16Type, BoolType), + (Gt(_), Some((U32Type, []))) => (U32Gt, U32Type, BoolType), + (Gt(_), Some((U64Type, []))) => (U64Gt, U64Type, BoolType), + + (Gt(_), Some((S8Type, []))) => (S8Gt, S8Type, BoolType), + (Gt(_), Some((S16Type, []))) => (S16Gt, S16Type, BoolType), + (Gt(_), Some((S32Type, []))) => (S32Gt, S32Type, BoolType), + (Gt(_), Some((S64Type, []))) => (S64Gt, S64Type, BoolType), + + (Gte(_), Some((U8Type, []))) => (U8Gte, U8Type, BoolType), + (Gte(_), Some((U16Type, []))) => (U16Gte, U16Type, BoolType), + (Gte(_), Some((U32Type, []))) => (U32Gte, U32Type, BoolType), + (Gte(_), Some((U64Type, []))) => (U64Gte, U64Type, BoolType), + + (Gte(_), Some((S8Type, []))) => (S8Gte, S8Type, BoolType), + (Gte(_), Some((S16Type, []))) => (S16Gte, S16Type, BoolType), + (Gte(_), Some((S32Type, []))) => (S32Gte, S32Type, BoolType), + (Gte(_), Some((S64Type, []))) => (S64Gte, S64Type, BoolType), _ => { - self.push_message(Message::BinOpMismatchedTypes { - range: self.file_range(range), - lhs_range: self.file_range(lhs.range()), - rhs_range: self.file_range(rhs.range()), - op: op.map_range(|range| self.file_range(range)), - lhs: self.pretty_value(&lhs_type), - rhs: self.pretty_value(&rhs_type), - }); - return self.synth_reported_error(range); + let (rhs_expr, rhs_type) = self.synth_and_insert_implicit_apps(rhs); + let rhs_type = self.elim_env().force(&rhs_type); + let rhs_prim = rhs_type.match_prim_spine(); + + let operand_types = Option::zip(lhs_prim, rhs_prim); + let (prim, ret_prim_type) = match (op, operand_types) { + (Add(_), Some(((PosType, []), (U8Type, [])))) => (PosAddU8, PosType), + (Add(_), Some(((PosType, []), (U16Type, [])))) => (PosAddU16, PosType), + (Add(_), Some(((PosType, []), (U32Type, [])))) => (PosAddU32, PosType), + (Add(_), Some(((PosType, []), (U64Type, [])))) => (PosAddU64, PosType), + _ => { + self.push_message(Message::BinOpMismatchedTypes { + range: self.file_range(range), + lhs_range: self.file_range(lhs.range()), + rhs_range: self.file_range(rhs.range()), + op: op.map_range(|range| self.file_range(range)), + lhs: self.pretty_value(&lhs_type), + rhs: self.pretty_value(&rhs_type), + }); + return self.synth_reported_error(range); + } + }; + + let ret_type = Spanned::empty(Arc::new(Value::prim(ret_prim_type, []))); + + let fun_head = core::Term::Prim(self.file_range(op.range()).into(), prim); + let fun_app = core::Term::FunApp( + self.file_range(range).into(), + Plicity::Explicit, + self.scope.to_scope(core::Term::FunApp( + Span::merge(&lhs_expr.span(), &rhs_expr.span()), + Plicity::Explicit, + self.scope.to_scope(fun_head), + self.scope.to_scope(lhs_expr), + )), + self.scope.to_scope(rhs_expr), + ); + + return (fun_app, ret_type); } }; - let fun_head = core::Term::Prim(self.file_range(op.range()).into(), fun); + let rhs_type = Spanned::empty(Arc::new(Value::prim(rhs_prim_type, []))); + let ret_type = Spanned::empty(Arc::new(Value::prim(ret_prim_type, []))); + + let rhs_expr = self.check(rhs, &rhs_type); + + let fun_head = core::Term::Prim(self.file_range(op.range()).into(), prim); let fun_app = core::Term::FunApp( self.file_range(range).into(), Plicity::Explicit, @@ -1996,11 +2024,8 @@ impl<'arena> Context<'arena> { self.scope.to_scope(rhs_expr), ); - // TODO: Maybe it would be good to reuse lhs_type here if body_type is the same - ( - fun_app, - Spanned::empty(Arc::new(Value::prim(body_type, []))), - ) + // TODO: Maybe it would be good to reuse lhs_type here if ret_type is the same + (fun_app, ret_type) } fn check_bin_op( diff --git a/tests/succeed/binops/synth.fathom b/tests/succeed/binops/synth.fathom index b89ae12f7..e2a1e97e0 100644 --- a/tests/succeed/binops/synth.fathom +++ b/tests/succeed/binops/synth.fathom @@ -1,39 +1,109 @@ -let device_table = ( - let u16_div_ceil = fun (numerator : U16) => fun (denominator : U16) => ( - let quotient = numerator / denominator; - match ((quotient * denominator) < numerator) { - true => quotient + (1 : U16), - false => quotient, - } - ); - - let delta_bits = fun (delta_format : U16) => fun (num_sizes : U16) => - match delta_format { - // Signed 2-bit value, 8 values per u16be - 0x0001 => num_sizes * (2 : U16), - // Signed 4-bit value, 4 values per u16be - 0x0002 => num_sizes * (4 : U16), - // Signed 8-bit value, 2 values per u16be - 0x0003 => num_sizes * (8 : U16), - // Unreachable due to match done in device_or_variation_index_table - _ => 0, - }; - - let num_sizes = fun (start : U16) => fun (end : U16) => - (end - start) + (1 : U16); - - { - /// Smallest size to correct, in ppem - start_size <- u16be, - /// Largest size to correct, in ppem - end_size <- u16be, - /// Format of deltaValue array data - delta_format <- u16be, - /// Array of compressed data - delta_values <- - let delta_bits = delta_bits delta_format (num_sizes start_size end_size); - repeat_len16 (u16_div_ceil delta_bits 16) u16be, - } -); +let _ = (1 : U8 ) + 1; +let _ = (1 : U16) + 1; +let _ = (1 : U32) + 1; +let _ = (1 : U64) + 1; + +let _ = (1 : S8 ) + 1; +let _ = (1 : S16) + 1; +let _ = (1 : S32) + 1; +let _ = (1 : S64) + 1; + +let _ = (1 : U8 ) - 1; +let _ = (1 : U16) - 1; +let _ = (1 : U32) - 1; +let _ = (1 : U64) - 1; + +let _ = (1 : S8 ) - 1; +let _ = (1 : S16) - 1; +let _ = (1 : S32) - 1; +let _ = (1 : S64) - 1; + +let _ = (1 : U8 ) * 1; +let _ = (1 : U16) * 1; +let _ = (1 : U32) * 1; +let _ = (1 : U64) * 1; + +let _ = (1 : S8 ) * 1; +let _ = (1 : S16) * 1; +let _ = (1 : S32) * 1; +let _ = (1 : S64) * 1; + +let _ = (1 : U8 ) / 1; +let _ = (1 : U16) / 1; +let _ = (1 : U32) / 1; +let _ = (1 : U64) / 1; + +let _ = (1 : S8 ) / 1; +let _ = (1 : S16) / 1; +let _ = (1 : S32) / 1; +let _ = (1 : S64) / 1; + +let _ = true == true; +let _ = true != true; + +let _ = (1 : U8 ) == 1; +let _ = (1 : U16) == 1; +let _ = (1 : U32) == 1; +let _ = (1 : U64) == 1; + +let _ = (1 : S8 ) == 1; +let _ = (1 : S16) == 1; +let _ = (1 : S32) == 1; +let _ = (1 : S64) == 1; + +let _ = (1 : U8 ) != 1; +let _ = (1 : U16) != 1; +let _ = (1 : U32) != 1; +let _ = (1 : U64) != 1; + +let _ = (1 : S8 ) != 1; +let _ = (1 : S16) != 1; +let _ = (1 : S32) != 1; +let _ = (1 : S64) != 1; + +let _ = (1 : U8 ) > 1; +let _ = (1 : U16) > 1; +let _ = (1 : U32) > 1; +let _ = (1 : U64) > 1; + +let _ = (1 : S8 ) > 1; +let _ = (1 : S16) > 1; +let _ = (1 : S32) > 1; +let _ = (1 : S64) > 1; + +let _ = (1 : U8 ) >= 1; +let _ = (1 : U16) >= 1; +let _ = (1 : U32) >= 1; +let _ = (1 : U64) >= 1; + +let _ = (1 : S8 ) >= 1; +let _ = (1 : S16) >= 1; +let _ = (1 : S32) >= 1; +let _ = (1 : S64) >= 1; + +let _ = (1 : U8 ) < 1; +let _ = (1 : U16) < 1; +let _ = (1 : U32) < 1; +let _ = (1 : U64) < 1; + +let _ = (1 : S8 ) < 1; +let _ = (1 : S16) < 1; +let _ = (1 : S32) < 1; +let _ = (1 : S64) < 1; + +let _ = (1 : U8 ) <= 1; +let _ = (1 : U16) <= 1; +let _ = (1 : U32) <= 1; +let _ = (1 : U64) <= 1; + +let _ = (1 : S8 ) <= 1; +let _ = (1 : S16) <= 1; +let _ = (1 : S32) <= 1; +let _ = (1 : S64) <= 1; + +let _ = fun (x : Pos) => x + (1 : U8); +let _ = fun (x : Pos) => x + (1 : U16); +let _ = fun (x : Pos) => x + (1 : U32); +let _ = fun (x : Pos) => x + (1 : U64); {} diff --git a/tests/succeed/binops/synth.snap b/tests/succeed/binops/synth.snap index ff3bf27b2..328f8a43f 100644 --- a/tests/succeed/binops/synth.snap +++ b/tests/succeed/binops/synth.snap @@ -1,23 +1,90 @@ stdout = ''' -let device_table : Format = let u16_div_ceil : U16 -> U16 -> U16 = -fun numerator denominator => let quotient : U16 = numerator / denominator; -if (quotient * denominator) < numerator then quotient + (1 : U16) else quotient; -let delta_bits : U16 -> U16 -> U16 = -fun delta_format num_sizes => match delta_format { - 0x1 => num_sizes * (2 : U16), - 0x2 => num_sizes * (4 : U16), - 0x3 => num_sizes * (8 : U16), - _ => 0, -}; -let num_sizes : U16 -> U16 -> U16 = fun start end => end - start + (1 : U16); -{ - start_size <- u16be, - end_size <- u16be, - delta_format <- u16be, - delta_values <- let delta_bits : U16 = - delta_bits delta_format (num_sizes start_size end_size); - repeat_len16 (u16_div_ceil delta_bits 16) u16be, -}; +let _ : U8 = (1 : U8) + (1 : U8); +let _ : U16 = (1 : U16) + (1 : U16); +let _ : U32 = (1 : U32) + (1 : U32); +let _ : U64 = (1 : U64) + (1 : U64); +let _ : S8 = (1 : S8) + (1 : S8); +let _ : S16 = (1 : S16) + (1 : S16); +let _ : S32 = (1 : S32) + (1 : S32); +let _ : S64 = (1 : S64) + (1 : S64); +let _ : U8 = (1 : U8) - (1 : U8); +let _ : U16 = (1 : U16) - (1 : U16); +let _ : U32 = (1 : U32) - (1 : U32); +let _ : U64 = (1 : U64) - (1 : U64); +let _ : S8 = (1 : S8) - (1 : S8); +let _ : S16 = (1 : S16) - (1 : S16); +let _ : S32 = (1 : S32) - (1 : S32); +let _ : S64 = (1 : S64) - (1 : S64); +let _ : U8 = (1 : U8) * (1 : U8); +let _ : U16 = (1 : U16) * (1 : U16); +let _ : U32 = (1 : U32) * (1 : U32); +let _ : U64 = (1 : U64) * (1 : U64); +let _ : S8 = (1 : S8) * (1 : S8); +let _ : S16 = (1 : S16) * (1 : S16); +let _ : S32 = (1 : S32) * (1 : S32); +let _ : S64 = (1 : S64) * (1 : S64); +let _ : U8 = (1 : U8) / (1 : U8); +let _ : U16 = (1 : U16) / (1 : U16); +let _ : U32 = (1 : U32) / (1 : U32); +let _ : U64 = (1 : U64) / (1 : U64); +let _ : S8 = (1 : S8) / (1 : S8); +let _ : S16 = (1 : S16) / (1 : S16); +let _ : S32 = (1 : S32) / (1 : S32); +let _ : S64 = (1 : S64) / (1 : S64); +let _ : Bool = true == true; +let _ : Bool = true != true; +let _ : Bool = (1 : U8) == (1 : U8); +let _ : Bool = (1 : U16) == (1 : U16); +let _ : Bool = (1 : U32) == (1 : U32); +let _ : Bool = (1 : U64) == (1 : U64); +let _ : Bool = (1 : S8) == (1 : S8); +let _ : Bool = (1 : S16) == (1 : S16); +let _ : Bool = (1 : S32) == (1 : S32); +let _ : Bool = (1 : S64) == (1 : S64); +let _ : Bool = (1 : U8) != (1 : U8); +let _ : Bool = (1 : U16) != (1 : U16); +let _ : Bool = (1 : U32) != (1 : U32); +let _ : Bool = (1 : U64) != (1 : U64); +let _ : Bool = (1 : S8) != (1 : S8); +let _ : Bool = (1 : S16) != (1 : S16); +let _ : Bool = (1 : S32) != (1 : S32); +let _ : Bool = (1 : S64) != (1 : S64); +let _ : Bool = (1 : U8) > (1 : U8); +let _ : Bool = (1 : U16) > (1 : U16); +let _ : Bool = (1 : U32) > (1 : U32); +let _ : Bool = (1 : U64) > (1 : U64); +let _ : Bool = (1 : S8) > (1 : S8); +let _ : Bool = (1 : S16) > (1 : S16); +let _ : Bool = (1 : S32) > (1 : S32); +let _ : Bool = (1 : S64) > (1 : S64); +let _ : Bool = (1 : U8) >= (1 : U8); +let _ : Bool = (1 : U16) >= (1 : U16); +let _ : Bool = (1 : U32) >= (1 : U32); +let _ : Bool = (1 : U64) >= (1 : U64); +let _ : Bool = (1 : S8) >= (1 : S8); +let _ : Bool = (1 : S16) >= (1 : S16); +let _ : Bool = (1 : S32) >= (1 : S32); +let _ : Bool = (1 : S64) >= (1 : S64); +let _ : Bool = (1 : U8) < (1 : U8); +let _ : Bool = (1 : U16) < (1 : U16); +let _ : Bool = (1 : U32) < (1 : U32); +let _ : Bool = (1 : U64) < (1 : U64); +let _ : Bool = (1 : S8) < (1 : S8); +let _ : Bool = (1 : S16) < (1 : S16); +let _ : Bool = (1 : S32) < (1 : S32); +let _ : Bool = (1 : S64) < (1 : S64); +let _ : Bool = (1 : U8) <= (1 : U8); +let _ : Bool = (1 : U16) <= (1 : U16); +let _ : Bool = (1 : U32) <= (1 : U32); +let _ : Bool = (1 : U64) <= (1 : U64); +let _ : Bool = (1 : S8) <= (1 : S8); +let _ : Bool = (1 : S16) <= (1 : S16); +let _ : Bool = (1 : S32) <= (1 : S32); +let _ : Bool = (1 : S64) <= (1 : S64); +let _ : Pos -> Pos = fun x => x + (1 : U8); +let _ : Pos -> Pos = fun x => x + (1 : U16); +let _ : Pos -> Pos = fun x => x + (1 : U32); +let _ : Pos -> Pos = fun x => x + (1 : U64); () : () ''' stderr = ''