summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/builtins.rs19
-rw-r--r--dhall/src/lib.rs15
-rw-r--r--dhall/src/semantics/resolve/cache.rs2
-rw-r--r--dhall/src/semantics/resolve/hir.rs4
-rw-r--r--dhall/src/semantics/resolve/resolve.rs69
-rw-r--r--dhall/src/semantics/tck/typecheck.rs4
6 files changed, 74 insertions, 39 deletions
diff --git a/dhall/src/builtins.rs b/dhall/src/builtins.rs
index 39cc4ef..123e03d 100644
--- a/dhall/src/builtins.rs
+++ b/dhall/src/builtins.rs
@@ -2,15 +2,13 @@ use std::collections::{BTreeMap, HashMap};
use std::convert::TryInto;
use crate::operations::{BinOp, OpKind};
-use crate::semantics::{
- nze, skip_resolve_expr, typecheck, Hir, HirKind, Nir, NirKind, NzEnv,
- VarEnv,
-};
+use crate::semantics::{nze, Hir, HirKind, Nir, NirKind, NzEnv, VarEnv};
use crate::syntax::Const::Type;
use crate::syntax::{
Const, Expr, ExprKind, InterpolatedText, InterpolatedTextContents, Label,
NaiveDouble, NumKind, Span, UnspannedExpr, V,
};
+use crate::{Ctxt, Parsed};
/// Built-ins
#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
@@ -178,7 +176,7 @@ macro_rules! make_type {
};
}
-pub fn type_of_builtin<'cx>(b: Builtin) -> Hir<'cx> {
+pub fn type_of_builtin<'cx>(cx: Ctxt<'cx>, b: Builtin) -> Hir<'cx> {
use Builtin::*;
let expr = match b {
Bool | Natural | Integer | Double | Text => make_type!(Type),
@@ -253,7 +251,10 @@ pub fn type_of_builtin<'cx>(b: Builtin) -> Hir<'cx> {
forall (A: Type) -> Optional A
),
};
- skip_resolve_expr(&expr).unwrap()
+ Parsed::from_expr_without_imports(expr)
+ .resolve(cx)
+ .unwrap()
+ .0
}
// Ad-hoc macro to help construct closures
@@ -323,8 +324,12 @@ fn apply_builtin<'cx>(
DoneAsIs,
}
let make_closure = |e| {
- typecheck(cx, &skip_resolve_expr(&e).unwrap())
+ Parsed::from_expr_without_imports(e)
+ .resolve(cx)
+ .unwrap()
+ .typecheck(cx)
.unwrap()
+ .as_hir()
.eval(env.clone())
};
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 7f77334..c27b633 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -58,6 +58,11 @@ pub struct ToExprOptions {
}
impl Parsed {
+ /// Construct from an `Expr`. This `Expr` will have imports disabled.
+ pub fn from_expr_without_imports(e: Expr) -> Self {
+ Parsed(e, ImportLocation::dhall_code_without_imports())
+ }
+
pub fn parse_file(f: &Path) -> Result<Parsed, Error> {
parse::parse_file(f)
}
@@ -78,8 +83,11 @@ impl Parsed {
pub fn resolve<'cx>(self, cx: Ctxt<'cx>) -> Result<Resolved<'cx>, Error> {
resolve::resolve(cx, self)
}
- pub fn skip_resolve<'cx>(self) -> Result<Resolved<'cx>, Error> {
- resolve::skip_resolve(self)
+ pub fn skip_resolve<'cx>(
+ self,
+ cx: Ctxt<'cx>,
+ ) -> Result<Resolved<'cx>, Error> {
+ resolve::skip_resolve(cx, self)
}
/// Converts a value back to the corresponding AST expression.
@@ -122,6 +130,9 @@ impl<'cx> Typed<'cx> {
self.hir.to_expr(cx, ToExprOptions { alpha: false })
}
+ pub fn as_hir(&self) -> &Hir<'cx> {
+ &self.hir
+ }
pub fn ty(&self) -> &Type<'cx> {
&self.ty
}
diff --git a/dhall/src/semantics/resolve/cache.rs b/dhall/src/semantics/resolve/cache.rs
index 9a5e835..1fc8dd3 100644
--- a/dhall/src/semantics/resolve/cache.rs
+++ b/dhall/src/semantics/resolve/cache.rs
@@ -94,7 +94,7 @@ fn read_cache_file<'cx>(
}
}
- Ok(parse_binary(&data)?.skip_resolve()?.typecheck(cx)?)
+ Ok(parse_binary(&data)?.resolve(cx)?.typecheck(cx)?)
}
/// Write a file to the cache.
diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs
index cfde47e..3e282b4 100644
--- a/dhall/src/semantics/resolve/hir.rs
+++ b/dhall/src/semantics/resolve/hir.rs
@@ -1,5 +1,5 @@
use crate::error::TypeError;
-use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv};
+use crate::semantics::{type_with, typecheck, NameEnv, Nir, NzEnv, Tir, TyEnv};
use crate::syntax::{Expr, ExprKind, Span, V};
use crate::{Ctxt, ImportId, ToExprOptions};
@@ -81,7 +81,7 @@ impl<'cx> Hir<'cx> {
&'hir self,
cx: Ctxt<'cx>,
) -> Result<Tir<'cx, 'hir>, TypeError> {
- self.typecheck(&TyEnv::new(cx))
+ typecheck(cx, self)
}
/// Eval the Hir. It will actually get evaluated only as needed on demand.
diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs
index 011ed45..e040cf4 100644
--- a/dhall/src/semantics/resolve/resolve.rs
+++ b/dhall/src/semantics/resolve/resolve.rs
@@ -29,8 +29,10 @@ enum ImportLocationKind {
Remote(Url),
/// Environment variable
Env(String),
- /// Data without a location
+ /// Data without a location; chaining will start from current directory.
Missing,
+ /// Token to signal that thi sfile should contain no imports.
+ NoImport,
}
/// The location of some data.
@@ -101,6 +103,7 @@ impl ImportLocationKind {
url = url.join(&path.file_path.join("/"))?;
ImportLocationKind::Remote(url)
}
+ ImportLocationKind::NoImport => unreachable!(),
})
}
@@ -120,6 +123,7 @@ impl ImportLocationKind {
ImportLocationKind::Missing => {
return Err(ImportError::Missing.into())
}
+ ImportLocationKind::NoImport => unreachable!(),
})
}
@@ -134,6 +138,7 @@ impl ImportLocationKind {
ImportLocationKind::Missing => {
return Err(ImportError::Missing.into())
}
+ ImportLocationKind::NoImport => unreachable!(),
})
}
@@ -149,6 +154,7 @@ impl ImportLocationKind {
("Environment", Some(name.clone()))
}
ImportLocationKind::Missing => ("Missing", None),
+ ImportLocationKind::NoImport => unreachable!(),
};
let asloc_ty = make_aslocation_uniontype();
@@ -171,6 +177,12 @@ impl ImportLocation {
mode: ImportMode::Code,
}
}
+ pub fn dhall_code_without_imports() -> Self {
+ ImportLocation {
+ kind: ImportLocationKind::NoImport,
+ mode: ImportMode::Code,
+ }
+ }
pub fn local_dhall_code(path: PathBuf) -> Self {
ImportLocation {
kind: ImportLocationKind::Local(path),
@@ -191,6 +203,10 @@ impl ImportLocation {
fn chain(&self, import: &Import) -> Result<ImportLocation, Error> {
// Makes no sense to chain an import if the current file is not a dhall file.
assert!(matches!(self.mode, ImportMode::Code));
+ if matches!(self.kind, ImportLocationKind::NoImport) {
+ Err(ImportError::UnexpectedImport(import.clone()))?;
+ }
+
let kind = match &import.location {
ImportTarget::Local(prefix, path) => {
self.kind.chain_local(*prefix, path)?
@@ -232,30 +248,37 @@ impl ImportLocation {
env: &mut ImportEnv<'cx>,
span: Span,
) -> Result<Typed<'cx>, Error> {
- let (hir, ty) = match self.mode {
+ let cx = env.cx();
+ let typed = match self.mode {
ImportMode::Code => {
let parsed = self.kind.fetch_dhall()?;
- let typed =
- resolve_with_env(env, parsed)?.typecheck(env.cx())?;
- let hir = typed.normalize(env.cx()).to_hir();
- (hir, typed.ty)
+ let typed = resolve_with_env(env, parsed)?.typecheck(cx)?;
+ Typed {
+ // TODO: manage to keep the Nir around. Will need fixing variables.
+ hir: typed.normalize(cx).to_hir(),
+ ty: typed.ty,
+ }
}
ImportMode::RawText => {
let text = self.kind.fetch_text()?;
- let hir = Hir::new(
- HirKind::Expr(ExprKind::TextLit(text.into())),
- span,
- );
- (hir, Type::from_builtin(env.cx(), Builtin::Text))
+ Typed {
+ hir: Hir::new(
+ HirKind::Expr(ExprKind::TextLit(text.into())),
+ span,
+ ),
+ ty: Type::from_builtin(cx, Builtin::Text),
+ }
}
ImportMode::Location => {
let expr = self.kind.to_location();
- let hir = skip_resolve_expr(&expr)?;
- let ty = hir.typecheck_noenv(env.cx())?.ty().clone();
- (hir, ty)
+ Parsed::from_expr_without_imports(expr)
+ .resolve(cx)
+ .unwrap()
+ .typecheck(cx)
+ .unwrap()
}
};
- Ok(Typed { hir, ty })
+ Ok(typed)
}
}
@@ -476,16 +499,12 @@ pub fn resolve<'cx>(
resolve_with_env(&mut ImportEnv::new(cx), parsed)
}
-pub fn skip_resolve_expr<'cx>(expr: &Expr) -> Result<Hir<'cx>, Error> {
- traverse_resolve_expr(&mut NameEnv::new(), expr, &mut |import, _span| {
- Err(ImportError::UnexpectedImport(import).into())
- })
-}
-
-pub fn skip_resolve<'cx>(parsed: Parsed) -> Result<Resolved<'cx>, Error> {
- let Parsed(expr, _) = parsed;
- let resolved = skip_resolve_expr(&expr)?;
- Ok(Resolved(resolved))
+pub fn skip_resolve<'cx>(
+ cx: Ctxt<'cx>,
+ parsed: Parsed,
+) -> Result<Resolved<'cx>, Error> {
+ let parsed = Parsed::from_expr_without_imports(parsed.0);
+ Ok(resolve(cx, parsed)?)
}
pub trait Canonicalize {
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index f47563e..5a44c9c 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -62,8 +62,8 @@ fn type_one_layer<'cx>(
},
),
ExprKind::Builtin(b) => {
- let t_hir = type_of_builtin(b);
- typecheck(env.cx(), &t_hir)?.eval_to_type(env)?
+ let t_hir = type_of_builtin(cx, b);
+ typecheck(cx, &t_hir)?.eval_to_type(env)?
}
ExprKind::TextLit(interpolated) => {
let text_type = Type::from_builtin(cx, Builtin::Text);
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 05:16:56 +0000