diff --git a/core/src/core_check.rs b/core/src/core_check.rs index 96bd928..447311a 100644 --- a/core/src/core_check.rs +++ b/core/src/core_check.rs @@ -18,7 +18,7 @@ use crate::core_term::{ Atom, CoreConstructor, CoreLit, CoreMatchCase, CoreNative, CoreTerm, DebugName, MetaId, close, - close_n, open_with, + close_n, open_with, permute_binders, }; use crate::core_unify::{MetaContext, UnifyError, force, instantiate, open_n, unify}; use crate::term::{Identifier, ModulePath, Multiplicity, TypeConstraint}; @@ -342,6 +342,138 @@ fn match_case_field_types( ) } +/// Resolved shape of a field-pattern match case (`plans/implementations/ +/// struct-field-destructuring.md`), computed once per case and reused by +/// both `infer`/`check` (read-only — just need each WRITTEN-order +/// pattern binder's real field TYPE, to type-check the case body +/// correctly) and `desugar_struct_literals` (which additionally rebuilds +/// the case itself onto declared order, via `core_term::permute_binders` +/// — see that function's own doc comment for why the body's binder order +/// needs retargeting at all, not just its types). +struct ResolvedFieldPattern { + /// The real constructor name — for a bare (`{ .. }`) case this is NEVER + /// `case.name` (the parser's `id("")` placeholder): `lower_core_ir.rs`'s + /// tag dispatch and `MetaContext::record_match_resolution`'s own name + /// list both need the real name to route/find this case correctly. + resolved_name: Identifier, + /// Declared-order field names, parallel to `declared_field_tys`. + declared_field_names: Vec, + /// Declared-order field types, already substituted for the scrutinee's + /// own concrete type args (same shape `match_case_field_types` itself + /// returns) — `None` under the same rare condition that function + /// returns `None` for (the inductive's own type-param arity doesn't + /// match what's on hand); callers fall back to `Hole` per field, same + /// as the pre-existing positional-case path already does. + declared_field_tys: Option>, + /// `written_to_declared[w]` = the declared-order position that WRITTEN + /// pattern position `w` (`case.field_pattern.unwrap().fields[w]`) fills. + written_to_declared: Vec, +} + +/// Resolve `case` (`case.field_pattern` must be `Some`) against +/// `scrutinee_ty`: pick the target constructor (the scrutinee's sole +/// constructor for a bare pattern, `case.name` directly for a named one), +/// require every one of its params to be named, and match the pattern's +/// written fields against the constructor's declared ones — unknown +/// field, duplicate field, and (without a trailing `..`) uncovered field +/// are all real errors here, not soft failures, matching every other +/// `InferError` this checker already raises for a malformed program. +fn resolve_field_pattern_case( + mctx: &mut MetaContext, + structs: &StructFields, + scrutinee_ty: &CoreTerm, + case: &CoreMatchCase, +) -> Result { + let fp = case + .field_pattern + .as_ref() + .expect("resolve_field_pattern_case: caller must check field_pattern.is_some() first"); + let forced = instantiate_foralls(mctx, structs, scrutinee_ty); + let inductive_atom = + head_atom_of(mctx, &forced).ok_or(InferError::FieldPatternUnresolvedScrutinee)?; + let (resolved_name, info): (Identifier, &ConstructorInfo) = if case.name.as_str().is_empty() { + let mut candidates = structs + .constructors + .iter() + .filter(|((atom, _), _)| *atom == inductive_atom); + let first = candidates.next(); + let second = candidates.next(); + match (first, second) { + (Some(((_, name), info)), None) => (name.clone(), info), + _ => { + let mut names: Vec = structs + .constructors + .iter() + .filter(|((atom, _), _)| *atom == inductive_atom) + .map(|((_, name), _)| name.clone()) + .collect(); + names.sort(); + return Err(InferError::FieldPatternAmbiguousConstructor { + inductive: inductive_atom, + candidates: names, + }); + } + } + } else { + let info = structs + .constructors + .get(&(inductive_atom, case.name.clone())) + .ok_or_else(|| InferError::FieldPatternUnknownConstructor { + inductive: inductive_atom, + name: case.name.clone(), + })?; + (case.name.clone(), info) + }; + if info.field_names.iter().any(|n| n.as_str().is_empty()) { + return Err(InferError::FieldPatternConstructorNotAllNamed { + constructor: resolved_name, + }); + } + let arity = info.field_names.len(); + let mut written_to_declared: Vec = Vec::with_capacity(fp.fields.len()); + let mut covered = vec![false; arity]; + for (field_name, _binder) in &fp.fields { + let d = info + .field_names + .iter() + .position(|n| n == field_name) + .ok_or_else(|| InferError::FieldPatternUnknownField { + constructor: resolved_name.clone(), + field: field_name.clone(), + })?; + if covered[d] { + return Err(InferError::FieldPatternDuplicateField { + constructor: resolved_name.clone(), + field: field_name.clone(), + }); + } + covered[d] = true; + written_to_declared.push(d); + } + if !fp.rest { + let missing: Vec = info + .field_names + .iter() + .zip(covered.iter()) + .filter(|(_, c)| !**c) + .map(|(n, _)| n.clone()) + .collect(); + if !missing.is_empty() { + return Err(InferError::FieldPatternMissingFields { + constructor: resolved_name, + fields: missing, + }); + } + } + let declared_field_tys = match_case_field_types(mctx, structs, scrutinee_ty, &resolved_name); + Ok(ResolvedFieldPattern { + resolved_name, + declared_field_names: info.field_names.clone(), + declared_field_tys, + written_to_declared, + }) +} + /// What a class method's own atom needs, to resolve a call site to a /// concrete instance: which class it belongs to, the (single, for now — /// see `desugar_struct_literals`'s class-method arm) class-level type @@ -464,6 +596,49 @@ pub enum InferError { target: Atom, field: Identifier, }, + /// `plans/implementations/struct-field-destructuring.md`: a bare `{ + /// .. }` match-case/parameter pattern's scrutinee type doesn't resolve + /// to a registered inductive at all (an ordinary type-error case would + /// normally already have been caught elsewhere; this is the fallback + /// when resolution genuinely can't identify ANY candidate). + FieldPatternUnresolvedScrutinee, + /// A bare `{ .. }` pattern's scrutinee inductive has zero or more than + /// one constructor — `candidates` lists every constructor found (empty + /// only if the inductive itself has none, which shouldn't happen for a + /// well-formed registration). + FieldPatternAmbiguousConstructor { + inductive: Atom, + candidates: Vec, + }, + /// A named `ConsName { .. }` pattern's `ConsName` isn't a real + /// constructor of the scrutinee's resolved inductive. + FieldPatternUnknownConstructor { + inductive: Atom, + name: Identifier, + }, + /// The resolved constructor has at least one anonymous (unnamed) param + /// — `{ .. }` patterns require every param to be named; use the + /// existing positional pattern instead. + FieldPatternConstructorNotAllNamed { + constructor: Identifier, + }, + /// A `{ field, .. }` pattern named a field that isn't among the + /// resolved constructor's declared params. + FieldPatternUnknownField { + constructor: Identifier, + field: Identifier, + }, + /// The same field name appeared more than once in one pattern. + FieldPatternDuplicateField { + constructor: Identifier, + field: Identifier, + }, + /// Without a trailing `..`, every declared field of the resolved + /// constructor must be listed — `fields` names the ones that weren't. + FieldPatternMissingFields { + constructor: Identifier, + fields: Vec, + }, } impl From for InferError { @@ -946,7 +1121,26 @@ fn infer_lit( for case in cases { let arity = case.dbgs.len() as u32; let (atoms, opened_value) = crate::core_unify::open_n(&case.value, 0, arity); - let field_tys = match_case_field_types(mctx, structs, &scrutinee_ty, &case.name); + // A field-pattern case's `dbgs`/`atoms` are still in WRITTEN + // order at this point (`desugar_struct_literals` is what + // retargets them onto declared order — see + // `CoreMatchCase.field_pattern`'s own doc comment) — reindex + // `resolved.declared_field_tys` (declared order) into that same + // written order before the per-atom lookup below, which assumes + // `field_tys[i]` lines up with `atoms[i]`/`case.dbgs[i]`. + let field_tys: Option> = match &case.field_pattern { + Some(_) => { + let resolved = resolve_field_pattern_case(mctx, structs, &scrutinee_ty, case)?; + resolved.declared_field_tys.map(|declared| { + resolved + .written_to_declared + .iter() + .map(|&d| declared[d].clone()) + .collect() + }) + } + None => match_case_field_types(mctx, structs, &scrutinee_ty, &case.name), + }; let mut ctx2 = ctx.clone(); for (i, atom) in atoms.iter().enumerate() { let field_ty = field_tys @@ -1386,8 +1580,22 @@ pub fn check( let arity = case.dbgs.len() as u32; let (atoms, opened_value) = crate::core_unify::open_n(&case.value, 0, arity); // E2: see `infer`'s own `Match` arm for the full rationale — same - // real-field-types-instead-of-`Hole` substitution here too. - let field_tys = match_case_field_types(mctx, structs, &scrutinee_ty, &case.name); + // real-field-types-instead-of-`Hole` substitution here too. Same + // written-order reindexing for a field-pattern case too — see + // `infer`'s own `Match` arm for why. + let field_tys: Option> = match &case.field_pattern { + Some(_) => { + let resolved = resolve_field_pattern_case(mctx, structs, &scrutinee_ty, case)?; + resolved.declared_field_tys.map(|declared| { + resolved + .written_to_declared + .iter() + .map(|&d| declared[d].clone()) + .collect() + }) + } + None => match_case_field_types(mctx, structs, &scrutinee_ty, &case.name), + }; let mut ctx2 = ctx.clone(); for (i, atom) in atoms.iter().enumerate() { let field_ty = field_tys @@ -2238,6 +2446,7 @@ fn project_dict_field( cases: vec![CoreMatchCase { name: case_name, dbgs: vec![DebugName::Anonymous; fields.len()], + field_pattern: None, value: Box::new(CoreTerm::Bound(bound_index)), }], })) @@ -2971,8 +3180,32 @@ pub fn desugar_struct_literals( let scrutinee_atom = scrutinee_ty .as_ref() .and_then(|ty| resolve_match_inductive_atom(mctx, structs, ty)); + // A field-pattern case's `c.name` is the parser's `id("")` + // placeholder for the bare form — `record_match_resolution`'s own + // name list (below) and `lower_core_ir.rs`'s later by-name tag + // dispatch both need the REAL resolved constructor name instead, + // or a resolved bare-form case becomes unreachable at that later + // stage (matches neither a real constructor tag nor the `"_"` + // wildcard sentinel). Resolved here, once, ahead of the per-case + // rebuild below (which re-resolves independently — this function + // never persists cross-call state, matching its own "never + // mutates/re-derives independently" style elsewhere). + let case_names_for_resolution: Vec = cases + .iter() + .map(|c| { + if c.field_pattern.is_some() { + scrutinee_ty + .as_ref() + .and_then(|ty| resolve_field_pattern_case(mctx, structs, ty, c).ok()) + .map(|r| r.resolved_name) + .unwrap_or_else(|| c.name.clone()) + } else { + c.name.clone() + } + }) + .collect(); if let Some(atom) = scrutinee_atom { - mctx.record_match_resolution(cases.iter().map(|c| c.name.clone()).collect(), atom); + mctx.record_match_resolution(case_names_for_resolution, atom); // The resolved inductive atom is captured into `match_resolutions` // above, but nothing guarantees it also appears as a literal // `Free(atom)` node anywhere else in this def's own body — a @@ -2999,6 +3232,70 @@ pub fn desugar_struct_literals( cases: cases .iter() .map(|case| { + // A field-pattern case (`plans/implementations/ + // struct-field-destructuring.md`) needs its own dedicated + // path: its `dbgs`/`value` are still indexed in WRITTEN field + // order at this point (`lower_core.rs`'s first pass has no + // constructor-registration data to resolve declared order + // against — see `CoreMatchCase.field_pattern`'s own doc + // comment), so before the ordinary per-arg E2 machinery below + // can apply at all, this retargets the case onto the resolved + // constructor's true declared order via `permute_binders` + // (see ITS doc comment for why a straight reindex, not a + // re-lower, is what's needed here). + if case.field_pattern.is_some() + && let Some(resolved) = scrutinee_ty + .as_ref() + .and_then(|ty| resolve_field_pattern_case(mctx, structs, ty, case).ok()) + { + let old_n = case.dbgs.len() as u32; + let new_n = resolved.declared_field_names.len() as u32; + let mut depth_map = vec![0u32; old_n as usize]; + for (w, &d) in resolved.written_to_declared.iter().enumerate() { + let old_depth = old_n - 1 - w as u32; + let new_depth = new_n - 1 - d as u32; + depth_map[old_depth as usize] = new_depth; + } + let mut declared_dbgs = vec![DebugName::Anonymous; new_n as usize]; + for (w, &d) in resolved.written_to_declared.iter().enumerate() { + declared_dbgs[d] = case.dbgs[w].clone(); + } + let permuted_value = permute_binders(&case.value, 0, old_n, new_n, &depth_map); + let (atoms, opened_value) = open_n(&permuted_value, 0, new_n); + let field_tys = resolved.declared_field_tys; + let mut ctx2 = ctx.clone(); + for (i, atom) in atoms.iter().enumerate() { + let field_ty = field_tys + .as_ref() + .and_then(|f| f.get(atoms.len() - 1 - i)) + .cloned() + .unwrap_or(CoreTerm::Hole); + ctx2 = ctx2.extend(*atom, field_ty); + } + let d = desugar_struct_literals( + mctx, + &ctx2, + structs, + atom_paths, + known_class_methods, + known_instances, + dict_scope, + &opened_value, + expected, + ); + return CoreMatchCase { + name: resolved.resolved_name, + dbgs: declared_dbgs, + field_pattern: None, + value: Box::new(close_n(&d, 0, &atoms)), + }; + } + // Ordinary positional case (or — should be unreachable, since + // `check` already validated this exact case successfully + // before this function ever runs — a field-pattern case whose + // resolution unexpectedly failed here; `field_pattern` stays + // populated below so that stays visible/inspectable rather + // than silently masquerading as a resolved case). let arity = case.dbgs.len() as u32; let (atoms, opened_value) = open_n(&case.value, 0, arity); // E2: same real-field-types-instead-of-`Hole` substitution as @@ -3045,6 +3342,7 @@ pub fn desugar_struct_literals( CoreMatchCase { name: case.name.clone(), dbgs: case.dbgs.clone(), + field_pattern: case.field_pattern.clone(), value: Box::new(close_n(&d, 0, &atoms)), } }) @@ -3233,6 +3531,7 @@ pub fn desugar_struct_literals( cases: vec![CoreMatchCase { name: Identifier::new("mk".to_string()), dbgs: vec![DebugName::Anonymous; n], + field_pattern: None, value: Box::new(CoreTerm::Bound((n - 1 - idx) as u32)), }], }) diff --git a/core/src/core_check_module.rs b/core/src/core_check_module.rs index d739c74..78317c9 100644 --- a/core/src/core_check_module.rs +++ b/core/src/core_check_module.rs @@ -1671,7 +1671,14 @@ fn infer_error_location(e: &InferError) -> Option { | InferError::UnexpectedBound(_) | InferError::CannotInferHole | InferError::NamedCallUnknownField { .. } - | InferError::NamedCallMissingField { .. } => None, + | InferError::NamedCallMissingField { .. } + | InferError::FieldPatternUnresolvedScrutinee + | InferError::FieldPatternAmbiguousConstructor { .. } + | InferError::FieldPatternUnknownConstructor { .. } + | InferError::FieldPatternConstructorNotAllNamed { .. } + | InferError::FieldPatternUnknownField { .. } + | InferError::FieldPatternDuplicateField { .. } + | InferError::FieldPatternMissingFields { .. } => None, } } @@ -1709,6 +1716,62 @@ fn infer_error_to_type_error(e: InferError, atoms: &AtomTable) -> TypeError { render_atom(*target, atoms), field.as_str() ), + InferError::FieldPatternUnresolvedScrutinee => { + "cannot resolve `{ .. }`: the matched value's type isn't known here".to_string() + } + InferError::FieldPatternAmbiguousConstructor { + inductive, + candidates, + } => { + if candidates.is_empty() { + format!( + "`{}` has no constructors to destructure with `{{ .. }}`", + render_atom(*inductive, atoms) + ) + } else { + let names = candidates + .iter() + .map(|n| n.as_str()) + .collect::>() + .join(", "); + format!( + "`{{ .. }}` requires exactly one constructor, but `{}` has several ({}); use `ConsName {{ .. }}` instead", + render_atom(*inductive, atoms), + names + ) + } + } + InferError::FieldPatternUnknownConstructor { inductive, name } => format!( + "`{}` is not a constructor of `{}`", + name.as_str(), + render_atom(*inductive, atoms) + ), + InferError::FieldPatternConstructorNotAllNamed { constructor } => format!( + "constructor `{}` has an unnamed field; use the positional pattern instead of `{{ .. }}`", + constructor.as_str() + ), + InferError::FieldPatternUnknownField { constructor, field } => format!( + "constructor `{}` has no field named `{}`", + constructor.as_str(), + field.as_str() + ), + InferError::FieldPatternDuplicateField { constructor, field } => format!( + "field `{}` listed more than once in this `{}` pattern", + field.as_str(), + constructor.as_str() + ), + InferError::FieldPatternMissingFields { + constructor, + fields, + } => format!( + "`{}` pattern is missing field(s) {} (add `..` to discard them)", + constructor.as_str(), + fields + .iter() + .map(|f| format!("`{}`", f.as_str())) + .collect::>() + .join(", ") + ), }; TypeError::Generic(message, location.unwrap_or_default()) } @@ -3095,6 +3158,154 @@ mod test { ); } + // ------------------------------------------------------------------- + // Phase 2 of `plans/implementations/struct-field-destructuring.md`: + // type-checker elaboration for match-case field patterns. Runtime + // correctness (binder ORDER actually landing on the right values, not + // just type-checking) is covered separately by + // `core/tests/field_pattern_integration_test.rs`, which runs the full + // check -> lower -> evaluate pipeline -- these tests only exercise + // `check_module_source`, same scope as this file's other type-check + // unit tests. + // ------------------------------------------------------------------- + + const FP_SHAPE_SOURCE: &str = + "type Shape {\n circle (radius : F64),\n rectangle (width : F64) (height : F64)\n}\n"; + + #[test] + fn test_field_pattern_bare_struct_destructure_all() { + let env = ModuleCheckEnv::new(); + let source = "struct Point { x : I64, y : I64 }\ndef sum (p : Point) : I64 := match p { { x, y } => x + y }\n"; + let report = check_module_source(&env, source); + assert_eq!(report.defs.len(), 1); + assert!( + report.defs[0].result.is_ok(), + "expected pass, got {:?}", + report.defs[0].result + ); + } + + #[test] + fn test_field_pattern_bare_rename_and_rest() { + let env = ModuleCheckEnv::new(); + let source = "struct Rect { width : I64, height : I64 }\ndef left (r : Rect) : I64 := match r { { width := w, .. } => w }\n"; + let report = check_module_source(&env, source); + assert_eq!(report.defs.len(), 1); + assert!( + report.defs[0].result.is_ok(), + "expected pass, got {:?}", + report.defs[0].result + ); + } + + #[test] + fn test_field_pattern_named_multi_constructor() { + let env = ModuleCheckEnv::new(); + let source = format!( + "{FP_SHAPE_SOURCE}def area (s : Shape) : F64 := match s {{ circle {{ radius }} => radius, rectangle {{ width, height }} => width }}\n" + ); + let report = check_module_source(&env, &source); + assert_eq!(report.defs.len(), 1); + assert!( + report.defs[0].result.is_ok(), + "expected pass, got {:?}", + report.defs[0].result + ); + } + + #[test] + fn test_field_pattern_bare_form_on_multi_constructor_is_an_error() { + let env = ModuleCheckEnv::new(); + // Bare `{ .. }` requires exactly one constructor -- `Shape` has two. + let source = format!( + "{FP_SHAPE_SOURCE}def bad (s : Shape) : F64 := match s {{ {{ radius }} => radius }}\n" + ); + let report = check_module_source(&env, &source); + assert_eq!(report.defs.len(), 1); + let debug = format!("{:?}", report.defs[0].result); + assert!( + debug.contains("FieldPatternAmbiguousConstructor"), + "a bare pattern against a multi-constructor type must be rejected \ + by the NEW field-pattern check specifically, got {debug}" + ); + } + + #[test] + fn test_field_pattern_unknown_field_is_an_error() { + let env = ModuleCheckEnv::new(); + let source = + "struct Point { x : I64, y : I64 }\ndef bad (p : Point) : I64 := match p { { x, z } => x }\n"; + let report = check_module_source(&env, source); + assert_eq!(report.defs.len(), 1); + let debug = format!("{:?}", report.defs[0].result); + assert!( + debug.contains("FieldPatternUnknownField"), + "a typo'd field name must be rejected by the NEW field-pattern \ + check specifically, got {debug}" + ); + } + + #[test] + fn test_field_pattern_duplicate_field_is_an_error() { + let env = ModuleCheckEnv::new(); + let source = + "struct Point { x : I64, y : I64 }\ndef bad (p : Point) : I64 := match p { { x, x } => x }\n"; + let report = check_module_source(&env, source); + assert_eq!(report.defs.len(), 1); + let debug = format!("{:?}", report.defs[0].result); + assert!( + debug.contains("FieldPatternDuplicateField"), + "a field listed twice must be rejected, got {debug}" + ); + } + + #[test] + fn test_field_pattern_missing_field_without_rest_is_an_error() { + let env = ModuleCheckEnv::new(); + // `y` is neither listed nor discarded via `..`. + let source = + "struct Point { x : I64, y : I64 }\ndef bad (p : Point) : I64 := match p { { x } => x }\n"; + let report = check_module_source(&env, source); + assert_eq!(report.defs.len(), 1); + let debug = format!("{:?}", report.defs[0].result); + assert!( + debug.contains("FieldPatternMissingFields"), + "an uncovered field without `..` must be rejected, got {debug}" + ); + } + + #[test] + fn test_field_pattern_on_anonymous_param_constructor_is_an_error() { + let env = ModuleCheckEnv::new(); + // `write`'s sole param is anonymous (tuple-like) -- `{ .. }` isn't + // legal against it at all; use the positional pattern instead. + let source = "type Cmd {\n write (String)\n}\ndef bad (c : Cmd) : String := match c { write { .. } => \"\" }\n"; + let report = check_module_source(&env, &source); + assert_eq!(report.defs.len(), 1); + let debug = format!("{:?}", report.defs[0].result); + assert!( + debug.contains("FieldPatternConstructorNotAllNamed"), + "a field pattern against a constructor with an anonymous param must \ + be rejected, got {debug}" + ); + } + + #[test] + fn test_field_pattern_unknown_constructor_is_an_error() { + let env = ModuleCheckEnv::new(); + let source = format!( + "{FP_SHAPE_SOURCE}def bad (s : Shape) : F64 := match s {{ triangle {{ radius }} => radius, rectangle {{ width, height }} => width, circle {{ radius }} => radius }}\n" + ); + let report = check_module_source(&env, &source); + assert_eq!(report.defs.len(), 1); + let debug = format!("{:?}", report.defs[0].result); + assert!( + debug.contains("FieldPatternUnknownConstructor"), + "a named field pattern against a nonexistent constructor must be \ + rejected, got {debug}" + ); + } + // ------------------------------------------------------------------- // Phase 2 of `plans/implementations/named-field-construction.md`: // def-function-target named calls. diff --git a/core/src/core_term.rs b/core/src/core_term.rs index 5e28d67..54a4c1a 100644 --- a/core/src/core_term.rs +++ b/core/src/core_term.rs @@ -23,7 +23,7 @@ use std::fmt; use std::sync::atomic::{AtomicU64, Ordering}; use crate::Map; -use crate::term::{F64Wrap, Identifier, ModulePath, Multiplicity, NumSuffix}; +use crate::term::{F64Wrap, FieldPattern, Identifier, ModulePath, Multiplicity, NumSuffix}; // --------------------------------------------------------------------------- // DebugName — display-only, never used for identity @@ -189,6 +189,23 @@ impl AtomTable { pub struct CoreMatchCase { pub name: Identifier, pub dbgs: Vec, + /// `Some` only pre-elaboration — mirrors `crate::term::MatchCase`'s own + /// field (`plans/implementations/struct-field-destructuring.md`). + /// `lower_core.rs` carries a parsed `{ x, y } => ...`/`ConsName { x, y } + /// => ...` pattern through unresolved (it has no constructor- + /// registration data to resolve field names against); `dbgs`/`value` at + /// that point are pushed/indexed in the pattern's WRITTEN field order + /// (the only order available pre-type-checking), NOT the target + /// constructor's declared order. `core_check.rs`'s `desugar_struct_ + /// literals` (the pass whose OUTPUT actually gets lowered/evaluated -- + /// `infer`/`check` never mutate, see `raise_core.rs`'s module doc) + /// resolves this once the scrutinee's real type is known, rewriting + /// `dbgs`/`value` into the constructor's true declared order (via + /// `permute_binders`, below) and clearing this back to `None` — so + /// every OTHER consumer (`eval.rs`, `lower_core_ir.rs`) only ever sees + /// `None` here, exactly as `crate::term::MatchCase::field_pattern`'s own + /// doc comment describes for the parser-level type. + pub field_pattern: Option, pub value: Box, } @@ -666,6 +683,7 @@ fn open_at_lit(lit: &CoreLit, depth: u32, replacement: &CoreTerm) -> CoreLit { .map(|c| CoreMatchCase { name: c.name.clone(), dbgs: c.dbgs.clone(), + field_pattern: c.field_pattern.clone(), value: Box::new(open_at(&c.value, depth + c.dbgs.len() as u32, replacement)), }) .collect(), @@ -790,6 +808,7 @@ fn close_at_lit(lit: &CoreLit, depth: u32, atom: Atom) -> CoreLit { .map(|c| CoreMatchCase { name: c.name.clone(), dbgs: c.dbgs.clone(), + field_pattern: c.field_pattern.clone(), value: Box::new(close_at(&c.value, depth + c.dbgs.len() as u32, atom)), }) .collect(), @@ -837,6 +856,189 @@ pub(crate) fn close_n(term: &CoreTerm, depth: u32, atoms: &[Atom]) -> CoreTerm { current } +// --------------------------------------------------------------------------- +// Binder permutation — the one piece of *general* index arithmetic this +// representation otherwise avoids (see this section's own header comment +// above `open_at`). Needed by `plans/implementations/ +// struct-field-destructuring.md`'s field-pattern elaboration specifically: +// a match arm's body is de-Bruijn-indexed once, at `lower_core.rs`'s +// syntactic first pass, against whatever field order is available THEN -- +// for `{ x, y } => ...`, that's the pattern's WRITTEN order (the only one +// knowable before any constructor is resolved). The runtime, however, +// always binds a matched constructor's fields POSITIONALLY in its +// DECLARED order (`core_eval.rs`'s `CoreLit::Match` handling: "fields are +// pushed in their natural (declaration) order"), which is only knowable +// once the scrutinee's type is inferred -- at `core_check.rs`'s `Match` +// handling, by which point the body's indices are already fixed relative +// to written order. `permute_binders` bridges the two: once elaboration +// knows the declared order, it retargets the ALREADY-INDEXED body from +// written order onto declared order directly, rather than needing to +// re-lower from scratch. +// --------------------------------------------------------------------------- + +/// Permute (and, when `new_n > old_n`, widen with fresh discard slots) the +/// innermost `old_n` `Bound` indices of `term`, mapping old absolute depth +/// `d` (`d < old_n`, relative to `cutoff`) to `depth_map[d as usize]` (a +/// new absolute depth `< new_n`, also relative to `cutoff`) -- +/// `depth_map` must be injective (no two old depths mapping to the same +/// new one); any new depth in `0..new_n` absent from `depth_map`'s image +/// is a fresh, necessarily-unreferenced slot (the caller's own +/// `CoreMatchCase.dbgs` gets a matching discard entry for it -- a +/// declared field elided from the pattern via `..`, which the body could +/// never have mentioned in the first place, since the parser has no name +/// for it). +/// +/// A `Bound` referring to a binder introduced BELOW this frame (index `< +/// cutoff`, i.e. more local than what's being permuted) is left +/// completely untouched. A `Bound` referring to a binder OUTSIDE this +/// frame (index `>= cutoff + old_n`) shifts by `new_n - old_n`, to keep +/// reaching the same outer binder now that this frame holds `new_n` slots +/// instead of `old_n`. Call with `cutoff: 0` at the match arm's own body; +/// the recursion grows `cutoff` by however many further binders each node +/// introduces while descending, exactly mirroring `open_at`'s own `depth` +/// threading (including its `Lit::Match` arm, which grows by a NESTED +/// case's own `dbgs.len()` -- a case fully inside the body being permuted +/// here, unrelated to the `old_n`/`new_n` frame this call is retargeting). +pub(crate) fn permute_binders( + term: &CoreTerm, + cutoff: u32, + old_n: u32, + new_n: u32, + depth_map: &[u32], +) -> CoreTerm { + match term { + CoreTerm::Bound(i) if *i < cutoff => term.clone(), + CoreTerm::Bound(i) if *i < cutoff + old_n => { + let local = *i - cutoff; + CoreTerm::Bound(cutoff + depth_map[local as usize]) + } + CoreTerm::Bound(i) => CoreTerm::Bound(i + (new_n - old_n)), + CoreTerm::Free(_) | CoreTerm::Meta(_) | CoreTerm::Sort { .. } | CoreTerm::Hole => term.clone(), + CoreTerm::Forall { dbg, typ, body } => CoreTerm::Forall { + dbg: dbg.clone(), + typ: Box::new(permute_binders(typ, cutoff, old_n, new_n, depth_map)), + body: Box::new(permute_binders(body, cutoff + 1, old_n, new_n, depth_map)), + }, + CoreTerm::Pi { + dbg, + arg, + ret, + mult, + } => CoreTerm::Pi { + dbg: dbg.clone(), + arg: Box::new(permute_binders(arg, cutoff, old_n, new_n, depth_map)), + ret: Box::new(permute_binders(ret, cutoff + 1, old_n, new_n, depth_map)), + mult: mult.clone(), + }, + CoreTerm::Lam { + dbg, + param_typ, + body, + } => CoreTerm::Lam { + dbg: dbg.clone(), + param_typ: Box::new(permute_binders(param_typ, cutoff, old_n, new_n, depth_map)), + body: Box::new(permute_binders(body, cutoff + 1, old_n, new_n, depth_map)), + }, + CoreTerm::App { fun, arg } => CoreTerm::App { + fun: Box::new(permute_binders(fun, cutoff, old_n, new_n, depth_map)), + arg: Box::new(permute_binders(arg, cutoff, old_n, new_n, depth_map)), + }, + CoreTerm::Lit(lit) => CoreTerm::Lit(permute_binders_lit(lit, cutoff, old_n, new_n, depth_map)), + CoreTerm::Con(c) => CoreTerm::Con(CoreConstructor { + name: c.name.clone(), + typ_name: c.typ_name.clone(), + num_args: c.num_args, + args: permute_binders_args(&c.args, cutoff, old_n, new_n, depth_map), + }), + CoreTerm::Ntv(n) => CoreTerm::Ntv(CoreNative { + native_name: n.native_name.clone(), + num_args: n.num_args, + args: permute_binders_args(&n.args, cutoff, old_n, new_n, depth_map), + }), + CoreTerm::Ctx { loc, term } => CoreTerm::Ctx { + loc: loc.clone(), + term: Box::new(permute_binders(term, cutoff, old_n, new_n, depth_map)), + }, + } +} + +fn permute_binders_args( + args: &[Option], + cutoff: u32, + old_n: u32, + new_n: u32, + depth_map: &[u32], +) -> Vec> { + args + .iter() + .map(|a| { + a.as_ref() + .map(|t| permute_binders(t, cutoff, old_n, new_n, depth_map)) + }) + .collect() +} + +fn permute_binders_lit( + lit: &CoreLit, + cutoff: u32, + old_n: u32, + new_n: u32, + depth_map: &[u32], +) -> CoreLit { + match lit { + CoreLit::Str { .. } | CoreLit::Char { .. } | CoreLit::Num { .. } | CoreLit::Float { .. } => { + lit.clone() + } + CoreLit::Match { scrutinee, cases } => CoreLit::Match { + scrutinee: Box::new(permute_binders(scrutinee, cutoff, old_n, new_n, depth_map)), + cases: cases + .iter() + .map(|c| CoreMatchCase { + name: c.name.clone(), + dbgs: c.dbgs.clone(), + field_pattern: c.field_pattern.clone(), + value: Box::new(permute_binders( + &c.value, + cutoff + c.dbgs.len() as u32, + old_n, + new_n, + depth_map, + )), + }) + .collect(), + }, + CoreLit::If { cond, then, els } => CoreLit::If { + cond: Box::new(permute_binders(cond, cutoff, old_n, new_n, depth_map)), + then: Box::new(permute_binders(then, cutoff, old_n, new_n, depth_map)), + els: Box::new(permute_binders(els, cutoff, old_n, new_n, depth_map)), + }, + CoreLit::StructLit { fields, type_name } => CoreLit::StructLit { + fields: fields + .iter() + .map(|(k, v)| { + ( + k.clone(), + permute_binders(v, cutoff, old_n, new_n, depth_map), + ) + }) + .collect(), + type_name: *type_name, + }, + CoreLit::StructUpdate { base, fields } => CoreLit::StructUpdate { + base: Box::new(permute_binders(base, cutoff, old_n, new_n, depth_map)), + fields: fields + .iter() + .map(|(k, v)| { + ( + k.clone(), + permute_binders(v, cutoff, old_n, new_n, depth_map), + ) + }) + .collect(), + }, + } +} + /// Replace every occurrence of `Meta(target)` with `replacement` /// throughout `term`. No index arithmetic is needed (unlike `open`/ /// `close`): a metavariable's solution is only ever built out of atoms @@ -923,6 +1125,7 @@ fn subst_meta_lit(lit: &CoreLit, target: MetaId, replacement: &CoreTerm) -> Core .map(|c| CoreMatchCase { name: c.name.clone(), dbgs: c.dbgs.clone(), + field_pattern: c.field_pattern.clone(), value: Box::new(subst_meta(&c.value, target, replacement)), }) .collect(), @@ -1447,6 +1650,7 @@ mod test { cases: vec![CoreMatchCase { name: Identifier::new("cons".to_string()), dbgs: vec![named(a), named(t)], + field_pattern: None, value: Box::new(CoreTerm::Bound(1)), // refs the first pattern arg }], }) @@ -1465,6 +1669,7 @@ mod test { cases: vec![CoreMatchCase { name: Identifier::new("cons".to_string()), dbgs: vec![DebugName::Anonymous, DebugName::Anonymous], + field_pattern: None, value: Box::new(CoreTerm::Bound(2)), }], }); @@ -1497,6 +1702,7 @@ mod test { cases: vec![CoreMatchCase { name: Identifier::new("x".to_string()), dbgs: vec![], + field_pattern: None, value: Box::new(CoreTerm::Meta(m)), }], }); diff --git a/core/src/core_unify.rs b/core/src/core_unify.rs index 28653dd..5448181 100644 --- a/core/src/core_unify.rs +++ b/core/src/core_unify.rs @@ -819,6 +819,7 @@ fn zonk_lit(mctx: &MetaContext, lit: &CoreLit) -> CoreLit { .map(|c| CoreMatchCase { name: c.name.clone(), dbgs: c.dbgs.clone(), + field_pattern: c.field_pattern.clone(), value: Box::new(zonk(mctx, &c.value)), }) .collect(), @@ -936,6 +937,7 @@ fn close_meta_at_lit(lit: &CoreLit, depth: u32, target: MetaId) -> CoreLit { .map(|c| CoreMatchCase { name: c.name.clone(), dbgs: c.dbgs.clone(), + field_pattern: c.field_pattern.clone(), value: Box::new(close_meta_at(&c.value, depth + c.dbgs.len() as u32, target)), }) .collect(), @@ -1530,6 +1532,7 @@ mod test { CoreMatchCase { name: Identifier::new(name.to_string()), dbgs: (0..arity).map(|_| DebugName::Anonymous).collect(), + field_pattern: None, value: Box::new(value), } } diff --git a/core/src/eval/macro_expand.rs b/core/src/eval/macro_expand.rs index 52b7cfb..a8bc55b 100644 --- a/core/src/eval/macro_expand.rs +++ b/core/src/eval/macro_expand.rs @@ -4,7 +4,7 @@ use crate::term::{ AttrArg, Constructor, Decl, DeclGenDef, Def, Identifier, Inductive, Literal, ModulePath, NameRef, Named, Par, Param, SourceContext, Term::{self, Ann, App, Con, Ctx, Forall, Lam, Lit, Pi, Quote, Var}, - case, id, instance, match_term, mpvar, + case_with_optional_field_pattern, id, instance, match_term, mpvar, }; /// Names of the built-in macro-expansion reflection intrinsics — recognized @@ -850,7 +850,12 @@ fn expand_term( .into_iter() .map(|c| { let value = expand_term(*c.value, macro_defs, inductives, depth)?; - Ok(case(c.name, c.args, value)) + Ok(case_with_optional_field_pattern( + c.name, + c.args, + c.field_pattern, + value, + )) }) .collect::, MacroError>>()?; Ok(match_term(value, cases)) @@ -1003,7 +1008,12 @@ fn resolve_quote( .into_iter() .map(|c| { let value = resolve_quote(*c.value, macro_defs, inductives, depth)?; - Ok(case(c.name, c.args, value)) + Ok(case_with_optional_field_pattern( + c.name, + c.args, + c.field_pattern, + value, + )) }) .collect::, MacroError>>()?; Ok(match_term(value, cases)) @@ -1214,7 +1224,14 @@ fn rename_macro_var(term: Term, old: &Identifier, new: &Identifier) -> Term { let value = rename_macro_var(*value, old, new); let cases = cases .into_iter() - .map(|c| case(c.name, c.args, rename_macro_var(*c.value, old, new))) + .map(|c| { + case_with_optional_field_pattern( + c.name, + c.args, + c.field_pattern, + rename_macro_var(*c.value, old, new), + ) + }) .collect(); match_term(value, cases) } @@ -1339,7 +1356,14 @@ fn alpha_rename_body(term: Term) -> Term { let value = alpha_rename_body(*value); let cases = cases .into_iter() - .map(|c| case(c.name, c.args, alpha_rename_body(*c.value))) + .map(|c| { + case_with_optional_field_pattern( + c.name, + c.args, + c.field_pattern, + alpha_rename_body(*c.value), + ) + }) .collect(); match_term(value, cases) } @@ -1468,7 +1492,14 @@ fn subst_macro(term: Term, name: &NameRef, replacement: &Term) -> Term { let value = subst_macro(*value, name, replacement); let cases = cases .into_iter() - .map(|c| case(c.name, c.args, subst_macro(*c.value, name, replacement))) + .map(|c| { + case_with_optional_field_pattern( + c.name, + c.args, + c.field_pattern, + subst_macro(*c.value, name, replacement), + ) + }) .collect(); match_term(value, cases) } diff --git a/core/src/lower_core.rs b/core/src/lower_core.rs index e695568..a4fa1e8 100644 --- a/core/src/lower_core.rs +++ b/core/src/lower_core.rs @@ -441,20 +441,40 @@ fn lower_lit(ctx: &mut LowerContext, lit: &Literal) -> Result ...`/`ConsName { x, y } => + // ...`, `case.field_pattern: Some(fp)`, `plans/implementations/ + // struct-field-destructuring.md`) has an EMPTY `case.args` (see + // `term::case_with_field_pattern`) -- its real binders are + // `fp.fields`' own (possibly renamed/punned) binder names + // instead. Push those, in WRITTEN order (the only order + // available here -- this pass has no constructor-registration + // data to resolve the pattern's real declared field order + // against; see `CoreMatchCase.field_pattern`'s own doc comment). + // `core_check.rs`'s `desugar_struct_literals` retargets `dbgs`/ + // `value` onto the constructor's true declared order later, via + // `core_term::permute_binders` -- this pass only needs to get the + // body's OWN free-standing names bound to SOME consistent set of + // fresh local slots, or they'd wrongly resolve as free/global + // references instead (a field-pattern case's `args` being empty + // otherwise means this loop would push nothing at all). + let pattern_binders: Vec = match &case.field_pattern { + Some(fp) => fp.fields.iter().map(|(_, binder)| binder.clone()).collect(), + None => case.args.clone(), + }; + for a in &pattern_binders { ctx.push(a.clone()); } let value_c = lower_term(ctx, &case.value); - for _ in &case.args { + for _ in &pattern_binders { ctx.pop(); } out_cases.push(CoreMatchCase { name: case.name.clone(), - dbgs: case - .args + dbgs: pattern_binders .iter() .map(|a| DebugName::Named(a.clone())) .collect(), + field_pattern: case.field_pattern.clone(), value: Box::new(value_c?), }); } diff --git a/core/src/parser.rs b/core/src/parser.rs index 145b1a9..3d040be 100644 --- a/core/src/parser.rs +++ b/core/src/parser.rs @@ -460,6 +460,41 @@ fn lam_param(input: Span) -> Res { .parse(input) } +/// `lam_param`, but ALSO accepting a destructured form (`({ x, y } : +/// Type)`, requires an explicit type annotation -- same restriction +/// `def_param`'s own destructured alternative has, and for the same +/// reason: nothing else could resolve the pattern's target constructor +/// otherwise). `plans/implementations/struct-field-destructuring.md`'s +/// Phase 4 -- unlike Phase 3's `def_param`, this is NOT wired into +/// `lam_param` itself: `lam_param` has two OTHER call sites +/// (`class_parser`/`inductive_parser`) parsing a `class`/`type` +/// declaration's own GENERIC TYPE params, not value-level function +/// parameters -- destructuring a type variable is meaningless, so only +/// `lambda` (the actual `\x => ...` anonymous-function literal) gets +/// this alternative. Reuses `ParsedParam` (`def_param`'s own wrapper +/// type) rather than a duplicate lambda-specific one -- same shape, +/// same meaning. +fn lam_param_destructurable(input: Span) -> Res { + alt(( + map( + delimited( + (char('('), ws0), + separated_pair(struct_pattern_parser, ws0, type_annotation), + ( + ws0, + context("closing parenthesis for function parameter", char(')')), + ), + ), + |(fp, typ)| { + let name = Identifier::gensym("__struct_param"); + ParsedParam::Destructured(param(name, typ), fp) + }, + ), + map(lam_param, ParsedParam::Plain), + )) + .parse(input) +} + /// `#[arg]`-style attributes on a single named constructor parameter, e.g. /// `compile (#[arg] verbose : Bool)` — consumed by `#[derive_cli]` /// generation (`lang/cli.mo`'s `derive_cli_meta`). Only meaningful ahead of the @@ -553,26 +588,70 @@ fn implicit_params(input: Span) -> Res, X> { .parse(input) } -fn def_param(input: Span) -> Res, X> { - delimited( - (char('('), ws0), +/// A single `def`/`lam` parameter as parsed: either an ordinary explicit +/// param (`(x : T)`, unchanged), or a destructured one (`({ x, y } : T)`, +/// `plans/implementations/struct-field-destructuring.md`'s Phase 3) -- +/// paired with the `FieldPattern` a wrapping `match` needs to actually +/// bind `x`/`y` from the gensym'd `Param` this variant also carries. Kept +/// as a thin wrapper (rather than adding a pattern slot to `Param` itself) +/// so every OTHER `Param` consumer (`Pi`/`Lam` construction, `eval.rs` +/// substitution, ...) needs no changes at all — a `Destructured` entry's +/// own `Param` is an ordinary, real binder by the time it reaches any of +/// them; only `def_parser` (see below) ever inspects the `FieldPattern` +/// half, to wrap the body in one extra `match` per `Destructured` param +/// before building the final `Lam` chain. +#[derive(Debug, Clone, PartialEq)] +enum ParsedParam { + Plain(Param), + Destructured(Param, FieldPattern), +} + +fn def_param(input: Span) -> Res, X> { + alt(( + // Destructured: `({ x, y } : Type)` -- exactly one gensym'd `Param` + // (`Identifier::gensym`, same convention `raise_core.rs` uses for + // synthetic binder names) paired with the parsed `FieldPattern`. + // Reuses `struct_pattern_parser` (Phase 1's own match-case pattern + // grammar) verbatim -- same `{ field, other := binder, .. }` syntax, + // same reason to share the parser rather than duplicate it. Tried + // FIRST: `{` can never start `multiplicity_prefix`/`identifier`, so + // this never backtracks into (or is shadowed by) the plain + // alternative below. map( - pair( - multiplicity_prefix, - separated_pair(many1(terminated(identifier, ws0)), ws0, type_annotation), + delimited( + (char('('), ws0), + separated_pair(struct_pattern_parser, ws0, type_annotation), + ( + ws0, + context("closing parenthesis for function parameters", char(')')), + ), ), - |(mult, (ids, typ))| { - ids - .into_iter() - .map(|i| param_with_mult(i, typ.clone(), mult.clone())) - .collect() + |(fp, typ)| { + let name = Identifier::gensym("__struct_param"); + vec![ParsedParam::Destructured(param(name, typ), fp)] }, ), - ( - ws0, - context("closing parenthesis for function parameters", char(')')), + // Existing: `(mult id+ : Type)`, unchanged. + delimited( + (char('('), ws0), + map( + pair( + multiplicity_prefix, + separated_pair(many1(terminated(identifier, ws0)), ws0, type_annotation), + ), + |(mult, (ids, typ))| { + ids + .into_iter() + .map(|i| ParsedParam::Plain(param_with_mult(i, typ.clone(), mult.clone()))) + .collect() + }, + ), + ( + ws0, + context("closing parenthesis for function parameters", char(')')), + ), ), - ) + )) .parse(input) } /// A `def`'s own top-level parameter list, in EITHER of two spellings: @@ -599,7 +678,7 @@ fn def_param(input: Span) -> Res, X> { /// one field regardless -- so the boundary case needs no extra /// disambiguation logic in THIS function, only the (pre-existing, /// unchanged) ordering of `implicit_params` before `def_params`. -fn def_params(input: Span) -> Res, X> { +fn def_params(input: Span) -> Res, X> { alt(( // `terminated(.., ws0)`: mirrors the paren alternative's OWN trailing- // whitespace consumption below (`fold_many0(terminated(def_param, @@ -607,10 +686,21 @@ fn def_params(input: Span) -> Res, X> { // without this, the space between the closing `}` and this def's // `: ReturnType` annotation is left unconsumed, and `def_type_ // annotation` (which does NOT skip leading whitespace itself) fails - // immediately on it. + // immediately on it. This is the WHOLE-param-list brace-declaration + // convenience (`named-field-construction.md`'s own Phase 3) -- an + // entirely different feature from `def_param`'s OWN destructured + // alternative just above (that one destructures ONE parenthesized + // param's BINDER; this one spells the ENTIRE param list as one brace + // block, no parens, no destructuring) -- never ambiguous with it: this + // alternative only ever matches at the position `def_params` itself + // starts (never inside an already-open `(`), so a `({ x, y } : T)` + // destructured param can never be mistaken for it. terminated( map(struct_inner_parser, |fields: Vec| { - fields.into_iter().map(stru_field_to_def_param).collect() + fields + .into_iter() + .map(|f| ParsedParam::Plain(stru_field_to_def_param(f))) + .collect() }), ws0, ), @@ -678,12 +768,26 @@ fn application(input: Span) -> Res { fn lambda(input: Span) -> Res { let (input, _) = alt((tag("\\"), terminated(tag("fn"), ws1), tag("ꟛ"))).parse(input)?; let (input, _) = ws0(input)?; - let (input, params) = many1(terminated(lam_param, ws0)).parse(input)?; + let (input, parsed_params) = many1(terminated(lam_param_destructurable, ws0)).parse(input)?; let (input, _) = ws0(input)?; let (input, _) = tag("=>")(input)?; let (input, _) = ws0(input)?; let (input, body) = term(input)?; + // Same "wrap `body` once per destructured param, then `lams` the + // whole thing" shape as `def_parser`'s own Phase 3 handling -- see its + // own comment for why wrap order doesn't matter for correctness here. + let mut body = body; + for pp in parsed_params.iter().rev() { + if let ParsedParam::Destructured(param, fp) = pp { + body = match_term( + var_id(param.name.clone()), + vec![case_with_field_pattern(id(""), fp.clone(), body)], + ); + } + } + let params: Vec = parsed_params.iter().map(parsed_param_as_param).collect(); + Ok((input, lams(params, body))) } @@ -1413,7 +1517,14 @@ fn def_parser(input: Span) -> Res { )) })?; - let mut def = def_with_native(native_name, name.clone(), params.clone(), return_typ, attrs) + // A native def has no Monad-level body to wrap in a `match` -- a + // destructured param here degrades to an ordinary (un-destructured) + // param under its own gensym'd name, which is harmless: a native's + // params are dispatched by builtin ID, never referenced by name in + // the (nonexistent) body, so there's nothing for the destructuring to + // actually do here regardless. + let plain_params: Vec = params.iter().map(parsed_param_as_param).collect(); + let mut def = def_with_native(native_name, name.clone(), plain_params, return_typ, attrs) .map_err(|e| { nom::Err::Failure(ParseError::new( input.clone(), @@ -1437,7 +1548,33 @@ fn def_parser(input: Span) -> Res { (input, term) }; - if params.is_empty() { + // Wrap `term` in one `match` per destructured param -- `plans/ + // implementations/struct-field-destructuring.md`'s Phase 3 -- BEFORE + // `lams` wraps it in the final `Lam` chain below. Uses the bare form + // (`case_with_field_pattern(id(""), fp, ..)`) verbatim, reusing Phase + // 1/2's own match-case machinery: works for structs and, for free, any + // other sole-constructor `type`, resolved dynamically at elaboration + // time. Order among multiple destructured params doesn't matter for + // correctness here: `term` at this point is still a NAMED `Term` + // (`var(param.name)`/free identifier references resolve by name, not + // yet by de-Bruijn position -- that only happens much later, in + // `lower_core.rs`), so a destructured param's own gensym'd scrutinee + // variable resolves correctly by ordinary lexical scoping regardless of + // which wrap ends up physically innermost/outermost; they bind disjoint + // names unless the user reuses a field name across two params, which + // shadows exactly as normal scoping would. + let mut term = term; + for pp in params.iter().rev() { + if let ParsedParam::Destructured(param, fp) = pp { + term = match_term( + var_id(param.name.clone()), + vec![case_with_field_pattern(id(""), fp.clone(), term)], + ); + } + } + + let plain_params: Vec = params.iter().map(parsed_param_as_param).collect(); + if plain_params.is_empty() { let mut typ = return_typ; if !implicit_params.is_empty() { typ = foralls(implicit_params, typ); @@ -1447,19 +1584,32 @@ fn def_parser(input: Span) -> Res { Ok((input, d)) } else { let mut full_typ = return_typ; - for param in params.iter().rev() { + for param in plain_params.iter().rev() { full_typ = pi_with_mult((*param.typ).clone(), full_typ, param.mult.clone()); } if !implicit_params.is_empty() { full_typ = foralls(implicit_params, full_typ); } - let body = lams(params, term); + let body = lams(plain_params, term); let mut d = def(name, type_cons, full_typ, body, attrs); d.vis = vis; Ok((input, d)) } } +/// Project a `ParsedParam` down to the plain `Param` it wraps either way +/// -- used wherever a def's param LIST shape (`Pi`-type-building, +/// `lams`, a native's own param list) is being assembled, which only +/// ever needs each param's name/type/multiplicity, never its +/// `FieldPattern` half (that's consumed separately, by the +/// destructuring-`match`-wrapping loop above). +fn parsed_param_as_param(pp: &ParsedParam) -> Param { + match pp { + ParsedParam::Plain(p) => p.clone(), + ParsedParam::Destructured(p, _) => p.clone(), + } +} + fn macro_param(input: Span) -> Res, X> { alt(( // Untyped param: identifier diff --git a/core/src/parser/test/declarations.rs b/core/src/parser/test/declarations.rs index a05179d..7fcba83 100644 --- a/core/src/parser/test/declarations.rs +++ b/core/src/parser/test/declarations.rs @@ -104,9 +104,23 @@ fn test_class() { ); } +/// Test-only: unwraps every `ParsedParam::Plain` entry down to its inner +/// `Param` -- panics on a `Destructured` one, since these are the tests +/// exercising the pre-existing PLAIN param forms only (destructured-param +/// parsing has its own dedicated tests, see Phase 3 of `plans/ +/// implementations/struct-field-destructuring.md` below). +fn plain_params(pp: Vec) -> Vec { + pp.into_iter() + .map(|p| match p { + ParsedParam::Plain(p) => p, + ParsedParam::Destructured(..) => panic!("expected a Plain param, got a Destructured one"), + }) + .collect() +} + #[test] fn test_def_param() { - let def_param = |s: &'static str| def_param::<()>(s.into()); + let def_param = |s: &'static str| def_param::<()>(s.into()).map(|(i, r)| (i, plain_params(r))); let (_, r) = def_param(r#"(a : String)"#.into()).unwrap(); similar!(r, vec![dpar("a", typ("String"))]); let (_, r) = def_param(r#"(a b : String)"#.into()).unwrap(); @@ -123,7 +137,7 @@ fn test_def_param() { #[test] fn test_def_params_brace_form_matches_paren_form() { - let def_params = |s: &'static str| def_params::<()>(s.into()); + let def_params = |s: &'static str| def_params::<()>(s.into()).map(|(i, r)| (i, plain_params(r))); let (_, brace) = def_params(r#"{factor : I64, p : I64}"#.into()).unwrap(); let (_, paren) = def_params(r#"(factor : I64) (p : I64)"#.into()).unwrap(); similar!(brace.clone(), paren); @@ -135,7 +149,7 @@ fn test_def_params_brace_form_matches_paren_form() { #[test] fn test_def_params_brace_form_default_populates_param_default() { - let def_params = |s: &'static str| def_params::<()>(s.into()); + let def_params = |s: &'static str| def_params::<()>(s.into()).map(|(i, r)| (i, plain_params(r))); let (_, r) = def_params(r#"{factor : I64 := 1, p : I64}"#.into()).unwrap(); assert_eq!(r.len(), 2); assert_eq!(r[0].name, id("factor")); @@ -201,6 +215,166 @@ fn test_def_params_implicit_multi_name_form_unaffected() { ); } +// ------------------------------------------------------------------- +// Phase 3 of `plans/implementations/struct-field-destructuring.md`: +// `def` parameter destructuring (`def area ({ x, y } : Point) : I64 := +// x + y`, desugared to a gensym'd param + a wrapping bare-form match). +// ------------------------------------------------------------------- + +#[test] +fn test_def_destructured_param_desugars_to_wrapping_match() { + let s = r#"def area ({ x, y } : Point) : I64 := x + y"#.into(); + let (_, res) = def_parser(s).unwrap(); + // `def area (__struct_param#N : Point) : I64 := match __struct_param#N { { x, y } => x + y }` + let Term::Lam { param, body } = &res.term else { + panic!("expected a Lam, got {:?}", res.term); + }; + let Par::P(p) = param else { + panic!("expected an explicit Par::P param, got {param:?}"); + }; + assert!( + p.name.as_str().starts_with("__struct_param"), + "destructured param must bind a gensym'd name, got `{}`", + p.name.as_str() + ); + similar!((*p.typ).clone(), typ("Point")); + let Term::Lit { + value: Literal::Match { value, cases }, + } = body.as_ref() + else { + panic!("expected the body to be a Lit::Match, got {body:?}"); + }; + match value.as_ref() { + Term::Var { + name: NameRef::Id(scrutinee_name), + } => assert_eq!( + scrutinee_name, &p.name, + "the wrapping match's scrutinee must be the SAME gensym'd param" + ), + other => panic!("expected the scrutinee to be a bare Var, got {other:?}"), + } + assert_eq!(cases.len(), 1); + assert_eq!(cases[0].name, id(""), "bare-form match case"); + assert_eq!( + cases[0].field_pattern, + Some(FieldPattern { + fields: vec![(id("x"), id("x")), (id("y"), id("y"))], + rest: false, + }) + ); + similar!((*cases[0].value).clone(), oper(var("x"), "+", var("y"))); +} + +#[test] +fn test_def_destructured_and_plain_param_mixed() { + let s = r#"def scale ({ x, y } : Point) (factor : I64) : Point := { x := x * factor, y := y * factor }"#.into(); + let (_, res) = def_parser(s).unwrap(); + // The wrapping match is built ONCE, around the ORIGINAL body, before + // `lams` wraps the (now match-augmented) term in EVERY param's own + // `Lam` -- both the destructured param's and the plain `factor`'s -- + // in written order (`lams`' own convention: first param outermost). So + // the match itself ends up innermost, sitting UNDER both lambdas + // (`factor` must still be in scope inside it, which it is): `Lam + // {__struct_param, Lam {factor, Match {...}}}`, not immediately inside + // the destructured param's own Lam alone. + let Term::Lam { param, body } = &res.term else { + panic!( + "expected outer Lam (destructured param), got {:?}", + res.term + ); + }; + let Par::P(p0) = param else { + panic!("expected explicit Par::P"); + }; + assert!(p0.name.as_str().starts_with("__struct_param")); + let Term::Lam { + param: factor_param, + body: inner_body, + } = body.as_ref() + else { + panic!("expected an inner Lam (`factor`), got {body:?}"); + }; + let Par::P(p1) = factor_param else { + panic!("expected explicit Par::P"); + }; + assert_eq!(p1.name, id("factor")); + let Term::Lit { + value: Literal::Match { value, cases }, + } = inner_body.as_ref() + else { + panic!("expected the innermost body to be a wrapping Lit::Match, got {inner_body:?}"); + }; + match value.as_ref() { + Term::Var { + name: NameRef::Id(scrutinee_name), + } => assert_eq!(scrutinee_name, &p0.name), + other => panic!("expected the scrutinee to be a bare Var, got {other:?}"), + } + assert_eq!( + cases[0].field_pattern, + Some(FieldPattern { + fields: vec![(id("x"), id("x")), (id("y"), id("y"))], + rest: false, + }) + ); +} + +#[test] +fn test_def_destructured_param_partial_rest() { + let s = r#"def left_edge ({ x, .. } : Rect) : I64 := x"#.into(); + let (_, res) = def_parser(s).unwrap(); + let Term::Lam { body, .. } = &res.term else { + panic!("expected a Lam, got {:?}", res.term); + }; + let Term::Lit { + value: Literal::Match { cases, .. }, + } = body.as_ref() + else { + panic!("expected a Lit::Match, got {body:?}"); + }; + assert_eq!( + cases[0].field_pattern, + Some(FieldPattern { + fields: vec![(id("x"), id("x"))], + rest: true, + }) + ); +} + +#[test] +fn test_def_destructured_param_rename() { + let s = r#"def scale ({ x := px, y := py } : Point) (factor : I64) : Point := + { x := px * factor, y := py * factor }"# + .into(); + let (_, res) = def_parser(s).unwrap(); + // Two params here (destructured + plain `factor`) -- see + // `test_def_destructured_and_plain_param_mixed`'s own comment for why + // the match ends up under BOTH lambdas, not immediately inside the + // destructured param's own one. + let Term::Lam { + body: outer_body, .. + } = &res.term + else { + panic!("expected an outer Lam, got {:?}", res.term); + }; + let Term::Lam { body, .. } = outer_body.as_ref() else { + panic!("expected an inner Lam (`factor`), got {outer_body:?}"); + }; + let Term::Lit { + value: Literal::Match { cases, .. }, + } = body.as_ref() + else { + panic!("expected a Lit::Match, got {body:?}"); + }; + assert_eq!( + cases[0].field_pattern, + Some(FieldPattern { + fields: vec![(id("x"), id("px")), (id("y"), id("py"))], + rest: false, + }) + ); +} + #[test] fn test_def_params_empty_braces_do_not_parse() { // Inherits `struct_inner_parser`'s pre-existing `many1` (>=1 field) diff --git a/core/src/parser/test/expressions.rs b/core/src/parser/test/expressions.rs index 27463c9..7c6f8ef 100644 --- a/core/src/parser/test/expressions.rs +++ b/core/src/parser/test/expressions.rs @@ -10,6 +10,84 @@ fn test_lambda() { similar!(r, lams(vec![par("a"), par("b")], var("a"))); } +// ------------------------------------------------------------------- +// Phase 4 of `plans/implementations/struct-field-destructuring.md`: +// lambda-literal parameter destructuring (`\({ x, y } : Point) => x + +// y`), mirroring `def`'s own Phase 3 -- only `lambda` itself gets this +// (not `class_parser`/`inductive_parser`'s OWN `lam_param` call sites, +// which parse a declaration's generic TYPE params, not value params). +// ------------------------------------------------------------------- + +#[test] +fn test_lambda_destructured_param_desugars_to_wrapping_match() { + let lambda = |s: &'static str| lambda::<()>(s.into()); + let (_, r) = lambda(r#"\({ x, y } : Point) => x + y"#.into()).unwrap(); + let Term::Lam { param, body } = &r else { + panic!("expected a Lam, got {r:?}"); + }; + let Par::P(p) = param else { + panic!("expected an explicit Par::P param, got {param:?}"); + }; + assert!( + p.name.as_str().starts_with("__struct_param"), + "destructured param must bind a gensym'd name, got `{}`", + p.name.as_str() + ); + similar!((*p.typ).clone(), typ("Point")); + let Term::Lit { + value: Literal::Match { value, cases }, + } = body.as_ref() + else { + panic!("expected the body to be a Lit::Match, got {body:?}"); + }; + match value.as_ref() { + Term::Var { + name: NameRef::Id(scrutinee_name), + } => assert_eq!(scrutinee_name, &p.name), + other => panic!("expected the scrutinee to be a bare Var, got {other:?}"), + } + assert_eq!(cases.len(), 1); + assert_eq!(cases[0].name, id("")); + assert_eq!( + cases[0].field_pattern, + Some(FieldPattern { + fields: vec![(id("x"), id("x")), (id("y"), id("y"))], + rest: false, + }) + ); + similar!((*cases[0].value).clone(), oper(var("x"), "+", var("y"))); +} + +#[test] +fn test_lambda_destructured_and_plain_param_mixed() { + let lambda = |s: &'static str| lambda::<()>(s.into()); + let (_, r) = lambda(r#"\({ x, y } : Point) factor => x * factor"#.into()).unwrap(); + let Term::Lam { param, body } = &r else { + panic!("expected outer Lam, got {r:?}"); + }; + let Par::P(p0) = param else { + panic!("expected explicit Par::P"); + }; + assert!(p0.name.as_str().starts_with("__struct_param")); + let Term::Lam { + param: factor_param, + body: inner_body, + } = body.as_ref() + else { + panic!("expected an inner Lam (`factor`), got {body:?}"); + }; + let Par::P(p1) = factor_param else { + panic!("expected explicit Par::P"); + }; + assert_eq!(p1.name, id("factor")); + let Term::Lit { + value: Literal::Match { .. }, + } = inner_body.as_ref() + else { + panic!("expected the innermost body to be a wrapping Lit::Match, got {inner_body:?}"); + }; +} + #[test] fn test_application() { let application = |s: &'static str| application::<()>(s.into()); diff --git a/core/src/term.rs b/core/src/term.rs index 602d543..3e3ded5 100644 --- a/core/src/term.rs +++ b/core/src/term.rs @@ -1205,6 +1205,29 @@ pub fn case_with_field_pattern( } } +/// Like `case`, but preserves an existing `field_pattern` through a +/// tree-rewrite that otherwise reconstructs a `MatchCase` unchanged +/// (macro expansion's `expand_term`/`resolve_quote`/`rename_macro_var`/ +/// `alpha_rename_body`/`subst_macro`, `core/src/eval/macro_expand.rs` -- +/// every one of these previously rebuilt each case via `case(c.name, +/// c.args, value)`, which silently dropped `c.field_pattern` back to +/// `None`, corrupting an unresolved `{ x, y } => ...` case into a +/// zero-arg positional one before this plan's own elaboration pass ever +/// got to see it). +pub fn case_with_optional_field_pattern( + name: Identifier, + args: Vec, + field_pattern: Option, + value: Term, +) -> MatchCase { + MatchCase { + name, + args, + field_pattern, + value: Box::new(value), + } +} + #[derive(Debug, Clone, Copy, PartialEq, Hash, Eq, PartialOrd, Ord)] pub enum NumSuffix { I8, diff --git a/core/tests/field_pattern_integration_test.rs b/core/tests/field_pattern_integration_test.rs new file mode 100644 index 0000000..d4c21e5 --- /dev/null +++ b/core/tests/field_pattern_integration_test.rs @@ -0,0 +1,211 @@ +//! End-to-end runtime tests for Phases 1-4 of +//! `plans/implementations/struct-field-destructuring.md` (field-pattern +//! match-case destructuring, `{ x, y } => ...` / `ConsName { x, y } => +//! ...`, and Phases 3/4's `def`/lambda parameter destructuring, `def f +//! ({ x, y } : T) := ...` / `\({ x, y } : T) => ...`, both desugaring to +//! a gensym'd param + a wrapping bare-form match, reusing Phase 1/2's own +//! machinery) — unlike `core_check_module.rs`'s own unit tests (which only +//! exercise type-checking via `check_module_source`), these run the FULL +//! pipeline (check -> lower -> evaluate) via `eval_core_program`, the same +//! entry point `named_call_integration_test.rs` uses. +//! +//! This distinction matters here even more than for that plan's own +//! integration tests: Finding 2 of this plan's own evaluation (see its +//! Changelog) predicted that `check`/`infer` succeeding is not enough +//! proof the FIELD ORDER a field-pattern case's binders actually get is +//! correct at runtime — `lower_core.rs` lowers a case's body against its +//! WRITTEN field order (the only order available pre-type-checking), and +//! `desugar_struct_literals` must retarget it onto the constructor's real +//! DECLARED order (`core_term::permute_binders`) before evaluation, or a +//! type-checked-fine program could silently bind the WRONG values to the +//! WRONG names. Every test below writes fields in an order that would +//! produce a visibly wrong (but still well-typed) answer if that +//! retargeting were missing or buggy, rather than just checking "did it +//! run without error." + +use monad_core::eval_core_program; +use monad_core::term::ModulePath; + +fn run(source: &str) -> monad_core::core_value::Value { + let path = ModulePath::top("'field_pattern_e2e_test"); + eval_core_program(&path, source).unwrap_or_else(|e| panic!("eval_core_program failed: {e}")) +} + +fn as_i64(v: &monad_core::core_value::Value) -> i64 { + match v { + monad_core::core_value::Value::Lit(monad_core::core_ir::IrLit::Num(n, _)) => *n, + other => panic!("expected an int literal, got {other:?}"), + } +} + +/// Bare `{ ... }` destructure of a struct, fields written in the OPPOSITE +/// order from the struct's own declaration (`y` before `x`) -- if +/// `permute_binders` weren't retargeting the case onto declared order, +/// `x`/`y` inside the body would silently read each other's values. +const BARE_STRUCT_REORDERED: &str = r#" +struct Point { x : I64, y : I64 } + +def sub (p : Point) : I64 := + match p { + { y, x } => x - y + } + +def main : I64 := sub { x := 10, y := 3 } +"#; + +#[test] +fn phase2_bare_struct_destructure_reordered_fields_binds_correctly() { + assert_eq!(as_i64(&run(BARE_STRUCT_REORDERED)), 7); +} + +/// Bare `{ ... }` with field RENAME (`x := px`) and a partial destructure +/// via `..` -- `w` must resolve to `Rect`'s `width` field specifically +/// (declared FIRST), discarding `height` (declared second) without it +/// ever reaching the body. +const BARE_RENAME_AND_REST: &str = r#" +struct Rect { width : I64, height : I64 } + +def left_edge (r : Rect) : I64 := + match r { + { width := w, .. } => w + } + +def main : I64 := left_edge { width := 9, height := 100 } +"#; + +#[test] +fn phase2_bare_rename_and_rest_binds_only_named_field() { + assert_eq!(as_i64(&run(BARE_RENAME_AND_REST)), 9); +} + +/// Named-constructor form against a MULTI-constructor `type` (the +/// Rust-enum-struct-variant case) -- `rectangle`'s two fields written in +/// the OPPOSITE order from its declaration, same reordering-correctness +/// proof as the struct case above, but through the named-form resolution +/// path instead of the bare-form one. +const NAMED_MULTI_CONSTRUCTOR_REORDERED: &str = r#" +type Shape { + circle (radius : I64), + rectangle { width : I64, height : I64 } +} + +def area (s : Shape) : I64 := + match s { + circle { radius } => radius * radius, + rectangle { height, width } => width * height + } + +def main : I64 := area (Shape.rectangle 3 4) +"#; + +#[test] +fn phase2_named_multi_constructor_reordered_fields_binds_correctly() { + assert_eq!(as_i64(&run(NAMED_MULTI_CONSTRUCTOR_REORDERED)), 12); +} + +/// Function-parameter destructuring is out of this plan's already-landed +/// scope (Phase 3/4, not yet implemented) -- this test instead exercises +/// a field-pattern case NESTED inside another field-pattern case's own +/// body, proving the retargeting composes (each case's own `permute_binders` +/// call is scoped correctly relative to the OTHER case's binders already +/// in scope, per `permute_binders`' own `cutoff` threading). +const NESTED_FIELD_PATTERN_CASES: &str = r#" +struct Point { x : I64, y : I64 } +struct Line { from : Point, to : Point } + +def dx (l : Line) : I64 := + match l { + { to, from } => + match to { + { y := ty, x := tx } => + match from { + { x := fx, y := fy } => (tx - fx) + (ty - fy) + } + } + } + +def main : I64 := dx { from := { x := 1, y := 2 }, to := { x := 10, y := 20 } } +"#; + +#[test] +fn phase2_nested_field_pattern_cases_compose_correctly() { + // (10 - 1) + (20 - 2) = 9 + 18 = 27 + assert_eq!(as_i64(&run(NESTED_FIELD_PATTERN_CASES)), 27); +} + +// ------------------------------------------------------------------- +// Phase 3: `def` parameter destructuring. +// ------------------------------------------------------------------- + +/// A destructured param's gensym'd binder desugars to a wrapping `match` +/// -- same reordering-correctness proof as the match-case tests above, +/// applied through the PARAMETER-position path instead. +const DESTRUCTURED_PARAM_REORDERED: &str = r#" +struct Point { x : I64, y : I64 } + +def sub ({ y, x } : Point) : I64 := x - y + +def main : I64 := sub { x := 10, y := 3 } +"#; + +#[test] +fn phase3_destructured_param_reordered_fields_binds_correctly() { + assert_eq!(as_i64(&run(DESTRUCTURED_PARAM_REORDERED)), 7); +} + +/// Two destructured params in one signature -- proves each gets its own +/// independent wrapping match, correctly scoped (per +/// `permute_binders`'s own `cutoff` threading composing across separate +/// match nodes, not just nested ones as the Phase 2 test above covers). +const TWO_DESTRUCTURED_PARAMS: &str = r#" +struct Point { x : I64, y : I64 } + +def dist ({ x := x1, y := y1 } : Point) ({ x := x2, y := y2 } : Point) : I64 := + (x2 - x1) + (y2 - y1) + +def main : I64 := dist { x := 1, y := 2 } { x := 10, y := 20 } +"#; + +#[test] +fn phase3_two_destructured_params_bind_independently() { + // (10 - 1) + (20 - 2) = 27 + assert_eq!(as_i64(&run(TWO_DESTRUCTURED_PARAMS)), 27); +} + +/// A destructured param mixed with an ordinary plain one, and a partial +/// (`..`) destructure -- both need to still see each other correctly +/// (the plain param referenced from inside the destructured param's own +/// wrapping match). +const MIXED_PARAMS_WITH_REST: &str = r#" +struct Rect { width : I64, height : I64 } + +def scaled_width ({ width, .. } : Rect) (factor : I64) : I64 := width * factor + +def main : I64 := scaled_width { width := 4, height := 100 } 3 +"#; + +#[test] +fn phase3_mixed_destructured_and_plain_param_with_rest() { + assert_eq!(as_i64(&run(MIXED_PARAMS_WITH_REST)), 12); +} + +// ------------------------------------------------------------------- +// Phase 4: lambda-literal parameter destructuring. +// ------------------------------------------------------------------- + +/// Same reordering-correctness proof as Phase 3's own `def`-param test, +/// through a `\({ ... } : T) => ...` lambda literal instead -- applied +/// via a higher-order `List.map`-style call so it's a genuine lambda +/// value, not just sugar for a `def`. +const LAMBDA_DESTRUCTURED_PARAM: &str = r#" +struct Point { x : I64, y : I64 } + +def sub (f : Point -> I64) (p : Point) : I64 := f p + +def main : I64 := sub (\({ y, x } : Point) => x - y) { x := 10, y := 3 } +"#; + +#[test] +fn phase4_lambda_destructured_param_reordered_fields_binds_correctly() { + assert_eq!(as_i64(&run(LAMBDA_DESTRUCTURED_PARAM)), 7); +}