From 5945dfb4370eca6142918c151bc93a6f242cee6c Mon Sep 17 00:00:00 2001
From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Wed, 18 Nov 2009 14:36:17 +0000
Subject: [PATCH] NCicRefiner.force_to_sort implemented on top of
 NCicUnification.sortfy.

---
 .../components/ng_refiner/nCicRefiner.ml      | 38 ++++++++-----------
 .../components/ng_refiner/nCicUnification.mli |  6 +++
 2 files changed, 21 insertions(+), 23 deletions(-)

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 415afdc1d..784ceeea8 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -453,29 +453,21 @@ and try_coercions rdb
         rdb metasenv subst context infty expty)
 
 and force_to_sort rdb metasenv subst context t orig_t localise ty =
-  match NCicReduction.whd ~subst context ty with
-  | C.Meta (_,(0,(C.Irl 0 | C.Ctx []))) as ty -> 
-     metasenv, subst, t, ty
-  | C.Meta (_i,(_,(C.Irl 0 | C.Ctx []))) -> assert false (*CSC: ???
-     metasenv, subst, t, C.Meta(i,(0,C.Irl 0)) *)
-  | C.Meta (i,(_,lc)) ->
-     let len = match lc with C.Irl len->len | C.Ctx l->List.length l in
-     let metasenv, subst, newmeta, _ = 
-       if len > 0 then
-         NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 (len+1))
-       else metasenv, subst, i, []
-     in
-     metasenv, subst, t, C.Meta (newmeta,(0,C.Irl 0))
-  | C.Sort _ as ty -> metasenv, subst, t, ty 
-  | ty -> 
-      try_coercions rdb ~localise metasenv subst context
-        t orig_t ty (NCic.Sort (NCic.Type 
-          (match NCicEnvironment.get_universes () with
-           | x::_ -> x 
-           | _ -> assert false))) false 
-         (Uncertain (lazy (localise orig_t, 
-         "The type of " ^ NCicPp.ppterm ~metasenv ~subst ~context t
-         ^ " is not a sort: " ^ NCicPp.ppterm ~metasenv ~subst ~context ty)))
+  try 
+    let metasenv, subst, ty = 
+      NCicUnification.sortfy (Failure "sortfy") metasenv subst context ty in
+      metasenv, subst, t, ty
+  with
+      Failure _ -> 
+        let ty = NCicReduction.whd ~subst context ty in
+          try_coercions rdb ~localise metasenv subst context
+            t orig_t ty (NCic.Sort (NCic.Type 
+              (match NCicEnvironment.get_universes () with
+               | x::_ -> x 
+               | _ -> assert false))) false 
+             (Uncertain (lazy (localise orig_t, 
+             "The type of " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^
+             " is not a sort: " ^ NCicPp.ppterm ~metasenv ~subst ~context ty)))
 
 and sort_of_prod 
   localise metasenv subst context orig_s orig_t (name,s) t (t1, t2) 
diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli
index fef24b2d5..954f56e58 100644
--- a/helm/software/components/ng_refiner/nCicUnification.mli
+++ b/helm/software/components/ng_refiner/nCicUnification.mli
@@ -37,5 +37,11 @@ val delift_type_wrt_terms:
   NCic.term -> NCic.term list -> 
    NCic.metasenv * NCic.substitution * NCic.term
 
+val sortfy :
+    exn ->
+    NCic.metasenv ->
+    NCic.substitution ->
+    NCic.context ->
+    NCic.term -> NCic.metasenv * NCic.substitution * NCic.term
 
 val debug : bool ref
-- 
2.39.2