From: Andrea Asperti Date: Mon, 16 Jan 2006 09:38:52 +0000 (+0000) Subject: Added recursive path ordering and demodulation tactic. X-Git-Tag: make_still_working~7833 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5886d890afe8fbb3b6bae0fffdfa657b894cae3f;p=helm.git Added recursive path ordering and demodulation tactic. --- diff --git a/helm/ocaml/tactics/paramodulation/indexing.ml b/helm/ocaml/tactics/paramodulation/indexing.ml index b60435e04..8ece33e35 100644 --- a/helm/ocaml/tactics/paramodulation/indexing.ml +++ b/helm/ocaml/tactics/paramodulation/indexing.ml @@ -179,7 +179,6 @@ let rec find_matches metasenv context ugraph lift_amount term termty = let other' = U.guarded_simpl context (apply_subst s other) in *) let other' = apply_subst s other in let order = cmp c' other' in - let names = U.names_of_context context in if order = U.Gt then res else @@ -250,7 +249,6 @@ let rec find_all_matches ?(unif_fun=Inference.unification) let c' = apply_subst s c and other' = apply_subst s other in let order = cmp c' other' in - 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 termty tl) @@ -346,6 +344,8 @@ let subsumption env table target = let rec demodulation_aux ?(typecheck=false) metasenv context ugraph table lift_amount term = + (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *) + let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -832,13 +832,6 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = let newgoal, newproof = (* qua *) let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in - let t' = - let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in - incr sup_r_counter; - let l, r = - if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in - (name, ty, S.lift 1 eq_ty, l, r) - in let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in incr sup_r_counter; let bo'' = @@ -859,8 +852,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = and newargs = args @ args' in let eq' = let w = Utils.compute_equality_weight eq_ty left right in - (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) - and env = (metasenv, context, ugraph) in + (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) in let newm, eq' = Inference.fix_metas !maxmeta eq' in newm, eq' in @@ -889,6 +881,7 @@ let rec demodulation_goal newmeta env table goal = let maxmeta = ref newmeta in let proof, metas, term = goal 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 @@ -938,11 +931,7 @@ let rec demodulation_goal newmeta env table goal = | Inference.ProofGoalBlock (_, parent_proof) -> (* debug_print (lazy "replacing another ProofGoalBlock"); *) Inference.ProofGoalBlock (pb, parent_proof) - | (Inference.SubProof (term, meta_index, p) as subproof) -> -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "replacing %s" *) -(* (Inference.string_of_proof subproof))); *) + | Inference.SubProof (term, meta_index, p) -> Inference.SubProof (term, meta_index, repl p) | _ -> assert false in repl proof @@ -953,9 +942,11 @@ let rec demodulation_goal newmeta env table goal = let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas 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 @@ -963,7 +954,11 @@ let rec demodulation_goal newmeta env table goal = if Inference.meta_convertibility term newg then newmeta, newgoal else - demodulation_goal newmeta env table newgoal + begin + Printf.eprintf "reducing %s to %s \n" + (CicPp.ppterm term) (CicPp.ppterm newg); + demodulation_goal newmeta env table newgoal + end | None -> newmeta, goal ;; @@ -977,10 +972,9 @@ let rec demodulation_theorem newmeta env table theorem = let module HL = HelmLibraryObjects in let metasenv, context, ugraph = env in let maxmeta = ref newmeta in - let proof, metas, term = theorem in let term, termty, metas = theorem in let metasenv' = metasenv @ metas in - + let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) = 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 @@ -995,7 +989,8 @@ let rec demodulation_theorem newmeta env table theorem = Inference.BasicProof term) in (Inference.build_proof_term newproof, bo) - in + in + let m = Inference.metas_of_term newterm in let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in !maxmeta, (newterm, newty, newmetasenv) @@ -1018,27 +1013,40 @@ let rec demodulation_theorem newmeta env table theorem = 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) as conjecture = CicUtil.lookup_meta goal metasenv 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, [], goalterm 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 _,(newproof, newty, newmetasenv) = demodulation_goal + let newmeta,(newproof,newmetasenv, newty) = demodulation_goal maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal in - let proofterm = Inference.build_proof_term newproof in - ProofEngineTypes.apply_tactic - (PrimitiveTactics.apply_tac ~term:proofterm) - initialstatus + 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/inference.ml b/helm/ocaml/tactics/paramodulation/inference.ml index 6c2a9b9dc..f22b49cee 100644 --- a/helm/ocaml/tactics/paramodulation/inference.ml +++ b/helm/ocaml/tactics/paramodulation/inference.ml @@ -39,7 +39,7 @@ type equality = Cic.term list (* arguments *) and proof = - | NoProof + | NoProof (* term is the goal missing a proof *) | BasicProof of Cic.term | ProofBlock of Cic.substitution * UriManager.uri * @@ -70,7 +70,7 @@ let string_of_equality ?env = let rec string_of_proof = function - | NoProof -> "NoProof" + | NoProof -> "NoProof " | BasicProof t -> "BasicProof " ^ (CicPp.ppterm t) | SubProof (t, i, p) -> Printf.sprintf "SubProof(%s, %s, %s)" @@ -101,12 +101,12 @@ let build_ens_for_sym_eq sym_eq_URI termlist = ;; -let build_proof_term proof = +let build_proof_term ?(noproof=Cic.Implicit None) proof = let rec do_build_proof proof = match proof with | NoProof -> Printf.fprintf stderr "WARNING: no proof!\n"; - Cic.Implicit None + noproof | BasicProof term -> term | ProofGoalBlock (proofbit, proof) -> print_endline "found ProofGoalBlock, going up..."; @@ -191,11 +191,6 @@ exception NotMetaConvertible;; let meta_convertibility_aux table t1 t2 = let module C = Cic in - let print_table t = - String.concat ", " - (List.map - (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t) - in let rec aux ((table_l, table_r) as table) t1 t2 = match t1, t2 with | C.Meta (m1, tl1), C.Meta (m2, tl2) -> @@ -309,16 +304,11 @@ let meta_convertibility_eq eq1 eq2 = let meta_convertibility t1 t2 = - let f t = - String.concat ", " - (List.map - (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t) - in if t1 = t2 then true else try - let l, r = meta_convertibility_aux ([], []) t1 t2 in + ignore(meta_convertibility_aux ([], []) t1 t2); true with NotMetaConvertible -> false @@ -648,7 +638,6 @@ let find_library_equalities dbd context status maxmeta = let candidates = List.fold_left (fun l uri -> - let suri = UriManager.string_of_uri uri in if UriManager.UriSet.mem uri blacklist then l else @@ -806,7 +795,7 @@ let find_context_hypotheses env equalities_indexes = ;; -let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = +let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) = let table = Hashtbl.create (List.length args) in let newargs, newmeta = List.fold_right @@ -866,7 +855,7 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = (Hashtbl.copy table) in let rec fix_proof = function - | NoProof -> NoProof + | NoProof -> NoProof | BasicProof term -> BasicProof (repl term) | ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) -> let subst' = @@ -922,8 +911,8 @@ let equality_of_term proof term = type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;; -let is_identity ((metasenv, context, ugraph) as env) = function - | ((_, _, (ty, left, right, _), menv, _) as equality) -> +let is_identity (metasenv, context, ugraph) = function + | (_, _, (ty, left, right, _), menv, _) -> (left = right || (* (meta_convertibility left right) || *) (fst (CicReduction.are_convertible diff --git a/helm/ocaml/tactics/paramodulation/inference.mli b/helm/ocaml/tactics/paramodulation/inference.mli index 30927dc72..fde29e352 100644 --- a/helm/ocaml/tactics/paramodulation/inference.mli +++ b/helm/ocaml/tactics/paramodulation/inference.mli @@ -34,7 +34,7 @@ type equality = Cic.term list (* arguments *) and proof = - | NoProof + | NoProof (* no proof *) | BasicProof of Cic.term (* already a proof of a goal *) | ProofBlock of (* proof of a rewrite step *) Cic.substitution * UriManager.uri * (* eq_ind or eq_ind_r *) @@ -48,7 +48,7 @@ and proof = type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph (** builds the Cic.term encoded by proof *) -val build_proof_term: proof -> Cic.term +val build_proof_term: ?noproof:Cic.term -> proof -> Cic.term val string_of_proof: proof -> string diff --git a/helm/ocaml/tactics/paramodulation/saturation.ml b/helm/ocaml/tactics/paramodulation/saturation.ml index d73428c8a..6946df1a2 100644 --- a/helm/ocaml/tactics/paramodulation/saturation.ml +++ b/helm/ocaml/tactics/paramodulation/saturation.ml @@ -56,7 +56,7 @@ let symbols_ratio = ref (* 0 *) 3;; let symbols_counter = ref 0;; (* non-recursive Knuth-Bendix term ordering by default *) -Utils.compare_terms := Utils.rpo;; +(* Utils.compare_terms := Utils.rpo;; *) (* Utils.compare_terms := Utils.nonrec_kbo;; *) (* Utils.compare_terms := Utils.ao;; *) @@ -81,8 +81,7 @@ type goal = proof * Cic.metasenv * Cic.term;; type theorem = Cic.term * Cic.term * Cic.metasenv;; - -let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) = +let symbols_of_equality (_, _, (_, left, right, _), _, _) = let m1 = symbols_of_term left in let m = TermMap.fold @@ -97,7 +96,6 @@ let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) = m ;; - module OrderedEquality = struct type t = Inference.equality @@ -564,7 +562,6 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = and pp = List.map (fun e -> (Positive, e)) pp in pn @ pp, Some pt in - let all = active_list @ pl in let t2 = Unix.gettimeofday () in fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1); @@ -771,7 +768,6 @@ let simplify_goal env goal ?passive (active_list, active_table) = and pp = List.map (fun e -> (Positive, e)) pp in pn @ pp, Some pt in - let all = if pl = [] then active_list else active_list @ pl in let demodulate table goal = let newmeta, newgoal = @@ -826,7 +822,6 @@ let simplify_theorems env theorems ?passive (active_list, active_table) = and pp = List.map (fun e -> (Positive, e)) pp in pn @ pp, Some pt in - let all = if pl = [] then active_list else active_list @ pl in let a_theorems, p_theorems = theorems in let demodulate table theorem = let newmeta, newthm = @@ -1075,7 +1070,7 @@ let rec apply_to_goal_conj env theorems ?passive active (depth, goals) = let aux (goal, r) tl = let propagate_subst subst (proof, metas, term) = let rec repl = function - | NoProof -> NoProof + | NoProof -> NoProof | BasicProof t -> BasicProof (CicMetaSubst.apply_subst subst t) | ProofGoalBlock (p, pb) -> @@ -1507,7 +1502,6 @@ and given_clause_aux dbd env goals theorems passive active = al @ [(sign, current)], Indexing.index tbl current in let passive = add_to_passive passive new' in - let (_, ns), (_, ps), _ = passive in given_clause dbd env goals theorems passive active | true, goal -> let proof = @@ -2160,13 +2154,6 @@ let saturate let init () = ();; -(* UGLY SIDE EFFECT... -if connect_to_auto then ( - AutoTactic.paramodulation_tactic := saturate; - AutoTactic.term_is_equality := Inference.term_is_equality; -);; -*) - let retrieve_and_print dbd term metasenv ugraph = let module C = Cic in let module T = CicTypeChecker in @@ -2191,72 +2178,69 @@ let retrieve_and_print dbd term metasenv ugraph = in let ugraph = CicUniv.empty_ugraph in let env = (metasenv, context, ugraph) in - let goal = Inference.BasicProof new_meta_goal, [], goal in let t1 = Unix.gettimeofday () in let lib_eq_uris, library_equalities, maxm = - find_library_equalities dbd context (proof, goal') (maxm+2) - in + find_library_equalities dbd context (proof, goal') (maxm+2) in let t2 = Unix.gettimeofday () in - maxmeta := maxm+2; - let equalities = - let equalities = (* equalities @ *) library_equalities in - debug_print - (lazy - (Printf.sprintf "\n\nequalities:\n%s\n" - (String.concat "\n" - (List.map - (fun (u, e) -> -(* Printf.sprintf "%s: %s" *) - (UriManager.string_of_uri u) -(* (string_of_equality e) *) - ) - equalities)))); - debug_print (lazy "SIMPLYFYING EQUALITIES..."); - let rec simpl e others others_simpl = - let (u, e) = e in - let active = List.map (fun (u, e) -> (Positive, e)) - (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 (Positive, e) (active, tbl) in - match others with - | hd::tl -> ( - match res with - | None -> simpl hd tl others_simpl - | Some e -> simpl hd tl ((u, (snd e))::others_simpl) - ) - | [] -> ( - match res with - | None -> others_simpl - | Some e -> (u, (snd e))::others_simpl - ) - in - match equalities with - | [] -> [] - | hd::tl -> - let others = tl in (* List.map (fun e -> (Positive, e)) tl in *) - let res = - List.rev (simpl (*(Positive,*) hd others []) - in - debug_print - (lazy - (Printf.sprintf "\nequalities AFTER:\n%s\n" - (String.concat "\n" - (List.map - (fun (u, e) -> - Printf.sprintf "%s: %s" - (UriManager.string_of_uri u) - (string_of_equality e) - ) - res)))); - res + maxmeta := maxm+2; + let equalities = (* equalities @ *) library_equalities in + debug_print + (lazy + (Printf.sprintf "\n\nequalities:\n%s\n" + (String.concat "\n" + (List.map + (fun (u, e) -> +(* Printf.sprintf "%s: %s" *) + (UriManager.string_of_uri u) +(* (string_of_equality e) *) + ) + equalities)))); + debug_print (lazy "SIMPLYFYING EQUALITIES..."); + let rec simpl e others others_simpl = + let (u, e) = e in + let active = List.map (fun (u, e) -> (Positive, e)) + (others @ others_simpl) in + let tbl = + List.fold_left + (fun t (_, e) -> Indexing.index t e) + Indexing.empty active in - debug_print - (lazy - (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1))) + let res = forward_simplify env (Positive, e) (active, tbl) in + match others with + | hd::tl -> ( + match res with + | None -> simpl hd tl others_simpl + | Some e -> simpl hd tl ((u, (snd e))::others_simpl) + ) + | [] -> ( + match res with + | None -> others_simpl + | Some e -> (u, (snd e))::others_simpl + ) + in + let equalities = + match equalities with + | [] -> [] + | hd::tl -> + let others = tl in (* List.map (fun e -> (Positive, e)) tl in *) + let res = + List.rev (simpl (*(Positive,*) hd others []) + in + debug_print + (lazy + (Printf.sprintf "\nequalities AFTER:\n%s\n" + (String.concat "\n" + (List.map + (fun (u, e) -> + Printf.sprintf "%s: %s" + (UriManager.string_of_uri u) + (string_of_equality e) + ) + res)))); + res in + debug_print + (lazy + (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1))) ;; @@ -2289,7 +2273,6 @@ let main_demod_equalities dbd term metasenv ugraph = ty in let env = (metasenv, context, ugraph) in - let t1 = Unix.gettimeofday () in (*try*) let goal = Inference.BasicProof new_meta_goal, [], goal in let equalities = @@ -2343,23 +2326,19 @@ let main_demod_equalities dbd term metasenv ugraph = (List.map (string_of_equality ~env) equalities)); print_endline "--------------------------------------------------"; - let start = Unix.gettimeofday () in print_endline "GO!"; start_time := Unix.gettimeofday (); if !time_limit < 1. then time_limit := 60.; let ra, rp = saturate_equations env goal (fun e -> true) passive active in - let finish = Unix.gettimeofday () in let initial = List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities in - let addfun s e = EqualitySet.add e s - (* + let addfun s e = if not (EqualitySet.mem e initial) then EqualitySet.add e s else s - *) in let passive = diff --git a/helm/ocaml/tactics/paramodulation/utils.ml b/helm/ocaml/tactics/paramodulation/utils.ml index 3cafedd54..b2555cdb4 100644 --- a/helm/ocaml/tactics/paramodulation/utils.ml +++ b/helm/ocaml/tactics/paramodulation/utils.ml @@ -131,7 +131,7 @@ let sig_order t1 t2 = else begin prerr_endline ("t1 = "^(CicPp.ppterm t1)); - prerr_endline ("t2 = "^(CicPp.ppterm t2)); flush; + prerr_endline ("t2 = "^(CicPp.ppterm t2)); assert false end with @@ -635,9 +635,9 @@ 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 (*