fixed propagation under Fix/Lambda/Case of coercions, better names are

generated.

there is still a question for CSC about the context of the metavariables opened
by example 51 that seems too long.

code still needs some refactoring, auxiliary functions are ready to be
lambdalifet out.

potential slowdown: The coerce_atom_to_something now looks for the *best*
coercion, where best means the one that opens the least number of metas.

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index 7f378ed4b9919fb8b7003ddce9b756143f712e03..f6bc9a4450dfd2500e7c02d8e220be0e560f9c60 100644 (file)
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -1361,6 +1361,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
   =
     let module CS = CicSubstitution in
     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 =
       let coer = 
         CoercGraph.look_for_coercion metasenv subst context infty expty
@@ -1375,7 +1376,9 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
       | CoercGraph.SomeCoercion candidates -> 
           let uncertain = ref false in
           let selected = 
-            HExtlib.list_findopt
+(*             HExtlib.list_findopt *)
+            let posibilities =
+              HExtlib.filter_map
               (fun (metasenv,last,c) -> 
                try
                 let subst,metasenv,ugraph =
@@ -1392,6 +1395,14 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                | Uncertain _ -> uncertain := true; None
                | RefineFailure _ -> None)
               candidates
+            in
+            match 
+              List.fast_sort 
+                (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2) 
+                posibilities 
+            with
+            | [] -> None
+            | x::_ -> Some x
           in
           match selected with
           | Some x -> x
@@ -1424,9 +1435,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                     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 ~avoid_beta_redexes:true rel1 (CS.lift_from 2 1 bo)
-                   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
@@ -1458,7 +1467,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                       | _ -> assert false
                     in
                     let get_l_r_p n = function
-                            | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
+                      | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
                       | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
                           HExtlib.split_nth n args
                       | _ -> assert false
@@ -1472,7 +1481,10 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                       List.map 
                         (fun ty -> 
                           List.fold_left 
-                            (fun t p -> CS.subst ~avoid_beta_redexes:true p t)
+                            (fun t p -> match t with
+                              | Cic.Prod (_,_,t) ->
+                                  cs_subst p t
+                              | _-> assert false)
                             ty left_p) 
                         cl 
                     in
@@ -1502,12 +1514,16 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                        (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
                 | _ -> assert false
               in
-              let add_params uri tyno cty outty leftno i =
+              let add_params 
+                metasenv subst context uri tyno cty outty leftno i 
+              =
                 let mytl = function [] -> [] | _::tl -> tl in
-                let rec aux outty par k = function
+                let rec aux context outty par k = function
                   | Cic.Prod (name, src, tgt) ->
                       Cic.Prod (name, src, 
-                        aux (CS.lift 1 outty) (Cic.Rel k::par) (k+1) tgt)
+                        aux 
+                          (Some (name, Cic.Decl src) :: context)
+                        (CS.lift 1 outty) (Cic.Rel k::par) (k+1) tgt)
                   | Cic.MutInd _ ->
                       let par = mytl par in
                       let k = 
@@ -1517,23 +1533,26 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                       CR.head_beta_reduce ~delta:false 
                         (Cic.Appl [outty;k])
                   | Cic.Appl (Cic.MutInd _::pl) ->
-                      let par = mytl par in
-                      let left_p,right_p = HExtlib.split_nth leftno pl in
+                      let left_p,_ = HExtlib.split_nth leftno pl 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
                       CR.head_beta_reduce ~delta:false 
                         (Cic.Appl (outty ::right_p @ [k]))
                   | _ -> assert false
                 in
-                  aux outty [] 1 cty
-              in
-              let rec add_params2 expty = function
-                | Cic.Prod (name, src, tgt) ->
-                    Cic.Prod (name, src, add_params2 (CS.lift 1 expty) tgt)
-                | Cic.MutInd _ | Cic.Appl (Cic.MutInd _::_) -> expty
-                | _ -> assert false
+                  aux context outty [] 1 cty
               in
               (* constructors types with left params already instantiated *)
               let outty = CicMetaSubst.apply_subst subst outty in
@@ -1561,14 +1580,15 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
               in
               let _,pl,subst,metasenv,ugraph = 
                 List.fold_right2
-                  (fun cty pbo (i, acc, subst, metasenv, ugraph) -> 
-                     (* Pi k_par, outty right_par (K_i left_par k_par)*)
-                     let infty_pbo = add_params uri tyno cty outty leftno i in
-                     (* Pi k_par, expty *)
-                     let expty_pbo = add_params2 expty cty in
+                  (fun cty pbo (i, acc, s, m, ugraph) -> 
+                     (* Pi k_par, (naw_)outty right_par (K_i left_par k_par) *)
+                     let infty_pbo = 
+                       add_params m s context uri tyno cty outty leftno i in
+                     let expty_pbo = 
+                       add_params m s context uri tyno cty new_outty leftno i in
                      let (pbo, _), subst, metasenv, ugraph =
                        coerce_to_something_aux pbo infty_pbo expty_pbo 
-                         subst metasenv context ugraph
+                         s m context ugraph
                      in
                      (i-1, pbo::acc, subst, metasenv, ugraph))
                   cl pl (List.length pl, [], subst, metasenv, ugraph)
@@ -1576,7 +1596,10 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
               let t = Cic.MutCase(uri, tyno, new_outty, m, pl) in
               (t, expty), subst, metasenv, ugraph
           | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ -> 
-              let name_con = Cic.Name "name_con" in
+              let name_con = 
+                FreshNamesGenerator.mk_fresh_name 
+                  ~subst metasenv context Cic.Anonymous ~typ:src2
+              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 = 
@@ -1587,17 +1610,19 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
               (* 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 ~avoid_beta_redexes:true rel1 (CS.lift_from 2 1 bo)
+                | 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 ~avoid_beta_redexes:true rel1 (CS.lift_from 2 1 ty) in
+              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 ("coerced: "^ CicMetaSubst.ppterm_in_context 
+                ~metasenv subst coerced context)(;
+              (coerced, expty), subst, metasenv, ugraph
           | _ -> 
             coerce_atom_to_something t infty expty subst metasenv context ugraph
     in

diff --git a/matita/tests/coercions_propagation.ma b/matita/tests/coercions_propagation.ma
index f87052086bda26aa80eebde5acaac1fd370531ce..8ff8f9c759ba41d26541571040df79e6b11586af 100644 (file)
--- a/matita/tests/coercions_propagation.ma
+++ b/matita/tests/coercions_propagation.ma
@@ -50,7 +50,7 @@ qed.
 
 theorem test4: (∃n. 1 ≤ n) → ∃n. 0 < n.
  apply ((λn:nat.n) : (∃n. 1 ≤ n) → ∃n. 0 < n);
- cases name_con;
+ cases s;
  assumption.
 qed.
 
@@ -64,7 +64,7 @@ apply (
  in
   aux
 : nat → ∃n. 1 ≤ n);
-[ cases (aux name_con); simplify; ] autobatch;
+[ cases (aux n1); simplify; ] autobatch;
 qed.
 
 inductive NN (A:Type) : nat -> Type ≝
@@ -110,8 +110,7 @@ qed.
 
 theorem test51: ∀A,k. NN A k → ∃n:NN A (S k). PN ? ? n.
 intros 1;
-(* MANCA UN LIFT forse NEL FIX *)
-apply (
+letin xxx ≝ (
  let rec aux (w : nat) (n : NN A w) on n : NN A (S w) ≝
   match n in NN return λx.λm:NN A x.NN A (S x) with
    [ NO ⇒ NS A ? (NO A)
@@ -119,8 +118,8 @@ apply (
    ]
  in
   aux
-: ∀n:nat. NN A n → ∃m:NN A (S n). PN ? ? m);
-[ cases (aux name_con); simplify; ] autobatch;
+: ∀n:nat. NN A n → ∃m:NN A (S n). PN ? ? m); [3: apply xxx];
+unfold PN in aux ⊢ %; [cases (aux n2 n3)] autobatch
 qed.
 
 (* guarded troppo debole