4 let build_equality term =
6 C.Implicit None, (C.Implicit None, term, C.Rel 1, Utils.Gt), [], []
17 let path_indexing_test () =
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 eq1 = build_equality (C.Appl [C.Rel 1; C.Meta (1, []); C.Meta (1, [])])
34 and eq2 = build_equality (C.Appl [C.Rel 1; C.Meta (1, []); C.Meta (2, [])]) in
35 let res1 = in_index table eq1
36 and res2 = in_index table eq2 in
37 let print_results res =
42 "(" ^ (Utils.string_of_pos p) ^ ", " ^
43 (Inference.string_of_equality e) ^ ")"
48 Printf.printf "path_strings:\n%s\n\n"
52 "{" ^ (String.concat "; " (List.map string_of_path_string l)) ^ "}"
54 Printf.printf "table:\n%s\n\n" (string_of_pstrie table);
55 Printf.printf "matches:\n%s\n\n" (print_results matches);
56 Printf.printf "unifications:\n%s\n\n" (print_results unifications);
57 Printf.printf "in_index %s: %s\n"
58 (Inference.string_of_equality eq1) (string_of_bool res1);
59 Printf.printf "in_index %s: %s\n"
60 (Inference.string_of_equality eq2) (string_of_bool res2);
67 C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Meta (1, [])]; C.Rel 5]
69 C.Appl [C.Rel 1; C.Appl [C.Rel 5; C.Rel 4; C.Meta (1, [])]; C.Rel 5]
71 let res = Inference.extract_differing_subterms t1 t2 in
73 | None -> print_endline "NO DIFFERING SUBTERMS???"
75 Printf.printf "OK: %s, %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2);
82 C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Rel 4]; C.Rel 5]
84 let pos1 = Discrimination_tree.next_t [1] t in
85 let pos2 = Discrimination_tree.after_t [1] t in
86 Printf.printf "next_t 1: %s\nafter_t 1: %s\n"
87 (CicPp.ppterm (Discrimination_tree.subterm_at_pos pos1 t))
88 (CicPp.ppterm (Discrimination_tree.subterm_at_pos pos2 t));
92 let discrimination_tree_test () =
95 C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Meta (1, [])]; C.Rel 5];
96 C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 4]; C.Meta (1, [])];
97 C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Rel 4]; C.Rel 5];
98 C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 5]; C.Rel 4];
99 C.Appl [C.Rel 10; C.Meta (5, []); C.Rel 11]
102 List.map Discrimination_tree.path_string_of_term terms in
105 Discrimination_tree.index
106 Discrimination_tree.DiscriminationTree.empty
107 (List.map build_equality terms)
110 (* C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 4]; C.Rel 5] in *)
111 let query = C.Appl [C.Rel 10; C.Meta (14, []); C.Meta (13, [])] in
112 let matches = Discrimination_tree.retrieve_generalizations table query in
113 let unifications = Discrimination_tree.retrieve_unifiables table query in
114 let eq1 = build_equality (C.Appl [C.Rel 1; C.Meta (1, []); C.Meta (1, [])])
115 and eq2 = build_equality (C.Appl [C.Rel 1; C.Meta (1, []); C.Meta (2, [])]) in
116 let res1 = Discrimination_tree.in_index table eq1
117 and res2 = Discrimination_tree.in_index table eq2 in
118 let print_results res =
120 (Discrimination_tree.PosEqSet.fold
123 "(" ^ (Utils.string_of_pos p) ^ ", " ^
124 (Inference.string_of_equality e) ^ ")"
129 Printf.printf "path_strings:\n%s\n\n"
131 (List.map Discrimination_tree.string_of_path_string path_strings));
132 Printf.printf "table:\n%s\n\n"
133 (Discrimination_tree.string_of_discrimination_tree table);
134 Printf.printf "matches:\n%s\n\n" (print_results matches);
135 Printf.printf "unifications:\n%s\n\n" (print_results unifications);
136 Printf.printf "in_index %s: %s\n"
137 (Inference.string_of_equality eq1) (string_of_bool res1);
138 Printf.printf "in_index %s: %s\n"
139 (Inference.string_of_equality eq2) (string_of_bool res2);
144 let module C = Cic in
145 let module M = CicMetaSubst in
150 C.Appl [C.Rel 15; C.Rel 12; C.Meta (41, [])]];
152 C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (11, [])];
153 C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (12, [])]]
156 (43, ([], C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (11, [])], C.Rel 16));
157 (10, ([], C.Rel 12, C.Rel 16));
158 (12, ([], C.Meta (41, []), C.Rel 16))
161 (43, ([], C.Appl [C.Rel 15; C.Rel 12; C.Meta (11, [])], C.Rel 16));
162 (10, ([], C.Rel 12, C.Rel 16));
163 (12, ([], C.Meta (41, []), C.Rel 16))
165 let t1 = M.apply_subst subst1 term
166 and t2 = M.apply_subst subst2 term in
167 Printf.printf "t1 = %s\nt2 = %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2);
172 (* next_after ();; *)
173 (* discrimination_tree_test ();; *)
174 (* path_indexing_test ();; *)