Add builtin and syntax sugar for Nats

This commit is contained in:
imaqtkatt 2024-03-18 16:37:56 -03:00
parent 13f08ea26b
commit cf69b99e5a
18 changed files with 110 additions and 39 deletions

View File

@ -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 Nat = (Nat.succ pred) | (Nat.zero)

View File

@ -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])
}

View File

@ -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)

View File

@ -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

View File

@ -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 => {}
}
}

View File

@ -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,
))
})

View File

@ -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() });

View File

@ -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!(),
})
}

View File

@ -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();
}
}
}
});
}
}

View File

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

View File

@ -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)

View File

@ -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))))

View File

@ -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)

View File

@ -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

View File

@ -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)

View File

@ -0,0 +1,9 @@
---
source: tests/golden_tests.rs
input_file: tests/golden_tests/run_file/nat_add.hvm
---
Lazy mode:
#34
Strict mode:
#34

View File

@ -26,8 +26,8 @@ input_file: tests/golden_tests/simplify_matches/already_flat.hvm
(CtrA2) = λa λb #Bar λ* #Bar λd #Bar λ* #Bar (d a b)
(CtrA) = #Foo λa #Foo λ* a
(CtrA1) = λa #Bar λb #Bar λ* #Bar λ* #Bar (b a)
(CtrB) = λa #Foo λ* #Foo λc #Foo (c a)
(CtrA1) = λa #Bar λb #Bar λ* #Bar λ* #Bar (b a)
(CtrA) = #Foo λa #Foo λ* a