]> matita.cs.unibo.it Git - helm.git/commitdiff
in the case of coerce_to_sort the whd was done with delta:true, that caused an incred...
authorEnrico Tassi <enrico.tassi@inria.fr>
Sun, 9 Sep 2007 15:16:46 +0000 (15:16 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sun, 9 Sep 2007 15:16:46 +0000 (15:16 +0000)
more debug printings added and some comments for vim folding mechanism

helm/software/components/cic_unification/cicRefine.ml

index 1242a1cded879cb24a21c7d3be344f34a8228d1b..9fb3548d6e4362d8a621b50939f55f85763b5b18 100644 (file)
@@ -328,21 +328,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
     let module C = Cic in
     let module S = CicSubstitution in
     let module U = UriManager in
-(*
-    let try_coercion t subst context ugraph coercion_tgt (metasenv,last,coerced) =
-     let subst,metasenv,ugraph =
-      fo_unif_subst subst context metasenv last t ugraph
-     in
-      try
-        let newt, tty, subst, metasenv, ugraph = 
-         avoid_double_coercion context subst metasenv ugraph coerced
-          coercion_tgt
-        in
-          Some (newt, tty, subst, metasenv, ugraph)
-      with 
-      | RefineFailure _ | Uncertain _ -> None
-    in
-*)
      let (t',_,_,_,_) as res =
       match t with
           (*    function *)
@@ -1308,6 +1293,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
     let module CR = CicReduction in
     let cs_subst = CS.subst ~avoid_beta_redexes:true in
     let coerce_atom_to_something t infty expty subst metasenv context ugraph =
+      debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
       let coer = 
         CoercGraph.look_for_coercion metasenv subst context infty expty
       in
@@ -1319,8 +1305,8 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
       | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
           "coerce_atom_to_something fails since no coercions found"))
       | CoercGraph.SomeCoercion candidates -> 
-          debug_print (lazy (string_of_int (List.length candidates) ^ "
-          candidates found"));
+          debug_print (lazy (string_of_int (List.length candidates) ^ 
+            " candidates found"));
           let uncertain = ref false in
           let selected = 
             let posibilities =
@@ -1336,7 +1322,6 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                 let subst,metasenv,ugraph =
                  fo_unif_subst subst context metasenv last t ugraph
                 in
-
                 let newt,newhety,subst,metasenv,ugraph = 
                  type_of_aux subst metasenv context c ugraph in
                 let newt, newty, subst, metasenv, ugraph = 
@@ -1384,280 +1369,284 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
           CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
           CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
           CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
-          match infty, expty, t with
-          | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2), Cic.Fix (n,fl) ->
-              debug_print (lazy "FIX");
-             (match fl with
-                 [name,i,_(* infty *),bo] ->
-                   let context_bo =
-                    Some (Cic.Name name,Cic.Decl expty)::context in
-                   let (rel1, _), subst, metasenv, ugraph =
-                    coerce_to_something_aux (Cic.Rel 1) 
-                      (CS.lift 1 expty) (CS.lift 1 infty) subst
-                     metasenv context_bo ugraph in
-                   let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
-                   let (bo,_), subst, metasenv, ugraph =
-                    coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
-                    expty) subst
-                     metasenv context_bo ugraph
-                   in
-                    (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
-               | _ -> assert false (* not implemented yet *))
-          | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
-              debug_print (lazy "CASE");
-              (* {{{ helper functions *)
-              let get_cl_and_left_p uri tyno outty ugraph =
-                match CicEnvironment.get_obj ugraph uri with
-                | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
-                    let count_pis t =
-                      let rec aux ctx t = 
-                        match CicReduction.whd ~delta:false ctx t with
-                        | Cic.Prod (name,src,tgt) ->
-                            let ctx = Some (name, Cic.Decl src) :: ctx in
-                            1 + aux ctx tgt
-                        | _ -> 0
-                      in
-                        aux [] t
-                    in
-                    let rec skip_lambda_delifting t n =
-                      match t,n with
-                      | _,0 -> t
-                      | Cic.Lambda (_,_,t),n -> 
-                          skip_lambda_delifting
-                            (CS.subst (Cic.Implicit None) t) (n - 1)
-                      | _ -> assert false
-                    in
-                    let get_l_r_p n = function
-                      | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
-                      | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
-                          HExtlib.split_nth n args
-                      | _ -> assert false
+          let (coerced,_),subst,metasenv,_ as result = 
+           match infty, expty, t with
+           | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
+              (*{{{*) debug_print (lazy "FIX");
+              (match fl with
+                  [name,i,_(* infty *),bo] ->
+                    let context_bo =
+                     Some (Cic.Name name,Cic.Decl expty)::context in
+                    let (rel1, _), subst, metasenv, ugraph =
+                     coerce_to_something_aux (Cic.Rel 1) 
+                       (CS.lift 1 expty) (CS.lift 1 infty) subst
+                      metasenv context_bo ugraph in
+                    let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
+                    let (bo,_), subst, metasenv, ugraph =
+                     coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
+                     expty) subst
+                      metasenv context_bo ugraph
                     in
-                    let _, _, ty, cl = List.nth tl tyno in
-                    let pis = count_pis ty in
-                    let rno = pis - leftno in
-                    let t = skip_lambda_delifting outty rno in
-                    let left_p, _ = get_l_r_p leftno t in
-                    let instantiale_with_left cl =
-                      List.map 
-                        (fun ty -> 
-                          List.fold_left 
-                            (fun t p -> match t with
-                              | Cic.Prod (_,_,t) ->
-                                  cs_subst p t
-                              | _-> assert false)
-                            ty left_p) 
-                        cl 
-                    in
-                    let cl = instantiale_with_left (List.map snd cl) in
-                    cl, left_p, leftno, rno, ugraph
-                | _ -> raise exn
-              in
-              let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
-                match t,n with
-                | _,0 ->
-                  let rec mkr n = function 
-                    | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
-                  in
-                  let bo =
-                  CicReplace.replace_lifting
-                    ~equality:(fun _ -> CicUtil.alpha_equivalence)
-                    ~context:ctx
-                    ~what:(matched::right_p)
-                    ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
-                    ~where:bo
-                  in
-                  bo
-                | Cic.Lambda (name, src, tgt),_ ->
-                    Cic.Lambda (name, src,
+                     (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
+                | _ -> assert false (* not implemented yet *)) (*}}}*)
+           | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
+               (*{{{*) debug_print (lazy "CASE");
+               (* {{{ helper functions *)
+               let get_cl_and_left_p uri tyno outty ugraph =
+                 match CicEnvironment.get_obj ugraph uri with
+                 | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
+                     let count_pis t =
+                       let rec aux ctx t = 
+                         match CicReduction.whd ~delta:false ctx t with
+                         | Cic.Prod (name,src,tgt) ->
+                             let ctx = Some (name, Cic.Decl src) :: ctx in
+                             1 + aux ctx tgt
+                         | _ -> 0
+                       in
+                         aux [] t
+                     in
+                     let rec skip_lambda_delifting t n =
+                       match t,n with
+                       | _,0 -> t
+                       | Cic.Lambda (_,_,t),n -> 
+                           skip_lambda_delifting
+                             (CS.subst (Cic.Implicit None) t) (n - 1)
+                       | _ -> assert false
+                     in
+                     let get_l_r_p n = function
+                       | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
+                       | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
+                           HExtlib.split_nth n args
+                       | _ -> assert false
+                     in
+                     let _, _, ty, cl = List.nth tl tyno in
+                     let pis = count_pis ty in
+                     let rno = pis - leftno in
+                     let t = skip_lambda_delifting outty rno in
+                     let left_p, _ = get_l_r_p leftno t in
+                     let instantiale_with_left cl =
+                       List.map 
+                         (fun ty -> 
+                           List.fold_left 
+                             (fun t p -> match t with
+                               | Cic.Prod (_,_,t) ->
+                                   cs_subst p t
+                               | _-> assert false)
+                             ty left_p) 
+                         cl 
+                     in
+                     let cl = instantiale_with_left (List.map snd cl) in
+                     cl, left_p, leftno, rno, ugraph
+                 | _ -> raise exn
+               in
+               let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
+                 match t,n with
+                 | _,0 ->
+                   let rec mkr n = function 
+                     | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
+                   in
+                   let bo =
+                   CicReplace.replace_lifting
+                     ~equality:(fun _ -> CicUtil.alpha_equivalence)
+                     ~context:ctx
+                     ~what:(matched::right_p)
+                     ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
+                     ~where:bo
+                   in
+                   bo
+                 | Cic.Lambda (name, src, tgt),_ ->
+                     Cic.Lambda (name, src,
                       keep_lambdas_and_put_expty 
                        (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
                        (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
-                | _ -> assert false
-              in
-              let eq_uri, eq, eq_refl = 
-                match LibraryObjects.eq_URI () with 
-                | None -> HLog.warn "no default equality"; raise exn
-                | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
-              in
-              let add_params 
-                metasenv subst context uri tyno cty outty mty m leftno i 
-              =
-                let rec aux context outty par k mty m = function
-                  | Cic.Prod (name, src, tgt) ->
-                      let t,k = 
-                        aux 
-                          (Some (name, Cic.Decl src) :: context)
-                          (CS.lift 1 outty) (Cic.Rel k::par) (k+1) 
-                          (CS.lift 1 mty) (CS.lift 1 m) tgt
-                      in
-                      Cic.Prod (name, src, t), k
-                  | Cic.MutInd _ ->
-                      let k = 
-                        let k = Cic.MutConstruct (uri,tyno,i,[]) in
-                        if par <> [] then Cic.Appl (k::par) else k
-                      in
-                      Cic.Prod (Cic.Name "p", 
-                       Cic.Appl [eq; mty; m; k],
-                       (CS.lift 1
-                        (CR.head_beta_reduce ~delta:false 
-                         (Cic.Appl [outty;k])))),k
-                  | Cic.Appl (Cic.MutInd _::pl) ->
-                      let left_p,right_p = HExtlib.split_nth leftno pl in
-                      let has_rights = right_p <> [] in
-                      let k = 
-                        let k = Cic.MutConstruct (uri,tyno,i,[]) in
-                        Cic.Appl (k::left_p@par)
-                      in
-                      let right_p = 
-                        try match 
-                          CicTypeChecker.type_of_aux' ~subst metasenv context k
-                            CicUniv.oblivion_ugraph 
-                        with
-                        | Cic.Appl (Cic.MutInd _::args),_ ->
-                            snd (HExtlib.split_nth leftno args)
-                        | _ -> assert false
-                        with CicTypeChecker.TypeCheckerFailure _ -> assert false
-                      in
-                      if has_rights then
-                        CR.head_beta_reduce ~delta:false 
-                          (Cic.Appl (outty ::right_p @ [k])),k
-                      else
-                        Cic.Prod (Cic.Name "p", 
-                         Cic.Appl [eq; mty; m; k],
-                         (CS.lift 1
-                          (CR.head_beta_reduce ~delta:false 
-                           (Cic.Appl (outty ::right_p @ [k]))))),k
-                  | _ -> assert false
-                in
-                  aux context outty [] 1 mty m cty
-              in
-              let add_lambda_for_refl_m pbo rno mty m k cty =
-                (* k lives in the right context *)
-                if rno <> 0 then pbo else
-                let rec aux mty m = function 
-                  | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
-                     Cic.Lambda (name,src,
-                      (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
-                  | t,_ -> 
-                      Cic.Lambda (Cic.Name "p",
-                        Cic.Appl [eq; mty; m; k],CS.lift 1 t)
-                in
-                aux mty m (pbo,cty)
-              in
-              let add_pi_for_refl_m new_outty mty m rno =
-                if rno <> 0 then new_outty else
-                  let rec aux m mty = function
-                    | Cic.Lambda (name, src, tgt) ->
-                        Cic.Lambda (name, src, 
-                          aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
-                    | t ->
-                        Cic.Prod 
-                          (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
-                          CS.lift 1 t)
-                  in
-                    aux m mty new_outty
-              in (* }}} end helper functions *)
-              (* constructors types with left params already instantiated *)
-              let outty = CicMetaSubst.apply_subst subst outty in
-              let cl, left_p, leftno,rno,ugraph = 
-                get_cl_and_left_p uri tyno outty ugraph 
-              in
-              let right_p, mty = 
-                try
-                  match 
-                    CicTypeChecker.type_of_aux' ~subst metasenv context m
-                      CicUniv.oblivion_ugraph 
-                  with
-                  | Cic.MutInd _ as mty,_ -> [], mty
-                  | Cic.Appl (Cic.MutInd _::args) as mty,_ ->
-                      snd (HExtlib.split_nth leftno args), mty
-                  | _ -> assert false
-                with CicTypeChecker.TypeCheckerFailure _ -> assert false
-              in
-              let new_outty =
+                 | _ -> assert false
+               in
+               let eq_uri, eq, eq_refl = 
+                 match LibraryObjects.eq_URI () with 
+                 | None -> HLog.warn "no default equality"; raise exn
+                 | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
+               in
+               let add_params 
+                 metasenv subst context uri tyno cty outty mty m leftno i 
+               =
+                 let rec aux context outty par k mty m = function
+                   | Cic.Prod (name, src, tgt) ->
+                       let t,k = 
+                         aux 
+                           (Some (name, Cic.Decl src) :: context)
+                           (CS.lift 1 outty) (Cic.Rel k::par) (k+1) 
+                           (CS.lift 1 mty) (CS.lift 1 m) tgt
+                       in
+                       Cic.Prod (name, src, t), k
+                   | Cic.MutInd _ ->
+                       let k = 
+                         let k = Cic.MutConstruct (uri,tyno,i,[]) in
+                         if par <> [] then Cic.Appl (k::par) else k
+                       in
+                       Cic.Prod (Cic.Name "p", 
+                        Cic.Appl [eq; mty; m; k],
+                        (CS.lift 1
+                         (CR.head_beta_reduce ~delta:false 
+                          (Cic.Appl [outty;k])))),k
+                   | Cic.Appl (Cic.MutInd _::pl) ->
+                       let left_p,right_p = HExtlib.split_nth leftno pl in
+                       let has_rights = right_p <> [] in
+                       let k = 
+                         let k = Cic.MutConstruct (uri,tyno,i,[]) in
+                         Cic.Appl (k::left_p@par)
+                       in
+                       let right_p = 
+                         try match 
+                           CicTypeChecker.type_of_aux' ~subst metasenv context k
+                             CicUniv.oblivion_ugraph 
+                         with
+                         | Cic.Appl (Cic.MutInd _::args),_ ->
+                             snd (HExtlib.split_nth leftno args)
+                         | _ -> assert false
+                         with CicTypeChecker.TypeCheckerFailure _-> assert false
+                       in
+                       if has_rights then
+                         CR.head_beta_reduce ~delta:false 
+                           (Cic.Appl (outty ::right_p @ [k])),k
+                       else
+                         Cic.Prod (Cic.Name "p", 
+                          Cic.Appl [eq; mty; m; k],
+                          (CS.lift 1
+                           (CR.head_beta_reduce ~delta:false 
+                            (Cic.Appl (outty ::right_p @ [k]))))),k
+                   | _ -> assert false
+                 in
+                   aux context outty [] 1 mty m cty
+               in
+               let add_lambda_for_refl_m pbo rno mty m k cty =
+                 (* k lives in the right context *)
+                 if rno <> 0 then pbo else
+                 let rec aux mty m = function 
+                   | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
+                      Cic.Lambda (name,src,
+                       (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
+                   | t,_ -> 
+                       Cic.Lambda (Cic.Name "p",
+                         Cic.Appl [eq; mty; m; k],CS.lift 1 t)
+                 in
+                 aux mty m (pbo,cty)
+               in
+               let add_pi_for_refl_m new_outty mty m rno =
+                 if rno <> 0 then new_outty else
+                   let rec aux m mty = function
+                     | Cic.Lambda (name, src, tgt) ->
+                         Cic.Lambda (name, src, 
+                           aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
+                     | t ->
+                         Cic.Prod 
+                           (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
+                           CS.lift 1 t)
+                   in
+                     aux m mty new_outty
+               in (* }}} end helper functions *)
+               (* constructors types with left params already instantiated *)
+               let outty = CicMetaSubst.apply_subst subst outty in
+               let cl, left_p, leftno,rno,ugraph = 
+                 get_cl_and_left_p uri tyno outty ugraph 
+               in
+               let right_p, mty = 
+                 try
+                   match 
+                     CicTypeChecker.type_of_aux' ~subst metasenv context m
+                       CicUniv.oblivion_ugraph 
+                   with
+                   | Cic.MutInd _ as mty,_ -> [], mty
+                   | Cic.Appl (Cic.MutInd _::args) as mty,_ ->
+                       snd (HExtlib.split_nth leftno args), mty
+                   | _ -> assert false
+                 with CicTypeChecker.TypeCheckerFailure _ -> assert false
+               in
+               let new_outty =
                 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
-              in
-              debug_print 
-                (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context 
-                 ~metasenv subst new_outty context));
-              let _,pl,subst,metasenv,ugraph = 
-                List.fold_right2
-                  (fun cty pbo (i, acc, s, menv, ugraph) -> 
-                    (* Pi k_par, (Pi H:m=(K_i left_par k_par)), 
-                     *   (new_)outty right_par (K_i left_par k_par) *)
-                     let infty_pbo, _ = 
-                       add_params menv s context uri tyno 
-                         cty outty mty m leftno i in
-                     debug_print 
+               in
+               debug_print 
+                 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context 
+                  ~metasenv subst new_outty context));
+               let _,pl,subst,metasenv,ugraph = 
+                 List.fold_right2
+                   (fun cty pbo (i, acc, s, menv, ugraph) -> 
+                     (* Pi k_par, (Pi H:m=(K_i left_par k_par)), 
+                      *   (new_)outty right_par (K_i left_par k_par) *)
+                      let infty_pbo, _ = 
+                        add_params menv s context uri tyno 
+                          cty outty mty m leftno i in
+                      debug_print 
                        (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
-                       ~metasenv subst infty_pbo context));
-                     let expty_pbo, k = (* k is (K_i left_par k_par) *)
-                       add_params menv s context uri tyno 
-                         cty new_outty mty m leftno i in
-                     debug_print 
+                        ~metasenv subst infty_pbo context));
+                      let expty_pbo, k = (* k is (K_i left_par k_par) *)
+                        add_params menv s context uri tyno 
+                          cty new_outty mty m leftno i in
+                      debug_print 
                        (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
-                       ~metasenv subst expty_pbo context));
-                     let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
-                     debug_print 
-                       (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context 
-                       ~metasenv subst pbo context));
-                     let (pbo, _), subst, metasenv, ugraph =
-                       coerce_to_something_aux pbo infty_pbo expty_pbo 
-                         s menv context ugraph
-                     in
-                     debug_print 
-                       (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context 
-                       ~metasenv subst pbo context));
-                     (i-1, pbo::acc, subst, metasenv, ugraph))
-                  cl pl (List.length pl, [], subst, metasenv, ugraph)
-              in
-              let new_outty = add_pi_for_refl_m new_outty mty m rno in
-              debug_print 
-                (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context 
-                 ~metasenv subst new_outty context));
-              let t = 
-                if rno = 0 then
-                  let refl_m=Cic.Appl[eq_refl;mty;m]in
-                  Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m] 
-                else 
-                  Cic.MutCase(uri,tyno,new_outty,m,pl)
-              in
-              (t, expty), subst, metasenv, ugraph
-          | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ -> 
-              debug_print (lazy "LAM");
-              let name_con = 
-                FreshNamesGenerator.mk_fresh_name 
-                  ~subst metasenv context ~typ:src2 Cic.Anonymous
-              in
-              let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
-              (* contravariant part: the argument of f:src->ty *)
-              let (rel1, _), subst, metasenv, ugraph = 
-                coerce_to_something_aux
-                 (Cic.Rel 1) (CS.lift 1 src2) 
-                 (CS.lift 1 src) subst metasenv context_src2 ugraph
-              in
-              (* covariant part: the result of f(c x); x:src2; (c x):src *)
-              let name_t, bo = 
-                match t with
-                | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
-                | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
-              in
-              (* we fix the possible dependency problem in the source ty *)
-              let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
-              let (bo, _), subst, metasenv, ugraph = 
-                coerce_to_something_aux
-                  bo ty ty2 subst metasenv context_src2 ugraph
-              in
-              let coerced = Cic.Lambda (name_t,src2, bo) in
-              debug_print (lazy ("coerced: "^ CicMetaSubst.ppterm_in_context 
-                ~metasenv subst coerced context));
-              (coerced, expty), subst, metasenv, ugraph
-          | _ -> 
-              debug_print (lazy ("ATOM: " ^ CicMetaSubst.ppterm_in_context
-              ~metasenv subst infty context ^ " ==> " ^
-              CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
-            coerce_atom_to_something t infty expty subst metasenv context ugraph
+                        ~metasenv subst expty_pbo context));
+                      let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
+                      debug_print 
+                        (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context 
+                        ~metasenv subst pbo context));
+                      let (pbo, _), subst, metasenv, ugraph =
+                        coerce_to_something_aux pbo infty_pbo expty_pbo 
+                          s menv context ugraph
+                      in
+                      debug_print 
+                        (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context 
+                        ~metasenv subst pbo context));
+                      (i-1, pbo::acc, subst, metasenv, ugraph))
+                   cl pl (List.length pl, [], subst, metasenv, ugraph)
+               in
+               let new_outty = add_pi_for_refl_m new_outty mty m rno in
+               debug_print 
+                 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context 
+                  ~metasenv subst new_outty context));
+               let t = 
+                 if rno = 0 then
+                   let refl_m=Cic.Appl[eq_refl;mty;m]in
+                   Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m] 
+                 else 
+                   Cic.MutCase(uri,tyno,new_outty,m,pl)
+               in
+               (t, expty), subst, metasenv, ugraph (*}}}*)
+           | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ -> 
+               (*{{{*) debug_print (lazy "LAM");
+               let name_con = 
+                 FreshNamesGenerator.mk_fresh_name 
+                   ~subst metasenv context ~typ:src2 Cic.Anonymous
+               in
+               let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
+               (* contravariant part: the argument of f:src->ty *)
+               let (rel1, _), subst, metasenv, ugraph = 
+                 coerce_to_something_aux
+                  (Cic.Rel 1) (CS.lift 1 src2) 
+                  (CS.lift 1 src) subst metasenv context_src2 ugraph
+               in
+               (* covariant part: the result of f(c x); x:src2; (c x):src *)
+               let name_t, bo = 
+                 match t with
+                 | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
+                 | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
+               in
+               (* we fix the possible dependency problem in the source ty *)
+               let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
+               let (bo, _), subst, metasenv, ugraph = 
+                 coerce_to_something_aux
+                   bo ty ty2 subst metasenv context_src2 ugraph
+               in
+               let coerced = Cic.Lambda (name_t,src2, bo) in
+               (coerced, expty), subst, metasenv, ugraph (*}}}*)
+           | _ -> 
+               (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
+                ~metasenv subst infty context ^ " ==> " ^
+                CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
+               coerce_atom_to_something
+               t infty expty subst metasenv context ugraph (*}}}*)
+          in
+          debug_print (lazy ("COERCE TO SOMETHING END: "^
+            CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
+          result
     in
     try
       coerce_to_something_aux t infty expty subst metasenv context ugraph
@@ -1672,16 +1661,20 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
         enrich localization_tbl ~f t exn
 
   and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
-    match CicReduction.whd ~subst:subst context infty with
+    match CicReduction.whd ~delta:false ~subst context infty with
     | Cic.Meta _ | Cic.Sort _ -> 
         t,infty, subst, metasenv, ugraph
     | src ->
+       debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
+         ~metasenv subst src context));
        let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
        try
          let (t, ty_t), subst, metasenv, ugraph =
            coerce_to_something true
              localization_tbl t src tgt subst metasenv context ugraph
          in
+         debug_print (lazy ("COERCE TO SORT END: "^ 
+           CicMetaSubst.ppterm_in_context ~metasenv subst t context));
          t, ty_t, subst, metasenv, ugraph
        with HExtlib.Localized (_, exn) -> 
          let f _ =