Better (but still broken) fix for the case ?sort vs ?term.

To implement the right thing, we need to be able to mark metas as sort without
using the fact that their type is an Implicit.

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index a3c980648f9b87128128a815f9c01a0e85dd1ecb..291dcabdde30c808b88db0c362bc09fbefa1e0b6 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -141,6 +141,18 @@ let rec mk_irl =
   | n -> NCic.Rel n :: mk_irl (n-1)
 ;;
 
+(* the argument must be a term in whd *)
+let rec could_reduce =
+ function
+  | C.Meta _ -> true
+  | C.Appl (C.Const (Ref.Ref (_,Ref.Fix (_,recno,_)))::args)
+     when List.length args > recno -> could_reduce (List.nth args recno)
+  | C.Match (_,_,arg,_) -> could_reduce arg
+  | C.Appl (he::_) -> could_reduce he
+  | C.Sort _ | C.Rel _ | C.Prod _ | C.Lambda _ | C.Const _ -> false
+  | C.Appl [] | C.LetIn _ | C.Implicit _ -> assert false
+;;
+
 let rec lambda_intros rdb metasenv subst context t args =
  let tty = NCicTypeChecker.typeof ~metasenv ~subst context t in
  let argsty =
@@ -191,40 +203,39 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
   let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
   let metasenv, subst, t = 
     match ty with 
-    | NCic.Implicit (`Typeof _) -> 
-       (let ty_t =
-         try
-          t (*
-          NCicTypeChecker.typeof ~subst ~metasenv context t*)
-         with
-            NCicTypeChecker.AssertFailure msg ->
-             let exc_to_be =
-              fail_exc metasenv subst context (NCic.Meta (n,lc)) t in
-             pp (lazy "fine typeof (fallimento)");
-             let ft = fix_sorts swap exc_to_be t in
-             if ft == t then 
-               (prerr_endline ( ("ILLTYPED: " ^ 
-                  NCicPp.ppterm ~metasenv ~subst ~context t
-              ^ "\nBECAUSE:" ^ Lazy.force msg ^ 
-              ppcontext ~metasenv ~subst context ^ 
-              ppmetasenv ~subst metasenv
-              ));
-                       assert false)
-             else
-              (try 
-                pp (lazy ("typeof: " ^ 
-                  NCicPp.ppterm ~metasenv ~subst ~context ft));
-                NCicTypeChecker.typeof ~subst ~metasenv context ft
-              with NCicTypeChecker.AssertFailure _ -> 
-                assert false)
-          | NCicTypeChecker.TypeCheckerFailure _ -> assert false
-        in
-         match NCicReduction.whd ~subst context ty_t with
-            NCic.Sort _ -> metasenv,subst, t
-          | NCic.Meta _ -> metasenv,subst,t (* CSC: TO BE IMPLEMENTED *)
-          | _ -> raise (Uncertain (lazy "Trying to instantiate a metavariable that represents a sort with a term")))
-            (*CSC: TO BE IMPLEMENTED: UnificationFailure of string Lazy.t;; *)
-         (* fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t *)
+    | NCic.Implicit (`Typeof _) ->
+       (match NCicReduction.whd ~subst context t with
+          NCic.Sort _ -> metasenv,subst,t
+        | NCic.Meta (i,_) when
+           let _,_,ty = NCicUtils.lookup_meta i metasenv in
+            (match ty with
+                NCic.Implicit (`Typeof _) -> true
+              | _ -> false)
+           -> metasenv,subst,t
+        | NCic.Meta (i,_) ->
+           let rec remove_and_hope i =
+            let _,ctx,ty = NCicUtils.lookup_meta i metasenv in
+            match ty with
+               NCic.Implicit _ -> List.filter (fun i',_ -> i <> i') metasenv
+             | _ ->
+               match NCicReduction.whd ~subst ctx ty with
+                  NCic.Meta (j,_) ->
+                   let metasenv = remove_and_hope j in
+                    List.filter (fun i',_ -> i <> i') metasenv
+                | _ -> assert false (* NON POSSO RESTRINGERE *)
+           in
+           let metasenv = remove_and_hope i in
+           let metasenv =
+            (i,(None,[],NCic.Implicit (`Typeof i)))::
+             List.filter (fun i',_ -> i <> i') metasenv
+           in
+            metasenv,subst,t
+        | NCic.Appl (NCic.Meta _::_) ->
+           raise (Uncertain (lazy "Trying to instantiate a metavariable that represents a sort with a term"))
+        | t when could_reduce t -> 
+           raise (Uncertain (lazy "Trying to instantiate a metavariable that represents a sort with a term"))
+        | _ ->
+           raise (UnificationFailure (lazy "Trying to instantiate a metavariable that represents a sort with a term")))
     | _ ->
        pp (lazy (
                "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^
@@ -571,8 +582,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
                (fun (metasenv,subst) -> 
                   unify rdb test_eq_only metasenv subst context)
                (metasenv, subst) pl1 pl2
-             with Invalid_argument _ -> 
-               raise (uncert_exc metasenv subst context t1 t2))
+             with Invalid_argument _ -> assert false)
        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
        | _ when NCicUntrusted.metas_of_term subst context t1 = [] && 
                 NCicUntrusted.metas_of_term subst context t2 = [] ->