From 70b192226bf8165c3c8b12c13c47a3828d685eee Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 25 Jan 2006 08:09:21 +0000 Subject: [PATCH] Code restructuring. --- helm/ocaml/tactics/paramodulation/indexing.ml | 90 +++---- .../ocaml/tactics/paramodulation/indexing.mli | 4 +- .../ocaml/tactics/paramodulation/inference.ml | 15 +- .../tactics/paramodulation/inference.mli | 1 + .../tactics/paramodulation/saturation.ml | 219 ++++++++---------- .../tactics/paramodulation/saturation.mli | 3 + helm/ocaml/tactics/paramodulation/utils.ml | 133 +++++++---- helm/ocaml/tactics/paramodulation/utils.mli | 2 +- 8 files changed, 220 insertions(+), 247 deletions(-) diff --git a/helm/ocaml/tactics/paramodulation/indexing.ml b/helm/ocaml/tactics/paramodulation/indexing.ml index 4eed05790..207fb9433 100644 --- a/helm/ocaml/tactics/paramodulation/indexing.ml +++ b/helm/ocaml/tactics/paramodulation/indexing.ml @@ -130,6 +130,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty = let module M = CicMetaSubst in let module HL = HelmLibraryObjects in let cmp = !Utils.compare_terms in + ignore(CicTypeChecker.type_of_aux' metasenv context term); let check = match termty with C.Implicit None -> false | _ -> true in function | [] -> None @@ -150,10 +151,13 @@ let rec find_matches metasenv context ugraph lift_amount term termty = let t2 = Unix.gettimeofday () in match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1); r - with Inference.MatchingFailure as e -> + with + | Inference.MatchingFailure as e -> let t2 = Unix.gettimeofday () in match_unif_time_no := !match_unif_time_no +. (t2 -. t1); - raise e + raise e + | CicUtil.Meta_not_found _ as exn -> + prerr_endline "siam qua"; raise exn in Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph', (candidate, eq_URI)) @@ -446,7 +450,14 @@ let rec demodulation_equality newmeta env table sign target = 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 w, proof, (eq_ty, left, right, order), metas, args = target in + (* first, we simplify *) + let right = U.guarded_simpl context right in + let left = U.guarded_simpl context left in + let w = Utils.compute_equality_weight eq_ty left right in + let order = !Utils.compare_terms left right in + let target = w, proof, (eq_ty, left, right, order), metas, args in + let metasenv' = metasenv @ metas in let maxmeta = ref newmeta in @@ -520,7 +531,8 @@ let rec demodulation_equality newmeta env table sign target = in let left, right = if is_left then newterm, right else left, newterm in let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in - let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') + (* let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') *) + let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metasenv' @ menv') and newargs = args in let ordering = !Utils.compare_terms left right in @@ -539,7 +551,7 @@ let rec demodulation_equality newmeta env table sign target = match res with | Some t -> let newmeta, newtarget = build_newtarget true t in - if (Inference.is_identity (metasenv', context, ugraph) newtarget) || + if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) || (Inference.meta_convertibility_eq target newtarget) then newmeta, newtarget else @@ -549,7 +561,7 @@ let rec demodulation_equality newmeta env table sign target = match res with | Some t -> let newmeta, newtarget = build_newtarget false t in - if (Inference.is_identity (metasenv', context, ugraph) newtarget) || + if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) || (Inference.meta_convertibility_eq target newtarget) then newmeta, newtarget else @@ -558,13 +570,7 @@ let rec demodulation_equality newmeta env table sign target = newmeta, target in (* newmeta, newtarget *) - (* tentiamo di normalizzare *) - let w, p, (ty, left, right, o), m, a = newtarget in - let left = U.guarded_simpl context left in - let right = U.guarded_simpl context right in - let w' = Utils.compute_equality_weight ty left right in - let o' = !Utils.compare_terms left right in - newmeta, (w', p, (ty, left, right, o'), m, a) + newmeta,newtarget ;; @@ -865,7 +871,10 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = in let new1 = List.map (build_new U.Gt) res1 and new2 = List.map (build_new U.Lt) res2 in +(* let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in +*) + let ok e = not (Inference.is_identity (metasenv', context, ugraph) e) in (!maxmeta, (List.filter ok (new1 @ new2))) ;; @@ -880,8 +889,9 @@ let rec demodulation_goal newmeta env table goal = let metasenv, context, ugraph = env in let maxmeta = ref newmeta in let proof, metas, term = goal in + let term = Utils.guarded_simpl (~debug:true) context term in + let goal = proof, metas, term in let metasenv' = metasenv @ metas in - Printf.eprintf "siam qua\n"; let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) = let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in @@ -939,14 +949,12 @@ let rec demodulation_goal newmeta env table goal = bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof) in let m = Inference.metas_of_term newterm in - let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in + let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv')in !maxmeta, (newproof, newmetasenv, newterm) in - Printf.eprintf "bum0\n"; let res = demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term in - Printf.eprintf "bum\n"; match res with | Some t -> let newmeta, newgoal = build_newgoal t in @@ -954,11 +962,7 @@ let rec demodulation_goal newmeta env table goal = if Inference.meta_convertibility term newg then newmeta, newgoal else - begin - Printf.eprintf "reducing %s to %s \n" - (CicPp.ppterm term) (CicPp.ppterm newg); - demodulation_goal newmeta env table newgoal - end + demodulation_goal newmeta env table newgoal | None -> newmeta, goal ;; @@ -992,7 +996,7 @@ let rec demodulation_theorem newmeta env table theorem = in let m = Inference.metas_of_term newterm in - let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in + let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') in !maxmeta, (newterm, newty, newmetasenv) in let res = @@ -1010,43 +1014,3 @@ let rec demodulation_theorem newmeta env table theorem = newmeta, theorem ;; -let demodulate_tac ~dbd ~pattern (proof,goal) = - let module I = Inference in - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let eq_indexes, equalities, maxm = I.find_equalities context proof in - let lib_eq_uris, library_equalities, maxm = - I.find_library_equalities dbd context (proof, goal) (maxm+2) in - let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - let library_equalities = List.map snd library_equalities in - let goalterm = Cic.Meta (metano,irl) in - let initgoal = Inference.BasicProof goalterm, [], ty in - let equalities = equalities @ library_equalities in - let table = - List.fold_left - (fun tbl eq -> index tbl eq) - empty equalities - in - let newmeta,(newproof,newmetasenv, newty) = demodulation_goal - maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal - in - if newmeta != maxm then - begin - let opengoal = Cic.Meta(maxm,irl) in - let proofterm = - Inference.build_proof_term ~noproof:opengoal newproof in - prerr_endline ("proffterm ="^(CicMetaSubst.ppterm_in_context [] proofterm context)); - let extended_metasenv = (maxm,context,newty)::metasenv in - prerr_endline ("metasenv ="^(CicMetaSubst.ppmetasenv [] extended_metasenv)); - let extended_status = - (curi,extended_metasenv,pbo,pty),goal in - let (status,newgoals) = - ProofEngineTypes.apply_tactic - (PrimitiveTactics.apply_tac ~term:proofterm) - extended_status in - (status,maxm::newgoals) - end - else raise (ProofEngineTypes.Fail (lazy "no progress")) - -let demodulate_tac ~dbd ~pattern = - ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern) diff --git a/helm/ocaml/tactics/paramodulation/indexing.mli b/helm/ocaml/tactics/paramodulation/indexing.mli index 9b051bc40..d2807447c 100644 --- a/helm/ocaml/tactics/paramodulation/indexing.mli +++ b/helm/ocaml/tactics/paramodulation/indexing.mli @@ -83,6 +83,4 @@ val demodulation_theorem : Index.t -> Cic.term * Index.key * Cic.metasenv -> 'a * (Cic.term * Index.key * Cic.metasenv) -val demodulate_tac: - dbd:HMysql.dbd -> - pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic + diff --git a/helm/ocaml/tactics/paramodulation/inference.ml b/helm/ocaml/tactics/paramodulation/inference.ml index f22b49cee..21dadc868 100644 --- a/helm/ocaml/tactics/paramodulation/inference.ml +++ b/helm/ocaml/tactics/paramodulation/inference.ml @@ -500,7 +500,7 @@ let matching metasenv context t1 t2 ugraph = try unification metasenv context t1 t2 ugraph with CicUtil.Meta_not_found _ as exn -> - Printf.eprintf "t1 = %s\nt2 = %s\nmetasenv = %s\n%!" + Printf.eprintf "t1 == %s\nt2 = %s\nmetasenv == %s\n%!" (CicPp.ppterm t1) (CicPp.ppterm t2) (CicMetaSubst.ppmetasenv [] metasenv); raise exn in @@ -910,12 +910,21 @@ let equality_of_term proof term = type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;; +let is_weak_identity (metasenv, context, ugraph) = function + | (_, _, (ty, left, right, _), menv, _) -> + (left = right || + (meta_convertibility left right)) + (* the test below is not a good idea since it stops + demodulation too early *) + (* (fst (CicReduction.are_convertible + ~metasenv:(metasenv @ menv) context left right ugraph)))*) +;; let is_identity (metasenv, context, ugraph) = function | (_, _, (ty, left, right, _), menv, _) -> (left = right || - (* (meta_convertibility left right) || *) - (fst (CicReduction.are_convertible + (* (meta_convertibility left right)) *) + (fst (CicReduction.are_convertible ~metasenv:(metasenv @ menv) context left right ugraph))) ;; diff --git a/helm/ocaml/tactics/paramodulation/inference.mli b/helm/ocaml/tactics/paramodulation/inference.mli index fde29e352..b31d8bacf 100644 --- a/helm/ocaml/tactics/paramodulation/inference.mli +++ b/helm/ocaml/tactics/paramodulation/inference.mli @@ -123,6 +123,7 @@ val meta_convertibility: Cic.term -> Cic.term -> bool (** meta convertibility between two equations *) val meta_convertibility_eq: equality -> equality -> bool +val is_weak_identity: environment -> equality -> bool val is_identity: environment -> equality -> bool val string_of_equality: ?env:environment -> equality -> string diff --git a/helm/ocaml/tactics/paramodulation/saturation.ml b/helm/ocaml/tactics/paramodulation/saturation.ml index 0514ed503..07fbaa41c 100644 --- a/helm/ocaml/tactics/paramodulation/saturation.ml +++ b/helm/ocaml/tactics/paramodulation/saturation.ml @@ -847,6 +847,49 @@ let simplify_theorems env theorems ?passive (active_list, active_table) = ;; +let rec simpl env e others others_simpl = + let active = others @ others_simpl in + let tbl = + List.fold_left + (fun t (_, e) -> Indexing.index t e) + Indexing.empty active + in + let res = forward_simplify env e (active, tbl) in + match others with + | hd::tl -> ( + match res with + | None -> simpl env hd tl others_simpl + | Some e -> simpl env hd tl (e::others_simpl) + ) + | [] -> ( + match res with + | None -> others_simpl + | Some e -> e::others_simpl + ) +;; + +let simplify_equalities env equalities = + debug_print + (lazy + (Printf.sprintf "equalities:\n%s\n" + (String.concat "\n" + (List.map string_of_equality equalities)))); + debug_print (lazy "SIMPLYFYING EQUALITIES..."); + match equalities with + | [] -> [] + | hd::tl -> + let others = List.map (fun e -> (Positive, e)) tl in + let res = + List.rev (List.map snd (simpl env (Positive, hd) others [])) + in + debug_print + (lazy + (Printf.sprintf "equalities AFTER:\n%s\n" + (String.concat "\n" + (List.map string_of_equality res)))); + res +;; + (* applies equality to goal to see if the goal can be closed *) let apply_equality_to_goal env equality goal = let module C = Cic in @@ -1826,48 +1869,7 @@ let main dbd full term metasenv ugraph = in (*try*) let goal = Inference.BasicProof new_meta_goal, [], goal in - let equalities = - let equalities = equalities @ library_equalities in - debug_print - (lazy - (Printf.sprintf "equalities:\n%s\n" - (String.concat "\n" - (List.map string_of_equality equalities)))); - debug_print (lazy "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 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 - (lazy - (Printf.sprintf "equalities AFTER:\n%s\n" - (String.concat "\n" - (List.map string_of_equality res)))); - res - in + let equalities = simplify_equalities env (equalities@library_equalities) in let active = make_active () in let passive = make_passive [] equalities in Printf.printf "\ncurrent goal: %s\n" @@ -2005,48 +2007,7 @@ let saturate let library_equalities = List.map snd library_equalities in let t2 = Unix.gettimeofday () in maxmeta := maxm+2; - let equalities = - let equalities = equalities @ library_equalities in - debug_print - (lazy - (Printf.sprintf "equalities:\n%s\n" - (String.concat "\n" - (List.map string_of_equality equalities)))); - debug_print (lazy "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 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 - (lazy - (Printf.sprintf "equalities AFTER:\n%s\n" - (String.concat "\n" - (List.map string_of_equality res)))); - res - in + let equalities = simplify_equalities env (equalities@library_equalities) in debug_print (lazy (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1))); @@ -2275,48 +2236,7 @@ let main_demod_equalities dbd term metasenv ugraph = let env = (metasenv, context, ugraph) in (*try*) let goal = Inference.BasicProof new_meta_goal, [], goal in - let equalities = - let equalities = equalities @ library_equalities in - debug_print - (lazy - (Printf.sprintf "equalities:\n%s\n" - (String.concat "\n" - (List.map string_of_equality equalities)))); - debug_print (lazy "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 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 - (lazy - (Printf.sprintf "equalities AFTER:\n%s\n" - (String.concat "\n" - (List.map string_of_equality res)))); - res - in + let equalities = simplify_equalities env (equalities@library_equalities) in let active = make_active () in let passive = make_passive [] equalities in Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context); @@ -2363,3 +2283,50 @@ let main_demod_equalities dbd term metasenv ugraph = debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e))) *) ;; + +let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = + let module I = Inference in + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let eq_indexes, equalities, maxm = I.find_equalities context proof in + let lib_eq_uris, library_equalities, maxm = + I.find_library_equalities dbd context (proof, goal) (maxm+2) in + if library_equalities = [] then prerr_endline "VUOTA!!!"; + let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in + let library_equalities = List.map snd library_equalities in + let goalterm = Cic.Meta (metano,irl) in + let initgoal = Inference.BasicProof goalterm, [], ty in + let env = (metasenv, context, CicUniv.empty_ugraph) in + let equalities = simplify_equalities env (equalities@library_equalities) in + let table = + List.fold_left + (fun tbl eq -> Indexing.index tbl eq) + Indexing.empty equalities + in + let newmeta,(newproof,newmetasenv, newty) = Indexing.demodulation_goal + maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal + in + if newmeta != maxm then + begin + let opengoal = Cic.Meta(maxm,irl) in + let proofterm = + Inference.build_proof_term ~noproof:opengoal newproof in + let extended_metasenv = (maxm,context,newty)::metasenv in + let extended_status = + (curi,extended_metasenv,pbo,pty),goal in + let (status,newgoals) = + ProofEngineTypes.apply_tactic + (PrimitiveTactics.apply_tac ~term:proofterm) + extended_status in + (status,maxm::newgoals) + end + else if newty = ty then + raise (ProofEngineTypes.Fail (lazy "no progress")) + else ProofEngineTypes.apply_tactic + (ReductionTactics.simpl_tac ~pattern) + initialstatus +;; + +let demodulate_tac ~dbd ~pattern = + ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern) +;; diff --git a/helm/ocaml/tactics/paramodulation/saturation.mli b/helm/ocaml/tactics/paramodulation/saturation.mli index 259ab5e6c..34159810d 100644 --- a/helm/ocaml/tactics/paramodulation/saturation.mli +++ b/helm/ocaml/tactics/paramodulation/saturation.mli @@ -47,3 +47,6 @@ val main_demod_equalities: HMysql.dbd -> Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit val main: HMysql.dbd -> bool -> Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit +val demodulate_tac: + dbd:HMysql.dbd -> + pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/paramodulation/utils.ml b/helm/ocaml/tactics/paramodulation/utils.ml index b2555cdb4..defd72b16 100644 --- a/helm/ocaml/tactics/paramodulation/utils.ml +++ b/helm/ocaml/tactics/paramodulation/utils.ml @@ -25,7 +25,7 @@ (* $Id$ *) -let debug = true;; +let debug = false;; let debug_print s = if debug then prerr_endline (Lazy.force s);; @@ -109,7 +109,14 @@ let number = [ HelmLibraryObjects.Peano.pred_URI, 12; HelmLibraryObjects.Peano.plus_URI, 15; HelmLibraryObjects.Peano.minus_URI, 18; - HelmLibraryObjects.Peano.mult_URI, 21 + HelmLibraryObjects.Peano.mult_URI, 21; + UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind#xpointer(1/1)",103; + UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)",106; + UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)",109; + UriManager.uri_of_string "cic:/matita/nat/nat/pred.con",112; + UriManager.uri_of_string "cic:/matita/nat/plus/plus.con",115; + UriManager.uri_of_string "cic:/matita/nat/minus/minus.con",118; + UriManager.uri_of_string "cic:/matita/nat/times/times.con",121; ] ;; @@ -117,10 +124,11 @@ let atomic t = match t with Cic.Const _ | Cic.MutInd _ - | Cic.MutConstruct _ -> true + | Cic.MutConstruct _ + | Cic.Rel _ -> true | _ -> false -let sig_order t1 t2 = +let sig_order_const t1 t2 = try let u1 = CicUtil.uri_of_term t1 in let u2 = CicUtil.uri_of_term t2 in @@ -138,52 +146,73 @@ let sig_order t1 t2 = Invalid_argument _ | Not_found -> Incomparable -let rec rpo t1 t2 = +let sig_order t1 t2 = + match t1, t2 with + Cic.Rel n, Cic.Rel m when n < m -> Gt (* inverted order *) + | Cic.Rel n, Cic.Rel m when n = m -> Incomparable + | Cic.Rel n, Cic.Rel m when n > m -> Lt + | Cic.Rel _, _ -> Gt + | _, Cic.Rel _ -> Lt + | _,_ -> sig_order_const t1 t2 + +let rec rpo_lt t1 t2 = let module C = Cic in - match t1,t2 with - C.Meta (_, _), C.Meta (_,_) -> Incomparable - | C.Meta (_,_) as t1,t2 when TermSet.mem t1 (metas_of_term t2) - -> Lt - | t1, (C.Meta (_,_) as t2) when TermSet.mem t2 (metas_of_term t1) - -> Gt - | C.Appl (h1::arg1),C.Appl (h2::arg2) when h1=h2 -> - (match lex arg1 arg2 with - | Lt when (check Gt t2 arg1) -> Lt - | Gt when (check Gt t1 arg2) -> Gt - | _ -> Incomparable ) - | C.Appl (h1::arg1),C.Appl (h2::arg2) -> - (match sig_order h1 h2 with - | Lt when (check Gt t2 arg1) -> Lt - | Gt when (check Gt t1 arg2) -> Gt - | _ -> Incomparable ) - | C.Appl (h1::arg1), t2 when atomic t2 -> - (match sig_order h1 t2 with - | Lt when (check Gt t2 arg1) -> Lt - | Gt -> Gt - | _ -> Incomparable ) - | t1 , C.Appl (h2::arg2) when atomic t1 -> - (match sig_order t1 h2 with - | Lt -> Lt - | Gt when (check Gt t1 arg2) -> Gt - | _ -> Incomparable ) - | C.Appl [] , _ -> assert false - | _ , C.Appl [] -> assert false - | _,_ -> Incomparable - -and lex l1 l2 = + let first_trie = + match t1,t2 with + C.Meta (_, _), C.Meta (_,_) -> false + | C.Meta (_,_) , t2 -> TermSet.mem t1 (metas_of_term t2) + | t1, C.Meta (_,_) -> false + | C.Appl [h1;a1],C.Appl [h2;a2] when h1=h2 -> + rpo_lt a1 a2 + | C.Appl (h1::arg1),C.Appl (h2::arg2) when h1=h2 -> + if lex_lt arg1 arg2 then + check_lt arg1 t2 + else false + | C.Appl (h1::arg1),C.Appl (h2::arg2) -> + (match sig_order h1 h2 with + | Lt -> check_lt arg1 t2 + | _ -> false) + | C.Appl (h1::arg1), t2 when atomic t2 -> + (match sig_order h1 t2 with + | Lt -> check_lt arg1 t2 + | _ -> false) + | t1 , C.Appl (h2::arg2) when atomic t1 -> + (match sig_order t1 h2 with + | Lt -> true + | _ -> false ) + | C.Appl [] , _ -> assert false + | _ , C.Appl [] -> assert false + | t1, t2 when (atomic t1 && atomic t2 && t1<>t2) -> + (match sig_order t1 t2 with + | Lt -> true + | _ -> false) + | _,_ -> false + in + if first_trie then true else + match t2 with + C.Appl (_::args) -> + List.exists (fun a -> t1 = a || rpo_lt t1 a) args + | _ -> false + +and lex_lt l1 l2 = match l1,l2 with - [],[] -> Incomparable + [],[] -> false | [],_ -> assert false | _, [] -> assert false - | a1::l1, a2::l2 when a1 = a2 -> lex l1 l2 - | a1::_, a2::_ -> rpo a1 a2 - -and check o t l = + | a1::l1, a2::l2 when a1 = a2 -> lex_lt l1 l2 + | a1::_, a2::_ -> rpo_lt a1 a2 + +and check_lt l t = List.fold_left - (fun b a -> b && (rpo t a = o)) + (fun b a -> b && (rpo_lt a t)) true l ;; +let rpo t1 t2 = + if rpo_lt t2 t1 then Gt + else if rpo_lt t1 t2 then Lt + else Incomparable + (*********************** fine rpo *****************************) @@ -635,18 +664,20 @@ 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 compare_terms = ref rpo;; *) +let compare_terms = ref rpo;; -let guarded_simpl context t = t -(* +let guarded_simpl ?(debug=false) 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 *) + if t = t' then t else + begin + let simpl_order = !compare_terms t t' in + if debug then + prerr_endline ("comparing "^(CicPp.ppterm t)^(CicPp.ppterm t')); + if simpl_order = Gt then (if debug then prerr_endline "GT";t') + else (if debug then prerr_endline "NO_GT";t) + end ;; type equality_sign = Negative | Positive;; diff --git a/helm/ocaml/tactics/paramodulation/utils.mli b/helm/ocaml/tactics/paramodulation/utils.mli index 2b09e59ae..ce14d480f 100644 --- a/helm/ocaml/tactics/paramodulation/utils.mli +++ b/helm/ocaml/tactics/paramodulation/utils.mli @@ -63,7 +63,7 @@ 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 +val guarded_simpl: ?debug:bool -> Cic.context -> Cic.term -> Cic.term type equality_sign = Negative | Positive -- 2.39.2