hints work better now

diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend
index 89e6fd7e9eb3a044a4e0b15b16ce70f959bd04e2..11418eb59a6da77b9b144c2b74d6799687e80119 100644 (file)
--- 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 c797b2eee6d752ca6a5e868384d0c26ba3465663..7961be96a80a234afed831403bdfb11cb7586de1 100644 (file)
--- 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 d224e6b0e25b1442085ed5dadea99a8e2a4b637f..54b784caae96b84d1ea88e9933938f8b1240c450 100644 (file)
--- 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.