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 main_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 (* differing ();; *)
  93 (* main_test ();; *)
  94 next_after ();;
  95