Small cleanups

src/fun/builtins.bend

@@ -109,7 +109,7 @@ def DiffList/append(diff: List(T) -> List(T), val: T) -> (List(T) -> List(T)):
 # Concatenates two difference lists.
 def DiffList/concat(
   left: List(T) -> List(T),
-  right: List(T) -> List(T) 
+  right: List(T) -> List(T)
 ) -> (List(T) -> List(T)):
   return lambda x: left(right(x))
 
@@ -263,7 +263,7 @@ def IO/bind(a: IO(A), b: ((Id -> Id) -> A -> IO(B))) -> IO(B):
 # Calls an IO by its name with the given arguments.
 #
 # The arguments are untyped and not checked for type correctness.
-# If type safety is desired, this function should be wrapped with 
+# If type safety is desired, this function should be wrapped with
 # another that checks the types of the arguments and of the return.
 #
 # Always returns a `Result` where the error is an `IOError`, a type
@@ -427,7 +427,7 @@ def IO/FS/write_file(path: String, bytes: List(u24)) -> IO(Result(None, u24)):
     res_f <- IO/FS/open(path, "w")
     match res_f:
       case Result/Ok:
-        f = res_f.val 
+        f = res_f.val
         res1 <- IO/FS/write(f, bytes)
         res2 <- IO/FS/close(f)
         return wrap(Result/and(res2, res1))

src/fun/transform/encode_adts.rs

@@ -1,26 +1,23 @@
 use crate::{
-  fun::{Book, Definition, Name, Num, Pattern, Rule, Source, SourceKind, Term, Type},
+  fun::{Book, Definition, Name, Num, Pattern, Rule, Source, Term},
   AdtEncoding,
 };
 
 impl Book {
   /// Defines a function for each constructor in each ADT in the book.
   pub fn encode_adts(&mut self, adt_encoding: AdtEncoding) {
     let mut defs = vec![];
-    let mut tags = vec![];
 
-    for (adt_name, adt) in self.adts.iter() {
+    for (_, adt) in self.adts.iter() {
       for (ctr_idx, (ctr_name, ctr)) in adt.ctrs.iter().enumerate() {
         let ctrs: Vec<_> = adt.ctrs.keys().cloned().collect();
 
         let body = match adt_encoding {
           AdtEncoding::Scott => encode_ctr_scott(ctr.fields.iter().map(|f| &f.nam), ctrs, ctr_name),
           AdtEncoding::NumScott => {
-            let tag = make_tag(adt_name == ctr_name, ctr_name);
-            let body = encode_ctr_num_scott(ctr.fields.iter().map(|f| &f.nam), &tag);
-            let tag_def = make_tag_def(ctr_idx, &tag, adt.source.clone());
-            tags.push((tag, tag_def));
-            body
+            let tag = encode_num_scott_tag(ctr_idx as u32, ctr_name, adt.source.clone());
+            defs.push((tag.name.clone(), tag.clone()));
+            encode_ctr_num_scott(ctr.fields.iter().map(|f| &f.nam), &tag.name)
           }
         };
 
@@ -36,16 +33,6 @@ impl Book {
       }
     }
     self.defs.extend(defs);
-    self.defs.extend(tags);
-  }
-}
-
-fn make_tag(is_object: bool, ctr_name: &Name) -> Name {
-  if is_object {
-    Name::new(format!("{ctr_name}/tag"))
-  } else {
-    let (typ, ctr) = ctr_name.rsplit_once('/').expect("To split at '/'");
-    Name::new(format!("{typ}/{ctr}/tag"))
   }
 }
 
@@ -71,9 +58,8 @@ fn encode_ctr_num_scott<'a>(ctr_args: impl DoubleEndedIterator<Item = &'a Name>
   Term::rfold_lams(term, ctr_args.cloned().map(Some))
 }
 
-fn make_tag_def(ctr_idx: usize, tag: &Name, source: Source) -> Definition {
-  let rules = vec![Rule { pats: vec![], body: Term::Num { val: Num::U24(ctr_idx as u32) } }];
-  let kind = if source.is_builtin() { SourceKind::Builtin } else { SourceKind::Generated };
-  let source = Source { kind, ..source };
-  Definition { name: tag.clone(), typ: Type::U24, check: true, rules, source }
+fn encode_num_scott_tag(tag : u32, ctr_name: &Name, source: Source) -> Definition {
+  let tag_nam = Name::new(format!("{ctr_name}/tag"));
+  let rules = vec![Rule { pats: vec![], body: Term::Num { val: Num::U24(tag) } }];
+  Definition::new_gen(tag_nam.clone(), rules, source, true)
 }

src/fun/transform/encode_match_terms.rs

@@ -5,13 +5,11 @@ use crate::{
 
 impl Book {
   /// Encodes pattern matching expressions in the book into their
-  /// native/core form. Must be run after [`Ctr::fix_match_terms`].
+  /// core form. Must be run after [`Ctr::fix_match_terms`].
   ///
   /// ADT matches are encoded based on `adt_encoding`.
   ///
   /// Num matches are encoded as a sequence of native num matches (on 0 and 1+).
-  ///
-  /// Var and pair matches become a let expression.
   pub fn encode_matches(&mut self, adt_encoding: AdtEncoding) {
     for def in self.defs.values_mut() {
       for rule in &mut def.rules {

src/fun/transform/fix_match_terms.rs

@@ -16,29 +16,33 @@ enum FixMatchErr {
 impl Ctx<'_> {
   /// Convert all match and switch expressions to a normalized form.
   /// * For matches, resolve the constructors and create the name of the field variables.
-  /// * For switches, resolve the succ case ("_") and create the name of the pred variable.
-  /// * If the match arg is not a variable, it is separated into a let expression and bound to "%matched"
+  /// * For switches, the resolution and name bind is already done during parsing.
   /// * Check for redundant arms and non-exhaustive matches.
+  /// * Converts the initial bind to an alias on every arm, rebuilding the eliminated constructor
+  /// * Since the bind is not needed anywhere else, it's erased from the term.
   ///
   /// Example:
   /// For the program
   /// ```hvm
   /// data MyList = (Cons h t) | Nil
   /// match x {
   ///   Cons: (A x.h x.t)
-  ///   Nil: switch (Foo y) { 0: B; 1: C; _: D }
+  ///   Nil: switch %arg = (Foo y) { 0: B; 1: C; _ %arg-2: D }
   /// }
   /// ```
   /// The following AST transformations will be made:
   /// * The binds `x.h` and `x.t` will be generated and stored in the match term.
-  /// * `(Foo y)`` will be put in a let expression, bound to the variable `%matched`;
-  /// * The bind `%matched-2` will be generated and stored in the switch term.
-  /// * If either was missing one of the match cases (a number or a constructor), we'd get an error.
-  /// * If either included one of the cases more than once (including wildcard patterns), we'd get a warning.
+  /// * If it was missing one of the match cases, we'd get an error.
+  /// * If it included one of the cases more than once (including wildcard patterns), we'd get a warning.
   /// ```hvm
-  /// match x {
-  ///   Cons x.h x.t: (A x.h x.t)
-  ///   Nil: let %matched = (Foo y); switch %matched { 0: B; 1: C; _: D }
+  /// match * = x {
+  ///   Cons x.h x.t: use x = (Cons x.h x.t); (A x.h x.t)
+  ///   Nil: use x = Nil;
+  ///     switch * = (Foo y) {
+  ///       0: use %arg = 0; B;
+  ///       1: use %arg = 1; C;
+  ///       _: use %arg = (+ %arg-2 2); D
+  ///       }
   /// }
   /// ```
   pub fn fix_match_terms(&mut self) -> Result<(), Diagnostics> {

src/fun/transform/float_combinators.rs

@@ -170,8 +170,7 @@ impl Term {
 
         // Check if the function it's referring to is safe
         let safe = if let Some(def) = ctx.book.defs.get(nam) {
-          let ref_safe = def.rule().body.is_safe(ctx);
-          ref_safe
+          def.rule().body.is_safe(ctx)
         } else if let Some((safe, _)) = ctx.combinators.get(nam) {
           *safe
         } else {
@@ -187,13 +186,15 @@ impl Term {
     })
   }
 
-  /// Checks if the term is a lambda sequence with the body being a variable in the scope or a reference.
+  /// Checks if the term is a lambda sequence with a safe body.
+  /// If the body is a variable bound in the lambdas, it's a nullary constructor.
+  /// If the body is a reference, it's in inactive position, so always safe.
   fn is_safe_lambda(&self, ctx: &mut FloatCombinatorsCtx) -> bool {
     let mut current = self;
     let mut scope = Vec::new();
 
-    while let Term::Lam { bod, .. } = current {
-      scope.extend(current.pattern().unwrap().binds().filter_map(|x| x.as_ref()));
+    while let Term::Lam { pat, bod, .. } = current {
+      scope.extend(pat.binds().filter_map(|x| x.as_ref()));
       current = bod;
     }
 

tests/snapshots/desugar_file__ask_branch.bend.snap

@@ -17,30 +17,30 @@ undefer: (((a -> a) -> b) -> b)
 unchecked main: Any
 (main) = (IO/bind (Bool/T λa switch a { 0: (IO/wrap 0); _: λ* (IO/wrap 0); }) λb (b λc λd (c d) IO/wrap))
 
-IO/Done: ((u24, u24) -> a -> (IO a))
-(IO/Done) = λa λb λc (c IO/Done/tag a b)
-
-IO/Call: ((u24, u24) -> String -> Any -> ((Result Any (IOError Any)) -> (IO a)) -> (IO a))
-(IO/Call) = λa λb λc λd λe (e IO/Call/tag a b c d)
-
-Bool/T: Bool
-(Bool/T) = λa (a Bool/T/tag)
-
-Bool/F: Bool
-(Bool/F) = λa (a Bool/F/tag)
-
 IO/Done/tag: u24
 (IO/Done/tag) = 0
 
+IO/Done: ((u24, u24) -> a -> (IO a))
+(IO/Done) = λa λb λc (c IO/Done/tag a b)
+
 IO/Call/tag: u24
 (IO/Call/tag) = 1
 
+IO/Call: ((u24, u24) -> String -> Any -> ((Result Any (IOError Any)) -> (IO a)) -> (IO a))
+(IO/Call) = λa λb λc λd λe (e IO/Call/tag a b c d)
+
 Bool/T/tag: u24
 (Bool/T/tag) = 0
 
+Bool/T: Bool
+(Bool/T) = λa (a Bool/T/tag)
+
 Bool/F/tag: u24
 (Bool/F/tag) = 1
 
+Bool/F: Bool
+(Bool/F) = λa (a Bool/F/tag)
+
 IO/bind__C0: _
 (IO/bind__C0) = λ* λa λb (undefer b a)
 

tests/snapshots/desugar_file__bind_syntax.bend.snap

@@ -17,30 +17,30 @@ unchecked Main: Any
 undefer: (((a -> a) -> b) -> b)
 (undefer) = λa (a λb b)
 
-String/Nil: String
-(String/Nil) = λa (a String/Nil/tag)
-
-String/Cons: (u24 -> String -> String)
-(String/Cons) = λa λb λc (c String/Cons/tag a b)
-
-Result/Ok: (b -> (Result b a))
-(Result/Ok) = λa λb (b Result/Ok/tag a)
-
-Result/Err: (a -> (Result b a))
-(Result/Err) = λa λb (b Result/Err/tag a)
-
 String/Nil/tag: u24
 (String/Nil/tag) = 0
 
+String/Nil: String
+(String/Nil) = λa (a String/Nil/tag)
+
 String/Cons/tag: u24
 (String/Cons/tag) = 1
 
+String/Cons: (u24 -> String -> String)
+(String/Cons) = λa λb λc (c String/Cons/tag a b)
+
 Result/Ok/tag: u24
 (Result/Ok/tag) = 0
 
+Result/Ok: (b -> (Result b a))
+(Result/Ok) = λa λb (b Result/Ok/tag a)
+
 Result/Err/tag: u24
 (Result/Err/tag) = 1
 
+Result/Err: (a -> (Result b a))
+(Result/Err) = λa λb (b Result/Err/tag a)
+
 unchecked Result/bind__C0: _
 (Result/bind__C0) = λa λb (undefer b a)
 

tests/snapshots/desugar_file__combinators.bend.snap

@@ -35,18 +35,18 @@ unchecked B: Any
 unchecked Main: Any
 (Main) = (List/Cons 0 (List/Cons list List/Nil))
 
-List/Nil: (List a)
-(List/Nil) = λa (a List/Nil/tag)
-
-List/Cons: (a -> (List a) -> (List a))
-(List/Cons) = λa λb λc (c List/Cons/tag a b)
-
 List/Nil/tag: u24
 (List/Nil/tag) = 0
 
+List/Nil: (List a)
+(List/Nil) = λa (a List/Nil/tag)
+
 List/Cons/tag: u24
 (List/Cons/tag) = 1
 
+List/Cons: (a -> (List a) -> (List a))
+(List/Cons) = λa λb λc (c List/Cons/tag a b)
+
 unchecked A__C0: _
 (A__C0) = let {a b} = A; λc (a b c)
 

tests/snapshots/desugar_file__deref_loop.bend.snap

@@ -11,18 +11,18 @@ unchecked bar: Any
 unchecked main: Any
 (main) = (foo 0)
 
-nat/succ: (Any -> nat)
-(nat/succ) = λa λb (b nat/succ/tag a)
-
-nat/zero: nat
-(nat/zero) = λa (a nat/zero/tag)
-
 nat/succ/tag: u24
 (nat/succ/tag) = 0
 
+nat/succ: (Any -> nat)
+(nat/succ) = λa λb (b nat/succ/tag a)
+
 nat/zero/tag: u24
 (nat/zero/tag) = 1
 
+nat/zero: nat
+(nat/zero) = λa (a nat/zero/tag)
+
 unchecked foo__C0: _
 (foo__C0) = λ* (bar 0)
 

tests/snapshots/desugar_file__mapper_syntax.bend.snap

@@ -20,18 +20,18 @@ unreachable: Any
 unchecked main: Any
 (main) = let (c, d) = (Map/get (Map/map (Map/map (Map/set (Map/set Map/empty 0 3) 1 4) 1 λa (+ a 1)) 1 λb (* b 2)) 1); let (e, *) = (Map/get d 0); ((λf (+ f 1) 1), c, e)
 
-Map/Node: (a -> (Map a) -> (Map a) -> (Map a))
-(Map/Node) = λa λb λc λd (d Map/Node/tag a b c)
-
-Map/Leaf: (Map a)
-(Map/Leaf) = λa (a Map/Leaf/tag)
-
 Map/Node/tag: u24
 (Map/Node/tag) = 0
 
+Map/Node: (a -> (Map a) -> (Map a) -> (Map a))
+(Map/Node) = λa λb λc λd (d Map/Node/tag a b c)
+
 Map/Leaf/tag: u24
 (Map/Leaf/tag) = 1
 
+Map/Leaf: (Map a)
+(Map/Leaf) = λa (a Map/Leaf/tag)
+
 Map/get__C0: _
 (Map/get__C0) = λa λb λc λd let (e, f) = (Map/get c (/ a 2)); (e, (Map/Node b f d))
 

tests/snapshots/desugar_file__tree_syntax.bend.snap

@@ -35,18 +35,18 @@ unchecked imp3: Any
 unchecked imp4: (Any -> Any)
 (imp4) = λa switch a { 0: (Tree/Leaf 0); _: imp4__C0; }
 
-Tree/Node: ((Tree a) -> (Tree a) -> (Tree a))
-(Tree/Node) = λa λb λc (c Tree/Node/tag a b)
-
-Tree/Leaf: (a -> (Tree a))
-(Tree/Leaf) = λa λb (b Tree/Leaf/tag a)
-
 Tree/Node/tag: u24
 (Tree/Node/tag) = 0
 
+Tree/Node: ((Tree a) -> (Tree a) -> (Tree a))
+(Tree/Node) = λa λb λc (c Tree/Node/tag a b)
+
 Tree/Leaf/tag: u24
 (Tree/Leaf/tag) = 1
 
+Tree/Leaf: (a -> (Tree a))
+(Tree/Leaf) = λa λb (b Tree/Leaf/tag a)
+
 unchecked fun4__C0: _
 (fun4__C0) = λa let {b c} = a; (Tree/Node (fun4 b) (fun4 c))
 

tests/snapshots/encode_pattern_match__adt_tup_era.bend.snap

@@ -19,8 +19,8 @@ unchecked Foo: Any
 unchecked Main: Any
 (Main) = (Foo (Tuple/Pair 1 5))
 
+Tuple/Pair/tag: _
+(Tuple/Pair/tag) = 0
+
 Tuple/Pair: (Any -> Any -> Tuple)
 (Tuple/Pair) = λa λb λc (c Tuple/Pair/tag a b)
-
-Tuple/Pair/tag: u24
-(Tuple/Pair/tag) = 0

tests/snapshots/encode_pattern_match__and3.bend.snap

@@ -22,14 +22,14 @@ unchecked And: Any
 unchecked main: Any
 (main) = (And (Bool/F, Bool/T, Bool/F))
 
+Bool/T/tag: _
+(Bool/T/tag) = 0
+
 Bool/T: Bool
 (Bool/T) = λa (a Bool/T/tag)
 
+Bool/F/tag: _
+(Bool/F/tag) = 1
+
 Bool/F: Bool
 (Bool/F) = λa (a Bool/F/tag)
-
-Bool/T/tag: u24
-(Bool/T/tag) = 0
-
-Bool/F/tag: u24
-(Bool/F/tag) = 1