Remove implicit unsigned integer extensions

Author: Kmeakin

fathom/src/surface/elaboration.rs

@@ -596,31 +596,7 @@ impl<'arena> Context<'arena> {
                     self.scope.to_scope(expr),
                 )
             }
-
-            (_, _) => {
-                // Implictly extend unsigned integer types
-                let extend_prim = match Option::zip(from.match_prim_spine(), to.match_prim_spine())
-                {
-                    Some(((Prim::U8Type, []), (Prim::U16Type, []))) => Prim::U8ExtendU16,
-                    Some(((Prim::U8Type, []), (Prim::U32Type, []))) => Prim::U8ExtendU32,
-                    Some(((Prim::U8Type, []), (Prim::U64Type, []))) => Prim::U8ExtendU64,
-
-                    Some(((Prim::U16Type, []), (Prim::U32Type, []))) => Prim::U16ExtendU32,
-                    Some(((Prim::U16Type, []), (Prim::U64Type, []))) => Prim::U16ExtendU64,
-
-                    Some(((Prim::U32Type, []), (Prim::U64Type, []))) => Prim::U32ExtendU64,
-
-                    // Otherwise, unify the types
-                    _ => return self.convert(surface_range, expr, &from, &to),
-                };
-
-                core::Term::FunApp(
-                    span,
-                    Plicity::Explicit,
-                    self.scope.to_scope(core::Term::Prim(span, extend_prim)),
-                    self.scope.to_scope(expr),
-                )
-            }
+            _ => return self.convert(surface_range, expr, &from, &to),
         }
     }
 

formats/gif.fathom

@@ -50,7 +50,7 @@ def color_table_entry = {
 ///
 /// - [GIF89a Specification: Section 19](https://www.w3.org/Graphics/GIF/spec-gif89a.txt)
 def global_color_table (len : U16) = {
-    entries <- repeat_len64 len color_table_entry,
+    entries <- repeat_len64 (u16_extend_u64 len) color_table_entry,
 };
 
 def main = {

formats/image.fathom

@@ -15,5 +15,5 @@ def main = {
     /// The height of the image, in pixels.
     height <- u32be,
     /// The pixel data.
-    pixels <- repeat_len64 (width * height) pixel,
+    pixels <- repeat_len64 (u32_extend_u64 (width * height)) pixel,
 };

formats/image.snap

@@ -3,7 +3,7 @@ def pixel : Format = { red <- s32be, green <- s32be, blue <- s32be };
 def main : Format = {
     width <- u32be,
     height <- u32be,
-    pixels <- repeat_len64 (u32_extend_u64 width * u32_extend_u64 height) pixel,
+    pixels <- repeat_len64 (u32_extend_u64 (width * height)) pixel,
 };
 '''
 stderr = ''

formats/opentype.fathom

@@ -57,15 +57,15 @@ def cmap_subtable_format4 : Repr platform_id -> Format = fun platform => {
     length <- u16be,
     language <- cmap_language_id platform,
     seg_count_x2 <- u16be,
-    let seg_count : U16 = seg_count_x2 / (2 : U16),
+    let seg_count : U64 = u16_extend_u64 (seg_count_x2 / (2 : U16)),
     search_range <- u16be,
     entry_selector <- u16be,
     range_shift <- u16be,
-    end_code <- repeat_len64 (u16_extend_u64 seg_count) u16be,
+    end_code <- repeat_len64 seg_count u16be,
     _reserved_pad <- reserved s16be 0,
-    start_code <- repeat_len64 (u16_extend_u64 seg_count) u16be,
-    id_delta <- repeat_len64 (u16_extend_u64 seg_count) s16be,
-    id_range_offsets <- repeat_len64 (u16_extend_u64 seg_count) u16be,
+    start_code <- repeat_len64 seg_count u16be,
+    id_delta <- repeat_len64 seg_count s16be,
+    id_range_offsets <- repeat_len64 seg_count u16be,
 };
 def cmap_subtable_format6 : Repr platform_id -> Format = fun platform => {
     length <- u16be,
@@ -384,7 +384,8 @@ def simple_glyph : U16 -> Format = fun number_of_contours => {
     end_pts_of_contours <- repeat_len64 (u16_extend_u64 number_of_contours) u16be,
     instruction_length <- u16be,
     instructions <- repeat_len64 (u16_extend_u64 instruction_length) u8,
-    let last_end_point_index : U16 = array64_index @(u16_extend_u64 number_of_contours) @U16 (u16_extend_u64 number_of_contours - u16_extend_u64 1) end_pts_of_contours,
+    let last_end_point_index : U16 = array64_index @(u16_extend_u64 number_of_contours) @U16 (u16_extend_u64 (number_of_contours - (1 :
+    U16))) end_pts_of_contours,
     let number_of_coords : U16 = last_end_point_index + (1 : U16),
 };
 def glyph : Format = {

formats/opentype.snap

@@ -28,5 +28,5 @@ def triangle = {
 def main = {
     header <- repeat_len64 80 u8,
     triangle_count <- u32le,
-    triangles <- repeat_len64 triangle_count triangle,
+    triangles <- repeat_len64 (u32_extend_u64 triangle_count) triangle,
 };

formats/stl-binary.fathom

@@ -32,7 +32,7 @@ let device_table = (
         /// Array of compressed data
         delta_values <-
             let delta_bits = delta_bits delta_format (num_sizes start_size end_size);
-            repeat_len64 (u16_div_ceil delta_bits 16) u16be,
+            repeat_len64 (u16_extend_u64 (u16_div_ceil delta_bits 16)) u16be,
     }
 );
 

tests/succeed/binops/synth.fathom

@@ -3,5 +3,5 @@
   link <- link start u16be,
   len <- deref link,
   _reserved <- u16be,
-  data <- repeat_len64 len u16be,
+  data <- repeat_len64 (u16_extend_u64 len) u16be,
 }

tests/succeed/format-deref/simple.fathom

@@ -7,7 +7,7 @@ let record0 = {
 
 let record1 = fun (length : U8) => {
     _length <- u8, // Skip length
-    data <- repeat_len64 length u8,
+    data <- repeat_len64 (u8_extend_u64 length) u8,
 };
 
 let silly = overlap {
@@ -18,7 +18,7 @@ let silly = overlap {
 let _ :
         Repr silly -> {
             record0 : { length : U8 },
-            record1 : { _length : U8, data : Array64 record0.length U8 },
+            record1 : { _length : U8, data : Array64 (u8_extend_u64 record0.length) U8 },
         }
     = fun silly => silly;