X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=c8f6bdb59eb763e99cc03d7875804e6c412452f8;hb=9b09890767aaa93e512324f8e7f13e2cdeebac88;hp=7ea11f3120035edaf8d4c63e43f7be8830c270fd;hpb=002d456397be2f0046bb50356e80816f7296647d;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 7ea11f312..c8f6bdb59 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -22,12 +22,14 @@ 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 wrap_exc msg = function
@@ -99,7 +101,6 @@ let rec typeof
   ?(localise=fun _ -> Stdpp.dummy_loc) 
   ~look_for_coercion metasenv subst context term expty 
 =
-        prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context term);
   let force_ty metasenv subst context orig t infty expty =
     (*D*)inside 'F'; try let rc = 
     match expty with
@@ -163,10 +164,16 @@ let rec typeof
        metasenv, subst, t, NCicTypeChecker.typeof ~subst ~metasenv context t
     | C.Prod (name,(s as orig_s),(t as orig_t)) ->
        let metasenv, subst, s, s1 = typeof_aux metasenv subst context None s in
+       let metasenv, subst, s, s1 = 
+         force_to_sort ~look_for_coercion
+           metasenv subst context s orig_s localise s1 in
        let context1 = (name,(C.Decl s))::context in
        let metasenv, subst, t, s2 = typeof_aux metasenv subst context1 None t in
+       let metasenv, subst, t, s2 = 
+         force_to_sort ~look_for_coercion
+           metasenv subst context1 t orig_t localise s2 in
        let metasenv, subst, s, t, ty = 
-         sort_of_prod ~look_for_coercion localise metasenv subst 
+         sort_of_prod localise metasenv subst 
            context orig_s orig_t (name,s) t (s1,s2)
        in
        metasenv, subst, NCic.Prod(name,s,t), ty
@@ -295,9 +302,23 @@ and try_coercions
         (NCicPp.ppterm ~metasenv ~subst ~context expty))) exc)
   | (metasenv, newterm, newtype, meta)::tl ->
       try 
+          pp (lazy ( "UNIFICATION in CTX:\n"^ 
+            NCicPp.ppcontext ~metasenv ~subst context
+            ^ "\nMENV: " ^
+            NCicPp.ppmetasenv metasenv ~subst
+            ^ "\nOF: " ^
+            NCicPp.ppterm ~metasenv ~subst ~context meta ^  " === " ^
+            NCicPp.ppterm ~metasenv ~subst ~context t ^ "\n"));
         let metasenv, subst = 
           NCicUnification.unify metasenv subst context meta t
         in
+          pp (lazy ( "UNIFICATION in CTX:\n"^ 
+            NCicPp.ppcontext ~metasenv ~subst context
+            ^ "\nMENV: " ^
+            NCicPp.ppmetasenv metasenv ~subst
+            ^ "\nOF: " ^
+            NCicPp.ppterm ~metasenv ~subst ~context newtype ^  " === " ^
+            NCicPp.ppterm ~metasenv ~subst ~context expty ^ "\n"));
         let metasenv, subst = 
           if perform_unification then
             NCicUnification.unify metasenv subst context newtype expty
@@ -331,23 +352,18 @@ and force_to_sort
   | ty -> 
       try_coercions ~localise ~look_for_coercion metasenv subst context
         t orig_t ty (NCic.Sort (NCic.Type NCicEnvironment.type0)) false 
-         (RefineFailure (lazy (localise orig_t, 
+         (Uncertain (lazy (localise orig_t, 
          "The type of " ^ NCicPp.ppterm ~metasenv ~subst ~context t
          ^ " is not a sort: " ^ NCicPp.ppterm ~metasenv ~subst ~context ty)))
 
-and sort_of_prod ~look_for_coercion
+and sort_of_prod 
   localise metasenv subst context orig_s orig_t (name,s) t (t1, t2) 
 =
-   let metasenv, subst, s, t1 = 
-     force_to_sort 
-      ~look_for_coercion metasenv subst context s orig_s localise t1 in
-   let metasenv, subst, t, t2 = 
-     force_to_sort ~look_for_coercion metasenv subst ((name,C.Decl s)::context) 
-       t orig_t localise t2 in
+   (* force to sort is done in the Prod case in typeof *)
    match t1, t2 with
    | C.Sort _, C.Sort C.Prop -> metasenv, subst, s, t, t2
    | C.Sort (C.Type u1), C.Sort (C.Type u2) ->
-        metasenv, subst, s, t, C.Sort (C.Type (u1@u2)) 
+        metasenv, subst, s, t, C.Sort (C.Type (NCicEnvironment.max u1 u2)) 
    | C.Sort C.Prop,C.Sort (C.Type _) -> metasenv, subst, s, t, t2
    | C.Meta _, C.Sort _ 
    | C.Meta _, C.Meta (_,(_,_))
@@ -386,6 +402,10 @@ and eat_prods
               (("_",C.Decl ty_arg) :: context) `Type
           in
           let flex_prod = C.Prod ("_", ty_arg, meta) in
+          (* next line grants that ty_args is a type *)
+          let metasenv,subst, flex_prod, _ =
+           typeof ~look_for_coercion ~localise metasenv subst
+            context flex_prod None in
           pp (lazy ( "UNIFICATION in CTX:\n"^ 
             NCicPp.ppcontext ~metasenv ~subst context
             ^ "\nOF: " ^