Skip to content

Commit

Permalink
Merge pull request pikelet-lang#174 from brendanzab/env-cleanups
Browse files Browse the repository at this point in the history 
Environment cleanups
  • Loading branch information
@brendanzab
brendanzab authored Oct 29, 2018
2 parents ba7c7f7 + 9ba20ea commit 8cf04f3
Show file tree
Hide file tree
Showing 8 changed files with 477 additions and 484 deletions.
27 changes: 14 additions & 13 deletions crates/pikelet-driver/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -146,17 +146,17 @@ 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};

/// An environment that keeps track of the state of a Pikelet program during
/// 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,
Expand All @@ -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(),
}
Expand Down Expand Up @@ -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(())
Expand All @@ -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))
}
Expand All @@ -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)
}
}

Expand Down
134 changes: 55 additions & 79 deletions crates/pikelet-elaborate/src/env.rs → crates/pikelet-elaborate/src/context.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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 {
Expand Down Expand Up @@ -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;
Expand All @@ -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)),
Expand All @@ -290,45 +276,44 @@ 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())),
universe0.clone(),
))),
)));

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 {
Expand All @@ -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);
}};
}

Expand Down Expand Up @@ -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
}
Expand Down Expand Up @@ -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> {
Expand All @@ -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) {
Expand All @@ -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)
}
}
Loading

0 comments on commit 8cf04f3

Please sign in to comment.