X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=8f696d6f3e330b960c0d3782c62f2d3720f46ece;hb=abb7b4623d6c2eb93f289c44fe46f45faa7e3374;hp=e6a2463c099a8a084e4ac83e42497eac382e3653;hpb=b1ec882fae6023000ff6076e0a45f9809a6210e4;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index e6a2463c0..8f696d6f3 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* let _profiler = <:profiler<_profiler>>;; *) + (* $Id$ *) module Index = Equality_indexing.DT (* discrimination tree based indexing *) @@ -30,8 +32,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;; (* @@ -59,10 +59,10 @@ 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) - (Inference.string_of_equality ?env e) + (Equality.string_of_equality ?env e) (CicPp.ppterm t) ;; @@ -85,15 +85,12 @@ 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)); ;; -let indexing_retrieval_time = ref 0.;; - - -let apply_subst = Inference.apply_subst +let apply_subst = Subst.apply_subst let index = Index.index let remove_index = Index.remove_index @@ -103,7 +100,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); @@ -112,31 +109,86 @@ let check_disjoint_invariant subst metasenv msg = ;; let check_for_duplicates metas msg = - if List.length metas <> - List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then - begin + let rec aux = function + | [] -> true + | (m,_,_)::tl -> not (List.exists (fun (i, _, _) -> i = m) tl) && aux tl in + let b = aux metas in + if not b then + begin prerr_endline ("DUPLICATI " ^ msg); prerr_endline (CicMetaSubst.ppmetasenv [] metas); assert false - end + end + else () +;; + +let check_metasenv msg menv = + List.iter + (fun (i,ctx,ty) -> + try ignore(CicTypeChecker.type_of_aux' menv ctx ty + CicUniv.empty_ugraph) + with + | CicUtil.Meta_not_found _ -> + prerr_endline (msg ^ CicMetaSubst.ppmetasenv [] menv); + assert false + | _ -> () + ) menv +;; + +(* the metasenv returned by res must included in the original one, +due to matching. If it fails, it is probably because we are not +demodulating with a unit equality *) + +let not_unit_eq ctx eq = + let (_,_,(ty,left,right,o),metas,_) = Equality.open_equality eq in + let b = + List.exists + (fun (_,_,ty) -> + try + let s,_ = CicTypeChecker.type_of_aux' metas ctx ty CicUniv.empty_ugraph + in s = Cic.Sort(Cic.Prop) + with _ -> + prerr_endline ("ERROR typing " ^ CicPp.ppterm ty); assert false) metas + in b +(* +if b then prerr_endline ("not a unit equality: " ^ Equality.string_of_equality eq); b *) +;; + +let check_demod_res res metasenv msg = + match res with + | Some (_, _, menv, _, _) -> + let b = + List.for_all + (fun (i,_,_) -> + (List.exists (fun (j,_,_) -> i=j) metasenv)) menv + in + if (not b) then + begin + prerr_endline ("extended context " ^ msg); + prerr_endline (CicMetaSubst.ppmetasenv [] menv); + end; + b + | None -> false ;; 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 + | Some (t, subst, menv, ug, eq_found) -> + let eqs = Equality.string_of_equality (snd eq_found) in + check_metasenv msg menv; 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 check_target bag context target msg = + 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 bag proof) in let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in let _ = if menv <> metas then begin @@ -153,11 +205,11 @@ let check_target context target msg = (* try ignore(CicTypeChecker.type_of_aux' - metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph) + metas context (Founif.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 (Founif.string_of_proof proof); + prerr_endline (CicPp.ppterm (Founif.build_proof_term proof)); prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left)); prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right)); raise e @@ -177,41 +229,19 @@ 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 - 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 @@ -234,7 +264,7 @@ let match_unif_time_no = ref 0.;; the build_newtarget functions] )) *) -let rec find_matches metasenv context ugraph lift_amount term termty = +let rec find_matches bag metasenv context ugraph lift_amount term termty = let module C = Cic in let module U = Utils in let module S = CicSubstitution in @@ -245,62 +275,66 @@ 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 + (* if not_unit_eq context equality then + begin + prerr_endline "not a unit"; + prerr_endline (Equality.string_of_equality equality) + end; *) + 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"); + ignore(check_target bag 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 ms="metasenv =" ^ (CicMetaSubst.ppmetasenv [] metasenv) ^ "\n" in + let eq_uri = + match LibraryObjects.eq_URI () with + | Some (uri) -> uri + | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in + let p="proof = "^ + (CicPp.ppterm(Equality.build_proof_term bag eq_uri [] 0 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 "gia nel metasenv"; + check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^ms^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 + find_matches bag 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 + Founif.matching + metasenv metas context term (S.lift lift_amount c) ugraph in - Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph', - (candidate, eq_URI)) + check_metasenv "founif :" metasenv'; + 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 - with Inference.MatchingFailure -> - find_matches metasenv context ugraph lift_amount term termty tl + do_match c + with Founif.MatchingFailure -> + find_matches bag metasenv context ugraph lift_amount term termty tl in if Utils.debug_res then ignore (check_res res "find1"); res else let res = - try do_match c eq_URI - with Inference.MatchingFailure -> None + try do_match c + with Founif.MatchingFailure -> None in - if Utils.debug_res then ignore (check_res res "find2"); + if Utils.debug_res then ignore (check_res res "find2"); match res with | Some (_, s, _, _, _) -> let c' = apply_subst s c in @@ -311,17 +345,22 @@ let rec find_matches metasenv context ugraph lift_amount term termty = if order = U.Gt then res else - find_matches + find_matches bag metasenv context ugraph lift_amount term termty tl | None -> - find_matches metasenv context ugraph lift_amount term termty tl + find_matches bag 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 + can be either Founif.matching or Inference.unification *) -let rec find_all_matches ?(unif_fun=Inference.unification) +(* XXX termty unused *) +let rec find_all_matches ?(unif_fun=Founif.unification) metasenv context ugraph lift_amount term termty = let module C = Cic in let module U = Utils in @@ -329,49 +368,41 @@ let rec find_all_matches ?(unif_fun=Inference.unification) let module M = CicMetaSubst in let module HL = HelmLibraryObjects in let cmp = !Utils.compare_terms in + let check = match termty with C.Implicit None -> false | _ -> true in function | [] -> [] | candidate::tl -> - let pos, (_, _, (ty, left, right, o), metas) = candidate in - let do_match c eq_URI = + let pos, equality = candidate in + let (_,_,(ty,left,right,o),metas,_)= Equality.open_equality equality in + if check && not (fst (CicReduction.are_convertible + ~metasenv context termty ty ugraph)) then ( + find_all_matches metasenv context ugraph lift_amount term termty tl + ) else + let do_match c = 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) 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 - | Inference.MatchingFailure + | Founif.MatchingFailure | CicUnification.UnificationFailure _ | CicUnification.Uncertain _ -> find_all_matches ~unif_fun metasenv context ugraph 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 @@ -384,7 +415,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification) find_all_matches ~unif_fun metasenv context ugraph lift_amount term termty tl with - | Inference.MatchingFailure + | Founif.MatchingFailure | CicUnification.UnificationFailure _ | CicUnification.Uncertain _ -> find_all_matches ~unif_fun metasenv context ugraph @@ -394,126 +425,178 @@ 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; + List.iter (fun (_,x)->prerr_endline (Founif.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 subsumption env table target = - let _, _, (ty, left, right, _), tmetas = target in - let metasenv, context, ugraph = env in +(* +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 _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in + let _, context, ugraph = env in let metasenv = tmetas in - let merge_if_possible s1 s2 = - let already_in = Hashtbl.create 13 in - let rec aux acc = function - | ((i,x) as s)::tl -> - (try - let x' = Hashtbl.find already_in i in - if x = x' then aux acc tl else None - with - | Not_found -> - Hashtbl.add already_in i x; - aux (s::acc) tl) - | [] -> Some acc - in - aux [] (s1@s2) + let predicate, unif_fun = + if use_unification then + Unification, Founif.unification + else + Matching, Founif.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 - let rec ok what = function - | [] -> false, [] - | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m)), _))::tl -> + let rec ok what leftorright = 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 other' = Subst.apply_subst subst other in let subst', menv', ug' = - let t1 = Unix.gettimeofday () in - try - let r = - Inference.matching metasenv menv 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 - (match merge_if_possible subst subst' with - | None -> ok what tl - | Some s -> true, s) - with Inference.MatchingFailure -> - ok what tl + (match Subst.merge_subst_if_possible subst subst' with + | None -> ok what leftorright tl + | Some s -> Some (s, equation, leftorright <> pos )) + with + | Founif.MatchingFailure + | CicUnification.UnificationFailure _ -> ok what leftorright tl in - let r, subst = ok right leftr in - let r, s = - if r then - true, subst - else + match ok right Utils.Left 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 - ok left rightr + ok left Utils.Right rightr +;; + +let subsumption x y z = + subsumption_aux false x y z +;; + +let unification x y z = + subsumption_aux true x y z +;; + +(* the target must be disjoint from the equations in the table *) +let subsumption_aux_all use_unification env table target = + let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in + let _, context, ugraph = env in + let metasenv = tmetas in + check_for_duplicates metasenv "subsumption_aux_all"; + let predicate, unif_fun = + if use_unification then + Unification, Founif.unification + else + Matching, Founif.matching 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 leftr = + match left with + | Cic.Meta _ (*when not use_unification*) -> [] + | _ -> + let leftc = get_candidates predicate table left in + find_all_matches ~unif_fun + metasenv context ugraph 0 left ty leftc + in + let rightr = + match right with + | Cic.Meta _ (*when not use_unification*) -> [] + | _ -> + let rightc = get_candidates predicate table right in + find_all_matches ~unif_fun + metasenv context ugraph 0 right ty rightc + in + let rec ok_all what leftorright = function + | [] -> [] + | (_, 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 + in + (match Subst.merge_subst_if_possible subst subst' with + | None -> ok_all what leftorright tl + | Some s -> + (s, equation, leftorright <> pos )::(ok_all what leftorright tl)) + with + | Founif.MatchingFailure + | CicUnification.UnificationFailure _ -> (ok_all what leftorright tl) + in + (ok_all right Utils.Left leftr)@(ok_all left Utils.Right rightr ) +;; + +let subsumption_all x y z = + subsumption_aux_all false x y z +;; + +let unification_all x y z = + subsumption_aux_all true x y z ;; -let rec demodulation_aux ?from ?(typecheck=false) +let rec demodulation_aux bag ?from ?(typecheck=false) metasenv context ugraph table lift_amount term = - (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *) let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in + (* prerr_endline ("demodulating " ^ CicPp.ppterm term); *) + check_for_duplicates metasenv "in input a demodulation aux"; 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 (Inference.string_of_equality x)) - candidates; - prerr_endline ("-------"); - prerr_endline ("+++++++")); -(* let candidates = List.map make_variant candidates in *) + get_candidates + ~env:(metasenv,context,ugraph) (* Unification *) Matching table term + in let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates + in let res = match term with | C.Meta _ -> None | term -> - let termty, ugraph = - if typecheck then - CicTypeChecker.type_of_aux' metasenv context term ugraph - else - C.Implicit None, ugraph - in - let res = - find_matches metasenv context ugraph lift_amount term termty candidates + let res = + try + let termty, ugraph = + if typecheck then + CicTypeChecker.type_of_aux' metasenv context term ugraph + else + C.Implicit None, ugraph + in + find_matches bag metasenv context ugraph + lift_amount term termty candidates + with _ -> + prerr_endline "type checking error"; + prerr_endline ("menv :\n" ^ CicMetaSubst.ppmetasenv [] metasenv); + prerr_endline ("term: " ^ (CicPp.ppterm term)); + assert false; + (* None *) in - if Utils.debug_res then ignore(check_res res "demod1"); - if res <> None then + let res = + (if Utils.debug_res then + ignore(check_res res "demod1"); + if check_demod_res res metasenv "demod" then res else None) in + if res <> None then res else match term with @@ -525,7 +608,7 @@ let rec demodulation_aux ?from ?(typecheck=false) (res, tl @ [S.lift 1 t]) else let r = - demodulation_aux ~from:"1" metasenv context ugraph table + demodulation_aux bag ~from:"1" metasenv context ugraph table ~typecheck lift_amount t in match r with @@ -538,14 +621,15 @@ let rec demodulation_aux ?from ?(typecheck=false) | Some (_, subst, menv, ug, eq_found) -> Some (C.Appl ll, subst, menv, ug, eq_found) ) +(* | C.Prod (nn, s, t) -> let r1 = - demodulation_aux ~from:"2" + demodulation_aux bag ~from:"2" metasenv context ugraph table lift_amount s in ( match r1 with | None -> let r2 = - demodulation_aux metasenv + demodulation_aux bag metasenv ((Some (nn, C.Decl s))::context) ugraph table (lift_amount+1) t in ( @@ -560,13 +644,14 @@ let rec demodulation_aux ?from ?(typecheck=false) subst, menv, ug, eq_found) ) | C.Lambda (nn, s, t) -> + prerr_endline "siam qui"; let r1 = - demodulation_aux + demodulation_aux bag metasenv context ugraph table lift_amount s in ( match r1 with | None -> let r2 = - demodulation_aux metasenv + demodulation_aux bag metasenv ((Some (nn, C.Decl s))::context) ugraph table (lift_amount+1) t in ( @@ -580,6 +665,7 @@ let rec demodulation_aux ?from ?(typecheck=false) Some (C.Lambda (nn, s', (S.lift 1 t)), subst, menv, ug, eq_found) ) +*) | t -> None in @@ -587,169 +673,109 @@ 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 bag ?from eq_uri newmeta env table target = + (* + prerr_endline ("demodulation_eq:\n"); + Index.iter table (fun l -> + let l = Index.PosEqSet.elements l in + let l = + List.map (fun (p,e) -> + Utils.string_of_pos p ^ Equality.string_of_equality e) l in + prerr_endline (String.concat "\n" l) + ); + *) let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in 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"); + ignore(check_target bag context target "demod equalities input"); 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 ignore(check_for_duplicates menv "input1"); ignore(check_disjoint_invariant subst menv "input2"); - let substs = Inference.ppsubst subst in - ignore(check_target context (snd eq_found) ("input3" ^ substs)) + let substs = Subst.ppsubst subst in + ignore(check_target bag 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 ty, eq_ty = apply_subst subst ty, apply_subst subst eq_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 - incr demod_counter; + 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 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, - Inference.ProofBlock ( - subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof)) - else - 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' = - 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 - (subst, eq_URI, (name, ty), bo', - eq_found, Inference.BasicProof ([],metaproof)) - in - match proof with - | Inference.BasicProof _ -> - (* print_endline "replacing a BasicProof"; *) - pb - | Inference.ProofGoalBlock (_, parent_proof) -> - (* print_endline "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 is_left then right else left] - in - (bo, - Inference.ProofGoalBlock (Inference.BasicProof ([],refl), 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); - () - with exc -> - prerr_endline "sempre lui"; - prerr_endline (Inference.ppsubst subst); - prerr_endline (CicPp.ppterm (Inference.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: " ^ (Inference.ppsubst subst)); - raise exc; - else () + (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'), + (Cic.Lambda (name, ty, bo')))))) 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 - (w, newproof, stat,newmenv) in + (Equality.mk_equality bag (w, newproof, stat,newmenv)) + in if Utils.debug_metas then - ignore(check_target context res "buildnew_target output"); + ignore(check_target bag 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 + let res = + demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left + in if Utils.debug_res then check_res res "demod result"; let newmeta, newtarget = 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 bag ?from eq_uri newmeta env table newtarget | None -> - let res = demodulation_aux metasenv' context ugraph table 0 right in + let res = demodulation_aux bag 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 bag ?from eq_uri newmeta env table newtarget | None -> newmeta, target in @@ -762,16 +788,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) -> @@ -843,8 +871,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 @@ -860,7 +888,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', @@ -872,126 +900,20 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term = | C.Meta (i, l) -> res, lifted_term | term -> let termty, ugraph = - C.Implicit None, ugraph -(* CicTypeChecker.type_of_aux' metasenv context term ugraph *) +(* 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 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 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) - - in - !maxmeta, List.map build_new expansions -;; - - -let sup_r_counter = ref 1;; - (** superposition_right returns a list of new clauses inferred with a right superposition step @@ -999,29 +921,27 @@ 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 bag + ?(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 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"); + ignore (check_target bag context target "superpositionright"); 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 @@ -1029,188 +949,406 @@ 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 + ignore (check_target bag context (snd eq_found) "buildnew1" ); - 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 ty, eq_ty = apply_subst s ty, apply_subst s eq_ty 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 - incr sup_r_counter; + let bo' = + Utils.guarded_simpl context (apply_subst s (S.subst other bo)) + in + let name = C.Name "x" in 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', - 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 = if ordering = U.Gt then newgoal, apply_subst s right else apply_subst s left, newgoal in let neworder = !Utils.compare_terms left right in - let newmenv = (* Inference.filter s *) m in + let newmenv = (* Founif.filter s *) m in 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 bag (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 + ignore (check_target bag context eq' "buildnew3"); + let newm, eq' = Equality.fix_metas bag !maxmeta eq' in if Utils.debug_metas then - ignore (check_target context eq' "buildnew4"); + ignore (check_target bag context eq' "buildnew4"); 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"); + ignore(check_target bag context newequality "buildnew2"); newequality 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 = +(** demodulation, when the target is a theorem *) +let rec demodulation_theorem bag env table theorem = let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in + let eq_uri = + match LibraryObjects.eq_URI() with + | Some u -> u + | None -> assert false in let metasenv, context, ugraph = env in - let maxmeta = ref newmeta in - let proof, metas, term = goal in - let term = Utils.guarded_simpl (~debug:true) context term in - let goal = proof, 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) -> - prerr_endline "subproof!"; - Inference.SubProof (term, meta_index, repl p) - | _ -> assert false - in repl proof - in - bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof) + let proof, theo, metas = theorem in + 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 + let peq = + match proof' with + | Equality.Exact p -> p + | _ -> assert false in + let what, other = + if pos = Utils.Left then what, other else other, what in + let newtheo = apply_subst subst (S.subst other t) in + let name = C.Name "x" in + let body = apply_subst subst t in + let pred = C.Lambda(name,ty,body) in + let newproof = + match pos with + | Utils.Left -> + Equality.mk_eq_ind eq_uri ty what pred proof other peq + | Utils.Right -> + Equality.mk_eq_ind eq_uri ty what pred proof other peq 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 + newproof,newtheo in + let res = demodulation_aux bag metas context ugraph table 0 theo in match res with | Some t -> - let newmeta, newgoal = build_newgoal t in - let _, _, newg = newgoal in - if Inference.meta_convertibility term newg then - newmeta, newgoal + let newproof, newtheo = build_newtheorem t in + if Equality.meta_convertibility theo newtheo then + newproof, newtheo else - demodulation_goal newmeta env table newgoal + demodulation_theorem bag env table (newproof,newtheo,[]) | None -> - newmeta, goal + proof,theo ;; -(** demodulation, when the target is a theorem *) -let rec demodulation_theorem newmeta env table theorem = - 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 term, termty, metas = theorem in - 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 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 - incr demod_counter; - let newproof = - Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found, - Inference.BasicProof ([],term)) - in - (Inference.build_proof_term newproof, bo) - in - !maxmeta, (newterm, newty, menv) - in - let res = - demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty +(*****************************************************************************) +(** OPERATIONS ON GOALS **) +(** **) +(** DEMODULATION_GOAL & SUPERPOSITION_LEFT **) +(*****************************************************************************) + +(* new: demodulation of non_equality terms *) +let build_newg bag context goal rule expansion = + let goalproof,_,_ = goal in + let (t,subst,menv,ug,eq_found) = 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 ty = apply_subst subst ty 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 = (* Founif.filter subst *) menv in + (newgoalproof, newmetasenv, newterm) +;; + +let rec demod bag env table goal = + let goalproof,menv,t = goal in + let _, context, ugraph = env in + let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:true)in match res with + | Some newt -> + let newg = + build_newg bag context goal Equality.Demodulation newt + in + let _,_,newt = newg in + if Equality.meta_convertibility t newt then + false, goal + else + true, snd (demod bag env table newg) + | None -> + false, goal +;; + +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 bag 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 ty = apply_subst subst ty 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 = (* Founif.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 bag (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 bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl + @ + List.map (build_newgoal bag 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 bag 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 bag 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 bag 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 bag menv context ugraph table 0 right in + match resright with + | Some t -> + let newg = + build_newgoal bag context goal Utils.Left Equality.Demodulation t + in + if goal_metaconvertibility_eq goal newg then + false, goal + else + true, snd (demodulation_goal bag env table newg) + | None -> false, goal + in + let resleft = demodulation_aux bag menv context ugraph table 0 left in + match resleft with | Some t -> - let newmeta, newthm = build_newtheorem t in - let newt, newty, _ = newthm in - if Inference.meta_convertibility termty newty then - newmeta, newthm + let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in + if goal_metaconvertibility_eq goal newg then + do_right () else - demodulation_theorem newmeta env table newthm - | None -> - newmeta, theorem + true, snd (demodulation_goal bag env table newg) + | None -> do_right () +;; + +type next = L | R +type solved = Yes of Equality.goal | No of Equality.goal list + +(* returns all the 1 step demodulations *) +module C = Cic;; +module S = CicSubstitution;; +let rec demodulation_all_aux + metasenv context ugraph table lift_amount term += + let candidates = + get_candidates ~env:(metasenv,context,ugraph) Matching table term + in + match term with + | C.Meta _ -> [] + | _ -> + let termty, ugraph = C.Implicit None, ugraph in + let res = + find_all_matches + metasenv context ugraph lift_amount term termty candidates + in + match term with + | C.Appl l -> + let res, _, _ = + List.fold_left + (fun (res,l,r) t -> + res @ + List.map + (fun (rel, s, m, ug, c) -> + (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c)) + (demodulation_all_aux + metasenv context ugraph table lift_amount t), + l@[List.hd r], List.tl r) + (res, [], List.map (S.lift 1) l) l + in + res + | C.Prod (nn, s, t) + | C.Lambda (nn, s, t) -> + let context = (Some (nn, C.Decl s))::context in + let mk s t = + match term with + | Cic.Prod _ -> Cic.Prod (nn,s,t) | _ -> Cic.Lambda (nn,s,t) + in + res @ + List.map + (fun (rel, subst, m, ug, c) -> + mk (S.lift 1 s) rel, subst, m, ug, c) + (demodulation_all_aux + metasenv context ugraph table (lift_amount+1) t) + (* we could demodulate also in s, but then t may be badly + * typed... *) + | t -> res +;; + +let solve_demodulating bag env table initgoal steps = + let _, context, ugraph = env in + let solved goal res side = + let newg = build_newgoal bag context goal side Equality.Demodulation res in + match newg with + | (goalproof,m,Cic.Appl[Cic.MutInd(uri,n,ens);eq_ty;left;right]) + when LibraryObjects.is_eq_URI uri -> + (try + let _ = + Founif.unification m m context left right CicUniv.empty_ugraph + in + Yes newg + with CicUnification.UnificationFailure _ -> No [newg]) + | _ -> No [newg] + in + let solved goal res_list side = + let newg = List.map (fun x -> solved goal x side) res_list in + try + List.find (function Yes _ -> true | _ -> false) newg + with Not_found -> + No (List.flatten (List.map (function No s -> s | _-> assert false) newg)) + in + let rec first f l = + match l with + | [] -> None + | x::tl -> + match f x with + | None -> first f tl + | Some x as ok -> ok + in + let rec aux steps next goal = + if steps = 0 then None else + let goalproof,menv,_,_,left,right = open_goal goal in + let do_step t = + demodulation_all_aux menv context ugraph table 0 t + in + match next with + | L -> + (match do_step left with + | _::_ as res -> + (match solved goal res Utils.Right with + | No newgoals -> + (match first (aux (steps - 1) L) newgoals with + | Some g as success -> success + | None -> aux steps R goal) + | Yes newgoal -> Some newgoal) + | [] -> aux steps R goal) + | R -> + (match do_step right with + | _::_ as res -> + (match solved goal res Utils.Left with + | No newgoals -> + (match first (aux (steps - 1) L) newgoals with + | Some g as success -> success + | None -> None) + | Yes newgoal -> Some newgoal) + | [] -> None) + in + aux steps L initgoal ;; +let get_stats () = "" ;;