- mk_restricted_irl removed, the non-optimized code was the same

[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..202e68e4c86c3d056a8914451a70b6c4b25aae13 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -72,18 +72,26 @@ 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 ->  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
@@ -157,35 +165,31 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
     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,fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t
     | _ ->
        pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
        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
+           let ft = 
+            fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t
+           in
+           if ft == t then 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);
+            with NCicTypeChecker.TypeCheckerFailure _ -> 
               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