removed empty lines

[helm.git] / helm / software / components / ng_refiner / nCicUnification.ml

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index d3c86d2816c2c9bd050bbe1b336d033d95e4c8dd..0e119f34b73949079b03cce21be67e0173f8d6ef 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -72,18 +72,27 @@ let indent = ref "";;
 let inside c = indent := !indent ^ String.make 1 c;;
 let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
 
+(*
 let pp s = 
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
 ;;  
+*)
 
-(* let pp _ = ();; *)
+let pp _ = ();;
 
-let fix_sorts metasenv subst context meta t =
+let fix_sorts swap metasenv subst context meta t =
   let rec aux () = function
     | NCic.Sort (NCic.Type u) as orig ->
-       (match NCicEnvironment.sup u with
-       | None ->  raise (fail_exc metasenv subst context meta t)
-       | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1))
+        if swap then
+         match NCicEnvironment.sup u with
+         | None -> prerr_endline "no sup for" ;
+            raise (fail_exc metasenv subst context meta t)
+         | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)
+        else
+         NCic.Sort (NCic.Type (
+           match NCicEnvironment.sup NCicEnvironment.type0 with 
+           | Some x -> x 
+           | _ -> assert false))
     | NCic.Meta _ as orig -> orig
     | t -> NCicUtils.map (fun _ _ -> ()) () aux t
   in
@@ -153,49 +162,71 @@ and beta_expand_many test_equality_only swap metasenv subst context t args =
 
 and instantiate test_eq_only metasenv subst context n lc t swap =
  (*D*)  inside 'I'; try let rc =  
+         pp (lazy(string_of_int n ^ " :=?= "^
+           NCicPp.ppterm ~metasenv ~subst ~context t));
   let unify test_eq_only m s c t1 t2 = 
     if swap then unify test_eq_only m s c t2 t1 
     else unify test_eq_only m s c t1 t2
   in
-  let fix_sorts t = 
-    if swap then fix_sorts metasenv subst context (NCic.Meta (n,lc)) t
-    else 
-      NCic.Sort (NCic.Type (
-        match NCicEnvironment.sup NCicEnvironment.type0 with Some x ->x| _ ->
-                assert false))
-  in
   let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
   let metasenv, subst, t = 
     match ty with 
-    | NCic.Implicit (`Typeof _) -> metasenv, subst, fix_sorts t
+    | NCic.Implicit (`Typeof _) -> 
+       metasenv,subst, t
+         (* fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t *)
     | _ ->
-       pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
+       pp (lazy (
+         "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\nctx:\n"^
+          NCicPp.ppcontext ~metasenv ~subst context ^ "\nmenv:\n"^
+          NCicPp.ppmetasenv ~subst metasenv));
        let t, ty_t = 
          try t, NCicTypeChecker.typeof ~subst ~metasenv context t 
-         with NCicTypeChecker.TypeCheckerFailure _ -> 
-           let ft = fix_sorts t in
-           if ft == t then assert false else
+         with 
+         | NCicTypeChecker.AssertFailure msg -> 
+           (pp (lazy "fine typeof (fallimento)");
+           let ft = 
+            fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t
+           in
+           if ft == t then 
+             (prerr_endline ( ("ILLTYPED: " ^ 
+                NCicPp.ppterm ~metasenv ~subst ~context t
+            ^ "\nBECAUSE:" ^ Lazy.force msg ^ "\nCONTEXT:\n" ^
+            NCicPp.ppcontext ~metasenv ~subst context ^ "\nMENV:\n" ^
+            NCicPp.ppmetasenv ~subst metasenv
+            ));
+                     assert false)
+           else
             try 
               pp (lazy ("typeof: " ^ 
                 NCicPp.ppterm ~metasenv ~subst ~context ft));
               ft, NCicTypeChecker.typeof ~subst ~metasenv context ft 
-            with NCicTypeChecker.TypeCheckerFailure msg -> 
-              prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context ft);
-              prerr_endline (Lazy.force msg);
-              assert false
+            with NCicTypeChecker.AssertFailure _ -> 
+              assert false)
+         | NCicTypeChecker.TypeCheckerFailure msg ->
+              pp msg; assert false
        in
        let lty = NCicSubstitution.subst_meta lc ty in
        pp (lazy("On the types: " ^
+        NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^
         NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
          ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); 
        let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in
        metasenv, subst, t
   in
+         pp (lazy(string_of_int n ^ " := 111 = "^
+           NCicPp.ppterm ~metasenv ~subst ~context t));
   let (metasenv, subst), t = 
     try NCicMetaSubst.delift metasenv subst context n lc t
-    with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg)
-    |    NCicMetaSubst.MetaSubstFailure msg -> raise (UnificationFailure msg)
+    with NCicMetaSubst.Uncertain msg -> 
+         pp (lazy ("delift fails: " ^ Lazy.force msg));
+         raise (Uncertain msg)
+    | NCicMetaSubst.MetaSubstFailure msg -> 
+         pp (lazy ("delift fails: " ^ Lazy.force msg));
+         raise (UnificationFailure msg)
   in
+         pp (lazy(string_of_int n ^ " := 222 = "^
+           NCicPp.ppterm ~metasenv ~subst ~context:ctx t
+         ^ "\n" ^ NCicPp.ppmetasenv ~subst metasenv));
   (* Unifying the types may have already instantiated n. *)
   try
     let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
@@ -262,10 +293,12 @@ and unify test_eq_only metasenv subst context t1 t2 =
                   metasenv, subst, i::to_restrict, i-1)
              l1 l2 (metasenv, subst, [], List.length l1)
            in
-           let metasenv, subst, _ = 
-             NCicMetaSubst.restrict metasenv subst n1 to_restrict
-           in
-             metasenv, subst
+           if to_restrict <> [] then
+             let metasenv, subst, _ = 
+               NCicMetaSubst.restrict metasenv subst n1 to_restrict
+             in
+               metasenv, subst
+           else metasenv, subst
           with 
            | Invalid_argument _ -> assert false
            | NCicMetaSubst.MetaSubstFailure msg ->