]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/paramodulation/test_indexing.ml
New naming policy for local variables.
[helm.git] / helm / ocaml / paramodulation / test_indexing.ml
1 open Path_indexing
2
3 (*
4 let build_equality term =
5   let module C = Cic in
6   C.Implicit None, (C.Implicit None, term, C.Rel 1, Utils.Gt), [], []
7 ;;
8
9
10 (*
11   f = Rel 1
12   g = Rel 2
13   a = Rel 3
14   b = Rel 4
15   c = Rel 5
16 *)
17 let path_indexing_test () =
18   let module C = Cic in
19   let terms = [
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, [])]
25   ] in
26   let path_strings = List.map (path_strings_of_term 0) terms in
27   let table =
28     List.fold_left index PSTrie.empty (List.map build_equality terms) in
29   let query =
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 =
38     String.concat "\n"
39       (PosEqSet.fold
40          (fun (p, e) l ->
41             let s = 
42               "(" ^ (Utils.string_of_pos p) ^ ", " ^
43                 (Inference.string_of_equality e) ^ ")"
44             in
45             s::l)
46          res [])
47   in
48   Printf.printf "path_strings:\n%s\n\n"
49     (String.concat "\n"
50        (List.map
51           (fun l ->
52              "{" ^ (String.concat "; " (List.map string_of_path_string l)) ^ "}"
53           ) path_strings));
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);
61 ;;
62
63
64 let differing () =
65   let module C = Cic in
66   let t1 =
67     C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Meta (1, [])]; C.Rel 5]
68   and t2 = 
69     C.Appl [C.Rel 1; C.Appl [C.Rel 5; C.Rel 4; C.Meta (1, [])]; C.Rel 5]
70   in
71   let res = Inference.extract_differing_subterms t1 t2 in
72   match res with
73   | None -> print_endline "NO DIFFERING SUBTERMS???"
74   | Some (t1, t2) ->
75       Printf.printf "OK: %s, %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2);
76 ;;
77
78
79 let next_after () =
80   let module C = Cic in
81   let t =
82     C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Rel 4]; C.Rel 5]
83   in
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));
89 ;;
90
91
92 let discrimination_tree_test () =
93   let module C = Cic in
94   let terms = [
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]
100   ] in
101   let path_strings =
102     List.map Discrimination_tree.path_string_of_term terms in
103   let table =
104     List.fold_left
105       Discrimination_tree.index
106       Discrimination_tree.DiscriminationTree.empty
107       (List.map build_equality terms)
108   in
109 (*   let query = *)
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 =
119     String.concat "\n"
120       (Discrimination_tree.PosEqSet.fold
121          (fun (p, e) l ->
122             let s = 
123               "(" ^ (Utils.string_of_pos p) ^ ", " ^
124                 (Inference.string_of_equality e) ^ ")"
125             in
126             s::l)
127          res [])
128   in
129   Printf.printf "path_strings:\n%s\n\n"
130     (String.concat "\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);
140 ;;
141
142
143 let test_subst () =
144   let module C = Cic in
145   let module M = CicMetaSubst in
146   let term = C.Appl [
147     C.Rel 1;
148     C.Appl [C.Rel 11;
149             C.Meta (43, []);
150             C.Appl [C.Rel 15; C.Rel 12; C.Meta (41, [])]];
151     C.Appl [C.Rel 11;
152             C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (11, [])];
153             C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (12, [])]]
154   ] in
155   let subst1 = [
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))
159   ]
160   and subst2 = [
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))
164   ] in
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);
168 ;;
169 *)
170   
171
172 let test_refl () =
173   let module C = Cic in
174   let context = [
175     Some (C.Name "H", C.Decl (
176             C.Prod (C.Name "z", C.Rel 3,
177                     C.Appl [
178                       C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
179                       C.Rel 4; C.Rel 3; C.Rel 1])));
180     Some (C.Name "x", C.Decl (C.Rel 2));
181     Some (C.Name "y", C.Decl (C.Rel 1));
182     Some (C.Name "A", C.Decl (C.Sort C.Set))
183   ]
184   in
185   let term = C.Appl [
186     C.Const (HelmLibraryObjects.Logic.eq_ind_URI, []); C.Rel 4;
187     C.Rel 2;
188     C.Lambda (C.Name "z", C.Rel 4,
189               C.Appl [
190                 C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
191                 C.Rel 5; C.Rel 1; C.Rel 3
192               ]);
193     C.Appl [C.MutConstruct
194               (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); (* reflexivity *)
195             C.Rel 4; C.Rel 2];
196     C.Rel 3;
197 (*     C.Appl [C.Const (HelmLibraryObjects.Logic.sym_eq_URI, []); (\* symmetry *\) *)
198 (*             C.Rel 4; C.Appl [C.Rel 1; C.Rel 2]] *)
199     C.Appl [
200       C.Const (HelmLibraryObjects.Logic.eq_ind_URI, []);
201       C.Rel 4; C.Rel 3;
202       C.Lambda (C.Name "z", C.Rel 4,
203                 C.Appl [
204                   C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
205                   C.Rel 5; C.Rel 1; C.Rel 4
206                 ]);
207       C.Appl [C.MutConstruct (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
208               C.Rel 4; C.Rel 3];
209       C.Rel 2; C.Appl [C.Rel 1; C.Rel 2]
210     ]
211   ] in
212   let ens = [
213     (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var",
214      C.Rel 4);
215     (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var",
216      C.Rel 3);
217     (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var",
218      C.Rel 2);    
219   ] in
220   let term2 = C.Appl [
221     C.Const (HelmLibraryObjects.Logic.sym_eq_URI, ens);
222     C.Appl [C.Rel 1; C.Rel 2]
223   ] in
224   let ty, ug =
225     CicTypeChecker.type_of_aux' [] context term CicUniv.empty_ugraph
226   in
227   Printf.printf "OK, %s ha tipo %s\n" (CicPp.ppterm term) (CicPp.ppterm ty);
228   let ty, ug =
229     CicTypeChecker.type_of_aux' [] context term2 CicUniv.empty_ugraph
230   in
231   Printf.printf "OK, %s ha tipo %s\n" (CicPp.ppterm term2) (CicPp.ppterm ty); 
232 ;;
233
234
235 let test_lib () =
236   let uri = Sys.argv.(1) in
237   let t = CicUtil.term_of_uri (UriManager.uri_of_string uri) in
238   let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
239   Printf.printf "Term of %s: %s\n" uri (CicPp.ppterm t);
240   Printf.printf "type: %s\n" (CicPp.ppterm ty);
241 ;;
242
243
244 (* differing ();; *)
245 (* next_after ();; *)
246 (* discrimination_tree_test ();; *)
247 (* path_indexing_test ();; *)
248 (* test_subst ();; *)
249 Helm_registry.load_from "../../matita/matita.conf.xml";
250 (* test_refl ();; *)
251 test_lib ();;