improved check in delift for flexible lc entries.

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

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 5a6f1028fdf9a4ad177a2483961a090096f8a697..56ec069d2c77bb7d30eff3773073908bdc01b6ff 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -109,15 +109,19 @@ let rec typeof rdb
        | C.Lambda _ when skip_lambda -> metasenv, subst, t, expty
        | C.Appl _ when skip_appl -> metasenv, subst, t, expty
        | _ ->
-          pp (lazy (
+          pp (lazy ("forcing infty=expty: "^
           (NCicPp.ppterm ~metasenv ~subst ~context infty) ^  " === " ^
           (NCicPp.ppterm ~metasenv ~subst:[] ~context expty)));
            try 
              let metasenv, subst =
+    (*D*)inside 'U'; try let rc = 
                NCicUnification.unify rdb metasenv subst context infty expty 
+    (*D*)in outside(); rc with exc -> outside (); raise exc
              in
              metasenv, subst, t, expty
-           with exc -> 
+           with 
+           | NCicUnification.Uncertain _ 
+           | NCicUnification.UnificationFailure _ as exc -> 
              try_coercions rdb ~localise 
                metasenv subst context t orig infty expty true exc)
     | None -> metasenv, subst, t, infty
@@ -126,7 +130,7 @@ let rec typeof rdb
   let rec typeof_aux metasenv subst context expty = 
     fun t as orig -> 
     (*D*)inside 'R'; try let rc = 
-    pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " expty= " ^
+    pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " ::exp:: " ^
        match expty with None -> "None" | Some e -> 
        NCicPp.ppterm ~metasenv ~subst ~context e));
     let metasenv, subst, t, infty = 
@@ -229,8 +233,18 @@ let rec typeof rdb
        let metasenv, subst, t, _ = 
          typeof_aux metasenv subst context (Some ty) t in
        let context1 = (n, C.Def (t,ty)) :: context in
+       let metasenv, subst, expty1 = 
+         match expty with 
+         | None -> metasenv, subst, None 
+         | Some x -> 
+             let m, s, x = 
+               NCicUnification.delift_term_wrt_terms 
+                 rdb metasenv subst context x [t]
+             in
+               m, s, Some x
+       in
        let metasenv, subst, bo, bo_ty = 
-         typeof_aux metasenv subst context1 None bo 
+         typeof_aux metasenv subst context1 expty1 bo 
        in
        let bo_ty = NCicSubstitution.subst ~avoid_beta_redexes:true t bo_ty in
        metasenv, subst, C.LetIn (n, ty, t, bo), bo_ty
@@ -332,7 +346,7 @@ let rec typeof rdb
                 NCicTypeChecker.type_of_branch 
                   ~subst context leftno outtype cons ty_cons in
               pp (lazy ("TYPEOFBRANCH: " ^
-               NCicPp.ppterm ~metasenv ~subst ~context p ^ " ::: " ^
+               NCicPp.ppterm ~metasenv ~subst ~context p ^ " ::inf:: " ^
                NCicPp.ppterm ~metasenv ~subst ~context ty_branch ));
               let metasenv, subst, p, _ = 
                 typeof_aux metasenv subst context (Some ty_branch) p in
@@ -344,7 +358,7 @@ let rec typeof rdb
       metasenv, subst, C.Match (r, outtype, term, pl),resty
     | C.Match _ -> assert false
     in
-    pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^
+    pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " ::inf:: "^
          NCicPp.ppterm ~metasenv ~subst ~context infty ));
       force_ty true true metasenv subst context orig t infty expty
     (*D*)in outside(); rc with exc -> outside (); raise exc
@@ -467,7 +481,9 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
        " of type " ^ NCicPp.ppterm ~metasenv ~subst ~context ty_he
        ^ " to type " ^ match expty with None -> "None" | Some x -> 
        NCicPp.ppterm ~metasenv ~subst ~context x));
-      force_ty true false metasenv subst context orig_t res ty_he expty
+     (* whatever the term is, we force the type. in case of ((Lambda..) ?...)
+      * the application may also be a lambda! *)
+     force_ty false false metasenv subst context orig_t res ty_he expty
   | NCic.Implicit `Vector::tl ->
       let has_some_more_pis x =
         match NCicReduction.whd ~subst context x with
@@ -507,11 +523,13 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
           let metasenv,subst, flex_prod, _ =
            typeof rdb ~localise metasenv subst
             context flex_prod None in
+(*
           pp (lazy ( "UNIFICATION in CTX:\n"^ 
             NCicPp.ppcontext ~metasenv ~subst context
             ^ "\nOF: " ^
             NCicPp.ppterm ~metasenv ~subst ~context t ^  " === " ^
             NCicPp.ppterm ~metasenv ~subst ~context flex_prod ^ "\n"));
+*)
           let metasenv, subst =
              try NCicUnification.unify rdb metasenv subst context t flex_prod 
              with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf
@@ -520,7 +538,11 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
               (NCicPp.ppterm ~metasenv ~subst ~context he)
               (NCicPp.ppterm ~metasenv ~subst ~context t)
               (NCicPp.ppterm ~metasenv ~subst ~context arg)
-              (NCicPp.ppterm ~metasenv ~subst ~context ty_arg))) exc)
+              (NCicPp.ppterm ~metasenv ~subst ~context ty_arg))) 
+                 (match exc with
+                 | NCicUnification.UnificationFailure m -> 
+                     NCicUnification.Uncertain m
+                 | x -> x))
               (* XXX coerce to funclass *)
           in
           let meta = NCicSubstitution.subst ~avoid_beta_redexes:true arg meta in