- 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 10bc29a62d2ca398aa9b092859fea079b1d6f5db..202e68e4c86c3d056a8914451a70b6c4b25aae13 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -80,6 +80,24 @@ let pp s =
 
 let pp _ = ();;
 
+let fix_sorts swap metasenv subst context meta t =
+  let rec aux () = function
+    | NCic.Sort (NCic.Type u) as orig ->
+        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
+    aux () t
+;;
+
 let rec beta_expand num test_eq_only swap metasenv subst context t arg =
   let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
    try
@@ -142,28 +160,40 @@ and beta_expand_many test_equality_only swap metasenv subst context t args =
 (* (*D*)  in outside (); rc with exn -> outside (); raise exn *)
 
 and instantiate test_eq_only metasenv subst context n lc t swap =
-(* (*D*)  inside 'I'; try let rc =  *)
+ (*D*)  inside 'I'; try let rc =  
   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 name, ctx, ty = NCicUtils.lookup_meta n metasenv in
-  let metasenv, subst = 
+  let metasenv, subst, t = 
     match ty with 
-    | NCic.Implicit (`Typeof _) -> metasenv, subst
+    | NCic.Implicit (`Typeof _) -> 
+       metasenv,subst,fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t
     | _ ->
-       let lty = NCicSubstitution.subst_meta lc ty in
-       let ty_t = 
-         try NCicTypeChecker.typeof ~subst ~metasenv context t 
-         with NCicTypeChecker.TypeCheckerFailure msg -> 
-           prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
-           prerr_endline (Lazy.force msg);
-           assert false
+       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 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 _ -> 
+              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)); 
-       unify test_eq_only metasenv subst context lty ty_t 
+       let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in
+       metasenv, subst, t
   in
   let (metasenv, subst), t = 
     try NCicMetaSubst.delift metasenv subst context n lc t
@@ -174,6 +204,7 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
   try
     let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
     let oldt = NCicSubstitution.subst_meta lc oldt in
+    let t = NCicSubstitution.subst_meta lc t in
     (* conjecture: always fail --> occur check *)
     unify test_eq_only metasenv subst context oldt t
   with NCicUtils.Subst_not_found _ -> 
@@ -181,21 +212,19 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
      * we could ? := Type_j with j <= i... *)
     let subst = (n, (name, ctx, t, ty)) :: subst in
     pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm
-      ~metasenv ~subst ~context:ctx (NCicSubstitution.subst_meta lc t)));
+      ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t)));
     let metasenv = 
       List.filter (fun (m,_) -> not (n = m)) metasenv 
     in
     metasenv, subst
-(* (*D*)  in outside(); rc with exn -> outside (); raise exn *)
+ (*D*)  in outside(); rc with exn -> outside (); raise exn 
 
 and unify test_eq_only metasenv subst context t1 t2 =
-(* (*D*) inside 'U'; try let rc = *)
+ (*D*) inside 'U'; try let rc = 
    let fo_unif test_eq_only metasenv subst t1 t2 =
-(*    (*D*) inside 'F'; try let rc =  *)
-(*
+    (*D*) inside 'F'; try let rc =  
      pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ 
          NCicPp.ppterm ~metasenv ~subst ~context t2));
-*)
      if t1 === t2 then
        metasenv, subst
      else
@@ -379,7 +408,7 @@ and unify test_eq_only metasenv subst context t1 t2 =
                raise (uncert_exc metasenv subst context t1 t2))
        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
        | _ -> raise (uncert_exc metasenv subst context t1 t2)
-(*     (*D*)  in outside(); rc with exn -> outside (); raise exn *)
+     (*D*)  in outside(); rc with exn -> outside (); raise exn 
     in
     let height_of = function
      | NCic.Const (Ref.Ref (_,Ref.Def h)) 
@@ -410,7 +439,7 @@ and unify test_eq_only metasenv subst context t1 t2 =
     let rec unif_machines metasenv subst = 
       function
       | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
-(*     (*D*) inside 'M'; try let rc = *)
+     (*D*) inside 'M'; try let rc = 
 (*
          pp (lazy((if are_normal then "*" else " ") ^ " " ^
            NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^
@@ -445,7 +474,7 @@ and unify test_eq_only metasenv subst context t1 t2 =
         try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
         with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
            unif_machines metasenv subst (small_delta_step m1 m2)
-(*      (*D*)  in outside(); rc with exn -> outside (); raise exn *)
+      (*D*)  in outside(); rc with exn -> outside (); raise exn 
      in
      try fo_unif test_eq_only metasenv subst t1 t2
      with UnificationFailure msg | Uncertain msg as exn -> 
@@ -455,7 +484,7 @@ and unify test_eq_only metasenv subst context t1 t2 =
        with 
        | UnificationFailure _ -> raise (UnificationFailure msg)
        | Uncertain _ -> raise exn
-(* (*D*)  in outside(); rc with exn -> outside (); raise exn *)
+ (*D*)  in outside(); rc with exn -> outside (); raise exn 
 ;;
 
 let unify =