aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/evd.ml5
-rw-r--r--pretyping/evd.mli12
-rw-r--r--pretyping/find_subterm.ml98
-rw-r--r--pretyping/find_subterm.mli16
-rw-r--r--pretyping/locusops.ml17
-rw-r--r--pretyping/locusops.mli8
-rw-r--r--pretyping/pretype_errors.ml6
-rw-r--r--pretyping/pretype_errors.mli6
-rw-r--r--pretyping/pretyping.ml62
-rw-r--r--pretyping/pretyping.mli7
-rw-r--r--pretyping/tacred.ml2
-rw-r--r--pretyping/unification.ml105
-rw-r--r--pretyping/unification.mli15
13 files changed, 253 insertions, 106 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 93d47d6b18..9022db79f5 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1600,6 +1600,11 @@ let dependent_evar_ident ev evd =
| _ -> anomaly (str "Not an evar resulting of a dependent binding")
(*******************************************************************)
+
+type pending = (* before: *) evar_map * (* after: *) evar_map
+
+type pending_constr = pending * constr
+
type open_constr = evar_map * constr
(*******************************************************************)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index cc64b3594c..8acf811751 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -575,10 +575,16 @@ val eq_constr_univs_test : evar_map -> constr -> constr -> bool
(** Syntactic equality up to universes, throwing away the (consistent) constraints
in case of success. *)
-(********************************************************************
- constr with holes *)
+(********************************************************************)
+(* constr with holes and pending resolution of classes, conversion *)
+(* problems, candidates, etc. *)
+
+type pending = (* before: *) evar_map * (* after: *) evar_map
+
+type pending_constr = pending * constr
+
+type open_constr = evar_map * constr (* Special case when before is empty *)
-type open_constr = evar_map * constr
(** Partially constructed constrs. *)
type unsolvability_explanation = SeveralInstancesFound of int
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index d8698a1651..2ffbee4d04 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -50,8 +50,7 @@ let check_used_occurrences nbocc (nowhere_except_in,locs) =
let proceed_with_occurrences f occs x =
match occs with
| NoOccurrences -> x
- | _ ->
- (* TODO FINISH ADAPTING WITH HUGO *)
+ | occs ->
let plocs = Locusops.convert_occs occs in
assert (List.for_all (fun x -> x >= 0) (snd plocs));
let (nbocc,x) = f 1 x in
@@ -85,7 +84,7 @@ type 'a testing_function = {
match_fun : 'a -> constr -> 'a;
merge_fun : 'a -> 'a -> 'a;
mutable testing_state : 'a;
- mutable last_found : ((Id.t * hyp_location_flag) option * int * constr) option
+ mutable last_found : position_reporting option
}
(* Find subterms using a testing function, but only at a list of
@@ -93,7 +92,76 @@ type 'a testing_function = {
(b,l), b=true means no occurrence except the ones in l and b=false,
means all occurrences except the ones in l *)
-let replace_term_occ_gen_modulo occs test bywhat cl occ t =
+(*
+type 'a loc_state = {
+ hyp_location : (Id.t * hyp_location_flag) option;
+ maxocc : bool * int;
+ locs : occurrences;
+ current : int;
+ like_first : bool
+}
+
+let all_found pos =
+ let nowhere_except_in, maxocc = pos.maxocc in
+ nowhere_except_in && pos.current > maxocc
+
+let is_selected pos = Locusops.is_selected pos.current pos.locs
+
+let incr pos = pos := { !pos with current = (!pos).current + 1 }
+
+let make_current_pos cl pos = function
+ | AtOccs occs ->
+ let nowhere_except_in,locs = Locusops.convert_occs occs in
+ let maxocc = List.fold_right max locs 0 in
+ { hyp_location = cl;
+ maxocc = (nowhere_except_in,maxocc);
+ locs = occs;
+ current = pos;
+ like_first = false }
+ | LikeFirst ->
+ { hyp_location = None;
+ maxocc = (false,max_int);
+ locs = AllOccurrences;
+ current = pos;
+ like_first = true }
+
+let extract pos = (pos.hyp_location,pos.current)
+
+let like_first pos = pos.like_first
+
+let replace_term_occ_gen_modulo occs test bywhat cl pos t =
+ let nested = ref false in
+ let currentpos = ref (make_current_pos cl pos occs) in
+ let add_subst t subst =
+ try
+ test.testing_state <- test.merge_fun subst test.testing_state;
+ test.last_found <- Some (extract !currentpos,t)
+ with NotUnifiable e when not (like_first !currentpos) ->
+ let lastpos = Option.get test.last_found in
+ raise
+ (SubtermUnificationError (!nested,(extract !currentpos,t),lastpos,e)) in
+ let rec substrec k t =
+ if all_found !currentpos then (* shortcut *) t else
+ try
+ let subst = test.match_fun test.testing_state t in
+ if is_selected !currentpos then
+ (add_subst t subst; incr currentpos;
+ (* Check nested matching subterms *)
+ nested := true; ignore (subst_below k t); nested := false;
+ (* Do the effective substitution *)
+ Vars.lift k (bywhat ()))
+ else
+ (incr currentpos; subst_below k t)
+ with NotUnifiable _ ->
+ subst_below k t
+ and subst_below k t =
+ map_constr_with_binders_left_to_right (fun d k -> k+1) substrec k t
+ in
+ let t' = substrec 0 t in
+ (!currentpos, t')
+*)
+
+let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t =
let (nowhere_except_in,locs) = Locusops.convert_occs occs in
let maxocc = List.fold_right max locs 0 in
let pos = ref occ in
@@ -101,10 +169,10 @@ let replace_term_occ_gen_modulo occs test bywhat cl occ t =
let add_subst t subst =
try
test.testing_state <- test.merge_fun subst test.testing_state;
- test.last_found <- Some (cl,!pos,t)
- with NotUnifiable e ->
+ test.last_found <- Some ((cl,!pos),t)
+ with NotUnifiable e when not like_first ->
let lastpos = Option.get test.last_found in
- raise (SubtermUnificationError (!nested,(cl,!pos,t),lastpos,e)) in
+ raise (SubtermUnificationError (!nested,((cl,!pos),t),lastpos,e)) in
let rec substrec k t =
if nowhere_except_in && !pos > maxocc then t else
if not (Vars.closed0 t) then subst_below k t else
@@ -127,13 +195,17 @@ let replace_term_occ_gen_modulo occs test bywhat cl occ t =
(!pos, t')
let replace_term_occ_modulo occs test bywhat t =
+ let occs',like_first =
+ match occs with AtOccs occs -> occs,false | LikeFirst -> AllOccurrences,true in
proceed_with_occurrences
- (replace_term_occ_gen_modulo occs test bywhat None) occs t
+ (replace_term_occ_gen_modulo occs' like_first test bywhat None) occs' t
-let replace_term_occ_decl_modulo (plocs,hyploc) test bywhat d =
+let replace_term_occ_decl_modulo occs test bywhat d =
+ let (plocs,hyploc),like_first =
+ match occs with AtOccs occs -> occs,false | LikeFirst -> (AllOccurrences,InHyp),true in
proceed_with_occurrences
(map_named_declaration_with_hyploc
- (replace_term_occ_gen_modulo plocs test bywhat)
+ (replace_term_occ_gen_modulo plocs like_first test bywhat)
hyploc)
plocs d
@@ -157,11 +229,13 @@ let subst_closed_term_occ env evd occs c t =
let t' = replace_term_occ_modulo occs test bywhat t in
t', test.testing_state
-let subst_closed_term_occ_decl env evd (plocs,hyploc) c d =
+let subst_closed_term_occ_decl env evd occs c d =
let test = make_eq_univs_test env evd c in
+ let (plocs,hyploc),like_first =
+ match occs with AtOccs occs -> occs,false | LikeFirst -> (AllOccurrences,InHyp),true in
let bywhat () = mkRel 1 in
proceed_with_occurrences
(map_named_declaration_with_hyploc
- (fun _ -> replace_term_occ_gen_modulo plocs test bywhat None)
+ (fun _ -> replace_term_occ_gen_modulo plocs like_first test bywhat None)
hyploc) plocs d,
test.testing_state
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index b24c958074..ea1ce6228b 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -26,11 +26,12 @@ exception SubtermUnificationError of subterm_unification_error
function to merge substitutions and an initial substitution;
last_found is used for error messages and it has to be initialized
with None. *)
+
type 'a testing_function = {
match_fun : 'a -> constr -> 'a;
merge_fun : 'a -> 'a -> 'a;
mutable testing_state : 'a;
- mutable last_found : ((Id.t * hyp_location_flag) option * int * constr) option
+ mutable last_found : position_reporting option
}
(** This is the basic testing function, looking for exact matches of a
@@ -42,25 +43,26 @@ val make_eq_univs_test : env -> evar_map -> constr -> evar_map testing_function
matching subterms at the indicated occurrences [occl] with [mk
()]; it turns a NotUnifiable exception raised by the testing
function into a SubtermUnificationError. *)
-val replace_term_occ_modulo :
- occurrences -> 'a testing_function -> (unit -> constr) -> constr -> constr
+val replace_term_occ_modulo : occurrences or_like_first ->
+ 'a testing_function -> (unit -> constr) -> constr -> constr
(** [replace_term_occ_decl_modulo] is similar to
[replace_term_occ_modulo] but for a named_declaration. *)
val replace_term_occ_decl_modulo :
- occurrences * hyp_location_flag -> 'a testing_function -> (unit -> constr) ->
+ (occurrences * hyp_location_flag) or_like_first ->
+ 'a testing_function -> (unit -> constr) ->
named_declaration -> named_declaration
(** [subst_closed_term_occ occl c d] replaces occurrences of
closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC),
unifying universes which results in a set of constraints. *)
-val subst_closed_term_occ : env -> evar_map -> occurrences -> constr ->
- constr -> constr * evar_map
+val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first ->
+ constr -> constr -> constr * evar_map
(** [subst_closed_term_occ_decl evd occl c decl] replaces occurrences of
closed [c] at positions [occl] by [Rel 1] in [decl]. *)
val subst_closed_term_occ_decl : env -> evar_map ->
- occurrences * hyp_location_flag ->
+ (occurrences * hyp_location_flag) or_like_first ->
constr -> named_declaration -> named_declaration * evar_map
(** Miscellaneous *)
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 5484c80950..21157d9d5a 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -87,17 +87,22 @@ let out_arg = function
| Misctypes.ArgVar _ -> Errors.anomaly (Pp.str "Unevaluated or_var variable")
| Misctypes.ArgArg x -> x
-let occurrences_of_hyp id cls =
+let occurrences_of_hyp id =function
+ | LikeFirst -> LikeFirst
+ | AtOccs cls ->
let rec hyp_occ = function
[] -> NoOccurrences, InHyp
| ((occs,id'),hl)::_ when Names.Id.equal id id' ->
occurrences_map (List.map out_arg) occs, hl
| _::l -> hyp_occ l in
- match cls.onhyps with
+ AtOccs (match cls.onhyps with
None -> AllOccurrences,InHyp
- | Some l -> hyp_occ l
+ | Some l -> hyp_occ l)
-let occurrences_of_goal cls =
- occurrences_map (List.map out_arg) cls.concl_occs
+let occurrences_of_goal = function
+ | LikeFirst -> LikeFirst
+ | AtOccs cls -> AtOccs (occurrences_map (List.map out_arg) cls.concl_occs)
-let in_every_hyp cls = Option.is_empty cls.onhyps
+let in_every_hyp = function
+ | LikeFirst -> true
+ | AtOccs cls -> Option.is_empty cls.onhyps
diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli
index 73d13c0bc0..f6d27a1850 100644
--- a/pretyping/locusops.mli
+++ b/pretyping/locusops.mli
@@ -38,7 +38,7 @@ val concrete_clause_of : (unit -> Id.t list) -> clause -> concrete_clause
(** Miscellaneous functions *)
-val occurrences_of_hyp : Id.t -> Id.t clause_expr ->
- occurrences * hyp_location_flag
-val occurrences_of_goal : 'a clause_expr -> occurrences
-val in_every_hyp : 'a clause_expr -> bool
+val occurrences_of_hyp : Id.t -> clause or_like_first ->
+ (occurrences * hyp_location_flag) or_like_first
+val occurrences_of_goal : clause or_like_first -> occurrences or_like_first
+val in_every_hyp : clause or_like_first -> bool
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index e16d1206aa..99b5a51f93 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -23,9 +23,11 @@ type unification_error =
| InstanceNotSameType of existential_key * env * types * types
| UnifUnivInconsistency of Univ.univ_inconsistency
-type position =(Id.t * Locus.hyp_location_flag) option
+type position = (Id.t * Locus.hyp_location_flag) option
-type subterm_unification_error = bool * (position * int * constr) * (position * int * constr) * (constr * constr * unification_error) option
+type position_reporting = (position * int) * constr
+
+type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option
type pretype_error =
(* Old Case *)
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index b74ca19368..5882d8b9c2 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -24,9 +24,11 @@ type unification_error =
| InstanceNotSameType of existential_key * env * types * types
| UnifUnivInconsistency of Univ.univ_inconsistency
-type position =(Id.t * Locus.hyp_location_flag) option
+type position = (Id.t * Locus.hyp_location_flag) option
-type subterm_unification_error = bool * (position * int * constr) * (position * int * constr) * (constr * constr * unification_error) option
+type position_reporting = (position * int) * constr
+
+type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option
type pretype_error =
(** Old Case *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5383101b49..6dbf7915bc 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -142,19 +142,27 @@ type inference_flags = {
expand_evars : bool
}
-let apply_typeclasses env evdref fail_evar =
+let fold_pending_holes f (sigma,sigma') =
+ Evd.fold_undefined
+ (fun evk _ acc -> if Evd.mem sigma evk then acc else f evk acc)
+ sigma'
+
+let is_pending_hole (sigma,sigma') evk =
+ Evd.is_undefined sigma' evk && not (Evd.mem sigma evk)
+
+let apply_typeclasses env evdref pending fail_evar =
evdref := Typeclasses.resolve_typeclasses
~filter:(if Flags.is_program_mode ()
- then Typeclasses.no_goals_or_obligations else Typeclasses.no_goals)
+ then (fun evk evi -> is_pending_hole pending evk && Typeclasses.no_goals_or_obligations evk evi)
+ else (fun evk evi -> is_pending_hole pending evk && Typeclasses.no_goals evk evi))
~split:true ~fail:fail_evar env !evdref;
if Flags.is_program_mode () then (* Try optionally solving the obligations *)
evdref := Typeclasses.resolve_typeclasses
- ~filter:Typeclasses.all_evars ~split:true ~fail:false env !evdref
+ ~filter:(fun evk evi -> is_pending_hole pending evk && Typeclasses.all_evars evk evi) ~split:true ~fail:false env !evdref
-let apply_inference_hook hook initial_sigma evdref =
- evdref := fold_undefined (fun evk evi sigma ->
- if not (Evd.mem initial_sigma evk) &&
- is_undefined sigma evk (* i.e. not defined by side-effect *)
+let apply_inference_hook hook evdref pending =
+ evdref := fold_pending_holes (fun evk sigma ->
+ if Evd.is_undefined sigma evk (* in particular not defined by side-effect *)
then
try
let c = hook sigma evk in
@@ -162,7 +170,7 @@ let apply_inference_hook hook initial_sigma evdref =
with Exit ->
sigma
else
- sigma) !evdref !evdref
+ sigma) pending !evdref
let apply_heuristics env evdref fail_evar =
(* Resolve eagerly, potentially making wrong choices *)
@@ -171,39 +179,39 @@ let apply_heuristics env evdref fail_evar =
with e when Errors.noncritical e ->
let e = Errors.push e in if fail_evar then raise e
-let check_typeclasses_instances_are_solved env sigma =
+let check_typeclasses_instances_are_solved env current_sigma pending =
(* Naive way, call resolution again with failure flag *)
- apply_typeclasses env (ref sigma) true
+ apply_typeclasses env (ref current_sigma) pending true
-let check_extra_evars_are_solved env initial_sigma sigma =
- Evd.fold_undefined
- (fun evk evi () ->
- if not (Evd.mem initial_sigma evk) then
- let (loc,k) = evar_source evk sigma in
+let check_extra_evars_are_solved env current_sigma pending =
+ fold_pending_holes
+ (fun evk () ->
+ if not (Evd.is_defined current_sigma evk) then
+ let (loc,k) = evar_source evk current_sigma in
match k with
| Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
| _ ->
- let evi = nf_evar_info sigma (Evd.find_undefined sigma evk) in
- error_unsolvable_implicit loc env sigma evi k None) sigma ()
+ let evi = nf_evar_info current_sigma (Evd.find_undefined current_sigma evk) in
+ error_unsolvable_implicit loc env current_sigma evi k None) pending ()
-let check_evars_are_solved env initial_sigma sigma =
- check_typeclasses_instances_are_solved env sigma;
- check_problems_are_solved env sigma;
- check_extra_evars_are_solved env initial_sigma sigma
+let check_evars_are_solved env current_sigma pending =
+ check_typeclasses_instances_are_solved env current_sigma pending;
+ check_problems_are_solved env current_sigma;
+ check_extra_evars_are_solved env current_sigma pending
(* Try typeclasses, hooks, unification heuristics ... *)
-let solve_remaining_evars flags env initial_sigma sigma =
- let evdref = ref sigma in
- if flags.use_typeclasses then apply_typeclasses env evdref false;
+let solve_remaining_evars flags env current_sigma pending =
+ let evdref = ref current_sigma in
+ if flags.use_typeclasses then apply_typeclasses env evdref pending false;
if Option.has_some flags.use_hook then
- apply_inference_hook (Option.get flags.use_hook env) initial_sigma evdref;
+ apply_inference_hook (Option.get flags.use_hook env) evdref pending;
if flags.use_unif_heuristics then apply_heuristics env evdref false;
- if flags.fail_evar then check_evars_are_solved env initial_sigma !evdref;
+ if flags.fail_evar then check_evars_are_solved env !evdref pending;
!evdref
let process_inference_flags flags env initial_sigma (sigma,c) =
- let sigma = solve_remaining_evars flags env initial_sigma sigma in
+ let sigma = solve_remaining_evars flags env sigma (initial_sigma,sigma) in
let c = if flags.expand_evars then nf_evar sigma c else c in
sigma,c
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 5df4c8372f..eb56264749 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -108,14 +108,17 @@ val understand_judgment_tcc : env -> evar_map ref ->
(** Trying to solve remaining evars and remaining conversion problems
with type classes, heuristics, and possibly an external solver *)
+(* For simplicity, it is assumed that current map has no other evars
+ with candidate and no other conversion problems that the one in
+ [pending], however, it can contain more evars than the pending ones. *)
val solve_remaining_evars : inference_flags ->
- env -> (* initial map *) evar_map -> (* map to solve *) evar_map -> evar_map
+ env -> (* initial map *) evar_map -> (* map to solve *) pending -> evar_map
(** Checking evars are all solved and reporting an appropriate error message *)
val check_evars_are_solved :
- env -> (* initial map: *) evar_map -> (* map to check: *) evar_map -> unit
+ env -> (* current map: *) evar_map -> (* map to check: *) pending -> unit
(**/**)
(** Internal of Pretyping... *)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index b2938cb99f..d86da79d6b 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1131,7 +1131,7 @@ let abstract_scheme env (locc,a) (c, sigma) =
if occur_meta a then
mkLambda (na,ta,c), sigma
else
- let c', sigma' = subst_closed_term_occ env sigma locc a c in
+ let c', sigma' = subst_closed_term_occ env sigma (AtOccs locc) a c in
mkLambda (na,ta,c'), sigma'
let pattern_occs loccs_trm env sigma c =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 527199e3b6..2f1c230b78 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -90,7 +90,7 @@ let abstract_scheme env evd c l lname_typ =
let abstract_list_all env evd typ c l =
let ctxt,_ = splay_prod_n env evd (List.length l) typ in
- let l_with_all_occs = List.map (function a -> (AllOccurrences,a)) l in
+ let l_with_all_occs = List.map (function a -> (LikeFirst,a)) l in
let p,evd = abstract_scheme env evd c l_with_all_occs ctxt in
let evd,typp =
try Typing.e_type_of env evd p
@@ -1362,9 +1362,10 @@ let indirectly_dependent c d decls =
let indirect_dependency d decls =
pi1 (List.hd (List.filter (fun (id,_,_) -> dependent_in_decl (mkVar id) d) decls))
-let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env initial_sigma (sigma,c) =
- let sigma = Pretyping.solve_remaining_evars flags env initial_sigma sigma
- in Evd.evar_universe_context sigma, nf_evar sigma c
+let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
+ let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in
+ let sigma, subst = nf_univ_variables sigma in
+ sigma, subst_univs_constr subst (nf_evar sigma c)
let default_matching_core_flags sigma =
let ts = Names.full_transparent_state in {
@@ -1394,7 +1395,7 @@ let default_matching_merge_flags sigma =
use_pattern_unification = true;
}
-let default_matching_flags sigma =
+let default_matching_flags (sigma,_) =
let flags = default_matching_core_flags sigma in {
core_unify_flags = flags;
merge_unify_flags = default_matching_merge_flags sigma;
@@ -1404,12 +1405,35 @@ let default_matching_flags sigma =
}
(* This supports search of occurrences of term from a pattern *)
+(* from_prefix is useful e.g. for subterms in an inductive type: we can say *)
+(* "destruct t" and it finds "t u" *)
-let make_pattern_test inf_flags env sigma0 (sigma,c) =
- let flags = default_matching_flags sigma0 in
+exception PatternNotFound
+
+let make_pattern_test from_prefix_of_ind env sigma (pending,c) =
+ let flags = default_matching_flags pending in
+ let n = List.length (snd (decompose_app c)) in
let matching_fun _ t =
- try let sigma = w_typed_unify env sigma Reduction.CONV flags c t in
- Some(sigma, t)
+ try
+ let t' =
+ if from_prefix_of_ind then
+ (* We check for fully applied subterms of the form "u u1 .. un" *)
+ (* of inductive type knowning only a prefix "u u1 .. ui" *)
+ let t,l = decompose_app t in
+ let l1,l2 =
+ try List.chop n l with Failure _ -> raise (NotUnifiable None) in
+ if not (List.for_all closed0 l2) then raise (NotUnifiable None)
+ else
+ applist (t,l1)
+ else t in
+ let sigma = w_typed_unify env sigma Reduction.CONV flags c t' in
+ let _ =
+ if from_prefix_of_ind then
+ (* We check that the subterm we found from prefix is applied *)
+ (* enough to be of inductive type *)
+ try ignore (Inductiveops.find_mrectype env sigma (Retyping.get_type_of env sigma t))
+ with UserError _ -> raise (NotUnifiable None) in
+ Some(sigma, t)
with
| PretypeError (_,_,CannotUnify (c1,c2,Some e)) ->
raise (NotUnifiable (Some (c1,c2,e)))
@@ -1425,22 +1449,25 @@ let make_pattern_test inf_flags env sigma0 (sigma,c) =
{ match_fun = matching_fun; merge_fun = merge_fun;
testing_state = None; last_found = None },
(fun test -> match test.testing_state with
- | None ->
- finish_evar_resolution ~flags:inf_flags env sigma0 (sigma,c)
+ | None -> None
+(*
+ let sigma, c = finish_evar_resolution ~flags:inf_flags env sigma (pending,c) in
+ sigma,c
+*)
| Some (sigma,_) ->
+ let c = nf_evar sigma (local_strong whd_meta sigma c) in
let univs, subst = nf_univ_variables sigma in
- Evd.evar_universe_context univs,
- subst_univs_constr subst (nf_evar sigma c))
+ Some (sigma,subst_univs_constr subst c))
let make_eq_test env evd c =
let out cstr =
- Evd.evar_universe_context cstr.testing_state, c
+ match cstr.last_found with None -> None | _ -> Some (cstr.testing_state, c)
in
- (make_eq_univs_test env evd c, out)
+ (make_eq_univs_test env evd c, out)
-let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env concl =
+let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
let id =
- let t = match ty with Some t -> t | None -> get_type_of env sigmac c in
+ let t = match ty with Some t -> t | None -> get_type_of env sigma c in
let x = id_of_name_using_hdchar (Global.env()) t name in
let ids = ids_of_named_context (named_context env) in
if name == Anonymous then next_ident_away_in_goal x ids else
@@ -1450,9 +1477,9 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc
x
in
let mkvarid () = mkVar id in
- let compute_dependency _ (hyp,_,_ as d) depdecls =
+ let compute_dependency _ (hyp,_,_ as d) (sign,depdecls) =
match occurrences_of_hyp hyp occs with
- | NoOccurrences, InHyp ->
+ | AtOccs (NoOccurrences, InHyp) ->
if indirectly_dependent c d depdecls then
(* Told explicitly not to abstract over [d], but it is dependent *)
let id' = indirect_dependency d depdecls in
@@ -1460,31 +1487,34 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc
++ str " without also abstracting or erasing " ++ Nameops.pr_id hyp
++ str ".")
else
- depdecls
- | (AllOccurrences, InHyp) as occ ->
+ (push_named_context_val d sign,depdecls)
+ | (AtOccs (AllOccurrences, InHyp) | LikeFirst) as occ ->
let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in
if Context.eq_named_declaration d newdecl
&& not (indirectly_dependent c d depdecls)
then
if check_occs && not (in_every_hyp occs)
- then raise (PretypeError (env,sigmac,NoOccurrenceFound (c,Some hyp)))
- else depdecls
+ then raise (PretypeError (env,sigma,NoOccurrenceFound (c,Some hyp)))
+ else (push_named_context_val d sign, depdecls)
else
- newdecl :: depdecls
+ (push_named_context_val newdecl sign, newdecl :: depdecls)
| occ ->
- replace_term_occ_decl_modulo occ test mkvarid d :: depdecls in
+ let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in
+ (push_named_context_val newdecl sign, newdecl :: depdecls) in
try
- let depdecls = fold_named_context compute_dependency env ~init:[] in
+ let sign,depdecls =
+ fold_named_context compute_dependency env
+ ~init:(empty_named_context_val,[]) in
let ccl = match occurrences_of_goal occs with
- | NoOccurrences -> concl
+ | AtOccs NoOccurrences -> concl
| occ -> replace_term_occ_modulo occ test mkvarid concl
in
let lastlhyp =
if List.is_empty depdecls then None else Some (pi1(List.last depdecls)) in
- (id,depdecls,lastlhyp,ccl,out test)
+ (id,sign,depdecls,lastlhyp,ccl,out test)
with
SubtermUnificationError e ->
- raise (PretypeError (env,sigmac,CannotUnifyOccurrences e))
+ raise (PretypeError (env,sigma,CannotUnifyOccurrences e))
(** [make_abstraction] is the main entry point to abstract over a term
or pattern at some occurrences; it returns:
@@ -1497,22 +1527,27 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc
- the term or pattern to abstract fully instantiated
*)
+type prefix_of_inductive_support_flag = bool
+
type abstraction_request =
-| AbstractPattern of Name.t * (evar_map * constr) * clause * bool * Pretyping.inference_flags
+| AbstractPattern of prefix_of_inductive_support_flag * Name.t * pending_constr * clause or_like_first * bool
| AbstractExact of Name.t * constr * types option * clause * bool
type abstraction_result =
- Names.Id.t * Context.named_declaration list * Names.Id.t option *
- constr * (Evd.evar_universe_context * constr)
+ Names.Id.t * named_context_val *
+ Context.named_declaration list * Names.Id.t option *
+ types * (Evd.evar_map * constr) option
let make_abstraction env evd ccl abs =
match abs with
- | AbstractPattern (name,c,occs,check_occs,flags) ->
+ | AbstractPattern (from_prefix,name,c,occs,check_occs) ->
make_abstraction_core name
- (make_pattern_test flags env evd c) c None occs check_occs env ccl
+ (make_pattern_test from_prefix env evd c)
+ env evd (snd c) None occs check_occs ccl
| AbstractExact (name,c,ty,occs,check_occs) ->
make_abstraction_core name
- (make_eq_test env evd c) (evd,c) ty occs check_occs env ccl
+ (make_eq_test env evd c)
+ env evd c ty (AtOccs occs) check_occs ccl
let keyed_unify env evd kop =
if not !keyed_unification then fun cl -> true
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index bedd6bf161..3b49981290 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -45,7 +45,7 @@ val elim_no_delta_flags : unit -> unify_flags
val w_unify :
env -> evar_map -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map
-(** [w_unify_to_subterm env (c,t) m] performs unification of [c] with a
+(** [w_unify_to_subterm env m (c,t)] performs unification of [c] with a
subterm of [t]. Constraints are added to [m] and the matched
subterm of [t] is also returned. *)
val w_unify_to_subterm :
@@ -63,20 +63,25 @@ val w_coerce_to_type : env -> evar_map -> constr -> types -> types ->
(* Looking for subterms in contexts at some occurrences, possibly with pattern*)
+exception PatternNotFound
+
type abstraction_request =
-| AbstractPattern of Names.Name.t * (evar_map * constr) * Locus.clause * bool * Pretyping.inference_flags
+| AbstractPattern of bool * Names.Name.t * pending_constr * Locus.clause Locus.or_like_first * bool
| AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool
val finish_evar_resolution : ?flags:Pretyping.inference_flags ->
- env -> Evd.evar_map -> open_constr -> Evd.evar_universe_context * constr
+ env -> Evd.evar_map -> pending_constr -> Evd.evar_map * constr
type abstraction_result =
- Names.Id.t * Context.named_declaration list * Names.Id.t option *
- constr * (Evd.evar_universe_context * constr)
+ Names.Id.t * named_context_val *
+ Context.named_declaration list * Names.Id.t option *
+ types * (Evd.evar_map * constr) option
val make_abstraction : env -> Evd.evar_map -> constr ->
abstraction_request -> abstraction_result
+val pose_all_metas_as_evars : env -> evar_map -> constr -> evar_map * constr
+
(*i This should be in another module i*)
(** [abstract_list_all env evd t c l]
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-12 22:28:13 +0000