X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fparamodulation%2Findexing.ml;h=207fb94338b64e37b078c9cc1de6a77e94edf3ce;hb=cbac948d507d74a558ba7f11ce10bc252b1ba8ba;hp=8ece33e35251e9e642a95086617eea29fadf9d5b;hpb=5886d890afe8fbb3b6bae0fffdfa657b894cae3f;p=helm.git diff --git a/helm/ocaml/tactics/paramodulation/indexing.ml b/helm/ocaml/tactics/paramodulation/indexing.ml index 8ece33e35..207fb9433 100644 --- a/helm/ocaml/tactics/paramodulation/indexing.ml +++ b/helm/ocaml/tactics/paramodulation/indexing.ml @@ -130,6 +130,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty = let module M = CicMetaSubst in let module HL = HelmLibraryObjects in let cmp = !Utils.compare_terms in + ignore(CicTypeChecker.type_of_aux' metasenv context term); let check = match termty with C.Implicit None -> false | _ -> true in function | [] -> None @@ -150,10 +151,13 @@ let rec find_matches metasenv context ugraph lift_amount term termty = let t2 = Unix.gettimeofday () in match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1); r - with Inference.MatchingFailure as e -> + with + | Inference.MatchingFailure as e -> let t2 = Unix.gettimeofday () in match_unif_time_no := !match_unif_time_no +. (t2 -. t1); - raise e + raise e + | CicUtil.Meta_not_found _ as exn -> + prerr_endline "siam qua"; raise exn in Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph', (candidate, eq_URI)) @@ -446,7 +450,14 @@ let rec demodulation_equality newmeta env table sign target = let module HL = HelmLibraryObjects in let module U = Utils in let metasenv, context, ugraph = env in - let _, proof, (eq_ty, left, right, order), metas, args = target in + let w, proof, (eq_ty, left, right, order), metas, args = target in + (* first, we simplify *) + let right = U.guarded_simpl context right in + let left = U.guarded_simpl context left in + let w = Utils.compute_equality_weight eq_ty left right in + let order = !Utils.compare_terms left right in + let target = w, proof, (eq_ty, left, right, order), metas, args in + let metasenv' = metasenv @ metas in let maxmeta = ref newmeta in @@ -520,7 +531,8 @@ let rec demodulation_equality newmeta env table sign target = in let left, right = if is_left then newterm, right else left, newterm in let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in - let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') + (* let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') *) + let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metasenv' @ menv') and newargs = args in let ordering = !Utils.compare_terms left right in @@ -539,7 +551,7 @@ let rec demodulation_equality newmeta env table sign target = match res with | Some t -> let newmeta, newtarget = build_newtarget true t in - if (Inference.is_identity (metasenv', context, ugraph) newtarget) || + if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) || (Inference.meta_convertibility_eq target newtarget) then newmeta, newtarget else @@ -549,7 +561,7 @@ let rec demodulation_equality newmeta env table sign target = match res with | Some t -> let newmeta, newtarget = build_newtarget false t in - if (Inference.is_identity (metasenv', context, ugraph) newtarget) || + if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) || (Inference.meta_convertibility_eq target newtarget) then newmeta, newtarget else @@ -558,13 +570,7 @@ let rec demodulation_equality newmeta env table sign target = newmeta, target in (* newmeta, newtarget *) - (* tentiamo di normalizzare *) - let w, p, (ty, left, right, o), m, a = newtarget in - let left = U.guarded_simpl context left in - let right = U.guarded_simpl context right in - let w' = Utils.compute_equality_weight ty left right in - let o' = !Utils.compare_terms left right in - newmeta, (w', p, (ty, left, right, o'), m, a) + newmeta,newtarget ;; @@ -865,7 +871,10 @@ 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 (Inference.is_identity (metasenv', context, ugraph) e) in (!maxmeta, (List.filter ok (new1 @ new2))) ;; @@ -880,8 +889,9 @@ let rec demodulation_goal newmeta env table goal = 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' = 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 @@ -939,14 +949,12 @@ let rec demodulation_goal newmeta env table goal = bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof) in let m = Inference.metas_of_term newterm in - let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in + let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv')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 @@ -954,11 +962,7 @@ let rec demodulation_goal newmeta env table goal = if Inference.meta_convertibility term newg then newmeta, newgoal else - begin - Printf.eprintf "reducing %s to %s \n" - (CicPp.ppterm term) (CicPp.ppterm newg); - demodulation_goal newmeta env table newgoal - end + demodulation_goal newmeta env table newgoal | None -> newmeta, goal ;; @@ -992,7 +996,7 @@ let rec demodulation_theorem newmeta env table theorem = in let m = Inference.metas_of_term newterm in - let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in + let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') in !maxmeta, (newterm, newty, newmetasenv) in let res = @@ -1010,43 +1014,3 @@ let rec demodulation_theorem newmeta env table theorem = newmeta, theorem ;; -let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = - let module I = Inference in - let curi,metasenv,pbo,pty = proof 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, [], ty in - let equalities = equalities @ library_equalities in - let table = - List.fold_left - (fun tbl eq -> index tbl eq) - empty equalities - in - let newmeta,(newproof,newmetasenv, newty) = demodulation_goal - maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal - in - 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)