* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
+module Index = Equality_indexing.DT (* discrimination tree based indexing *)
+(*
+module Index = Equality_indexing.DT (* path tree based indexing *)
+*)
+
let debug_print = Utils.debug_print;;
type retrieval_mode = Matching | Unification;;
-
let print_candidates mode term res =
let _ =
match mode with
let apply_subst = CicMetaSubst.apply_subst
-
-
-(*
-(* NO INDEXING *)
-let init_index () = ()
-
-let empty_table () = []
-
-let index table equality =
- let _, _, (_, l, r, ordering), _, _ = equality in
- match ordering with
- | Utils.Gt -> (Utils.Left, equality)::table
- | Utils.Lt -> (Utils.Right, equality)::table
- | _ -> (Utils.Left, equality)::(Utils.Right, equality)::table
-;;
-
-let remove_index table equality =
- List.filter (fun (p, e) -> e != equality) table
-;;
-
-let in_index table equality =
- List.exists (fun (p, e) -> e == equality) table
-;;
-
-let get_candidates mode table term = table
-*)
-
-
-(*
-(* PATH INDEXING *)
-let init_index () = ()
-
-let empty_table () =
- Path_indexing.PSTrie.empty
-;;
-
-let index = Path_indexing.index
-and remove_index = Path_indexing.remove_index
-and in_index = Path_indexing.in_index;;
-
-let get_candidates mode trie term =
- let t1 = Unix.gettimeofday () in
- let res =
- let s =
- match mode with
- | Matching -> Path_indexing.retrieve_generalizations trie term
- | Unification -> Path_indexing.retrieve_unifiables trie term
-(* Path_indexing.retrieve_all trie term *)
- in
- Path_indexing.PosEqSet.elements s
- in
-(* print_candidates mode term res; *)
- let t2 = Unix.gettimeofday () in
- indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
- res
-;;
+let index = Index.index
+let remove_index = Index.remove_index
+let in_index = Index.in_index
+let empty = Index.empty
+let init_index = Index.init_index
+
+(* returns a list of all the equalities in the tree that are in relation
+ "mode" with the given term, where mode can be either Matching or
+ Unification.
+
+ Format of the return value: list of tuples in the form:
+ (position - Left or Right - of the term that matched the given one in this
+ equality,
+ equality found)
+
+ Note that if equality is "left = right", if the ordering is left > right,
+ the position will always be Left, and if the ordering is left < right,
+ position will be Right.
*)
-
-
-(* DISCRIMINATION TREES *)
-let init_index () =
- Hashtbl.clear Discrimination_tree.arities;
-;;
-
-let empty_table () =
- Discrimination_tree.DiscriminationTree.empty
-;;
-
-let index = Discrimination_tree.index
-and remove_index = Discrimination_tree.remove_index
-and in_index = Discrimination_tree.in_index;;
-
let get_candidates mode tree term =
let t1 = Unix.gettimeofday () in
let res =
let s =
match mode with
- | Matching -> Discrimination_tree.retrieve_generalizations tree term
- | Unification -> Discrimination_tree.retrieve_unifiables tree term
+ | Matching -> Index.retrieve_generalizations tree term
+ | Unification -> Index.retrieve_unifiables tree term
in
- Discrimination_tree.PosEqSet.elements s
+ Index.PosEqSet.elements s
in
-(* print_candidates mode term res; *)
+ (* print_candidates mode term res; *)
(* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
(* print_newline (); *)
let t2 = Unix.gettimeofday () in
termty can be Implicit if it is not needed. The result (one of the sides of
the equality, actually) should be not greater (wrt the term ordering) than
term
+
+ Format of the return value:
+
+ (term to substitute, [Cic.Rel 1 properly lifted - see the various
+ build_newtarget functions inside the various
+ demodulation_* functions]
+ substitution used for the matching,
+ metasenv,
+ ugraph, [substitution, metasenv and ugraph have the same meaning as those
+ returned by CicUnification.fo_unif]
+ (equality where the matching term was found, [i.e. the equality to use as
+ rewrite rule]
+ uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
+ the equality: this is used to build the proof term, again see one of
+ the build_newtarget functions]
+ ))
*)
let rec find_matches metasenv context ugraph lift_amount term termty =
let module C = Cic in
in
match res with
| Some (_, s, _, _, _) ->
- let c' = apply_subst s c
- and other' = apply_subst s other in
+ let c' = apply_subst s c in
+ let other' = U.guarded_simpl context (apply_subst s other) in
let order = cmp c' other' in
let names = U.names_of_context context in
if order = U.Gt then
let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
+ let module U = Utils in
let metasenv, context, ugraph = env in
let _, proof, (eq_ty, left, right, order), metas, args = target in
let metasenv' = metasenv @ metas in
in
let what, other = if pos = Utils.Left then what, other else other, what in
let newterm, newproof =
- let bo = apply_subst subst (S.subst other t) in
+ let bo = U.guarded_simpl context (apply_subst subst (S.subst other t)) in
let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
incr demod_counter;
let bo' =
let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
let what, other = if pos = Utils.Left then what, other else other, what in
let newgoal, newproof =
- let bo' = apply_subst s (S.subst other bo) in
+ let bo' = U.guarded_simpl context (apply_subst s (S.subst other bo)) in
let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
incr sup_l_counter;
let bo'' =
projects / helm.git / blobdiff