From 189cd88a0532779547e8c10ff6f78ca93aae363a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 3 Oct 2008 16:29:28 +0000
Subject: [PATCH] ...

---
 helm/software/components/ng_refiner/check.ml  | 15 ++++++--
 .../software/components/ng_refiner/esempio.ma | 36 +++++++++++++++++++
 .../components/ng_refiner/nCicUnification.ml  |  6 ++--
 3 files changed, 52 insertions(+), 5 deletions(-)
 create mode 100644 helm/software/components/ng_refiner/esempio.ma

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 3a155329e..851cda9d2 100644
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -198,17 +198,28 @@ let _ =
       let u = OCic2NCic.nuri_of_ouri u in
       indent := 0;
       match NCicLibrary.get_obj u with
-      | _,_,_,_,NCic.Constant (_,_,Some bo, ty, _) ->
+      | _,_,_,_,NCic.Constant (_,_,_, 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 rec perforate ctx menv = function
+            | NCic.Appl (NCic.Const (NReference.Ref (u,_))::ty::_)
+              when NUri.string_of_uri u = "cic:/matita/tests/hole.con" ->
+                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 sty, menv, _ = 
             NCicMetaSubst.saturate ~delta:max_int [] ctx ty 0
           in
+*)
           let ctx, ty = intros ty in
           let whd ty =
             match ty with
@@ -225,7 +236,7 @@ let _ =
           let metasenv, subst = 
             try 
 (*                     prerr_endline ("INIZIO: " ^ NUri.string_of_uri u); *)
-              NCicUnification.unify menv [] ctx ity (whd sty) 
+              NCicUnification.unify menv [] ctx ity sty
             with
             | NCicUnification.Uncertain msg 
             | NCicUnification.UnificationFailure msg 
diff --git a/helm/software/components/ng_refiner/esempio.ma b/helm/software/components/ng_refiner/esempio.ma
new file mode 100644
index 000000000..4005ee98a
--- /dev/null
+++ b/helm/software/components/ng_refiner/esempio.ma
@@ -0,0 +1,36 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "nat/plus.ma".
+
+definition hole : ∀A:Type.A → A ≝ λA.λx.x.
+
+inductive pippo (T:Type) (x:T) : Prop ≝ . 
+
+axiom A: Type. 
+axiom B:A.
+
+axiom foo : \forall x: (hole ? A).pippo (hole ? A) x.
+
+axiom foo: (λx,y:A. pippo (hole ? A) x y) 
+           (hole ? B) (hole ? B).
+
+axiom foo: λx:(hole ? Type).λy:(hole ? Type). pippo (hole ? Type) x y.
+
+axiom foo: (λx,y.(λz. z x + z (x+y)) (λw:nat.hole ? w)) = λx,y.x. (* KO, delift rels only *) 
+axiom foo: (λx,y.(λz. z (x+y) + z x) (λw:nat.hole ? w)) = λx,y.x. (* OK *) 
+
+
+axiom foo: (λx,y.(λz. z x + z y) (λw:nat.hole ? w)) = λx,y.x. (* OK *) 
+
diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index a1a325fa5..fcc0b953e 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -72,12 +72,10 @@ let indent = ref "";;
 let inside c = indent := !indent ^ String.make 1 c;;
 let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
 
-(*
 let pp s = 
  prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ s);; 
-*)
 
-let pp _ = ();;
+(* let pp _ = ();; *)
 
 let rec beta_expand num test_eq_only swap metasenv subst context t arg =
   let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
@@ -172,6 +170,8 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
     (* by cumulativity when unify(?,Type_i) 
      * we could ? := Type_j with j <= i... *)
     let subst = (n, (name, ctx, t, ty)) :: subst in
+    pp ("?"^string_of_int n^" := "^NCicPp.ppterm
+      ~metasenv ~subst ~context:ctx t);
     let metasenv = 
       List.filter (fun (m,_) -> not (n = m)) metasenv 
     in
-- 
2.39.2