Fix Ctr patterns not being renamed in imports (#725)

This commit is contained in:
Nicolas Abril 2024-10-07 14:26:47 +00:00 committed by GitHub
parent 53d52626ea
commit 4d6f461d54
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
2 changed files with 23 additions and 8 deletions

View File

@ -2,7 +2,7 @@ use super::{BindMap, ImportsMap, PackageLoader};
use crate::{
diagnostics::{Diagnostics, DiagnosticsConfig},
fun::{
parser::ParseBook, Adt, AdtCtr, Book, Definition, HvmDefinition, Name, Rule, Source, SourceKind, Term,
parser::ParseBook, Adt, AdtCtr, Book, Definition, HvmDefinition, Name, Pattern, Source, SourceKind, Term,
},
imp::{self, Expr, MatchArm, Stmt},
imports::packages::Packages,
@ -346,19 +346,30 @@ trait Def {
impl Def for Definition {
fn apply_binds(&mut self, maybe_constructor: bool, binds: &BindMap) {
fn rename_ctr_patterns(rule: &mut Rule, binds: &BindMap) {
for pat in &mut rule.pats {
for bind in pat.binds_mut().flatten() {
if let Some(alias) = binds.get(bind) {
*bind = alias.clone();
fn rename_ctr_pattern(pat: &mut Pattern, binds: &BindMap) {
for pat in pat.children_mut() {
rename_ctr_pattern(pat, binds);
}
match pat {
Pattern::Ctr(nam, _) => {
if let Some(alias) = binds.get(nam) {
*nam = alias.clone();
}
}
Pattern::Var(Some(nam)) => {
if let Some(alias) = binds.get(nam) {
*nam = alias.clone();
}
}
_ => {}
}
}
for rule in &mut self.rules {
if maybe_constructor {
rename_ctr_patterns(rule, binds);
for pat in &mut rule.pats {
rename_ctr_pattern(pat, binds);
}
}
let bod = std::mem::take(&mut rule.body);
rule.body = bod.fold_uses(binds.iter().rev());

View File

@ -1,7 +1,11 @@
from lib/MyOption import (MyOption, MyOption/bind, MyOption/wrap)
unwrap (val : (MyOption u24)) : u24
unwrap (MyOption/Some x) = x
unwrap (MyOption/None) = 0
def main() -> MyOption((u24, u24)):
with MyOption:
a <- MyOption/Some(1)
b <- MyOption/Some(2)
b = unwrap(MyOption/Some(2))
return wrap((a, b))