Crate restructure in preparation for NbE

Cargo.toml

@@ -1,9 +1,10 @@
 [workspace]
 members = [
     "./crates/pikelet",
+    "./crates/pikelet-concrete",
+    "./crates/pikelet-core",
     "./crates/pikelet-driver",
-    "./crates/pikelet-elaborate",
     "./crates/pikelet-language-server",
+    "./crates/pikelet-library",
     "./crates/pikelet-repl",
-    "./crates/pikelet-syntax",
 ]

crates/README.md

@@ -19,14 +19,14 @@ your stay!
 
 ### Compiler
 
-| Name                        | Description                                             |
-|-----------------------------|---------------------------------------------------------|
-| [`pikelet-driver`]          | Main entry-point for the compiler pipeline              |
-| [`pikelet-library`]         | Builtin libraries                                       |
-| [`pikelet-syntax`]          | Parsing, ASTs, pretty printing, and desugaring          |
-| [`pikelet-elaborate`]       | Type checking, normalization, and elaboration of terms  |
+| Name                        | Description                                                       |
+|-----------------------------|-------------------------------------------------------------------|
+| [`pikelet-driver`]          | Main entry-point for the compiler pipeline                        |
+| [`pikelet-library`]         | Builtin libraries                                                 |
+| [`pikelet-concrete`]        | Parsing, pretty printing, and elaboration of the concrete syntax  |
+| [`pikelet-core`]            | Normalization-by-evaluation and checking of the core language     |
 
 [`pikelet-driver`]: /crates/pikelet-driver
 [`pikelet-library`]: /crates/pikelet-library
-[`pikelet-syntax`]: /crates/pikelet-syntax
-[`pikelet-elaborate`]: /crates/pikelet-elaborate
+[`pikelet-concrete`]: /crates/pikelet-concrete
+[`pikelet-core`]: /crates/pikelet-core

crates/pikelet-syntax/Cargo.toml → crates/pikelet-concrete/Cargo.toml

@@ -1,5 +1,5 @@
 [package]
-name = "pikelet-syntax"
+name = "pikelet-concrete"
 version = "0.1.0"
 license = "Apache-2.0"
 readme = "README.md"
@@ -15,6 +15,7 @@ failure = "0.1.2"
 im = "12.2.0"
 lalrpop-util = "0.16.0"
 moniker = { version = "0.5.0", features = ["codespan", "im"] }
+pikelet-core = { version = "0.1.0", path = "../pikelet-core" }
 pretty = { version = "0.5.2", features = ["termcolor"] }
 unicode-xid = "0.1.0"
 

crates/pikelet-concrete/README.md

@@ -0,0 +1,17 @@
+# Pikelet Concrete Syntax
+
+This crate is responsible for:
+
+- defining data structures for:
+  - concrete terms
+  - raw terms
+- parsing the concrete syntax
+- pretty printing
+- desugaring from the concrete syntax
+- resugaring to the concrete syntax
+- bidirectional elaboration, involving:
+  - bidirectional type checking
+  - passing implicit arguments explicitly (TODO)
+  - passing instance arguments explicitly (TODO)
+  - returning the fully explicit core syntax
+

crates/pikelet-syntax/src/translation/desugar.rs → crates/pikelet-concrete/src/desugar.rs

@@ -3,9 +3,10 @@ use codespan_reporting::{Diagnostic, Label as DiagnosticLabel};
 use im;
 use moniker::{Binder, Embed, FreeVar, Nest, Scope, Var};
 
-use concrete;
-use raw;
-use {Label, Level, LevelShift};
+use pikelet_core::syntax::{Label, Level, LevelShift};
+
+use syntax::concrete;
+use syntax::raw;
 
 /// The environment used when desugaring from the concrete to raw syntax
 #[derive(Debug, Clone)]
@@ -386,41 +387,33 @@ fn desugar_record_ty(
 fn desugar_record_intro(
     env: &DesugarEnv,
     span: ByteSpan,
-    fields: &[concrete::RecordField],
+    fields: &[concrete::RecordIntroField],
 ) -> Result<raw::RcTerm, DesugarError> {
-    use concrete::RecordField;
-
-    let mut env = env.clone();
+    use syntax::concrete::RecordIntroField;
 
     let fields = fields
         .iter()
         .map(|field| match field {
-            RecordField::Punned {
+            RecordIntroField::Punned {
                 label: (_, ref name),
                 shift,
             } => {
                 let var = env.on_name(span, name, shift.unwrap_or(0));
-                let free_var = env.on_binding(name);
-                Ok((Label(name.clone()), Binder(free_var), Embed(var)))
+                Ok((Label(name.clone()), var))
             },
-            RecordField::Explicit {
+            RecordIntroField::Explicit {
                 label: (_, ref name),
                 ref params,
                 ref return_ann,
                 ref term,
-            } => {
-                let expr =
-                    desugar_fun_intro(&env, params, return_ann.as_ref().map(<_>::as_ref), term)?;
-                let free_var = env.on_binding(name);
-                Ok((Label(name.clone()), Binder(free_var), Embed(expr)))
-            },
+            } => Ok((
+                Label(name.clone()),
+                desugar_fun_intro(env, params, return_ann.as_ref().map(<_>::as_ref), term)?,
+            )),
         })
         .collect::<Result<Vec<_>, _>>()?;
 
-    Ok(raw::RcTerm::from(raw::Term::RecordIntro(
-        span,
-        Scope::new(Nest::new(fields), ()),
-    )))
+    Ok(raw::RcTerm::from(raw::Term::RecordIntro(span, fields)))
 }
 
 impl Desugar<raw::Literal> for concrete::Literal {

crates/pikelet-elaborate/src/context.rs → crates/pikelet-concrete/src/elaborate/context.rs

@@ -1,11 +1,13 @@
 use im;
 use moniker::{Binder, FreeVar, Var};
-use std::fmt;
 use std::rc::Rc;
 
-use pikelet_syntax::core::{Literal, RcTerm, RcType, RcValue, Value};
-use pikelet_syntax::translation::{Resugar, ResugarEnv};
-use pikelet_syntax::{FloatFormat, IntFormat};
+use pikelet_core::nbe;
+use pikelet_core::syntax::core::RcTerm;
+use pikelet_core::syntax::domain::{RcType, RcValue, Value};
+use pikelet_core::syntax::{Import, Literal};
+
+use resugar::{Resugar, ResugarEnv};
 
 // Some helper traits for marshalling between Rust and Pikelet values
 //
@@ -28,32 +30,21 @@ macro_rules! impl_into_value {
             }
         }
     };
-    ($T:ty, $ty:ident, $Variant:ident, $format:expr) => {
-        impl IntoValue for $T {
-            fn ty(context: &Context) -> RcType {
-                context.$ty().clone()
-            }
-
-            fn into_value(self) -> RcValue {
-                RcValue::from(Value::Literal(Literal::$Variant(self, $format)))
-            }
-        }
-    };
 }
 
 impl_into_value!(String, string, String);
 impl_into_value!(char, char, Char);
 impl_into_value!(bool, bool, Bool);
-impl_into_value!(u8, u8, U8, IntFormat::Dec);
-impl_into_value!(u16, u16, U16, IntFormat::Dec);
-impl_into_value!(u32, u32, U32, IntFormat::Dec);
-impl_into_value!(u64, u64, U64, IntFormat::Dec);
-impl_into_value!(i8, s8, S8, IntFormat::Dec);
-impl_into_value!(i16, s16, S16, IntFormat::Dec);
-impl_into_value!(i32, s32, S32, IntFormat::Dec);
-impl_into_value!(i64, s64, S64, IntFormat::Dec);
-impl_into_value!(f32, f32, F32, FloatFormat::Dec);
-impl_into_value!(f64, f64, F64, FloatFormat::Dec);
+impl_into_value!(u8, u8, U8);
+impl_into_value!(u16, u16, U16);
+impl_into_value!(u32, u32, U32);
+impl_into_value!(u64, u64, U64);
+impl_into_value!(i8, s8, S8);
+impl_into_value!(i16, s16, S16);
+impl_into_value!(i32, s32, S32);
+impl_into_value!(i64, s64, S64);
+impl_into_value!(f32, f32, F32);
+impl_into_value!(f64, f64, F64);
 
 trait TryFromValueRef {
     fn try_from_value_ref(src: &Value) -> Option<&Self>;
@@ -89,7 +80,7 @@ impl TryFromValueRef for bool {
 impl TryFromValueRef for u8 {
     fn try_from_value_ref(src: &Value) -> Option<&Self> {
         match *src {
-            Value::Literal(Literal::U8(ref val, _)) => Some(val),
+            Value::Literal(Literal::U8(ref val)) => Some(val),
             _ => None,
         }
     }
@@ -98,7 +89,7 @@ impl TryFromValueRef for u8 {
 impl TryFromValueRef for u16 {
     fn try_from_value_ref(src: &Value) -> Option<&Self> {
         match *src {
-            Value::Literal(Literal::U16(ref val, _)) => Some(val),
+            Value::Literal(Literal::U16(ref val)) => Some(val),
             _ => None,
         }
     }
@@ -107,7 +98,7 @@ impl TryFromValueRef for u16 {
 impl TryFromValueRef for u32 {
     fn try_from_value_ref(src: &Value) -> Option<&Self> {
         match *src {
-            Value::Literal(Literal::U32(ref val, _)) => Some(val),
+            Value::Literal(Literal::U32(ref val)) => Some(val),
             _ => None,
         }
     }
@@ -116,7 +107,7 @@ impl TryFromValueRef for u32 {
 impl TryFromValueRef for u64 {
     fn try_from_value_ref(src: &Value) -> Option<&Self> {
         match *src {
-            Value::Literal(Literal::U64(ref val, _)) => Some(val),
+            Value::Literal(Literal::U64(ref val)) => Some(val),
             _ => None,
         }
     }
@@ -125,7 +116,7 @@ impl TryFromValueRef for u64 {
 impl TryFromValueRef for i8 {
     fn try_from_value_ref(src: &Value) -> Option<&Self> {
         match *src {
-            Value::Literal(Literal::S8(ref val, _)) => Some(val),
+            Value::Literal(Literal::S8(ref val)) => Some(val),
             _ => None,
         }
     }
@@ -134,7 +125,7 @@ impl TryFromValueRef for i8 {
 impl TryFromValueRef for i16 {
     fn try_from_value_ref(src: &Value) -> Option<&Self> {
         match *src {
-            Value::Literal(Literal::S16(ref val, _)) => Some(val),
+            Value::Literal(Literal::S16(ref val)) => Some(val),
             _ => None,
         }
     }
@@ -143,7 +134,7 @@ impl TryFromValueRef for i16 {
 impl TryFromValueRef for i32 {
     fn try_from_value_ref(src: &Value) -> Option<&Self> {
         match *src {
-            Value::Literal(Literal::S32(ref val, _)) => Some(val),
+            Value::Literal(Literal::S32(ref val)) => Some(val),
             _ => None,
         }
     }
@@ -152,7 +143,7 @@ impl TryFromValueRef for i32 {
 impl TryFromValueRef for i64 {
     fn try_from_value_ref(src: &Value) -> Option<&Self> {
         match *src {
-            Value::Literal(Literal::S64(ref val, _)) => Some(val),
+            Value::Literal(Literal::S64(ref val)) => Some(val),
             _ => None,
         }
     }
@@ -161,7 +152,7 @@ impl TryFromValueRef for i64 {
 impl TryFromValueRef for f32 {
     fn try_from_value_ref(src: &Value) -> Option<&Self> {
         match *src {
-            Value::Literal(Literal::F32(ref val, _)) => Some(val),
+            Value::Literal(Literal::F32(ref val)) => Some(val),
             _ => None,
         }
     }
@@ -170,28 +161,12 @@ impl TryFromValueRef for f32 {
 impl TryFromValueRef for f64 {
     fn try_from_value_ref(src: &Value) -> Option<&Self> {
         match *src {
-            Value::Literal(Literal::F64(ref val, _)) => Some(val),
+            Value::Literal(Literal::F64(ref val)) => Some(val),
             _ => None,
         }
     }
 }
 
-/// Imported definitions
-#[derive(Clone)]
-pub enum Import {
-    Term(RcTerm),
-    Prim(for<'a> fn(&'a [RcValue]) -> Option<RcValue>),
-}
-
-impl fmt::Debug for Import {
-    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
-        match *self {
-            Import::Term(ref term) => f.debug_tuple("Term").field(term).finish(),
-            Import::Prim(_) => f.debug_tuple("Prim").field(&"|params| { .. }").finish(),
-        }
-    }
-}
-
 #[derive(Clone, Debug)]
 pub struct Globals {
     ty_bool: RcType,
@@ -239,7 +214,7 @@ impl Default for Context {
     fn default() -> Context {
         use moniker::{Embed, Scope};
 
-        use pikelet_syntax::core::Term;
+        use pikelet_core::syntax::core::Term;
 
         let var_bool = FreeVar::fresh_named("Bool");
         let var_true = FreeVar::fresh_named("true");
@@ -553,14 +528,14 @@ impl Context {
     }
 
     pub fn array<'a>(&self, ty: &'a RcType) -> Option<(u64, &'a RcType)> {
-        use pikelet_syntax::LevelShift;
+        use pikelet_core::syntax::LevelShift;
 
         match ty.free_var_app() {
             // Conservatively forcing the shift to be zero for now. Perhaps this
             // could be relaxed in the future if it becomes a problem?
             Some((fv, LevelShift(0), &[ref len, ref elem_ty])) if *fv == self.globals.var_array => {
                 match **len {
-                    Value::Literal(Literal::U64(len, _)) => Some((len, elem_ty)),
+                    Value::Literal(Literal::U64(len)) => Some((len, elem_ty)),
                     _ => None,
                 }
             },
@@ -594,3 +569,13 @@ impl Context {
         self.definitions.insert(free_var, term);
     }
 }
+
+impl nbe::Env for Context {
+    fn get_import(&self, name: &str) -> Option<&Import> {
+        self.imports.get(name).map(|&(ref import, _)| import)
+    }
+
+    fn get_definition(&self, free_var: &FreeVar<String>) -> Option<&RcTerm> {
+        self.definitions.get(free_var)
+    }
+}