Universes introduction

[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 59ccc9ae907b4912f9674f59f7b57e3d4cf1f155..35eb18f450974d61fc238b77d3f985203b249d6b 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -25,8 +25,9 @@
 
 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 debug_print = prerr_endline
 


@@ -37,9 +38,10 @@ let type_of_aux' metasenv subst context term =
   | CicMetaSubst.MetaSubstFailure msg ->
     raise (AssertFailure
       ((sprintf
   | CicMetaSubst.MetaSubstFailure msg ->
     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


@@ -50,127 +52,190 @@ let type_of_aux' metasenv subst context term =
    a new substitution which is _NOT_ unwinded. It must be unwinded before
    applying it. *)
 
    a new substitution which is _NOT_ unwinded. It must be unwinded before
    applying it. *)
 

-let rec fo_unif_subst subst context metasenv t1 t2 =  
+let rec fo_unif_subst test_equality_only subst context metasenv t1 t2 =  

  let module C = Cic in
  let module R = CicMetaSubst in
  let module S = CicSubstitution in
   match (t1, t2) with
      (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
  let module C = Cic in
  let module R = CicMetaSubst in
  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 
+                    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
        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 ->
-       fo_unif_subst subst context metasenv t2 t1
+            "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)) ->
    | (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

        let subst'',metasenv' =
         try
          let oldt = (List.assoc n subst) in
          let lifted_oldt = S.lift_meta l oldt in
        let subst'',metasenv' =
         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 
+          test_equality_only subst context metasenv t lifted_oldt

         with Not_found ->
          let t',metasenv',subst' =
         with Not_found ->
          let t',metasenv',subst' =

+          try

            CicMetaSubst.delift n subst context metasenv l t
            CicMetaSubst.delift n subst context metasenv l t

+          with
+             (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
+           | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)

          in
          in

-          (n, t')::subst', metasenv'
+         let t'' =
+          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
+          (n, t'')::subst', metasenv'

        in
         let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv' in
         (try
           let tyt =
             type_of_aux' metasenv' subst'' context t
           in
        in
         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' (S.lift_meta l meta_type) tyt
-        with CicTypeChecker.SortExpectedMetaFound _ ->
+           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)
            *)
           (* 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
           (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

-       fo_unif_subst_exp_named_subst subst context metasenv
+       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 constants"
         exp_named_subst1 exp_named_subst2
       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
    | 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
+       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"
         exp_named_subst1 exp_named_subst2
       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

-       fo_unif_subst_exp_named_subst subst context metasenv
+       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"
         exp_named_subst1 exp_named_subst2
       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
-   | (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
+        (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
+   | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only 
+                              subst context metasenv t1 te

    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> 
    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> 

-       let subst',metasenv' = fo_unif_subst subst context metasenv s1 s2 in
-        fo_unif_subst subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 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

    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> 
    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> 

-       let subst',metasenv' = fo_unif_subst subst context metasenv s1 s2 in
-        fo_unif_subst subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 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

    | (C.LetIn (_,s1,t1), t2)  
    | (t2, C.LetIn (_,s1,t1)) -> 
    | (C.LetIn (_,s1,t1), t2)  
    | (t2, C.LetIn (_,s1,t1)) -> 

-       fo_unif_subst subst context metasenv t2 (S.subst s1 t1)
+       fo_unif_subst 
+        test_equality_only subst context metasenv t2 (S.subst s1 t1)

    | (C.Appl l1, C.Appl l2) -> 
        let lr1 = List.rev l1 in
        let lr2 = List.rev l2 in
    | (C.Appl l1, C.Appl l2) -> 
        let lr1 = List.rev l1 in
        let lr2 = List.rev l2 in

-       let rec fo_unif_l subst metasenv =
+       let rec fo_unif_l test_equality_only subst metasenv =

         function
            [],_
          | _,[] -> assert false
          | ([h1],[h2]) ->
         function
            [],_
          | _,[] -> assert false
          | ([h1],[h2]) ->

-             fo_unif_subst subst context metasenv h1 h2
+             fo_unif_subst test_equality_only subst context metasenv h1 h2

          | ([h],l) 
          | (l,[h]) ->
          | ([h],l) 
          | (l,[h]) ->

-             fo_unif_subst subst context metasenv h (C.Appl (List.rev l))
+             fo_unif_subst 
+             test_equality_only subst context metasenv h (C.Appl (List.rev l))

          | ((h1::l1),(h2::l2)) -> 
             let subst', metasenv' = 
          | ((h1::l1),(h2::l2)) -> 
             let subst', metasenv' = 

-             fo_unif_subst subst context metasenv h1 h2
+             fo_unif_subst test_equality_only subst context metasenv h1 h2

             in 
             in 

-             fo_unif_l subst' metasenv' (l1,l2)
+             fo_unif_l test_equality_only subst' metasenv' (l1,l2)

        in
        in

-        fo_unif_l subst metasenv (lr1, lr2) 
-   | (C.MutCase (_,_,outt1,t1,pl1), C.MutCase (_,_,outt2,t2,pl2))->
+        fo_unif_l test_equality_only subst metasenv (lr1, lr2) 
+   | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->

        let subst', metasenv' = 
        let subst', metasenv' = 

-        fo_unif_subst subst context metasenv outt1 outt2 in
+        fo_unif_subst test_equality_only subst context metasenv outt1 outt2 in

        let subst'',metasenv'' = 
        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 test_equality_only subst' context metasenv' t1' t2' in
+       (try
+         List.fold_left2 
+          (function (subst,metasenv) ->
+            fo_unif_subst test_equality_only 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 _)


@@ -183,29 +248,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
+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
 =

-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 test_equality_only 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.                                             *)


@@ -214,16 +285,17 @@ 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 = fo_unif_subst [] context metasenv t1 t2 ;;
+let fo_unif metasenv context t1 t2 = 
+ fo_unif_subst false [] 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")
       (try
         CicPp.ppterm (type_of_aux' metasenv subst context t2)
       with _ -> "MALFORMED")


@@ -231,7 +303,7 @@ let fo_unif_subst subst context metasenv t1 t2 =
       (CicMetaSubst.ppmetasenv metasenv subst) msg
   in
   try
       (CicMetaSubst.ppmetasenv metasenv subst) msg
   in
   try

-    fo_unif_subst subst context metasenv t1 t2
+    fo_unif_subst false subst context metasenv t1 t2

   with
   | AssertFailure msg -> raise (AssertFailure (enrich_msg msg))
   | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg))
   with
   | AssertFailure msg -> raise (AssertFailure (enrich_msg msg))
   | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg))