open Path_indexing let build_equality term = let module C = Cic in C.Implicit None, (C.Implicit None, term, C.Rel 1, Utils.Gt), [], [] ;; (* f = Rel 1 g = Rel 2 a = Rel 3 b = Rel 4 c = Rel 5 *) let path_indexing_test () = let module C = Cic in let terms = [ C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Meta (1, [])]; C.Rel 5]; C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 4]; C.Meta (1, [])]; C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Rel 4]; C.Rel 5]; C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 5]; C.Rel 4]; C.Appl [C.Rel 1; C.Meta (1, []); C.Meta (1, [])] ] in let path_strings = List.map (path_strings_of_term 0) terms in let table = List.fold_left index PSTrie.empty (List.map build_equality terms) in let query = C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 4]; C.Rel 5] in let matches = retrieve_generalizations table query in let unifications = retrieve_unifiables table query in let eq1 = build_equality (C.Appl [C.Rel 1; C.Meta (1, []); C.Meta (1, [])]) and eq2 = build_equality (C.Appl [C.Rel 1; C.Meta (1, []); C.Meta (2, [])]) in let res1 = in_index table eq1 and res2 = in_index table eq2 in let print_results res = String.concat "\n" (PosEqSet.fold (fun (p, e) l -> let s = "(" ^ (Utils.string_of_pos p) ^ ", " ^ (Inference.string_of_equality e) ^ ")" in s::l) res []) in Printf.printf "path_strings:\n%s\n\n" (String.concat "\n" (List.map (fun l -> "{" ^ (String.concat "; " (List.map string_of_path_string l)) ^ "}" ) path_strings)); Printf.printf "table:\n%s\n\n" (string_of_pstrie table); Printf.printf "matches:\n%s\n\n" (print_results matches); Printf.printf "unifications:\n%s\n\n" (print_results unifications); Printf.printf "in_index %s: %s\n" (Inference.string_of_equality eq1) (string_of_bool res1); Printf.printf "in_index %s: %s\n" (Inference.string_of_equality eq2) (string_of_bool res2); ;; let differing () = let module C = Cic in let t1 = C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Meta (1, [])]; C.Rel 5] and t2 = C.Appl [C.Rel 1; C.Appl [C.Rel 5; C.Rel 4; C.Meta (1, [])]; C.Rel 5] in let res = Inference.extract_differing_subterms t1 t2 in match res with | None -> print_endline "NO DIFFERING SUBTERMS???" | Some (t1, t2) -> Printf.printf "OK: %s, %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); ;; let next_after () = let module C = Cic in let t = C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Rel 4]; C.Rel 5] in let pos1 = Discrimination_tree.next_t [1] t in let pos2 = Discrimination_tree.after_t [1] t in Printf.printf "next_t 1: %s\nafter_t 1: %s\n" (CicPp.ppterm (Discrimination_tree.subterm_at_pos pos1 t)) (CicPp.ppterm (Discrimination_tree.subterm_at_pos pos2 t)); ;; let discrimination_tree_test () = let module C = Cic in let terms = [ C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Meta (1, [])]; C.Rel 5]; C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 4]; C.Meta (1, [])]; C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Rel 4]; C.Rel 5]; C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 5]; C.Rel 4]; C.Appl [C.Rel 10; C.Meta (5, []); C.Rel 11] ] in let path_strings = List.map Discrimination_tree.path_string_of_term terms in let table = List.fold_left Discrimination_tree.index Discrimination_tree.DiscriminationTree.empty (List.map build_equality terms) in (* let query = *) (* C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 4]; C.Rel 5] in *) let query = C.Appl [C.Rel 10; C.Meta (14, []); C.Meta (13, [])] in let matches = Discrimination_tree.retrieve_generalizations table query in let unifications = Discrimination_tree.retrieve_unifiables table query in let eq1 = build_equality (C.Appl [C.Rel 1; C.Meta (1, []); C.Meta (1, [])]) and eq2 = build_equality (C.Appl [C.Rel 1; C.Meta (1, []); C.Meta (2, [])]) in let res1 = Discrimination_tree.in_index table eq1 and res2 = Discrimination_tree.in_index table eq2 in let print_results res = String.concat "\n" (Discrimination_tree.PosEqSet.fold (fun (p, e) l -> let s = "(" ^ (Utils.string_of_pos p) ^ ", " ^ (Inference.string_of_equality e) ^ ")" in s::l) res []) in Printf.printf "path_strings:\n%s\n\n" (String.concat "\n" (List.map Discrimination_tree.string_of_path_string path_strings)); Printf.printf "table:\n%s\n\n" (Discrimination_tree.string_of_discrimination_tree table); Printf.printf "matches:\n%s\n\n" (print_results matches); Printf.printf "unifications:\n%s\n\n" (print_results unifications); Printf.printf "in_index %s: %s\n" (Inference.string_of_equality eq1) (string_of_bool res1); Printf.printf "in_index %s: %s\n" (Inference.string_of_equality eq2) (string_of_bool res2); ;; let test_subst () = let module C = Cic in let module M = CicMetaSubst in let term = C.Appl [ C.Rel 1; C.Appl [C.Rel 11; C.Meta (43, []); C.Appl [C.Rel 15; C.Rel 12; C.Meta (41, [])]]; C.Appl [C.Rel 11; C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (11, [])]; C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (12, [])]] ] in let subst1 = [ (43, ([], C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (11, [])], C.Rel 16)); (10, ([], C.Rel 12, C.Rel 16)); (12, ([], C.Meta (41, []), C.Rel 16)) ] and subst2 = [ (43, ([], C.Appl [C.Rel 15; C.Rel 12; C.Meta (11, [])], C.Rel 16)); (10, ([], C.Rel 12, C.Rel 16)); (12, ([], C.Meta (41, []), C.Rel 16)) ] in let t1 = M.apply_subst subst1 term and t2 = M.apply_subst subst2 term in Printf.printf "t1 = %s\nt2 = %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); ;; (* differing ();; *) (* next_after ();; *) (* discrimination_tree_test ();; *) (* path_indexing_test ();; *) test_subst ();;