Merge pull request #118 from HigherOrderCO/feature/sc-196/add-n-tuples-to-hvm-lang

[sc-196] Add n-tuples to hvm-lang
This commit is contained in:
Nicolas Abril 2024-01-16 18:16:33 +01:00 committed by GitHub
commit ca987568ca
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 109 additions and 12 deletions

View File

@ -176,15 +176,6 @@ where
})
.boxed();
// (x, y)
let tup = term
.clone()
.then_ignore(just(Token::Comma))
.then(term.clone())
.delimited_by(just(Token::LParen), just(Token::RParen))
.map(|(fst, snd)| Term::Tup { fst: Box::new(fst), snd: Box::new(snd) })
.boxed();
// let a = ...
// let (a, b) = ...
let let_ = just(Token::Let)
@ -256,6 +247,16 @@ where
.map(|((op, fst), snd)| Term::Opx { op, fst: Box::new(fst), snd: Box::new(snd) })
.boxed();
// (x, ..n)
let tup = term
.clone()
.separated_by(just(Token::Comma))
.at_least(2)
.collect::<Vec<Term>>()
.map(|xs| make_tup_tree(&xs, |a, b| Term::Tup { fst: Box::new(a), snd: Box::new(b) }))
.delimited_by(just(Token::LParen), just(Token::RParen))
.boxed();
let str = select!(Token::Str(s) => Term::Str { val: s }).boxed();
let chr = select!(Token::Char(c) => Term::Num { val: c }).boxed();
@ -281,6 +282,18 @@ where
})
}
fn make_tup_tree<A: Clone>(xs: &[A], make: fn(A, A) -> A) -> A {
match xs {
[] => unreachable!(),
[x] => x.clone(),
xs => {
let half = xs.len() / 2;
let (x, y) = xs.split_at(half);
make(make_tup_tree(x, make), make_tup_tree(y, make))
}
}
}
fn pattern<'a, I>() -> impl Parser<'a, I, Pattern, extra::Err<Rich<'a, Token>>>
where
I: ValueInput<'a, Token = Token, Span = SimpleSpan>,
@ -296,10 +309,11 @@ where
let tup = pattern
.clone()
.then_ignore(just(Token::Comma))
.then(pattern.clone())
.separated_by(just(Token::Comma))
.at_least(2)
.collect::<Vec<Pattern>>()
.delimited_by(just(Token::LParen), just(Token::RParen))
.map(|(fst, snd)| Pattern::Tup(Box::new(fst), Box::new(snd)))
.map(|xs| make_tup_tree(&xs, |a, b| Pattern::Tup(Box::new(a), Box::new(b))))
.boxed();
let zero = select!(Token::Num(0) => Pattern::Num(MatchNum::Zero));

View File

@ -0,0 +1,6 @@
data Bool = T | F
And (T, T, T) = T
And * = F
main = (And (F, T, F))

View File

@ -0,0 +1,3 @@
ntupSum (a, b, c, d, e) = (+ a (+ b (+ c (+ d e))))
main = (ntupSum (1, 3, 3, 2, 1))

View File

@ -0,0 +1,43 @@
---
source: tests/golden_tests.rs
input_file: tests/golden_tests/encode_pattern_match/and3.hvm
---
(And) = λx (And$P x)
(main) = (And (F, (T, F)))
(T) = #Bool λT #Bool λF T
(F) = #Bool λT #Bool λF F
(And$F0) = λx #Bool (x And$F0$PT And$F0$PF)
(And$F0$F0) = λx #Bool (x And$F0$F0$PT And$F0$F0$PF)
(And$R0) = λ%0 let (x$0, x$1) = %0; (And$F0 x$0 x$1)
(And$R1) = λ* F
(And$P) = λy0 (And$R0 y0)
(And$F0$R0) = λ%0 let (x$0, x$1) = %0; (And$F0$F0 x$0 x$1)
(And$F0$R1) = λ* λ* F
(And$F0$PT$P) = λy0 (And$F0$R0 y0)
(And$F0$PT) = λx (And$F0$PT$P x)
(And$F0$PF) = (And$F0$R1 *)
(And$F0$F0$R0) = T
(And$F0$F0$R1) = λ* λ* F
(And$F0$F0$PT$PT) = And$F0$F0$R0
(And$F0$F0$PT$PF) = (And$F0$F0$R1 * *)
(And$F0$F0$PT) = λx #Bool (x And$F0$F0$PT$PT And$F0$F0$PT$PF)
(And$F0$F0$PF) = (And$F0$F0$R1 *)

View File

@ -0,0 +1,31 @@
---
source: tests/golden_tests.rs
input_file: tests/golden_tests/encode_pattern_match/ntup_sum.hvm
---
(ntupSum) = λx (ntupSum$P x)
(main) = (ntupSum ((1, 3), (3, (2, 1))))
(ntupSum$F0) = λx (ntupSum$F0$P x)
(ntupSum$F0$F0) = λx (ntupSum$F0$F0$P x)
(ntupSum$R0) = λ%0 let (x$0, x$1) = %0; (ntupSum$F0 x$0 x$1)
(ntupSum$P) = λy0 (ntupSum$R0 y0)
(ntupSum$F0$R0) = λ%0 let (x$0, x$1) = %0; λ%0 let (x$2, x$3) = %0; (ntupSum$F0$F0 x$0 x$1 x$2 x$3)
(ntupSum$F0$P$P) = λy0 λx0 (ntupSum$F0$R0 x0 y0)
(ntupSum$F0$P) = λy0 λx (ntupSum$F0$P$P x y0)
(ntupSum$F0$F0$R0) = λa λb λc λ%0 let (d, e) = %0; (+ a (+ b (+ c (+ d e))))
(ntupSum$F0$F0$P$P$P$P) = λy0 λx0 λx1 λx2 (ntupSum$F0$F0$R0 x0 x1 x2 y0)
(ntupSum$F0$F0$P$P$P) = λy0 λx0 λx1 λx (ntupSum$F0$F0$P$P$P$P x x0 x1 y0)
(ntupSum$F0$F0$P$P) = λy0 λx0 λx (ntupSum$F0$F0$P$P$P x x0 y0)
(ntupSum$F0$F0$P) = λy0 λx (ntupSum$F0$F0$P$P x y0)