src/checker.ml

   1 let same_traces (traces : ((Languages.ast * AST.trace) list)) =
   2   let compare_trace trace1 trace2 =
   3     let occs_trace1 = Misc.ListExt.multi_set_of_list trace1
   4     and occs_trace2 = Misc.ListExt.multi_set_of_list trace2 in
   5     Misc.ListExt.assoc_diff occs_trace1 occs_trace2
   6   in
   7   let check_trace (_, (_, trace1)) (_, (_, trace2)) =
   8     compare_trace trace1 trace2 = []
   9   in
  10   let print_trace lang1 lang2 ds =
  11     let string_of_value = function
  12       | None -> "is not present"
  13       | Some v -> Printf.sprintf "appears %d times" v
  14     in
  15     let sentence (k, (v1, v2)) =
  16       Printf.sprintf "  Label %s %s in language `%s' \
  17                         whereas it %s in language `%s'."
  18         k (string_of_value v1) lang1 (string_of_value v2) lang2
  19     in
  20     String.concat "\n" (List.map sentence ds)
  21   in
  22   match Misc.ListExt.transitive_forall2 check_trace traces with
  23     | None -> ()
  24     | Some ((ast1, (res1, trace1)), (ast2, (res2, trace2))) ->
  25       let lang1 = Languages.to_string (Languages.language_of_ast ast1)
  26       and lang2 = Languages.to_string (Languages.language_of_ast ast2) in
  27       let diff = compare_trace trace1 trace2 in
  28       Error.global_error "during trace comparison"
  29         (Printf.sprintf
  30            "The traces of two intermediate programs differ:\n%s"
  31            (print_trace lang1 lang2 diff))