diff options
| -rw-r--r-- | abnf_to_pest/src/lib.rs | 81 | ||||
| -rw-r--r-- | dhall/src/context.rs | 7 | ||||
| -rw-r--r-- | dhall/src/core.rs | 6 | ||||
| -rw-r--r-- | dhall/src/grammar_util.rs | 4 | ||||
| -rw-r--r-- | dhall/src/lexer.rs | 108 | ||||
| -rw-r--r-- | dhall/src/main.rs | 35 | ||||
| -rw-r--r-- | dhall/src/parser.rs | 16 | ||||
| -rw-r--r-- | dhall/src/typecheck.rs | 650 | ||||
| -rw-r--r-- | dhall/tests/macros.rs | 55 | ||||
| -rw-r--r-- | dhall_parser/build.rs | 45 |
10 files changed, 658 insertions, 349 deletions
diff --git a/abnf_to_pest/src/lib.rs b/abnf_to_pest/src/lib.rs index 7381113..38347ed 100644 --- a/abnf_to_pest/src/lib.rs +++ b/abnf_to_pest/src/lib.rs @@ -1,5 +1,5 @@ -use std::collections::HashMap; use itertools::Itertools; +use std::collections::HashMap; pub struct PestRuleSettings { pub visible: bool, @@ -8,14 +8,23 @@ pub struct PestRuleSettings { impl Default for PestRuleSettings { fn default() -> Self { - PestRuleSettings { visible: true, replace: None } + PestRuleSettings { + visible: true, + replace: None, + } } } -pub fn abnf_to_pest(data: &Vec<u8>, rule_settings: &HashMap<String, PestRuleSettings>) -> std::io::Result<String> { +pub fn abnf_to_pest( + data: &Vec<u8>, + rule_settings: &HashMap<String, PestRuleSettings>, +) -> std::io::Result<String> { use abnf::abnf::*; - use pretty::{Doc, BoxDoc}; - fn format_rule(x: Rule, rule_settings: &HashMap<String, PestRuleSettings>) -> Doc<BoxDoc<()>> { + use pretty::{BoxDoc, Doc}; + fn format_rule( + x: Rule, + rule_settings: &HashMap<String, PestRuleSettings>, + ) -> Doc<BoxDoc<()>> { let rulename = format_rulename(x.name); let default = Default::default(); let setting = rule_settings.get(&rulename).unwrap_or(&default); @@ -36,7 +45,13 @@ pub fn abnf_to_pest(data: &Vec<u8>, rule_settings: &HashMap<String, PestRuleSett } fn format_rulename(x: String) -> String { let x = x.replace("-", "_"); - if x == "if" || x == "else" || x == "as" || x == "let" || x == "in" || x == "fn" { + if x == "if" + || x == "else" + || x == "as" + || x == "let" + || x == "in" + || x == "fn" + { x + "_" } else { x @@ -44,19 +59,27 @@ pub fn abnf_to_pest(data: &Vec<u8>, rule_settings: &HashMap<String, PestRuleSett } fn format_alternation(x: Alternation) -> Doc<'static, BoxDoc<'static, ()>> { Doc::intersperse( - x.concatenations.into_iter().map(|x| format_concatenation(x).nest(2).group()), - Doc::space().append(Doc::text("| ")) + x.concatenations + .into_iter() + .map(|x| format_concatenation(x).nest(2).group()), + Doc::space().append(Doc::text("| ")), ) } - fn format_concatenation(x: Concatenation) -> Doc<'static, BoxDoc<'static, ()>> { + fn format_concatenation( + x: Concatenation, + ) -> Doc<'static, BoxDoc<'static, ()>> { Doc::intersperse( x.repetitions.into_iter().map(format_repetition), - Doc::space().append(Doc::text("~ ")) + Doc::space().append(Doc::text("~ ")), ) } fn format_repetition(x: Repetition) -> Doc<'static, BoxDoc<'static, ()>> { - format_element(x.element) - .append(x.repeat.map(format_repeat).map(Doc::text).unwrap_or(Doc::nil())) + format_element(x.element).append( + x.repeat + .map(format_repeat) + .map(Doc::text) + .unwrap_or(Doc::nil()), + ) } fn format_repeat(x: Repeat) -> String { match (x.min.unwrap_or(0), x.max) { @@ -72,15 +95,16 @@ pub fn abnf_to_pest(data: &Vec<u8>, rule_settings: &HashMap<String, PestRuleSett use abnf::abnf::Element::*; match x { Rulename(s) => Doc::text(format_rulename(s)), - Group(g) => - Doc::text("(") - .append(format_alternation(g.alternation).nest(4).group()) - .append(Doc::text(")")), - Option(o) => - Doc::text("(") - .append(format_alternation(o.alternation).nest(4).group()) - .append(Doc::text(")?")), - CharVal(s) => Doc::text(format!("^\"{}\"", s.replace("\"", "\\\"").replace("\\", "\\\\"))), + Group(g) => Doc::text("(") + .append(format_alternation(g.alternation).nest(4).group()) + .append(Doc::text(")")), + Option(o) => Doc::text("(") + .append(format_alternation(o.alternation).nest(4).group()) + .append(Doc::text(")?")), + CharVal(s) => Doc::text(format!( + "^\"{}\"", + s.replace("\"", "\\\"").replace("\\", "\\\\") + )), NumVal(r) => Doc::text(format_range(r)), ProseVal(_) => unimplemented!(), } @@ -88,8 +112,12 @@ pub fn abnf_to_pest(data: &Vec<u8>, rule_settings: &HashMap<String, PestRuleSett fn format_range(x: Range) -> String { use abnf::abnf::Range::*; match x { - Range(x, y) => format!("'{}'..'{}'", format_char(x), format_char(y)), - OneOf(v) => format!("\"{}\"", v.into_iter().map(format_char).join("")), + Range(x, y) => { + format!("'{}'..'{}'", format_char(x), format_char(y)) + } + OneOf(v) => { + format!("\"{}\"", v.into_iter().map(format_char).join("")) + } } } fn format_char(x: u64) -> String { @@ -104,11 +132,12 @@ pub fn abnf_to_pest(data: &Vec<u8>, rule_settings: &HashMap<String, PestRuleSett } format!("\\u{{{:02X}}}", x) } - let make_err = |e| std::io::Error::new(std::io::ErrorKind::Other, format!("{}", e)); + let make_err = + |e| std::io::Error::new(std::io::ErrorKind::Other, format!("{}", e)); let rules = rulelist_comp(&data).map_err(make_err)?.1; - let formatted_rules = rules.into_iter().map(|x| format_rule(x, rule_settings)); + let formatted_rules = + rules.into_iter().map(|x| format_rule(x, rule_settings)); let doc: Doc<_> = Doc::intersperse(formatted_rules, Doc::newline()); Ok(format!("{}", doc.pretty(80))) } - 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 diff --git a/dhall/tests/macros.rs b/dhall/tests/macros.rs index 131683b..66b9dbf 100644 --- a/dhall/tests/macros.rs +++ b/dhall/tests/macros.rs @@ -1,27 +1,34 @@ #[macro_export] macro_rules! include_test_str { - ($x:expr) => { include_str!(concat!("../../dhall-lang/tests/", $x, ".dhall")) }; + ($x:expr) => { + include_str!(concat!("../../dhall-lang/tests/", $x, ".dhall")) + }; } #[macro_export] macro_rules! include_test_strs_ab { - ($x:expr) => { (include_test_str!(concat!($x, "A")), include_test_str!(concat!($x, "B"))) }; + ($x:expr) => { + ( + include_test_str!(concat!($x, "A")), + include_test_str!(concat!($x, "B")), + ) + }; } #[macro_export] macro_rules! parse_str { - ($str:expr) => { - { - let pest_expr = parser::parse_expr_pest(&$str).map_err(|e| println!("{}", e)).unwrap(); - // // Check with old parser - // match parser::parse_expr_lalrpop(&$str) { - // Ok(larlpop_expr) => assert_eq!(pest_expr, larlpop_expr), - // Err(_) => {}, - // }; - // panic!("{:?}", pest_expr); - pest_expr - } - }; + ($str:expr) => {{ + let pest_expr = parser::parse_expr_pest(&$str) + .map_err(|e| println!("{}", e)) + .unwrap(); + // // Check with old parser + // match parser::parse_expr_lalrpop(&$str) { + // Ok(larlpop_expr) => assert_eq!(pest_expr, larlpop_expr), + // Err(_) => {}, + // }; + // panic!("{:?}", pest_expr); + pest_expr + }}; } #[macro_export] @@ -60,7 +67,10 @@ macro_rules! run_spec_test { let (expr_str, expected_str) = include_test_strs_ab!($path); let expr = parse_str!(expr_str); let expected = parse_str!(expected_str); - assert_eq_!(normalize::<_, X, _>(&expr), normalize::<_, X, _>(&expected)); + assert_eq_!( + normalize::<_, X, _>(&expr), + normalize::<_, X, _>(&expected) + ); }; (parser, $path:expr) => { let expr_str = include_test_str!(concat!($path, "A")); @@ -79,13 +89,18 @@ macro_rules! make_spec_test { #[allow(non_snake_case)] #[allow(unused_variables)] #[allow(unused_imports)] - fn $name(){ - use std::thread; + fn $name() { use dhall::*; + use std::thread; - thread::Builder::new().stack_size(16 * 1024 * 1024).spawn(move || { - run_spec_test!($type, $path); - }).unwrap().join().unwrap(); + thread::Builder::new() + .stack_size(16 * 1024 * 1024) + .spawn(move || { + run_spec_test!($type, $path); + }) + .unwrap() + .join() + .unwrap(); } }; } diff --git a/dhall_parser/build.rs b/dhall_parser/build.rs index 743aa2d..a206517 100644 --- a/dhall_parser/build.rs +++ b/dhall_parser/build.rs @@ -1,8 +1,8 @@ -use std::fs::File; -use std::io::{Read,Write,BufReader,BufRead}; use std::collections::HashMap; +use std::fs::File; +use std::io::{BufRead, BufReader, Read, Write}; -use abnf_to_pest::{PestRuleSettings, abnf_to_pest}; +use abnf_to_pest::{abnf_to_pest, PestRuleSettings}; fn main() -> std::io::Result<()> { // TODO: upstream changes to grammar @@ -22,26 +22,47 @@ fn main() -> std::io::Result<()> { for line in BufReader::new(File::open(visibility_path)?).lines() { let line = line?; if line.len() >= 2 && &line[0..2] == "# " { - rule_settings.insert(line[2..].into(), PestRuleSettings { visible: false, ..Default::default() }); + rule_settings.insert( + line[2..].into(), + PestRuleSettings { + visible: false, + ..Default::default() + }, + ); } else { - rule_settings.insert(line, PestRuleSettings { visible: true, ..Default::default() }); + rule_settings.insert( + line, + PestRuleSettings { + visible: true, + ..Default::default() + }, + ); } } - rule_settings.insert("simple_label".to_owned(), PestRuleSettings { - visible: true, - replace: Some(" + rule_settings.insert( + "simple_label".to_owned(), + PestRuleSettings { + visible: true, + replace: Some( + " keyword_raw ~ simple_label_next_char+ | !keyword_raw ~ simple_label_first_char ~ simple_label_next_char* - ".to_owned()), - }); + " + .to_owned(), + ), + }, + ); let mut file = File::create(pest_path)?; writeln!(&mut file, "// AUTO-GENERATED FILE. See build.rs.")?; writeln!(&mut file, "{}", abnf_to_pest(&data, &rule_settings)?)?; - writeln!(&mut file, "keyword_raw = _{{ + writeln!( + &mut file, + "keyword_raw = _{{ let_raw | in_raw | if_raw | then_raw | else_raw | Infinity_raw | NaN_raw - }}")?; + }}" + )?; writeln!( &mut file, "final_expression = {{ SOI ~ complete_expression ~ EOI }}" |