X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=f3af1b482e8afb2eece8d1ce79d3e10af7812ec7;hb=4ab3123d6a8e5080009d7b471b0cefd05f4817ed;hp=d35fbff34ee0f36f96236369d9b05eba7f78f5a2;hpb=fadd7bc21be08f3da589772db01b6645d20769f9;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index d35fbff34..f3af1b482 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -23,17 +23,15 @@ * http://cs.unibo.it/helm/. *) -(* $Id$ *) +(* let _profiler = <:profiler<_profiler>>;; *) -type goal = Equality.goal_proof * Cic.metasenv * Cic.term +(* $Id$ *) module Index = Equality_indexing.DT (* discrimination tree based indexing *) (* module Index = Equality_indexing.DT (* path tree based indexing *) *) -let beta_expand_time = ref 0.;; - let debug_print = Utils.debug_print;; (* @@ -61,7 +59,7 @@ type retrieval_mode = Matching | Unification;; let string_of_res ?env = function None -> "None" - | Some (t, s, m, u, ((p,e), eq_URI)) -> + | Some (t, s, m, u, (p,e)) -> Printf.sprintf "Some: (%s, %s, %s)" (Utils.string_of_pos p) (Equality.string_of_equality ?env e) @@ -92,9 +90,6 @@ let print_candidates ?env mode term res = ;; -let indexing_retrieval_time = ref 0.;; - - let apply_subst = Subst.apply_subst let index = Index.index @@ -125,7 +120,7 @@ let check_for_duplicates metas msg = let check_res res msg = match res with - Some (t, subst, menv, ug, (eq_found, eq_URI)) -> + Some (t, subst, menv, ug, eq_found) -> let eqs = Equality.string_of_equality (snd eq_found) in check_disjoint_invariant subst menv msg; check_for_duplicates menv (msg ^ "\nchecking " ^ eqs); @@ -182,32 +177,17 @@ let check_target context target msg = *) let get_candidates ?env mode tree term = - let t1 = Unix.gettimeofday () in - let res = - let s = - match mode with - | Matching -> Index.retrieve_generalizations tree term - | Unification -> Index.retrieve_unifiables tree term - in - Index.PosEqSet.elements s + let s = + match mode with + | Matching -> + Index.retrieve_generalizations tree term + | Unification -> + Index.retrieve_unifiables tree term + in -(* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *) -(* print_newline (); *) - let t2 = Unix.gettimeofday () in - indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1); - (* make fresh instances *) - res + Index.PosEqSet.elements s ;; -let profiler = HExtlib.profile "P/Indexing.get_candidates" - -let get_candidates ?env mode tree term = - profiler.HExtlib.profile (get_candidates ?env mode tree) term - -let match_unif_time_ok = ref 0.;; -let match_unif_time_no = ref 0.;; - - (* finds the first equality in the index that matches "term", of type "termty" termty can be Implicit if it is not needed. The result (one of the sides of @@ -252,45 +232,33 @@ let rec find_matches metasenv context ugraph lift_amount term termty = let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in let t="t = " ^ (CicPp.ppterm term) ^ "\n" in let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in +(* let p="proof = "^ (CicPp.ppterm(Equality.build_proof_term proof))^"\n" in +*) check_for_duplicates metas "gia nella metas"; - check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^p) + check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m(*^p*)) end; if check && not (fst (CicReduction.are_convertible ~metasenv context termty ty ugraph)) then ( find_matches metasenv context ugraph lift_amount term termty tl ) else - let do_match c eq_URI = + let do_match c = let subst', metasenv', ugraph' = - let t1 = Unix.gettimeofday () in - try - let r = - ( Inference.matching metasenv metas context - term (S.lift lift_amount c)) ugraph - in - let t2 = Unix.gettimeofday () in - match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1); - r - with - | Inference.MatchingFailure as e -> - let t2 = Unix.gettimeofday () in - match_unif_time_no := !match_unif_time_no +. (t2 -. t1); - raise e - | CicUtil.Meta_not_found _ as exn -> raise exn + Inference.matching + metasenv metas context term (S.lift lift_amount c) ugraph in - Some (Cic.Rel (1 + lift_amount), subst', metasenv', ugraph', - (candidate, eq_URI)) + Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate) in - let c, other, eq_URI = - if pos = Utils.Left then left, right, Utils.eq_ind_URI () - else right, left, Utils.eq_ind_r_URI () + let c, other = + if pos = Utils.Left then left, right + else right, left in if o <> U.Incomparable then let res = try - do_match c eq_URI + do_match c with Inference.MatchingFailure -> find_matches metasenv context ugraph lift_amount term termty tl in @@ -298,7 +266,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty = res else let res = - try do_match c eq_URI + try do_match c with Inference.MatchingFailure -> None in if Utils.debug_res then ignore (check_res res "find2"); @@ -318,6 +286,10 @@ let rec find_matches metasenv context ugraph lift_amount term termty = find_matches metasenv context ugraph lift_amount term termty tl ;; +let find_matches metasenv context ugraph lift_amount term termty = + find_matches metasenv context ugraph lift_amount term termty +;; + (* as above, but finds all the matching equalities, and the matching condition can be either Inference.matching or Inference.unification @@ -335,46 +307,19 @@ let rec find_all_matches ?(unif_fun=Inference.unification) | candidate::tl -> let pos, equality = candidate in let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in - let do_match c eq_URI = + let do_match c = let subst', metasenv', ugraph' = - let t1 = Unix.gettimeofday () in - try - let term = - match c,term with - | Cic.Meta _, Cic.Appl[Cic.MutInd(u,0,_);_;l;r] - when LibraryObjects.is_eq_URI u -> l -(* - if Utils.compare_weights (Utils.weight_of_term l) - (Utils.weight_of_term r) = Utils.Gt - then l else r -*) - | _ -> term - in - - let r = - unif_fun metasenv metas context - term (S.lift lift_amount c) ugraph in - let t2 = Unix.gettimeofday () in - match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1); - r - with - | Inference.MatchingFailure - | CicUnification.UnificationFailure _ - | CicUnification.Uncertain _ as e -> - let t2 = Unix.gettimeofday () in - match_unif_time_no := !match_unif_time_no +. (t2 -. t1); - raise e + unif_fun metasenv metas context term (S.lift lift_amount c) ugraph in - (C.Rel (1 + lift_amount), subst', metasenv', ugraph', - (candidate, eq_URI)) + (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate) in - let c, other, eq_URI = - if pos = Utils.Left then left, right, Utils.eq_ind_URI () - else right, left, Utils.eq_ind_r_URI () + let c, other = + if pos = Utils.Left then left, right + else right, left in if o <> U.Incomparable then try - let res = do_match c eq_URI in + let res = do_match c in res::(find_all_matches ~unif_fun metasenv context ugraph lift_amount term termty tl) with @@ -385,7 +330,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification) lift_amount term termty tl else try - let res = do_match c eq_URI in + let res = do_match c in match res with | _, s, _, _, _ -> let c' = apply_subst s c @@ -408,24 +353,22 @@ let rec find_all_matches ?(unif_fun=Inference.unification) let find_all_matches ?unif_fun metasenv context ugraph lift_amount term termty l = - let rc = find_all_matches ?unif_fun metasenv context ugraph lift_amount term termty l - in (*prerr_endline "CANDIDATES:"; List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l; prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int (List.length rc));*) - rc - +;; (* returns true if target is subsumed by some equality in table *) +let print_res l = + prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug, + ((pos,equation),_)) -> Equality.string_of_equality equation)l)) +;; + let subsumption_aux use_unification env table target = -(* let print_res l =*) -(* prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,*) -(* ((pos,equation),_)) -> Equality.string_of_equality equation)l))*) -(* in*) let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in let metasenv, context, ugraph = env in let metasenv = tmetas in @@ -443,25 +386,25 @@ let subsumption_aux use_unification env table target = find_all_matches ~unif_fun metasenv context ugraph 0 left ty leftc in -(* print_res leftr;*) - let rec ok what = function + let rec ok what leftorright = function | [] -> None - | (_, subst, menv, ug, ((pos,equation),_))::tl -> + | (_, subst, menv, ug, (pos,equation))::tl -> let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in try let other = if pos = Utils.Left then r else l in let what' = Subst.apply_subst subst what in + let other' = Subst.apply_subst subst other in let subst', menv', ug' = - unif_fun metasenv m context what' other ugraph + unif_fun metasenv m context what' other' ugraph in (match Subst.merge_subst_if_possible subst subst' with - | None -> ok what tl - | Some s -> Some (s, equation)) + | None -> ok what leftorright tl + | Some s -> Some (s, equation, leftorright <> pos )) with | Inference.MatchingFailure - | CicUnification.UnificationFailure _ -> ok what tl + | CicUnification.UnificationFailure _ -> ok what leftorright tl in - match ok right leftr with + match ok right Utils.Left leftr with | Some _ as res -> res | None -> let rightr = @@ -472,17 +415,16 @@ let subsumption_aux use_unification env table target = find_all_matches ~unif_fun metasenv context ugraph 0 right ty rightc in -(* print_res rightr;*) - ok left rightr -(* (if r then *) -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *) -(* (Inference.string_of_equality target) (Utils.print_subst s)))); *) + ok left Utils.Right rightr +;; + +let subsumption x y z = + subsumption_aux false x y z ;; -let subsumption = subsumption_aux false;; -let unification = subsumption_aux true;; +let unification x y z = + subsumption_aux true x y z +;; let rec demodulation_aux ?from ?(typecheck=false) metasenv context ugraph table lift_amount term = @@ -583,18 +525,10 @@ let rec demodulation_aux ?from ?(typecheck=false) res ;; - -let build_newtarget_time = ref 0.;; - - -let demod_counter = ref 1;; - exception Foo -let profiler = HExtlib.profile "P/Indexing.demod_eq[build_new_target]" - (** demodulation, when target is an equality *) -let rec demodulation_equality ?from newmeta env table sign target = +let rec demodulation_equality ?from eq_uri newmeta env table target = let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -616,8 +550,7 @@ let rec demodulation_equality ?from newmeta env table sign target = 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 + let build_newtarget is_left (t, subst, menv, ug, eq_found) = if Utils.debug_metas then begin @@ -639,110 +572,25 @@ let rec demodulation_equality ?from newmeta env table sign target = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in (* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*) let name = C.Name "x" in - incr demod_counter; let bo' = let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in - C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); - S.lift 1 eq_ty; l; r] + C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r] in - if sign = Utils.Positive then (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'), (Cic.Lambda (name, ty, bo')))))) - else - assert false -(* - begin - prerr_endline "***************************************negative"; - let metaproof = - incr maxmeta; - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context in -(* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *) -(* print_newline (); *) - C.Meta (!maxmeta, irl) - in - let eq_found = - let proof'_old' = - let termlist = - if pos = Utils.Left then [ty; what; other] - else [ty; other; what] - in - Equality.ProofSymBlock (termlist, proof'_old) - in - let proof'_new' = assert false (* not implemented *) in - let what, other = - if pos = Utils.Left then what, other else other, what - in - pos, - Equality.mk_equality - (0, (proof'_new',proof'_old'), - (ty, other, what, Utils.Incomparable),menv') - in - let target_proof = - let pb = - Equality.ProofBlock - (subst, eq_URI, (name, ty), bo', - eq_found, Equality.BasicProof (Equality.empty_subst,metaproof)) - in - assert false, (* not implemented *) - (match snd proof with - | Equality.BasicProof _ -> - (* print_endline "replacing a BasicProof"; *) - pb - | Equality.ProofGoalBlock (_, parent_proof) -> - (* print_endline "replacing another ProofGoalBlock"; *) - Equality.ProofGoalBlock (pb, parent_proof) - | _ -> assert false) - in - let refl = - C.Appl [C.MutConstruct (* reflexivity *) - (LibraryObjects.eq_URI (), 0, 1, []); - eq_ty; if is_left then right else left] - in - (bo, - (assert false, (* not implemented *) - Equality.ProofGoalBlock - (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof))) - end -*) - in - let newmenv = (* Inference.filter subst *) menv in - let _ = - if Utils.debug_metas then - try ignore(CicTypeChecker.type_of_aux' - newmenv context - (Equality.build_proof_term newproof) ugraph); - () - with exc -> - prerr_endline "sempre lui"; - prerr_endline (Subst.ppsubst subst); - prerr_endline (CicPp.ppterm - (Equality.build_proof_term newproof)); - prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t)); - prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what)); - prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other)); - prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst)); - prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv [] - newmenv)); - raise exc; - else () in + let newmenv = menv in let left, right = if is_left then newterm, right else left, newterm in let ordering = !Utils.compare_terms left right in let stat = (eq_ty, left, right, ordering) in - let time2 = Unix.gettimeofday () in - build_newtarget_time := !build_newtarget_time +. (time2 -. time1); let res = let w = Utils.compute_equality_weight stat in - Equality.mk_equality (w, newproof, stat,newmenv) + (Equality.mk_equality (w, newproof, stat,newmenv)) in if Utils.debug_metas then ignore(check_target context res "buildnew_target output"); !maxmeta, res in - let build_newtarget is_left x = - profiler.HExtlib.profile (build_newtarget is_left) x - in let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in if Utils.debug_res then check_res res "demod result"; @@ -755,7 +603,7 @@ let rec demodulation_equality ?from newmeta env table sign target = (Equality.meta_convertibility_eq target newtarget) then newmeta, newtarget else - demodulation_equality ?from newmeta env table sign newtarget + demodulation_equality ?from eq_uri newmeta env table newtarget | None -> let res = demodulation_aux metasenv' context ugraph table 0 right in if Utils.debug_res then check_res res "demod result 1"; @@ -766,7 +614,7 @@ let rec demodulation_equality ?from newmeta env table sign target = (Equality.meta_convertibility_eq target newtarget) then newmeta, newtarget else - demodulation_equality ?from newmeta env table sign newtarget + demodulation_equality ?from eq_uri newmeta env table newtarget | None -> newmeta, target in @@ -779,16 +627,18 @@ let rec demodulation_equality ?from newmeta env table sign target = i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2 in table. *) -let rec betaexpand_term metasenv context ugraph table lift_amount term = +let rec betaexpand_term + ?(subterms_only=false) metasenv context ugraph table lift_amount term += let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in - let candidates = get_candidates Unification table term in let res, lifted_term = match term with | C.Meta (i, l) -> + let l = [] in let l', lifted_l = List.fold_right (fun arg (res, lifted_tl) -> @@ -860,8 +710,8 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term = | C.Appl l -> let l', lifted_l = - List.fold_right - (fun arg (res, lifted_tl) -> + List.fold_left + (fun (res, lifted_tl) arg -> let arg_res, lifted_arg = betaexpand_term metasenv context ugraph table lift_amount arg in @@ -877,7 +727,7 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term = lifted_arg::r, s, m, ug, eq_found) res), lifted_arg::lifted_tl) - ) l ([], []) + ) ([], []) (List.rev l) in (List.map (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l', @@ -892,88 +742,17 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term = C.Implicit None, ugraph (* CicTypeChecker.type_of_aux' metasenv context term ugraph *) in + let candidates = get_candidates Unification table term in let r = - find_all_matches - metasenv context ugraph lift_amount term termty candidates + if subterms_only then + [] + else + find_all_matches + metasenv context ugraph lift_amount term termty candidates in r @ res, lifted_term ;; -let profiler = HExtlib.profile "P/Indexing.betaexpand_term" - -let betaexpand_term metasenv context ugraph table lift_amount term = - profiler.HExtlib.profile - (betaexpand_term metasenv context ugraph table lift_amount) term - - -let sup_l_counter = ref 1;; - -(** - superposition_left - returns a list of new clauses inferred with a left superposition step - the negative equation "target" and one of the positive equations in "table" -*) -let fix_expansion (eq,ty,unchanged,posu) (t, subst, menv, ug, eq_f) = - let unchanged = CicSubstitution.lift 1 unchanged in - let ty = CicSubstitution.lift 1 ty in - let pred = - match posu with - | Utils.Left -> Cic.Appl [eq;ty;unchanged;t] - | Utils.Right -> Cic.Appl [eq;ty;t;unchanged] - in - (pred, subst, menv, ug, eq_f) -;; - -let build_newgoal context goalproof goal_info expansion = - let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal_info expansion in - let pos, equality = eq_found in - let (_, proof', (ty, what, other, _), menv',id) = - Equality.open_equality equality in - let what, other = if pos = Utils.Left then what, other else other, what in - let newterm, newgoalproof = - let bo = - Utils.guarded_simpl context - (apply_subst subst (CicSubstitution.subst other t)) - in - let bo' = (*apply_subst subst*) t in - let name = Cic.Name "x" in - let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in - bo, (newgoalproofstep::goalproof) - in - let newmetasenv = (* Inference.filter subst *) menv in - (newgoalproof, newmetasenv, newterm) -;; - -let superposition_left - (metasenv, context, ugraph) table (proof,menv,ty) -= - 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 big,small,pos,eq,ty = - match ty with - | Cic.Appl [eq;ty;l;r] -> - let c = - Utils.compare_weights ~normalize:true - (Utils.weight_of_term l) (Utils.weight_of_term r) - in - (match c with - | Utils.Gt -> l,r,Utils.Right,eq,ty - | _ -> r,l,Utils.Left,eq,ty) - | _ -> - let names = Utils.names_of_context context in - prerr_endline ("NON TROVO UN EQ: " ^ CicPp.pp ty names); - assert false - in - let expansions, _ = betaexpand_term menv context ugraph table 0 big in - List.map (build_newgoal context proof (eq,ty,small,pos)) expansions -;; - -let sup_r_counter = ref 1;; - (** superposition_right returns a list of new clauses inferred with a right superposition step @@ -981,7 +760,8 @@ let sup_r_counter = ref 1;; the first free meta index, i.e. the first number above the highest meta index: its updated value is also returned *) -let superposition_right newmeta (metasenv, context, ugraph) table target = +let superposition_right + ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target= let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -996,18 +776,11 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = let metasenv' = newmetas in let maxmeta = ref newmeta in let res1, res2 = - let betaexpand_term metasenv context ugraph table d term = - let t1 = Unix.gettimeofday () in - let res = betaexpand_term metasenv context ugraph table d term in - let t2 = Unix.gettimeofday () in - beta_expand_time := !beta_expand_time +. (t2 -. t1); - res - in match ordering with | U.Gt -> - fst (betaexpand_term metasenv' context ugraph table 0 left), [] + fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), [] | U.Lt -> - [], fst (betaexpand_term metasenv' context ugraph table 0 right) + [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right) | _ -> let res l r = List.filter @@ -1015,14 +788,13 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = let subst = apply_subst subst in let o = !Utils.compare_terms (subst l) (subst r) in o <> U.Lt && o <> U.Le) - (fst (betaexpand_term metasenv' context ugraph table 0 l)) + (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l)) in (res left right), (res right left) in - let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) = + let build_new ordering (bo, s, m, ug, eq_found) = if Utils.debug_metas then ignore (check_target context (snd eq_found) "buildnew1" ); - let time1 = Unix.gettimeofday () in let pos, equality = eq_found in let (_, proof', (ty, what, other, _), menv',id') = @@ -1035,12 +807,10 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in let name = C.Name "x" in - incr sup_r_counter; let bo'' = let l, r = if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in - C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); - S.lift 1 eq_ty; l; r] + C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r] in bo', Equality.Step @@ -1065,8 +835,6 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = newm, eq' in maxmeta := newmeta; - let time2 = Unix.gettimeofday () in - build_newtarget_time := !build_newtarget_time +. (time2 -. time1); if Utils.debug_metas then ignore(check_target context newequality "buildnew2"); newequality @@ -1078,47 +846,6 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = (List.filter ok (new1 @ new2))) ;; -(** demodulation, when the target is a goal *) -let goal_metaconvertibility_eq (_,_,g1) (_,_,g2) = - Equality.meta_convertibility g1 g2 -;; - -let rec demodulation_goal env table goal = - let metasenv, context, ugraph = env in - let goalproof, metas, term = goal in - let term = Utils.guarded_simpl (~debug:true) context term in - let goal = goalproof, metas, term in - let metasenv' = metas in - - let left,right,eq,ty = - match term with - | Cic.Appl [eq;ty;l;r] -> l,r,eq,ty - | _ -> assert false - in - let do_right () = - let resright = demodulation_aux metasenv' context ugraph table 0 right in - match resright with - | Some t -> - let newg=build_newgoal context goalproof (eq,ty,left,Utils.Left) t in - if goal_metaconvertibility_eq goal newg then - false, goal - else - true, snd (demodulation_goal env table newg) - | None -> false, goal - in - let resleft = - demodulation_aux (*~typecheck:true*) metasenv' context ugraph table 0 left - in - match resleft with - | Some t -> - let newg = build_newgoal context goalproof (eq,ty,right,Utils.Right) t in - if goal_metaconvertibility_eq goal newg then - do_right () - else - true, snd (demodulation_goal env table newg) - | None -> do_right () -;; - (** demodulation, when the target is a theorem *) let rec demodulation_theorem newmeta env table theorem = let module C = Cic in @@ -1130,7 +857,7 @@ let rec demodulation_theorem newmeta env table theorem = let term, termty, metas = theorem in let metasenv' = metas in - let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) = + let build_newtheorem (t, subst, menv, ug, eq_found) = let pos, equality = eq_found in let (_, proof', (ty, what, other, _), menv',id) = Equality.open_equality equality in @@ -1139,7 +866,6 @@ let rec demodulation_theorem newmeta env table theorem = let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in (* let bo' = apply_subst subst t in *) (* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*) - incr demod_counter; (* let newproofold = Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found, @@ -1167,3 +893,144 @@ let rec demodulation_theorem newmeta env table theorem = newmeta, theorem ;; +(*****************************************************************************) +(** OPERATIONS ON GOALS **) +(** **) +(** DEMODULATION_GOAL & SUPERPOSITION_LEFT **) +(*****************************************************************************) + +let open_goal g = + match g with + | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) -> + assert (LibraryObjects.is_eq_URI uri); + proof,menv,eq,ty,l,r + | _ -> assert false +;; + +let ty_of_goal (_,_,ty) = ty ;; + +(* checks if two goals are metaconvertible *) +let goal_metaconvertibility_eq g1 g2 = + Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2) +;; + +(* when the betaexpand_term function is called on the left/right side of the + * goal, the predicate has to be fixed + * C[x] ---> (eq ty unchanged C[x]) + * [posu] is the side of the [unchanged] term in the original goal + *) +let fix_expansion goal posu (t, subst, menv, ug, eq_f) = + let _,_,eq,ty,l,r = open_goal goal in + let unchanged = if posu = Utils.Left then l else r in + let unchanged = CicSubstitution.lift 1 unchanged in + let ty = CicSubstitution.lift 1 ty in + let pred = + match posu with + | Utils.Left -> Cic.Appl [eq;ty;unchanged;t] + | Utils.Right -> Cic.Appl [eq;ty;t;unchanged] + in + (pred, subst, menv, ug, eq_f) +;; + +(* ginve the old [goal], the side that has not changed [posu] and the + * expansion builds a new goal *) +let build_newgoal context goal posu rule expansion = + let goalproof,_,_,_,_,_ = open_goal goal in + let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in + let pos, equality = eq_found in + let (_, proof', (ty, what, other, _), menv',id) = + Equality.open_equality equality in + let what, other = if pos = Utils.Left then what, other else other, what in + let newterm, newgoalproof = + let bo = + Utils.guarded_simpl context + (apply_subst subst (CicSubstitution.subst other t)) + in + let bo' = (*apply_subst subst*) t in + let name = Cic.Name "x" in + let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in + bo, (newgoalproofstep::goalproof) + in + let newmetasenv = (* Inference.filter subst *) menv in + (newgoalproof, newmetasenv, newterm) +;; + +(** + superposition_left + returns a list of new clauses inferred with a left superposition step + the negative equation "target" and one of the positive equations in "table" +*) +let superposition_left (metasenv, context, ugraph) table goal maxmeta = + let names = Utils.names_of_context context in + let proof,menv,eq,ty,l,r = open_goal goal in + let c = !Utils.compare_terms l r in + let newgoals = + if c = Utils.Incomparable then + begin + let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in + let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in + (* prerr_endline "incomparable"; + prerr_endline (string_of_int (List.length expansionsl)); + prerr_endline (string_of_int (List.length expansionsr)); + *) + List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl + @ + List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr + end + else + match c with + | Utils.Gt -> (* prerr_endline "GT"; *) + let big,small,possmall = l,r,Utils.Right in + let expansions, _ = betaexpand_term menv context ugraph table 0 big in + List.map + (build_newgoal context goal possmall Equality.SuperpositionLeft) + expansions + | Utils.Lt -> (* prerr_endline "LT"; *) + let big,small,possmall = r,l,Utils.Left in + let expansions, _ = betaexpand_term menv context ugraph table 0 big in + List.map + (build_newgoal context goal possmall Equality.SuperpositionLeft) + expansions + | Utils.Eq -> [] + | _ -> + prerr_endline + ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names); + assert false + in + (* rinfresco le meta *) + List.fold_right + (fun g (max,acc) -> + let max,g = Equality.fix_metas_goal max g in max,g::acc) + newgoals (maxmeta,[]) +;; + +(** demodulation, when the target is a goal *) +let rec demodulation_goal env table goal = + let goalproof,menv,_,_,left,right = open_goal goal in + let _, context, ugraph = env in +(* let term = Utils.guarded_simpl (~debug:true) context term in*) + let do_right () = + let resright = demodulation_aux menv context ugraph table 0 right in + match resright with + | Some t -> + let newg = + build_newgoal context goal Utils.Left Equality.Demodulation t + in + if goal_metaconvertibility_eq goal newg then + false, goal + else + true, snd (demodulation_goal env table newg) + | None -> false, goal + in + let resleft = demodulation_aux menv context ugraph table 0 left in + match resleft with + | Some t -> + let newg = build_newgoal context goal Utils.Right Equality.Demodulation t in + if goal_metaconvertibility_eq goal newg then + do_right () + else + true, snd (demodulation_goal env table newg) + | None -> do_right () +;; + +let get_stats () = "" ;;