From c75bfa659bee91e9b12a2a4f856673b94a29d2db Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 16 Dec 2008 19:13:46 +0000 Subject: [PATCH] hints work better now --- helm/software/components/ng_refiner/.depend | 6 +- .../components/ng_refiner/nCicUnifHint.ml | 56 +++++++++++++--- helm/software/matita/tests/pullback.ma | 67 ++++++++++++++----- 3 files changed, 104 insertions(+), 25 deletions(-) diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend index 89e6fd7e9..11418eb59 100644 --- a/helm/software/components/ng_refiner/.depend +++ b/helm/software/components/ng_refiner/.depend @@ -1,3 +1,5 @@ +nCicUnification.cmi: nCicUnifHint.cmi +nCicRefiner.cmi: nCicUnifHint.cmi nDiscriminationTree.cmo: nDiscriminationTree.cmi nDiscriminationTree.cmx: nDiscriminationTree.cmi nCicMetaSubst.cmo: nCicMetaSubst.cmi @@ -6,7 +8,7 @@ nCicCoercion.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicCoercion.cmi nCicCoercion.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicCoercion.cmi nCicUnifHint.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicUnifHint.cmi nCicUnifHint.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicUnifHint.cmi -nCicUnification.cmo: nCicMetaSubst.cmi nCicUnification.cmi -nCicUnification.cmx: nCicMetaSubst.cmx nCicUnification.cmi +nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi +nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi nCicRefiner.cmo: nCicUnification.cmi nCicMetaSubst.cmi nCicRefiner.cmi nCicRefiner.cmx: nCicUnification.cmx nCicMetaSubst.cmx nCicRefiner.cmi diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml index c797b2eee..7961be96a 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.ml +++ b/helm/software/components/ng_refiner/nCicUnifHint.ml @@ -57,16 +57,56 @@ let index_hint hdb context t1 t2 = let empty_db = DB.empty ;; let db () = - let _,_,_,x,_,_ = NCicEnvironment.get_checked_def - (NReference.reference_of_string "cic:/matita/tests/pullback/xxx.def(0)") + let combine f cmp l1 l2 = + List.flatten + (List.map + (fun u1 -> + HExtlib.filter_map + (fun u2 -> if cmp u1 u2 then None else Some (f u1 u2)) l2) + l1) in - let rec decontextualize ctx = function - | NCic.Prod (n,s,t) -> decontextualize ((n,NCic.Decl s)::ctx) t - | t -> ctx, t + let mk_hint (u1,_,_) (u2,_,_) = + let l = OCic2NCic.convert_obj u1 + (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph u1)) in + let r = OCic2NCic.convert_obj u2 + (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph u2)) in + match List.hd l,List.hd r with + | (_,_,_,_,NCic.Constant (_,_,Some l,_,_)), + (_,_,_,_,NCic.Constant (_,_,Some r,_,_)) -> + let rec aux ctx t1 t2 = + match t1, t2 with + | NCic.Lambda (n1,s1,b1), NCic.Lambda(_,s2,b2) -> + if NCicReduction.are_convertible ~subst:[] ~metasenv:[] ctx s1 s2 + then aux ((n1, NCic.Decl s1) :: ctx) b1 b2 + else None + | b1,b2 -> + if NCicReduction.are_convertible ~subst:[] ~metasenv:[] ctx b1 b2 + then begin +(* + prerr_endline ("hint: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] + ~context:ctx b1 ^ " === " ^ NCicPp.ppterm ~metasenv:[] + ~subst:[] ~context:ctx b2); +*) + Some (ctx,b1,b2) + end else None + in + aux [] l r + | _ -> None + in + let hints = + List.fold_left + (fun acc (_,_,l) -> + acc @ + if List.length l > 1 then + combine mk_hint (fun (u1,_,_) (u2,_,_) -> UriManager.eq u1 u2) l l + else []) + [] (CoercDb.to_list ()) in - match (decontextualize [] x) with - | ctx, NCic.Appl [_;_;a;b] -> index_hint empty_db ctx a b - | _ -> assert false + List.fold_left + (fun db -> function + |None -> db + | Some (ctx,b1,b2) -> index_hint db ctx b1 b2) + empty_db hints ;; diff --git a/helm/software/matita/tests/pullback.ma b/helm/software/matita/tests/pullback.ma index d224e6b0e..54b784caa 100644 --- a/helm/software/matita/tests/pullback.ma +++ b/helm/software/matita/tests/pullback.ma @@ -1,16 +1,27 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) + +(* +axiom A : Type. +axiom B : Type. +axiom B1 : Type. +axiom C : Type. + +axiom f1 : A → B. +axiom f2 : A → B1. +axiom f3 : B → C. +axiom f4 : B1 → C. + +coercion f1. +coercion f2. +coercion f3. +coercion f4. + + + + +axiom P : Prop. + +lemma x : P. +*) include "logic/equality.ma". @@ -25,7 +36,7 @@ record R : Type \def { }. record LR_ : Type \def { - lr_L : L ; + lr_L :> L ; lr_R_ : R ; lr_w : r_c lr_R_ = l_c lr_L }. @@ -36,14 +47,40 @@ intros;constructor 1; |rewrite < (lr_w l);apply (r_op (lr_R_ l));] qed. +(* +axiom F : Prop → Prop. +axiom C : Prop → Prop. + +axiom daemon : ∀x.F x = C x. + +lemma xxx : ∀x.F x = C x. apply daemon; qed. + +axiom yyyy : ∀x.C (C x) = C (C x) → F (F x) = F (F x). + +coercion yyyy. + +lemma x : ∀x. (λy:F (F x) = F (F x).True) (refl_eq ? (C (C x))). + +include "nat/factorial.ma". +lemma xxx : 8! = 8 * 7!. intros; reflexivity; qed. + +lemma x : (λy:8!=8!.True) (refl_eq ? (8 * 7!)). +apply (refl_eq ??); +*) + +(* lemma xxx : \forall x. r_c (lr_R x) = l_c (lr_L x). intros; reflexivity; qed. +*) -coercion lr_L. +definition Prop_OR_LR_1 : LR_ → Prop. +apply (λx.r_c (lr_R x)). +qed. +coercion Prop_OR_LR_1. coercion lr_R. lemma foo : \forall x,y.l_op ? x (r_op ? x y) = x. -- 2.39.2