X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicRefine.ml;h=1f92a5fa881b95396c1eaf06fd2a06fdcc0fc1fc;hb=f820f75a0b94bcc6b6d31c9471c8921ce098427d;hp=844260480134d42fd61acc3efbae44b755ccd2ef;hpb=27b3610b7add7ee75eb25f8f01e0f1426c278f52;p=helm.git

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index 844260480..1f92a5fa8 100644
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -480,7 +480,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
             in
             let tl',applty,subst''',metasenv''',ugraph3 =
               eat_prods true subst'' metasenv'' context 
-                he hetype tlbody_and_type ugraph2
+                he' hetype tlbody_and_type ugraph2
             in
               avoid_double_coercion context 
                 subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
@@ -1099,7 +1099,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                 CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt);
                assert false
             | Uncertain _ ->
-               prerr_endline ("#### Coercion not packed (Uncercatin case): " ^
+               prerr_endline ("#### Coercion not packed (Uncerctain case): " ^
                 CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt);
                assert false)
       | _ -> assert false) (* the composite coercion must exist *)
@@ -1159,7 +1159,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
         ~f:(fun _ ->
           (lazy ("The term " ^
             CicMetaSubst.ppterm_in_context subst he
-             context ^ "(that has type " ^
+             context ^ " (that has type " ^
             CicMetaSubst.ppterm_in_context subst hetype
              context ^ ") is here applied to " ^
             string_of_int (List.length tlbody_and_type) ^
@@ -1182,7 +1182,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                        (* we search a coercion from hety to s *)
                        let coer, tgt_carr = 
                          let carr t subst context = 
-                           CicMetaSubst.apply_subst subst t 
+                           CicReduction.whd ~delta:false 
+                             context (CicMetaSubst.apply_subst subst t )
                          in
                          let c_hety = carr hety subst context in
                          let c_s = carr s subst context in 
@@ -1467,7 +1468,7 @@ let typecheck metasenv uri obj ~localization_tbl =
 ;;
 
 (* sara' piu' veloce che raffinare da zero? mah.... *)
-let pack_coercion metasenv t =
+let pack_coercion metasenv ctx t =
  let module C = Cic in
  let rec merge_coercions ctx =
    let aux = (fun (u,t) -> u,merge_coercions ctx t) in
@@ -1489,32 +1490,29 @@ let pack_coercion metasenv t =
    | C.LetIn (name,so,dest) -> 
        let ctx' = Some (name,(C.Def (so,None)))::ctx in
        C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
-   | C.Appl l as t -> 
+   | C.Appl l -> 
+      let l = List.map (merge_coercions ctx) l in
+      let t = C.Appl l in
        let b,_,_,_ = is_a_double_coercion t in
        (* prerr_endline "CANDIDATO!!!!"; *)
-       let newt = 
-         if b then
-           let ugraph = CicUniv.empty_ugraph in
-           let old_insert_coercions = !insert_coercions in
-           insert_coercions := false;
-           let newt, _, menv, _ = 
-             try 
-               type_of_aux' metasenv ctx t ugraph 
-             with RefineFailure _ | Uncertain _ -> 
-               prerr_endline (CicPp.ppterm t);
-               t, t, [], ugraph 
-           in
-           insert_coercions := old_insert_coercions;
-           if metasenv <> [] || menv = [] then 
-             newt 
-           else 
-             (prerr_endline "PUO' SUCCEDERE!!!!!";t)
-         else
-           t
-       in
-       (match newt with
-       | C.Appl l -> C.Appl (List.map (merge_coercions ctx) l)
-       | _ -> assert false)
+       if b then
+         let ugraph = CicUniv.empty_ugraph in
+         let old_insert_coercions = !insert_coercions in
+         insert_coercions := false;
+         let newt, _, menv, _ = 
+           try 
+             type_of_aux' metasenv ctx t ugraph 
+           with RefineFailure _ | Uncertain _ -> 
+             prerr_endline (CicPp.ppterm t);
+             t, t, [], ugraph 
+         in
+         insert_coercions := old_insert_coercions;
+         if metasenv <> [] || menv = [] then 
+           newt 
+         else 
+           (prerr_endline "PUO' SUCCEDERE!!!!!";t)
+       else
+         t
    | C.Var (uri,exp_named_subst) -> 
        let exp_named_subst = List.map aux exp_named_subst in
        C.Var (uri, exp_named_subst)
@@ -1531,7 +1529,7 @@ let pack_coercion metasenv t =
        let pl = List.map (merge_coercions ctx) pl in
        C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
    | C.Fix (fno, fl) ->
-       let ctx =
+       let ctx' =
          List.fold_left
            (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l) 
            ctx fl
@@ -1539,12 +1537,12 @@ let pack_coercion metasenv t =
        let fl = 
          List.map 
            (fun (name,idx,ty,bo) -> 
-             (name,idx,merge_coercions ctx ty,merge_coercions ctx bo)) 
+             (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo)) 
          fl
        in
        C.Fix (fno, fl)
    | C.CoFix (fno, fl) ->
-       let ctx =
+       let ctx' =
          List.fold_left
            (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l) 
            ctx fl
@@ -1552,12 +1550,12 @@ let pack_coercion metasenv t =
        let fl = 
          List.map 
            (fun (name,ty,bo) -> 
-             (name, merge_coercions ctx ty, merge_coercions ctx bo)) 
+             (name, merge_coercions ctx ty, merge_coercions ctx' bo)) 
          fl 
        in
        C.CoFix (fno, fl)
  in
- merge_coercions [] t
+  merge_coercions ctx t
 ;;
 
 let pack_coercion_obj obj =
@@ -1567,48 +1565,52 @@ let pack_coercion_obj obj =
       let body = 
         match body with 
         | None -> None 
-        | Some body -> Some (pack_coercion [] body) 
+        | Some body -> Some (pack_coercion [] [] body) 
       in
-      let ty = pack_coercion [] ty in
+      let ty = pack_coercion [] [] ty in
         C.Constant (id, body, ty, params, attrs)
   | C.Variable (name, body, ty, params, attrs) ->
       let body = 
         match body with 
         | None -> None 
-        | Some body -> Some (pack_coercion [] body) 
+        | Some body -> Some (pack_coercion [] [] body) 
       in
-      let ty = pack_coercion [] ty in
+      let ty = pack_coercion [] [] ty in
         C.Variable (name, body, ty, params, attrs)
   | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
       let conjectures = 
         List.map 
           (fun (i, ctx, ty) -> 
             let ctx = 
-              List.map 
-                (function 
-                | Some (name, C.Decl t) -> 
-                    Some (name, C.Decl (pack_coercion conjectures t))
-                | Some (name, C.Def (t,None)) -> 
-                    Some (name, C.Def (pack_coercion conjectures t, None))
-                | Some (name, C.Def (t,Some ty)) -> 
-                    Some (name, C.Def (pack_coercion conjectures t, 
-                                    Some (pack_coercion conjectures ty)))
-                | None -> None) 
-                ctx 
+              List.fold_right 
+                (fun item ctx ->
+                  let item' =
+                   match item with
+                      Some (name, C.Decl t) -> 
+                        Some (name, C.Decl (pack_coercion conjectures ctx t))
+                    | Some (name, C.Def (t,None)) -> 
+                        Some (name,C.Def (pack_coercion conjectures ctx t,None))
+                    | Some (name, C.Def (t,Some ty)) -> 
+                        Some (name, C.Def (pack_coercion conjectures ctx t, 
+                                       Some (pack_coercion conjectures ctx ty)))
+                    | None -> None
+                  in
+                   item'::ctx
+                ) ctx []
             in
-            ((i,ctx,pack_coercion conjectures ty))) 
-          conjectures
+             ((i,ctx,pack_coercion conjectures ctx ty))
+          ) conjectures
       in
-      let body = pack_coercion conjectures body in
-      let ty = pack_coercion conjectures ty in
+      let body = pack_coercion conjectures [] body in
+      let ty = pack_coercion conjectures [] ty in
       C.CurrentProof (name, conjectures, body, ty, params, attrs)
   | C.InductiveDefinition (indtys, params, leftno, attrs) ->
       let indtys = 
         List.map 
           (fun (name, ind, arity, cl) -> 
-            let arity = pack_coercion [] arity in
+            let arity = pack_coercion [] [] arity in
             let cl = 
-              List.map (fun (name, ty) -> (name,pack_coercion [] ty)) cl 
+              List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl 
             in
             (name, ind, arity, cl))
           indtys
@@ -1644,3 +1646,5 @@ let type_of_aux' ?localization_tbl metasenv context term ugraph =
 
 let typecheck ~localization_tbl metasenv uri obj =
  profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
+
+let _ = DoubleTypeInference.pack_coercion := pack_coercion;;