type result =
| ParamodulationFailure
- | ParamodulationSuccess of Inference.proof option * environment
+ | ParamodulationSuccess of (Inference.proof * Cic.metasenv) option
;;
type goal = proof * Cic.metasenv * Cic.term;;
else
match passive_table with
| None ->
- if fst (Indexing.subsumption env active_table c) then
- None
- else
+ if Indexing.subsumption env active_table c = None then
res
+ else
+ None
| Some passive_table ->
if Indexing.in_index passive_table c then None
else
- let r1, _ = Indexing.subsumption env active_table c in
- if r1 then None else
- let r2, _ = Indexing.subsumption env passive_table c in
- if r2 then None else res
+ if Indexing.subsumption env active_table c = None then
+ if Indexing.subsumption env passive_table c = None then
+ res
+ else
+ None
+ else
+ None
;;
type fs_time_info_t = {
let subs =
match passive_table with
| None ->
- (fun e -> not (fst (Indexing.subsumption env active_table e)))
+ (fun e -> (Indexing.subsumption env active_table e = None))
| Some passive_table ->
- (fun e -> not ((fst (Indexing.subsumption env active_table e)) ||
- (fst (Indexing.subsumption env passive_table e))))
+ (fun e -> ((Indexing.subsumption env active_table e = None) &&
+ (Indexing.subsumption env passive_table e = None)))
in
(* let t1 = Unix.gettimeofday () in *)
(* let t2 = Unix.gettimeofday () in *)
let changed', goal = demodulate passive_table goal in
(changed || changed'), goal
in
- changed, if not changed then goal
- else snd (simplify_goal env goal ?passive (active_list, active_table))
+ changed,
+ if not changed then
+ goal
+ else
+ snd (simplify_goal env goal ?passive (active_list, active_table))
;;
let activate_goal (active, passive) =
- match passive with
- | goal_conj::tl -> true, (goal_conj::active, tl)
- | [] -> false, (active, passive)
+ if active = [] then
+ match passive with
+ | goal_conj::tl -> true, (goal_conj::active, tl)
+ | [] -> false, (active, passive)
+ else
+ true, (active,passive)
;;
;;
*)
+let check_if_goal_is_subsumed env (proof,menv,ty) table =
+ match ty with
+ | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right]
+ when UriManager.eq uri (LibraryObjects.eq_URI ()) ->
+ (let goal_equation = 0,proof,(eq_ty,left,right,Eq),menv in
+ match Indexing.subsumption env table goal_equation with
+ | Some (subst, (_,p,_,m)) ->
+ let p = Inference.apply_subst subst (Inference.build_proof_term p) in
+ let newp =
+ let rec repl = function
+ | Inference.ProofGoalBlock (_, gp) ->
+ Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp)
+ | Inference.NoProof -> Inference.BasicProof ([],p)
+ | Inference.BasicProof _ -> Inference.BasicProof ([],p)
+ | Inference.SubProof (t, i, p2) ->
+ Inference.SubProof (t, i, repl p2)
+ | _ -> assert false
+ in
+ repl proof
+ in
+ Some (newp,Inference.apply_subst_metasenv subst m @ menv)
+ | None -> None)
+ | _ -> None
+;;
+
let counter = ref 0
(** given-clause algorithm with full reduction strategy *)
| _ -> assert false
in
repl proof
- in true, Some newp
- | (_, [proof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]])::_->
- (* here we check if the goal is subsumed by an active *)
- let ok, subst =
- (* the first m is unused *)
- Indexing.subsumption (m,context,CicUniv.empty_ugraph)
- (snd active)
- (0,proof,(eq_ty,left,right,Eq),m)
- in
- if ok then
- begin
- prerr_endline "The goal is subsumed by an active";
- false, None
- end
- else
- ok, None
+ in true, Some (newp,m)
+ | (_, [proof,m,ty])::_ ->
+ (match check_if_goal_is_subsumed env (proof,m,ty) (snd active) with
+ | None -> false,None
+ | Some (newproof,m) ->
+ prerr_endline "Proof found by subsumption!";
+ true, Some (newproof,m))
| _ -> false, None
in
if ok then
(let x,y,_ = passive in (fst x)@(fst y)))) in
prerr_endline s;
prerr_endline sp; *)
- ParamodulationSuccess (proof, env))
+ ParamodulationSuccess (proof))
else
given_clause_fullred_aux dbd env goals theorems passive active
else
(lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
(string_of_equality ~env current)));
let _, proof, _, m = current in
- ParamodulationSuccess (Some proof, env)
+ ParamodulationSuccess (Some (proof, m))
) else (
debug_print
(lazy "\n================================================");
| true, goal ->
let proof =
match goal with
- | Some goal -> let _, proof, _, _ = goal in Some proof
+ | Some goal -> let _, proof, _, env = goal in Some (proof,env)
| None -> None
in
- ParamodulationSuccess (proof, env)
+ ParamodulationSuccess proof
)
;;
match res with
| ParamodulationFailure ->
Printf.printf "NO proof found! :-(\n\n"
- | ParamodulationSuccess (Some proof, env) ->
+ | ParamodulationSuccess (Some (proof, env)) ->
let proof = Inference.build_proof_term proof in
Printf.printf "OK, found a proof!\n";
(* REMEMBER: we have to instantiate meta_proof, we should use
in
()
- | ParamodulationSuccess (None, env) ->
+ | ParamodulationSuccess None ->
Printf.printf "Success, but no proof?!?\n\n"
in
if Utils.time then
let module C = Cic in
reset_refs ();
Indexing.init_index ();
+ counter := 0;
maxdepth := depth;
maxwidth := width;
(* CicUnification.unif_ty := false;*)
(res, finish -. start)
in
match res with
- | ParamodulationSuccess (Some proof, _) ->
+ | ParamodulationSuccess (Some (proof, proof_menv)) ->
debug_print (lazy "OK, found a proof!");
let proof = Inference.build_proof_term proof in
+ let equality_for_replace i t1 =
+ match t1 with
+ | C.Meta (n, _) -> n = i
+ | _ -> false
+ in
+ let proof_menv, what, with_what =
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
+ List.fold_left
+ (fun (acc1,acc2,acc3) (i,_,ty) ->
+ (i,context,ty)::acc1,
+ (Cic.Meta(i,[]))::acc2,
+ (Cic.Meta(i,irl)) ::acc3)
+ ([],[],[]) proof_menv
+ in
+ let proof = ProofEngineReduction.replace_lifting
+ ~equality:(=)
+ ~what ~with_what
+ ~where:proof
+ in
(* prerr_endline (CicPp.ppterm proof); *)
let names = names_of_context context in
let newmetasenv =
in
List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv
in
+ let newmetasenv = newmetasenv@proof_menv in
let newstatus =
try
let ty, ug =
(string_of_bool
(fst (CicReduction.are_convertible
context type_of_goal ty ug)))));
- let equality_for_replace i t1 =
- match t1 with
- | C.Meta (n, _) -> n = i
- | _ -> false
- in
let real_proof =
ProofEngineReduction.replace
~equality:equality_for_replace
(print_metasenv newmetasenv)
(CicPp.pp real_proof [](* names *))
(CicPp.pp term_to_prove names)));
- ((uri, newmetasenv, real_proof, term_to_prove), [])
+ ((uri, newmetasenv, real_proof, term_to_prove),
+ List.map (fun (i,_,_) -> i) proof_menv)
with CicTypeChecker.TypeCheckerFailure _ ->
debug_print (lazy "THE PROOF DOESN'T TYPECHECK!!!");
debug_print (lazy (CicPp.pp proof names));
projects / helm.git / blobdiff