diff options
author | Nadrieril | 2019-03-08 14:22:03 +0100 |
---|---|---|
committer | Nadrieril | 2019-03-08 14:22:03 +0100 |
commit | 7f9d988a3e0555123030f48f3759216ef2e14ec3 (patch) | |
tree | b7e1c0107ec5a76b9da4d04415b63efb4c59fdea | |
parent | 465c3d2b97cfebcf47cbcef1dc847e592d31f434 (diff) |
Generalise Context on its type of keys
-rw-r--r-- | dhall/src/typecheck.rs | 8 | ||||
-rw-r--r-- | dhall_core/src/context.rs | 18 | ||||
-rw-r--r-- | dhall_generator/src/lib.rs | 24 |
3 files changed, 28 insertions, 22 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index e36a6fa..23ab7a6 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -146,7 +146,7 @@ where } fn op2_type<'i, S, EF>( - ctx: &Context<'i, Expr<'i, S, X>>, + ctx: &Context<&'i str, Expr<'i, S, X>>, e: &Expr<'i, S, X>, t: core::Builtin, ef: EF, @@ -179,7 +179,7 @@ where /// is not necessary for just type-checking. If you actually care about the /// returned type then you may want to `normalize` it afterwards. pub fn type_with<'i, S>( - ctx: &Context<'i, Expr<'i, S, X>>, + ctx: &Context<&'i str, Expr<'i, S, X>>, e: &Expr<'i, S, X>, ) -> Result<Expr<'i, S, X>, TypeError<'i, S>> where @@ -773,14 +773,14 @@ pub enum TypeMessage<'i, S> { /// A structured type error that includes context #[derive(Debug)] pub struct TypeError<'i, S> { - pub context: Context<'i, Expr<'i, S, X>>, + pub context: Context<&'i str, Expr<'i, S, X>>, pub current: Expr<'i, S, X>, pub type_message: TypeMessage<'i, S>, } impl<'i, S: Clone> TypeError<'i, S> { pub fn new( - context: &Context<'i, Expr<'i, S, X>>, + context: &Context<&'i str, Expr<'i, S, X>>, current: &Expr<'i, S, X>, type_message: TypeMessage<'i, S>, ) -> Self { diff --git a/dhall_core/src/context.rs b/dhall_core/src/context.rs index b88a677..412d3f0 100644 --- a/dhall_core/src/context.rs +++ b/dhall_core/src/context.rs @@ -1,4 +1,6 @@ +use std::cmp::Eq; use std::collections::HashMap; +use std::hash::Hash; /// A `(Context a)` associates `Text` labels with values of type `a` /// @@ -13,9 +15,9 @@ use std::collections::HashMap; /// `n`th occurrence of a given key. /// #[derive(Debug, Clone)] -pub struct Context<'i, T>(HashMap<&'i str, Vec<T>>); +pub struct Context<K: Eq + Hash, T>(HashMap<K, Vec<T>>); -impl<'i, T> Context<'i, T> { +impl<K: Hash + Eq + Clone, T> Context<K, T> { /// An empty context with no key-value pairs pub fn new() -> Self { Context(HashMap::new()) @@ -29,23 +31,23 @@ impl<'i, T> Context<'i, T> { /// 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: &str, n: usize) -> Option<&'a T> { - self.0.get(k).and_then(|v| v.get(v.len() - 1 - n)) + pub fn lookup<'a>(&'a self, k: K, n: usize) -> Option<&'a T> { + self.0.get(&k).and_then(|v| v.get(v.len() - 1 - n)) } - pub fn map<U, F: Fn(&T) -> U>(&self, f: F) -> Context<'i, U> { + pub fn map<U, F: Fn(&T) -> U>(&self, f: F) -> Context<K, U> { Context( self.0 .iter() - .map(|(k, v)| (*k, v.iter().map(&f).collect())) + .map(|(k, v)| ((*k).clone(), v.iter().map(&f).collect())) .collect(), ) } } -impl<'i, T: Clone> Context<'i, T> { +impl<K: Hash + Eq + Clone, T: Clone> Context<K, T> { /// Add a key-value pair to the `Context` - pub fn insert(&self, k: &'i str, v: T) -> Self { + 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); diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs index b316f51..1cc62d0 100644 --- a/dhall_generator/src/lib.rs +++ b/dhall_generator/src/lib.rs @@ -4,6 +4,8 @@ use dhall_core::*; use proc_macro2::Literal; use proc_macro2::TokenStream; use quote::quote; +use std::fmt::Debug; +use std::hash::Hash; #[proc_macro] pub fn dhall(input: proc_macro::TokenStream) -> proc_macro::TokenStream { @@ -12,15 +14,15 @@ pub fn dhall(input: proc_macro::TokenStream) -> proc_macro::TokenStream { let no_import = |_: &Import| -> X { panic!("Don't use import in dhall!()") }; let expr = expr.map_embed(&no_import); - let output = dhall_to_tokenstream(&expr, &Context::new()); + let output = dhall_to_tokenstream::<&str>(&expr, &Context::new()); output.into() } // Returns an expression of type Expr<_, _>. Expects input variables // to be of type Box<Expr<_, _>> (future-proof for structural sharing). -fn dhall_to_tokenstream<'i>( - expr: &Expr<'i, X, X>, - ctx: &Context<'i, ()>, +fn dhall_to_tokenstream<L: Eq + Hash + Clone + Debug + Into<String>>( + expr: &Expr_<L, X, X>, + ctx: &Context<L, ()>, ) -> TokenStream { use dhall_core::Expr_::*; match expr { @@ -30,8 +32,8 @@ fn dhall_to_tokenstream<'i>( } Lam(x, t, b) => { let t = dhall_to_tokenstream_bx(t, ctx); - let b = dhall_to_tokenstream_bx(b, &ctx.insert(x, ())); - let x = Literal::string(x); + let b = dhall_to_tokenstream_bx(b, &ctx.insert(x.clone(), ())); + let x = Literal::string(&x.clone().into()); quote! { Lam(#x, #t, #b) } } App(f, a) => { @@ -74,20 +76,22 @@ fn dhall_to_tokenstream<'i>( } // Returns an expression of type Box<Expr<_, _>> -fn dhall_to_tokenstream_bx<'i>( - expr: &Expr<'i, X, X>, - ctx: &Context<'i, ()>, +fn dhall_to_tokenstream_bx<L: Eq + Hash + Clone + Debug + Into<String>>( + expr: &Expr_<L, X, X>, + ctx: &Context<L, ()>, ) -> TokenStream { use dhall_core::Expr_::*; match expr { Var(V(s, n)) => { - match ctx.lookup(s, *n) { + match ctx.lookup(s.clone(), *n) { // Non-free variable; interpolates as itself Some(()) => { + let s: String = s.clone().into(); quote! { bx(Var(V(#s, #n))) } } // Free variable; interpolates as a rust variable None => { + let s: String = s.clone().into(); // TODO: insert appropriate shifts ? let v: TokenStream = s.parse().unwrap(); quote! { { |