Skip to content

Commit

Permalink
Merge pull request #143 from ch-systems/alex/specific-type-formalization
Browse files Browse the repository at this point in the history 
Specific Type Formalization
  • Loading branch information
@sezna
sezna authored Aug 3, 2024
2 parents c39db92 + b942dbf commit e4b9cd0
Show file tree
Hide file tree
Showing 14 changed files with 2,934 additions and 2,101 deletions.
15 changes: 12 additions & 3 deletions petr-cli/src/main.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,8 @@ pub mod error {
Pkg(#[from] petr_pkg::error::PkgError),
#[error("Failed to lower code")]
FailedToLower,
#[error("Program contained type errors")]
FailedToTypeCheck,
}
}

Expand Down Expand Up @@ -220,12 +222,20 @@ pub fn compile(

timings.start("type check");
// type check
let (type_errs, type_checker) = petr_typecheck::type_check(resolved);
let res = petr_typecheck::type_check(resolved);

timings.end("type check");
let type_solution = match res {
Ok(o) => o,
Err(e) => {
render_errors(parse_errs, &source_map);
render_errors(e, &source_map);
return Err(PeteError::FailedToTypeCheck);
},
};

timings.start("lowering");
let lowerer: Lowerer = match Lowerer::new(type_checker) {
let lowerer: Lowerer = match Lowerer::new(type_solution) {
Ok(l) => l,
Err(e) => {
eprintln!("Failed to lower: {:?}", e);
Expand All @@ -235,7 +245,6 @@ pub fn compile(
timings.end("lowering");

render_errors(parse_errs, &source_map);
render_errors(type_errs, &source_map);
render_errors(resolution_errs, &source_map);
Ok(lowerer)
}
Expand Down
8 changes: 6 additions & 2 deletions petr-fmt/src/tests.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -636,10 +636,14 @@ fn let_bindings_no_trailing_comma() {

#[test]
fn sum_ty_formatting() {
check(Default::default(), "fn myFunc(x in 'sum 1 | 2 | 3) returns 'int 5", expect![[r#"
check(
Default::default(),
"fn myFunc(x in 'sum 1 | 2 | 3) returns 'int 5",
expect![[r#"
fn myFunc(
x ∈ 'Σ 1 | 2 | 3,
) → 'int
5
"#]])
"#]],
)
}
53 changes: 29 additions & 24 deletions petr-ir/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@

use std::{collections::BTreeMap, rc::Rc};

use petr_typecheck::{FunctionSignature, SpecificType, Type, TypeChecker, TypeVariable, TypedExpr, TypedExprKind};
use petr_typecheck::{FunctionSignature, SpecificType, TypeSolution, TypeVariable, TypedExpr, TypedExprKind};
use petr_utils::{idx_map_key, Identifier, IndexMap, SpannedItem, SymbolId};

mod error;
Expand All @@ -19,8 +19,8 @@ pub use error::LoweringError;
use opcodes::*;
pub use opcodes::{DataLabel, Intrinsic, IrOpcode, LabelId, Reg, ReservedRegister};

pub fn lower(checker: TypeChecker) -> Result<(DataSection, Vec<IrOpcode>)> {
let lowerer = Lowerer::new(checker)?;
pub fn lower(solution: TypeSolution) -> Result<(DataSection, Vec<IrOpcode>)> {
let lowerer = Lowerer::new(solution)?;
Ok(lowerer.finalize())
}

Expand All @@ -38,7 +38,7 @@ pub struct Lowerer {
data_section: DataSection,
entry_point: Option<MonomorphizedFunctionId>,
reg_assigner: usize,
type_checker: TypeChecker,
type_solution: TypeSolution,
variables_in_scope: Vec<BTreeMap<SymbolId, Reg>>,
monomorphized_functions: IndexMap<MonomorphizedFunctionId, (FunctionSignature, Function)>,
errors: Vec<SpannedItem<LoweringError>>,
Expand All @@ -53,16 +53,16 @@ pub enum DataSectionEntry {
}

impl Lowerer {
pub fn new(type_checker: TypeChecker) -> Result<Self> {
pub fn new(type_solution: petr_typecheck::TypeSolution) -> Result<Self> {
// if there is an entry point, set that
// set entry point to func named main
let entry_point = type_checker.get_main_function();
let entry_point = type_solution.get_main_function().map(|(a, b)| (*a, b.clone()));

let mut lowerer = Self {
data_section: IndexMap::default(),
entry_point: None,
reg_assigner: 0,
type_checker,
type_solution,
variables_in_scope: Default::default(),
monomorphized_functions: Default::default(),
label_assigner: 0,
Expand Down Expand Up @@ -110,7 +110,7 @@ impl Lowerer {
return Ok(previously_monomorphized_definition.0);
}

let func_def = self.type_checker.get_monomorphized_function(&func).clone();
let func_def = self.type_solution.get_monomorphized_function(&func).clone();

let mut buf = vec![];
self.with_variable_context(|ctx| -> Result<_> {
Expand Down Expand Up @@ -181,8 +181,8 @@ impl Lowerer {
for (arg_name, arg_expr) in args {
let reg = self.fresh_reg();
let mut expr = self.lower_expr(arg_expr, ReturnDestination::Reg(reg))?;
let arg_ty = self.type_checker.expr_ty(arg_expr);
let petr_ty = self.type_checker.look_up_variable(arg_ty);
let arg_ty = self.type_solution.expr_ty(arg_expr);
let petr_ty = self.type_solution.get_latest_type(arg_ty);
arg_types.push((*arg_name, petr_ty.clone()));
let ir_ty = self.lower_type(petr_ty.clone());
expr.push(IrOpcode::StackPush(TypedReg { ty: ir_ty, reg }));
Expand All @@ -192,7 +192,7 @@ impl Lowerer {
// push current PC onto the stack
buf.push(IrOpcode::PushPc());

let arg_petr_types = arg_types.iter().map(|(_name, ty)| ty.generalize(self.type_checker.ctx())).collect();
let arg_petr_types = arg_types.iter().map(|(_name, ty)| self.type_solution.generalize(ty)).collect();

let monomorphized_func_id = self.monomorphize_function((*func, arg_petr_types))?;

Expand All @@ -215,7 +215,7 @@ impl Lowerer {
List { elements, .. } => {
let size_of_each_elements = elements
.iter()
.map(|el| self.to_ir_type(self.type_checker.expr_ty(el)).size().num_bytes() as u64)
.map(|el| self.to_ir_type(self.type_solution.expr_ty(el)).size().num_bytes() as u64)
.sum::<u64>();
let size_of_list = size_of_each_elements * elements.len() as u64;
let size_of_list_reg = self.fresh_reg();
Expand All @@ -235,7 +235,7 @@ impl Lowerer {
buf.push(IrOpcode::LoadImmediate(current_offset_reg, current_offset));
buf.push(IrOpcode::Add(current_offset_reg, current_offset_reg, return_reg));
buf.push(IrOpcode::WriteRegisterToMemory(reg, current_offset_reg));
current_offset += self.to_ir_type(self.type_checker.expr_ty(el)).size().num_bytes() as u64;
current_offset += self.to_ir_type(self.type_solution.expr_ty(el)).size().num_bytes() as u64;
}
Ok(buf)
},
Expand Down Expand Up @@ -291,7 +291,7 @@ impl Lowerer {
buf.push(IrOpcode::Add(current_size_offset_reg, current_size_offset_reg, return_destination));
buf.push(IrOpcode::WriteRegisterToMemory(reg, current_size_offset_reg));

let arg_ty = self.type_checker.expr_ty(arg);
let arg_ty = self.type_solution.expr_ty(arg);

current_size_offset += self.to_ir_type(arg_ty).size().num_bytes() as u64;
}
Expand Down Expand Up @@ -345,7 +345,7 @@ impl Lowerer {
// Generalize the type. These general types are much more useful for codegen.
// Specific types include extra information about constant literal value types,
// data flow analysis, effects tracking, etc., that codegen does not care about.
let ty = ty.generalize(self.type_checker.ctx());
let ty = self.type_solution.generalize(&ty.as_specific_ty());
use petr_typecheck::GeneralType::*;
match ty {
Unit => IrTy::Unit,
Expand Down Expand Up @@ -406,7 +406,7 @@ impl Lowerer {
&mut self,
param_ty: TypeVariable,
) -> IrTy {
let ty = self.type_checker.look_up_variable(param_ty).clone();
let ty = self.type_solution.get_latest_type(param_ty).clone();
self.lower_type(ty)
}

Expand Down Expand Up @@ -450,7 +450,7 @@ impl Lowerer {
Ok(buf)
},
SizeOf(expr) => {
let ty = self.type_checker.expr_ty(expr);
let ty = self.type_solution.expr_ty(expr);
let size = self.to_ir_type(ty).size();
match return_destination {
ReturnDestination::Reg(reg) => {
Expand Down Expand Up @@ -582,6 +582,7 @@ mod tests {

use expect_test::{expect, Expect};
use petr_resolve::resolve_symbols;
use petr_typecheck::TypeChecker;
use petr_utils::render_error;

use super::*;
Expand All @@ -606,15 +607,19 @@ mod tests {
}
panic!("resolving names failed");
}
let type_checker = TypeChecker::new(resolved);
let mut type_checker = TypeChecker::new(resolved);

let typecheck_errors = type_checker.errors();
if !typecheck_errors.is_empty() {
typecheck_errors.iter().for_each(|err| eprintln!("{:?}", err));
panic!("ir gen failed: code didn't typecheck");
}
type_checker.fully_type_check();

let solution = match type_checker.into_solution() {
Ok(o) => o,
Err(errs) => {
errs.iter().for_each(|err| eprintln!("{:?}", err));
panic!("ir gen failed: code didn't typecheck");
},
};

let lowerer = match Lowerer::new(type_checker) {
let lowerer = match Lowerer::new(solution) {
Ok(lowerer) => lowerer,
Err(err) => {
eprintln!("{:?}", err);
Expand Down
2 changes: 2 additions & 0 deletions petr-playground/index.js
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ monaco.languages.setMonarchTokensProvider("petr", {
[/\@[a-zA-Z_]+/, "intrinsic"],
[/[0-9]+/, "integer-literal"],
[/\".*\"/, "string-literal"],
[/\{-.*-\}/, "comment"],
],
},
});
Expand Down Expand Up @@ -52,6 +53,7 @@ monaco.editor.defineTheme("petr-theme", {
{ token: "string-literal", foreground: literalColor },
{ token: "integer-literal", foreground: literalColor },
{ token: "keyword", foreground: literalColor },
{ token: "comment", foreground: "C4A484", fontStyle: "italic"},
],
colors: {
"editor.foreground": "#ffffff",
Expand Down
9 changes: 7 additions & 2 deletions petr-playground/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,13 +74,18 @@ fn compile_snippet(input: String) -> Result<Lowerer, Vec<String>> {
return Err(errs.into_iter().map(|err| format!("{:?}", render_error(&source_map, err))).collect());
}

let (errs, type_checker) = type_check(resolved);
let solution = match type_check(resolved) {
Ok(o) => o,
Err(e) => {
return Err(e.into_iter().map(|err| format!("{:?}", render_error(&source_map, err))).collect());
},
};

if !errs.is_empty() {
return Err(errs.into_iter().map(|err| format!("{:?}", render_error(&source_map, err))).collect());
}

let lowerer = match Lowerer::new(type_checker) {
let lowerer = match Lowerer::new(solution) {
Ok(l) => l,
Err(err) => panic!("lowering failed: {:?}", err),
};
Expand Down
Loading

0 comments on commit e4b9cd0

Please sign in to comment.