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 56ec069d2c77bb7d30eff3773073908bdc01b6ff..656955808d5abaa231668c99ede556c9325627ac 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -145,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
@@ -238,7 +239,7 @@ let rec typeof rdb
          | None -> metasenv, subst, None 
          | Some x -> 
              let m, s, x = 
-               NCicUnification.delift_term_wrt_terms 
+               NCicUnification.delift_type_wrt_terms 
                  rdb metasenv subst context x [t]
              in
                m, s, Some x
@@ -379,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
@@ -746,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
@@ -809,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: *)