slow example

[helm.git] / helm / software / components / ng_refiner / check.ml

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 6f1c9293a912f03a156b22a7819cf29377d71f0e..82aff623b84c66a5919ac6ffc149c4aa94ca033b 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -208,25 +208,35 @@ let _ =
           let rec perforate ctx menv = function
             | NCic.Appl (NCic.Const (NReference.Ref (u,_))::ty::_)
               when NUri.string_of_uri u = "cic:/matita/tests/hole.con" ->
+                let menv, ty =  perforate ctx menv ty in
                 NCicMetaSubst.mk_meta menv ctx ty
             | t -> 
                 NCicUntrusted.map_term_fold_a
                  (fun e ctx -> e::ctx) ctx perforate menv t
           in
-          let ctx, ity = intros ty in
-          let menv, pty = perforate [] [] ty in
+          let ctx, pty = intros ty in
+          let menv, pty = perforate ctx [] pty in
 (*
           let sty, menv, _ = 
             NCicMetaSubst.saturate ~delta:max_int [] ctx ty 0
           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"
@@ -235,26 +245,31 @@ let _ =
 *)
           let metasenv, subst = 
             try 
-(*                     prerr_endline ("INIZIO: " ^ NUri.string_of_uri u); *)
-              NCicUnification.unify menv [] ctx ity pty
+              NCicUnification.unify menv [] ctx left right
             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 pty));
                 [], []
             | Sys.Break -> [],[]
           in
-          if (NCicReduction.are_convertible ~subst ctx ity pty)
+          if (NCicReduction.are_convertible ~subst ctx left right)
           then
             prerr_endline ("OK: " ^ NUri.string_of_uri u)
           else
-            prerr_endline ("FAIL: " ^ NUri.string_of_uri u);
+            (prerr_endline ("FAIL: " ^ NUri.string_of_uri u);
+                prerr_endline 
+                 (Printf.sprintf 
+                   ("\t\tRESULT OF UNIF\n\nsubst:\n%s\nmenv:\n%s\n" ^^ 
+                   "context:\n%s\n%s == %s\n%s == %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*)