we can test the unification algorithm!

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 00ea9f24e32e5a79b2a71877d6361c9e13cd9a49..5f29d25d87093d71cf26875d045e7af5e99ec614 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -132,7 +132,12 @@ let trivial_pp_term ~context ~subst:_ ~metasenv:_ ?(inside_fix=false) t =
        if not toplevel then F.fprintf f ")";
        F.fprintf f "@]"
    | C.Implicit _ -> F.fprintf f "?"
-   | C.Meta (n,_) -> F.fprintf f "?%d" n
+   | C.Meta (n,(shift,C.Irl len)) -> 
+        F.fprintf f "?%d(%d,%d)" n shift len
+   | C.Meta (n,(shift,C.Ctx l)) -> 
+        F.fprintf f "?%d(%d,[" n shift;
+        List.iter (fun x -> aux ctx x; F.fprintf f ",") l;
+        F.fprintf f "])"
    | C.Sort C.Prop -> F.fprintf f "Prop"
    | C.Sort (C.Type []) -> F.fprintf f "IllFormedUniverse"
    | C.Sort (C.Type [false, u]) -> F.fprintf f "%s" (NUri.name_of_uri u)

diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend
index b71e499a165043fbff379fae6975f2d046361b47..42a02ebf19445f9c6a7685c7f5caeadde71815b7 100644 (file)
--- a/helm/software/components/ng_refiner/.depend
+++ b/helm/software/components/ng_refiner/.depend
@@ -2,7 +2,7 @@ nDiscriminationTree.cmo: nDiscriminationTree.cmi
 nDiscriminationTree.cmx: nDiscriminationTree.cmi 
 nCicMetaSubst.cmo: nCicMetaSubst.cmi 
 nCicMetaSubst.cmx: nCicMetaSubst.cmi 
-nCicUnification.cmo: nCicUnification.cmi 
-nCicUnification.cmx: nCicUnification.cmi 
+nCicUnification.cmo: nCicMetaSubst.cmi nCicUnification.cmi 
+nCicUnification.cmx: nCicMetaSubst.cmx nCicUnification.cmi 
 nCicRefiner.cmo: nCicRefiner.cmi 
 nCicRefiner.cmx: nCicRefiner.cmi 

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index c1ce4260794ce9bb4388dc6a3f756f34eaa2ab5b..4adff1569d3051721352c6de92ee3e7be387d370 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -193,23 +193,47 @@ let _ =
   NCicTypeChecker.set_logger (fun _ -> ());
   do_old_logging := false;
   prerr_endline "typechecking, first with the new and then with the old kernel";
-  let prima = Unix.gettimeofday () in
   List.iter 
     (fun u ->
-       let u= OCic2NCic.nuri_of_ouri u in
+      let u = OCic2NCic.nuri_of_ouri u in
       indent := 0;
-      NCicTypeChecker.typecheck_obj (NCicLibrary.get_obj u))
+      match NCicLibrary.get_obj u with
+      | _,_,_,_,NCic.Constant (_,_,Some bo, ty, _) ->
+          let rec intros = function
+            | NCic.Prod (name, s, t) ->
+                let ctx, t = intros t in
+                ctx @ [(name, (NCic.Decl s))] , t
+            | t -> [], t
+          in
+          let ctx, ity = intros ty in
+          let sty, menv, _ = 
+            NCicMetaSubst.saturate ~delta:max_int [] ctx ty 0
+          in
+          let ctx, ty = intros ty in
+          let metasenv, subst = 
+            try 
+              NCicUnification.unify menv [] ctx ity sty
+            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));
+                [], []
+          in
+          if (NCicReduction.are_convertible 
+             ~subst (fun ~subst:_ _ _ _ ->[]) ctx ity sty)
+          then
+            prerr_endline ("OK: " ^ NUri.string_of_uri u)
+          else
+            prerr_endline ("FAIL: " ^ NUri.string_of_uri u);
+          (*let inferred_ty = 
+            NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] bo
+          in*)
+      | _ -> ())
     alluris;
-  let dopo = Unix.gettimeofday () in
-  Gc.compact ();
-  let dopo2 = Unix.gettimeofday () in
-  Printf.eprintf "NEW typing: %3.2f, gc: %3.2f\n%!" (dopo -. prima) (dopo2 -.  dopo);
-  CicEnvironment.invalidate ();
-  Gc.compact ();
-  let prima = Unix.gettimeofday () in
-  List.iter (fun u -> ignore (CicTypeChecker.typecheck u)) alluris;
-  let dopo = Unix.gettimeofday () in
-  Gc.compact ();
-  let dopo2 = Unix.gettimeofday () in
-  Printf.eprintf "OLD typing: %3.2f, gc: %3.2f\n%!" (dopo -. prima) (dopo2 -. dopo)
 ;;

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index abc9eae6a03aa7e7b6cc9aef17dfd0f8457dbccc..188d4dc207ff4bf8e4f47d4bf28d8407b12be214 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -547,3 +547,30 @@ let delift_rels subst metasenv n t =
   delift_rels_from subst metasenv 1 n t
 *) 
 
+let mk_meta ?name metasenv context ty = 
+  let n = newmeta () in
+  let len = List.length context in
+  let menv_entry = (n, (name, context, ty)) in
+  menv_entry :: metasenv, NCic.Meta (n, (0,NCic.Irl len))
+;;
+
+let saturate ?(delta=0) metasenv context ty goal_arity =
+ assert (goal_arity >= 0);
+  let rec aux metasenv = function
+   | NCic.Prod (name,s,t) ->
+       let metasenv1, arg = mk_meta ~name:name metasenv context s in            
+       let t, metasenv1, args, pno = 
+           aux metasenv1 (NCicSubstitution.subst arg t) 
+       in
+       if pno + 1 = goal_arity then
+         ty, metasenv, [], goal_arity+1
+       else
+         t, metasenv1, arg::args, pno+1
+   | ty ->
+        match NCicReduction.whd context ty ~delta with
+        | NCic.Prod _ as ty -> aux metasenv ty
+        | ty -> ty, metasenv, [], 0
+  in
+  let res, newmetasenv, arguments, _ = aux metasenv ty in
+  res, newmetasenv, arguments
+;;

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli
index 91752fbf75e433b7155581c79859f0ef2d9cabcc..6c6ddf554e55def7d020a33a32bffba440e39894 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.mli
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli
@@ -52,3 +52,11 @@ val restrict:
     NCic.substitution ->
       int -> int list -> NCic.metasenv * NCic.substitution * int
 
+val mk_meta: 
+    ?name:string ->
+    NCic.metasenv -> NCic.context -> NCic.term -> NCic.metasenv * NCic.term
+
+val saturate:
+    ?delta:int -> NCic.metasenv -> NCic.context -> NCic.term -> int ->
+       NCic.term * NCic.metasenv * NCic.term list
+