diff options
Diffstat (limited to 'vernac')
36 files changed, 1085 insertions, 879 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 0c9b9c7255..f3ad324aa5 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -113,8 +113,8 @@ let mkFullInd (ind,u) n = else mkIndU (ind,u) let check_bool_is_defined () = - try let _ = Typeops.type_of_global_in_context (Global.env ()) Coqlib.(lib_ref "core.bool.type") in () - with e when CErrors.noncritical e -> raise (UndefinedCst "bool") + if not (Coqlib.has_ref "core.bool.type") + then raise (UndefinedCst "bool") let check_no_indices mib = if Array.exists (fun mip -> mip.mind_nrealargs <> 0) mib.mind_packets then @@ -236,10 +236,11 @@ let build_beq_scheme mode kn = (* Needs Hints, see test suite *) let eq_lbl = Label.make ("eq_" ^ Label.to_string (Constant.label kn)) in let kneq = Constant.change_label kn eq_lbl in - try let _ = Environ.constant_opt_value_in env (kneq, u) in + if Environ.mem_constant kneq env then + let _ = Environ.constant_opt_value_in env (kneq, u) in Term.applist (mkConst kneq,a), Evd.empty_side_effects - with Not_found -> raise (ParameterWithoutEquality (GlobRef.ConstRef kn))) + else raise (ParameterWithoutEquality (GlobRef.ConstRef kn))) | Proj _ -> raise (EqUnknown "projection") | Construct _ -> raise (EqUnknown "constructor") | Case _ -> raise (EqUnknown "match") @@ -373,7 +374,7 @@ so from Ai we can find the correct eq_Ai bl_ai or lb_ai let do_replace_lb mode lb_scheme_key aavoid narg p q = let open EConstr in let avoid = Array.of_list aavoid in - let do_arg sigma hd v offset = + let do_arg env sigma hd v offset = match kind sigma v with | Var s -> let x = narg*offset in @@ -390,7 +391,9 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = Parameter (see example "J" in test file SchemeEquality.v) *) let lbl = Label.to_string (Constant.label cst) in let newlbl = if Int.equal offset 1 then ("eq_" ^ lbl) else (lbl ^ "_lb") in - mkConst (Constant.change_label cst (Label.make newlbl)) + let newcst = Constant.change_label cst (Label.make newlbl) in + if Environ.mem_constant newcst env then mkConst newcst + else raise (ConstructorWithNonParametricInductiveType (fst hd)) | _ -> raise (ConstructorWithNonParametricInductiveType (fst hd)) in @@ -419,8 +422,8 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = Proofview.tclEVARMAP >>= fun sigma -> let lb_args = Array.append (Array.append v - (Array.Smart.map (fun x -> do_arg sigma u x 1) v)) - (Array.Smart.map (fun x -> do_arg sigma u x 2) v) + (Array.Smart.map (fun x -> do_arg env sigma u x 1) v)) + (Array.Smart.map (fun x -> do_arg env sigma u x 2) v) in let app = if Array.is_empty lb_args then lb_type_of_p else mkApp (lb_type_of_p,lb_args) in @@ -433,7 +436,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = let open EConstr in let avoid = Array.of_list aavoid in - let do_arg sigma hd v offset = + let do_arg env sigma hd v offset = match kind sigma v with | Var s -> let x = narg*offset in @@ -450,7 +453,9 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = Parameter (see example "J" in test file SchemeEquality.v) *) let lbl = Label.to_string (Constant.label cst) in let newlbl = if Int.equal offset 1 then ("eq_" ^ lbl) else (lbl ^ "_bl") in - mkConst (Constant.change_label cst (Label.make newlbl)) + let newcst = Constant.change_label cst (Label.make newlbl) in + if Environ.mem_constant newcst env then mkConst newcst + else raise (ConstructorWithNonParametricInductiveType (fst hd)) | _ -> raise (ConstructorWithNonParametricInductiveType (fst hd)) in @@ -487,8 +492,8 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = in let bl_args = Array.append (Array.append v - (Array.Smart.map (fun x -> do_arg sigma u x 1) v)) - (Array.Smart.map (fun x -> do_arg sigma u x 2) v ) + (Array.Smart.map (fun x -> do_arg env sigma u x 1) v)) + (Array.Smart.map (fun x -> do_arg env sigma u x 2) v ) in let app = if Array.is_empty bl_args then bl_t1 else mkApp (bl_t1,bl_args) @@ -837,8 +842,8 @@ let _ = lb_scheme_kind_aux := fun () -> lb_scheme_kind (* Decidable equality *) let check_not_is_defined () = - try ignore (Coqlib.lib_ref "core.not.type") - with Not_found -> raise (UndefinedCst "not") + if not (Coqlib.has_ref "core.not.type") + then raise (UndefinedCst "not") (* {n=m}+{n<>m} part *) let compute_dec_goal ind lnamesparrec nparrec = diff --git a/vernac/classes.ml b/vernac/classes.ml index dafd1cc5e4..3d38713e09 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -304,22 +304,19 @@ let id_of_class cl = mip.(0).Declarations.mind_typename | _ -> assert false -let instance_hook info global imps ?hook cst = - Impargs.maybe_declare_manual_implicits false cst imps; +let instance_hook info global ?hook cst = let info = intern_info info in let env = Global.env () in let sigma = Evd.from_env env in declare_instance env sigma (Some info) (not global) cst; (match hook with Some h -> h cst | None -> ()) -let declare_instance_constant info global imps ?hook name udecl poly sigma term termtype = +let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in - let sigma, entry = DeclareDef.prepare_definition - ~allow_evars:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in - let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in - Declare.definition_message name; - DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma); - instance_hook info global imps ?hook (GlobRef.ConstRef kn) + let scope = DeclareDef.Global Declare.ImportDefaultBehavior in + let kn = DeclareDef.declare_definition ~name ~kind ~scope ~impargs + ~opaque:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in + instance_hook info global ?hook kn let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name = let subst = List.fold_left2 @@ -328,30 +325,31 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst in let (_, ty_constr) = instance_constructor (k,u) subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma ~udecl ~types:termtype in + let sigma, entry = DeclareDef.prepare_parameter ~poly sigma ~udecl ~types:termtype in let cst = Declare.declare_constant ~name ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma); - instance_hook pri global impargs (GlobRef.ConstRef cst) + let cst = (GlobRef.ConstRef cst) in + Impargs.maybe_declare_manual_implicits false cst impargs; + instance_hook pri global cst -let declare_instance_program env sigma ~global ~poly name pri imps udecl term termtype = +let declare_instance_program env sigma ~global ~poly name pri impargs udecl term termtype = let hook { DeclareDef.Hook.S.scope; dref; _ } = let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in - Impargs.declare_manual_implicits false dref imps; let pri = intern_info pri in let env = Global.env () in let sigma = Evd.from_env env in declare_instance env sigma (Some pri) (not global) (GlobRef.ConstRef cst) in - let obls, _, term, typ = Obligations.eterm_obligations env name sigma 0 term termtype in + let obls, _, term, typ = RetrieveObl.retrieve_obligations env name sigma 0 term termtype in let hook = DeclareDef.Hook.make hook in let uctx = Evd.evar_universe_context sigma in let scope, kind = DeclareDef.Global Declare.ImportDefaultBehavior, Decls.Instance in let _ : DeclareObl.progress = - Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook typ ~uctx obls + Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls in () -let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype = +let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl ids term termtype = (* spiwack: it is hard to reorder the actions to do the pretyping after the proof has opened. As a consequence, we use the low-level primitives to code @@ -359,12 +357,12 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t let gls = List.rev (Evd.future_goals sigma) in let sigma = Evd.reset_future_goals sigma in let kind = Decls.(IsDefinition Instance) in - let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global imps ?hook dref)) in + let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in let info = Lemmas.Info.make ~hook ~kind () in (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails! This is due to a bug in proof_global :( *) let termtype = Evarutil.nf_evar sigma termtype in - let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma termtype in + let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info ~impargs sigma termtype in (* spiwack: I don't know what to do with the status here. *) let lemma = match term with @@ -516,7 +514,8 @@ let interp_instance_context ~program_mode env ctx ~generalize pl tclass = else 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 flags = Pretyping.{ all_no_fail_flags with program_mode } in + let sigma, (c', imps') = interp_type_evars_impls ~flags ~impls env' sigma tclass in let imps = imps @ imps' in let ctx', c = decompose_prod_assum sigma c' in let ctx'' = ctx' @ ctx in diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index dc9c8e2d3c..1e2e2e53e2 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -70,7 +70,8 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name (gr,inst) let interp_assumption ~program_mode sigma env impls c = - let sigma, (ty, impls) = interp_type_evars_impls ~program_mode env sigma ~impls c in + let flags = { Pretyping.all_no_fail_flags with program_mode } in + let sigma, (ty, impls) = interp_type_evars_impls ~flags env sigma ~impls c in sigma, (ty, impls) (* When monomorphic the universe constraints and universe names are @@ -203,8 +204,12 @@ let context_insection sigma ~poly ctx = else Monomorphic_entry Univ.ContextSet.empty in let entry = Declare.definition_entry ~univs ~types:t b in - let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge - ~kind:Decls.(IsDefinition Definition) ~ubind:UnivNames.empty_binders ~impargs:[] entry + (* XXX Fixme: Use DeclareDef.prepare_definition *) + let uctx = Evd.evar_universe_context sigma in + let kind = Decls.(IsDefinition Definition) in + let _ : GlobRef.t = + DeclareDef.declare_entry ~name ~scope:DeclareDef.Discharge + ~kind ~impargs:[] ~uctx entry in () in diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index ba2c1ac115..66d5a4f7f5 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -12,7 +12,6 @@ open Pp open Util open Redexpr open Constrintern -open Pretyping (* Commands of the interface: Constant definitions *) @@ -40,15 +39,56 @@ let check_imps ~impsty ~impsbody = | [], [] -> () in aux impsty impsbody +let protect_pattern_in_binder bl c ctypopt = + (* We turn "Definition d binders := body : typ" into *) + (* "Definition d := fun binders => body:type" *) + (* This is a hack while waiting for LocalPattern in regular environments *) + if List.exists (function Constrexpr.CLocalPattern _ -> true | _ -> false) bl + then + let t = match ctypopt with + | None -> CAst.make ?loc:c.CAst.loc (Constrexpr.CHole (None,Namegen.IntroAnonymous,None)) + | Some t -> t in + let loc = Loc.merge_opt c.CAst.loc t.CAst.loc in + let c = CAst.make ?loc @@ Constrexpr.CCast (c, Glob_term.CastConv t) in + let loc = match List.hd bl with + | Constrexpr.CLocalAssum (a::_,_,_) | Constrexpr.CLocalDef (a,_,_) -> a.CAst.loc + | Constrexpr.CLocalPattern {CAst.loc} -> loc + | Constrexpr.CLocalAssum ([],_,_) -> assert false in + let apply_under_binders f env evd c = + let rec aux env evd c = + let open Constr in + let open EConstr in + let open Context.Rel.Declaration in + match kind evd c with + | Lambda (x,t,c) -> + let evd,c = aux (push_rel (LocalAssum (x,t)) env) evd c in + evd, mkLambda (x,t,c) + | LetIn (x,b,t,c) -> + let evd,c = aux (push_rel (LocalDef (x,b,t)) env) evd c in + evd, mkLetIn (x,t,b,c) + | Case (ci,p,a,bl) -> + let evd,bl = Array.fold_left_map (aux env) evd bl in + evd, mkCase (ci,p,a,bl) + | Cast (c,_,_) -> f env evd c (* we remove the cast we had set *) + (* This last case may happen when reaching the proof of an + impossible case, as when pattern-matching on a vector of length 1 *) + | _ -> (evd,c) in + aux env evd c in + ([], Constrexpr_ops.mkLambdaCN ?loc:(Loc.merge_opt loc c.CAst.loc) bl c, None, apply_under_binders) + else + (bl, c, ctypopt, fun f env evd c -> f env evd c) + let interp_definition ~program_mode pl bl ~poly red_option c ctypopt = + let flags = Pretyping.{ all_no_fail_flags with program_mode } in let env = Global.env() in (* Explicitly bound universes and constraints *) let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in + let (bl, c, ctypopt, apply_under_binders) = protect_pattern_in_binder bl c ctypopt in (* Build the parameters *) 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 ~program_mode ~impls env_bl) + (interp_type_evars_impls ~flags ~impls env_bl) evd ctypopt in (* Build the body, and merge implicits from parameters and from type/body *) @@ -63,46 +103,31 @@ let interp_definition ~program_mode pl bl ~poly red_option c ctypopt = evd, c, imps1@impsty, Some ty in (* Do the reduction *) - let evd, c = red_constant_body red_option env_bl evd c in + let evd, c = apply_under_binders (red_constant_body red_option) env_bl evd c in (* Declare the definition *) let c = EConstr.it_mkLambda_or_LetIn c ctx in let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in + (c, tyopt), evd, udecl, imps - let evd, ce = DeclareDef.prepare_definition ~allow_evars:program_mode - ~opaque:false ~poly evd ~udecl ~types:tyopt ~body:c in - - (ce, evd, udecl, imps) - -let check_definition ~program_mode (ce, evd, _, imps) = - let env = Global.env () in - check_evars_are_solved ~program_mode env evd; - ce +let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = + let program_mode = false in + let (body, types), evd, udecl, impargs = + interp_definition ~program_mode udecl bl ~poly red_option c ctypopt + in + let kind = Decls.IsDefinition kind in + let _ : Names.GlobRef.t = + DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs + ~opaque:false ~poly evd ~udecl ~types ~body + in () -let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = - let (ce, evd, udecl, impargs as def) = +let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = + let program_mode = true in + let (body, types), evd, udecl, impargs = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in - if program_mode then - let env = Global.env () in - let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in - assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private); - assert(Univ.ContextSet.is_empty ctx); - Obligations.check_evars env evd; - let c = EConstr.of_constr c in - let typ = match ce.Declare.proof_entry_type with - | Some t -> EConstr.of_constr t - | None -> Retyping.get_type_of env evd c - in - let obls, _, c, cty = - Obligations.eterm_obligations env name evd 0 c typ - in - let uctx = Evd.evar_universe_context evd in - ignore(Obligations.add_definition - ~name ~term:c cty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls) - else - let ce = check_definition ~program_mode def in - let uctx = Evd.evar_universe_context evd in - let hook_data = Option.map (fun hook -> hook, uctx, []) hook in - let kind = Decls.IsDefinition kind in - ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind:(Evd.universe_binders evd) ce ~impargs) + let term, ty, uctx, obls = DeclareDef.prepare_obligation ~name ~poly ~body ~types ~udecl evd in + let _ : DeclareObl.progress = + Obligations.add_definition + ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls + in () diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 6c6da8952e..337da22018 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -15,8 +15,7 @@ open Constrexpr (** {6 Definitions/Let} *) val do_definition - : program_mode:bool - -> ?hook:DeclareDef.Hook.t + : ?hook:DeclareDef.Hook.t -> name:Id.t -> scope:DeclareDef.locality -> poly:bool @@ -28,18 +27,15 @@ val do_definition -> constr_expr option -> unit -(************************************************************************) -(** Internal API *) -(************************************************************************) - -(** Not used anywhere. *) -val interp_definition - : program_mode:bool +val do_definition_program + : ?hook:DeclareDef.Hook.t + -> name:Id.t + -> scope:DeclareDef.locality + -> poly:bool + -> kind:Decls.definition_object_kind -> universe_decl_expr option -> local_binder_expr list - -> poly:bool -> red_expr option -> constr_expr -> constr_expr option - -> Evd.side_effects Declare.proof_entry * - Evd.evar_map * UState.universe_decl * Impargs.manual_implicits + -> unit diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 6580495295..e4fa212a23 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -107,7 +107,8 @@ let interp_fix_context ~program_mode ~cofix env sigma fix = sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot) let interp_fix_ccl ~program_mode sigma impls (env,_) fix = - let sigma, (c, impl) = interp_type_evars_impls ~program_mode ~impls env sigma fix.Vernacexpr.rtype in + let flags = Pretyping.{ all_no_fail_flags with program_mode } in + let sigma, (c, impl) = interp_type_evars_impls ~flags ~impls env sigma fix.Vernacexpr.rtype in let r = Retyping.relevance_of_type env sigma c in sigma, (c, r, impl) @@ -140,8 +141,8 @@ let compute_possible_guardness_evidences (ctx,_,recindex) = fixpoints ?) *) List.interval 0 (Context.Rel.nhyps ctx - 1) -type recursive_preentry = - Id.t list * Sorts.relevance list * Constr.t option list * Constr.types list +type ('constr, 'types) recursive_preentry = + Id.t list * Sorts.relevance list * 'constr option list * 'types list (* Wellfounded definition *) @@ -230,7 +231,11 @@ let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) = let fixtypes = List.map EConstr.(to_constr evd) fixtypes in Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes) -let interp_fixpoint ~cofix l = +(* XXX: Unify with interp_recursive *) +let interp_fixpoint ~cofix l : + ( (Constr.t, Constr.types) recursive_preentry * + UState.universe_decl * UState.t * + (EConstr.rel_context * Impargs.manual_implicits * int option) list) = let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l in check_recursive true env evd fix; let uctx,fix = ground_fixpoint env evd fix in @@ -243,8 +248,10 @@ let build_recthms ~indexes fixnames fixtypes fiximps = in let thms = List.map3 (fun name typ (ctx,impargs,_) -> - { DeclareDef.Recthm.name; typ - ; args = List.map Context.Rel.Declaration.get_name ctx; impargs}) + { DeclareDef.Recthm.name + ; typ + ; args = List.map Context.Rel.Declaration.get_name ctx + ; impargs}) fixnames fixtypes fiximps in fix_kind, cofix, thms diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 2ad6c03bae..a19b96f0f3 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Constr open Vernacexpr (** {6 Fixpoints and cofixpoints} *) @@ -40,6 +39,9 @@ val adjust_rec_order -> Constrexpr.recursion_order_expr option -> lident option +(** names / relevance / defs / types *) +type ('constr, 'types) recursive_preentry = Id.t list * Sorts.relevance list * 'constr option list * 'types list + (** Exported for Program *) val interp_recursive : (* Misc arguments *) @@ -49,18 +51,17 @@ val interp_recursive : (* env / signature / univs / evar_map *) (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) * (* names / defs / types *) - (Id.t list * Sorts.relevance list * EConstr.constr option list * EConstr.types list) * + (EConstr.t, EConstr.types) recursive_preentry * (* ctx per mutual def / implicits / struct annotations *) (EConstr.rel_context * Impargs.manual_implicits * int option) list (** Exported for Funind *) -type recursive_preentry = Id.t list * Sorts.relevance list * constr option list * types list - val interp_fixpoint : cofix:bool -> lident option fix_expr_gen list - -> recursive_preentry * UState.universe_decl * UState.t * + -> (Constr.t, Constr.types) recursive_preentry * + UState.universe_decl * UState.t * (EConstr.rel_context * Impargs.manual_implicits * int option) list (** Very private function, do not use *) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 1f1700b4d6..cc9b840bed 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -20,7 +20,6 @@ open Nameops open Constrexpr open Constrexpr_ops open Constrintern -open Reductionops open Type_errors open Pretyping open Context.Rel.Declaration @@ -51,20 +50,6 @@ let should_auto_template = if b then warn_auto_template id; b -let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function - | CProdN (bl,c) -> CProdN (bl,complete_conclusion a cs c) - | CLetIn (na,b,t,c) -> CLetIn (na,b,t,complete_conclusion a cs c) - | CHole (k, _, _) -> - let (has_no_args,name,params) = a in - if not has_no_args then - user_err ?loc - (strbrk"Cannot infer the non constant arguments of the conclusion of " - ++ Id.print cs ++ str "."); - let args = List.map (fun id -> CAst.(make ?loc @@ CRef(qualid_of_ident ?loc id,None))) params in - CAppExpl ((None,qualid_of_ident ?loc name,None),List.rev args) - | c -> c - ) - let push_types env idl rl tl = List.fold_left3 (fun env id r t -> EConstr.push_rel (LocalAssum (make_annot (Name id) r,t)) env) env idl rl tl @@ -93,10 +78,6 @@ let check_all_names_different indl = | [] -> () | _ -> raise (InductiveError (SameNamesOverlap l)) -let mk_mltype_data sigma env assums arity indname = - let is_ml_type = is_sort env sigma arity in - (is_ml_type,indname,assums) - (** Make the arity conclusion flexible to avoid generating an upper bound universe now, only if the universe does not appear anywhere else. This is really a hack to stay compatible with the semantics of template polymorphic @@ -145,16 +126,50 @@ let pretype_ind_arity env sigma (loc, c, impls, pseudo_poly) = in sigma, (t, Retyping.relevance_of_sort s, concl, impls) -let interp_cstrs env sigma impls mldata arity ind = +(* ind_rel is the Rel for this inductive in the context without params. + n is how many arguments there are in the constructor. *) +let model_conclusion env sigma ind_rel params n arity_indices = + let model_head = EConstr.mkRel (n + Context.Rel.length params + ind_rel) in + let model_params = Context.Rel.to_extended_vect EConstr.mkRel n params in + let sigma,model_indices = + List.fold_right + (fun (_,t) (sigma, subst) -> + let t = EConstr.Vars.substl subst (EConstr.Vars.liftn n (List.length subst + 1) (EConstr.Vars.liftn 1 (List.length params + List.length subst + 1) t)) in + let sigma, c = Evarutil.new_evar env sigma t in + sigma, c::subst) + arity_indices (sigma, []) in + sigma, EConstr.mkApp (EConstr.mkApp (model_head, model_params), Array.of_list (List.rev model_indices)) + +let interp_cstrs env (sigma, ind_rel) impls params ind arity = let cnames,ctyps = List.split ind.ind_lc in - (* Complete conclusions of constructor types if given in ML-style syntax *) - let ctyps' = List.map2 (complete_conclusion mldata) cnames ctyps in + let arity_indices, cstr_sort = Reductionops.splay_arity env sigma arity in (* Interpret the constructor types *) - let sigma, (ctyps'', cimpls) = + let interp_cstr sigma ctyp = + let flags = + Pretyping.{ all_no_fail_flags with + use_typeclasses = UseTCForConv; + solve_unification_constraints = false } + in + let sigma, (ctyp, cimpl) = interp_type_evars_impls ~flags env sigma ~impls ctyp in + let ctx, concl = Reductionops.splay_prod_assum env sigma ctyp in + let concl_env = EConstr.push_rel_context ctx env in + let sigma_with_model_evars, model = + model_conclusion concl_env sigma ind_rel params (Context.Rel.length ctx) arity_indices + in + (* unify the expected with the provided conclusion *) + let sigma = + try Evarconv.unify concl_env sigma_with_model_evars Reduction.CONV concl model + with Evarconv.UnableToUnify (sigma,e) -> + user_err (Himsg.explain_pretype_error concl_env sigma + (Pretype_errors.CannotUnify (concl, model, (Some e)))) + in + sigma, (ctyp, cimpl) + in + let sigma, (ctyps, cimpls) = on_snd List.split @@ - List.fold_left_map (fun sigma l -> - interp_type_evars_impls ~program_mode:false env sigma ~impls l) sigma ctyps' in - sigma, (cnames, ctyps'', cimpls) + List.fold_left_map interp_cstr sigma ctyps + in + (sigma, pred ind_rel), (cnames, ctyps, cimpls) let sign_level env evd sign = fst (List.fold_right @@ -427,6 +442,30 @@ let interp_params env udecl uparamsl paramsl = sigma, env_params, (ctx_params, env_uparams, ctx_uparams, List.map (RelDecl.get_name %> Name.get_id) assums, userimpls, useruimpls, impls, udecl) +(* When a hole remains for a param, pretend the param is uniform and + do the unification. + [env_ar_par] is [uparams; inds; params] + *) +let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams c = + let is_ind sigma k c = match EConstr.kind sigma c with + | Constr.Rel n -> + (* env is [uparams; inds; params; k other things] *) + n > k + nparams && n <= k + nparams + ninds + | _ -> false + in + let rec aux (env,k as envk) sigma c = match EConstr.kind sigma c with + | Constr.App (h,args) when is_ind sigma k h -> + Array.fold_left_i (fun i sigma arg -> + if i >= nparams || not (EConstr.isEvar sigma arg) then sigma + else Evarconv.unify_delay env sigma arg (EConstr.mkRel (k+nparams-i))) + sigma args + | _ -> Termops.fold_constr_with_full_binders + sigma + (fun d (env,k) -> EConstr.push_rel d env, k+1) + aux envk sigma c + in + aux (env_ar_par,0) sigma c + let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite = check_all_names_different indl; List.iter check_param paramsl; @@ -464,20 +503,31 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not (* Compute interpretation metadatas *) let indimpls = List.map (fun impls -> userimpls @ impls) indimpls in - let impls = compute_internalization_env env_uparams sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in - let ntn_impls = compute_internalization_env env_uparams sigma (Inductive (params,true)) indnames fullarities indimpls in - let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in + let impls = compute_internalization_env env_uparams sigma ~impls Inductive indnames fullarities indimpls in + let ntn_impls = compute_internalization_env env_uparams sigma Inductive indnames fullarities indimpls in - let sigma, constructors = + let ninds = List.length indl in + let (sigma, _), constructors = Metasyntax.with_syntax_protection (fun () -> - (* Temporary declaration of notations and scopes *) - List.iter (Metasyntax.set_notation_for_interpretation env_params ntn_impls) notations; - (* Interpret the constructor types *) - List.fold_left3_map (fun sigma -> interp_cstrs env_ar_params sigma impls) sigma mldatas arities indl) - () in + (* Temporary declaration of notations and scopes *) + List.iter (Metasyntax.set_notation_for_interpretation env_params ntn_impls) notations; + (* Interpret the constructor types *) + List.fold_left2_map + (fun (sigma, ind_rel) -> interp_cstrs env_ar_params (sigma, ind_rel) impls ctx_params) + (sigma, ninds) indl arities) + () + in - (* generalize over the uniform parameters *) let nparams = Context.Rel.length ctx_params in + let sigma = + List.fold_left (fun sigma (_,ctyps,_) -> + List.fold_left (fun sigma ctyp -> + maybe_unify_params_in env_ar_params sigma ~ninds ~nparams ctyp) + sigma ctyps) + sigma constructors + in + + (* generalize over the uniform parameters *) let nuparams = Context.Rel.length ctx_uparams in let uargs = Context.Rel.to_extended_vect EConstr.mkRel 0 ctx_uparams in let uparam_subst = diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 2b9da1d4e5..984581152a 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -88,3 +88,9 @@ val template_polymorphism_candidate polymorphic. It should have at least one universe in its monomorphic universe context that can be made parametric in its conclusion sort, if one is given. *) + +val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:int + -> EConstr.t -> Evd.evar_map +(** [nparams] is the number of parameters which aren't treated as + uniform, ie the length of params (including letins) where the env + is [uniform params, inductives, params]. *) diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 3bac0419ef..80e7e6ab96 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -195,12 +195,12 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let lift_lets = lift_rel_context 1 letbinders in let sigma, intern_body = let ctx = LocalAssum (make_annot (Name recname) Sorts.Relevant, get_type curry_fun) :: binders_rel in - let (r, l, impls, scopes) = + let (r, impls, scopes) = Constrintern.compute_internalization_data env sigma Constrintern.Recursive full_arity impls in let newimpls = Id.Map.singleton recname - (r, l, impls @ [Some (ExplByName (Id.of_string "recproof"), Impargs.Manual, (true, false))], + (r, impls @ [Some (ExplByName (Id.of_string "recproof"), Impargs.Manual, (true, false))], scopes @ [None]) in interp_casted_constr_evars ~program_mode:true (push_rel_context ctx env) sigma ~impls:newimpls body (lift 1 top_arity) @@ -254,9 +254,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = in (* XXX: Capturing sigma here... bad bad *) let hook = DeclareDef.Hook.make (hook sigma) in - Obligations.check_evars env sigma; + RetrieveObl.check_evars env sigma; let evars, _, evars_def, evars_typ = - Obligations.eterm_obligations env recname sigma 0 def typ + RetrieveObl.retrieve_obligations env recname sigma 0 def typ in let uctx = Evd.evar_universe_context sigma in ignore(Obligations.add_definition ~name:recname ~term:evars_def ~udecl @@ -281,15 +281,15 @@ let do_program_recursive ~scope ~poly fixkind fixl = let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in (* Solve remaining evars *) let evd = nf_evar_map_undefined evd in - let collect_evars id def typ imps = + let collect_evars name def typ impargs = (* Generalize by the recursive prototypes *) let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in let evm = collect_evars_of_term evd def typ in let evars, _, def, typ = - Obligations.eterm_obligations env id evm + RetrieveObl.retrieve_obligations env name evm (List.length rec_sign) def typ in - (id, def, typ, imps, evars) + ({ DeclareDef.Recthm.name; typ; impargs; args = [] }, def, evars) in let (fixnames,fixrs,fixdefs,fixtypes) = fix in let fiximps = List.map pi2 info in diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index fc53abdcea..1607771598 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -9,7 +9,6 @@ (************************************************************************) open Declare -open Impargs type locality = Discharge | Global of Declare.import_status @@ -34,41 +33,39 @@ module Hook = struct let make hook = CEphemeron.create hook - let call ?hook ?fix_exn x = - try Option.iter (fun hook -> CEphemeron.get hook x) hook - with e when CErrors.noncritical e -> - let e = Exninfo.capture e in - let e = Option.cata (fun fix -> fix e) e fix_exn in - Exninfo.iraise e + let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x) hook + end (* Locality stuff *) -let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce = - let fix_exn = Declare.Internal.get_fix_exn ce in - let should_suggest = ce.Declare.proof_entry_opaque && - Option.is_empty ce.Declare.proof_entry_secctx in +let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry = + let should_suggest = entry.Declare.proof_entry_opaque && + Option.is_empty entry.Declare.proof_entry_secctx in + let ubind = UState.universe_binders uctx in let dref = match scope with | Discharge -> - let () = declare_variable ~name ~kind (SectionLocalDef ce) in + let () = declare_variable ~name ~kind (SectionLocalDef entry) in if should_suggest then Proof_using.suggest_variable (Global.env ()) name; Names.GlobRef.VarRef name | Global local -> - let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in + let kn = declare_constant ~name ~local ~kind (DefinitionEntry entry) in let gr = Names.GlobRef.ConstRef kn in if should_suggest then Proof_using.suggest_constant (Global.env ()) kn; let () = DeclareUniv.declare_univ_binders gr ubind in gr in - let () = maybe_declare_manual_implicits false dref impargs in + let () = Impargs.maybe_declare_manual_implicits false dref impargs in let () = definition_message name in - begin - match hook_data with - | None -> () - | Some (hook, uctx, obls) -> - Hook.call ~fix_exn ~hook { Hook.S.uctx; obls; scope; dref } - end; + Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook; dref +let declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry = + try declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry + with exn -> + let exn = Exninfo.capture exn in + let fix_exn = Declare.Internal.get_fix_exn entry in + Exninfo.iraise (fix_exn exn) + let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes = match possible_indexes with | Some possible_indexes -> @@ -98,22 +95,21 @@ end let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems = let vars, fixdecls, indexes = mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in - let ubind, univs = + let uctx, univs = (* XXX: Obligations don't do this, this seems like a bug? *) if restrict_ucontext then - let evd = Evd.from_ctx uctx in - let evd = Evd.restrict_universe_context evd vars in - let univs = Evd.check_univ_decl ~poly evd udecl in - Evd.universe_binders evd, univs + let uctx = UState.restrict uctx vars in + let univs = UState.check_univ_decl ~poly uctx udecl in + uctx, univs else let univs = UState.univ_entry ~poly uctx in - UnivNames.empty_binders, univs + uctx, univs in let csts = CList.map2 (fun Recthm.{ name; typ; impargs } body -> - let ce = Declare.definition_entry ~opaque ~types:typ ~univs body in - declare_definition ~name ~scope ~kind ~ubind ~impargs ce) + let entry = Declare.definition_entry ~opaque ~types:typ ~univs body in + declare_entry ~name ~scope ~kind ~impargs ~uctx entry) fixitems fixdecls in let isfix = Option.is_empty possible_indexes in @@ -127,7 +123,7 @@ let warn_let_as_axiom = Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++ spc () ++ strbrk "declared as an axiom.") -let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = +let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe = let local = match scope with | Discharge -> warn_let_as_axiom name; Declare.ImportNeedQualified | Global local -> local @@ -139,26 +135,58 @@ let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = let () = Impargs.maybe_declare_manual_implicits false dref impargs in let () = Declare.assumption_message name in let () = DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx) in - let () = Hook.(call ?fix_exn ?hook { S.uctx; obls = []; scope; dref}) in + let () = Hook.(call ?hook { S.uctx; obls = []; scope; dref}) in dref +let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = + try declare_assumption ~name ~scope ~hook ~impargs ~uctx pe + with exn -> + let exn = Exninfo.capture exn in + let exn = Option.cata (fun fix -> fix exn) exn fix_exn in + Exninfo.iraise exn + (* Preparing proof entries *) -let check_definition_evars ~allow_evars sigma = +let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma = let env = Global.env () in - if not allow_evars then Pretyping.check_evars_are_solved ~program_mode:false env sigma + Pretyping.check_evars_are_solved ~program_mode:false env sigma; + let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true + sigma (fun nf -> nf body, Option.map nf types) + in + let univs = Evd.check_univ_decl ~poly sigma udecl in + let entry = definition_entry ?fix_exn ?opaque ?inline ?types ~univs body in + let uctx = Evd.evar_universe_context sigma in + entry, uctx + +let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook + ?obls ~poly ?inline ~types ~body ?fix_exn sigma = + let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in + declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry -let prepare_definition ~allow_evars ?opaque ?inline ~poly ~udecl ~types ~body sigma = - check_definition_evars ~allow_evars sigma; - let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars) +let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma = + let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false sigma (fun nf -> nf body, Option.map nf types) in let univs = Evd.check_univ_decl ~poly sigma udecl in - sigma, definition_entry ?opaque ?inline ?types ~univs body + let ce = definition_entry ?opaque ?inline ?types ~univs body in + let env = Global.env () in + let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in + assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private); + assert(Univ.ContextSet.is_empty ctx); + RetrieveObl.check_evars env sigma; + let c = EConstr.of_constr c in + let typ = match ce.Declare.proof_entry_type with + | Some t -> EConstr.of_constr t + | None -> Retyping.get_type_of env sigma c + in + let obls, _, c, cty = RetrieveObl.retrieve_obligations env name sigma 0 c typ in + let uctx = Evd.evar_universe_context sigma in + c, cty, uctx, obls -let prepare_parameter ~allow_evars ~poly ~udecl ~types sigma = - check_definition_evars ~allow_evars sigma; - let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars) +let prepare_parameter ~poly ~udecl ~types sigma = + let env = Global.env () in + Pretyping.check_evars_are_solved ~program_mode:false env sigma; + let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:true sigma (fun nf -> nf types) in let univs = Evd.check_univ_decl ~poly sigma udecl in diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 1d7fd3a3bf..3bc1e25f19 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -36,19 +36,44 @@ module Hook : sig end val make : (S.t -> unit) -> t - val call : ?hook:t -> ?fix_exn:Future.fix_exn -> S.t -> unit + val call : ?hook:t -> S.t -> unit end -val declare_definition +(** Declare an interactively-defined constant *) +val declare_entry : name:Id.t -> scope:locality -> kind:Decls.logical_kind - -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) - -> ubind:UnivNames.universe_binders + -> ?hook:Hook.t + -> ?obls:(Id.t * Constr.t) list -> impargs:Impargs.manual_implicits + -> uctx:UState.t -> Evd.side_effects Declare.proof_entry -> GlobRef.t +(** Declares a non-interactive constant; [body] and [types] will be + normalized w.r.t. the passed [evar_map] [sigma]. Universes should + be handled properly, including minimization and restriction. Note + that [sigma] is checked for unresolved evars, thus you should be + careful not to submit open terms or evar maps with stale, + unresolved existentials *) +val declare_definition + : name:Id.t + -> scope:locality + -> kind:Decls.logical_kind + -> opaque:bool + -> impargs:Impargs.manual_implicits + -> udecl:UState.universe_decl + -> ?hook:Hook.t + -> ?obls:(Id.t * Constr.t) list + -> poly:bool + -> ?inline:bool + -> types:EConstr.t option + -> body:EConstr.t + -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) + -> Evd.evar_map + -> GlobRef.t + val declare_assumption : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) -> name:Id.t @@ -88,20 +113,19 @@ val declare_mutually_recursive -> Recthm.t list -> Names.GlobRef.t list -val prepare_definition - : allow_evars:bool - -> ?opaque:bool +val prepare_obligation + : ?opaque:bool -> ?inline:bool + -> name:Id.t -> poly:bool -> udecl:UState.universe_decl -> types:EConstr.t option -> body:EConstr.t -> Evd.evar_map - -> Evd.evar_map * Evd.side_effects Declare.proof_entry + -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info val prepare_parameter - : allow_evars:bool - -> poly:bool + : poly:bool -> udecl:UState.universe_decl -> types:EConstr.types -> Evd.evar_map diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 98a9e4b9c9..bba3687256 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -362,34 +362,21 @@ let get_fix_exn, stm_get_fix_exn = Hook.make () let declare_definition prg = let varsubst = obligation_substitution true prg in - let body, typ = subst_prog varsubst prg in - let nf = - UnivSubst.nf_evars_and_universes_opt_subst - (fun x -> None) - (UState.subst prg.prg_ctx) - in - let opaque = prg.prg_opaque in + let sigma = Evd.from_ctx prg.prg_ctx in + let body, types = subst_prog varsubst prg in + let body, types = EConstr.(of_constr body, Some (of_constr types)) in + (* All these should be grouped into a struct a some point *) + let opaque, poly, udecl, hook = prg.prg_opaque, prg.prg_poly, prg.prg_univdecl, prg.prg_hook in + let name, scope, kind, impargs = prg.prg_name, prg.prg_scope, Decls.(IsDefinition prg.prg_kind), prg.prg_implicits in let fix_exn = Hook.get get_fix_exn () in - let typ = nf typ in - let body = nf body in - let obls = List.map (fun (id, (_, c)) -> (id, nf c)) varsubst in - let uvars = - Univ.LSet.union - (Vars.universes_of_constr typ) - (Vars.universes_of_constr body) - in - let uctx = UState.restrict prg.prg_ctx uvars in - let univs = - UState.check_univ_decl ~poly:prg.prg_poly uctx prg.prg_univdecl - in - let ce = Declare.definition_entry ~fix_exn ~opaque ~types:typ ~univs body in + let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in + (* XXX: This is doing normalization twice *) let () = progmap_remove prg in - let ubind = UState.universe_binders uctx in - let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in - DeclareDef.declare_definition - ~name:prg.prg_name ~scope:prg.prg_scope ~ubind - ~kind:Decls.(IsDefinition prg.prg_kind) ce - ~impargs:prg.prg_implicits ?hook_data + let kn = + DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook ~obls + ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma + in + kn let rec lam_index n t acc = match Constr.kind t with @@ -464,9 +451,8 @@ let declare_mutual_definition l = ~restrict_ucontext:false fixitems in (* Only for the first constant *) - let fix_exn = Hook.get get_fix_exn () in let dref = List.hd kns in - DeclareDef.Hook.(call ?hook:first.prg_hook ~fix_exn { S.uctx = first.prg_ctx; obls; scope; dref }); + DeclareDef.Hook.(call ?hook:first.prg_hook { S.uctx = first.prg_ctx; obls; scope; dref }); List.iter progmap_remove l; dref @@ -529,10 +515,6 @@ let obligation_terminator entries uctx { name; num; auto } = Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body); (* Declare the obligation ourselves and drop the hook *) let prg = CEphemeron.get (ProgMap.find name !from_prg) in - (* Ensure universes are substituted properly in body and type *) - let body = EConstr.to_constr sigma (EConstr.of_constr body) in - let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in - let ctx = Evd.evar_universe_context sigma in let { obls; remaining=rem } = prg.prg_obligations in let obl = obls.(num) in let status = @@ -545,24 +527,24 @@ let obligation_terminator entries uctx { name; num; auto } = | (_, status), false -> status in let obl = { obl with obl_status = false, status } in - let ctx = - if prg.prg_poly then ctx - else UState.union prg.prg_ctx ctx + let uctx = + if prg.prg_poly then uctx + else UState.union prg.prg_ctx uctx in - let uctx = UState.univ_entry ~poly:prg.prg_poly ctx in - let (defined, obl) = declare_obligation prg obl body ty uctx in + let univs = UState.univ_entry ~poly:prg.prg_poly uctx in + let (defined, obl) = declare_obligation prg obl body ty univs in let prg_ctx = if prg.prg_poly then (* Polymorphic *) (* We merge the new universes and constraints of the polymorphic obligation with the existing ones *) - UState.union prg.prg_ctx ctx + UState.union prg.prg_ctx uctx else (* The first obligation, if defined, declares the univs of the constant, each subsequent obligation declares its own additional universes and constraints if any *) if defined then UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) - else ctx + else uctx in update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto | _ -> diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 5dae389a62..fdc8b1ba4c 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -325,51 +325,48 @@ let is_binder_level custom (custom',from) e = match e with | _ -> false let make_sep_rules = function - | [tk] -> Atoken tk + | [tk] -> + Pcoq.Symbol.token tk | tkl -> - let rec mkrule : 'a Tok.p list -> 'a rules = function - | [] -> Rules (Stop, fun _ -> (* dropped anyway: *) "") - | tkn :: rem -> - let Rules (r, f) = mkrule rem in - let r = NextNoRec (r, Atoken tkn) in - Rules (r, fun _ -> f) - in - let r = mkrule (List.rev tkl) in - Arules [r] + let r = Pcoq.mk_rule (List.rev tkl) in + Pcoq.Symbol.rules [r] type ('s, 'a) mayrec_symbol = -| MayRecNo : ('s, norec, 'a) symbol -> ('s, 'a) mayrec_symbol -| MayRecMay : ('s, mayrec, 'a) symbol -> ('s, 'a) mayrec_symbol +| MayRecNo : ('s, Gramlib.Grammar.norec, 'a) Symbol.t -> ('s, 'a) mayrec_symbol +| MayRecMay : ('s, Gramlib.Grammar.mayrec, 'a) Symbol.t -> ('s, 'a) mayrec_symbol let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_symbol = fun custom p assoc from forpat -> - if is_binder_level custom from p then (* Prevent self *) MayRecNo (Aentryl (target_entry custom forpat, "200")) - else if is_self custom from p then MayRecMay Aself + if is_binder_level custom from p + then + (* Prevent self *) + MayRecNo (Pcoq.Symbol.nterml (target_entry custom forpat) "200") + else if is_self custom from p then MayRecMay Pcoq.Symbol.self else let g = target_entry custom forpat in let lev = adjust_level custom assoc from p in begin match lev with - | DefaultLevel -> MayRecNo (Aentry g) - | NextLevel -> MayRecMay Anext - | NumLevel lev -> MayRecNo (Aentryl (g, string_of_int lev)) + | DefaultLevel -> MayRecNo (Pcoq.Symbol.nterm g) + | NextLevel -> MayRecMay Pcoq.Symbol.next + | NumLevel lev -> MayRecNo (Pcoq.Symbol.nterml g (string_of_int lev)) end let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = fun assoc from typ -> match typ with | TTConstr (s, p, forpat) -> symbol_of_target s p assoc from forpat | TTConstrList (s, typ', [], forpat) -> begin match symbol_of_target s typ' assoc from forpat with - | MayRecNo s -> MayRecNo (Alist1 s) - | MayRecMay s -> MayRecMay (Alist1 s) end + | MayRecNo s -> MayRecNo (Pcoq.Symbol.list1 s) + | MayRecMay s -> MayRecMay (Pcoq.Symbol.list1 s) end | TTConstrList (s, typ', tkl, forpat) -> begin match symbol_of_target s typ' assoc from forpat with - | MayRecNo s -> MayRecNo (Alist1sep (s, make_sep_rules tkl)) - | MayRecMay s -> MayRecMay (Alist1sep (s, make_sep_rules tkl)) end -| TTPattern p -> MayRecNo (Aentryl (Constr.pattern, string_of_int p)) -| TTClosedBinderList [] -> MayRecNo (Alist1 (Aentry Constr.binder)) -| TTClosedBinderList tkl -> MayRecNo (Alist1sep (Aentry Constr.binder, make_sep_rules tkl)) -| TTName -> MayRecNo (Aentry Prim.name) -| TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders) -| TTBigint -> MayRecNo (Aentry Prim.bignat) -| TTReference -> MayRecNo (Aentry Constr.global) + | MayRecNo s -> MayRecNo (Pcoq.Symbol.list1sep s (make_sep_rules tkl) false) + | MayRecMay s -> MayRecMay (Pcoq.Symbol.list1sep s (make_sep_rules tkl) false) end +| TTPattern p -> MayRecNo (Pcoq.Symbol.nterml Constr.pattern (string_of_int p)) +| TTClosedBinderList [] -> MayRecNo (Pcoq.Symbol.list1 (Pcoq.Symbol.nterm Constr.binder)) +| TTClosedBinderList tkl -> MayRecNo (Pcoq.Symbol.list1sep (Pcoq.Symbol.nterm Constr.binder) (make_sep_rules tkl) false) +| TTName -> MayRecNo (Pcoq.Symbol.nterm Prim.name) +| TTOpenBinderList -> MayRecNo (Pcoq.Symbol.nterm Constr.open_binders) +| TTBigint -> MayRecNo (Pcoq.Symbol.nterm Prim.bignat) +| TTReference -> MayRecNo (Pcoq.Symbol.nterm Constr.global) let interp_entry forpat e = match e with | ETProdName -> TTAny TTName @@ -461,22 +458,22 @@ let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env -> ty_eval rem f { env with constrs; constrlists; } type ('s, 'a, 'r) mayrec_rule = -| MayRecRNo : ('s, Extend.norec, 'a, 'r) Extend.rule -> ('s, 'a, 'r) mayrec_rule -| MayRecRMay : ('s, Extend.mayrec, 'a, 'r) Extend.rule -> ('s, 'a, 'r) mayrec_rule +| MayRecRNo : ('s, Gramlib.Grammar.norec, 'a, 'r) Rule.t -> ('s, 'a, 'r) mayrec_rule +| MayRecRMay : ('s, Gramlib.Grammar.mayrec, 'a, 'r) Rule.t -> ('s, 'a, 'r) mayrec_rule let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) mayrec_rule = function -| TyStop -> MayRecRNo Stop +| TyStop -> MayRecRNo Rule.stop | TyMark (_, _, _, r) -> ty_erase r | TyNext (rem, TyTerm tok) -> begin match ty_erase rem with - | MayRecRNo rem -> MayRecRMay (Next (rem, Atoken tok)) - | MayRecRMay rem -> MayRecRMay (Next (rem, Atoken tok)) end + | MayRecRNo rem -> MayRecRMay (Rule.next rem (Symbol.token tok)) + | MayRecRMay rem -> MayRecRMay (Rule.next rem (Symbol.token tok)) end | TyNext (rem, TyNonTerm (_, _, s, _)) -> begin match ty_erase rem, s with - | MayRecRNo rem, MayRecNo s -> MayRecRMay (Next (rem, s)) - | MayRecRNo rem, MayRecMay s -> MayRecRMay (Next (rem, s)) - | MayRecRMay rem, MayRecNo s -> MayRecRMay (Next (rem, s)) - | MayRecRMay rem, MayRecMay s -> MayRecRMay (Next (rem, s)) end + | MayRecRNo rem, MayRecNo s -> MayRecRMay (Rule.next rem s) + | MayRecRNo rem, MayRecMay s -> MayRecRMay (Rule.next rem s) + | MayRecRMay rem, MayRecNo s -> MayRecRMay (Rule.next rem s) + | MayRecRMay rem, MayRecMay s -> MayRecRMay (Rule.next rem s) end type ('self, 'r) any_ty_rule = | AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule @@ -504,7 +501,7 @@ let target_to_bool : type r. r target -> bool = function | ForPattern -> true let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) = - let empty = (pos, [(name, p4assoc, [])]) in + let empty = { pos; data = [(name, p4assoc, [])] } in match reinit with | None -> ExtendRule (target_entry where forpat, empty) @@ -522,7 +519,13 @@ let rec pure_sublevels' assoc from forpat level = function let rem = pure_sublevels' assoc from forpat level rem in let push where p rem = match symbol_of_target where p assoc from forpat with - | MayRecNo (Aentryl (_,i)) when different_levels (fst from,level) (where,i) -> (where,int_of_string i) :: rem + | MayRecNo sym -> + (match Pcoq.level_of_nonterm sym with + | None -> rem + | Some i -> + if different_levels (fst from,level) (where,i) then + (where,int_of_string i) :: rem + else rem) | _ -> rem in (match e with | ETProdPattern i -> push InConstrEntry (NumLevel i,InternalProd) rem @@ -553,14 +556,15 @@ let extend_constr state forpat ng = let act = ty_eval r (make_act forpat ng.notgram_notation) empty in let rule = let r = match ty_erase r with - | MayRecRNo symbs -> Rule (symbs, act) - | MayRecRMay symbs -> Rule (symbs, act) in + | MayRecRNo symbs -> Pcoq.Production.make symbs act + | MayRecRMay symbs -> Pcoq.Production.make symbs act + in name, p4assoc, [r] in let r = match reinit with | None -> - ExtendRule (entry, (pos, [rule])) + ExtendRule (entry, { pos; data = [rule]}) | Some reinit -> - ExtendRuleReinit (entry, reinit, (pos, [rule])) + ExtendRuleReinit (entry, reinit, { pos; data = [rule]}) in (accu @ empty_rules @ [r], state) in diff --git a/vernac/egramml.ml b/vernac/egramml.ml index 793aad6b24..bda1401bc9 100644 --- a/vernac/egramml.ml +++ b/vernac/egramml.ml @@ -19,14 +19,14 @@ open Vernacexpr type 's grammar_prod_item = | GramTerminal of string | GramNonTerminal : - ('a raw_abstract_argument_type * ('s, _, 'a) symbol) Loc.located -> 's grammar_prod_item + ('a raw_abstract_argument_type * ('s, _, 'a) Symbol.t) Loc.located -> 's grammar_prod_item type 'a ty_arg = ('a -> raw_generic_argument) type ('self, 'tr, _, 'r) ty_rule = -| TyStop : ('self, Extend.norec, 'r, 'r) ty_rule -| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Extend.symbol * 'b ty_arg option -> - ('self, Extend.mayrec, 'b -> 'a, 'r) ty_rule +| TyStop : ('self, Gramlib.Grammar.norec, 'r, 'r) ty_rule +| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Symbol.t * 'b ty_arg option -> + ('self, Gramlib.Grammar.mayrec, 'b -> 'a, 'r) ty_rule type ('self, 'r) any_ty_rule = | AnyTyRule : ('self, _, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule @@ -35,7 +35,7 @@ let rec ty_rule_of_gram = function | [] -> AnyTyRule TyStop | GramTerminal s :: rem -> let AnyTyRule rem = ty_rule_of_gram rem in - let tok = Atoken (CLexer.terminal s) in + let tok = Pcoq.Symbol.token (CLexer.terminal s) in let r = TyNext (rem, tok, None) in AnyTyRule r | GramNonTerminal (_, (t, tok)) :: rem -> @@ -44,9 +44,9 @@ let rec ty_rule_of_gram = function let r = TyNext (rem, tok, inj) in AnyTyRule r -let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Extend.rule = function -| TyStop -> Extend.Stop -| TyNext (rem, tok, _) -> Extend.Next (ty_erase rem, tok) +let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Pcoq.Rule.t = function +| TyStop -> Pcoq.Rule.stop +| TyNext (rem, tok, _) -> Pcoq.Rule.next (ty_erase rem) tok type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r @@ -62,7 +62,7 @@ let make_rule f prod = let symb = ty_erase ty_rule in let f loc l = f loc (List.rev l) in let act = ty_eval ty_rule f in - Extend.Rule (symb, act) + Pcoq.Production.make symb act let rec proj_symbol : type a b c. (a, b, c) ty_user_symbol -> (a, b, c) genarg_type = function | TUentry a -> ExtraArg a @@ -90,4 +90,4 @@ let extend_vernac_command_grammar s nt gl = vernac_exts := (s,gl) :: !vernac_exts; let mkact loc l = VernacExtend (s, l) in let rules = [make_rule mkact gl] in - grammar_extend nt (None, [None, None, rules]) + grammar_extend nt { pos=None; data=[None, None, rules]} diff --git a/vernac/egramml.mli b/vernac/egramml.mli index 7f6656b079..15f415ca3b 100644 --- a/vernac/egramml.mli +++ b/vernac/egramml.mli @@ -18,7 +18,7 @@ open Vernacexpr type 's grammar_prod_item = | GramTerminal of string | GramNonTerminal : ('a Genarg.raw_abstract_argument_type * - ('s, _, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item + ('s, _, 'a) Pcoq.Symbol.t) Loc.located -> 's grammar_prod_item val extend_vernac_command_grammar : extend_name -> vernac_expr Pcoq.Entry.t option -> @@ -32,4 +32,4 @@ val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.gena val make_rule : (Loc.t -> Genarg.raw_generic_argument list -> 'a) -> - 'a grammar_prod_item list -> 'a Extend.production_rule + 'a grammar_prod_item list -> 'a Pcoq.Production.t diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index dd75693c5b..a1cdc718d7 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -348,25 +348,11 @@ GRAMMAR EXTEND Gram (* Simple definitions *) def_body: [ [ bl = binders; ":="; red = reduce; c = lconstr -> - { if List.exists (function CLocalPattern _ -> true | _ -> false) bl - then - (* FIXME: "red" will be applied to types in bl and Cast with remain *) - let c = mkLambdaCN ~loc bl c in - DefineBody ([], red, c, None) - else - (match c with - | { CAst.v = CCast(c, CastConv t) } -> DefineBody (bl, red, c, Some t) - | _ -> DefineBody (bl, red, c, None)) } + { match c.CAst.v with + | CCast(c, Glob_term.CastConv t) -> DefineBody (bl, red, c, Some t) + | _ -> DefineBody (bl, red, c, None) } | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> - { let ((bl, c), tyo) = - if List.exists (function CLocalPattern _ -> true | _ -> false) bl - then - (* FIXME: "red" will be applied to types in bl and Cast with remain *) - let c = CAst.make ~loc @@ CCast (c, CastConv t) in - (([],mkLambdaCN ~loc bl c), None) - else ((bl, c), Some t) - in - DefineBody (bl, red, c, tyo) } + { DefineBody (bl, red, c, Some t) } | bl = binders; ":"; t = lconstr -> { ProveBody (bl, t) } ] ] ; @@ -983,13 +969,6 @@ GRAMMAR EXTEND Gram { fun g -> VernacSearch (SearchRewrite c,g, l) } | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." -> { let (sl,m) = l in fun g -> VernacSearch (Search (s::sl),g, m) } - (* compatibility: SearchAbout *) - | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries; "." -> - { fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m) } - (* compatibility: SearchAbout with "[ ... ]" *) - | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]"; - l = in_or_out_modules; "." -> - { fun g -> VernacSearch (SearchAbout sl,g, l) } ] ] ; printable: diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index e08d2ce117..7f7340bb34 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -27,15 +27,12 @@ module Proof_ending = struct | Regular | End_obligation of DeclareObl.obligation_qed_info | End_derive of { f : Id.t; name : Id.t } - | End_equations of { hook : Constant.t list -> Evd.evar_map -> unit - ; i : Id.t - ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list - ; wits : EConstr.t list ref - (* wits are actually computed by the proof - engine by side-effect after creating the - proof! This is due to the start_dependent_proof API *) - ; sigma : Evd.evar_map - } + | End_equations of + { hook : Constant.t list -> Evd.evar_map -> unit + ; i : Id.t + ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list + ; sigma : Evd.evar_map + } end @@ -43,22 +40,21 @@ module Info = struct type t = { hook : DeclareDef.Hook.t option - ; compute_guard : lemma_possible_guards - ; impargs : Impargs.manual_implicits ; proof_ending : Proof_ending.t CEphemeron.key (* This could be improved and the CEphemeron removed *) - ; other_thms : DeclareDef.Recthm.t list ; scope : DeclareDef.locality ; kind : Decls.logical_kind + (* thms and compute guard are specific only to start_lemma_with_initialization + regular terminator *) + ; thms : DeclareDef.Recthm.t list + ; compute_guard : lemma_possible_guards } let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.(IsProof Lemma)) () = { hook ; compute_guard = [] - ; impargs = [] ; proof_ending = CEphemeron.create proof_ending - ; other_thms = [] + ; thms = [] ; scope ; kind } @@ -100,18 +96,30 @@ let initialize_named_context_for_proof () = let d = if Decls.variable_opacity id then NamedDecl.drop_body d else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val +let add_first_thm ~info ~name ~typ ~impargs = + let thms = + { DeclareDef.Recthm.name + ; impargs + ; typ = EConstr.Unsafe.to_constr typ + ; args = [] } :: info.Info.thms + in + { info with Info.thms } + (* Starting a goal *) let start_lemma ~name ~poly ?(udecl=UState.default_univ_decl) - ?(info=Info.make ()) - sigma c = + ?(info=Info.make ()) ?(impargs=[]) sigma c = (* We remove the bodies of variables in the named context marked "opaque", this is a hack tho, see #10446 *) let sign = initialize_named_context_for_proof () in let goals = [ Global.env_of_context sign , c ] in let proof = Proof_global.start_proof sigma ~name ~udecl ~poly goals in - { proof ; info } + let info = add_first_thm ~info ~name ~typ:c ~impargs in + { proof; info } +(* Note that proofs opened by start_dependent lemma cannot be closed + by the regular terminators, thus we don't need to update the [thms] + field. We will capture this invariant by typing in the future *) let start_dependent_lemma ~name ~poly ?(udecl=UState.default_univ_decl) ?(info=Info.make ()) telescope = @@ -153,17 +161,18 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua intro_tac (List.hd thms), [] in match thms with | [] -> CErrors.anomaly (Pp.str "No proof to start.") - | { DeclareDef.Recthm.name; typ; impargs; _}::other_thms -> + | { DeclareDef.Recthm.name; typ; impargs; _} :: thms -> let info = Info.{ hook - ; impargs ; compute_guard - ; other_thms ; proof_ending = CEphemeron.create Proof_ending.Regular + ; thms ; scope ; kind } in - let lemma = start_lemma ~name ~poly ~udecl ~info sigma (EConstr.of_constr typ) in + (* start_lemma has the responsibility to add (name, impargs, typ) + to thms, once Info.t is more refined this won't be necessary *) + let lemma = start_lemma ~name ~impargs ~poly ~udecl ~info sigma (EConstr.of_constr typ) in pf_map (Proof_global.map_proof (fun p -> pi1 @@ Proof.run_tactic Global.(env ()) init_tac p)) lemma @@ -179,39 +188,19 @@ module MutualEntry : sig val declare_variable : info:Info.t -> uctx:UState.t - (* Only for the first constant, introduced by compat *) - -> ubind:UnivNames.universe_binders - -> name:Id.t -> Entries.parameter_entry -> Names.GlobRef.t list val declare_mutdef (* Common to all recthms *) : info:Info.t - -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) -> uctx:UState.t - -> ?hook_data:DeclareDef.Hook.t * UState.t * (Names.Id.t * Constr.t) list - (* Only for the first constant, introduced by compat *) - -> ubind:UnivNames.universe_binders - -> name:Id.t -> Evd.side_effects Declare.proof_entry -> Names.GlobRef.t list end = struct - (* Body with the fix *) - type et = - | NoBody of Entries.parameter_entry - | Single of Evd.side_effects Declare.proof_entry - | Mutual of Evd.side_effects Declare.proof_entry - - type t = - { entry : et - ; info : Info.t - } - - (* XXX: Refactor this with the code in - [ComFixpoint.declare_fixpoint_generic] *) + (* XXX: Refactor this with the code in [DeclareDef.declare_mutdef] *) let guess_decreasing env possible_indexes ((body, ctx), eff) = let open Constr in match Constr.kind body with @@ -221,74 +210,55 @@ end = struct (mkFix ((indexes,0),fixdecls), ctx), eff | _ -> (body, ctx), eff - let adjust_guardness_conditions ~info const = - let entry = match info.Info.compute_guard with - | [] -> - (* Not a recursive statement *) - Single const - | possible_indexes -> - (* Try all combinations... not optimal *) - let env = Global.env() in - let pe = Declare.Internal.map_entry_body const - ~f:(guess_decreasing env possible_indexes) - in - Mutual pe - in { entry; info } - - let rec select_body i t = + let select_body i t = let open Constr in match Constr.kind t with | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) | CoFix (0,decls) -> mkCoFix (i,decls) - | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, select_body i t2) - | Lambda(na,ty,t) -> mkLambda(na,ty, select_body i t) - | App (t, args) -> mkApp (select_body i t, args) | _ -> CErrors.anomaly Pp.(str "Not a proof by induction: " ++ Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".") - let declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind ~name ?typ ~impargs ~info mutpe i = - let { Info.hook; compute_guard; scope; kind; _ } = info in - match mutpe with - | NoBody pe -> - DeclareDef.declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe - | Single pe -> - (* We'd like to do [assert (i = 0)] here, however this codepath - is used when declaring mutual cofixpoints *) - DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe - | Mutual pe -> - (* if typ = None , we don't touch the type; used in the base case *) - let pe = - match typ with - | None -> pe - | Some typ -> - Declare.Internal.map_entry_type pe ~f:(fun _ -> Some typ) - in - let pe = Declare.Internal.map_entry_body pe - ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) in - DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe - - let declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind ~name { entry; info } = - (* At some point make this a single iteration *) - (* At some point make this a single iteration *) - (* impargs here are special too, fixed in upcoming PRs *) - let impargs = info.Info.impargs in - let r = declare_mutdef ?fix_exn ~info ~ubind ?hook_data ~uctx ~name ~impargs entry 0 in - (* Before we used to do this, check if that's right *) - let ubind = UnivNames.empty_binders in - let rs = - List.map_i ( - fun i { DeclareDef.Recthm.name; typ; impargs } -> - declare_mutdef ?fix_exn ~name ~info ~ubind ?hook_data ~uctx ~typ ~impargs entry i) 1 info.Info.other_thms - in r :: rs - - let declare_variable ~info ~uctx ~ubind ~name pe = - declare_mutdef ~uctx ~ubind ~name { entry = NoBody pe; info } - - let declare_mutdef ~info ?fix_exn ~uctx ?hook_data ~ubind ~name const = - let mutpe = adjust_guardness_conditions ~info const in - declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind ~name mutpe + let declare_mutdef ~uctx ~info pe i DeclareDef.Recthm.{ name; impargs; typ; _} = + let { Info.hook; scope; kind; compute_guard; _ } = info in + (* if i = 0 , we don't touch the type; this is for compat + but not clear it is the right thing to do. + *) + let pe, ubind = + if i > 0 && not (CList.is_empty compute_guard) + then Declare.Internal.map_entry_type pe ~f:(fun _ -> Some typ), UnivNames.empty_binders + else pe, UState.universe_binders uctx + in + (* We when compute_guard was [] in the previous step we should not + substitute the body *) + let pe = match compute_guard with + | [] -> pe + | _ -> + Declare.Internal.map_entry_body pe + ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) + in + DeclareDef.declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe + + let declare_mutdef ~info ~uctx const = + let pe = match info.Info.compute_guard with + | [] -> + (* Not a recursive statement *) + const + | possible_indexes -> + (* Try all combinations... not optimal *) + let env = Global.env() in + Declare.Internal.map_entry_body const + ~f:(guess_decreasing env possible_indexes) + in + List.map_i (declare_mutdef ~info ~uctx pe) 0 info.Info.thms + + let declare_variable ~info ~uctx pe = + let { Info.scope; hook } = info in + List.map_i ( + fun i { DeclareDef.Recthm.name; typ; impargs } -> + DeclareDef.declare_assumption ~name ~scope ~hook ~impargs ~uctx pe + ) 0 info.Info.thms end @@ -316,14 +286,13 @@ let compute_proof_using_for_admitted proof typ pproofs = Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) | _ -> None -let finish_admitted ~name ~info ~uctx pe = - let ubind = UnivNames.empty_binders in - let _r : Names.GlobRef.t list = MutualEntry.declare_variable ~info ~uctx ~ubind ~name pe in +let finish_admitted ~info ~uctx pe = + let _r : Names.GlobRef.t list = MutualEntry.declare_variable ~info ~uctx pe in () let save_lemma_admitted ~(lemma : t) : unit = let udecl = Proof_global.get_universe_decl lemma.proof in - let Proof.{ name; poly; entry } = Proof.data (Proof_global.get_proof lemma.proof) in + let Proof.{ poly; entry } = Proof.data (Proof_global.get_proof lemma.proof) in let typ = match Proofview.initial_goals entry with | [typ] -> snd typ | _ -> CErrors.anomaly ~label:"Lemmas.save_lemma_admitted" (Pp.str "more than one statement.") @@ -332,48 +301,26 @@ let save_lemma_admitted ~(lemma : t) : unit = let proof = Proof_global.get_proof lemma.proof in let pproofs = Proof.partial_proof proof in let sec_vars = compute_proof_using_for_admitted lemma.proof typ pproofs in - let universes = Proof_global.get_initial_euctx lemma.proof in - let ctx = UState.check_univ_decl ~poly universes udecl in - finish_admitted ~name ~info:lemma.info ~uctx:universes (sec_vars, (typ, ctx), None) + let uctx = Proof_global.get_initial_euctx lemma.proof in + let univs = UState.check_univ_decl ~poly uctx udecl in + finish_admitted ~info:lemma.info ~uctx (sec_vars, (typ, univs), None) (************************************************************************) (* Saving a lemma-like constant *) (************************************************************************) -let default_thm_id = Id.of_string "Unnamed_thm" - -let check_anonymity id save_ident = - if not (String.equal (Nameops.atompart_of_id id) (Id.to_string (default_thm_id))) then - CErrors.user_err Pp.(str "This command can only be used for unnamed theorem.") - -let finish_proved idopt po info = +let finish_proved po info = let open Proof_global in - let { Info.hook } = info in match po with - | { name; entries=[const]; uctx; udecl } -> - let name = match idopt with - | None -> name - | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in - let fix_exn = Declare.Internal.get_fix_exn const in - let () = try - let hook_data = Option.map (fun hook -> hook, uctx, []) hook in - let ubind = UState.universe_binders uctx in - let _r : Names.GlobRef.t list = - MutualEntry.declare_mutdef ~info ~fix_exn ~uctx ?hook_data ~ubind ~name const - in () - with e when CErrors.noncritical e -> - let e = Exninfo.capture e in - Exninfo.iraise (fix_exn e) - in () + | { entries=[const]; uctx } -> + let _r : Names.GlobRef.t list = MutualEntry.declare_mutdef ~info ~uctx const in + () | _ -> CErrors.anomaly ~label:"finish_proved" Pp.(str "close_proof returned more than one proof term") -let finish_derived ~f ~name ~idopt ~entries = +let finish_derived ~f ~name ~entries = (* [f] and [name] correspond to the proof of [f] and of [suchthat], respectively. *) - if Option.has_some idopt then - CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name."); - let f_def, lemma_def = match entries with | [_;f_def;lemma_def] -> @@ -406,11 +353,11 @@ let finish_derived ~f ~name ~idopt ~entries = let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in () -let finish_proved_equations lid kind proof_obj hook i types wits sigma0 = +let finish_proved_equations ~kind ~hook i proof_obj types sigma0 = let obls = ref 1 in let sigma, recobls = - CList.fold_left2_map (fun sigma (wit, (evar_env, ev, evi, local_context, type_)) entry -> + CList.fold_left2_map (fun sigma (_evar_env, ev, _evi, local_context, _type) entry -> let id = match Evd.evar_ident ev sigma0 with | Some id -> id @@ -421,34 +368,51 @@ let finish_proved_equations lid kind proof_obj hook i types wits sigma0 = let sigma, app = Evarutil.new_global sigma (GlobRef.ConstRef cst) in let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in sigma, cst) sigma0 - (CList.combine (List.rev !wits) types) proof_obj.Proof_global.entries + types proof_obj.Proof_global.entries in hook recobls sigma -let finalize_proof idopt proof_obj proof_info = +let finalize_proof proof_obj proof_info = let open Proof_global in let open Proof_ending in match CEphemeron.default proof_info.Info.proof_ending Regular with | Regular -> - finish_proved idopt proof_obj proof_info + finish_proved proof_obj proof_info | End_obligation oinfo -> DeclareObl.obligation_terminator proof_obj.entries proof_obj.uctx oinfo | End_derive { f ; name } -> - finish_derived ~f ~name ~idopt ~entries:proof_obj.entries - | End_equations { hook; i; types; wits; sigma } -> - finish_proved_equations idopt proof_info.Info.kind proof_obj hook i types wits sigma + finish_derived ~f ~name ~entries:proof_obj.entries + | End_equations { hook; i; types; sigma } -> + finish_proved_equations ~kind:proof_info.Info.kind ~hook i proof_obj types sigma + +let err_save_forbidden_in_place_of_qed () = + CErrors.user_err (Pp.str "Cannot use Save with more than one constant or in this proof mode") + +let process_idopt_for_save ~idopt info = + match idopt with + | None -> info + | Some { CAst.v = save_name } -> + (* Save foo was used; we override the info in the first theorem *) + let thms = + match info.Info.thms, CEphemeron.default info.Info.proof_ending Proof_ending.Regular with + | [ { DeclareDef.Recthm.name; _} as decl ], Proof_ending.Regular -> + [ { decl with DeclareDef.Recthm.name = save_name } ] + | _ -> + err_save_forbidden_in_place_of_qed () + in { info with Info.thms } let save_lemma_proved ~lemma ~opaque ~idopt = (* Env and sigma are just used for error printing in save_remaining_recthms *) - let proof_obj = Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) lemma.proof in - finalize_proof idopt proof_obj lemma.info + let proof_obj = Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false lemma.proof in + let proof_info = process_idopt_for_save ~idopt lemma.info in + finalize_proof proof_obj proof_info (***********************************************************************) (* Special case to close a lemma without forcing a proof *) (***********************************************************************) let save_lemma_admitted_delayed ~proof ~info = let open Proof_global in - let { name; entries; uctx; udecl } = proof in + let { entries; uctx } = proof in if List.length entries <> 1 then CErrors.user_err Pp.(str "Admitted does not support multiple statements"); let { Declare.proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in @@ -460,6 +424,14 @@ let save_lemma_admitted_delayed ~proof ~info = | Some typ -> typ in let ctx = UState.univ_entry ~poly uctx in let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in - finish_admitted ~name ~uctx ~info (sec_vars, (typ, ctx), None) - -let save_lemma_proved_delayed ~proof ~info ~idopt = finalize_proof idopt proof info + finish_admitted ~uctx ~info (sec_vars, (typ, ctx), None) + +let save_lemma_proved_delayed ~proof ~info ~idopt = + (* vio2vo calls this but with invalid info, we have to workaround + that to add the name to the info structure *) + if CList.is_empty info.Info.thms then + let info = add_first_thm ~info ~name:proof.Proof_global.name ~typ:EConstr.mkSet ~impargs:[] in + finalize_proof proof info + else + let info = process_idopt_for_save ~idopt info in + finalize_proof proof info diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 6a1f8c09f3..8a23daa85f 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -35,12 +35,12 @@ module Proof_ending : sig | Regular | End_obligation of DeclareObl.obligation_qed_info | End_derive of { f : Id.t; name : Id.t } - | End_equations of { hook : Constant.t list -> Evd.evar_map -> unit - ; i : Id.t - ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list - ; wits : EConstr.t list ref - ; sigma : Evd.evar_map - } + | End_equations of + { hook : Constant.t list -> Evd.evar_map -> unit + ; i : Id.t + ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list + ; sigma : Evd.evar_map + } end @@ -68,6 +68,7 @@ val start_lemma -> poly:bool -> ?udecl:UState.universe_decl -> ?info:Info.t + -> ?impargs:Impargs.manual_implicits -> Evd.evar_map -> EConstr.types -> t @@ -95,8 +96,6 @@ val start_lemma_with_initialization -> int list option -> t -val default_thm_id : Names.Id.t - (** {4 Saving proofs} *) val save_lemma_admitted : lemma:t -> unit diff --git a/vernac/library.ml b/vernac/library.ml index 85645b92d4..1b0bd4c0f7 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -103,17 +103,13 @@ type library_summary = { libsum_digests : Safe_typing.vodigest; } -module LibraryOrdered = DirPath -module LibraryMap = Map.Make(LibraryOrdered) -module LibraryFilenameMap = Map.Make(LibraryOrdered) - (* This is a map from names to loaded libraries *) -let libraries_table : library_summary LibraryMap.t ref = - Summary.ref LibraryMap.empty ~name:"LIBRARY" +let libraries_table : library_summary DPmap.t ref = + Summary.ref DPmap.empty ~name:"LIBRARY" (* This is the map of loaded libraries filename *) (* (not synchronized so as not to be caught in the states on disk) *) -let libraries_filename_table = ref LibraryFilenameMap.empty +let libraries_filename_table = ref DPmap.empty (* These are the _ordered_ sets of loaded, imported and exported libraries *) let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD" @@ -121,7 +117,7 @@ let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD" (* various requests to the tables *) let find_library dir = - LibraryMap.find dir !libraries_table + DPmap.find dir !libraries_table let try_find_library dir = try find_library dir @@ -133,16 +129,16 @@ let register_library_filename dir f = (* Not synchronized: overwrite the previous binding if one existed *) (* from a previous play of the session *) libraries_filename_table := - LibraryFilenameMap.add dir f !libraries_filename_table + DPmap.add dir f !libraries_filename_table let library_full_filename dir = - try LibraryFilenameMap.find dir !libraries_filename_table + try DPmap.find dir !libraries_filename_table with Not_found -> "<unavailable filename>" let overwrite_library_filenames f = let f = if Filename.is_relative f then Filename.concat (Sys.getcwd ()) f else f in - LibraryMap.iter (fun dir _ -> register_library_filename dir f) + DPmap.iter (fun dir _ -> register_library_filename dir f) !libraries_table let library_is_loaded dir = @@ -159,15 +155,16 @@ let register_loaded_library m = let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in let f = prefix ^ "cmo" in let f = Dynlink.adapt_filename f in - if Coq_config.native_compiler then - Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f + Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f in let rec aux = function - | [] -> link (); [libname] + | [] -> + let () = if Flags.get_native_compiler () then link () in + [libname] | m'::_ as l when DirPath.equal m' libname -> l | m'::l' -> m' :: aux l' in libraries_loaded_list := aux !libraries_loaded_list; - libraries_table := LibraryMap.add libname m !libraries_table + libraries_table := DPmap.add libname m !libraries_table let loaded_libraries () = !libraries_loaded_list @@ -187,13 +184,13 @@ type 'a table_status = | Fetched of 'a array let opaque_tables = - ref (LibraryMap.empty : (Opaqueproof.opaque_proofterm table_status) LibraryMap.t) + ref (DPmap.empty : (Opaqueproof.opaque_proofterm table_status) DPmap.t) let add_opaque_table dp st = - opaque_tables := LibraryMap.add dp st !opaque_tables + opaque_tables := DPmap.add dp st !opaque_tables let access_table what tables dp i = - let t = match LibraryMap.find dp !tables with + let t = match DPmap.find dp !tables with | Fetched t -> t | ToFetch f -> let dir_path = Names.DirPath.to_string dp in @@ -206,7 +203,7 @@ let access_table what tables dp i = str ") is inaccessible or corrupted,\ncannot load some " ++ str what ++ str " in it.\n") in - tables := LibraryMap.add dp (Fetched t) !tables; + tables := DPmap.add dp (Fetched t) !tables; t in assert (i < Array.length t); t.(i) @@ -261,14 +258,12 @@ let intern_from_file f = | Some (_,false) -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty -module DPMap = Map.Make(DirPath) - let rec intern_library ~lib_resolver (needed, contents) (dir, f) from = (* Look if in the current logical environment *) try (find_library dir).libsum_digests, (needed, contents) with Not_found -> (* Look if already listed and consequently its dependencies too *) - try (DPMap.find dir contents).library_digests, (needed, contents) + try (DPmap.find dir contents).library_digests, (needed, contents) with Not_found -> Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); (* [dir] is an absolute name which matches [f] which must be in loadpath *) @@ -286,7 +281,7 @@ and intern_library_deps ~lib_resolver libs dir m from = let needed, contents = Array.fold_left (intern_mandatory_library ~lib_resolver dir from) libs m.library_deps in - (dir :: needed, DPMap.add dir m contents ) + (dir :: needed, DPmap.add dir m contents ) and intern_mandatory_library ~lib_resolver caller from libs (dir,d) = let digest, libs = intern_library ~lib_resolver libs (dir, None) (Some from) in @@ -372,8 +367,8 @@ let warn_require_in_module = strbrk "and optionally Import it inside another one.") let require_library_from_dirpath ~lib_resolver modrefl export = - let needed, contents = List.fold_left (rec_intern_library ~lib_resolver) ([], DPMap.empty) modrefl in - let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in + let needed, contents = List.fold_left (rec_intern_library ~lib_resolver) ([], DPmap.empty) modrefl in + let needed = List.rev_map (fun dir -> DPmap.find dir contents) needed in let modrefl = List.map fst modrefl in if Lib.is_module_or_modtype () then begin @@ -500,14 +495,11 @@ let save_library_to todo_proofs ~output_native_objects dir f otab = let save_library_raw f sum lib univs proofs = save_library_base f sum lib (Some univs) None proofs -module StringOrd = struct type t = string let compare = String.compare end -module StringSet = Set.Make(StringOrd) - let get_used_load_paths () = - StringSet.elements - (List.fold_left (fun acc m -> StringSet.add + String.Set.elements + (List.fold_left (fun acc m -> String.Set.add (Filename.dirname (library_full_filename m)) acc) - StringSet.empty !libraries_loaded_list) + String.Set.empty !libraries_loaded_list) let _ = Nativelib.get_load_paths := get_used_load_paths diff --git a/vernac/obligations.ml b/vernac/obligations.ml index a29ba44907..435085793c 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -10,252 +10,16 @@ open Printf -(** - - Get types of existentials ; - - Flatten dependency tree (prefix order) ; - - Replace existentials by de Bruijn indices in term, applied to the right arguments ; - - Apply term prefixed by quantification on "existentials". -*) - -open Constr open Names open Pp open CErrors open Util -module NamedDecl = Context.Named.Declaration - (* For the records fields, opens should go away one these types are private *) open DeclareObl open DeclareObl.Obligation open DeclareObl.ProgramDecl -let succfix (depth, fixrels) = - (succ depth, List.map succ fixrels) - -let check_evars env evm = - Evar.Map.iter - (fun key evi -> - if Evd.is_obligation_evar evm key then () - else - let (loc,k) = Evd.evar_source key evm in - Pretype_errors.error_unsolvable_implicit ?loc env evm key None) - (Evd.undefined_map evm) - -type oblinfo = - { ev_name: int * Id.t; - ev_hyps: EConstr.named_context; - ev_status: bool * Evar_kinds.obligation_definition_status; - ev_chop: int option; - ev_src: Evar_kinds.t Loc.located; - ev_typ: types; - ev_tac: unit Proofview.tactic option; - ev_deps: Int.Set.t } - -(** Substitute evar references in t using de Bruijn indices, - where n binders were passed through. *) - -let subst_evar_constr evm evs n idf t = - let seen = ref Int.Set.empty in - let transparent = ref Id.Set.empty in - let evar_info id = List.assoc_f Evar.equal id evs in - let rec substrec (depth, fixrels) c = match EConstr.kind evm c with - | Evar (k, args) -> - let { ev_name = (id, idstr) ; - ev_hyps = hyps ; ev_chop = chop } = - try evar_info k - with Not_found -> - anomaly ~label:"eterm" (Pp.str "existential variable " ++ int (Evar.repr k) ++ str " not found.") - in - seen := Int.Set.add id !seen; - (* Evar arguments are created in inverse order, - and we must not apply to defined ones (i.e. LetIn's) - *) - let args = - let n = match chop with None -> 0 | Some c -> c in - let (l, r) = List.chop n (List.rev (Array.to_list args)) in - List.rev r - in - let args = - let rec aux hyps args acc = - let open Context.Named.Declaration in - match hyps, args with - (LocalAssum _ :: tlh), (c :: tla) -> - aux tlh tla ((substrec (depth, fixrels) c) :: acc) - | (LocalDef _ :: tlh), (_ :: tla) -> - aux tlh tla acc - | [], [] -> acc - | _, _ -> acc (*failwith "subst_evars: invalid argument"*) - in aux hyps args [] - in - if List.exists - (fun x -> match EConstr.kind evm x with - | Rel n -> Int.List.mem n fixrels - | _ -> false) args - then - transparent := Id.Set.add idstr !transparent; - EConstr.mkApp (idf idstr, Array.of_list args) - | Fix _ -> - EConstr.map_with_binders evm succfix substrec (depth, 1 :: fixrels) c - | _ -> EConstr.map_with_binders evm succfix substrec (depth, fixrels) c - in - let t' = substrec (0, []) t in - EConstr.to_constr evm t', !seen, !transparent - - -(** Substitute variable references in t using de Bruijn indices, - where n binders were passed through. *) -let subst_vars acc n t = - let var_index id = Util.List.index Id.equal id acc in - let rec substrec depth c = match Constr.kind c with - | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c) - | _ -> Constr.map_with_binders succ substrec depth c - in - substrec 0 t - -(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ]) - to a product : forall H1 : t1, ..., forall Hn : tn, concl. - Changes evars and hypothesis references to variable references. -*) -let etype_of_evar evm evs hyps concl = - let open Context.Named.Declaration in - let rec aux acc n = function - decl :: tl -> - let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar (NamedDecl.get_type decl) in - let t'' = subst_vars acc 0 t' in - let rest, s', trans' = aux (NamedDecl.get_id decl :: acc) (succ n) tl in - let s' = Int.Set.union s s' in - let trans' = Id.Set.union trans trans' in - (match decl with - | LocalDef (id,c,_) -> - let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in - let c' = subst_vars acc 0 c' in - Term.mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest, - Int.Set.union s'' s', - Id.Set.union trans'' trans' - | LocalAssum (id,_) -> - Term.mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans') - | [] -> - let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in - subst_vars acc 0 t', s, trans - in aux [] 0 (List.rev hyps) - -let trunc_named_context n ctx = - let len = List.length ctx in - List.firstn (len - n) ctx - -let rec chop_product n t = - let pop t = Vars.lift (-1) t in - if Int.equal n 0 then Some t - else - match Constr.kind t with - | Prod (_, _, b) -> if Vars.noccurn 1 b then chop_product (pred n) (pop b) else None - | _ -> None - -let evar_dependencies evm oev = - let one_step deps = - Evar.Set.fold (fun ev s -> - let evi = Evd.find evm ev in - let deps' = Evd.evars_of_filtered_evar_info evm evi in - if Evar.Set.mem oev deps' then - invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ Pp.string_of_ppcmds @@ Evar.print oev) - else Evar.Set.union deps' s) - deps deps - in - let rec aux deps = - let deps' = one_step deps in - if Evar.Set.equal deps deps' then deps - else aux deps' - in aux (Evar.Set.singleton oev) - -let move_after (id, ev, deps as obl) l = - let rec aux restdeps = function - | (id', _, _) as obl' :: tl -> - let restdeps' = Evar.Set.remove id' restdeps in - if Evar.Set.is_empty restdeps' then - obl' :: obl :: tl - else obl' :: aux restdeps' tl - | [] -> [obl] - in aux (Evar.Set.remove id deps) l - -let sort_dependencies evl = - let rec aux l found list = - match l with - | (id, ev, deps) as obl :: tl -> - let found' = Evar.Set.union found (Evar.Set.singleton id) in - if Evar.Set.subset deps found' then - aux tl found' (obl :: list) - else aux (move_after obl tl) found list - | [] -> List.rev list - in aux evl Evar.Set.empty [] - -let eterm_obligations env name evm fs ?status t ty = - (* 'Serialize' the evars *) - let nc = Environ.named_context env in - let nc_len = Context.Named.length nc in - let evm = Evarutil.nf_evar_map_undefined evm in - let evl = Evarutil.non_instantiated evm in - let evl = Evar.Map.bindings evl in - let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in - let sevl = sort_dependencies evl in - let evl = List.map (fun (id, ev, _) -> id, ev) sevl in - let evn = - let i = ref (-1) in - List.rev_map (fun (id, ev) -> incr i; - (id, (!i, Id.of_string - (Id.to_string name ^ "_obligation_" ^ string_of_int (succ !i))), - ev)) evl - in - let evts = - (* Remove existential variables in types and build the corresponding products *) - List.fold_right - (fun (id, (n, nstr), ev) l -> - let hyps = Evd.evar_filtered_context ev in - let hyps = trunc_named_context nc_len hyps in - let evtyp, deps, transp = etype_of_evar evm l hyps ev.Evd.evar_concl in - let evtyp, hyps, chop = - match chop_product fs evtyp with - | Some t -> t, trunc_named_context fs hyps, fs - | None -> evtyp, hyps, 0 - in - let loc, k = Evd.evar_source id evm in - let status = match k with - | Evar_kinds.QuestionMark { Evar_kinds.qm_obligation=o } -> o - | _ -> match status with - | Some o -> o - | None -> Evar_kinds.Define (not (Program.get_proofs_transparency ())) - in - let force_status, status, chop = match status with - | Evar_kinds.Define true as stat -> - if not (Int.equal chop fs) then true, Evar_kinds.Define false, None - else false, stat, Some chop - | s -> false, s, None - in - let info = { ev_name = (n, nstr); - ev_hyps = hyps; ev_status = force_status, status; ev_chop = chop; - ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = None } - in (id, info) :: l) - evn [] - in - let t', _, transparent = (* Substitute evar refs in the term by variables *) - subst_evar_constr evm evts 0 EConstr.mkVar t - in - let ty, _, _ = subst_evar_constr evm evts 0 EConstr.mkVar ty in - let evars = - List.map (fun (ev, info) -> - let { ev_name = (_, name); ev_status = force_status, status; - ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info - in - let force_status, status = match status with - | Evar_kinds.Define true when Id.Set.mem name transparent -> - true, Evar_kinds.Define false - | _ -> force_status, status - in name, typ, src, (force_status, status), deps, tac) evts - in - let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in - let evmap f c = pi1 (subst_evar_constr evm evts 0 f c) in - Array.of_list (List.rev evars), (evnames, evmap), t', ty - let pperror cmd = CErrors.user_err ~hdr:"Program" cmd let error s = pperror (str s) @@ -270,11 +34,6 @@ let explain_no_obligations = function Some ident -> str "No obligations for program " ++ Id.print ident | None -> str "No obligations remaining" -type obligation_info = - (Names.Id.t * types * Evar_kinds.t Loc.located * - (bool * Evar_kinds.obligation_definition_status) - * Int.Set.t * unit Proofview.tactic option) array - let assumption_message = Declare.assumption_message let default_tactic = ref (Proofview.tclUNIT ()) @@ -571,12 +330,12 @@ let add_definition ~name ?term t ~uctx ?(udecl=UState.default_univ_decl) let add_mutual_definitions l ~uctx ?(udecl=UState.default_univ_decl) ?tactic ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce) ?hook ?(opaque = false) notations fixkind = - let deps = List.map (fun (n, b, t, imps, obls) -> n) l in + let deps = List.map (fun ({ DeclareDef.Recthm.name; _ }, _, _) -> name) l in List.iter - (fun (n, b, t, impargs, obls) -> - let prg = ProgramDecl.make ~opaque n ~udecl (Some b) t ~uctx deps (Some fixkind) + (fun ({ DeclareDef.Recthm.name; typ; impargs; _ }, b, obls) -> + let prg = ProgramDecl.make ~opaque name ~udecl (Some b) typ ~uctx deps (Some fixkind) notations obls ~impargs ~poly ~scope ~kind reduce ?hook - in progmap_add n (CEphemeron.create prg)) l; + in progmap_add name (CEphemeron.create prg)) l; let _defined = List.fold_left (fun finished x -> if finished then finished diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 101958072a..f42d199e18 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -8,51 +8,73 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Environ open Constr -open Evd -open Names - -val check_evars : env -> evar_map -> unit - -val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t -val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar_info * Evar.Set.t) list - -(* ident, type, location, (opaque or transparent, expand or define), dependencies, tactic to solve it *) -type obligation_info = - (Id.t * types * Evar_kinds.t Loc.located * - (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array - -(* env, id, evars, number of function prototypes to try to clear from - evars contexts, object and type *) -val eterm_obligations - : env - -> Id.t - -> evar_map - -> int - -> ?status:Evar_kinds.obligation_definition_status - -> EConstr.constr - -> EConstr.types - -> obligation_info * - - (* Existential key, obl. name, type as product, location of the - original evar, associated tactic, status and dependencies as - indexes into the array *) - ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) * - - (* Translations from existential identifiers to obligation - identifiers and for terms with existentials to closed terms, - given a translation from obligation identifiers to constrs, - new term, new type *) - constr * types + +(** Coq's Program mode support. This mode extends declarations of + constants and fixpoints with [Program Definition] and [Program + Fixpoint] to support incremental construction of terms using + delayed proofs, called "obligations" + + The mode also provides facilities for managing and auto-solving + sets of obligations. + + The basic code flow of programs/obligations is as follows: + + - [add_definition] / [add_mutual_definitions] are called from the + respective [Program] vernacular command interpretation; at this + point the only extra work we do is to prepare the new definition + [d] using [RetrieveObl], which consists in turning unsolved evars + into obligations. [d] is not sent to the kernel yet, as it is not + complete and cannot be typchecked, but saved in a special + data-structure. Auto-solving of obligations is tried at this stage + (see below) + + - [next_obligation] will retrieve the next obligation + ([RetrieveObl] sorts them by topological order) and will try to + solve it. When all obligations are solved, the original constant + [d] is grounded and sent to the kernel for addition to the global + environment. Auto-solving of obligations is also triggered on + obligation completion. + +{2} Solving of obligations: Solved obligations are stored as regular + global declarations in the global environment, usually with name + [constant_obligation_number] where [constant] is the original + [constant] and [number] is the corresponding (internal) number. + + Solving an obligation can trigger a bit of a complex cascaded + callback path; closing an obligation can indeed allow all other + obligations to be closed, which in turn may trigged the declaration + of the original constant. Care must be taken, as this can modify + [Global.env] in arbitrarily ways. Current code takes some care to + refresh the [env] in the proper boundaries, but the invariants + remain delicate. + +{2} Saving of obligations: as open obligations use the regular proof + mode, a `Qed` will call `Lemmas.save_lemma` first. For this reason + obligations code is split in two: this file, [Obligations], taking + care of the top-level vernac commands, and [DeclareObl], which is + called by `Lemmas` to close an obligation proof and eventually to + declare the top-level [Program]ed constant. + + There is little obligations-specific code in [DeclareObl], so + eventually that file should be integrated in the regular [Declare] + path, as it gains better support for "dependent_proofs". + + *) val default_tactic : unit Proofview.tactic ref -val add_definition - : name:Names.Id.t - -> ?term:constr -> types +(** Start a [Program Definition c] proof. [uctx] [udecl] [impargs] + [kind] [scope] [poly] etc... come from the interpretation of the + vernacular; `obligation_info` was generated by [RetrieveObl] It + will return whether all the obligations were solved; if so, it will + also register [c] with the kernel. *) +val add_definition : + name:Names.Id.t + -> ?term:constr + -> types -> uctx:UState.t - -> ?udecl:UState.universe_decl (* Universe binders and constraints *) + -> ?udecl:UState.universe_decl (** Universe binders and constraints *) -> ?impargs:Impargs.manual_implicits -> poly:bool -> ?scope:DeclareDef.locality @@ -61,52 +83,56 @@ val add_definition -> ?reduce:(constr -> constr) -> ?hook:DeclareDef.Hook.t -> ?opaque:bool - -> obligation_info + -> RetrieveObl.obligation_info -> DeclareObl.progress -val add_mutual_definitions - (* XXX: unify with MutualEntry *) - : (Names.Id.t * constr * types * Impargs.manual_implicits * obligation_info) list +(* XXX: unify with MutualEntry *) + +(** Start a [Program Fixpoint] declaration, similar to the above, + except it takes a list now. *) +val add_mutual_definitions : + (DeclareDef.Recthm.t * Constr.t * RetrieveObl.obligation_info) list -> uctx:UState.t - -> ?udecl:UState.universe_decl - (** Universe binders and constraints *) + -> ?udecl:UState.universe_decl (** Universe binders and constraints *) -> ?tactic:unit Proofview.tactic -> poly:bool -> ?scope:DeclareDef.locality -> ?kind:Decls.definition_object_kind -> ?reduce:(constr -> constr) - -> ?hook:DeclareDef.Hook.t -> ?opaque:bool + -> ?hook:DeclareDef.Hook.t + -> ?opaque:bool -> Vernacexpr.decl_notation list - -> DeclareObl.fixpoint_kind -> unit + -> DeclareObl.fixpoint_kind + -> unit -val obligation - : int * Names.Id.t option * Constrexpr.constr_expr option +(** Implementation of the [Obligation] command *) +val obligation : + int * Names.Id.t option * Constrexpr.constr_expr option -> Genarg.glob_generic_argument option -> Lemmas.t -val next_obligation - : Names.Id.t option - -> Genarg.glob_generic_argument option - -> Lemmas.t +(** Implementation of the [Next Obligation] command *) +val next_obligation : + Names.Id.t option -> Genarg.glob_generic_argument option -> Lemmas.t -val solve_obligations : Names.Id.t option -> unit Proofview.tactic option - -> DeclareObl.progress -(* Number of remaining obligations to be solved for this program *) +(** Implementation of the [Solve Obligation] command *) +val solve_obligations : + Names.Id.t option -> unit Proofview.tactic option -> DeclareObl.progress val solve_all_obligations : unit Proofview.tactic option -> unit -val try_solve_obligation : int -> Names.Id.t option -> unit Proofview.tactic option -> unit +(** Number of remaining obligations to be solved for this program *) +val try_solve_obligation : + int -> Names.Id.t option -> unit Proofview.tactic option -> unit -val try_solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> unit +val try_solve_obligations : + Names.Id.t option -> unit Proofview.tactic option -> unit val show_obligations : ?msg:bool -> Names.Id.t option -> unit - val show_term : Names.Id.t option -> Pp.t - val admit_obligations : Names.Id.t option -> unit exception NoObligations of Names.Id.t option val explain_no_obligations : Names.Id.t option -> Pp.t - val check_program_libraries : unit -> unit diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index a3de88d4dc..054b60853f 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -142,7 +142,7 @@ open Pputils | SearchOutside [] -> mt() | SearchOutside l -> spc() ++ keyword "outside" ++ spc() ++ prlist_with_sep sep pr_module l - let pr_search_about (b,c) = + let pr_search (b,c) = (if b then str "-" else mt()) ++ match c with | SearchSubPattern p -> @@ -158,10 +158,8 @@ open Pputils | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b - | SearchAbout sl -> - keyword "SearchAbout" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b | Search sl -> - keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b + keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search sl ++ pr_in_out_modules b let pr_option_ref_value = function | QualidRefValue id -> pr_qualid id diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index 08625b41a6..f4cb1adfe8 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -51,14 +51,13 @@ module Vernac_ = let noedit_mode = gec_vernac "noedit_command" let () = - let open Extend in let act_vernac v loc = Some v in let act_eoi _ loc = None in let rule = [ - Rule (Next (Stop, Atoken Tok.PEOI), act_eoi); - Rule (Next (Stop, Aentry vernac_control), act_vernac); + Pcoq.(Production.make (Rule.next Rule.stop (Symbol.token Tok.PEOI)) act_eoi); + Pcoq.(Production.make (Rule.next Rule.stop (Symbol.nterm vernac_control)) act_vernac); ] in - Pcoq.grammar_extend main_entry (None, [None, None, rule]) + Pcoq.(grammar_extend main_entry {pos=None; data=[None, None, rule]}) let select_tactic_entry spec = match spec with diff --git a/vernac/record.ml b/vernac/record.ml index d974ead942..b9d450044b 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -59,26 +59,37 @@ let () = optread = (fun () -> !typeclasses_unique); optwrite = (fun b -> typeclasses_unique := b); } -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 ~program_mode:false env sigma ~impls t in - let r = Retyping.relevance_of_type env sigma t' in - let sigma, b' = - Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@ - interp_casted_constr_evars_impls ~program_mode:false env sigma ~impls x t') (sigma,None) b in - let impls = - match i with - | Anonymous -> impls - | Name id -> Id.Map.add id (compute_internalization_data env sigma Constrintern.Method t' impl) impls - in - let d = match b' with - | None -> LocalAssum (make_annot i r,t') - | Some b' -> LocalDef (make_annot i r,b',t') +let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l = + let _, sigma, impls, newfs, _ = + 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 r = Retyping.relevance_of_type env sigma t' in + let sigma, b' = + Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@ + interp_casted_constr_evars_impls ~program_mode:false env sigma ~impls x t') (sigma,None) b in + let impls = + match i with + | Anonymous -> impls + | Name id -> Id.Map.add id (compute_internalization_data env sigma Constrintern.Method t' impl) impls + in + let d = match b' with + | None -> LocalAssum (make_annot i r,t') + | Some b' -> LocalDef (make_annot i r,b',t') + in + List.iter (Metasyntax.set_notation_for_interpretation env impls) no; + (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls)) + (env, sigma, [], [], impls_env) nots l + in + let _, sigma = Context.Rel.fold_outside ~init:(env,sigma) (fun f (env,sigma) -> + let sigma = RelDecl.fold_constr (fun c sigma -> + ComInductive.maybe_unify_params_in env sigma ~ninds ~nparams c) + f sigma in - List.iter (Metasyntax.set_notation_for_interpretation env impls) no; - (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls)) - (env, sigma, [], [], impls_env) nots l + EConstr.push_rel f env, sigma) + newfs + in + sigma, (impls, newfs) let compute_constructor_level evars env l = List.fold_right (fun d (env, univ) -> @@ -103,7 +114,7 @@ let check_anonymous_type ind = | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true | _ -> false -let typecheck_params_and_fields finite def poly pl ps records = +let typecheck_params_and_fields def poly pl ps records = let env0 = Global.env () in (* Special case elaboration for template-polymorphic inductives, lower bound on introduced universes is Prop so that we do not miss @@ -157,17 +168,15 @@ let typecheck_params_and_fields finite def poly pl ps records = let fold accu (id, _, _, _) arity r = EConstr.push_rel (LocalAssum (make_annot (Name id) r,arity)) accu in let env_ar = EConstr.push_rel_context newps (List.fold_left3 fold env0 records arities relevances) in - let assums = List.filter is_local_assum newps in let impls_env = - let params = List.map (RelDecl.get_name %> Name.get_id) assums in - let ty = Inductive (params, (finite != Declarations.BiFinite)) in let ids = List.map (fun (id, _, _, _) -> id) records in let imps = List.map (fun _ -> imps) arities in - compute_internalization_env env0 sigma ~impls:impls_env ty ids arities imps + compute_internalization_env env0 sigma ~impls:impls_env Inductive ids arities imps in + let ninds = List.length arities in + let nparams = List.length newps in let fold sigma (_, _, nots, fs) arity = - let _, sigma, impls, newfs, _ = interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs) in - (sigma, (impls, newfs)) + interp_fields_evars env_ar sigma ~ninds ~nparams impls_env nots (binders_of_decls fs) in let (sigma, data) = List.fold_left2_map fold sigma records arities in let sigma = @@ -702,7 +711,7 @@ let definition_structure udecl kind ~template ~cumulative ~poly finite records = let ps, data = extract_record_data records in let ubinders, univs, auto_template, params, implpars, data = States.with_state_protection (fun () -> - typecheck_params_and_fields finite (kind = Class true) poly udecl ps data) () in + typecheck_params_and_fields (kind = Class true) poly udecl ps data) () in let template = template, auto_template in match kind with | Class def -> diff --git a/vernac/retrieveObl.ml b/vernac/retrieveObl.ml new file mode 100644 index 0000000000..c529972b8d --- /dev/null +++ b/vernac/retrieveObl.ml @@ -0,0 +1,296 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names + +(** + - Get types of existentials ; + - Flatten dependency tree (prefix order) ; + - Replace existentials by de Bruijn indices in term, applied to the right arguments ; + - Apply term prefixed by quantification on "existentials". +*) + +let check_evars env evm = + Evar.Map.iter + (fun key evi -> + if Evd.is_obligation_evar evm key then () + else + let loc, k = Evd.evar_source key evm in + Pretype_errors.error_unsolvable_implicit ?loc env evm key None) + (Evd.undefined_map evm) + +type obligation_info = + ( Names.Id.t + * Constr.types + * Evar_kinds.t Loc.located + * (bool * Evar_kinds.obligation_definition_status) + * Int.Set.t + * unit Proofview.tactic option ) + array + +type oblinfo = + { ev_name : int * Id.t + ; ev_hyps : EConstr.named_context + ; ev_status : bool * Evar_kinds.obligation_definition_status + ; ev_chop : int option + ; ev_src : Evar_kinds.t Loc.located + ; ev_typ : Constr.types + ; ev_tac : unit Proofview.tactic option + ; ev_deps : Int.Set.t } + +(** Substitute evar references in t using de Bruijn indices, + where n binders were passed through. *) + +let succfix (depth, fixrels) = (succ depth, List.map succ fixrels) + +let subst_evar_constr evm evs n idf t = + let seen = ref Int.Set.empty in + let transparent = ref Id.Set.empty in + let evar_info id = CList.assoc_f Evar.equal id evs in + let rec substrec (depth, fixrels) c = + match EConstr.kind evm c with + | Constr.Evar (k, args) -> + let {ev_name = id, idstr; ev_hyps = hyps; ev_chop = chop} = + try evar_info k + with Not_found -> + CErrors.anomaly ~label:"eterm" + Pp.( + str "existential variable " + ++ int (Evar.repr k) + ++ str " not found.") + in + seen := Int.Set.add id !seen; + (* Evar arguments are created in inverse order, + and we must not apply to defined ones (i.e. LetIn's) + *) + let args = + let n = match chop with None -> 0 | Some c -> c in + let l, r = CList.chop n (List.rev (Array.to_list args)) in + List.rev r + in + let args = + let rec aux hyps args acc = + let open Context.Named.Declaration in + match (hyps, args) with + | LocalAssum _ :: tlh, c :: tla -> + aux tlh tla (substrec (depth, fixrels) c :: acc) + | LocalDef _ :: tlh, _ :: tla -> aux tlh tla acc + | [], [] -> acc + | _, _ -> acc + (*failwith "subst_evars: invalid argument"*) + in + aux hyps args [] + in + if + List.exists + (fun x -> + match EConstr.kind evm x with + | Constr.Rel n -> Int.List.mem n fixrels + | _ -> false) + args + then transparent := Id.Set.add idstr !transparent; + EConstr.mkApp (idf idstr, Array.of_list args) + | Constr.Fix _ -> + EConstr.map_with_binders evm succfix substrec (depth, 1 :: fixrels) c + | _ -> EConstr.map_with_binders evm succfix substrec (depth, fixrels) c + in + let t' = substrec (0, []) t in + (EConstr.to_constr evm t', !seen, !transparent) + +(** Substitute variable references in t using de Bruijn indices, + where n binders were passed through. *) +let subst_vars acc n t = + let var_index id = Util.List.index Id.equal id acc in + let rec substrec depth c = + match Constr.kind c with + | Constr.Var v -> ( + try Constr.mkRel (depth + var_index v) with Not_found -> c ) + | _ -> Constr.map_with_binders succ substrec depth c + in + substrec 0 t + +(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ]) + to a product : forall H1 : t1, ..., forall Hn : tn, concl. + Changes evars and hypothesis references to variable references. +*) +let etype_of_evar evm evs hyps concl = + let open Context.Named.Declaration in + let rec aux acc n = function + | decl :: tl -> ( + let t', s, trans = + subst_evar_constr evm evs n EConstr.mkVar + (Context.Named.Declaration.get_type decl) + in + let t'' = subst_vars acc 0 t' in + let rest, s', trans' = + aux (Context.Named.Declaration.get_id decl :: acc) (succ n) tl + in + let s' = Int.Set.union s s' in + let trans' = Id.Set.union trans trans' in + match decl with + | LocalDef (id, c, _) -> + let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in + let c' = subst_vars acc 0 c' in + ( Term.mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest + , Int.Set.union s'' s' + , Id.Set.union trans'' trans' ) + | LocalAssum (id, _) -> + (Term.mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans') ) + | [] -> + let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in + (subst_vars acc 0 t', s, trans) + in + aux [] 0 (List.rev hyps) + +let trunc_named_context n ctx = + let len = List.length ctx in + CList.firstn (len - n) ctx + +let rec chop_product n t = + let pop t = Vars.lift (-1) t in + if Int.equal n 0 then Some t + else + match Constr.kind t with + | Constr.Prod (_, _, b) -> + if Vars.noccurn 1 b then chop_product (pred n) (pop b) else None + | _ -> None + +let evar_dependencies evm oev = + let one_step deps = + Evar.Set.fold + (fun ev s -> + let evi = Evd.find evm ev in + let deps' = Evd.evars_of_filtered_evar_info evm evi in + if Evar.Set.mem oev deps' then + invalid_arg + ( "Ill-formed evar map: cycle detected for evar " + ^ Pp.string_of_ppcmds @@ Evar.print oev ) + else Evar.Set.union deps' s) + deps deps + in + let rec aux deps = + let deps' = one_step deps in + if Evar.Set.equal deps deps' then deps else aux deps' + in + aux (Evar.Set.singleton oev) + +let move_after ((id, ev, deps) as obl) l = + let rec aux restdeps = function + | ((id', _, _) as obl') :: tl -> + let restdeps' = Evar.Set.remove id' restdeps in + if Evar.Set.is_empty restdeps' then obl' :: obl :: tl + else obl' :: aux restdeps' tl + | [] -> [obl] + in + aux (Evar.Set.remove id deps) l + +let sort_dependencies evl = + let rec aux l found list = + match l with + | ((id, ev, deps) as obl) :: tl -> + let found' = Evar.Set.union found (Evar.Set.singleton id) in + if Evar.Set.subset deps found' then aux tl found' (obl :: list) + else aux (move_after obl tl) found list + | [] -> List.rev list + in + aux evl Evar.Set.empty [] + +let retrieve_obligations env name evm fs ?status t ty = + (* 'Serialize' the evars *) + let nc = Environ.named_context env in + let nc_len = Context.Named.length nc in + let evm = Evarutil.nf_evar_map_undefined evm in + let evl = Evarutil.non_instantiated evm in + let evl = Evar.Map.bindings evl in + let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in + let sevl = sort_dependencies evl in + let evl = List.map (fun (id, ev, _) -> (id, ev)) sevl in + let evn = + let i = ref (-1) in + List.rev_map + (fun (id, ev) -> + incr i; + ( id + , ( !i + , Id.of_string + (Id.to_string name ^ "_obligation_" ^ string_of_int (succ !i)) ) + , ev )) + evl + in + let evts = + (* Remove existential variables in types and build the corresponding products *) + List.fold_right + (fun (id, (n, nstr), ev) l -> + let hyps = Evd.evar_filtered_context ev in + let hyps = trunc_named_context nc_len hyps in + let evtyp, deps, transp = etype_of_evar evm l hyps ev.Evd.evar_concl in + let evtyp, hyps, chop = + match chop_product fs evtyp with + | Some t -> (t, trunc_named_context fs hyps, fs) + | None -> (evtyp, hyps, 0) + in + let loc, k = Evd.evar_source id evm in + let status = + match k with + | Evar_kinds.QuestionMark {Evar_kinds.qm_obligation = o} -> o + | _ -> ( + match status with + | Some o -> o + | None -> + Evar_kinds.Define (not (Program.get_proofs_transparency ())) ) + in + let force_status, status, chop = + match status with + | Evar_kinds.Define true as stat -> + if not (Int.equal chop fs) then (true, Evar_kinds.Define false, None) + else (false, stat, Some chop) + | s -> (false, s, None) + in + let info = + { ev_name = (n, nstr) + ; ev_hyps = hyps + ; ev_status = (force_status, status) + ; ev_chop = chop + ; ev_src = (loc, k) + ; ev_typ = evtyp + ; ev_deps = deps + ; ev_tac = None } + in + (id, info) :: l) + evn [] + in + let t', _, transparent = + (* Substitute evar refs in the term by variables *) + subst_evar_constr evm evts 0 EConstr.mkVar t + in + let ty, _, _ = subst_evar_constr evm evts 0 EConstr.mkVar ty in + let evars = + List.map + (fun (ev, info) -> + let { ev_name = _, name + ; ev_status = force_status, status + ; ev_src = src + ; ev_typ = typ + ; ev_deps = deps + ; ev_tac = tac } = + info + in + let force_status, status = + match status with + | Evar_kinds.Define true when Id.Set.mem name transparent -> + (true, Evar_kinds.Define false) + | _ -> (force_status, status) + in + (name, typ, src, (force_status, status), deps, tac)) + evts + in + let evnames = List.map (fun (ev, info) -> (ev, snd info.ev_name)) evts in + let evmap f c = Util.pi1 (subst_evar_constr evm evts 0 f c) in + (Array.of_list (List.rev evars), (evnames, evmap), t', ty) diff --git a/vernac/retrieveObl.mli b/vernac/retrieveObl.mli new file mode 100644 index 0000000000..c9c45bd889 --- /dev/null +++ b/vernac/retrieveObl.mli @@ -0,0 +1,46 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +val check_evars : Environ.env -> Evd.evar_map -> unit + +type obligation_info = + ( Names.Id.t + * Constr.types + * Evar_kinds.t Loc.located + * (bool * Evar_kinds.obligation_definition_status) + * Int.Set.t + * unit Proofview.tactic option ) + array +(** ident, type, location of the original evar, (opaque or + transparent, expand or define), dependencies as indexes into the + array, tactic to solve it *) + +val retrieve_obligations : + Environ.env + -> Names.Id.t + -> Evd.evar_map + -> int + -> ?status:Evar_kinds.obligation_definition_status + -> EConstr.t + -> EConstr.types + -> obligation_info + * ( (Evar.t * Names.Id.t) list + * ((Names.Id.t -> EConstr.t) -> EConstr.t -> Constr.t) ) + * Constr.t + * Constr.t +(** [retrieve_obligations env id sigma fs ?status body type] returns + [obls, (evnames, evmap), nbody, ntype] a list of obligations built + from evars in [body, type]. + + [fs] is the number of function prototypes to try to clear from + evars contexts. [evnames, evmap) is the list of names / + substitution functions used to program with holes. This is not used + in Coq, but in the equations plugin; [evnames] is actually + redundant with the information contained in [obls] *) diff --git a/vernac/search.ml b/vernac/search.ml index ceff8acc79..68a30b4231 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -23,8 +23,8 @@ module NamedDecl = Context.Named.Declaration type filter_function = GlobRef.t -> env -> constr -> bool type display_function = GlobRef.t -> env -> constr -> unit -(* This option restricts the output of [SearchPattern ...], -[SearchAbout ...], etc. to the names of the symbols matching the +(* This option restricts the output of [SearchPattern ...], etc. +to the names of the symbols matching the query, separated by a newline. This type of output is useful for editors (like emacs), to generate a list of completion candidates without having to parse through the types of all symbols. *) @@ -226,7 +226,7 @@ let module_filter (mods, outside) ref env typ = let name_of_reference ref = Id.to_string (Nametab.basename_of_global ref) -let search_about_filter query gr env typ = match query with +let search_filter query gr env typ = match query with | GlobSearchSubPattern pat -> Constr_matching.is_matching_appsubterm ~closed:false env (Evd.from_env env) pat (EConstr.of_constr typ) | GlobSearchString s -> @@ -283,14 +283,14 @@ let search_by_head ?pstate gopt pat mods pr_search = in generic_search ?pstate gopt iter -(** SearchAbout *) +(** Search *) -let search_about ?pstate gopt items mods pr_search = +let search ?pstate gopt items mods pr_search = let filter ref env typ = let eqb b1 b2 = if b1 then b2 else not b2 in module_filter mods ref env typ && List.for_all - (fun (b,i) -> eqb b (search_about_filter i ref env typ)) items && + (fun (b,i) -> eqb b (search_filter i ref env typ)) items && blacklist_filter ref env typ in let iter ref env typ = diff --git a/vernac/search.mli b/vernac/search.mli index 11dd0c6794..6dbbff3a8c 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -30,8 +30,7 @@ val blacklist_filter : filter_function val module_filter : DirPath.t list * bool -> filter_function (** Check whether a reference pertains or not to a set of modules *) -val search_about_filter : glob_search_about_item -> filter_function -(** Check whether a reference matches a SearchAbout query. *) +val search_filter : glob_search_about_item -> filter_function (** {6 Specialized search functions} @@ -45,7 +44,7 @@ val search_rewrite : ?pstate:Proof_global.t -> int option -> constr_pattern -> D -> display_function -> unit val search_pattern : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool -> display_function -> unit -val search_about : ?pstate:Proof_global.t -> int option -> (bool * glob_search_about_item) list +val search : ?pstate:Proof_global.t -> int option -> (bool * glob_search_about_item) list -> DirPath.t list * bool -> display_function -> unit type search_constraint = diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 6e398d87ca..5a2bdb43d4 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -14,6 +14,7 @@ Proof_using Egramcoq Metasyntax DeclareUniv +RetrieveObl DeclareDef DeclareObl Canonical diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 8641c67d9f..2e509921c1 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -486,11 +486,14 @@ let program_inference_hook env sigma ev = let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = let env0 = Global.env () in + let flags = Pretyping.{ all_no_fail_flags with program_mode } in let decl = fst (List.hd thms) in let evd, udecl = 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)) = Constrintern.interp_context_evars ~program_mode env0 evd bl in - let evd, (t', imps') = Constrintern.interp_type_evars_impls ~program_mode ~impls env evd t in + let evd, (impls, ((env, ctx), imps)) = + Constrintern.interp_context_evars ~program_mode env0 evd bl + in + let evd, (t', imps') = Constrintern.interp_type_evars_impls ~flags ~impls env evd t in let flags = Pretyping.{ all_and_fail_flags with program_mode } in let inference_hook = if program_mode then Some program_inference_hook else None in let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in @@ -527,8 +530,10 @@ let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref))) | _ -> None +let default_thm_id = Id.of_string "Unnamed_thm" + let fresh_name_for_anonymous_theorem () = - Namegen.next_global_ident_away Lemmas.default_thm_id Id.Set.empty + Namegen.next_global_ident_away default_thm_id Id.Set.empty let vernac_definition_name lid local = let lid = @@ -565,7 +570,9 @@ let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt let env = Global.env () in let sigma = Evd.from_env env in Some (snd (Hook.get f_interp_redexp env sigma r)) in - ComDefinition.do_definition ~program_mode ~name:name.v + let do_definition = + ComDefinition.(if program_mode then do_definition_program else do_definition) in + do_definition ~name:name.v ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook (* NB: pstate argument to use combinators easily *) @@ -1773,10 +1780,6 @@ let () = optread = (fun () -> !search_output_name_only); optwrite = (:=) search_output_name_only } -let warn_deprecated_search_about = - CWarnings.create ~name:"deprecated-search-about" ~category:"deprecated" - (fun () -> strbrk "The SearchAbout command is deprecated. Please use Search instead.") - let vernac_search ~pstate ~atts s gopt r = let gopt = query_command_selector gopt in let r = interp_search_restriction r in @@ -1809,12 +1812,8 @@ let vernac_search ~pstate ~atts s gopt r = (Search.search_rewrite ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search | SearchHead c -> (Search.search_by_head ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search - | SearchAbout sl -> - warn_deprecated_search_about (); - (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> - Search.prioritize_search) pr_search | Search sl -> - (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> + (Search.search ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> Search.prioritize_search) pr_search); Feedback.msg_notice (str "(use \"About\" for full details on implicit arguments)") diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index b7c6d3c490..d6e7a3947a 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -69,7 +69,6 @@ type searchable = | SearchPattern of constr_pattern_expr | SearchRewrite of constr_pattern_expr | SearchHead of constr_pattern_expr - | SearchAbout of (bool * search_about_item) list | Search of (bool * search_about_item) list type locatable = diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 0e8202da9f..1920c276af 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -166,15 +166,15 @@ let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args -> vernac_c | Some Refl -> untype_command ty (f v) args end -let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Extend.norec, a) Extend.symbol = +let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Gramlib.Grammar.norec, a) Pcoq.Symbol.t = let open Extend in function -| TUlist1 l -> Alist1 (untype_user_symbol l) -| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s)) -| TUlist0 l -> Alist0 (untype_user_symbol l) -| TUlist0sep (l, s) -> Alist0sep (untype_user_symbol l, Atoken (CLexer.terminal s)) -| TUopt o -> Aopt (untype_user_symbol o) -| TUentry a -> Aentry (Pcoq.genarg_grammar (Genarg.ExtraArg a)) -| TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (Genarg.ExtraArg a), string_of_int i) + | TUlist1 l -> Pcoq.Symbol.list1 (untype_user_symbol l) + | TUlist1sep (l, s) -> Pcoq.Symbol.list1sep (untype_user_symbol l) (Pcoq.Symbol.token (CLexer.terminal s)) false + | TUlist0 l -> Pcoq.Symbol.list0 (untype_user_symbol l) + | TUlist0sep (l, s) -> Pcoq.Symbol.list0sep (untype_user_symbol l) (Pcoq.Symbol.token (CLexer.terminal s)) false + | TUopt o -> Pcoq.Symbol.opt (untype_user_symbol o) + | TUentry a -> Pcoq.Symbol.nterm (Pcoq.genarg_grammar (Genarg.ExtraArg a)) + | TUentryl (a, i) -> Pcoq.Symbol.nterml (Pcoq.genarg_grammar (Genarg.ExtraArg a)) (string_of_int i) let rec untype_grammar : type r s. (r, s) ty_sig -> 'a Egramml.grammar_prod_item list = function | TyNil -> [] @@ -229,7 +229,7 @@ let vernac_extend ~command ?classifier ?entry ext = type 'a argument_rule = | Arg_alias of 'a Pcoq.Entry.t -| Arg_rules of 'a Extend.production_rule list +| Arg_rules of 'a Pcoq.Production.t list type 'a vernac_argument = { arg_printer : Environ.env -> Evd.evar_map -> 'a -> Pp.t; @@ -244,7 +244,7 @@ let vernac_argument_extend ~name arg = e | Arg_rules rules -> let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in - let () = Pcoq.grammar_extend e (None, [(None, None, rules)]) in + let () = Pcoq.grammar_extend e {Pcoq.pos=None; data=[(None, None, rules)]} in e in let pr = arg.arg_printer in diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 90c00415d4..0d0ebc1086 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -111,7 +111,7 @@ type 'a argument_rule = | Arg_alias of 'a Pcoq.Entry.t (** This is used because CAMLP5 parser can be dumb about rule factorization, which sometimes requires two entries to be the same. *) -| Arg_rules of 'a Extend.production_rule list +| Arg_rules of 'a Pcoq.Production.t list (** There is a discrepancy here as we use directly extension rules and thus entries instead of ty_user_symbol and thus arguments as roots. *) diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 6846826bfa..a4e9c8e1ab 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -164,14 +164,15 @@ module Proof_global = struct type closed_proof = Proof_global.proof_object * Lemmas.Info.t - let return_proof ?allow_partial () = cc (return_proof ?allow_partial) + let return_proof () = cc return_proof + let return_partial_proof () = cc return_partial_proof - let close_future_proof ~opaque ~feedback_id pf = - cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~opaque ~feedback_id st pf) pt, + let close_future_proof ~feedback_id pf = + cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~feedback_id st pf) pt, Internal.get_info pt) - let close_proof ~opaque ~keep_body_ucst_separate f = - cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate f)) pt, + let close_proof ~opaque ~keep_body_ucst_separate = + cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate)) pt, Internal.get_info pt) let discard_all () = s_lemmas := None diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index 7607f8373a..9c4de7720c 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -65,16 +65,16 @@ module Proof_global : sig val with_current_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a - val return_proof : ?allow_partial:bool -> unit -> Proof_global.closed_proof_output + val return_proof : unit -> Proof_global.closed_proof_output + val return_partial_proof : unit -> Proof_global.closed_proof_output type closed_proof = Proof_global.proof_object * Lemmas.Info.t val close_future_proof : - opaque:Proof_global.opacity_flag -> feedback_id:Stateid.t -> Proof_global.closed_proof_output Future.computation -> closed_proof - val close_proof : opaque:Proof_global.opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof + val close_proof : opaque:Proof_global.opacity_flag -> keep_body_ucst_separate:bool -> closed_proof val discard_all : unit -> unit val update_global_env : unit -> unit |