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 ();;