From 7abd49772643ee4e131ef47de66db22ba7c1e037 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 15 Dec 2019 19:47:20 +0000 Subject: Move contents of dhall under a semantics submodule --- dhall/src/semantics/core/context.rs | 145 ++++++ dhall/src/semantics/core/mod.rs | 4 + dhall/src/semantics/core/value.rs | 338 ++++++++++++++ dhall/src/semantics/core/valuef.rs | 323 +++++++++++++ dhall/src/semantics/core/var.rs | 295 ++++++++++++ dhall/src/semantics/error/mod.rs | 179 ++++++++ dhall/src/semantics/mod.rs | 3 + dhall/src/semantics/phase/binary.rs | 748 ++++++++++++++++++++++++++++++ dhall/src/semantics/phase/mod.rs | 254 ++++++++++ dhall/src/semantics/phase/normalize.rs | 794 ++++++++++++++++++++++++++++++++ dhall/src/semantics/phase/parse.rs | 37 ++ dhall/src/semantics/phase/resolve.rs | 180 ++++++++ dhall/src/semantics/phase/typecheck.rs | 815 +++++++++++++++++++++++++++++++++ 13 files changed, 4115 insertions(+) create mode 100644 dhall/src/semantics/core/context.rs create mode 100644 dhall/src/semantics/core/mod.rs create mode 100644 dhall/src/semantics/core/value.rs create mode 100644 dhall/src/semantics/core/valuef.rs create mode 100644 dhall/src/semantics/core/var.rs create mode 100644 dhall/src/semantics/error/mod.rs create mode 100644 dhall/src/semantics/mod.rs create mode 100644 dhall/src/semantics/phase/binary.rs create mode 100644 dhall/src/semantics/phase/mod.rs create mode 100644 dhall/src/semantics/phase/normalize.rs create mode 100644 dhall/src/semantics/phase/parse.rs create mode 100644 dhall/src/semantics/phase/resolve.rs create mode 100644 dhall/src/semantics/phase/typecheck.rs (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs new file mode 100644 index 0000000..00e1493 --- /dev/null +++ b/dhall/src/semantics/core/context.rs @@ -0,0 +1,145 @@ +use std::collections::HashMap; +use std::rc::Rc; + +use crate::syntax::{Label, V}; + +use crate::core::value::Value; +use crate::core::valuef::ValueF; +use crate::core::var::{AlphaVar, Shift, Subst}; +use crate::error::TypeError; + +#[derive(Debug, Clone)] +enum CtxItem { + Kept(AlphaVar, Value), + Replaced(Value), +} + +#[derive(Debug, Clone)] +pub(crate) struct TypecheckContext(Rc>); + +impl TypecheckContext { + pub fn new() -> Self { + TypecheckContext(Rc::new(Vec::new())) + } + pub fn insert_type(&self, x: &Label, t: Value) -> Self { + let mut vec = self.0.as_ref().clone(); + vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x)))); + TypecheckContext(Rc::new(vec)) + } + pub fn insert_value(&self, x: &Label, e: Value) -> Result { + let mut vec = self.0.as_ref().clone(); + vec.push((x.clone(), CtxItem::Replaced(e))); + Ok(TypecheckContext(Rc::new(vec))) + } + pub fn lookup(&self, var: &V