X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Finference.ml;h=e2f21b25cfe823d004c5579238d5f3562586f3dd;hb=801f0eb3eabe1cbcd66d6a3f52c24eb8f1189611;hp=f5508c8c146cc72bc2c418b5ae80770febf6fd4c;hpb=86d27070abaa7844fa53ab83b8a57489cc2d7e1a;p=helm.git diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml index f5508c8c1..e2f21b25c 100644 --- a/components/tactics/paramodulation/inference.ml +++ b/components/tactics/paramodulation/inference.ml @@ -37,8 +37,7 @@ type equality = Cic.term * (* left side *) Cic.term * (* right side *) Utils.comparison) * (* ordering *) - Cic.metasenv * (* environment for metas *) - Cic.term list (* arguments *) + Cic.metasenv (* environment for metas *) and proof = | NoProof (* term is the goal missing a proof *) @@ -55,14 +54,14 @@ let string_of_equality ?env = match env with | None -> ( function - | w, _, (ty, left, right, o), _, _ -> + | w, _, (ty, left, right, o), _ -> Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty) (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right) ) | Some (_, context, _) -> ( let names = names_of_context context in function - | w, _, (ty, left, right, o), _, _ -> + | w, _, (ty, left, right, o), _ -> Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names) (CicPp.pp left names) (string_of_comparison o) (CicPp.pp right names) @@ -139,11 +138,11 @@ let build_proof_term ?(noproof=Cic.Implicit None) proof = | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) -> let t' = Cic.Lambda (name, ty, bo) in let proof' = - let _, proof', _, _, _ = eq in + let _, proof', _, _ = eq in do_build_proof proof' in let eqproof = do_build_proof eqproof in - let _, _, (ty, what, other, _), menv', args' = eq in + let _, _, (ty, what, other, _), menv' = eq in let what, other = if pos = Utils.Left then what, other else other, what in @@ -311,8 +310,8 @@ let meta_convertibility_aux table t1 t2 = let meta_convertibility_eq eq1 eq2 = - let _, _, (ty, left, right, _), _, _ = eq1 - and _, _, (ty', left', right', _), _, _ = eq2 in + let _, _, (ty, left, right, _), _ = eq1 + and _, _, (ty', left', right', _), _ = eq2 in if ty <> ty' then false else if (left = left') && (right = right') then @@ -451,7 +450,10 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph = List.rev subst, menv, ugraph ;; -let profiler = HExtlib.profile "flatten" +let profiler = HExtlib.profile "P/Inference.unif_simple[flatten]" +let profiler2 = HExtlib.profile "P/Inference.unif_simple[flatten_fast]" +let profiler3 = HExtlib.profile "P/Inference.unif_simple[resolve_meta]" +let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]" let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph = let metasenv = metasenv1 @ metasenv2 in @@ -480,8 +482,25 @@ let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph = let ty = CicMetaSubst.apply_subst subst ty in (i, (context, term, ty))) subst in - let flatten subst = profiler.HExtlib.profile flatten subst in - let subst = flatten subst in + let flatten_fast subst = + let resolve_meta (i, (context, term, ty)) subst = + let term = CicMetaSubst.apply_subst subst term in + let ty = CicMetaSubst.apply_subst subst ty in + (i, (context, term, ty)) + in + let resolve_meta t s = profiler3.HExtlib.profile (resolve_meta t) s in + let filter j (i,_) = i <> j in + let filter a b = profiler4.HExtlib.profile (filter a) b in + List.fold_left + (fun subst (j,(c,t,ty)) as s -> + let s = resolve_meta s subst in + s::(List.filter (filter j) subst)) + subst subst + in + (*let flatten subst = profiler.HExtlib.profile flatten subst in*) + let flatten_fast subst = profiler2.HExtlib.profile flatten_fast subst in + (*let subst = flatten subst in*) +(* let subst = flatten_fast subst in*) subst, menv, ug ;; @@ -726,7 +745,7 @@ let matching metasenv1 metasenv2 context t1 t2 ugraph = let matching = matching1;; let check_eq context msg eq = - let w, proof, (eq_ty, left, right, order), metas, args = eq in + let w, proof, (eq_ty, left, right, order), metas = eq in if not (fst (CicReduction.are_convertible ~metasenv:metas context eq_ty (fst (CicTypeChecker.type_of_aux' metas context left CicUniv.empty_ugraph)) CicUniv.empty_ugraph)) @@ -773,7 +792,7 @@ let find_equalities context proof = let stat = (ty,t1,t2,o) in let w = compute_equality_weight stat in let proof = BasicProof p in - let e = (w, proof, stat, newmetas, args) in + let e = (w, proof, stat, newmetas) in Some e, (newmeta+1) | _ -> None, newmeta ) @@ -785,7 +804,7 @@ let find_equalities context proof = let o = !Utils.compare_terms t1 t2 in let stat = (ty,t1,t2,o) in let w = compute_equality_weight stat in - let e = (w, BasicProof (C.Rel index), stat, [], []) in + let e = (w, BasicProof (C.Rel index), stat, []) in Some e, (newmeta+1) | _ -> None, newmeta in ( @@ -923,7 +942,7 @@ let find_library_equalities dbd context status maxmeta = let stat = (ty,t1,t2,o) in let w = compute_equality_weight stat in let proof = BasicProof p in - let e = (w, proof, stat, newmetas, args) in + let e = (w, proof, stat, newmetas) in Some e, (newmeta+1) | _ -> None, newmeta ) @@ -932,7 +951,7 @@ let find_library_equalities dbd context status maxmeta = let o = !Utils.compare_terms t1 t2 in let stat = (ty,t1,t2,o) in let w = compute_equality_weight stat in - let e = (w, BasicProof term, stat, [], []) in + let e = (w, BasicProof term, stat, []) in Some e, (newmeta+1) | _ -> None, newmeta in @@ -1135,7 +1154,7 @@ let relocate newmeta menv = subst, metasenv, newmeta -let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) = +let fix_metas newmeta (w, p, (ty, left, right, o), menv) = (* let metas = (metas_of_term left)@(metas_of_term right) @(metas_of_term ty)@(metas_of_proof p) in @@ -1149,7 +1168,6 @@ let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) = let ty = CicMetaSubst.apply_subst subst ty in let left = CicMetaSubst.apply_subst subst left in let right = CicMetaSubst.apply_subst subst right in - let args = List.map (CicMetaSubst.apply_subst subst) args in let rec fix_proof = function | NoProof -> NoProof | BasicProof term -> BasicProof (CicMetaSubst.apply_subst subst term) @@ -1171,7 +1189,7 @@ let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) = @(metas_of_term ty)@(metas_of_proof p) in let metasenv = List.filter (fun (i, _, _) -> List.mem i metas) metasenv in *) - let eq = (w, p, (ty, left, right, o), metasenv, args) in + let eq = (w, p, (ty, left, right, o), metasenv) in (* debug prerr_endline (string_of_equality eq); *) newmeta+1, eq @@ -1193,7 +1211,7 @@ let equality_of_term proof term = let o = !Utils.compare_terms t1 t2 in let stat = (ty,t1,t2,o) in let w = compute_equality_weight stat in - let e = (w, BasicProof proof, stat, [], []) in + let e = (w, BasicProof proof, stat, []) in e | _ -> raise TermIsNotAnEquality @@ -1203,7 +1221,7 @@ let equality_of_term proof term = type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;; let is_weak_identity (metasenv, context, ugraph) = function - | (_, _, (ty, left, right, _), menv, _) -> + | (_, _, (ty, left, right, _), menv) -> (left = right || (meta_convertibility left right)) (* the test below is not a good idea since it stops @@ -1213,7 +1231,7 @@ let is_weak_identity (metasenv, context, ugraph) = function ;; let is_identity (metasenv, context, ugraph) = function - | (_, _, (ty, left, right, _), menv, _) -> + | (_, _, (ty, left, right, _), menv) -> (left = right || (* (meta_convertibility left right)) *) (fst (CicReduction.are_convertible @@ -1222,7 +1240,7 @@ let is_identity (metasenv, context, ugraph) = function let term_of_equality equality = - let _, _, (ty, left, right, _), menv, _ = equality in + let _, _, (ty, left, right, _), menv = equality in let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in let argsno = List.length menv in let t =