yatima_core/check/
error.rs

1use sp_std::{
2  borrow::ToOwned,
3  fmt,
4};
5
6use alloc::string::String;
7
8use crate::{
9  check::ctx::*,
10  literal::LitType,
11  position::Pos,
12  term::Term,
13  uses::Uses,
14};
15
16/// Errors that may occur during typechecking
17#[derive(Debug)]
18pub enum CheckError {
19  UndefinedReference(Pos, String),
20  UnboundVariable(Pos, ErrCtx, String, u64),
21  UntypedLambda(Pos, ErrCtx),
22  UntypedData(Pos, ErrCtx),
23  QuantityTooLittle(Pos, ErrCtx, String, Uses, Uses),
24  QuantityTooMuch(Pos, ErrCtx, String, Uses, Uses),
25  TypeMismatch(Pos, ErrCtx, Term, Term),
26  LamAllMismatch(Pos, ErrCtx, Term, Term),
27  DatSlfMismatch(Pos, ErrCtx, Term, Term),
28  AppFunMismatch(Pos, ErrCtx, Term, Term),
29  CseDatMismatch(Pos, ErrCtx, Term, Term),
30  NonInductiveLitType(Pos, ErrCtx, LitType),
31  GenericError(Pos, ErrCtx, String),
32}
33
34impl CheckError {
35  /// Returns the source position of a typecheck error
36  pub fn pos(&self) -> Pos {
37    match self {
38      Self::TypeMismatch(pos, ..) => *pos,
39      Self::GenericError(pos, ..) => *pos,
40      _ => Pos::None,
41    }
42  }
43}
44
45/// Formats the source position for pretty-printing
46pub fn pretty_pos(pos: Pos) -> String {
47  if let Pos::Some(pos) = pos {
48    format!(
49      "from {}:{} to {}:{} in {}",
50      pos.from_line, pos.from_column, pos.upto_line, pos.upto_column, pos.input
51    )
52  }
53  else {
54    "at unknown location".to_owned()
55  }
56}
57
58impl fmt::Display for CheckError {
59  fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
60    match self {
61      CheckError::UnboundVariable(pos, ctx, name, dep) => {
62        write!(
63          f,
64          "Unbound free variable \"{}\" with depth {} {}",
65          name,
66          dep,
67          pretty_pos(*pos)
68        )?;
69        if !ctx.is_empty() {
70          writeln!(f, "• Context:")?;
71          for (n, uses, typ) in ctx {
72            writeln!(f, "  - {} {}: {}", uses, n, typ)?;
73          }
74        }
75        Ok(())
76      }
77      CheckError::UndefinedReference(pos, name) => {
78        write!(f, "Undefined reference \"{}\" {}", name, pretty_pos(*pos))
79      }
80      CheckError::UntypedLambda(pos, ctx) => {
81        write!(f, "Untyped lambda {}", pretty_pos(*pos))?;
82        if !ctx.is_empty() {
83          writeln!(f, "• Context:")?;
84          for (n, uses, typ) in ctx {
85            writeln!(f, "  - {} {}: {}", uses, n, typ)?;
86          }
87        }
88        Ok(())
89      }
90      CheckError::UntypedData(pos, ctx) => {
91        write!(f, "Untyped data expression {}", pretty_pos(*pos))?;
92        if !ctx.is_empty() {
93          writeln!(f, "• Context:")?;
94          for (n, uses, typ) in ctx {
95            writeln!(f, "  - {} {}: {}", uses, n, typ)?;
96          }
97        }
98        Ok(())
99      }
100      CheckError::LamAllMismatch(pos, ctx, trm, typ) => {
101        writeln!(
102          f,
103          "The type of a lambda (λ) is not a forall (∀) {}",
104          pretty_pos(*pos)
105        )?;
106        if !ctx.is_empty() {
107          writeln!(f, "• Context:")?;
108          for (n, uses, typ) in ctx {
109            writeln!(f, "  - {} {}: {}", uses, n, typ)?;
110          }
111        }
112        writeln!(f, "• Checked: {}", trm)?;
113        writeln!(f, "• Against: {}", typ)?;
114        Ok(())
115      }
116      CheckError::AppFunMismatch(pos, ctx, fun, typ) => {
117        writeln!(
118          f,
119          "Tried to apply an expression which is not a function {}",
120          pretty_pos(*pos)
121        )?;
122        if !ctx.is_empty() {
123          writeln!(f, "• Context:")?;
124          for (n, uses, typ) in ctx {
125            writeln!(f, "  - {} {}: {}", uses, n, typ)?;
126          }
127        }
128        writeln!(f, "• Checked: {}", fun)?;
129        writeln!(f, "• Against: {}", typ)?;
130        Ok(())
131      }
132      CheckError::CseDatMismatch(pos, ctx, dat, typ) => {
133        writeln!(
134          f,
135          "Tried to case match on an expression which is not an inductive \
136           datatype or literal {}",
137          pretty_pos(*pos)
138        )?;
139        if !ctx.is_empty() {
140          writeln!(f, "• Context:")?;
141          for (n, uses, typ) in ctx {
142            writeln!(f, "  - {} {}: {}", uses, n, typ)?;
143          }
144        }
145        writeln!(f, "• Checked: {}", dat)?;
146        writeln!(f, "• Against: {}", typ)?;
147        Ok(())
148      }
149      CheckError::NonInductiveLitType(pos, ctx, typ) => {
150        writeln!(
151          f,
152          "{} is not an inductive literal {}",
153          typ,
154          pretty_pos(*pos)
155        )?;
156        if !ctx.is_empty() {
157          writeln!(f, "• Context:")?;
158          for (n, uses, typ) in ctx {
159            writeln!(f, "  - {} {}: {}", uses, n, typ)?;
160          }
161        }
162        Ok(())
163      }
164      CheckError::DatSlfMismatch(pos, ctx, trm, typ) => {
165        writeln!(
166          f,
167          "The type of a data constructor is not a self-type {}",
168          pretty_pos(*pos)
169        )?;
170        if !ctx.is_empty() {
171          writeln!(f, "• Context:")?;
172          for (n, uses, typ) in ctx {
173            writeln!(f, "  - {} {}: {}", uses, n, typ)?;
174          }
175        }
176        writeln!(f, "• Checked: {}", trm)?;
177        writeln!(f, "• Against: {}", typ)?;
178        Ok(())
179      }
180      CheckError::QuantityTooLittle(pos, ctx, nam, exp, det) => {
181        writeln!(f, "Variable `{}` not used enough {}", nam, pretty_pos(*pos))?;
182        if !ctx.is_empty() {
183          writeln!(f, "• Context:")?;
184          for (n, uses, typ) in ctx {
185            writeln!(f, "  - {} {}: {}", uses, n, typ)?;
186          }
187        }
188        writeln!(f, "• Expected: {}", exp)?;
189        writeln!(f, "• Detected: {}", det)?;
190        Ok(())
191      }
192      CheckError::QuantityTooMuch(pos, ctx, nam, exp, det) => {
193        writeln!(f, "Variable `{}` used too much {}", nam, pretty_pos(*pos))?;
194        if !ctx.is_empty() {
195          writeln!(f, "• Context:")?;
196          for (n, uses, typ) in ctx {
197            writeln!(f, "  - {} {}: {}", uses, n, typ)?;
198          }
199        }
200        writeln!(f, "• Expected: {}", exp)?;
201        writeln!(f, "• Detected: {}", det)?;
202        Ok(())
203      }
204      CheckError::TypeMismatch(pos, ctx, exp, det) => {
205        writeln!(f, "Type Mismatch {}", pretty_pos(*pos))?;
206        if !ctx.is_empty() {
207          writeln!(f, "• Context:")?;
208          for (n, uses, typ) in ctx {
209            writeln!(f, "  - {} {}: {}", uses, n, typ)?;
210          }
211        }
212        writeln!(f, "• Expected: {}", exp)?;
213        writeln!(f, "• Detected: {}", det)?;
214        Ok(())
215      }
216      CheckError::GenericError(pos, ctx, msg) => {
217        writeln!(f, "{} {} ", msg, pretty_pos(*pos))?;
218        if !ctx.is_empty() {
219          write!(f, "With context:\n{} ", pretty_context(ctx))?;
220        }
221        Ok(())
222      }
223    }
224  }
225}
yatima_core/check/error.rs

yatima_core/check/
error.rs
