kind_tree/desugared/
mod.rs

1//! This module describes an unsugared tree that
2//! is used by the type checker and by the targets.
3
4use std::fmt::{Display, Error, Formatter};
5
6use fxhash::FxHashMap;
7use kind_span::Range;
8use linked_hash_map::LinkedHashMap;
9
10pub use crate::Operator;
11
12use crate::{
13    symbol::{Ident, QualifiedIdent},
14    telescope::Telescope,
15    Attributes,
16};
17
18/// Just a vector of expressions. It is called spine because
19/// it is usually in a form like (a b c d e) that can be interpret
20/// as ((((a b) c) d) e) that looks like a spine.
21pub type Spine = Vec<Box<Expr>>;
22
23#[derive(Clone, Debug, Hash, PartialEq, Eq)]
24pub struct AppBinding {
25    pub data: Box<Expr>,
26    pub erased: bool,
27}
28
29#[derive(Clone, Debug, Hash, PartialEq, Eq)]
30pub enum ExprKind {
31    /// Name of a variable
32    Var { name: Ident },
33    /// The dependent function space (e.g. (x : Int) -> y)
34    All {
35        param: Ident,
36        typ: Box<Expr>,
37        body: Box<Expr>,
38        erased: bool,
39    },
40    /// A anonymous function that receives one argument
41    Lambda {
42        param: Ident,
43        body: Box<Expr>,
44        erased: bool,
45    },
46    /// Application of a expression to a spine of expressions
47    App {
48        fun: Box<Expr>,
49        args: Vec<AppBinding>,
50    },
51    /// Application of a function
52    Fun { name: QualifiedIdent, args: Spine },
53    /// Application of a Construtor
54    Ctr { name: QualifiedIdent, args: Spine },
55    /// Declaration of a local variable
56    Let {
57        name: Ident,
58        val: Box<Expr>,
59        next: Box<Expr>,
60    },
61    /// Type ascription (x : y)
62    Ann { expr: Box<Expr>, typ: Box<Expr> },
63    /// Substitution
64    Sub {
65        name: Ident,
66        indx: usize,
67        redx: usize,
68        expr: Box<Expr>,
69    },
70    /// Type Literal
71    Typ,
72    /// 60 bit integer type
73    NumTypeU60,
74    /// 60 bit floating point number type
75    NumTypeF60,
76    /// 60 bit integer
77    NumU60 { numb: u64 },
78    /// 60 bit floating point number
79    NumF60 { numb: u64 },
80    /// Very special constructor :)
81    Str { val: String },
82    /// Binary operation (e.g. 2 + 3)
83    Binary {
84        op: Operator,
85        left: Box<Expr>,
86        right: Box<Expr>,
87    },
88    /// A expression open to unification (e.g. _)
89    Hole { num: u64 },
90    /// Help
91    Hlp(Ident),
92    /// Error node (It's useful as a sentinel value
93    /// to be able to continue compilation even with
94    /// parts of the tree with problems)
95    Err,
96}
97
98#[derive(Clone, Debug, Hash, PartialEq, Eq)]
99pub struct Expr {
100    pub data: ExprKind,
101    pub range: Range,
102}
103
104impl Expr {
105    pub fn var(name: Ident) -> Box<Expr> {
106        Box::new(Expr {
107            range: name.range,
108            data: ExprKind::Var { name },
109        })
110    }
111
112    pub fn all(
113        range: Range,
114        param: Ident,
115        typ: Box<Expr>,
116        body: Box<Expr>,
117        erased: bool,
118    ) -> Box<Expr> {
119        Box::new(Expr {
120            range,
121            data: ExprKind::All {
122                param,
123                typ,
124                body,
125                erased,
126            },
127        })
128    }
129
130    pub fn sub(range: Range, name: Ident, indx: usize, redx: usize, expr: Box<Expr>) -> Box<Expr> {
131        Box::new(Expr {
132            range,
133            data: ExprKind::Sub {
134                name,
135                indx,
136                redx,
137                expr,
138            },
139        })
140    }
141
142    pub fn lambda(range: Range, param: Ident, body: Box<Expr>, erased: bool) -> Box<Expr> {
143        Box::new(Expr {
144            range,
145            data: ExprKind::Lambda {
146                param,
147                body,
148                erased,
149            },
150        })
151    }
152
153    pub fn identity_lambda(ident: Ident) -> Box<Expr> {
154        Box::new(Expr {
155            range: ident.range,
156            data: ExprKind::Lambda {
157                param: ident.clone(),
158                body: Self::var(ident),
159                erased: false,
160            },
161        })
162    }
163
164    pub fn unfold_lambda(irrelev: &[bool], idents: &[Ident], body: Box<Expr>) -> Box<Expr> {
165        idents
166            .iter()
167            .rev()
168            .zip(irrelev)
169            .fold(body, |body, (ident, irrelev)| {
170                Expr::lambda(ident.range, ident.clone(), body, *irrelev)
171            })
172    }
173
174    pub fn unfold_all(
175        irrelev: &[bool],
176        idents: &[(Ident, Box<Expr>)],
177        body: Box<Expr>,
178    ) -> Box<Expr> {
179        idents
180            .iter()
181            .rev()
182            .zip(irrelev)
183            .fold(body, |body, ((ident, typ), irrelev)| {
184                Expr::all(ident.range, ident.clone(), typ.clone(), body, *irrelev)
185            })
186    }
187
188    pub fn app(range: Range, fun: Box<Expr>, args: Vec<AppBinding>) -> Box<Expr> {
189        Box::new(Expr {
190            range,
191            data: ExprKind::App { fun, args },
192        })
193    }
194
195    pub fn fun(range: Range, name: QualifiedIdent, args: Vec<Box<Expr>>) -> Box<Expr> {
196        Box::new(Expr {
197            range,
198            data: ExprKind::Fun { name, args },
199        })
200    }
201
202    pub fn ctr(range: Range, name: QualifiedIdent, args: Vec<Box<Expr>>) -> Box<Expr> {
203        Box::new(Expr {
204            range,
205            data: ExprKind::Ctr { name, args },
206        })
207    }
208
209    pub fn let_(range: Range, name: Ident, val: Box<Expr>, next: Box<Expr>) -> Box<Expr> {
210        Box::new(Expr {
211            range,
212            data: ExprKind::Let { name, val, next },
213        })
214    }
215
216    pub fn ann(range: Range, expr: Box<Expr>, typ: Box<Expr>) -> Box<Expr> {
217        Box::new(Expr {
218            range,
219            data: ExprKind::Ann { expr, typ },
220        })
221    }
222
223    pub fn typ(range: Range) -> Box<Expr> {
224        Box::new(Expr {
225            range,
226            data: ExprKind::Typ,
227        })
228    }
229
230    pub fn type_u60(range: Range) -> Box<Expr> {
231        Box::new(Expr {
232            range,
233            data: ExprKind::NumTypeU60,
234        })
235    }
236
237    pub fn type_f60(range: Range) -> Box<Expr> {
238        Box::new(Expr {
239            range,
240            data: ExprKind::NumTypeF60,
241        })
242    }
243
244    pub fn num_u60(range: Range, numb: u64) -> Box<Expr> {
245        Box::new(Expr {
246            range,
247            data: ExprKind::NumU60 { numb },
248        })
249    }
250
251    pub fn num_u120(range: Range, numb: u128) -> Box<Expr> {
252        let name = QualifiedIdent::new_static("Data.U120.new", None, range);
253        let lo = Expr::num_u60(range, (numb & 0xFFFFFFFFFFFFFFF) as u64);
254        let hi = Expr::num_u60(range, (numb >> 60) as u64);
255        Box::new(Expr {
256            range,
257            data: ExprKind::Ctr {
258                name,
259                args: vec![hi, lo],
260            },
261        })
262    }
263
264    pub fn num_f60(range: Range, numb: u64) -> Box<Expr> {
265        Box::new(Expr {
266            range,
267            data: ExprKind::NumF60 { numb },
268        })
269    }
270
271    pub fn binary(range: Range, op: Operator, left: Box<Expr>, right: Box<Expr>) -> Box<Expr> {
272        Box::new(Expr {
273            range,
274            data: ExprKind::Binary { op, left, right },
275        })
276    }
277
278    pub fn hole(range: Range, num: u64) -> Box<Expr> {
279        Box::new(Expr {
280            range,
281            data: ExprKind::Hole { num },
282        })
283    }
284
285    pub fn str(range: Range, val: String) -> Box<Expr> {
286        Box::new(Expr {
287            range,
288            data: ExprKind::Str { val },
289        })
290    }
291
292    pub fn hlp(range: Range, hlp: Ident) -> Box<Expr> {
293        Box::new(Expr {
294            range,
295            data: ExprKind::Hlp(hlp),
296        })
297    }
298
299    pub fn err(range: Range) -> Box<Expr> {
300        Box::new(Expr {
301            data: ExprKind::Err,
302            range,
303        })
304    }
305}
306
307/// An argument is a 'binding' of a name to a type
308/// it has some other options like
309/// eras: that express the erasure of this type when
310/// compiled.
311/// hide: that express a implicit argument (that will
312/// be discovered through unification).
313#[derive(Clone, Debug)]
314pub struct Argument {
315    pub hidden: bool,
316    pub erased: bool,
317    pub name: Ident,
318    pub typ: Box<Expr>,
319    pub range: Range,
320}
321
322/// A rule is a equation that in the left-hand-side
323/// contains a list of patterns @pats@ and on the
324/// right hand side a value.
325#[derive(Clone, Debug)]
326pub struct Rule {
327    pub name: QualifiedIdent,
328    pub pats: Vec<Box<Expr>>,
329    pub body: Box<Expr>,
330    pub range: Range,
331}
332
333/// An entry describes a function that is typed
334/// and has rules. The type of the function
335/// consists of the arguments @args@ and the
336/// return type @typ@.
337#[derive(Clone, Debug)]
338pub struct Entry {
339    pub name: QualifiedIdent,
340    pub args: Vec<Argument>,
341    pub typ: Box<Expr>,
342    pub rules: Vec<Rule>,
343    pub attrs: Attributes,
344    pub range: Range,
345}
346
347/// Type family information
348#[derive(Clone, Debug)]
349pub struct Family {
350    pub name: QualifiedIdent,
351    pub parameters: Telescope<Argument>,
352    pub constructors: Vec<QualifiedIdent>,
353}
354
355/// A book is a collection of desugared entries.
356#[derive(Clone, Debug, Default)]
357pub struct Book {
358    pub entrs: LinkedHashMap<String, Box<Entry>>,
359    pub names: FxHashMap<String, usize>,
360    pub families: FxHashMap<String, Family>,
361    pub holes: u64,
362}
363
364impl Expr {
365    pub fn new_var(name: Ident) -> Expr {
366        Expr {
367            range: name.range,
368            data: ExprKind::Var { name },
369        }
370    }
371
372    pub fn traverse_pi_types(&self) -> String {
373        match &self.data {
374            ExprKind::All {
375                param,
376                typ,
377                body,
378                erased,
379            } => {
380                let tilde = if *erased { "~" } else { "" };
381                if param.to_string().starts_with('_') {
382                    format!("{}{} -> {}", tilde, typ, body.traverse_pi_types())
383                } else {
384                    let body = body.traverse_pi_types();
385                    format!("{}({} : {}) -> {}", tilde, param, typ, body)
386                }
387            }
388            _ => format!("{}", self),
389        }
390    }
391}
392
393impl Display for AppBinding {
394    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
395        if self.erased {
396            write!(f, "~({})", self.data)
397        } else {
398            write!(f, "{}", self.data)
399        }
400    }
401}
402
403pub fn try_desugar_to_nat(name: &QualifiedIdent, spine: &[Box<Expr>], acc: u128) -> Option<u128> {
404    match (name.to_str(), spine) {
405        ("Data.Nat.zero", []) => Some(acc),
406        ("Data.Nat.succ", [spine]) => match &spine.data {
407            ExprKind::Ctr { name, args } => try_desugar_to_nat(name, args, acc + 1),
408            _ => None,
409        },
410        _ => None,
411    }
412}
413
414impl Display for Expr {
415    fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
416        use ExprKind::*;
417        match &self.data {
418            Typ => write!(f, "Type"),
419            NumTypeU60 => write!(f, "Data.U60"),
420            NumTypeF60 => write!(f, "Data.F60"),
421            Str { val } => write!(f, "\"{}\"", val),
422            NumU60 { numb } => write!(f, "{}", numb),
423            NumF60 { numb: _ } => todo!(),
424            All { .. } => write!(f, "({})", self.traverse_pi_types()),
425            Var { name } => write!(f, "{}", name),
426            Lambda {
427                param,
428                body,
429                erased: false,
430            } => write!(f, "({} => {})", param, body),
431            Lambda {
432                param,
433                body,
434                erased: true,
435            } => write!(f, "(~{} => {})", param, body),
436            Sub {
437                name, redx, expr, ..
438            } => write!(f, "(## {}/{} {})", name, redx, expr),
439            App { fun, args } => write!(
440                f,
441                "({}{})",
442                fun,
443                args.iter().map(|x| format!(" {}", x)).collect::<String>()
444            ),
445            Fun { name, args } | Ctr { name, args } => {
446                if let Some(res) = try_desugar_to_nat(name, args, 0) {
447                    write!(f, "{res}n")
448                } else if args.is_empty() {
449                    write!(f, "{}", name)
450                } else {
451                    write!(
452                        f,
453                        "({}{})",
454                        name,
455                        args.iter().map(|x| format!(" {}", x)).collect::<String>()
456                    )
457                }
458            }
459            Let { name, val, next } => write!(f, "(let {} = {}; {})", name, val, next),
460            Ann { expr, typ } => write!(f, "({} :: {})", expr, typ),
461            Binary { op, left, right } => write!(f, "({} {} {})", op, left, right),
462            Hole { .. } => write!(f, "_"),
463            Hlp(name) => write!(f, "?{}", name),
464            Err => write!(f, "ERR"),
465        }
466    }
467}
468
469impl Display for Book {
470    fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
471        for entr in self.entrs.values() {
472            writeln!(f, "{}\n", entr)?;
473        }
474        Ok(())
475    }
476}
477
478impl Display for Argument {
479    fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
480        let (open, close) = match (self.erased, self.hidden) {
481            (false, false) => ("(", ")"),
482            (false, true) => ("+<", ">"),
483            (true, false) => ("-(", ")"),
484            (true, true) => ("<", ">"),
485        };
486        write!(f, "{}{}: {}{}", open, self.name, self.typ, close)
487    }
488}
489
490impl Display for Entry {
491    fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
492        write!(f, "{}", self.name.clone())?;
493
494        for arg in &self.args {
495            write!(f, " {}", arg)?;
496        }
497
498        write!(f, " : {}", &self.typ)?;
499
500        for rule in &self.rules {
501            write!(f, "\n{}", rule)?
502        }
503
504        Ok(())
505    }
506}
507
508impl Display for Rule {
509    fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
510        write!(f, "{}", self.name)?;
511        for pat in &self.pats {
512            write!(f, " {}", pat)?;
513        }
514        write!(f, " = {}", self.body)
515    }
516}
517
518impl Argument {
519    pub fn to_irrelevant(&self) -> Argument {
520        Argument {
521            hidden: true,
522            erased: true,
523            name: self.name.clone(),
524            typ: self.typ.clone(),
525            range: self.range,
526        }
527    }
528
529    pub fn from_field(name: &Ident, typ: Box<Expr>, range: Range) -> Argument {
530        Argument {
531            hidden: false,
532            erased: false,
533            name: name.clone(),
534            typ,
535            range,
536        }
537    }
538}
kind_tree/desugared/mod.rs

kind_tree/desugared/
mod.rs
