diff options
53 files changed, 543 insertions, 538 deletions
diff --git a/CHANGES.md b/CHANGES.md index 1a0b53f84a..26573b9185 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -126,6 +126,10 @@ Vernacular commands class will have to be changed into `Instance foo : C := {}.` or `Instance foo : C. Proof. Qed.`. +- Option `Program Mode` now means that the `Program` attribute is enabled + for all commands that support it. In particular, it does not have any effect + on tactics anymore. May cause some incompatibilities. + Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: diff --git a/engine/evarutil.ml b/engine/evarutil.ml index db56d0628f..d70c009c6d 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -337,6 +337,7 @@ type naming_mode = | KeepUserNameAndRenameExistingEvenSectionNames | KeepExistingNames | FailIfConflict + | ProgramNaming let push_rel_decl_to_named_context ?(hypnaming=KeepUserNameAndRenameExistingButSectionNames) @@ -364,7 +365,7 @@ let push_rel_decl_to_named_context using this function. For now, we only attempt to preserve the old behaviour of Program, but ultimately, one should do something about this whole name generation problem. *) - if Flags.is_program_mode () then next_name_away na avoid + if hypnaming = ProgramNaming then next_name_away na avoid else (* id_of_name_using_hdchar only depends on the rel context which is empty here *) @@ -372,7 +373,8 @@ let push_rel_decl_to_named_context in match extract_if_neq id na with | Some id0 when hypnaming = KeepUserNameAndRenameExistingEvenSectionNames || - hypnaming = KeepUserNameAndRenameExistingButSectionNames && + (hypnaming = KeepUserNameAndRenameExistingButSectionNames || + hypnaming = ProgramNaming) && not (is_section_variable id0) -> (* spiwack: if [id<>id0], rather than introducing a new binding named [id], we will keep [id0] (the name given diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 0e67475778..23b240f1a0 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -38,6 +38,7 @@ type naming_mode = | KeepUserNameAndRenameExistingEvenSectionNames | KeepExistingNames | FailIfConflict + | ProgramNaming val new_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c8c38ffe05..24894fc9f5 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2328,36 +2328,38 @@ let interp_open_constr env sigma c = (* Not all evars expected to be resolved and computation of implicit args *) -let interp_constr_evars_gen_impls env sigma +let interp_constr_evars_gen_impls ?(program_mode=false) env sigma ?(impls=empty_internalization_env) expected_type c = let c = intern_gen expected_type ~impls env sigma c in let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in - let sigma, c = understand_tcc env sigma ~expected_type c in + let flags = { Pretyping.all_no_fail_flags with program_mode } in + let sigma, c = understand_tcc ~flags env sigma ~expected_type c in sigma, (c, imps) -let interp_constr_evars_impls env sigma ?(impls=empty_internalization_env) c = - interp_constr_evars_gen_impls env sigma ~impls WithoutTypeConstraint c +let interp_constr_evars_impls ?program_mode env sigma ?(impls=empty_internalization_env) c = + interp_constr_evars_gen_impls ?program_mode env sigma ~impls WithoutTypeConstraint c -let interp_casted_constr_evars_impls env evdref ?(impls=empty_internalization_env) c typ = - interp_constr_evars_gen_impls env evdref ~impls (OfType typ) c +let interp_casted_constr_evars_impls ?program_mode env evdref ?(impls=empty_internalization_env) c typ = + interp_constr_evars_gen_impls ?program_mode env evdref ~impls (OfType typ) c -let interp_type_evars_impls env sigma ?(impls=empty_internalization_env) c = - interp_constr_evars_gen_impls env sigma ~impls IsType c +let interp_type_evars_impls ?program_mode env sigma ?(impls=empty_internalization_env) c = + interp_constr_evars_gen_impls ?program_mode env sigma ~impls IsType c (* Not all evars expected to be resolved, with side-effect on evars *) -let interp_constr_evars_gen env sigma ?(impls=empty_internalization_env) expected_type c = +let interp_constr_evars_gen ?(program_mode=false) env sigma ?(impls=empty_internalization_env) expected_type c = let c = intern_gen expected_type ~impls env sigma c in - understand_tcc env sigma ~expected_type c + let flags = { Pretyping.all_no_fail_flags with program_mode } in + understand_tcc ~flags env sigma ~expected_type c -let interp_constr_evars env evdref ?(impls=empty_internalization_env) c = - interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c +let interp_constr_evars ?program_mode env evdref ?(impls=empty_internalization_env) c = + interp_constr_evars_gen ?program_mode env evdref WithoutTypeConstraint ~impls c -let interp_casted_constr_evars env sigma ?(impls=empty_internalization_env) c typ = - interp_constr_evars_gen env sigma ~impls (OfType typ) c +let interp_casted_constr_evars ?program_mode env sigma ?(impls=empty_internalization_env) c typ = + interp_constr_evars_gen ?program_mode env sigma ~impls (OfType typ) c -let interp_type_evars env sigma ?(impls=empty_internalization_env) c = - interp_constr_evars_gen env sigma IsType ~impls c +let interp_type_evars ?program_mode env sigma ?(impls=empty_internalization_env) c = + interp_constr_evars_gen ?program_mode env sigma IsType ~impls c (* Miscellaneous *) @@ -2419,8 +2421,9 @@ let intern_context global_level env impl_env binders = with InternalizationError (loc,e) -> user_err ?loc ~hdr:"internalize" (explain_internalization_error e) -let interp_glob_context_evars env sigma k bl = +let interp_glob_context_evars ?(program_mode=false) env sigma k bl = let open EConstr in + let flags = { Pretyping.all_no_fail_flags with program_mode } in let env, sigma, par, _, impls = List.fold_left (fun (env,sigma,params,n,impls) (na, k, b, t) -> @@ -2428,7 +2431,7 @@ let interp_glob_context_evars env sigma k bl = if Option.is_empty b then locate_if_hole ?loc:(loc_of_glob_constr t) na t else t in - let sigma, t = understand_tcc env sigma ~expected_type:IsType t' in + let sigma, t = understand_tcc ~flags env sigma ~expected_type:IsType t' in match b with None -> let d = LocalAssum (na,t) in @@ -2440,13 +2443,13 @@ let interp_glob_context_evars env sigma k bl = in (push_rel d env, sigma, d::params, succ n, impls) | Some b -> - let sigma, c = understand_tcc env sigma ~expected_type:(OfType t) b in + let sigma, c = understand_tcc ~flags env sigma ~expected_type:(OfType t) b in let d = LocalDef (na, c, t) in (push_rel d env, sigma, d::params, n, impls)) (env,sigma,[],k+1,[]) (List.rev bl) in sigma, ((env, par), impls) -let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params = +let interp_context_evars ?program_mode ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params = let int_env,bl = intern_context global_level env impl_env params in - let sigma, x = interp_glob_context_evars env sigma shift bl in + let sigma, x = interp_glob_context_evars ?program_mode env sigma shift bl in sigma, (int_env, x) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 61acd09d65..2d14a0d0a7 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -113,26 +113,26 @@ val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr (** Accepting unresolved evars *) -val interp_constr_evars : env -> evar_map -> +val interp_constr_evars : ?program_mode:bool -> env -> evar_map -> ?impls:internalization_env -> constr_expr -> evar_map * constr -val interp_casted_constr_evars : env -> evar_map -> +val interp_casted_constr_evars : ?program_mode:bool -> env -> evar_map -> ?impls:internalization_env -> constr_expr -> types -> evar_map * constr -val interp_type_evars : env -> evar_map -> +val interp_type_evars : ?program_mode:bool -> env -> evar_map -> ?impls:internalization_env -> constr_expr -> evar_map * types (** Accepting unresolved evars and giving back the manual implicit arguments *) -val interp_constr_evars_impls : env -> evar_map -> +val interp_constr_evars_impls : ?program_mode:bool -> env -> evar_map -> ?impls:internalization_env -> constr_expr -> evar_map * (constr * Impargs.manual_implicits) -val interp_casted_constr_evars_impls : env -> evar_map -> +val interp_casted_constr_evars_impls : ?program_mode:bool -> env -> evar_map -> ?impls:internalization_env -> constr_expr -> types -> evar_map * (constr * Impargs.manual_implicits) -val interp_type_evars_impls : env -> evar_map -> +val interp_type_evars_impls : ?program_mode:bool -> env -> evar_map -> ?impls:internalization_env -> constr_expr -> evar_map * (types * Impargs.manual_implicits) @@ -158,7 +158,7 @@ val interp_binder_evars : env -> evar_map -> Name.t -> constr_expr -> evar_map * (** Interpret contexts: returns extended env and context *) val interp_context_evars : - ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> + ?program_mode:bool -> ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> env -> evar_map -> local_binder_expr list -> evar_map * (internalization_env * ((env * rel_context) * Impargs.manual_implicits)) diff --git a/lib/flags.ml b/lib/flags.ml index 55bfa3cbde..29406ef275 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -107,12 +107,6 @@ let polymorphic_inductive_cumulativity = ref false let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity -(** [program_mode] tells that Program mode has been activated, either - globally via [Set Program] or locally via the Program command prefix. *) - -let program_mode = ref false -let is_program_mode () = !program_mode - let warn = ref true let make_warn flag = warn := flag; () let if_warn f x = if !warn then f x diff --git a/lib/flags.mli b/lib/flags.mli index 7336b9beaf..b9c5e20f47 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -77,10 +77,6 @@ val verbosely : ('a -> 'b) -> 'a -> 'b val if_silent : ('a -> unit) -> 'a -> unit val if_verbose : ('a -> unit) -> 'a -> unit -(* Miscellaneus flags for vernac *) -val program_mode : bool ref -val is_program_mode : unit -> bool - (** Global polymorphic inductive cumulativity flag. *) val make_polymorphic_inductive_cumulativity : bool -> unit val is_polymorphic_inductive_cumulativity : unit -> bool diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 6f9384941b..d06a241969 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -40,7 +40,7 @@ let start_deriving f suchthat lemma = let f_type = EConstr.Unsafe.to_constr f_type in let ef = EConstr.Unsafe.to_constr ef in let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in - let sigma, suchthat = Constrintern.interp_type_evars env' sigma suchthat in + let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in TCons ( env' , sigma , suchthat , (fun sigma _ -> TNil sigma)))))) in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d9b0330e2b..42dc66dcf4 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -166,7 +166,7 @@ let build_newrecursive let arityc = Constrexpr_ops.mkCProdN bl arityc in let arity,ctx = Constrintern.interp_type env0 sigma arityc in let evd = Evd.from_env env0 in - let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in + let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd bl in let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in let open Context.Named.Declaration in (EConstr.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls)) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 1b5286dce4..0c97f9f373 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1518,10 +1518,10 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let open CVars in let env = Global.env() in let evd = Evd.from_env env in - let evd, function_type = interp_type_evars env evd type_of_f in + let evd, function_type = interp_type_evars ~program_mode:false env evd type_of_f in let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) - let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in + let evd, ty = interp_type_evars ~program_mode:false env evd ~impls:rec_impls eq in let evd = Evd.minimize_universes evd in let equation_lemma_type = Reductionops.nf_betaiotazeta env evd (Evarutil.nf_evar evd ty) in let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 47f593ff3e..ffd8b71e5d 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -50,7 +50,8 @@ let with_delayed_uconstr ist c tac = Pretyping.use_typeclasses = false; solve_unification_constraints = true; fail_evar = false; - expand_evars = true + expand_evars = true; + program_mode = false; } in let c = Tacinterp.type_uconstr ~flags ist c in Tacticals.New.tclDELAYEDWITHHOLES false c tac @@ -344,7 +345,9 @@ let constr_flags () = { Pretyping.use_typeclasses = true; Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics (); Pretyping.fail_evar = false; - Pretyping.expand_evars = true } + Pretyping.expand_evars = true; + Pretyping.program_mode = false; +} let refine_tac ist simple with_classes c = Proofview.Goal.enter begin fun gl -> diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 7be8f67616..663537f3e8 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -56,7 +56,8 @@ let eval_uconstrs ist cs = Pretyping.use_typeclasses = false; solve_unification_constraints = true; fail_evar = false; - expand_evars = true + expand_evars = true; + program_mode = false; } in let map c env sigma = c env sigma in List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 3e7479903a..525ff7fd0f 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -544,7 +544,9 @@ let constr_flags () = { use_typeclasses = true; solve_unification_constraints = true; fail_evar = true; - expand_evars = true } + expand_evars = true; + program_mode = false; +} (* Interprets a constr; expects evars to be solved *) let interp_constr_gen kind ist env sigma c = @@ -558,19 +560,25 @@ let open_constr_use_classes_flags () = { use_typeclasses = true; solve_unification_constraints = true; fail_evar = false; - expand_evars = true } + expand_evars = true; + program_mode = false; +} let open_constr_no_classes_flags () = { use_typeclasses = false; solve_unification_constraints = true; fail_evar = false; - expand_evars = true } + expand_evars = true; + program_mode = false; +} let pure_open_constr_flags = { use_typeclasses = false; solve_unification_constraints = true; fail_evar = false; - expand_evars = false } + expand_evars = false; + program_mode = false; +} (* Interprets an open constr *) let interp_open_constr ?(expected_type=WithoutTypeConstraint) ?(flags=open_constr_no_classes_flags ()) ist env sigma c = diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index c3b9bde9b8..0961edb6cb 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -243,7 +243,9 @@ let interp_refine ist gl rc = Pretyping.use_typeclasses = true; solve_unification_constraints = true; fail_evar = false; - expand_evars = true } + expand_evars = true; + program_mode = false; + } in let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in (* ppdebug(lazy(str"sigma@interp_refine=" ++ pr_evar_map None sigma)); *) 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) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 1f1bdf4da7..9540d3de44 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -677,7 +677,7 @@ let define_with_type sigma env ev c = let t = Retyping.get_type_of env sigma ev in let ty = Retyping.get_type_of env sigma c in let j = Environ.make_judge c ty in - let (sigma, j) = Coercion.inh_conv_coerce_to true env sigma j t in + let (sigma, j) = Coercion.inh_conv_coerce_to ~program_mode:false true env sigma j t in let (ev, _) = destEvar sigma ev in let sigma = Evd.define ev j.Environ.uj_val sigma in sigma diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 6c4193c66b..1b2756f49f 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -53,7 +53,9 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = Pretyping.use_typeclasses = true; Pretyping.solve_unification_constraints = true; Pretyping.fail_evar = false; - Pretyping.expand_evars = true } in + Pretyping.expand_evars = true; + Pretyping.program_mode = false; + } in try Pretyping.understand_ltac flags env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc with e when CErrors.noncritical e -> diff --git a/proofs/refine.ml b/proofs/refine.ml index 1d796fece5..06e6b89df1 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -137,26 +137,6 @@ let refine ~typecheck f = in Proofview.Goal.enter (make_refine_enter ~typecheck f) -(** Useful definitions *) - -let with_type env evd c t = - let my_type = Retyping.get_type_of env evd c in - let j = Environ.make_judge c my_type in - let (evd,j') = - Coercion.inh_conv_coerce_to true env evd j t - in - evd , j'.Environ.uj_val - -let refine_casted ~typecheck f = Proofview.Goal.enter begin fun gl -> - let concl = Proofview.Goal.concl gl in - let env = Proofview.Goal.env gl in - let f h = - let (h, c) = f h in - with_type env h c concl - in - refine ~typecheck f -end - (** {7 solve_constraints} Ensure no remaining unification problems are left. Run at every "." by default. *) diff --git a/proofs/refine.mli b/proofs/refine.mli index 1af6463a02..55dafe521f 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -34,17 +34,6 @@ val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic -> Proofview.Goal.t -> 'a tactic (** The general version of refine. *) -(** {7 Helper functions} *) - -val with_type : Environ.env -> Evd.evar_map -> - EConstr.constr -> EConstr.types -> Evd.evar_map * EConstr.constr -(** [with_type env sigma c t] ensures that [c] is of type [t] - inserting a coercion if needed. *) - -val refine_casted : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic -(** Like {!refine} except the refined term is coerced to the conclusion of the - current goal. *) - (** {7 Unification constraint handling} *) val solve_constraints : unit tactic diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 42540af991..feb8e2a67f 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -56,6 +56,7 @@ let options_affecting_stm_scheduling = [ Attributes.universe_polymorphism_option_name; stm_allow_nested_proofs_option_name; Vernacentries.proof_mode_opt_name; + Attributes.program_mode_option_name; ] let classify_vernac e = diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 356b43ec14..48997163de 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -250,7 +250,7 @@ let add_inversion_lemma ~poly name env sigma t sort dep inv_op = let add_inversion_lemma_exn ~poly na com comsort bool tac = let env = Global.env () in let sigma = Evd.from_env env in - let sigma, c = Constrintern.interp_type_evars env sigma com in + let sigma, c = Constrintern.interp_type_evars ~program_mode:false env sigma com in let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in try add_inversion_lemma ~poly na env sigma c sort bool tac diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 070b2356e5..afa623741a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1155,7 +1155,9 @@ let tactic_infer_flags with_evar = { Pretyping.use_typeclasses = true; Pretyping.solve_unification_constraints = true; Pretyping.fail_evar = not with_evar; - Pretyping.expand_evars = true } + Pretyping.expand_evars = true; + Pretyping.program_mode = false; +} type evars_flag = bool (* true = pose evars false = fail on evars *) type rec_flag = bool (* true = recursive false = not recursive *) diff --git a/test-suite/bugs/closed/HoTT_coq_056.v b/test-suite/bugs/closed/HoTT_coq_056.v index b80e0bb0e4..e28314cada 100644 --- a/test-suite/bugs/closed/HoTT_coq_056.v +++ b/test-suite/bugs/closed/HoTT_coq_056.v @@ -82,7 +82,7 @@ Notation "F ^op" := (OppositeFunctor F) : functor_scope. Definition FunctorProduct' C D C' D' (F : Functor C D) (F' : Functor C' D') : Functor (C * C') (D * D') := admit. -Global Class FunctorApplicationInterpretable +Class FunctorApplicationInterpretable {C D} (F : Functor C D) {argsT : Type} (args : argsT) {T : Type} (rtn : T) diff --git a/test-suite/bugs/closed/HoTT_coq_061.v b/test-suite/bugs/closed/HoTT_coq_061.v index 19551dc92e..72bc04e05e 100644 --- a/test-suite/bugs/closed/HoTT_coq_061.v +++ b/test-suite/bugs/closed/HoTT_coq_061.v @@ -96,7 +96,7 @@ Definition NTWhiskerR C D E (F F' : Functor D E) (T : NaturalTransformation F F' := Build_NaturalTransformation (F o G) (F' o G) (fun c => T (G c)) admit. -Global Class NTC_Composable A B (a : A) (b : B) (T : Type) (term : T) := {}. +Class NTC_Composable A B (a : A) (b : B) (T : Type) (term : T) := {}. Definition NTC_Composable_term `{@NTC_Composable A B a b T term} := term. Notation "T 'o' U" diff --git a/test-suite/bugs/closed/HoTT_coq_120.v b/test-suite/bugs/closed/HoTT_coq_120.v index a80d075f69..cd6539b51c 100644 --- a/test-suite/bugs/closed/HoTT_coq_120.v +++ b/test-suite/bugs/closed/HoTT_coq_120.v @@ -89,7 +89,7 @@ Definition set_cat : PreCategory := @Build_PreCategory hSet (fun x y => forall _ : x, y)%core (fun _ _ _ f g x => f (g x))%core. -Local Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A. +Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A. Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0. Admitted. Definition hexists {X} (P:X->Type):Type:= minus1Trunc (sigT P). Definition isepi {X Y} `(f:X->Y) := forall Z: hSet, diff --git a/test-suite/bugs/closed/bug_3427.v b/test-suite/bugs/closed/bug_3427.v index 317efb0b32..f00d2fcf09 100644 --- a/test-suite/bugs/closed/bug_3427.v +++ b/test-suite/bugs/closed/bug_3427.v @@ -146,7 +146,7 @@ Section Univalence. := (equiv_path A B)^-1 f. End Univalence. -Local Inductive minus1Trunc (A :Type) : Type := +Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A. Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0. diff --git a/test-suite/bugs/closed/bug_7795.v b/test-suite/bugs/closed/bug_7795.v index 5db0f81cc5..5f9d42f5f7 100644 --- a/test-suite/bugs/closed/bug_7795.v +++ b/test-suite/bugs/closed/bug_7795.v @@ -52,6 +52,8 @@ Definition hh: false = true. Admitted. +Require Import Program. + Set Program Mode. (* removing this line prevents the bug *) Obligation Tactic := repeat t_base. diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 4f238f38e6..9b8c4efb37 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -125,11 +125,25 @@ let qualify_attribute qual (parser:'a attribute) : 'a attribute = let extra = if rem = [] then extra else (qual, VernacFlagList rem) :: extra in extra, v +(** [program_mode] tells that Program mode has been activated, either + globally via [Set Program] or locally via the Program command prefix. *) + +let program_mode_option_name = ["Program";"Mode"] +let program_mode = ref false + +let () = let open Goptions in + declare_bool_option + { optdepr = false; + optname = "use of the program extension"; + optkey = program_mode_option_name; + optread = (fun () -> !program_mode); + optwrite = (fun b -> program_mode:=b) } + let program_opt = bool_attribute ~name:"Program mode" ~on:"program" ~off:"noprogram" let program = program_opt >>= function | Some b -> return b - | None -> return (Flags.is_program_mode()) + | None -> return (!program_mode) let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global" diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 66e10f94cd..3cb4d69ca0 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -53,7 +53,7 @@ val template : bool option attribute val locality : bool option attribute val deprecation : deprecation option attribute -val program_opt : bool option attribute +val program_mode_option_name : string list (** For internal use when messing with the global option. *) val only_locality : vernac_flags -> bool option diff --git a/vernac/classes.ml b/vernac/classes.ml index dd49f09d35..ea434dbc4f 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -82,14 +82,14 @@ let mismatched_props env n m = Implicit_quantifiers.mismatched_ctx_inst_err env (* Declare everything in the parameters as implicit, and the class instance as well *) -let type_ctx_instance env sigma ctx inst subst = +let type_ctx_instance ~program_mode env sigma ctx inst subst = let open Vars in let rec aux (sigma, subst, instctx) l = function decl :: ctx -> let t' = substl subst (RelDecl.get_type decl) in let (sigma, c'), l = match decl with - | LocalAssum _ -> interp_casted_constr_evars env sigma (List.hd l) t', List.tl l + | LocalAssum _ -> interp_casted_constr_evars ~program_mode env sigma (List.hd l) t', List.tl l | LocalDef (_,b,_) -> (sigma, substl subst b), l in let d = RelDecl.get_name decl, Some c', t' in @@ -206,7 +206,7 @@ let do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode ct | None -> (if List.is_empty k.cl_props then Some (Inl subst) else None), sigma | Some (Inr term) -> - let sigma, c = interp_casted_constr_evars env' sigma term cty in + let sigma, c = interp_casted_constr_evars ~program_mode env' sigma term cty in Some (Inr (c, subst)), sigma | Some (Inl props) -> let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in @@ -237,7 +237,7 @@ let do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode ct unbound_method env' k.cl_impl (get_id n) | _ -> let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in - let sigma, res = type_ctx_instance (push_rel_context ctx' env') sigma kcl_props props subst in + let sigma, res = type_ctx_instance ~program_mode (push_rel_context ctx' env') sigma kcl_props props subst in Some (Inl res), sigma in let term, termtype = @@ -276,7 +276,7 @@ let do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode ct else CErrors.user_err Pp.(str "Unsolved obligations remaining."); id -let interp_instance_context env ctx ?(generalize=false) pl bk cl = +let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl = let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in let tclass, ids = match bk with @@ -295,8 +295,8 @@ let interp_instance_context env ctx ?(generalize=false) pl bk cl = if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) else tclass in - let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in - let sigma, (c', imps') = interp_type_evars_impls ~impls env' sigma tclass in + let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in + let sigma, (c', imps') = interp_type_evars_impls ~program_mode ~impls env' sigma tclass in let len = Context.Rel.nhyps ctx in let imps = imps @ Impargs.lift_implicits len imps' in let ctx', c = decompose_prod_assum sigma c' in @@ -324,7 +324,7 @@ let new_instance ?(global=false) ?(refine= !refine_instance) ~program_mode let env = Global.env() in let ({CAst.loc;v=instid}, pl) = instid in let sigma, k, u, cty, ctx', ctx, imps, subst, decl = - interp_instance_context env ~generalize ctx pl bk cl + interp_instance_context ~program_mode env ~generalize ctx pl bk cl in let id = match instid with @@ -337,11 +337,11 @@ let new_instance ?(global=false) ?(refine= !refine_instance) ~program_mode do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props -let declare_new_instance ?(global=false) poly ctx (instid, bk, cl) pri = +let declare_new_instance ?(global=false) ~program_mode poly ctx (instid, bk, cl) pri = let env = Global.env() in let ({CAst.loc;v=instid}, pl) = instid in let sigma, k, u, cty, ctx', ctx, imps, subst, decl = - interp_instance_context env ctx pl bk cl + interp_instance_context ~program_mode env ctx pl bk cl in do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst instid @@ -361,7 +361,7 @@ let named_of_rel_context l = let context poly l = let env = Global.env() in let sigma = Evd.from_env env in - let sigma, (_, ((env', fullctx), impls)) = interp_context_evars env sigma l in + let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in (* Note, we must use the normalized evar from now on! *) let sigma = Evd.minimize_universes sigma in let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in diff --git a/vernac/classes.mli b/vernac/classes.mli index 6f61da66cf..7e0ec42625 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -55,6 +55,7 @@ val new_instance : val declare_new_instance : ?global:bool (** Not global by default. *) -> + program_mode:bool -> Decl_kinds.polymorphic -> local_binder_expr list -> ident_decl * Decl_kinds.binding_kind * constr_expr -> diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 7301e1fff7..73d0be04df 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -84,8 +84,8 @@ match local with in (gr,inst,Lib.is_modtype_strict ()) -let interp_assumption sigma env impls c = - let sigma, (ty, impls) = interp_type_evars_impls env sigma ~impls c in +let interp_assumption ~program_mode sigma env impls c = + let sigma, (ty, impls) = interp_type_evars_impls ~program_mode env sigma ~impls c in sigma, (ty, impls) (* When monomorphic the universe constraints are declared with the first declaration only. *) @@ -131,7 +131,7 @@ let process_assumptions_udecls kind l = in udecl, List.map (fun (coe, (idl, c)) -> coe, (List.map fst idl, c)) l -let do_assumptions kind nl l = +let do_assumptions ~program_mode kind nl l = let open Context.Named.Declaration in let env = Global.env () in let udecl, l = process_assumptions_udecls kind l in @@ -147,7 +147,7 @@ let do_assumptions kind nl l = in (* We intepret all declarations in the same evar_map, i.e. as a telescope. *) let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) -> - let sigma,(t,imps) = interp_assumption sigma env ienv c in + let sigma,(t,imps) = interp_assumption ~program_mode sigma env ienv c in let env = EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (id,t)) idl) env in let ienv = List.fold_right (fun {CAst.v=id} ienv -> diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index c5bf3725a9..385ec33bea 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -17,7 +17,7 @@ open Decl_kinds (** {6 Parameters/Assumptions} *) -val do_assumptions : locality * polymorphic * assumption_object_kind -> +val do_assumptions : program_mode:bool -> locality * polymorphic * assumption_object_kind -> Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list -> bool (************************************************************************) diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 79d45880fc..5e74114a86 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -41,26 +41,26 @@ let check_imps ~impsty ~impsbody = in if not b then warn_implicits_in_term () -let interp_definition pl bl poly red_option c ctypopt = +let interp_definition ~program_mode pl bl poly red_option c ctypopt = let open EConstr in let env = Global.env() in (* Explicitly bound universes and constraints *) let evd, decl = Constrexpr_ops.interp_univ_decl_opt env pl in (* Build the parameters *) - let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars env evd bl in + let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars ~program_mode env evd bl in (* Build the type *) let evd, tyopt = Option.fold_left_map - (interp_type_evars_impls ~impls env_bl) + (interp_type_evars_impls ~program_mode ~impls env_bl) evd ctypopt in (* Build the body, and merge implicits from parameters and from type/body *) let evd, c, imps, tyopt = match tyopt with | None -> - let evd, (c, impsbody) = interp_constr_evars_impls ~impls env_bl evd c in + let evd, (c, impsbody) = interp_constr_evars_impls ~program_mode ~impls env_bl evd c in evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsbody, None | Some (ty, impsty) -> - let evd, (c, impsbody) = interp_casted_constr_evars_impls ~impls env_bl evd c ty in + let evd, (c, impsbody) = interp_casted_constr_evars_impls ~program_mode ~impls env_bl evd c ty in check_imps ~impsty ~impsbody; evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty in @@ -85,14 +85,14 @@ let interp_definition pl bl poly red_option c ctypopt = let ce = definition_entry ?types:tyopt ~univs:uctx c in (ce, evd, decl, imps) -let check_definition (ce, evd, _, imps) = +let check_definition ~program_mode (ce, evd, _, imps) = let env = Global.env () in - check_evars_are_solved env evd; + check_evars_are_solved ~program_mode env evd; ce let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt = let (ce, evd, univdecl, imps as def) = - interp_definition univdecl bl (pi2 k) red_option c ctypopt + interp_definition ~program_mode univdecl bl (pi2 k) red_option c ctypopt in if program_mode then let env = Global.env () in @@ -111,5 +111,5 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt = let univ_hook = Obligations.mk_univ_hook (fun _ _ l r -> Lemmas.call_hook ?hook l r) in ignore(Obligations.add_definition ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~univ_hook obls) - else let ce = check_definition def in + else let ce = check_definition ~program_mode def in ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps ?hook) diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 0ac5762f71..9cb6190fcc 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -27,7 +27,7 @@ val do_definition : program_mode:bool -> (************************************************************************) (** Not used anywhere. *) -val interp_definition : +val interp_definition : program_mode:bool -> universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * UState.universe_decl * Impargs.manual_implicits diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 77227b64e6..5229d9e8e8 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -116,21 +116,23 @@ type structured_fixpoint_expr = { fix_type : constr_expr } -let interp_fix_context ~cofix env sigma fix = +let interp_fix_context ~program_mode ~cofix env sigma fix = let before, after = if not cofix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in - let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars env sigma before in - let sigma, (impl_env', ((env'', ctx'), imps')) = interp_context_evars ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after in + let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma before in + let sigma, (impl_env', ((env'', ctx'), imps')) = + interp_context_evars ~program_mode ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after + in let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot) -let interp_fix_ccl sigma impls (env,_) fix = - interp_type_evars_impls ~impls env sigma fix.fix_type +let interp_fix_ccl ~program_mode sigma impls (env,_) fix = + interp_type_evars_impls ~program_mode ~impls env sigma fix.fix_type -let interp_fix_body env_rec sigma impls (_,ctx) fix ccl = +let interp_fix_body ~program_mode env_rec sigma impls (_,ctx) fix ccl = let open EConstr in Option.cata (fun body -> let env = push_rel_context ctx env_rec in - let sigma, body = interp_casted_constr_evars env sigma ~impls body ccl in + let sigma, body = interp_casted_constr_evars ~program_mode env sigma ~impls body ccl in sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.fix_body let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx @@ -184,11 +186,11 @@ let interp_recursive ~program_mode ~cofix fixl notations = let sigma, decl = interp_univ_decl_opt env all_universes in let sigma, (fixctxs, fiximppairs, fixannots) = on_snd List.split3 @@ - List.fold_left_map (fun sigma -> interp_fix_context env sigma ~cofix) sigma fixl in + List.fold_left_map (fun sigma -> interp_fix_context ~program_mode env sigma ~cofix) sigma fixl in let fixctximpenvs, fixctximps = List.split fiximppairs in let sigma, (fixccls,fixcclimps) = on_snd List.split @@ - List.fold_left3_map interp_fix_ccl sigma fixctximpenvs fixctxs fixl in + List.fold_left3_map (interp_fix_ccl ~program_mode) sigma fixctximpenvs fixctxs fixl in let fixtypes = List.map2 build_fix_type fixctxs fixccls in let fixtypes = List.map (fun c -> nf_evar sigma c) fixtypes in let fiximps = List.map3 @@ -220,7 +222,7 @@ let interp_recursive ~program_mode ~cofix fixl notations = Metasyntax.with_syntax_protection (fun () -> List.iter (Metasyntax.set_notation_for_interpretation env_rec impls) notations; List.fold_left4_map - (fun sigma fixctximpenv -> interp_fix_body env_rec sigma (Id.Map.fold Id.Map.add fixctximpenv impls)) + (fun sigma fixctximpenv -> interp_fix_body ~program_mode env_rec sigma (Id.Map.fold Id.Map.add fixctximpenv impls)) sigma fixctximpenvs fixctxs fixl fixccls) () in @@ -239,7 +241,7 @@ let check_recursive isfix env evd (fixnames,fixdefs,_) = end let ground_fixpoint env evd (fixnames,fixdefs,fixtypes) = - check_evars_are_solved env evd; + check_evars_are_solved ~program_mode:false env evd; let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr evd) c) fixdefs in let fixtypes = List.map EConstr.(to_constr evd) fixtypes in Evd.evar_universe_context evd, (fixnames,fixdefs,fixtypes) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index afee2a5868..68ad276113 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -162,7 +162,7 @@ let interp_cstrs env sigma impls mldata arity ind = let sigma, (ctyps'', cimpls) = on_snd List.split @@ List.fold_left_map (fun sigma l -> - interp_type_evars_impls env sigma ~impls l) sigma ctyps' in + interp_type_evars_impls ~program_mode:false env sigma ~impls l) sigma ctyps' in sigma, (cnames, ctyps'', cimpls) let sign_level env evd sign = @@ -358,9 +358,9 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not then user_err (str "Inductives with uniform parameters may not have attached notations."); let sigma, udecl = interp_univ_decl_opt env0 udecl in let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) = - interp_context_evars env0 sigma uparamsl in + interp_context_evars ~program_mode:false env0 sigma uparamsl in let sigma, (impls, ((env_params, ctx_params), userimpls)) = - interp_context_evars ~impl_env:uimpls env_uparams sigma paramsl + interp_context_evars ~program_mode:false ~impl_env:uimpls env_uparams sigma paramsl in let indnames = List.map (fun ind -> ind.ind_name) indl in diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index edce8e255c..a30313d37c 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -91,17 +91,17 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = Coqlib.check_required_library ["Coq";"Program";"Wf"]; let env = Global.env() in let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in - let sigma, (_, ((env', binders_rel), impls)) = interp_context_evars env sigma bl in + let sigma, (_, ((env', binders_rel), impls)) = interp_context_evars ~program_mode:true env sigma bl in let len = List.length binders_rel in let top_env = push_rel_context binders_rel env in - let sigma, top_arity = interp_type_evars top_env sigma arityc in + let sigma, top_arity = interp_type_evars ~program_mode:true top_env sigma arityc in let full_arity = it_mkProd_or_LetIn top_arity binders_rel in let sigma, argtyp, letbinders, make = telescope sigma binders_rel in let argname = Id.of_string "recarg" in let arg = LocalAssum (Name argname, argtyp) in let binders = letbinders @ [arg] in let binders_env = push_rel_context binders_rel env in - let sigma, (rel, _) = interp_constr_evars_impls env sigma r in + let sigma, (rel, _) = interp_constr_evars_impls ~program_mode:true env sigma r in let relty = Typing.unsafe_type_of env sigma rel in let relargty = let error () = @@ -117,7 +117,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = | _, _ -> error () with e when CErrors.noncritical e -> error () in - let sigma, measure = interp_casted_constr_evars binders_env sigma measure relargty in + let sigma, measure = interp_casted_constr_evars ~program_mode:true binders_env sigma measure relargty in let sigma, wf_rel, wf_rel_fun, measure_fn = let measure_body, measure = it_mkLambda_or_LetIn measure letbinders, @@ -176,7 +176,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let newimpls = Id.Map.singleton recname (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))], scopes @ [None]) in - interp_casted_constr_evars (push_rel_context ctx env) sigma + interp_casted_constr_evars ~program_mode:true (push_rel_context ctx env) sigma ~impls:newimpls body (lift 1 top_arity) in let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 41057f8ab2..361ed1a737 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -57,7 +57,7 @@ let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t let check_definition_evars ~allow_evars sigma = let env = Global.env () in - if not allow_evars then Pretyping.check_evars_are_solved env sigma + if not allow_evars then Pretyping.check_evars_are_solved ~program_mode:false env sigma let prepare_definition ~allow_evars ?opaque ?inline ~poly sigma udecl ~types ~body = check_definition_evars ~allow_evars sigma; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 0dfbba0e83..4635883dc2 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -417,14 +417,14 @@ let start_proof_with_initialization ?hook kind sigma decl recguard thms snl = | None -> p,(true,[]) | Some tac -> Proof.run_tactic Global.(env ()) tac p)) -let start_proof_com ?inference_hook ?hook kind thms = +let start_proof_com ~program_mode ?inference_hook ?hook kind thms = let env0 = Global.env () in let decl = fst (List.hd thms) in let evd, decl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) -> - let evd, (impls, ((env, ctx), imps)) = interp_context_evars env0 evd bl in - let evd, (t', imps') = interp_type_evars_impls ~impls env evd t in - let flags = all_and_fail_flags in + let evd, (impls, ((env, ctx), imps)) = interp_context_evars ~program_mode env0 evd bl in + let evd, (t', imps') = interp_type_evars_impls ~program_mode ~impls env evd t in + let flags = { all_and_fail_flags with program_mode } in let hook = inference_hook in let evd = solve_remaining_evars ?hook flags env evd in let ids = List.map RelDecl.get_name ctx in diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 3ac12d3b0b..a9a10a6e38 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -31,7 +31,7 @@ val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.eva ?univ_hook:(UState.t option -> declaration_hook) -> EConstr.types -> unit val start_proof_com : - ?inference_hook:Pretyping.inference_hook -> + program_mode:bool -> ?inference_hook:Pretyping.inference_hook -> ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list -> unit diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 6642d04c98..6014452107 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -1197,15 +1197,7 @@ let next_obligation n tac = in solve_obligation prg i tac -let init_program () = +let check_program_libraries () = Coqlib.check_required_library Coqlib.datatypes_module_name; Coqlib.check_required_library ["Coq";"Init";"Specif"]; Coqlib.check_required_library ["Coq";"Program";"Tactics"] - -let set_program_mode c = - if c then - if !Flags.program_mode then () - else begin - init_program (); - Flags.program_mode := true; - end diff --git a/vernac/obligations.mli b/vernac/obligations.mli index c670e3a3b5..4eef668f56 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -110,7 +110,7 @@ exception NoObligations of Names.Id.t option val explain_no_obligations : Names.Id.t option -> Pp.t -val set_program_mode : bool -> unit +val check_program_libraries : unit -> unit type program_info val program_tcc_summary_tag : program_info Id.Map.t Summary.Dyn.tag diff --git a/vernac/record.ml b/vernac/record.ml index 1b7b828f47..247e0790d7 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -65,10 +65,10 @@ let () = let interp_fields_evars env sigma impls_env nots l = List.fold_left2 (fun (env, sigma, uimpls, params, impls) no ({CAst.loc;v=i}, b, t) -> - let sigma, (t', impl) = interp_type_evars_impls env sigma ~impls t in + let sigma, (t', impl) = interp_type_evars_impls ~program_mode:false env sigma ~impls t in let sigma, b' = Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@ - interp_casted_constr_evars_impls env sigma ~impls x t') (sigma,None) b in + interp_casted_constr_evars_impls ~program_mode:false env sigma ~impls x t') (sigma,None) b in let impls = match i with | Anonymous -> impls @@ -116,14 +116,14 @@ let typecheck_params_and_fields finite def poly pl ps records = | CLocalPattern {CAst.loc} -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")) ps in - let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars env0 sigma ps in + let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars ~program_mode:false env0 sigma ps in let fold (sigma, template) (_, t, _, _) = match t with | Some t -> let env = EConstr.push_rel_context newps env0 in let poly = match t with | { CAst.v = CSort (Glob_term.GType []) } -> true | _ -> false in - let sigma, s = interp_type_evars env sigma ~impls:empty_internalization_env t in + let sigma, s = interp_type_evars ~program_mode:false env sigma ~impls:empty_internalization_env t in let sred = Reductionops.whd_allnolet env sigma s in (match EConstr.kind sigma sred with | Sort s' -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7611355100..eb263757e2 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -514,9 +514,9 @@ let () = (***********) (* Gallina *) -let start_proof_and_print ?hook k l = +let start_proof_and_print ~program_mode ?hook k l = let inference_hook = - if Flags.is_program_mode () then + if program_mode then let hook env sigma ev = let tac = !Obligations.default_tactic in let evi = Evd.find sigma ev in @@ -536,7 +536,7 @@ let start_proof_and_print ?hook k l = in Some hook else None in - start_proof_com ?inference_hook ?hook k l + start_proof_com ~program_mode ?inference_hook ?hook k l let vernac_definition_hook p = function | Coercion -> @@ -549,7 +549,6 @@ let vernac_definition_hook p = function let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def = let open DefAttributes in - let atts = parse atts in let local = enforce_locality_exp atts.locality discharge in let hook = vernac_definition_hook atts.polymorphic kind in let () = @@ -560,7 +559,7 @@ let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def = | Discharge -> Dumpglob.dump_definition lid true "var" | Local | Global -> Dumpglob.dump_definition lid false "def" in - let program_mode = Flags.is_program_mode () in + let program_mode = atts.program in let name = match id with | Anonymous -> fresh_name_for_anonymous_theorem () @@ -568,7 +567,7 @@ let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def = in (match def with | ProveBody (bl,t) -> (* local binders, typ *) - start_proof_and_print (local, atts.polymorphic, DefinitionBody kind) + start_proof_and_print ~program_mode (local, atts.polymorphic, DefinitionBody kind) ?hook [(CAst.make ?loc name, pl), (bl, t)] | DefineBody (bl,red_option,c,typ_opt) -> let red_option = match red_option with @@ -581,11 +580,10 @@ let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def = let vernac_start_proof ~atts kind l = let open DefAttributes in - let atts = parse atts in let local = enforce_locality_exp atts.locality NoDischarge in if Dumpglob.dump () then List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l; - start_proof_and_print (local, atts.polymorphic, Proof kind) l + start_proof_and_print ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l let vernac_end_proof ?proof = function | Admitted -> save_proof ?proof Admitted @@ -600,7 +598,6 @@ let vernac_exact_proof c = let vernac_assumption ~atts discharge kind l nl = let open DefAttributes in - let atts = parse atts in let local = enforce_locality_exp atts.locality discharge in let global = local == Global in let kind = local, atts.polymorphic, kind in @@ -609,7 +606,7 @@ let vernac_assumption ~atts discharge kind l nl = List.iter (fun (lid, _) -> if global then Dumpglob.dump_definition lid false "ax" else Dumpglob.dump_definition lid true "var") idl) l; - let status = ComAssumption.do_assumptions kind nl l in + let status = ComAssumption.do_assumptions ~program_mode:atts.program kind nl l in if not status then Feedback.feedback Feedback.AddedAxiom let should_treat_as_cumulative cum poly = @@ -675,9 +672,7 @@ let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) = indicates whether the type is inductive, co-inductive or neither. *) let vernac_inductive ~atts cum lo finite indl = - let open DefAttributes in - let atts, template = Attributes.(parse_with_extra template atts) in - let atts = parse atts in + let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in let open Pp in let udecl, indl = extract_inductive_udecl indl in if Dumpglob.dump () then @@ -708,7 +703,7 @@ let vernac_inductive ~atts cum lo finite indl = let (coe, (lid, ce)) = l in let coe' = if coe then Some true else None in let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in - vernac_record ~template udecl cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]] + vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]] else if List.for_all is_record indl then (* Mutual record case *) let check_kind ((_, _, _, kind, _), _) = match kind with @@ -731,7 +726,7 @@ let vernac_inductive ~atts cum lo finite indl = let ((_, _, _, kind, _), _) = List.hd indl in let kind = match kind with Class _ -> Class false | _ -> kind in let recordl = List.map unpack indl in - vernac_record ~template udecl cum kind atts.polymorphic finite recordl + vernac_record ~template udecl cum kind poly finite recordl else if List.for_all is_constructor indl then (* Mutual inductive case *) let check_kind ((_, _, _, kind, _), _) = match kind with @@ -755,9 +750,9 @@ let vernac_inductive ~atts cum lo finite indl = | RecordDecl _ -> assert false (* ruled out above *) in let indl = List.map unpack indl in - let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in + let is_cumulative = should_treat_as_cumulative cum poly in let uniform = should_treat_as_uniform () in - ComInductive.do_mutual_inductive ~template udecl indl is_cumulative atts.polymorphic lo ~uniform finite + ComInductive.do_mutual_inductive ~template udecl indl is_cumulative poly lo ~uniform finite else user_err (str "Mixed record-inductive definitions are not allowed") (* @@ -773,12 +768,11 @@ let vernac_inductive ~atts cum lo finite indl = let vernac_fixpoint ~atts discharge l = let open DefAttributes in - let atts = parse atts in let local = enforce_locality_exp atts.locality discharge in if Dumpglob.dump () then List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; (* XXX: Switch to the attribute system and match on ~atts *) - let do_fixpoint = if Flags.is_program_mode () then + let do_fixpoint = if atts.program then ComProgramFixpoint.do_fixpoint else ComFixpoint.do_fixpoint @@ -787,11 +781,10 @@ let vernac_fixpoint ~atts discharge l = let vernac_cofixpoint ~atts discharge l = let open DefAttributes in - let atts = parse atts in let local = enforce_locality_exp atts.locality discharge in if Dumpglob.dump () then List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; - let do_cofixpoint = if Flags.is_program_mode () then + let do_cofixpoint = if atts.program then ComProgramFixpoint.do_cofixpoint else ComFixpoint.do_cofixpoint @@ -1029,18 +1022,16 @@ let vernac_identity_coercion ~atts id qids qidt = let vernac_instance ~atts sup inst props pri = let open DefAttributes in - let atts = parse atts in let global = not (make_section_locality atts.locality) in Dumpglob.dump_constraint (fst (pi1 inst)) false "inst"; - let program_mode = Flags.is_program_mode () in + let program_mode = atts.program in ignore(Classes.new_instance ~program_mode ~global atts.polymorphic sup inst props pri) let vernac_declare_instance ~atts sup inst pri = let open DefAttributes in - let atts = parse atts in let global = not (make_section_locality atts.locality) in Dumpglob.dump_definition (fst (pi1 inst)) false "inst"; - Classes.declare_new_instance ~global atts.polymorphic sup inst pri + Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic sup inst pri let vernac_context ~poly l = if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom @@ -1575,14 +1566,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "use of the program extension"; - optkey = ["Program";"Mode"]; - optread = (fun () -> !Flags.program_mode); - optwrite = (fun b -> Flags.program_mode:=b) } - -let () = - declare_bool_option - { optdepr = false; optname = "Polymorphic inductive cumulativity"; optkey = ["Polymorphic"; "Inductive"; "Cumulativity"]; optread = Flags.is_polymorphic_inductive_cumulativity; @@ -2189,6 +2172,11 @@ let with_module_locality ~atts f = let module_local = make_module_locality local in f ~module_local +let with_def_attributes ~atts f = + let atts = DefAttributes.parse atts in + if atts.DefAttributes.program then Obligations.check_program_libraries (); + f ~atts + (* "locality" is the prefix "Local" attribute, while the "local" component * is the outdated/deprecated "Local" attribute of some vernacular commands * still parsed as the obsolete_locality grammar entry for retrocompatibility. @@ -2232,15 +2220,15 @@ let interp ?proof ~atts ~st c = (* Gallina *) | VernacDefinition ((discharge,kind),lid,d) -> - vernac_definition ~atts discharge kind lid d - | VernacStartTheoremProof (k,l) -> vernac_start_proof ~atts k l + with_def_attributes ~atts vernac_definition discharge kind lid d + | VernacStartTheoremProof (k,l) -> with_def_attributes vernac_start_proof ~atts k l | VernacEndProof e -> unsupported_attributes atts; vernac_end_proof ?proof e | VernacExactProof c -> unsupported_attributes atts; vernac_exact_proof c | VernacAssumption ((discharge,kind),nl,l) -> - vernac_assumption ~atts discharge kind l nl + with_def_attributes vernac_assumption ~atts discharge kind l nl | VernacInductive (cum, priv, finite, l) -> vernac_inductive ~atts cum priv finite l - | VernacFixpoint (discharge, l) -> vernac_fixpoint ~atts discharge l - | VernacCoFixpoint (discharge, l) -> vernac_cofixpoint ~atts discharge l + | VernacFixpoint (discharge, l) -> with_def_attributes vernac_fixpoint ~atts discharge l + | VernacCoFixpoint (discharge, l) -> with_def_attributes vernac_cofixpoint ~atts discharge l | VernacScheme l -> unsupported_attributes atts; vernac_scheme l | VernacCombinedScheme (id, l) -> unsupported_attributes atts; vernac_combined_scheme id l | VernacUniverse l -> vernac_universe ~poly:(only_polymorphism atts) l @@ -2271,9 +2259,9 @@ let interp ?proof ~atts ~st c = (* Type classes *) | VernacInstance (sup, inst, props, info) -> - vernac_instance ~atts sup inst props info + with_def_attributes vernac_instance ~atts sup inst props info | VernacDeclareInstance (sup, inst, info) -> - vernac_declare_instance ~atts sup inst info + with_def_attributes vernac_declare_instance ~atts sup inst info | VernacContext sup -> vernac_context ~poly:(only_polymorphism atts) sup | VernacExistingInstance insts -> with_section_locality ~atts vernac_existing_instance insts | VernacExistingClass id -> unsupported_attributes atts; vernac_existing_class id @@ -2423,7 +2411,6 @@ let with_fail st b f = end let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} = - let orig_program_mode = Flags.is_program_mode () in let rec control = function | VernacExpr (atts, v) -> aux ~atts v @@ -2445,21 +2432,13 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} = vernac_load control fname | c -> - let program = let open Attributes in - parse_drop_extra program_opt atts - in (* NB: we keep polymorphism and program in the attributes, we're just parsing them to do our option magic. *) - Option.iter Obligations.set_program_mode program; try vernac_timeout begin fun () -> if verbosely then Flags.verbosely (interp ?proof ~atts ~st) c else Flags.silently (interp ?proof ~atts ~st) c; - (* If the command is `(Un)Set Program Mode` or `(Un)Set Universe Polymorphism`, - we should not restore the previous state of the flag... *) - if Option.has_some program then - Flags.program_mode := orig_program_mode; end with | reraise when @@ -2470,7 +2449,6 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} = let e = CErrors.push reraise in let e = locate_if_not_already ?loc e in let () = restore_timeout () in - Flags.program_mode := orig_program_mode; iraise e in if verbosely |