[sc-519] Add syntax sugar for Nats

cspell.json

@@ -44,6 +44,7 @@
     "mult",
     "namegen",
     "nams",
+    "nats",
     "numop",
     "nums",
     "oper",

src/term/builtins.hvm

@@ -1,3 +1,4 @@
 data String = (String.cons head tail) | (String.nil)
 data List   = (List.cons head tail) | (List.nil)
-data Result = (Result.ok val) | (Result.err val)
+data Result = (Result.ok val) | (Result.err val)
+data Nat    = (Nat.succ pred) | (Nat.zero)

src/term/builtins.rs

@@ -17,6 +17,10 @@ pub const RESULT: &str = "Result";
 pub const RESULT_OK: &str = "Result.ok";
 pub const RESULT_ERR: &str = "Result.err";
 
+pub const NAT: &str = "Nat";
+pub const NAT_SUCC: &str = "Nat.succ";
+pub const NAT_ZERO: &str = "Nat.zero";
+
 impl Book {
   pub fn builtins() -> Book {
     parse_book(BUILTINS, Book::default, true).expect("Error parsing builtin file, this should not happen")
@@ -37,6 +41,7 @@ impl Term {
     match self {
       Term::Lst { els } => *self = Term::encode_list(std::mem::take(els)),
       Term::Str { val } => *self = Term::encode_str(val),
+      Term::Nat { val } => *self = Term::encode_nat(*val),
       Term::Let { pat, val, nxt } => {
         pat.encode_builtins();
         val.encode_builtins();
@@ -87,6 +92,11 @@ impl Term {
       Term::call(Term::r#ref(SCONS), [Term::Num { val: u64::from(char) }, acc])
     })
   }
+
+  pub fn encode_nat(val: u64) -> Term {
+    (0 .. val).fold(Term::r#ref(NAT_ZERO), |acc, _| Term::app(Term::r#ref(NAT_SUCC), acc))
+  }
+
   pub fn encode_ok(val: Term) -> Term {
     Term::call(Term::r#ref(RESULT_OK), [val])
   }

src/term/display.rs

@@ -79,6 +79,7 @@ impl fmt::Display for Term {
       }
       Term::Era => write!(f, "*"),
       Term::Num { val } => write!(f, "{val}"),
+      Term::Nat { val } => write!(f, "#{val}"),
       Term::Str { val } => write!(f, "{val:?}"),
       Term::Opx { op, fst, snd } => {
         write!(f, "({} {} {})", op, fst, snd)

src/term/mod.rs

@@ -122,6 +122,9 @@ pub enum Term {
   Num {
     val: u64,
   },
+  Nat {
+    val: u64,
+  },
   Str {
     val: GlobalString,
   },
@@ -316,6 +319,7 @@ impl Clone for Term {
       }
       Self::Sup { tag, els } => Self::Sup { tag: tag.clone(), els: els.clone() },
       Self::Num { val } => Self::Num { val: *val },
+      Self::Nat { val } => Self::Nat { val: *val },
       Self::Str { val } => Self::Str { val: val.clone() },
       Self::Lst { els } => Self::Lst { els: els.clone() },
       Self::Opx { op, fst, snd } => Self::Opx { op: *op, fst: fst.clone(), snd: snd.clone() },
@@ -464,6 +468,7 @@ impl Term {
       Term::Var { .. }
       | Term::Lnk { .. }
       | Term::Num { .. }
+      | Term::Nat { .. }
       | Term::Str { .. }
       | Term::Ref { .. }
       | Term::Era
@@ -487,6 +492,7 @@ impl Term {
       Term::Var { .. }
       | Term::Lnk { .. }
       | Term::Num { .. }
+      | Term::Nat { .. }
       | Term::Str { .. }
       | Term::Ref { .. }
       | Term::Era
@@ -531,6 +537,7 @@ impl Term {
       Term::Var { .. }
       | Term::Lnk { .. }
       | Term::Num { .. }
+      | Term::Nat { .. }
       | Term::Str { .. }
       | Term::Ref { .. }
       | Term::Era
@@ -568,6 +575,7 @@ impl Term {
       Term::Var { .. }
       | Term::Lnk { .. }
       | Term::Num { .. }
+      | Term::Nat { .. }
       | Term::Str { .. }
       | Term::Ref { .. }
       | Term::Era
@@ -607,6 +615,7 @@ impl Term {
       Term::Var { .. }
       | Term::Lnk { .. }
       | Term::Num { .. }
+      | Term::Nat { .. }
       | Term::Str { .. }
       | Term::Ref { .. }
       | Term::Era
@@ -631,6 +640,7 @@ impl Term {
       | Term::Var { .. }
       | Term::Lnk { .. }
       | Term::Num { .. }
+      | Term::Nat { .. }
       | Term::Str { .. }
       | Term::Ref { .. }
       | Term::Era
@@ -655,6 +665,7 @@ impl Term {
       | Term::Var { .. }
       | Term::Lnk { .. }
       | Term::Num { .. }
+      | Term::Nat { .. }
       | Term::Str { .. }
       | Term::Ref { .. }
       | Term::Era

src/term/net_to_term.rs

@@ -347,7 +347,7 @@ impl Term {
         }
         n
       }
-      Term::Lst { .. } => unreachable!(),
+      Term::Nat { .. } | Term::Lst { .. } => unreachable!(),
       Term::Lnk { .. } | Term::Num { .. } | Term::Str { .. } | Term::Ref { .. } | Term::Era | Term::Err => 0,
     };
 
@@ -419,7 +419,7 @@ impl Term {
           rule.body.fix_names(id_counter, book);
         }
       }
-      Term::Let { .. } | Term::Use { .. } | Term::Lst { .. } => unreachable!(),
+      Term::Let { .. } | Term::Use { .. } | Term::Nat { .. } | Term::Lst { .. } => unreachable!(),
       Term::Var { .. } | Term::Lnk { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era | Term::Err => {}
     }
   }

src/term/parser/parser.rs

@@ -207,6 +207,13 @@ where
     }),
   );
 
+  let nat = just(Token::Hash).ignore_then(select!(Token::Num(num) => Term::Nat { val: num }).or(
+    select!(Token::Error(LexingError::InvalidNumberLiteral) => ()).validate(|_, span, emit| {
+      emit.emit(Rich::custom(span, "found invalid nat literal expected number"));
+      Term::Nat { val: 0 }
+    }),
+  ));
+
   let term_sep = just(Token::Semicolon).or_not();
   let list_sep = just(Token::Comma).or_not();
 
@@ -359,7 +366,7 @@ where
       // OBS: `num_op` has to be before app, idk why?
       // OBS: `app` has to be before `tup` to not overflow on huge app terms
       // TODO: What happens on huge `tup` and other terms?
-      num_op, app, tup, global_var, var, number, list, str, chr, sup, global_lam, lam, dup, let_, use_,
+      num_op, app, tup, global_var, var, number, nat, list, str, chr, sup, global_lam, lam, dup, let_, use_,
       match_, era,
     ))
   })

src/term/term_to_net.rs

@@ -239,8 +239,9 @@ impl EncodeTermState<'_> {
           self.inet.link(Port(node, 1), Port(node, 2));
           Some(Port(node, 0))
         }
-        Term::Str { .. } => unreachable!(), // Removed in desugar str
-        Term::Lst { .. } => unreachable!(), // Removed in desugar list
+        Term::Nat { .. } => unreachable!(), // Removed in encode_nat
+        Term::Str { .. } => unreachable!(), // Removed in encode_str
+        Term::Lst { .. } => unreachable!(), // Removed in encode_list
         // core: & fst ~ <op snd ret>
         Term::Opx { op, fst, snd } => {
           let opx = self.inet.new_node(Op2 { opr: op.to_hvmc_label() });

src/term/transform/definition_pruning.rs

@@ -71,7 +71,7 @@ impl Ctx<'_> {
     for def_name in unused {
       let def = &self.book.defs[&def_name];
       if prune_all || def.builtin {
-        self.book.defs.swap_remove(&def_name);
+        self.book.defs.shift_remove(&def_name);
       } else if !def_name.is_generated() {
         self.info.add_rule_warning(UnusedDefinitionWarning, WarningType::UnusedDefinition, def_name);
       }

src/term/transform/inline.rs

@@ -51,15 +51,15 @@ impl Term {
         },
 
         Term::Chn { .. } | Term::Lnk { .. } => false,
-        Term::Str { .. } | Term::Lst { .. } => false,
         Term::Let { .. } => false,
-        Term::Use { .. } => unreachable!(),
         Term::App { .. } => false,
         Term::Dup { .. } => false,
         Term::Opx { .. } => false,
         Term::Mat { .. } => false,
         Term::Ref { .. } => false,
 
+        Term::Nat { .. } | Term::Str { .. } | Term::Lst { .. } | Term::Use { .. } => unreachable!(),
+
         Term::Err => unreachable!(),
       })
     }

src/term/transform/resugar_builtins.rs

@@ -1,14 +1,41 @@
-use crate::term::{Term, LCONS, LNIL, SCONS, SNIL};
+use crate::term::{Term, LCONS, LNIL, NAT_SUCC, NAT_ZERO, SCONS, SNIL};
 
 impl Term {
   pub fn resugar_builtins(&mut self) {
     self.resugar_strings();
+    self.resugar_nats();
     self.resugar_lists();
   }
 
+  pub fn resugar_nats(&mut self) {
+    Term::recursive_call(move || match self {
+      // (Nat.succ pred)
+      Term::App { fun: box Term::Ref { nam: ctr }, arg: box pred, .. } => {
+        pred.resugar_nats();
+
+        if ctr == NAT_SUCC {
+          if let Term::Nat { val } = pred {
+            *self = Term::Nat { val: *val + 1 };
+          } else {
+            let n = std::mem::take(pred);
+            *self = Term::call(Term::Ref { nam: ctr.clone() }, [n]);
+          }
+        }
+      }
+      // (Nat.zero)
+      Term::Ref { nam: def_name } if def_name == NAT_ZERO => *self = Term::Nat { val: 0 },
+
+      _ => {
+        for child in self.children_mut() {
+          child.resugar_nats();
+        }
+      }
+    });
+  }
+
   /// Rebuilds the String syntax sugar, converting `(Cons 97 Nil)` into `"a"`.
   pub fn resugar_strings(&mut self) {
-    match self {
+    Term::recursive_call(move || match self {
       // (String.cons Num tail)
       Term::App {
         fun: box Term::App { fun: box Term::Ref { nam: ctr }, arg: box head, .. },
@@ -48,12 +75,12 @@ impl Term {
           child.resugar_strings();
         }
       }
-    }
+    });
   }
 
   /// Rebuilds the List syntax sugar, converting `(Cons head Nil)` into `[head]`.
   pub fn resugar_lists(&mut self) {
-    match self {
+    Term::recursive_call(move || match self {
       // (List.cons el tail)
       Term::App {
         fun: box Term::App { fun: box Term::Ref { nam: ctr }, arg: box head, .. },
@@ -84,6 +111,6 @@ impl Term {
           child.resugar_lists();
         }
       }
-    }
+    });
   }
 }

tests/golden_tests/cli/debug_u60_to_nat.hvm

@@ -1,4 +1,4 @@
-data Nat = (Z) | (S nat)
+data Nat_ = (Z) | (S nat)
 
 (U60ToNat 0)   = Z
 (U60ToNat 1+p) = (S (U60ToNat p))

tests/golden_tests/run_file/nat_add.hvm

@@ -0,0 +1,4 @@
+(Nat.add (Nat.zero)   x) = x
+(Nat.add (Nat.succ p) x) = (Nat.succ (Nat.add p x))
+
+(Main) = (Nat.add #25 #9)

tests/golden_tests/run_file/nat_add_num.hvm

@@ -0,0 +1,4 @@
+(Nat.add (Nat.zero)   x) = x
+(Nat.add (Nat.succ p) x) = (Nat.succ (Nat.add p x))
+
+main = (Nat.add #4 0)

tests/golden_tests/simplify_matches/already_flat.hvm

@@ -20,4 +20,4 @@ Rule5 (CtrA3 a) (CtrB3 b) = (a b)
 Rule5 a b = (a b)
 
 Rule6 a = a
-Rule6 b = b
+Rule6 b = b

tests/snapshots/cli__debug_u60_to_nat.hvm.snap

@@ -24,10 +24,10 @@ input_file: tests/golden_tests/cli/debug_u60_to_nat.hvm
 ---------------------------------------
 (S (S (S (S Z))))
 ---------------------------------------
-(S (S (S #Nat λ* #Nat λa #Nat (a Z))))
+(S (S (S #Nat_ λ* #Nat_ λa #Nat_ (a Z))))
 ---------------------------------------
-(S (S #Nat λ* #Nat λa #Nat (a #Nat λ* #Nat λb #Nat (b Z))))
+(S (S #Nat_ λ* #Nat_ λa #Nat_ (a #Nat_ λ* #Nat_ λb #Nat_ (b Z))))
 ---------------------------------------
-(S #Nat λ* #Nat λa #Nat (a #Nat λ* #Nat λb #Nat (b #Nat λ* #Nat λc #Nat (c Z))))
+(S #Nat_ λ* #Nat_ λa #Nat_ (a #Nat_ λ* #Nat_ λb #Nat_ (b #Nat_ λ* #Nat_ λc #Nat_ (c Z))))
 ---------------------------------------
 (S (S (S (S Z))))

tests/snapshots/cli__desugar_bool_scott.hvm.snap

@@ -4,6 +4,6 @@ input_file: tests/golden_tests/cli/desugar_bool_scott.hvm
 ---
 (main) = True
 
-(False) = λ* λb b
-
 (True) = λa λ* a
+
+(False) = λ* λb b

tests/snapshots/cli__desugar_bool_tagged.hvm.snap

@@ -4,6 +4,6 @@ input_file: tests/golden_tests/cli/desugar_bool_tagged.hvm
 ---
 (main) = True
 
-(False) = #Boolean λ* #Boolean λb b
-
 (True) = #Boolean λa #Boolean λ* a
+
+(False) = #Boolean λ* #Boolean λb b

tests/snapshots/compile_file_o_all__adt_option_and.hvm.snap

@@ -3,10 +3,10 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_all/adt_option_and.hvm
 ---
 @None = {2 * {2 a a}}
-@Option.and = ({2 @Option.and$C2 {2 @Option.and$C3_$_Option.and$C1 a}} a)
+@Option.and = ({2 @Option.and$C2 {2 @Option.and$C1_$_Option.and$C3 a}} a)
 @Option.and$C0 = {2 a (b {2 {2 [b a] c} {2 * c}})}
-@Option.and$C2 = {2 a ({2 @Option.and$C0 {2 @Option.and$C3_$_Option.and$C1 (a b)}} b)}
-@Option.and$C3_$_Option.and$C1 = (* @None)
+@Option.and$C1_$_Option.and$C3 = (* @None)
+@Option.and$C2 = {2 a ({2 @Option.and$C0 {2 @Option.and$C1_$_Option.and$C3 (a b)}} b)}
 @Some = (a {2 {2 a b} {2 * b}})
 @main = a
 & @Option.and ~ (b (c a))

tests/snapshots/compile_file_o_all__expr.hvm.snap

@@ -2,17 +2,17 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_all/expr.hvm
 ---
-@App = (a (b {4 * {4 * {4 {4 a {4 b c}} {4 * {4 * {4 * {4 * {4 * {4 * c}}}}}}}}}))
-@Dup = (a (b (c (d {4 * {4 * {4 * {4 * {4 * {4 * {4 {4 a {4 b {4 c {4 d e}}}} {4 * {4 * e}}}}}}}}}))))
-@Let = (a (b (c {4 * {4 * {4 * {4 * {4 * {4 {4 a {4 b {4 c d}}} {4 * {4 * {4 * d}}}}}}}}})))
-@Mul = {2 * @Mul$C1}
-@Mul$C0 = {2 a {2 * a}}
-@Mul$C1 = {2 * @Mul$C0}
-@Num = (a {4 * {4 {4 a b} {4 * {4 * {4 * {4 * {4 * {4 * {4 * b}}}}}}}}})
-@Op2 = (a (b (c {4 * {4 * {4 * {4 * {4 * {4 * {4 * {4 * {4 {4 a {4 b {4 c d}}} d}}}}}}}}})))
-@Sub = {2 * @Sub$C0}
-@Sub$C0 = {2 a {2 * {2 * a}}}
-@Var = (a {4 {4 a b} {4 * {4 * {4 * {4 * {4 * {4 * {4 * {4 * b}}}}}}}}})
+@App = (a (b {2 * {2 * {2 {2 a {2 b c}} {2 * {2 * {2 * {2 * {2 * {2 * c}}}}}}}}}))
+@Dup = (a (b (c (d {2 * {2 * {2 * {2 * {2 * {2 * {2 {2 a {2 b {2 c {2 d e}}}} {2 * {2 * e}}}}}}}}}))))
+@Let = (a (b (c {2 * {2 * {2 * {2 * {2 * {2 {2 a {2 b {2 c d}}} {2 * {2 * {2 * d}}}}}}}}})))
+@Mul = {4 * @Mul$C1}
+@Mul$C0 = {4 a {4 * a}}
+@Mul$C1 = {4 * @Mul$C0}
+@Num = (a {2 * {2 {2 a b} {2 * {2 * {2 * {2 * {2 * {2 * {2 * b}}}}}}}}})
+@Op2 = (a (b (c {2 * {2 * {2 * {2 * {2 * {2 * {2 * {2 * {2 {2 a {2 b {2 c d}}} d}}}}}}}}})))
+@Sub = {4 * @Sub$C0}
+@Sub$C0 = {4 a {4 * {4 * a}}}
+@Var = (a {2 {2 a b} {2 * {2 * {2 * {2 * {2 * {2 * {2 * {2 * b}}}}}}}}})
 @main = a
 & @Let ~ (b (c (d a)))
 & @Dup ~ (e (f (g (h d))))