X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=fcc0b953e70ad9f50c6dd3a8f144867bf1261fbb;hb=189cd88a0532779547e8c10ff6f78ca93aae363a;hp=16178bd3b3e8af51a21591322c6071074a75afca;hpb=a677e0d09755766c61ce9b30a98bec10cb8902b3;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 16178bd3b..fcc0b953e 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -68,6 +68,15 @@ let eta_reduce =
 module C = NCic;;
 module Ref = NReference;;
 
+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 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' =
    try
@@ -111,6 +120,9 @@ let rec beta_expand num test_eq_only swap metasenv subst context t arg =
     metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
 
 and beta_expand_many test_equality_only swap metasenv subst context t args =
+(*D*)  inside 'B'; try let rc =
+  pp (String.concat ", " (List.map (NCicPp.ppterm ~metasenv ~subst ~context)
+     args) ^ " ∈ " ^ NCicPp.ppterm ~metasenv ~subst ~context t);
   let _, subst, metasenv, hd =
     List.fold_right
       (fun arg (num,subst,metasenv,t) ->
@@ -120,22 +132,33 @@ and beta_expand_many test_equality_only swap metasenv subst context t args =
            num+1,subst,metasenv,t)
       args (1,subst,metasenv,t) 
   in
+  pp ("Head syntesized by b-exp: " ^ 
+    NCicPp.ppterm ~metasenv ~subst ~context hd);
     metasenv, subst, hd
+(*D*)  in outside (); rc with exn -> outside (); raise exn
 
 and instantiate test_eq_only metasenv subst context n lc t swap =
+(*D*)  inside 'I'; try let rc = 
   let unify test_eq_only m s c t1 t2 = 
     if swap then unify test_eq_only m s c t2 t1 
     else unify test_eq_only m s c t1 t2
   in
   let ty_t = 
     try NCicTypeChecker.typeof ~subst ~metasenv context t 
-    with NCicTypeChecker.TypeCheckerFailure _ -> assert false
+    with NCicTypeChecker.TypeCheckerFailure msg -> 
+      prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
+      prerr_endline (Lazy.force msg);
+      assert false
   in
   let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
-  let ty = NCicSubstitution.subst_meta lc ty in
-  let metasenv, subst = unify test_eq_only metasenv subst context ty ty_t in
+  let lty = NCicSubstitution.subst_meta lc ty in
+  pp ("On the types: " ^ NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
+    ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t); 
+  let metasenv, subst = unify test_eq_only metasenv subst context lty ty_t in
   let (metasenv, subst), t = 
-    NCicMetaSubst.delift metasenv subst context n lc t
+    try NCicMetaSubst.delift metasenv subst context n lc t
+    with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg)
+    |    NCicMetaSubst.MetaSubstFailure msg -> raise (UnificationFailure msg)
   in
   (* Unifying the types may have already instantiated n. *)
   try
@@ -147,13 +170,20 @@ 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
     metasenv, subst
+(*D*)  in outside(); rc with exn -> outside (); raise exn
 
 and unify test_eq_only metasenv subst context t1 t2 =
+(*D*) inside 'U'; try let rc =
    let fo_unif test_eq_only metasenv subst t1 t2 =
+   (*D*) inside 'F'; try let rc = 
+     pp ("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ 
+         NCicPp.ppterm ~metasenv ~subst ~context t2);
      if t1 === t2 then
        metasenv, subst
      else
@@ -337,26 +367,51 @@ and unify test_eq_only metasenv subst context t1 t2 =
                raise (uncert_exc metasenv subst context t1 t2))
        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
        | _ -> raise (uncert_exc metasenv subst context t1 t2)
+    (*D*)  in outside(); rc with exn -> outside (); raise exn
     in
     let height_of = function
      | NCic.Const (Ref.Ref (_,Ref.Def h)) 
      | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h))) 
      | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_) 
      | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
-     | NCic.Meta _ -> max_int
      | _ -> 0
     in
+    let put_in_whd m1 m2 =
+      NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
+      NCicReduction.reduce_machine ~delta:max_int ~subst context m2,
+      false (* not in normal form *)
+    in
     let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) = 
       let h1 = height_of t1 in 
       let h2 = height_of t2 in
-      let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
-      NCicReduction.reduce_machine ~delta ~subst context m1,
-      NCicReduction.reduce_machine ~delta ~subst context m2,
-      delta
+      let delta = 
+        if flexible [t1] then max 0 (h2 - 1) else
+        if flexible [t2] then max 0 (h1 - 1) else
+        if h1 = h2 then max 0 (h1 -1) else min h1 h2 
+      in
+      pp ("DELTA STEP TO: " ^ string_of_int delta);
+      let m1' = NCicReduction.reduce_machine ~delta ~subst context m1 in
+      let m2' = NCicReduction.reduce_machine ~delta ~subst context m2 in
+      if (m1' == m1 && m2' == m2 && delta > 0) then
+         (* if we have as heads a Fix of height n>m>0 and another term of height
+          * m, we set delta = m. The Fix may or may not reduce, depending on its
+          * rec argument. if no reduction was performed we decrease delta to m-1
+          * to reduce the other term *)
+         let delta = delta - 1 in
+         pp ("DELTA STEP TO: " ^ string_of_int delta);
+         let m1' = NCicReduction.reduce_machine ~delta ~subst context m1 in
+         let m2' = NCicReduction.reduce_machine ~delta ~subst context m2 in
+         m1', m2', (m1 == m1' && m2 == m2') || delta = 0
+      else m1', m2', delta = 0
     in
-    let rec unif_machines metasenv subst = function
-      | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) ->
-        try
+    let rec unif_machines metasenv subst = 
+      function
+      | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),are_normal) ->
+    (*D*) inside 'M'; try let rc =
+         pp ((if are_normal then "*" else " ") ^ " " ^
+           NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^
+           " === " ^ 
+           NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2));
           let relevance = [] (* TO BE UNDERSTOOD 
             match t1 with
             | C.Const r -> NCicEnvironment.get_relevance r
@@ -365,7 +420,7 @@ and unify test_eq_only metasenv subst context t1 t2 =
               try
                 let t1 = NCicReduction.from_stack t1 in
                 let t2 = NCicReduction.from_stack t2 in
-                unif_machines metasenv subst (small_delta_step t1 t2)
+                unif_machines metasenv subst (put_in_whd t1 t2)
               with UnificationFailure _ | Uncertain _ when not b ->
                 metasenv, subst
           in
@@ -382,24 +437,29 @@ and unify test_eq_only metasenv subst context t1 t2 =
                    (NCicReduction.unwind (k1,e1,t1,List.rev l1)) 
                    (NCicReduction.unwind (k2,e2,t2,List.rev l2))
           in
-           check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
-        with UnificationFailure _ | Uncertain _ when delta > 0 ->
+        try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
+        with UnificationFailure _ | Uncertain _ when not are_normal ->
+(*
           let delta = delta - 1 in 
           let red = NCicReduction.reduce_machine ~delta ~subst context in
-          unif_machines metasenv subst (red m1,red m2,delta)
+*)
+          unif_machines metasenv subst (small_delta_step m1 m2)
+     (*D*)  in outside(); rc with exn -> outside (); raise exn
      in
      try fo_unif test_eq_only metasenv subst t1 t2
-     with UnificationFailure msg |Uncertain msg as exn 
-     when not (flexible [t1;t2]) -> 
+     with UnificationFailure msg | Uncertain msg as exn -> 
        try 
          unif_machines metasenv subst 
-          (small_delta_step (0,[],t1,[]) (0,[],t2,[]))
+          (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
        with 
        | UnificationFailure _ -> raise (UnificationFailure msg)
        | Uncertain _ -> raise exn
+(*D*)  in outside(); rc with exn -> outside (); raise exn
 ;;
 
-let unify = unify false;;
+let unify = 
+  indent := "";      
+  unify false;;