]> matita.cs.unibo.it Git - helm.git/blob - components/tactics/paramodulation/test_indexing.ml
Bug fixed in injection: lifting was not performed correctly, but it worked
[helm.git] / components / tactics / paramodulation / test_indexing.ml
1 (* $Id$ *)
2
3 open Path_indexing
4
5 (*
6 let build_equality term =
7   let module C = Cic in
8   C.Implicit None, (C.Implicit None, term, C.Rel 1, Utils.Gt), [], []
9 ;;
10
11
12 (*
13   f = Rel 1
14   g = Rel 2
15   a = Rel 3
16   b = Rel 4
17   c = Rel 5
18 *)
19 let path_indexing_test () =
20   let module C = Cic in
21   let terms = [
22     C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Meta (1, [])]; C.Rel 5];
23     C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 4]; C.Meta (1, [])];
24     C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Rel 4]; C.Rel 5];
25     C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 5]; C.Rel 4];
26     C.Appl [C.Rel 1; C.Meta (1, []); C.Meta (1, [])]
27   ] in
28   let path_strings = List.map (path_strings_of_term 0) terms in
29   let table =
30     List.fold_left index PSTrie.empty (List.map build_equality terms) in
31   let query =
32     C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 4]; C.Rel 5] in
33   let matches = retrieve_generalizations table query in
34   let unifications = retrieve_unifiables table query in
35   let eq1 = build_equality (C.Appl [C.Rel 1; C.Meta (1, []); C.Meta (1, [])])
36   and eq2 = build_equality (C.Appl [C.Rel 1; C.Meta (1, []); C.Meta (2, [])]) in
37   let res1 = in_index table eq1
38   and res2 = in_index table eq2 in
39   let print_results res =
40     String.concat "\n"
41       (PosEqSet.fold
42          (fun (p, e) l ->
43             let s = 
44               "(" ^ (Utils.string_of_pos p) ^ ", " ^
45                 (Inference.string_of_equality e) ^ ")"
46             in
47             s::l)
48          res [])
49   in
50   Printf.printf "path_strings:\n%s\n\n"
51     (String.concat "\n"
52        (List.map
53           (fun l ->
54              "{" ^ (String.concat "; " (List.map string_of_path_string l)) ^ "}"
55           ) path_strings));
56   Printf.printf "table:\n%s\n\n" (string_of_pstrie table);
57   Printf.printf "matches:\n%s\n\n" (print_results matches);
58   Printf.printf "unifications:\n%s\n\n" (print_results unifications);
59   Printf.printf "in_index %s: %s\n"
60     (Inference.string_of_equality eq1) (string_of_bool res1);
61   Printf.printf "in_index %s: %s\n"
62     (Inference.string_of_equality eq2) (string_of_bool res2);
63 ;;
64
65
66 let differing () =
67   let module C = Cic in
68   let t1 =
69     C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Meta (1, [])]; C.Rel 5]
70   and t2 = 
71     C.Appl [C.Rel 1; C.Appl [C.Rel 5; C.Rel 4; C.Meta (1, [])]; C.Rel 5]
72   in
73   let res = Inference.extract_differing_subterms t1 t2 in
74   match res with
75   | None -> prerr_endline "NO DIFFERING SUBTERMS???"
76   | Some (t1, t2) ->
77       Printf.printf "OK: %s, %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2);
78 ;;
79
80
81 let next_after () =
82   let module C = Cic in
83   let t =
84     C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Rel 4]; C.Rel 5]
85   in
86   let pos1 = Discrimination_tree.next_t [1] t in
87   let pos2 = Discrimination_tree.after_t [1] t in
88   Printf.printf "next_t 1: %s\nafter_t 1: %s\n"
89     (CicPp.ppterm (Discrimination_tree.subterm_at_pos pos1 t))
90     (CicPp.ppterm (Discrimination_tree.subterm_at_pos pos2 t));
91 ;;
92
93
94 let discrimination_tree_test () =
95   let module C = Cic in
96   let terms = [
97     C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Meta (1, [])]; C.Rel 5];
98     C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 4]; C.Meta (1, [])];
99     C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Rel 4]; C.Rel 5];
100     C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 5]; C.Rel 4];
101     C.Appl [C.Rel 10; C.Meta (5, []); C.Rel 11]
102   ] in
103   let path_strings =
104     List.map Discrimination_tree.path_string_of_term terms in
105   let table =
106     List.fold_left
107       Discrimination_tree.index
108       Discrimination_tree.DiscriminationTree.empty
109       (List.map build_equality terms)
110   in
111 (*   let query = *)
112 (*     C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 4]; C.Rel 5] in *)
113   let query = C.Appl [C.Rel 10; C.Meta (14, []); C.Meta (13, [])] in
114   let matches = Discrimination_tree.retrieve_generalizations table query in
115   let unifications = Discrimination_tree.retrieve_unifiables table query in
116   let eq1 = build_equality (C.Appl [C.Rel 1; C.Meta (1, []); C.Meta (1, [])])
117   and eq2 = build_equality (C.Appl [C.Rel 1; C.Meta (1, []); C.Meta (2, [])]) in
118   let res1 = Discrimination_tree.in_index table eq1
119   and res2 = Discrimination_tree.in_index table eq2 in
120   let print_results res =
121     String.concat "\n"
122       (Discrimination_tree.PosEqSet.fold
123          (fun (p, e) l ->
124             let s = 
125               "(" ^ (Utils.string_of_pos p) ^ ", " ^
126                 (Inference.string_of_equality e) ^ ")"
127             in
128             s::l)
129          res [])
130   in
131   Printf.printf "path_strings:\n%s\n\n"
132     (String.concat "\n"
133        (List.map Discrimination_tree.string_of_path_string path_strings));
134   Printf.printf "table:\n%s\n\n"
135     (Discrimination_tree.string_of_discrimination_tree table);
136   Printf.printf "matches:\n%s\n\n" (print_results matches);
137   Printf.printf "unifications:\n%s\n\n" (print_results unifications);
138   Printf.printf "in_index %s: %s\n"
139     (Inference.string_of_equality eq1) (string_of_bool res1);
140   Printf.printf "in_index %s: %s\n"
141     (Inference.string_of_equality eq2) (string_of_bool res2);
142 ;;
143
144
145 let test_subst () =
146   let module C = Cic in
147   let module M = CicMetaSubst in
148   let term = C.Appl [
149     C.Rel 1;
150     C.Appl [C.Rel 11;
151             C.Meta (43, []);
152             C.Appl [C.Rel 15; C.Rel 12; C.Meta (41, [])]];
153     C.Appl [C.Rel 11;
154             C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (11, [])];
155             C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (12, [])]]
156   ] in
157   let subst1 = [
158     (43, ([], C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (11, [])], C.Rel 16));
159     (10, ([], C.Rel 12, C.Rel 16));
160     (12, ([], C.Meta (41, []), C.Rel 16))
161   ]
162   and subst2 = [
163     (43, ([], C.Appl [C.Rel 15; C.Rel 12; C.Meta (11, [])], C.Rel 16));
164     (10, ([], C.Rel 12, C.Rel 16));
165     (12, ([], C.Meta (41, []), C.Rel 16))
166   ] in
167   let t1 = M.apply_subst subst1 term
168   and t2 = M.apply_subst subst2 term in
169   Printf.printf "t1 = %s\nt2 = %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2);
170 ;;
171 *)
172   
173
174 let test_refl () =
175   let module C = Cic in
176   let context = [
177     Some (C.Name "H", C.Decl (
178             C.Prod (C.Name "z", C.Rel 3,
179                     C.Appl [
180                       C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
181                       C.Rel 4; C.Rel 3; C.Rel 1])));
182     Some (C.Name "x", C.Decl (C.Rel 2));
183     Some (C.Name "y", C.Decl (C.Rel 1));
184     Some (C.Name "A", C.Decl (C.Sort C.Set))
185   ]
186   in
187   let term = C.Appl [
188     C.Const (HelmLibraryObjects.Logic.eq_ind_URI, []); C.Rel 4;
189     C.Rel 2;
190     C.Lambda (C.Name "z", C.Rel 4,
191               C.Appl [
192                 C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
193                 C.Rel 5; C.Rel 1; C.Rel 3
194               ]);
195     C.Appl [C.MutConstruct
196               (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); (* reflexivity *)
197             C.Rel 4; C.Rel 2];
198     C.Rel 3;
199 (*     C.Appl [C.Const (HelmLibraryObjects.Logic.sym_eq_URI, []); (\* symmetry *\) *)
200 (*             C.Rel 4; C.Appl [C.Rel 1; C.Rel 2]] *)
201     C.Appl [
202       C.Const (HelmLibraryObjects.Logic.eq_ind_URI, []);
203       C.Rel 4; C.Rel 3;
204       C.Lambda (C.Name "z", C.Rel 4,
205                 C.Appl [
206                   C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
207                   C.Rel 5; C.Rel 1; C.Rel 4
208                 ]);
209       C.Appl [C.MutConstruct (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
210               C.Rel 4; C.Rel 3];
211       C.Rel 2; C.Appl [C.Rel 1; C.Rel 2]
212     ]
213   ] in
214   let ens = [
215     (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var",
216      C.Rel 4);
217     (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var",
218      C.Rel 3);
219     (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var",
220      C.Rel 2);    
221   ] in
222   let term2 = C.Appl [
223     C.Const (HelmLibraryObjects.Logic.sym_eq_URI, ens);
224     C.Appl [C.Rel 1; C.Rel 2]
225   ] in
226   let ty, ug =
227     CicTypeChecker.type_of_aux' [] context term CicUniv.empty_ugraph
228   in
229   Printf.printf "OK, %s ha tipo %s\n" (CicPp.ppterm term) (CicPp.ppterm ty);
230   let ty, ug =
231     CicTypeChecker.type_of_aux' [] context term2 CicUniv.empty_ugraph
232   in
233   Printf.printf "OK, %s ha tipo %s\n" (CicPp.ppterm term2) (CicPp.ppterm ty); 
234 ;;
235
236
237 let test_lib () =
238   let uri = Sys.argv.(1) in
239   let t = CicUtil.term_of_uri (UriManager.uri_of_string uri) in
240   let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
241   Printf.printf "Term of %s: %s\n" uri (CicPp.ppterm t);
242   Printf.printf "type: %s\n" (CicPp.ppterm ty);
243 ;;
244
245
246 (* differing ();; *)
247 (* next_after ();; *)
248 (* discrimination_tree_test ();; *)
249 (* path_indexing_test ();; *)
250 (* test_subst ();; *)
251 Helm_registry.load_from "../../matita/matita.conf.xml";
252 (* test_refl ();; *)
253 test_lib ();;