diff --git a/crates/pikelet-driver/src/lib.rs b/crates/pikelet-driver/src/lib.rs
index 454290520..f0f52232c 100644
--- a/crates/pikelet-driver/src/lib.rs
+++ b/crates/pikelet-driver/src/lib.rs
@@ -146,7 +146,7 @@ use codespan::{CodeMap, FileMap, FileName};
use codespan_reporting::Diagnostic;
use std::sync::Arc;
-use pikelet_elaborate::{Import, TcEnv};
+use pikelet_elaborate::{Context, Import};
use pikelet_syntax::translation::{Desugar, DesugarEnv, Resugar};
use pikelet_syntax::{core, raw};
@@ -154,9 +154,9 @@ use pikelet_syntax::{core, raw};
/// compilation or interactive sessions
#[derive(Debug, Clone)]
pub struct Driver {
- /// The base type checking environment, containing the built-in definitions
- tc_env: TcEnv,
- /// The base desugar environment, using the definitions from the `tc_env`
+ /// The base type checking context, containing the built-in definitions
+ context: Context,
+ /// The base desugar environment, using the definitions from the `context`
desugar_env: DesugarEnv,
/// A codemap that owns the source code for any terms that are currently loaded
code_map: CodeMap,
@@ -165,11 +165,11 @@ pub struct Driver {
impl Driver {
/// Create a new Pikelet environment, containing only the built-in definitions
pub fn new() -> Driver {
- let tc_env = TcEnv::default();
- let desugar_env = DesugarEnv::new(tc_env.mappings());
+ let context = Context::default();
+ let desugar_env = DesugarEnv::new(context.mappings());
Driver {
- tc_env,
+ context,
desugar_env,
code_map: CodeMap::new(),
}
@@ -207,7 +207,7 @@ impl Driver {
let raw_term = self.desugar(&concrete_term)?;
let (term, ty) = self.infer_term(&raw_term)?;
// FIXME: Check if import already exists
- self.tc_env
+ self.context
.insert_import(internal_path, Import::Term(term), ty);
Ok(())
@@ -226,8 +226,9 @@ impl Driver {
let (term, inferred) = self.infer_term(&raw_term)?;
let fv = self.desugar_env.on_binding(&name);
- self.tc_env.insert_declaration(fv.clone(), inferred.clone());
- self.tc_env.insert_definition(fv.clone(), term.clone());
+ self.context
+ .insert_declaration(fv.clone(), inferred.clone());
+ self.context.insert_definition(fv.clone(), term.clone());
Ok((term, inferred))
}
@@ -236,15 +237,15 @@ impl Driver {
&self,
raw_term: &raw::RcTerm,
) -> Result<(core::RcTerm, core::RcType), Vec<Diagnostic>> {
- pikelet_elaborate::infer_term(&self.tc_env, &raw_term).map_err(|e| vec![e.to_diagnostic()])
+ pikelet_elaborate::infer_term(&self.context, &raw_term).map_err(|e| vec![e.to_diagnostic()])
}
pub fn nf_term(&self, term: &core::RcTerm) -> Result<core::RcValue, Vec<Diagnostic>> {
- pikelet_elaborate::nf_term(&self.tc_env, term).map_err(|e| vec![e.to_diagnostic()])
+ pikelet_elaborate::nf_term(&self.context, term).map_err(|e| vec![e.to_diagnostic()])
}
pub fn resugar<T>(&self, src: &impl Resugar<T>) -> T {
- self.tc_env.resugar(src)
+ self.context.resugar(src)
}
}
diff --git a/crates/pikelet-elaborate/src/env.rs b/crates/pikelet-elaborate/src/context.rs
similarity index 88%
rename from crates/pikelet-elaborate/src/env.rs
rename to crates/pikelet-elaborate/src/context.rs
index f7c6491dc..083aae21c 100644
--- a/crates/pikelet-elaborate/src/env.rs
+++ b/crates/pikelet-elaborate/src/context.rs
@@ -12,15 +12,15 @@ use pikelet_syntax::{FloatFormat, IntFormat};
// I'm not super happy with the API at the moment, so these are currently private
trait IntoValue {
- fn ty(env: &TcEnv) -> RcType;
+ fn ty(context: &Context) -> RcType;
fn into_value(self) -> RcValue;
}
macro_rules! impl_into_value {
($T:ty, $ty:ident, $Variant:ident) => {
impl IntoValue for $T {
- fn ty(env: &TcEnv) -> RcType {
- env.$ty().clone()
+ fn ty(context: &Context) -> RcType {
+ context.$ty().clone()
}
fn into_value(self) -> RcValue {
@@ -30,8 +30,8 @@ macro_rules! impl_into_value {
};
($T:ty, $ty:ident, $Variant:ident, $format:expr) => {
impl IntoValue for $T {
- fn ty(env: &TcEnv) -> RcType {
- env.$ty().clone()
+ fn ty(context: &Context) -> RcType {
+ context.$ty().clone()
}
fn into_value(self) -> RcValue {
@@ -210,47 +210,33 @@ pub struct Globals {
var_array: FreeVar<String>,
}
-/// The type checking environment
+/// The type checking context
///
-/// A default environment with entries for built-in types is provided via the
+/// A default context with entries for built-in types is provided via the
/// implementation of the `Default` trait.
///
/// We use persistent data structures internally so that we can copy the
-/// environment as we enter into scopes, without having to deal with the
+/// context as we enter into scopes, without having to deal with the
/// error-prone tedium of working with mutable context.
#[derive(Clone, Debug)]
-pub struct TcEnv {
- /// The resugar environment
+pub struct Context {
+ /// The resugar context
///
/// We'll keep this up to date as we type check to make it easier to do
/// resugaring on any errors that we encounter
resugar_env: ResugarEnv,
/// The globals
globals: Rc<Globals>,
- /// Imported declarations
- import_declarations: im::HashMap<String, RcType>,
- /// Imported definitions
- import_definitions: im::HashMap<String, Import>,
+ /// Imports
+ imports: im::HashMap<String, (Import, RcType)>,
/// The type annotations of the binders we have passed over
declarations: im::HashMap<FreeVar<String>, RcType>,
/// Any definitions we have passed over
definitions: im::HashMap<FreeVar<String>, RcTerm>,
}
-impl TcEnv {
- pub fn mappings(&self) -> im::HashMap<String, FreeVar<String>> {
- self.declarations
- .iter()
- .filter_map(|(free_var, _)| {
- let pretty_name = free_var.pretty_name.as_ref()?;
- Some((pretty_name.clone(), free_var.clone()))
- })
- .collect()
- }
-}
-
-impl Default for TcEnv {
- fn default() -> TcEnv {
+impl Default for Context {
+ fn default() -> Context {
use moniker::{Embed, Scope};
use pikelet_syntax::core::Term;
@@ -272,7 +258,7 @@ impl Default for TcEnv {
let var_f64 = FreeVar::fresh_named("F64");
let var_array = FreeVar::fresh_named("Array");
- let mut tc_env = TcEnv {
+ let mut context = Context {
resugar_env: ResugarEnv::new(),
globals: Rc::new(Globals {
ty_bool: RcValue::from(Value::var(Var::Free(var_bool.clone()), 0)),
@@ -290,19 +276,18 @@ impl Default for TcEnv {
ty_f64: RcValue::from(Value::var(Var::Free(var_f64.clone()), 0)),
var_array: var_array.clone(),
}),
- import_declarations: im::HashMap::new(),
- import_definitions: im::HashMap::new(),
+ imports: im::HashMap::new(),
declarations: im::HashMap::new(),
definitions: im::HashMap::new(),
};
let universe0 = RcValue::from(Value::universe(0));
- let bool_ty = tc_env.globals.ty_bool.clone();
+ let bool_ty = context.globals.ty_bool.clone();
let bool_lit = |value| RcTerm::from(Term::Literal(Literal::Bool(value)));
let array_ty = RcValue::from(Value::Pi(Scope::new(
(
Binder(FreeVar::fresh_unnamed()),
- Embed(tc_env.globals.ty_u64.clone()),
+ Embed(context.globals.ty_u64.clone()),
),
RcValue::from(Value::Pi(Scope::new(
(Binder(FreeVar::fresh_unnamed()), Embed(universe0.clone())),
@@ -310,25 +295,25 @@ impl Default for TcEnv {
))),
)));
- tc_env.insert_declaration(var_bool, universe0.clone());
- tc_env.insert_declaration(var_string, universe0.clone());
- tc_env.insert_declaration(var_char, universe0.clone());
- tc_env.insert_declaration(var_u8, universe0.clone());
- tc_env.insert_declaration(var_u16, universe0.clone());
- tc_env.insert_declaration(var_u32, universe0.clone());
- tc_env.insert_declaration(var_u64, universe0.clone());
- tc_env.insert_declaration(var_s8, universe0.clone());
- tc_env.insert_declaration(var_s16, universe0.clone());
- tc_env.insert_declaration(var_s32, universe0.clone());
- tc_env.insert_declaration(var_s64, universe0.clone());
- tc_env.insert_declaration(var_f32, universe0.clone());
- tc_env.insert_declaration(var_f64, universe0.clone());
- tc_env.insert_declaration(var_array, array_ty);
-
- tc_env.insert_declaration(var_true.clone(), bool_ty.clone());
- tc_env.insert_declaration(var_false.clone(), bool_ty.clone());
- tc_env.insert_definition(var_true, bool_lit(true));
- tc_env.insert_definition(var_false, bool_lit(false));
+ context.insert_declaration(var_bool, universe0.clone());
+ context.insert_declaration(var_string, universe0.clone());
+ context.insert_declaration(var_char, universe0.clone());
+ context.insert_declaration(var_u8, universe0.clone());
+ context.insert_declaration(var_u16, universe0.clone());
+ context.insert_declaration(var_u32, universe0.clone());
+ context.insert_declaration(var_u64, universe0.clone());
+ context.insert_declaration(var_s8, universe0.clone());
+ context.insert_declaration(var_s16, universe0.clone());
+ context.insert_declaration(var_s32, universe0.clone());
+ context.insert_declaration(var_s64, universe0.clone());
+ context.insert_declaration(var_f32, universe0.clone());
+ context.insert_declaration(var_f64, universe0.clone());
+ context.insert_declaration(var_array, array_ty);
+
+ context.insert_declaration(var_true.clone(), bool_ty.clone());
+ context.insert_declaration(var_false.clone(), bool_ty.clone());
+ context.insert_definition(var_true, bool_lit(true));
+ context.insert_definition(var_false, bool_lit(false));
/// Define a primitive import
macro_rules! prim_import {
@@ -343,14 +328,14 @@ impl Default for TcEnv {
}
}
- let ty = <$RType>::ty(&tc_env);
+ let ty = <$RType>::ty(&context);
$(let ty = {
let param_var = FreeVar::fresh_unnamed();
- let param_ty = <$PType>::ty(&tc_env);
+ let param_ty = <$PType>::ty(&context);
RcValue::from(Value::Pi(Scope::new((Binder(param_var), Embed(param_ty)), ty)))
};)*
- tc_env.insert_import($name.to_owned(), Import::Prim(interpretation), ty);
+ context.insert_import($name.to_owned(), Import::Prim(interpretation), ty);
}};
}
@@ -496,15 +481,25 @@ impl Default for TcEnv {
prim_import!("prim/string/append", fn(x: String, y: String) -> String { x.clone() + y }); // FIXME: Clone
- tc_env
+ context
}
}
-impl TcEnv {
+impl Context {
pub fn resugar<T>(&self, src: &impl Resugar<T>) -> T {
src.resugar(&self.resugar_env)
}
+ pub fn mappings(&self) -> im::HashMap<String, FreeVar<String>> {
+ self.declarations
+ .iter()
+ .filter_map(|(free_var, _)| {
+ let pretty_name = free_var.pretty_name.as_ref()?;
+ Some((pretty_name.clone(), free_var.clone()))
+ })
+ .collect()
+ }
+
pub fn bool(&self) -> &RcType {
&self.globals.ty_bool
}
@@ -573,12 +568,8 @@ impl TcEnv {
}
}
- pub fn get_import_declaration(&self, name: &str) -> Option<&RcType> {
- self.import_declarations.get(name)
- }
-
- pub fn get_import_definition(&self, name: &str) -> Option<&Import> {
- self.import_definitions.get(name)
+ pub fn get_import(&self, name: &str) -> Option<&(Import, RcType)> {
+ self.imports.get(name)
}
pub fn get_declaration(&self, free_var: &FreeVar<String>) -> Option<&RcType> {
@@ -590,8 +581,7 @@ impl TcEnv {
}
pub fn insert_import(&mut self, name: String, import: Import, ty: RcType) {
- self.import_declarations.insert(name.clone(), ty);
- self.import_definitions.insert(name, import);
+ self.imports.insert(name, (import, ty));
}
pub fn insert_declaration(&mut self, free_var: FreeVar<String>, ty: RcType) {
@@ -603,18 +593,4 @@ impl TcEnv {
self.resugar_env.on_binder(&Binder(free_var.clone()));
self.definitions.insert(free_var, term);
}
-
- pub fn extend_declarations(
- &mut self,
- iter: impl IntoIterator<Item = (FreeVar<String>, RcType)>,
- ) {
- self.declarations.extend(iter)
- }
-
- pub fn extend_definitions<T>(
- &mut self,
- iter: impl IntoIterator<Item = (FreeVar<String>, RcTerm)>,
- ) {
- self.definitions.extend(iter)
- }
}
diff --git a/crates/pikelet-elaborate/src/lib.rs b/crates/pikelet-elaborate/src/lib.rs
index af78802a5..f1fefaf9f 100644
--- a/crates/pikelet-elaborate/src/lib.rs
+++ b/crates/pikelet-elaborate/src/lib.rs
@@ -19,16 +19,16 @@ use pikelet_syntax::core::{Literal, Pattern, RcPattern, RcTerm, RcType, RcValue,
use pikelet_syntax::raw;
use pikelet_syntax::Level;
-mod env;
+mod context;
mod errors;
mod normalize;
-pub use self::env::{Globals, Import, TcEnv};
+pub use self::context::{Context, Globals, Import};
pub use self::errors::{InternalError, TypeError};
pub use self::normalize::{match_value, nf_term};
/// Returns true if `ty1` is a subtype of `ty2`
-fn is_subtype(env: &TcEnv, ty1: &RcType, ty2: &RcType) -> bool {
+fn is_subtype(context: &Context, ty1: &RcType, ty2: &RcType) -> bool {
match (&*ty1.inner, &*ty2.inner) {
// ST-TYPE
(&Value::Universe(level1), &Value::Universe(level2)) => level1 <= level2,
@@ -38,10 +38,10 @@ fn is_subtype(env: &TcEnv, ty1: &RcType, ty2: &RcType) -> bool {
let ((_, Embed(ann1)), body1, (Binder(free_var2), Embed(ann2)), body2) =
Scope::unbind2(scope1.clone(), scope2.clone());
- is_subtype(env, &ann2, &ann1) && {
- let mut env = env.clone();
- env.insert_declaration(free_var2, ann2);
- is_subtype(&env, &body1, &body2)
+ is_subtype(context, &ann2, &ann1) && {
+ let mut context = context.clone();
+ context.insert_declaration(free_var2, ann2);
+ is_subtype(&context, &body1, &body2)
}
},
@@ -55,15 +55,15 @@ fn is_subtype(env: &TcEnv, ty1: &RcType, ty2: &RcType) -> bool {
let (fields1, (), fields2, ()) = Scope::unbind2(scope1.clone(), scope2.clone());
- let mut env = env.clone();
+ let mut context = context.clone();
for (field1, field2) in
Iterator::zip(fields1.unnest().into_iter(), fields2.unnest().into_iter())
{
let (label1, Binder(free_var1), Embed(ty1)) = field1;
let (label2, _, Embed(ty2)) = field2;
- if label1 == label2 && is_subtype(&env, &ty1, &ty2) {
- env.insert_declaration(free_var1, ty1);
+ if label1 == label2 && is_subtype(&context, &ty1, &ty2) {
+ context.insert_declaration(free_var1, ty1);
} else {
return false;
}
@@ -79,13 +79,13 @@ fn is_subtype(env: &TcEnv, ty1: &RcType, ty2: &RcType) -> bool {
/// Ensures that the given term is a universe, returning the level of that
/// universe and its elaborated form.
-fn infer_universe(env: &TcEnv, raw_term: &raw::RcTerm) -> Result<(RcTerm, Level), TypeError> {
- let (term, ty) = infer_term(env, raw_term)?;
+fn infer_universe(context: &Context, raw_term: &raw::RcTerm) -> Result<(RcTerm, Level), TypeError> {
+ let (term, ty) = infer_term(context, raw_term)?;
match *ty {
Value::Universe(level) => Ok((term, level)),
_ => Err(TypeError::ExpectedUniverse {
span: raw_term.span(),
- found: Box::new(env.resugar(&ty)),
+ found: Box::new(context.resugar(&ty)),
}),
}
}
@@ -93,47 +93,51 @@ fn infer_universe(env: &TcEnv, raw_term: &raw::RcTerm) -> Result<(RcTerm, Level)
/// Checks that a literal is compatible with the given type, returning the
/// elaborated literal if successful
fn check_literal(
- env: &TcEnv,
+ context: &Context,
raw_literal: &raw::Literal,
expected_ty: &RcType,
) -> Result<Literal, TypeError> {
+ use pikelet_syntax::core::Literal::*;
use pikelet_syntax::FloatFormat::Dec as FloatDec;
let ty = expected_ty;
match *raw_literal {
- raw::Literal::String(_, ref val) if env.string() == ty => Ok(Literal::String(val.clone())),
- raw::Literal::Char(_, val) if env.char() == ty => Ok(Literal::Char(val)),
+ raw::Literal::String(_, ref val) if context.string() == ty => Ok(String(val.clone())),
+ raw::Literal::Char(_, val) if context.char() == ty => Ok(Char(val)),
// FIXME: overflow?
- raw::Literal::Int(_, v, format) if env.u8() == ty => Ok(Literal::U8(v as u8, format)),
- raw::Literal::Int(_, v, format) if env.u16() == ty => Ok(Literal::U16(v as u16, format)),
- raw::Literal::Int(_, v, format) if env.u32() == ty => Ok(Literal::U32(v as u32, format)),
- raw::Literal::Int(_, v, format) if env.u64() == ty => Ok(Literal::U64(v, format)),
- raw::Literal::Int(_, v, format) if env.s8() == ty => Ok(Literal::S8(v as i8, format)),
- raw::Literal::Int(_, v, format) if env.s16() == ty => Ok(Literal::S16(v as i16, format)),
- raw::Literal::Int(_, v, format) if env.s32() == ty => Ok(Literal::S32(v as i32, format)),
- raw::Literal::Int(_, v, format) if env.s64() == ty => Ok(Literal::S64(v as i64, format)),
- raw::Literal::Int(_, v, _) if env.f32() == ty => Ok(Literal::F32(v as f32, FloatDec)),
- raw::Literal::Int(_, v, _) if env.f64() == ty => Ok(Literal::F64(v as f64, FloatDec)),
- raw::Literal::Float(_, v, format) if env.f32() == ty => Ok(Literal::F32(v as f32, format)),
- raw::Literal::Float(_, v, format) if env.f64() == ty => Ok(Literal::F64(v, format)),
+ raw::Literal::Int(_, v, format) if context.u8() == ty => Ok(U8(v as u8, format)),
+ raw::Literal::Int(_, v, format) if context.u16() == ty => Ok(U16(v as u16, format)),
+ raw::Literal::Int(_, v, format) if context.u32() == ty => Ok(U32(v as u32, format)),
+ raw::Literal::Int(_, v, format) if context.u64() == ty => Ok(U64(v, format)),
+ raw::Literal::Int(_, v, format) if context.s8() == ty => Ok(S8(v as i8, format)),
+ raw::Literal::Int(_, v, format) if context.s16() == ty => Ok(S16(v as i16, format)),
+ raw::Literal::Int(_, v, format) if context.s32() == ty => Ok(S32(v as i32, format)),
+ raw::Literal::Int(_, v, format) if context.s64() == ty => Ok(S64(v as i64, format)),
+ raw::Literal::Int(_, v, _) if context.f32() == ty => Ok(F32(v as f32, FloatDec)),
+ raw::Literal::Int(_, v, _) if context.f64() == ty => Ok(F64(v as f64, FloatDec)),
+ raw::Literal::Float(_, v, format) if context.f32() == ty => Ok(F32(v as f32, format)),
+ raw::Literal::Float(_, v, format) if context.f64() == ty => Ok(F64(v, format)),
_ => Err(TypeError::LiteralMismatch {
literal_span: raw_literal.span(),
found: raw_literal.clone(),
- expected: Box::new(env.resugar(expected_ty)),
+ expected: Box::new(context.resugar(expected_ty)),
}),
}
}
/// Synthesize the type of a literal, returning the elaborated literal and the
/// inferred type if successful
-fn infer_literal(env: &TcEnv, raw_literal: &raw::Literal) -> Result<(Literal, RcType), TypeError> {
+fn infer_literal(
+ context: &Context,
+ raw_literal: &raw::Literal,
+) -> Result<(Literal, RcType), TypeError> {
+ use pikelet_syntax::core::Literal::{Char, String};
+
match *raw_literal {
- raw::Literal::String(_, ref value) => {
- Ok((Literal::String(value.clone()), env.string().clone()))
- },
- raw::Literal::Char(_, value) => Ok((Literal::Char(value), env.char().clone())),
+ raw::Literal::String(_, ref val) => Ok((String(val.clone()), context.string().clone())),
+ raw::Literal::Char(_, val) => Ok((Char(val), context.char().clone())),
raw::Literal::Int(span, _, _) => Err(TypeError::AmbiguousIntLiteral { span }),
raw::Literal::Float(span, _, _) => Err(TypeError::AmbiguousFloatLiteral { span }),
}
@@ -142,7 +146,7 @@ fn infer_literal(env: &TcEnv, raw_literal: &raw::Literal) -> Result<(Literal, Rc
/// Checks that a pattern is compatible with the given type, returning the
/// elaborated pattern and a vector of the declarations it introduced if successful
pub fn check_pattern(
- env: &TcEnv,
+ context: &Context,
raw_pattern: &raw::RcPattern,
expected_ty: &RcType,
) -> Result<(RcPattern, Vec<(FreeVar<String>, RcType)>), TypeError> {
@@ -154,20 +158,20 @@ pub fn check_pattern(
));
},
(&raw::Pattern::Literal(ref raw_literal), _) => {
- let literal = check_literal(env, raw_literal, expected_ty)?;
+ let literal = check_literal(context, raw_literal, expected_ty)?;
return Ok((RcPattern::from(Pattern::Literal(literal)), vec![]));
},
_ => {},
}
- let (pattern, inferred_ty, declarations) = infer_pattern(env, raw_pattern)?;
- if is_subtype(env, &inferred_ty, expected_ty) {
+ let (pattern, inferred_ty, declarations) = infer_pattern(context, raw_pattern)?;
+ if is_subtype(context, &inferred_ty, expected_ty) {
Ok((pattern, declarations))
} else {
Err(TypeError::Mismatch {
span: raw_pattern.span(),
- found: Box::new(env.resugar(&inferred_ty)),
- expected: Box::new(env.resugar(expected_ty)),
+ found: Box::new(context.resugar(&inferred_ty)),
+ expected: Box::new(context.resugar(expected_ty)),
})
}
}
@@ -175,14 +179,14 @@ pub fn check_pattern(
/// Synthesize the type of a pattern, returning the elaborated pattern, the
/// inferred type, and a vector of the declarations it introduced if successful
pub fn infer_pattern(
- env: &TcEnv,
+ context: &Context,
raw_pattern: &raw::RcPattern,
) -> Result<(RcPattern, RcType, Vec<(FreeVar<String>, RcType)>), TypeError> {
match *raw_pattern.inner {
raw::Pattern::Ann(ref raw_pattern, Embed(ref raw_ty)) => {
- let (ty, _) = infer_universe(env, raw_ty)?;
- let value_ty = nf_term(env, &ty)?;
- let (pattern, declarations) = check_pattern(env, raw_pattern, &value_ty)?;
+ let (ty, _) = infer_universe(context, raw_ty)?;
+ let value_ty = nf_term(context, &ty)?;
+ let (pattern, declarations) = check_pattern(context, raw_pattern, &value_ty)?;
Ok((
RcPattern::from(Pattern::Ann(pattern, Embed(ty))),
@@ -195,7 +199,7 @@ pub fn infer_pattern(
binder: binder.clone(),
}),
raw::Pattern::Var(span, Embed(ref var), shift) => match *var {
- Var::Free(ref free_var) => match env.get_declaration(free_var) {
+ Var::Free(ref free_var) => match context.get_declaration(free_var) {
Some(ty) => {
let mut ty = ty.clone();
ty.shift_universes(shift);
@@ -219,7 +223,7 @@ pub fn infer_pattern(
.into()),
},
raw::Pattern::Literal(ref literal) => {
- let (literal, ty) = infer_literal(env, literal)?;
+ let (literal, ty) = infer_literal(context, literal)?;
Ok((RcPattern::from(Pattern::Literal(literal)), ty, vec![]))
},
}
@@ -228,13 +232,13 @@ pub fn infer_pattern(
/// Checks that a term is compatible with the given type, returning the
/// elaborated term if successful
pub fn check_term(
- env: &TcEnv,
+ context: &Context,
raw_term: &raw::RcTerm,
expected_ty: &RcType,
) -> Result<RcTerm, TypeError> {
match (&*raw_term.inner, &*expected_ty.inner) {
(&raw::Term::Literal(ref raw_literal), _) => {
- let literal = check_literal(env, raw_literal, expected_ty)?;
+ let literal = check_literal(context, raw_literal, expected_ty)?;
return Ok(RcTerm::from(Term::Literal(literal)));
},
@@ -247,9 +251,9 @@ pub fn check_term(
if let raw::Term::Hole(_) = *lam_ann.inner {
let lam_ann = RcTerm::from(Term::from(&*pi_ann));
let lam_body = {
- let mut body_env = env.clone();
- body_env.insert_declaration(pi_name, pi_ann);
- check_term(&body_env, &lam_body, &pi_body)?
+ let mut body_context = context.clone();
+ body_context.insert_declaration(pi_name, pi_ann);
+ check_term(&body_context, &lam_body, &pi_body)?
};
let lam_scope = Scope::new((lam_name, Embed(lam_ann)), lam_body);
@@ -262,7 +266,7 @@ pub fn check_term(
(&raw::Term::Lam(_, _), _) => {
return Err(TypeError::UnexpectedFunction {
span: raw_term.span(),
- expected: Box::new(env.resugar(expected_ty)),
+ expected: Box::new(context.resugar(expected_ty)),
});
},
@@ -295,8 +299,8 @@ pub fn check_term(
let (ty_label, Binder(ty_free_var), Embed(ann)) = ty_field;
if label == ty_label {
- let ann = nf_term(env, &ann.substs(&mappings))?;
- let expr = check_term(env, &raw_expr, &ann)?;
+ let ann = nf_term(context, &ann.substs(&mappings))?;
+ let expr = check_term(context, &raw_expr, &ann)?;
mappings.push((ty_free_var, expr.clone()));
Ok((label, Binder(free_var), Embed(expr)))
} else {
@@ -316,18 +320,22 @@ pub fn check_term(
},
(&raw::Term::Case(_, ref raw_head, ref raw_clauses), _) => {
- let (head, head_ty) = infer_term(env, raw_head)?;
+ let (head, head_ty) = infer_term(context, raw_head)?;
// TODO: ensure that patterns are exhaustive
let clauses = raw_clauses
.iter()
.map(|raw_clause| {
let (raw_pattern, raw_body) = raw_clause.clone().unbind();
- let (pattern, declarations) = check_pattern(env, &raw_pattern, &head_ty)?;
+ let (pattern, declarations) = check_pattern(context, &raw_pattern, &head_ty)?;
- let mut body_env = env.clone();
- body_env.extend_declarations(declarations);
- let body = check_term(&body_env, &raw_body, expected_ty)?;
+ let body = {
+ let mut body_context = context.clone();
+ for (free_var, ty) in declarations {
+ body_context.insert_declaration(free_var, ty);
+ }
+ check_term(&body_context, &raw_body, expected_ty)?
+ };
Ok(Scope::new(pattern, body))
})
@@ -337,11 +345,11 @@ pub fn check_term(
},
(&raw::Term::Array(span, ref elems), _) => {
- return match env.array(expected_ty) {
+ return match context.array(expected_ty) {
Some((len, elem_ty)) if len == elems.len() as u64 => {
let elems = elems
.iter()
- .map(|elem| check_term(env, elem, elem_ty))
+ .map(|elem| check_term(context, elem, elem_ty))
.collect::<Result<_, _>>()?;
Ok(RcTerm::from(Term::Array(elems)))
@@ -359,7 +367,7 @@ pub fn check_term(
},
(&raw::Term::Hole(span), _) => {
- let expected = Some(Box::new(env.resugar(expected_ty)));
+ let expected = Some(Box::new(context.resugar(expected_ty)));
return Err(TypeError::UnableToElaborateHole { span, expected });
},
@@ -367,29 +375,32 @@ pub fn check_term(
}
// C-CONV
- let (term, inferred_ty) = infer_term(env, raw_term)?;
- if is_subtype(env, &inferred_ty, expected_ty) {
+ let (term, inferred_ty) = infer_term(context, raw_term)?;
+ if is_subtype(context, &inferred_ty, expected_ty) {
Ok(term)
} else {
Err(TypeError::Mismatch {
span: raw_term.span(),
- found: Box::new(env.resugar(&inferred_ty)),
- expected: Box::new(env.resugar(expected_ty)),
+ found: Box::new(context.resugar(&inferred_ty)),
+ expected: Box::new(context.resugar(expected_ty)),
})
}
}
/// Synthesize the type of a term, returning the elaborated term and the
/// inferred type if successful
-pub fn infer_term(env: &TcEnv, raw_term: &raw::RcTerm) -> Result<(RcTerm, RcType), TypeError> {
+pub fn infer_term(
+ context: &Context,
+ raw_term: &raw::RcTerm,
+) -> Result<(RcTerm, RcType), TypeError> {
use std::cmp;
match *raw_term.inner {
// I-ANN
raw::Term::Ann(ref raw_expr, ref raw_ty) => {
- let (ty, _) = infer_universe(env, raw_ty)?;
- let value_ty = nf_term(env, &ty)?;
- let expr = check_term(env, raw_expr, &value_ty)?;
+ let (ty, _) = infer_universe(context, raw_ty)?;
+ let value_ty = nf_term(context, &ty)?;
+ let expr = check_term(context, raw_expr, &value_ty)?;
Ok((RcTerm::from(Term::Ann(expr, ty)), value_ty))
},
@@ -406,13 +417,13 @@ pub fn infer_term(env: &TcEnv, raw_term: &raw::RcTerm) -> Result<(RcTerm, RcType
},
raw::Term::Literal(ref raw_literal) => {
- let (literal, ty) = infer_literal(env, raw_literal)?;
+ let (literal, ty) = infer_literal(context, raw_literal)?;
Ok((RcTerm::from(Term::Literal(literal)), ty))
},
// I-VAR
raw::Term::Var(span, ref var, shift) => match *var {
- Var::Free(ref free_var) => match env.get_declaration(free_var) {
+ Var::Free(ref free_var) => match context.get_declaration(free_var) {
Some(ty) => {
let mut ty = ty.clone();
ty.shift_universes(shift);
@@ -435,8 +446,8 @@ pub fn infer_term(env: &TcEnv, raw_term: &raw::RcTerm) -> Result<(RcTerm, RcType
.into()),
},
- raw::Term::Import(_, name_span, ref name) => match env.get_import_declaration(name) {
- Some(ty) => Ok((RcTerm::from(Term::Import(name.clone())), ty.clone())),
+ raw::Term::Import(_, name_span, ref name) => match context.get_import(name) {
+ Some((_, ty)) => Ok((RcTerm::from(Term::Import(name.clone())), ty.clone())),
None => Err(TypeError::UndefinedImport {
span: name_span,
name: name.clone(),
@@ -447,12 +458,12 @@ pub fn infer_term(env: &TcEnv, raw_term: &raw::RcTerm) -> Result<(RcTerm, RcType
raw::Term::Pi(_, ref raw_scope) => {
let ((Binder(free_var), Embed(raw_ann)), raw_body) = raw_scope.clone().unbind();
- let (ann, ann_level) = infer_universe(env, &raw_ann)?;
+ let (ann, ann_level) = infer_universe(context, &raw_ann)?;
let (body, body_level) = {
- let ann = nf_term(env, &ann)?;
- let mut body_env = env.clone();
- body_env.insert_declaration(free_var.clone(), ann);
- infer_universe(&body_env, &raw_body)?
+ let ann = nf_term(context, &ann)?;
+ let mut body_context = context.clone();
+ body_context.insert_declaration(free_var.clone(), ann);
+ infer_universe(&body_context, &raw_body)?
};
Ok((
@@ -474,12 +485,12 @@ pub fn infer_term(env: &TcEnv, raw_term: &raw::RcTerm) -> Result<(RcTerm, RcType
});
}
- let (lam_ann, _) = infer_universe(env, &raw_ann)?;
- let pi_ann = nf_term(env, &lam_ann)?;
+ let (lam_ann, _) = infer_universe(context, &raw_ann)?;
+ let pi_ann = nf_term(context, &lam_ann)?;
let (lam_body, pi_body) = {
- let mut body_env = env.clone();
- body_env.insert_declaration(free_var.clone(), pi_ann.clone());
- infer_term(&body_env, &raw_body)?
+ let mut body_context = context.clone();
+ body_context.insert_declaration(free_var.clone(), pi_ann.clone());
+ infer_term(&body_context, &raw_body)?
};
let lam_param = (Binder(free_var.clone()), Embed(lam_ann));
@@ -496,28 +507,28 @@ pub fn infer_term(env: &TcEnv, raw_term: &raw::RcTerm) -> Result<(RcTerm, RcType
let (raw_fields, raw_body) = raw_scope.clone().unbind();
let (term, ty) = {
- let mut env = env.clone();
+ let mut context = context.clone();
let bindings = raw_fields
.unnest()
.into_iter()
.map(|(Binder(free_var), Embed((raw_ann, raw_term)))| {
let (term, ann, ann_value) = if let raw::Term::Hole(_) = *raw_ann {
- let (term, ann_value) = infer_term(&env, &raw_term)?;
+ let (term, ann_value) = infer_term(&context, &raw_term)?;
(term, RcTerm::from(&*ann_value.inner), ann_value)
} else {
- let (ann, _) = infer_universe(&env, &raw_ann)?;
- let ann_value = nf_term(&env, &ann)?;
- (check_term(&env, &raw_term, &ann_value)?, ann, ann_value)
+ let (ann, _) = infer_universe(&context, &raw_ann)?;
+ let ann_value = nf_term(&context, &ann)?;
+ (check_term(&context, &raw_term, &ann_value)?, ann, ann_value)
};
- env.insert_definition(free_var.clone(), term.clone());
- env.insert_declaration(free_var.clone(), ann_value);
+ context.insert_definition(free_var.clone(), term.clone());
+ context.insert_declaration(free_var.clone(), ann_value);
Ok((Binder(free_var), Embed((ann, term))))
})
.collect::<Result<_, TypeError>>()?;
- let (body, ty) = infer_term(&env, &raw_body)?;
+ let (body, ty) = infer_term(&context, &raw_body)?;
let term = RcTerm::from(Term::Let(Scope::new(Nest::new(bindings), body)));
(term, ty)
@@ -528,21 +539,21 @@ pub fn infer_term(env: &TcEnv, raw_term: &raw::RcTerm) -> Result<(RcTerm, RcType
// I-APP
raw::Term::App(ref raw_head, ref raw_arg) => {
- let (head, head_ty) = infer_term(env, raw_head)?;
+ let (head, head_ty) = infer_term(context, raw_head)?;
match *head_ty {
Value::Pi(ref scope) => {
let ((Binder(free_var), Embed(ann)), body) = scope.clone().unbind();
- let arg = check_term(env, raw_arg, &ann)?;
- let body = nf_term(env, &body.substs(&[(free_var, arg.clone())]))?;
+ let arg = check_term(context, raw_arg, &ann)?;
+ let body = nf_term(context, &body.substs(&[(free_var, arg.clone())]))?;
Ok((RcTerm::from(Term::App(head, arg)), body))
},
_ => Err(TypeError::ArgAppliedToNonFunction {
fn_span: raw_head.span(),
arg_span: raw_arg.span(),
- found: Box::new(env.resugar(&head_ty)),
+ found: Box::new(context.resugar(&head_ty)),
}),
}
},
@@ -554,16 +565,16 @@ pub fn infer_term(env: &TcEnv, raw_term: &raw::RcTerm) -> Result<(RcTerm, RcType
// FIXME: Check that record is well-formed?
let fields = {
- let mut env = env.clone();
+ let mut context = context.clone();
raw_fields
.unnest()
.into_iter()
.map(|(label, Binder(free_var), Embed(raw_ann))| {
- let (ann, ann_level) = infer_universe(&env, &raw_ann)?;
- let nf_ann = nf_term(&env, &ann)?;
+ let (ann, ann_level) = infer_universe(&context, &raw_ann)?;
+ let nf_ann = nf_term(&context, &ann)?;
max_level = cmp::max(max_level, ann_level);
- env.insert_declaration(free_var.clone(), nf_ann);
+ context.insert_declaration(free_var.clone(), nf_ann);
Ok((label, Binder(free_var), Embed(ann)))
})
@@ -588,8 +599,8 @@ pub fn infer_term(env: &TcEnv, raw_term: &raw::RcTerm) -> Result<(RcTerm, RcType
{
let mut ty_mappings = Vec::with_capacity(raw_fields.len());
for (label, Binder(free_var), Embed(raw_term)) in raw_fields {
- let (term, term_ty) = infer_term(env, &raw_term)?;
- let term_ty = nf_term(env, &term_ty.substs(&ty_mappings))?;
+ let (term, term_ty) = infer_term(context, &raw_term)?;
+ let term_ty = nf_term(context, &term_ty.substs(&ty_mappings))?;
fields.push((label.clone(), Binder(free_var.clone()), Embed(term.clone())));
ty_fields.push((label, Binder(free_var.clone()), Embed(term_ty)));
@@ -605,7 +616,7 @@ pub fn infer_term(env: &TcEnv, raw_term: &raw::RcTerm) -> Result<(RcTerm, RcType
// I-PROJ
raw::Term::Proj(_, ref expr, label_span, ref label, shift) => {
- let (expr, ty) = infer_term(env, expr)?;
+ let (expr, ty) = infer_term(context, expr)?;
if let Value::RecordType(ref scope) = *ty.inner {
let (fields, ()) = scope.clone().unbind();
@@ -613,7 +624,7 @@ pub fn infer_term(env: &TcEnv, raw_term: &raw::RcTerm) -> Result<(RcTerm, RcType
for (current_label, Binder(free_var), Embed(current_ann)) in fields.unnest() {
if current_label == *label {
- let mut ty = nf_term(env, ¤t_ann.substs(&mappings))?;
+ let mut ty = nf_term(context, ¤t_ann.substs(&mappings))?;
ty.shift_universes(shift);
return Ok((RcTerm::from(Term::Proj(expr, current_label, shift)), ty));
@@ -630,13 +641,13 @@ pub fn infer_term(env: &TcEnv, raw_term: &raw::RcTerm) -> Result<(RcTerm, RcType
Err(TypeError::NoFieldInType {
label_span,
expected_label: label.clone(),
- found: Box::new(env.resugar(&ty)),
+ found: Box::new(context.resugar(&ty)),
})
},
// I-CASE
raw::Term::Case(span, ref raw_head, ref raw_clauses) => {
- let (head, head_ty) = infer_term(env, raw_head)?;
+ let (head, head_ty) = infer_term(context, raw_head)?;
let mut ty = None;
// TODO: ensure that patterns are exhaustive
@@ -644,12 +655,14 @@ pub fn infer_term(env: &TcEnv, raw_term: &raw::RcTerm) -> Result<(RcTerm, RcType
.iter()
.map(|raw_clause| {
let (raw_pattern, raw_body) = raw_clause.clone().unbind();
- let (pattern, declarations) = check_pattern(env, &raw_pattern, &head_ty)?;
+ let (pattern, declarations) = check_pattern(context, &raw_pattern, &head_ty)?;
let (body, body_ty) = {
- let mut body_env = env.clone();
- body_env.extend_declarations(declarations);
- infer_term(&body_env, &raw_body)?
+ let mut body_context = context.clone();
+ for (free_var, ty) in declarations {
+ body_context.insert_declaration(free_var, ty);
+ }
+ infer_term(&body_context, &raw_body)?
};
match ty {
@@ -659,8 +672,8 @@ pub fn infer_term(env: &TcEnv, raw_term: &raw::RcTerm) -> Result<(RcTerm, RcType
Some(ref ty) => {
return Err(TypeError::Mismatch {
span: raw_body.span(),
- found: Box::new(env.resugar(&body_ty)),
- expected: Box::new(env.resugar(ty)),
+ found: Box::new(context.resugar(&body_ty)),
+ expected: Box::new(context.resugar(ty)),
});
},
}
diff --git a/crates/pikelet-elaborate/src/normalize.rs b/crates/pikelet-elaborate/src/normalize.rs
index c709f9056..9321a0a77 100644
--- a/crates/pikelet-elaborate/src/normalize.rs
+++ b/crates/pikelet-elaborate/src/normalize.rs
@@ -4,13 +4,13 @@ use pikelet_syntax::core::{
Head, Neutral, Pattern, RcNeutral, RcPattern, RcTerm, RcValue, Term, Value,
};
-use {Import, InternalError, TcEnv};
+use {Context, Import, InternalError};
/// Reduce a term to its normal form
-pub fn nf_term(env: &TcEnv, term: &RcTerm) -> Result<RcValue, InternalError> {
+pub fn nf_term(context: &Context, term: &RcTerm) -> Result<RcValue, InternalError> {
match *term.inner {
// E-ANN
- Term::Ann(ref expr, _) => nf_term(env, expr),
+ Term::Ann(ref expr, _) => nf_term(context, expr),
// E-TYPE
Term::Universe(level) => Ok(RcValue::from(Value::Universe(level))),
@@ -19,9 +19,9 @@ pub fn nf_term(env: &TcEnv, term: &RcTerm) -> Result<RcValue, InternalError> {
// E-VAR, E-VAR-DEF
Term::Var(ref var, shift) => match *var {
- Var::Free(ref name) => match env.get_definition(name) {
+ Var::Free(ref name) => match context.get_definition(name) {
Some(term) => {
- let mut value = nf_term(env, term)?;
+ let mut value = nf_term(context, term)?;
value.shift_universes(shift);
Ok(value)
},
@@ -37,9 +37,9 @@ pub fn nf_term(env: &TcEnv, term: &RcTerm) -> Result<RcValue, InternalError> {
}),
},
- Term::Import(ref name) => match env.get_import_definition(name) {
- Some(Import::Term(ref term)) => nf_term(env, term),
- Some(Import::Prim(ref interpretation)) => match interpretation(&[]) {
+ Term::Import(ref name) => match context.get_import(name) {
+ Some(&(Import::Term(ref term), _)) => nf_term(context, term),
+ Some(&(Import::Prim(ref interpretation), _)) => match interpretation(&[]) {
Some(value) => Ok(value),
None => Ok(RcValue::from(Value::from(Neutral::Head(Head::Import(
name.clone(),
@@ -55,8 +55,8 @@ pub fn nf_term(env: &TcEnv, term: &RcTerm) -> Result<RcValue, InternalError> {
let ((name, Embed(ann)), body) = scope.clone().unbind();
Ok(RcValue::from(Value::Pi(Scope::new(
- (name, Embed(nf_term(env, &ann)?)),
- nf_term(env, &body)?,
+ (name, Embed(nf_term(context, &ann)?)),
+ nf_term(context, &body)?,
))))
},
@@ -65,33 +65,33 @@ pub fn nf_term(env: &TcEnv, term: &RcTerm) -> Result<RcValue, InternalError> {
let ((name, Embed(ann)), body) = scope.clone().unbind();
Ok(RcValue::from(Value::Lam(Scope::new(
- (name, Embed(nf_term(env, &ann)?)),
- nf_term(env, &body)?,
+ (name, Embed(nf_term(context, &ann)?)),
+ nf_term(context, &body)?,
))))
},
// E-APP
Term::App(ref head, ref arg) => {
- match *nf_term(env, head)?.inner {
+ match *nf_term(context, head)?.inner {
Value::Lam(ref scope) => {
// FIXME: do a local unbind here
let ((Binder(free_var), Embed(_)), body) = scope.clone().unbind();
- nf_term(env, &body.substs(&[(free_var, arg.clone())]))
+ nf_term(context, &body.substs(&[(free_var, arg.clone())]))
},
Value::Neutral(ref neutral, ref spine) => {
- let arg = nf_term(env, arg)?;
+ let arg = nf_term(context, arg)?;
let mut spine = spine.clone();
match *neutral.inner {
Neutral::Head(Head::Import(ref name)) => {
spine.push(arg);
- match env.get_import_definition(name) {
- Some(Import::Term(ref _term)) => {
- // nf_term(env, term)
+ match context.get_import(name) {
+ Some(&(Import::Term(ref _term), _)) => {
+ // nf_term(context, term)
unimplemented!("import applications")
},
- Some(Import::Prim(ref interpretation)) => {
+ Some(&(Import::Prim(ref interpretation), _)) => {
match interpretation(&spine) {
Some(value) => return Ok(value),
None => {},
@@ -117,11 +117,11 @@ pub fn nf_term(env: &TcEnv, term: &RcTerm) -> Result<RcValue, InternalError> {
let mut mappings = Vec::with_capacity(bindings.unsafe_patterns.len());
for (Binder(free_var), Embed((_, term))) in bindings.unnest() {
- let value = nf_term(env, &term.substs(&mappings))?;
+ let value = nf_term(context, &term.substs(&mappings))?;
mappings.push((free_var, RcTerm::from(&*value.inner)));
}
- nf_term(env, &body.substs(&mappings))
+ nf_term(context, &body.substs(&mappings))
},
// E-RECORD-TYPE, E-EMPTY-RECORD-TYPE
@@ -132,7 +132,7 @@ pub fn nf_term(env: &TcEnv, term: &RcTerm) -> Result<RcValue, InternalError> {
.unnest()
.into_iter()
.map(|(label, binder, Embed(ann))| {
- Ok((label, binder, Embed(nf_term(env, &ann)?)))
+ Ok((label, binder, Embed(nf_term(context, &ann)?)))
})
.collect::<Result<_, _>>()?,
);
@@ -148,7 +148,7 @@ pub fn nf_term(env: &TcEnv, term: &RcTerm) -> Result<RcValue, InternalError> {
.unnest()
.into_iter()
.map(|(label, binder, Embed(term))| {
- Ok((label, binder, Embed(nf_term(env, &term)?)))
+ Ok((label, binder, Embed(nf_term(context, &term)?)))
})
.collect::<Result<_, _>>()?,
);
@@ -158,7 +158,7 @@ pub fn nf_term(env: &TcEnv, term: &RcTerm) -> Result<RcValue, InternalError> {
// E-PROJ
Term::Proj(ref expr, ref label, shift) => {
- match *nf_term(env, expr)? {
+ match *nf_term(context, expr)? {
Value::Neutral(ref neutral, ref spine) => {
return Ok(RcValue::from(Value::Neutral(
RcNeutral::from(Neutral::Proj(neutral.clone(), label.clone(), shift)),
@@ -185,7 +185,7 @@ pub fn nf_term(env: &TcEnv, term: &RcTerm) -> Result<RcValue, InternalError> {
// E-CASE
Term::Case(ref head, ref clauses) => {
- let head = nf_term(env, head)?;
+ let head = nf_term(context, head)?;
if let Value::Neutral(ref neutral, ref spine) = *head {
Ok(RcValue::from(Value::Neutral(
@@ -195,7 +195,7 @@ pub fn nf_term(env: &TcEnv, term: &RcTerm) -> Result<RcValue, InternalError> {
.iter()
.map(|clause| {
let (pattern, body) = clause.clone().unbind();
- Ok(Scope::new(pattern, nf_term(env, &body)?))
+ Ok(Scope::new(pattern, nf_term(context, &body)?))
})
.collect::<Result<_, _>>()?,
)),
@@ -204,12 +204,12 @@ pub fn nf_term(env: &TcEnv, term: &RcTerm) -> Result<RcValue, InternalError> {
} else {
for clause in clauses {
let (pattern, body) = clause.clone().unbind();
- if let Some(mappings) = match_value(env, &pattern, &head)? {
+ if let Some(mappings) = match_value(context, &pattern, &head)? {
let mappings = mappings
.into_iter()
.map(|(free_var, value)| (free_var, RcTerm::from(&*value.inner)))
.collect::<Vec<_>>();
- return nf_term(env, &body.substs(&mappings));
+ return nf_term(context, &body.substs(&mappings));
}
}
Err(InternalError::NoPatternsApplicable)
@@ -220,7 +220,7 @@ pub fn nf_term(env: &TcEnv, term: &RcTerm) -> Result<RcValue, InternalError> {
Term::Array(ref elems) => Ok(RcValue::from(Value::Array(
elems
.iter()
- .map(|elem| nf_term(env, elem))
+ .map(|elem| nf_term(context, elem))
.collect::<Result<_, _>>()?,
))),
}
@@ -229,7 +229,7 @@ pub fn nf_term(env: &TcEnv, term: &RcTerm) -> Result<RcValue, InternalError> {
/// If the pattern matches the value, this function returns the substitutions
/// needed to apply the pattern to some body expression
pub fn match_value(
- env: &TcEnv,
+ context: &Context,
pattern: &RcPattern,
value: &RcValue,
) -> Result<Option<Vec<(FreeVar<String>, RcValue)>>, InternalError> {
@@ -238,7 +238,10 @@ pub fn match_value(
Ok(Some(vec![(free_var.clone(), value.clone())]))
},
(&Pattern::Var(Embed(Var::Free(ref free_var)), _), _) => {
- match env.get_definition(free_var).map(|term| nf_term(env, term)) {
+ match context
+ .get_definition(free_var)
+ .map(|term| nf_term(context, term))
+ {
Some(Ok(ref term)) if term == value => Ok(Some(vec![])),
Some(Ok(_)) | None => Ok(None),
Some(Err(err)) => Err(err),
diff --git a/crates/pikelet-elaborate/tests/check.rs b/crates/pikelet-elaborate/tests/check.rs
index adf21a0a2..f93aabf66 100644
--- a/crates/pikelet-elaborate/tests/check.rs
+++ b/crates/pikelet-elaborate/tests/check.rs
@@ -6,7 +6,7 @@ extern crate pikelet_syntax;
use codespan::CodeMap;
-use pikelet_elaborate::{TcEnv, TypeError};
+use pikelet_elaborate::{Context, TypeError};
use pikelet_syntax::translation::{Desugar, DesugarEnv};
mod support;
@@ -14,30 +14,30 @@ mod support;
#[test]
fn record() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"Record { t : Type; x : String }";
let given_expr = r#"record { t = String; x = "hello" }"#;
- let expected_ty = support::parse_nf_term(&mut codemap, &tc_env, expected_ty);
- support::parse_check_term(&mut codemap, &tc_env, given_expr, &expected_ty);
+ let expected_ty = support::parse_nf_term(&mut codemap, &context, expected_ty);
+ support::parse_check_term(&mut codemap, &context, given_expr, &expected_ty);
}
#[test]
fn record_field_mismatch_lt() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
- let desugar_env = DesugarEnv::new(tc_env.mappings());
+ let context = Context::default();
+ let desugar_env = DesugarEnv::new(context.mappings());
let expected_ty = r"Record { x : String; y : String }";
let given_expr = r#"record { x = "hello" }"#;
- let expected_ty = support::parse_nf_term(&mut codemap, &tc_env, expected_ty);
+ let expected_ty = support::parse_nf_term(&mut codemap, &context, expected_ty);
let raw_term = support::parse_term(&mut codemap, given_expr)
.desugar(&desugar_env)
.unwrap();
- match pikelet_elaborate::check_term(&tc_env, &raw_term, &expected_ty) {
+ match pikelet_elaborate::check_term(&context, &raw_term, &expected_ty) {
Err(TypeError::RecordSizeMismatch { .. }) => {},
Err(err) => panic!("unexpected error: {:?}", err),
Ok(term) => panic!("expected error but found: {}", term),
@@ -47,18 +47,18 @@ fn record_field_mismatch_lt() {
#[test]
fn record_field_mismatch_gt() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
- let desugar_env = DesugarEnv::new(tc_env.mappings());
+ let context = Context::default();
+ let desugar_env = DesugarEnv::new(context.mappings());
let expected_ty = r"Record { x : String }";
let given_expr = r#"record { x = "hello"; y = "hello" }"#;
- let expected_ty = support::parse_nf_term(&mut codemap, &tc_env, expected_ty);
+ let expected_ty = support::parse_nf_term(&mut codemap, &context, expected_ty);
let raw_term = support::parse_term(&mut codemap, given_expr)
.desugar(&desugar_env)
.unwrap();
- match pikelet_elaborate::check_term(&tc_env, &raw_term, &expected_ty) {
+ match pikelet_elaborate::check_term(&context, &raw_term, &expected_ty) {
Err(TypeError::RecordSizeMismatch { .. }) => {},
Err(err) => panic!("unexpected error: {:?}", err),
Ok(term) => panic!("expected error but found: {}", term),
@@ -68,31 +68,31 @@ fn record_field_mismatch_gt() {
#[test]
fn dependent_record() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"Record { t : Type; x : t }";
let given_expr = r#"record { t = String; x = "hello" }"#;
- let expected_ty = support::parse_nf_term(&mut codemap, &tc_env, expected_ty);
- support::parse_check_term(&mut codemap, &tc_env, given_expr, &expected_ty);
+ let expected_ty = support::parse_nf_term(&mut codemap, &context, expected_ty);
+ support::parse_check_term(&mut codemap, &context, given_expr, &expected_ty);
}
#[test]
fn dependent_record_propagate_types() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"Record { t : Type; x : t }";
let given_expr = r#"record { t = S32; x = 1 }"#;
- let expected_ty = support::parse_nf_term(&mut codemap, &tc_env, expected_ty);
- support::parse_check_term(&mut codemap, &tc_env, given_expr, &expected_ty);
+ let expected_ty = support::parse_nf_term(&mut codemap, &context, expected_ty);
+ support::parse_check_term(&mut codemap, &context, given_expr, &expected_ty);
}
#[test]
fn case_expr() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"String";
let given_expr = r#"case "helloo" {
@@ -101,15 +101,15 @@ fn case_expr() {
greeting => (import "prim/string/append") greeting "!!";
}"#;
- let expected_ty = support::parse_nf_term(&mut codemap, &tc_env, expected_ty);
- support::parse_check_term(&mut codemap, &tc_env, given_expr, &expected_ty);
+ let expected_ty = support::parse_nf_term(&mut codemap, &context, expected_ty);
+ support::parse_check_term(&mut codemap, &context, given_expr, &expected_ty);
}
#[test]
fn case_expr_bad_literal() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
- let desugar_env = DesugarEnv::new(tc_env.mappings());
+ let context = Context::default();
+ let desugar_env = DesugarEnv::new(context.mappings());
let expected_ty = r"String";
let given_expr = r#"case "helloo" {
@@ -117,12 +117,12 @@ fn case_expr_bad_literal() {
1 => "byee";
}"#;
- let expected_ty = support::parse_nf_term(&mut codemap, &tc_env, expected_ty);
+ let expected_ty = support::parse_nf_term(&mut codemap, &context, expected_ty);
let raw_term = support::parse_term(&mut codemap, given_expr)
.desugar(&desugar_env)
.unwrap();
- match pikelet_elaborate::check_term(&tc_env, &raw_term, &expected_ty) {
+ match pikelet_elaborate::check_term(&context, &raw_term, &expected_ty) {
Err(TypeError::LiteralMismatch { .. }) => {},
Err(err) => panic!("unexpected error: {:?}", err),
Ok(term) => panic!("expected error but found: {}", term),
@@ -132,68 +132,68 @@ fn case_expr_bad_literal() {
#[test]
fn case_expr_wildcard() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"S32";
let given_expr = r#"case "helloo" {
_ => 123;
}"#;
- let expected_ty = support::parse_nf_term(&mut codemap, &tc_env, expected_ty);
- support::parse_check_term(&mut codemap, &tc_env, given_expr, &expected_ty);
+ let expected_ty = support::parse_nf_term(&mut codemap, &context, expected_ty);
+ support::parse_check_term(&mut codemap, &context, given_expr, &expected_ty);
}
#[test]
fn case_expr_empty() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"String";
let given_expr = r#"case "helloo" {}"#;
- let expected_ty = support::parse_nf_term(&mut codemap, &tc_env, expected_ty);
- support::parse_check_term(&mut codemap, &tc_env, given_expr, &expected_ty);
+ let expected_ty = support::parse_nf_term(&mut codemap, &context, expected_ty);
+ support::parse_check_term(&mut codemap, &context, given_expr, &expected_ty);
}
#[test]
fn array_0_string() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"Array 0 String";
let given_expr = r#"[]"#;
- let expected_ty = support::parse_nf_term(&mut codemap, &tc_env, expected_ty);
- support::parse_check_term(&mut codemap, &tc_env, given_expr, &expected_ty);
+ let expected_ty = support::parse_nf_term(&mut codemap, &context, expected_ty);
+ support::parse_check_term(&mut codemap, &context, given_expr, &expected_ty);
}
#[test]
fn array_3_string() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"Array 3 String";
let given_expr = r#"["hello"; "hi"; "byee"]"#;
- let expected_ty = support::parse_nf_term(&mut codemap, &tc_env, expected_ty);
- support::parse_check_term(&mut codemap, &tc_env, given_expr, &expected_ty);
+ let expected_ty = support::parse_nf_term(&mut codemap, &context, expected_ty);
+ support::parse_check_term(&mut codemap, &context, given_expr, &expected_ty);
}
#[test]
fn array_len_mismatch() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
- let desugar_env = DesugarEnv::new(tc_env.mappings());
+ let context = Context::default();
+ let desugar_env = DesugarEnv::new(context.mappings());
let expected_ty = r"Array 3 String";
let given_expr = r#"["hello"; "hi"]"#;
- let expected_ty = support::parse_nf_term(&mut codemap, &tc_env, expected_ty);
+ let expected_ty = support::parse_nf_term(&mut codemap, &context, expected_ty);
let raw_term = support::parse_term(&mut codemap, given_expr)
.desugar(&desugar_env)
.unwrap();
- match pikelet_elaborate::check_term(&tc_env, &raw_term, &expected_ty) {
+ match pikelet_elaborate::check_term(&context, &raw_term, &expected_ty) {
Err(TypeError::ArrayLengthMismatch { .. }) => {},
Err(err) => panic!("unexpected error: {:?}", err),
Ok(term) => panic!("expected error but found: {}", term),
@@ -203,18 +203,18 @@ fn array_len_mismatch() {
#[test]
fn array_elem_ty_mismatch() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
- let desugar_env = DesugarEnv::new(tc_env.mappings());
+ let context = Context::default();
+ let desugar_env = DesugarEnv::new(context.mappings());
let expected_ty = r"Array 3 String";
let given_expr = r#"["hello"; "hi"; 4]"#;
- let expected_ty = support::parse_nf_term(&mut codemap, &tc_env, expected_ty);
+ let expected_ty = support::parse_nf_term(&mut codemap, &context, expected_ty);
let raw_term = support::parse_term(&mut codemap, given_expr)
.desugar(&desugar_env)
.unwrap();
- match pikelet_elaborate::check_term(&tc_env, &raw_term, &expected_ty) {
+ match pikelet_elaborate::check_term(&context, &raw_term, &expected_ty) {
Err(_) => {},
Ok(term) => panic!("expected error but found: {}", term),
}
diff --git a/crates/pikelet-elaborate/tests/infer.rs b/crates/pikelet-elaborate/tests/infer.rs
index 2aac3815d..0b340aaf1 100644
--- a/crates/pikelet-elaborate/tests/infer.rs
+++ b/crates/pikelet-elaborate/tests/infer.rs
@@ -8,7 +8,7 @@ extern crate pikelet_syntax;
use codespan::{ByteIndex, ByteSpan, CodeMap};
use moniker::{FreeVar, Var};
-use pikelet_elaborate::{TcEnv, TypeError};
+use pikelet_elaborate::{Context, TypeError};
use pikelet_syntax::translation::{Desugar, DesugarEnv};
use pikelet_syntax::{concrete, raw};
@@ -18,7 +18,7 @@ mod support;
fn undefined_name() {
use pikelet_syntax::LevelShift;
- let tc_env = TcEnv::default();
+ let context = Context::default();
let x = FreeVar::fresh_named("x");
let given_expr = raw::RcTerm::from(raw::Term::Var(
@@ -28,7 +28,7 @@ fn undefined_name() {
));
assert_eq!(
- pikelet_elaborate::infer_term(&tc_env, &given_expr),
+ pikelet_elaborate::infer_term(&context, &given_expr),
Err(TypeError::UndefinedName {
span: ByteSpan::default(),
free_var: x.clone(),
@@ -39,8 +39,8 @@ fn undefined_name() {
#[test]
fn import_not_found() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
- let desugar_env = DesugarEnv::new(tc_env.mappings());
+ let context = Context::default();
+ let desugar_env = DesugarEnv::new(context.mappings());
let given_expr = r#"import "does-not-exist" : Record {}"#;
@@ -48,7 +48,7 @@ fn import_not_found() {
.desugar(&desugar_env)
.unwrap();
- match pikelet_elaborate::infer_term(&tc_env, &raw_term) {
+ match pikelet_elaborate::infer_term(&context, &raw_term) {
Err(TypeError::UndefinedImport { .. }) => {},
Err(err) => panic!("unexpected error: {:?}", err),
Ok((term, ty)) => panic!("expected error, found {} : {}", term, ty),
@@ -58,64 +58,64 @@ fn import_not_found() {
#[test]
fn ty() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"Type^1";
let given_expr = r"Type";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn ty_levels() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"Type^1";
let given_expr = r"Type^0 : Type^1 : Type^2 : Type^3"; //... Type^∞ ...+:｡(ﾉ･ω･)ﾉﾞ
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn ann_ty_id() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"Type -> Type";
let given_expr = r"(\a => a) : Type -> Type";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn ann_arrow_ty_id() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"(Type -> Type) -> (Type -> Type)";
let given_expr = r"(\a => a) : (Type -> Type) -> (Type -> Type)";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn ann_id_as_ty() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
- let desugar_env = DesugarEnv::new(tc_env.mappings());
+ let context = Context::default();
+ let desugar_env = DesugarEnv::new(context.mappings());
let given_expr = r"(\a => a) : Type";
@@ -123,7 +123,7 @@ fn ann_id_as_ty() {
.desugar(&desugar_env)
.unwrap();
- match pikelet_elaborate::infer_term(&tc_env, &raw_term) {
+ match pikelet_elaborate::infer_term(&context, &raw_term) {
Err(TypeError::UnexpectedFunction { .. }) => {},
other => panic!("unexpected result: {:#?}", other),
}
@@ -132,22 +132,22 @@ fn ann_id_as_ty() {
#[test]
fn app() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"Type^1";
let given_expr = r"(\a : Type^1 => a) Type";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn app_ty() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
- let desugar_env = DesugarEnv::new(tc_env.mappings());
+ let context = Context::default();
+ let desugar_env = DesugarEnv::new(context.mappings());
let given_expr = r"Type Type";
@@ -156,7 +156,7 @@ fn app_ty() {
.unwrap();
assert_eq!(
- pikelet_elaborate::infer_term(&tc_env, &raw_term),
+ pikelet_elaborate::infer_term(&context, &raw_term),
Err(TypeError::ArgAppliedToNonFunction {
fn_span: ByteSpan::new(ByteIndex(1), ByteIndex(5)),
arg_span: ByteSpan::new(ByteIndex(6), ByteIndex(10)),
@@ -168,56 +168,56 @@ fn app_ty() {
#[test]
fn lam() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"(a : Type) -> Type";
let given_expr = r"\a : Type => a";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn pi() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"Type^1";
let given_expr = r"(a : Type) -> a";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn id() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"(a : Type) -> a -> a";
let given_expr = r"\(a : Type) (x : a) => x";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn id_ann() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"(a : Type) -> a -> a";
let given_expr = r"(\a (x : a) => x) : (A : Type) -> A -> A";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
@@ -226,14 +226,14 @@ fn id_ann() {
#[test]
fn id_app_ty() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"Type -> Type";
let given_expr = r"(\(a : Type^1) (x : a) => x) Type";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
@@ -241,119 +241,119 @@ fn id_app_ty() {
#[test]
fn id_app_ty_ty() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"Type^1";
let given_expr = r"(\(a : Type^2) (x : a) => x) (Type^1) Type";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn id_app_ty_arr_ty() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"Type^1";
let given_expr = r"(\(a : Type^2) (x : a) => x) (Type^1) (Type -> Type)";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn id_app_arr_pi_ty() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"Type -> Type";
let given_expr = r"(\(a : Type^1) (x : a) => x) (Type -> Type) (\x => x)";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn apply() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"(a b : Type) -> (a -> b) -> a -> b";
let given_expr = r"\(a b : Type) (f : a -> b) (x : a) => f x";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn const_() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"(a b : Type) -> a -> b -> a";
let given_expr = r"\(a b : Type) (x : a) (y : b) => x";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn const_flipped() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"(a b : Type) -> a -> b -> b";
let given_expr = r"\(a b : Type) (x : a) (y : b) => y";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn flip() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"(a b c : Type) -> (a -> b -> c) -> (b -> a -> c)";
let given_expr = r"\(a b c : Type) (f : a -> b -> c) (y : b) (x : a) => f x y";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn compose() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"(a b c : Type) -> (b -> c) -> (a -> b) -> (a -> c)";
let given_expr = r"\(a b c : Type) (f : b -> c) (g : a -> b) (x : a) => f (g x)";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn let_expr_1() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"String";
let given_expr = r#"
@@ -363,15 +363,15 @@ fn let_expr_1() {
"#;
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn let_expr_2() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"String";
let given_expr = r#"
@@ -382,15 +382,15 @@ fn let_expr_2() {
"#;
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn let_shift_universes() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r#"
let
@@ -412,13 +412,13 @@ fn let_shift_universes() {
record {}
"#;
- support::parse_infer_term(&mut codemap, &tc_env, given_expr);
+ support::parse_infer_term(&mut codemap, &context, given_expr);
}
#[test]
fn let_shift_universes_id_self_application() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
// Here is a curious example from the Idris docs:
// http://docs.idris-lang.org/en/v1.3.0/tutorial/miscellany.html#cumulativity
@@ -445,13 +445,13 @@ fn let_shift_universes_id_self_application() {
record {}
"#;
- support::parse_infer_term(&mut codemap, &tc_env, given_expr);
+ support::parse_infer_term(&mut codemap, &context, given_expr);
}
#[test]
fn let_shift_universes_literals() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r#"
let
@@ -463,14 +463,14 @@ fn let_shift_universes_literals() {
record {}
"#;
- support::parse_infer_term(&mut codemap, &tc_env, given_expr);
+ support::parse_infer_term(&mut codemap, &context, given_expr);
}
#[test]
fn let_shift_universes_literals_bad() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
- let desugar_env = DesugarEnv::new(tc_env.mappings());
+ let context = Context::default();
+ let desugar_env = DesugarEnv::new(context.mappings());
let given_expr = r#"
let
@@ -486,7 +486,7 @@ fn let_shift_universes_literals_bad() {
.desugar(&desugar_env)
.unwrap();
- match pikelet_elaborate::infer_term(&tc_env, &raw_term) {
+ match pikelet_elaborate::infer_term(&context, &raw_term) {
Ok(_) => panic!("expected error"),
Err(TypeError::LiteralMismatch { .. }) => {},
Err(err) => panic!("unexpected error: {}", err),
@@ -496,8 +496,8 @@ fn let_shift_universes_literals_bad() {
#[test]
fn let_shift_universes_too_little() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
- let desugar_env = DesugarEnv::new(tc_env.mappings());
+ let context = Context::default();
+ let desugar_env = DesugarEnv::new(context.mappings());
let given_expr = r#"
let
@@ -513,7 +513,7 @@ fn let_shift_universes_too_little() {
.desugar(&desugar_env)
.unwrap();
- match pikelet_elaborate::infer_term(&tc_env, &raw_term) {
+ match pikelet_elaborate::infer_term(&context, &raw_term) {
Ok(_) => panic!("expected error"),
Err(TypeError::Mismatch { .. }) => {},
Err(err) => panic!("unexpected error: {}", err),
@@ -523,7 +523,7 @@ fn let_shift_universes_too_little() {
#[test]
fn let_shift_universes_too_much() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r#"
let
@@ -535,13 +535,13 @@ fn let_shift_universes_too_much() {
record {}
"#;
- support::parse_infer_term(&mut codemap, &tc_env, given_expr);
+ support::parse_infer_term(&mut codemap, &context, given_expr);
}
#[test]
fn case_expr() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"String";
let given_expr = r#"case "helloo" {
@@ -551,15 +551,15 @@ fn case_expr() {
}"#;
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn case_expr_bool() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"String";
let given_expr = r#"case true {
@@ -568,16 +568,16 @@ fn case_expr_bool() {
}"#;
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn case_expr_bool_bad() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
- let desugar_env = DesugarEnv::new(tc_env.mappings());
+ let context = Context::default();
+ let desugar_env = DesugarEnv::new(context.mappings());
let given_expr = r#"case "hello" {
true => "hello";
@@ -588,7 +588,7 @@ fn case_expr_bool_bad() {
.desugar(&desugar_env)
.unwrap();
- match pikelet_elaborate::infer_term(&tc_env, &raw_term) {
+ match pikelet_elaborate::infer_term(&context, &raw_term) {
Err(TypeError::Mismatch { .. }) => {},
Err(err) => panic!("unexpected error: {:?}", err),
Ok((term, ty)) => panic!("expected error, found {} : {}", term, ty),
@@ -598,7 +598,7 @@ fn case_expr_bool_bad() {
#[test]
fn case_expr_wildcard() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"String";
let given_expr = r#"case "helloo" {
@@ -606,16 +606,16 @@ fn case_expr_wildcard() {
}"#;
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn case_expr_empty() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
- let desugar_env = DesugarEnv::new(tc_env.mappings());
+ let context = Context::default();
+ let desugar_env = DesugarEnv::new(context.mappings());
let given_expr = r#"case "helloo" {}"#;
@@ -623,7 +623,7 @@ fn case_expr_empty() {
.desugar(&desugar_env)
.unwrap();
- match pikelet_elaborate::infer_term(&tc_env, &raw_term) {
+ match pikelet_elaborate::infer_term(&context, &raw_term) {
Err(TypeError::AmbiguousEmptyCase { .. }) => {},
other => panic!("unexpected result: {:#?}", other),
}
@@ -635,7 +635,7 @@ mod church_encodings {
#[test]
fn void() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r"
record {
@@ -652,13 +652,13 @@ mod church_encodings {
}
";
- support::parse_infer_term(&mut codemap, &tc_env, given_expr);
+ support::parse_infer_term(&mut codemap, &context, given_expr);
}
#[test]
fn unit() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r"
record {
@@ -675,13 +675,13 @@ mod church_encodings {
}
";
- support::parse_infer_term(&mut codemap, &tc_env, given_expr);
+ support::parse_infer_term(&mut codemap, &context, given_expr);
}
#[test]
fn and() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r"
record {
@@ -705,13 +705,13 @@ mod church_encodings {
}
";
- support::parse_infer_term(&mut codemap, &tc_env, given_expr);
+ support::parse_infer_term(&mut codemap, &context, given_expr);
}
#[test]
fn or() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r"
record {
@@ -733,85 +733,85 @@ mod church_encodings {
}
";
- support::parse_infer_term(&mut codemap, &tc_env, given_expr);
+ support::parse_infer_term(&mut codemap, &context, given_expr);
}
}
#[test]
fn empty_record_ty() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"Type";
let given_expr = r"Record {}";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn empty_record() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"Record {}";
let given_expr = r"record {}";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn dependent_record_ty() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"Type^2";
let given_expr = r"Record { t : Type^1; x : t }";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn record() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"Record { t : Type; x : String }";
let given_expr = r#"record { t = String; x = "Hello" }"#;
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn proj() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"String";
let given_expr = r#"(record { t = String; x = "hello" } : Record { t : Type; x : String }).x"#;
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn proj_missing() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
- let desugar_env = DesugarEnv::new(tc_env.mappings());
+ let context = Context::default();
+ let desugar_env = DesugarEnv::new(context.mappings());
let given_expr = r#"(record { x = "hello" } : Record { x : String }).bloop"#;
@@ -819,7 +819,7 @@ fn proj_missing() {
.desugar(&desugar_env)
.unwrap();
- match pikelet_elaborate::infer_term(&tc_env, &raw_term) {
+ match pikelet_elaborate::infer_term(&context, &raw_term) {
Err(TypeError::NoFieldInType { .. }) => {},
x => panic!("expected a field lookup error, found {:?}", x),
}
@@ -828,7 +828,7 @@ fn proj_missing() {
#[test]
fn proj_weird1() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"Type^1";
let given_expr = r"Record {
@@ -842,15 +842,15 @@ fn proj_weird1() {
}";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn proj_weird2() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"Type^1";
let given_expr = r"Record {
@@ -863,15 +863,15 @@ fn proj_weird2() {
}";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn proj_shift() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let expected_ty = r"(a : Type^1) -> a -> a";
let given_expr = r"record {
@@ -879,16 +879,16 @@ fn proj_shift() {
}.id^1";
assert_term_eq!(
- support::parse_infer_term(&mut codemap, &tc_env, given_expr).1,
- support::parse_nf_term(&mut codemap, &tc_env, expected_ty),
+ support::parse_infer_term(&mut codemap, &context, given_expr).1,
+ support::parse_nf_term(&mut codemap, &context, expected_ty),
);
}
#[test]
fn array_ambiguous() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
- let desugar_env = DesugarEnv::new(tc_env.mappings());
+ let context = Context::default();
+ let desugar_env = DesugarEnv::new(context.mappings());
let given_expr = r#"[1; 2 : S32]"#;
@@ -896,7 +896,7 @@ fn array_ambiguous() {
.desugar(&desugar_env)
.unwrap();
- match pikelet_elaborate::infer_term(&tc_env, &raw_term) {
+ match pikelet_elaborate::infer_term(&context, &raw_term) {
Err(TypeError::AmbiguousArrayLiteral { .. }) => {},
Err(err) => panic!("unexpected error: {:?}", err),
Ok((term, ty)) => panic!("expected error, found {} : {}", term, ty),
diff --git a/crates/pikelet-elaborate/tests/normalize.rs b/crates/pikelet-elaborate/tests/normalize.rs
index 3431f7e5b..050a25760 100644
--- a/crates/pikelet-elaborate/tests/normalize.rs
+++ b/crates/pikelet-elaborate/tests/normalize.rs
@@ -8,20 +8,20 @@ extern crate pikelet_syntax;
use codespan::CodeMap;
use moniker::{Binder, Embed, FreeVar, Scope, Var};
-use pikelet_elaborate::TcEnv;
+use pikelet_elaborate::Context;
use pikelet_syntax::core::{Neutral, RcNeutral, RcTerm, RcValue, Term, Value};
mod support;
#[test]
fn var() {
- let tc_env = TcEnv::default();
+ let context = Context::default();
let x = FreeVar::fresh_named("x");
let var = RcTerm::from(Term::var(Var::Free(x.clone()), 0));
assert_eq!(
- pikelet_elaborate::nf_term(&tc_env, &var).unwrap(),
+ pikelet_elaborate::nf_term(&context, &var).unwrap(),
RcValue::from(Value::var(Var::Free(x), 0)),
);
}
@@ -29,10 +29,10 @@ fn var() {
#[test]
fn ty() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
assert_eq!(
- support::parse_nf_term(&mut codemap, &tc_env, r"Type"),
+ support::parse_nf_term(&mut codemap, &context, r"Type"),
RcValue::from(Value::universe(0)),
);
}
@@ -40,12 +40,12 @@ fn ty() {
#[test]
fn lam() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let x = FreeVar::fresh_named("x");
assert_term_eq!(
- support::parse_nf_term(&mut codemap, &tc_env, r"\x : Type => x"),
+ support::parse_nf_term(&mut codemap, &context, r"\x : Type => x"),
RcValue::from(Value::Lam(Scope::new(
(Binder(x.clone()), Embed(RcValue::from(Value::universe(0)))),
RcValue::from(Value::var(Var::Free(x), 0)),
@@ -56,12 +56,12 @@ fn lam() {
#[test]
fn pi() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let x = FreeVar::fresh_named("x");
assert_term_eq!(
- support::parse_nf_term(&mut codemap, &tc_env, r"(x : Type) -> x"),
+ support::parse_nf_term(&mut codemap, &context, r"(x : Type) -> x"),
RcValue::from(Value::Pi(Scope::new(
(Binder(x.clone()), Embed(RcValue::from(Value::universe(0)))),
RcValue::from(Value::var(Var::Free(x), 0)),
@@ -72,7 +72,7 @@ fn pi() {
#[test]
fn lam_app() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r"\(x : Type -> Type) (y : Type) => x y";
@@ -87,7 +87,7 @@ fn lam_app() {
)));
assert_term_eq!(
- support::parse_nf_term(&mut codemap, &tc_env, given_expr,),
+ support::parse_nf_term(&mut codemap, &context, given_expr,),
RcValue::from(Value::Lam(Scope::new(
(Binder(x.clone()), Embed(ty_arr)),
RcValue::from(Value::Lam(Scope::new(
@@ -104,7 +104,7 @@ fn lam_app() {
#[test]
fn pi_app() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r"(x : Type -> Type) -> (y : Type) -> x y";
@@ -119,7 +119,7 @@ fn pi_app() {
)));
assert_term_eq!(
- support::parse_nf_term(&mut codemap, &tc_env, given_expr),
+ support::parse_nf_term(&mut codemap, &context, given_expr),
RcValue::from(Value::Pi(Scope::new(
(Binder(x.clone()), Embed(ty_arr)),
RcValue::from(Value::Pi(Scope::new(
@@ -138,14 +138,14 @@ fn pi_app() {
#[test]
fn id_app_ty() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r"(\(a : Type^1) (x : a) => x) Type";
let expected_expr = r"\x : Type => x";
assert_term_eq!(
- support::parse_nf_term(&mut codemap, &tc_env, given_expr),
- support::parse_nf_term(&mut codemap, &tc_env, expected_expr),
+ support::parse_nf_term(&mut codemap, &context, given_expr),
+ support::parse_nf_term(&mut codemap, &context, expected_expr),
);
}
@@ -153,14 +153,14 @@ fn id_app_ty() {
#[test]
fn id_app_ty_ty() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r"(\(a : Type^2) (x : a) => x) (Type^1) Type";
let expected_expr = r"Type";
assert_term_eq!(
- support::parse_nf_term(&mut codemap, &tc_env, given_expr),
- support::parse_nf_term(&mut codemap, &tc_env, expected_expr),
+ support::parse_nf_term(&mut codemap, &context, given_expr),
+ support::parse_nf_term(&mut codemap, &context, expected_expr),
);
}
@@ -169,14 +169,14 @@ fn id_app_ty_ty() {
#[test]
fn id_app_ty_arr_ty() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r"(\(a : Type^2) (x : a) => x) (Type^1) (Type -> Type)";
let expected_expr = r"Type -> Type";
assert_term_eq!(
- support::parse_nf_term(&mut codemap, &tc_env, given_expr),
- support::parse_nf_term(&mut codemap, &tc_env, expected_expr),
+ support::parse_nf_term(&mut codemap, &context, given_expr),
+ support::parse_nf_term(&mut codemap, &context, expected_expr),
);
}
@@ -184,7 +184,7 @@ fn id_app_ty_arr_ty() {
#[test]
fn id_app_id() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r"
(\(a : Type^1) (x : a) => x)
@@ -194,8 +194,8 @@ fn id_app_id() {
let expected_expr = r"\(a : Type) (x : a) => x";
assert_term_eq!(
- support::parse_nf_term(&mut codemap, &tc_env, given_expr),
- support::parse_nf_term(&mut codemap, &tc_env, expected_expr),
+ support::parse_nf_term(&mut codemap, &context, given_expr),
+ support::parse_nf_term(&mut codemap, &context, expected_expr),
);
}
@@ -204,7 +204,7 @@ fn id_app_id() {
#[test]
fn const_app_id_ty() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r"
(\(a : Type^1) (b : Type^2) (x : a) (y : b) => x)
@@ -216,43 +216,43 @@ fn const_app_id_ty() {
let expected_expr = r"\(a : Type) (x : a) => x";
assert_term_eq!(
- support::parse_nf_term(&mut codemap, &tc_env, given_expr),
- support::parse_nf_term(&mut codemap, &tc_env, expected_expr),
+ support::parse_nf_term(&mut codemap, &context, given_expr),
+ support::parse_nf_term(&mut codemap, &context, expected_expr),
);
}
#[test]
fn horrifying_app_1() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r"(\(t : Type) (f : (a : Type) -> Type) => f t) String (\(a : Type) => a)";
let expected_expr = r"String";
assert_term_eq!(
- support::parse_nf_term(&mut codemap, &tc_env, given_expr),
- support::parse_nf_term(&mut codemap, &tc_env, expected_expr),
+ support::parse_nf_term(&mut codemap, &context, given_expr),
+ support::parse_nf_term(&mut codemap, &context, expected_expr),
);
}
#[test]
fn horrifying_app_2() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r#"(\(t: String) (f: String -> String) => f t) "hello""#;
let expected_expr = r#"\(f : String -> String) => f "hello""#;
assert_term_eq!(
- support::parse_nf_term(&mut codemap, &tc_env, given_expr),
- support::parse_nf_term(&mut codemap, &tc_env, expected_expr),
+ support::parse_nf_term(&mut codemap, &context, given_expr),
+ support::parse_nf_term(&mut codemap, &context, expected_expr),
);
}
#[test]
fn let_expr_1() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r#"
let x = "helloo";
@@ -264,15 +264,15 @@ fn let_expr_1() {
"#;
assert_term_eq!(
- support::parse_nf_term(&mut codemap, &tc_env, given_expr),
- support::parse_nf_term(&mut codemap, &tc_env, expected_expr),
+ support::parse_nf_term(&mut codemap, &context, given_expr),
+ support::parse_nf_term(&mut codemap, &context, expected_expr),
);
}
#[test]
fn let_expr_2() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r#"
let x = "helloo";
@@ -285,15 +285,15 @@ fn let_expr_2() {
"#;
assert_term_eq!(
- support::parse_nf_term(&mut codemap, &tc_env, given_expr),
- support::parse_nf_term(&mut codemap, &tc_env, expected_expr),
+ support::parse_nf_term(&mut codemap, &context, given_expr),
+ support::parse_nf_term(&mut codemap, &context, expected_expr),
);
}
#[test]
fn if_true() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r#"
if true then "true" else "false"
@@ -303,15 +303,15 @@ fn if_true() {
"#;
assert_term_eq!(
- support::parse_nf_term(&mut codemap, &tc_env, given_expr),
- support::parse_nf_term(&mut codemap, &tc_env, expected_expr),
+ support::parse_nf_term(&mut codemap, &context, given_expr),
+ support::parse_nf_term(&mut codemap, &context, expected_expr),
);
}
#[test]
fn if_false() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r#"
if false then "true" else "false"
@@ -321,15 +321,15 @@ fn if_false() {
"#;
assert_term_eq!(
- support::parse_nf_term(&mut codemap, &tc_env, given_expr),
- support::parse_nf_term(&mut codemap, &tc_env, expected_expr),
+ support::parse_nf_term(&mut codemap, &context, given_expr),
+ support::parse_nf_term(&mut codemap, &context, expected_expr),
);
}
#[test]
fn if_eval_cond() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r#"
let is-hi (greeting : String) = case greeting {
@@ -350,15 +350,15 @@ fn if_eval_cond() {
"#;
assert_term_eq!(
- support::parse_nf_term(&mut codemap, &tc_env, given_expr),
- support::parse_nf_term(&mut codemap, &tc_env, expected_expr),
+ support::parse_nf_term(&mut codemap, &context, given_expr),
+ support::parse_nf_term(&mut codemap, &context, expected_expr),
);
}
#[test]
fn case_expr_bool() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r#"
record {
@@ -380,21 +380,21 @@ fn case_expr_bool() {
"#;
assert_term_eq!(
- support::parse_nf_term(&mut codemap, &tc_env, given_expr),
- support::parse_nf_term(&mut codemap, &tc_env, expected_expr),
+ support::parse_nf_term(&mut codemap, &context, given_expr),
+ support::parse_nf_term(&mut codemap, &context, expected_expr),
);
}
#[test]
fn record_shadow() {
let mut codemap = CodeMap::new();
- let tc_env = TcEnv::default();
+ let context = Context::default();
let given_expr = r"(\t : Type => Record { String : Type; x : t; y : String }) String";
let expected_expr = r#"Record { String as String1 : Type; x : String; y : String1 }"#;
assert_term_eq!(
- support::parse_nf_term(&mut codemap, &tc_env, given_expr),
- support::parse_nf_term(&mut codemap, &tc_env, expected_expr),
+ support::parse_nf_term(&mut codemap, &context, given_expr),
+ support::parse_nf_term(&mut codemap, &context, expected_expr),
);
}
diff --git a/crates/pikelet-elaborate/tests/support/mod.rs b/crates/pikelet-elaborate/tests/support/mod.rs
index be1cf42c9..b5946fec2 100644
--- a/crates/pikelet-elaborate/tests/support/mod.rs
+++ b/crates/pikelet-elaborate/tests/support/mod.rs
@@ -4,7 +4,7 @@ use codespan::{CodeMap, FileName};
use codespan_reporting;
use codespan_reporting::termcolor::{ColorChoice, StandardStream};
-use pikelet_elaborate::{self, TcEnv};
+use pikelet_elaborate::{self, Context};
use pikelet_syntax::concrete;
use pikelet_syntax::core::{RcTerm, RcType, RcValue};
use pikelet_syntax::parse;
@@ -25,11 +25,11 @@ pub fn parse_term(codemap: &mut CodeMap, src: &str) -> concrete::Term {
concrete_term
}
-pub fn parse_infer_term(codemap: &mut CodeMap, tc_env: &TcEnv, src: &str) -> (RcTerm, RcType) {
+pub fn parse_infer_term(codemap: &mut CodeMap, context: &Context, src: &str) -> (RcTerm, RcType) {
let raw_term = parse_term(codemap, src)
- .desugar(&DesugarEnv::new(tc_env.mappings()))
+ .desugar(&DesugarEnv::new(context.mappings()))
.unwrap();
- match pikelet_elaborate::infer_term(tc_env, &raw_term) {
+ match pikelet_elaborate::infer_term(context, &raw_term) {
Ok((term, ty)) => (term, ty),
Err(error) => {
let writer = StandardStream::stdout(ColorChoice::Always);
@@ -39,9 +39,9 @@ pub fn parse_infer_term(codemap: &mut CodeMap, tc_env: &TcEnv, src: &str) -> (Rc
}
}
-pub fn parse_nf_term(codemap: &mut CodeMap, tc_env: &TcEnv, src: &str) -> RcValue {
- let term = parse_infer_term(codemap, tc_env, src).0;
- match pikelet_elaborate::nf_term(tc_env, &term) {
+pub fn parse_nf_term(codemap: &mut CodeMap, context: &Context, src: &str) -> RcValue {
+ let term = parse_infer_term(codemap, context, src).0;
+ match pikelet_elaborate::nf_term(context, &term) {
Ok(value) => value,
Err(error) => {
let writer = StandardStream::stdout(ColorChoice::Always);
@@ -51,11 +51,11 @@ pub fn parse_nf_term(codemap: &mut CodeMap, tc_env: &TcEnv, src: &str) -> RcValu
}
}
-pub fn parse_check_term(codemap: &mut CodeMap, tc_env: &TcEnv, src: &str, expected: &RcType) {
+pub fn parse_check_term(codemap: &mut CodeMap, context: &Context, src: &str, expected: &RcType) {
let raw_term = parse_term(codemap, src)
- .desugar(&DesugarEnv::new(tc_env.mappings()))
+ .desugar(&DesugarEnv::new(context.mappings()))
.unwrap();
- match pikelet_elaborate::check_term(tc_env, &raw_term, expected) {
+ match pikelet_elaborate::check_term(context, &raw_term, expected) {
Ok(_) => {},
Err(error) => {
let writer = StandardStream::stdout(ColorChoice::Always);