From 7ca0a000878e864c92d94f77900bc2ca0ac143b9 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 30 Sep 2009 12:55:49 +0000
Subject: [PATCH] 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.

---
 .../components/ng_refiner/nCicUnification.ml  | 82 +++++++++++--------
 1 file changed, 46 insertions(+), 36 deletions(-)

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index a3c980648..291dcabdd 100644
--- 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 = [] -> 
-- 
2.39.2