The unification does not longer use the refiner (urrah!)

[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 c4534e8daf6f466430f1144abf40ed28ed3c691a..656955808d5abaa231668c99ede556c9325627ac 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -114,10 +114,14 @@ let rec typeof rdb
           (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
@@ -141,11 +145,12 @@ let rec typeof rdb
            raise (RefineFailure (lazy (localise t,"unbound variable"))))
         in
         metasenv, subst, t, infty
-    | C.Sort (C.Type [false,u]) -> metasenv,subst,t,(C.Sort (C.Type [true, u]))
-    | C.Sort (C.Type _) -> 
-        raise (AssertFailure (lazy ("Cannot type an inferred type: "^
-          NCicPp.ppterm ~subst ~metasenv ~context t)))
-    | C.Sort _ -> metasenv,subst,t,(C.Sort (C.Type NCicEnvironment.type0))
+    | C.Sort s -> 
+         (try metasenv, subst, t, C.Sort (NCicEnvironment.typeof_sort s)
+         with 
+         | NCicEnvironment.UntypableSort msg -> 
+              raise (RefineFailure (lazy (localise t, Lazy.force msg)))
+         | NCicEnvironment.AssertFailure msg -> raise (AssertFailure msg))
     | C.Implicit infos -> 
          let metasenv,_,t,ty =
            exp_implicit ~localise metasenv context expty t infos
@@ -229,8 +234,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_type_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
@@ -365,15 +380,16 @@ and try_coercions rdb
         (NCicPp.ppterm ~metasenv ~subst ~context expty))) exc)
   | (_,metasenv, newterm, newtype, meta)::tl ->
       try 
+          pp (lazy("K=" ^ NCicPp.ppterm ~metasenv ~subst ~context newterm));
           pp (lazy ( "UNIFICATION in CTX:\n"^ 
             NCicPp.ppcontext ~metasenv ~subst context
             ^ "\nMENV: " ^
             NCicPp.ppmetasenv metasenv ~subst
             ^ "\nOF: " ^
-            NCicPp.ppterm ~metasenv ~subst ~context meta ^  " === " ^
-            NCicPp.ppterm ~metasenv ~subst ~context t ^ "\n"));
+            NCicPp.ppterm ~metasenv ~subst ~context t ^  " === " ^
+            NCicPp.ppterm ~metasenv ~subst ~context meta ^ "\n"));
         let metasenv, subst = 
-          NCicUnification.unify rdb metasenv subst context meta t
+          NCicUnification.unify rdb metasenv subst context t meta
         in
           pp (lazy ( "UNIFICATION in CTX:\n"^ 
             NCicPp.ppcontext ~metasenv ~subst context
@@ -509,11 +525,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
@@ -522,7 +540,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
@@ -726,7 +748,7 @@ let typeof_obj
                       "and those of its inductive type"))))
                    else
                     metasenv,subst,item1::context
-                ) (metasenv,subst,[]) sx_context_ty_rev sx_context_te_rev
+                ) (metasenv,subst,tys) sx_context_ty_rev sx_context_te_rev
               with Invalid_argument "List.fold_left2" -> assert false in
              let con_sort= NCicTypeChecker.typeof ~subst ~metasenv context te in
               (match
@@ -789,6 +811,4 @@ let typeof_obj
       uri, height, metasenv, subst, C.Inductive (ind, leftno, itl, attr)
 ;;
 
-NCicUnification.set_refiner_typeof typeof;;
-
 (* vim:set foldmethod=marker: *)