X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=components%2Fcic_unification%2FcicRefine.ml;h=026fc9cb1b3a72432043e279af82d7747b77645c;hb=e7367f2ef8e2629fce81c0177ed16779bc93986a;hp=2ef492bc8e99aa436ba9b74efafcaf85c34acf0b;hpb=40d489654171aeb8e96c6d5dcd3d8976705e8517;p=helm.git diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 2ef492bc8..026fc9cb1 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -1359,6 +1359,9 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il and coerce_to_something allow_coercions localization_tbl t infty expty subst metasenv context ugraph = + 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 @@ -1373,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 = @@ -1383,13 +1388,21 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il let newt, newty, subst, metasenv, ugraph = avoid_double_coercion context subst metasenv ugraph newt expty in - let subst,metasenv,ugraph1 = + let subst,metasenv,ugraph = fo_unif_subst subst context metasenv newhety expty ugraph in Some ((newt,newty), subst, metasenv, ugraph) with | 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 @@ -1408,38 +1421,208 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il if not allow_coercions || not !insert_coercions then enrich localization_tbl t exn else - let clean t subst context = - CicReduction.whd - ~delta:false context (CicMetaSubst.apply_subst subst t) - in + let whd = CicReduction.whd ~delta:false in + let clean t s c = whd c (CicMetaSubst.apply_subst s t) in let infty = clean infty subst context in let expty = clean expty subst context in - match infty, expty with - | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2) -> - (* covariant part *) - let name_con = Cic.Name "name_con" in - let name_t, ty_s_bo, bo = - match t with - | Cic.Lambda (name, src, bo) -> name, src, bo - | _ -> name_con,src,Cic.Appl[CicSubstitution.lift 1 t;Cic.Rel 1] + match infty, expty, t with + | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2), Cic.Fix (n,fl) -> + (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) -> + (* move this stuff away *) + 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 context_bo = (Some (name_t, Cic.Decl ty_s_bo)) :: context in - let (bo, _), subst, metasenv, ugraph = - coerce_to_something_aux - bo ty ty2 subst metasenv context_bo ugraph + 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 - (* contravariant part *) - let context_rel1 = (Some (name_t, Cic.Decl src2) :: context) in + let add_params + metasenv subst context uri tyno cty outty leftno i + = + let mytl = function [] -> [] | _::tl -> tl in + let rec aux context outty par k = function + | Cic.Prod (name, src, tgt) -> + Cic.Prod (name, src, + 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 = + let k = Cic.MutConstruct (uri,tyno,i,[]) in + if par <> [] then Cic.Appl (k::par) else k + in + CR.head_beta_reduce ~delta:false + (Cic.Appl [outty;k]) + | Cic.Appl (Cic.MutInd _::pl) -> + 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 context outty [] 1 cty + in + (* 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 = + try + match + CicTypeChecker.type_of_aux' ~subst metasenv context m + CicUniv.oblivion_ugraph + with + | Cic.MutInd _,_ -> [] + | Cic.Appl (Cic.MutInd _::args),_ -> + snd (HExtlib.split_nth leftno args) + | _ -> assert false + with CicTypeChecker.TypeCheckerFailure _ -> + let rec foo = + function 0 -> [] | n -> Cic.Implicit None :: foo (n-1) + in + foo rno + in + let new_outty = + keep_lambdas_and_put_expty context outty expty right_p m (rno+1) + in + let _,pl,subst,metasenv,ugraph = + List.fold_right2 + (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 + s m context ugraph + in + (i-1, pbo::acc, subst, metasenv, ugraph)) + cl pl (List.length pl, [], subst, metasenv, ugraph) + in + 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 = + 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 = coerce_to_something_aux - (Cic.Rel 1) (CicSubstitution.lift 1 src2) - (CicSubstitution.lift 1 src) subst metasenv context_rel1 ugraph + (Cic.Rel 1) (CS.lift 1 src2) + (CS.lift 1 src) subst metasenv context_src2 ugraph in - let coerced = - Cic.Lambda (name_t,src2, - CicSubstitution.subst rel1 (CicSubstitution.lift_from 2 1 bo)) + (* 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 - (coerced, expty), subst, metasenv, ugraph + 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 | _ -> coerce_atom_to_something t infty expty subst metasenv context ugraph in