X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fparamodulation%2Findexing.ml;h=207fb94338b64e37b078c9cc1de6a77e94edf3ce;hb=cbac948d507d74a558ba7f11ce10bc252b1ba8ba;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..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)) @@ -179,7 +183,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 +253,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 +348,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 @@ -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 ;; @@ -832,13 +838,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 +858,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 @@ -873,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))) ;; @@ -888,6 +889,8 @@ 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 let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) = @@ -938,11 +941,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 @@ -950,7 +949,7 @@ 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 let res = @@ -977,10 +976,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,9 +993,10 @@ 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 + let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') in !maxmeta, (newterm, newty, newmetasenv) in let res = @@ -1015,30 +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) as conjecture = 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 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 - 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 - -let demodulate_tac ~dbd ~pattern = - ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern)