From: Alberto Griggio Date: Mon, 11 Jul 2005 18:24:43 +0000 (+0000) Subject: now proofs have the correct type :-) X-Git-Tag: pre_notation~34 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=22d39afadb3027477e4a42c315ec10518cbf47ed;p=helm.git now proofs have the correct type :-) --- diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index bd9091e4c..f15a0cee6 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -375,12 +375,22 @@ let rec demodulate_term metasenv context ugraph table lift_amount term = ;; +let build_ens_for_sym_eq ty x y = + [(UriManager.uri_of_string + "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var", ty); + (UriManager.uri_of_string + "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var", x); + (UriManager.uri_of_string + "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var", y)] +;; + + let build_newtarget_time = ref 0.;; let demod_counter = ref 1;; -let rec demodulation newmeta env table target = +let rec demodulation newmeta env table sign target = let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -388,6 +398,9 @@ let rec demodulation newmeta env table target = let metasenv, context, ugraph = env in let _, proof, (eq_ty, left, right, order), metas, args = target in let metasenv' = metasenv @ metas in + + let maxmeta = ref newmeta in + let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) = let time1 = Unix.gettimeofday () in @@ -398,29 +411,65 @@ let rec demodulation newmeta env table target = let t' = let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in incr demod_counter; - let l, r = if is_left then bo, right else left, bo in - (name, ty, eq_ty, l, r) + let l, r = + if is_left then t, S.lift 1 right else S.lift 1 left, t in + (name, ty, S.lift 1 eq_ty, l, r) in -(* let bo'' = *) -(* C.Appl ([C.MutInd (HL.Logic.eq_URI, 0, []); *) -(* S.lift 1 eq_ty] @ *) -(* if is_left then [S.lift 1 bo; S.lift 1 right] *) -(* else [S.lift 1 left; S.lift 1 bo]) *) -(* in *) -(* let t' = *) -(* let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in *) -(* incr demod_counter; *) -(* C.Lambda (name, ty, bo'') *) -(* in *) - bo, - Inference.ProofBlock (subst, eq_URI, t', eq_found, target) -(* (\* M. *\)apply_subst subst (C.Appl [C.Const (eq_URI, []); ty; what; t'; *) -(* proof; other; proof']) *) + if sign = Utils.Positive then + (bo, + Inference.ProofBlock (subst, eq_URI, t', eq_found, proof)) + else + let metaproof = + incr maxmeta; + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + Printf.printf "\nADDING META: %d\n" !maxmeta; + print_newline (); + C.Meta (!maxmeta, irl) + in + let target' = + let eq_found = + let proof' = + let ens = + if pos = Utils.Left then + build_ens_for_sym_eq ty what other + else + build_ens_for_sym_eq ty other what + in + Inference.ProofSymBlock (ens, proof') + in + let what, other = + if pos = Utils.Left then what, other else other, what + in + pos, (0, proof', (ty, other, what, Utils.Incomparable), + menv', args') + in + let target_proof = + let pb = + Inference.ProofBlock (subst, eq_URI, t', eq_found, + Inference.BasicProof metaproof) + in + match proof with + | Inference.BasicProof _ -> + print_endline "replacing a BasicProof"; + pb + | Inference.ProofGoalBlock (_, parent_eq) -> + print_endline "replacing another ProofGoalBlock"; + Inference.ProofGoalBlock (pb, parent_eq) + | _ -> assert false + in + (0, target_proof, (eq_ty, left, right, order), metas, args) + in + let refl = + C.Appl [C.MutConstruct (* reflexivity *) + (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); + eq_ty; if is_left then right else left] + in + (bo, + Inference.ProofGoalBlock (Inference.BasicProof refl, 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 m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas and newargs = List.filter @@ -436,12 +485,13 @@ let rec demodulation newmeta env table target = let w = Utils.compute_equality_weight eq_ty left right in (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs) in - newmeta, res +(* if sign = Utils.Positive then ( *) +(* let newm, res = Inference.fix_metas !maxmeta res in *) +(* maxmeta := newm; *) +(* !maxmeta, res *) +(* ) else *) + !maxmeta(* newmeta *), res in -(* let build_newtarget = *) -(* let profile = CicUtil.profile "Indexing.demodulation.build_newtarget" in *) -(* (fun a b -> profile (build_newtarget a) b) *) -(* in *) let res = demodulate_term metasenv' context ugraph table 0 left in (* let build_identity (w, p, (t, l, r, o), m, a) = *) (* match o with *) @@ -458,7 +508,7 @@ let rec demodulation newmeta env table target = (* if subsumption env table newtarget then *) (* newmeta, build_identity newtarget *) (* else *) - demodulation newmeta env table newtarget + demodulation newmeta env table sign newtarget | None -> let res = demodulate_term metasenv' context ugraph table 0 right in match res with @@ -471,7 +521,7 @@ let rec demodulation newmeta env table target = (* if subsumption env table newtarget then *) (* newmeta, build_identity newtarget *) (* else *) - demodulation newmeta env table newtarget + demodulation newmeta env table sign newtarget | None -> newmeta, target ;; @@ -578,19 +628,23 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term = let sup_l_counter = ref 1;; -let superposition_left (metasenv, context, ugraph) table target = +let superposition_left newmeta (metasenv, context, ugraph) table target = let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in let module CR = CicReduction in let module U = Utils in - let _, proof, (eq_ty, left, right, ordering), _, _ = target in + let weight, proof, (eq_ty, left, right, ordering), _, _ = target in let expansions, _ = let term = if ordering = U.Gt then left else right in betaexpand_term metasenv context ugraph table 0 term in + let maxmeta = ref newmeta in let build_new (bo, s, m, ug, (eq_found, eq_URI)) = + + print_endline "\nSUPERPOSITION LEFT\n"; + let time1 = Unix.gettimeofday () in let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in @@ -600,8 +654,9 @@ let superposition_left (metasenv, context, ugraph) table target = let t' = let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in incr sup_l_counter; - let l, r = if ordering = U.Gt then bo', right else left, bo' in - (name, ty, eq_ty, l, r) + 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 bo'' = *) (* C.Appl ( *) @@ -615,11 +670,51 @@ let superposition_left (metasenv, context, ugraph) table target = (* incr sup_l_counter; *) (* C.Lambda (name, ty, bo'') *) (* in *) - bo', - Inference.ProofBlock (s, eq_URI, t', eq_found, target) -(* (\* M. *\)apply_subst s *) -(* (C.Appl [C.Const (eq_URI, []); ty; what; t'; *) -(* proof; other; proof']) *) + incr maxmeta; + let metaproof = + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + C.Meta (!maxmeta, irl) + in + let target' = + let eq_found = + let proof' = + let ens = + if pos = Utils.Left then + build_ens_for_sym_eq ty what other + else + build_ens_for_sym_eq ty other what + in + Inference.ProofSymBlock (ens, proof') + in + let what, other = + if pos = Utils.Left then what, other else other, what + in + pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args') + in + let target_proof = + let pb = + Inference.ProofBlock (s, eq_URI, t', eq_found, + Inference.BasicProof metaproof) + in + match proof with + | Inference.BasicProof _ -> + print_endline "replacing a BasicProof"; + pb + | Inference.ProofGoalBlock (_, parent_eq) -> + print_endline "replacing another ProofGoalBlock"; + Inference.ProofGoalBlock (pb, parent_eq) + | _ -> assert false + in + (weight, target_proof, (eq_ty, left, right, ordering), [], []) + in + let refl = + C.Appl [C.MutConstruct (* reflexivity *) + (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); + eq_ty; if ordering = U.Gt then right else left] + in + (bo', + Inference.ProofGoalBlock (Inference.BasicProof refl, target')) in let left, right = if ordering = U.Gt then newgoal, right else left, newgoal in @@ -634,11 +729,7 @@ let superposition_left (metasenv, context, ugraph) table target = in res in -(* let build_new = *) -(* let profile = CicUtil.profile "Inference.superposition_left.build_new" in *) -(* (fun e -> profile build_new e) *) -(* in *) - List.map build_new expansions + !maxmeta, List.map build_new expansions ;; @@ -680,8 +771,9 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = 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', right else left, bo' in - (name, ty, eq_ty, l, r) + 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 bo'' = *) (* C.Appl ( *) @@ -695,7 +787,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = (* C.Lambda (name, ty, bo'') *) (* in *) bo', - Inference.ProofBlock (s, eq_URI, t', eq_found, target) + Inference.ProofBlock (s, eq_URI, t', eq_found, eqproof(* target *)) (* (\* M. *\)apply_subst s *) (* (C.Appl [C.Const (eq_URI, []); ty; what; t'; *) (* eqproof; other; proof']) *) diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 62308896f..38bc6abe5 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -12,13 +12,15 @@ type equality = Cic.term list (* arguments *) and proof = + | NoProof | BasicProof of Cic.term | ProofBlock of Cic.substitution * UriManager.uri * (* name, ty, eq_ty, left, right *) (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * - (Utils.pos * equality) * equality - | NoProof + (Utils.pos * equality) * proof + | ProofGoalBlock of proof * equality + | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof ;; @@ -41,33 +43,108 @@ let string_of_equality ?env = ;; -let rec build_term_proof equality = +let build_proof_term equality = (* Printf.printf "build_term_proof %s" (string_of_equality equality); *) (* print_newline (); *) + + let indent = ref 0 in + + let rec do_build_proof proof = + match proof with + | NoProof -> + Printf.fprintf stderr "WARNING: no proof!\n"; +(* (string_of_equality equality); *) + Cic.Implicit None + | BasicProof term -> term + | ProofGoalBlock (proofbit, equality) -> + print_endline "found ProofGoalBlock, going up..."; + let _, proof, _, _, _ = equality in + do_build_goal_proof proofbit proof + | ProofSymBlock (ens, proof) -> + let proof = do_build_proof proof in + Cic.Appl [ + Cic.Const (HelmLibraryObjects.Logic.sym_eq_URI, ens); (* symmetry *) + proof + ] + | ProofBlock (subst, eq_URI, t', (pos, eq), eqproof) -> +(* Printf.printf "\nsubst:\n%s\n" (print_subst subst); *) +(* print_newline (); *) + + let name, ty, eq_ty, left, right = t' in + let bo = + Cic.Appl [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); + eq_ty; left; right] + in + let t' = Cic.Lambda (name, ty, (* CicSubstitution.lift 1 *) bo) in + (* Printf.printf " ProofBlock: eq = %s, eq' = %s" *) + (* (string_of_equality eq) (string_of_equality eq'); *) + (* print_newline (); *) + +(* let s = String.make !indent ' ' in *) +(* incr indent; *) + +(* print_endline (s ^ "build proof'------------"); *) + + let proof' = + let _, proof', _, _, _ = eq in + do_build_proof proof' + in +(* print_endline (s ^ "END proof'"); *) + +(* print_endline (s ^ "build eqproof-----------"); *) + + let eqproof = do_build_proof eqproof in + +(* print_endline (s ^ "END eqproof"); *) +(* decr indent; *) + + + let _, _, (ty, what, other, _), menv', args' = eq in + let what, other = + if pos = Utils.Left then what, other else other, what + in + CicMetaSubst.apply_subst subst + (Cic.Appl [Cic.Const (eq_URI, []); ty; + what; t'; eqproof; other; proof']) + + and do_build_goal_proof proofbit proof = +(* match proofbit with *) +(* | BasicProof _ -> do_build_proof proof *) +(* | proofbit -> *) + match proof with + | ProofGoalBlock (pb, eq) -> + do_build_proof (ProofGoalBlock (replace_proof proofbit pb, eq)) +(* let _, proof, _, _, _ = eq in *) +(* let newproof = replace_proof proofbit proof in *) +(* do_build_proof newproof *) + +(* | ProofBlock (subst, eq_URI, t', poseq, eqproof) -> *) +(* let eqproof' = replace_proof proofbit eqproof in *) +(* do_build_proof (ProofBlock (subst, eq_URI, t', poseq, eqproof')) *) + | _ -> do_build_proof (replace_proof proofbit proof) (* assert false *) + + and replace_proof newproof = function + | ProofBlock (subst, eq_URI, t', poseq, eqproof) -> + let uri = eq_URI in +(* if eq_URI = HelmLibraryObjects.Logic.eq_ind_URI then *) +(* HelmLibraryObjects.Logic.eq_ind_r_URI *) +(* else *) +(* HelmLibraryObjects.Logic.eq_ind_URI *) +(* in *) + let eqproof' = replace_proof newproof eqproof in + ProofBlock (subst, uri(* eq_URI *), t', poseq, eqproof') +(* ProofBlock (subst, eq_URI, t', poseq, newproof) *) + | ProofGoalBlock (pb, equality) -> + let pb' = replace_proof newproof pb in + ProofGoalBlock (pb', equality) +(* let w, proof, t, menv, args = equality in *) +(* let proof' = replace_proof newproof proof in *) +(* ProofGoalBlock (pb, (w, proof', t, menv, args)) *) + | BasicProof _ -> newproof + | p -> p + in let _, proof, _, _, _ = equality in - match proof with - | NoProof -> - Printf.fprintf stderr "WARNING: no proof for %s\n" - (string_of_equality equality); - Cic.Implicit None - | BasicProof term -> term - | ProofBlock (subst, eq_URI, t', (pos, eq), eq') -> - let name, ty, eq_ty, left, right = t' in - let bo = - Cic.Appl [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); - eq_ty; left; right] - in - let t' = Cic.Lambda (name, ty, CicSubstitution.lift 1 bo) in -(* Printf.printf " ProofBlock: eq = %s, eq' = %s" *) -(* (string_of_equality eq) (string_of_equality eq'); *) -(* print_newline (); *) - let proof' = build_term_proof eq in - let eqproof = build_term_proof eq' in - let _, _, (ty, what, other, _), menv', args' = eq in - let what, other = if pos = Utils.Left then what, other else other, what in - CicMetaSubst.apply_subst subst - (Cic.Appl [Cic.Const (eq_URI, []); ty; - what; t'; eqproof; other; proof']) + do_build_proof proof ;; @@ -493,9 +570,10 @@ let unification metasenv context t1 t2 ugraph = in (* Printf.printf "| subst: %s\n" (print_subst ~prefix:" ; " subst); *) (* print_endline "|"; *) - (* fix_subst *) subst, menv, ug + fix_subst subst, menv, ug ;; + (* let unification = CicUnification.fo_unif;; *) exception MatchingFailure;; @@ -1040,16 +1118,24 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = +(* print_endline ("fix_metas " ^ (string_of_int newmeta)); *) let table = Hashtbl.create (List.length args) in - let newargs, _ = + let is_this_case = ref false in + let newargs, newmeta = List.fold_right (fun t (newargs, index) -> match t with | Cic.Meta (i, l) -> Hashtbl.add table i index; +(* if index = 5469 then ( *) +(* Printf.printf "?5469 COMES FROM (%d): %s\n" *) +(* i (string_of_equality equality); *) +(* print_newline (); *) +(* is_this_case := true *) +(* ); *) ((Cic.Meta (index, l))::newargs, index+1) | _ -> assert false) - args ([], newmeta) + args ([], newmeta+1) in let repl where = ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs @@ -1074,8 +1160,60 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = List.filter (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs in - (newmeta + (List.length newargs) + 1, - (w, p, (ty, left, right, o), menv', newargs)) + let rec fix_proof = function + | NoProof -> NoProof + | BasicProof term -> BasicProof (repl term) + | ProofBlock (subst, eq_URI, t', (pos, eq), p) -> + +(* Printf.printf "fix_proof of equality %s, subst is:\n%s\n" *) +(* (string_of_equality equality) (print_subst subst); *) + + let subst' = + List.fold_left + (fun s arg -> + match arg with + | Cic.Meta (i, l) -> ( + try + let j = Hashtbl.find table i in + if List.mem_assoc i subst then + s + else +(* let _, context, ty = CicUtil.lookup_meta j menv' in *) +(* (i, (context, Cic.Meta (j, l), ty))::s *) + let _, context, ty = CicUtil.lookup_meta i menv in + (i, (context, Cic.Meta (j, l), ty))::s + with _ -> s + ) + | _ -> assert false) + [] args + in +(* let subst'' = *) +(* List.map *) +(* (fun (i, e) -> *) +(* try let j = Hashtbl.find table i in (j, e) *) +(* with _ -> (i, e)) subst *) +(* in *) + +(* Printf.printf "subst' is:\n%s\n" (print_subst subst'); *) +(* print_newline (); *) + + ProofBlock (subst' @ subst, eq_URI, t', (pos, eq), p) +(* | ProofSymBlock (ens, p) -> *) +(* let ens' = List.map (fun (u, t) -> (u, repl t)) ens in *) +(* ProofSymBlock (ens', fix_proof p) *) + | p -> assert false + in +(* (newmeta + (List.length newargs) + 2, *) + let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in +(* if !is_this_case then ( *) +(* print_endline "\nTHIS IS THE TROUBLE!!!"; *) +(* let pt = build_proof_term neweq in *) +(* Printf.printf "equality: %s\nproof: %s\n" *) +(* (string_of_equality neweq) (CicPp.ppterm pt); *) +(* print_endline (String.make 79 '-'); *) +(* ); *) + (newmeta + 1, neweq) +(* (w, fix_proof p, (ty, left, right, o), menv', newargs)) *) ;; diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli index 0ce2e40a6..76d48603d 100644 --- a/helm/ocaml/paramodulation/inference.mli +++ b/helm/ocaml/paramodulation/inference.mli @@ -9,13 +9,15 @@ type equality = Cic.term list (* arguments *) and proof = + | NoProof | BasicProof of Cic.term | ProofBlock of Cic.substitution * UriManager.uri * (* name, ty, eq_ty, left, right *) (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * - (Utils.pos * equality) * equality - | NoProof + (Utils.pos * equality) * proof + | ProofGoalBlock of proof * equality + | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph @@ -99,4 +101,4 @@ val extract_differing_subterms: Cic.term -> Cic.term -> (Cic.term * Cic.term) option -val build_term_proof: equality -> Cic.term +val build_proof_term: equality -> Cic.term diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index c933aec0b..a6c4fc8ad 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -18,10 +18,10 @@ let elapsed_time = ref 0.;; let maximal_retained_equality = ref None;; (* equality-selection related globals *) -let use_fullred = ref false;; -let weight_age_ratio = ref 0;; (* settable by the user from the command line *) +let use_fullred = ref true;; +let weight_age_ratio = ref 3;; (* settable by the user from the command line *) let weight_age_counter = ref !weight_age_ratio;; -let symbols_ratio = ref 0;; +let symbols_ratio = ref 2;; let symbols_counter = ref 0;; (* statistics... *) @@ -376,7 +376,10 @@ let infer env sign current (active_list, active_table) = let new_neg, new_pos = match sign with | Negative -> - Indexing.superposition_left env active_table current, [] + let maxm, res = + Indexing.superposition_left !maxmeta env active_table current in + maxmeta := maxm; + res, [] | Positive -> let maxm, res = Indexing.superposition_right !maxmeta env active_table current in @@ -384,7 +387,9 @@ let infer env sign current (active_list, active_table) = let rec infer_positive table = function | [] -> [], [] | (Negative, equality)::tl -> - let res = Indexing.superposition_left env table equality in + let maxm, res = + Indexing.superposition_left !maxmeta env table equality in + maxmeta := maxm; let neg, pos = infer_positive table tl in res @ neg, pos | (Positive, equality)::tl -> @@ -455,7 +460,7 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = let demodulate table current = let newmeta, newcurrent = - Indexing.demodulation !maxmeta env table current in + Indexing.demodulation !maxmeta env table sign current in maxmeta := newmeta; if is_identity env newcurrent then if sign = Negative then Some (sign, newcurrent) @@ -542,8 +547,9 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = let t2 = Unix.gettimeofday () in fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1); - let demodulate table target = - let newmeta, newtarget = Indexing.demodulation !maxmeta env table target in + let demodulate sign table target = + let newmeta, newtarget = + Indexing.demodulation !maxmeta env table sign target in maxmeta := newmeta; newtarget in @@ -555,13 +561,13 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = let t1 = Unix.gettimeofday () in let new_neg, new_pos = - let new_neg = List.map (demodulate active_table) new_neg - and new_pos = List.map (demodulate active_table) new_pos in + let new_neg = List.map (demodulate Negative active_table) new_neg + and new_pos = List.map (demodulate Positive active_table) new_pos in match passive_table with | None -> new_neg, new_pos | Some passive_table -> - List.map (demodulate passive_table) new_neg, - List.map (demodulate passive_table) new_pos + List.map (demodulate Negative passive_table) new_neg, + List.map (demodulate Positive passive_table) new_pos in let t2 = Unix.gettimeofday () in @@ -835,7 +841,7 @@ let rec given_clause env passive active = al @ [(sign, current)], Indexing.index tbl current in let passive = add_to_passive passive new' in -(* let (_, ns), (_, ps), _ = passive in *) + let (_, ns), (_, ps), _ = passive in (* Printf.printf "passive:\n%s\n" *) (* (String.concat "\n" *) (* ((List.map (fun e -> "Negative " ^ *) @@ -963,6 +969,16 @@ let rec given_clause_fullred env passive active = match contains_empty env new' with | false, _ -> let passive = add_to_passive passive new' in + let (_, ns), (_, ps), _ = passive in +(* Printf.printf "passive:\n%s\n" *) +(* (String.concat "\n" *) +(* ((List.map (fun e -> "Negative " ^ *) +(* (string_of_equality ~env e)) *) +(* (EqualitySet.elements ns)) @ *) +(* (List.map (fun e -> "Positive " ^ *) +(* (string_of_equality ~env e)) *) +(* (EqualitySet.elements ps)))); *) +(* print_newline (); *) given_clause_fullred env passive active | true, goal -> Success (goal, env) @@ -996,16 +1012,26 @@ let main () = let module PP = CicPp in let term, metasenv, ugraph = get_from_user () in let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in - let proof, goals = - PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in - let goal = List.nth goals 0 in + let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in + let proof, goals = status in + let goal' = List.nth goals 0 in let _, metasenv, meta_proof, _ = proof in - let _, context, goal = CicUtil.lookup_meta goal metasenv in + let _, context, goal = CicUtil.lookup_meta goal' metasenv in let equalities, maxm = find_equalities context proof in - maxmeta := maxm; (* TODO ugly!! *) + maxmeta := maxm+2; (* TODO ugly!! *) + let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in + let new_meta_goal, metasenv, type_of_goal = + let _, context, ty = CicUtil.lookup_meta goal' metasenv in + Printf.printf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty); + print_newline (); + Cic.Meta (maxm+1, irl), + (maxm+1, context, ty)::metasenv, + ty + in +(* let new_meta_goal = Cic.Meta (goal', irl) in *) let env = (metasenv, context, ugraph) in try - let term_equality = equality_of_term meta_proof goal in + let term_equality = equality_of_term new_meta_goal goal in let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in let active = make_active () in let passive = make_passive [term_equality] equalities in @@ -1033,9 +1059,34 @@ let main () = Printf.printf "NO proof found! :-(\n\n" | Success (Some goal, env) -> Printf.printf "OK, found a proof!\n"; - let proof = Inference.build_term_proof goal in - print_endline (PP.pp proof (names_of_context context)); + let proof = Inference.build_proof_term goal in + (* REMEMBER: we have to instantiate meta_proof, we should use + apply the "apply" tactic to proof and status + *) + let names = names_of_context context in + print_endline (PP.pp proof names); +(* print_endline (PP.ppterm proof); *) + print_endline (string_of_float (finish -. start)); + let newmetasenv = + List.fold_left + (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities + in + let _ = + try + let ty, ug = + CicTypeChecker.type_of_aux' newmetasenv context proof ugraph + in + Printf.printf + "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n" + (CicPp.pp type_of_goal names) (CicPp.pp ty names) + (string_of_bool + (fst (CicReduction.are_convertible context type_of_goal ty ug))); + with e -> + Printf.printf "MAXMETA USED: %d\n" !maxmeta; + in + () + | Success (None, env) -> Printf.printf "Success, but no proof?!?\n\n" in @@ -1062,7 +1113,7 @@ let main () = ;; -let configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";; +let configuration_file = ref "../../matita/matita.conf.xml";; let _ = let set_ratio v = weight_age_ratio := (v+1); weight_age_counter := (v+1) @@ -1070,16 +1121,17 @@ let _ = and set_conf f = configuration_file := f and set_lpo () = Utils.compare_terms := lpo and set_kbo () = Utils.compare_terms := nonrec_kbo - and set_fullred () = use_fullred := true + and set_fullred b = use_fullred := b and set_time_limit v = time_limit := float_of_int v in Arg.parse [ - "-f", Arg.Unit set_fullred, "Use full-reduction strategy"; + "-f", Arg.Bool set_fullred, + "Enable/disable full-reduction strategy (default: enabled)"; - "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 0)"; + "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 3)"; "-s", Arg.Int set_sel, - "symbols-based selection ratio (relative to the weight ratio)"; + "symbols-based selection ratio (relative to the weight ratio, default: 2)"; "-c", Arg.String set_conf, "Configuration file (for the db connection)"; diff --git a/helm/ocaml/paramodulation/test_indexing.ml b/helm/ocaml/paramodulation/test_indexing.ml index 0324f9e56..7391812f3 100644 --- a/helm/ocaml/paramodulation/test_indexing.ml +++ b/helm/ocaml/paramodulation/test_indexing.ml @@ -1,6 +1,6 @@ open Path_indexing - +(* let build_equality term = let module C = Cic in C.Implicit None, (C.Implicit None, term, C.Rel 1, Utils.Gt), [], [] @@ -166,11 +166,75 @@ let test_subst () = and t2 = M.apply_subst subst2 term in Printf.printf "t1 = %s\nt2 = %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); ;; +*) + +let test_refl () = + let module C = Cic in + let context = [ + Some (C.Name "H", C.Decl ( + C.Prod (C.Name "z", C.Rel 3, + C.Appl [ + C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); + C.Rel 4; C.Rel 3; C.Rel 1]))); + Some (C.Name "x", C.Decl (C.Rel 2)); + Some (C.Name "y", C.Decl (C.Rel 1)); + Some (C.Name "A", C.Decl (C.Sort C.Set)) + ] + in + let term = C.Appl [ + C.Const (HelmLibraryObjects.Logic.eq_ind_URI, []); C.Rel 4; + C.Rel 2; + C.Lambda (C.Name "z", C.Rel 4, + C.Appl [ + C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); + C.Rel 5; C.Rel 1; C.Rel 3 + ]); + C.Appl [C.MutConstruct + (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); (* reflexivity *) + C.Rel 4; C.Rel 2]; + C.Rel 3; +(* C.Appl [C.Const (HelmLibraryObjects.Logic.sym_eq_URI, []); (\* symmetry *\) *) +(* C.Rel 4; C.Appl [C.Rel 1; C.Rel 2]] *) + C.Appl [ + C.Const (HelmLibraryObjects.Logic.eq_ind_URI, []); + C.Rel 4; C.Rel 3; + C.Lambda (C.Name "z", C.Rel 4, + C.Appl [ + C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); + C.Rel 5; C.Rel 1; C.Rel 4 + ]); + C.Appl [C.MutConstruct (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); + C.Rel 4; C.Rel 3]; + C.Rel 2; C.Appl [C.Rel 1; C.Rel 2] + ] + ] in + let ens = [ + (UriManager.uri_of_string"cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var", + C.Rel 4); + (UriManager.uri_of_string"cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var", + C.Rel 3); + (UriManager.uri_of_string"cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var", + C.Rel 2); + ] in + let term2 = C.Appl [ + C.Const (HelmLibraryObjects.Logic.sym_eq_URI, ens); + C.Appl [C.Rel 1; C.Rel 2] + ] in + let ty, ug = + CicTypeChecker.type_of_aux' [] context term CicUniv.empty_ugraph + in + Printf.printf "OK, %s ha tipo %s\n" (CicPp.ppterm term) (CicPp.ppterm ty); + let ty, ug = + CicTypeChecker.type_of_aux' [] context term2 CicUniv.empty_ugraph + in + Printf.printf "OK, %s ha tipo %s\n" (CicPp.ppterm term2) (CicPp.ppterm ty); +;; (* differing ();; *) (* next_after ();; *) (* discrimination_tree_test ();; *) (* path_indexing_test ();; *) -test_subst ();; - +(* test_subst ();; *) +Helm_registry.load_from "../../matita/matita.conf.xml"; +test_refl ();;