summaryrefslogtreecommitdiff
path: root/pretyping/cases.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/cases.ml')
-rw-r--r--pretyping/cases.ml101
1 files changed, 58 insertions, 43 deletions
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
(**************************************************************************)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 23:02:31 +0000