From c2c8816478b504e236cdc7f10cb96ca66dc33c32 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 7 Sep 2007 09:59:52 +0000 Subject: [PATCH] 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. --- .../components/cic_unification/cicRefine.ml | 81 ++++++++++++------- .../matita/tests/coercions_propagation.ma | 11 ++- 2 files changed, 58 insertions(+), 34 deletions(-) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 7f378ed4b..f6bc9a445 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/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/helm/software/matita/tests/coercions_propagation.ma b/helm/software/matita/tests/coercions_propagation.ma index f87052086..8ff8f9c75 100644 --- a/helm/software/matita/tests/coercions_propagation.ma +++ b/helm/software/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 -- 2.39.2