From b52f57d8573a909a486d52a7317e017f56d07199 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 19 Dec 2005 13:57:45 +0000 Subject: [PATCH] Discrimination and trie removed. --- helm/ocaml/paramodulation/.depend | 10 +- helm/ocaml/paramodulation/Makefile | 4 +- helm/ocaml/paramodulation/README | 22 ++ .../paramodulation/discrimination_tree.ml | 303 ------------------ helm/ocaml/paramodulation/indexing.ml | 72 ++++- helm/ocaml/paramodulation/inference.ml | 6 +- helm/ocaml/paramodulation/saturate_main.ml | 1 + helm/ocaml/paramodulation/saturation.ml | 5 +- helm/ocaml/paramodulation/trie.ml | 153 --------- helm/ocaml/paramodulation/utils.ml | 70 +++- helm/ocaml/paramodulation/utils.mli | 4 + 11 files changed, 161 insertions(+), 489 deletions(-) delete mode 100644 helm/ocaml/paramodulation/discrimination_tree.ml delete mode 100644 helm/ocaml/paramodulation/trie.ml diff --git a/helm/ocaml/paramodulation/.depend b/helm/ocaml/paramodulation/.depend index 8a74093c5..ec3ba7d6c 100644 --- a/helm/ocaml/paramodulation/.depend +++ b/helm/ocaml/paramodulation/.depend @@ -3,11 +3,9 @@ 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 trie.cmo inference.cmi -path_indexing.cmx: utils.cmx trie.cmx inference.cmx -discrimination_tree.cmo: utils.cmi trie.cmo inference.cmi -discrimination_tree.cmx: utils.cmx trie.cmx inference.cmx -indexing.cmo: utils.cmi inference.cmi discrimination_tree.cmo -indexing.cmx: utils.cmx inference.cmx discrimination_tree.cmx +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 saturation.cmo: utils.cmi inference.cmi indexing.cmo saturation.cmx: utils.cmx inference.cmx indexing.cmx diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile index df2c25d22..683bac671 100644 --- a/helm/ocaml/paramodulation/Makefile +++ b/helm/ocaml/paramodulation/Makefile @@ -2,12 +2,10 @@ PACKAGE = paramodulation INTERFACE_FILES = \ utils.mli \ - inference.mli + inference.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) \ - trie.ml \ path_indexing.ml \ - discrimination_tree.ml \ indexing.ml \ saturation.ml diff --git a/helm/ocaml/paramodulation/README b/helm/ocaml/paramodulation/README index d7cd0b98d..98deef5ad 100644 --- a/helm/ocaml/paramodulation/README +++ b/helm/ocaml/paramodulation/README @@ -19,3 +19,25 @@ Usage: -retrieve retrieve only -help Display this list of options --help Display this list of options + + +./saturate -l 10 -demod-equalities + +dove -l 10 e` il timeout in secondi. + +Il programma legge da standard input il teorema, per esempio + +\forall n:nat.n + n = 2 * n + +l'input termina con una riga vuota (quindi basta un doppio invio alla fine) + +In output, oltre ai vari messaggi di debug, vengono stampati gli insiemi +active e passive alla fine dell'esecuzione. Consiglio di redirigere l'output +su file, per esempio usando tee: + +./saturate -l 10 -demod-equalities | tee output.txt + +Il formato di stampa e` quello per gli oggetti di tipo equality (usa la +funzione Inference.string_of_equality) + + diff --git a/helm/ocaml/paramodulation/discrimination_tree.ml b/helm/ocaml/paramodulation/discrimination_tree.ml deleted file mode 100644 index d73eb9c3a..000000000 --- a/helm/ocaml/paramodulation/discrimination_tree.ml +++ /dev/null @@ -1,303 +0,0 @@ -(* 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/. - *) - -type path_string_elem = Cic.term;; -type path_string = path_string_elem list;; - - -(* needed by the retrieve_* functions, to know the arities of the "functions" *) -let arities = Hashtbl.create 11;; - - -let rec path_string_of_term = function - | Cic.Meta _ -> [Cic.Implicit None] - | Cic.Appl ((hd::tl) as l) -> - if not (Hashtbl.mem arities hd) then - Hashtbl.add arities hd (List.length tl); - List.concat (List.map path_string_of_term l) - | term -> [term] -;; - - -let string_of_path_string ps = - String.concat "." (List.map CicPp.ppterm ps) -;; - - -module OrderedPathStringElement = struct - type t = path_string_elem - - let compare = Pervasives.compare -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 DiscriminationTree = Trie.Make(PSMap);; - - -let string_of_discrimination_tree tree = - let rec to_string level = function - | DiscriminationTree.Node (value, map) -> - let s = - match value 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 = CicPp.ppterm k 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 tree -;; - - -let index tree equality = - let _, _, (_, l, r, ordering), _, _ = equality in - let psl = path_string_of_term l - and psr = path_string_of_term r in - let index pos tree ps = - let ps_set = - try DiscriminationTree.find ps tree with Not_found -> PosEqSet.empty in - let tree = - DiscriminationTree.add ps (PosEqSet.add (pos, equality) ps_set) tree in - tree - in - match ordering with - | Utils.Gt -> index Utils.Left tree psl - | Utils.Lt -> index Utils.Right tree psr - | _ -> - let tree = index Utils.Left tree psl in - index Utils.Right tree psr -;; - - -let remove_index tree equality = - let _, _, (_, l, r, ordering), _, _ = equality in - let psl = path_string_of_term l - and psr = path_string_of_term r in - let remove_index pos tree ps = - try - let ps_set = - PosEqSet.remove (pos, equality) (DiscriminationTree.find ps tree) in - if PosEqSet.is_empty ps_set then - DiscriminationTree.remove ps tree - else - DiscriminationTree.add ps ps_set tree - with Not_found -> - tree - in - match ordering with - | Utils.Gt -> remove_index Utils.Left tree psl - | Utils.Lt -> remove_index Utils.Right tree psr - | _ -> - let tree = remove_index Utils.Left tree psl in - remove_index Utils.Right tree psr -;; - - -let in_index tree equality = - let _, _, (_, l, r, ordering), _, _ = equality in - let psl = path_string_of_term l - and psr = path_string_of_term r in - let meta_convertibility = Inference.meta_convertibility_eq equality in - let ok ps = - try - let set = DiscriminationTree.find ps tree in - PosEqSet.exists (fun (p, e) -> meta_convertibility e) set - with Not_found -> - false - in - (ok psl) || (ok psr) -;; - - -let head_of_term = function - | Cic.Appl (hd::tl) -> hd - | term -> term -;; - - -let rec subterm_at_pos pos term = - match pos with - | [] -> term - | index::pos -> - match term with - | Cic.Appl l -> - (try subterm_at_pos pos (List.nth l index) - with Failure _ -> raise Not_found) - | _ -> raise Not_found -;; - - -let rec after_t pos term = - let pos' = - match pos with - | [] -> raise Not_found - | pos -> List.fold_right (fun i r -> if r = [] then [i+1] else i::r) pos [] - in - try - let t = subterm_at_pos pos' term in pos' - with Not_found -> - let pos, _ = - List.fold_right - (fun i (r, b) -> if b then (i::r, true) else (r, true)) pos ([], false) - in - after_t pos term -;; - - -let next_t pos term = - let t = subterm_at_pos pos term in - try - let _ = subterm_at_pos [1] t in - pos @ [1] - with Not_found -> - match pos with - | [] -> [1] - | pos -> after_t pos term -;; - - -let retrieve_generalizations tree term = - let rec retrieve tree term pos = - match tree with - | DiscriminationTree.Node (Some s, _) when pos = [] -> s - | DiscriminationTree.Node (_, map) -> - let res = - try - let hd_term = head_of_term (subterm_at_pos pos term) in - let n = PSMap.find hd_term map in - match n with - | DiscriminationTree.Node (Some s, _) -> s - | DiscriminationTree.Node (None, _) -> - let newpos = try next_t pos term with Not_found -> [] in - retrieve n term newpos - with Not_found -> - PosEqSet.empty - in - try - let n = PSMap.find (Cic.Implicit None) map in - let newpos = try after_t pos term with Not_found -> [-1] in - if newpos = [-1] then - match n with - | DiscriminationTree.Node (Some s, _) -> PosEqSet.union s res - | _ -> res - else - PosEqSet.union res (retrieve n term newpos) - with Not_found -> - res - in - retrieve tree term [] -;; - - -let jump_list = function - | DiscriminationTree.Node (value, map) -> - let rec get n tree = - match tree with - | DiscriminationTree.Node (v, m) -> - if n = 0 then - [tree] - else - PSMap.fold - (fun k v res -> - let a = try Hashtbl.find arities k with Not_found -> 0 in - (get (n-1 + a) v) @ res) m [] - in - PSMap.fold - (fun k v res -> - let arity = try Hashtbl.find arities k with Not_found -> 0 in - (get arity v) @ res) - map [] -;; - - -let retrieve_unifiables tree term = - let rec retrieve tree term pos = - match tree with - | DiscriminationTree.Node (Some s, _) when pos = [] -> s - | DiscriminationTree.Node (_, map) -> - let subterm = - try Some (subterm_at_pos pos term) with Not_found -> None - in - match subterm with - | None -> PosEqSet.empty - | Some (Cic.Meta _) -> - let newpos = try next_t pos term with Not_found -> [] in - let jl = jump_list tree in - List.fold_left - (fun r s -> PosEqSet.union r s) - PosEqSet.empty - (List.map (fun t -> retrieve t term newpos) jl) - | Some subterm -> - let res = - try - let hd_term = head_of_term subterm in - let n = PSMap.find hd_term map in - match n with - | DiscriminationTree.Node (Some s, _) -> s - | DiscriminationTree.Node (None, _) -> - retrieve n term (next_t pos term) - with Not_found -> - PosEqSet.empty - in - try - let n = PSMap.find (Cic.Implicit None) map in - let newpos = try after_t pos term with Not_found -> [-1] in - if newpos = [-1] then - match n with - | DiscriminationTree.Node (Some s, _) -> PosEqSet.union s res - | _ -> res - else - PosEqSet.union res (retrieve n term newpos) - with Not_found -> - res - in - retrieve tree term [] -;; diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index cb20afd81..8c4137556 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -23,6 +23,15 @@ * 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);; + let debug_print = Utils.debug_print;; @@ -53,8 +62,6 @@ let indexing_retrieval_time = ref 0.;; let apply_subst = CicMetaSubst.apply_subst - - (* (* NO INDEXING *) let init_index () = () @@ -90,8 +97,16 @@ let empty_table () = ;; let index = Path_indexing.index -and remove_index = Path_indexing.remove_index -and in_index = Path_indexing.in_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 @@ -111,19 +126,41 @@ let get_candidates mode trie term = ;; *) - (* DISCRIMINATION TREES *) let init_index () = - Hashtbl.clear Discrimination_tree.arities; + Hashtbl.clear DT.arities; ;; let empty_table () = - Discrimination_tree.DiscriminationTree.empty + DT.empty ;; -let index = Discrimination_tree.index -and remove_index = Discrimination_tree.remove_index -and in_index = Discrimination_tree.in_index;; +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 + (* 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 @@ -143,10 +180,10 @@ let get_candidates mode tree term = let res = let s = match mode with - | Matching -> Discrimination_tree.retrieve_generalizations tree term - | Unification -> Discrimination_tree.retrieve_unifiables tree term + | Matching -> DT.retrieve_generalizations tree term + | Unification -> DT.retrieve_unifiables tree term in - Discrimination_tree.PosEqSet.elements s + PosEqSet.elements s in (* print_candidates mode term res; *) (* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *) @@ -233,8 +270,8 @@ let rec find_matches metasenv context ugraph lift_amount term termty = 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 @@ -501,6 +538,7 @@ let rec demodulation_equality newmeta env table sign target = 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 @@ -517,7 +555,7 @@ let rec demodulation_equality newmeta env table sign target = 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' = @@ -789,7 +827,7 @@ let superposition_left newmeta (metasenv, context, ugraph) table target = 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'' = diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 5633599d2..43211ccf9 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -917,10 +917,12 @@ type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;; let is_identity ((metasenv, context, ugraph) as env) = function | ((_, _, (ty, left, right, _), menv, _) as equality) -> - (left = right || + (prerr_endline ("left = "^(CicPp.ppterm left)); + prerr_endline ("right = "^(CicPp.ppterm right)); + (left = right || (* (meta_convertibility left right) || *) (fst (CicReduction.are_convertible - ~metasenv:(metasenv @ menv) context left right ugraph))) + ~metasenv:(metasenv @ menv) context left right ugraph)))) ;; diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml index 14d81569a..758437b76 100644 --- a/helm/ocaml/paramodulation/saturate_main.ml +++ b/helm/ocaml/paramodulation/saturate_main.ml @@ -100,6 +100,7 @@ let _ = | "lpo" -> Utils.compare_terms := Utils.lpo | "kbo" -> Utils.compare_terms := Utils.kbo | "nr-kbo" -> Utils.compare_terms := Utils.nonrec_kbo + | "ao" -> Utils.compare_terms := Utils.ao | o -> raise (Arg.Bad ("Unknown term ordering: " ^ o)) and set_fullred b = S.use_fullred := b and set_time_limit v = S.time_limit := float_of_int v diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 9e533d8d6..2e7f1f21a 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -54,7 +54,8 @@ let symbols_ratio = ref (* 0 *) 3;; let symbols_counter = ref 0;; (* non-recursive Knuth-Bendix term ordering by default *) -Utils.compare_terms := Utils.nonrec_kbo;; +(* Utils.compare_terms := Utils.nonrec_kbo;; *) +Utils.compare_terms := Utils.ao;; (* statistics... *) let derived_clauses = ref 0;; @@ -141,7 +142,7 @@ let select env goals passive (active, _) = (* Negatives aren't indexed, no need to remove them... *) (Negative, hd), ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table) - | [], hd::tl -> + | [], (hd:EqualitySet.elt)::tl -> let passive_table = Indexing.remove_index passive_table hd in diff --git a/helm/ocaml/paramodulation/trie.ml b/helm/ocaml/paramodulation/trie.ml deleted file mode 100644 index f60b2d45c..000000000 --- a/helm/ocaml/paramodulation/trie.ml +++ /dev/null @@ -1,153 +0,0 @@ -(* - * Trie: maps over lists. - * Copyright (C) 2000 Jean-Christophe FILLIATRE - * - * This software is free software; you can redistribute it and/or - * modify it under the terms of the GNU Library General Public - * License version 2, as published by the Free Software Foundation. - * - * This software 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 Library General Public License version 2 for more details - * (enclosed in the file LGPL). - *) - -(* $Id$ *) - -(*s A trie is a tree-like structure to implement dictionaries over - keys which have list-like structures. The idea is that each node - branches on an element of the list and stores the value associated - to the path from the root, if any. Therefore, a trie can be - defined as soon as a map over the elements of the list is - given. *) - - -module Make (M : Map.S) = struct - -(*s Then a trie is just a tree-like structure, where a possible - information is stored at the node (['a option]) and where the sons - are given by a map from type [key] to sub-tries, so of type - ['a t M.t]. The empty trie is just the empty map. *) - - type key = M.key list - - type 'a t = Node of 'a option * 'a t M.t - - let empty = Node (None, M.empty) - -(*s To find a mapping in a trie is easy: when all the elements of the - key have been read, we just inspect the optional info at the - current node; otherwise, we descend in the appropriate sub-trie - using [M.find]. *) - - let rec find l t = match (l,t) with - | [], Node (None,_) -> raise Not_found - | [], Node (Some v,_) -> v - | x::r, Node (_,m) -> find r (M.find x m) - - let rec mem l t = match (l,t) with - | [], Node (None,_) -> false - | [], Node (Some _,_) -> true - | x::r, Node (_,m) -> try mem r (M.find x m) with Not_found -> false - -(*s Insertion is more subtle. When the final node is reached, we just - put the information ([Some v]). Otherwise, we have to insert the - binding in the appropriate sub-trie [t']. But it may not exists, - and in that case [t'] is bound to an empty trie. Then we get a new - sub-trie [t''] by a recursive insertion and we modify the - branching, so that it now points to [t''], with [M.add]. *) - - let add l v t = - let rec ins = function - | [], Node (_,m) -> Node (Some v,m) - | x::r, Node (v,m) -> - let t' = try M.find x m with Not_found -> empty in - let t'' = ins (r,t') in - Node (v, M.add x t'' m) - in - ins (l,t) - -(*s When removing a binding, we take care of not leaving bindings to empty - sub-tries in the nodes. Therefore, we test wether the result [t'] of - the recursive call is the empty trie [empty]: if so, we just remove - the branching with [M.remove]; otherwise, we modify it with [M.add]. *) - - let rec remove l t = match (l,t) with - | [], Node (_,m) -> Node (None,m) - | x::r, Node (v,m) -> - try - let t' = remove r (M.find x m) in - Node (v, if t' = empty then M.remove x m else M.add x t' m) - with Not_found -> - t - -(*s The iterators [map], [mapi], [iter] and [fold] are implemented in - a straigthforward way using the corresponding iterators [M.map], - [M.mapi], [M.iter] and [M.fold]. For the last three of them, - we have to remember the path from the root, as an extra argument - [revp]. Since elements are pushed in reverse order in [revp], - we have to reverse it with [List.rev] when the actual binding - has to be passed to function [f]. *) - - let rec map f = function - | Node (None,m) -> Node (None, M.map (map f) m) - | Node (Some v,m) -> Node (Some (f v), M.map (map f) m) - - let mapi f t = - let rec maprec revp = function - | Node (None,m) -> - Node (None, M.mapi (fun x -> maprec (x::revp)) m) - | Node (Some v,m) -> - Node (Some (f (List.rev revp) v), M.mapi (fun x -> maprec (x::revp)) m) - in - maprec [] t - - let iter f t = - let rec traverse revp = function - | Node (None,m) -> - M.iter (fun x -> traverse (x::revp)) m - | Node (Some v,m) -> - f (List.rev revp) v; M.iter (fun x t -> traverse (x::revp) t) m - in - traverse [] t - - let rec fold f t acc = - let rec traverse revp t acc = match t with - | Node (None,m) -> - M.fold (fun x -> traverse (x::revp)) m acc - | Node (Some v,m) -> - f (List.rev revp) v (M.fold (fun x -> traverse (x::revp)) m acc) - in - traverse [] t acc - - let compare cmp a b = - let rec comp a b = match a,b with - | Node (Some _, _), Node (None, _) -> 1 - | Node (None, _), Node (Some _, _) -> -1 - | Node (None, m1), Node (None, m2) -> - M.compare comp m1 m2 - | Node (Some a, m1), Node (Some b, m2) -> - let c = cmp a b in - if c <> 0 then c else M.compare comp m1 m2 - in - comp a b - - let equal eq a b = - let rec comp a b = match a,b with - | Node (None, m1), Node (None, m2) -> - M.equal comp m1 m2 - | Node (Some a, m1), Node (Some b, m2) -> - eq a b && M.equal comp m1 m2 - | _ -> - false - in - comp a b - - (* The base case is rather stupid, but constructable *) - let is_empty = function - | Node (None, m1) -> M.is_empty m1 - | _ -> false - -end diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml index a558001a5..6ee45f235 100644 --- a/helm/ocaml/paramodulation/utils.ml +++ b/helm/ocaml/paramodulation/utils.ml @@ -27,7 +27,6 @@ let debug = true;; let debug_print s = if debug then prerr_endline (Lazy.force s);; - let print_metasenv metasenv = String.concat "\n--------------------------\n" (List.map (fun (i, context, term) -> @@ -375,6 +374,62 @@ let rec kbo t1 t2 = | res -> res ;; +let rec ao t1 t2 = + let get_hd t = + match t with + Cic.MutConstruct(uri,tyno,cno,_) -> Some(uri,tyno,cno) + | Cic.Appl(Cic.MutConstruct(uri,tyno,cno,_)::_) -> + Some(uri,tyno,cno) + | _ -> None in + let aux = aux_ordering ~recursion:false in + let w1 = weight_of_term t1 + and w2 = weight_of_term t2 in + let rec cmp t1 t2 = + match t1, t2 with + | [], [] -> Eq + | _, [] -> Gt + | [], _ -> Lt + | hd1::tl1, hd2::tl2 -> + let o = + ao hd1 hd2 + in + if o = Eq then cmp tl1 tl2 + else o + in + match get_hd t1, get_hd t2 with + Some(_),None -> Lt + | None,Some(_) -> Gt + | _ -> + let comparison = compare_weights ~normalize:true w1 w2 in + match comparison with + | Le -> + let r = aux t1 t2 in + if r = Lt then Lt + else if r = Eq then ( + match t1, t2 with + | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 -> + if cmp tl1 tl2 = Lt then Lt else Incomparable + | _, _ -> Incomparable + ) else Incomparable + | Ge -> + let r = aux t1 t2 in + if r = Gt then Gt + else if r = Eq then ( + match t1, t2 with + | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 -> + if cmp tl1 tl2 = Gt then Gt else Incomparable + | _, _ -> Incomparable + ) else Incomparable + | Eq -> + let r = aux t1 t2 in + if r = Eq then ( + match t1, t2 with + | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 -> + cmp tl1 tl2 + | _, _ -> Incomparable + ) else r + | res -> res +;; let names_of_context context = List.map @@ -492,8 +547,17 @@ let rec lpo t1 t2 = (* settable by the user... *) -let compare_terms = ref nonrec_kbo;; - +(* let compare_terms = ref nonrec_kbo;; *) +let compare_terms = ref ao;; + +let guarded_simpl context t = + let t' = ProofEngineReduction.simpl context t in + let simpl_order = !compare_terms t t' in + if simpl_order = Gt then + (prerr_endline ("reduce: "^(CicPp.ppterm t)^(CicPp.ppterm t')); + t') + else t +;; type equality_sign = Negative | Positive;; diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli index 9704c45ec..d52483ddb 100644 --- a/helm/ocaml/paramodulation/utils.mli +++ b/helm/ocaml/paramodulation/utils.mli @@ -56,9 +56,13 @@ val lpo: Cic.term -> Cic.term -> comparison val kbo: Cic.term -> Cic.term -> comparison +val ao: Cic.term -> Cic.term -> comparison + (** term-ordering function settable by the user *) val compare_terms: (Cic.term -> Cic.term -> comparison) ref +val guarded_simpl: Cic.context -> Cic.term -> Cic.term + type equality_sign = Negative | Positive val string_of_sign: equality_sign -> string -- 2.39.2