use crate::ast::branded::{Ast, BText, CmdArg, IText, MathElem, Pattern};
use crate::elaborate::{Program, UserSynonymDecl, UserTypeDecl};
pub use crate::exhaustive::MatchWarning;
use crate::prim_types::{
self, arrow, builtin_variants_with_version, labeled, list, mandatory, optional, product, reff,
t_block_boxes, t_block_text, t_bool, t_context, t_deco, t_decoset, t_document, t_float,
t_font_key, t_graphics, t_image, t_inline_boxes, t_inline_text, t_int, t_length, t_math_boxes,
t_math_text, t_option, t_paren, t_path, t_prepath, t_string, t_unit, VariantDecl,
};
use crate::symbol::{Symbol, SymbolStore};
use crate::types::{
self, generalize, instantiate, resolve, resolve_row, BaseType, CmdArgType, Kind, MonoType,
PolyType, Row, Stage, TypeContext,
};
use crate::unify::{unify, UnifyError};
use rustyfi_syntax::cst::ast::{CmdTypeKind, TypeApp, TypeAtom, TypeExpr, TypeProd};
use rustyfi_syntax::cst::{RecordKind, SigConstraint, SigItem};
use rustyfi_syntax::span::Span;
use rustyfi_syntax::RustyfiVersion;
use std::collections::{BTreeSet, HashMap};
use std::fmt;
use std::rc::Rc;
#[derive(Debug)]
pub struct TypeError {
pub span: Option<Span>,
pub message: String,
pub source: Option<UnifyError>,
}
impl TypeError {
fn from_unify(span: Option<Span>, what: impl Into<String>, source: UnifyError) -> TypeError {
TypeError {
span,
message: format!("while typing {}", what.into()),
source: Some(source),
}
}
fn simple(span: Option<Span>, message: impl Into<String>) -> TypeError {
TypeError {
span,
message: message.into(),
source: None,
}
}
}
impl fmt::Display for TypeError {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self.span {
Some(span) => write!(f, "{span}: {}", self.message)?,
None => write!(f, "{}", self.message)?,
}
if let Some(src) = &self.source {
write!(f, ": {src}")?;
}
Ok(())
}
}
impl std::error::Error for TypeError {
fn source<'s>(&self) -> Option<&(dyn std::error::Error + 'static)> {
self.source
.as_ref()
.map(|e| e as &(dyn std::error::Error + 'static))
}
}
pub const PRIMITIVE_NAMES: &[&str] = &[
"read-inline",
"read-block",
"line-break",
"page-break",
"page-break-multicolumn",
"page-break-two-column",
"+",
"-",
"*",
"/",
"mod",
"==",
"<>",
"<",
">",
"<=",
">=",
"&&",
"||",
"not",
"+.",
"-.",
"*.",
"/.",
"float",
"round",
"+'",
"-'",
"*'",
"/'",
"<'",
">'",
"^",
"arabic",
"string-same",
"::",
"!",
"string-length",
"string-sub",
"string-explode",
"regexp-of-string",
"string-match",
"string-scan",
"split-on-regexp",
"embed-string",
"inline-fil",
"set-font-size",
"get-font-size",
"set-leading",
"set-paragraph-margin",
"get-text-width",
"get-initial-context",
"++",
"+++",
"inline-nil",
"block-nil",
"inline-skip",
"inline-glue",
"block-skip",
"list-mark",
"inline-mark",
"set-font-key",
"load-single-font",
"sin",
"asin",
"cos",
"acos",
"tan",
"atan",
"atan2",
"log",
"exp",
"ceil",
"floor",
"show-float",
"string-byte-length",
"string-sub-bytes",
"string-unexplode",
"display-message",
"abort-with-message",
"load-image",
"load-pdf-image",
"use-image-by-width",
"start-path",
"line-to",
"terminate-path",
"close-with-line",
"fill",
"stroke",
"inline-graphics",
"tabular",
"inline-graphics-outer",
"bezier-to",
"close-with-bezier",
"shift-path",
"linear-transform-path",
"shift-graphics",
"linear-transform-graphics",
"get-graphics-bbox",
"get-path-bbox",
"dashed-stroke",
"draw-text",
"get-natural-metrics",
"inline-frame-outer",
"inline-frame-inner",
"set-manual-rising",
"script-guard",
"discretionary",
"get-axis-height",
"hook-page-break",
"hook-page-break-block",
"register-cross-reference",
"get-cross-reference",
"probe-cross-reference",
"get-leftmost-script",
"get-rightmost-script",
"inline-frame-breakable",
"register-destination",
"register-link-to-uri",
"register-link-to-location",
"math-char",
"math-big-char",
"math-char-with-kern",
"math-big-char-with-kern",
"math-concat",
"math-group",
"math-sup",
"math-sub",
"math-frac",
"math-radical",
"math-lower",
"math-upper",
"math-pull-in-scripts",
"math-color",
"math-char-class",
"math-variant-char",
"set-math-variant-char",
"get-left-math-class",
"get-right-math-class",
"math-paren",
"math-paren-with-middle",
"text-in-math",
"convert-string-for-math",
"embed-math",
"set-math-command",
"set-math-font",
"space-between-maths",
"raise-inline",
"embed-block-breakable",
"unite-path",
"set-min-gap-of-lines",
"omit-skip-after",
"set-text-color",
"get-text-color",
"set-hyphen-penalty",
"set-hyphen-min",
"set-space-ratio",
"set-space-ratio-between-scripts",
"split-into-lines",
"block-frame-breakable",
"embed-block-top",
"set-font",
"get-font",
"set-code-text-command",
"get-natural-length",
"set-dominant-wide-script",
"set-dominant-narrow-script",
"set-language",
"set-every-word-break",
"register-outline",
"extract-string",
"get-dominant-wide-script",
"get-dominant-narrow-script",
"get-language",
"get-initial-text-info",
"deepen-indent",
"break",
"embed-block-bottom",
"line-stack-bottom",
"line-stack-top",
"add-footnote",
"clear-page",
"read-math",
"stringify-math",
"set-math-char",
"set-math-char-class",
"get-math-char-class",
"embed-inline-to-math",
"get-math-axis-height-ratio",
"%math-attach-scripts",
"load-hyphenation-dictionary",
"load-unicode-char-database",
"set-hyphenation-dictionary",
"set-unicode-char-database",
"here",
"<<",
">>",
"band",
"bor",
"bxor",
"bnot",
"normalize-string-to-nfc",
"normalize-string-to-nfd",
"split-grapheme-cluster",
"read-file",
"register-document-information",
"unite-graphics",
"clip-graphics-by-path",
">.",
"<.",
">=.",
"<=.",
];
#[allow(dead_code)]
fn base_type_env<'s>(store: &'s SymbolStore) -> TypeEnv<'s> {
base_type_env_with_version(store, RustyfiVersion::V0_0)
}
pub(crate) fn base_type_env_with_version<'s>(
store: &'s SymbolStore,
version: RustyfiVersion,
) -> TypeEnv<'s> {
let mut env = TypeEnv::default();
for name in PRIMITIVE_NAMES {
if let Some(poly) = prim_types::primitive_type_with_version(name, version) {
env = env.with_primitive(store.intern(name), poly);
}
}
env
}
fn version_scoped_type_env<'s>(
store: &'s SymbolStore,
env: &TypeEnv<'s>,
version: RustyfiVersion,
) -> TypeEnv<'s> {
let mut e = env.clone();
for name in PRIMITIVE_NAMES {
let sym = store.intern(name);
if e.is_shadowed(sym) {
continue;
}
if let Some(poly) = prim_types::primitive_type_with_version(name, version) {
e = e.with_primitive(sym, poly);
}
}
e
}
const OVERLAY_CAP: usize = 64;
struct EnvEntry {
poly: PolyType,
stage: Stage,
}
#[derive(Clone, Default)]
pub(crate) struct TypeEnv<'s> {
base: std::rc::Rc<HashMap<Symbol<'s>, std::rc::Rc<EnvEntry>>>,
overlay: HashMap<Symbol<'s>, std::rc::Rc<EnvEntry>>,
base_shadowed: std::rc::Rc<std::collections::HashSet<Symbol<'s>>>,
overlay_shadowed: std::collections::HashSet<Symbol<'s>>,
}
impl<'s> TypeEnv<'s> {
fn maybe_promote(&mut self) {
if self.overlay.len() < OVERLAY_CAP {
return;
}
let mut base = (*self.base).clone();
for (k, v) in self.overlay.drain() {
base.insert(k, v);
}
self.base = std::rc::Rc::new(base);
if !self.overlay_shadowed.is_empty() {
let mut sh = (*self.base_shadowed).clone();
for k in self.overlay_shadowed.drain() {
sh.insert(k);
}
self.base_shadowed = std::rc::Rc::new(sh);
}
}
pub(crate) fn with(&self, name: Symbol<'s>, poly: PolyType, stage: Stage) -> TypeEnv<'s> {
let mut e = self.clone();
e.overlay_shadowed.insert(name);
e.overlay.insert(name, std::rc::Rc::new(EnvEntry { poly, stage }));
e.maybe_promote();
e
}
fn with_primitive(&self, name: Symbol<'s>, poly: PolyType) -> TypeEnv<'s> {
let mut e = self.clone();
e.overlay.insert(
name,
std::rc::Rc::new(EnvEntry {
poly,
stage: Stage::Persistent0,
}),
);
e.maybe_promote();
e
}
fn entry(&self, name: Symbol<'s>) -> Option<&EnvEntry> {
self.overlay
.get(&name)
.or_else(|| self.base.get(&name))
.map(|p| &**p)
}
fn is_shadowed(&self, name: Symbol<'s>) -> bool {
self.overlay_shadowed.contains(&name) || self.base_shadowed.contains(&name)
}
pub(crate) fn with_all(
&self,
schemes: Vec<(Symbol<'s>, PolyType)>,
stage: Stage,
) -> TypeEnv<'s> {
let mut e = self.clone();
for (name, poly) in schemes {
e.overlay_shadowed.insert(name);
e.overlay
.insert(name, std::rc::Rc::new(EnvEntry { poly, stage }));
e.maybe_promote();
}
e
}
#[allow(dead_code)]
pub(crate) fn without_all(&self, names: &[Symbol<'s>]) -> TypeEnv<'s> {
let mut vars: HashMap<Symbol<'s>, std::rc::Rc<EnvEntry>> = (*self.base).clone();
for (k, v) in &self.overlay {
vars.insert(*k, v.clone());
}
let mut sh = (*self.base_shadowed).clone();
sh.extend(self.overlay_shadowed.iter().copied());
for n in names {
vars.remove(n);
sh.remove(n);
}
TypeEnv {
base: std::rc::Rc::new(vars),
overlay: HashMap::new(),
base_shadowed: std::rc::Rc::new(sh),
overlay_shadowed: std::collections::HashSet::new(),
}
}
}
fn name_to_mono(name: &str, version: RustyfiVersion) -> MonoType {
match name {
"unit" => t_unit(),
"bool" => t_bool(),
"int" => t_int(),
"float" => t_float(),
"length" => t_length(),
"string" => t_string(),
"inline-text" => t_inline_text(),
"block-text" => t_block_text(),
"math" if !version.math_is_split() => MonoType::Base(BaseType::MathText),
"math-text" if version.math_is_split() => MonoType::Base(BaseType::MathText),
"math-boxes" if version.math_is_split() => MonoType::Base(BaseType::MathBoxes),
"inline-boxes" => t_inline_boxes(),
"block-boxes" => t_block_boxes(),
"context" => t_context(),
"document" => t_document(),
"text-info" => MonoType::Base(BaseType::TextInfo),
"pre-path" => t_prepath(),
"path" => t_path(),
"graphics" => t_graphics(),
"image" => t_image(),
"deco" if version == RustyfiVersion::V0_1 => t_deco(version),
"deco-set" if version == RustyfiVersion::V0_1 => t_decoset(version),
"font" if version == RustyfiVersion::V0_1 => t_font_key(),
"paren" if version == RustyfiVersion::V0_1 => t_paren(version),
other => MonoType::Variant(other.to_string(), Vec::new()),
}
}
fn mono_type_alpha_eq(a: &MonoType, b: &MonoType) -> bool {
let mut vmap = HashMap::new();
let mut vmap_rev = HashMap::new();
let mut rmap = HashMap::new();
let mut rmap_rev = HashMap::new();
mono_alpha_eq(a, b, &mut vmap, &mut vmap_rev, &mut rmap, &mut rmap_rev)
}
fn mono_alpha_eq(
a: &MonoType,
b: &MonoType,
vmap: &mut HashMap<usize, usize>,
vmap_rev: &mut HashMap<usize, usize>,
rmap: &mut HashMap<usize, usize>,
rmap_rev: &mut HashMap<usize, usize>,
) -> bool {
match (&*resolve(a), &*resolve(b)) {
(MonoType::Var(va), MonoType::Var(vb)) => {
bijective_pair(va.ptr_key(), vb.ptr_key(), vmap, vmap_rev)
}
(MonoType::Base(ba), MonoType::Base(bb)) => ba == bb,
(MonoType::Func(ra, da, ca), MonoType::Func(rb, db, cb)) => {
row_alpha_eq(&ra, &rb, vmap, vmap_rev, rmap, rmap_rev)
&& mono_alpha_eq(&da, &db, vmap, vmap_rev, rmap, rmap_rev)
&& mono_alpha_eq(&ca, &cb, vmap, vmap_rev, rmap, rmap_rev)
}
(MonoType::Product(ta), MonoType::Product(tb)) => {
ta.len() == tb.len()
&& ta
.iter()
.zip(tb.iter())
.all(|(x, y)| mono_alpha_eq(x, y, vmap, vmap_rev, rmap, rmap_rev))
}
(MonoType::List(ta), MonoType::List(tb))
| (MonoType::Ref(ta), MonoType::Ref(tb))
| (MonoType::Code(ta), MonoType::Code(tb)) => {
mono_alpha_eq(&ta, &tb, vmap, vmap_rev, rmap, rmap_rev)
}
(MonoType::Record(ra), MonoType::Record(rb)) => {
row_alpha_eq(&ra, &rb, vmap, vmap_rev, rmap, rmap_rev)
}
(MonoType::Variant(na, aa), MonoType::Variant(nb, ab)) => {
na == nb
&& aa.len() == ab.len()
&& aa
.iter()
.zip(ab.iter())
.all(|(x, y)| mono_alpha_eq(x, y, vmap, vmap_rev, rmap, rmap_rev))
}
(MonoType::InlineCmd(ca), MonoType::InlineCmd(cb))
| (MonoType::BlockCmd(ca), MonoType::BlockCmd(cb))
| (MonoType::MathCmd(ca), MonoType::MathCmd(cb)) => {
cmd_args_alpha_eq(&ca, &cb, vmap, vmap_rev, rmap, rmap_rev)
}
_ => false,
}
}
fn row_alpha_eq(
a: &Row,
b: &Row,
vmap: &mut HashMap<usize, usize>,
vmap_rev: &mut HashMap<usize, usize>,
rmap: &mut HashMap<usize, usize>,
rmap_rev: &mut HashMap<usize, usize>,
) -> bool {
match (&*resolve_row(a), &*resolve_row(b)) {
(Row::Empty, Row::Empty) => true,
(Row::Var(va), Row::Var(vb)) => bijective_pair(va.ptr_key(), vb.ptr_key(), rmap, rmap_rev),
(Row::Cons(la, ta, ra), Row::Cons(lb, tb, rb)) => {
la == lb
&& mono_alpha_eq(&ta, &tb, vmap, vmap_rev, rmap, rmap_rev)
&& row_alpha_eq(&ra, &rb, vmap, vmap_rev, rmap, rmap_rev)
}
_ => false,
}
}
fn cmd_args_alpha_eq(
a: &[CmdArgType],
b: &[CmdArgType],
vmap: &mut HashMap<usize, usize>,
vmap_rev: &mut HashMap<usize, usize>,
rmap: &mut HashMap<usize, usize>,
rmap_rev: &mut HashMap<usize, usize>,
) -> bool {
a.len() == b.len()
&& a.iter().zip(b.iter()).all(|(ca, cb)| {
ca.optional == cb.optional
&& ca.opt_labels.len() == cb.opt_labels.len()
&& ca
.opt_labels
.iter()
.zip(cb.opt_labels.iter())
.all(|((la, tya), (lb, tyb))| {
la == lb && mono_alpha_eq(tya, tyb, vmap, vmap_rev, rmap, rmap_rev)
})
&& mono_alpha_eq(&ca.ty, &cb.ty, vmap, vmap_rev, rmap, rmap_rev)
})
}
fn bijective_pair(
ka: usize,
kb: usize,
map: &mut HashMap<usize, usize>,
map_rev: &mut HashMap<usize, usize>,
) -> bool {
match (map.get(&ka).copied(), map_rev.get(&kb).copied()) {
(Some(mapped_b), Some(mapped_a)) => mapped_b == kb && mapped_a == ka,
(None, None) => {
map.insert(ka, kb);
map_rev.insert(kb, ka);
true
}
_ => false,
}
}
pub(crate) fn forked_type_names() -> BTreeSet<String> {
[
"math",
"math-text",
"math-boxes",
"pre-path",
"path",
"graphics",
"image",
"deco",
"deco-set",
"font",
"paren",
"math-char-class",
]
.into_iter()
.filter(|&n| {
!mono_type_alpha_eq(
&name_to_mono(n, RustyfiVersion::V0_0),
&name_to_mono(n, RustyfiVersion::V0_1),
)
})
.map(str::to_string)
.collect()
}
fn lower_type_atom(
atom: &TypeAtom,
tyvars: &HashMap<String, MonoType>,
version: RustyfiVersion,
) -> MonoType {
match atom {
TypeAtom::Cmd { args, kind, .. } => {
let cmd_args: Vec<CmdArgType> = args
.iter()
.map(|a| {
let ty = lower_type_expr(&a.ty, tyvars, version);
if a.opt_labels.is_empty() {
if a.opt.is_some() {
optional(ty)
} else {
mandatory(ty)
}
} else {
let mut labels: Vec<(String, MonoType)> = a
.opt_labels
.iter()
.map(|f| {
(
f.label.name.clone(),
lower_type_expr(&f.ty, tyvars, version),
)
})
.collect();
labels.sort_by(|x, y| x.0.cmp(&y.0));
labeled(labels, ty)
}
})
.collect();
match kind {
CmdTypeKind::Inline(_) => MonoType::InlineCmd(cmd_args),
CmdTypeKind::Block(_) => MonoType::BlockCmd(cmd_args),
CmdTypeKind::Math(_) => MonoType::MathCmd(cmd_args),
}
}
TypeAtom::Paren { inner, .. } => lower_type_expr(inner, tyvars, version),
TypeAtom::Record { fields, .. } => {
let row = fields.iter().rev().fold(Row::Empty, |rest, f| {
Row::Cons(
f.name.name.clone(),
Box::new(lower_type_expr(&f.ty, tyvars, version)),
Box::new(rest),
)
});
MonoType::Record(row)
}
TypeAtom::RecordOpen { inner, .. } => {
let row = inner
.fields
.iter()
.rev()
.fold(Row::Var(types::new_row_var(0)), |rest, f| {
Row::Cons(
f.name.name.clone(),
Box::new(lower_type_expr(&f.ty, tyvars, version)),
Box::new(rest),
)
});
MonoType::Record(row)
}
TypeAtom::Var(tv) => match tyvars.get(&tv.name) {
Some(v) => v.clone(),
None => MonoType::Var(types::new_ty_var(0)),
},
TypeAtom::Name(name) => name_to_mono(&name.name, version),
TypeAtom::NameMod(qn) => {
MonoType::Variant(format!("{}.{}", qn.mods.join("."), qn.name), Vec::new())
}
}
}
fn lower_type_prod(
prod: &TypeProd,
tyvars: &HashMap<String, MonoType>,
version: RustyfiVersion,
) -> MonoType {
if prod.rest.is_empty() {
lower_type_app(&prod.first, tyvars, version)
} else {
let mut items = Vec::with_capacity(1 + prod.rest.len());
items.push(lower_type_app(&prod.first, tyvars, version));
for st in &prod.rest {
items.push(lower_type_app(&st.ty, tyvars, version));
}
product(items)
}
}
fn lower_type_app(
app: &TypeApp,
tyvars: &HashMap<String, MonoType>,
version: RustyfiVersion,
) -> MonoType {
if app.rest.is_empty() {
return lower_type_atom(&app.head, tyvars, version);
}
let (ctor, args): (&TypeAtom, Vec<MonoType>) = {
let n = app.rest.len();
let arg_tys = std::iter::once(&app.head)
.chain(app.rest[..n - 1].iter())
.map(|a| lower_type_atom(a, tyvars, version))
.collect();
(&app.rest[n - 1], arg_tys)
};
match ctor {
TypeAtom::Name(name) => {
let single = if args.len() == 1 {
Some(args[0].clone())
} else {
None
};
match name.name.as_str() {
"list" if single.is_some() => list(single.unwrap()),
"ref" if single.is_some() => reff(single.unwrap()),
"code" if single.is_some() && version.has_code_type_syntax() => {
MonoType::Code(Box::new(single.unwrap()))
}
"implicit" if single.is_some() => single.unwrap(),
other => MonoType::Variant(other.to_string(), args),
}
}
TypeAtom::NameMod(qn) => {
MonoType::Variant(format!("{}.{}", qn.mods.join("."), qn.name), args)
}
_ => lower_type_atom(ctor, tyvars, version),
}
}
pub(crate) fn lower_type_expr(
ty: &TypeExpr,
tyvars: &HashMap<String, MonoType>,
version: RustyfiVersion,
) -> MonoType {
match ty {
TypeExpr::Fun { opts, dom, cod, .. } => {
let result = arrow(
lower_type_prod(dom, tyvars, version),
lower_type_expr(cod, tyvars, version),
);
opts.iter().rev().fold(result, |acc, opt| {
arrow(t_option(lower_type_prod(&opt.ty, tyvars, version)), acc)
})
}
TypeExpr::Atom(prod) => lower_type_prod(prod, tyvars, version),
TypeExpr::OptRowFun {
opt_dom, dom, cod, ..
} => {
let row = opt_dom.entries.iter().rev().fold(Row::Empty, |acc, e| {
Row::Cons(
e.label.name.clone(),
Box::new(lower_type_expr(&e.ty, tyvars, version)),
Box::new(acc),
)
});
MonoType::Func(
Box::new(row),
Box::new(lower_type_prod(dom, tyvars, version)),
Box::new(lower_type_expr(cod, tyvars, version)),
)
}
}
}
fn check_type_expr_v0_1_only(ty: &TypeExpr, version: RustyfiVersion) -> Result<(), TypeError> {
if version.has_row_polymorphism() {
return Ok(());
}
if let Some(span) = find_opt_row_fun_in_expr(ty) {
return Err(TypeError::simple(
Some(span),
"`?(l : ty) -> ...` labeled-optional-argument type domains are SATySFi \
0.1 syntax — this file is compiled as 0.0.6",
));
}
Ok(())
}
fn find_opt_row_fun_in_expr(ty: &TypeExpr) -> Option<Span> {
match ty {
TypeExpr::OptRowFun { opt_dom, .. } => Some(opt_dom.q.0),
TypeExpr::Fun { dom, cod, .. } => {
find_opt_row_fun_in_prod(dom).or_else(|| find_opt_row_fun_in_expr(cod))
}
TypeExpr::Atom(p) => find_opt_row_fun_in_prod(p),
}
}
fn find_opt_row_fun_in_prod(p: &TypeProd) -> Option<Span> {
find_opt_row_fun_in_app(&p.first)
.or_else(|| p.rest.iter().find_map(|s| find_opt_row_fun_in_app(&s.ty)))
}
fn find_opt_row_fun_in_app(a: &TypeApp) -> Option<Span> {
std::iter::once(&a.head)
.chain(a.rest.iter())
.find_map(find_opt_row_fun_in_atom)
}
fn find_opt_row_fun_in_atom(a: &TypeAtom) -> Option<Span> {
match a {
TypeAtom::Cmd { args, .. } => args.iter().find_map(|it| find_opt_row_fun_in_expr(&it.ty)),
TypeAtom::Paren { inner, .. } => find_opt_row_fun_in_expr(inner),
TypeAtom::Record { fields, .. } => {
fields.iter().find_map(|f| find_opt_row_fun_in_expr(&f.ty))
}
TypeAtom::RecordOpen { inner, .. } => inner
.fields
.iter()
.find_map(|f| find_opt_row_fun_in_expr(&f.ty)),
TypeAtom::Var(_) | TypeAtom::Name(_) | TypeAtom::NameMod(_) => None,
}
}
#[allow(dead_code)]
fn collect_type_vars(ty: &TypeExpr, out: &mut Vec<String>) {
fn push(name: &str, out: &mut Vec<String>) {
if !out.iter().any(|n| n == name) {
out.push(name.to_string());
}
}
fn walk_atom(atom: &TypeAtom, out: &mut Vec<String>) {
match atom {
TypeAtom::Cmd { args, .. } => {
for a in args {
walk_expr(&a.ty, out);
}
}
TypeAtom::Paren { inner, .. } => walk_expr(inner, out),
TypeAtom::Record { fields, .. } => {
for f in fields {
walk_expr(&f.ty, out);
}
}
TypeAtom::Var(tv) => push(&tv.name, out),
TypeAtom::Name(_) => {}
TypeAtom::NameMod(_) => {}
TypeAtom::RecordOpen { inner, .. } => {
for f in &inner.fields {
walk_expr(&f.ty, out);
}
}
}
}
fn walk_app(app: &TypeApp, out: &mut Vec<String>) {
walk_atom(&app.head, out);
for a in &app.rest {
walk_atom(a, out);
}
}
fn walk_prod(prod: &TypeProd, out: &mut Vec<String>) {
walk_app(&prod.first, out);
for st in &prod.rest {
walk_app(&st.ty, out);
}
}
fn walk_expr(ty: &TypeExpr, out: &mut Vec<String>) {
match ty {
TypeExpr::Fun { opts, dom, cod, .. } => {
for opt in opts {
walk_prod(&opt.ty, out);
}
walk_prod(dom, out);
walk_expr(cod, out);
}
TypeExpr::Atom(prod) => walk_prod(prod, out),
TypeExpr::OptRowFun {
opt_dom, dom, cod, ..
} => {
for e in &opt_dom.entries {
walk_expr(&e.ty, out);
}
walk_prod(dom, out);
walk_expr(cod, out);
}
}
}
walk_expr(ty, out);
}
#[allow(dead_code)]
fn lower_record_kind(rk: &RecordKind) -> BTreeSet<String> {
rk.fields.iter().map(|f| f.name.name.clone()).collect()
}
#[allow(dead_code)]
pub(crate) fn lower_sig_item(
item: &SigItem,
ctx: &mut TypeContext,
version: RustyfiVersion,
) -> Option<(String, MonoType)> {
let (name, ty, constraints): (&str, &TypeExpr, &[SigConstraint]) = match item {
SigItem::ValHorzCmd {
name,
ty,
constraints,
..
} => (&name.name, ty, constraints),
SigItem::ValVertCmd {
name,
ty,
constraints,
..
} => (&name.name, ty, constraints),
SigItem::Val {
name,
ty,
constraints,
..
} => (&name.name, ty, constraints),
SigItem::DirectHorzCmd {
name,
ty,
constraints,
..
} => (&name.name, ty, constraints),
SigItem::DirectVertCmd {
name,
ty,
constraints,
..
} => (&name.name, ty, constraints),
SigItem::Type { .. } => return None,
};
let mut names = Vec::new();
collect_type_vars(ty, &mut names);
let mut tyvars = HashMap::new();
for n in names {
let found = constraints.iter().find(|c| c.tyvar.name == n);
let v = match found {
Some(c) => ctx.fresh_var_with_kind(Kind::Record(lower_record_kind(&c.kind))),
None => ctx.fresh_var_with_kind(Kind::Universal),
};
tyvars.insert(n, MonoType::Var(v));
}
Some((name.to_string(), lower_type_expr(ty, &tyvars, version)))
}
fn build_variant_decl(
decl: &UserTypeDecl,
synonyms: &HashMap<String, SynonymDecl>,
version: RustyfiVersion,
) -> Result<VariantDecl, TypeError> {
let param_vars: Vec<types::TyVarRef> =
decl.params.iter().map(|_| types::new_ty_var(0)).collect();
let tyvar_map: HashMap<String, MonoType> = decl
.params
.iter()
.cloned()
.zip(param_vars.iter().cloned().map(MonoType::Var))
.collect();
let mut ctors = Vec::with_capacity(decl.ctors.len());
for (name, ty) in &decl.ctors {
let payload = match ty {
None => None,
Some(t) => {
check_type_expr_v0_1_only(t, version)?;
Some(expand_synonyms(
&lower_type_expr(t, &tyvar_map, version),
synonyms,
)?)
}
};
ctors.push((name.clone(), payload));
}
Ok(VariantDecl {
name: decl.name.clone(),
params: decl.params.len(),
ctors,
param_vars,
})
}
struct SynonymDecl {
param_vars: Vec<types::TyVarRef>,
body: MonoType,
}
fn build_synonym_decl(decl: &UserSynonymDecl, version: RustyfiVersion) -> SynonymDecl {
let param_vars: Vec<types::TyVarRef> =
decl.params.iter().map(|_| types::new_ty_var(0)).collect();
let tyvar_map: HashMap<String, MonoType> = decl
.params
.iter()
.cloned()
.zip(param_vars.iter().cloned().map(MonoType::Var))
.collect();
SynonymDecl {
param_vars,
body: lower_type_expr(&decl.body, &tyvar_map, version),
}
}
fn synonym_refs(ty: &MonoType, synonyms: &HashMap<String, SynonymDecl>, out: &mut Vec<String>) {
ty.visit(|t: &MonoType| {
if let MonoType::Variant(name, _) = t {
if synonyms.contains_key(name) {
out.push(name.clone());
}
}
});
}
fn check_synonym_cycles(synonyms: &HashMap<String, SynonymDecl>) -> Result<(), TypeError> {
for start in synonyms.keys() {
let mut stack = vec![start.clone()];
check_synonym_cycles_from(start, synonyms, &mut stack)?;
}
Ok(())
}
fn check_synonym_cycles_from(
name: &str,
synonyms: &HashMap<String, SynonymDecl>,
stack: &mut Vec<String>,
) -> Result<(), TypeError> {
let mut refs = Vec::new();
synonym_refs(&synonyms[name].body, synonyms, &mut refs);
for r in refs {
if stack.contains(&r) {
let mut cycle = stack.clone();
cycle.push(r);
return Err(TypeError::simple(
None,
format!("cyclic type synonym: {}", cycle.join(" -> ")),
));
}
stack.push(r.clone());
check_synonym_cycles_from(&r, synonyms, stack)?;
stack.pop();
}
Ok(())
}
fn expand_synonyms(
ty: &MonoType,
synonyms: &HashMap<String, SynonymDecl>,
) -> Result<MonoType, TypeError> {
match ty {
MonoType::Var(_) | MonoType::Base(_) => Ok(ty.clone()),
MonoType::Func(row, dom, cod) => Ok(MonoType::Func(
Box::new(expand_synonyms_row(row, synonyms)?),
Box::new(expand_synonyms(dom, synonyms)?),
Box::new(expand_synonyms(cod, synonyms)?),
)),
MonoType::Product(ts) => Ok(MonoType::Product(
ts.iter()
.map(|t| expand_synonyms(t, synonyms))
.collect::<Result<_, _>>()?,
)),
MonoType::List(t) => Ok(MonoType::List(Box::new(expand_synonyms(t, synonyms)?))),
MonoType::Ref(t) => Ok(MonoType::Ref(Box::new(expand_synonyms(t, synonyms)?))),
MonoType::Code(t) => Ok(MonoType::Code(Box::new(expand_synonyms(t, synonyms)?))),
MonoType::Record(row) => Ok(MonoType::Record(expand_synonyms_row(row, synonyms)?)),
MonoType::Variant(name, args) => {
let args: Vec<MonoType> = args
.iter()
.map(|t| expand_synonyms(t, synonyms))
.collect::<Result<_, _>>()?;
let Some(syn) = synonyms.get(name) else {
return Ok(MonoType::Variant(name.clone(), args));
};
if args.len() != syn.param_vars.len() {
return Err(TypeError::simple(
None,
format!(
"type synonym '{name}' expects {} argument{}, got {}",
syn.param_vars.len(),
if syn.param_vars.len() == 1 { "" } else { "s" },
args.len()
),
));
}
let mut var_map: HashMap<usize, MonoType> = HashMap::new();
for (pv, arg) in syn.param_vars.iter().zip(args.iter()) {
var_map.insert(types::ptr_key(pv), arg.clone());
}
let substituted = types::substitute(&syn.body, &var_map, &HashMap::new());
expand_synonyms(&substituted, synonyms)
}
MonoType::InlineCmd(cs) => Ok(MonoType::InlineCmd(expand_synonyms_cmd_args(cs, synonyms)?)),
MonoType::BlockCmd(cs) => Ok(MonoType::BlockCmd(expand_synonyms_cmd_args(cs, synonyms)?)),
MonoType::MathCmd(cs) => Ok(MonoType::MathCmd(expand_synonyms_cmd_args(cs, synonyms)?)),
}
}
fn expand_synonyms_row(
row: &Row,
synonyms: &HashMap<String, SynonymDecl>,
) -> Result<Row, TypeError> {
match row {
Row::Empty => Ok(Row::Empty),
Row::Var(v) => Ok(Row::Var(v.clone())),
Row::Cons(label, t, rest) => Ok(Row::Cons(
label.clone(),
Box::new(expand_synonyms(t, synonyms)?),
Box::new(expand_synonyms_row(rest, synonyms)?),
)),
}
}
fn expand_synonyms_cmd_args(
cs: &[CmdArgType],
synonyms: &HashMap<String, SynonymDecl>,
) -> Result<Vec<CmdArgType>, TypeError> {
cs.iter()
.map(|c| {
Ok(CmdArgType {
optional: c.optional,
opt_labels: c
.opt_labels
.iter()
.map(|(l, t)| Ok((l.clone(), expand_synonyms(t, synonyms)?)))
.collect::<Result<_, TypeError>>()?,
ty: expand_synonyms(&c.ty, synonyms)?,
})
})
.collect()
}
pub(crate) struct Checker<'s> {
store: &'s SymbolStore,
ctx: TypeContext,
ctors: HashMap<String, Rc<VariantDecl>>,
variants: HashMap<String, Rc<VariantDecl>>,
synonyms: HashMap<String, SynonymDecl>,
warnings: Vec<MatchWarning>,
version: RustyfiVersion,
scoped_version: Option<RustyfiVersion>,
ctor_scope: Vec<String>,
stage: Stage,
}
pub(crate) enum BindingView<'a, 's> {
Let {
name: Symbol<'s>,
value: &'a Ast<'s>,
},
LetMath {
name: Symbol<'s>,
value: &'a Ast<'s>,
},
LetRec(&'a [(Symbol<'s>, Rc<Ast<'s>>)]),
LetMutable { name: Symbol<'s>, init: &'a Ast<'s> },
}
impl<'s> Checker<'s> {
#[allow(dead_code)]
fn new(program: &Program<'s>) -> Result<Checker<'s>, TypeError> {
Self::new_with_version(program, RustyfiVersion::V0_0)
}
pub(crate) fn empty(store: &'s SymbolStore) -> Checker<'s> {
Checker {
store,
ctx: TypeContext::new(),
ctors: HashMap::new(),
variants: HashMap::new(),
synonyms: HashMap::new(),
warnings: Vec::new(),
version: RustyfiVersion::V0_0,
scoped_version: None,
ctor_scope: Vec::new(),
stage: Stage::default(),
}
}
pub(crate) fn set_version(&mut self, version: RustyfiVersion) {
self.version = version;
}
fn text(&self, sym: Symbol<'s>) -> &'s str {
self.store.resolve(sym)
}
pub(crate) fn install_builtin_variants(&mut self, version: RustyfiVersion) {
self.version = version;
self.install_additional_builtin_variants(version);
}
pub(crate) fn install_additional_builtin_variants(&mut self, version: RustyfiVersion) {
for decl in builtin_variants_with_version(version) {
let decl = Rc::new(decl);
self.variants.insert(decl.name.clone(), decl.clone());
for (cname, _) in &decl.ctors {
self.ctors.insert(cname.clone(), decl.clone());
}
}
}
pub(crate) fn declare_synonym(&mut self, decl: &UserSynonymDecl) -> Result<(), TypeError> {
check_type_expr_v0_1_only(&decl.body, self.version)?;
self.synonyms
.insert(decl.name.clone(), build_synonym_decl(decl, self.version));
Ok(())
}
pub(crate) fn check_cycles(&self) -> Result<(), TypeError> {
check_synonym_cycles(&self.synonyms)
}
pub(crate) fn declare_variant(&mut self, decl: &UserTypeDecl) -> Result<(), TypeError> {
let decl = Rc::new(build_variant_decl(decl, &self.synonyms, self.version)?);
self.variants.insert(decl.name.clone(), decl.clone());
for (cname, _) in &decl.ctors {
self.ctors.insert(cname.clone(), decl.clone());
}
if let Some((modpfx, _)) = decl.name.rsplit_once('.') {
for (cname, _) in &decl.ctors {
self.ctors.insert(format!("{modpfx}.{cname}"), decl.clone());
}
}
Ok(())
}
fn new_with_version(
program: &Program<'s>,
version: RustyfiVersion,
) -> Result<Checker<'s>, TypeError> {
let mut c = Checker::empty(program.store);
c.set_version(version);
for usd in &program.synonym_decls {
c.declare_synonym(usd)?;
}
c.check_cycles()?;
c.install_builtin_variants(version);
for utd in &program.type_decls {
c.declare_variant(utd)?;
}
Ok(c)
}
fn fresh(&mut self) -> MonoType {
MonoType::Var(self.ctx.fresh_var())
}
fn unify_ctx(
&mut self,
expected: &MonoType,
found: &MonoType,
span: Option<Span>,
what: &str,
) -> Result<(), TypeError> {
unify(expected, found).map_err(|e| TypeError::from_unify(span, what, e))
}
fn command_scheme(
&mut self,
name: &str,
sigil: char,
tv: MonoType,
span: Option<Span>,
) -> Result<PolyType, TypeError> {
debug_assert!(sigil == '\\' || sigil == '+');
let is_inline = sigil == '\\';
let (want_result, kind, other_kind) = if is_inline {
(t_inline_boxes(), "inline", "block")
} else {
(t_block_boxes(), "block", "inline")
};
match &*resolve(&tv) {
MonoType::InlineCmd(_) if is_inline => {
return Ok(generalize(self.ctx.level(), &tv));
}
MonoType::BlockCmd(_) if !is_inline => {
return Ok(generalize(self.ctx.level(), &tv));
}
MonoType::InlineCmd(_) | MonoType::BlockCmd(_) => {
return Err(TypeError::simple(
span,
format!(
"'{name}' is bound to a {other_kind} command, but its \
name marks it as {article} {kind} command",
article = if kind == "inline" { "an" } else { "a" },
),
));
}
MonoType::MathCmd(_) if is_inline => {
return Ok(generalize(self.ctx.level(), &tv));
}
_ => {}
}
let params: Vec<CmdArgType> = if self.version.has_row_polymorphism() {
let (mut slots, result) = peel_func_chain_rows(tv);
if slots.is_empty() {
return Err(TypeError::simple(
span,
format!(
"the binding for '{name}' must be a function taking a \
context as its first argument (e.g. via `val inline ctx \
{name} .. = ..`)"
),
));
}
let (ctx_row, ctx_ty) = slots.remove(0);
if !matches!(&*resolve_row(&ctx_row), Row::Empty) {
return Err(TypeError::simple(
span,
format!(
"the context argument of '{name}' cannot carry a labeled \
optional bundle"
),
));
}
self.unify_ctx(
&t_context(),
&ctx_ty,
span,
&format!("the context argument of '{name}'"),
)?;
self.unify_ctx(
&want_result,
&result,
span,
&format!("the result of '{name}'"),
)?;
slots
.into_iter()
.map(|(row, dom)| harvest_slot(row, dom))
.collect()
} else {
let (mut doms, result) = peel_func_chain(tv);
if doms.is_empty() {
return Err(TypeError::simple(
span,
format!(
"the binding for '{name}' must be a function taking a \
context as its first argument (e.g. via `let-inline ctx \
{name} .. = ..`)"
),
));
}
let ctx_ty = doms.remove(0);
self.unify_ctx(
&t_context(),
&ctx_ty,
span,
&format!("the context argument of '{name}'"),
)?;
self.unify_ctx(
&want_result,
&result,
span,
&format!("the result of '{name}'"),
)?;
doms.into_iter()
.map(|d| match resolve(&d).into_owned() {
MonoType::Variant(vname, mut vargs)
if vname == "option" && vargs.len() == 1 =>
{
optional(vargs.pop().unwrap())
}
_ => mandatory(d),
})
.collect()
};
let cmd_ty = if is_inline {
MonoType::InlineCmd(params)
} else {
MonoType::BlockCmd(params)
};
Ok(generalize(self.ctx.level(), &cmd_ty))
}
fn math_command_scheme(
&mut self,
name: &str,
tv: MonoType,
span: Option<Span>,
) -> Result<PolyType, TypeError> {
let (doms, result) = peel_func_chain(tv);
self.unify_ctx(
&t_math_text(),
&result,
span,
&format!("the result of math command '{name}'"),
)?;
let params: Vec<CmdArgType> = doms
.into_iter()
.map(|d| match resolve(&d).into_owned() {
MonoType::Variant(vname, mut vargs) if vname == "option" && vargs.len() == 1 => {
optional(vargs.pop().unwrap())
}
_ => mandatory(d),
})
.collect();
Ok(generalize(self.ctx.level(), &MonoType::MathCmd(params)))
}
fn math_command_scheme_v01(
&mut self,
name: &str,
tv: MonoType,
span: Option<Span>,
) -> Result<PolyType, TypeError> {
let (mut slots, result) = peel_func_chain_rows(tv);
if slots.len() < 3 {
return Err(TypeError::simple(
span,
format!(
"'val math' command '{name}' must take a context and (via the \
synthesized `with sub sup`/`%math-attach-scripts` wrapper) two \
optional scripts as its trailing arguments — see the math-split spec"
),
));
}
let (row_sup, d_sup) = slots.pop().unwrap();
let (row_sub, d_sub) = slots.pop().unwrap();
let (row_ctx, d_ctx) = slots.pop().unwrap();
for (which, row) in [
("context", &row_ctx),
("'sub'", &row_sub),
("'sup'", &row_sup),
] {
if !matches!(&*resolve_row(row), Row::Empty) {
return Err(TypeError::simple(
span,
format!(
"the {which} argument of 'val math' command '{name}' cannot \
carry a labeled optional bundle"
),
));
}
}
self.unify_ctx(
&t_context(),
&d_ctx,
span,
&format!("the context argument of 'val math' command '{name}'"),
)?;
self.unify_ctx(
&t_option(t_math_text()),
&d_sub,
span,
&format!("the 'sub' argument of 'val math' command '{name}'"),
)?;
self.unify_ctx(
&t_option(t_math_text()),
&d_sup,
span,
&format!("the 'sup' argument of 'val math' command '{name}'"),
)?;
self.unify_ctx(
&t_math_boxes(),
&result,
span,
&format!(
"the result of 0.1 math command '{name}' — a `math-boxes`, \
usually via `read-math`"
),
)?;
let params: Vec<CmdArgType> = slots
.into_iter()
.map(|(row, dom)| harvest_slot(row, dom))
.collect();
Ok(generalize(self.ctx.level(), &MonoType::MathCmd(params)))
}
fn check_cmd_args(
&mut self,
env: &TypeEnv<'s>,
name: &str,
span: Span,
params: &[CmdArgType],
args: &[CmdArg<'s>],
) -> Result<(), TypeError> {
if params.len() != args.len() {
return Err(TypeError::simple(
Some(span),
format!(
"command '{name}' expects {} argument{}, got {}",
params.len(),
if params.len() == 1 { "" } else { "s" },
args.len()
),
));
}
for (i, (param, arg)) in params.iter().zip(args.iter()).enumerate() {
for (label, val) in &arg.opts {
match param.opt_labels.iter().find(|(l, _)| l == label) {
Some((_, lty)) => {
let tval = self.infer(env, val)?;
self.unify_ctx(
lty,
&tval,
ast_span(val).or(Some(span)),
&format!("optional argument `{label}` of '{name}'"),
)?;
}
None => {
return Err(TypeError::simple(
ast_span(val).or(Some(span)),
format!(
"command '{name}' has no optional label `{label}` \
on argument {}",
i + 1
),
));
}
}
}
let targ = self.infer(env, &arg.arg)?;
let expected = if param.optional {
t_option(param.ty.clone())
} else {
param.ty.clone()
};
self.unify_ctx(
&expected,
&targ,
ast_span(&arg.arg).or(Some(span)),
&format!("argument {} of '{name}'", i + 1),
)?;
}
Ok(())
}
pub(crate) fn infer_binding(
&mut self,
env: &TypeEnv<'s>,
binding: BindingView<'_, 's>,
) -> Result<Vec<(Symbol<'s>, PolyType)>, TypeError> {
match binding {
BindingView::Let { name, value } => {
self.ctx.enter_level();
let tv = self.infer(env, value)?;
self.ctx.leave_level();
let scheme = match command_sigil(self.text(name)) {
Some(sigil) => {
self.command_scheme(self.text(name), sigil, tv, ast_span(value))?
}
None => generalize(self.ctx.level(), &tv),
};
Ok(vec![(name, scheme)])
}
BindingView::LetMath { name, value } => {
self.ctx.enter_level();
let tv = self.infer(env, value)?;
self.ctx.leave_level();
let scheme = if self.binding_version(value).math_is_split() {
self.math_command_scheme_v01(self.text(name), tv, ast_span(value))?
} else {
self.math_command_scheme(self.text(name), tv, ast_span(value))?
};
Ok(vec![(name, scheme)])
}
BindingView::LetRec(bindings) => {
self.ctx.enter_level();
let group_stage = self.binding_stage_rec(bindings);
let mut rec_env = env.clone();
let mut vars = Vec::with_capacity(bindings.len());
for (name, _) in bindings {
let v = self.fresh();
vars.push(v.clone());
rec_env = rec_env.with(*name, PolyType::mono(v), group_stage);
}
for ((name, val), v) in bindings.iter().zip(vars.iter()) {
let tv = self.infer(&rec_env, val)?;
self.unify_ctx(
v,
&tv,
ast_span(val),
&format!("let-rec binding '{}'", self.text(*name)),
)?;
}
self.ctx.leave_level();
let mut schemes = Vec::with_capacity(bindings.len());
for ((name, _), v) in bindings.iter().zip(vars.iter()) {
let scheme = generalize(self.ctx.level(), v);
schemes.push((*name, scheme));
}
Ok(schemes)
}
BindingView::LetMutable { name, init } => {
let tinit = self.infer(env, init)?;
Ok(vec![(name, PolyType::mono(reff(tinit)))])
}
}
}
pub(crate) fn infer_expr(
&mut self,
env: &TypeEnv<'s>,
ast: &Ast<'s>,
) -> Result<MonoType, TypeError> {
self.infer(env, ast)
}
pub(crate) fn take_warnings(&mut self) -> Vec<MatchWarning> {
std::mem::take(&mut self.warnings)
}
pub(crate) fn ctx_mut(&mut self) -> &mut TypeContext {
&mut self.ctx
}
pub(crate) fn expand_synonyms_in(&self, ty: &MonoType) -> Result<MonoType, TypeError> {
expand_synonyms(ty, &self.synonyms)
}
pub(crate) fn hide_ctors(&mut self, entries: &[(String, String)]) {
for (ctor, tyname) in entries {
if self.ctors.get(ctor).is_some_and(|d| &d.name == tyname) {
self.ctors.remove(ctor);
}
if let Some((modpfx, _)) = tyname.rsplit_once('.') {
let q = format!("{modpfx}.{ctor}");
if self.ctors.get(&q).is_some_and(|d| &d.name == tyname) {
self.ctors.remove(&q);
}
}
}
}
#[inline(never)]
fn infer_apply_opt(
&mut self,
env: &TypeEnv<'s>,
func: &Ast<'s>,
opts: &[(String, Ast<'s>)],
arg: &Ast<'s>,
) -> Result<MonoType, TypeError> {
let tf = self.infer(env, func)?;
let ta = self.infer(env, arg)?;
let tr = self.fresh();
let mut opt_tys = Vec::with_capacity(opts.len());
for (label, e) in opts {
opt_tys.push((label.clone(), self.infer(env, e)?));
}
let mut row = Row::Var(self.ctx.fresh_row_var());
for (label, ty) in opt_tys.into_iter().rev() {
row = Row::Cons(label, Box::new(ty), Box::new(row));
}
self.unify_ctx(
&tf,
&MonoType::Func(Box::new(row), Box::new(ta), Box::new(tr.clone())),
ast_span(func),
"function application",
)?;
Ok(tr)
}
#[inline(never)]
fn infer_lambda_opt(
&mut self,
env: &TypeEnv<'s>,
opts: &[(String, Symbol<'s>)],
param: Symbol<'s>,
body: &Ast<'s>,
) -> Result<MonoType, TypeError> {
let mut inner = env.clone();
let mut opt_tys = Vec::with_capacity(opts.len());
for (label, binder) in opts {
let tl = self.fresh();
inner = inner.with(*binder, PolyType::mono(t_option(tl.clone())), self.stage);
opt_tys.push((label.clone(), tl));
}
let tp = self.fresh();
inner = inner.with(param, PolyType::mono(tp.clone()), self.stage);
let tb = self.infer(&inner, body)?;
let mut row = Row::Empty;
for (label, tl) in opt_tys.into_iter().rev() {
row = Row::Cons(label, Box::new(tl), Box::new(row));
}
Ok(MonoType::Func(Box::new(row), Box::new(tp), Box::new(tb)))
}
pub(crate) fn binding_stage(&self, value: &Ast<'s>) -> Stage {
fn declared<'s>(a: &Ast<'s>) -> Option<Stage> {
match a {
Ast::StageScope(st, _) => Some(*st),
Ast::ModuleScope(_, b) | Ast::VersionScope(_, b) => declared(b),
_ => None,
}
}
declared(value).unwrap_or(self.stage)
}
pub(crate) fn binding_version(&self, value: &Ast<'s>) -> RustyfiVersion {
fn declared<'s>(a: &Ast<'s>) -> Option<RustyfiVersion> {
match a {
Ast::VersionScope(v, _) => Some(*v),
Ast::StageScope(_, b) | Ast::ModuleScope(_, b) => declared(b),
_ => None,
}
}
declared(value)
.or(self.scoped_version)
.unwrap_or(self.version)
}
pub(crate) fn binding_stage_rec(&self, bindings: &[(Symbol<'s>, Rc<Ast<'s>>)]) -> Stage {
match bindings.first() {
Some((_, v)) => self.binding_stage(v),
None => self.stage,
}
}
fn staged<'e>(
&self,
env: &'e TypeEnv<'s>,
name: Symbol<'s>,
span: Option<Span>,
what: &str,
) -> Result<Option<&'e PolyType>, TypeError> {
let Some(entry) = env.entry(name) else {
return Ok(None);
};
if !self.stage.can_reference(entry.stage) {
return Err(TypeError::simple(
span,
format!(
"invalid occurrence of {what} '{}' as to stage: it is bound at {}, \
but this is {}",
self.text(name),
entry.stage.as_str(),
self.stage.as_str()
),
));
}
Ok(Some(&entry.poly))
}
fn infer_at(
&mut self,
stage: Stage,
env: &TypeEnv<'s>,
ast: &Ast<'s>,
) -> Result<MonoType, TypeError> {
let saved = std::mem::replace(&mut self.stage, stage);
let result = self.infer(env, ast);
self.stage = saved;
result
}
fn infer(&mut self, env: &TypeEnv<'s>, ast: &Ast<'s>) -> Result<MonoType, TypeError> {
match ast {
Ast::StageScope(stage, body) => self.infer_at(*stage, env, body),
Ast::Next(inner) => {
if self.stage != Stage::Stage0 {
return Err(TypeError::simple(
None,
format!(
"`&` (next-stage quote) is only valid at stage 0, but this is {}",
self.stage.as_str()
),
));
}
let ty = self.infer_at(Stage::Stage1, env, inner)?;
Ok(MonoType::Code(Box::new(ty)))
}
Ast::Prev(inner) => {
if self.stage != Stage::Stage1 {
return Err(TypeError::simple(
None,
format!(
"`~` (previous-stage splice) is only valid at stage 1, but this is {}",
self.stage.as_str()
),
));
}
let ty = self.infer_at(Stage::Stage0, env, inner)?;
let beta = MonoType::Var(self.ctx.fresh_var());
unify(&ty, &MonoType::Code(Box::new(beta.clone())))
.map_err(|e| TypeError::from_unify(None, "a `~` splice", e))?;
Ok(beta)
}
Ast::Unit => Ok(t_unit()),
Ast::Bool(_) => Ok(t_bool()),
Ast::Int(_) => Ok(t_int()),
Ast::Float(_) => Ok(t_float()),
Ast::Length(_) => Ok(t_length()),
Ast::Str(_) => Ok(t_string()),
Ast::Var(name, span) => match self.staged(env, *name, Some(*span), "variable")? {
Some(poly) => Ok(instantiate(poly, self.ctx.level())),
None => Err(TypeError::simple(
Some(*span),
format!(
"internal error: unbound variable '{}' reached the typechecker",
self.text(*name)
),
)),
},
Ast::Apply(f, a) => {
let tf = self.infer(env, f)?;
let ta = self.infer(env, a)?;
let tr = self.fresh();
let opts_row = if self.version.has_row_polymorphism() {
Row::Var(self.ctx.fresh_row_var())
} else {
Row::Empty
};
self.unify_ctx(
&tf,
&MonoType::Func(Box::new(opts_row), Box::new(ta), Box::new(tr.clone())),
ast_span(f),
"function application",
)?;
Ok(tr)
}
Ast::Lambda(param, body) => {
let tp = self.fresh();
let inner = env.with(*param, PolyType::mono(tp.clone()), self.stage);
let tb = self.infer(&inner, body)?;
Ok(arrow(tp, tb))
}
Ast::ApplyOpt { func, opts, arg } => self.infer_apply_opt(env, func, opts, arg),
Ast::LambdaOpt { opts, param, body } => self.infer_lambda_opt(env, opts, *param, body),
Ast::LetIn(name, value, body) => {
let schemes = self.infer_binding(env, BindingView::Let { name: *name, value })?;
let inner = env.with_all(schemes, self.binding_stage(value));
self.infer(&inner, body)
}
Ast::LetMathIn(name, value, body) => {
let schemes =
self.infer_binding(env, BindingView::LetMath { name: *name, value })?;
let inner = env.with_all(schemes, self.binding_stage(value));
self.infer(&inner, body)
}
Ast::LetRecIn(bindings, body) => {
let schemes = self.infer_binding(env, BindingView::LetRec(bindings))?;
let inner = env.with_all(schemes, self.binding_stage_rec(bindings));
self.infer(&inner, body)
}
Ast::IfThenElse(cond, then_b, else_b) => {
let tc = self.infer(env, cond)?;
self.unify_ctx(&t_bool(), &tc, ast_span(cond), "the condition of 'if'")?;
let tt = self.infer(env, then_b)?;
let te = self.infer(env, else_b)?;
self.unify_ctx(&tt, &te, ast_span(else_b), "the branches of 'if'")?;
Ok(tt)
}
Ast::Match(scrutinee, arms) => {
let tscrut = self.infer(env, scrutinee)?;
let mut result: Option<MonoType> = None;
for arm in arms {
let arm_env = self.bind_pattern(env.clone(), &arm.pat, &tscrut)?;
if let Some(guard) = &arm.guard {
let tg = self.infer(&arm_env, guard)?;
self.unify_ctx(&t_bool(), &tg, ast_span(guard), "a match guard")?;
}
let tbody = self.infer(&arm_env, &arm.body)?;
match &result {
None => result = Some(tbody),
Some(r) => {
self.unify_ctx(r, &tbody, ast_span(&arm.body), "the arms of 'match'")?
}
}
}
let resolved_scrut = resolve(&tscrut);
let new_warnings = crate::exhaustive::check_match(
self.store,
&resolved_scrut,
ast_span(scrutinee),
arms,
&self.variants,
);
self.warnings.extend(new_warnings);
Ok(result.unwrap_or_else(|| self.fresh()))
}
Ast::Tuple(items) => {
let tys = items
.iter()
.map(|it| self.infer(env, it))
.collect::<Result<Vec<_>, _>>()?;
Ok(product(tys))
}
Ast::Ctor(name, payload) => self.infer_ctor(env, name, payload.as_deref(), None),
Ast::Record(fields) => {
let mut typed = Vec::with_capacity(fields.len());
for (label, e) in fields {
typed.push((label.clone(), self.infer(env, e)?));
}
let mut row = Row::Empty;
for (label, ty) in typed.into_iter().rev() {
row = Row::Cons(label, Box::new(ty), Box::new(row));
}
Ok(MonoType::Record(row))
}
Ast::List(items) => {
let elem = self.fresh();
for it in items {
let t = self.infer(env, it)?;
self.unify_ctx(&elem, &t, ast_span(it), "a list element")?;
}
Ok(list(elem))
}
Ast::InlineText(elems) => {
for e in elems.iter() {
self.check_itext(env, e)?;
}
Ok(t_inline_text())
}
Ast::BlockText(elems) => {
for e in elems.iter() {
self.check_btext(env, e)?;
}
Ok(t_block_text())
}
Ast::MathText(elems) => {
for e in elems.iter() {
self.check_math_elem(env, e)?;
}
Ok(MonoType::Base(BaseType::MathText))
}
Ast::LetMutableIn(name, init, body) => {
let schemes =
self.infer_binding(env, BindingView::LetMutable { name: *name, init })?;
let inner = env.with_all(schemes, self.binding_stage(init));
self.infer(&inner, body)
}
Ast::Overwrite(name, span, value) => {
let t_ref = match self.staged(env, *name, Some(*span), "mutable variable")? {
Some(poly) => instantiate(poly, self.ctx.level()),
None => {
return Err(TypeError::simple(
Some(*span),
format!(
"internal error: unbound mutable variable '{}' reached the typechecker",
self.text(*name)
),
))
}
};
let inner = self.fresh();
self.unify_ctx(
&t_ref,
&reff(inner.clone()),
Some(*span),
&format!("the overwrite target '{}'", self.text(*name)),
)?;
let tvalue = self.infer(env, value)?;
self.unify_ctx(
&inner,
&tvalue,
ast_span(value).or(Some(*span)),
&format!("the overwrite value for '{}'", self.text(*name)),
)?;
Ok(t_unit())
}
Ast::WhileDo(cond, body) => {
let tc = self.infer(env, cond)?;
self.unify_ctx(&t_bool(), &tc, ast_span(cond), "the condition of 'while'")?;
let tb = self.infer(env, body)?;
self.unify_ctx(&t_unit(), &tb, ast_span(body), "the body of 'while'")?;
Ok(t_unit())
}
Ast::Sequential(a, b) => {
let ta = self.infer(env, a)?;
self.unify_ctx(
&t_unit(),
&ta,
ast_span(a),
"the left-hand side of 'before'",
)?;
self.infer(env, b)
}
Ast::AccessField(e, label, span) => {
let te = self.infer(env, e)?;
let field = self.fresh();
let rv = self.ctx.fresh_row_var();
let open_row = MonoType::Record(Row::Cons(
label.clone(),
Box::new(field.clone()),
Box::new(Row::Var(rv)),
));
self.unify_ctx(
&open_row,
&te,
Some(*span),
&format!("the field access '#{label}'"),
)?;
Ok(field)
}
Ast::UpdateField(base, label, value) => {
let tbase = self.infer(env, base)?;
let tvalue = self.infer(env, value)?;
let rv = self.ctx.fresh_row_var();
let open_row = MonoType::Record(Row::Cons(
label.clone(),
Box::new(tvalue),
Box::new(Row::Var(rv)),
));
self.unify_ctx(
&open_row,
&tbase,
ast_span(base),
&format!("the record update of '{label}'"),
)?;
Ok(tbase)
}
Ast::VersionScope(version, body) => {
self.install_additional_builtin_variants(*version);
let scoped = version_scoped_type_env(self.store, env, *version);
let saved = self.scoped_version.replace(*version);
let r = self.infer(&scoped, body);
self.scoped_version = saved;
r
}
Ast::ModuleScope(path, body) => {
let saved = std::mem::replace(&mut self.ctor_scope, path.clone());
let r = self.infer(env, body);
self.ctor_scope = saved;
r
}
}
}
fn lookup_ctor(&self, name: &str) -> Option<Rc<VariantDecl>> {
for k in (1..=self.ctor_scope.len()).rev() {
let key = format!("{}.{}", self.ctor_scope[..k].join("."), name);
if let Some(d) = self.ctors.get(&key) {
return Some(d.clone());
}
}
self.ctors.get(name).cloned()
}
fn infer_ctor(
&mut self,
env: &TypeEnv<'s>,
name: &str,
payload: Option<&Ast<'s>>,
expected_result: Option<&MonoType>,
) -> Result<MonoType, TypeError> {
let decl = self
.lookup_ctor(name)
.ok_or_else(|| TypeError::simple(None, format!("unknown constructor '{name}'")))?;
let args: Vec<MonoType> = (0..decl.params).map(|_| self.fresh()).collect();
let (payload_ty, result_ty) = decl.instantiate_ctor(name, &args).ok_or_else(|| {
TypeError::simple(
None,
format!("constructor '{name}' applied with the wrong number of type arguments"),
)
})?;
if let Some(expected) = expected_result {
self.unify_ctx(expected, &result_ty, None, &format!("constructor '{name}'"))?;
}
match (payload_ty, payload) {
(Some(expected), Some(actual)) => {
let actual_ty = self.infer(env, actual)?;
self.unify_ctx(
&expected,
&actual_ty,
ast_span(actual),
&format!("the payload of constructor '{name}'"),
)?;
}
(None, None) => {}
(Some(_), None) => {
return Err(TypeError::simple(
None,
format!("constructor '{name}' expects a payload but none was given"),
))
}
(None, Some(_)) => {
return Err(TypeError::simple(
None,
format!("constructor '{name}' takes no payload but one was given"),
))
}
}
Ok(result_ty)
}
fn bind_pattern(
&mut self,
env: TypeEnv<'s>,
pat: &Pattern<'s>,
ty: &MonoType,
) -> Result<TypeEnv<'s>, TypeError> {
match pat {
Pattern::Wild => Ok(env),
Pattern::Var(name) => Ok(env.with(*name, PolyType::mono(ty.clone()), self.stage)),
Pattern::Unit => {
self.unify_ctx(&t_unit(), ty, None, "a unit pattern")?;
Ok(env)
}
Pattern::Bool(_) => {
self.unify_ctx(&t_bool(), ty, None, "a boolean pattern")?;
Ok(env)
}
Pattern::Int(_) => {
self.unify_ctx(&t_int(), ty, None, "an integer pattern")?;
Ok(env)
}
Pattern::Str(_) => {
self.unify_ctx(&t_string(), ty, None, "a string pattern")?;
Ok(env)
}
Pattern::Tuple(pats) => {
let elem_tys: Vec<MonoType> = pats.iter().map(|_| self.fresh()).collect();
self.unify_ctx(&product(elem_tys.clone()), ty, None, "a tuple pattern")?;
let mut env = env;
for (p, t) in pats.iter().zip(elem_tys.iter()) {
env = self.bind_pattern(env, p, t)?;
}
Ok(env)
}
Pattern::EmptyList => {
let elem = self.fresh();
self.unify_ctx(&list(elem), ty, None, "an empty-list pattern")?;
Ok(env)
}
Pattern::Cons(head, tail) => {
let elem = self.fresh();
self.unify_ctx(&list(elem.clone()), ty, None, "a cons pattern")?;
let env = self.bind_pattern(env, head, &elem)?;
self.bind_pattern(env, tail, &list(elem))
}
Pattern::Ctor(name, payload) => {
let decl = self.lookup_ctor(name).ok_or_else(|| {
TypeError::simple(None, format!("unknown constructor '{name}' in a pattern"))
})?;
let args: Vec<MonoType> = (0..decl.params).map(|_| self.fresh()).collect();
let (payload_ty, result_ty) = decl.instantiate_ctor(name, &args).ok_or_else(|| {
TypeError::simple(
None,
format!(
"constructor '{name}' applied with the wrong number of type arguments in a pattern"
),
)
})?;
self.unify_ctx(
&result_ty,
ty,
None,
&format!("the constructor pattern '{name}'"),
)?;
match (payload_ty, payload) {
(Some(expected), Some(p)) => self.bind_pattern(env, p, &expected),
(None, None) => Ok(env),
(Some(_), None) => Err(TypeError::simple(
None,
format!(
"constructor pattern '{name}' expects a payload but none was given"
),
)),
(None, Some(_)) => Err(TypeError::simple(
None,
format!("constructor pattern '{name}' takes no payload but one was given"),
)),
}
}
Pattern::As(inner, name) => {
let env = self.bind_pattern(env, inner, ty)?;
Ok(env.with(*name, PolyType::mono(ty.clone()), self.stage))
}
}
}
fn check_itext(&mut self, env: &TypeEnv<'s>, it: &IText<'s>) -> Result<(), TypeError> {
match it {
IText::Text(_) | IText::CodeText(_) => Ok(()),
IText::Cmd { name, span, args } => {
let tcmd = match self.staged(env, *name, Some(*span), "inline command")? {
Some(poly) => instantiate(poly, self.ctx.level()),
None => {
return Err(TypeError::simple(
Some(*span),
format!(
"internal error: unbound inline command '{}' reached the typechecker",
self.text(*name)
),
))
}
};
match &*resolve(&tcmd) {
MonoType::InlineCmd(params) => {
self.check_cmd_args(env, self.text(*name), *span, ¶ms, args)
}
other => Err(TypeError::simple(
Some(*span),
format!(
"internal error: inline command '{}' does not have an \
inline-cmd type (found `{other}`)",
self.text(*name)
),
)),
}
}
IText::Embed { expr, span } => {
let te = self.infer(env, expr)?;
self.unify_ctx(
&t_inline_text(),
&te,
Some(*span),
"an inline-text '#…;' embed",
)?;
Ok(())
}
IText::EmbedMath { elems, span: _ } => {
for me in elems.iter() {
self.check_math_elem(env, me)?;
}
Ok(())
}
}
}
fn check_btext(&mut self, env: &TypeEnv<'s>, bt: &BText<'s>) -> Result<(), TypeError> {
match bt {
BText::Cmd { name, span, args } => {
let tcmd = match self.staged(env, *name, Some(*span), "block command")? {
Some(poly) => instantiate(poly, self.ctx.level()),
None => {
return Err(TypeError::simple(
Some(*span),
format!(
"internal error: unbound block command '{}' reached the typechecker",
self.text(*name)
),
))
}
};
match &*resolve(&tcmd) {
MonoType::BlockCmd(params) => {
self.check_cmd_args(env, self.text(*name), *span, ¶ms, args)
}
other => Err(TypeError::simple(
Some(*span),
format!(
"internal error: block command '{}' does not have a \
block-cmd type (found `{other}`)",
self.text(*name)
),
)),
}
}
BText::Embed { expr, span } => {
let te = self.infer(env, expr)?;
self.unify_ctx(
&t_block_text(),
&te,
Some(*span),
"a block-text '#…;' embed",
)?;
Ok(())
}
}
}
fn check_math_elem(&mut self, env: &TypeEnv<'s>, m: &MathElem<'s>) -> Result<(), TypeError> {
match m {
MathElem::Chars(_) => Ok(()),
MathElem::Group(elems) => {
for e in elems {
self.check_math_elem(env, e)?;
}
Ok(())
}
MathElem::Sub(base, script) | MathElem::Sup(base, script) => {
self.check_math_elem(env, base)?;
for e in script {
self.check_math_elem(env, e)?;
}
Ok(())
}
MathElem::Primes(base, _) => self.check_math_elem(env, base),
MathElem::Cmd { name, span, args } => {
let tcmd = match self.staged(env, *name, Some(*span), "math command")? {
Some(poly) => instantiate(poly, self.ctx.level()),
None => {
return Err(TypeError::simple(
Some(*span),
format!(
"internal error: unbound math command '{}' reached the typechecker",
self.text(*name)
),
))
}
};
match &*resolve(&tcmd) {
MonoType::MathCmd(params) => {
self.check_cmd_args(env, self.text(*name), *span, ¶ms, args)
}
other => Err(TypeError::simple(
Some(*span),
format!(
"internal error: math command '{}' does not have a \
math-cmd type (found `{other}`)",
self.text(*name)
),
)),
}
}
MathElem::Embed { expr, span } => {
let te = self.infer(env, expr)?;
self.unify_ctx(&t_math_text(), &te, Some(*span), "a math '#…' embed")?;
Ok(())
}
}
}
}
fn command_sigil(name: &str) -> Option<char> {
let local = name.rsplit('.').next().unwrap_or(name);
let mut chars = local.chars();
match chars.next() {
Some(c @ ('\\' | '+')) if chars.next().is_some_and(|c2| c2.is_ascii_alphabetic()) => {
Some(c)
}
_ => None,
}
}
fn peel_func_chain(ty: MonoType) -> (Vec<MonoType>, MonoType) {
let mut doms = Vec::new();
let mut cur = ty;
loop {
match resolve(&cur).into_owned() {
MonoType::Func(_row, dom, cod) => {
doms.push(*dom);
cur = *cod;
}
other => return (doms, other),
}
}
}
fn peel_func_chain_rows(ty: MonoType) -> (Vec<(Row, MonoType)>, MonoType) {
let mut slots = Vec::new();
let mut cur = ty;
loop {
match resolve(&cur).into_owned() {
MonoType::Func(row, dom, cod) => {
slots.push((*row, *dom));
cur = *cod;
}
other => return (slots, other),
}
}
}
fn harvest_slot(row: Row, dom: MonoType) -> CmdArgType {
let mut opt_labels: Vec<(String, MonoType)> = Vec::new();
let mut cur = resolve_row(&row).into_owned();
loop {
match cur {
Row::Empty => break,
Row::Var(_) => break,
Row::Cons(label, lty, rest) => {
opt_labels.push((label, *lty));
cur = resolve_row(&rest).into_owned();
}
}
}
opt_labels.sort_by(|a, b| a.0.cmp(&b.0));
labeled(opt_labels, dom)
}
pub(crate) fn ast_span<'s>(ast: &Ast<'s>) -> Option<Span> {
match ast {
Ast::Var(_, span) => Some(*span),
Ast::Overwrite(_, span, _) => Some(*span),
Ast::AccessField(_, _, span) => Some(*span),
Ast::VersionScope(_, inner) => ast_span(inner),
Ast::ModuleScope(_, inner) => ast_span(inner),
_ => None,
}
}
pub fn typecheck_verbose<'s>(program: &Program<'s>) -> Result<Vec<MatchWarning>, TypeError> {
typecheck_verbose_with_version(program, RustyfiVersion::V0_0)
}
pub fn typecheck_verbose_with_version<'s>(
program: &Program<'s>,
version: RustyfiVersion,
) -> Result<Vec<MatchWarning>, TypeError> {
let mut checker = Checker::new_with_version(program, version)?;
let env = base_type_env_with_version(checker.store, version);
checker.infer(&env, &program.body)?;
Ok(checker.warnings)
}
pub fn typecheck<'s>(program: &Program<'s>) -> Result<(), TypeError> {
typecheck_with_version(program, RustyfiVersion::V0_0)
}
pub fn typecheck_with_version<'s>(
program: &Program<'s>,
version: RustyfiVersion,
) -> Result<(), TypeError> {
typecheck_verbose_with_version(program, version).map(|_warnings| ())
}
#[cfg(test)]
mod l3_per_binding_tests {
use super::*;
use crate::{elaborate, primitives};
fn elaborate_src<'s>(store: &'s SymbolStore, src: &str) -> Program<'s> {
let file = rustyfi_syntax::parse_file(src).expect("parse failed");
let env = primitives::base_env();
let scope = elaborate::Scope::new(store, env.names());
elaborate::elaborate_program(&file, &scope).expect("elaborate failed")
}
fn drive_manually<'s>(
program: &Program<'s>,
version: RustyfiVersion,
) -> Result<Vec<MatchWarning>, TypeError> {
let mut checker = Checker::new_with_version(program, version)?;
let mut env = base_type_env_with_version(program.store, version);
let mut ast: &Ast<'s> = &program.body;
loop {
ast = match ast {
Ast::LetIn(name, value, body) => {
let schemes =
checker.infer_binding(&env, BindingView::Let { name: *name, value })?;
env = env.with_all(schemes, checker.binding_stage(value));
body
}
Ast::LetMathIn(name, value, body) => {
let schemes =
checker.infer_binding(&env, BindingView::LetMath { name: *name, value })?;
env = env.with_all(schemes, checker.binding_stage(value));
body
}
Ast::LetRecIn(bindings, body) => {
let schemes = checker.infer_binding(&env, BindingView::LetRec(bindings))?;
env = env.with_all(schemes, checker.binding_stage_rec(bindings));
body
}
Ast::LetMutableIn(name, init, body) => {
let schemes = checker
.infer_binding(&env, BindingView::LetMutable { name: *name, init })?;
env = env.with_all(schemes, checker.binding_stage(init));
body
}
other => {
checker.infer_expr(&env, other)?;
break;
}
};
}
Ok(checker.take_warnings())
}
fn assert_equivalent(src: &str) {
let version = RustyfiVersion::V0_0;
let store = SymbolStore::new();
let program = elaborate_src(&store, src);
let whole = typecheck_verbose_with_version(&program, version);
let manual = drive_manually(&program, version);
match (whole, manual) {
(Ok(w1), Ok(w2)) => {
assert_eq!(w1, w2, "warnings differ for {src:?}");
}
(Err(e1), Err(e2)) => {
assert_eq!(
format!("{e1}"),
format!("{e2}"),
"error strings differ for {src:?}"
);
}
(Ok(w), Err(e)) => panic!(
"{src:?}: whole-program accepted (warnings={w:?}), manual drive rejected: {e}"
),
(Err(e), Ok(w)) => panic!(
"{src:?}: whole-program rejected ({e}), manual drive accepted (warnings={w:?})"
),
}
}
#[test]
fn per_binding_drive_matches_whole_program_across_binding_kinds() {
let cases: &[&str] = &[
"let x = 1 in x + 1",
"let x = 1 in x + true", "let id = fun x -> x in (id 1, id true)",
"let-inline ctx \\emph it = read-inline ctx it
in
{ \\emph{ ok } }",
"let-inline ctx \\bad = ctx + 1
in
()", "let-block ctx +p it = line-break true true ctx (read-inline ctx it)
in
'< +p{ ok } >",
"let-block ctx +duo a b = read-block ctx a
in
'< +duo{x} >", "let-math \\g m = ${#m#m} in 0",
"let-math \\f = 3 in 0", "let-rec is-even n = if n == 0 then true else is-odd (n - 1)
and is-odd n = if n == 0 then false else is-even (n - 1)
in
is-even 4",
"let-rec f n = if n == 0 then 0 else (f true)
in
f 1", "let-mutable x <- 0
in
(x <- 5)",
"let-mutable r <- []
in
((r <- (1 :: !r)) before (r <- (true :: !r)))", "match Some 1 with
| Some n -> n
| None -> 0",
];
for src in cases {
assert_equivalent(src);
}
}
#[test]
fn session_incrementality_declare_variant_affects_only_later_bindings() {
let store = SymbolStore::new();
let program = elaborate_src(&store, "type t = | A of int in 0");
assert_eq!(program.type_decls.len(), 1);
let decl = &program.type_decls[0];
let mut checker = Checker::empty(&store);
checker.install_builtin_variants(RustyfiVersion::V0_0);
let env = base_type_env_with_version(&store, RustyfiVersion::V0_0);
let a_payload = Ast::Ctor("A".to_string(), Some(Box::new(Ast::Int(1))));
let before = checker
.infer_binding(
&env,
BindingView::Let {
name: store.intern("before"),
value: &a_payload,
},
)
.expect_err("`A` should be unknown before declare_variant");
assert_eq!(format!("{before}"), "unknown constructor 'A'");
let nosuch_payload = Ast::Ctor("NoSuchCtor".to_string(), None);
let genuinely_unknown = checker
.infer_binding(
&env,
BindingView::Let {
name: store.intern("n"),
value: &nosuch_payload,
},
)
.expect_err("a genuinely undeclared ctor should also fail");
assert_eq!(
format!("{genuinely_unknown}"),
"unknown constructor 'NoSuchCtor'"
);
checker
.declare_variant(decl)
.expect("declare_variant should succeed");
let after = checker.infer_binding(
&env,
BindingView::Let {
name: store.intern("after"),
value: &a_payload,
},
);
assert!(
after.is_ok(),
"A(1) should typecheck after declare_variant: {after:?}"
);
}
}
#[cfg(test)]
mod x2b_shadow_tests {
use super::*;
#[test]
fn version_scope_does_not_clobber_a_user_shadowed_primitive() {
assert!(
PRIMITIVE_NAMES.contains(&"page-break"),
"fixture assumption: page-break must be a PRIMITIVE_NAMES member"
);
let span = Span::default();
let store = SymbolStore::new();
let page_break = store.intern("page-break");
let ast = Ast::LetIn(
page_break,
Box::new(Ast::Int(42)),
Box::new(Ast::VersionScope(
RustyfiVersion::V0_0,
Box::new(Ast::Var(page_break, span)),
)),
);
let program = Program {
type_decls: Vec::new(),
synonym_decls: Vec::new(),
body: ast,
store: &store,
};
let mut checker = Checker::new_with_version(&program, RustyfiVersion::V0_1)
.expect("checker construction over an empty-decls program should succeed");
let env = base_type_env_with_version(&store, RustyfiVersion::V0_1);
let ty = checker.infer(&env, &program.body).unwrap_or_else(|e| {
panic!(
"inferring the version-scoped `Var` over the user's shadowed \
`page-break = 42` binding should type-check as `int`, not error: {e}"
)
});
assert!(
matches!(ty, MonoType::Base(BaseType::Int)),
"the VersionScope env swap must respect the user's `page-break` shadow \
(expected MonoType::Base(BaseType::Int), got {ty:?} instead) — a \
MonoType::Func here would mean version_scoped_type_env re-stomped the \
user binding with V0_0's builtin page-break scheme"
);
}
#[test]
fn version_scope_still_resolves_unshadowed_forked_primitive() {
let span = Span::default();
let store = SymbolStore::new();
let ast = Ast::VersionScope(
RustyfiVersion::V0_0,
Box::new(Ast::Var(store.intern("page-break"), span)),
);
let program = Program {
type_decls: Vec::new(),
synonym_decls: Vec::new(),
body: ast,
store: &store,
};
let mut checker = Checker::new_with_version(&program, RustyfiVersion::V0_1)
.expect("checker construction over an empty-decls program should succeed");
let env = base_type_env_with_version(&store, RustyfiVersion::V0_1);
let ty = checker.infer(&env, &program.body).unwrap_or_else(|e| {
panic!(
"an unshadowed page-break reference inside a VersionScope should still \
type-check (X2a's original capability, unaffected by X2b): {e}"
)
});
assert!(
matches!(ty, MonoType::Func(..)),
"page-break (unshadowed) inside a VersionScope should still resolve to its \
builtin (function-typed) scheme, got {ty:?} instead — the X2b shadow guard \
must not have blocked this NON-shadowed overwrite"
);
}
}
#[cfg(test)]
mod sig_constraint_tests {
use super::*;
use rustyfi_syntax::cst::{SigAnnot, TopBinding};
fn parse_module_sig(src: &str) -> SigAnnot {
let file = rustyfi_syntax::parse_file(src).expect("parse failed");
for b in &file.prelude {
if let TopBinding::Module { sig: Some(sig), .. } = b {
return sig.clone();
}
}
panic!("no `module .. : sig .. end` found in {src:?}");
}
#[test]
fn constraint_suffix_lowers_to_a_kind_record_bound_on_its_tyvar() {
let sig = parse_module_sig(
"module M : sig\n\
val document : 'a -> config ?-> block-text -> document\n\
constraint 'a :: (| title : inline-text; author : inline-text |)\n\
end = struct\n\
let document x c bt = bt\n\
end",
);
let mut ctx = TypeContext::new();
let mut saw_record_kind = false;
for item in &sig.items {
let (name, ty) =
lower_sig_item(item, &mut ctx, RustyfiVersion::V0_0).expect("a value item");
assert_eq!(name, "document");
if let MonoType::Func(_row, dom, _) = &ty {
if let MonoType::Var(v) = &**dom {
if let Kind::Record(labels) = v.kind() {
saw_record_kind = true;
let expected: BTreeSet<String> =
["title", "author"].iter().map(|s| s.to_string()).collect();
assert_eq!(labels, expected);
}
}
}
}
assert!(
saw_record_kind,
"expected 'a's fresh variable to carry a Kind::Record bound"
);
}
#[test]
fn kind_record_bound_accepts_a_row_with_every_required_label() {
let mut ctx = TypeContext::new();
let labels: BTreeSet<String> = ["title", "author"].iter().map(|s| s.to_string()).collect();
let v = ctx.fresh_var_with_kind(Kind::Record(labels));
let constrained = MonoType::Var(v);
let full = MonoType::Record(Row::Cons(
"title".to_string(),
Box::new(t_inline_text()),
Box::new(Row::Cons(
"author".to_string(),
Box::new(t_inline_text()),
Box::new(Row::Empty),
)),
));
unify(&constrained, &full).expect("row has both required labels");
}
#[test]
fn kind_record_bound_rejects_a_row_missing_a_required_label() {
let mut ctx = TypeContext::new();
let labels: BTreeSet<String> = ["title", "author"].iter().map(|s| s.to_string()).collect();
let v = ctx.fresh_var_with_kind(Kind::Record(labels));
let constrained = MonoType::Var(v);
let missing_author = MonoType::Record(Row::Cons(
"title".to_string(),
Box::new(t_inline_text()),
Box::new(Row::Empty),
));
let err = unify(&constrained, &missing_author)
.expect_err("row is missing the required 'author' label");
assert!(
format!("{err:?}").contains("author"),
"error should name the missing label: {err:?}"
);
}
#[test]
fn real_stdja_sig_block_lowers_every_item_to_a_monotype() {
let sig = parse_module_sig(
"module StdJa : sig\n\
val default-config : config\n\
val document : 'a -> config ?-> block-text -> document\n\
constraint 'a :: (|\n\
title : inline-text;\n\
author : inline-text;\n\
show-toc : bool;\n\
show-title : bool;\n\
|)\n\
val font-latin-roman : string * float * float\n\
direct \\ref : [string] inline-cmd\n\
direct \\ref-page : [string] inline-cmd\n\
direct \\figure : [inline-text; block-text] inline-cmd\n\
direct +p : [inline-text] block-cmd\n\
direct +pn : [inline-text] block-cmd\n\
direct +section : [string?; string?; inline-text; block-text] block-cmd\n\
direct +subsection : [string?; string?; inline-text; block-text] block-cmd\n\
direct \\emph : [inline-text] inline-cmd\n\
end = struct\n\
end",
);
let mut ctx = TypeContext::new();
let mut names = Vec::new();
for item in &sig.items {
let (name, _ty) =
lower_sig_item(item, &mut ctx, RustyfiVersion::V0_0).expect("a value item");
names.push(name);
}
assert_eq!(
names,
vec![
"default-config",
"document",
"font-latin-roman",
"\\ref",
"\\ref-page",
"\\figure",
"+p",
"+pn",
"+section",
"+subsection",
"\\emph",
]
);
}
}