phase_rs/
typecheck.rs

1//! Functions and datastructures for type checking
2
3use std::collections::HashMap;
4
5use miette::Diagnostic;
6use thiserror::Error;
7
8use crate::{
9    raw_syntax::{PatternR, TermR, pattern::PatTensorR, term::TensorR},
10    text::{Name, Span},
11    typed_syntax::{PatternType, TermT, TermType},
12};
13
14/// Errors that can occur during typechecking.
15#[derive(Error, Diagnostic, Debug, Clone)]
16pub enum TypeCheckError<S: Span> {
17    /// Error for mismatching type between terms in a composition.
18    #[error("Type mismatch when composing")]
19    #[diagnostic(code("Type mismatch."))]
20    TypeMismatch {
21        /// Term 1
22        #[label("Has type {ty1}")]
23        t1: TensorR<S>,
24        /// Type of term 1
25        ty1: TermType,
26        /// Term 2
27        #[label("Has type {ty2}")]
28        t2: TensorR<S>,
29        /// Type of term 2
30        ty2: TermType,
31    },
32    /// Error for mismatching type between a term and pattern in an "if let" statement.
33    #[error("Type mismatch between pattern and term in 'if let'")]
34    #[diagnostic(code("If let type mismatch."))]
35    IfTypeMismatch {
36        /// Pattern
37        #[label("Has type {pty}")]
38        p: PatternR<S>,
39        /// Type of pattern
40        pty: PatternType,
41        /// Body term
42        #[label("Has type {tty}")]
43        t: TensorR<S>,
44        /// Type of body term
45        tty: TermType,
46    },
47    /// Error for mismatching type between composed patterns.
48    #[error("Type mismatch when composing patterns")]
49    #[diagnostic(code("Pattern type mismatch."))]
50    PatternTypeMismatch {
51        /// Pattern 1
52        #[label("Has type {ty1}")]
53        p1: PatTensorR<S>,
54        /// Type of pattern 1
55        ty1: PatternType,
56        /// Pattern 2
57        #[label("Has type {ty2}")]
58        p2: PatTensorR<S>,
59        /// Type of pattern 2
60        ty2: PatternType,
61    },
62    /// Error for an unknown top-level symbol.
63    #[error("Unrecognised top-level symbol {name}.")]
64    #[diagnostic(code("Unknown symbol."))]
65    UnknownSymbol {
66        /// The unknown symbol encountered
67        name: Name,
68        /// Span of symbol
69        #[label("Symbol used here")]
70        span: S,
71    },
72    /// Error for when a sqrt operation is applied to a term with compositions.
73    #[error("Tried to root unrootable unitary term.")]
74    #[diagnostic(code("Invalid root."))]
75    TermNotRootable {
76        /// Term which contains compositions
77        tm: TermR<S>,
78        #[label("This compostion prevents square rooting")]
79        /// Span of sqrt term causing error
80        #[label("Square root applied here")]
81        span_of_root: S,
82    },
83}
84
85/// Typing enviroment, holding definitions of top level symbols.
86#[derive(Default)]
87pub struct Env(pub(crate) HashMap<Name, TermT>);
phase_rs/typecheck.rs

phase_rs/
typecheck.rs
