X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Findexing.ml;h=a2e6eda07443be5d7e644136861f7520e14d3121;hb=33f9ff7f9693a77f194112291bd149e7c0d80e71;hp=fd3caa345963398b86ef482ef920e57164f39e12;hpb=d446e47c39af1ae40a3072c188c81a978e95804c;p=helm.git diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml index fd3caa345..a2e6eda07 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +let _profiler = <:profiler<_profiler>>;; + (* $Id$ *) type goal = Equality.goal_proof * Cic.metasenv * Cic.term @@ -32,8 +34,6 @@ 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;; (* @@ -92,9 +92,6 @@ let print_candidates ?env mode term res = ;; -let indexing_retrieval_time = ref 0.;; - - let apply_subst = Subst.apply_subst let index = Index.index @@ -156,7 +153,7 @@ let check_target context target msg = (* try ignore(CicTypeChecker.type_of_aux' - metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph) + metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph) with e -> prerr_endline msg; prerr_endline (Inference.string_of_proof proof); @@ -182,32 +179,14 @@ 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 @@ -242,8 +221,9 @@ let rec find_matches metasenv context ugraph lift_amount term termty = | [] -> None | candidate::tl -> let pos, equality = candidate in - let (_, proof, (ty, left, right, o), metas,_) = - Equality.open_equality equality in + let (_, proof, (ty, left, right, o), metas,_) = + Equality.open_equality equality + in if Utils.debug_metas then ignore(check_target context (snd candidate) "find_matches"); if Utils.debug_res then @@ -251,11 +231,13 @@ 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 ( @@ -263,23 +245,10 @@ let rec find_matches metasenv context ugraph lift_amount term termty = ) else let do_match c eq_URI = 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 (C.Rel (1 + lift_amount), subst', metasenv', ugraph', + Some (Cic.Rel (1 + lift_amount), subst', metasenv', ugraph', (candidate, eq_URI)) in let c, other, eq_URI = @@ -317,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 @@ -333,27 +306,12 @@ 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 (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in let do_match c eq_URI = let subst', metasenv', ugraph' = - let t1 = Unix.gettimeofday () in - try - 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, eq_URI)) in let c, other, eq_URI = if pos = Utils.Left then left, right, Utils.eq_ind_URI () @@ -395,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 @@ -430,27 +386,15 @@ 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 | [] -> None | (_, 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 subst', menv', ug' = - let t1 = Unix.gettimeofday () in - try - let other = Subst.apply_subst subst other in - let r = unif_fun metasenv m context what other ugraph in - let t2 = Unix.gettimeofday () in - match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1); - r - with - | Inference.MatchingFailure - | CicUnification.UnificationFailure _ as e -> - let t2 = Unix.gettimeofday () in - match_unif_time_no := !match_unif_time_no +. (t2 -. t1); - raise e + unif_fun metasenv m context what' other ugraph in (match Subst.merge_subst_if_possible subst subst' with | None -> ok what tl @@ -470,34 +414,28 @@ 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)))); *) ;; -let subsumption = subsumption_aux false;; -let unification = subsumption_aux true;; +let subsumption x y z = + subsumption_aux false x y z +;; + +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 = - (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *) +(* Printf.eprintf "term = %s\n" (CicPp.ppterm 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 ~env:(metasenv,context,ugraph) (* Unification *) Matching table term in - if List.exists (fun (i,_,_) -> i = 2840) metasenv - then - (prerr_endline ("term: " ^(CicPp.ppterm term)); - List.iter (fun (_,x) -> prerr_endline (Equality.string_of_equality x)) - candidates; - prerr_endline ("-------"); - prerr_endline ("+++++++")); + get_candidates + ~env:(metasenv,context,ugraph) (* Unification *) Matching table term + in let res = match term with | C.Meta _ -> None @@ -586,16 +524,8 @@ 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 module C = Cic in @@ -620,7 +550,6 @@ let rec demodulation_equality ?from newmeta env table sign target = let maxmeta = ref newmeta in let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) = - let time1 = Unix.gettimeofday () in if Utils.debug_metas then begin @@ -642,7 +571,6 @@ 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, []); @@ -654,7 +582,7 @@ let rec demodulation_equality ?from newmeta env table sign target = else assert false (* - begin + begin prerr_endline "***************************************negative"; let metaproof = incr maxmeta; @@ -684,7 +612,7 @@ let rec demodulation_equality ?from newmeta env table sign target = let target_proof = let pb = Equality.ProofBlock - (subst, eq_URI, (name, ty), bo', + (subst, eq_URI, (name, ty), bo', eq_found, Equality.BasicProof (Equality.empty_subst,metaproof)) in assert false, (* not implemented *) @@ -710,6 +638,7 @@ let rec demodulation_equality ?from newmeta env table sign target = *) in let newmenv = (* Inference.filter subst *) menv in +(* let _ = if Utils.debug_metas then try ignore(CicTypeChecker.type_of_aux' @@ -730,22 +659,18 @@ let rec demodulation_equality ?from newmeta env table sign target = raise exc; else () 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"; @@ -753,7 +678,7 @@ let rec demodulation_equality ?from newmeta env table sign target = match res with | Some t -> let newmeta, newtarget = build_newtarget true t in - assert (not (Equality.meta_convertibility_eq target newtarget)); + assert (not (Equality.meta_convertibility_eq target newtarget)); if (Equality.is_weak_identity newtarget) || (Equality.meta_convertibility_eq target newtarget) then newmeta, newtarget @@ -782,12 +707,13 @@ 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 @@ -895,87 +821,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 build_newgoal context goalproof (t, subst, menv, ug, (eq_found, eq_URI)) = - 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) - | _ -> assert false - in - let small = CicSubstitution.lift 1 small in - let ty = CicSubstitution.lift 1 ty in - let expansions, _ = betaexpand_term menv context ugraph table 0 big in - let fix_preds (t, subst, menv, ug, (eq_found, eq_URI)) = - let pred = - match pos with - | Utils.Left -> - Cic.Appl [eq;ty;small;t] - | Utils.Right -> - Cic.Appl [eq;ty;t;small] - in - (pred, subst, menv, ug, (eq_found, eq_URI)) - in - List.map (build_newgoal context proof) - (List.map fix_preds expansions) -;; - -let sup_r_counter = ref 1;; - (** superposition_right returns a list of new clauses inferred with a right superposition step @@ -983,7 +839,9 @@ 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) newmeta (metasenv, context, ugraph) table target += let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -998,16 +856,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), [] - | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right) + | U.Gt -> + fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), [] + | U.Lt -> + [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right) | _ -> let res l r = List.filter @@ -1015,26 +868,25 @@ 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)) = 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') = Equality.open_equality equality in let what, other = if pos = Utils.Left then what, other else other, what in + let newgoal, newproof = (* qua *) let bo' = 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 @@ -1064,8 +916,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 @@ -1077,62 +927,6 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = (List.filter ok (new1 @ new2))) ;; - -(** demodulation, when the target is a goal *) -let rec demodulation_goal newmeta env table goal = - let module C = Cic in - let module S = CicSubstitution in - let module M = CicMetaSubst in - let module HL = HelmLibraryObjects in - let metasenv, context, ugraph = env in - let maxmeta = ref newmeta 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 build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) = - 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 ty = - try fst (CicTypeChecker.type_of_aux' menv' context what ugraph) - with - | CicUtil.Meta_not_found _ - | Invalid_argument("List.fold_left2") -> ty - in - let newterm, newgoalproof = - 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" in - incr demod_counter; - let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in - bo, (newgoalproofstep::goalproof) - in - let newmetasenv = (* Inference.filter subst *) menv in - !maxmeta, (newgoalproof, newmetasenv, newterm) - in - let res = - demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term - in - match res with - | Some t -> - let newmeta, newgoal = build_newgoal t in - let _, _, newg = newgoal in - if Equality.meta_convertibility term newg then - false, newmeta, newgoal - else - let changed, newmeta, newgoal = - demodulation_goal newmeta env table newgoal - in - true, newmeta, newgoal - | None -> - false, newmeta, goal -;; - (** demodulation, when the target is a theorem *) let rec demodulation_theorem newmeta env table theorem = let module C = Cic in @@ -1153,7 +947,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, @@ -1181,3 +974,111 @@ 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 expansion = + let goalproof,_,_,_,_,_ = open_goal goal in + let (t,subst,menv,ug,(eq_found,eq_URI)) = 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 = (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 = + let proof,menv,eq,ty,l,r = open_goal goal in + let c = + Utils.compare_weights ~normalize:true + (Utils.weight_of_term l) (Utils.weight_of_term r) + in + let big,small,possmall = + match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left + in + let expansions, _ = betaexpand_term menv context ugraph table 0 big in + List.map (build_newgoal context goal possmall) expansions +;; + +(** demodulation, when the target is a goal *) +let rec demodulation_goal env table goal = + let goalproof,menv,_,_,left,right = open_goal goal in + let metasenv, 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 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 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 () = <:show> ;;