source: Deliverables/D2.2/8051/src/checker.ml @ 486

Last change on this file since 486 was 486, checked in by ayache, 8 years ago

Deliverable D2.2

File size: 1.3 KB
Line 
1let same_traces (traces : ((Languages.ast * (Label.t list)) 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, trace1), (ast2, 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))
Note: See TracBrowser for help on using the repository browser.