X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=291dcabdde30c808b88db0c362bc09fbefa1e0b6;hb=7ca0a000878e864c92d94f77900bc2ca0ac143b9;hp=a3c980648f9b87128128a815f9c01a0e85dd1ecb;hpb=0126a3d56c31231c38367ad7190fe80e471ca8cc;p=helm.git

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 = [] ->