From: Alberto Griggio Date: Thu, 19 May 2005 13:12:56 +0000 (+0000) Subject: added lpo term-ordering X-Git-Tag: single_binding~33 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=92d100db14a01e3fb70a7d5151ac1e60d5a782a0;p=helm.git added lpo term-ordering --- diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml index 7f0a8ba55..b0aa00e89 100644 --- a/helm/ocaml/paramodulation/utils.ml +++ b/helm/ocaml/paramodulation/utils.ml @@ -222,7 +222,7 @@ let rec aux_ordering t1 t2 = | t1, t2 when t1 = t2 -> Eq - | C.Rel n, C.Rel m -> if n > m then Lt else Gt (* ALB: changed < to > *) + | C.Rel n, C.Rel m -> if n > m then Lt else Gt | C.Rel _, _ -> Lt | _, C.Rel _ -> Gt @@ -289,21 +289,111 @@ let names_of_context context = ;; -let string_of_equality ?env = - match env with - | None -> ( - function - | _, (ty, left, right), _, _ -> - Printf.sprintf "{%s}: %s = %s" (CicPp.ppterm ty) - (CicPp.ppterm left) (CicPp.ppterm right) - ) - | Some (_, context, _) -> ( - let names = names_of_context context in - function - | _, (ty, left, right), _, _ -> - Printf.sprintf "{%s}: %s = %s" (CicPp.pp ty names) - (CicPp.pp left names) (CicPp.pp right names) +module OrderedTerm = +struct + type t = Cic.term + + let compare = Pervasives.compare +end + +module TermSet = Set.Make(OrderedTerm);; +module TermMap = Map.Make(OrderedTerm);; + +let symbols_of_term term = + let module C = Cic in + let rec aux map = function + | C.Meta _ -> map + | C.Appl l -> + List.fold_left (fun res t -> (aux res t)) map l + | t -> + let map = + try + let c = TermMap.find t map in + TermMap.add t (c+1) map + with Not_found -> + TermMap.add t 1 map + in + map + in + aux TermMap.empty term +;; + + +let metas_of_term term = + let module C = Cic in + let rec aux = function + | C.Meta _ as t -> TermSet.singleton t + | C.Appl l -> + List.fold_left (fun res t -> TermSet.union res (aux t)) TermSet.empty l + | t -> TermSet.empty (* TODO: maybe add other cases? *) + in + aux term +;; + + +let rec lpo t1 t2 = + let module C = Cic in + match t1, t2 with + | t1, t2 when t1 = t2 -> Eq + | t1, (C.Meta _ as m) -> + if TermSet.mem m (metas_of_term t1) then Gt else Incomparable + | (C.Meta _ as m), t2 -> + if TermSet.mem m (metas_of_term t2) then Lt else Incomparable + | C.Appl (hd1::tl1), C.Appl (hd2::tl2) -> ( + let res = + let f o r t = + if r then true else + match lpo t o with + | Gt | Eq -> true + | _ -> false + in + let res1 = List.fold_left (f t2) false tl1 in + if res1 then Gt + else let res2 = List.fold_left (f t1) false tl2 in + if res2 then Lt + else Incomparable + in + if res <> Incomparable then + res + else + let f o r t = + if not r then false else + match lpo o t with + | Gt -> true + | _ -> false + in + match aux_ordering hd1 hd2 with + | Gt -> + let res = List.fold_left (f t1) false tl2 in + if res then Gt + else Incomparable + | Lt -> + let res = List.fold_left (f t2) false tl1 in + if res then Lt + else Incomparable + | Eq -> ( + let lex_res = + try + List.fold_left2 + (fun r t1 t2 -> if r <> Eq then r else lpo t1 t2) + Eq tl1 tl2 + with Invalid_argument _ -> + Incomparable + in + match lex_res with + | Gt -> + if List.fold_left (f t1) false tl2 then Gt + else Incomparable + | Lt -> + if List.fold_left (f t2) false tl1 then Lt + else Incomparable + | _ -> Incomparable + ) + | _ -> Incomparable ) + | t1, t2 -> aux_ordering t1 t2 ;; +(* settable by the user... *) +let compare_terms = ref nonrec_kbo;; diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli index 235085ab1..1adf90e50 100644 --- a/helm/ocaml/paramodulation/utils.mli +++ b/helm/ocaml/paramodulation/utils.mli @@ -19,11 +19,15 @@ val compare_weights: ?normalize:bool -> weight -> weight -> comparison val nonrec_kbo: Cic.term -> Cic.term -> comparison -val string_of_equality: - ?env:Inference.environment -> Inference.equality -> string - val nonrec_kbo_w: (Cic.term * weight) -> (Cic.term * weight) -> comparison val names_of_context: Cic.context -> (Cic.name option) list +module TermMap: Map.S with type key = Cic.term + +val symbols_of_term: Cic.term -> int TermMap.t + +val lpo: Cic.term -> Cic.term -> comparison +(** term-ordering function settable by the user *) +val compare_terms: (Cic.term -> Cic.term -> comparison) ref