summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/core/context.rs (renamed from dhall/src/core/context.rs)11
-rw-r--r--dhall/src/semantics/core/mod.rs (renamed from dhall/src/core/mod.rs)0
-rw-r--r--dhall/src/semantics/core/value.rs (renamed from dhall/src/core/value.rs)17
-rw-r--r--dhall/src/semantics/core/valuef.rs (renamed from dhall/src/core/valuef.rs)14
-rw-r--r--dhall/src/semantics/core/var.rs (renamed from dhall/src/core/var.rs)10
-rw-r--r--dhall/src/semantics/error/mod.rs (renamed from dhall/src/error/mod.rs)11
-rw-r--r--dhall/src/semantics/mod.rs3
-rw-r--r--dhall/src/semantics/phase/mod.rs (renamed from dhall/src/phase/mod.rs)18
-rw-r--r--dhall/src/semantics/phase/normalize.rs (renamed from dhall/src/phase/normalize.rs)22
-rw-r--r--dhall/src/semantics/phase/parse.rs (renamed from dhall/src/phase/parse.rs)14
-rw-r--r--dhall/src/semantics/phase/resolve.rs (renamed from dhall/src/phase/resolve.rs)13
-rw-r--r--dhall/src/semantics/phase/typecheck.rs (renamed from dhall/src/phase/typecheck.rs)53
12 files changed, 90 insertions, 96 deletions
diff --git a/dhall/src/core/context.rs b/dhall/src/semantics/core/context.rs
index 2bf39c5..d150e56 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -1,12 +1,11 @@
use std::collections::HashMap;
use std::rc::Rc;
-use dhall_syntax::{Label, V};
-
-use crate::core::value::Value;
-use crate::core::valuef::ValueF;
-use crate::core::var::{AlphaVar, Shift, Subst};
-use crate::error::TypeError;
+use crate::semantics::core::value::Value;
+use crate::semantics::core::valuef::ValueF;
+use crate::semantics::core::var::{AlphaVar, Shift, Subst};
+use crate::semantics::error::TypeError;
+use crate::syntax::{Label, V};
#[derive(Debug, Clone)]
enum CtxItem {
diff --git a/dhall/src/core/mod.rs b/dhall/src/semantics/core/mod.rs
index 08213f7..08213f7 100644
--- a/dhall/src/core/mod.rs
+++ b/dhall/src/semantics/core/mod.rs
diff --git a/dhall/src/core/value.rs b/dhall/src/semantics/core/value.rs
index d4f5131..6e6739f 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -1,15 +1,14 @@
use std::cell::{Ref, RefCell, RefMut};
use std::rc::Rc;
-use dhall_syntax::{Builtin, Const, Span};
-
-use crate::core::context::TypecheckContext;
-use crate::core::valuef::ValueF;
-use crate::core::var::{AlphaVar, Shift, Subst};
-use crate::error::{TypeError, TypeMessage};
-use crate::phase::normalize::{apply_any, normalize_whnf};
-use crate::phase::typecheck::{builtin_to_value, const_to_value};
-use crate::phase::{NormalizedExpr, Typed};
+use crate::semantics::core::context::TypecheckContext;
+use crate::semantics::core::valuef::ValueF;
+use crate::semantics::core::var::{AlphaVar, Shift, Subst};
+use crate::semantics::error::{TypeError, TypeMessage};
+use crate::semantics::phase::normalize::{apply_any, normalize_whnf};
+use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value};
+use crate::semantics::phase::{NormalizedExpr, Typed};
+use crate::syntax::{Builtin, Const, Span};
#[derive(Debug, Clone, Copy)]
pub(crate) enum Form {
diff --git a/dhall/src/core/valuef.rs b/dhall/src/semantics/core/valuef.rs
index e5d0807..73c715a 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/semantics/core/valuef.rs
@@ -1,15 +1,15 @@
use std::collections::HashMap;
-use dhall_syntax::{
+use crate::semantics::core::value::{ToExprOptions, Value};
+use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
+use crate::semantics::phase::typecheck::rc;
+use crate::semantics::phase::{Normalized, NormalizedExpr};
+use crate::syntax;
+use crate::syntax::{
Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label,
NaiveDouble, Natural,
};
-use crate::core::value::{ToExprOptions, Value};
-use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
-use crate::phase::typecheck::rc;
-use crate::phase::{Normalized, NormalizedExpr};
-
/// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are
/// normalized on-demand.
/// If you compare for equality two `ValueF`s in WHNF, then equality will be up to
@@ -117,7 +117,7 @@ impl ValueF {
.collect(),
)),
ValueF::Equivalence(x, y) => rc(ExprF::BinOp(
- dhall_syntax::BinOp::Equivalence,
+ syntax::BinOp::Equivalence,
x.to_expr(opts),
y.to_expr(opts),
)),
diff --git a/dhall/src/core/var.rs b/dhall/src/semantics/core/var.rs
index 3795f10..184a372 100644
--- a/dhall/src/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -1,6 +1,6 @@
use std::collections::HashMap;
-use dhall_syntax::{Label, V};
+use crate::syntax::{ExprF, InterpolatedTextContents, Label, V};
/// Stores a pair of variables: a normal one and one
/// that corresponds to the alpha-normalized version of the first one.
@@ -190,7 +190,7 @@ impl<T: Shift> Shift for std::cell::RefCell<T> {
}
}
-impl<T: Shift, E: Clone> Shift for dhall_syntax::ExprF<T, E> {
+impl<T: Shift, E: Clone> Shift for ExprF<T, E> {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(self.traverse_ref_with_special_handling_of_binders(
|v| Ok(v.shift(delta, var)?),
@@ -222,7 +222,7 @@ where
}
}
-impl<T: Shift> Shift for dhall_syntax::InterpolatedTextContents<T> {
+impl<T: Shift> Shift for InterpolatedTextContents<T> {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(self.traverse_ref(|x| Ok(x.shift(delta, var)?))?)
}
@@ -262,7 +262,7 @@ impl<S, T: Subst<S>> Subst<S> for std::cell::RefCell<T> {
}
}
-impl<S: Shift, T: Subst<S>, E: Clone> Subst<S> for dhall_syntax::ExprF<T, E> {
+impl<S: Shift, T: Subst<S>, E: Clone> Subst<S> for ExprF<T, E> {
fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
self.map_ref_with_special_handling_of_binders(
|v| v.subst_shift(var, val),
@@ -277,7 +277,7 @@ impl<S, T: Subst<S>> Subst<S> for Vec<T> {
}
}
-impl<S, T: Subst<S>> Subst<S> for dhall_syntax::InterpolatedTextContents<T> {
+impl<S, T: Subst<S>> Subst<S> for InterpolatedTextContents<T> {
fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
self.map_ref(|x| x.subst_shift(var, val))
}
diff --git a/dhall/src/error/mod.rs b/dhall/src/semantics/error/mod.rs
index e4baea0..1288c12 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/semantics/error/mod.rs
@@ -1,11 +1,10 @@
use std::io::Error as IOError;
-use dhall_syntax::{BinOp, Import, Label, ParseError, Span};
-
-use crate::core::context::TypecheckContext;
-use crate::core::value::Value;
-use crate::phase::resolve::ImportStack;
-use crate::phase::NormalizedExpr;
+use crate::semantics::core::context::TypecheckContext;
+use crate::semantics::core::value::Value;
+use crate::semantics::phase::resolve::ImportStack;
+use crate::semantics::phase::NormalizedExpr;
+use crate::syntax::{BinOp, Import, Label, ParseError, Span};
pub type Result<T> = std::result::Result<T, Error>;
diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs
new file mode 100644
index 0000000..9d2e462
--- /dev/null
+++ b/dhall/src/semantics/mod.rs
@@ -0,0 +1,3 @@
+pub mod core;
+pub mod error;
+pub mod phase;
diff --git a/dhall/src/phase/mod.rs b/dhall/src/semantics/phase/mod.rs
index 337ce3d..752c257 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/semantics/phase/mod.rs
@@ -1,16 +1,14 @@
use std::fmt::Display;
use std::path::Path;
-use dhall_syntax::{Builtin, Const, Expr};
-
-use crate::core::value::{ToExprOptions, Value};
-use crate::core::valuef::ValueF;
-use crate::core::var::{AlphaVar, Shift, Subst};
-use crate::error::{EncodeError, Error, ImportError, TypeError};
-
+use crate::semantics::core::value::{ToExprOptions, Value};
+use crate::semantics::core::valuef::ValueF;
+use crate::semantics::core::var::{AlphaVar, Shift, Subst};
+use crate::semantics::error::{EncodeError, Error, ImportError, TypeError};
+use crate::syntax::binary;
+use crate::syntax::{Builtin, Const, Expr};
use resolve::ImportRoot;
-pub(crate) mod binary;
pub(crate) mod normalize;
pub(crate) mod parse;
pub(crate) mod resolve;
@@ -62,7 +60,7 @@ impl Parsed {
}
pub fn encode(&self) -> Result<Vec<u8>, EncodeError> {
- crate::phase::binary::encode(&self.0)
+ binary::encode(&self.0)
}
}
@@ -172,7 +170,7 @@ impl Typed {
impl Normalized {
pub fn encode(&self) -> Result<Vec<u8>, EncodeError> {
- crate::phase::binary::encode(&self.to_expr())
+ binary::encode(&self.to_expr())
}
pub(crate) fn to_expr(&self) -> NormalizedExpr {
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index b712027..81c3ce1 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -1,21 +1,21 @@
use std::collections::HashMap;
-use dhall_syntax::Const::Type;
-use dhall_syntax::{
+use crate::semantics::core::value::Value;
+use crate::semantics::core::valuef::ValueF;
+use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
+use crate::semantics::phase::Normalized;
+use crate::syntax;
+use crate::syntax::Const::Type;
+use crate::syntax::{
BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, Label,
NaiveDouble,
};
-use crate::core::value::Value;
-use crate::core::valuef::ValueF;
-use crate::core::var::{AlphaLabel, Shift, Subst};
-use crate::phase::Normalized;
-
// Ad-hoc macro to help construct closures
macro_rules! make_closure {
(#$var:ident) => { $var.clone() };
(var($var:ident, $n:expr, $($ty:tt)*)) => {{
- let var = crate::core::var::AlphaVar::from_var_and_alpha(
+ let var = AlphaVar::from_var_and_alpha(
Label::from(stringify!($var)).into(),
$n
);
@@ -47,7 +47,7 @@ macro_rules! make_closure {
}};
(1 + $($rest:tt)*) => {
ValueF::PartialExpr(ExprF::BinOp(
- dhall_syntax::BinOp::NaturalPlus,
+ syntax::BinOp::NaturalPlus,
make_closure!($($rest)*),
Value::from_valuef_and_type(
ValueF::NaturalLit(1),
@@ -62,7 +62,7 @@ macro_rules! make_closure {
let tail = make_closure!($($tail)*);
let list_type = tail.get_type_not_sort();
ValueF::PartialExpr(ExprF::BinOp(
- dhall_syntax::BinOp::ListAppend,
+ syntax::BinOp::ListAppend,
ValueF::NEListLit(vec![head])
.into_value_with_type(list_type.clone()),
tail,
@@ -76,7 +76,7 @@ pub(crate) fn apply_builtin(
args: Vec<Value>,
ty: &Value,
) -> ValueF {
- use dhall_syntax::Builtin::*;
+ use syntax::Builtin::*;
use ValueF::*;
// Small helper enum
diff --git a/dhall/src/phase/parse.rs b/dhall/src/semantics/phase/parse.rs
index 540ceea..4c8ad7b 100644
--- a/dhall/src/phase/parse.rs
+++ b/dhall/src/semantics/phase/parse.rs
@@ -2,11 +2,11 @@ use std::fs::File;
use std::io::Read;
use std::path::Path;
-use dhall_syntax::parse_expr;
-
-use crate::error::Error;
-use crate::phase::resolve::ImportRoot;
-use crate::phase::Parsed;
+use crate::semantics::error::Error;
+use crate::semantics::phase::resolve::ImportRoot;
+use crate::semantics::phase::Parsed;
+use crate::syntax::binary;
+use crate::syntax::parse_expr;
pub(crate) fn parse_file(f: &Path) -> Result<Parsed, Error> {
let mut buffer = String::new();
@@ -23,7 +23,7 @@ pub(crate) fn parse_str(s: &str) -> Result<Parsed, Error> {
}
pub(crate) fn parse_binary(data: &[u8]) -> Result<Parsed, Error> {
- let expr = crate::phase::binary::decode(data)?;
+ let expr = binary::decode(data)?;
let root = ImportRoot::LocalDir(std::env::current_dir()?);
Ok(Parsed(expr, root))
}
@@ -31,7 +31,7 @@ pub(crate) fn parse_binary(data: &[u8]) -> Result<Parsed, Error> {
pub(crate) fn parse_binary_file(f: &Path) -> Result<Parsed, Error> {
let mut buffer = Vec::new();
File::open(f)?.read_to_end(&mut buffer)?;
- let expr = crate::phase::binary::decode(&buffer)?;
+ let expr = binary::decode(&buffer)?;
let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned());
Ok(Parsed(expr, root))
}
diff --git a/dhall/src/phase/resolve.rs b/dhall/src/semantics/phase/resolve.rs
index c302bfa..86dc7ae 100644
--- a/dhall/src/phase/resolve.rs
+++ b/dhall/src/semantics/phase/resolve.rs
@@ -1,11 +1,12 @@
use std::collections::HashMap;
use std::path::{Path, PathBuf};
-use crate::error::{Error, ImportError};
-use crate::phase::{Normalized, NormalizedExpr, Parsed, Resolved};
-use dhall_syntax::{FilePath, ImportLocation, URL};
+use crate::semantics::error::{Error, ImportError};
+use crate::semantics::phase::{Normalized, NormalizedExpr, Parsed, Resolved};
+use crate::syntax;
+use crate::syntax::{FilePath, ImportLocation, URL};
-type Import = dhall_syntax::Import<NormalizedExpr>;
+type Import = syntax::Import<NormalizedExpr>;
/// A root from which to resolve relative imports.
#[derive(Debug, Clone, PartialEq, Eq)]
@@ -24,8 +25,8 @@ fn resolve_import(
import_stack: &ImportStack,
) -> Result<Normalized, ImportError> {
use self::ImportRoot::*;
- use dhall_syntax::FilePrefix::*;
- use dhall_syntax::ImportLocation::*;
+ use syntax::FilePrefix::*;
+ use syntax::ImportLocation::*;
let cwd = match root {
LocalDir(cwd) => cwd,
};
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index ef8340d..59380a3 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -1,24 +1,25 @@
use std::cmp::max;
use std::collections::HashMap;
-use dhall_syntax::{
+use crate::semantics::core::context::TypecheckContext;
+use crate::semantics::core::value::Value;
+use crate::semantics::core::valuef::ValueF;
+use crate::semantics::core::var::{Shift, Subst};
+use crate::semantics::error::{TypeError, TypeMessage};
+use crate::semantics::phase::normalize::merge_maps;
+use crate::semantics::phase::Normalized;
+use crate::syntax;
+use crate::syntax::{
Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, RawExpr, Span,
};
-use crate::core::context::TypecheckContext;
-use crate::core::value::Value;
-use crate::core::valuef::ValueF;
-use crate::core::var::{Shift, Subst};
-use crate::error::{TypeError, TypeMessage};
-use crate::phase::Normalized;
-
fn tck_pi_type(
ctx: &TypecheckContext,
x: Label,
tx: Value,
te: Value,
) -> Result<Value, TypeError> {
- use crate::error::TypeMessage::*;
+ use TypeMessage::*;
let ctx2 = ctx.insert_type(&x, tx.clone());
let ka = match tx.get_type()?.as_const() {
@@ -48,8 +49,8 @@ fn tck_record_type(
ctx: &TypecheckContext,
kts: impl IntoIterator<Item = Result<(Label, Value), TypeError>>,
) -> Result<Value, TypeError> {
- use crate::error::TypeMessage::*;
use std::collections::hash_map::Entry;
+ use TypeMessage::*;
let mut new_kts = HashMap::new();
// An empty record type has type Type
let mut k = Const::Type;
@@ -83,8 +84,8 @@ fn tck_union_type<Iter>(
where
Iter: IntoIterator<Item = Result<(Label, Option<Value>), TypeError>>,
{
- use crate::error::TypeMessage::*;
use std::collections::hash_map::Entry;
+ use TypeMessage::*;
let mut new_kts = HashMap::new();
// Check that all types are the same const
let mut k = None;
@@ -155,7 +156,7 @@ macro_rules! make_type {
(Double) => { ExprF::Builtin(Builtin::Double) };
(Text) => { ExprF::Builtin(Builtin::Text) };
($var:ident) => {
- ExprF::Var(dhall_syntax::V(stringify!($var).into(), 0))
+ ExprF::Var(syntax::V(stringify!($var).into(), 0))
};
(Optional $ty:ident) => {
ExprF::App(
@@ -170,7 +171,7 @@ macro_rules! make_type {
)
};
({ $($label:ident : $ty:ident),* }) => {{
- let mut kts = dhall_syntax::map::DupTreeMap::new();
+ let mut kts = syntax::map::DupTreeMap::new();
$(
kts.insert(
Label::from(stringify!($label)),
@@ -203,7 +204,7 @@ macro_rules! make_type {
}
fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
- use dhall_syntax::Builtin::*;
+ use syntax::Builtin::*;
rc(match b {
Bool | Natural | Integer | Double | Text => make_type!(Type),
List | Optional => make_type!(
@@ -303,7 +304,7 @@ fn type_with(
ctx: &TypecheckContext,
e: Expr<Normalized>,
) -> Result<Value, TypeError> {
- use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var};
+ use syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var};
let span = e.span();
Ok(match e.as_ref() {
@@ -361,11 +362,11 @@ fn type_last_layer(
e: ExprF<Value, Normalized>,
span: Span,
) -> Result<Value, TypeError> {
- use crate::error::TypeMessage::*;
- use dhall_syntax::BinOp::*;
- use dhall_syntax::Builtin::*;
- use dhall_syntax::Const::Type;
- use dhall_syntax::ExprF::*;
+ use syntax::BinOp::*;
+ use syntax::Builtin::*;
+ use syntax::Const::Type;
+ use syntax::ExprF::*;
+ use TypeMessage::*;
let mkerr = |msg: TypeMessage| Err(TypeError::new(ctx, msg));
/// Intermediary return type
@@ -434,7 +435,7 @@ fn type_last_layer(
}
EmptyListLit(t) => {
match &*t.as_whnf() {
- ValueF::AppliedBuiltin(dhall_syntax::Builtin::List, args)
+ ValueF::AppliedBuiltin(syntax::Builtin::List, args)
if args.len() == 1 => {}
_ => return mkerr(InvalidListType(t.clone())),
}
@@ -457,7 +458,7 @@ fn type_last_layer(
return mkerr(InvalidListType(t));
}
- RetTypeOnly(Value::from_builtin(dhall_syntax::Builtin::List).app(t))
+ RetTypeOnly(Value::from_builtin(syntax::Builtin::List).app(t))
}
SomeLit(x) => {
let t = x.get_type()?;
@@ -465,9 +466,7 @@ fn type_last_layer(
return mkerr(InvalidOptionalType(t));
}
- RetTypeOnly(
- Value::from_builtin(dhall_syntax::Builtin::Optional).app(t),
- )
+ RetTypeOnly(Value::from_builtin(syntax::Builtin::Optional).app(t))
}
RecordType(kts) => RetWhole(tck_record_type(
ctx,
@@ -548,8 +547,6 @@ fn type_last_layer(
RetTypeOnly(text_type)
}
BinOp(RightBiasedRecordMerge, l, r) => {
- use crate::phase::normalize::merge_maps;
-
let l_type = l.get_type()?;
let r_type = r.get_type()?;
@@ -589,8 +586,6 @@ fn type_last_layer(
Span::Artificial,
)?),
BinOp(RecursiveRecordTypeMerge, l, r) => {
- use crate::phase::normalize::merge_maps;
-
// Extract the LHS record type
let borrow_l = l.as_whnf();
let kts_x = match &*borrow_l {
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-06 18:14:34 +0000