From 45be2ff1f5bb3d6e0faa098402adf985b3d5e7ca Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 4 May 2019 12:38:36 +0200 Subject: Rename dhall_core to dhall_syntax --- dhall_syntax/Cargo.toml | 16 + dhall_syntax/src/context.rs | 80 ++++ dhall_syntax/src/core.rs | 563 +++++++++++++++++++++++++ dhall_syntax/src/import.rs | 64 +++ dhall_syntax/src/label.rs | 34 ++ dhall_syntax/src/lib.rs | 28 ++ dhall_syntax/src/parser.rs | 984 ++++++++++++++++++++++++++++++++++++++++++++ dhall_syntax/src/printer.rs | 498 ++++++++++++++++++++++ dhall_syntax/src/text.rs | 116 ++++++ dhall_syntax/src/visitor.rs | 667 ++++++++++++++++++++++++++++++ 10 files changed, 3050 insertions(+) create mode 100644 dhall_syntax/Cargo.toml create mode 100644 dhall_syntax/src/context.rs create mode 100644 dhall_syntax/src/core.rs create mode 100644 dhall_syntax/src/import.rs create mode 100644 dhall_syntax/src/label.rs create mode 100644 dhall_syntax/src/lib.rs create mode 100644 dhall_syntax/src/parser.rs create mode 100644 dhall_syntax/src/printer.rs create mode 100644 dhall_syntax/src/text.rs create mode 100644 dhall_syntax/src/visitor.rs (limited to 'dhall_syntax') diff --git a/dhall_syntax/Cargo.toml b/dhall_syntax/Cargo.toml new file mode 100644 index 0000000..3e32930 --- /dev/null +++ b/dhall_syntax/Cargo.toml @@ -0,0 +1,16 @@ +[package] +name = "dhall_syntax" +version = "0.1.0" +authors = ["NanoTech ", "Nadrieril "] +license = "BSD-2-Clause" +edition = "2018" + +[lib] +doctest = false + +[dependencies] +itertools = "0.8.0" +percent-encoding = "1.0.1" +pest = "2.1" +dhall_generated_parser = { path = "../dhall_generated_parser" } +improved_slice_patterns = { version = "2.0.0", path = "../improved_slice_patterns" } diff --git a/dhall_syntax/src/context.rs b/dhall_syntax/src/context.rs new file mode 100644 index 0000000..55bfff5 --- /dev/null +++ b/dhall_syntax/src/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 X)` +/// +/// * 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<'a>(&'a self) -> impl Iterator { + self.0 + .iter() + .flat_map(|(k, vs)| vs.iter().map(move |v| (k, v))) + } + + pub fn iter_keys<'a>(&'a 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_syntax/src/core.rs b/dhall_syntax/src/core.rs new file mode 100644 index 0000000..3db07dd --- /dev/null +++ b/dhall_syntax/src/core.rs @@ -0,0 +1,563 @@ +#![allow(non_snake_case)] +use std::collections::BTreeMap; +use std::collections::HashMap; +use std::rc::Rc; + +use crate::context::Context; +use crate::visitor; +use crate::*; + +pub type Integer = isize; +pub type Natural = usize; +pub type Double = NaiveDouble; + +/// An empty type +#[derive(Debug, Copy, Clone, PartialEq, Eq)] +pub enum X {} + +pub fn trivial_result(x: Result) -> T { + match x { + Ok(x) => x, + Err(e) => match 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 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)] +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)] +pub struct V