more work

[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 82aff623b84c66a5919ac6ffc149c4aa94ca033b..7fe8cf3663303b9820f10141be11a79f7c3cae09 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -198,7 +198,7 @@ let _ =
       let u = OCic2NCic.nuri_of_ouri u in
       indent := 0;
       match NCicLibrary.get_obj u with
-      | _,_,_,_,NCic.Constant (_,_,_, ty, _) ->
+      | _,_,_,_,NCic.Constant (_,_,Some bo, ty, _) ->
           let rec intros = function
             | NCic.Prod (name, s, t) ->
                 let ctx, t = intros t in
@@ -209,25 +209,36 @@ let _ =
             | 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
+                let a,b,_ = NCicMetaSubst.mk_meta menv ctx (`WithType ty) in a,b
             | t -> 
                 NCicUntrusted.map_term_fold_a
                  (fun e ctx -> e::ctx) ctx perforate menv 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 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 =
@@ -243,9 +254,12 @@ let _ =
                  (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx ity)
                  (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx sty));
 *)
+          let menv, subst, bo, infty = 
+            NCicRefiner.typeof [] [] [] (curryfy [] bo) None
+          in
           let metasenv, subst = 
             try 
-              NCicUnification.unify menv [] ctx left right
+              NCicUnification.unify menv subst [] infty ty
             with
             | NCicUnification.Uncertain msg 
             | NCicUnification.UnificationFailure msg 
@@ -254,11 +268,16 @@ let _ =
                 [], []
             | Sys.Break -> [],[]
           in
-          if (NCicReduction.are_convertible ~subst ctx left right)
+          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\nmenv:\n%s\n" ^^