Procedural: we added the support for rendering definitions and axioms

[helm.git] / helm / software / components / cic_unification / cicUnification.ml

diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index 517c013d42b2ac4ffcb6fe7973725561d0fa01da..2bcb099370029d4a418bbb28ca28f1b5c7e53c5e 100644 (file)
--- a/helm/software/components/cic_unification/cicUnification.ml
+++ b/helm/software/components/cic_unification/cicUnification.ml
@@ -594,51 +594,85 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
               | UnificationFailure s
               | Uncertain s as exn -> 
                   (match l1, l2 with
-                  | (((Cic.Const (uri1, ens1)) as c1) :: tl1), 
-                     (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
-                    CoercDb.is_a_coercion' c1 && 
-                    CoercDb.is_a_coercion' c2 &&
+                  | (((Cic.Const (uri1, ens1)) as cc1) :: tl1), 
+                     (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
+                    CoercDb.is_a_coercion cc1 <> None && 
+                    CoercDb.is_a_coercion cc2 <> None &&
                     not (UriManager.eq uri1 uri2) ->
-(*DEBUGGING ONLY:
+(*DEBUGGING ONLY: 
 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
 let res =
-*)
-                     let rec look_for_first_coercion c tl =
-                      match
-                       CicMetaSubst.apply_subst subst (HExtlib.list_last tl)
-                      with
-                         Cic.Appl ((Cic.Const (uri1,ens1) as c')::tl')
-                          when CoercDb.is_a_coercion' c' ->
-                           look_for_first_coercion c' tl'
-                       | last_tl -> c,last_tl
+        *)
+                     let inner_coerced t =
+                      let t = CicMetaSubst.apply_subst subst t in
+                      let rec aux c x t =
+                        match t with
+                        | Cic.Appl l -> 
+                            (match CoercGraph.coerced_arg l with
+                            | None -> c, x
+                            | Some (t,_) -> aux (List.hd l) t t)
+                        | _ ->  c, x
+                      in
+                      aux (Cic.Implicit None) (Cic.Implicit None) t
                      in
-                      let c1,last_tl1 = look_for_first_coercion c1 tl1 in 
-                      let c2,last_tl2 = look_for_first_coercion c2 tl2 in
-                      let car1 =
-                        CoercDb.coerc_carr_of_term (CoercGraph.source_of c1) in
-                      let car2 = 
-                        CoercDb.coerc_carr_of_term (CoercGraph.source_of c2) in
+                      let c1,last_tl1 = inner_coerced (Cic.Appl l1) in 
+                      let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
+                      let car1, car2 =
+                        match 
+                          CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
+                        with
+                        | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
+                        | _ -> assert false
+                      in
+                      let head1_c, head2_c =
+                        match 
+                          CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
+                        with
+                        | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
+                        | _ -> assert false
+                      in
+                      let unfold uri ens args =
+                        let o, _ = 
+                          CicEnvironment.get_obj CicUniv.oblivion_ugraph uri 
+                        in
+                        assert (ens = []);
+                        match o with
+                        | Cic.Constant (_,Some bo,_,_,_) -> 
+                            CicReduction.head_beta_reduce ~delta:false
+                              (Cic.Appl (bo::args))
+                        | _ -> assert false
+                      in
                       if CoercDb.eq_carr car1 car2 then
-                       (match last_tl1,last_tl2 with
-                           C.Meta (i1,_),C.Meta(i2,_) when i1=i2 -> raise exn
-                         | C.Meta _, _
-                         | _, C.Meta _ ->
+                         match last_tl1,last_tl2 with
+                         | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
+                         | _, C.Meta _
+                         | C.Meta _, _ ->
                            let subst,metasenv,ugraph =
                             fo_unif_subst test_equality_only subst context
                              metasenv last_tl1 last_tl2 ugraph
                            in
                             fo_unif_subst test_equality_only subst context
-                             metasenv (C.Appl l1) (C.Appl l2) ugraph
-                         | _ -> raise exn)
+                             metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
+                         | _ when CoercDb.eq_carr head1_c head2_c ->
+                           let l1, l2 = 
+                               (* composite VS composition + metas avoiding
+                                * coercions not only in coerced position *)
+                               if c1 = cc1 then 
+                                 unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
+                               else Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
+                           in
+                            fo_unif_subst test_equality_only subst context
+                             metasenv l1 l2 ugraph
+                         | _ -> raise exn
                       else
                        let meets = 
                          CoercGraph.meets metasenv subst context car1 car2 
                        in
-                        (match meets with
+                       (match meets with
                         | [] -> raise exn
                         | (carr,metasenv,to1,to2)::xxx -> 
                           (match xxx with
-                          [] -> ()
+                          | [] -> ()
                           | (m2,_,c2,c2')::_ ->
                           let m1,_,c1,c1' = carr,metasenv,to1,to2 in
                           let unopt = 
@@ -647,10 +681,10 @@ let res =
                           in
                           HLog.warn 
                             ("There are two minimal joins of "^
-                            CoercDb.name_of_carr car1^" and "^
-                            CoercDb.name_of_carr car2^": " ^ 
-                            CoercDb.name_of_carr m1 ^ " via "^unopt c1^" + "^
-                            unopt c1'^" and " ^ CoercDb.name_of_carr m2^" via "^
+                            CoercDb.string_of_carr car1^" and "^
+                            CoercDb.string_of_carr car2^": " ^ 
+                            CoercDb.string_of_carr m1 ^ " via "^unopt c1^" + "^
+                            unopt c1'^" and "^CoercDb.string_of_carr m2^" via "^
                             unopt c2^" + "^unopt c2'));
                           let last_tl1',(subst,metasenv,ugraph) =
                            match last_tl1,to1 with
@@ -683,6 +717,7 @@ let subst,metasenv,ugraph = res in
 prerr_endline (">>>> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
 res
 *)
+
                   (*CSC: This is necessary because of the "elim H" tactic
                          where the type of H is only reducible to an
                          inductive type. This could be extended from inductive