Skip to content

Commit

Permalink
Clean up matching against globals
Browse files Browse the repository at this point in the history
  • Loading branch information
@brendanzab
brendanzab committed Nov 10, 2020
1 parent 2a0dea6 commit 543c4d3
Show file tree
Hide file tree
Showing 4 changed files with 115 additions and 142 deletions.
1 change: 0 additions & 1 deletion pikelet/src/lang/core.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -134,7 +134,6 @@ pub enum TermData {

/// Ordered sequences.
SequenceTerm(Vec<Arc<Term>>),

/// Constants.
Constant(Constant),

Expand Down
10 changes: 10 additions & 0 deletions pikelet/src/lang/core/semantics.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -85,6 +85,16 @@ impl Value {
Value::Stuck(Head::Local(level.into()), Vec::new())
}

/// Attempt to match against a stuck global.
pub fn try_global(&self) -> Option<(&str, UniverseOffset, &[Elim])> {
match self {
Value::Stuck(Head::Global(name, universe_offset), elims) => {
Some((name, *universe_offset, elims))
}
_ => None,
}
}

/// Force any unstuck values.
pub fn force(&self, globals: &Globals) -> &Value {
match self {
Expand Down
54 changes: 24 additions & 30 deletions pikelet/src/lang/core/typing.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ use contracts::debug_ensures;
use crossbeam_channel::Sender;
use std::sync::Arc;

use crate::lang::core::semantics::{self, Elim, Head, RecordClosure, Unfold, Value};
use crate::lang::core::semantics::{self, Elim, RecordClosure, Unfold, Value};
use crate::lang::core::{
Constant, Globals, LocalLevel, Locals, Term, TermData, UniverseLevel, UniverseOffset,
};
Expand Down Expand Up @@ -198,39 +198,33 @@ impl<'me> State<'me> {
}
}

(TermData::SequenceTerm(entry_terms), Value::Stuck(Head::Global(name, _), spine)) => {
match (name.as_ref(), spine.as_slice()) {
("Array", [Elim::Function(len), Elim::Function(entry_type)]) => {
let entry_type = entry_type.force(self.globals);
for entry_term in entry_terms {
self.check_type(entry_term, entry_type);
}

match len.force(self.globals).as_ref() {
Value::Constant(Constant::U32(len))
if *len as usize == entry_terms.len() => {}
len => self.report(CoreTypingMessage::MismatchedSequenceLength {
found_len: entry_terms.len(),
expected_len: self.read_back_value(len),
}),
}
(TermData::SequenceTerm(entry_terms), forced_type) => match forced_type.try_global() {
Some(("Array", _, [Elim::Function(len), Elim::Function(entry_type)])) => {
let entry_type = entry_type.force(self.globals);
for entry_term in entry_terms {
self.check_type(entry_term, entry_type);
}
("List", [Elim::Function(entry_type)]) => {
let entry_type = entry_type.force(self.globals);
for entry_term in entry_terms {
self.check_type(entry_term, entry_type);
}

match len.force(self.globals).as_ref() {
Value::Constant(Constant::U32(len))
if *len as usize == entry_terms.len() => {}
len => self.report(CoreTypingMessage::MismatchedSequenceLength {
found_len: entry_terms.len(),
expected_len: self.read_back_value(len),
}),
}
_ => {
let expected_type = self.read_back_value(expected_type);
self.report(CoreTypingMessage::NoSequenceConversion { expected_type })
}
Some(("List", _, [Elim::Function(entry_type)])) => {
let entry_type = entry_type.force(self.globals);
for entry_term in entry_terms {
self.check_type(entry_term, entry_type);
}
}
}
(TermData::SequenceTerm(_), _) => {
let expected_type = self.read_back_value(expected_type);
self.report(CoreTypingMessage::NoSequenceConversion { expected_type })
}
Some(_) | None => {
let expected_type = self.read_back_value(expected_type);
self.report(CoreTypingMessage::NoSequenceConversion { expected_type })
}
},

(_, _) => match self.synth_type(term) {
found_type if self.is_subtype(&found_type, expected_type) => {}
Expand Down
192 changes: 81 additions & 111 deletions pikelet/src/pass/surface_to_core.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ use std::ops::Range;
use std::sync::Arc;

use crate::lang::core;
use crate::lang::core::semantics::{self, Elim, Head, RecordClosure, Unfold, Value};
use crate::lang::core::semantics::{self, Elim, RecordClosure, Unfold, Value};
use crate::lang::surface::{Term, TermData};
use crate::literal;
use crate::pass::core_to_surface;
Expand Down Expand Up @@ -310,111 +310,69 @@ impl<'me> State<'me> {
)
}

(TermData::SequenceTerm(entry_terms), Value::Stuck(Head::Global(name, _), spine)) => {
match (name.as_ref(), spine.as_slice()) {
("Array", [Elim::Function(len), Elim::Function(core_entry_type)]) => {
let core_entry_type = core_entry_type.force(self.globals);
let core_entry_terms = entry_terms
.iter()
.map(|entry_term| {
Arc::new(self.check_type(entry_term, core_entry_type))
})
.collect();

let len = len.force(self.globals);
match len.as_ref() {
Value::Constant(core::Constant::U32(len))
if *len as usize == entry_terms.len() =>
{
core::Term::new(
term.range(),
core::TermData::SequenceTerm(core_entry_terms),
)
}
Value::Error => core::Term::new(term.range(), core::TermData::Error),
_ => {
let expected_len = self.read_back_to_surface_term(&len);
self.report(SurfaceToCoreMessage::MismatchedSequenceLength {
range: term.range(),
found_len: entry_terms.len(),
expected_len,
});
core::Term::new(term.range(), core::TermData::Error)
}
(TermData::SequenceTerm(entry_terms), forced_type) => match forced_type.try_global() {
Some(("Array", _, [Elim::Function(len), Elim::Function(core_entry_type)])) => {
let core_entry_type = core_entry_type.force(self.globals);
let core_entry_terms = entry_terms
.iter()
.map(|entry_term| Arc::new(self.check_type(entry_term, core_entry_type)))
.collect();

let len = len.force(self.globals);
match len.as_ref() {
Value::Constant(core::Constant::U32(len))
if *len as usize == entry_terms.len() =>
{
core::Term::new(
term.range(),
core::TermData::SequenceTerm(core_entry_terms),
)
}
Value::Error => core::Term::new(term.range(), core::TermData::Error),
_ => {
let expected_len = self.read_back_to_surface_term(&len);
self.report(SurfaceToCoreMessage::MismatchedSequenceLength {
range: term.range(),
found_len: entry_terms.len(),
expected_len,
});
core::Term::new(term.range(), core::TermData::Error)
}
}
("List", [Elim::Function(core_entry_type)]) => {
let core_entry_type = core_entry_type.force(self.globals);
let core_entry_terms = entry_terms
.iter()
.map(|entry_term| {
Arc::new(self.check_type(entry_term, core_entry_type))
})
.collect();

core::Term::new(
term.range(),
core::TermData::SequenceTerm(core_entry_terms),
)
}
_ => {
let expected_type = self.read_back_to_surface_term(expected_type);
self.report(SurfaceToCoreMessage::NoSequenceConversion {
range: term.range(),
expected_type,
});
core::Term::new(term.range(), core::TermData::Error)
}
}
}
(TermData::SequenceTerm(_), _) => {
let expected_type = self.read_back_to_surface_term(expected_type);
self.report(SurfaceToCoreMessage::NoSequenceConversion {
range: term.range(),
expected_type,
});
core::Term::new(term.range(), core::TermData::Error)
}

(TermData::NumberTerm(data), Value::Stuck(Head::Global(name, _), spine)) => {
match (name.as_ref(), spine.as_slice()) {
("U8", []) => self.parse_unsigned(term.range(), data, core::Constant::U8),
("U16", []) => self.parse_unsigned(term.range(), data, core::Constant::U16),
("U32", []) => self.parse_unsigned(term.range(), data, core::Constant::U32),
("U64", []) => self.parse_unsigned(term.range(), data, core::Constant::U64),
("S8", []) => self.parse_signed(term.range(), data, core::Constant::S8),
("S16", []) => self.parse_signed(term.range(), data, core::Constant::S16),
("S32", []) => self.parse_signed(term.range(), data, core::Constant::S32),
("S64", []) => self.parse_signed(term.range(), data, core::Constant::S64),
("F32", []) => self.parse_float(term.range(), data, core::Constant::F32),
("F64", []) => self.parse_float(term.range(), data, core::Constant::F64),
(_, _) => {
let expected_type = self.read_back_to_surface_term(expected_type);
self.report(SurfaceToCoreMessage::NoLiteralConversion {
range: term.range(),
expected_type,
});
core::Term::new(term.range(), core::TermData::Error)
}
Some(("List", _, [Elim::Function(core_entry_type)])) => {
let core_entry_type = core_entry_type.force(self.globals);
let core_entry_terms = entry_terms
.iter()
.map(|entry_term| Arc::new(self.check_type(entry_term, core_entry_type)))
.collect();

core::Term::new(term.range(), core::TermData::SequenceTerm(core_entry_terms))
}
}
(TermData::CharTerm(data), Value::Stuck(Head::Global(name, _), spine)) => {
match (name.as_ref(), spine.as_slice()) {
("Char", []) => self.parse_char(term.range(), data),
(_, _) => {
let expected_type = self.read_back_to_surface_term(expected_type);
self.report(SurfaceToCoreMessage::NoLiteralConversion {
range: term.range(),
expected_type,
});
core::Term::new(term.range(), core::TermData::Error)
}
Some(_) | None => {
let expected_type = self.read_back_to_surface_term(expected_type);
self.report(SurfaceToCoreMessage::NoSequenceConversion {
range: term.range(),
expected_type,
});
core::Term::new(term.range(), core::TermData::Error)
}
}
(TermData::StringTerm(data), Value::Stuck(Head::Global(name, _), spine)) => {
match (name.as_ref(), spine.as_slice()) {
("String", []) => self.parse_string(term.range(), data),
(_, _) => {
},
(TermData::NumberTerm(data), forced_type) => {
use crate::lang::core::Constant::*;

match forced_type.try_global() {
Some(("U8", _, [])) => self.parse_unsigned(term.range(), data, U8),
Some(("U16", _, [])) => self.parse_unsigned(term.range(), data, U16),
Some(("U32", _, [])) => self.parse_unsigned(term.range(), data, U32),
Some(("U64", _, [])) => self.parse_unsigned(term.range(), data, U64),
Some(("S8", _, [])) => self.parse_signed(term.range(), data, S8),
Some(("S16", _, [])) => self.parse_signed(term.range(), data, S16),
Some(("S32", _, [])) => self.parse_signed(term.range(), data, S32),
Some(("S64", _, [])) => self.parse_signed(term.range(), data, S64),
Some(("F32", _, [])) => self.parse_float(term.range(), data, F32),
Some(("F64", _, [])) => self.parse_float(term.range(), data, F64),
Some(_) | None => {
let expected_type = self.read_back_to_surface_term(expected_type);
self.report(SurfaceToCoreMessage::NoLiteralConversion {
range: term.range(),
Expand All @@ -424,16 +382,28 @@ impl<'me> State<'me> {
}
}
}
(TermData::NumberTerm(_), _)
| (TermData::CharTerm(_), _)
| (TermData::StringTerm(_), _) => {
let expected_type = self.read_back_to_surface_term(expected_type);
self.report(SurfaceToCoreMessage::NoLiteralConversion {
range: term.range(),
expected_type,
});
core::Term::new(term.range(), core::TermData::Error)
}
(TermData::CharTerm(data), forced_type) => match forced_type.try_global() {
Some(("Char", _, [])) => self.parse_char(term.range(), data),
Some(_) | None => {
let expected_type = self.read_back_to_surface_term(expected_type);
self.report(SurfaceToCoreMessage::NoLiteralConversion {
range: term.range(),
expected_type,
});
core::Term::new(term.range(), core::TermData::Error)
}
},
(TermData::StringTerm(data), forced_type) => match forced_type.try_global() {
Some(("String", _, [])) => self.parse_string(term.range(), data),
Some(_) | None => {
let expected_type = self.read_back_to_surface_term(expected_type);
self.report(SurfaceToCoreMessage::NoLiteralConversion {
range: term.range(),
expected_type,
});
core::Term::new(term.range(), core::TermData::Error)
}
},

(_, _) => match self.synth_type(term) {
(term, found_type) if self.is_subtype(&found_type, expected_type) => term,
Expand Down

0 comments on commit 543c4d3

Please sign in to comment.