X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2Fcheck.ml;h=bc22a21608c1042ea20cbe3cd4d6bf582097056e;hb=1ee5193677b8e2a80d4f068ee79ecac335de1196;hp=3a155329e679ba235f2c5da77987ae69455b96c4;hpb=bfb7d5f4d6c812d5c5b036da654fd4f987f69bc9;p=helm.git

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 3a155329e..bc22a2160 100644
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -169,6 +169,17 @@ let _ =
   in
   prerr_endline "ranked....";
   prerr_endline (NCicEnvironment.pp_constraints ());
+(*
+  let [_,type0_uri] = mk_type 0 in
+  let [_,type1_uri] = mk_type 1 in
+  let [_,type2_uri] = mk_type 2 in
+  prerr_endline 
+   ("Min:" ^ 
+   (match NCicEnvironment.sup [true,type0_uri;true,type2_uri] with
+       | None -> "NO SUP"
+       | Some t -> NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] 
+          (NCic.Sort (NCic.Type t))));
+*)
   HExtlib.profiling_enabled := false;
   List.iter (fun uu ->
     let uu= OCic2NCic.nuri_of_ouri uu in
@@ -205,45 +216,98 @@ let _ =
                 ctx @ [(name, (NCic.Decl s))] , t
             | t -> [], t
           in
-          let ctx, ity = intros ty in
-          let sty, menv, _ = 
+          let rec perforate ctx metasenv = function
+            | NCic.Appl (NCic.Const (NReference.Ref (u,_))::ty::_)
+              when NUri.string_of_uri u = "cic:/matita/tests/hole.con" ->
+                let metasenv, ty =  perforate ctx metasenv ty in
+                let a,b,_ = NCicMetaSubst.mk_meta metasenv ctx (`WithType ty) in a,b
+            | t -> 
+                NCicUntrusted.map_term_fold_a
+                 (fun e ctx -> e::ctx) ctx perforate metasenv t
+          in
+          let rec curryfy ctx = function
+            | NCic.Lambda (name, s, tgt) ->
+                let tgt = curryfy ((name,NCic.Decl s) :: ctx) tgt in
+                NCic.Lambda (name, NCic.Implicit `Type, tgt)
+            | t -> 
+                NCicUtils.map
+                 (fun e ctx -> e::ctx) ctx curryfy t
+          in
+(*
+          let ctx, pty = intros ty in
+          let metasenv, pty = perforate ctx [] pty in
+*)
+(*
+          let sty, metasenv, _ = 
             NCicMetaSubst.saturate ~delta:max_int [] ctx ty 0
           in
-          let ctx, ty = intros ty in
+*)
+(*           let ctx, ty = intros ty in *)
+(*
+          let left, right = 
+            match  NCicReduction.whd ~delta:max_int ctx pty with
+            | NCic.Appl [eq;t;a;b] -> a, b
+            | _-> assert false
+          in
+*)             
+
+(*
           let whd ty =
             match ty with
             | NCic.Appl [eq;t;a;b] ->
                NCic.Appl [eq;t;NCicReduction.whd ~delta:0 ctx a;b]
             | t -> NCicReduction.whd ~delta:0 ctx t
           in
+*)
 (*
                 prerr_endline 
                  (Printf.sprintf "%s == %s"
-                 (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx ity)
-                 (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx sty));
+                 (NCicPp.ppterm ~metasenv:metasenv ~subst:[] ~context:ctx ity)
+                 (NCicPp.ppterm ~metasenv:metasenv ~subst:[] ~context:ctx sty));
 *)
+          let metasenv, subst, bo, infty = 
+            let bo = curryfy [] bo in
+            try NCicRefiner.typeof [] [] [] bo None
+            with
+            | NCicRefiner.RefineFailure msg 
+            | NCicRefiner.Uncertain msg ->
+               let _, msg = Lazy.force msg in
+               prerr_endline msg;
+               assert false
+          in
           let metasenv, subst = 
             try 
-(*                     prerr_endline ("INIZIO: " ^ NUri.string_of_uri u); *)
-              NCicUnification.unify menv [] ctx ity (whd sty) 
+              NCicUnification.unify metasenv subst [] infty ty
             with
             | NCicUnification.Uncertain msg 
             | NCicUnification.UnificationFailure msg 
             | NCicMetaSubst.MetaSubstFailure msg ->
                 prerr_endline (Lazy.force msg); 
-                prerr_endline 
-                 (Printf.sprintf "RESULT OF UNIF\n%s\n%s == %s\n"
-                 (NCicPp.ppcontext ~metasenv:menv ~subst:[] ctx)
-                 (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx ity)
-                 (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx sty));
-                [], []
-            | Sys.Break -> [],[]
+                metasenv, subst
+            | Sys.Break -> metasenv, subst
           in
-          if (NCicReduction.are_convertible ~subst ctx ity sty)
+          if (NCicReduction.are_convertible ~subst [] infty ty)
           then
             prerr_endline ("OK: " ^ NUri.string_of_uri u)
           else
-            prerr_endline ("FAIL: " ^ NUri.string_of_uri u);
+            (
+          let ctx = [] in
+          let right = infty in
+          let left = ty in
+                    
+                    prerr_endline ("FAIL: " ^ NUri.string_of_uri u);
+                prerr_endline 
+                 (Printf.sprintf 
+                   ("\t\tRESULT OF UNIF\n\nsubst:\n%s\nmetasenv:\n%s\n" ^^ 
+                   "context:\n%s\nTERMS NO SUBST:\n%s\n==\n%s\n"^^
+                   "TERMS:\n%s\n==\n%s\n")
+                 (NCicPp.ppsubst ~metasenv subst)
+                 (NCicPp.ppmetasenv ~subst metasenv)
+                 (NCicPp.ppcontext ~metasenv ~subst ctx)
+                 (NCicPp.ppterm ~metasenv ~subst:[] ~context:ctx left)
+                 (NCicPp.ppterm ~metasenv ~subst:[] ~context:ctx right)
+                 (NCicPp.ppterm ~metasenv ~subst ~context:ctx left)
+                 (NCicPp.ppterm ~metasenv ~subst ~context:ctx right) ))
           (*let inferred_ty = 
             NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] bo
           in*)