From 0fc957ea6e55635dc2e066326488cfba03a34271 Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Tue, 27 Feb 2024 21:58:03 +0100 Subject: [PATCH 1/3] [sc-441] Add string patterns --- src/term/builtins.rs | 14 ++++++++++++-- src/term/check/ctrs_arities.rs | 2 +- src/term/check/unbound_pats.rs | 2 +- src/term/display.rs | 1 + src/term/mod.rs | 14 ++++++++------ src/term/parser/parser.rs | 15 ++++++++------- .../transform/desugar_implicit_match_binds.rs | 3 ++- src/term/transform/resolve_ctrs_in_pats.rs | 1 + tests/golden_tests/simplify_matches/match_str.hvm | 6 ++++++ .../snapshots/compile_file__missing_pat.hvm.snap | 2 +- .../simplify_matches__match_str.hvm.snap | 7 +++++++ 11 files changed, 48 insertions(+), 19 deletions(-) create mode 100644 tests/golden_tests/simplify_matches/match_str.hvm create mode 100644 tests/snapshots/simplify_matches__match_str.hvm.snap diff --git a/src/term/builtins.rs b/src/term/builtins.rs index 751aaaed0..30d52cbf4 100644 --- a/src/term/builtins.rs +++ b/src/term/builtins.rs @@ -1,4 +1,4 @@ -use super::{parser::parse_book, Book, Name, Pattern, Term}; +use super::{parser::parse_book, Book, Name, NumCtr, Pattern, Term}; const BUILTINS: &str = include_str!(concat!(env!("CARGO_MANIFEST_DIR"), "/src/term/builtins.hvm")); @@ -80,6 +80,7 @@ impl Pattern { pub fn encode_builtins(&mut self) { match self { Pattern::Lst(pats) => *self = Self::encode_list(std::mem::take(pats)), + Pattern::Str(str) => *self = Self::encode_str(str), Pattern::Ctr(_, pats) => { for pat in pats { pat.encode_builtins(); @@ -94,11 +95,20 @@ impl Pattern { } fn encode_list(elements: Vec) -> Pattern { - let lnil = Pattern::Var(Some(Name::from(LNIL))); + let lnil = Pattern::Ctr(Name::from(LNIL), vec![]); elements.into_iter().rfold(lnil, |acc, mut nxt| { nxt.encode_builtins(); Pattern::Ctr(Name::from(LCONS), vec![nxt, acc]) }) } + + fn encode_str(str: &str) -> Pattern { + let lnil = Pattern::Ctr(Name::from(LNIL), vec![]); + + str.chars().rfold(lnil, |tail, head| { + let head = Pattern::Num(NumCtr::Num(head as u64)); + Pattern::Ctr(Name::from(LCONS), vec![head, tail]) + }) + } } diff --git a/src/term/check/ctrs_arities.rs b/src/term/check/ctrs_arities.rs index ecbd327f4..153416f56 100644 --- a/src/term/check/ctrs_arities.rs +++ b/src/term/check/ctrs_arities.rs @@ -66,7 +66,7 @@ impl Pattern { to_check.push(el); } } - Pattern::Var(..) | Pattern::Num(..) => {} + Pattern::Var(..) | Pattern::Num(..) | Pattern::Str(_) => {} } } Ok(()) diff --git a/src/term/check/unbound_pats.rs b/src/term/check/unbound_pats.rs index 53e599fc7..a45db6c15 100644 --- a/src/term/check/unbound_pats.rs +++ b/src/term/check/unbound_pats.rs @@ -58,7 +58,7 @@ impl Pattern { check.push(snd); } Pattern::Lst(args) => args.iter().for_each(|arg| check.push(arg)), - Pattern::Var(_) | Pattern::Num(_) => {} + Pattern::Var(_) | Pattern::Num(_) | Pattern::Str(_) => {} } } unbounds diff --git a/src/term/display.rs b/src/term/display.rs index 8071542ef..e61376491 100644 --- a/src/term/display.rs +++ b/src/term/display.rs @@ -111,6 +111,7 @@ impl fmt::Display for Pattern { Pattern::Num(num) => write!(f, "{num}"), Pattern::Tup(fst, snd) => write!(f, "({}, {})", fst, snd,), Pattern::Lst(pats) => write!(f, "[{}]", DisplayJoin(|| pats, ", ")), + Pattern::Str(str) => write!(f, "\"{str}\""), } } } diff --git a/src/term/mod.rs b/src/term/mod.rs index 6f60c28ce..3665dc0b4 100644 --- a/src/term/mod.rs +++ b/src/term/mod.rs @@ -147,6 +147,7 @@ pub enum Pattern { Num(NumCtr), Tup(Box, Box), Lst(Vec), + Str(GlobalString), } #[derive(Debug, Clone, PartialEq, Eq, Hash)] @@ -640,6 +641,7 @@ impl Pattern { set.push(nam); } Pattern::Num(_) => {} + Pattern::Str(_) => {} } } let mut set = Vec::new(); @@ -664,6 +666,7 @@ impl Pattern { Pattern::Num(_) => Box::new([].iter()), Pattern::Tup(fst, snd) => Box::new([fst.as_ref(), snd.as_ref()].into_iter()), Pattern::Lst(els) => Box::new(els.iter()), + Pattern::Str(_) => Box::new([].iter()), } } @@ -687,6 +690,7 @@ impl Pattern { Pattern::Num(NumCtr::Succ(num, _)) => Some(Name::new(format!("{num}+"))), Pattern::Tup(_, _) => Some(Name::new("(,)")), Pattern::Lst(_) => todo!(), + Pattern::Str(_) => todo!(), } } @@ -702,11 +706,12 @@ impl Pattern { pub fn is_simple(&self) -> bool { match self { Pattern::Var(_) => true, - Pattern::Ctr(_, args) | Pattern::Lst(args) => args.iter().all(|arg| matches!(arg, Pattern::Var(_))), + Pattern::Ctr(_, args) => args.iter().all(|arg| matches!(arg, Pattern::Var(_))), Pattern::Num(_) => true, Pattern::Tup(fst, snd) => { matches!(fst.as_ref(), Pattern::Var(_)) && matches!(snd.as_ref(), Pattern::Var(_)) } + Pattern::Lst(_) | Pattern::Str(_) => todo!(), } } @@ -721,6 +726,7 @@ impl Pattern { Pattern::Num(NumCtr::Num(_)) => Type::Num, Pattern::Num(NumCtr::Succ(n, _)) => Type::NumSucc(*n), Pattern::Lst(..) => Type::Adt(builtins::LIST.into()), + Pattern::Str(..) => Type::Adt(builtins::STRING.into()), } } @@ -736,11 +742,7 @@ impl Pattern { Pattern::Num(NumCtr::Succ(val, Some(Some(nam)))) => Term::add_num(Term::Var { nam: nam.clone() }, *val), Pattern::Num(NumCtr::Succ(_, Some(None))) => Term::Era, Pattern::Tup(fst, snd) => Term::Tup { fst: Box::new(fst.to_term()), snd: Box::new(snd.to_term()) }, - Pattern::Lst(_) => { - let mut p = self.clone(); - p.encode_builtins(); - p.to_term() - } + Pattern::Lst(_) | Pattern::Str(_) => todo!(), } } diff --git a/src/term/parser/parser.rs b/src/term/parser/parser.rs index 6eae0d173..5a7ad56fc 100644 --- a/src/term/parser/parser.rs +++ b/src/term/parser/parser.rs @@ -405,26 +405,27 @@ where .map(Pattern::Lst) .boxed(); - let num = any() + let num_val = any() .filter(|t| matches!(t, Token::Num(_))) .map(|t| { let Token::Num(n) = t else { unreachable!() }; n - }) - .labelled(""); + }); - let num_pat = num.map(|n| Pattern::Num(NumCtr::Num(n))); + let num = num_val.map(|n| Pattern::Num(NumCtr::Num(n))).labelled(""); - let succ_pat = num + let succ = num_val .then_ignore(just(Token::Add)) .then(name_or_era().or_not()) .map(|(num, nam)| Pattern::Num(NumCtr::Succ(num, nam))) .labelled("+") .boxed(); - let chr_pat = select!(Token::Char(c) => Pattern::Num(NumCtr::Num(c))).labelled("").boxed(); + let chr = select!(Token::Char(c) => Pattern::Num(NumCtr::Num(c))).labelled("").boxed(); + + let str = select!(Token::Str(s) => Pattern::Str(s)).labelled("").boxed(); - choice((succ_pat, num_pat, chr_pat, var, ctr, list, tup)) + choice((succ, num, chr, str, var, ctr, list, tup)) }) } diff --git a/src/term/transform/desugar_implicit_match_binds.rs b/src/term/transform/desugar_implicit_match_binds.rs index 9d6d929be..46b1f20e7 100644 --- a/src/term/transform/desugar_implicit_match_binds.rs +++ b/src/term/transform/desugar_implicit_match_binds.rs @@ -52,7 +52,8 @@ impl Term { *p = Some(Some(Name::new(format!("{nam}-{n}")))); } Pattern::Tup(_, _) => (), - Pattern::Lst(..) => unreachable!(), + Pattern::Lst(..) => (), + Pattern::Str(..) => (), } } } diff --git a/src/term/transform/resolve_ctrs_in_pats.rs b/src/term/transform/resolve_ctrs_in_pats.rs index 7ba73650f..9b62d865f 100644 --- a/src/term/transform/resolve_ctrs_in_pats.rs +++ b/src/term/transform/resolve_ctrs_in_pats.rs @@ -36,6 +36,7 @@ impl Pattern { } Pattern::Var(None) => (), Pattern::Num(_) => (), + Pattern::Str(_) => (), Pattern::Tup(fst, snd) => { to_resolve.push(fst); to_resolve.push(snd); diff --git a/tests/golden_tests/simplify_matches/match_str.hvm b/tests/golden_tests/simplify_matches/match_str.hvm new file mode 100644 index 000000000..c92404122 --- /dev/null +++ b/tests/golden_tests/simplify_matches/match_str.hvm @@ -0,0 +1,6 @@ +(is_as "As") = 2 +(is_as "as") = 2 +(is_as "") = 1 +(is_as *) = 0 + +main = * \ No newline at end of file diff --git a/tests/snapshots/compile_file__missing_pat.hvm.snap b/tests/snapshots/compile_file__missing_pat.hvm.snap index e9780f8dc..93fd5db35 100644 --- a/tests/snapshots/compile_file__missing_pat.hvm.snap +++ b/tests/snapshots/compile_file__missing_pat.hvm.snap @@ -2,5 +2,5 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/compile_file/missing_pat.hvm --- -At tests/golden_tests/compile_file/missing_pat.hvm:2:3: found ':' expected '(', '#', '$', , '[', '{', 'λ', 'let', 'match', '*', '|', +, , or +At tests/golden_tests/compile_file/missing_pat.hvm:2:3: found ':' expected '(', '#', '$', , '[', '{', 'λ', 'let', 'match', '*', '|', +, , , or  2 | : * diff --git a/tests/snapshots/simplify_matches__match_str.hvm.snap b/tests/snapshots/simplify_matches__match_str.hvm.snap new file mode 100644 index 000000000..6ba1af670 --- /dev/null +++ b/tests/snapshots/simplify_matches__match_str.hvm.snap @@ -0,0 +1,7 @@ +--- +source: tests/golden_tests.rs +input_file: tests/golden_tests/simplify_matches/match_str.hvm +--- +(is_as) = λa match a { (List.cons b c): (match b { 65: λd (match d { (List.cons f g): λh (match f { 115: λ* λj (match j { (List.cons * *): λ* 0; (List.nil): λ* 2 } *); *: λ* λ* 0 } h g); (List.nil): λ* 0 } *); 97: λhb (match hb { (List.cons jb kb): λlb (match jb { 115: λ* λnb (match nb { (List.cons * *): λ* 0; (List.nil): λ* 2 } *); *: λ* λ* 0 } lb kb); (List.nil): λ* 0 } *); *: λ* 0 } c); (List.nil): 1 } + +(main) = * From 7b859fc41e29d4eaddffc435e7b9f7d384e687ac Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Tue, 27 Feb 2024 22:01:08 +0100 Subject: [PATCH 2/3] [sc-441] Fix CI warnings --- cspell.json | 1 + src/term/parser/parser.rs | 10 ++++------ 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/cspell.json b/cspell.json index fca40f4d3..7bd1f52e8 100644 --- a/cspell.json +++ b/cspell.json @@ -42,6 +42,7 @@ "namegen", "nams", "numop", + "nums", "oper", "opre", "oprune", diff --git a/src/term/parser/parser.rs b/src/term/parser/parser.rs index 5a7ad56fc..6c728f7cf 100644 --- a/src/term/parser/parser.rs +++ b/src/term/parser/parser.rs @@ -405,12 +405,10 @@ where .map(Pattern::Lst) .boxed(); - let num_val = any() - .filter(|t| matches!(t, Token::Num(_))) - .map(|t| { - let Token::Num(n) = t else { unreachable!() }; - n - }); + let num_val = any().filter(|t| matches!(t, Token::Num(_))).map(|t| { + let Token::Num(n) = t else { unreachable!() }; + n + }); let num = num_val.map(|n| Pattern::Num(NumCtr::Num(n))).labelled(""); From fb8f3fefc77bbbcfa86df2844460aa6525b734b6 Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Wed, 28 Feb 2024 13:09:00 +0100 Subject: [PATCH 3/3] [sc-441] Fix encoding of string patterns --- src/term/builtins.rs | 4 ++-- tests/golden_tests/run_file/match_str.hvm | 9 +++++++++ tests/snapshots/run_file__match_str.hvm.snap | 5 +++++ tests/snapshots/simplify_matches__match_str.hvm.snap | 2 +- 4 files changed, 17 insertions(+), 3 deletions(-) create mode 100644 tests/golden_tests/run_file/match_str.hvm create mode 100644 tests/snapshots/run_file__match_str.hvm.snap diff --git a/src/term/builtins.rs b/src/term/builtins.rs index 30d52cbf4..112187ecb 100644 --- a/src/term/builtins.rs +++ b/src/term/builtins.rs @@ -104,11 +104,11 @@ impl Pattern { } fn encode_str(str: &str) -> Pattern { - let lnil = Pattern::Ctr(Name::from(LNIL), vec![]); + let lnil = Pattern::Ctr(Name::from(SNIL), vec![]); str.chars().rfold(lnil, |tail, head| { let head = Pattern::Num(NumCtr::Num(head as u64)); - Pattern::Ctr(Name::from(LCONS), vec![head, tail]) + Pattern::Ctr(Name::from(SCONS), vec![head, tail]) }) } } diff --git a/tests/golden_tests/run_file/match_str.hvm b/tests/golden_tests/run_file/match_str.hvm new file mode 100644 index 000000000..ff1255163 --- /dev/null +++ b/tests/golden_tests/run_file/match_str.hvm @@ -0,0 +1,9 @@ +(is_as "As") = 2 +(is_as "as") = 2 +(is_as "") = 1 +(is_as *) = 0 + +map f (List.cons x xs) = (List.cons (f x) (map f xs)) +map f [] = [] + +main = (map is_as ["As" "as" "" "Asd" "qwerty" "AAs"]) \ No newline at end of file diff --git a/tests/snapshots/run_file__match_str.hvm.snap b/tests/snapshots/run_file__match_str.hvm.snap new file mode 100644 index 000000000..984f5b323 --- /dev/null +++ b/tests/snapshots/run_file__match_str.hvm.snap @@ -0,0 +1,5 @@ +--- +source: tests/golden_tests.rs +input_file: tests/golden_tests/run_file/match_str.hvm +--- +[2, 2, 1, 0, 0, 0] diff --git a/tests/snapshots/simplify_matches__match_str.hvm.snap b/tests/snapshots/simplify_matches__match_str.hvm.snap index 6ba1af670..a88f78f14 100644 --- a/tests/snapshots/simplify_matches__match_str.hvm.snap +++ b/tests/snapshots/simplify_matches__match_str.hvm.snap @@ -2,6 +2,6 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/simplify_matches/match_str.hvm --- -(is_as) = λa match a { (List.cons b c): (match b { 65: λd (match d { (List.cons f g): λh (match f { 115: λ* λj (match j { (List.cons * *): λ* 0; (List.nil): λ* 2 } *); *: λ* λ* 0 } h g); (List.nil): λ* 0 } *); 97: λhb (match hb { (List.cons jb kb): λlb (match jb { 115: λ* λnb (match nb { (List.cons * *): λ* 0; (List.nil): λ* 2 } *); *: λ* λ* 0 } lb kb); (List.nil): λ* 0 } *); *: λ* 0 } c); (List.nil): 1 } +(is_as) = λa match a { (String.cons b c): (match b { 65: λd (match d { (String.cons f g): λh (match f { 115: λ* λj (match j { (String.cons * *): λ* 0; (String.nil): λ* 2 } *); *: λ* λ* 0 } h g); (String.nil): λ* 0 } *); 97: λhb (match hb { (String.cons jb kb): λlb (match jb { 115: λ* λnb (match nb { (String.cons * *): λ* 0; (String.nil): λ* 2 } *); *: λ* λ* 0 } lb kb); (String.nil): λ* 0 } *); *: λ* 0 } c); (String.nil): 1 } (main) = *