Skip to content

Commit 7003365

Browse files
KmeakinKmeakin
committed
asdf
1 parent 82a70b9 commit 7003365

File tree

2 files changed

+64
-103
lines changed

2 files changed

+64
-103
lines changed

‎fathom/src/surface/elaboration.rs

Lines changed: 62 additions & 99 deletions
Original file line numberDiff line numberDiff line change
@@ -798,51 +798,24 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
798798
match (surface_term, expected_type.as_ref()) {
799799
(Term::Let(range, def_pattern, def_type, def_expr, body_expr), _) => {
800800
let (def_pattern, def_type_value) = self.synth_ann_pattern(def_pattern, *def_type);
801-
let mut scrut = self.check_scrutinee(def_expr, def_type_value.clone());
801+
let scrut = self.check_scrutinee(def_expr, def_type_value.clone());
802802
let value = self.eval_env().eval(scrut.expr);
803-
804-
// Bind the scrut to a fresh variable if it is unsafe to evaluate multiple times,
805-
// and may be evaluated multiple times by the pattern match compiler
806-
let extra_def = match (scrut.expr.is_atomic(), def_pattern.is_atomic()) {
807-
(false, false) => {
808-
let def_name = None; // TODO: generate a fresh name
809-
let def_type = self.quote_env().quote(self.scope, &scrut.r#type);
810-
let def_expr = scrut.expr.clone();
811-
812-
let var = core::Term::LocalVar(def_expr.span(), env::Index::last());
813-
scrut.expr = self.scope.to_scope(var);
814-
(self.local_env).push_def(def_name, value.clone(), scrut.r#type.clone());
815-
Some((def_name, def_type, def_expr))
816-
}
817-
_ => None,
818-
};
803+
let (scrut, extra_def) =
804+
self.freshen_scrutinee(scrut, &value, &[def_pattern.clone()]);
819805

820806
let initial_len = self.local_env.len();
821807
let defs = self.push_local_def(&def_pattern, scrut.clone(), value);
822808
let body_expr = self.check(body_expr, &expected_type);
823809
self.local_env.truncate(initial_len);
824810

825811
let matrix = PatMatrix::singleton(scrut, def_pattern);
826-
let expr = self.elab_match(
812+
let body = self.elab_match(
827813
matrix,
828814
&[Body::new(body_expr, defs)],
829815
*range,
830816
def_expr.range(),
831817
);
832-
let expr = match extra_def {
833-
None => expr,
834-
Some((def_name, def_type, def_expr)) => {
835-
self.local_env.pop();
836-
core::Term::Let(
837-
range.into(),
838-
def_name,
839-
self.scope.to_scope(def_type),
840-
self.scope.to_scope(def_expr),
841-
self.scope.to_scope(expr),
842-
)
843-
}
844-
};
845-
expr
818+
self.bind_scrutinee(*range, body, extra_def)
846819
}
847820
(Term::If(range, cond_expr, then_expr, else_expr), _) => {
848821
let cond_expr = self.check(cond_expr, &self.bool_type.clone());
@@ -1134,51 +1107,25 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
11341107
}
11351108
Term::Let(range, def_pattern, def_type, def_expr, body_expr) => {
11361109
let (def_pattern, def_type_value) = self.synth_ann_pattern(def_pattern, *def_type);
1137-
let mut scrut = self.check_scrutinee(def_expr, def_type_value.clone());
1110+
let scrut = self.check_scrutinee(def_expr, def_type_value.clone());
11381111
let value = self.eval_env().eval(scrut.expr);
1139-
1140-
// Bind the scrut to a fresh variable if it is unsafe to evaluate multiple times,
1141-
// and may be evaluated multiple times by the pattern match compiler
1142-
let extra_def = match (scrut.expr.is_atomic(), def_pattern.is_atomic()) {
1143-
(false, false) => {
1144-
let def_name = None; // TODO: generate a fresh name
1145-
let def_type = self.quote_env().quote(self.scope, &scrut.r#type);
1146-
let def_expr = scrut.expr.clone();
1147-
1148-
let var = core::Term::LocalVar(def_expr.span(), env::Index::last());
1149-
scrut.expr = self.scope.to_scope(var);
1150-
(self.local_env).push_def(def_name, value.clone(), scrut.r#type.clone());
1151-
Some((def_name, def_type, def_expr))
1152-
}
1153-
_ => None,
1154-
};
1112+
let (scrut, extra_def) =
1113+
self.freshen_scrutinee(scrut, &value, &[def_pattern.clone()]);
11551114

11561115
let initial_len = self.local_env.len();
11571116
let defs = self.push_local_def(&def_pattern, scrut.clone(), value);
11581117
let (body_expr, body_type) = self.synth(body_expr);
11591118
self.local_env.truncate(initial_len);
11601119

11611120
let matrix = patterns::PatMatrix::singleton(scrut, def_pattern);
1162-
let expr = self.elab_match(
1121+
let body = self.elab_match(
11631122
matrix,
11641123
&[Body::new(body_expr, defs)],
11651124
*range,
11661125
def_expr.range(),
11671126
);
1168-
let expr = match extra_def {
1169-
None => expr,
1170-
Some((def_name, def_type, def_expr)) => {
1171-
self.local_env.pop();
1172-
core::Term::Let(
1173-
range.into(),
1174-
def_name,
1175-
self.scope.to_scope(def_type),
1176-
self.scope.to_scope(def_expr),
1177-
self.scope.to_scope(expr),
1178-
)
1179-
}
1180-
};
1181-
(expr, body_type)
1127+
let let_expr = self.bind_scrutinee(*range, body, extra_def);
1128+
(let_expr, body_type)
11821129
}
11831130
Term::If(range, cond_expr, then_expr, else_expr) => {
11841131
let cond_expr = self.check(cond_expr, &self.bool_type.clone());
@@ -1871,32 +1818,14 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
18711818
expected_type: &ArcValue<'arena>,
18721819
) -> core::Term<'arena> {
18731820
let expected_type = self.elim_env().force(expected_type);
1874-
let mut scrut = self.synth_scrutinee(scrutinee_expr);
1821+
let scrut = self.synth_scrutinee(scrutinee_expr);
18751822
let value = self.eval_env().eval(scrut.expr);
18761823

18771824
let patterns: Vec<_> = equations
18781825
.iter()
18791826
.map(|(pat, _)| self.check_pattern(pat, &scrut.r#type))
18801827
.collect();
1881-
1882-
// Bind the scrut to a fresh variable if it is unsafe to evaluate multiple times,
1883-
// and may be evaluated multiple times by the pattern match compiler
1884-
let extra_def = match (
1885-
scrut.expr.is_atomic(),
1886-
patterns.iter().all(|pat| pat.is_atomic()),
1887-
) {
1888-
(false, false) => {
1889-
let def_name = None; // TODO: generate a fresh name
1890-
let def_type = self.quote_env().quote(self.scope, &scrut.r#type);
1891-
let def_expr = scrut.expr.clone();
1892-
1893-
let var = core::Term::LocalVar(def_expr.span(), env::Index::last());
1894-
scrut.expr = self.scope.to_scope(var);
1895-
(self.local_env).push_def(def_name, value.clone(), scrut.r#type.clone());
1896-
Some((def_name, def_type, def_expr))
1897-
}
1898-
_ => None,
1899-
};
1828+
let (scrut, extra_def) = self.freshen_scrutinee(scrut, &value, &patterns);
19001829

19011830
let mut rows = Vec::with_capacity(equations.len());
19021831
let mut bodies = Vec::with_capacity(equations.len());
@@ -1918,21 +1847,8 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
19181847
}
19191848

19201849
let matrix = patterns::PatMatrix::new(rows);
1921-
let expr = self.elab_match(matrix, &bodies, range, scrut.range);
1922-
let expr = match extra_def {
1923-
None => expr,
1924-
Some((def_name, def_type, def_expr)) => {
1925-
self.local_env.pop();
1926-
core::Term::Let(
1927-
range.into(),
1928-
def_name,
1929-
self.scope.to_scope(def_type),
1930-
self.scope.to_scope(def_expr),
1931-
self.scope.to_scope(expr),
1932-
)
1933-
}
1934-
};
1935-
expr
1850+
let body = self.elab_match(matrix, &bodies, range, scrut.range);
1851+
self.bind_scrutinee(range, body, extra_def)
19361852
}
19371853

19381854
fn synth_scrutinee(&mut self, scrutinee_expr: &Term<'_, ByteRange>) -> Scrutinee<'arena> {
@@ -1957,6 +1873,53 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
19571873
}
19581874
}
19591875

1876+
// Bind `scrut` to a fresh variable if it is unsafe to evaluate multiple times,
1877+
// and may be evaluated multiple times by any of `patterns`
1878+
fn freshen_scrutinee(
1879+
&mut self,
1880+
mut scrut: Scrutinee<'arena>,
1881+
value: &ArcValue<'arena>,
1882+
patterns: &[CheckedPattern<'arena>],
1883+
) -> (
1884+
Scrutinee<'arena>,
1885+
Option<(Option<StringId>, core::Term<'arena>, core::Term<'arena>)>,
1886+
) {
1887+
if scrut.expr.is_atomic() || patterns.iter().all(|pat| pat.is_atomic()) {
1888+
return (scrut, None);
1889+
}
1890+
1891+
let def_name = None; // TODO: generate a fresh name
1892+
let def_type = self.quote_env().quote(self.scope, &scrut.r#type);
1893+
let def_expr = scrut.expr.clone();
1894+
1895+
let var = core::Term::LocalVar(def_expr.span(), env::Index::last());
1896+
scrut.expr = self.scope.to_scope(var);
1897+
(self.local_env).push_def(def_name, value.clone(), scrut.r#type.clone());
1898+
let extra_def = Some((def_name, def_type, def_expr));
1899+
(scrut, extra_def)
1900+
}
1901+
1902+
fn bind_scrutinee(
1903+
&mut self,
1904+
range: ByteRange,
1905+
body: core::Term<'arena>,
1906+
extra_def: Option<(Option<StringId>, core::Term<'arena>, core::Term<'arena>)>,
1907+
) -> core::Term<'arena> {
1908+
match extra_def {
1909+
None => body,
1910+
Some((def_name, def_type, def_expr)) => {
1911+
self.local_env.pop();
1912+
core::Term::Let(
1913+
range.into(),
1914+
def_name,
1915+
self.scope.to_scope(def_type),
1916+
self.scope.to_scope(def_expr),
1917+
self.scope.to_scope(body),
1918+
)
1919+
}
1920+
}
1921+
}
1922+
19601923
fn synth_param(
19611924
&mut self,
19621925
pattern: &Pattern<'_, ByteRange>,

‎fathom/src/surface/elaboration/patterns.rs

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ impl<'arena> CheckedPattern<'arena> {
5151
}
5252
}
5353

54-
/// Returns `true` if `self` binds its scrutinee exactly once.
54+
/// Returns `true` if `self` evaluates its scrutinee exactly once.
5555
/// Used as a heuristic to prevent increase in runtime when expanding
5656
/// pattern matches
5757
pub fn is_atomic(&self) -> bool {
@@ -60,9 +60,7 @@ impl<'arena> CheckedPattern<'arena> {
6060
| CheckedPattern::Placeholder(_)
6161
| CheckedPattern::Binder(_, _)
6262
| CheckedPattern::ConstLit(_, _) => true,
63-
CheckedPattern::RecordLit(_, _, patterns) => {
64-
patterns.len() == 1 && patterns[0].is_atomic()
65-
}
63+
CheckedPattern::RecordLit(_, _, _) => false,
6664
}
6765
}
6866
}

0 commit comments

Comments
 (0)