From: Alberto Griggio Date: Mon, 22 Aug 2005 14:25:54 +0000 (+0000) Subject: some fixes X-Git-Tag: working_equations_only~19 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d622a1ce338d9db774ddc8b98fa58cdcec7b22e5;p=helm.git some fixes --- diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index 4e222fd6a..cf6a76cdc 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -73,6 +73,31 @@ let apply_subst = (* +(* NO INDEXING *) +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 empty_table () = Path_indexing.PSTrie.empty ;; @@ -100,6 +125,7 @@ let get_candidates mode trie term = *) +(* DISCRIMINATION TREES *) let empty_table () = Discrimination_tree.DiscriminationTree.empty ;; @@ -137,28 +163,28 @@ let match_unif_time_ok = ref 0.;; let match_unif_time_no = ref 0.;; -let rec find_matches metasenv context ugraph lift_amount term = +let rec find_matches metasenv context ugraph lift_amount term termty = let module C = Cic in let module U = Utils in let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in let cmp = !Utils.compare_terms in - let names = Utils.names_of_context context in - let termty, ugraph = - CicTypeChecker.type_of_aux' metasenv context term ugraph - in +(* let names = Utils.names_of_context context in *) +(* let termty, ugraph = *) +(* CicTypeChecker.type_of_aux' metasenv context term ugraph *) +(* in *) function | [] -> None | candidate::tl -> let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in - if not (fst (CicReduction.are_convertible - ~metasenv context termty ty ugraph)) then ( - debug_print ( - Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" - (CicPp.pp termty names) (CicPp.pp ty names)); - find_matches metasenv context ugraph lift_amount term tl - ) else +(* if not (fst (CicReduction.are_convertible *) +(* ~metasenv context termty ty ugraph)) then ( *) +(* (\* debug_print ( *\) *) +(* (\* Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" *\) *) +(* (\* (CicPp.pp termty names) (CicPp.pp ty names)); *\) *) +(* find_matches metasenv context ugraph lift_amount term termty tl *) +(* ) else *) let do_match c other eq_URI = let subst', metasenv', ugraph' = let t1 = Unix.gettimeofday () in @@ -185,7 +211,7 @@ let rec find_matches metasenv context ugraph lift_amount term = try do_match c other eq_URI with Inference.MatchingFailure -> - find_matches metasenv context ugraph lift_amount term tl + find_matches metasenv context ugraph lift_amount term termty tl else let res = try do_match c other eq_URI @@ -200,36 +226,37 @@ let rec find_matches metasenv context ugraph lift_amount term = if order = U.Gt then res else - find_matches metasenv context ugraph lift_amount term tl + find_matches + metasenv context ugraph lift_amount term termty tl | None -> - find_matches metasenv context ugraph lift_amount term tl + find_matches metasenv context ugraph lift_amount term termty tl ;; let rec find_all_matches ?(unif_fun=Inference.unification) - metasenv context ugraph lift_amount term = + metasenv context ugraph lift_amount term termty = let module C = Cic in let module U = Utils in let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in let cmp = !Utils.compare_terms in - let names = Utils.names_of_context context in - let termty, ugraph = - CicTypeChecker.type_of_aux' metasenv context term ugraph - in +(* let names = Utils.names_of_context context in *) +(* let termty, ugraph = *) +(* CicTypeChecker.type_of_aux' metasenv context term ugraph *) +(* in *) function | [] -> [] | candidate::tl -> let pos, (_, _, (ty, left, right, o), metas, args) = candidate in - if not (fst (CicReduction.are_convertible - ~metasenv context termty ty ugraph)) then ( - debug_print ( - Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" - (CicPp.pp termty names) (CicPp.pp ty names)); - find_all_matches ~unif_fun metasenv context ugraph - lift_amount term tl - ) else +(* if not (fst (CicReduction.are_convertible *) +(* ~metasenv context termty ty ugraph)) then ( *) +(* (\* debug_print ( *\) *) +(* (\* Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" *\) *) +(* (\* (CicPp.pp termty names) (CicPp.pp ty names)); *\) *) +(* find_all_matches ~unif_fun metasenv context ugraph *) +(* lift_amount term termty tl *) +(* ) else *) let do_match c other eq_URI = let subst', metasenv', ugraph' = let t1 = Unix.gettimeofday () in @@ -259,13 +286,13 @@ let rec find_all_matches ?(unif_fun=Inference.unification) try let res = do_match c other eq_URI in res::(find_all_matches ~unif_fun metasenv context ugraph - lift_amount term tl) + lift_amount term termty tl) with | Inference.MatchingFailure | CicUnification.UnificationFailure _ | CicUnification.Uncertain _ -> find_all_matches ~unif_fun metasenv context ugraph - lift_amount term tl + lift_amount term termty tl else try let res = do_match c other eq_URI in @@ -277,16 +304,16 @@ let rec find_all_matches ?(unif_fun=Inference.unification) let names = U.names_of_context context in if order <> U.Lt && order <> U.Le then res::(find_all_matches ~unif_fun metasenv context ugraph - lift_amount term tl) + lift_amount term termty tl) else find_all_matches ~unif_fun metasenv context ugraph - lift_amount term tl + lift_amount term termty tl with | Inference.MatchingFailure | CicUnification.UnificationFailure _ | CicUnification.Uncertain _ -> find_all_matches ~unif_fun metasenv context ugraph - lift_amount term tl + lift_amount term termty tl ;; @@ -313,7 +340,7 @@ let subsumption env table target = | _ -> let leftc = get_candidates Matching table left in find_all_matches ~unif_fun:Inference.matching - metasenv context ugraph 0 left leftc + metasenv context ugraph 0 left ty leftc in let ok what (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), _, _)), _)) = try @@ -345,7 +372,7 @@ let subsumption env table target = | _ -> let rightc = get_candidates Matching table right in find_all_matches ~unif_fun:Inference.matching - metasenv context ugraph 0 right rightc + metasenv context ugraph 0 right ty rightc in List.exists (ok left) rightr ;; @@ -360,8 +387,12 @@ let rec demodulate_term metasenv context ugraph table lift_amount term = match term with | C.Meta _ -> None | term -> + let termty, ugraph = + C.Implicit None, ugraph +(* CicTypeChecker.type_of_aux' metasenv context term ugraph *) + in let res = - find_matches metasenv context ugraph lift_amount term candidates + find_matches metasenv context ugraph lift_amount term termty candidates in if res <> None then res @@ -657,8 +688,13 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term = match term with | C.Meta _ -> res, lifted_term | term -> + let termty, ugraph = + C.Implicit None, ugraph +(* CicTypeChecker.type_of_aux' metasenv context term ugraph *) + in let r = - find_all_matches metasenv context ugraph lift_amount term candidates + find_all_matches + metasenv context ugraph lift_amount term termty candidates in r @ res, lifted_term ;; diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 09a023457..eeffd9f1a 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -438,6 +438,8 @@ let rec is_simple_term = function | Cic.Meta (i, l) -> check_irl 1 l | Cic.Rel _ -> true | Cic.Const _ -> true + | Cic.MutInd (_, _, []) -> true + | Cic.MutConstruct (_, _, _, []) -> true | _ -> false ;; @@ -521,9 +523,12 @@ let unification_simple metasenv context t1 t2 ugraph = let unification metasenv context t1 t2 ugraph = (* Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *) let subst, menv, ug = - if not (is_simple_term t1) || not (is_simple_term t2) then + if not (is_simple_term t1) || not (is_simple_term t2) then ( + debug_print ( + Printf.sprintf "NOT SIMPLE TERMS: %s %s" + (CicPp.ppterm t1) (CicPp.ppterm t2)); CicUnification.fo_unif metasenv context t1 t2 ugraph - else + ) else unification_simple metasenv context t1 t2 ugraph in let rec fix_term = function @@ -1182,7 +1187,16 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta = | None -> aux newmeta tl in - aux maxmeta candidates + let found, maxm = aux maxmeta candidates in + (List.fold_left + (fun l e -> + if List.exists (meta_convertibility_eq e) l then ( + debug_print ( + Printf.sprintf "NO!! %s already there!" (string_of_equality e)); + l + ) + else e::l) + [] found), maxm ;; diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml index 6d3c9966c..a2a4e1f07 100644 --- a/helm/ocaml/paramodulation/saturate_main.ml +++ b/helm/ocaml/paramodulation/saturate_main.ml @@ -20,8 +20,12 @@ let _ = let set_ratio v = S.weight_age_ratio := (v+1); S.weight_age_counter := (v+1) and set_sel v = S.symbols_ratio := v; S.symbols_counter := v; and set_conf f = configuration_file := f - and set_lpo () = Utils.compare_terms := Utils.lpo - and set_kbo () = Utils.compare_terms := Utils.nonrec_kbo + and set_ordering o = + match o with + | "lpo" -> Utils.compare_terms := Utils.lpo + | "kbo" -> Utils.compare_terms := Utils.kbo + | "nr-kbo" -> Utils.compare_terms := Utils.nonrec_kbo + | 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 in @@ -29,18 +33,20 @@ let _ = "-f", Arg.Bool set_fullred, "Enable/disable full-reduction strategy (default: enabled)"; - "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 3)"; + "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 4)"; "-s", Arg.Int set_sel, - "symbols-based selection ratio (relative to the weight ratio, default: 2)"; + "symbols-based selection ratio (relative to the weight ratio, default: 0)"; "-c", Arg.String set_conf, "Configuration file (for the db connection)"; - "-lpo", Arg.Unit set_lpo, "Use lpo term ordering"; + "-o", Arg.String set_ordering, + "Term ordering. Possible values are:\n" ^ + "\tkbo: Knuth-Bendix ordering (default)\n" ^ + "\tnr-kbo: Non-recursive variant of kbo\n" ^ + "\tlpo: Lexicographic path ordering"; - "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)"; - - "-l", Arg.Int set_time_limit, "Time limit (in seconds)"; + "-l", Arg.Int set_time_limit, "Time limit in seconds (default: no limit)"; ] (fun a -> ()) "Usage:" in Helm_registry.load_from !configuration_file; diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 5d5273d51..515060aac 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -23,11 +23,14 @@ let maximal_retained_equality = ref None;; (* equality-selection related globals *) let use_fullred = ref true;; -let weight_age_ratio = ref 3;; (* settable by the user from the command line *) +let weight_age_ratio = ref (* 5 *) 3;; (* settable by the user *) let weight_age_counter = ref !weight_age_ratio;; -let symbols_ratio = ref 2;; +let symbols_ratio = ref (* 0 *) 2;; let symbols_counter = ref 0;; +(* non-recursive Knuth-Bendix term ordering by default *) +Utils.compare_terms := Utils.nonrec_kbo;; + (* statistics... *) let derived_clauses = ref 0;; let kept_clauses = ref 0;; @@ -633,18 +636,22 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = ;; -let backward_simplify_active env new_pos new_table active = +let backward_simplify_active env new_pos new_table min_weight active = let active_list, active_table = active in let active_list, newa = List.fold_right (fun (s, equality) (res, newn) -> - match forward_simplify env (s, equality) (new_pos, new_table) with - | None -> res, newn - | Some (s, e) -> - if equality = e then - (s, e)::res, newn - else - res, (s, e)::newn) + let ew, _, _, _, _ = equality in + if ew < min_weight then + (s, equality)::res, newn + else + match forward_simplify env (s, equality) (new_pos, new_table) with + | None -> res, newn + | Some (s, e) -> + if equality = e then + (s, e)::res, newn + else + res, (s, e)::newn) active_list ([], []) in let find eq1 where = @@ -677,17 +684,22 @@ let backward_simplify_active env new_pos new_table active = ;; -let backward_simplify_passive env new_pos new_table passive = +let backward_simplify_passive env new_pos new_table min_weight passive = let (nl, ns), (pl, ps), passive_table = passive in let f sign equality (resl, ress, newn) = - match forward_simplify env (sign, equality) (new_pos, new_table) with - | None -> resl, EqualitySet.remove equality ress, newn - | Some (s, e) -> - if equality = e then - equality::resl, ress, newn - else - let ress = EqualitySet.remove equality ress in - resl, ress, e::newn + let ew, _, _, _, _ = equality in + if ew < min_weight then +(* let _ = debug_print (Printf.sprintf "OK: %d %d" ew min_weight) in *) + equality::resl, ress, newn + else + match forward_simplify env (sign, equality) (new_pos, new_table) with + | None -> resl, EqualitySet.remove equality ress, newn + | Some (s, e) -> + if equality = e then + equality::resl, ress, newn + else + let ress = EqualitySet.remove equality ress in + resl, ress, e::newn in let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, []) and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in @@ -702,18 +714,21 @@ let backward_simplify_passive env new_pos new_table passive = let backward_simplify env new' ?passive active = - let new_pos, new_table = + let new_pos, new_table, min_weight = List.fold_left - (fun (l, t) e -> (Positive, e)::l, Indexing.index t e) - ([], Indexing.empty_table ()) (snd new') - in - let active, newa = backward_simplify_active env new_pos new_table active in + (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') + in + let active, newa = + backward_simplify_active env new_pos new_table min_weight active in match passive with | None -> active, (make_passive [] []), newa, None | Some passive -> let passive, newp = - backward_simplify_passive env new_pos new_table passive in + backward_simplify_passive env new_pos new_table min_weight passive in active, passive, newa, newp ;; @@ -1036,10 +1051,48 @@ let main dbd term metasenv ugraph = in () else - let active = make_active () in - let passive = - make_passive [term_equality] (equalities @ library_equalities) + let equalities = + let equalities = equalities @ library_equalities in + debug_print ( + Printf.sprintf "equalities:\n%s\n" + (String.concat "\n" + (List.map string_of_equality equalities))); + debug_print "SIMPLYFYING EQUALITIES..."; + let rec simpl e others others_simpl = + let active = others @ others_simpl in + let tbl = + List.fold_left + (fun t (_, e) -> Indexing.index t e) + (Indexing.empty_table ()) active + in + let res = forward_simplify env e (active, tbl) in + match others with + | hd::tl -> ( + match res with + | None -> simpl hd tl others_simpl + | Some e -> simpl hd tl (e::others_simpl) + ) + | [] -> ( + match res with + | None -> others_simpl + | Some e -> e::others_simpl + ) + in + match equalities with + | [] -> [] + | hd::tl -> + let others = List.map (fun e -> (Positive, e)) tl in + let res = + List.rev (List.map snd (simpl (Positive, hd) others [])) + in + debug_print ( + Printf.sprintf "equalities AFTER:\n%s\n" + (String.concat "\n" + (List.map string_of_equality res))); + res in + let active = make_active () in + let passive = make_passive [term_equality] equalities in Printf.printf "\ncurrent goal: %s\n" (string_of_equality ~env term_equality); Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context); @@ -1048,7 +1101,7 @@ let main dbd term metasenv ugraph = (String.concat "\n" (List.map (string_of_equality ~env) - equalities)); + (equalities @ library_equalities))); print_endline "--------------------------------------------------"; let start = Unix.gettimeofday () in print_endline "GO!"; @@ -1091,6 +1144,7 @@ let main dbd term metasenv ugraph = with e -> Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e); Printf.printf "MAXMETA USED: %d\n" !maxmeta; + print_endline (string_of_float (finish -. start)); in () @@ -1140,7 +1194,7 @@ let saturate dbd (proof, goal) = let env = (metasenv, context, ugraph) in (* try *) let term_equality = equality_of_term new_meta_goal goal in - let res = + let res, time = if is_identity env term_equality then let w, _, (eq_ty, left, right, o), m, a = term_equality in let proof = @@ -1148,21 +1202,60 @@ let saturate dbd (proof, goal) = (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); eq_ty; left] in - ParamodulationSuccess - (Some (0, Inference.BasicProof proof, - (eq_ty, left, right, o), m, a), env) + (ParamodulationSuccess + (Some (0, Inference.BasicProof proof, + (eq_ty, left, right, o), m, a), env), 0.) else let library_equalities, maxm = find_library_equalities ~dbd context (proof, goal') (maxm+2) in maxmeta := maxm+2; - + let equalities = + let equalities = equalities @ library_equalities in + debug_print ( + Printf.sprintf "equalities:\n%s\n" + (String.concat "\n" + (List.map string_of_equality equalities))); + debug_print "SIMPLYFYING EQUALITIES..."; + let rec simpl e others others_simpl = + let active = others @ others_simpl in + let tbl = + List.fold_left + (fun t (_, e) -> Indexing.index t e) + (Indexing.empty_table ()) active + in + let res = forward_simplify env e (active, tbl) in + match others with + | hd::tl -> ( + match res with + | None -> simpl hd tl others_simpl + | Some e -> simpl hd tl (e::others_simpl) + ) + | [] -> ( + match res with + | None -> others_simpl + | Some e -> e::others_simpl + ) + in + match equalities with + | [] -> [] + | hd::tl -> + let others = List.map (fun e -> (Positive, e)) tl in + let res = + List.rev (List.map snd (simpl (Positive, hd) others [])) + in + debug_print ( + Printf.sprintf "equalities AFTER:\n%s\n" + (String.concat "\n" + (List.map string_of_equality res))); + res + in let active = make_active () in - let passive = - make_passive [term_equality] (equalities @ library_equalities) - in + let passive = make_passive [term_equality] equalities in + let start = Unix.gettimeofday () in let res = given_clause_fullred env passive active in - res + let finish = Unix.gettimeofday () in + (res, finish -. start) in match res with | ParamodulationSuccess (Some goal, env) -> @@ -1223,6 +1316,7 @@ let saturate dbd (proof, goal) = raise (ProofEngineTypes.Fail "Found a proof, but it doesn't typecheck") in + debug_print (Printf.sprintf "\nTIME NEEDED: %.9f" time); newstatus | _ -> raise (ProofEngineTypes.Fail "NO proof found") diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml index 1968f017c..f2ece4baa 100644 --- a/helm/ocaml/paramodulation/utils.ml +++ b/helm/ocaml/paramodulation/utils.ml @@ -88,16 +88,28 @@ let weight_of_term ?(consider_metas=true) term = ;; +module OrderedInt = struct + type t = int + + let compare = Pervasives.compare +end + +module IntSet = Set.Make(OrderedInt) + let compute_equality_weight ty left right = +(* let metasw = ref IntSet.empty in *) let metasw = ref 0 in let weight_of t = let w, m = (weight_of_term ~consider_metas:true(* false *) t) in (* let mw = List.fold_left (fun mw (_, c) -> mw + 2 * c) 0 m in *) (* metasw := !metasw + mw; *) metasw := !metasw + (2 * (List.length m)); +(* metasw := List.fold_left (fun s (i, _) -> IntSet.add i s) !metasw m; *) w in - (weight_of ty) + (weight_of left) + (weight_of right) + !metasw + (weight_of ty) + (weight_of left) + (weight_of right) + + !metasw +(* (4 * IntSet.cardinal !metasw) *) ;; @@ -227,7 +239,7 @@ let compare_weights ?(normalize=false) ;; -let rec aux_ordering t1 t2 = +let rec aux_ordering ?(recursion=true) t1 t2 = let module C = Cic in let compare_uris u1 u2 = let res = @@ -259,7 +271,7 @@ let rec aux_ordering t1 t2 = | C.MutConstruct _, _ -> Lt | _, C.MutConstruct _ -> Gt - | C.Appl l1, C.Appl l2 -> + | C.Appl l1, C.Appl l2 when recursion -> let rec cmp t1 t2 = match t1, t2 with | [], [] -> Eq @@ -271,10 +283,13 @@ let rec aux_ordering t1 t2 = else o in cmp l1 l2 + | C.Appl (h1::t1), C.Appl (h2::t2) when not recursion -> + aux_ordering h1 h2 | t1, t2 -> - Printf.printf "These two terms are not comparable:\n%s\n%s\n\n" - (CicPp.ppterm t1) (CicPp.ppterm t2); + debug_print ( + Printf.sprintf "These two terms are not comparable:\n%s\n%s\n\n" + (CicPp.ppterm t1) (CicPp.ppterm t2)); Incomparable ;; @@ -300,6 +315,68 @@ let nonrec_kbo t1 t2 = ;; +let rec kbo t1 t2 = +(* debug_print ( *) +(* Printf.sprintf "kbo %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2)); *) +(* if t1 = t2 then *) +(* Eq *) +(* else *) + 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 = +(* debug_print ( *) +(* Printf.sprintf "recursion kbo on %s %s" *) +(* (CicPp.ppterm hd1) (CicPp.ppterm hd2)); *) + kbo hd1 hd2 + in + if o = Eq then cmp tl1 tl2 + else o + in + let comparison = compare_weights ~normalize:true w1 w2 in +(* debug_print ( *) +(* Printf.sprintf "Weights are: %s %s: %s" *) +(* (string_of_weight w1) (string_of_weight w2) *) +(* (string_of_comparison comparison)); *) + match comparison with + | Le -> + let r = aux t1 t2 in +(* debug_print ("HERE! " ^ (string_of_comparison r)); *) + 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 -> +(* if cmp tl1 tl2 = Gt then Gt else Incomparable *) + cmp tl1 tl2 + | _, _ -> Incomparable + ) else r + | res -> res +;; + + let names_of_context context = List.map (function diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli index 0187f94a7..34e261d17 100644 --- a/helm/ocaml/paramodulation/utils.mli +++ b/helm/ocaml/paramodulation/utils.mli @@ -29,6 +29,8 @@ val symbols_of_term: Cic.term -> int TermMap.t val lpo: Cic.term -> Cic.term -> comparison +val kbo: Cic.term -> Cic.term -> comparison + (** term-ordering function settable by the user *) val compare_terms: (Cic.term -> Cic.term -> comparison) ref