diff options
author | Nadrieril | 2020-04-06 22:24:15 +0100 |
---|---|---|
committer | Nadrieril | 2020-04-06 22:26:08 +0100 |
commit | 56efd2ac39149d8652bd625fbf0679c10823b137 (patch) | |
tree | 4d9e58ad86ea37dca7a2232ab475791669000684 | |
parent | 2cf9169e1a21e1196e0265847abcfa904e2d45a3 (diff) |
Move BinOp and Builtin definitions in the relevant module
Diffstat (limited to '')
-rw-r--r-- | dhall/src/builtins.rs | 122 | ||||
-rw-r--r-- | dhall/src/operations.rs | 37 | ||||
-rw-r--r-- | dhall/src/semantics/nze/nir.rs | 7 | ||||
-rw-r--r-- | dhall/src/semantics/resolve/resolve.rs | 7 | ||||
-rw-r--r-- | dhall/src/semantics/tck/tir.rs | 3 | ||||
-rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 6 | ||||
-rw-r--r-- | dhall/src/syntax/ast/expr.rs | 69 | ||||
-rw-r--r-- | dhall/src/syntax/binary/decode.rs | 4 | ||||
-rw-r--r-- | dhall/src/syntax/binary/encode.rs | 8 | ||||
-rw-r--r-- | dhall/src/syntax/text/parser.rs | 48 | ||||
-rw-r--r-- | dhall/src/syntax/text/printer.rs | 48 | ||||
-rw-r--r-- | serde_dhall/src/value.rs | 3 |
12 files changed, 182 insertions, 180 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::*; diff --git a/serde_dhall/src/value.rs b/serde_dhall/src/value.rs index e8f333e..03cfdba 100644 --- a/serde_dhall/src/value.rs +++ b/serde_dhall/src/value.rs @@ -1,8 +1,9 @@ use std::collections::{BTreeMap, HashMap}; +use dhall::builtins::Builtin; use dhall::operations::OpKind; use dhall::semantics::{Hir, HirKind, Nir, NirKind}; -use dhall::syntax::{Builtin, Expr, ExprKind, NumKind, Span}; +use dhall::syntax::{Expr, ExprKind, NumKind, Span}; use crate::{Error, ErrorKind, FromDhall, Result, Sealed}; |