X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=d3c86d2816c2c9bd050bbe1b336d033d95e4c8dd;hb=1ee5193677b8e2a80d4f068ee79ecac335de1196;hp=a12ef1164dd8fbc0bf54eb03fb1c4db1860ceacf;hpb=68e7533f986352a86ea0288909b27f83d44893a6;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index a12ef1164..d3c86d281 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -72,13 +72,23 @@ 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 ^ " " ^ Lazy.force s)
 ;;  
-*)
 
-let pp _ = ();;
+(* let pp _ = ();; *)
+
+let fix_sorts metasenv subst context meta t =
+  let rec aux () = function
+    | NCic.Sort (NCic.Type u) as orig ->
+       (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))
+    | 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' =
@@ -142,24 +152,45 @@ and beta_expand_many test_equality_only swap metasenv subst context t args =
 (* (*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
+  let fix_sorts t = 
+    if swap then fix_sorts metasenv subst context (NCic.Meta (n,lc)) t
+    else 
+      NCic.Sort (NCic.Type (
+        match NCicEnvironment.sup NCicEnvironment.type0 with Some x ->x| _ ->
+                assert false))
   in
   let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
-  let lty = NCicSubstitution.subst_meta lc ty in
-  pp (lazy("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 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 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 msg -> 
+              prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context ft);
+              prerr_endline (Lazy.force msg);
+              assert false
+       in
+       let lty = NCicSubstitution.subst_meta lc ty in
+       pp (lazy("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
+       metasenv, subst, t
+  in
   let (metasenv, subst), t = 
     try NCicMetaSubst.delift metasenv subst context n lc t
     with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg)
@@ -169,6 +200,7 @@ 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 _ -> 
@@ -176,21 +208,19 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
      * 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:ctx (NCicSubstitution.subst_meta lc t)));
+      ~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 =  *)
-(*
+    (*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
@@ -374,7 +404,7 @@ 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)) 
@@ -385,36 +415,27 @@ and unify test_eq_only metasenv subst context t1 t2 =
     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 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 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 (lazy("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 (lazy("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
+      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 = *)
+      | ((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) ^
@@ -447,9 +468,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 ->
-          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 -> 
@@ -459,7 +480,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 =