]> matita.cs.unibo.it Git - helm.git/blobdiff - components/cic_unification/cicUnification.ml
projects / helm.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
helm_registry: added the pair unmarshaller
[helm.git] / components / cic_unification / cicUnification.ml
diff --git a/components/cic_unification/cicUnification.ml b/components/cic_unification/cicUnification.ml
index 44712199e412b370170b8753c6aa0e488d6a12bf..86f280842f6a7480bb95cb60b35f00811b89b9fc 100644 (file)
--- a/components/cic_unification/cicUnification.ml
+++ b/components/cic_unification/cicUnification.ml
@@ -53,28 +53,32 @@ let foo () =
           (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.ppterm ~metasenv subst term)
+             (CicMetaSubst.ppterm ~metasenv [] term)
+             (CicMetaSubst.ppcontext ~metasenv subst context)
              (CicMetaSubst.ppmetasenv subst metasenv) 
-             (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
+             (CicMetaSubst.ppsubst ~metasenv 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.ppterm ~metasenv subst term)
+             (CicMetaSubst.ppterm ~metasenv [] term)
+             (CicMetaSubst.ppcontext ~metasenv subst context)
              (CicMetaSubst.ppmetasenv subst metasenv) 
-             (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
+             (CicMetaSubst.ppsubst ~metasenv 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
+  List.exists 
+    (function 
+       | Cic.Meta _  
+       | Cic.Appl (Cic.Meta _::_) -> true
+       | _ -> false) l
 
 let rec deref subst t =
   let snd (_,a,_) = a in
@@ -363,16 +367,16 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                     (*
                     (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))) *)
+                      (CicMetaSubst.ppterm ~metasenv subst t1) 
+                      (CicMetaSubst.ppterm ~metasenv 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)))) *)
+                      (CicMetaSubst.ppterm ~metasenv subst t1) 
+                      (CicMetaSubst.ppterm ~metasenv 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
@@ -427,10 +431,14 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                C.Sort (C.Type u) when not test_equality_only ->
                  let u' = CicUniv.fresh () in
                  let s = C.Sort (C.Type u') in
-                 let ugraph2 =   
-                   CicUniv.add_ge (upper u u') (lower u u') ugraph1
-                 in
-                   s,ugraph2
+                  (try
+                    let ugraph2 =   
+                     CicUniv.add_ge (upper u u') (lower u u') ugraph1
+                    in
+                     s,ugraph2
+                   with
+                    CicUniv.UniverseInconsistency msg ->
+                     raise (UnificationFailure msg))
              | _ -> t',ugraph1
          in
          (* Unifying the types may have already instantiated n. Let's check *)
@@ -456,19 +464,20 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
        raise (UnificationFailure (lazy 
           (sprintf
             "Can't unify %s with %s due to different constants"
-            (CicMetaSubst.ppterm subst t1) 
-            (CicMetaSubst.ppterm subst t2)))) 
+            (CicMetaSubst.ppterm ~metasenv subst t1) 
+            (CicMetaSubst.ppterm ~metasenv 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 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))) *)
+         raise (UnificationFailure
+           (lazy
+            (sprintf
+             "Can't unify %s with %s due to different inductive principles"
+             (CicMetaSubst.ppterm ~metasenv subst t1) 
+             (CicMetaSubst.ppterm ~metasenv 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
@@ -476,11 +485,12 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
            test_equality_only 
            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
        else
-         raise (UnificationFailure (lazy "5"))
-           (* (sprintf
+         raise (UnificationFailure
+          (lazy
+            (sprintf
               "Can't unify %s with %s due to different inductive constructors"
-              (CicMetaSubst.ppterm subst t1) 
-              (CicMetaSubst.ppterm subst t2))) *)
+              (CicMetaSubst.ppterm ~metasenv subst t1) 
+              (CicMetaSubst.ppterm ~metasenv subst t2))))
    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only 
                               subst context metasenv te t2 ugraph
@@ -578,13 +588,14 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                 fo_unif_l 
                   test_equality_only subst metasenv (lr1, lr2)  ugraph
               with 
-              | UnificationFailure _
-              | Uncertain _ as exn -> 
+              | 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
                     CoercGraph.is_a_coercion c1 && 
-                    CoercGraph.is_a_coercion c2 ->
+                    CoercGraph.is_a_coercion c2 &&
+                    not (UriManager.eq uri1 uri2) ->
                       let body1, attrs1, ugraph = 
                         match CicEnvironment.get_obj ugraph uri1 with
                         | Cic.Constant (_,Some bo, _, _, attrs),u  -> bo,attrs,u
@@ -596,9 +607,15 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                         | _ -> assert false
                       in
                       let is_composite1 = 
-                        List.exists ((=) (`Class `Coercion)) attrs1 in
+                        List.exists 
+                         (function `Class (`Coercion _) -> true | _-> false) 
+                         attrs1 
+                      in
                       let is_composite2 = 
-                        List.exists ((=) (`Class `Coercion)) attrs2 in
+                        List.exists 
+                         (function `Class (`Coercion _) -> true | _-> false) 
+                         attrs2 
+                      in
                       (match is_composite1, is_composite2 with
                       | false, false -> raise exn
                       | true, false ->
@@ -646,7 +663,9 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                           C.Appl (C.MutInd _::_) -> 
                             fo_unif_subst test_equality_only 
                               subst context metasenv t1 t2' ugraph         
-                        | _ -> raise (UnificationFailure (lazy "99")))
+                        | _ -> raise 
+                           (UnificationFailure 
+                              (lazy ("not a mutind :"^CicMetaSubst.ppterm ~metasenv subst t2 ))))
                   | _ -> raise exn)))
    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
        let subst', metasenv',ugraph1 = 
@@ -666,8 +685,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
           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)))) *)
+              (CicMetaSubst.ppterm ~metasenv subst t1) 
+              (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
    | (C.Rel _, _) | (_,  C.Rel _) ->
        if t1 = t2 then
          subst, metasenv,ugraph
@@ -675,8 +694,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
         raise (UnificationFailure (lazy 
            (sprintf
              "Can't unify %s with %s because they are not convertible"
-             (CicMetaSubst.ppterm subst t1) 
-             (CicMetaSubst.ppterm subst t2))))
+             (CicMetaSubst.ppterm ~metasenv subst t1) 
+             (CicMetaSubst.ppterm ~metasenv 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 
@@ -720,8 +739,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
              raise 
                 (UnificationFailure (lazy (sprintf
                    "Can't unify %s with %s because they are not convertible"
-                   (CicMetaSubst.ppterm subst t1) 
-                   (CicMetaSubst.ppterm subst t2)))))
+                   (CicMetaSubst.ppterm ~metasenv subst t1) 
+                   (CicMetaSubst.ppterm ~metasenv subst t2)))))
 *)
    | (_,_) ->
      (* delta-beta reduction should almost never be a problem for
@@ -740,8 +759,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
         (lazy 
           (sprintf
             "Can't unify %s with %s because they are not convertible"
-            (CicMetaSubst.ppterm subst t1) 
-            (CicMetaSubst.ppterm subst t2))))
+            (CicMetaSubst.ppterm ~metasenv subst t1) 
+            (CicMetaSubst.ppterm ~metasenv subst t2))))
       else
        try
         fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
@@ -752,8 +771,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
             (lazy 
               (sprintf
                 "Can't unify %s with %s because they are not convertible"
-                (CicMetaSubst.ppterm subst t1) 
-                (CicMetaSubst.ppterm subst t2))))
+                (CicMetaSubst.ppterm ~metasenv subst t1) 
+                (CicMetaSubst.ppterm ~metasenv subst t2))))
 
 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
  exp_named_subst1 exp_named_subst2 ugraph
@@ -770,7 +789,7 @@ and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
     String.concat " ; "
      (List.map
        (fun (uri,t) ->
-         UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
+         UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
        ) ens) 
    in
     raise (UnificationFailure (lazy (sprintf
@@ -790,7 +809,7 @@ 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)
+    (CicMetaSubst.ppterm ~metasenv subst t1)
     (try
       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
       CicPp.ppterm ty_t1
@@ -798,7 +817,7 @@ let enrich_msg msg subst context metasenv t1 t2 ugraph =
     | UnificationFailure s
     | Uncertain s
     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
-    (CicMetaSubst.ppterm subst t2)
+    (CicMetaSubst.ppterm ~metasenv subst t2)
     (try
       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
       CicPp.ppterm ty_t2
@@ -806,28 +825,28 @@ let enrich_msg msg subst context metasenv t1 t2 ugraph =
     | UnificationFailure s
     | Uncertain s
     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
-    (CicMetaSubst.ppcontext subst context)
+    (CicMetaSubst.ppcontext ~metasenv subst context)
     (CicMetaSubst.ppmetasenv subst metasenv)
-    (CicMetaSubst.ppsubst subst) (Lazy.force msg)
+    (CicMetaSubst.ppsubst ~metasenv 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)
+    (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
     (try
       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
-      CicMetaSubst.ppterm_in_context subst ty_t1 context
+      CicMetaSubst.ppterm_in_context ~metasenv 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)
+    (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
     (try
       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
-      CicMetaSubst.ppterm_in_context subst ty_t2 context
+      CicMetaSubst.ppterm_in_context ~metasenv 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.ppcontext ~metasenv subst context)
     (CicMetaSubst.ppmetasenv subst metasenv)
     (Lazy.force msg)
  )
Unnamed repository; edit this file 'description' to name the repository.