HigherOrderCO/Bend
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Bend.git synced 2024-11-05 04:51:40 +03:00
Code Issues Packages Projects Releases Wiki Activity

[sc-301] Some small improvements on mathing code

Browse Source
This commit is contained in:
Nicolas Abril 2024-02-27 19:35:19 +01:00
parent 4c8a9f915e
commit 0c509b4367
10 changed files with 31 additions and 81 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
src/term/mod.rs
View File

@ -298,9 +298,9 @@ impl Term {
Term::Str { val: STRINGS.get(str) }
}
pub fn native_num_match(arg: Term, zero: Term, succ: Term) -> Term {
pub fn native_num_match(arg: Term, zero: Term, succ: Term, succ_var: Option<Option<Name>>) -> Term {
let zero = Rule { pats: vec![Pattern::Num(NumCtr::Num(0))], body: zero };
let succ = Rule { pats: vec![Pattern::Num(NumCtr::Succ(1, None))], body: succ };
let succ = Rule { pats: vec![Pattern::Num(NumCtr::Succ(1, succ_var))], body: succ };
Term::Mat { args: vec![arg], rules: vec![zero, succ] }
}
@ -695,16 +695,7 @@ impl Pattern {
}
pub fn is_native_num_match(&self) -> bool {
if let Pattern::Num(ctr) = self {
match ctr {
NumCtr::Num(0) => true,
NumCtr::Num(_) => false,
NumCtr::Succ(1, None) => true,
NumCtr::Succ(_, _) => false,
}
} else {
false
}
matches!(self, Pattern::Num(NumCtr::Num(0) | NumCtr::Succ(1, _)))
}
/// True if this pattern has no nested subpatterns.
@ -758,9 +749,7 @@ impl Pattern {
match (self, other) {
(Pattern::Ctr(a, _), Pattern::Ctr(b, _)) if a == b => true,
(Pattern::Num(NumCtr::Num(a)), Pattern::Num(NumCtr::Num(b))) if a == b => true,
(Pattern::Num(NumCtr::Num(_)), Pattern::Num(NumCtr::Num(_))) => false,
(Pattern::Num(NumCtr::Succ(a, _)), Pattern::Num(NumCtr::Succ(b, _))) if a == b => true,
(Pattern::Num(NumCtr::Succ(_, _)), Pattern::Num(NumCtr::Succ(_, _))) => false,
(Pattern::Tup(_, _), Pattern::Tup(_, _)) => true,
(Pattern::Lst(_), Pattern::Lst(_)) => true,
(Pattern::Var(_), Pattern::Var(_)) => true,

49
src/term/net_to_term.rs
View File

@ -1,7 +1,6 @@
use super::Rule;
use crate::{
net::{INet, NodeId, NodeKind::*, Port, SlotId, ROOT},
term::{num_to_name, term_to_net::Labels, Book, Name, NumCtr, Op, Pattern, Tag, Term},
term::{num_to_name, term_to_net::Labels, Book, Name, Op, Pattern, Tag, Term},
};
use std::collections::{BTreeSet, HashMap, HashSet};
@ -103,16 +102,16 @@ impl<'a> Reader<'a> {
if *sel_kind != (Con { lab: None }) {
// TODO: Is there any case where we expect a different node type here on readback?
self.error(ReadbackError::InvalidNumericMatch);
Term::new_native_match(scrutinee, Term::Era, None, Term::Era)
Term::native_num_match(scrutinee, Term::Era, Term::Era, None)
} else {
let zero_term = self.read_term(self.net.enter_port(Port(sel_node, 1)));
let succ_term = self.read_term(self.net.enter_port(Port(sel_node, 2)));
match succ_term {
Term::Lam { nam, bod, .. } => Term::new_native_match(scrutinee, zero_term, nam, *bod),
Term::Lam { nam, bod, .. } => Term::native_num_match(scrutinee, zero_term, *bod, Some(nam)),
_ => {
self.error(ReadbackError::InvalidNumericMatch);
Term::new_native_match(scrutinee, zero_term, None, succ_term)
Term::native_num_match(scrutinee, zero_term, succ_term, None)
}
}
}
@ -392,46 +391,6 @@ impl Term {
Term::Var { .. } | Term::Lnk { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era | Term::Err => {}
}
}
/// Creates a new [`Term::Match`] from the given terms.
/// If `scrutinee` is not a `Term::Var`, creates a let binding containing the match in its body
fn new_native_match(arg: Self, zero_term: Self, mut succ_label: Option<Name>, mut succ_term: Self) -> Self {
let zero = Rule { pats: vec![Pattern::Num(NumCtr::Num(0))], body: zero_term };
if let Term::Var { nam } = &arg {
if let Some(label) = &succ_label {
let new_label = Name::new(format!("{}-1", nam));
succ_term.subst(label, &Term::Var { nam: new_label.clone() });
succ_label = Some(new_label);
}
let succ = Rule { pats: vec![Pattern::Num(NumCtr::Succ(1, Some(succ_label)))], body: succ_term };
Term::Mat { args: vec![arg], rules: vec![zero, succ] }
} else {
match succ_label {
Some(succ) => {
let match_bind = succ.clone();
let new_label = Name::new(format!("{}-1", succ));
succ_term.subst(&succ, &Term::Var { nam: new_label.clone() });
succ_label = Some(new_label);
let succ = Rule { pats: vec![Pattern::Num(NumCtr::Succ(1, Some(succ_label)))], body: succ_term };
Term::Let {
pat: Pattern::Var(Some(match_bind.clone())),
val: Box::new(arg),
nxt: Box::new(Term::Mat { args: vec![Term::Var { nam: match_bind }], rules: vec![zero, succ] }),
}
}
None => {
let succ = Rule { pats: vec![Pattern::Num(NumCtr::Succ(1, None))], body: succ_term };
Term::Mat { args: vec![arg], rules: vec![zero, succ] }
}
}
}
}
}
#[derive(Default)]

2
src/term/transform/encode_pattern_matching.rs
View File

@ -134,6 +134,7 @@ fn encode_num(arg: Term, mut rules: Vec<Rule>) -> Term {
Term::sub_num(arg.unwrap(), *val),
rule.body,
go(rules, last_rule, Some(*val), None),
None,
)
}
// Middle match
@ -147,6 +148,7 @@ fn encode_num(arg: Term, mut rules: Vec<Rule>) -> Term {
Term::sub_num(Term::Var { nam: pred_nam }, val.wrapping_sub(prev_num).wrapping_sub(1)),
rule.body,
go(rules, last_rule, Some(*val), None),
None,
),
)
}

32
src/term/transform/eta_reduction.rs
View File

@ -37,34 +37,34 @@ impl Term {
_ => {}
}
}
Term::Lam { bod, .. } => bod.eta_reduction(),
Term::Let { pat: _, val, nxt } | Term::Dup { tag: _, fst: _, snd: _, val, nxt } => {
val.eta_reduction();
nxt.eta_reduction();
}
Term::App { fun: fst, arg: snd, .. }
| Term::Tup { fst, snd }
| Term::Sup { fst, snd, .. }
| Term::Opx { op: _, fst, snd } => {
fst.eta_reduction();
snd.eta_reduction();
}
Term::Lam { tag: _, nam: None, bod } => bod.eta_reduction(),
Term::Mat { args, rules } => {
for arg in args {
arg.eta_reduction();
}
for rule in rules {
for pat in &rule.pats {
debug_assert!(pat.is_native_num_match());
}
rule.body.eta_reduction();
}
}
Term::Lst { els } => {
for el in els {
el.eta_reduction();
}
}
Term::Let { val: fst, nxt: snd, .. }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::App { fun: fst, arg: snd, .. }
| Term::Tup { fst, snd }
| Term::Sup { fst, snd, .. }
| Term::Opx { fst, snd, .. } => {
fst.eta_reduction();
snd.eta_reduction();
}
Term::Lnk { .. }
| Term::Var { .. }
| Term::Num { .. }
| Term::Str { .. }
| Term::Lst { .. }
| Term::Ref { .. }
| Term::Era
| Term::Err => {}

2
tests/snapshots/readback_lnet__invalid_mat_mat.hvm.snap
View File

@ -5,4 +5,4 @@ input_file: tests/golden_tests/readback_lnet/invalid_mat_mat.hvm
Readback Warning:
Invalid Numeric Match (4 occurrences)
λa match match <Invalid> { 0: 3; 1+: 4 } { 0: <Invalid>; 1+: <Invalid> }
λa match match <Invalid> { 0: 3; 1+*: 4 } { 0: <Invalid>; 1+: <Invalid> }

2
tests/snapshots/readback_lnet__match.hvm.snap
View File

@ -2,4 +2,4 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/readback_lnet/match.hvm
---
let b = 1; match b { 0: λa a; 1+b-1: b-1 }
match 1 { 0: λa a; 1+b: b }

2
tests/snapshots/run_file__linearize_match.hvm.snap
View File

@ -2,4 +2,4 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/run_file/linearize_match.hvm
---
λa match a { 0: λb b; 1+a-1: λd (+ a-1 d) }
λa match a { 0: λb b; 1+c: λd (+ c d) }

2
tests/snapshots/run_file__match_mult_linearization.hvm.snap
View File

@ -2,4 +2,4 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/run_file/match_mult_linearization.hvm
---
λa match a { 0: λb λc λd (+ (+ b c) d); 1+a-1: λf λg λh (+ (+ (+ a-1 f) g) h) }
λa match a { 0: λb λc λd (+ (+ b c) d); 1+e: λf λg λh (+ (+ (+ e f) g) h) }

2
tests/snapshots/run_lazy__linearize_match.hvm.snap
View File

@ -2,4 +2,4 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/run_lazy/linearize_match.hvm
---
λa match a { 0: λb b; 1+a-1: λd (+ a-1 d) }
λa match a { 0: λb b; 1+c: λd (+ c d) }

2
tests/snapshots/run_lazy__match_mult_linearization.hvm.snap
View File

@ -2,4 +2,4 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/run_lazy/match_mult_linearization.hvm
---
λa match a { 0: λb λc λd (+ (+ b c) d); 1+a-1: λf λg λh (+ (+ (+ a-1 f) g) h) }
λa match a { 0: λb λc λd (+ (+ b c) d); 1+e: λf λg λh (+ (+ (+ e f) g) h) }