From: Enrico Tassi Date: Fri, 7 Sep 2007 15:46:51 +0000 (+0000) Subject: when a coercion is passed through a case on right-params-free term m, X-Git-Tag: 0.4.95@7852~214 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=596125c5354c73f19fc57476166e5e8c5edacde8;p=helm.git when a coercion is passed through a case on right-params-free term m, branches and outtype are adjusted to receive an extra argument (refl m) to have extra assumptions on it substituded. see tests/coercions_russell.ma --- diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 026fc9cb1..e3e92d098 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -34,8 +34,10 @@ exception AssertFailure of string Lazy.t;; let insert_coercions = ref true let pack_coercions = ref true -let debug_print = fun _ -> ();; -(*let debug_print x = prerr_endline (Lazy.force x);;*) +let debug = false;; + +let debug_print = + if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ());; let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2" @@ -1425,8 +1427,10 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il 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 + let t = clean t subst context in 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 = @@ -1444,7 +1448,8 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il (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 *) + 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 -> @@ -1514,26 +1519,36 @@ 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 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 leftno i + metasenv subst context uri tyno cty outty mty m leftno i = - let mytl = function [] -> [] | _::tl -> tl in - let rec aux context outty par k = function + let rec aux context outty par k mty m = function | Cic.Prod (name, src, tgt) -> - Cic.Prod (name, src, + let t,k = aux (Some (name, Cic.Decl src) :: context) - (CS.lift 1 outty) (Cic.Rel k::par) (k+1) tgt) + (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 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.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,_ = HExtlib.split_nth leftno pl in + 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) @@ -1548,57 +1563,116 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il | _ -> assert false with CicTypeChecker.TypeCheckerFailure _ -> assert false in - CR.head_beta_reduce ~delta:false - (Cic.Appl (outty ::right_p @ [k])) + 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 cty + 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 = + let right_p, mty = 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) + | Cic.MutInd _ as mty,_ -> [], mty + | Cic.Appl (Cic.MutInd _::args) as mty,_ -> + snd (HExtlib.split_nth leftno args), mty | _ -> assert false - with CicTypeChecker.TypeCheckerFailure _ -> - let rec foo = - function 0 -> [] | n -> Cic.Implicit None :: foo (n-1) - in - foo rno + 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, 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 + (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 + (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 m context ugraph + 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 t = Cic.MutCase(uri, tyno, new_outty, m, pl) 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 Cic.Anonymous ~typ:src2 + ~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 *) @@ -1624,6 +1698,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il ~metasenv subst coerced context)); (coerced, expty), subst, metasenv, ugraph | _ -> + debug_print (lazy "ATOM"); coerce_atom_to_something t infty expty subst metasenv context ugraph in try