X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=9db77c5d526200246379772cd0a9a1d8cf78c67a;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=81e794c8c6f6709c873f6a6b49802b234ec6d7dc;hpb=9945374a5594c068883fa6c775f17b640fcac64d;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 81e794c8c..9db77c5d5 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -25,109 +25,218 @@
 
 open Printf
 
-exception UnificationFailure of string;;
-exception Uncertain of string;;
-exception AssertFailure of string;;
+exception UnificationFailure of string Lazy.t;;
+exception Uncertain of string Lazy.t;;
+exception AssertFailure of string Lazy.t;;
 
-let debug_print = prerr_endline
+let verbose = false;;
+let debug_print = fun _ -> () 
 
-let type_of_aux' metasenv subst context term =
-  try
-    CicMetaSubst.type_of_aux' metasenv subst context term
+let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
+let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
+let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
+let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
+
+let type_of_aux' metasenv subst context term ugraph =
+let foo () =
+  try 
+    CicTypeChecker.type_of_aux' ~subst metasenv context term ugraph 
   with
-  | CicMetaSubst.MetaSubstFailure msg ->
-    raise (AssertFailure
-      ((sprintf
-        "Type checking error: %s in context\n%s\nand metasenv\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms"
-        (CicMetaSubst.ppterm subst term)
-        (CicMetaSubst.ppcontext subst context)
-        (CicMetaSubst.ppmetasenv metasenv subst) msg)))
+      CicTypeChecker.TypeCheckerFailure msg ->
+        let msg =
+         lazy
+          (sprintf
+           "Kernel Type checking error: 
+%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
+             (CicMetaSubst.ppterm subst term)
+             (CicMetaSubst.ppterm [] term)
+             (CicMetaSubst.ppcontext subst context)
+             (CicMetaSubst.ppmetasenv subst metasenv) 
+             (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
+        raise (AssertFailure msg)
+    | CicTypeChecker.AssertFailure msg ->
+        let msg = lazy
+         (sprintf
+           "Kernel Type checking assertion failure: 
+%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
+             (CicMetaSubst.ppterm subst term)
+             (CicMetaSubst.ppterm [] term)
+             (CicMetaSubst.ppcontext subst context)
+             (CicMetaSubst.ppmetasenv subst metasenv) 
+             (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
+        raise (AssertFailure msg)
+in profiler_toa.HExtlib.profile foo ()
+;;
+
+let exists_a_meta l = 
+  List.exists (function Cic.Meta _ -> true | _ -> false) l
 
-let rec beta_expand test_equality_only metasenv subst context t arg =
+let rec deref subst t =
+  let snd (_,a,_) = a in
+  match t with
+      Cic.Meta(n,l) -> 
+        (try 
+           deref subst
+             (CicSubstitution.subst_meta 
+                l (snd (CicUtil.lookup_subst n subst))) 
+         with 
+             CicUtil.Subst_not_found _ -> t)
+    | Cic.Appl(Cic.Meta(n,l)::args) ->
+        (match deref subst (Cic.Meta(n,l)) with
+           | Cic.Lambda _ as t -> 
+               deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
+           | r -> Cic.Appl(r::args))
+    | Cic.Appl(((Cic.Lambda _) as t)::args) ->
+           deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
+    | t -> t
+;; 
+
+let deref subst t =
+ let foo () = deref subst t
+ in profiler_deref.HExtlib.profile foo ()
+
+exception WrongShape;;
+let eta_reduce after_beta_expansion after_beta_expansion_body
+     before_beta_expansion
+ =
+ try
+  match before_beta_expansion,after_beta_expansion_body with
+     Cic.Appl l, Cic.Appl l' ->
+      let rec all_but_last check_last =
+       function
+          [] -> assert false
+        | [Cic.Rel 1] -> []
+        | [_] -> if check_last then raise WrongShape else []
+        | he::tl -> he::(all_but_last check_last tl)
+      in
+       let all_but_last check_last l =
+        match all_but_last check_last l with
+           [] -> assert false
+         | [he] -> he
+         | l -> Cic.Appl l
+       in
+       let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
+       let all_but_last = all_but_last false l in
+        (* here we should test alpha-equivalence; however we know by
+           construction that here alpha_equivalence is equivalent to = *)
+        if t = all_but_last then
+         all_but_last
+        else
+         after_beta_expansion
+   | _,_ -> after_beta_expansion
+ with
+  WrongShape -> after_beta_expansion
+
+let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
  let module S = CicSubstitution in
  let module C = Cic in
-  let rec aux metasenv subst n context t' =
-(*prerr_endline ("1 ciclo di beta_expand arg=" ^ CicMetaSubst.ppterm subst arg ^ " ; term=" ^ CicMetaSubst.ppterm subst t') ;*)
+let foo () =
+  let rec aux metasenv subst n context t' ugraph =
    try
-    let subst,metasenv =
-     fo_unif_subst test_equality_only subst context metasenv arg t'
+
+    let subst,metasenv,ugraph1 =
+     fo_unif_subst test_equality_only subst context metasenv 
+      (CicSubstitution.lift n arg) t' ugraph
+
     in
-     subst,metasenv,C.Rel (1 + n)
+     subst,metasenv,C.Rel (1 + n),ugraph1
    with
       Uncertain _
     | UnificationFailure _ ->
        match t' with
-        | C.Rel m  -> subst,metasenv, if m <= n then C.Rel m else C.Rel (m+1)
+        | C.Rel m  -> subst,metasenv, 
+           (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
         | C.Var (uri,exp_named_subst) ->
-           let subst,metasenv,exp_named_subst' =
-            aux_exp_named_subst metasenv subst n context exp_named_subst
+           let subst,metasenv,exp_named_subst',ugraph1 =
+            aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
            in
-            subst,metasenv,C.Var (uri,exp_named_subst')
-        | C.Meta (i,l) as t->
-           (try
-             let t' = List.assoc i subst in
-              aux metasenv subst n context t'
-            with
-             Not_found -> subst,metasenv,t)
+            subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
+        | C.Meta (i,l) ->
+            (* andrea: in general, beta_expand can create badly typed
+             terms. This happens quite seldom in practice, UNLESS we
+             iterate on the local context. For this reason, we renounce
+             to iterate and just lift *)
+            let l = 
+              List.map 
+                (function
+                     Some t -> Some (CicSubstitution.lift 1 t)
+                   | None -> None) l in
+            subst, metasenv, C.Meta (i,l), ugraph
         | C.Sort _
-        | C.Implicit _ as t -> subst,metasenv,t
+        | C.Implicit _ as t -> subst,metasenv,t,ugraph
         | C.Cast (te,ty) ->
-           let subst,metasenv,te' = aux metasenv subst n context te in
-           let subst,metasenv,ty' = aux metasenv subst n context ty in
-           subst,metasenv,C.Cast (te', ty')
+            let subst,metasenv,te',ugraph1 = 
+              aux metasenv subst n context te ugraph in
+            let subst,metasenv,ty',ugraph2 = 
+              aux metasenv subst n context ty ugraph1 in 
+            (* TASSI: sure this is in serial? *)
+            subst,metasenv,(C.Cast (te', ty')),ugraph2
         | C.Prod (nn,s,t) ->
-           let subst,metasenv,s' = aux metasenv subst n context s in
-           let subst,metasenv,t' =
-            aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
+           let subst,metasenv,s',ugraph1 = 
+             aux metasenv subst n context s ugraph in
+           let subst,metasenv,t',ugraph2 =
+             aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t 
+               ugraph1
            in
-            subst,metasenv,C.Prod (nn, s', t')
+           (* TASSI: sure this is in serial? *)
+           subst,metasenv,(C.Prod (nn, s', t')),ugraph2
         | C.Lambda (nn,s,t) ->
-           let subst,metasenv,s' = aux metasenv subst n context s in
-           let subst,metasenv,t' =
-            aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
+           let subst,metasenv,s',ugraph1 = 
+             aux metasenv subst n context s ugraph in
+           let subst,metasenv,t',ugraph2 =
+            aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
            in
-            subst,metasenv,C.Lambda (nn, s', t')
+           (* TASSI: sure this is in serial? *)
+            subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
         | C.LetIn (nn,s,t) ->
-           let subst,metasenv,s' = aux metasenv subst n context s in
-           let subst,metasenv,t' =
+           let subst,metasenv,s',ugraph1 = 
+             aux metasenv subst n context s ugraph in
+           let subst,metasenv,t',ugraph2 =
             aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
+              ugraph1
            in
-            subst,metasenv,C.LetIn (nn, s', t')
+           (* TASSI: sure this is in serial? *)
+            subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
         | C.Appl l ->
-           let subst,metasenv,revl' =
+           let subst,metasenv,revl',ugraph1 =
             List.fold_left
-             (fun (subst,metasenv,appl) t ->
-               let subst,metasenv,t' = aux metasenv subst n context t in
-                subst,metasenv,t'::appl
-             ) (subst,metasenv,[]) l
+             (fun (subst,metasenv,appl,ugraph) t ->
+               let subst,metasenv,t',ugraph1 = 
+                 aux metasenv subst n context t ugraph in
+                subst,metasenv,(t'::appl),ugraph1
+             ) (subst,metasenv,[],ugraph) l
            in
-            subst,metasenv,C.Appl (List.rev revl')
+            subst,metasenv,(C.Appl (List.rev revl')),ugraph1
         | C.Const (uri,exp_named_subst) ->
-           let subst,metasenv,exp_named_subst' =
-            aux_exp_named_subst metasenv subst n context exp_named_subst
+           let subst,metasenv,exp_named_subst',ugraph1 =
+            aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
            in
-            subst,metasenv,C.Const (uri,exp_named_subst')
+            subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
         | C.MutInd (uri,i,exp_named_subst) ->
-           let subst,metasenv,exp_named_subst' =
-            aux_exp_named_subst metasenv subst n context exp_named_subst
+           let subst,metasenv,exp_named_subst',ugraph1 =
+            aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
            in
-            subst,metasenv,C.MutInd (uri,i,exp_named_subst')
+            subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
         | C.MutConstruct (uri,i,j,exp_named_subst) ->
-           let subst,metasenv,exp_named_subst' =
-            aux_exp_named_subst metasenv subst n context exp_named_subst
+           let subst,metasenv,exp_named_subst',ugraph1 =
+            aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
            in
-            subst,metasenv,C.MutConstruct (uri,i,j,exp_named_subst')
+            subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
         | C.MutCase (sp,i,outt,t,pl) ->
-           let subst,metasenv,outt' = aux metasenv subst n context outt in
-           let subst,metasenv,t' = aux metasenv subst n context t in
-           let subst,metasenv,revpl' =
+           let subst,metasenv,outt',ugraph1 = 
+             aux metasenv subst n context outt ugraph in
+           let subst,metasenv,t',ugraph2 = 
+             aux metasenv subst n context t ugraph1 in
+           let subst,metasenv,revpl',ugraph3 =
             List.fold_left
-             (fun (subst,metasenv,pl) t ->
-               let subst,metasenv,t' = aux metasenv subst n context t in
-                subst,metasenv,t'::pl
-             ) (subst,metasenv,[]) pl
+             (fun (subst,metasenv,pl,ugraph) t ->
+               let subst,metasenv,t',ugraph1 = 
+                 aux metasenv subst n context t ugraph in
+               subst,metasenv,(t'::pl),ugraph1
+             ) (subst,metasenv,[],ugraph2) pl
            in
-           subst,metasenv,C.MutCase (sp,i,outt', t', List.rev revpl')
+           subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
+           (* TASSI: not sure this is serial *)
         | C.Fix (i,fl) ->
 (*CSC: not implemented
            let tylen = List.length fl in
@@ -137,7 +246,8 @@ let rec beta_expand test_equality_only metasenv subst context t arg =
                fl
             in
              C.Fix (i, substitutedfl)
-*) subst,metasenv,CicMetaSubst.lift subst 1 t'
+*)
+            subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
         | C.CoFix (i,fl) ->
 (*CSC: not implemented
            let tylen = List.length fl in
@@ -147,29 +257,40 @@ let rec beta_expand test_equality_only metasenv subst context t arg =
                fl
             in
              C.CoFix (i, substitutedfl)
-*) subst,metasenv,CicMetaSubst.lift subst 1 t'
 
-  and aux_exp_named_subst metasenv subst n context ens =
+*) 
+            subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
+
+  and aux_exp_named_subst metasenv subst n context ens ugraph =
    List.fold_right
-    (fun (uri,t) (subst,metasenv,l) ->
-      let subst,metasenv,t' = aux metasenv subst n context t in
-       subst,metasenv,(uri,t')::l) ens (subst,metasenv,[])
+    (fun (uri,t) (subst,metasenv,l,ugraph) ->
+      let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
+       subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
   in
-   let argty =
-    type_of_aux' metasenv subst context arg
- in
+  let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
   let fresh_name =
-   FreshNamesGenerator.mk_fresh_name
-    metasenv context (Cic.Name "Heta") ~typ:argty
+   FreshNamesGenerator.mk_fresh_name ~subst
+    metasenv context (Cic.Name "Hbeta") ~typ:argty
+  in
+   let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
+   let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
+   subst, metasenv, t'', ugraph2
+in profiler_beta_expand.HExtlib.profile foo ()
+
+
+and beta_expand_many test_equality_only metasenv subst context t args ugraph =
+  let subst,metasenv,hd,ugraph =
+    List.fold_right
+      (fun arg (subst,metasenv,t,ugraph) ->
+         let subst,metasenv,t,ugraph1 =
+           beta_expand test_equality_only 
+             metasenv subst context t arg ugraph 
+         in
+           subst,metasenv,t,ugraph1 
+      ) args (subst,metasenv,t,ugraph) 
   in
-   let subst,metasenv,t' = aux metasenv subst 0 context t in
-    subst,metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg]
+    subst,metasenv,hd,ugraph
 
-and beta_expand_many test_equality_only metasenv subst context t =
- List.fold_left
-  (fun (subst,metasenv,t) arg ->
-    beta_expand test_equality_only metasenv subst context t arg
-  ) (subst,metasenv,t)
 
 (* NUOVA UNIFICAZIONE *)
 (* A substitution is a (int * Cic.term) list that associates a
@@ -180,257 +301,374 @@ and beta_expand_many test_equality_only metasenv subst context t =
    a new substitution which is _NOT_ unwinded. It must be unwinded before
    applying it. *)
 
-and fo_unif_subst test_equality_only subst context metasenv t1 t2 =  
+and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =  
  let module C = Cic in
- let module R = CicMetaSubst in
+ let module R = CicReduction in
  let module S = CicSubstitution in
-  match (t1, t2) with
-     (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
-       let ok,subst,metasenv =
-       try
-        List.fold_left2
-         (fun (b,subst,metasenv) t1 t2 ->
-           if b then true,subst,metasenv else
-            match t1,t2 with
-               None,_
-             | _,None -> true,subst,metasenv
-             | Some t1', Some t2' ->
-                (* First possibility:  restriction    *)
-                (* Second possibility: unification    *)
-                (* Third possibility:  convertibility *)
-                if R.are_convertible subst context t1' t2' then
-                 true,subst,metasenv
-                else
-                 (try
-                   let subst,metasenv =
-                    fo_unif_subst 
-                     test_equality_only subst context metasenv t1' t2'
-                   in
-                    true,subst,metasenv
-                 with
-                  Not_found -> false,subst,metasenv)
-         ) (true,subst,metasenv) ln lm
-       with
-        Invalid_argument _ ->
-         raise (UnificationFailure (sprintf
-           "Error trying to unify %s with %s: the lengths of the two local contexts do not match." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
-       in
-        if ok then
-          subst,metasenv
-        else
-          raise (UnificationFailure (sprintf
-            "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
-            (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
-   | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
-       fo_unif_subst test_equality_only subst context metasenv t2 t1
-   | (C.Meta (n,l), t)   
-   | (t, C.Meta (n,l)) ->
-       let swap =
-        match t1,t2 with
-           C.Meta (n,_), C.Meta (m,_) when n < m -> false
-         | _, C.Meta _ -> false
-         | _,_ -> true
-       in
-       let lower = fun x y -> if swap then y else x in
-       let upper = fun x y -> if swap then x else y in
-       let fo_unif_subst_ordered 
-        test_equality_only subst context metasenv m1 m2 =
-          fo_unif_subst test_equality_only subst context metasenv 
-           (lower m1 m2) (upper m1 m2)
-       in
-        begin
-        try
-         let oldt = (List.assoc n subst) in
-         let lifted_oldt = S.lift_meta l oldt in
-          fo_unif_subst_ordered 
-           test_equality_only subst context metasenv t lifted_oldt
-        with Not_found ->
-         (* First of all we unify the type of the meta with the type of the term *)
-         let subst,metasenv =
-          let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
-          (try
-            let tyt =
-              type_of_aux' metasenv subst context t
-            in
-             fo_unif_subst 
-              test_equality_only 
-               subst context metasenv tyt (S.lift_meta l meta_type)
-          with AssertFailure _ ->
-            (* TODO huge hack!!!!
-             * we keep on unifying/refining in the hope that the problem will be
-             * eventually solved. In the meantime we're breaking a big invariant:
-             * the terms that we are unifying are no longer well typed in the
-             * current context (in the worst case we could even diverge)
-             *)
-(*
-prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN.";
-prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
-*)
-            (subst, metasenv))
+ let t1 = deref subst t1 in
+ let t2 = deref subst t2 in
+ let b,ugraph  = 
+let foo () =
+   R.are_convertible ~subst ~metasenv context t1 t2 ugraph 
+in profiler_are_convertible.HExtlib.profile foo ()
+ in
+   if b then
+     subst, metasenv, ugraph 
+   else
+   match (t1, t2) with
+     | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
+         let _,subst,metasenv,ugraph1 =
+           (try
+              List.fold_left2
+                (fun (j,subst,metasenv,ugraph) t1 t2 ->
+                   match t1,t2 with
+                       None,_
+                     | _,None -> j+1,subst,metasenv,ugraph
+                     | Some t1', Some t2' ->
+                         (* First possibility:  restriction    *)
+                         (* Second possibility: unification    *)
+                         (* Third possibility:  convertibility *)
+                         let b, ugraph1 = 
+                         R.are_convertible 
+                           ~subst ~metasenv context t1' t2' ugraph
+                         in
+                         if b then
+                           j+1,subst,metasenv, ugraph1 
+                         else
+                           (try
+                              let subst,metasenv,ugraph2 =
+                                fo_unif_subst 
+                                  test_equality_only 
+                                  subst context metasenv t1' t2' ugraph
+                              in
+                                j+1,subst,metasenv,ugraph2
+                            with
+                                Uncertain _
+                              | UnificationFailure _ ->
+debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j))); 
+                                  let metasenv, subst = 
+                                    CicMetaSubst.restrict 
+                                      subst [(n,j)] metasenv in
+                                    j+1,subst,metasenv,ugraph1)
+                ) (1,subst,metasenv,ugraph) ln lm
+            with
+                Exit ->
+                  raise 
+                    (UnificationFailure (lazy "1"))
+                    (*
+                    (sprintf
+                      "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
+                      (CicMetaSubst.ppterm subst t1) 
+                      (CicMetaSubst.ppterm subst t2))) *)
+              | Invalid_argument _ ->
+                  raise 
+                    (UnificationFailure (lazy "2")))
+                    (*
+                    (sprintf
+                      "Error trying to unify %s with %s: the lengths of the two local contexts do not match." 
+                      (CicMetaSubst.ppterm subst t1) 
+                      (CicMetaSubst.ppterm subst t2)))) *)
+         in subst,metasenv,ugraph1
+     | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
+         fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
+     | (C.Meta (n,l), t)   
+     | (t, C.Meta (n,l)) ->
+         let swap =
+           match t1,t2 with
+               C.Meta (n,_), C.Meta (m,_) when n < m -> false
+             | _, C.Meta _ -> false
+             | _,_ -> true
          in
-          let t',metasenv,subst =
-           try
-            CicMetaSubst.delift n subst context metasenv l t
+         let lower = fun x y -> if swap then y else x in
+         let upper = fun x y -> if swap then x else y in
+         let fo_unif_subst_ordered 
+             test_equality_only subst context metasenv m1 m2 ugraph =
+           fo_unif_subst test_equality_only subst context metasenv 
+             (lower m1 m2) (upper m1 m2) ugraph
+         in
+         begin
+         let subst,metasenv,ugraph1 =
+           let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
+           (try
+              let tyt,ugraph1 = 
+                type_of_aux' metasenv subst context t ugraph 
+              in
+                fo_unif_subst 
+                  test_equality_only 
+                  subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
+            with 
+                UnificationFailure _ as e -> raise e
+              | Uncertain msg -> raise (UnificationFailure msg)
+              | AssertFailure _ ->
+                  debug_print (lazy "siamo allo huge hack");
+                  (* TODO huge hack!!!!
+                   * we keep on unifying/refining in the hope that 
+                   * the problem will be eventually solved. 
+                   * In the meantime we're breaking a big invariant:
+                   * the terms that we are unifying are no longer well 
+                   * typed in the current context (in the worst case 
+                   * we could even diverge) *)
+                  (subst, metasenv,ugraph)) in
+         let t',metasenv,subst =
+           try 
+             CicMetaSubst.delift n subst context metasenv l t
            with
-              (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
-            | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
-          in
-           let t'' =
-            match t' with
+               (CicMetaSubst.MetaSubstFailure msg)-> 
+                 raise (UnificationFailure msg)
+             | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
+         in
+         let t'',ugraph2 =
+           match t' with
                C.Sort (C.Type u) when not test_equality_only ->
                  let u' = CicUniv.fresh () in
                  let s = C.Sort (C.Type u') in
-                  ignore (CicUniv.add_ge (upper u u') (lower u u')) ;
-                 s
-              | _ -> t'
-           in
-            (* Unifying the types may have already instantiated n. Let's check *)
-            try
-             let oldt = (List.assoc n subst) in
-             let lifted_oldt = S.lift_meta l oldt in
-              fo_unif_subst_ordered 
-               test_equality_only subst context metasenv t lifted_oldt
-            with
-             Not_found -> 
-              (n,t'')::subst, metasenv
-        end
+                 let ugraph2 =   
+                   CicUniv.add_ge (upper u u') (lower u u') ugraph1
+                 in
+                   s,ugraph2
+             | _ -> t',ugraph1
+         in
+         (* Unifying the types may have already instantiated n. Let's check *)
+         try
+           let (_, oldt,_) = CicUtil.lookup_subst n subst in
+           let lifted_oldt = S.subst_meta l oldt in
+             fo_unif_subst_ordered 
+               test_equality_only subst context metasenv t lifted_oldt ugraph2
+         with
+             CicUtil.Subst_not_found _ -> 
+               let (_, context, ty) = CicUtil.lookup_meta n metasenv in
+               let subst = (n, (context, t'',ty)) :: subst in
+               let metasenv =
+                 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
+               subst, metasenv, ugraph2
+         end
    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
       if UriManager.eq uri1 uri2 then
        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
-        exp_named_subst1 exp_named_subst2
+        exp_named_subst1 exp_named_subst2 ugraph
       else
-       raise (UnificationFailure (sprintf
-        "Can't unify %s with %s due to different constants"
-        (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
+       raise (UnificationFailure (lazy 
+          (sprintf
+            "Can't unify %s with %s due to different constants"
+            (CicMetaSubst.ppterm subst t1) 
+            (CicMetaSubst.ppterm subst t2)))) 
    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
-      if UriManager.eq uri1 uri2 && i1 = i2 then
-       fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
-        exp_named_subst1 exp_named_subst2
-      else
-       raise (UnificationFailure (sprintf
-        "Can't unify %s with %s due to different inductive principles"
-        (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
+       if UriManager.eq uri1 uri2 && i1 = i2 then
+         fo_unif_subst_exp_named_subst 
+           test_equality_only 
+           subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
+       else
+         raise (UnificationFailure (lazy "4"))
+           (* (sprintf
+              "Can't unify %s with %s due to different inductive principles"
+              (CicMetaSubst.ppterm subst t1) 
+              (CicMetaSubst.ppterm subst t2))) *)
    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
-     C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
-      if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
-       fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
-        exp_named_subst1 exp_named_subst2
-      else
-       raise (UnificationFailure (sprintf
-        "Can't unify %s with %s due to different inductive constructors"
-        (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
+       C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
+       if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
+         fo_unif_subst_exp_named_subst
+           test_equality_only 
+           subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
+       else
+         raise (UnificationFailure (lazy "5"))
+           (* (sprintf
+              "Can't unify %s with %s due to different inductive constructors"
+              (CicMetaSubst.ppterm subst t1) 
+              (CicMetaSubst.ppterm subst t2))) *)
    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only 
-                              subst context metasenv te t2
+                              subst context metasenv te t2 ugraph
    | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only 
-                              subst context metasenv t1 te
+                              subst context metasenv t1 te ugraph
    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> 
-        (* TASSI: this is the only case in which we want == *)
-       let subst',metasenv' = fo_unif_subst true 
-                               subst context metasenv s1 s2 in
-        fo_unif_subst test_equality_only 
-	 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
+       let subst',metasenv',ugraph1 = 
+         fo_unif_subst true subst context metasenv s1 s2 ugraph 
+       in
+         fo_unif_subst test_equality_only 
+           subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> 
-        (* TASSI: ask someone a reason for not putting true here *)
-       let subst',metasenv' = fo_unif_subst test_equality_only 
-                               subst context metasenv s1 s2 in
-        fo_unif_subst test_equality_only 
-	 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
+       let subst',metasenv',ugraph1 = 
+         fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph 
+       in
+         fo_unif_subst test_equality_only 
+           subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
    | (C.LetIn (_,s1,t1), t2)  
    | (t2, C.LetIn (_,s1,t1)) -> 
        fo_unif_subst 
-        test_equality_only subst context metasenv t2 (S.subst s1 t1)
+        test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
    | (C.Appl l1, C.Appl l2) -> 
-       let subst,metasenv,t1',t2' =
-        match l1,l2 with
-           C.Meta (i,_)::_, C.Meta (j,_)::_ when i = j ->
-             subst,metasenv,t1,t2
-         (* In the first two cases when we reach the next begin ... end
-            section useless work is done since, by construction, the list
-            of arguments will be equal.
-         *)
-         | C.Meta (i,l)::args, _ ->
-            let subst,metasenv,t2' =
-             beta_expand_many test_equality_only metasenv subst context t2 args
-            in
-             subst,metasenv,t1,t2'
-         | _, C.Meta (i,l)::args ->
-            let subst,metasenv,t1' =
-             beta_expand_many test_equality_only metasenv subst context t1 args
-            in
-             subst,metasenv,t1',t2
-         | _,_ ->
-             subst,metasenv,t1,t2
-       in
-        begin
-         match t1',t2' with
-            C.Appl l1, C.Appl l2 ->
-             let lr1 = List.rev l1 in
-             let lr2 = List.rev l2 in
-             let rec fo_unif_l test_equality_only subst metasenv =
-              function
-                 [],_
-               | _,[] -> assert false
-               | ([h1],[h2]) ->
-                   fo_unif_subst test_equality_only subst context metasenv h1 h2
-               | ([h],l) 
-               | (l,[h]) ->
-                  fo_unif_subst 
-	           test_equality_only subst context metasenv h (C.Appl (List.rev l))
-               | ((h1::l1),(h2::l2)) -> 
-                  let subst', metasenv' = 
-                   fo_unif_subst test_equality_only subst context metasenv h1 h2
-                  in 
-                   fo_unif_l test_equality_only subst' metasenv' (l1,l2)
-             in
-              fo_unif_l test_equality_only subst metasenv (lr1, lr2) 
-          | _ -> assert false
-        end
+       (* andrea: this case should be probably rewritten in the 
+          spirit of deref *)
+       (match l1,l2 with
+          | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
+              (try 
+                 List.fold_left2 
+                   (fun (subst,metasenv,ugraph) t1 t2 ->
+                      fo_unif_subst 
+                        test_equality_only subst context metasenv t1 t2 ugraph)
+                   (subst,metasenv,ugraph) l1 l2 
+               with (Invalid_argument msg) -> 
+                 raise (UnificationFailure (lazy msg)))
+          | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
+              (* we verify that none of the args is a Meta, 
+                since beta expanding with respoect to a metavariable 
+                makes no sense  *)
+ (*
+              (try 
+                 let (_,t,_) = CicUtil.lookup_subst i subst in
+                 let lifted = S.subst_meta l t in
+                 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
+                   fo_unif_subst 
+                    test_equality_only 
+                     subst context metasenv reduced t2 ugraph
+               with CicUtil.Subst_not_found _ -> *)
+              let subst,metasenv,beta_expanded,ugraph1 =
+                beta_expand_many 
+                  test_equality_only metasenv subst context t2 args ugraph 
+              in
+                fo_unif_subst test_equality_only subst context metasenv 
+                  (C.Meta (i,l)) beta_expanded ugraph1
+          | _, C.Meta (i,l)::args when not(exists_a_meta args)  ->
+              (* (try 
+                 let (_,t,_) = CicUtil.lookup_subst i subst in
+                 let lifted = S.subst_meta l t in
+                 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
+                   fo_unif_subst 
+                     test_equality_only 
+                     subst context metasenv t1 reduced ugraph
+               with CicUtil.Subst_not_found _ -> *)
+                 let subst,metasenv,beta_expanded,ugraph1 =
+                   beta_expand_many 
+                     test_equality_only 
+                     metasenv subst context t1 args ugraph 
+                 in
+                   fo_unif_subst test_equality_only subst context metasenv 
+                     (C.Meta (i,l)) beta_expanded ugraph1
+          | _,_ ->
+              let lr1 = List.rev l1 in
+              let lr2 = List.rev l2 in
+              let rec 
+                  fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
+                match (l1,l2) with
+                    [],_
+                  | _,[] -> assert false
+                  | ([h1],[h2]) ->
+                      fo_unif_subst 
+                        test_equality_only subst context metasenv h1 h2 ugraph
+                  | ([h],l) 
+                  | (l,[h]) ->
+                      fo_unif_subst test_equality_only subst context metasenv
+                        h (C.Appl (List.rev l)) ugraph
+                  | ((h1::l1),(h2::l2)) -> 
+                      let subst', metasenv',ugraph1 = 
+                        fo_unif_subst 
+                          test_equality_only 
+                          subst context metasenv h1 h2 ugraph
+                      in 
+                        fo_unif_l 
+                          test_equality_only subst' metasenv' (l1,l2) ugraph1
+              in
+                fo_unif_l 
+                  test_equality_only subst metasenv (lr1, lr2)  ugraph)
    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
-       let subst', metasenv' = 
-        fo_unif_subst test_equality_only subst context metasenv outt1 outt2 in
-       let subst'',metasenv'' = 
-        fo_unif_subst test_equality_only subst' context metasenv' t1' t2' in
+       let subst', metasenv',ugraph1 = 
+        fo_unif_subst test_equality_only subst context metasenv outt1 outt2
+          ugraph in
+       let subst'',metasenv'',ugraph2 = 
+        fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
+          ugraph1 in
        (try
          List.fold_left2 
-          (function (subst,metasenv) ->
-            fo_unif_subst test_equality_only subst context metasenv
-          ) (subst'',metasenv'') pl1 pl2 
+          (fun (subst,metasenv,ugraph) t1 t2 ->
+            fo_unif_subst 
+             test_equality_only subst context metasenv t1 t2 ugraph
+          ) (subst'',metasenv'',ugraph2) pl1 pl2 
         with
          Invalid_argument _ ->
-          raise (UnificationFailure (sprintf
-            "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))))
-   | (C.Rel _, _) | (_,  C.Rel _)
+          raise (UnificationFailure (lazy "6.1")))
+           (* (sprintf
+              "Error trying to unify %s with %s: the number of branches is not the same." 
+              (CicMetaSubst.ppterm subst t1) 
+              (CicMetaSubst.ppterm subst t2)))) *)
+   | (C.Rel _, _) | (_,  C.Rel _) ->
+       if t1 = t2 then
+         subst, metasenv,ugraph
+       else
+        raise (UnificationFailure (lazy 
+           (sprintf
+             "Can't unify %s with %s because they are not convertible"
+             (CicMetaSubst.ppterm subst t1) 
+             (CicMetaSubst.ppterm subst t2))))
+   | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
+       let subst,metasenv,beta_expanded,ugraph1 =
+         beta_expand_many 
+           test_equality_only metasenv subst context t2 args ugraph 
+       in
+         fo_unif_subst test_equality_only subst context metasenv 
+           (C.Meta (i,l)) beta_expanded ugraph1
+   | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
+       let subst,metasenv,beta_expanded,ugraph1 =
+         beta_expand_many 
+           test_equality_only metasenv subst context t1 args ugraph 
+       in
+         fo_unif_subst test_equality_only subst context metasenv 
+           beta_expanded (C.Meta (i,l)) ugraph1
    | (C.Sort _ ,_) | (_, C.Sort _)
    | (C.Const _, _) | (_, C.Const _)
    | (C.MutInd  _, _) | (_, C.MutInd _)
    | (C.MutConstruct _, _) | (_, C.MutConstruct _)
    | (C.Fix _, _) | (_, C.Fix _) 
    | (C.CoFix _, _) | (_, C.CoFix _) -> 
-       if R.are_convertible subst context t1 t2 then
-        subst, metasenv
-       else
-        raise (UnificationFailure (sprintf
-          "Can't unify %s with %s because they are not convertible"
-          (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
+       if t1 = t2 then
+         subst, metasenv, ugraph
+       else 
+         let b,ugraph1 = 
+           R.are_convertible ~subst ~metasenv context t1 t2 ugraph 
+         in
+           if b then 
+             subst, metasenv, ugraph1
+           else
+             raise
+                (UnificationFailure (lazy (sprintf
+                  "Can't unify %s with %s because they are not convertible"
+                  (CicMetaSubst.ppterm subst t1) 
+                  (CicMetaSubst.ppterm subst t2))))
+   | (C.Prod _, t2) ->
+       let t2' = R.whd ~subst context t2 in
+       (match t2' with
+            C.Prod _ -> 
+              fo_unif_subst test_equality_only 
+                subst context metasenv t1 t2' ugraph         
+          | _ -> raise (UnificationFailure (lazy "8")))
+   | (t1, C.Prod _) ->
+       let t1' = R.whd ~subst context t1 in
+       (match t1' with
+            C.Prod _ -> 
+              fo_unif_subst test_equality_only 
+                subst context metasenv t1' t2 ugraph         
+          | _ -> (* raise (UnificationFailure "9")) *)
+             raise 
+                (UnificationFailure (lazy (sprintf
+                   "Can't unify %s with %s because they are not convertible"
+                   (CicMetaSubst.ppterm subst t1) 
+                   (CicMetaSubst.ppterm subst t2)))))
    | (_,_) ->
-       if R.are_convertible subst context t1 t2 then
-        subst, metasenv
-       else
-        raise (UnificationFailure (sprintf
-          "Can't unify %s with %s because they are not convertible"
-          (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
+       raise (UnificationFailure (lazy "10"))
+         (* (sprintf
+            "Can't unify %s with %s because they are not convertible"
+            (CicMetaSubst.ppterm subst t1) 
+            (CicMetaSubst.ppterm subst t2))) *)
 
 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
- exp_named_subst1 exp_named_subst2
+ exp_named_subst1 exp_named_subst2 ugraph
 =
  try
   List.fold_left2
-   (fun (subst,metasenv) (uri1,t1) (uri2,t2) ->
+   (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
      assert (uri1=uri2) ;
-     fo_unif_subst test_equality_only subst context metasenv t1 t2
-   ) (subst,metasenv) exp_named_subst1 exp_named_subst2
+     fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
+   ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
  with
   Invalid_argument _ ->
    let print_ens ens =
@@ -440,8 +678,8 @@ and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
          UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
        ) ens) 
    in
-    raise (UnificationFailure (sprintf
-     "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2)))
+    raise (UnificationFailure (lazy (sprintf
+     "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2))))
 
 (* A substitution is a (int * Cic.term) list that associates a               *)
 (* metavariable i with its body.                                             *)
@@ -450,27 +688,61 @@ and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 (* a new substitution which is already unwinded and ready to be applied and  *)
 (* a new metasenv in which some hypothesis in the contexts of the            *)
 (* metavariables may have been restricted.                                   *)
-let fo_unif metasenv context t1 t2 = 
- fo_unif_subst false [] context metasenv t1 t2 ;;
+let fo_unif metasenv context t1 t2 ugraph = 
+ fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
 
-let fo_unif_subst subst context metasenv t1 t2 =
-  let enrich_msg msg =
-    sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
-      (CicMetaSubst.ppterm subst t1)
-      (try
-        CicPp.ppterm (type_of_aux' metasenv subst context t1)
-      with _ -> "MALFORMED")
-      (CicMetaSubst.ppterm subst t2)
-      (try
-        CicPp.ppterm (type_of_aux' metasenv subst context t2)
-      with _ -> "MALFORMED")
-      (CicMetaSubst.ppcontext subst context)
-      (CicMetaSubst.ppmetasenv metasenv subst) msg
-  in
+let enrich_msg msg subst context metasenv t1 t2 ugraph =
+ lazy (
+  if verbose then
+   sprintf "[Verbose] Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s"
+    (CicMetaSubst.ppterm subst t1)
+    (try
+      let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
+      CicPp.ppterm ty_t1
+    with 
+    | UnificationFailure s
+    | Uncertain s
+    | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
+    (CicMetaSubst.ppterm subst t2)
+    (try
+      let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
+      CicPp.ppterm ty_t2
+    with
+    | UnificationFailure s
+    | Uncertain s
+    | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
+    (CicMetaSubst.ppcontext subst context)
+    (CicMetaSubst.ppmetasenv subst metasenv)
+    (CicMetaSubst.ppsubst subst) (Lazy.force msg)
+ else
+   sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
+    (CicMetaSubst.ppterm_in_context subst t1 context)
+    (try
+      let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
+      CicMetaSubst.ppterm_in_context subst ty_t1 context
+    with 
+    | UnificationFailure s
+    | Uncertain s
+    | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
+    (CicMetaSubst.ppterm_in_context subst t2 context)
+    (try
+      let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
+      CicMetaSubst.ppterm_in_context subst ty_t2 context
+    with
+    | UnificationFailure s
+    | Uncertain s
+    | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
+    (CicMetaSubst.ppcontext subst context)
+    (CicMetaSubst.ppmetasenv subst metasenv)
+    (Lazy.force msg)
+ )
+
+let fo_unif_subst subst context metasenv t1 t2 ugraph =
   try
-    fo_unif_subst false subst context metasenv t1 t2
+    fo_unif_subst false subst context metasenv t1 t2 ugraph
   with
-  | AssertFailure msg -> raise (AssertFailure (enrich_msg msg))
-  | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg))
+  | AssertFailure msg ->
+     raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
+  | UnificationFailure msg ->
+     raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
 ;;
-