summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/resolve
diff options
context:
space:
mode:
authorNadrieril Feneanar2020-02-19 17:25:57 +0000
committerGitHub2020-02-19 17:25:57 +0000
commitffbde252a850c7d96e1000e1be52792c41733a28 (patch)
treee668b7f764fb4981a802bc619e0b2ff62fa9ce16 /dhall/src/semantics/resolve
parente4b3a879907b6dcc75d25847ae21a23d0201aae1 (diff)
parent7cbfc1a0d32766a383d1f48902502adaa2234d2f (diff)
Merge pull request #131 from Nadrieril/hir
Decouple main expression types
Diffstat (limited to 'dhall/src/semantics/resolve')
-rw-r--r--dhall/src/semantics/resolve/env.rs104
-rw-r--r--dhall/src/semantics/resolve/hir.rs135
-rw-r--r--dhall/src/semantics/resolve/mod.rs6
-rw-r--r--dhall/src/semantics/resolve/resolve.rs231
4 files changed, 476 insertions, 0 deletions
diff --git a/dhall/src/semantics/resolve/env.rs b/dhall/src/semantics/resolve/env.rs
new file mode 100644
index 0000000..43676cc
--- /dev/null
+++ b/dhall/src/semantics/resolve/env.rs
@@ -0,0 +1,104 @@
+use std::collections::HashMap;
+
+use crate::error::{Error, ImportError};
+use crate::semantics::{AlphaVar, Import, TypedHir, VarEnv};
+use crate::syntax::{Label, V};
+
+/// Environment for resolving names.
+#[derive(Debug, Clone)]
+pub(crate) struct NameEnv {
+ names: Vec<Label>,
+}
+
+pub(crate) type ImportCache = HashMap<Import, TypedHir>;
+pub(crate) type ImportStack = Vec<Import>;
+
+/// Environment for resolving imports
+#[derive(Debug, Clone)]
+pub(crate) struct ImportEnv {
+ cache: ImportCache,
+ stack: ImportStack,
+}
+
+impl NameEnv {
+ pub fn new() -> Self {
+ NameEnv { names: Vec::new() }
+ }
+ pub fn as_varenv(&self) -> VarEnv {
+ VarEnv::from_size(self.names.len())
+ }
+
+ pub fn insert(&self, x: &Label) -> Self {
+ let mut env = self.clone();
+ env.insert_mut(x);
+ env
+ }
+ pub fn insert_mut(&mut self, x: &Label) {
+ self.names.push(x.clone())
+ }
+ pub fn remove_mut(&mut self) {
+ self.names.pop();
+ }
+
+ pub fn unlabel_var(&self, var: &V) -> Option<AlphaVar> {
+ let V(name, idx) = var;
+ let (idx, _) = self
+ .names
+ .iter()
+ .rev()
+ .enumerate()
+ .filter(|(_, n)| *n == name)
+ .nth(*idx)?;
+ Some(AlphaVar::new(idx))
+ }
+ pub fn label_var(&self, var: &AlphaVar) -> V {
+ let name = &self.names[self.names.len() - 1 - var.idx()];
+ let idx = self
+ .names
+ .iter()
+ .rev()
+ .take(var.idx())
+ .filter(|n| *n == name)
+ .count();
+ V(name.clone(), idx)
+ }
+}
+
+impl ImportEnv {
+ pub fn new() -> Self {
+ ImportEnv {
+ cache: HashMap::new(),
+ stack: Vec::new(),
+ }
+ }
+
+ pub fn handle_import(
+ &mut self,
+ import: Import,
+ mut do_resolve: impl FnMut(&mut Self, &Import) -> Result<TypedHir, Error>,
+ ) -> Result<TypedHir, Error> {
+ if self.stack.contains(&import) {
+ return Err(
+ ImportError::ImportCycle(self.stack.clone(), import).into()
+ );
+ }
+ Ok(match self.cache.get(&import) {
+ Some(expr) => expr.clone(),
+ None => {
+ // Push the current import on the stack
+ self.stack.push(import.clone());
+
+ // Resolve the import recursively
+ let expr = do_resolve(self, &import)?;
+
+ // Remove import from the stack.
+ self.stack.pop();
+
+ // Add the import to the cache
+ self.cache.insert(import, expr.clone());
+
+ expr
+ }
+ })
+ }
+}
diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs
new file mode 100644
index 0000000..2f3464a
--- /dev/null
+++ b/dhall/src/semantics/resolve/hir.rs
@@ -0,0 +1,135 @@
+use crate::error::TypeError;
+use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv, Type};
+use crate::syntax::{Expr, ExprKind, Span, V};
+use crate::{NormalizedExpr, ToExprOptions};
+
+/// Stores an alpha-normalized variable.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
+pub struct AlphaVar {
+ idx: usize,
+}
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) enum HirKind {
+ /// A resolved variable (i.e. a DeBruijn index)
+ Var(AlphaVar),
+ /// Result of resolving an import.
+ Import(Hir, Type),
+ // Forbidden ExprKind variants: Var, Import, Completion
+ Expr(ExprKind<Hir>),
+}
+
+// An expression with resolved variables and imports.
+#[derive(Debug, Clone)]
+pub(crate) struct Hir {
+ kind: Box<HirKind>,
+ span: Span,
+}
+
+impl AlphaVar {
+ pub(crate) fn new(idx: usize) -> Self {
+ AlphaVar { idx }
+ }
+ pub(crate) fn idx(&self) -> usize {
+ self.idx
+ }
+}
+
+impl Hir {
+ pub fn new(kind: HirKind, span: Span) -> Self {
+ Hir {
+ kind: Box::new(kind),
+ span,
+ }
+ }
+
+ pub fn kind(&self) -> &HirKind {
+ &*self.kind
+ }
+ pub fn span(&self) -> Span {
+ self.span.clone()
+ }
+
+ /// Converts a closed Hir expr back to the corresponding AST expression.
+ pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
+ hir_to_expr(self, opts, &mut NameEnv::new())
+ }
+ /// Converts a closed Hir expr back to the corresponding AST expression.
+ pub fn to_expr_noopts(&self) -> NormalizedExpr {
+ let opts = ToExprOptions { alpha: false };
+ self.to_expr(opts)
+ }
+ pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
+ let opts = ToExprOptions { alpha: false };
+ let mut env = env.as_nameenv().clone();
+ hir_to_expr(self, opts, &mut env)
+ }
+
+ /// Typecheck the Hir.
+ pub fn typecheck<'hir>(
+ &'hir self,
+ env: &TyEnv,
+ ) -> Result<Tir<'hir>, TypeError> {
+ type_with(env, self, None)
+ }
+
+ /// Eval the Hir. It will actually get evaluated only as needed on demand.
+ pub fn eval(&self, env: impl Into<NzEnv>) -> Nir {
+ Nir::new_thunk(env.into(), self.clone())
+ }
+ /// Eval a closed Hir (i.e. without free variables). It will actually get evaluated only as
+ /// needed on demand.
+ pub fn eval_closed_expr(&self) -> Nir {
+ self.eval(NzEnv::new())
+ }
+ /// Eval a closed Hir fully and recursively;
+ pub fn rec_eval_closed_expr(&self) -> Nir {
+ let val = self.eval_closed_expr();
+ val.normalize();
+ val
+ }
+}
+
+fn hir_to_expr(
+ hir: &Hir,
+ opts: ToExprOptions,
+ env: &mut NameEnv,
+) -> NormalizedExpr {
+ let kind = match hir.kind() {
+ HirKind::Var(v) if opts.alpha => ExprKind::Var(V("_".into(), v.idx())),
+ HirKind::Var(v) => ExprKind::Var(env.label_var(v)),
+ HirKind::Import(hir, _) => {
+ return hir_to_expr(hir, opts, &mut NameEnv::new())
+ }
+ HirKind::Expr(e) => {
+ let e = e.map_ref_maybe_binder(|l, hir| {
+ if let Some(l) = l {
+ env.insert_mut(l);
+ }
+ let e = hir_to_expr(hir, opts, env);
+ if let Some(_) = l {
+ env.remove_mut();
+ }
+ e
+ });
+
+ match e {
+ ExprKind::Lam(_, t, e) if opts.alpha => {
+ ExprKind::Lam("_".into(), t, e)
+ }
+ ExprKind::Pi(_, t, e) if opts.alpha => {
+ ExprKind::Pi("_".into(), t, e)
+ }
+ e => e,
+ }
+ }
+ };
+ Expr::new(kind, hir.span())
+}
+
+impl std::cmp::PartialEq for Hir {
+ fn eq(&self, other: &Self) -> bool {
+ self.kind == other.kind
+ }
+}
+impl std::cmp::Eq for Hir {}
diff --git a/dhall/src/semantics/resolve/mod.rs b/dhall/src/semantics/resolve/mod.rs
new file mode 100644
index 0000000..517907b
--- /dev/null
+++ b/dhall/src/semantics/resolve/mod.rs
@@ -0,0 +1,6 @@
+pub mod env;
+pub mod hir;
+pub mod resolve;
+pub(crate) use env::*;
+pub(crate) use hir::*;
+pub(crate) use resolve::*;
diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs
new file mode 100644
index 0000000..82800ec
--- /dev/null
+++ b/dhall/src/semantics/resolve/resolve.rs
@@ -0,0 +1,231 @@
+use std::borrow::Cow;
+use std::path::{Path, PathBuf};
+
+use crate::error::ErrorBuilder;
+use crate::error::{Error, ImportError};
+use crate::semantics::{mkerr, Hir, HirKind, ImportEnv, NameEnv, Type};
+use crate::syntax;
+use crate::syntax::{BinOp, Expr, ExprKind, FilePath, ImportLocation, URL};
+use crate::{Parsed, ParsedExpr, Resolved};
+
+// TODO: evaluate import headers
+pub(crate) type Import = syntax::Import<()>;
+
+/// Owned Hir with a type. Different from Tir because the Hir is owned.
+pub(crate) type TypedHir = (Hir, Type);
+
+/// A root from which to resolve relative imports.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) enum ImportRoot {
+ LocalDir(PathBuf),
+}
+
+fn resolve_one_import(
+ env: &mut ImportEnv,
+ import: &Import,
+ root: &ImportRoot,
+) -> Result<TypedHir, Error> {
+ use self::ImportRoot::*;
+ use syntax::FilePrefix::*;
+ use syntax::ImportLocation::*;
+ let cwd = match root {
+ LocalDir(cwd) => cwd,
+ };
+ match &import.location {
+ Local(prefix, path) => {
+ let path_buf: PathBuf = path.file_path.iter().collect();
+ let path_buf = match prefix {
+ // TODO: fail gracefully
+ Parent => cwd.parent().unwrap().join(path_buf),
+ Here => cwd.join(path_buf),
+ _ => unimplemented!("{:?}", import),
+ };
+ Ok(load_import(env, &path_buf)?)
+ }
+ _ => unimplemented!("{:?}", import),
+ }
+}
+
+fn load_import(env: &mut ImportEnv, f: &Path) -> Result<TypedHir, Error> {
+ let parsed = Parsed::parse_file(f)?;
+ let typed = resolve_with_env(env, parsed)?.typecheck()?;
+ Ok((typed.normalize().to_hir(), typed.ty().clone()))
+}
+
+/// Desugar the first level of the expression.
+fn desugar(expr: &Expr) -> Cow<'_, Expr> {
+ match expr.kind() {
+ ExprKind::Completion(ty, compl) => {
+ let ty_field_default = Expr::new(
+ ExprKind::Field(ty.clone(), "default".into()),
+ expr.span(),
+ );
+ let merged = Expr::new(
+ ExprKind::BinOp(
+ BinOp::RightBiasedRecordMerge,
+ ty_field_default,
+ compl.clone(),
+ ),
+ expr.span(),
+ );
+ let ty_field_type = Expr::new(
+ ExprKind::Field(ty.clone(), "Type".into()),
+ expr.span(),
+ );
+ Cow::Owned(Expr::new(
+ ExprKind::Annot(merged, ty_field_type),
+ expr.span(),
+ ))
+ }
+ _ => Cow::Borrowed(expr),
+ }
+}
+
+/// Traverse the expression, handling import alternatives and passing
+/// found imports to the provided function. Also resolving names.
+fn traverse_resolve_expr(
+ name_env: &mut NameEnv,
+ expr: &Expr,
+ f: &mut impl FnMut(Import) -> Result<TypedHir, Error>,
+) -> Result<Hir, Error> {
+ let expr = desugar(expr);
+ Ok(match expr.kind() {
+ ExprKind::Var(var) => match name_env.unlabel_var(&var) {
+ Some(v) => Hir::new(HirKind::Var(v), expr.span()),
+ None => mkerr(
+ ErrorBuilder::new(format!("unbound variable `{}`", var))
+ .span_err(expr.span(), "not found in this scope")
+ .format(),
+ )?,
+ },
+ ExprKind::BinOp(BinOp::ImportAlt, l, r) => {
+ match traverse_resolve_expr(name_env, l, f) {
+ Ok(l) => l,
+ Err(_) => {
+ match traverse_resolve_expr(name_env, r, f) {
+ Ok(r) => r,
+ // TODO: keep track of the other error too
+ Err(e) => return Err(e),
+ }
+ }
+ }
+ }
+ kind => {
+ let kind = kind.traverse_ref_maybe_binder(|l, e| {
+ if let Some(l) = l {
+ name_env.insert_mut(l);
+ }
+ let hir = traverse_resolve_expr(name_env, e, f)?;
+ if let Some(_) = l {
+ name_env.remove_mut();
+ }
+ Ok::<_, Error>(hir)
+ })?;
+ let kind = match kind {
+ ExprKind::Import(import) => {
+ // TODO: evaluate import headers
+ let import = import.traverse_ref(|_| Ok::<_, Error>(()))?;
+ let imported = f(import)?;
+ HirKind::Import(imported.0, imported.1)
+ }
+ kind => HirKind::Expr(kind),
+ };
+ Hir::new(kind, expr.span())
+ }
+ })
+}
+
+fn resolve_with_env(
+ env: &mut ImportEnv,
+ parsed: Parsed,
+) -> Result<Resolved, Error> {
+ let Parsed(expr, root) = parsed;
+ let resolved =
+ traverse_resolve_expr(&mut NameEnv::new(), &expr, &mut |import| {
+ env.handle_import(import, |env, import| {
+ resolve_one_import(env, import, &root)
+ })
+ })?;
+ Ok(Resolved(resolved))
+}
+
+pub(crate) fn resolve(parsed: Parsed) -> Result<Resolved, Error> {
+ resolve_with_env(&mut ImportEnv::new(), parsed)
+}
+
+pub(crate) fn skip_resolve(expr: &ParsedExpr) -> Result<Hir, Error> {
+ traverse_resolve_expr(&mut NameEnv::new(), expr, &mut |import| {
+ Err(ImportError::UnexpectedImport(import).into())
+ })
+}
+
+pub trait Canonicalize {
+ fn canonicalize(&self) -> Self;
+}
+
+impl Canonicalize for FilePath {
+ fn canonicalize(&self) -> FilePath {
+ let mut file_path = Vec::new();
+ let mut file_path_components = self.file_path.clone().into_iter();
+
+ loop {
+ let component = file_path_components.next();
+ match component.as_ref() {
+ // ───────────────────
+ // canonicalize(ε) = ε
+ None => break,
+
+ // canonicalize(directory₀) = directory₁
+ // ───────────────────────────────────────
+ // canonicalize(directory₀/.) = directory₁
+ Some(c) if c == "." => continue,
+
+ Some(c) if c == ".." => match file_path_components.next() {
+ // canonicalize(directory₀) = ε
+ // ────────────────────────────
+ // canonicalize(directory₀/..) = /..
+ None => file_path.push("..".to_string()),
+
+ // canonicalize(directory₀) = directory₁/..
+ // ──────────────────────────────────────────────
+ // canonicalize(directory₀/..) = directory₁/../..
+ Some(ref c) if c == ".." => {
+ file_path.push("..".to_string());
+ file_path.push("..".to_string());
+ }
+
+ // canonicalize(directory₀) = directory₁/component
+ // ─────────────────────────────────────────────── ; If "component" is not
+ // canonicalize(directory₀/..) = directory₁ ; ".."
+ Some(_) => continue,
+ },
+
+ // canonicalize(directory₀) = directory₁
+ // ───────────────────────────────────────────────────────── ; If no other
+ // canonicalize(directory₀/component) = directory₁/component ; rule matches
+ Some(c) => file_path.push(c.clone()),
+ }
+ }
+
+ FilePath { file_path }
+ }
+}
+
+impl<SE: Copy> Canonicalize for ImportLocation<SE> {
+ fn canonicalize(&self) -> ImportLocation<SE> {
+ match self {
+ ImportLocation::Local(prefix, file) => {
+ ImportLocation::Local(*prefix, file.canonicalize())
+ }
+ ImportLocation::Remote(url) => ImportLocation::Remote(URL {
+ scheme: url.scheme,
+ authority: url.authority.clone(),
+ path: url.path.canonicalize(),
+ query: url.query.clone(),
+ headers: url.headers.clone(),
+ }),
+ ImportLocation::Env(name) => ImportLocation::Env(name.to_string()),
+ ImportLocation::Missing => ImportLocation::Missing,
+ }
+ }
+}