summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/context.rs7
-rw-r--r--dhall/src/core.rs6
-rw-r--r--dhall/src/grammar_util.rs4
-rw-r--r--dhall/src/lexer.rs108
-rw-r--r--dhall/src/main.rs35
-rw-r--r--dhall/src/parser.rs16
-rw-r--r--dhall/src/typecheck.rs650
7 files changed, 535 insertions, 291 deletions
diff --git a/dhall/src/context.rs b/dhall/src/context.rs
index c2e1913..b88a677 100644
--- a/dhall/src/context.rs
+++ b/dhall/src/context.rs
@@ -34,7 +34,12 @@ impl<'i, T> Context<'i, T> {
}
pub fn map<U, F: Fn(&T) -> U>(&self, f: F) -> Context<'i, U> {
- Context(self.0.iter().map(|(k, v)| (*k, v.iter().map(&f).collect())).collect())
+ Context(
+ self.0
+ .iter()
+ .map(|(k, v)| (*k, v.iter().map(&f).collect()))
+ .collect(),
+ )
}
}
diff --git a/dhall/src/core.rs b/dhall/src/core.rs
index a0e686d..340cb04 100644
--- a/dhall/src/core.rs
+++ b/dhall/src/core.rs
@@ -1078,8 +1078,10 @@ where
}
(App(box Builtin(OptionalBuild), a0), g) => {
let e2: Expr<_, _> = app(app(app(g,
- App(bx(Builtin(Optional)), a0.clone())),
- Lam("x", a0.clone(), bx(OptionalLit(Some(a0.clone()), vec![Var(V("x", 0))])))), OptionalLit(Some(a0), vec![]));
+ App(bx(Builtin(Optional)), a0.clone())),
+ Lam("x", a0.clone(),
+ bx(OptionalLit(Some(a0.clone()), vec![Var(V("x", 0))])))),
+ OptionalLit(Some(a0), vec![]));
normalize(&e2)
}
(f2, a2) => app(f2, a2),
diff --git a/dhall/src/grammar_util.rs b/dhall/src/grammar_util.rs
index c185632..ce73444 100644
--- a/dhall/src/grammar_util.rs
+++ b/dhall/src/grammar_util.rs
@@ -3,5 +3,5 @@ use crate::core::{Expr, X};
pub type ParsedExpr<'i> = Expr<'i, X, X>; // FIXME Parse paths and replace the second X with Path
pub type BoxExpr<'i> = Box<ParsedExpr<'i>>;
pub type ExprOpFn<'i> = fn(BoxExpr<'i>, BoxExpr<'i>) -> ParsedExpr<'i>;
-pub type ExprListFn<'i> = fn(Option<BoxExpr<'i>>, Vec<ParsedExpr<'i>>) -> ParsedExpr<'i>;
-
+pub type ExprListFn<'i> =
+ fn(Option<BoxExpr<'i>>, Vec<ParsedExpr<'i>>) -> ParsedExpr<'i>;
diff --git a/dhall/src/lexer.rs b/dhall/src/lexer.rs
index b5cbe6b..5fc0f05 100644
--- a/dhall/src/lexer.rs
+++ b/dhall/src/lexer.rs
@@ -1,8 +1,8 @@
use nom::*;
-use crate::core::Const;
use crate::core::Builtin;
use crate::core::Builtin::*;
+use crate::core::Const;
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Keyword {
@@ -74,11 +74,13 @@ fn is_identifier_rest_char(c: char) -> bool {
macro_rules! digits {
($i:expr, $t:tt, $radix:expr) => {{
- let r: nom::IResult<&str, $t> =
- map_res!($i, take_while1_s!(call!(|c: char| c.is_digit($radix))),
- |s| $t::from_str_radix(s, $radix));
+ let r: nom::IResult<&str, $t> = map_res!(
+ $i,
+ take_while1_s!(call!(|c: char| c.is_digit($radix))),
+ |s| $t::from_str_radix(s, $radix)
+ );
r
- }}
+ }};
}
named!(natural<&str, usize>, digits!(usize, 10));
@@ -105,29 +107,32 @@ macro_rules! ident_tag {
if s == $tag {
nom::IResult::Done(i, s)
} else {
- nom::IResult::Error(error_position!(nom::ErrorKind::Tag, $i))
+ nom::IResult::Error(error_position!(
+ nom::ErrorKind::Tag,
+ $i
+ ))
}
}
r => r,
}
- }
+ };
}
fn string_escape_single(c: char) -> Option<&'static str> {
match c {
- 'n' => Some("\n"),
- 'r' => Some("\r"),
- 't' => Some("\t"),
- '"' => Some("\""),
+ 'n' => Some("\n"),
+ 'r' => Some("\r"),
+ 't' => Some("\t"),
+ '"' => Some("\""),
'\'' => Some("'"),
'\\' => Some("\\"),
- '0' => Some("\0"),
- 'a' => Some("\x07"),
- 'b' => Some("\x08"),
- 'f' => Some("\x0c"),
- 'v' => Some("\x0b"),
- '&' => Some(""),
- _ => None,
+ '0' => Some("\0"),
+ 'a' => Some("\x07"),
+ 'b' => Some("\x08"),
+ 'f' => Some("\x0c"),
+ 'v' => Some("\x0b"),
+ '&' => Some(""),
+ _ => None,
}
}
@@ -138,41 +143,53 @@ named!(string_escape_numeric<&str, char>, map_opt!(alt!(
), ::std::char::from_u32));
fn string_lit_inner(input: &str) -> nom::IResult<&str, String> {
- use nom::IResult::*;;
use nom::ErrorKind;
+ use nom::IResult::*; ;
let mut s = String::new();
let mut cs = input.char_indices().peekable();
- while let Some((i, c)) = cs.next() {
+ while let Some((i, c)) = cs.next() {
match c {
'"' => return nom::IResult::Done(&input[i..], s),
'\\' => match cs.next() {
Some((_, s)) if s.is_whitespace() => {
- while cs.peek().map(|&(_, s)| s.is_whitespace()) == Some(true) {
+ while cs.peek().map(|&(_, s)| s.is_whitespace())
+ == Some(true)
+ {
let _ = cs.next();
}
if cs.next().map(|p| p.1) != Some('\\') {
- return Error(error_position!(ErrorKind::Custom(4 /* FIXME */), input));
+ return Error(error_position!(
+ ErrorKind::Custom(4 /* FIXME */),
+ input
+ ));
}
}
Some((j, ec)) => {
if let Some(esc) = string_escape_single(ec) {
s.push_str(esc);
- // FIXME Named ASCII escapes and control character escapes
+ // FIXME Named ASCII escapes and control character escapes
} else {
match string_escape_numeric(&input[j..]) {
Done(rest, esc) => {
let &(k, _) = cs.peek().unwrap();
// digits are always single byte ASCII characters
let consumed = input[k..].len() - rest.len();
- for _ in 0..consumed { let _ = cs.next(); }
+ for _ in 0..consumed {
+ let _ = cs.next();
+ }
s.push(esc);
}
Incomplete(s) => return Incomplete(s),
Error(e) => return Error(e),
}
}
- },
- _ => return Error(error_position!(ErrorKind::Custom(5 /* FIXME */), input)),
+ }
+ _ => {
+ return Error(error_position!(
+ ErrorKind::Custom(5 /* FIXME */),
+ input
+ ));
+ }
},
_ => s.push(c),
}
@@ -303,7 +320,8 @@ impl<'input> Lexer<'input> {
"{-" => find_end(input, "-}"),
"--" => find_end(input, "\n"), // Also skips past \r\n (CRLF)
_ => None,
- }.unwrap_or(0);
+ }
+ .unwrap_or(0);
// println!("skipped {} bytes of comment", skip);
self.offset += skip;
skip != 0
@@ -337,9 +355,7 @@ impl<'input> Iterator for Lexer<'input> {
self.offset = self.input.len();
Some(Err(LexicalError::Error(offset, e)))
}
- Incomplete(needed) => {
- Some(Err(LexicalError::Incomplete(needed)))
- }
+ Incomplete(needed) => Some(Err(LexicalError::Incomplete(needed))),
}
}
}
@@ -348,23 +364,31 @@ impl<'input> Iterator for Lexer<'input> {
fn test_lex() {
use self::Tok::*;
let s = "λ(b : Bool) → b == False";
- let expected = [Lambda,
- ParenL,
- Identifier("b"),
- Ascription,
- Builtin(crate::core::Builtin::Bool),
- ParenR,
- Arrow,
- Identifier("b"),
- CompareEQ,
- Bool(false)];
+ let expected = [
+ Lambda,
+ ParenL,
+ Identifier("b"),
+ Ascription,
+ Builtin(crate::core::Builtin::Bool),
+ ParenR,
+ Arrow,
+ Identifier("b"),
+ CompareEQ,
+ Bool(false),
+ ];
let lexer = Lexer::new(s);
let tokens = lexer.map(|r| r.unwrap().1).collect::<Vec<_>>();
assert_eq!(&tokens, &expected);
assert_eq!(string_lit(r#""a\&b""#).to_result(), Ok("ab".to_owned()));
- assert_eq!(string_lit(r#""a\ \b""#).to_result(), Ok("ab".to_owned()));
+ assert_eq!(
+ string_lit(r#""a\ \b""#).to_result(),
+ Ok("ab".to_owned())
+ );
assert!(string_lit(r#""a\ b""#).is_err());
assert_eq!(string_lit(r#""a\nb""#).to_result(), Ok("a\nb".to_owned()));
- assert_eq!(string_lit(r#""\o141\x62\99""#).to_result(), Ok("abc".to_owned()));
+ assert_eq!(
+ string_lit(r#""\o141\x62\99""#).to_result(),
+ Ok("abc".to_owned())
+ );
}
diff --git a/dhall/src/main.rs b/dhall/src/main.rs
index 58826bb..78a2905 100644
--- a/dhall/src/main.rs
+++ b/dhall/src/main.rs
@@ -1,5 +1,5 @@
-use std::io::{self, Read};
use std::error::Error;
+use std::io::{self, Read};
use term_painter::ToStyle;
use dhall::*;
@@ -42,9 +42,13 @@ fn print_error(message: &str, source: &str, start: usize, end: usize) {
BOLD.with(|| {
print!("{:w$} |", "", w = line_number_width);
ERROR_STYLE.with(|| {
- println!(" {:so$}{:^>ew$}", "", "",
- so = source[line_start..start].chars().count(),
- ew = ::std::cmp::max(1, source[start..end].chars().count()));
+ println!(
+ " {:so$}{:^>ew$}",
+ "",
+ "",
+ so = source[line_start..start].chars().count(),
+ ew = ::std::cmp::max(1, source[start..end].chars().count())
+ );
});
});
}
@@ -54,12 +58,27 @@ fn main() {
io::stdin().read_to_string(&mut buffer).unwrap();
let expr = match parser::parse_expr_lalrpop(&buffer) {
Ok(e) => e,
- Err(lalrpop_util::ParseError::User { error: lexer::LexicalError::Error(pos, e) }) => {
- print_error(&format!("Unexpected token {:?}", e), &buffer, pos, pos);
+ Err(lalrpop_util::ParseError::User {
+ error: lexer::LexicalError::Error(pos, e),
+ }) => {
+ print_error(
+ &format!("Unexpected token {:?}", e),
+ &buffer,
+ pos,
+ pos,
+ );
return;
}
- Err(lalrpop_util::ParseError::UnrecognizedToken { token: Some((start, t, end)), expected: e }) => {
- print_error(&format!("Unrecognized token {:?}", t), &buffer, start, end);
+ Err(lalrpop_util::ParseError::UnrecognizedToken {
+ token: Some((start, t, end)),
+ expected: e,
+ }) => {
+ print_error(
+ &format!("Unrecognized token {:?}", t),
+ &buffer,
+ start,
+ end,
+ );
if !e.is_empty() {
println!("Expected {:?}", e);
}
diff --git a/dhall/src/parser.rs b/dhall/src/parser.rs
index 303e2ad..6b20c01 100644
--- a/dhall/src/parser.rs
+++ b/dhall/src/parser.rs
@@ -7,7 +7,7 @@ use pest::Parser;
use dhall_parser::{DhallParser, Rule};
use crate::core;
-use crate::core::{bx, Builtin, Const, Expr, BinOp, V};
+use crate::core::{bx, BinOp, Builtin, Const, Expr, V};
use crate::grammar;
use crate::grammar_util::{BoxExpr, ParsedExpr};
use crate::lexer::{Lexer, LexicalError, Tok};
@@ -762,8 +762,8 @@ pub fn parse_expr_pest(s: &str) -> ParseResult<BoxExpr> {
#[test]
fn test_parse() {
- use crate::core::Expr::*;
use crate::core::BinOp::*;
+ use crate::core::Expr::*;
// let expr = r#"{ x = "foo", y = 4 }.x"#;
// let expr = r#"(1 + 2) * 3"#;
let expr = r#"if True then 1 + 3 * 5 else 2"#;
@@ -790,9 +790,11 @@ fn test_parse() {
assert!(parse_expr_lalrpop("(22)").is_ok());
assert_eq!(
parse_expr_lalrpop("3 + 5 * 10").ok(),
- Some(Box::new(BinOp(NaturalPlus,
+ Some(Box::new(BinOp(
+ NaturalPlus,
Box::new(NaturalLit(3)),
- Box::new(BinOp(NaturalTimes,
+ Box::new(BinOp(
+ NaturalTimes,
Box::new(NaturalLit(5)),
Box::new(NaturalLit(10))
))
@@ -801,9 +803,11 @@ fn test_parse() {
// The original parser is apparently right-associative
assert_eq!(
parse_expr_lalrpop("2 * 3 * 4").ok(),
- Some(Box::new(BinOp(NaturalTimes,
+ Some(Box::new(BinOp(
+ NaturalTimes,
Box::new(NaturalLit(2)),
- Box::new(BinOp(NaturalTimes,
+ Box::new(BinOp(
+ NaturalTimes,
Box::new(NaturalLit(3)),
Box::new(NaturalLit(4))
))
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 90e5f55..976293d 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -5,15 +5,17 @@ use std::fmt;
use crate::context::Context;
use crate::core;
-use crate::core::{Expr, V, X, bx, normalize, shift, subst};
-use crate::core::{pi, app};
use crate::core::Builtin::*;
use crate::core::Const::*;
use crate::core::Expr::*;
+use crate::core::{app, pi};
+use crate::core::{bx, normalize, shift, subst, Expr, V, X};
use self::TypeMessage::*;
-fn axiom<'i, S: Clone>(c: core::Const) -> Result<core::Const, TypeError<'i, S>> {
+fn axiom<'i, S: Clone>(
+ c: core::Const,
+) -> Result<core::Const, TypeError<'i, S>> {
match c {
Type => Ok(Kind),
Kind => Err(TypeError::new(&Context::new(), &Const(Kind), Untyped)),
@@ -24,8 +26,7 @@ fn rule(a: core::Const, b: core::Const) -> Result<core::Const, ()> {
match (a, b) {
(Type, Kind) => Err(()),
(Kind, Kind) => Ok(Kind),
- (Type, Type) |
- (Kind, Type) => Ok(Type),
+ (Type, Type) | (Kind, Type) => Ok(Type),
}
}
@@ -33,7 +34,11 @@ fn match_vars(vl: &V, vr: &V, ctx: &[(&str, &str)]) -> bool {
let xxs = ctx.get(0).map(|x| (x, ctx.split_at(1).1));
match (vl, vr, xxs) {
(&V(xL, nL), &V(xR, nR), None) => xL == xR && nL == nR,
- (&V(xL, 0), &V(xR, 0), Some((&(xL2, xR2), _))) if xL == xL2 && xR == xR2 => true,
+ (&V(xL, 0), &V(xR, 0), Some((&(xL2, xR2), _)))
+ if xL == xL2 && xR == xR2 =>
+ {
+ true
+ }
(&V(xL, nL), &V(xR, nR), Some((&(xL2, xR2), xs))) => {
let nL2 = if xL == xL2 { nL - 1 } else { nL };
let nR2 = if xR == xR2 { nR - 1 } else { nR };
@@ -43,16 +48,21 @@ fn match_vars(vl: &V, vr: &V, ctx: &[(&str, &str)]) -> bool {
}
fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
- where S: Clone + ::std::fmt::Debug,
- T: Clone + ::std::fmt::Debug
+where
+ S: Clone + ::std::fmt::Debug,
+ T: Clone + ::std::fmt::Debug,
{
- fn go<'i, S, T>(ctx: &mut Vec<(&'i str, &'i str)>, el: &'i Expr<'i, S, X>, er: &'i Expr<'i, T, X>) -> bool
- where S: Clone + ::std::fmt::Debug,
- T: Clone + ::std::fmt::Debug
+ fn go<'i, S, T>(
+ ctx: &mut Vec<(&'i str, &'i str)>,
+ el: &'i Expr<'i, S, X>,
+ er: &'i Expr<'i, T, X>,
+ ) -> bool
+ where
+ S: Clone + ::std::fmt::Debug,
+ T: Clone + ::std::fmt::Debug,
{
match (el, er) {
- (&Const(Type), &Const(Type)) |
- (&Const(Kind), &Const(Kind)) => true,
+ (&Const(Type), &Const(Type)) | (&Const(Kind), &Const(Kind)) => true,
(&Var(ref vL), &Var(ref vR)) => match_vars(vL, vR, &*ctx),
(&Pi(xL, ref tL, ref bL), &Pi(xR, ref tR, ref bR)) => {
//ctx <- State.get
@@ -68,8 +78,13 @@ fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
false
}
}
- (&App(ref fL, ref aL), &App(ref fR, ref aR)) =>
- if go(ctx, fL, fR) { go(ctx, aL, aR) } else { false },
+ (&App(ref fL, ref aL), &App(ref fR, ref aR)) => {
+ if go(ctx, fL, fR) {
+ go(ctx, aL, aR)
+ } else {
+ false
+ }
+ }
(&Builtin(a), &Builtin(b)) => a == b,
(&Record(ref ktsL0), &Record(ref ktsR0)) => {
if ktsL0.len() != ktsR0.len() {
@@ -97,28 +112,30 @@ fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
}
true
*/
- !ktsL0.iter().zip(ktsR0.iter()).any(|((kL, tL), (kR, tR))| {
- kL != kR || !go(ctx, tL, tR)
- })
+ !ktsL0
+ .iter()
+ .zip(ktsR0.iter())
+ .any(|((kL, tL), (kR, tR))| kL != kR || !go(ctx, tL, tR))
}
(&Union(ref ktsL0), &Union(ref ktsR0)) => {
if ktsL0.len() != ktsR0.len() {
return false;
}
- /*
- let loop ((kL, tL):ktsL) ((kR, tR):ktsR)
- | kL == kR = do
- b <- go tL tR
- if b
- then loop ktsL ktsR
- else return False
- loop [] [] = return True
- loop _ _ = return False
- loop (Data.Map.toList ktsL0) (Data.Map.toList ktsR0)
- */
- !ktsL0.iter().zip(ktsR0.iter()).any(|((kL, tL), (kR, tR))| {
- kL != kR || !go(ctx, tL, tR)
- })
+ /*
+ let loop ((kL, tL):ktsL) ((kR, tR):ktsR)
+ | kL == kR = do
+ b <- go tL tR
+ if b
+ then loop ktsL ktsR
+ else return False
+ loop [] [] = return True
+ loop _ _ = return False
+ loop (Data.Map.toList ktsL0) (Data.Map.toList ktsR0)
+ */
+ !ktsL0
+ .iter()
+ .zip(ktsR0.iter())
+ .any(|((kL, tL), (kR, tR))| kL != kR || !go(ctx, tL, tR))
}
(_, _) => false,
}
@@ -127,15 +144,17 @@ fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
go::<S, T>(&mut ctx, &normalize(eL0), &normalize(eR0))
}
-fn op2_type<'i, S, EF>(ctx: &Context<'i, Expr<'i, S, X>>,
- e: &Expr<'i, S, X>,
- t: core::Builtin,
- ef: EF,
- l: &Expr<'i, S, X>,
- r: &Expr<'i, S, X>)
- -> Result<Expr<'i, S, X>, TypeError<'i, S>>
- where S: Clone + ::std::fmt::Debug + 'i,
- EF: FnOnce(Expr<'i, S, X>, Expr<'i, S, X>) -> TypeMessage<'i, S>,
+fn op2_type<'i, S, EF>(
+ ctx: &Context<'i, Expr<'i, S, X>>,
+ e: &Expr<'i, S, X>,
+ t: core::Builtin,
+ ef: EF,
+ l: &Expr<'i, S, X>,
+ r: &Expr<'i, S, X>,
+) -> Result<Expr<'i, S, X>, TypeError<'i, S>>
+where
+ S: Clone + ::std::fmt::Debug + 'i,
+ EF: FnOnce(Expr<'i, S, X>, Expr<'i, S, X>) -> TypeMessage<'i, S>,
{
let tl = normalize(&type_with(ctx, l)?);
match tl {
@@ -158,10 +177,12 @@ fn op2_type<'i, S, EF>(ctx: &Context<'i, Expr<'i, S, X>>,
/// `type_with` does not necessarily normalize the type since full normalization
/// is not necessary for just type-checking. If you actually care about the
/// returned type then you may want to `normalize` it afterwards.
-pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
- e: &Expr<'i, S, X>)
- -> Result<Expr<'i, S, X>, TypeError<'i, S>>
- where S: Clone + ::std::fmt::Debug + 'i
+pub fn type_with<'i, S>(
+ ctx: &Context<'i, Expr<'i, S, X>>,
+ e: &Expr<'i, S, X>,
+) -> Result<Expr<'i, S, X>, TypeError<'i, S>>
+where
+ S: Clone + ::std::fmt::Debug + 'i,
{
use crate::BinOp::*;
match *e {
@@ -173,7 +194,9 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
.ok_or_else(|| TypeError::new(ctx, e, UnboundVariable))
}
Lam(x, ref tA, ref b) => {
- let ctx2 = ctx.insert(x, (**tA).clone()).map(|e| core::shift(1, V(x, 0), e));
+ let ctx2 = ctx
+ .insert(x, (**tA).clone())
+ .map(|e| core::shift(1, V(x, 0), e));
let tB = type_with(&ctx2, b)?;
let p = Pi(x, tA.clone(), bx(tB));
let _ = type_with(ctx, &p)?;
@@ -184,18 +207,32 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
let tA2 = normalize::<S, S, X>(&type_with(ctx, tA)?);
let kA = match tA2 {
Const(k) => k,
- _ => return Err(TypeError::new(ctx, e, InvalidInputType((**tA).clone()))),
+ _ => {
+ return Err(TypeError::new(
+ ctx,
+ e,
+ InvalidInputType((**tA).clone()),
+ ));
+ }
};
- let ctx2 = ctx.insert(x, (**tA).clone()).map(|e| core::shift(1, V(x, 0), e));
+ let ctx2 = ctx
+ .insert(x, (**tA).clone())
+ .map(|e| core::shift(1, V(x, 0), e));
let tB = normalize(&type_with(&ctx2, tB)?);
let kB = match tB {
Const(k) => k,
- _ => return Err(TypeError::new(&ctx2, e, InvalidOutputType(tB))),
+ _ => {
+ return Err(TypeError::new(&ctx2, e, InvalidOutputType(tB)));
+ }
};
match rule(kA, kB) {
- Err(()) => Err(TypeError::new(ctx, e, NoDependentTypes((**tA).clone(), tB))),
+ Err(()) => Err(TypeError::new(
+ ctx,
+ e,
+ NoDependentTypes((**tA).clone(), tB),
+ )),
Ok(k) => Ok(Const(k)),
}
}
@@ -203,39 +240,49 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
let tf = normalize(&type_with(ctx, f)?);
let (x, tA, tB) = match tf {
Pi(x, tA, tB) => (x, tA, tB),
- _ => return Err(TypeError::new(ctx, e, NotAFunction((**f).clone(), tf))),
+ _ => {
+ return Err(TypeError::new(
+ ctx,
+ e,
+ NotAFunction((**f).clone(), tf),
+ ));
+ }
};
let tA2 = type_with(ctx, a)?;
if prop_equal(&tA, &tA2) {
let vx0 = V(x, 0);
- let a2 = shift::<S, S, X>( 1, vx0, a);
+ let a2 = shift::<S, S, X>(1, vx0, a);
let tB2 = subst(vx0, &a2, &tB);
let tB3 = shift::<S, S, X>(-1, vx0, &tB2);
Ok(tB3)
} else {
- let nf_A = normalize(&tA);
+ let nf_A = normalize(&tA);
let nf_A2 = normalize(&tA2);
- Err(TypeError::new(ctx, e, TypeMismatch((**f).clone(), nf_A, (**a).clone(), nf_A2)))
+ Err(TypeError::new(
+ ctx,
+ e,
+ TypeMismatch((**f).clone(), nf_A, (**a).clone(), nf_A2),
+ ))
}
}
Let(f, ref mt, ref r, ref b) => {
- let tR = type_with(ctx, r)?;
+ let tR = type_with(ctx, r)?;
let ttR = normalize::<S, S, X>(&type_with(ctx, &tR)?);
- let kR = match ttR {
+ let kR = match ttR {
Const(k) => k,
// Don't bother to provide a `let`-specific version of this error
// message because this should never happen anyway
- _ => return Err(TypeError::new(ctx, e, InvalidInputType(tR))),
+ _ => return Err(TypeError::new(ctx, e, InvalidInputType(tR))),
};
let ctx2 = ctx.insert(f, tR.clone());
- let tB = type_with(&ctx2, b)?;
+ let tB = type_with(&ctx2, b)?;
let ttB = normalize::<S, S, X>(&type_with(ctx, &tB)?);
- let kB = match ttB {
+ let kB = match ttB {
Const(k) => k,
// Don't bother to provide a `let`-specific version of this error
// message because this should never happen anyway
- _ => return Err(TypeError::new(ctx, e, InvalidOutputType(tB))),
+ _ => return Err(TypeError::new(ctx, e, InvalidOutputType(tB))),
};
if let Err(()) = rule(kR, kB) {
@@ -243,10 +290,14 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
}
if let Some(ref t) = *mt {
- let nf_t = normalize(t);
+ let nf_t = normalize(t);
let nf_tR = normalize(&tR);
if !prop_equal(&nf_tR, &nf_t) {
- return Err(TypeError::new(ctx, e, AnnotMismatch((**r).clone(), nf_t, nf_tR)));
+ return Err(TypeError::new(
+ ctx,
+ e,
+ AnnotMismatch((**r).clone(), nf_t, nf_tR),
+ ));
}
}
@@ -260,9 +311,13 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
if prop_equal(t, &t2) {
Ok((**t).clone())
} else {
- let nf_t = normalize(t);
+ let nf_t = normalize(t);
let nf_t2 = normalize(&t2);
- Err(TypeError::new(ctx, e, AnnotMismatch((**x).clone(), nf_t, nf_t2)))
+ Err(TypeError::new(
+ ctx,
+ e,
+ AnnotMismatch((**x).clone(), nf_t, nf_t2),
+ ))
}
}
BoolLit(_) => Ok(Builtin(Bool)),
@@ -274,48 +329,91 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
let tx = normalize(&type_with(ctx, x)?);
match tx {
Builtin(Bool) => {}
- _ => return Err(TypeError::new(ctx, e, InvalidPredicate((**x).clone(), tx))),
+ _ => {
+ return Err(TypeError::new(
+ ctx,
+ e,
+ InvalidPredicate((**x).clone(), tx),
+ ));
+ }
}
let ty = normalize(&type_with(ctx, y)?);
let tty = normalize(&type_with(ctx, &ty)?);
match tty {
Const(Type) => {}
- _ => return Err(TypeError::new(ctx, e, IfBranchMustBeTerm(true, (**y).clone(), ty, tty))),
+ _ => {
+ return Err(TypeError::new(
+ ctx,
+ e,
+ IfBranchMustBeTerm(true, (**y).clone(), ty, tty),
+ ));
+ }
}
let tz = normalize(&type_with(ctx, z)?);
let ttz = normalize(&type_with(ctx, &tz)?);
match ttz {
Const(Type) => {}
- _ => return Err(TypeError::new(ctx, e, IfBranchMustBeTerm(false, (**z).clone(), tz, ttz))),
+ _ => {
+ return Err(TypeError::new(
+ ctx,
+ e,
+ IfBranchMustBeTerm(false, (**z).clone(), tz, ttz),
+ ));
+ }
}
if !prop_equal(&ty, &tz) {
- return Err(TypeError::new(ctx, e, IfBranchMismatch((**y).clone(), (**z).clone(), ty, tz)));
+ return Err(TypeError::new(
+ ctx,
+ e,
+ IfBranchMismatch((**y).clone(), (**z).clone(), ty, tz),
+ ));
}
Ok(ty)
}
NaturalLit(_) => Ok(Builtin(Natural)),
- Builtin(NaturalFold) =>
- Ok(pi("_", Natural,
- pi("natural", Const(Type),
- pi("succ", pi("_", "natural", "natural"),
- pi("zero", "natural", "natural"))))),
- Builtin(NaturalBuild) =>
- Ok(pi("_",
- pi("natural", Const(Type),
- pi("succ", pi("_", "natural", "natural"),
- pi("zero", "natural", "natural"))),
- Natural)),
- Builtin(NaturalIsZero) |
- Builtin(NaturalEven) |
- Builtin(NaturalOdd) => Ok(pi("_", Natural, Bool)),
- BinOp(NaturalPlus, ref l, ref r) => op2_type(ctx, e, Natural, CantAdd, l, r),
- BinOp(NaturalTimes, ref l, ref r) => op2_type(ctx, e, Natural, CantMultiply, l, r),
+ Builtin(NaturalFold) => Ok(pi(
+ "_",
+ Natural,
+ pi(
+ "natural",
+ Const(Type),
+ pi(
+ "succ",
+ pi("_", "natural", "natural"),
+ pi("zero", "natural", "natural"),
+ ),
+ ),
+ )),
+ Builtin(NaturalBuild) => Ok(pi(
+ "_",
+ pi(
+ "natural",
+ Const(Type),
+ pi(
+ "succ",
+ pi("_", "natural", "natural"),
+ pi("zero", "natural", "natural"),
+ ),
+ ),
+ Natural,
+ )),
+ Builtin(NaturalIsZero) | Builtin(NaturalEven) | Builtin(NaturalOdd) => {
+ Ok(pi("_", Natural, Bool))
+ }
+ BinOp(NaturalPlus, ref l, ref r) => {
+ op2_type(ctx, e, Natural, CantAdd, l, r)
+ }
+ BinOp(NaturalTimes, ref l, ref r) => {
+ op2_type(ctx, e, Natural, CantMultiply, l, r)
+ }
IntegerLit(_) => Ok(Builtin(Integer)),
DoubleLit(_) => Ok(Builtin(Double)),
TextLit(_) => Ok(Builtin(Text)),
- BinOp(TextAppend, ref l, ref r) => op2_type(ctx, e, Text, CantTextAppend, l, r),
+ BinOp(TextAppend, ref l, ref r) => {
+ op2_type(ctx, e, Text, CantTextAppend, l, r)
+ }
ListLit(ref t, ref xs) => {
let mut iter = xs.iter().enumerate();
let t: Box<Expr<_, _>> = match t {
@@ -323,7 +421,7 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
None => {
let (_, first_x) = iter.next().unwrap();
bx(type_with(ctx, first_x)?)
- },
+ }
};
let s = normalize::<_, S, _>(&type_with(ctx, &t)?);
@@ -334,39 +432,74 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
for (i, x) in iter {
let t2 = type_with(ctx, x)?;
if !prop_equal(&t, &t2) {
- let nf_t = normalize(&t);
+ let nf_t = normalize(&t);
let nf_t2 = normalize(&t2);
- return Err(TypeError::new(ctx, e, InvalidListElement(i, nf_t, x.clone(), nf_t2)) )
+ return Err(TypeError::new(
+ ctx,
+ e,
+ InvalidListElement(i, nf_t, x.clone(), nf_t2),
+ ));
}
}
Ok(App(bx(Builtin(List)), t))
}
- Builtin(ListBuild) =>
- Ok(pi("a", Const(Type),
- pi("_",
- pi("list", Const(Type),
- pi("cons", pi("_", "a", pi("_", "list", "list")),
- pi("nil", "list", "list"))),
- app(List, "a")))),
- Builtin(ListFold) =>
- Ok(pi("a", Const(Type),
- pi("_", app(List, "a"),
- pi("list", Const(Type),
- pi("cons", pi("_", "a", pi("_", "list", "list")),
- pi("nil", "list", "list")))))),
- Builtin(ListLength) =>
- Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural))),
- Builtin(ListHead) |
- Builtin(ListLast) =>
- Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(Optional, "a")))),
+ Builtin(ListBuild) => Ok(pi(
+ "a",
+ Const(Type),
+ pi(
+ "_",
+ pi(
+ "list",
+ Const(Type),
+ pi(
+ "cons",
+ pi("_", "a", pi("_", "list", "list")),
+ pi("nil", "list", "list"),
+ ),
+ ),
+ app(List, "a"),
+ ),
+ )),
+ Builtin(ListFold) => Ok(pi(
+ "a",
+ Const(Type),
+ pi(
+ "_",
+ app(List, "a"),
+ pi(
+ "list",
+ Const(Type),
+ pi(
+ "cons",
+ pi("_", "a", pi("_", "list", "list")),
+ pi("nil", "list", "list"),
+ ),
+ ),
+ ),
+ )),
+ Builtin(ListLength) => {
+ Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural)))
+ }
+ Builtin(ListHead) | Builtin(ListLast) => Ok(pi(
+ "a",
+ Const(Type),
+ pi("_", app(List, "a"), app(Optional, "a")),
+ )),
Builtin(ListIndexed) => {
let mut m = BTreeMap::new();
m.insert("index", Builtin(Natural));
m.insert("value", Expr::from("a"));
- Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(List, Record(m)))))
+ Ok(pi(
+ "a",
+ Const(Type),
+ pi("_", app(List, "a"), app(List, Record(m))),
+ ))
}
- Builtin(ListReverse) =>
- Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(List, "a")))),
+ Builtin(ListReverse) => Ok(pi(
+ "a",
+ Const(Type),
+ pi("_", app(List, "a"), app(List, "a")),
+ )),
OptionalLit(ref t, ref xs) => {
let mut iter = xs.iter();
let t: Box<Expr<_, _>> = match t {
@@ -374,13 +507,15 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
None => {
let first_x = iter.next().unwrap();
bx(type_with(ctx, first_x)?)
- },
+ }
};
let s = normalize::<_, S, _>(&type_with(ctx, &t)?);
match s {
Const(Type) => {}
- _ => return Err(TypeError::new(ctx, e, InvalidOptionalType(*t))),
+ _ => {
+ return Err(TypeError::new(ctx, e, InvalidOptionalType(*t)));
+ }
}
let n = xs.len();
if 2 <= n {
@@ -389,140 +524,180 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
for x in iter {
let t2 = type_with(ctx, x)?;
if !prop_equal(&t, &t2) {
- let nf_t = normalize(&t);
+ let nf_t = normalize(&t);
let nf_t2 = normalize(&t2);
- return Err(TypeError::new(ctx, e, InvalidOptionalElement(nf_t, x.clone(), nf_t2)));
+ return Err(TypeError::new(
+ ctx,
+ e,
+ InvalidOptionalElement(nf_t, x.clone(), nf_t2),
+ ));
}
}
Ok(App(bx(Builtin(Optional)), t))
}
- Builtin(OptionalFold) =>
- Ok(pi("a", Const(Type),
- pi("_", app(Optional, "a"),
- pi("optional", Const(Type),
- pi("just", pi("_", "a", "optional"),
- pi("nothing", "optional", "optional")))))),
- Builtin(List) | Builtin(Optional) =>
- Ok(pi("_", Const(Type), Const(Type))),
- Builtin(Bool) | Builtin(Natural) | Builtin(Integer) | Builtin(Double) | Builtin(Text) =>
- Ok(Const(Type)),
+ Builtin(OptionalFold) => Ok(pi(
+ "a",
+ Const(Type),
+ pi(
+ "_",
+ app(Optional, "a"),
+ pi(
+ "optional",
+ Const(Type),
+ pi(
+ "just",
+ pi("_", "a", "optional"),
+ pi("nothing", "optional", "optional"),
+ ),
+ ),
+ ),
+ )),
+ Builtin(List) | Builtin(Optional) => {
+ Ok(pi("_", Const(Type), Const(Type)))
+ }
+ Builtin(Bool) | Builtin(Natural) | Builtin(Integer)
+ | Builtin(Double) | Builtin(Text) => Ok(Const(Type)),
Record(ref kts) => {
for (k, t) in kts {
let s = normalize::<S, S, X>(&type_with(ctx, t)?);
match s {
Const(Type) => {}
- _ => return Err(TypeError::new(ctx, e, InvalidFieldType((*k).to_owned(), (*t).clone()))),
+ _ => {
+ return Err(TypeError::new(
+ ctx,
+ e,
+ InvalidFieldType((*k).to_owned(), (*t).clone()),
+ ));
+ }
}
}
Ok(Const(Type))
}
RecordLit(ref kvs) => {
- let kts = kvs.iter().map(|(&k, v)| {
- let t = type_with(ctx, v)?;
- let s = normalize::<S, S, X>(&type_with(ctx, &t)?);
- match s {
- Const(Type) => {}
- _ => return Err(TypeError::new(ctx, e, InvalidField((*k).to_owned(), (*v).clone()))),
- }
- Ok((k, t))
- }).collect::<Result<_, _>>()?;
+ let kts = kvs
+ .iter()
+ .map(|(&k, v)| {
+ let t = type_with(ctx, v)?;
+ let s = normalize::<S, S, X>(&type_with(ctx, &t)?);
+ match s {
+ Const(Type) => {}
+ _ => {
+ return Err(TypeError::new(
+ ctx,
+ e,
+ InvalidField((*k).to_owned(), (*v).clone()),
+ ));
+ }
+ }
+ Ok((k, t))
+ })
+ .collect::<Result<_, _>>()?;
Ok(Record(kts))
}
-/*
-type_with ctx e@(Union kts ) = do
- let process (k, t) = do
- s <- fmap Dhall.Core.normalize (type_with ctx t)
- case s of
- Const Type -> return ()
- _ -> Left (TypeError ctx e (InvalidAlternativeType k t))
- mapM_ process (Data.Map.toList kts)
- return (Const Type)
-type_with ctx e@(UnionLit k v kts) = do
- case Data.Map.lookup k kts of
- Just _ -> Left (TypeError ctx e (DuplicateAlternative k))
- Nothing -> return ()
- t <- type_with ctx v
- let union = Union (Data.Map.insert k t kts)
- _ <- type_with ctx union
- return union
-type_with ctx e@(Combine kvsX kvsY) = do
- tKvsX <- fmap Dhall.Core.normalize (type_with ctx kvsX)
- ktsX <- case tKvsX of
- Record kts -> return kts
- _ -> Left (TypeError ctx e (MustCombineARecord kvsX tKvsX))
-
- tKvsY <- fmap Dhall.Core.normalize (type_with ctx kvsY)
- ktsY <- case tKvsY of
- Record kts -> return kts
- _ -> Left (TypeError ctx e (MustCombineARecord kvsY tKvsY))
-
- let combineTypes ktsL ktsR = do
- let ks =
- Data.Set.union (Data.Map.keysSet ktsL) (Data.Map.keysSet ktsR)
- kts <- forM (toList ks) (\k -> do
- case (Data.Map.lookup k ktsL, Data.Map.lookup k ktsR) of
- (Just (Record ktsL'), Just (Record ktsR')) -> do
- t <- combineTypes ktsL' ktsR'
- return (k, t)
- (Nothing, Just t) -> do
- return (k, t)
- (Just t, Nothing) -> do
- return (k, t)
- _ -> do
- Left (TypeError ctx e (FieldCollision k)) )
- return (Record (Data.Map.fromList kts))
-
- combineTypes ktsX ktsY
-type_with ctx e@(Merge kvsX kvsY t) = do
- tKvsX <- fmap Dhall.Core.normalize (type_with ctx kvsX)
- ktsX <- case tKvsX of
- Record kts -> return kts
- _ -> Left (TypeError ctx e (MustMergeARecord kvsX tKvsX))
- let ksX = Data.Map.keysSet ktsX
-
- tKvsY <- fmap Dhall.Core.normalize (type_with ctx kvsY)
- ktsY <- case tKvsY of
- Union kts -> return kts
- _ -> Left (TypeError ctx e (MustMergeUnion kvsY tKvsY))
- let ksY = Data.Map.keysSet ktsY
-
- let diffX = Data.Set.difference ksX ksY
- let diffY = Data.Set.difference ksY ksX
-
- if Data.Set.null diffX
- then return ()
- else Left (TypeError ctx e (UnusedHandler diffX))
-
- let process (kY, tY) = do
- case Data.Map.lookup kY ktsX of
- Nothing -> Left (TypeError ctx e (MissingHandler diffY))
- Just tX ->
- case tX of
- Pi _ tY' t' -> do
- if prop_equal tY tY'
- then return ()
- else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY'))
- if prop_equal t t'
- then return ()
- else Left (TypeError ctx e (HandlerOutputTypeMismatch kY t t'))
- _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX))
- mapM_ process (Data.Map.toList ktsY)
- return t
- */
+ /*
+ type_with ctx e@(Union kts ) = do
+ let process (k, t) = do
+ s <- fmap Dhall.Core.normalize (type_with ctx t)
+ case s of
+ Const Type -> return ()
+ _ -> Left (TypeError ctx e (InvalidAlternativeType k t))
+ mapM_ process (Data.Map.toList kts)
+ return (Const Type)
+ type_with ctx e@(UnionLit k v kts) = do
+ case Data.Map.lookup k kts of
+ Just _ -> Left (TypeError ctx e (DuplicateAlternative k))
+ Nothing -> return ()
+ t <- type_with ctx v
+ let union = Union (Data.Map.insert k t kts)
+ _ <- type_with ctx union
+ return union
+ type_with ctx e@(Combine kvsX kvsY) = do
+ tKvsX <- fmap Dhall.Core.normalize (type_with ctx kvsX)
+ ktsX <- case tKvsX of
+ Record kts -> return kts
+ _ -> Left (TypeError ctx e (MustCombineARecord kvsX tKvsX))
+
+ tKvsY <- fmap Dhall.Core.normalize (type_with ctx kvsY)
+ ktsY <- case tKvsY of
+ Record kts -> return kts
+ _ -> Left (TypeError ctx e (MustCombineARecord kvsY tKvsY))
+
+ let combineTypes ktsL ktsR = do
+ let ks =
+ Data.Set.union (Data.Map.keysSet ktsL) (Data.Map.keysSet ktsR)
+ kts <- forM (toList ks) (\k -> do
+ case (Data.Map.lookup k ktsL, Data.Map.lookup k ktsR) of
+ (Just (Record ktsL'), Just (Record ktsR')) -> do
+ t <- combineTypes ktsL' ktsR'
+ return (k, t)
+ (Nothing, Just t) -> do
+ return (k, t)
+ (Just t, Nothing) -> do
+ return (k, t)
+ _ -> do
+ Left (TypeError ctx e (FieldCollision k)) )
+ return (Record (Data.Map.fromList kts))
+
+ combineTypes ktsX ktsY
+ type_with ctx e@(Merge kvsX kvsY t) = do
+ tKvsX <- fmap Dhall.Core.normalize (type_with ctx kvsX)
+ ktsX <- case tKvsX of
+ Record kts -> return kts
+ _ -> Left (TypeError ctx e (MustMergeARecord kvsX tKvsX))
+ let ksX = Data.Map.keysSet ktsX
+
+ tKvsY <- fmap Dhall.Core.normalize (type_with ctx kvsY)
+ ktsY <- case tKvsY of
+ Union kts -> return kts
+ _ -> Left (TypeError ctx e (MustMergeUnion kvsY tKvsY))
+ let ksY = Data.Map.keysSet ktsY
+
+ let diffX = Data.Set.difference ksX ksY
+ let diffY = Data.Set.difference ksY ksX
+
+ if Data.Set.null diffX
+ then return ()
+ else Left (TypeError ctx e (UnusedHandler diffX))
+
+ let process (kY, tY) = do
+ case Data.Map.lookup kY ktsX of
+ Nothing -> Left (TypeError ctx e (MissingHandler diffY))
+ Just tX ->
+ case tX of
+ Pi _ tY' t' -> do
+ if prop_equal tY tY'
+ then return ()
+ else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY'))
+ if prop_equal t t'
+ then return ()
+ else Left (TypeError ctx e (HandlerOutputTypeMismatch kY t t'))
+ _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX))
+ mapM_ process (Data.Map.toList ktsY)
+ return t
+ */
Field(ref r, x) => {
let t = normalize(&type_with(ctx, r)?);
match t {
- Record(ref kts) =>
- kts.get(x).cloned().ok_or_else(|| TypeError::new(ctx, e, MissingField(x.to_owned(), t.clone()))),
- _ => Err(TypeError::new(ctx, e, NotARecord(x.to_owned(), (**r).clone(), t.clone()))),
+ Record(ref kts) => kts.get(x).cloned().ok_or_else(|| {
+ TypeError::new(
+ ctx,
+ e,
+ MissingField(x.to_owned(), t.clone()),
+ )
+ }),
+ _ => Err(TypeError::new(
+ ctx,
+ e,
+ NotARecord(x.to_owned(), (**r).clone(), t.clone()),
+ )),
}
}
/*
-type_with ctx (Note s e' ) = case type_with ctx e' of
- Left (TypeError ctx2 (Note s' e'') m) -> Left (TypeError ctx2 (Note s' e'') m)
- Left (TypeError ctx2 e'' m) -> Left (TypeError ctx2 (Note s e'') m)
- Right r -> Right r
-*/
+ type_with ctx (Note s e' ) = case type_with ctx e' of
+ Left (TypeError ctx2 (Note s' e'') m) -> Left (TypeError ctx2 (Note s' e'') m)
+ Left (TypeError ctx2 e'' m) -> Left (TypeError ctx2 (Note s e'') m)
+ Right r -> Right r
+ */
Embed(p) => match p {},
_ => panic!("Unimplemented typecheck case: {:?}", e),
}
@@ -531,7 +706,9 @@ type_with ctx (Note s e' ) = case type_with ctx e' of
/// `typeOf` is the same as `type_with` with an empty context, meaning that the
/// expression must be closed (i.e. no free variables), otherwise type-checking
/// will fail.
-pub fn type_of<'i, S: Clone + ::std::fmt::Debug + 'i>(e: &Expr<'i, S, X>) -> Result<Expr<'i, S, X>, TypeError<'i, S>> {
+pub fn type_of<'i, S: Clone + ::std::fmt::Debug + 'i>(
+ e: &Expr<'i, S, X>,
+) -> Result<Expr<'i, S, X>, TypeError<'i, S>> {
let ctx = Context::new();
type_with(&ctx, e) //.map(|e| e.into_owned())
}
@@ -543,7 +720,12 @@ pub enum TypeMessage<'i, S> {
InvalidInputType(Expr<'i, S, X>),
InvalidOutputType(Expr<'i, S, X>),
NotAFunction(Expr<'i, S, X>, Expr<'i, S, X>),
- TypeMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
+ TypeMismatch(
+ Expr<'i, S, X>,
+ Expr<'i, S, X>,
+ Expr<'i, S, X>,
+ Expr<'i, S, X>,
+ ),
AnnotMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
Untyped,
InvalidListElement(usize, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
@@ -552,7 +734,12 @@ pub enum TypeMessage<'i, S> {
InvalidOptionalLiteral(usize),
InvalidOptionalType(Expr<'i, S, X>),
InvalidPredicate(Expr<'i, S, X>, Expr<'i, S, X>),
- IfBranchMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
+ IfBranchMismatch(
+ Expr<'i, S, X>,
+ Expr<'i, S, X>,
+ Expr<'i, S, X>,
+ Expr<'i, S, X>,
+ ),
IfBranchMustBeTerm(bool, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
InvalidField(String, Expr<'i, S, X>),
InvalidFieldType(String, Expr<'i, S, X>),
@@ -590,10 +777,11 @@ pub struct TypeError<'i, S> {
}
impl<'i, S: Clone> TypeError<'i, S> {
- pub fn new(context: &Context<'i, Expr<'i, S, X>>,
- current: &Expr<'i, S, X>,
- type_message: TypeMessage<'i, S>)
- -> Self {
+ pub fn new(
+ context: &Context<'i, Expr<'i, S, X>>,
+ current: &Expr<'i, S, X>,
+ type_message: TypeMessage<'i, S>,
+ ) -> Self {
TypeError {
context: context.clone(),
current: current.clone(),
@@ -618,7 +806,9 @@ impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<'i, S> {
impl<'i, S> fmt::Display for TypeMessage<'i, S> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
match *self {
- UnboundVariable => f.write_str(include_str!("errors/UnboundVariable.txt")),
+ UnboundVariable => {
+ f.write_str(include_str!("errors/UnboundVariable.txt"))
+ }
TypeMismatch(ref e0, ref e1, ref e2, ref e3) => {
let template = include_str!("errors/TypeMismatch.txt");
let s = template
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 20:16:56 +0000