Skip to content

Commit d9d16f3

Browse files
brendanzabbrendanzab
authored
Merge pull request #439 from Kmeakin/implicit-args
Implicit args
2 parents 2e6490f + 975f7f9 commit d9d16f3

25 files changed

+753
-275
lines changed

‎doc/roadmap.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
- [x] let expressions
99
- [x] dependent function types
1010
- [x] condensed syntax for multiple parameters
11-
- [ ] implicit parameters
11+
- [x] implicit parameters
1212
- [x] records
1313
- [x] non-dependent
1414
- [x] dependent

‎fathom/src/core.rs‎

Lines changed: 30 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
//! Core language.
22
3+
use std::fmt;
4+
35
use crate::env::{Index, Level};
46
use crate::source::{Span, StringId};
57

@@ -38,6 +40,21 @@ pub enum LocalInfo {
3840
Param,
3941
}
4042

43+
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
44+
pub enum Plicity {
45+
Explicit,
46+
Implicit,
47+
}
48+
49+
impl fmt::Display for Plicity {
50+
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
51+
match self {
52+
Plicity::Explicit => write!(f, "explicit"),
53+
Plicity::Implicit => write!(f, "implicit"),
54+
}
55+
}
56+
}
57+
4158
/// Core language terms.
4259
#[derive(Debug, Clone)]
4360
pub enum Term<'arena> {
@@ -141,16 +158,17 @@ pub enum Term<'arena> {
141158
/// Also known as: pi types, dependent product types.
142159
FunType(
143160
Span,
161+
Plicity,
144162
Option<StringId>,
145163
&'arena Term<'arena>,
146164
&'arena Term<'arena>,
147165
),
148166
/// Function literals.
149167
///
150168
/// Also known as: lambda expressions, anonymous functions.
151-
FunLit(Span, Option<StringId>, &'arena Term<'arena>),
169+
FunLit(Span, Plicity, Option<StringId>, &'arena Term<'arena>),
152170
/// Function applications.
153-
FunApp(Span, &'arena Term<'arena>, &'arena Term<'arena>),
171+
FunApp(Span, Plicity, &'arena Term<'arena>, &'arena Term<'arena>),
154172

155173
/// Dependent record types.
156174
RecordType(Span, &'arena [StringId], &'arena [Term<'arena>]),
@@ -196,9 +214,9 @@ impl<'arena> Term<'arena> {
196214
| Term::Ann(span, _, _)
197215
| Term::Let(span, _, _, _, _)
198216
| Term::Universe(span)
199-
| Term::FunType(span, _, _, _)
200-
| Term::FunLit(span, _, _)
201-
| Term::FunApp(span, _, _)
217+
| Term::FunType(span, ..)
218+
| Term::FunLit(span, ..)
219+
| Term::FunApp(span, ..)
202220
| Term::RecordType(span, _, _)
203221
| Term::RecordLit(span, _, _)
204222
| Term::RecordProj(span, _, _)
@@ -229,11 +247,11 @@ impl<'arena> Term<'arena> {
229247
|| def_expr.binds_local(var)
230248
|| body_expr.binds_local(var.prev())
231249
}
232-
Term::FunType(_, _, param_type, body_type) => {
250+
Term::FunType(.., param_type, body_type) => {
233251
param_type.binds_local(var) || body_type.binds_local(var.prev())
234252
}
235-
Term::FunLit(_, _, body_expr) => body_expr.binds_local(var.prev()),
236-
Term::FunApp(_, head_expr, arg_expr) => {
253+
Term::FunLit(.., body_expr) => body_expr.binds_local(var.prev()),
254+
Term::FunApp(.., head_expr, arg_expr) => {
237255
head_expr.binds_local(var) || arg_expr.binds_local(var)
238256
}
239257
Term::RecordType(_, _, terms)
@@ -256,6 +274,10 @@ impl<'arena> Term<'arena> {
256274
}
257275
}
258276
}
277+
278+
pub fn is_error(&self) -> bool {
279+
matches!(self, Term::Prim(_, Prim::ReportedError))
280+
}
259281
}
260282

261283
macro_rules! def_prims {

‎fathom/src/core/binary.rs‎

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -381,8 +381,8 @@ impl<'arena, 'data> Context<'arena, 'data> {
381381
Value::Stuck(Head::LocalVar(_), _)
382382
| Value::Stuck(Head::MetaVar(_), _)
383383
| Value::Universe
384-
| Value::FunType(_, _, _)
385-
| Value::FunLit(_, _)
384+
| Value::FunType(..)
385+
| Value::FunLit(..)
386386
| Value::RecordType(_, _)
387387
| Value::RecordLit(_, _)
388388
| Value::ArrayLit(_)
@@ -419,22 +419,22 @@ impl<'arena, 'data> Context<'arena, 'data> {
419419
(Prim::FormatF32Le, []) => read_const(reader, span, read_f32le, Const::F32),
420420
(Prim::FormatF64Be, []) => read_const(reader, span, read_f64be, Const::F64),
421421
(Prim::FormatF64Le, []) => read_const(reader, span, read_f64le, Const::F64),
422-
(Prim::FormatArray8, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format),
423-
(Prim::FormatArray16, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format),
424-
(Prim::FormatArray32, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format),
425-
(Prim::FormatArray64, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format),
426-
(Prim::FormatRepeatUntilEnd, [FunApp(format)]) => self.read_repeat_until_end(reader, format),
427-
(Prim::FormatLimit8, [FunApp(limit), FunApp(format)]) => self.read_limit(reader, limit, format),
428-
(Prim::FormatLimit16, [FunApp(limit), FunApp(format)]) => self.read_limit(reader, limit, format),
429-
(Prim::FormatLimit32, [FunApp(limit), FunApp(format)]) => self.read_limit(reader, limit, format),
430-
(Prim::FormatLimit64, [FunApp(limit), FunApp(format)]) => self.read_limit(reader, limit, format),
431-
(Prim::FormatLink, [FunApp(pos), FunApp(format)]) => self.read_link(span, pos, format),
432-
(Prim::FormatDeref, [FunApp(format), FunApp(r#ref)]) => self.read_deref(format, r#ref),
422+
(Prim::FormatArray8, [FunApp(_, len), FunApp(_, format)]) => self.read_array(reader, span, len, format),
423+
(Prim::FormatArray16, [FunApp(_, len), FunApp(_, format)]) => self.read_array(reader, span, len, format),
424+
(Prim::FormatArray32, [FunApp(_, len), FunApp(_, format)]) => self.read_array(reader, span, len, format),
425+
(Prim::FormatArray64, [FunApp(_, len), FunApp(_, format)]) => self.read_array(reader, span, len, format),
426+
(Prim::FormatRepeatUntilEnd, [FunApp(_,format)]) => self.read_repeat_until_end(reader, format),
427+
(Prim::FormatLimit8, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
428+
(Prim::FormatLimit16, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
429+
(Prim::FormatLimit32, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
430+
(Prim::FormatLimit64, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
431+
(Prim::FormatLink, [FunApp(_, pos), FunApp(_, format)]) => self.read_link(span, pos, format),
432+
(Prim::FormatDeref, [FunApp(_, format), FunApp(_, r#ref)]) => self.read_deref(format, r#ref),
433433
(Prim::FormatStreamPos, []) => read_stream_pos(reader, span),
434-
(Prim::FormatSucceed, [_, FunApp(elem)]) => Ok(elem.clone()),
434+
(Prim::FormatSucceed, [_, FunApp(_, elem)]) => Ok(elem.clone()),
435435
(Prim::FormatFail, []) => Err(ReadError::ReadFailFormat(span)),
436-
(Prim::FormatUnwrap, [_, FunApp(option)]) => match option.match_prim_spine() {
437-
Some((Prim::OptionSome, [FunApp(elem)])) => Ok(elem.clone()),
436+
(Prim::FormatUnwrap, [_, FunApp(_, option)]) => match option.match_prim_spine() {
437+
Some((Prim::OptionSome, [FunApp(_, elem)])) => Ok(elem.clone()),
438438
Some((Prim::OptionNone, [])) => Err(ReadError::UnwrappedNone(span)),
439439
_ => Err(ReadError::InvalidValue(span)),
440440
},

‎fathom/src/core/pretty.rs‎

Lines changed: 14 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@
2727
use pretty::RcDoc;
2828
use std::cell::RefCell;
2929

30-
use crate::core::{Item, Module, Term};
30+
use crate::core::{Item, Module, Plicity, Term};
3131
use crate::source::{StringId, StringInterner};
3232
use crate::surface::lexer::is_keyword;
3333

@@ -113,6 +113,13 @@ impl<'interner, 'arena> Context<'interner> {
113113
)
114114
}
115115

116+
fn plicity(&'arena self, plicity: Plicity) -> RcDoc {
117+
match plicity {
118+
Plicity::Explicit => RcDoc::nil(),
119+
Plicity::Implicit => RcDoc::text("@"),
120+
}
121+
}
122+
116123
pub fn term(&'arena self, term: &Term<'arena>) -> RcDoc {
117124
self.term_prec(Prec::Top, term)
118125
}
@@ -159,7 +166,7 @@ impl<'interner, 'arena> Context<'interner> {
159166
]),
160167
),
161168
Term::Universe(_) => RcDoc::text("Type"),
162-
Term::FunType(_, param_name, param_type, body_type) => self.paren(
169+
Term::FunType(_, plicity, param_name, param_type, body_type) => self.paren(
163170
prec > Prec::Fun,
164171
RcDoc::concat([
165172
RcDoc::concat([
@@ -170,6 +177,7 @@ impl<'interner, 'arena> Context<'interner> {
170177
prec > Prec::Top,
171178
RcDoc::concat([
172179
RcDoc::concat([
180+
self.plicity(*plicity),
173181
if let Some(name) = param_name {
174182
self.string_id(*name)
175183
} else {
@@ -191,12 +199,13 @@ impl<'interner, 'arena> Context<'interner> {
191199
self.term_prec(Prec::Fun, body_type),
192200
]),
193201
),
194-
Term::FunLit(_, param_name, body_expr) => self.paren(
202+
Term::FunLit(_, plicity, param_name, body_expr) => self.paren(
195203
prec > Prec::Fun,
196204
RcDoc::concat([
197205
RcDoc::concat([
198206
RcDoc::text("fun"),
199207
RcDoc::space(),
208+
self.plicity(*plicity),
200209
if let Some(name) = param_name {
201210
self.string_id(*name)
202211
} else {
@@ -210,9 +219,10 @@ impl<'interner, 'arena> Context<'interner> {
210219
self.term_prec(Prec::Let, body_expr),
211220
]),
212221
),
213-
Term::FunApp(_, head_expr, arg_expr) => self.paren(
222+
Term::FunApp(_, plicity, head_expr, arg_expr) => self.paren(
214223
prec > Prec::App,
215224
RcDoc::concat([
225+
self.plicity(*plicity),
216226
self.term_prec(Prec::Proj, head_expr),
217227
RcDoc::space(),
218228
self.term_prec(Prec::Proj, arg_expr),

0 commit comments

Comments
 (0)