From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- pretyping/cases.ml | 101 ++++++++++++++++++++++++++++++----------------------- 1 file changed, 58 insertions(+), 43 deletions(-) (limited to 'pretyping/cases.ml') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index fe0f20f8..ac00015e 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -295,8 +295,11 @@ let inductive_template evdref env tmloc ind = | LocalAssum (na,ty) -> let ty = EConstr.of_constr ty in let ty' = substl subst ty in - let e = e_new_evar env evdref ~src:(hole_source n) ty' in - (e::subst,e::evarl,n+1) + let e = evd_comb1 + (Evarutil.new_evar env ~src:(hole_source n)) + evdref ty' + in + (e::subst,e::evarl,n+1) | LocalDef (na,b,ty) -> let b = EConstr.of_constr b in (substl subst b::subst,evarl,n+1)) @@ -314,13 +317,15 @@ let try_find_ind env sigma typ realnames = IsInd (typ,ind,names) let inh_coerce_to_ind evdref env loc ty tyi = - let sigma = !evdref in + let orig = !evdref in let expected_typ = inductive_template evdref env loc tyi in (* Try to refine the type with inductive information coming from the constructor and renounce if not able to give more information *) (* devrait être indifférent d'exiger leq ou pas puisque pour un inductif cela doit être égal *) - if not (e_cumul env evdref expected_typ ty) then evdref := sigma + match cumul env !evdref expected_typ ty with + | Some sigma -> evdref := sigma + | None -> evdref := orig let binding_vars_of_inductive sigma = function | NotInd _ -> [] @@ -368,15 +373,20 @@ let ltac_interp_realnames lvar = function | t, IsInd (ty,ind,realnal) -> t, IsInd (ty,ind,List.map (ltac_interp_name lvar) realnal) | _ as x -> x +let is_patvar pat = + match DAst.get pat with + | PatVar _ -> true + | _ -> false + let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) = let loc = loc_of_glob_constr tomatch in let tycon,realnames = find_tomatch_tycon evdref env loc indopt in let j = typing_fun tycon env evdref !lvar tomatch in - let evd, j = Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env !evdref j in - evdref := evd; + let j = evd_comb1 (Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env) evdref j in let typ = nf_evar !evdref j.uj_type in lvar := make_return_predicate_ltac_lvar !evdref na tomatch j.uj_val !lvar; let t = + if realnames = None && pats <> [] && List.for_all is_patvar pats then NotInd (None,typ) else try try_find_ind env !evdref typ realnames with Not_found -> unify_tomatch_with_patterns evdref env loc typ pats realnames in @@ -396,12 +406,8 @@ let coerce_to_indtype typing_fun evdref env lvar matx tomatchl = (* Utils *) let mkExistential env ?(src=(Loc.tag Evar_kinds.InternalHole)) evdref = - let e, u = e_new_type_evar env evdref univ_flexible_alg ~src:src in e - -let evd_comb2 f evdref x y = - let (evd',y) = f !evdref x y in - evdref := evd'; - y + let (e, u) = evd_comb1 (new_type_evar env ~src:src) evdref univ_flexible_alg in + e let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = (* Ideally, we could find a common inductive type to which both the @@ -424,7 +430,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = let current = if List.is_empty deps && isEvar !(pb.evdref) typ then (* Don't insert coercions if dependent; only solve evars *) - let _ = e_cumul pb.env pb.evdref indt typ in + let () = Option.iter ((:=) pb.evdref) (cumul pb.env !(pb.evdref) indt typ) in current else (evd_comb2 (Coercion.inh_conv_coerce_to true pb.env) @@ -574,7 +580,7 @@ let dependent_decl sigma a = let rec dep_in_tomatch sigma n = function | (Pushed _ | Alias _ | NonDepAlias) :: l -> dep_in_tomatch sigma n l - | Abstract (_,d) :: l -> dependent_decl sigma (mkRel n) d || dep_in_tomatch sigma (n+1) l + | Abstract (_,d) :: l -> RelDecl.exists (fun c -> not (noccurn sigma n c)) d || dep_in_tomatch sigma (n+1) l | [] -> false let dependencies_in_rhs sigma nargs current tms eqns = @@ -1014,8 +1020,8 @@ let adjust_impossible_cases pb pred tomatch submat = begin match Constr.kind pred with | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) == Evar_kinds.ImpossibleCase -> if not (Evd.is_defined !(pb.evdref) evk) then begin - let evd, default = use_unit_judge !(pb.evdref) in - pb.evdref := Evd.define evk (EConstr.Unsafe.to_constr default.uj_type) evd + let default = evd_comb0 use_unit_judge pb.evdref in + pb.evdref := Evd.define evk default.uj_type !(pb.evdref) end; add_assert_false_case pb tomatch | _ -> @@ -1425,8 +1431,9 @@ and match_current pb (initial,tomatch) = let ci = make_case_info pb.env (fst mind) pb.casestyle in let pred = nf_betaiota pb.env !(pb.evdref) pred in let case = - make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals + make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals in + let _ = Evarutil.evd_comb1 (Typing.type_of pb.env) pb.evdref pred in Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred; { uj_val = applist (case, inst); uj_type = prod_applist !(pb.evdref) typ inst } @@ -1662,7 +1669,7 @@ let rec list_assoc_in_triple x = function let abstract_tycon ?loc env evdref subst tycon extenv t = let t = nf_betaiota env !evdref t in (* it helps in some cases to remove K-redex*) let src = match EConstr.kind !evdref t with - | Evar (evk,_) -> (Loc.tag ?loc @@ Evar_kinds.SubEvar evk) + | Evar (evk,_) -> (Loc.tag ?loc @@ Evar_kinds.SubEvar (None,evk)) | _ -> (Loc.tag ?loc @@ Evar_kinds.CasesType true) in let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv !evdref subst t in (* We traverse the type T of the original problem Xi looking for subterms @@ -1681,7 +1688,7 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = (fun i _ -> try list_assoc_in_triple i subst0 with Not_found -> mkRel i) 1 (rel_context env) in - let ev' = e_new_evar env evdref ~src ty in + let ev' = evd_comb1 (Evarutil.new_evar env ~src) evdref ty in begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with | Success evd -> evdref := evd | UnifFailure _ -> assert false @@ -1698,21 +1705,24 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = let ty = get_type_of env !evdref t in Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in - let ty = lift (-k) (aux x ty) in + let dummy_subst = List.init k (fun _ -> mkProp) in + let ty = substl dummy_subst (aux x ty) in let depvl = free_rels !evdref ty in let inst = List.map_i (fun i _ -> if Int.List.mem i vl then u else mkRel i) 1 (rel_context extenv) in - let rel_filter = - List.map (fun a -> not (isRel !evdref a) || dependent !evdref a u - || Int.Set.mem (destRel !evdref a) depvl) inst in + let map a = match EConstr.kind !evdref a with + | Rel n -> not (noccurn !evdref n u) || Int.Set.mem n depvl + | _ -> true + in + let rel_filter = List.map map inst in let named_filter = List.map (fun d -> local_occur_var !evdref (NamedDecl.get_id d) u) (named_context extenv) in let filter = Filter.make (rel_filter @ named_filter) in - let candidates = u :: List.map mkRel vl in - let ev = e_new_evar extenv evdref ~src ~filter ~candidates ty in + let candidates = List.rev (u :: List.map mkRel vl) in + let ev = evd_comb1 (Evarutil.new_evar extenv ~src ~filter ~candidates) evdref ty in lift k ev in aux (0,extenv,subst0) t0 @@ -1724,17 +1734,20 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t = we are in an impossible branch *) let n = Context.Rel.length (rel_context env) in let n' = Context.Rel.length (rel_context tycon_env) in - let impossible_case_type, u = - e_new_type_evar (reset_context env) evdref univ_flexible_alg ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) in - (lift (n'-n) impossible_case_type, mkSort u) + let impossible_case_type, u = + evd_comb1 + (new_type_evar (reset_context env) ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase)) + evdref univ_flexible_alg + in + (lift (n'-n) impossible_case_type, mkSort u) | Some t -> let t = abstract_tycon ?loc tycon_env evdref subst tycon extenv t in - let evd,tt = Typing.type_of extenv !evdref t in - evdref := evd; + let tt = evd_comb1 (Typing.type_of extenv) evdref t in (t,tt) in - let b = e_cumul env evdref tt (mkSort s) (* side effect *) in - if not b then anomaly (Pp.str "Build_tycon: should be a type."); - { uj_val = t; uj_type = tt } + match cumul env !evdref tt (mkSort s) with + | None -> anomaly (Pp.str "Build_tycon: should be a type."); + | Some sigma -> evdref := sigma; + { uj_val = t; uj_type = tt } (* For a multiple pattern-matching problem Xi on t1..tn with return * type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return @@ -1923,9 +1936,7 @@ let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign = let inh_conv_coerce_to_tycon ?loc env evdref j tycon = match tycon with | Some p -> - let (evd',j) = Coercion.inh_conv_coerce_to ?loc true env !evdref j p in - evdref := evd'; - j + evd_comb2 (Coercion.inh_conv_coerce_to ?loc true env) evdref j p | None -> j (* We put the tycon inside the arity signature, possibly discovering dependencies. *) @@ -1936,8 +1947,8 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = List.fold_right2 (fun (tm, tmtype) sign (subst, len) -> let signlen = List.length sign in match EConstr.kind sigma tm with - | Rel n when dependent sigma tm c - && Int.equal signlen 1 (* The term to match is not of a dependent type itself *) -> + | Rel n when Int.equal signlen 1 && not (noccurn sigma n c) + (* The term to match is not of a dependent type itself *) -> ((n, len) :: subst, len - signlen) | Rel n when signlen > 1 (* The term is of a dependent type, maybe some variable in its type appears in the tycon. *) -> @@ -1948,13 +1959,13 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = List.fold_left (fun (subst, len) arg -> match EConstr.kind sigma arg with - | Rel n when dependent sigma arg c -> + | Rel n when not (noccurn sigma n c) -> ((n, len) :: subst, pred len) | _ -> (subst, pred len)) (subst, len) realargs in let subst = - if dependent sigma tm c && List.for_all (isRel sigma) realargs + if not (noccurn sigma n c) && List.for_all (isRel sigma) realargs then (n, len) :: subst else subst in (subst, pred len)) | _ -> (subst, len - signlen)) @@ -2099,8 +2110,11 @@ let mk_JMeq_refl evdref typ x = papp evdref coq_JMeq_refl [| typ; x |] let hole na = DAst.make @@ - GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na), - Misctypes.IntroAnonymous, None) + GHole (Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation= Evar_kinds.Define false; + Evar_kinds.qm_name=na; + Evar_kinds.qm_record_field=None}, + IntroAnonymous, None) let constr_of_pat env evdref arsign pat avoid = let rec typ env (ty, realargs) pat avoid = @@ -2581,7 +2595,8 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar let body = it_mkLambda_or_LetIn (applist (j.uj_val, args)) lets in let j = { uj_val = it_mkLambda_or_LetIn body tomatchs_lets; - uj_type = EConstr.of_constr (EConstr.to_constr !evdref tycon); } + (* XXX: is this normalization needed? *) + uj_type = Evarutil.nf_evar !evdref tycon; } in j (**************************************************************************) -- cgit v1.2.3