From 78e9e32e1357d50313287dd2a3c437132c83aeb6 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 15 Dec 2019 20:10:54 +0000 Subject: Move contents of dhall_syntax to dhall --- dhall/src/syntax/core/context.rs | 80 ++++ dhall/src/syntax/core/expr.rs | 377 ++++++++++++++++ dhall/src/syntax/core/import.rs | 130 ++++++ dhall/src/syntax/core/label.rs | 34 ++ dhall/src/syntax/core/map.rs | 394 ++++++++++++++++ dhall/src/syntax/core/mod.rs | 13 + dhall/src/syntax/core/span.rs | 81 ++++ dhall/src/syntax/core/text.rs | 181 ++++++++ dhall/src/syntax/core/visitor.rs | 360 +++++++++++++++ dhall/src/syntax/mod.rs | 15 + dhall/src/syntax/parser.rs | 942 +++++++++++++++++++++++++++++++++++++++ dhall/src/syntax/printer.rs | 500 +++++++++++++++++++++ 12 files changed, 3107 insertions(+) create mode 100644 dhall/src/syntax/core/context.rs create mode 100644 dhall/src/syntax/core/expr.rs create mode 100644 dhall/src/syntax/core/import.rs create mode 100644 dhall/src/syntax/core/label.rs create mode 100644 dhall/src/syntax/core/map.rs create mode 100644 dhall/src/syntax/core/mod.rs create mode 100644 dhall/src/syntax/core/span.rs create mode 100644 dhall/src/syntax/core/text.rs create mode 100644 dhall/src/syntax/core/visitor.rs create mode 100644 dhall/src/syntax/mod.rs create mode 100644 dhall/src/syntax/parser.rs create mode 100644 dhall/src/syntax/printer.rs (limited to 'dhall/src/syntax') diff --git a/dhall/src/syntax/core/context.rs b/dhall/src/syntax/core/context.rs new file mode 100644 index 0000000..6844baa --- /dev/null +++ b/dhall/src/syntax/core/context.rs @@ -0,0 +1,80 @@ +use std::cmp::Eq; +use std::collections::HashMap; +use std::hash::Hash; + +/// A `(Context a)` associates `Text` labels with values of type `a` +/// +/// The `Context` is used for type-checking when `(a = Expr)` +/// +/// * You create a `Context` using `empty` and `insert` +/// * You transform a `Context` using `fmap` +/// * You consume a `Context` using `lookup` and `toList` +/// +/// The difference between a `Context` and a `Map` is that a `Context` lets you +/// have multiple ordered occurrences of the same key and you can query for the +/// `n`th occurrence of a given key. +/// +#[derive(Debug, Clone)] +pub struct Context(HashMap>); + +impl Context { + /// An empty context with no key-value pairs + pub fn new() -> Self { + Context(HashMap::new()) + } + + /// Look up a key by name and index + /// + /// ```c + /// lookup _ _ empty = Nothing + /// lookup k 0 (insert k v c) = Just v + /// lookup k n (insert k v c) = lookup k (n - 1) c -- 1 <= n + /// lookup k n (insert j v c) = lookup k n c -- k /= j + /// ``` + pub fn lookup<'a>(&'a self, k: &K, n: usize) -> Option<&'a T> { + self.0.get(k).and_then(|v| { + if n < v.len() { + v.get(v.len() - 1 - n) + } else { + None + } + }) + } + + pub fn map U>(&self, f: F) -> Context { + Context( + self.0 + .iter() + .map(|(k, vs)| { + ((*k).clone(), vs.iter().map(|v| f(k, v)).collect()) + }) + .collect(), + ) + } + + pub fn lookup_all<'a>(&'a self, k: &K) -> impl Iterator { + self.0.get(k).into_iter().flat_map(|v| v.iter()) + } + + pub fn iter(&self) -> impl Iterator { + self.0 + .iter() + .flat_map(|(k, vs)| vs.iter().map(move |v| (k, v))) + } + + pub fn iter_keys(&self) -> impl Iterator)> { + self.0.iter() + } +} + +impl Context { + /// Add a key-value pair to the `Context` + pub fn insert(&self, k: K, v: T) -> Self { + let mut ctx = (*self).clone(); + { + let m = ctx.0.entry(k).or_insert_with(Vec::new); + m.push(v); + } + ctx + } +} diff --git a/dhall/src/syntax/core/expr.rs b/dhall/src/syntax/core/expr.rs new file mode 100644 index 0000000..7972283 --- /dev/null +++ b/dhall/src/syntax/core/expr.rs @@ -0,0 +1,377 @@ +use crate::syntax::map::{DupTreeMap, DupTreeSet}; +use crate::syntax::visitor::{self, ExprFMutVisitor, ExprFVisitor}; +use crate::syntax::*; + +pub type Integer = isize; +pub type Natural = usize; +pub type Double = NaiveDouble; + +pub fn trivial_result(x: Result) -> T { + match x { + Ok(x) => x, + Err(e) => e, + } +} + +/// Double with bitwise equality +#[derive(Debug, Copy, Clone)] +pub struct NaiveDouble(f64); + +impl PartialEq for NaiveDouble { + fn eq(&self, other: &Self) -> bool { + self.0.to_bits() == other.0.to_bits() + } +} + +impl Eq for NaiveDouble {} + +impl std::hash::Hash for NaiveDouble { + fn hash(&self, state: &mut H) + where + H: std::hash::Hasher, + { + self.0.to_bits().hash(state) + } +} + +impl From for NaiveDouble { + fn from(x: f64) -> Self { + NaiveDouble(x) + } +} + +impl From for f64 { + fn from(x: NaiveDouble) -> f64 { + x.0 + } +} + +/// Constants for a pure type system +#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub enum Const { + Type, + Kind, + Sort, +} + +/// Bound variable +/// +/// The `Label` field is the variable's name (i.e. \"`x`\"). +/// The `Int` field is a DeBruijn index. +/// See dhall-lang/standard/semantics.md for details +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +pub struct V