diff --git a/charon-ml/src/NameMatcher.ml b/charon-ml/src/NameMatcher.ml index 0c334ae3..d5b6710d 100644 --- a/charon-ml/src/NameMatcher.ml +++ b/charon-ml/src/NameMatcher.ml @@ -182,11 +182,19 @@ let match_literal (pl : literal) (l : Values.literal) : bool = let rec match_name_with_generics (ctx : ctx) (c : match_config) (p : pattern) (n : T.name) (g : T.generic_args) : bool = match (p, n) with - | [], [] -> false (* We shouldn't get there: the names should be non empty *) + | [], [] -> + raise + (Failure + "match_name_with_generics: attempt to match empty names and patterns") + (* We shouldn't get there: the names/patterns should be non empty *) | [ PIdent (pid, pg) ], [ PeIdent (id, _) ] -> (* We reached the end: match the generics. We have to generate an empty map. *) pid = id && match_generic_args ctx c (mk_empty_maps ()) pg g + | [ PImpl pty ], [ PeImpl impl ] -> + (* We can get there when matching a prefix of the name with a pattern *) + match_expr_with_ty ctx c (mk_empty_maps ()) pty impl.ty + && g = TypesUtils.empty_generic_args | PIdent (pid, pg) :: p, PeIdent (id, _) :: n -> (* This is not the end: check that the generics are empty *) pid = id && pg = [] && match_name_with_generics ctx c p n g @@ -898,6 +906,29 @@ module NameMatcherMap = struct let of_list (ls : (pattern * 'a) list) : 'a t = List.fold_left (fun m (pat, v) -> add pat v m) empty ls + + let rec to_string_aux (current_indent : string) (indent : string) + (v_to_string : 'a -> string) (m : 'a t) : string = + let (Node (opt_v, children)) = m in + let opt_v = + current_indent ^ PrintUtils.option_to_string v_to_string opt_v + in + let children = + String.concat "\n" + (List.map (child_to_string current_indent indent v_to_string) children) + in + opt_v ^ " [\n" ^ children ^ "\n" ^ current_indent ^ "]" + + and child_to_string (current_indent : string) (indent : string) + (v_to_string : 'a -> string) (child_pat, child) : string = + let c : print_config = { tgt = TkPattern } in + current_indent + ^ pattern_to_string c child_pat + ^ " ->\n" + ^ to_string_aux (current_indent ^ indent) indent v_to_string child + + let to_string (v_to_string : 'a -> string) (m : 'a t) : string = + to_string_aux "" " " v_to_string m end (* Test *)