X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=202e68e4c86c3d056a8914451a70b6c4b25aae13;hb=04c05cf08605156ba8c6fa7225b4a90496c03698;hp=99286591d9c2f01c0b67f5f362bccf6f4ebec482;hpb=1ef41da37d7b39da1521f53d3b22981556bfbe68;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 99286591d..202e68e4c 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -74,11 +74,30 @@ let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
 
 (*
 let pp s = 
- prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ s);; 
+  prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
+;;  
 *)
 
 let pp _ = ();;
 
+let fix_sorts swap metasenv subst context meta t =
+  let rec aux () = function
+    | NCic.Sort (NCic.Type u) as orig ->
+        if swap then
+         match NCicEnvironment.sup u with
+         | None ->  raise (fail_exc metasenv subst context meta t)
+         | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)
+        else
+         NCic.Sort (NCic.Type (
+           match NCicEnvironment.sup NCicEnvironment.type0 with 
+           | Some x -> x 
+           | _ -> assert false))
+    | NCic.Meta _ as orig -> orig
+    | t -> NCicUtils.map (fun _ _ -> ()) () aux t
+  in
+    aux () t
+;;
+
 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
@@ -122,9 +141,10 @@ 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);
+(* (*D*)  inside 'B'; try let rc = *)
+  pp (lazy (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) ->
@@ -134,29 +154,47 @@ 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);
+  pp (lazy ("Head syntesized by b-exp: " ^ 
+    NCicPp.ppterm ~metasenv ~subst ~context hd));
     metasenv, subst, hd
-(*D*)  in outside (); rc with exn -> outside (); raise exn
+(* (*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 = 
+ (*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 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 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 = 
+    match ty with 
+    | NCic.Implicit (`Typeof _) -> 
+       metasenv,subst,fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t
+    | _ ->
+       pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
+       let t, ty_t = 
+         try t, NCicTypeChecker.typeof ~subst ~metasenv context t 
+         with NCicTypeChecker.TypeCheckerFailure _ -> 
+           let ft = 
+            fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t
+           in
+           if ft == t then assert false
+           else
+            try 
+              pp (lazy ("typeof: " ^ 
+                NCicPp.ppterm ~metasenv ~subst ~context ft));
+              ft, NCicTypeChecker.typeof ~subst ~metasenv context ft 
+            with NCicTypeChecker.TypeCheckerFailure _ -> 
+              assert false
+       in
+       let lty = NCicSubstitution.subst_meta lc ty in
+       pp (lazy("On the types: " ^
+        NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^
+        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
+       metasenv, subst, t
+  in
   let (metasenv, subst), t = 
     try NCicMetaSubst.delift metasenv subst context n lc t
     with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg)
@@ -166,24 +204,27 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
   try
     let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
     let oldt = NCicSubstitution.subst_meta lc oldt in
+    let t = NCicSubstitution.subst_meta lc t in
     (* conjecture: always fail --> occur check *)
     unify test_eq_only metasenv subst context oldt t
   with NCicUtils.Subst_not_found _ -> 
     (* by cumulativity when unify(?,Type_i) 
      * we could ? := Type_j with j <= i... *)
     let subst = (n, (name, ctx, t, ty)) :: subst in
+    pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm
+      ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t)));
     let metasenv = 
       List.filter (fun (m,_) -> not (n = m)) metasenv 
     in
     metasenv, subst
-(*D*)  in outside(); rc with exn -> outside (); raise exn
+ (*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 =
+ (*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);
+    (*D*) inside 'F'; try let rc =  
+     pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ 
+         NCicPp.ppterm ~metasenv ~subst ~context t2));
      if t1 === t2 then
        metasenv, subst
      else
@@ -367,46 +408,44 @@ 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
+     (*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, false
-     | NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> 0, true
-     | _ -> 0, false
+     | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
+     | _ -> 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 *)
+      NCicReduction.reduce_machine ~delta:max_int ~subst context m2
     in
-    let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) = 
-      let h1, flex1 = height_of t1 in 
-      let h2, flex2 = height_of t2 in
-      let delta = 
-        if flex1 then max 0 (h2 - 1) else
-        if flex2 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
-      m1', m2', (m1' == m1 && m2' == m2) || delta = 0
-      (* if we have as heads two Fix of height n>0, they may or may not
-       * reduce, depending on their rec argument... we thus check if
-       * something changed or not. This relies on the reduction machine
-       * preserving the original machine if it performs no action *)
+    let small_delta_step 
+      ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
+    =
+     assert (not (norm1 && norm2));
+     if norm1 then
+      x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2
+     else if norm2 then
+      NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2
+     else 
+      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
     in
     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 " ") ^ " " ^
+      | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
+     (*D*) inside 'M'; try let rc = 
+(*
+         pp (lazy((if are_normal then "*" else " ") ^ " " ^
            NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^
            " === " ^ 
-           NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2));
+           NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2)));
+*)
           let relevance = [] (* TO BE UNDERSTOOD 
             match t1 with
             | C.Const r -> NCicEnvironment.get_relevance r
@@ -433,13 +472,9 @@ and unify test_eq_only metasenv subst context t1 t2 =
                    (NCicReduction.unwind (k2,e2,t2,List.rev l2))
           in
         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 (small_delta_step m1 m2)
-     (*D*)  in outside(); rc with exn -> outside (); raise exn
+        with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
+	    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 -> 
@@ -449,7 +484,7 @@ and unify test_eq_only metasenv subst context t1 t2 =
        with 
        | UnificationFailure _ -> raise (UnificationFailure msg)
        | Uncertain _ -> raise exn
-(*D*)  in outside(); rc with exn -> outside (); raise exn
+ (*D*)  in outside(); rc with exn -> outside (); raise exn 
 ;;
 
 let unify =