summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/builtins.rs122
-rw-r--r--dhall/src/operations.rs37
-rw-r--r--dhall/src/semantics/nze/nir.rs7
-rw-r--r--dhall/src/semantics/resolve/resolve.rs7
-rw-r--r--dhall/src/semantics/tck/tir.rs3
-rw-r--r--dhall/src/semantics/tck/typecheck.rs6
-rw-r--r--dhall/src/syntax/ast/expr.rs69
-rw-r--r--dhall/src/syntax/binary/decode.rs4
-rw-r--r--dhall/src/syntax/binary/encode.rs8
-rw-r--r--dhall/src/syntax/text/parser.rs48
-rw-r--r--dhall/src/syntax/text/printer.rs48
11 files changed, 180 insertions, 179 deletions
diff --git a/dhall/src/builtins.rs b/dhall/src/builtins.rs
index f65e8d1..bb8173c 100644
--- a/dhall/src/builtins.rs
+++ b/dhall/src/builtins.rs
@@ -1,17 +1,92 @@
-use crate::operations::OpKind;
+use crate::operations::{BinOp, OpKind};
use crate::semantics::{
skip_resolve_expr, typecheck, Hir, HirKind, Nir, NirKind, NzEnv, VarEnv,
};
use crate::syntax::map::DupTreeMap;
use crate::syntax::Const::Type;
use crate::syntax::{
- BinOp, Builtin, Const, Expr, ExprKind, InterpolatedText,
- InterpolatedTextContents, Label, NaiveDouble, NumKind, Span, UnspannedExpr,
- V,
+ Const, Expr, ExprKind, InterpolatedText, InterpolatedTextContents, Label,
+ NaiveDouble, NumKind, Span, UnspannedExpr, V,
};
use std::collections::HashMap;
use std::convert::TryInto;
+/// Built-ins
+#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
+pub enum Builtin {
+ Bool,
+ Natural,
+ Integer,
+ Double,
+ Text,
+ List,
+ Optional,
+ OptionalNone,
+ NaturalBuild,
+ NaturalFold,
+ NaturalIsZero,
+ NaturalEven,
+ NaturalOdd,
+ NaturalToInteger,
+ NaturalShow,
+ NaturalSubtract,
+ IntegerToDouble,
+ IntegerShow,
+ IntegerNegate,
+ IntegerClamp,
+ DoubleShow,
+ ListBuild,
+ ListFold,
+ ListLength,
+ ListHead,
+ ListLast,
+ ListIndexed,
+ ListReverse,
+ OptionalFold,
+ OptionalBuild,
+ TextShow,
+}
+
+impl Builtin {
+ pub fn parse(s: &str) -> Option<Self> {
+ use Builtin::*;
+ match s {
+ "Bool" => Some(Bool),
+ "Natural" => Some(Natural),
+ "Integer" => Some(Integer),
+ "Double" => Some(Double),
+ "Text" => Some(Text),
+ "List" => Some(List),
+ "Optional" => Some(Optional),
+ "None" => Some(OptionalNone),
+ "Natural/build" => Some(NaturalBuild),
+ "Natural/fold" => Some(NaturalFold),
+ "Natural/isZero" => Some(NaturalIsZero),
+ "Natural/even" => Some(NaturalEven),
+ "Natural/odd" => Some(NaturalOdd),
+ "Natural/toInteger" => Some(NaturalToInteger),
+ "Natural/show" => Some(NaturalShow),
+ "Natural/subtract" => Some(NaturalSubtract),
+ "Integer/toDouble" => Some(IntegerToDouble),
+ "Integer/show" => Some(IntegerShow),
+ "Integer/negate" => Some(IntegerNegate),
+ "Integer/clamp" => Some(IntegerClamp),
+ "Double/show" => Some(DoubleShow),
+ "List/build" => Some(ListBuild),
+ "List/fold" => Some(ListFold),
+ "List/length" => Some(ListLength),
+ "List/head" => Some(ListHead),
+ "List/last" => Some(ListLast),
+ "List/indexed" => Some(ListIndexed),
+ "List/reverse" => Some(ListReverse),
+ "Optional/fold" => Some(OptionalFold),
+ "Optional/build" => Some(OptionalBuild),
+ "Text/show" => Some(TextShow),
+ _ => None,
+ }
+ }
+}
+
/// A partially applied builtin.
/// Invariant: the evaluation of the given args must not be able to progress further
#[derive(Debug, Clone)]
@@ -492,3 +567,42 @@ impl std::cmp::PartialEq for BuiltinClosure {
}
}
impl std::cmp::Eq for BuiltinClosure {}
+
+impl std::fmt::Display for Builtin {
+ fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
+ use Builtin::*;
+ f.write_str(match *self {
+ Bool => "Bool",
+ Natural => "Natural",
+ Integer => "Integer",
+ Double => "Double",
+ Text => "Text",
+ List => "List",
+ Optional => "Optional",
+ OptionalNone => "None",
+ NaturalBuild => "Natural/build",
+ NaturalFold => "Natural/fold",
+ NaturalIsZero => "Natural/isZero",
+ NaturalEven => "Natural/even",
+ NaturalOdd => "Natural/odd",
+ NaturalToInteger => "Natural/toInteger",
+ NaturalShow => "Natural/show",
+ NaturalSubtract => "Natural/subtract",
+ IntegerToDouble => "Integer/toDouble",
+ IntegerNegate => "Integer/negate",
+ IntegerClamp => "Integer/clamp",
+ IntegerShow => "Integer/show",
+ DoubleShow => "Double/show",
+ ListBuild => "List/build",
+ ListFold => "List/fold",
+ ListLength => "List/length",
+ ListHead => "List/head",
+ ListLast => "List/last",
+ ListIndexed => "List/indexed",
+ ListReverse => "List/reverse",
+ OptionalFold => "Optional/fold",
+ OptionalBuild => "Optional/build",
+ TextShow => "Text/show",
+ })
+ }
+}
diff --git a/dhall/src/operations.rs b/dhall/src/operations.rs
index 363cd10..1ebf288 100644
--- a/dhall/src/operations.rs
+++ b/dhall/src/operations.rs
@@ -3,15 +3,46 @@ use std::borrow::Cow;
use std::cmp::max;
use std::collections::HashMap;
+use crate::builtins::Builtin;
use crate::error::{ErrorBuilder, TypeError};
use crate::semantics::{
merge_maps, mk_span_err, mkerr, ret_kind, ret_op, ret_ref, Binder, Closure,
Hir, HirKind, Nir, NirKind, Ret, TextLit, Tir, TyEnv, Type,
};
use crate::syntax::map::DupTreeSet;
-use crate::syntax::{
- trivial_result, BinOp, Builtin, Const, ExprKind, Label, NumKind, Span,
-};
+use crate::syntax::{trivial_result, Const, ExprKind, Label, NumKind, Span};
+
+// Definition order must match precedence order for
+// pretty-printing to work correctly
+#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
+pub enum BinOp {
+ /// `x ? y`
+ ImportAlt,
+ /// `x || y`
+ BoolOr,
+ /// `x + y`
+ NaturalPlus,
+ /// `x ++ y`
+ TextAppend,
+ /// `x # y`
+ ListAppend,
+ /// `x && y`
+ BoolAnd,
+ /// `x ∧ y`
+ RecursiveRecordMerge,
+ /// `x ⫽ y`
+ RightBiasedRecordMerge,
+ /// `x ⩓ y`
+ RecursiveRecordTypeMerge,
+ /// `x * y`
+ NaturalTimes,
+ /// `x == y`
+ BoolEQ,
+ /// `x != y`
+ BoolNE,
+ /// x === y
+ Equivalence,
+}
/// Operations
#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index e2a0113..12f1b14 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -1,16 +1,15 @@
use std::collections::HashMap;
use std::rc::Rc;
-use crate::builtins::BuiltinClosure;
-use crate::operations::OpKind;
+use crate::builtins::{Builtin, BuiltinClosure};
+use crate::operations::{BinOp, OpKind};
use crate::semantics::nze::lazy;
use crate::semantics::{
apply_any, normalize_hir, normalize_one_layer, squash_textlit, Binder, Hir,
HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv,
};
use crate::syntax::{
- BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label,
- NumKind, Span,
+ Const, Expr, ExprKind, InterpolatedTextContents, Label, NumKind, Span,
};
use crate::ToExprOptions;
diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs
index bbcd240..cd5232a 100644
--- a/dhall/src/semantics/resolve/resolve.rs
+++ b/dhall/src/semantics/resolve/resolve.rs
@@ -4,15 +4,16 @@ use std::env;
use std::path::PathBuf;
use url::Url;
+use crate::builtins::Builtin;
use crate::error::ErrorBuilder;
use crate::error::{Error, ImportError};
-use crate::operations::OpKind;
+use crate::operations::{BinOp, OpKind};
use crate::semantics::{mkerr, Hir, HirKind, ImportEnv, NameEnv, Type};
use crate::syntax;
use crate::syntax::map::DupTreeMap;
use crate::syntax::{
- BinOp, Builtin, Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode,
- ImportTarget, Span, UnspannedExpr, URL,
+ Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode, ImportTarget, Span,
+ UnspannedExpr, URL,
};
use crate::{Parsed, Resolved};
diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs
index 89a8027..ec15a1f 100644
--- a/dhall/src/semantics/tck/tir.rs
+++ b/dhall/src/semantics/tck/tir.rs
@@ -1,6 +1,7 @@
+use crate::builtins::Builtin;
use crate::error::{ErrorBuilder, TypeError};
use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv};
-use crate::syntax::{Builtin, Const, Expr, Span};
+use crate::syntax::{Const, Expr, Span};
/// The type of a type. 0 is `Type`, 1 is `Kind`, etc...
#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)]
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index a31f15c..c6300d9 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -1,13 +1,11 @@
use std::cmp::max;
use std::collections::HashMap;
-use crate::builtins::type_of_builtin;
+use crate::builtins::{type_of_builtin, Builtin};
use crate::error::{ErrorBuilder, TypeError, TypeMessage};
use crate::operations::typecheck_operation;
use crate::semantics::{Hir, HirKind, Nir, NirKind, Tir, TyEnv, Type};
-use crate::syntax::{
- Builtin, Const, ExprKind, InterpolatedTextContents, NumKind, Span,
-};
+use crate::syntax::{Const, ExprKind, InterpolatedTextContents, NumKind, Span};
fn function_check(a: Const, b: Const) -> Const {
if b == Const::Type {
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 62734bf..8f55540 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -1,5 +1,6 @@
use std::collections::BTreeMap;
+use crate::builtins::Builtin;
use crate::error::Error;
use crate::operations::OpKind;
use crate::semantics::Universe;
@@ -37,74 +38,6 @@ impl Const {
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub struct V(pub Label, pub usize);
-// Definition order must match precedence order for
-// pretty-printing to work correctly
-#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
-pub enum BinOp {
- /// `x ? y`
- ImportAlt,
- /// `x || y`
- BoolOr,
- /// `x + y`
- NaturalPlus,
- /// `x ++ y`
- TextAppend,
- /// `x # y`
- ListAppend,
- /// `x && y`
- BoolAnd,
- /// `x ∧ y`
- RecursiveRecordMerge,
- /// `x ⫽ y`
- RightBiasedRecordMerge,
- /// `x ⩓ y`
- RecursiveRecordTypeMerge,
- /// `x * y`
- NaturalTimes,
- /// `x == y`
- BoolEQ,
- /// `x != y`
- BoolNE,
- /// x === y
- Equivalence,
-}
-
-/// Built-ins
-#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
-pub enum Builtin {
- Bool,
- Natural,
- Integer,
- Double,
- Text,
- List,
- Optional,
- OptionalNone,
- NaturalBuild,
- NaturalFold,
- NaturalIsZero,
- NaturalEven,
- NaturalOdd,
- NaturalToInteger,
- NaturalShow,
- NaturalSubtract,
- IntegerToDouble,
- IntegerShow,
- IntegerNegate,
- IntegerClamp,
- DoubleShow,
- ListBuild,
- ListFold,
- ListLength,
- ListHead,
- ListLast,
- ListIndexed,
- ListReverse,
- OptionalFold,
- OptionalBuild,
- TextShow,
-}
-
// Each node carries an annotation.
#[derive(Debug, Clone)]
pub struct Expr {
diff --git a/dhall/src/syntax/binary/decode.rs b/dhall/src/syntax/binary/decode.rs
index f062089..195bd0a 100644
--- a/dhall/src/syntax/binary/decode.rs
+++ b/dhall/src/syntax/binary/decode.rs
@@ -25,8 +25,10 @@ fn rc(x: UnspannedExpr) -> Expr {
}
fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
+ use crate::builtins::Builtin;
+ use crate::operations::BinOp;
use cbor::Value::*;
- use syntax::{BinOp, Builtin, Const};
+ use syntax::Const;
use ExprKind::*;
use OpKind::*;
Ok(rc(match data {
diff --git a/dhall/src/syntax/binary/encode.rs b/dhall/src/syntax/binary/encode.rs
index cef2af8..913dd67 100644
--- a/dhall/src/syntax/binary/encode.rs
+++ b/dhall/src/syntax/binary/encode.rs
@@ -2,8 +2,9 @@ use serde_cbor::value::value as cbor;
use std::collections::BTreeMap;
use std::vec;
+use crate::builtins::Builtin;
use crate::error::EncodeError;
-use crate::operations::OpKind;
+use crate::operations::{BinOp, OpKind};
use crate::syntax;
use crate::syntax::map::DupTreeMap;
use crate::syntax::{
@@ -47,7 +48,6 @@ where
{
use cbor::Value::{String, I64, U64};
use std::iter::once;
- use syntax::Builtin;
use syntax::ExprKind::*;
use syntax::NumKind::*;
use OpKind::*;
@@ -116,7 +116,7 @@ where
SomeLit(x) => ser_seq!(ser; tag(5), null(), expr(x)),
EmptyListLit(x) => match x.as_ref() {
Op(App(f, a)) => match f.as_ref() {
- ExprKind::Builtin(Builtin::List) => {
+ ExprKind::Builtin(self::Builtin::List) => {
ser_seq!(ser; tag(4), expr(a))
}
_ => ser_seq!(ser; tag(28), expr(x)),
@@ -138,7 +138,7 @@ where
UnionType(map) => ser_seq!(ser; tag(11), UnionMap(map)),
Op(Field(x, l)) => ser_seq!(ser; tag(9), expr(x), label(l)),
Op(BinOp(op, x, y)) => {
- use syntax::BinOp::*;
+ use self::BinOp::*;
let op = match op {
BoolOr => 0,
BoolAnd => 1,
diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs
index 8d76225..dbf5c75 100644
--- a/dhall/src/syntax/text/parser.rs
+++ b/dhall/src/syntax/text/parser.rs
@@ -36,46 +36,6 @@ enum Selector {
ProjectionByExpr(Expr),
}
-impl crate::syntax::Builtin {
- pub fn parse(s: &str) -> Option<Self> {
- use crate::syntax::Builtin::*;
- match s {
- "Bool" => Some(Bool),
- "Natural" => Some(Natural),
- "Integer" => Some(Integer),
- "Double" => Some(Double),
- "Text" => Some(Text),
- "List" => Some(List),
- "Optional" => Some(Optional),
- "None" => Some(OptionalNone),
- "Natural/build" => Some(NaturalBuild),
- "Natural/fold" => Some(NaturalFold),
- "Natural/isZero" => Some(NaturalIsZero),
- "Natural/even" => Some(NaturalEven),
- "Natural/odd" => Some(NaturalOdd),
- "Natural/toInteger" => Some(NaturalToInteger),
- "Natural/show" => Some(NaturalShow),
- "Natural/subtract" => Some(NaturalSubtract),
- "Integer/toDouble" => Some(IntegerToDouble),
- "Integer/show" => Some(IntegerShow),
- "Integer/negate" => Some(IntegerNegate),
- "Integer/clamp" => Some(IntegerClamp),
- "Double/show" => Some(DoubleShow),
- "List/build" => Some(ListBuild),
- "List/fold" => Some(ListFold),
- "List/length" => Some(ListLength),
- "List/head" => Some(ListHead),
- "List/last" => Some(ListLast),
- "List/indexed" => Some(ListIndexed),
- "List/reverse" => Some(ListReverse),
- "Optional/fold" => Some(OptionalFold),
- "Optional/build" => Some(OptionalBuild),
- "Text/show" => Some(TextShow),
- _ => None,
- }
- }
-}
-
fn input_to_span(input: ParseInput) -> Span {
Span::make(input.user_data().clone(), input.as_pair().as_span())
}
@@ -129,7 +89,7 @@ fn trim_indent(lines: &mut Vec<ParsedText>) {
/// Insert the expr into the map; in case of collision, create a RecursiveRecordMerge node.
fn insert_recordlit_entry(map: &mut BTreeMap<Label, Expr>, l: Label, e: Expr) {
- use crate::syntax::BinOp::RecursiveRecordMerge;
+ use crate::operations::BinOp::RecursiveRecordMerge;
use std::collections::btree_map::Entry;
match map.entry(l) {
Entry::Vacant(entry) => {
@@ -147,7 +107,7 @@ fn insert_recordlit_entry(map: &mut BTreeMap<Label, Expr>, l: Label, e: Expr) {
}
fn desugar_with_expr(x: Expr, labels: &[Label], y: Expr) -> Expr {
- use crate::syntax::BinOp::RightBiasedRecordMerge;
+ use crate::operations::BinOp::RightBiasedRecordMerge;
let expr = |k| Expr::new(k, Span::WithSugar);
match labels {
[] => y,
@@ -391,7 +351,7 @@ impl DhallParser {
#[alias(expression)]
fn builtin(input: ParseInput) -> ParseResult<Expr> {
let s = input.as_str();
- let e = match crate::syntax::Builtin::parse(s) {
+ let e = match crate::builtins::Builtin::parse(s) {
Some(b) => Builtin(b),
None => match s {
"True" => Num(Bool(true)),
@@ -784,7 +744,7 @@ impl DhallParser {
op: ParseInput,
r: Expr,
) -> ParseResult<Expr> {
- use crate::syntax::BinOp::*;
+ use crate::operations::BinOp::*;
use Rule::*;
let op = match op.as_rule() {
import_alt => ImportAlt,
diff --git a/dhall/src/syntax/text/printer.rs b/dhall/src/syntax/text/printer.rs
index a85f435..9e90660 100644
--- a/dhall/src/syntax/text/printer.rs
+++ b/dhall/src/syntax/text/printer.rs
@@ -1,4 +1,5 @@
-use crate::operations::OpKind;
+use crate::builtins::Builtin;
+use crate::operations::{BinOp, OpKind};
use crate::syntax::*;
use itertools::Itertools;
use std::fmt::{self, Display};
@@ -15,7 +16,7 @@ enum PrintPhase {
// `operator-expression`
Operator,
// All the `<operator>-expression`s
- BinOp(ast::BinOp),
+ BinOp(self::BinOp),
// `application-expression`
App,
// `import-expression`
@@ -335,7 +336,7 @@ impl Display for Const {
impl Display for BinOp {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- use crate::syntax::BinOp::*;
+ use BinOp::*;
f.write_str(match self {
BoolOr => "||",
TextAppend => "++",
@@ -383,7 +384,7 @@ impl Display for Label {
let is_reserved = match s.as_str() {
"let" | "in" | "if" | "then" | "else" | "Type" | "Kind"
| "Sort" | "True" | "False" | "Some" => true,
- _ => crate::syntax::Builtin::parse(&s).is_some(),
+ _ => Builtin::parse(&s).is_some(),
};
if !is_reserved && s.chars().all(|c| c.is_ascii_alphanumeric()) {
write!(f, "{}", s)
@@ -481,45 +482,6 @@ impl<SubExpr: Display> Display for Import<SubExpr> {
}
}
-impl Display for Builtin {
- fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- use crate::syntax::Builtin::*;
- f.write_str(match *self {
- Bool => "Bool",
- Natural => "Natural",
- Integer => "Integer",
- Double => "Double",
- Text => "Text",
- List => "List",
- Optional => "Optional",
- OptionalNone => "None",
- NaturalBuild => "Natural/build",
- NaturalFold => "Natural/fold",
- NaturalIsZero => "Natural/isZero",
- NaturalEven => "Natural/even",
- NaturalOdd => "Natural/odd",
- NaturalToInteger => "Natural/toInteger",
- NaturalShow => "Natural/show",
- NaturalSubtract => "Natural/subtract",
- IntegerToDouble => "Integer/toDouble",
- IntegerNegate => "Integer/negate",
- IntegerClamp => "Integer/clamp",
- IntegerShow => "Integer/show",
- DoubleShow => "Double/show",
- ListBuild => "List/build",
- ListFold => "List/fold",
- ListLength => "List/length",
- ListHead => "List/head",
- ListLast => "List/last",
- ListIndexed => "List/indexed",
- ListReverse => "List/reverse",
- OptionalFold => "Optional/fold",
- OptionalBuild => "Optional/build",
- TextShow => "Text/show",
- })
- }
-}
-
impl Display for Scheme {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
use crate::syntax::Scheme::*;
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 19:37:00 +0000