4 let build_equality term =
6 C.Implicit None, (C.Implicit None, term, C.Rel 1, Utils.Gt), [], []
20 C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Meta (1, [])]; C.Rel 5];
21 C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 4]; C.Meta (1, [])];
22 C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Rel 4]; C.Rel 5];
23 C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 5]; C.Rel 4];
24 C.Appl [C.Rel 1; C.Meta (1, []); C.Meta (1, [])]
26 let path_strings = List.map (path_strings_of_term 0) terms in
28 List.fold_left index PSTrie.empty (List.map build_equality terms) in
30 C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 4]; C.Rel 5] in
31 let matches = retrieve_generalizations table query in
32 let unifications = retrieve_unifiables table query in
33 let print_results res =
38 "(" ^ (Utils.string_of_pos p) ^ ", " ^
39 (Inference.string_of_equality e) ^ ")"
44 Printf.printf "path_strings:\n%s\n\n"
48 "{" ^ (String.concat "; " (List.map string_of_path_string l)) ^ "}"
50 Printf.printf "table:\n%s\n\n" (string_of_pstrie table);
51 Printf.printf "matches:\n%s\n\n" (print_results matches);
52 Printf.printf "unifications:\n%s\n" (print_results unifications)