iter 22b.3.4: synthesise_mono_fn — instance body + class default fallback

2026-05-09 20:41:45 +02:00
parent 9f86c072dc
commit d6084a71fb
3 changed files with 232 additions and 3 deletions
@@ -183,3 +183,127 @@ fn mono_symbol_compound_type_uses_hash_suffix() {
    let again = ailang_check::mono::mono_symbol("show", &pair_ty);
    assert_eq!(name, again, "mono_symbol must be deterministic");
 }
+
+/// Property: synthesise_mono_fn copies the matching instance method's
+/// body verbatim and produces a fully-concrete `FnDef` whose name uses
+/// the `mono_symbol` form, whose `ty` is the class method's declared
+/// type with the class param substituted to the target type, and whose
+/// `params` / `body` come from the instance's `Term::Lam`.
+#[test]
+fn synthesise_mono_fn_uses_instance_body_lam() {
+    use ailang_check::mono::{synthesise_mono_fn, MonoTarget};
+    use ailang_core::ast::{ClassDef, ClassMethod, InstanceDef, InstanceMethod, Term};
+
+    let class_def = ClassDef {
+        name: "Foo".into(),
+        param: "a".into(),
+        superclass: None,
+        methods: vec![ClassMethod {
+            name: "bar".into(),
+            ty: Type::Fn {
+                params: vec![Type::Var { name: "a".into() }],
+                ret: Box::new(Type::int()),
+                effects: vec![],
+                param_modes: vec![],
+                ret_mode: ailang_core::ast::ParamMode::Implicit,
+            },
+            default: None,
+        }],
+        doc: None,
+    };
+    let instance = InstanceDef {
+        class: "Foo".into(),
+        type_: Type::int(),
+        methods: vec![InstanceMethod {
+            name: "bar".into(),
+            body: Term::Lam {
+                params: vec!["i".into()],
+                param_tys: vec![Type::Var { name: "a".into() }],
+                ret_ty: Box::new(Type::int()),
+                effects: vec![],
+                body: Box::new(Term::Var { name: "i".into() }),
+            },
+        }],
+        doc: None,
+    };
+    let target = MonoTarget {
+        class: "Foo".into(),
+        method: "bar".into(),
+        type_: Type::int(),
+        defining_module: "m".into(),
+    };
+
+    let f = synthesise_mono_fn(&target, &class_def, &instance).expect("synth");
+    assert_eq!(f.name, "bar#Int");
+    assert!(
+        matches!(
+            &f.ty,
+            Type::Fn { params, ret, .. }
+                if params.len() == 1
+                && matches!(&params[0], Type::Con { name, args } if name == "Int" && args.is_empty())
+                && matches!(ret.as_ref(), Type::Con { name, args } if name == "Int" && args.is_empty())
+        ),
+        "ty = {:?}",
+        f.ty
+    );
+    assert_eq!(f.params, vec!["i".to_string()]);
+    assert!(
+        matches!(&f.body, Term::Var { name } if name == "i"),
+        "body = {:?}",
+        f.body
+    );
+}
+
+/// Property: when the instance omits a method that has a class-level
+/// `default` body, synthesise_mono_fn falls back to that default and
+/// uses its params/body verbatim — registry-build's `MissingMethod`
+/// has already enforced that one of the two is present.
+#[test]
+fn synthesise_mono_fn_falls_back_to_class_default() {
+    use ailang_check::mono::{synthesise_mono_fn, MonoTarget};
+    use ailang_core::ast::{ClassDef, ClassMethod, InstanceDef, Literal, Term};
+
+    let class_def = ClassDef {
+        name: "Greet".into(),
+        param: "a".into(),
+        superclass: None,
+        methods: vec![ClassMethod {
+            name: "hello".into(),
+            ty: Type::Fn {
+                params: vec![Type::Var { name: "a".into() }],
+                ret: Box::new(Type::str_()),
+                effects: vec![],
+                param_modes: vec![],
+                ret_mode: ailang_core::ast::ParamMode::Implicit,
+            },
+            default: Some(Term::Lam {
+                params: vec!["_x".into()],
+                param_tys: vec![Type::Var { name: "a".into() }],
+                ret_ty: Box::new(Type::str_()),
+                effects: vec![],
+                body: Box::new(Term::Lit {
+                    lit: Literal::Str { value: "hi".into() },
+                }),
+            }),
+        }],
+        doc: None,
+    };
+    // Instance carries no `hello` body — must fall back to default.
+    let instance = InstanceDef {
+        class: "Greet".into(),
+        type_: Type::int(),
+        methods: vec![],
+        doc: None,
+    };
+    let target = MonoTarget {
+        class: "Greet".into(),
+        method: "hello".into(),
+        type_: Type::int(),
+        defining_module: "m".into(),
+    };
+
+    let f = synthesise_mono_fn(&target, &class_def, &instance).expect("synth");
+    assert_eq!(f.name, "hello#Int");
+    assert_eq!(f.params, vec!["_x".to_string()]);
+    assert!(matches!(&f.body, Term::Lit { .. }), "body = {:?}", f.body);
+}