X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fparamodulation%2Findexing.ml;h=4eed05790fd777060db24f2d757e9b97cfd69425;hb=b555e6b8c27c765a4611dda9528963ebff116412;hp=b60435e04ba16cd7e77f76b463c689994c70fe07;hpb=b1527286e32c8651d65619af61e3f638b3b89f8d;p=helm.git diff --git a/helm/ocaml/tactics/paramodulation/indexing.ml b/helm/ocaml/tactics/paramodulation/indexing.ml index b60435e04..4eed05790 100644 --- a/helm/ocaml/tactics/paramodulation/indexing.ml +++ b/helm/ocaml/tactics/paramodulation/indexing.ml @@ -179,7 +179,6 @@ let rec find_matches metasenv context ugraph lift_amount term termty = let other' = U.guarded_simpl context (apply_subst s other) in *) let other' = apply_subst s other in let order = cmp c' other' in - let names = U.names_of_context context in if order = U.Gt then res else @@ -250,7 +249,6 @@ let rec find_all_matches ?(unif_fun=Inference.unification) let c' = apply_subst s c and other' = apply_subst s other in let order = cmp c' other' in - let names = U.names_of_context context in if order <> U.Lt && order <> U.Le then res::(find_all_matches ~unif_fun metasenv context ugraph lift_amount term termty tl) @@ -346,6 +344,8 @@ let subsumption env table target = let rec demodulation_aux ?(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 @@ -832,13 +832,6 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = let newgoal, newproof = (* qua *) let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in - let t' = - let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in - incr sup_r_counter; - let l, r = - if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in - (name, ty, S.lift 1 eq_ty, l, r) - in let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in incr sup_r_counter; let bo'' = @@ -859,8 +852,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = and newargs = args @ args' in let eq' = let w = Utils.compute_equality_weight eq_ty left right in - (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) - and env = (metasenv, context, ugraph) in + (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) in let newm, eq' = Inference.fix_metas !maxmeta eq' in newm, eq' in @@ -889,6 +881,7 @@ let rec demodulation_goal newmeta env table goal = let maxmeta = ref newmeta in let proof, metas, term = goal in let metasenv' = metasenv @ metas in + Printf.eprintf "siam qua\n"; let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) = let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in @@ -938,11 +931,7 @@ let rec demodulation_goal newmeta env table goal = | Inference.ProofGoalBlock (_, parent_proof) -> (* debug_print (lazy "replacing another ProofGoalBlock"); *) Inference.ProofGoalBlock (pb, parent_proof) - | (Inference.SubProof (term, meta_index, p) as subproof) -> -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "replacing %s" *) -(* (Inference.string_of_proof subproof))); *) + | Inference.SubProof (term, meta_index, p) -> Inference.SubProof (term, meta_index, repl p) | _ -> assert false in repl proof @@ -953,9 +942,11 @@ let rec demodulation_goal newmeta env table goal = let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in !maxmeta, (newproof, newmetasenv, newterm) in + Printf.eprintf "bum0\n"; let res = demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term in + Printf.eprintf "bum\n"; match res with | Some t -> let newmeta, newgoal = build_newgoal t in @@ -963,7 +954,11 @@ let rec demodulation_goal newmeta env table goal = if Inference.meta_convertibility term newg then newmeta, newgoal else - demodulation_goal newmeta env table newgoal + begin + Printf.eprintf "reducing %s to %s \n" + (CicPp.ppterm term) (CicPp.ppterm newg); + demodulation_goal newmeta env table newgoal + end | None -> newmeta, goal ;; @@ -977,10 +972,9 @@ let rec demodulation_theorem newmeta env table theorem = let module HL = HelmLibraryObjects in let metasenv, context, ugraph = env in let maxmeta = ref newmeta in - let proof, metas, term = theorem in let term, termty, metas = theorem in let metasenv' = metasenv @ metas in - + let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) = let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in let what, other = if pos = Utils.Left then what, other else other, what in @@ -995,7 +989,8 @@ let rec demodulation_theorem newmeta env table theorem = Inference.BasicProof term) in (Inference.build_proof_term newproof, bo) - in + in + let m = Inference.metas_of_term newterm in let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in !maxmeta, (newterm, newty, newmetasenv) @@ -1015,30 +1010,43 @@ let rec demodulation_theorem newmeta env table theorem = newmeta, theorem ;; -let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = +let demodulate_tac ~dbd ~pattern (proof,goal) = let module I = Inference in let curi,metasenv,pbo,pty = proof in - let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in let eq_indexes, equalities, maxm = I.find_equalities context proof in let lib_eq_uris, library_equalities, maxm = I.find_library_equalities dbd context (proof, goal) (maxm+2) in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let library_equalities = List.map snd library_equalities in let goalterm = Cic.Meta (metano,irl) in - let initgoal = Inference.BasicProof goalterm, [], goalterm in + let initgoal = Inference.BasicProof goalterm, [], ty in let equalities = equalities @ library_equalities in let table = List.fold_left (fun tbl eq -> index tbl eq) empty equalities in - let _,(newproof, newty, newmetasenv) = demodulation_goal + let newmeta,(newproof,newmetasenv, newty) = demodulation_goal maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal in - let proofterm = Inference.build_proof_term newproof in - ProofEngineTypes.apply_tactic - (PrimitiveTactics.apply_tac ~term:proofterm) - initialstatus + if newmeta != maxm then + begin + let opengoal = Cic.Meta(maxm,irl) in + let proofterm = + Inference.build_proof_term ~noproof:opengoal newproof in + prerr_endline ("proffterm ="^(CicMetaSubst.ppterm_in_context [] proofterm context)); + let extended_metasenv = (maxm,context,newty)::metasenv in + prerr_endline ("metasenv ="^(CicMetaSubst.ppmetasenv [] extended_metasenv)); + let extended_status = + (curi,extended_metasenv,pbo,pty),goal in + let (status,newgoals) = + ProofEngineTypes.apply_tactic + (PrimitiveTactics.apply_tac ~term:proofterm) + extended_status in + (status,maxm::newgoals) + end + else raise (ProofEngineTypes.Fail (lazy "no progress")) let demodulate_tac ~dbd ~pattern = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern)