aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml416
-rw-r--r--pretyping/cases.mli6
-rw-r--r--pretyping/coercion.ml46
-rw-r--r--pretyping/coercion.mli10
-rw-r--r--pretyping/globEnv.ml16
-rw-r--r--pretyping/globEnv.mli9
-rw-r--r--pretyping/pretyping.ml178
-rw-r--r--pretyping/pretyping.mli5
-rw-r--r--pretyping/unification.ml2
9 files changed, 358 insertions, 330 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 62c27297f3..ed7c3d6770 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -378,11 +378,11 @@ let is_patvar pat =
| PatVar _ -> true
| _ -> false
-let coerce_row typing_fun env sigma pats (tomatch,(na,indopt)) =
+let coerce_row ~program_mode typing_fun env sigma pats (tomatch,(na,indopt)) =
let loc = loc_of_glob_constr tomatch in
let sigma, tycon, realnames = find_tomatch_tycon !!env sigma loc indopt in
let sigma, j = typing_fun tycon env sigma tomatch in
- let sigma, j = Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) !!env sigma j in
+ let sigma, j = Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) ~program_mode !!env sigma j in
let typ = nf_evar sigma j.uj_type in
let env = make_return_predicate_ltac_lvar env sigma na tomatch j.uj_val in
let sigma, t =
@@ -395,12 +395,12 @@ let coerce_row typing_fun env sigma pats (tomatch,(na,indopt)) =
in
((env, sigma), (j.uj_val,t))
-let coerce_to_indtype typing_fun env sigma matx tomatchl =
+let coerce_to_indtype ~program_mode typing_fun env sigma matx tomatchl =
let pats = List.map (fun r -> r.patterns) matx in
let matx' = match matrix_transpose pats with
| [] -> List.map (fun _ -> []) tomatchl (* no patterns at all *)
| m -> m in
- let (env, sigma), tms = List.fold_left2_map (fun (env, sigma) -> coerce_row typing_fun env sigma) (env, sigma) matx' tomatchl in
+ let (env, sigma), tms = List.fold_left2_map (fun (env, sigma) -> coerce_row ~program_mode typing_fun env sigma) (env, sigma) matx' tomatchl in
env, sigma, tms
(************************************************************************)
@@ -410,7 +410,7 @@ let mkExistential ?(src=(Loc.tag Evar_kinds.InternalHole)) env sigma =
let sigma, (e, u) = Evarutil.new_type_evar env sigma ~src:src univ_flexible_alg in
sigma, e
-let adjust_tomatch_to_pattern sigma pb ((current,typ),deps,dep) =
+let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) =
(* Ideally, we could find a common inductive type to which both the
term to match and the patterns coerce *)
(* In practice, we coerce the term to match if it is not already an
@@ -435,7 +435,7 @@ let adjust_tomatch_to_pattern sigma pb ((current,typ),deps,dep) =
| None -> sigma, current
| Some sigma -> sigma, current
else
- let sigma, j = Coercion.inh_conv_coerce_to true !!(pb.env) sigma (make_judge current typ) indt in
+ let sigma, j = Coercion.inh_conv_coerce_to ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in
sigma, j.uj_val
in
sigma, (current, try_find_ind !!(pb.env) sigma indt names))
@@ -468,10 +468,11 @@ let remove_current_pattern eqn =
alias_stack = alias_of_pat pat :: eqn.alias_stack }
| [] -> anomaly (Pp.str "Empty list of patterns.")
-let push_current_pattern sigma (cur,ty) eqn =
+let push_current_pattern ~program_mode sigma (cur,ty) eqn =
+ let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
match eqn.patterns with
| pat::pats ->
- let _,rhs_env = push_rel sigma (LocalDef (alias_of_pat pat,cur,ty)) eqn.rhs.rhs_env in
+ let _,rhs_env = push_rel ~hypnaming sigma (LocalDef (alias_of_pat pat,cur,ty)) eqn.rhs.rhs_env in
{ eqn with
rhs = { eqn.rhs with rhs_env = rhs_env };
patterns = pats }
@@ -562,16 +563,17 @@ let occur_in_rhs na rhs =
| Name id -> Id.Set.mem id rhs.rhs_vars
let is_dep_patt_in eqn pat = match DAst.get pat with
- | PatVar name -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs
+ | PatVar name -> occur_in_rhs name eqn.rhs
| PatCstr _ -> true
-let mk_dep_patt_row (pats,_,eqn) =
- List.map (is_dep_patt_in eqn) pats
+let mk_dep_patt_row ~program_mode (pats,_,eqn) =
+ if program_mode then List.map (fun _ -> true) pats
+ else List.map (is_dep_patt_in eqn) pats
-let dependencies_in_pure_rhs nargs eqns =
+let dependencies_in_pure_rhs ~program_mode nargs eqns =
if List.is_empty eqns then
- List.make nargs (not (Flags.is_program_mode ())) (* Only "_" patts *) else
- let deps_rows = List.map mk_dep_patt_row eqns in
+ List.make nargs (not program_mode) (* Only "_" patts *) else
+ let deps_rows = List.map (mk_dep_patt_row ~program_mode) eqns in
let deps_columns = matrix_transpose deps_rows in
List.map (List.exists (fun x -> x)) deps_columns
@@ -585,10 +587,10 @@ let rec dep_in_tomatch sigma n = function
| 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 =
+let dependencies_in_rhs ~program_mode sigma nargs current tms eqns =
match EConstr.kind sigma current with
| Rel n when dep_in_tomatch sigma n tms -> List.make nargs true
- | _ -> dependencies_in_pure_rhs nargs eqns
+ | _ -> dependencies_in_pure_rhs ~program_mode nargs eqns
(* Computing the matrix of dependencies *)
@@ -788,9 +790,9 @@ let recover_and_adjust_alias_names (_,avoid) names sign =
in
List.split (aux (names,sign))
-let push_rels_eqn sigma sign eqn =
+let push_rels_eqn ~hypnaming sigma sign eqn =
{eqn with
- rhs = {eqn.rhs with rhs_env = snd (push_rel_context sigma sign eqn.rhs.rhs_env) } }
+ rhs = {eqn.rhs with rhs_env = snd (push_rel_context ~hypnaming sigma sign eqn.rhs.rhs_env) } }
let push_rels_eqn_with_names sigma sign eqn =
let subpats = List.rev (List.firstn (List.length sign) eqn.patterns) in
@@ -798,12 +800,12 @@ let push_rels_eqn_with_names sigma sign eqn =
let sign = recover_initial_subpattern_names subpatnames sign in
push_rels_eqn sigma sign eqn
-let push_generalized_decl_eqn env sigma n decl eqn =
+let push_generalized_decl_eqn ~hypnaming env sigma n decl eqn =
match RelDecl.get_name decl with
| Anonymous ->
- push_rels_eqn sigma [decl] eqn
+ push_rels_eqn ~hypnaming sigma [decl] eqn
| Name _ ->
- push_rels_eqn sigma [RelDecl.set_name (RelDecl.get_name (Environ.lookup_rel n !!(eqn.rhs.rhs_env))) decl] eqn
+ push_rels_eqn ~hypnaming sigma [RelDecl.set_name (RelDecl.get_name (Environ.lookup_rel n !!(eqn.rhs.rhs_env))) decl] eqn
let drop_alias_eqn eqn =
{ eqn with alias_stack = List.tl eqn.alias_stack }
@@ -1266,7 +1268,7 @@ let build_leaf sigma pb =
(* Build the sub-pattern-matching problem for a given branch "C x1..xn as x" *)
(* spiwack: the [initial] argument keeps track whether the branch is a
toplevel branch ([true]) or a deep one ([false]). *)
-let build_branch initial current realargs deps (realnames,curname) sigma pb arsign eqns const_info =
+let build_branch ~program_mode initial current realargs deps (realnames,curname) sigma pb arsign eqns const_info =
(* We remember that we descend through constructor C *)
let history =
push_history_pattern const_info.cs_nargs (fst const_info.cs_cstr) pb.history in
@@ -1296,7 +1298,8 @@ let build_branch initial current realargs deps (realnames,curname) sigma pb arsi
let typs' =
List.map_i (fun i d -> (mkRel i, map_constr (lift i) d)) 1 typs in
- let typs,extenv = push_rel_context sigma typs pb.env in
+ let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+ let typs,extenv = push_rel_context ~hypnaming sigma typs pb.env in
let typs' =
List.map (fun (c,d) ->
@@ -1306,7 +1309,7 @@ let build_branch initial current realargs deps (realnames,curname) sigma pb arsi
(* generalization *)
let dep_sign =
find_dependencies_signature sigma
- (dependencies_in_rhs sigma const_info.cs_nargs current pb.tomatch eqns)
+ (dependencies_in_rhs ~program_mode sigma const_info.cs_nargs current pb.tomatch eqns)
(List.rev typs') in
(* The dependent term to subst in the types of the remaining UnPushed
@@ -1375,7 +1378,7 @@ let build_branch initial current realargs deps (realnames,curname) sigma pb arsi
tomatch = tomatch;
pred = pred;
history = history;
- mat = List.map (push_rels_eqn_with_names sigma typs) submat }
+ mat = List.map (push_rels_eqn_with_names ~hypnaming sigma typs) submat }
(**********************************************************************
INVARIANT:
@@ -1390,181 +1393,187 @@ let build_branch initial current realargs deps (realnames,curname) sigma pb arsi
(**********************************************************************)
(* Main compiling descent *)
-let rec compile sigma pb =
- match pb.tomatch with
- | Pushed cur :: rest -> match_current sigma { pb with tomatch = rest } cur
- | Alias (initial,x) :: rest -> compile_alias initial sigma pb x rest
- | NonDepAlias :: rest -> compile_non_dep_alias sigma pb rest
- | Abstract (i,d) :: rest -> compile_generalization sigma pb i d rest
- | [] -> build_leaf sigma pb
+let compile ~program_mode sigma pb =
+ let rec compile sigma pb =
+ match pb.tomatch with
+ | Pushed cur :: rest -> match_current sigma { pb with tomatch = rest } cur
+ | Alias (initial,x) :: rest -> compile_alias initial sigma pb x rest
+ | NonDepAlias :: rest -> compile_non_dep_alias sigma pb rest
+ | Abstract (i,d) :: rest -> compile_generalization sigma pb i d rest
+ | [] -> build_leaf sigma pb
(* Case splitting *)
-and match_current sigma pb (initial,tomatch) =
- let sigma, tm = adjust_tomatch_to_pattern sigma pb tomatch in
- let pb,tomatch = adjust_predicate_from_tomatch tomatch tm pb in
- let ((current,typ),deps,dep) = tomatch in
- match typ with
- | NotInd (_,typ) ->
- check_all_variables !!(pb.env) sigma typ pb.mat;
- compile_all_variables initial tomatch sigma pb
- | IsInd (_,(IndType(indf,realargs) as indt),names) ->
+ and match_current sigma pb (initial,tomatch) =
+ let sigma, tm = adjust_tomatch_to_pattern ~program_mode sigma pb tomatch in
+ let pb,tomatch = adjust_predicate_from_tomatch tomatch tm pb in
+ let ((current,typ),deps,dep) = tomatch in
+ match typ with
+ | NotInd (_,typ) ->
+ check_all_variables !!(pb.env) sigma typ pb.mat;
+ compile_all_variables initial tomatch sigma pb
+ | IsInd (_,(IndType(indf,realargs) as indt),names) ->
let mind,_ = dest_ind_family indf in
- let mind = Tacred.check_privacy !!(pb.env) mind in
- let cstrs = get_constructors !!(pb.env) indf in
- let arsign, _ = get_arity !!(pb.env) indf in
+ let mind = Tacred.check_privacy !!(pb.env) mind in
+ let cstrs = get_constructors !!(pb.env) indf in
+ let arsign, _ = get_arity !!(pb.env) indf in
let eqns,onlydflt = group_equations pb (fst mind) current cstrs pb.mat in
- let no_cstr = Int.equal (Array.length cstrs) 0 in
+ let no_cstr = Int.equal (Array.length cstrs) 0 in
if (not no_cstr || not (List.is_empty pb.mat)) && onlydflt then
- compile_all_variables initial tomatch sigma pb
+ compile_all_variables initial tomatch sigma pb
else
(* We generalize over terms depending on current term to match *)
- let pb,deps = generalize_problem (names,dep) sigma pb deps in
+ let pb,deps = generalize_problem (names,dep) sigma pb deps in
(* We compile branches *)
- let fold_br sigma eqn cstr =
- compile_branch initial current realargs (names,dep) deps sigma pb arsign eqn cstr
- in
- let sigma, brvals = Array.fold_left2_map fold_br sigma eqns cstrs in
+ let fold_br sigma eqn cstr =
+ compile_branch initial current realargs (names,dep) deps sigma pb arsign eqn cstr
+ in
+ let sigma, brvals = Array.fold_left2_map fold_br sigma eqns cstrs in
(* We build the (elementary) case analysis *)
- let depstocheck = current::binding_vars_of_inductive sigma typ in
- let brvals,tomatch,pred,inst =
- postprocess_dependencies sigma depstocheck
- brvals pb.tomatch pb.pred deps cstrs in
- let brvals = Array.map (fun (sign,body) ->
- it_mkLambda_or_LetIn body sign) brvals in
+ let depstocheck = current::binding_vars_of_inductive sigma typ in
+ let brvals,tomatch,pred,inst =
+ postprocess_dependencies sigma depstocheck
+ brvals pb.tomatch pb.pred deps cstrs in
+ let brvals = Array.map (fun (sign,body) ->
+ it_mkLambda_or_LetIn body sign) brvals in
let (pred,typ) =
- find_predicate pb.caseloc pb.env sigma
+ find_predicate pb.caseloc pb.env sigma
pred current indt (names,dep) tomatch in
- let ci = make_case_info !!(pb.env) (fst mind) pb.casestyle in
- let pred = nf_betaiota !!(pb.env) sigma pred in
+ let ci = make_case_info !!(pb.env) (fst mind) pb.casestyle in
+ let pred = nf_betaiota !!(pb.env) sigma pred in
let case =
- make_case_or_project !!(pb.env) sigma indf ci pred current brvals
+ make_case_or_project !!(pb.env) sigma indf ci pred current brvals
in
- let sigma, _ = Typing.type_of !!(pb.env) sigma pred in
- Typing.check_allowed_sort !!(pb.env) sigma mind current pred;
- sigma, { uj_val = applist (case, inst);
- uj_type = prod_applist sigma typ inst }
-
-
-(* Building the sub-problem when all patterns are variables. Case
- where [current] is an intially pushed term. *)
-and shift_problem ((current,t),_,na) sigma pb =
- let ty = type_of_tomatch t in
- let tomatch = lift_tomatch_stack 1 pb.tomatch in
- let pred = specialize_predicate_var (current,t,na) !!(pb.env) pb.tomatch pb.pred in
- let env = Name.fold_left (fun env id -> hide_variable env Anonymous id) pb.env na in
- let pb =
- { pb with
- env = snd (push_rel sigma (LocalDef (na,current,ty)) env);
- tomatch = tomatch;
- pred = lift_predicate 1 pred tomatch;
- history = pop_history pb.history;
- mat = List.map (push_current_pattern sigma (current,ty)) pb.mat } in
- let sigma, j = compile sigma pb in
- sigma, { uj_val = subst1 current j.uj_val;
- uj_type = subst1 current j.uj_type }
-
-(* Building the sub-problem when all patterns are variables,
- non-initial case. Variables which appear as subterms of constructor
- are already introduced in the context, we avoid creating aliases to
- themselves by treating this case specially. *)
-and pop_problem ((current,t),_,na) sigma pb =
- let pred = specialize_predicate_var (current,t,na) !!(pb.env) pb.tomatch pb.pred in
- let pb =
- { pb with
- pred = pred;
- history = pop_history pb.history;
- mat = List.map push_noalias_current_pattern pb.mat } in
- compile sigma pb
+ let sigma, _ = Typing.type_of !!(pb.env) sigma pred in
+ Typing.check_allowed_sort !!(pb.env) sigma mind current pred;
+ sigma, { uj_val = applist (case, inst);
+ uj_type = prod_applist sigma typ inst }
+
+
+ (* Building the sub-problem when all patterns are variables. Case
+ where [current] is an intially pushed term. *)
+ and shift_problem ((current,t),_,na) sigma pb =
+ let ty = type_of_tomatch t in
+ let tomatch = lift_tomatch_stack 1 pb.tomatch in
+ let pred = specialize_predicate_var (current,t,na) !!(pb.env) pb.tomatch pb.pred in
+ let env = Name.fold_left (fun env id -> hide_variable env Anonymous id) pb.env na in
+ let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+ let pb =
+ { pb with
+ env = snd (push_rel ~hypnaming sigma (LocalDef (na,current,ty)) env);
+ tomatch = tomatch;
+ pred = lift_predicate 1 pred tomatch;
+ history = pop_history pb.history;
+ mat = List.map (push_current_pattern ~program_mode sigma (current,ty)) pb.mat } in
+ let sigma, j = compile sigma pb in
+ sigma, { uj_val = subst1 current j.uj_val;
+ uj_type = subst1 current j.uj_type }
+
+ (* Building the sub-problem when all patterns are variables,
+ non-initial case. Variables which appear as subterms of constructor
+ are already introduced in the context, we avoid creating aliases to
+ themselves by treating this case specially. *)
+ and pop_problem ((current,t),_,na) sigma pb =
+ let pred = specialize_predicate_var (current,t,na) !!(pb.env) pb.tomatch pb.pred in
+ let pb =
+ { pb with
+ pred = pred;
+ history = pop_history pb.history;
+ mat = List.map push_noalias_current_pattern pb.mat } in
+ compile sigma pb
-(* Building the sub-problem when all patterns are variables. *)
-and compile_all_variables initial cur sigma pb =
- if initial then shift_problem cur sigma pb
- else pop_problem cur sigma pb
+ (* Building the sub-problem when all patterns are variables. *)
+ and compile_all_variables initial cur sigma pb =
+ if initial then shift_problem cur sigma pb
+ else pop_problem cur sigma pb
-(* Building the sub-problem when all patterns are variables *)
-and compile_branch initial current realargs names deps sigma pb arsign eqns cstr =
- let sigma, sign, pb = build_branch initial current realargs deps names sigma pb arsign eqns cstr in
- let sigma, j = compile sigma pb in
- sigma, (sign, j.uj_val)
+ (* Building the sub-problem when all patterns are variables *)
+ and compile_branch initial current realargs names deps sigma pb arsign eqns cstr =
+ let sigma, sign, pb = build_branch ~program_mode initial current realargs deps names sigma pb arsign eqns cstr in
+ let sigma, j = compile sigma pb in
+ sigma, (sign, j.uj_val)
-(* Abstract over a declaration before continuing splitting *)
-and compile_generalization sigma pb i d rest =
- let pb =
- { pb with
- env = snd (push_rel sigma d pb.env);
- tomatch = rest;
- mat = List.map (push_generalized_decl_eqn pb.env sigma i d) pb.mat } in
- let sigma, j = compile sigma pb in
- sigma, { uj_val = mkLambda_or_LetIn d j.uj_val;
- uj_type = mkProd_wo_LetIn d j.uj_type }
-
-(* spiwack: the [initial] argument keeps track whether the alias has
- been introduced by a toplevel branch ([true]) or a deep one
- ([false]). *)
-and compile_alias initial sigma pb (na,orig,(expanded,expanded_typ)) rest =
- let f c t =
- let alias = LocalDef (na,c,t) in
+ (* Abstract over a declaration before continuing splitting *)
+ and compile_generalization sigma pb i d rest =
+ let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
let pb =
{ pb with
- env = snd (push_rel sigma alias pb.env);
- tomatch = lift_tomatch_stack 1 rest;
- pred = lift_predicate 1 pb.pred pb.tomatch;
- history = pop_history_pattern pb.history;
- mat = List.map (push_alias_eqn sigma alias) pb.mat } in
+ env = snd (push_rel ~hypnaming sigma d pb.env);
+ tomatch = rest;
+ mat = List.map (push_generalized_decl_eqn ~hypnaming pb.env sigma i d) pb.mat } in
let sigma, j = compile sigma pb in
- sigma, { uj_val =
- if isRel sigma c || isVar sigma c || count_occurrences sigma (mkRel 1) j.uj_val <= 1 then
- subst1 c j.uj_val
- else
- mkLetIn (na,c,t,j.uj_val);
- uj_type = subst1 c j.uj_type } in
- (* spiwack: when an alias appears on a deep branch, its non-expanded
- form is automatically a variable of the same name. We avoid
- introducing such superfluous aliases so that refines are elegant. *)
- let just_pop sigma =
+ sigma, { uj_val = mkLambda_or_LetIn d j.uj_val;
+ uj_type = mkProd_wo_LetIn d j.uj_type }
+
+ (* spiwack: the [initial] argument keeps track whether the alias has
+ been introduced by a toplevel branch ([true]) or a deep one
+ ([false]). *)
+ and compile_alias initial sigma pb (na,orig,(expanded,expanded_typ)) rest =
+ let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+ let f c t =
+ let alias = LocalDef (na,c,t) in
+ let pb =
+ { pb with
+ env = snd (push_rel ~hypnaming sigma alias pb.env);
+ tomatch = lift_tomatch_stack 1 rest;
+ pred = lift_predicate 1 pb.pred pb.tomatch;
+ history = pop_history_pattern pb.history;
+ mat = List.map (push_alias_eqn ~hypnaming sigma alias) pb.mat } in
+ let sigma, j = compile sigma pb in
+ sigma, { uj_val =
+ if isRel sigma c || isVar sigma c || count_occurrences sigma (mkRel 1) j.uj_val <= 1 then
+ subst1 c j.uj_val
+ else
+ mkLetIn (na,c,t,j.uj_val);
+ uj_type = subst1 c j.uj_type } in
+ (* spiwack: when an alias appears on a deep branch, its non-expanded
+ form is automatically a variable of the same name. We avoid
+ introducing such superfluous aliases so that refines are elegant. *)
+ let just_pop sigma =
+ let pb =
+ { pb with
+ tomatch = rest;
+ history = pop_history_pattern pb.history;
+ mat = List.map drop_alias_eqn pb.mat } in
+ compile sigma pb
+ in
+ (* If the "match" was orginally over a variable, as in "match x with
+ O => true | n => n end", we give preference to non-expansion in
+ the default clause (i.e. "match x with O => true | n => n end"
+ rather than "match x with O => true | S p => S p end";
+ computationally, this avoids reallocating constructors in cbv
+ evaluation; the drawback is that it might duplicate the instances
+ of the term to match when the corresponding variable is
+ substituted by a non-evaluated expression *)
+ if not program_mode && (isRel sigma orig || isVar sigma orig) then
+ (* Try to compile first using non expanded alias *)
+ try
+ if initial then f orig (Retyping.get_type_of !!(pb.env) sigma orig)
+ else just_pop sigma
+ with e when precatchable_exception e ->
+ (* Try then to compile using expanded alias *)
+ (* Could be needed in case of dependent return clause *)
+ f expanded expanded_typ
+ else
+ (* Try to compile first using expanded alias *)
+ try f expanded expanded_typ
+ with e when precatchable_exception e ->
+ (* Try then to compile using non expanded alias *)
+ (* Could be needed in case of a recursive call which requires to
+ be on a variable for size reasons *)
+ if initial then f orig (Retyping.get_type_of !!(pb.env) sigma orig)
+ else just_pop sigma
+
+
+ (* Remember that a non-trivial pattern has been consumed *)
+ and compile_non_dep_alias sigma pb rest =
let pb =
{ pb with
- tomatch = rest;
- history = pop_history_pattern pb.history;
- mat = List.map drop_alias_eqn pb.mat } in
+ tomatch = rest;
+ history = pop_history_pattern pb.history;
+ mat = List.map drop_alias_eqn pb.mat } in
compile sigma pb
in
- (* If the "match" was orginally over a variable, as in "match x with
- O => true | n => n end", we give preference to non-expansion in
- the default clause (i.e. "match x with O => true | n => n end"
- rather than "match x with O => true | S p => S p end";
- computationally, this avoids reallocating constructors in cbv
- evaluation; the drawback is that it might duplicate the instances
- of the term to match when the corresponding variable is
- substituted by a non-evaluated expression *)
- if not (Flags.is_program_mode ()) && (isRel sigma orig || isVar sigma orig) then
- (* Try to compile first using non expanded alias *)
- try
- if initial then f orig (Retyping.get_type_of !!(pb.env) sigma orig)
- else just_pop sigma
- with e when precatchable_exception e ->
- (* Try then to compile using expanded alias *)
- (* Could be needed in case of dependent return clause *)
- f expanded expanded_typ
- else
- (* Try to compile first using expanded alias *)
- try f expanded expanded_typ
- with e when precatchable_exception e ->
- (* Try then to compile using non expanded alias *)
- (* Could be needed in case of a recursive call which requires to
- be on a variable for size reasons *)
- if initial then f orig (Retyping.get_type_of !!(pb.env) sigma orig)
- else just_pop sigma
-
-
-(* Remember that a non-trivial pattern has been consumed *)
-and compile_non_dep_alias sigma pb rest =
- let pb =
- { pb with
- tomatch = rest;
- history = pop_history_pattern pb.history;
- mat = List.map drop_alias_eqn pb.mat } in
compile sigma pb
(* pour les alias des initiaux, enrichir les env de ce qu'il faut et
@@ -1650,7 +1659,7 @@ let adjust_to_extended_env_and_remove_deps env extenv sigma subst t =
(subst0, t0)
let push_binder sigma d (k,env,subst) =
- (k+1,snd (push_rel sigma d env),List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst)
+ (k+1,snd (push_rel ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma d env),List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst)
let rec list_assoc_in_triple x = function
[] -> raise Not_found
@@ -1771,7 +1780,7 @@ let build_tycon ?loc env tycon_env s subst tycon extenv sigma t =
* further explanations
*)
-let build_inversion_problem loc env sigma tms t =
+let build_inversion_problem ~program_mode loc env sigma tms t =
let make_patvar t (subst,avoid) =
let id = next_name_away (named_hd !!env sigma t Anonymous) avoid in
DAst.make @@ PatVar (Name id), ((id,t)::subst, Id.Set.add id avoid) in
@@ -1796,13 +1805,13 @@ let build_inversion_problem loc env sigma tms t =
let patl = pat :: List.rev patl in
let patl,sign = recover_and_adjust_alias_names acc patl sign in
let p = List.length patl in
- let _,env' = push_rel_context sigma sign env in
+ let _,env' = push_rel_context ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma sign env in
let patl',acc_sign,acc = aux (n+p) env' (sign@acc_sign) tms acc in
List.rev_append patl patl',acc_sign,acc
| (t, NotInd (bo,typ)) :: tms ->
let pat,acc = make_patvar t acc in
let d = LocalAssum (alias_of_pat pat,typ) in
- let patl,acc_sign,acc = aux (n+1) (snd (push_rel sigma d env)) (d::acc_sign) tms acc in
+ let patl,acc_sign,acc = aux (n+1) (snd (push_rel ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma d env)) (d::acc_sign) tms acc in
pat::patl,acc_sign,acc in
let avoid0 = GlobEnv.vars_of_env env in
(* [patl] is a list of patterns revealing the substructure of
@@ -1820,7 +1829,7 @@ let build_inversion_problem loc env sigma tms t =
let decls =
List.map_i (fun i d -> (mkRel i, map_constr (lift i) d)) 1 sign in
- let _,pb_env = push_rel_context sigma sign env in
+ let _,pb_env = push_rel_context ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma sign env in
let decls =
List.map (fun (c,d) -> (c,extract_inductive_data !!(pb_env) sigma d,d)) decls in
@@ -1881,7 +1890,7 @@ let build_inversion_problem loc env sigma tms t =
caseloc = loc;
casestyle = RegularStyle;
typing_function = build_tycon ?loc env pb_env s subst} in
- let sigma, j = compile sigma pb in
+ let sigma, j = compile ~program_mode sigma pb in
(sigma, j.uj_val)
(* Here, [pred] is assumed to be in the context built from all *)
@@ -1934,9 +1943,9 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
| _ -> assert false
in List.rev (buildrec 0 (tomatchl,tmsign))
-let inh_conv_coerce_to_tycon ?loc env sigma j tycon =
+let inh_conv_coerce_to_tycon ?loc ~program_mode env sigma j tycon =
match tycon with
- | Some p -> Coercion.inh_conv_coerce_to ?loc true env sigma j p
+ | Some p -> Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma j p
| None -> sigma, j
(* We put the tycon inside the arity signature, possibly discovering dependencies. *)
@@ -1953,7 +1962,7 @@ let dependent_rel_or_var sigma tm c =
| Var id -> Termops.local_occur_var sigma id c
| _ -> assert false
-let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
+let prepare_predicate_from_arsign_tycon ~program_mode env sigma loc tomatchs arsign c =
let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in
let (rel_subst,var_subst), len =
List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
@@ -2006,7 +2015,8 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
in
assert (len == 0);
let p = predicate 0 c in
- let arsign,env' = List.fold_right_map (push_rel_context sigma) arsign env in
+ let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+ let arsign,env' = List.fold_right_map (push_rel_context ~hypnaming sigma) arsign env in
try let sigma' = fst (Typing.type_of !!env' sigma p) in
Some (sigma', p, arsign)
with e when precatchable_exception e -> None
@@ -2019,7 +2029,7 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
* Each matched term is independently considered dependent or not.
*)
-let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
+let prepare_predicate ?loc ~program_mode typing_fun env sigma tomatchs arsign tycon pred =
let refresh_tycon sigma t =
(* If we put the typing constraint in the term, it has to be
refreshed to preserve the invariant that no algebraic universe
@@ -2041,10 +2051,10 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
sigma, t in
(* First strategy: we build an "inversion" predicate, also replacing the *)
(* dependencies with existential variables *)
- let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
+ let sigma1,pred1 = build_inversion_problem loc ~program_mode env sigma tomatchs t in
(* Optional second strategy: we abstract the tycon wrt to the dependencies *)
let p2 =
- prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
+ prepare_predicate_from_arsign_tycon ~program_mode env sigma loc tomatchs arsign t in
(* Third strategy: we take the type constraint as it is; of course we could *)
(* need something inbetween, abstracting some but not all of the dependencies *)
(* the "inversion" strategy deals with that but unification may not be *)
@@ -2060,7 +2070,7 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
(* Some type annotation *)
| Some rtntyp ->
(* We extract the signature of the arity *)
- let building_arsign,envar = List.fold_right_map (push_rel_context sigma) arsign env in
+ let building_arsign,envar = List.fold_right_map (push_rel_context ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma) arsign env in
let sigma, newt = new_sort_variable univ_flexible sigma in
let sigma, predcclj = typing_fun (mk_tycon (mkSort newt)) envar sigma rtntyp in
let predccl = nf_evar sigma predcclj.uj_val in
@@ -2320,7 +2330,7 @@ let constrs_of_pats typing_fun env sigma eqns tomatchs sign neqs arity =
in
let sigma, ineqs = build_ineqs sigma prevpatterns pats signlen in
let rhs_rels' = rels_of_patsign sigma rhs_rels in
- let _signenv,_ = push_rel_context sigma rhs_rels' env in
+ let _signenv,_ = push_rel_context ~hypnaming:ProgramNaming sigma rhs_rels' env in
let arity =
let args, nargs =
List.fold_right (fun (sign, c, (_, args), _) (allargs,n) ->
@@ -2340,7 +2350,7 @@ let constrs_of_pats typing_fun env sigma eqns tomatchs sign neqs arity =
let eqs_rels, arity = decompose_prod_n_assum sigma neqs arity in
eqs_rels @ neqs_rels @ rhs_rels', arity
in
- let _,rhs_env = push_rel_context sigma rhs_rels' env in
+ let _,rhs_env = push_rel_context ~hypnaming:ProgramNaming sigma rhs_rels' env in
let sigma, j = typing_fun (mk_tycon tycon) rhs_env sigma eqn.rhs.it in
let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
@@ -2518,10 +2528,10 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
(* We build the vector of terms to match consistently with the *)
(* constructors found in patterns *)
- let env, sigma, tomatchs = coerce_to_indtype typing_function env sigma matx tomatchl in
+ let env, sigma, tomatchs = coerce_to_indtype ~program_mode:true typing_function env sigma matx tomatchl in
let tycon = valcon_of_tycon tycon in
let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env sigma tomatchs tycon in
- let _,env = push_rel_context sigma tomatchs_lets env in
+ let _,env = push_rel_context ~hypnaming:ProgramNaming sigma tomatchs_lets env in
let len = List.length eqns in
let sigma, sign, allnames, signlen, eqs, neqs, args =
(* The arity signature *)
@@ -2540,7 +2550,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
sigma, ev, lift nar ev
| Some t ->
let sigma, pred =
- match prepare_predicate_from_arsign_tycon env sigma loc tomatchs sign t with
+ match prepare_predicate_from_arsign_tycon ~program_mode:true env sigma loc tomatchs sign t with
| Some (evd, pred, arsign) -> evd, pred
| None -> sigma, lift nar t
in
@@ -2557,7 +2567,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
in
let matx = List.rev matx in
let _ = assert (Int.equal len (List.length lets)) in
- let _,env = push_rel_context sigma lets env in
+ let _,env = push_rel_context ~hypnaming:ProgramNaming sigma lets env in
let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in
let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in
let args = List.rev_map (lift len) args in
@@ -2604,7 +2614,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
casestyle= style;
typing_function = typing_function } in
- let sigma, j = compile sigma pb in
+ let sigma, j = compile ~program_mode:true sigma pb in
(* We check for unused patterns *)
List.iter (check_unused_pattern !!env) matx;
let body = it_mkLambda_or_LetIn (applist (j.uj_val, args)) lets in
@@ -2617,8 +2627,8 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
(**************************************************************************)
(* Main entry of the matching compilation *)
-let compile_cases ?loc style (typing_fun, sigma) tycon env (predopt, tomatchl, eqns) =
- if predopt == None && Flags.is_program_mode () && Program.is_program_cases () then
+let compile_cases ?loc ~program_mode style (typing_fun, sigma) tycon env (predopt, tomatchl, eqns) =
+ if predopt == None && program_mode && Program.is_program_cases () then
compile_program_cases ?loc style (typing_fun, sigma)
tycon env (predopt, tomatchl, eqns)
else
@@ -2628,13 +2638,13 @@ let compile_cases ?loc style (typing_fun, sigma) tycon env (predopt, tomatchl, e
(* We build the vector of terms to match consistently with the *)
(* constructors found in patterns *)
- let predenv, sigma, tomatchs = coerce_to_indtype typing_fun env sigma matx tomatchl in
+ let predenv, sigma, tomatchs = coerce_to_indtype ~program_mode typing_fun env sigma matx tomatchl in
(* If an elimination predicate is provided, we check it is compatible
with the type of arguments to match; if none is provided, we
build alternative possible predicates *)
let arsign = extract_arity_signature !!env tomatchs tomatchl in
- let preds = prepare_predicate ?loc typing_fun predenv sigma tomatchs arsign tycon predopt in
+ let preds = prepare_predicate ?loc ~program_mode typing_fun predenv sigma tomatchs arsign tycon predopt in
let compile_for_one_predicate (sigma,nal,pred) =
(* We push the initial terms to match and push their alias to rhs' envs *)
@@ -2679,10 +2689,10 @@ let compile_cases ?loc style (typing_fun, sigma) tycon env (predopt, tomatchl, e
casestyle = style;
typing_function = typing_fun } in
- let sigma, j = compile sigma pb in
+ let sigma, j = compile ~program_mode sigma pb in
(* We coerce to the tycon (if an elim predicate was provided) *)
- inh_conv_coerce_to_tycon ?loc !!env sigma j tycon
+ inh_conv_coerce_to_tycon ?loc ~program_mode !!env sigma j tycon
in
(* Return the term compiled with the first possible elimination *)
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 36cfa0a70d..b0349a3d05 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -40,7 +40,7 @@ val irrefutable : env -> cases_pattern -> bool
(** {6 Compilation primitive. } *)
val compile_cases :
- ?loc:Loc.t -> case_style ->
+ ?loc:Loc.t -> program_mode:bool -> case_style ->
(type_constraint -> GlobEnv.t -> evar_map -> glob_constr -> evar_map * unsafe_judgment) * evar_map ->
type_constraint ->
GlobEnv.t -> glob_constr option * tomatch_tuples * cases_clauses ->
@@ -111,9 +111,9 @@ type 'a pattern_matching_problem =
casestyle : case_style;
typing_function: type_constraint -> GlobEnv.t -> evar_map -> 'a option -> evar_map * unsafe_judgment }
-val compile : evar_map -> 'a pattern_matching_problem -> evar_map * unsafe_judgment
+val compile : program_mode:bool -> evar_map -> 'a pattern_matching_problem -> evar_map * unsafe_judgment
-val prepare_predicate : ?loc:Loc.t ->
+val prepare_predicate : ?loc:Loc.t -> program_mode:bool ->
(type_constraint ->
GlobEnv.t -> Evd.evar_map -> glob_constr -> Evd.evar_map * unsafe_judgment) ->
GlobEnv.t ->
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 4d1d405bd7..9e93c470b1 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -393,7 +393,7 @@ let apply_coercion env sigma p hj typ_cl =
with NoCoercion as e -> raise e
(* Try to coerce to a funclass; raise NoCoercion if not possible *)
-let inh_app_fun_core env evd j =
+let inh_app_fun_core ~program_mode env evd j =
let t = whd_all env evd j.uj_type in
match EConstr.kind evd t with
| Prod (_,_,_) -> (evd,j)
@@ -404,25 +404,25 @@ let inh_app_fun_core env evd j =
try let t,p =
lookup_path_to_fun_from env evd j.uj_type in
apply_coercion env evd p j t
- with Not_found | NoCoercion ->
- if Flags.is_program_mode () then
- try
- let evdref = ref evd in
- let coercef, t = mu env evdref t in
- let res = { uj_val = app_opt env evdref coercef j.uj_val; uj_type = t } in
- (!evdref, res)
- with NoSubtacCoercion | NoCoercion ->
- (evd,j)
- else raise NoCoercion
+ with Not_found | NoCoercion ->
+ if program_mode then
+ try
+ let evdref = ref evd in
+ let coercef, t = mu env evdref t in
+ let res = { uj_val = app_opt env evdref coercef j.uj_val; uj_type = t } in
+ (!evdref, res)
+ with NoSubtacCoercion | NoCoercion ->
+ (evd,j)
+ else raise NoCoercion
(* Try to coerce to a funclass; returns [j] if no coercion is applicable *)
-let inh_app_fun resolve_tc env evd j =
- try inh_app_fun_core env evd j
+let inh_app_fun ~program_mode resolve_tc env evd j =
+ try inh_app_fun_core ~program_mode env evd j
with
| NoCoercion when not resolve_tc
|| not (get_use_typeclasses_for_conversion ()) -> (evd, j)
| NoCoercion ->
- try inh_app_fun_core env (saturate_evd env evd) j
+ try inh_app_fun_core ~program_mode env (saturate_evd env evd) j
with NoCoercion -> (evd, j)
let type_judgment env sigma j =
@@ -449,8 +449,8 @@ let inh_coerce_to_sort ?loc env evd j =
| _ ->
inh_tosort_force ?loc env evd j
-let inh_coerce_to_base ?loc env evd j =
- if Flags.is_program_mode () then
+let inh_coerce_to_base ?loc ~program_mode env evd j =
+ if program_mode then
let evdref = ref evd in
let ct, typ' = mu env evdref j.uj_type in
let res =
@@ -459,8 +459,8 @@ let inh_coerce_to_base ?loc env evd j =
in !evdref, res
else (evd, j)
-let inh_coerce_to_prod ?loc env evd t =
- if Flags.is_program_mode () then
+let inh_coerce_to_prod ?loc ~program_mode env evd t =
+ if program_mode then
let evdref = ref evd in
let _, typ' = mu env evdref t in
!evdref, typ'
@@ -520,13 +520,13 @@ let rec inh_conv_coerce_to_fail ?loc env evd rigidonly v t c1 =
| _ -> raise (NoCoercionNoUnifier (best_failed_evd,e))
(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
-let inh_conv_coerce_to_gen ?loc resolve_tc rigidonly env evd cj t =
+let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly env evd cj t =
let (evd', val') =
try
inh_conv_coerce_to_fail ?loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
with NoCoercionNoUnifier (best_failed_evd,e) ->
try
- if Flags.is_program_mode () then
+ if program_mode then
coerce_itf ?loc env evd (Some cj.uj_val) cj.uj_type t
else raise NoSubtacCoercion
with
@@ -545,9 +545,11 @@ let inh_conv_coerce_to_gen ?loc resolve_tc rigidonly env evd cj t =
let val' = match val' with Some v -> v | None -> assert(false) in
(evd',{ uj_val = val'; uj_type = t })
-let inh_conv_coerce_to ?loc resolve_tc = inh_conv_coerce_to_gen ?loc resolve_tc false
+let inh_conv_coerce_to ?loc ~program_mode resolve_tc =
+ inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc false
-let inh_conv_coerce_rigid_to ?loc resolve_tc = inh_conv_coerce_to_gen resolve_tc ?loc true
+let inh_conv_coerce_rigid_to ?loc ~program_mode resolve_tc =
+ inh_conv_coerce_to_gen ~program_mode resolve_tc ?loc true
let inh_conv_coerces_to ?loc env evd t t' =
try
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 6cfd958b46..a941391125 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -21,7 +21,7 @@ open Glob_term
type a product; it returns [j] if no coercion is applicable.
resolve_tc=false disables resolving type classes (as the last
resort before failing) *)
-val inh_app_fun : bool ->
+val inh_app_fun : program_mode:bool -> bool ->
env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
(** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
@@ -33,11 +33,11 @@ val inh_coerce_to_sort : ?loc:Loc.t ->
(** [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
inserts a coercion into [j], if needed, in such a way it gets as
type its base type (the notion depends on the coercion system) *)
-val inh_coerce_to_base : ?loc:Loc.t ->
+val inh_coerce_to_base : ?loc:Loc.t -> program_mode:bool ->
env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
(** [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
-val inh_coerce_to_prod : ?loc:Loc.t ->
+val inh_coerce_to_prod : ?loc:Loc.t -> program_mode:bool ->
env -> evar_map -> types -> evar_map * types
(** [inh_conv_coerce_to resolve_tc Loc.t env isevars j t] coerces [j] to an
@@ -45,10 +45,10 @@ val inh_coerce_to_prod : ?loc:Loc.t ->
a way [t] and [j.uj_type] are convertible; it fails if no coercion is
applicable. resolve_tc=false disables resolving type classes (as the last
resort before failing) *)
-val inh_conv_coerce_to : ?loc:Loc.t -> bool ->
+val inh_conv_coerce_to : ?loc:Loc.t -> program_mode:bool -> bool ->
env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
-val inh_conv_coerce_rigid_to : ?loc:Loc.t -> bool ->
+val inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool ->bool ->
env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
(** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index 49a08afe80..d6b204561e 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -38,10 +38,10 @@ type t = {
lvar : ltac_var_map;
}
-let make env sigma lvar =
+let make ~hypnaming env sigma lvar =
let get_extra env sigma =
let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in
- Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc)
+ Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ~hypnaming sigma d acc)
(rel_context env) ~init:(empty_csubst, avoid, named_context env) in
{
static_env = env;
@@ -66,32 +66,32 @@ let ltac_interp_id { ltac_idents ; ltac_genargs } id =
let ltac_interp_name lvar = Nameops.Name.map (ltac_interp_id lvar)
-let push_rel sigma d env =
+let push_rel ~hypnaming sigma d env =
let d' = Context.Rel.Declaration.map_name (ltac_interp_name env.lvar) d in
let env = {
static_env = push_rel d env.static_env;
renamed_env = push_rel d' env.renamed_env;
- extra = lazy (push_rel_decl_to_named_context sigma d' (Lazy.force env.extra));
+ extra = lazy (push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d' (Lazy.force env.extra));
lvar = env.lvar;
} in
d', env
-let push_rel_context ?(force_names=false) sigma ctx env =
+let push_rel_context ~hypnaming ?(force_names=false) sigma ctx env =
let open Context.Rel.Declaration in
let ctx' = List.Smart.map (map_name (ltac_interp_name env.lvar)) ctx in
let ctx' = if force_names then Namegen.name_context env.renamed_env sigma ctx' else ctx' in
let env = {
static_env = push_rel_context ctx env.static_env;
renamed_env = push_rel_context ctx' env.renamed_env;
- extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context sigma d acc) ctx' (Lazy.force env.extra));
+ extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d acc) ctx' (Lazy.force env.extra));
lvar = env.lvar;
} in
ctx', env
-let push_rec_types sigma (lna,typarray) env =
+let push_rec_types ~hypnaming sigma (lna,typarray) env =
let open Context.Rel.Declaration in
let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in
- let env,ctx = Array.fold_left_map (fun e assum -> let (d,e) = push_rel sigma assum e in (e,d)) env ctxt in
+ let env,ctx = Array.fold_left_map (fun e assum -> let (d,e) = push_rel sigma assum e ~hypnaming in (e,d)) env ctxt in
Array.map get_name ctx, env
let new_evar env sigma ?src ?naming typ =
diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli
index e8a2fbdd16..63f72e60bd 100644
--- a/pretyping/globEnv.mli
+++ b/pretyping/globEnv.mli
@@ -13,6 +13,7 @@ open Environ
open Evd
open EConstr
open Ltac_pretype
+open Evarutil
(** To embed constr in glob_constr *)
@@ -37,7 +38,7 @@ type t
(** Build a pretyping environment from an ltac environment *)
-val make : env -> evar_map -> ltac_var_map -> t
+val make : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t
(** Export the underlying environement *)
@@ -47,9 +48,9 @@ val vars_of_env : t -> Id.Set.t
(** Push to the environment, returning the declaration(s) with interpreted names *)
-val push_rel : evar_map -> rel_declaration -> t -> rel_declaration * t
-val push_rel_context : ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t
-val push_rec_types : evar_map -> Name.t array * constr array -> t -> Name.t array * t
+val push_rel : hypnaming:naming_mode -> evar_map -> rel_declaration -> t -> rel_declaration * t
+val push_rel_context : hypnaming:naming_mode -> ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t
+val push_rec_types : hypnaming:naming_mode -> evar_map -> Name.t array * constr array -> t -> Name.t array * t
(** Declare an evar using renaming information *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 57705fa209..46e463512d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -190,7 +190,8 @@ type inference_flags = {
use_typeclasses : bool;
solve_unification_constraints : bool;
fail_evar : bool;
- expand_evars : bool
+ expand_evars : bool;
+ program_mode : bool;
}
(* Compute the set of still-undefined initial evars up to restriction
@@ -226,17 +227,17 @@ let frozen_and_pending_holes (sigma, sigma') =
end in
FrozenProgress data
-let apply_typeclasses env sigma frozen fail_evar =
+let apply_typeclasses ~program_mode env sigma frozen fail_evar =
let filter_frozen = match frozen with
| FrozenId map -> fun evk -> Evar.Map.mem evk map
| FrozenProgress (lazy (frozen, _)) -> fun evk -> Evar.Set.mem evk frozen
in
let sigma = Typeclasses.resolve_typeclasses
- ~filter:(if Flags.is_program_mode ()
+ ~filter:(if program_mode
then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk))
else (fun evk evi -> Typeclasses.no_goals evk evi && not (filter_frozen evk)))
~split:true ~fail:fail_evar env sigma in
- let sigma = if Flags.is_program_mode () then (* Try optionally solving the obligations *)
+ let sigma = if program_mode then (* Try optionally solving the obligations *)
Typeclasses.resolve_typeclasses
~filter:(fun evk evi -> Typeclasses.all_evars evk evi && not (filter_frozen evk)) ~split:true ~fail:false env sigma
else sigma in
@@ -264,9 +265,9 @@ let apply_heuristics env sigma fail_evar =
let e = CErrors.push e in
if fail_evar then iraise e else sigma
-let check_typeclasses_instances_are_solved env current_sigma frozen =
+let check_typeclasses_instances_are_solved ~program_mode env current_sigma frozen =
(* Naive way, call resolution again with failure flag *)
- apply_typeclasses env current_sigma frozen true
+ apply_typeclasses ~program_mode env current_sigma frozen true
let check_extra_evars_are_solved env current_sigma frozen = match frozen with
| FrozenId _ -> ()
@@ -295,18 +296,19 @@ let check_evars env initial_sigma sigma c =
| _ -> EConstr.iter sigma proc_rec c
in proc_rec c
-let check_evars_are_solved env sigma frozen =
- let sigma = check_typeclasses_instances_are_solved env sigma frozen in
+let check_evars_are_solved ~program_mode env sigma frozen =
+ let sigma = check_typeclasses_instances_are_solved ~program_mode env sigma frozen in
check_problems_are_solved env sigma;
check_extra_evars_are_solved env sigma frozen
(* Try typeclasses, hooks, unification heuristics ... *)
let solve_remaining_evars ?hook flags env ?initial sigma =
+ let program_mode = flags.program_mode in
let frozen = frozen_and_pending_holes (initial, sigma) in
let sigma =
if flags.use_typeclasses
- then apply_typeclasses env sigma frozen false
+ then apply_typeclasses ~program_mode env sigma frozen false
else sigma
in
let sigma = match hook with
@@ -317,12 +319,12 @@ let solve_remaining_evars ?hook flags env ?initial sigma =
then apply_heuristics env sigma false
else sigma
in
- if flags.fail_evar then check_evars_are_solved env sigma frozen;
+ if flags.fail_evar then check_evars_are_solved ~program_mode env sigma frozen;
sigma
-let check_evars_are_solved env ?initial current_sigma =
+let check_evars_are_solved ~program_mode env ?initial current_sigma =
let frozen = frozen_and_pending_holes (initial, current_sigma) in
- check_evars_are_solved env current_sigma frozen
+ check_evars_are_solved ~program_mode env current_sigma frozen
let process_inference_flags flags env initial (sigma,c,cty) =
let sigma = solve_remaining_evars flags env ~initial sigma in
@@ -351,10 +353,10 @@ let adjust_evar_source sigma na c =
| _, _ -> sigma, c
(* coerce to tycon if any *)
-let inh_conv_coerce_to_tycon ?loc resolve_tc env sigma j = function
+let inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j = function
| None -> sigma, j
| Some t ->
- Coercion.inh_conv_coerce_to ?loc resolve_tc !!env sigma j t
+ Coercion.inh_conv_coerce_to ?loc ~program_mode resolve_tc !!env sigma j t
let check_instance loc subst = function
| [] -> ()
@@ -453,20 +455,18 @@ let new_type_evar env sigma loc =
new_type_evar env sigma ~src:(Loc.tag ?loc Evar_kinds.InternalHole)
let mark_obligation_evar sigma k evc =
- if Flags.is_program_mode () then
- match k with
- | Evar_kinds.QuestionMark _
- | Evar_kinds.ImplicitArg (_, _, false) ->
- Evd.set_obligation_evar sigma (fst (destEvar sigma evc))
- | _ -> sigma
- else sigma
+ match k with
+ | Evar_kinds.QuestionMark _
+ | Evar_kinds.ImplicitArg (_, _, false) ->
+ Evd.set_obligation_evar sigma (fst (destEvar sigma evc))
+ | _ -> sigma
(* [pretype tycon env sigma lvar lmeta cstr] attempts to type [cstr] *)
(* in environment [env], with existential variables [sigma] and *)
(* the type constraint tycon *)
-let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma : evar_map) t =
- let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc resolve_tc in
+let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma : evar_map) t =
+ let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc in
let pretype_type = pretype_type k0 resolve_tc in
let pretype = pretype k0 resolve_tc in
let open Context.Rel.Declaration in
@@ -477,7 +477,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
inh_conv_coerce_to_tycon ?loc env sigma t_ref tycon
| GVar id ->
- let sigma, t_id = pretype_id (fun e r t -> pretype tycon e r t) k0 loc env sigma id in
+ let sigma, t_id = pretype_id (fun e r t -> pretype ~program_mode tycon e r t) k0 loc env sigma id in
inh_conv_coerce_to_tycon ?loc env sigma t_id tycon
| GEvar (id, inst) ->
@@ -488,7 +488,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
try Evd.evar_key id sigma
with Not_found -> error_evar_not_found ?loc !!env sigma id in
let hyps = evar_filtered_context (Evd.find sigma evk) in
- let sigma, args = pretype_instance k0 resolve_tc env sigma loc hyps evk inst in
+ let sigma, args = pretype_instance ~program_mode k0 resolve_tc env sigma loc hyps evk inst in
let c = mkEvar (evk, args) in
let j = Retyping.get_judgment_of !!env sigma c in
inh_conv_coerce_to_tycon ?loc env sigma j tycon
@@ -513,7 +513,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
| Some ty -> sigma, ty
| None -> new_type_evar env sigma loc in
let sigma, uj_val = new_evar env sigma ~src:(loc,k) ~naming ty in
- let sigma = mark_obligation_evar sigma k uj_val in
+ let sigma = if program_mode then mark_obligation_evar sigma k uj_val else sigma in
sigma, { uj_val; uj_type = ty }
| GHole (k, _naming, Some arg) ->
@@ -525,24 +525,25 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
sigma, { uj_val = c; uj_type = ty }
| GRec (fixkind,names,bl,lar,vdef) ->
+ let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
let rec type_bl env sigma ctxt = function
| [] -> sigma, ctxt
| (na,bk,None,ty)::bl ->
- let sigma, ty' = pretype_type empty_valcon env sigma ty in
- let dcl = LocalAssum (na, ty'.utj_val) in
- let dcl', env = push_rel sigma dcl env in
+ let sigma, ty' = pretype_type ~program_mode empty_valcon env sigma ty in
+ let dcl = LocalAssum (na, ty'.utj_val) in
+ let dcl', env = push_rel ~hypnaming sigma dcl env in
type_bl env sigma (Context.Rel.add dcl' ctxt) bl
| (na,bk,Some bd,ty)::bl ->
- let sigma, ty' = pretype_type empty_valcon env sigma ty in
- let sigma, bd' = pretype (mk_tycon ty'.utj_val) env sigma bd in
+ let sigma, ty' = pretype_type ~program_mode empty_valcon env sigma ty in
+ let sigma, bd' = pretype ~program_mode (mk_tycon ty'.utj_val) env sigma bd in
let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in
- let dcl', env = push_rel sigma dcl env in
+ let dcl', env = push_rel ~hypnaming sigma dcl env in
type_bl env sigma (Context.Rel.add dcl' ctxt) bl in
let sigma, ctxtv = Array.fold_left_map (fun sigma -> type_bl env sigma Context.Rel.empty) sigma bl in
let sigma, larj =
Array.fold_left2_map
(fun sigma e ar ->
- pretype_type empty_valcon (snd (push_rel_context sigma e env)) sigma ar)
+ pretype_type ~program_mode empty_valcon (snd (push_rel_context ~hypnaming sigma e env)) sigma ar)
sigma ctxtv lar in
let lara = Array.map (fun a -> a.utj_val) larj in
let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
@@ -562,7 +563,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
| None -> sigma
in
(* Note: bodies are not used by push_rec_types, so [||] is safe *)
- let names,newenv = push_rec_types sigma (names,ftys) env in
+ let names,newenv = push_rec_types ~hypnaming sigma (names,ftys) env in
let sigma, vdefj =
Array.fold_left2_map_i
(fun i sigma ctxt def ->
@@ -571,8 +572,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
let (ctxt,ty) =
decompose_prod_n_assum sigma (Context.Rel.length ctxt)
(lift nbfix ftys.(i)) in
- let ctxt,nenv = push_rel_context sigma ctxt newenv in
- let sigma, j = pretype (mk_tycon ty) nenv sigma def in
+ let ctxt,nenv = push_rel_context ~hypnaming sigma ctxt newenv in
+ let sigma, j = pretype ~program_mode (mk_tycon ty) nenv sigma def in
sigma, { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
sigma ctxtv vdef in
@@ -618,14 +619,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
inh_conv_coerce_to_tycon ?loc env sigma j tycon
| GApp (f,args) ->
- let sigma, fj = pretype empty_tycon env sigma f in
+ let sigma, fj = pretype ~program_mode empty_tycon env sigma f in
let floc = loc_of_glob_constr f in
let length = List.length args in
let candargs =
(* Bidirectional typechecking hint:
parameters of a constructor are completely determined
by a typing constraint *)
- if Flags.is_program_mode () && length > 0 && isConstruct sigma fj.uj_val then
+ if program_mode && length > 0 && isConstruct sigma fj.uj_val then
match tycon with
| None -> []
| Some ty ->
@@ -656,12 +657,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
| [] -> sigma, resj
| c::rest ->
let argloc = loc_of_glob_constr c in
- let sigma, resj = Coercion.inh_app_fun resolve_tc !!env sigma resj in
+ let sigma, resj = Coercion.inh_app_fun ~program_mode resolve_tc !!env sigma resj in
let resty = whd_all !!env sigma resj.uj_type in
match EConstr.kind sigma resty with
| Prod (na,c1,c2) ->
let tycon = Some c1 in
- let sigma, hj = pretype tycon env sigma c in
+ let sigma, hj = pretype ~program_mode tycon env sigma c in
let sigma, candargs, ujval =
match candargs with
| [] -> sigma, [], j_val hj
@@ -678,7 +679,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
let j = { uj_val = value; uj_type = typ } in
apply_rec env sigma (n+1) j candargs rest
| _ ->
- let sigma, hj = pretype empty_tycon env sigma c in
+ let sigma, hj = pretype ~program_mode empty_tycon env sigma c in
error_cant_apply_not_functional
?loc:(Loc.merge_opt floc argloc) !!env sigma resj [|hj|]
in
@@ -703,29 +704,31 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
match tycon with
| None -> sigma, tycon
| Some ty ->
- let sigma, ty' = Coercion.inh_coerce_to_prod ?loc !!env sigma ty in
+ let sigma, ty' = Coercion.inh_coerce_to_prod ?loc ~program_mode !!env sigma ty in
sigma, Some ty'
in
let sigma, (name',dom,rng) = split_tycon ?loc !!env sigma tycon' in
let dom_valcon = valcon_of_tycon dom in
- let sigma, j = pretype_type dom_valcon env sigma c1 in
+ let sigma, j = pretype_type ~program_mode dom_valcon env sigma c1 in
let var = LocalAssum (name, j.utj_val) in
- let var',env' = push_rel sigma var env in
- let sigma, j' = pretype rng env' sigma c2 in
+ let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+ let var',env' = push_rel ~hypnaming sigma var env in
+ let sigma, j' = pretype ~program_mode rng env' sigma c2 in
let name = get_name var' in
let resj = judge_of_abstraction !!env (orelse_name name name') j j' in
inh_conv_coerce_to_tycon ?loc env sigma resj tycon
| GProd(name,bk,c1,c2) ->
- let sigma, j = pretype_type empty_valcon env sigma c1 in
+ let sigma, j = pretype_type ~program_mode empty_valcon env sigma c1 in
+ let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
let sigma, name, j' = match name with
| Anonymous ->
- let sigma, j = pretype_type empty_valcon env sigma c2 in
+ let sigma, j = pretype_type ~program_mode empty_valcon env sigma c2 in
sigma, name, { j with utj_val = lift 1 j.utj_val }
| Name _ ->
let var = LocalAssum (name, j.utj_val) in
- let var, env' = push_rel sigma var env in
- let sigma, c2_j = pretype_type empty_valcon env' sigma c2 in
+ let var, env' = push_rel ~hypnaming sigma var env in
+ let sigma, c2_j = pretype_type ~program_mode empty_valcon env' sigma c2 in
sigma, get_name var, c2_j
in
let resj =
@@ -741,23 +744,24 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
let sigma, tycon1 =
match t with
| Some t ->
- let sigma, t_j = pretype_type empty_valcon env sigma t in
+ let sigma, t_j = pretype_type ~program_mode empty_valcon env sigma t in
sigma, mk_tycon t_j.utj_val
| None ->
sigma, empty_tycon in
- let sigma, j = pretype tycon1 env sigma c1 in
+ let sigma, j = pretype ~program_mode tycon1 env sigma c1 in
let sigma, t = Evarsolve.refresh_universes
~onlyalg:true ~status:Evd.univ_flexible (Some false) !!env sigma j.uj_type in
let var = LocalDef (name, j.uj_val, t) in
let tycon = lift_tycon 1 tycon in
- let var, env = push_rel sigma var env in
- let sigma, j' = pretype tycon env sigma c2 in
+ let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+ let var, env = push_rel ~hypnaming sigma var env in
+ let sigma, j' = pretype ~program_mode tycon env sigma c2 in
let name = get_name var in
sigma, { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
uj_type = subst1 j.uj_val j'.uj_type }
| GLetTuple (nal,(na,po),c,d) ->
- let sigma, cj = pretype empty_tycon env sigma c in
+ let sigma, cj = pretype ~program_mode empty_tycon env sigma c in
let (IndType (indf,realargs)) =
try find_rectype !!env sigma cj.uj_type
with Not_found ->
@@ -792,7 +796,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
| _ -> assert false
in aux 1 1 (List.rev nal) cs.cs_args, true in
let fsign = Context.Rel.map (whd_betaiota sigma) fsign in
- let fsign,env_f = push_rel_context sigma fsign env in
+ let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+ let fsign,env_f = push_rel_context ~hypnaming sigma fsign env in
let obj ind p v f =
if not record then
let f = it_mkLambda_or_LetIn f fsign in
@@ -810,10 +815,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in
let predenv = Cases.make_return_predicate_ltac_lvar env sigma na c cj.uj_val in
let nar = List.length arsgn in
- let psign',env_p = push_rel_context ~force_names:true sigma psign predenv in
+ let psign',env_p = push_rel_context ~hypnaming ~force_names:true sigma psign predenv in
(match po with
| Some p ->
- let sigma, pj = pretype_type empty_valcon env_p sigma p in
+ let sigma, pj = pretype_type ~program_mode empty_valcon env_p sigma p in
let ccl = nf_evar sigma pj.utj_val in
let p = it_mkLambda_or_LetIn ccl psign' in
let inst =
@@ -821,7 +826,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
@[EConstr.of_constr (build_dependent_constructor cs)] in
let lp = lift cs.cs_nargs p in
let fty = hnf_lam_applist !!env sigma lp inst in
- let sigma, fj = pretype (mk_tycon fty) env_f sigma d in
+ let sigma, fj = pretype ~program_mode (mk_tycon fty) env_f sigma d in
let v =
let ind,_ = dest_ind_family indf in
Typing.check_allowed_sort !!env sigma ind cj.uj_val p;
@@ -831,7 +836,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
| None ->
let tycon = lift_tycon cs.cs_nargs tycon in
- let sigma, fj = pretype tycon env_f sigma d in
+ let sigma, fj = pretype ~program_mode tycon env_f sigma d in
let ccl = nf_evar sigma fj.uj_type in
let ccl =
if noccur_between sigma 1 cs.cs_nargs ccl then
@@ -848,7 +853,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
in sigma, { uj_val = v; uj_type = ccl })
| GIf (c,(na,po),b1,b2) ->
- let sigma, cj = pretype empty_tycon env sigma c in
+ let sigma, cj = pretype ~program_mode empty_tycon env sigma c in
let (IndType (indf,realargs)) =
try find_rectype !!env sigma cj.uj_type
with Not_found ->
@@ -869,10 +874,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *)
let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in
let predenv = Cases.make_return_predicate_ltac_lvar env sigma na c cj.uj_val in
- let psign,env_p = push_rel_context sigma psign predenv in
+ let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+ let psign,env_p = push_rel_context ~hypnaming sigma psign predenv in
let sigma, pred, p = match po with
| Some p ->
- let sigma, pj = pretype_type empty_valcon env_p sigma p in
+ let sigma, pj = pretype_type ~program_mode empty_valcon env_p sigma p in
let ccl = nf_evar sigma pj.utj_val in
let pred = it_mkLambda_or_LetIn ccl psign in
let typ = lift (- nar) (beta_applist sigma (pred,[cj.uj_val])) in
@@ -894,8 +900,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
let csgn =
List.map (set_name Anonymous) cs_args
in
- let _,env_c = push_rel_context sigma csgn env in
- let sigma, bj = pretype (mk_tycon pi) env_c sigma b in
+ let _,env_c = push_rel_context ~hypnaming sigma csgn env in
+ let sigma, bj = pretype ~program_mode (mk_tycon pi) env_c sigma b in
sigma, it_mkLambda_or_LetIn bj.uj_val cs_args in
let sigma, b1 = f sigma cstrs.(0) b1 in
let sigma, b2 = f sigma cstrs.(1) b2 in
@@ -910,23 +916,23 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
inh_conv_coerce_to_tycon ?loc env sigma cj tycon
| GCases (sty,po,tml,eqns) ->
- Cases.compile_cases ?loc sty (pretype, sigma) tycon env (po,tml,eqns)
+ Cases.compile_cases ?loc ~program_mode sty (pretype ~program_mode, sigma) tycon env (po,tml,eqns)
| GCast (c,k) ->
let sigma, cj =
match k with
| CastCoerce ->
- let sigma, cj = pretype empty_tycon env sigma c in
- Coercion.inh_coerce_to_base ?loc !!env sigma cj
+ let sigma, cj = pretype ~program_mode empty_tycon env sigma c in
+ Coercion.inh_coerce_to_base ?loc ~program_mode !!env sigma cj
| CastConv t | CastVM t | CastNative t ->
let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in
- let sigma, tj = pretype_type empty_valcon env sigma t in
+ let sigma, tj = pretype_type ~program_mode empty_valcon env sigma t in
let sigma, tval = Evarsolve.refresh_universes
~onlyalg:true ~status:Evd.univ_flexible (Some false) !!env sigma tj.utj_val in
let tval = nf_evar sigma tval in
let (sigma, cj), tval = match k with
| VMcast ->
- let sigma, cj = pretype empty_tycon env sigma c in
+ let sigma, cj = pretype ~program_mode empty_tycon env sigma c in
let cty = nf_evar sigma cj.uj_type and tval = nf_evar sigma tval in
if not (occur_existential sigma cty || occur_existential sigma tval) then
match Reductionops.vm_infer_conv !!env sigma cty tval with
@@ -937,7 +943,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
else user_err ?loc (str "Cannot check cast with vm: " ++
str "unresolved arguments remain.")
| NATIVEcast ->
- let sigma, cj = pretype empty_tycon env sigma c in
+ let sigma, cj = pretype ~program_mode empty_tycon env sigma c in
let cty = nf_evar sigma cj.uj_type and tval = nf_evar sigma tval in
begin
match Nativenorm.native_infer_conv !!env sigma cty tval with
@@ -947,7 +953,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
(ConversionFailed (!!env,cty,tval))
end
| _ ->
- pretype (mk_tycon tval) env sigma c, tval
+ pretype ~program_mode (mk_tycon tval) env sigma c, tval
in
let v = mkCast (cj.uj_val, k, tval) in
sigma, { uj_val = v; uj_type = tval }
@@ -961,7 +967,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
in
inh_conv_coerce_to_tycon ?loc env sigma resj tycon
-and pretype_instance k0 resolve_tc env sigma loc hyps evk update =
+and pretype_instance ~program_mode k0 resolve_tc env sigma loc hyps evk update =
let f decl (subst,update,sigma) =
let id = NamedDecl.get_id decl in
let b = Option.map (replace_vars subst) (NamedDecl.get_value decl) in
@@ -993,7 +999,7 @@ and pretype_instance k0 resolve_tc env sigma loc hyps evk update =
let sigma, c, update =
try
let c = List.assoc id update in
- let sigma, c = pretype k0 resolve_tc (mk_tycon t) env sigma c in
+ let sigma, c = pretype ~program_mode k0 resolve_tc (mk_tycon t) env sigma c in
check_body sigma id (Some c.uj_val);
sigma, c.uj_val, List.remove_assoc id update
with Not_found ->
@@ -1018,7 +1024,7 @@ and pretype_instance k0 resolve_tc env sigma loc hyps evk update =
sigma, Array.map_of_list snd subst
(* [pretype_type valcon env sigma c] coerces [c] into a type *)
-and pretype_type k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get c with
+and pretype_type ~program_mode k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get c with
| GHole (knd, naming, None) ->
let loc = loc_of_glob_constr c in
(match valcon with
@@ -1042,10 +1048,10 @@ and pretype_type k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get
| None ->
let sigma, s = new_sort_variable univ_flexible_alg sigma in
let sigma, utj_val = new_evar env sigma ~src:(loc, knd) ~naming (mkSort s) in
- let sigma = mark_obligation_evar sigma knd utj_val in
+ let sigma = if program_mode then mark_obligation_evar sigma knd utj_val else sigma in
sigma, { utj_val; utj_type = s})
| _ ->
- let sigma, j = pretype k0 resolve_tc empty_tycon env sigma c in
+ let sigma, j = pretype ~program_mode k0 resolve_tc empty_tycon env sigma c in
let loc = loc_of_glob_constr c in
let sigma, tj = Coercion.inh_coerce_to_sort ?loc !!env sigma j in
match valcon with
@@ -1059,17 +1065,21 @@ and pretype_type k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get
end
let ise_pretype_gen flags env sigma lvar kind c =
- let env = GlobEnv.make env sigma lvar in
+ let program_mode = flags.program_mode in
+ let hypnaming =
+ if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames
+ in
+ let env = GlobEnv.make ~hypnaming env sigma lvar in
let k0 = Context.Rel.length (rel_context !!env) in
let sigma', c', c'_ty = match kind with
| WithoutTypeConstraint ->
- let sigma, j = pretype k0 flags.use_typeclasses empty_tycon env sigma c in
+ let sigma, j = pretype ~program_mode k0 flags.use_typeclasses empty_tycon env sigma c in
sigma, j.uj_val, j.uj_type
| OfType exptyp ->
- let sigma, j = pretype k0 flags.use_typeclasses (mk_tycon exptyp) env sigma c in
+ let sigma, j = pretype ~program_mode k0 flags.use_typeclasses (mk_tycon exptyp) env sigma c in
sigma, j.uj_val, j.uj_type
| IsType ->
- let sigma, tj = pretype_type k0 flags.use_typeclasses empty_valcon env sigma c in
+ let sigma, tj = pretype_type ~program_mode k0 flags.use_typeclasses empty_valcon env sigma c in
sigma, tj.utj_val, mkSort tj.utj_type
in
process_inference_flags flags !!env sigma (sigma',c',c'_ty)
@@ -1078,13 +1088,17 @@ let default_inference_flags fail = {
use_typeclasses = true;
solve_unification_constraints = true;
fail_evar = fail;
- expand_evars = true }
+ expand_evars = true;
+ program_mode = false;
+}
let no_classes_no_fail_inference_flags = {
use_typeclasses = false;
solve_unification_constraints = true;
fail_evar = false;
- expand_evars = true }
+ expand_evars = true;
+ program_mode = false;
+}
let all_and_fail_flags = default_inference_flags true
let all_no_fail_flags = default_inference_flags false
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 59e6c00037..3c875e69d2 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -36,7 +36,8 @@ type inference_flags = {
use_typeclasses : bool;
solve_unification_constraints : bool;
fail_evar : bool;
- expand_evars : bool
+ expand_evars : bool;
+ program_mode : bool;
}
val default_inference_flags : bool -> inference_flags
@@ -101,7 +102,7 @@ val solve_remaining_evars : ?hook:inference_hook -> inference_flags ->
reporting an appropriate error message *)
val check_evars_are_solved :
- env -> ?initial:evar_map -> (* current map: *) evar_map -> unit
+ program_mode:bool -> env -> ?initial:evar_map -> (* current map: *) evar_map -> unit
(** [check_evars env initial_sigma extended_sigma c] fails if some
new unresolved evar remains in [c] *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e4d96da0a6..ac0b58b92b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1269,7 +1269,7 @@ let is_mimick_head sigma ts f =
let try_to_coerce env evd c cty tycon =
let j = make_judge c cty in
- let (evd',j') = inh_conv_coerce_rigid_to true env evd j tycon in
+ let (evd',j') = inh_conv_coerce_rigid_to ~program_mode:false true env evd j tycon in
let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in
let evd' = Evd.map_metas_fvalue (fun c -> nf_evar evd' c) evd' in
(evd',j'.uj_val)
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 23:00:46 +0000