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