summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-03-04 18:26:28 +0100
committerNadrieril2019-03-04 18:26:28 +0100
commitc1c21e3ae53ffdbc639fa950093baa60e710e022 (patch)
tree90db36bc1eef7756f1b88138a92174cf603adacd
parent24d3e235399ef421723cd597fe7a9408c3da54ec (diff)
Make some annotations optional in AST
-rw-r--r--dhall/src/core.rs64
-rw-r--r--dhall/src/grammar.lalrpop2
-rw-r--r--dhall/src/grammar_util.rs2
-rw-r--r--dhall/src/typecheck.rs42
4 files changed, 74 insertions, 36 deletions
diff --git a/dhall/src/core.rs b/dhall/src/core.rs
index 5b82160..8ac9a42 100644
--- a/dhall/src/core.rs
+++ b/dhall/src/core.rs
@@ -155,10 +155,10 @@ pub enum Expr<'i, S, A> {
/// `TextAppend x y ~ x ++ y`
TextAppend(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
/// `ListLit t [x, y, z] ~ [x, y, z] : List t`
- ListLit(Box<Expr<'i, S, A>>, Vec<Expr<'i, S, A>>),
+ ListLit(Option<Box<Expr<'i, S, A>>>, Vec<Expr<'i, S, A>>),
/// `OptionalLit t [e] ~ [e] : Optional t`
/// `OptionalLit t [] ~ [] : Optional t`
- OptionalLit(Box<Expr<'i, S, A>>, Vec<Expr<'i, S, A>>),
+ OptionalLit(Option<Box<Expr<'i, S, A>>>, Vec<Expr<'i, S, A>>),
/// `Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }`
Record(BTreeMap<&'i str, Expr<'i, S, A>>),
/// `RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }`
@@ -178,7 +178,7 @@ pub enum Expr<'i, S, A> {
/// x # y
ListAppend(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
/// `Merge x y t ~ merge x y : t`
- Merge(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
+ Merge(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>, Option<Box<Expr<'i, S, A>>>),
/// `Field e x ~ e.x`
Field(Box<Expr<'i, S, A>>, &'i str),
/// `Note S x ~ e`
@@ -321,20 +321,40 @@ impl<'i, S, A: Display> Expr<'i, S, A> {
d.fmt_b(f)
}
&ListLit(ref t, ref es) => {
- fmt_list("[", "] : List ", es, f, |e, f| e.fmt(f))?;
- t.fmt_e(f)
+ fmt_list("[", "]", es, f, |e, f| e.fmt(f))?;
+ match t {
+ Some(t) => {
+ write!(f, " : List ")?;
+ t.fmt_e(f)?
+ },
+ None => {},
+ }
+ Ok(())
}
&OptionalLit(ref t, ref es) => {
- fmt_list("[", "] : Optional ", es, f, |e, f| e.fmt(f))?;
- t.fmt_e(f)
+ fmt_list("[", "]", es, f, |e, f| e.fmt(f))?;
+ match t {
+ Some(t) => {
+ write!(f, " : Optional ")?;
+ t.fmt_e(f)?
+ },
+ None => {},
+ }
+ Ok(())
}
&Merge(ref a, ref b, ref c) => {
write!(f, "merge ")?;
a.fmt_e(f)?;
write!(f, " ")?;
b.fmt_e(f)?;
- write!(f, " : ")?;
- c.fmt_d(f)
+ match c {
+ Some(c) => {
+ write!(f, " : ")?;
+ c.fmt_d(f)?
+ },
+ None => {},
+ }
+ Ok(())
}
&Note(_, ref b) => b.fmt_b(f),
a => a.fmt_c(f),
@@ -680,11 +700,11 @@ pub fn shift<'i, S, T, A: Clone>(d: isize, v: V, e: &Expr<'i, S, A>) -> Expr<'i,
TextLit(ref a) => TextLit(a.clone()),
TextAppend(ref a, ref b) => shift_op2(TextAppend, d, v, a, b),
ListLit(ref t, ref es) => {
- ListLit(bx(shift(d, v, t)),
+ ListLit(t.as_ref().map(|t| bx(shift(d, v, t))),
es.iter().map(|e| shift(d, v, e)).collect())
}
OptionalLit(ref t, ref es) => {
- OptionalLit(bx(shift(d, v, t)),
+ OptionalLit(t.as_ref().map(|t| bx(shift(d, v, t))),
es.iter().map(|e| shift(d, v, e)).collect())
}
Record(ref a) => Record(map_record_value(a, |val| shift(d, v, val))),
@@ -697,7 +717,7 @@ pub fn shift<'i, S, T, A: Clone>(d: isize, v: V, e: &Expr<'i, S, A>) -> Expr<'i,
}
Combine(ref a, ref b) => shift_op2(Combine, d, v, a, b),
Merge(ref a, ref b, ref c) => {
- Merge(bx(shift(d, v, a)), bx(shift(d, v, b)), bx(shift(d, v, c)))
+ Merge(bx(shift(d, v, a)), bx(shift(d, v, b)), c.as_ref().map(|c| bx(shift(d, v, c))))
}
Field(ref a, b) => Field(bx(shift(d, v, a)), b),
Note(_, ref b) => shift(d, v, b),
@@ -777,14 +797,14 @@ pub fn subst<'i, S, T, A>(v: V<'i>, e: &Expr<'i, S, A>, b: &Expr<'i, T, A>) -> E
TextLit(ref a) => TextLit(a.clone()),
TextAppend(ref a, ref b) => subst_op2(TextAppend, v, e, a, b),
ListLit(ref a, ref b) => {
- let a2 = subst(v, e, a);
+ let a2 = a.as_ref().map(|a| bx(subst(v, e, a)));
let b2 = b.iter().map(|be| subst(v, e, be)).collect();
- ListLit(bx(a2), b2)
+ ListLit(a2, b2)
}
OptionalLit(ref a, ref b) => {
- let a2 = subst(v, e, a);
+ let a2 = a.as_ref().map(|a| bx(subst(v, e, a)));
let b2 = b.iter().map(|be| subst(v, e, be)).collect();
- OptionalLit(bx(a2), b2)
+ OptionalLit(a2, b2)
}
Record(ref kts) => Record(map_record_value(kts, |t| subst(v, e, t))),
RecordLit(ref kvs) => RecordLit(map_record_value(kvs, |val| subst(v, e, val))),
@@ -796,7 +816,7 @@ pub fn subst<'i, S, T, A>(v: V<'i>, e: &Expr<'i, S, A>, b: &Expr<'i, T, A>) -> E
}
Combine(ref a, ref b) => subst_op2(Combine, v, e, a, b),
Merge(ref a, ref b, ref c) => {
- Merge(bx(subst(v, e, a)), bx(subst(v, e, b)), bx(subst(v, e, c)))
+ Merge(bx(subst(v, e, a)), bx(subst(v, e, b)), c.as_ref().map(|c| bx(subst(v, e, c))))
}
Field(ref a, b) => Field(bx(subst(v, e, a)), b),
Note(_, ref b) => subst(v, e, b),
@@ -920,7 +940,7 @@ pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A>
if check(&labeled) {
let mut v = vec![];
list_to_vector(&mut v, labeled);
- ListLit(bx(t), v)
+ ListLit(Some(bx(t)), v)
} else {
app(App(f, bx(t)), k)
}
@@ -1022,14 +1042,14 @@ pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A>
normalize(x), normalize(y))
}
ListLit(ref t, ref es) => {
- let t2 = normalize(t);
+ let t2 = t.as_ref().map(|x| x.as_ref()).map(normalize).map(bx);
let es2 = es.iter().map(normalize).collect();
- ListLit(bx(t2), es2)
+ ListLit(t2, es2)
}
OptionalLit(ref t, ref es) => {
- let t2 = normalize(t);
+ let t2 = t.as_ref().map(|x| x.as_ref()).map(normalize).map(bx);
let es2 = es.iter().map(normalize).collect();
- OptionalLit(bx(t2), es2)
+ OptionalLit(t2, es2)
}
Record(ref kts) => Record(map_record_value(kts, normalize)),
RecordLit(ref kvs) => RecordLit(map_record_value(kvs, normalize)),
diff --git a/dhall/src/grammar.lalrpop b/dhall/src/grammar.lalrpop
index 1d832b7..6f87e6e 100644
--- a/dhall/src/grammar.lalrpop
+++ b/dhall/src/grammar.lalrpop
@@ -67,7 +67,7 @@ ExprB: BoxExpr<'input> = {
If <Expr> Then <ExprB> Else <ExprC> => bx(BoolIf(<>)),
<ExprC> "->" <ExprB> => bx(Pi("_", <>)),
Let <Label> <(":" <Expr>)?> "=" <Expr> In <ExprB> => bx(Let(<>)),
- "[" <a:Elems> "]" ":" <b:ListLike> <c:ExprE> => bx(b(c, a)),
+ "[" <a:Elems> "]" ":" <b:ListLike> <c:ExprE> => bx(b(Some(c), a)),
<ExprC> ":" <Expr> => bx(Annot(<>)),
ExprC,
};
diff --git a/dhall/src/grammar_util.rs b/dhall/src/grammar_util.rs
index 2250acd..c185632 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(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/typecheck.rs b/dhall/src/typecheck.rs
index 51ea848..aa8d382 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -316,20 +316,29 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
TextLit(_) => Ok(Builtin(Text)),
TextAppend(ref l, ref r) => op2_type(ctx, e, Text, CantTextAppend, l, r),
ListLit(ref t, ref xs) => {
- let s = normalize::<_, S, _>(&type_with(ctx, t)?);
+ let mut iter = xs.iter().enumerate();
+ let t: Box<Expr<_, _>> = match t {
+ Some(t) => t.clone(),
+ 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, InvalidListType((**t).clone()))),
+ _ => return Err(TypeError::new(ctx, e, InvalidListType(*t))),
}
- for (i, x) in xs.iter().enumerate() {
+ for (i, x) in iter {
let t2 = type_with(ctx, x)?;
- if !prop_equal(t, &t2) {
- let nf_t = normalize(t);
+ if !prop_equal(&t, &t2) {
+ let nf_t = normalize(&t);
let nf_t2 = normalize(&t2);
return Err(TypeError::new(ctx, e, InvalidListElement(i, nf_t, x.clone(), nf_t2)) )
}
}
- Ok(App(bx(Builtin(List)), t.clone()))
+ Ok(App(bx(Builtin(List)), t))
}
Builtin(ListBuild) =>
Ok(pi("a", Const(Type),
@@ -358,24 +367,33 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
Builtin(ListReverse) =>
Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(List, "a")))),
OptionalLit(ref t, ref xs) => {
- let s = normalize::<_, S, _>(&type_with(ctx, t)?);
+ let mut iter = xs.iter();
+ let t: Box<Expr<_, _>> = match t {
+ Some(t) => t.clone(),
+ 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).clone()))),
+ _ => return Err(TypeError::new(ctx, e, InvalidOptionalType(*t))),
}
let n = xs.len();
if 2 <= n {
return Err(TypeError::new(ctx, e, InvalidOptionalLiteral(n)));
}
- for x in xs {
+ for x in iter {
let t2 = type_with(ctx, x)?;
- if !prop_equal(t, &t2) {
- let nf_t = normalize(t);
+ if !prop_equal(&t, &t2) {
+ let nf_t = normalize(&t);
let nf_t2 = normalize(&t2);
return Err(TypeError::new(ctx, e, InvalidOptionalElement(nf_t, x.clone(), nf_t2)));
}
}
- Ok(App(bx(Builtin(Optional)), t.clone()))
+ Ok(App(bx(Builtin(Optional)), t))
}
Builtin(OptionalFold) =>
Ok(pi("a", Const(Type),