X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2Fparamodulation%2Findexing.ml;h=d35fbff34ee0f36f96236369d9b05eba7f78f5a2;hb=0c2abc0eb74a5387469375a4a5897265633be340;hp=b4cf802d0624e4cee3014393be32f1d7b82d6e28;hpb=801f0eb3eabe1cbcd66d6a3f52c24eb8f1189611;p=helm.git diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml index b4cf802d0..d35fbff34 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -25,6 +25,8 @@ (* $Id$ *) +type goal = Equality.goal_proof * Cic.metasenv * Cic.term + module Index = Equality_indexing.DT (* discrimination tree based indexing *) (* module Index = Equality_indexing.DT (* path tree based indexing *) @@ -62,7 +64,7 @@ let string_of_res ?env = | Some (t, s, m, u, ((p,e), eq_URI)) -> Printf.sprintf "Some: (%s, %s, %s)" (Utils.string_of_pos p) - (Inference.string_of_equality ?env e) + (Equality.string_of_equality ?env e) (CicPp.ppterm t) ;; @@ -85,7 +87,7 @@ let print_candidates ?env mode term res = (List.map (fun (p, e) -> Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p) - (Inference.string_of_equality ?env e)) + (Equality.string_of_equality ?env e)) res)); ;; @@ -93,7 +95,7 @@ let print_candidates ?env mode term res = let indexing_retrieval_time = ref 0.;; -let apply_subst = CicMetaSubst.apply_subst +let apply_subst = Subst.apply_subst let index = Index.index let remove_index = Index.remove_index @@ -103,7 +105,7 @@ let init_index = Index.init_index let check_disjoint_invariant subst metasenv msg = if (List.exists - (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv) + (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv) then begin prerr_endline ("not disjoint: " ^ msg); @@ -124,19 +126,20 @@ let check_for_duplicates metas msg = let check_res res msg = match res with Some (t, subst, menv, ug, (eq_found, eq_URI)) -> - let eqs = Inference.string_of_equality (snd eq_found) in + let eqs = Equality.string_of_equality (snd eq_found) in check_disjoint_invariant subst menv msg; check_for_duplicates menv (msg ^ "\nchecking " ^ eqs); | None -> () ;; let check_target context target msg = - let w, proof, (eq_ty, left, right, order), metas = target in + let w, proof, (eq_ty, left, right, order), metas,_ = + Equality.open_equality target in (* check that metas does not contains duplicates *) - let eqs = Inference.string_of_equality target in + let eqs = Equality.string_of_equality target in let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in - let actual = (Inference.metas_of_term left)@(Inference.metas_of_term right) - @(Inference.metas_of_term eq_ty)@(Inference.metas_of_proof proof) in + let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right) + @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof proof) in let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in let _ = if menv <> metas then begin @@ -148,19 +151,20 @@ let check_target context target msg = prerr_endline ("right: " ^ (CicPp.ppterm right)); prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty)); assert false - end - else () in + end + else () in () +(* try - CicTypeChecker.type_of_aux' - metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph + ignore(CicTypeChecker.type_of_aux' + metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph) with e -> prerr_endline msg; prerr_endline (Inference.string_of_proof proof); prerr_endline (CicPp.ppterm (Inference.build_proof_term proof)); prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left)); prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right)); - raise e -;; + raise e +*) (* returns a list of all the equalities in the tree that are in relation @@ -176,13 +180,6 @@ let check_target context target msg = the position will always be Left, and if the ordering is left < right, position will be Right. *) -let local_max = ref 100;; - -let make_variant (p,eq) = - let maxmeta, eq = Inference.fix_metas !local_max eq in - local_max := maxmeta; - p, eq -;; let get_candidates ?env mode tree term = let t1 = Unix.gettimeofday () in @@ -244,17 +241,22 @@ let rec find_matches metasenv context ugraph lift_amount term termty = function | [] -> None | candidate::tl -> - let pos, (_, proof, (ty, left, right, o), metas) = candidate in + let pos, equality = candidate 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 begin - let c = "eq = " ^ (Inference.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 (Inference.build_proof_term proof)) ^ "\n" in + 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 ( @@ -278,7 +280,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty = raise e | CicUtil.Meta_not_found _ as exn -> raise exn 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 = @@ -331,11 +333,24 @@ let rec find_all_matches ?(unif_fun=Inference.unification) function | [] -> [] | candidate::tl -> - let pos, (_, _, (ty, left, right, o), metas) = candidate in + let pos, equality = candidate 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 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 @@ -406,90 +421,80 @@ let find_all_matches (* returns true if target is subsumed by some equality in table *) -let subsumption env table target = - let _, _, (ty, left, right, _), tmetas = target in +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 = metasenv @ tmetas in - let samesubst subst subst' = - let tbl = Hashtbl.create (List.length subst) in - List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst; - List.for_all - (fun (m, (c, t1, t2)) -> - try - let c', t1', t2' = Hashtbl.find tbl m in - if (c = c') && (t1 = t1') && (t2 = t2') then true - else false - with Not_found -> - true) - subst' + let metasenv = tmetas in + let predicate, unif_fun = + if use_unification then + Unification, Inference.unification + else + Matching, Inference.matching in let leftr = match left with - | Cic.Meta _ -> [] + | Cic.Meta _ when not use_unification -> [] | _ -> - let leftc = get_candidates Matching table left in - find_all_matches ~unif_fun:Inference.matching + let leftc = get_candidates predicate table left in + find_all_matches ~unif_fun metasenv context ugraph 0 left ty leftc in +(* print_res leftr;*) let rec ok what = function - | [] -> false, [] - | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m)), _))::tl -> + | [] -> 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 r = - Inference.matching menv 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 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 - if samesubst subst subst' then - true, subst - else - ok what tl - with Inference.MatchingFailure -> - ok what tl + (match Subst.merge_subst_if_possible subst subst' with + | None -> ok what tl + | Some s -> Some (s, equation)) + with + | Inference.MatchingFailure + | CicUnification.UnificationFailure _ -> ok what tl in - let r, subst = ok right leftr in - let r, s = - if r then - true, subst - else + match ok right leftr with + | Some _ as res -> res + | None -> let rightr = match right with - | Cic.Meta _ -> [] + | Cic.Meta _ when not use_unification -> [] | _ -> - let rightc = get_candidates Matching table right in - find_all_matches ~unif_fun:Inference.matching + let rightc = get_candidates predicate table right in + find_all_matches ~unif_fun metasenv context ugraph 0 right ty rightc in +(* print_res rightr;*) ok left rightr - in (* (if r then *) (* debug_print *) (* (lazy *) (* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *) (* (Inference.string_of_equality target) (Utils.print_subst s)))); *) - r, s ;; +let subsumption = subsumption_aux false;; +let unification = subsumption_aux true;; + 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) Matching table term in -(* let candidates = List.map make_variant candidates in *) + get_candidates + ~env:(metasenv,context,ugraph) (* Unification *) Matching table term + in let res = match term with | C.Meta _ -> None @@ -596,14 +601,16 @@ let rec demodulation_equality ?from newmeta env table sign target = let module HL = HelmLibraryObjects in let module U = Utils in let metasenv, context, ugraph = env in - let w, proof, (eq_ty, left, right, order), metas = target in + let w, proof, (eq_ty, left, right, order), metas, id = + Equality.open_equality target + in (* first, we simplify *) - let right = U.guarded_simpl context right in - let left = U.guarded_simpl context left in - let order = !Utils.compare_terms left right in - let stat = (eq_ty, left, right, order) in - let w = Utils.compute_equality_weight stat in - let target = w, proof, stat, metas in +(* let right = U.guarded_simpl context right in *) +(* let left = U.guarded_simpl context left in *) +(* let order = !Utils.compare_terms left right in *) +(* let stat = (eq_ty, left, right, order) in *) +(* let w = Utils.compute_equality_weight stat in*) + (* let target = Equality.mk_equality (w, proof, stat, metas) in *) if Utils.debug_metas then ignore(check_target context target "demod equalities input"); let metasenv' = (* metasenv @ *) metas in @@ -616,18 +623,22 @@ let rec demodulation_equality ?from newmeta env table sign target = begin ignore(check_for_duplicates menv "input1"); ignore(check_disjoint_invariant subst menv "input2"); - let substs = CicMetaSubst.ppsubst subst in + let substs = Subst.ppsubst subst in ignore(check_target context (snd eq_found) ("input3" ^ substs)) end; - let pos, (_, proof', (ty, what, other, _), menv') = eq_found in + let pos, equality = eq_found in + let (_, proof', + (ty, what, other, _), menv',id') = Equality.open_equality equality in let ty = - try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph) + try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph) with CicUtil.Meta_not_found _ -> ty in let what, other = if pos = Utils.Left then what, other else other, what in let newterm, newproof = - let bo = 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 bo = + 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 @@ -635,45 +646,53 @@ let rec demodulation_equality ?from newmeta env table sign target = S.lift 1 eq_ty; l; r] in if sign = Utils.Positive then - (bo, - Inference.ProofBlock ( - subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof)) + (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 (); *) +(* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *) +(* print_newline (); *) C.Meta (!maxmeta, irl) in let eq_found = - let proof' = + let proof'_old' = let termlist = if pos = Utils.Left then [ty; what; other] else [ty; other; what] in - Inference.ProofSymBlock (termlist, proof') + 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, (0, proof', (ty, other, what, Utils.Incomparable),menv') + pos, + Equality.mk_equality + (0, (proof'_new',proof'_old'), + (ty, other, what, Utils.Incomparable),menv') in let target_proof = let pb = - Inference.ProofBlock (subst, eq_URI, (name, ty), bo', - eq_found, Inference.BasicProof metaproof) + Equality.ProofBlock + (subst, eq_URI, (name, ty), bo', + eq_found, Equality.BasicProof (Equality.empty_subst,metaproof)) in - match proof with - | Inference.BasicProof _ -> + assert false, (* not implemented *) + (match snd proof with + | Equality.BasicProof _ -> (* print_endline "replacing a BasicProof"; *) pb - | Inference.ProofGoalBlock (_, parent_proof) -> - + | Equality.ProofGoalBlock (_, parent_proof) -> (* print_endline "replacing another ProofGoalBlock"; *) - Inference.ProofGoalBlock (pb, parent_proof) - | _ -> assert false + Equality.ProofGoalBlock (pb, parent_proof) + | _ -> assert false) in let refl = C.Appl [C.MutConstruct (* reflexivity *) @@ -681,22 +700,30 @@ let rec demodulation_equality ?from newmeta env table sign target = eq_ty; if is_left then right else left] in (bo, - Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof)) + (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 (Inference.build_proof_term newproof) ugraph); + newmenv context + (Equality.build_proof_term newproof) ugraph); () with exc -> prerr_endline "sempre lui"; - prerr_endline (CicMetaSubst.ppsubst subst); - prerr_endline (CicPp.ppterm (Inference.build_proof_term newproof)); + 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: " ^ (CicMetaSubst.ppsubst subst)); + prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst)); + prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv [] + newmenv)); raise exc; else () in @@ -707,7 +734,8 @@ let rec demodulation_equality ?from newmeta env table sign target = build_newtarget_time := !build_newtarget_time +. (time2 -. time1); let res = let w = Utils.compute_equality_weight stat in - (w, newproof, stat,newmenv) in + Equality.mk_equality (w, newproof, stat,newmenv) + in if Utils.debug_metas then ignore(check_target context res "buildnew_target output"); !maxmeta, res @@ -722,22 +750,23 @@ let rec demodulation_equality ?from newmeta env table sign target = match res with | Some t -> let newmeta, newtarget = build_newtarget true t in - if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) || - (Inference.meta_convertibility_eq target newtarget) then + assert (not (Equality.meta_convertibility_eq target newtarget)); + if (Equality.is_weak_identity newtarget) || + (Equality.meta_convertibility_eq target newtarget) then newmeta, newtarget else - demodulation_equality newmeta env table sign newtarget + demodulation_equality ?from newmeta env table sign newtarget | None -> let res = demodulation_aux metasenv' context ugraph table 0 right in if Utils.debug_res then check_res res "demod result 1"; match res with | Some t -> let newmeta, newtarget = build_newtarget false t in - if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) || - (Inference.meta_convertibility_eq target newtarget) then + if (Equality.is_weak_identity newtarget) || + (Equality.meta_convertibility_eq target newtarget) then newmeta, newtarget else - demodulation_equality newmeta env table sign newtarget + demodulation_equality ?from newmeta env table sign newtarget | None -> newmeta, target in @@ -884,100 +913,65 @@ let sup_l_counter = ref 1;; 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 newmeta (metasenv, context, ugraph) table target = +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 weight, proof, (eq_ty, left, right, ordering), menv = target in - if Utils.debug_metas then - ignore(check_target context target "superpositionleft"); - let expansions, _ = - let term = if ordering = U.Gt then left else right in - begin - let t1 = Unix.gettimeofday () in - let res = betaexpand_term metasenv context ugraph table 0 term in - let t2 = Unix.gettimeofday () in - beta_expand_time := !beta_expand_time +. (t2 -. t1); - res - end - in - let maxmeta = ref newmeta in - let build_new (bo, s, m, ug, (eq_found, eq_URI)) = -(* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *) - let time1 = Unix.gettimeofday () in - - let pos, (_, proof', (ty, what, other, _), menv') = eq_found in - let what, other = if pos = Utils.Left then what, other else other, what in - let newgoal, newproof = - let bo' = U.guarded_simpl context (apply_subst s (S.subst other bo)) in - let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in - incr sup_l_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] - in - incr maxmeta; - let metaproof = - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context in - C.Meta (!maxmeta, irl) - in - let eq_found = - let proof' = - let termlist = - if pos = Utils.Left then [ty; what; other] - else [ty; other; what] - in - Inference.ProofSymBlock (termlist, 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') - in - let target_proof = - let pb = - Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, - Inference.BasicProof metaproof) - in - match proof with - | Inference.BasicProof _ -> -(* debug_print (lazy "replacing a BasicProof"); *) - pb - | Inference.ProofGoalBlock (_, parent_proof) -> -(* debug_print (lazy "replacing another ProofGoalBlock"); *) - Inference.ProofGoalBlock (pb, parent_proof) - | _ -> assert false - in - let refl = - C.Appl [C.MutConstruct (* reflexivity *) - (LibraryObjects.eq_URI (), 0, 1, []); - eq_ty; if ordering = U.Gt then right else left] - in - (bo', - Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof)) - in - let left, right = - if ordering = U.Gt then newgoal, right else left, newgoal in - let neworder = !Utils.compare_terms left right in - let stat = (eq_ty, left, right, neworder) in - let newmenv = (* Inference.filter s *) menv in - let time2 = Unix.gettimeofday () in - build_newtarget_time := !build_newtarget_time +. (time2 -. time1); - - let w = Utils.compute_equality_weight stat in - (w, newproof, stat, newmenv) - + 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 - !maxmeta, List.map build_new expansions + 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;; (** @@ -994,7 +988,9 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = let module HL = HelmLibraryObjects in let module CR = CicReduction in let module U = Utils in - let w, eqproof, (eq_ty, left, right, ordering), newmetas = target in + let w, eqproof, (eq_ty, left, right, ordering), newmetas,id = + Equality.open_equality target + in if Utils.debug_metas then ignore (check_target context target "superpositionright"); let metasenv' = newmetas in @@ -1008,8 +1004,10 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = 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 metasenv' context ugraph table 0 left), [] + | U.Lt -> + [], fst (betaexpand_term metasenv' context ugraph table 0 right) | _ -> let res l r = List.filter @@ -1026,12 +1024,17 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = ignore (check_target context (snd eq_found) "buildnew1" ); let time1 = Unix.gettimeofday () in - let pos, (_, proof', (ty, what, other, _), menv') = eq_found 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_SupR_" ^ (string_of_int !sup_r_counter)) in + 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 = @@ -1040,7 +1043,9 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = S.lift 1 eq_ty; l; r] in bo', - Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof) + Equality.Step + (s,(Equality.SuperpositionRight, + id,(pos,id'),(Cic.Lambda(name,ty,bo'')))) in let newmeta, newequality = let left, right = @@ -1051,10 +1056,10 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = let stat = (eq_ty, left, right, neworder) in let eq' = let w = Utils.compute_equality_weight stat in - (w, newproof, stat, newmenv) in + Equality.mk_equality (w, newproof, stat, newmenv) in if Utils.debug_metas then ignore (check_target context eq' "buildnew3"); - let newm, eq' = Inference.fix_metas !maxmeta eq' in + let newm, eq' = Equality.fix_metas !maxmeta eq' in if Utils.debug_metas then ignore (check_target context eq' "buildnew4"); newm, eq' @@ -1068,95 +1073,50 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = in let new1 = List.map (build_new U.Gt) res1 and new2 = List.map (build_new U.Lt) res2 in - let ok e = not (Inference.is_identity (metasenv', context, ugraph) e) in + let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in (!maxmeta, (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 goal_metaconvertibility_eq (_,_,g1) (_,_,g2) = + Equality.meta_convertibility g1 g2 +;; + +let rec demodulation_goal env table goal = let metasenv, context, ugraph = env in - let maxmeta = ref newmeta in - let proof, metas, term = goal in + let goalproof, metas, term = goal in let term = Utils.guarded_simpl (~debug:true) context term in - let goal = proof, metas, 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, (_, proof', (ty, what, other, _), menv') = eq_found in - let what, other = if pos = Utils.Left then what, other else other, what in - let ty = - try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph) - with CicUtil.Meta_not_found _ -> ty - in - let newterm, newproof = - 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_DemodGoal_" ^ (string_of_int !demod_counter)) in - incr demod_counter; - let metaproof = - incr maxmeta; - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context in -(* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *) - C.Meta (!maxmeta, irl) - in - let eq_found = - let proof' = - let termlist = - if pos = Utils.Left then [ty; what; other] - else [ty; other; what] - in - Inference.ProofSymBlock (termlist, 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') - in - let goal_proof = - let pb = - Inference.ProofBlock (subst, eq_URI, (name, ty), bo', - eq_found, Inference.BasicProof metaproof) - in - let rec repl = function - | Inference.NoProof -> -(* debug_print (lazy "replacing a NoProof"); *) - pb - | Inference.BasicProof _ -> -(* debug_print (lazy "replacing a BasicProof"); *) - pb - | Inference.ProofGoalBlock (_, parent_proof) -> -(* debug_print (lazy "replacing another ProofGoalBlock"); *) - Inference.ProofGoalBlock (pb, parent_proof) - | Inference.SubProof (term, meta_index, p) -> - Inference.SubProof (term, meta_index, repl p) - | _ -> assert false - in repl proof - in - bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof) - in - let newmetasenv = (* Inference.filter subst *) menv in - !maxmeta, (newproof, newmetasenv, newterm) - in - let res = - demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term + let left,right,eq,ty = + match term with + | Cic.Appl [eq;ty;l;r] -> l,r,eq,ty + | _ -> assert false in - match res with + 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 newmeta, newgoal = build_newgoal t in - let _, _, newg = newgoal in - if Inference.meta_convertibility term newg then - newmeta, newgoal + let newg = build_newgoal context goalproof (eq,ty,right,Utils.Right) t in + if goal_metaconvertibility_eq goal newg then + do_right () else - demodulation_goal newmeta env table newgoal - | None -> - newmeta, goal + true, snd (demodulation_goal env table newg) + | None -> do_right () ;; (** demodulation, when the target is a theorem *) @@ -1171,21 +1131,25 @@ let rec demodulation_theorem newmeta env table theorem = let metasenv' = metas in let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) = - let pos, (_, proof', (ty, what, other, _), menv') = eq_found 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, newty = 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 +(* let bo' = apply_subst subst t in *) +(* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*) incr demod_counter; - let newproof = - Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found, - Inference.BasicProof term) +(* + let newproofold = + Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found, + Equality.BasicProof (Equality.empty_subst,term)) in - (Inference.build_proof_term newproof, bo) + (Equality.build_proof_term_old newproofold, bo) +*) + (* TODO, not ported to the new proofs *) + if true then assert false; term, bo in - - (* let m = Inference.metas_of_term newterm in *) !maxmeta, (newterm, newty, menv) in let res = @@ -1195,7 +1159,7 @@ let rec demodulation_theorem newmeta env table theorem = | Some t -> let newmeta, newthm = build_newtheorem t in let newt, newty, _ = newthm in - if Inference.meta_convertibility termty newty then + if Equality.meta_convertibility termty newty then newmeta, newthm else demodulation_theorem newmeta env table newthm