[sc-519] Add syntax sugar for Nats

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/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 @@
           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 @@
           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/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/compile_file_o_all__list_merge_sort.hvm.snap

@@ -6,19 +6,19 @@ input_file: tests/golden_tests/compile_file_o_all/list_merge_sort.hvm
 @If$C0 = (a (* a))
 @If$C1 = (* (a a))
 @Map = ({4 @Map$C0 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 a}} a)
-@Map$C0 = {4 a {4 {4 @Map$C0 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 (b c)}} ({5 (a d) b} {4 {4 d {4 c e}} {4 * e}})}}
+@Map$C0 = {4 a {4 {4 @Map$C0 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 (b c)}} ({7 (a d) b} {4 {4 d {4 c e}} {4 * e}})}}
 @Merge$C0 = {4 {9 a {9 b c}} {4 {11 d {4 @Merge$C0 {4 @Merge$C1 (e (f (g h)))}}} ({13 (i (a {2 @If$C0 {2 @If$C1 ({4 {4 j {4 k l}} {4 * l}} ({4 {4 c {4 h m}} {4 * m}} n))}})) {13 o e}} ({15 i {15 j f}} ({17 {4 @Merge$C2 {4 @Merge$C3 (o ({4 {4 b {4 d p}} {4 * p}} k))}} g} n)))}}
 @Merge$C1 = (* @Cons)
 @Merge$C2 = {4 a {4 b (c ({4 @Merge$C0 {4 @Merge$C1 (c (a (b d)))}} d))}}
 @Merge$C3 = (* (a a))
-@MergePair$C0 = {4 a {4 {4 @MergePair$C3 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 (b c)}} ({7 d b} ({4 @Merge$C2 {4 @Merge$C3 (d (a e))}} {4 {4 e {4 c f}} {4 * f}}))}}
+@MergePair$C0 = {4 a {4 {4 @MergePair$C3 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 (b c)}} ({5 d b} ({4 @Merge$C2 {4 @Merge$C3 (d (a e))}} {4 {4 e {4 c f}} {4 * f}}))}}
 @MergePair$C1 = (a {4 {4 a {4 @Nil b}} {4 * b}})
 @MergePair$C2 = (* @MergePair$C1)
 @MergePair$C3 = {4 a {4 {4 @MergePair$C0 {4 @MergePair$C2 (b (a c))}} (b c)}}
 @Nil = {4 * {4 a a}}
 @Pure = (a {4 {4 a {4 @Nil b}} {4 * b}})
 @Unpack = (a ({4 @Unpack$C2 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 (a b)}} b))
-@Unpack$C0 = {4 a {4 {4 @MergePair$C3 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 (b {4 @Unpack$C0 {4 @Unpack$C1 (c (d e))}})}} ({3 c {7 f b}} ({4 @Merge$C2 {4 @Merge$C3 (f (a d))}} e))}}
+@Unpack$C0 = {4 a {4 {4 @MergePair$C3 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 (b {4 @Unpack$C0 {4 @Unpack$C1 (c (d e))}})}} ({3 c {5 f b}} ({4 @Merge$C2 {4 @Merge$C3 (f (a d))}} e))}}
 @Unpack$C1 = (* (a a))
 @Unpack$C2 = {4 a {4 {4 @Unpack$C0 {4 @Unpack$C1 (b (a c))}} (b c)}}
 @Unpack$C3_$_MergePair$C4_$_Map$C1 = (* @Nil)

tests/snapshots/encode_pattern_match__common.hvm.snap

@@ -15,6 +15,10 @@ TaggedScott:
 
 (Yellow) = #Light λ* #Light λb #Light λ* b
 
+(Red) = #Light λa #Light λ* #Light λ* a
+
+(False) = #Bool λ* #Bool λb b
+
 (Filled) = λa #Box λb #Box λ* #Box (b a)
 
 (Empty) = #Box λ* #Box λb b
@@ -33,10 +37,6 @@ TaggedScott:
 
 (True) = #Bool λa #Bool λ* a
 
-(False) = #Bool λ* #Bool λb b
-
-(Red) = #Light λa #Light λ* #Light λ* a
-
 Scott:
 (West) = λ* λ* λ* λd d
 
@@ -50,6 +50,10 @@ Scott:
 
 (Yellow) = λ* λb λ* b
 
+(Red) = λa λ* λ* a
+
+(False) = λ* λb b
+
 (Filled) = λa λb λ* (b a)
 
 (Empty) = λ* λb b
@@ -67,7 +71,3 @@ Scott:
 (Nil) = λ* λb b
 
 (True) = λa λ* a
-
-(False) = λ* λb b
-
-(Red) = λa λ* λ* a

tests/snapshots/encode_pattern_match__expr.hvm.snap

@@ -15,6 +15,10 @@ TaggedScott:
 
 (Tup) = λa λb #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λj #Expr λ* #Expr (j a b)
 
+(Dup) = λa λb λc λd #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λk #Expr λ* #Expr λ* #Expr (k a b c d)
+
+(Let) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λi #Expr λ* #Expr λ* #Expr λ* #Expr (i a b c)
+
 (Var) = λa #Expr λb #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (b a)
 
 (Num) = λa #Expr λ* #Expr λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (c a)
@@ -25,10 +29,6 @@ TaggedScott:
 
 (If) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λh #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (h a b c)
 
-(Let) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λi #Expr λ* #Expr λ* #Expr λ* #Expr (i a b c)
-
-(Dup) = λa λb λc λd #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λk #Expr λ* #Expr λ* #Expr (k a b c d)
-
 Scott:
 (Div) = λ* λ* λ* λd d
 
@@ -42,6 +42,10 @@ Scott:
 
 (Tup) = λa λb λ* λ* λ* λ* λ* λ* λ* λj λ* (j a b)
 
+(Dup) = λa λb λc λd λ* λ* λ* λ* λ* λ* λk λ* λ* (k a b c d)
+
+(Let) = λa λb λc λ* λ* λ* λ* λ* λi λ* λ* λ* (i a b c)
+
 (Var) = λa λb λ* λ* λ* λ* λ* λ* λ* λ* (b a)
 
 (Num) = λa λ* λc λ* λ* λ* λ* λ* λ* λ* (c a)
@@ -51,7 +55,3 @@ Scott:
 (Fun) = λa λb λ* λ* λ* λf λ* λ* λ* λ* λ* (f a b)
 
 (If) = λa λb λc λ* λ* λ* λ* λh λ* λ* λ* λ* (h a b c)
-
-(Let) = λa λb λc λ* λ* λ* λ* λ* λi λ* λ* λ* (i a b c)
-
-(Dup) = λa λb λc λd λ* λ* λ* λ* λ* λ* λk λ* λ* (k a b c d)