cicUtil.cmi: cic.cmo
helmLibraryObjects.cmi: cic.cmo
discrimination_tree.cmi: cic.cmo
+path_indexing.cmi: cic.cmo
cic.cmo: cicUniv.cmi
cic.cmx: cicUniv.cmx
unshare.cmo: cic.cmo unshare.cmi
libraryObjects.cmx: helmLibraryObjects.cmx libraryObjects.cmi
discrimination_tree.cmo: cic.cmo discrimination_tree.cmi
discrimination_tree.cmx: cic.cmx discrimination_tree.cmi
+path_indexing.cmo: cic.cmo path_indexing.cmi
+path_indexing.cmx: cic.cmx path_indexing.cmi
cicUtil.mli \
helmLibraryObjects.mli \
libraryObjects.mli \
- discrimination_tree.mli
+ discrimination_tree.mli \
+ path_indexing.mli
IMPLEMENTATION_FILES = \
cic.ml $(INTERFACE_FILES:%.mli=%.ml)
EXTRA_OBJECTS_TO_INSTALL = cic.ml cic.cmi
* http://cs.unibo.it/helm/.
*)
-module DiscriminationTreeIndexing =
+module DiscriminationTreeIndexing =
functor (A:Set.S) ->
struct
module DiscriminationTree = Trie.Make(PSMap);;
type t = A.t DiscriminationTree.t
- type elt = A.elt
let empty = DiscriminationTree.empty
(*
module DiscriminationTreeIndexing :
functor (A : Set.S) ->
sig
- type path_string_elem = Cic.term
- type path_string = path_string_elem list
val arities : (Cic.term, int) Hashtbl.t
- val path_string_of_term : Cic.term -> Cic.term list
type key = Cic.term
type t
- type elt = A.elt
val empty : t
- val index : t -> Cic.term -> A.elt -> t
- val remove_index : t -> Cic.term -> A.elt -> t
- val in_index : t -> Cic.term -> (A.elt -> bool) -> bool
+ val index : t -> key -> A.elt -> t
+ val remove_index : t -> key -> A.elt -> t
+ val in_index : t -> key -> (A.elt -> bool) -> bool
val retrieve_generalizations : t -> key -> A.t
val retrieve_unifiables : t -> key -> A.t
end
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* path indexing implementation *)
+
+(* position of the subterm, subterm (Appl are not stored...) *)
+
+module PathIndexing =
+ functor(A:Set.S) ->
+ struct
+
+type path_string_elem = Index of int | Term of Cic.term;;
+type path_string = path_string_elem list;;
+
+
+let rec path_strings_of_term index =
+ let module C = Cic in function
+ | C.Meta _ -> [ [Index index; Term (C.Implicit None)] ]
+ | C.Appl (hd::tl) ->
+ let p = if index > 0 then [Index index; Term hd] else [Term hd] in
+ let _, res =
+ List.fold_left
+ (fun (i, r) t ->
+ let rr = path_strings_of_term i t in
+ (i+1, r @ (List.map (fun ps -> p @ ps) rr)))
+ (1, []) tl
+ in
+ res
+ | term -> [ [Index index; Term term] ]
+;;
+
+(*
+let string_of_path_string ps =
+ String.concat "."
+ (List.map
+ (fun e ->
+ let s =
+ match e with
+ | Index i -> "Index " ^ (string_of_int i)
+ | Term t -> "Term " ^ (CicPp.ppterm t)
+ in
+ "(" ^ s ^ ")")
+ ps)
+;;
+*)
+
+module OrderedPathStringElement = struct
+ type t = path_string_elem
+
+ let compare t1 t2 =
+ match t1, t2 with
+ | Index i, Index j -> Pervasives.compare i j
+ | Term t1, Term t2 -> if t1 = t2 then 0 else Pervasives.compare t1 t2
+ | Index _, Term _ -> -1
+ | Term _, Index _ -> 1
+end
+
+module PSMap = Map.Make(OrderedPathStringElement);;
+
+module PSTrie = Trie.Make(PSMap);;
+
+type t = A.t PSTrie.t
+type key = Cic.term
+let empty = PSTrie.empty
+let arities = Hashtbl.create 0
+
+let index trie term info =
+ let ps = path_strings_of_term 0 term in
+ List.fold_left
+ (fun trie ps ->
+ let ps_set = try PSTrie.find ps trie with Not_found -> A.empty in
+ let trie = PSTrie.add ps (A.add info ps_set) trie in
+ trie) trie ps
+
+let remove_index trie term info=
+ let ps = path_strings_of_term 0 term in
+ List.fold_left
+ (fun trie ps ->
+ try
+ let ps_set = A.remove info (PSTrie.find ps trie) in
+ if A.is_empty ps_set then
+ PSTrie.remove ps trie
+ else
+ PSTrie.add ps ps_set trie
+ with Not_found -> trie) trie ps
+;;
+
+let in_index trie term test =
+ let ps = path_strings_of_term 0 term in
+ let ok ps =
+ try
+ let set = PSTrie.find ps trie in
+ A.exists test set
+ with Not_found ->
+ false
+ in
+ List.exists ok ps
+;;
+
+
+let head_of_term = function
+ | Cic.Appl (hd::tl) -> hd
+ | term -> term
+;;
+
+
+let subterm_at_pos index term =
+ if index = 0 then
+ term
+ else
+ match term with
+ | Cic.Appl l ->
+ (try List.nth l index with Failure _ -> raise Not_found)
+ | _ -> raise Not_found
+;;
+
+
+let rec retrieve_generalizations trie term =
+ match trie with
+ | PSTrie.Node (value, map) ->
+ let res =
+ match term with
+ | Cic.Meta _ -> A.empty
+ | term ->
+ let hd_term = head_of_term term in
+ try
+ let n = PSMap.find (Term hd_term) map in
+ match n with
+ | PSTrie.Node (Some s, _) -> s
+ | PSTrie.Node (None, m) ->
+ let l =
+ PSMap.fold
+ (fun k v res ->
+ match k with
+ | Index i ->
+ let t = subterm_at_pos i term in
+ let s = retrieve_generalizations v t in
+ s::res
+ | _ -> res)
+ m []
+ in
+ match l with
+ | hd::tl ->
+ List.fold_left (fun r s -> A.inter r s) hd tl
+ | _ -> A.empty
+ with Not_found ->
+ A.empty
+ in
+ try
+ let n = PSMap.find (Term (Cic.Implicit None)) map in
+ match n with
+ | PSTrie.Node (Some s, _) -> A.union res s
+ | _ -> res
+ with Not_found ->
+ res
+;;
+
+
+let rec retrieve_unifiables trie term =
+ match trie with
+ | PSTrie.Node (value, map) ->
+ let res =
+ match term with
+ | Cic.Meta _ ->
+ PSTrie.fold
+ (fun ps v res -> A.union res v)
+ (PSTrie.Node (None, map))
+ A.empty
+ | _ ->
+ let hd_term = head_of_term term in
+ try
+ let n = PSMap.find (Term hd_term) map in
+ match n with
+ | PSTrie.Node (Some v, _) -> v
+ | PSTrie.Node (None, m) ->
+ let l =
+ PSMap.fold
+ (fun k v res ->
+ match k with
+ | Index i ->
+ let t = subterm_at_pos i term in
+ let s = retrieve_unifiables v t in
+ s::res
+ | _ -> res)
+ m []
+ in
+ match l with
+ | hd::tl ->
+ List.fold_left (fun r s -> A.inter r s) hd tl
+ | _ -> A.empty
+ with Not_found ->
+ A.empty
+ in
+ try
+ let n = PSMap.find (Term (Cic.Implicit None)) map in
+ match n with
+ | PSTrie.Node (Some s, _) -> A.union res s
+ | _ -> res
+ with Not_found ->
+ res
+;;
+
+end
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+module PathIndexing :
+ functor (A : Set.S) ->
+ sig
+ val arities : (Cic.term, int) Hashtbl.t
+
+ type key = Cic.term
+ type t
+
+ val empty : t
+ val index : t -> key -> A.elt -> t
+ val remove_index : t -> key -> A.elt -> t
+ val in_index : t -> key -> (A.elt -> bool) -> bool
+ val retrieve_generalizations : t -> key -> A.t
+ val retrieve_unifiables : t -> key -> A.t
+ end
+
+
inference.cmi: utils.cmi
+equality_indexing.cmi: utils.cmi inference.cmi
utils.cmo: utils.cmi
utils.cmx: utils.cmi
inference.cmo: utils.cmi inference.cmi
inference.cmx: utils.cmx inference.cmi
-path_indexing.cmo: utils.cmi inference.cmi
-path_indexing.cmx: utils.cmx inference.cmx
-indexing.cmo: utils.cmi inference.cmi
-indexing.cmx: utils.cmx inference.cmx
+equality_indexing.cmo: utils.cmi inference.cmi equality_indexing.cmi
+equality_indexing.cmx: utils.cmx inference.cmx equality_indexing.cmi
+indexing.cmo: utils.cmi inference.cmi equality_indexing.cmi
+indexing.cmx: utils.cmx inference.cmx equality_indexing.cmx
saturation.cmo: utils.cmi inference.cmi indexing.cmo
saturation.cmx: utils.cmx inference.cmx indexing.cmx
INTERFACE_FILES = \
utils.mli \
- inference.mli
+ inference.mli\
+ equality_indexing.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) \
- path_indexing.ml \
indexing.ml \
saturation.ml
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+module type EqualityIndex =
+ sig
+ module PosEqSet : Set.S with type elt = Utils.pos * Inference.equality
+ val arities : (Cic.term, int) Hashtbl.t
+ type key = Cic.term
+ type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t
+ val empty : t
+ val retrieve_generalizations : t -> key -> PosEqSet.t
+ val retrieve_unifiables : t -> key -> PosEqSet.t
+ val init_index : unit -> unit
+ val remove_index : t -> Inference.equality -> t
+ val index : t -> Inference.equality -> t
+ val in_index : t -> Inference.equality -> bool
+ end
+
+module DT =
+struct
+ module OrderedPosEquality = struct
+ type t = Utils.pos * Inference.equality
+ let compare = Pervasives.compare
+ end
+
+ module PosEqSet = Set.Make(OrderedPosEquality);;
+
+ include Discrimination_tree.DiscriminationTreeIndexing(PosEqSet)
+
+
+ (* DISCRIMINATION TREES *)
+ let init_index () =
+ Hashtbl.clear arities;
+ ;;
+
+ let remove_index tree equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ match ordering with
+ | Utils.Gt -> remove_index tree l (Utils.Left, equality)
+ | Utils.Lt -> remove_index tree r (Utils.Right, equality)
+ | _ ->
+ let tree = remove_index tree r (Utils.Right, equality) in
+ remove_index tree l (Utils.Left, equality)
+
+ let index tree equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ match ordering with
+ | Utils.Gt -> index tree l (Utils.Left, equality)
+ | Utils.Lt -> index tree r (Utils.Right, equality)
+ | _ ->
+ let tree = index tree r (Utils.Right, equality) in
+ index tree l (Utils.Left, equality)
+
+
+ let in_index tree equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ let meta_convertibility (pos,equality') =
+ Inference.meta_convertibility_eq equality equality'
+ in
+ in_index tree l meta_convertibility || in_index tree r meta_convertibility
+
+ end
+
+module PT =
+ struct
+ module OrderedPosEquality = struct
+ type t = Utils.pos * Inference.equality
+ let compare = Pervasives.compare
+ end
+
+ module PosEqSet = Set.Make(OrderedPosEquality);;
+
+ include Discrimination_tree.DiscriminationTreeIndexing(PosEqSet)
+
+
+ (* DISCRIMINATION TREES *)
+ let init_index () =
+ Hashtbl.clear arities;
+ ;;
+
+ let remove_index tree equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ match ordering with
+ | Utils.Gt -> remove_index tree l (Utils.Left, equality)
+ | Utils.Lt -> remove_index tree r (Utils.Right, equality)
+ | _ ->
+ let tree = remove_index tree r (Utils.Right, equality) in
+ remove_index tree l (Utils.Left, equality)
+
+ let index tree equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ match ordering with
+ | Utils.Gt -> index tree l (Utils.Left, equality)
+ | Utils.Lt -> index tree r (Utils.Right, equality)
+ | _ ->
+ let tree = index tree r (Utils.Right, equality) in
+ index tree l (Utils.Left, equality)
+
+
+ let in_index tree equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ let meta_convertibility (pos,equality') =
+ Inference.meta_convertibility_eq equality equality'
+ in
+ in_index tree l meta_convertibility || in_index tree r meta_convertibility
+end
+
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+module type EqualityIndex =
+ sig
+ module PosEqSet : Set.S with type elt = Utils.pos * Inference.equality
+ val arities : (Cic.term, int) Hashtbl.t
+ type key = Cic.term
+ type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t
+ val empty : t
+ val retrieve_generalizations : t -> key -> PosEqSet.t
+ val retrieve_unifiables : t -> key -> PosEqSet.t
+ val init_index : unit -> unit
+ val remove_index : t -> Inference.equality -> t
+ val index : t -> Inference.equality -> t
+ val in_index : t -> Inference.equality -> bool
+ end
+
+module DT : EqualityIndex
+module PT : EqualityIndex
+
* http://cs.unibo.it/helm/.
*)
-module OrderedPosEquality = struct
- type t = Utils.pos * Inference.equality
- let compare = Pervasives.compare
- end
-
-module PosEqSet = Set.Make(OrderedPosEquality);;
-
-module DT = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet);;
+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
-let remove_index tree equality =
- let _, _, (_, l, r, ordering), _, _ = equality in
- match ordering with
- | Utils.Gt -> DT.remove_index tree l equality
- | Utils.Lt -> DT.remove_index tree r equality
- | _ ->
- DT.remove_index (DT.remove_index tree r equality) l equality
-
-
-let 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
-;;
-*)
-
-(* DISCRIMINATION TREES *)
-let init_index () =
- Hashtbl.clear DT.arities;
-;;
-
-let empty_table () =
- DT.empty
-;;
-
-let remove_index tree equality =
- let _, _, (_, l, r, ordering), _, _ = equality in
- match ordering with
- | Utils.Gt -> DT.remove_index tree l (Utils.Left, equality)
- | Utils.Lt -> DT.remove_index tree r (Utils.Right, equality)
- | _ ->
- let tree = DT.remove_index tree r (Utils.Right, equality) in
- DT.remove_index tree l (Utils.Left, equality)
-
-let index tree equality =
- let _, _, (_, l, r, ordering), _, _ = equality in
- match ordering with
- | Utils.Gt -> DT.index tree l (Utils.Left, equality)
- | Utils.Lt -> DT.index tree r (Utils.Right, equality)
- | _ ->
- let tree = DT.index tree r (Utils.Right, equality) in
- DT.index tree l (Utils.Left, equality)
-
-
-let in_index tree equality =
- let _, _, (_, l, r, ordering), _, _ = equality in
- let meta_convertibility (pos,equality') =
- Inference.meta_convertibility_eq equality equality'
- in
- DT.in_index tree l meta_convertibility || DT.in_index tree r meta_convertibility
-
+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
let res =
let s =
match mode with
- | Matching -> DT.retrieve_generalizations tree term
- | Unification -> DT.retrieve_unifiables tree term
+ | Matching -> Index.retrieve_generalizations tree term
+ | Unification -> Index.retrieve_unifiables tree term
in
- PosEqSet.elements s
+ Index.PosEqSet.elements s
in
(* print_candidates mode term res; *)
(* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
+++ /dev/null
-(* Copyright (C) 2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* path indexing implementation *)
-
-(* position of the subterm, subterm (Appl are not stored...) *)
-type path_string_elem = Index of int | Term of Cic.term;;
-type path_string = path_string_elem list;;
-
-
-let rec path_strings_of_term index =
- let module C = Cic in function
- | C.Meta _ -> [ [Index index; Term (C.Implicit None)] ]
- | C.Appl (hd::tl) ->
- let p = if index > 0 then [Index index; Term hd] else [Term hd] in
- let _, res =
- List.fold_left
- (fun (i, r) t ->
- let rr = path_strings_of_term i t in
- (i+1, r @ (List.map (fun ps -> p @ ps) rr)))
- (1, []) tl
- in
- res
- | term -> [ [Index index; Term term] ]
-;;
-
-
-let string_of_path_string ps =
- String.concat "."
- (List.map
- (fun e ->
- let s =
- match e with
- | Index i -> "Index " ^ (string_of_int i)
- | Term t -> "Term " ^ (CicPp.ppterm t)
- in
- "(" ^ s ^ ")")
- ps)
-;;
-
-
-module OrderedPathStringElement = struct
- type t = path_string_elem
-
- let compare t1 t2 =
- match t1, t2 with
- | Index i, Index j -> Pervasives.compare i j
- | Term t1, Term t2 -> if t1 = t2 then 0 else Pervasives.compare t1 t2
- | Index _, Term _ -> -1
- | Term _, Index _ -> 1
-end
-
-module PSMap = Map.Make(OrderedPathStringElement);;
-
-module OrderedPosEquality = struct
- type t = Utils.pos * Inference.equality
-
- let compare = Pervasives.compare
-end
-
-module PosEqSet = Set.Make(OrderedPosEquality);;
-
-
-module PSTrie = Trie.Make(PSMap);;
-
-
-let index trie equality =
- let _, _, (_, l, r, ordering), _, _ = equality in
- let psl = path_strings_of_term 0 l
- and psr = path_strings_of_term 0 r in
- let index pos trie ps =
- let ps_set = try PSTrie.find ps trie with Not_found -> PosEqSet.empty in
- let trie = PSTrie.add ps (PosEqSet.add (pos, equality) ps_set) trie in
- trie
- in
- match ordering with
- | Utils.Gt -> List.fold_left (index Utils.Left) trie psl
- | Utils.Lt -> List.fold_left (index Utils.Right) trie psr
- | _ ->
- let trie = List.fold_left (index Utils.Left) trie psl in
- List.fold_left (index Utils.Right) trie psr
-;;
-
-
-let remove_index trie equality =
- let _, _, (_, l, r, ordering), _, _ = equality in
- let psl = path_strings_of_term 0 l
- and psr = path_strings_of_term 0 r in
- let remove_index pos trie ps =
- try
- let ps_set = PosEqSet.remove (pos, equality) (PSTrie.find ps trie) in
- if PosEqSet.is_empty ps_set then
- PSTrie.remove ps trie
- else
- PSTrie.add ps ps_set trie
- with Not_found ->
- trie
- in
- match ordering with
- | Utils.Gt -> List.fold_left (remove_index Utils.Left) trie psl
- | Utils.Lt -> List.fold_left (remove_index Utils.Right) trie psr
- | _ ->
- let trie = List.fold_left (remove_index Utils.Left) trie psl in
- List.fold_left (remove_index Utils.Right) trie psr
-;;
-
-
-let in_index trie equality =
- let _, _, (_, l, r, ordering), _, _ = equality in
- let psl = path_strings_of_term 0 l
- and psr = path_strings_of_term 0 r in
- let meta_convertibility = Inference.meta_convertibility_eq equality in
- let ok ps =
- try
- let set = PSTrie.find ps trie in
- PosEqSet.exists (fun (p, e) -> meta_convertibility e) set
- with Not_found ->
- false
- in
- (List.exists ok psl) || (List.exists ok psr)
-;;
-
-
-let head_of_term = function
- | Cic.Appl (hd::tl) -> hd
- | term -> term
-;;
-
-
-let subterm_at_pos index term =
- if index = 0 then
- term
- else
- match term with
- | Cic.Appl l ->
- (try List.nth l index with Failure _ -> raise Not_found)
- | _ -> raise Not_found
-;;
-
-
-let rec retrieve_generalizations trie term =
- match trie with
- | PSTrie.Node (value, map) ->
- let res =
- match term with
- | Cic.Meta _ -> PosEqSet.empty
- | term ->
- let hd_term = head_of_term term in
- try
- let n = PSMap.find (Term hd_term) map in
- match n with
- | PSTrie.Node (Some s, _) -> s
- | PSTrie.Node (None, m) ->
- let l =
- PSMap.fold
- (fun k v res ->
- match k with
- | Index i ->
- let t = subterm_at_pos i term in
- let s = retrieve_generalizations v t in
- s::res
- | _ -> res)
- m []
- in
- match l with
- | hd::tl ->
- List.fold_left (fun r s -> PosEqSet.inter r s) hd tl
- | _ -> PosEqSet.empty
- with Not_found ->
- PosEqSet.empty
- in
- try
- let n = PSMap.find (Term (Cic.Implicit None)) map in
- match n with
- | PSTrie.Node (Some s, _) -> PosEqSet.union res s
- | _ -> res
- with Not_found ->
- res
-;;
-
-
-let rec retrieve_unifiables trie term =
- match trie with
- | PSTrie.Node (value, map) ->
- let res =
- match term with
- | Cic.Meta _ ->
- PSTrie.fold
- (fun ps v res -> PosEqSet.union res v)
- (PSTrie.Node (None, map))
- PosEqSet.empty
- | _ ->
- let hd_term = head_of_term term in
- try
- let n = PSMap.find (Term hd_term) map in
- match n with
- | PSTrie.Node (Some v, _) -> v
- | PSTrie.Node (None, m) ->
- let l =
- PSMap.fold
- (fun k v res ->
- match k with
- | Index i ->
- let t = subterm_at_pos i term in
- let s = retrieve_unifiables v t in
- s::res
- | _ -> res)
- m []
- in
- match l with
- | hd::tl ->
- List.fold_left (fun r s -> PosEqSet.inter r s) hd tl
- | _ -> PosEqSet.empty
- with Not_found ->
- PosEqSet.empty
- in
- try
- let n = PSMap.find (Term (Cic.Implicit None)) map in
- match n with
- | PSTrie.Node (Some s, _) -> PosEqSet.union res s
- | _ -> res
- with Not_found ->
- res
-;;
-
-
-let retrieve_all trie term =
- PSTrie.fold
- (fun k v s -> PosEqSet.union v s) trie PosEqSet.empty
-;;
-
-
-let string_of_pstrie trie =
- let rec to_string level = function
- | PSTrie.Node (v, map) ->
- let s =
- match v with
- | Some v ->
- (String.make (2 * level) ' ') ^
- "{" ^ (String.concat "; "
- (List.map
- (fun (p, e) ->
- "(" ^ (Utils.string_of_pos p) ^ ", " ^
- (Inference.string_of_equality e) ^ ")")
- (PosEqSet.elements v))) ^ "}"
- | None -> ""
- in
- let rest =
- String.concat "\n"
- (PSMap.fold
- (fun k v s ->
- let ks =
- match k with
- | Index i -> "Index " ^ (string_of_int i)
- | Term t -> "Term " ^ (CicPp.ppterm t)
- in
- let rs = to_string (level+1) v in
- ((String.make (2 * level) ' ') ^ ks ^ "\n" ^ rs)::s)
- map [])
- in
- s ^ rest
- in
- to_string 0 trie
-;;
-
List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
in
let table =
- List.fold_left (fun tbl e -> Indexing.index tbl e)
- (Indexing.empty_table ()) pos
+ List.fold_left (fun tbl e -> Indexing.index tbl e) Indexing.empty pos
in
(neg, set_of neg),
(pos, set_of pos),
let make_active () =
- [], Indexing.empty_table ()
+ [], Indexing.empty
;;
maximal_retained_equality := Some (EqualitySet.max_elt ps);
let tbl =
EqualitySet.fold
- (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
+ (fun e tbl -> Indexing.index tbl e) ps Indexing.empty
in
(nl, ns), (pl, ps), tbl
;;
let neg, pos = infer_positive table tl in
neg, res @ pos
in
- let curr_table = Indexing.index (Indexing.empty_table ()) current in
+ let curr_table = Indexing.index Indexing.empty current in
let neg, pos = infer_positive curr_table active_list in
neg, res @ pos
in
)
else
(s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
- active_list ([], Indexing.empty_table ()),
+ active_list ([], Indexing.empty),
List.fold_right
(fun (s, eq) (n, p) ->
if (s <> Negative) && (is_identity env eq) then (
and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
let passive_table =
List.fold_left
- (fun tbl e -> Indexing.index tbl e) (Indexing.empty_table ()) pl
+ (fun tbl e -> Indexing.index tbl e) Indexing.empty pl
in
match newn, newp with
| [], [] -> ((nl, ns), (pl, ps), passive_table), None
(fun (l, t, w) e ->
let ew, _, _, _, _ = e in
(Positive, e)::l, Indexing.index t e, min ew w)
- ([], Indexing.empty_table (), 1000000) (snd new')
+ ([], Indexing.empty, 1000000) (snd new')
in
let active, newa =
backward_simplify_active env new_pos new_table min_weight active in
let tbl =
List.fold_left
(fun t (_, e) -> Indexing.index t e)
- (Indexing.empty_table ()) active
+ Indexing.empty active
in
let res = forward_simplify env e (active, tbl) in
match others with
let tbl =
List.fold_left
(fun t (_, e) -> Indexing.index t e)
- (Indexing.empty_table ()) active
+ Indexing.empty active
in
let res = forward_simplify env e (active, tbl) in
match others with
let tbl =
List.fold_left
(fun t (_, e) -> Indexing.index t e)
- (Indexing.empty_table ()) active
+ Indexing.empty active
in
let res = forward_simplify env (Positive, e) (active, tbl) in
match others with
let tbl =
List.fold_left
(fun t (_, e) -> Indexing.index t e)
- (Indexing.empty_table ()) active
+ Indexing.empty active
in
let res = forward_simplify env e (active, tbl) in
match others with
projects / helm.git / commitdiff