1use super::pat::PatIdent;
7use crate::symbol::{Ident, QualifiedIdent};
8use crate::Operator;
9
10use kind_span::{Locatable, Range};
11use std::fmt::{Display, Error, Formatter};
12
13#[derive(Clone, Debug)]
16pub enum Binding {
17 Positional(Box<Expr>),
18 Named(Range, Ident, Box<Expr>),
19}
20
21pub type Spine = Vec<Binding>;
23
24#[derive(Clone, Debug)]
26pub struct AppBinding {
27 pub data: Box<Expr>,
28 pub erased: bool,
29}
30
31impl AppBinding {
32 pub fn explicit(data: Box<Expr>) -> AppBinding {
33 AppBinding {
34 data,
35 erased: false,
36 }
37 }
38
39 pub fn from_ident(data: Ident) -> AppBinding {
40 AppBinding {
41 data: Expr::var(data),
42 erased: false,
43 }
44 }
45}
46
47#[derive(Clone, Debug)]
50pub enum CaseBinding {
51 Field(Ident),
52 Renamed(Ident, Ident),
53}
54
55#[derive(Clone, Debug)]
60pub struct Case {
61 pub constructor: Ident,
62 pub bindings: Vec<CaseBinding>,
63 pub value: Box<Expr>,
64 pub ignore_rest: Option<Range>,
65}
66
67#[derive(Clone, Debug)]
70pub struct Match {
71 pub typ: QualifiedIdent,
72 pub scrutinee: Ident,
73 pub value: Option<Box<Expr>>,
74 pub with_vars: Vec<(Ident, Option<Box<Expr>>)>,
75 pub cases: Vec<Case>,
76 pub motive: Option<Box<Expr>>,
77}
78
79#[derive(Clone, Debug)]
81pub struct Substitution {
82 pub name: Ident,
83 pub redx: usize,
84 pub indx: usize,
85 pub expr: Box<Expr>,
86}
87
88#[derive(Clone, Debug)]
89pub enum Literal {
90 Type,
92 Help(Ident),
95 NumTypeU60,
97 NumTypeF60,
98 Char(char),
100 NumU60(u64),
102 NumU120(u128),
104 NumF60(u64),
106 Nat(u128),
108 String(String),
110}
111
112#[derive(Clone, Debug)]
115pub enum Destruct {
116 Destruct(Range, QualifiedIdent, Vec<CaseBinding>, Option<Range>),
117 Ident(Ident),
118}
119
120#[derive(Clone, Debug)]
121pub enum SttmKind {
122 Expr(Box<Expr>, Box<Sttm>),
123 Ask(Destruct, Box<Expr>, Box<Sttm>),
124 Let(Destruct, Box<Expr>, Box<Sttm>),
125 Return(Box<Expr>),
126 RetExpr(Box<Expr>),
127}
128
129#[derive(Clone, Debug)]
134pub struct Sttm {
135 pub data: SttmKind,
136 pub range: Range,
137}
138
139#[derive(Clone, Debug)]
140pub enum SeqOperation {
141 Set(Box<Expr>),
142 Mut(Box<Expr>),
143 Get,
144}
145
146#[derive(Clone, Debug)]
147pub struct SeqRecord {
148 pub typ: Box<Expr>,
149 pub expr: Box<Expr>,
150 pub fields: Vec<Ident>,
151 pub operation: SeqOperation,
152}
153
154#[derive(Clone, Debug)]
155pub enum ExprKind {
156 Var { name: Ident },
158 Constr { name: QualifiedIdent, args: Spine },
160 All {
162 param: Option<Ident>,
163 typ: Box<Expr>,
164 body: Box<Expr>,
165 erased: bool,
166 },
167 Sigma {
169 param: Option<Ident>,
170 fst: Box<Expr>,
171 snd: Box<Expr>,
172 },
173 Lambda {
175 param: Ident,
176 typ: Option<Box<Expr>>,
177 body: Box<Expr>,
178 erased: bool,
179 },
180 App {
182 fun: Box<Expr>,
183 args: Vec<AppBinding>,
184 },
185 Let {
187 name: Destruct,
188 val: Box<Expr>,
189 next: Box<Expr>,
190 },
191 Ann { val: Box<Expr>, typ: Box<Expr> },
193 Lit { lit: Literal },
195 Binary {
197 op: Operator,
198 fst: Box<Expr>,
199 snd: Box<Expr>,
200 },
201 Hole,
203 Do {
205 typ: QualifiedIdent,
206 sttm: Box<Sttm>,
207 },
208 If {
210 cond: Box<Expr>,
211 then_: Box<Expr>,
212 else_: Box<Expr>,
213 },
214 Pair { fst: Box<Expr>, snd: Box<Expr> },
216 List { args: Vec<Expr> },
218 Subst(Substitution),
220 Match(Box<Match>),
223 Open {
225 type_name: QualifiedIdent,
226 var_name: Ident,
227 motive: Option<Box<Expr>>,
228 next: Box<Expr>,
229 },
230
231 SeqRecord(SeqRecord),
232}
233
234#[derive(Clone, Debug)]
236pub struct Expr {
237 pub data: ExprKind,
238 pub range: Range,
239}
240
241impl Expr {
242 pub fn var(name: Ident) -> Box<Expr> {
243 Box::new(Expr {
244 range: name.range,
245 data: ExprKind::Var { name },
246 })
247 }
248
249 pub fn cons(name: QualifiedIdent, args: Spine, range: Range) -> Box<Expr> {
250 Box::new(Expr {
251 range,
252 data: ExprKind::Constr { name, args },
253 })
254 }
255
256 pub fn all(
257 param: Ident,
258 typ: Box<Expr>,
259 body: Box<Expr>,
260 erased: bool,
261 range: Range,
262 ) -> Box<Expr> {
263 Box::new(Expr {
264 range,
265 data: ExprKind::All {
266 param: Some(param),
267 typ,
268 body,
269 erased,
270 },
271 })
272 }
273
274 pub fn lambda(
275 param: Ident,
276 typ: Option<Box<Expr>>,
277 body: Box<Expr>,
278 erased: bool,
279 range: Range,
280 ) -> Box<Expr> {
281 Box::new(Expr {
282 data: ExprKind::Lambda {
283 param,
284 typ,
285 body,
286 erased,
287 },
288 range,
289 })
290 }
291
292 pub fn typ(range: Range) -> Box<Expr> {
293 Box::new(Expr {
294 data: ExprKind::Lit { lit: Literal::Type },
295 range,
296 })
297 }
298
299 pub fn app(fun: Box<Expr>, args: Vec<AppBinding>, range: Range) -> Box<Expr> {
300 Box::new(Expr {
301 data: ExprKind::App { fun, args },
302 range,
303 })
304 }
305
306 pub fn hole(range: Range) -> Box<Expr> {
307 Box::new(Expr {
308 data: ExprKind::Hole,
309 range,
310 })
311 }
312}
313
314impl Locatable for Binding {
315 fn locate(&self) -> kind_span::Range {
316 match self {
317 Binding::Positional(e) => e.locate(),
318 Binding::Named(s, _, _) => *s,
319 }
320 }
321}
322
323impl Locatable for Expr {
324 fn locate(&self) -> Range {
325 self.range
326 }
327}
328
329impl Locatable for Sttm {
330 fn locate(&self) -> Range {
331 self.range
332 }
333}
334
335impl Locatable for Ident {
336 fn locate(&self) -> Range {
337 self.range
338 }
339}
340
341impl Locatable for PatIdent {
342 fn locate(&self) -> Range {
343 self.0.range
344 }
345}
346
347impl Locatable for CaseBinding {
348 fn locate(&self) -> Range {
349 match self {
350 CaseBinding::Field(i) => i.locate(),
351 CaseBinding::Renamed(i, renamed) => i.locate().mix(renamed.locate()),
352 }
353 }
354}
355
356impl Locatable for Destruct {
357 fn locate(&self) -> Range {
358 match self {
359 Destruct::Destruct(range, _, _, _) => *range,
360 Destruct::Ident(i) => i.locate(),
361 }
362 }
363}
364
365impl Expr {
366 pub fn traverse_pi_types(&self) -> String {
367 match &self.data {
368 ExprKind::All {
369 param,
370 typ,
371 body,
372 erased,
373 } => {
374 let tilde = if *erased { "~" } else { "" };
375 match param {
376 None => format!("{}{} -> {}", tilde, typ, body.traverse_pi_types()),
377 Some(binder) => format!(
378 "{}({} : {}) -> {}",
379 tilde,
380 binder,
381 typ,
382 body.traverse_pi_types()
383 ),
384 }
385 }
386 ExprKind::Sigma { param, fst, snd } => match param {
387 None => format!("{} -> {}", fst, snd.traverse_pi_types()),
388 Some(binder) => format!("[{} : {}] -> {}", binder, fst, snd.traverse_pi_types()),
389 },
390 _ => format!("{}", self),
391 }
392 }
393}
394
395impl Display for Literal {
396 fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
397 match self {
398 Literal::Help(s) => write!(f, "?{}", s),
399 Literal::Type => write!(f, "Type"),
400 Literal::NumTypeU60 => write!(f, "Data.U60"),
401 Literal::NumTypeF60 => write!(f, "Data.F60"),
402 Literal::Char(c) => write!(f, "'{}'", c),
403 Literal::NumU60(numb) => write!(f, "{}", numb),
404 Literal::Nat(numb) => write!(f, "{}numb", numb),
405 Literal::NumU120(numb) => write!(f, "{}u120", numb),
406 Literal::NumF60(numb) => write!(f, "{}f60", numb),
407 Literal::String(str) => {
408 write!(f, "{:?}", str)
409 }
410 }
411 }
412}
413
414impl Display for Destruct {
415 fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
416 match self {
417 Destruct::Destruct(_range, i, bindings, ignore) => {
418 write!(f, "{}", i)?;
419 for binding in bindings {
420 write!(f, " {}", binding)?;
421 }
422 if ignore.is_some() {
423 write!(f, " ..")?;
424 }
425 Ok(())
426 }
427 Destruct::Ident(ident) => write!(f, "{}", ident),
428 }
429 }
430}
431
432impl Display for SttmKind {
433 fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
434 match self {
435 SttmKind::Ask(name, block, next) => {
436 write!(f, "ask {} = {};\n {}", name, block, next)
437 }
438 SttmKind::Let(name, block, next) => {
439 write!(f, "let {} = {};\n {}", name, block, next)
440 }
441 SttmKind::Expr(expr, next) => {
442 write!(f, "{};\n{}", expr, next)
443 }
444 SttmKind::Return(ret) => {
445 writeln!(f, "return {}", ret)
446 }
447 SttmKind::RetExpr(ret) => {
448 writeln!(f, "{}", ret)
449 }
450 }
451 }
452}
453
454impl Display for Sttm {
455 fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
456 write!(f, "{}", self.data)
457 }
458}
459
460impl Display for CaseBinding {
461 fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
462 match self {
463 CaseBinding::Field(n) => write!(f, "{}", n),
464 CaseBinding::Renamed(m, n) => write!(f, "({} = {})", m, n),
465 }
466 }
467}
468
469impl Display for Case {
470 fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
471 write!(f, "{}", self.constructor)?;
472 for bind in &self.bindings {
473 write!(f, " {}", bind)?
474 }
475 if self.ignore_rest.is_some() {
476 write!(f, " ..")?;
477 }
478 write!(f, " => {}", self.value)
479 }
480}
481
482impl Display for Match {
483 fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
484 write!(f, "match {} {}", self.typ, self.scrutinee)?;
485
486 match &self.motive {
487 None => Ok(()),
488 Some(res) => write!(f, " : {}", res),
489 }?;
490 write!(f, " {{ ")?;
491
492 for case in &self.cases {
493 write!(f, "{}; ", case)?
494 }
495 write!(f, "}}")
496 }
497}
498
499impl Display for Substitution {
500 fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
501 write!(f, "## {} / {} {}", self.name, self.redx, self.expr)
502 }
503}
504
505impl Display for Binding {
506 fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
507 match self {
508 Binding::Positional(e) => write!(f, "{}", e),
509 Binding::Named(_, i, e) => write!(f, "({} : {})", i, e),
510 }
511 }
512}
513
514impl Display for AppBinding {
515 fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
516 if self.erased {
517 write!(f, "~({})", self.data)
518 } else {
519 write!(f, "{}", self.data)
520 }
521 }
522}
523
524impl Display for Expr {
525 fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
526 use ExprKind::*;
527 match &self.data {
528 Do { typ, sttm } => write!(f, "(do {} {{{}}})", typ, sttm),
529 All { .. } => write!(f, "({})", self.traverse_pi_types()),
530 Sigma { .. } => write!(f, "({})", self.traverse_pi_types()),
531 Lit { lit } => write!(f, "{}", lit),
532 Var { name } => write!(f, "{}", name),
533 Constr { name, args } => write!(
534 f,
535 "({}{})",
536 name,
537 args.iter().map(|x| format!(" {}", x)).collect::<String>()
538 ),
539 Lambda {
540 param,
541 typ: None,
542 body,
543 erased: false,
544 } => write!(f, "({} => {})", param, body),
545 Lambda {
546 param,
547 typ: Some(typ),
548 body,
549 erased: false,
550 } => {
551 write!(f, "(({} : {}) => {})", param, typ, body)
552 }
553 Lambda {
554 param,
555 typ: None,
556 body,
557 erased: true,
558 } => write!(f, "(~({}) => {})", param, body),
559 Lambda {
560 param,
561 typ: Some(typ),
562 body,
563 erased: true,
564 } => {
565 write!(f, "({{{} : {}}} => {})", param, typ, body)
566 }
567 Pair { fst, snd } => write!(f, "($ {} {})", fst, snd),
568 App { fun, args } => write!(
569 f,
570 "({}{})",
571 fun,
572 args.iter().map(|x| format!(" {}", x)).collect::<String>()
573 ),
574 Let { name, val, next } => write!(f, "(let {} = {}; {})", name, val, next),
575 Open {
576 type_name,
577 var_name,
578 motive: Some(motive),
579 next,
580 } => write!(f, "(open {} {} : {motive}; {})", type_name, var_name, next),
581 Open {
582 type_name,
583 var_name,
584 motive: None,
585 next,
586 } => write!(f, "(open {} {}; {})", type_name, var_name, next),
587 If { cond, then_, else_ } => {
588 write!(f, "(if {} {{{}}} else {{{}}})", cond, then_, else_)
589 }
590 List { args } => write!(
591 f,
592 "[{}]",
593 args.iter()
594 .map(|x| format!("{}", x))
595 .collect::<Vec<String>>()
596 .join(" ")
597 ),
598 Ann { val: name, typ } => write!(f, "({} :: {})", name, typ),
599 Binary { op, fst, snd } => write!(f, "({} {} {})", op, fst, snd),
600 Match(matcher) => write!(f, "({})", matcher),
601 Subst(subst) => write!(f, "({})", subst),
602 Hole => write!(f, "_"),
603 SeqRecord(rec) => {
604 use SeqOperation::*;
605 write!(
606 f,
607 "(!({}) {} {}",
608 rec.typ,
609 rec.expr,
610 rec.fields
611 .iter()
612 .map(|x| format!(".{}", x.to_str()))
613 .collect::<Vec<_>>()
614 .join(",")
615 )?;
616 match &rec.operation {
617 Set(expr) => write!(f, "+= {})", expr),
618 Mut(expr) => write!(f, "@= {})", expr),
619 Get => write!(f, ")"),
620 }
621 }
622 }
623 }
624}
625
626impl Binding {
627 pub fn to_app_binding(&self) -> AppBinding {
628 match self {
629 Binding::Positional(expr) => AppBinding {
630 data: expr.clone(),
631 erased: false,
632 },
633 Binding::Named(_, _, expr) => AppBinding {
634 data: expr.clone(),
635 erased: false,
636 },
637 }
638 }
639}