Big bug fixed: in the case t <?= ?1, the instantiation ?1 := t was generated

[helm.git] / helm / ocaml / cic_unification / cicUnification.ml

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index e0ec5cb447d0c30d43ac5fd1cd883b1c24b098d7..b9f87cf9a14a4f4b3e27ecb9d2524cc90fb25471 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -25,20 +25,23 @@
 
 open Printf
 
 
 open Printf
 

-exception AssertFailure of string;;

 exception UnificationFailure of string;;
 exception UnificationFailure of string;;

+exception Uncertain of string;;
+exception AssertFailure of string;;

 
 let debug_print = prerr_endline
 
 let type_of_aux' metasenv subst context term =
   try
     CicMetaSubst.type_of_aux' metasenv subst context term
 
 let debug_print = prerr_endline
 
 let type_of_aux' metasenv subst context term =
   try
     CicMetaSubst.type_of_aux' metasenv subst context term

-  with CicMetaSubst.MetaSubstFailure msg ->
+  with
+  | CicMetaSubst.MetaSubstFailure msg ->

     raise (AssertFailure
       ((sprintf
     raise (AssertFailure
       ((sprintf

-        "Type checking error: %s in context\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms"
-        (CicPp.ppterm (CicMetaSubst.apply_subst subst term))
-        (CicMetaSubst.ppcontext subst context) msg)))
+        "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)))

 
 (* NUOVA UNIFICAZIONE *)
 (* A substitution is a (int * Cic.term) list that associates a
 
 (* NUOVA UNIFICAZIONE *)
 (* A substitution is a (int * Cic.term) list that associates a


@@ -55,43 +58,88 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
  let module S = CicSubstitution in
   match (t1, t2) with
      (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
  let module S = CicSubstitution in
   match (t1, t2) with
      (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->

-       let ok =
+       let ok,subst,metasenv =
+       try

         List.fold_left2
         List.fold_left2

-         (fun b t1 t2 ->
-           b &&
+         (fun (b,subst,metasenv) t1 t2 ->
+           if b then true,subst,metasenv else

             match t1,t2 with
                None,_
             match t1,t2 with
                None,_

-             | _,None -> true
+             | _,None -> true,subst,metasenv

              | Some t1', Some t2' ->
                 (* First possibility:  restriction    *)
                 (* Second possibility: unification    *)
                 (* Third possibility:  convertibility *)
              | Some t1', Some t2' ->
                 (* First possibility:  restriction    *)
                 (* Second possibility: unification    *)
                 (* Third possibility:  convertibility *)

-                R.are_convertible subst context t1' t2'
-         ) true ln lm
+                if R.are_convertible subst context t1' t2' then
+                 true,subst,metasenv
+                else
+                 (try
+                   let subst,metasenv =
+                    fo_unif_subst 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
        in
         if ok then
           subst,metasenv
         else
           raise (UnificationFailure (sprintf

-            "Error trying to unify %s with %s: the algorithm only tried to check convertibility of the two substitutions"
-            (CicPp.ppterm t1) (CicPp.ppterm t2)))
-   | (C.Meta (n,l), C.Meta (m,_)) when n>m ->
+            "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 subst context metasenv t2 t1
    | (C.Meta (n,l), t)   
    | (t, C.Meta (n,l)) ->
        fo_unif_subst subst context metasenv t2 t1
    | (C.Meta (n,l), t)   
    | (t, C.Meta (n,l)) ->

-       let subst',metasenv' =
+       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 subst context metasenv m1 m2 =
+          fo_unif_subst subst context metasenv (lower m1 m2) (upper m1 m2)
+       in
+       let subst'',metasenv' =

         try
          let oldt = (List.assoc n subst) in
          let lifted_oldt = S.lift_meta l oldt in
         try
          let oldt = (List.assoc n subst) in
          let lifted_oldt = S.lift_meta l oldt in

-          fo_unif_subst subst context metasenv lifted_oldt t
+          fo_unif_subst_ordered subst context metasenv t lifted_oldt

         with Not_found ->
         with Not_found ->

-         let t',metasenv' = CicMetaSubst.delift context metasenv l t in
-          (n, t')::subst, metasenv'
+         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
+         (n, t')::subst', metasenv'

        in
        in

-        let (_,_,meta_type) = 
-         List.find (function (m,_,_) -> m=n) metasenv' in
-        let tyt = type_of_aux' metasenv' subst' context t in
-         fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt
+        let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv' in
+        (try
+          let tyt =
+            type_of_aux' metasenv' subst'' context t
+          in
+           fo_unif_subst 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'))

    | (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
    | (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


@@ -100,7 +148,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
       else
        raise (UnificationFailure (sprintf
         "Can't unify %s with %s due to different constants"
       else
        raise (UnificationFailure (sprintf
         "Can't unify %s with %s due to different constants"

-        (CicPp.ppterm t1) (CicPp.ppterm t1)))
+        (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 subst context metasenv
    | 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 subst context metasenv


@@ -108,7 +156,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
       else
        raise (UnificationFailure (sprintf
         "Can't unify %s with %s due to different inductive principles"
       else
        raise (UnificationFailure (sprintf
         "Can't unify %s with %s due to different inductive principles"

-        (CicPp.ppterm t1) (CicPp.ppterm t1)))
+        (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
    | 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


@@ -117,8 +165,8 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
       else
        raise (UnificationFailure (sprintf
         "Can't unify %s with %s due to different inductive constructors"
       else
        raise (UnificationFailure (sprintf
         "Can't unify %s with %s due to different inductive constructors"

-        (CicPp.ppterm t1) (CicPp.ppterm t1)))
-   | (C.Implicit, _) | (_, C.Implicit) ->  assert false
+        (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
+   | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false

    | (C.Cast (te,ty), t2) -> fo_unif_subst subst context metasenv te t2
    | (t1, C.Cast (te,ty)) -> fo_unif_subst subst context metasenv t1 te
    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> 
    | (C.Cast (te,ty), t2) -> fo_unif_subst subst context metasenv te t2
    | (t1, C.Cast (te,ty)) -> fo_unif_subst subst context metasenv t1 te
    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> 


@@ -149,15 +197,20 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
              fo_unif_l subst' metasenv' (l1,l2)
        in
         fo_unif_l subst metasenv (lr1, lr2) 
              fo_unif_l subst' metasenv' (l1,l2)
        in
         fo_unif_l subst metasenv (lr1, lr2) 

-   | (C.MutCase (_,_,outt1,t1,pl1), C.MutCase (_,_,outt2,t2,pl2))->
+   | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->

        let subst', metasenv' = 
         fo_unif_subst subst context metasenv outt1 outt2 in
        let subst'',metasenv'' = 
        let subst', metasenv' = 
         fo_unif_subst subst context metasenv outt1 outt2 in
        let subst'',metasenv'' = 

-        fo_unif_subst subst' context metasenv' t1 t2 in
-       List.fold_left2 
-        (function (subst,metasenv) ->
-          fo_unif_subst subst context metasenv
-        ) (subst'',metasenv'') pl1 pl2 
+        fo_unif_subst subst' context metasenv' t1' t2' in
+       (try
+         List.fold_left2 
+          (function (subst,metasenv) ->
+            fo_unif_subst subst context metasenv
+          ) (subst'',metasenv'') 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 _)
    | (C.Sort _ ,_) | (_, C.Sort _)
    | (C.Const _, _) | (_, C.Const _)
    | (C.Rel _, _) | (_,  C.Rel _)
    | (C.Sort _ ,_) | (_, C.Sort _)
    | (C.Const _, _) | (_, C.Const _)


@@ -170,29 +223,35 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
        else
         raise (UnificationFailure (sprintf
           "Can't unify %s with %s because they are not convertible"
        else
         raise (UnificationFailure (sprintf
           "Can't unify %s with %s because they are not convertible"

-          (CicPp.ppterm t1) (CicPp.ppterm t2)))
+          (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"
    | (_,_) ->
        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"

-          (CicPp.ppterm t1) (CicPp.ppterm t2)))
+          (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))

 
 and fo_unif_subst_exp_named_subst subst context metasenv
  exp_named_subst1 exp_named_subst2
 =
 
 and fo_unif_subst_exp_named_subst subst context metasenv
  exp_named_subst1 exp_named_subst2
 =

-try
- List.fold_left2
-  (fun (subst,metasenv) (uri1,t1) (uri2,t2) ->
-    assert (uri1=uri2) ;
-    fo_unif_subst subst context metasenv t1 t2
-  ) (subst,metasenv) exp_named_subst1 exp_named_subst2
-with
-e ->
-let uri = UriManager.uri_of_string "cic:/dummy.var" in
-debug_print ("@@@: " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst1)) ^
-" <==> " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst2))) ; raise e
+ try
+  List.fold_left2
+   (fun (subst,metasenv) (uri1,t1) (uri2,t2) ->
+     assert (uri1=uri2) ;
+     fo_unif_subst subst context metasenv t1 t2
+   ) (subst,metasenv) exp_named_subst1 exp_named_subst2
+ with
+  Invalid_argument _ ->
+   let print_ens ens =
+    String.concat " ; "
+     (List.map
+       (fun (uri,t) ->
+         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)))

 
 (* A substitution is a (int * Cic.term) list that associates a               *)
 (* metavariable i with its body.                                             *)
 
 (* A substitution is a (int * Cic.term) list that associates a               *)
 (* metavariable i with its body.                                             *)


@@ -201,24 +260,21 @@ debug_print ("@@@: " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst1)) ^
 (* 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.                                   *)
 (* 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 =
- let subst_to_unwind,metasenv' = fo_unif_subst [] context metasenv t1 t2 in
-  CicMetaSubst.unwind_subst metasenv' subst_to_unwind
-;;
+let fo_unif metasenv context t1 t2 = fo_unif_subst [] context metasenv t1 t2 ;;

 
 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"
 
 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"

-      (CicPp.ppterm (CicMetaSubst.apply_subst subst t1))
+      (CicMetaSubst.ppterm subst t1)

       (try
         CicPp.ppterm (type_of_aux' metasenv subst context t1)
       with _ -> "MALFORMED")
       (try
         CicPp.ppterm (type_of_aux' metasenv subst context t1)
       with _ -> "MALFORMED")

-      (CicPp.ppterm (CicMetaSubst.apply_subst subst t2))
+      (CicMetaSubst.ppterm subst t2)

       (try
         CicPp.ppterm (type_of_aux' metasenv subst context t2)
       with _ -> "MALFORMED")
       (CicMetaSubst.ppcontext subst context)
       (try
         CicPp.ppterm (type_of_aux' metasenv subst context t2)
       with _ -> "MALFORMED")
       (CicMetaSubst.ppcontext subst context)

-      (CicMetaSubst.ppmetasenv subst metasenv) msg
+      (CicMetaSubst.ppmetasenv metasenv subst) msg

   in
   try
     fo_unif_subst subst context metasenv t1 t2
   in
   try
     fo_unif_subst subst context metasenv t1 t2