Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix nesting mapping tuple with no location infomation when type error #834

Conversation

rez5427
Copy link

@rez5427 rez5427 commented Dec 17, 2024

I add a test file to recurrent the situation happend in here.
I'm new with sail, so I'm not sure this is right.

mapping A : (bool, bool) <-> string = {
  (true, true) <-> "a",
  (true, false) <-> "b",
}

mapping B : bool <-> string = {
  true <-> "a" ^ A(true, false, false),
  false <-> "b" ^ A(false, false),
}

val main : unit -> unit

function main() = {
  let str = B(true);
  ()
}

The problem seems happen when there is a mapping inside mapping,
Seems like sail type checked this use the code below.
Like A(true, false, false) , it check true false false, one by one recursively.
But when it traverse in those args, it kind lost the location infomation of mapping A.

| MP_tuple [] -> begin
      match Env.expand_synonyms env typ with
      | Typ_aux (Typ_id typ_id, _) when string_of_id typ_id = "unit" -> (annot_mpat (MP_tuple []) typ, env, [])
      | _ -> typ_error l "Cannot match unit mapping-pattern against non-unit type"
    end
  | MP_tuple mpats -> begin
      match Env.expand_synonyms env typ with
      | Typ_aux (Typ_tuple typs, _) ->
          let tpats, env, guards =
            try List.fold_left2 bind_tuple_mpat ([], env, []) mpats typs
            with Invalid_argument _ -> typ_error l "Tuple mapping-pattern and tuple type have different length"
          in
          (annot_mpat (MP_tuple (List.rev tpats)) typ, env, guards)
      | _ -> typ_error l "Cannot bind tuple mapping-pattern against non tuple type"

before

Type error:
Tuple mapping-pattern and tuple type have different length

after

Type error:
/sail/test/pattern_completeness/nested_mapping.sail:7.17-38:
7 |  true <-> "a" ^ A(true, false, false),
  |                 ^-------------------^
  | Mapping A applied to 3 args, expected 2: bool, bool

@rez5427 rez5427 force-pushed the sail2_fix_nesting_mapping_tuple_with_no_location branch 2 times, most recently from 24f399c to c15d025 Compare December 17, 2024 16:04
Fix nesting mapping has no location info when Type error
@rez5427 rez5427 force-pushed the sail2_fix_nesting_mapping_tuple_with_no_location branch from c15d025 to 74867b9 Compare December 17, 2024 16:05
@Alasdair
Copy link
Collaborator

Thanks for finding this! In this case it can be fixed by just adding a location to the mk_mpat call, without duplicating the error logic. I've made a PR with just that change

@Alasdair
Copy link
Collaborator

Closing as should be fixed by that PR, let me know if the issue persists

@Alasdair Alasdair closed this Dec 17, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants