kind_tree/concrete/
expr.rs

1//! This module describes a abstract syntax tree
2//! that is almost like a concrete tree. It helps when it
3//! we have to statically analyse the tree in order to generate
4//! better error messages.
5
6use 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/// A binding express the positional or named argument of
14/// a constructor or function.
15#[derive(Clone, Debug)]
16pub enum Binding {
17    Positional(Box<Expr>),
18    Named(Range, Ident, Box<Expr>),
19}
20
21/// Vector of bindings
22pub type Spine = Vec<Binding>;
23
24/// A binding that is used inside applications.
25#[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/// A case binding is a field or a rename of some field
48/// inside a match expression.
49#[derive(Clone, Debug)]
50pub enum CaseBinding {
51    Field(Ident),
52    Renamed(Ident, Ident),
53}
54
55/// A match case with a constructor that will match the
56/// strutinizer, bindings to the names of each arguments and
57/// a right-hand side value. The ignore_rest flag useful to just
58/// fill all of the case bindings that are not used with a default name.
59#[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/// A match block that will be desugared
68/// into an eliminator of a datatype.
69#[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/// Substitution
80#[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    /// The universe of types (e.g. Type)
91    Type,
92    /// The help operator that prints the context
93    /// and the goal (e.g. ?)
94    Help(Ident),
95    /// The type literal of 60 bit numbers (e.g. 2 : U60)
96    NumTypeU60,
97    NumTypeF60,
98    // Char literal
99    Char(char),
100    /// A 60 bit number literal (e.g 32132)
101    NumU60(u64),
102    // A 120 bit number literal
103    NumU120(u128),
104    // A 60 bit floating point number literal
105    NumF60(u64),
106    // Naturals represented by u128
107    Nat(u128),
108    // A String literal
109    String(String),
110}
111
112/// A destruct of a single constructor. It's a flat destruct
113/// and just translates into a eliminator for records.
114#[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/// Structure of the insides of the `do` notation. It
130/// describes the idea of `sequence` inside a monad
131/// each monadic action contains a `next` element that is
132/// desugared into a 'monadic bind'.
133#[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    /// Name of a variable
157    Var { name: Ident },
158    /// Name of a function/constructor
159    Constr { name: QualifiedIdent, args: Spine },
160    /// The dependent function space (e.g. (x : Int) -> y)
161    All {
162        param: Option<Ident>,
163        typ: Box<Expr>,
164        body: Box<Expr>,
165        erased: bool,
166    },
167    /// The dependent product space (e.g. [x : Int] -> y)
168    Sigma {
169        param: Option<Ident>,
170        fst: Box<Expr>,
171        snd: Box<Expr>,
172    },
173    /// A anonymous function that receives one argument
174    Lambda {
175        param: Ident,
176        typ: Option<Box<Expr>>,
177        body: Box<Expr>,
178        erased: bool,
179    },
180    /// Application of a expression to a spine of expressions
181    App {
182        fun: Box<Expr>,
183        args: Vec<AppBinding>,
184    },
185    /// Declaration of a local variable
186    Let {
187        name: Destruct,
188        val: Box<Expr>,
189        next: Box<Expr>,
190    },
191    /// Type ascription (x : y)
192    Ann { val: Box<Expr>, typ: Box<Expr> },
193    /// Literal
194    Lit { lit: Literal },
195    /// Binary operation (e.g. 2 + 3)
196    Binary {
197        op: Operator,
198        fst: Box<Expr>,
199        snd: Box<Expr>,
200    },
201    /// A expression open to unification (e.g. _)
202    Hole,
203    /// Do notation
204    Do {
205        typ: QualifiedIdent,
206        sttm: Box<Sttm>,
207    },
208    /// If else statement
209    If {
210        cond: Box<Expr>,
211        then_: Box<Expr>,
212        else_: Box<Expr>,
213    },
214    /// If else statement
215    Pair { fst: Box<Expr>, snd: Box<Expr> },
216    /// Array
217    List { args: Vec<Expr> },
218    /// Substituion
219    Subst(Substitution),
220    /// A match block that will be translated
221    /// into an eliminator of a datatype.
222    Match(Box<Match>),
223    /// Adds all of the variables inside the context
224    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/// Describes a single expression inside Kind2.
235#[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}