(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \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) *) (************************************************************************)
module CVars = Vars
open Pp open Util open Names open Context open EConstr open Constrexpr open Constrintern open Vernacexpr
(* An (unoptimized) function that maps preorders to partial orders...
Input: a list of associations (x,[y1;...;yn]), all yi distincts and different of x, meaning x<=y1, ..., x<=yn
Output: a list of associations (x,Inr [y1;...;yn]), collecting all distincts yi greater than x, _or_, (x, Inl y) meaning that x is in the same class as y (in which case, x occurs nowhere else in the association map)
partial_order : ('a * 'a list) list -> ('a * ('a,'a list) union) list
*)
let rec partial_order cmp = function
| [] -> []
| (x,xge)::rest -> let rec browse res xge' = function
| [] -> let res = List.map (function
| (z, Inr zge) when List.mem_f cmp x zge ->
(z, Inr (List.union cmp zge xge'))
| r -> r) res in
(x,Inr xge')::res
| y::xge -> let rec link y = trymatchList.assoc_f cmp y res with
| Inl z -> link z
| Inr yge -> ifList.mem_f cmp x yge then let res = List.remove_assoc_f cmp y res in let res = List.map (function
| (z, Inl t) -> if cmp t y then (z, Inl x) else (z, Inl t)
| (z, Inr zge) -> ifList.mem_f cmp y zge then
(z, Inr (List.add_set cmp x (List.remove cmp y zge))) else
(z, Inr zge)) res in
browse ((y,Inl x)::res) xge' (List.union cmp xge yge) else
browse res (List.add_set cmp y (List.union cmp xge' yge)) xge with Not_found -> browse res (List.add_set cmp y xge') xge in link y in browse (partial_order cmp rest) [] xge
let string_of_kind = function
| Decls.IsDefinition Fixpoint -> "fixpoint"
| IsDefinition CoFixpoint -> "cofixpoint"
| _ -> "declaration"
let non_full_mutual_message x xge y yge kind rest = let reason = if Id.List.mem x yge then
Id.print y ++ str " depends on " ++ Id.print x ++ strbrk " but not conversely" elseif Id.List.mem y xge then
Id.print x ++ str " depends on " ++ Id.print y ++ strbrk " but not conversely" else
Id.print y ++ str " and " ++ Id.print x ++ strbrk " are not mutually dependent"in let e = ifList.is_empty rest then reason else strbrk "e.g., " ++ reason in let w = if kind <> Decls.IsDefinition CoFixpoint then strbrk "Well-foundedness check may fail unexpectedly." ++ fnl() else mt () in
strbrk "Not a fully mutually defined " ++ str (string_of_kind kind) ++ fnl () ++
str "(" ++ e ++ str ")." ++ fnl () ++ w
let warn_non_full_mutual =
CWarnings.create ~name:"non-full-mutual" ~category:CWarnings.CoreCategories.fixpoints
(fun (x,xge,y,yge,kind,rest) ->
non_full_mutual_message x xge y yge kind rest)
let check_true_recursivity env evd ~kind fixl = let names = List.map fst fixl in let preorder = List.map (fun (id,def) ->
(id.CAst.v, List.filter_map (fun {CAst.v=id'} -> if Termops.occur_var env evd id' def then Some id' else None) names))
fixl in let po = partial_order Id.equal preorder in matchList.filter (function (_,Inr _) -> true | _ -> false) po with
| (x,Inr xge)::(y,Inr yge)::rest ->
warn_non_full_mutual (x,xge,y,yge,kind,rest)
| _ -> match po with
| [x,Inr []] -> warn_non_recursive (x,kind)
| _ -> ()
(*****************************************************) (* Utilities for Program Fixpoint with wf or measure *)
open Rocqlib let init_constant sigma rf = Evd.fresh_global sigma rf let fix_sub_ref () = lib_ref "program.wf.fix_sub" let measure_on_R_ref () = lib_ref "program.wf.mr" let well_founded sigma = init_constant (Global.env ()) sigma (lib_ref "core.wf.well_founded") let mkSubset sigma name typ prop = letopen EConstr in let sigma, app_h = Evd.fresh_global (Global.env ()) sigma (delayed_force build_sigma).typ in
sigma, mkApp (app_h, [| typ; mkLambda (make_annot name ERelevance.relevant, typ, prop) |])
let ensure_program () = try fix_sub_ref (), measure_on_R_ref () with NotFoundRef r ->
CErrors.user_err
Pp.(str r ++ spc() ++ str "not registered," ++ spc() ++
str "you should try requiring library Corelib.Program.Wf.")
let recproofid = Id.of_string "recproof" let argname = Id.of_string "recarg"
let encapsulate_Fix_sub env sigma recname ctx body ccl (extradecl, rel, relargty, measure_body) = let len = Context.Rel.length ctx in let fix_sub_ref, measure_on_R_ref = ensure_program () in (* We curry the binders [x1:A1;...;xn:An] into [x:{x1&...&xn};x1:=x.1;...;xn:=x.2...2] *) (* argtyp is [{x1&...&xn}], letbinders is [x1:=x.1;...;xn:=x.2...2], argvalue is [(x.1,...,x.2...2)] *) letopen Combinators in let sigma, letbinders, {telescope_type = tuple_type; telescope_value = tuple_value} =
telescope env sigma ctx in let tupled_ctx = letbinders @ [LocalAssum (make_annot (Name argname) ERelevance.relevant, tuple_type)] in (* The function measure has type [tuple_type -> relargty] *) let measure = it_mkLambda_or_LetIn measure_body tupled_ctx in (* The relation wf_rel_measure is [fun x y => rel (measure x) (measure y)] *) let sigma, comb = Evd.fresh_global (Global.env ()) sigma measure_on_R_ref in let rel_measure = mkApp (comb, [| tuple_type; relargty; rel; measure |]) in (* The statement that rel_measure is well-founded *) let sigma, wf_term = well_founded sigma in let wf_type = mkApp (wf_term, [| tuple_type ; rel_measure |]) in (* A combinator building [rel (measure x) (measure y)] *) let tupled_measure_body = it_mkLambda_or_LetIn measure_body letbinders in let make_applied_rel x y =
mkApp (rel, [| Vars.subst1 x tupled_measure_body; Vars.subst1 y tupled_measure_body |]) in (* Conclusion of fixpoint in currified context *) let tupled_ccl = it_mkLambda_or_LetIn ccl letbinders in (* Making Fix_sub ready to take the extended body as argument *) let sigma, fix_sub = let sigma, fix_sub_term = Evd.fresh_global (Global.env ()) sigma fix_sub_ref in let typeclass_candidate = Typeclasses.is_maybe_class_type sigma wf_type in let sigma, wf_proof = Evarutil.new_evar ~typeclass_candidate env sigma
~src:(Loc.tag @@ Evar_kinds.QuestionMark {
Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Evar_kinds.Define false;
}) wf_type in let sigma = Evd.set_obligation_evar sigma (fst (destEvar sigma wf_proof)) in let ccl_pred = mkLambda (make_annot (Name argname) ERelevance.relevant, tuple_type, tupled_ccl) in let def = mkApp (fix_sub_term, [| tuple_type ; rel_measure ; wf_proof ; ccl_pred |]) in
Typing.solve_evars env sigma def in let arg = RelDecl.LocalAssum (make_annot (Name argname) ERelevance.relevant, tuple_type) in let argid' = Id.of_string (Id.to_string argname ^ "'") in let sigma, wfa = let sigma, ss_term = mkSubset sigma (Name argid') tuple_type (make_applied_rel (mkRel 1) (mkRel 2)) in
sigma, RelDecl.LocalAssum (make_annot (Name argid') ERelevance.relevant, ss_term) in let sigma, fix_sub_F_sub_ctx = let sigma, proj = Evd.fresh_global (Global.env ()) sigma (delayed_force build_sigma).Rocqlib.proj1 in let wfargpred = mkLambda (make_annot (Name argid') ERelevance.relevant, tuple_type, make_applied_rel (mkRel 1) (mkRel 3)) in let projection = (* in wfarg :: arg :: before *)
mkApp (proj, [| tuple_type ; wfargpred ; mkRel 1 |]) in let ccl_on_smaller_arg = Vars.substl [projection] (it_mkLambda_or_LetIn ccl letbinders) in (* substitute the projection of wfarg for something,
now ccl_let is in wfarg :: arg *) let ccl_on_smaller_arg = it_mkProd_or_LetIn ccl_on_smaller_arg [wfa] in let recname' = Nameops.add_suffix recname "'" in let smaller_arg = RelDecl.LocalAssum (make_annot (Name recname') ERelevance.relevant,
ccl_on_smaller_arg) in
sigma, Vars.lift_rel_context 1 letbinders @ smaller_arg :: [arg] in let sigma, curryfier_body, curryfier_ty = (* In tupled_context where the function argument of Fix_sub (argid'), is inserted, that is, all expanded: [recarg;argid';letbinders], build the curryfying combinator [fun ctx (recproof : rel (measure ctx) (measure tupled_context)) => argid' (tuple_value,recproof)] of type
[forall ctx (recproof : rel (measure ctx) (measure tupled_context)) => ccl] *) let sigma, intro = Evd.fresh_global (Global.env ()) sigma (delayed_force build_sigma).Rocqlib.intro in letapp = let wfpred = mkLambda (make_annot (Name argid') ERelevance.relevant, tuple_type, make_applied_rel (mkRel 1) (mkRel (2 * len + 4))) in (* Build the sig pair [exist _ tuple_value recproof] *) let arg = mkApp (intro, [| tuple_type; wfpred; Vars.lift 1 tuple_value; mkRel 1 |]) in (* Build the body of combinator *)
mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in let extended_ctx = extradecl :: ctx in let body = it_mkLambda_or_LetIn app extended_ctx in let ty = it_mkProd_or_LetIn (Vars.lift 1 ccl) extended_ctx in
sigma, body, ty in (* Rephrase the body of the fixpoint as dependent in the telescope *) let body_ctx = RelDecl.LocalDef (make_annot (Name recname) ERelevance.relevant, curryfier_body, curryfier_ty) :: fix_sub_F_sub_ctx in let intern_body_lam = it_mkLambda_or_LetIn body body_ctx in (* Instantiate the argument Fix_sub_F of Fix_sub with the body of the fixpoint *) let sigma, fix_sub = Typing.solve_evars env sigma fix_sub in
sigma, tupled_ctx, tuple_value, mkApp (fix_sub, [|intern_body_lam|])
let build_wellfounded env sigma poly udecl {CAst.v=recname; loc} ctx body ccl impls rel_measure = let len = Context.Rel.length ctx in (* Restore body in the context of binders + extradecl *) let _, body = decompose_lambda_n_decls sigma (len + 1) body in (* Restore ccl in the context of binders *) let ccl = Vars.subst1 (mkRel 1) (snd (decompose_prod_n_decls sigma (len + 1) ccl)) in (* Apply the body to Program.Wf.Fix_sub *) let sigma, tupled_ctx, tuple_value, def = encapsulate_Fix_sub env sigma recname ctx body ccl rel_measure in (* Turn everything to constr *) let ctx = Evarutil.nf_rel_context_evar sigma ctx in let tupled_ctx = Evarutil.nf_rel_context_evar sigma tupled_ctx in let ccl = Evarutil.nf_evar sigma ccl in let tuple_value = Evarutil.nf_evar sigma tuple_value in (* Decide if using a curryfied indirection via recname_func *) let recname_func, typ = if len > 1 then
Nameops.add_suffix recname "_func", it_mkProd_or_LetIn ccl tupled_ctx else
recname, it_mkProd_or_LetIn ccl ctx in let body, typ, _uctx, evmap, obls =
Declare.Obls.prepare_obligations ~name:recname_func ~body:def ~types:typ env sigma in let hook, impls = if len > 1 then let hook { Declare.Hook.S.dref; uctx; obls; _ } = let update c = CVars.replace_vars obls (evmap mkVar (Evarutil.nf_evar (Evd.from_ctx uctx) c)) in let tuple_value = update tuple_value in let ccl = update ccl in let ctx = Context.Rel.map_het (ERelevance.kind sigma) update ctx in let univs = UState.check_univ_decl ~poly uctx udecl in let h_body = let inst = UState.(match fst univs with
| Polymorphic_entry uctx -> UVars.UContext.instance uctx
| Monomorphic_entry _ -> UVars.Instance.empty) in
Constr.mkRef (dref, inst) in let body = Term.it_mkLambda_or_LetIn (Constr.mkApp (h_body, [|tuple_value|])) ctx in let ty = Term.it_mkProd_or_LetIn ccl ctx in let ce = Declare.definition_entry ~types:ty ~univs body in (* FIXME: include locality *) let c = Declare.declare_constant ?loc ~name:recname ~kind:Decls.(IsDefinition Definition) (DefinitionEntry ce) in let gr = GlobRef.ConstRef c in if Impargs.is_implicit_args () || not (List.is_empty impls) then
Impargs.declare_manual_implicits false gr impls in
Some (Declare.Hook.make hook), [] else
None, impls in
sigma, CAst.make ?loc recname_func, body, typ, impls, obls, hook
(*********************************) (* Interpretation of Co/Fixpoint *)
let make_qref s = Libnames.qualid_of_string s let lt_ref = make_qref "Init.Peano.lt"
let position_of_argument ctx binders na = let exception Found of int in let name = Name na.CAst.v in try
Context.Rel.fold_outside (fun decl n -> match Context.Rel.Declaration.(get_value decl, Name.equal (get_name decl) name) with
| None, true -> raise (Found n)
| Some _, true -> let loc = List.find_map (fun id -> if Name.equal name id.CAst.v then Some id.CAst.loc else None) (Constrexpr_ops.names_of_local_binders binders) in let loc = Option.default na.CAst.loc loc in
CErrors.user_err ?loc
(Name.print name ++ str" must be a proper parameter and not a local definition.")
| None, false -> n + 1
| Some _, false -> n (* let-ins don't count *))
~init:0 ctx |> ignore;
CErrors.user_err ?loc:na.loc
(str "No parameter named " ++ Id.print na.v ++ str"."); with
Found k -> k
(* Interpret the index of a recursion order annotation *) let find_rec_annot ~program_mode ~function_mode env sigma Vernacexpr.{fname={CAst.loc}; binders} ctx typ = function
| None -> let ctx', _ = Reductionops.whd_decompose_prod_decls (push_rel_context ctx env) sigma typ in let n = Context.Rel.nhyps ctx + Context.Rel.nhyps ctx' in if Int.equal n 0 then CErrors.user_err ?loc Pp.(str "A fixpoint needs at least one parameter.");
None, List.interval 0 (n - 1)
| Some CAst.{v=rec_order;loc} -> let default_order r = Option.default (CAst.make @@ CRef (lt_ref,None)) r in match rec_order with
| CStructRec na -> None, [position_of_argument ctx binders na]
| CWfRec (na,r) -> if function_mode then None, [] else Some (r, Constrexpr_ops.mkIdentC na.CAst.v), [] (* useless for Program: will use Fix_sub *)
| CMeasureRec (na, mes, rfel) -> if function_mode then let _ = match binders, na with
| [CLocalDef({ CAst.v = Name id },_,_,_) | CLocalAssum([{ CAst.v = Name id }],_,_,_)], None -> ()
| _, None -> CErrors.user_err ?loc Pp.(str "Decreasing argument must be specified in measure clause.")
| _, Some na -> (* check that the name exists *) ignore (position_of_argument ctx binders na) in (* Dummy *) None, [] else let r = match na, rfel with
| Some id, None -> let loc = id.CAst.loc in
CAst.make ?loc @@ CRef (Libnames.qualid_of_ident ?loc id.CAst.v,None)
| Some _, Some _ -> CErrors.user_err ?loc Pp.(str"Measure takes three arguments only in Function.")
| None, rfel -> default_order rfel in
Some (r, mes), [] (* useless: will use Fix_sub *)
let interp_rec_annot ~program_mode ~function_mode env sigma fixl ctxl ccll rec_order = letopen Pretyping in let nowf () = List.map (fun _ -> None) fixl in match rec_order with (* If recursive argument was not given by user, we try all args. An earlier approach was to look only for inductive arguments, but doing it properly involves delta-reduction, and it finally doesn't seem to worth the effort (except for huge mutual
fixpoints ?) *)
| CFixRecOrder fix_orders -> let fixwf, possible_guard = List.split (List.map4 (find_rec_annot ~program_mode ~function_mode env sigma) fixl ctxl ccll fix_orders) in
fixwf, {possibly_cofix = false; possible_fix_indices = possible_guard}
| CCoFixRecOrder -> nowf (), {possibly_cofix = true; possible_fix_indices = List.map (fun _ -> []) fixl}
| CUnknownRecOrder -> nowf (), RecLemmas.find_mutually_recursive_statements sigma ctxl ccll
let interp_fix_context ~program_mode env sigma {Vernacexpr.binders} = let sigma, (impl_env, ((env', ctx), imps, _locs)) = interp_context_evars ~program_mode env sigma binders in
sigma, (env', ctx, impl_env, imps)
let interp_fix_ccl ~program_mode sigma impls env fix = 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)
let interp_fix_body ~program_mode env_rec ctx sigma impls fix ccl = Option.cata (fun body -> let env_rec_ctx = push_rel_context ctx env_rec in let sigma, body = interp_casted_constr_evars ~program_mode env_rec_ctx sigma ~impls body ccl in
sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.Vernacexpr.body_def
let build_fix_type sigma ctx ccl (_, extradecl) = let ccl = it_mkProd_or_LetIn (Vars.lift (Context.Rel.length extradecl) ccl) extradecl in
Evarutil.nf_evar sigma (it_mkProd_or_LetIn ccl ctx)
let build_dummy_fix_type sigma ctx ccl (_, extradecl) = (* Hack: the extra declarations are smashed to a dummy non-dependent
so as not to contribute to the computation of implicit arguments *) let ccl = it_mkProd_or_LetIn (Vars.lift (Context.Rel.length extradecl) ccl) (List.map (RelDecl.map_type (fun _ -> mkProp)) extradecl) in
Evarutil.nf_evar sigma (it_mkProd_or_LetIn ccl ctx)
(* Wellfounded definition *)
let encapsulate env sigma r t = (* Would probably be overkill to use a specific fix_proto in SProp when in SProp?? *) let fix_proto sigma =
Evd.fresh_global (Global.env ()) sigma (Rocqlib.lib_ref "program.tactic.fix_proto") in let fix_proto_relevance = EConstr.ERelevance.relevant in let sigma, sort = Typing.type_of ~refresh:true env sigma t in try let sigma, h_term = fix_proto sigma in letapp = EConstr.mkApp (h_term, [|sort; t|]) in let sigma, app = Typing.solve_evars env sigma appin
sigma, fix_proto_relevance, app with e when CErrors.noncritical e -> sigma, r, t
let interp_wf ~program_mode env sigma recname ctx ccl = function
| None -> sigma, ((false, []), None, [])
| Some (r, measure) -> (* We have to insert an argument for the measure/wellfoundedness *) (* The extra implicit argument *) let impl = CAst.make (Some (Name recproofid, true)) in (* The well-founded relation *) let env_ctx = push_rel_context ctx env in let sigma, (rel, _) = interp_constr_evars_impls ~program_mode env sigma r in let relargty = Hipattern.is_homogeneous_relation ?loc:(Constrexpr_ops.constr_loc r) env_ctx sigma rel in (* The measure *) let sigma, measure = interp_casted_constr_evars ~program_mode env_ctx sigma measure relargty in let sigma, after, extradecl = if program_mode then let len = Context.Rel.length ctx in let applied_rel_measure = mkApp (rel, [| measure; Vars.lift len measure |]) in let extradecl = RelDecl.LocalAssum (make_annot (Name recproofid) ERelevance.relevant, applied_rel_measure) in
sigma, true, extradecl else let sigma, wf_term = well_founded sigma in let applied_wf = mkApp (wf_term, [| relargty; rel; measure |]) in let extradecl = RelDecl.LocalAssum (make_annot (Name recproofid) ERelevance.relevant, applied_wf) in
sigma, false, extradecl in
sigma, ((after, [extradecl]), Some (extradecl, rel, relargty, measure), [impl])
let interp_mutual_definition env ~program_mode ~function_mode rec_order fixl = letopen Context.Named.Declaration in letopen EConstr in let fixlnames = List.map (fun fix -> fix.Vernacexpr.fname) fixl in let fixnames = List.map (fun na -> na.CAst.v) fixlnames in
(* Interp arities allowing for unresolved types *) let sigma, decl = interp_mutual_univ_decl_opt env (List.map (fun Vernacexpr.{univs} -> univs) fixl) in let sigma, (fixenv, fixctxs, fixctximpenvs, fixctximps) =
on_snd List.split4 @@ List.fold_left_map (fun sigma -> interp_fix_context ~program_mode env sigma) sigma fixl in let sigma, (fixccls,fixrs,fixcclimps) =
on_snd List.split3 @@ List.fold_left3_map (interp_fix_ccl ~program_mode) sigma fixctximpenvs fixenv fixl in let fixwfs, possible_guard = interp_rec_annot ~program_mode ~function_mode env sigma fixl fixctxs fixccls rec_order in let sigma, (fixextras, fixwfs, fixwfimps) =
on_snd List.split3 @@ (List.fold_left4_map (interp_wf ~program_mode env) sigma fixnames fixctxs fixccls fixwfs) in let fixtypes = List.map3 (build_fix_type sigma) fixctxs fixccls fixextras in let sigma, rec_sign = List.fold_left4
(fun (sigma, rec_sign) id r t (_,extradecl) -> let sigma, r, t = if program_mode && List.is_empty extradecl then encapsulate env sigma r t else sigma, r, t in
sigma, LocalAssum (Context.make_annot id r, t) :: rec_sign)
(sigma, []) fixnames fixrs fixtypes fixextras in let fixrecimps = List.map3 (fun ctximps wfimps cclimps -> ctximps @ wfimps @ cclimps) fixctximps fixwfimps fixcclimps in let fiximps = List.map2 (fun ctximps cclimps -> ctximps @ cclimps) fixctximps fixcclimps in
(* Interp bodies with rollback because temp use of notations/implicit *) let fixntns = List.map_append (fun { Vernacexpr.notations } -> List.map Metasyntax.prepare_where_notation notations ) fixl in let sigma, fixdefs = let force = List.map (fun (_,extra) -> Id.Set.of_list (List.map_filter (fun d -> Nameops.Name.to_option (RelDecl.get_name d)) extra)) fixextras in let dummy_fixtypes = List.map3 (build_dummy_fix_type sigma) fixctxs fixccls fixextras in let impls = compute_internalization_env env sigma ~force Recursive fixnames dummy_fixtypes fixrecimps in
Metasyntax.with_syntax_protection (fun () -> List.iter (Metasyntax.set_notation_for_interpretation env impls) fixntns; List.fold_left5_map
(fun sigma fixctximpenv (after,extradecl) ctx body ccl -> let impls = Id.Map.fold Id.Map.add fixctximpenv impls in let env', ctx = if after then env, List.map NamedDecl.to_rel_decl rec_sign @ ctx else push_named_context rec_sign env, extradecl@ctx in
interp_fix_body ~program_mode env' ctx sigma impls body (Vars.lift (Context.Rel.length extradecl) ccl))
sigma fixctximpenvs fixextras fixctxs fixl fixccls)
() in
(* Build the fix declaration block *) let fix = {fixnames=fixlnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs} in
(env, rec_sign, sigma), (fix, possible_guard, decl)
let check_recursive ~kind env evd {fixnames;fixdefs;fixwfs} = (* TO MOVE AT FINAL DEFINITION TIME? *) ifList.for_all Option.has_some fixdefs && List.for_all Option.is_empty fixwfs thenbegin let fixdefs = List.mapOption.get fixdefs in
check_true_recursivity env evd ~kind (List.combine fixnames fixdefs) end
let ground_fixpoint env evd {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs} =
Pretyping.check_evars_are_solved ~program_mode:false env evd; let fixrs = List.map (fun r -> EConstr.ERelevance.kind evd r) fixrs in let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr evd) c) fixdefs in let fixtypes = List.map EConstr.(to_constr evd) fixtypes in
{fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs}
(** For Funind *)
let interp_fixpoint_short rec_order fixpoint_exprl = let env = Global.env () in let (_, _, sigma),(fix, _, _) = interp_mutual_definition ~program_mode:false ~function_mode:true env (CFixRecOrder rec_order) fixpoint_exprl in (* Instantiate evars and check all are resolved *) let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in let sigma = Evd.minimize_universes sigma in let sigma = Pretyping.(solve_remaining_evars all_no_fail_flags env sigma) in let typel = (ground_fixpoint env sigma fix).fixtypes in
typel, sigma
let build_recthms {fixnames;fixtypes;fixctxs;fiximps} = List.map4 (fun {CAst.v=name; loc} typ ctx impargs -> let args = List.map Context.Rel.Declaration.get_name ctx in
Declare.CInfo.make ?loc ~name ~typ ~args ~impargs ()
) fixnames fixtypes fixctxs fiximps
let collect_evars_of_term evd c ty =
Evar.Set.union (Evd.evars_of_term evd c) (Evd.evars_of_term evd ty)
let collect_evars env sigma rec_sign recname def typ = (* Generalize by the recursive prototypes *) let deps = collect_evars_of_term sigma def typ in let evars, _, def, typ =
RetrieveObl.retrieve_obligations env recname.CAst.v sigma
(List.length rec_sign) ~deps def typ in
(Some def, typ, evars)
let out_def = function
| Some def -> def
| None -> CErrors.user_err Pp.(str "Program Fixpoint needs defined bodies.")
let build_program_fixpoint env sigma rec_sign possible_guard fixnames fixrs fixdefs fixtypes fixwfs =
assert (List.for_all Option.is_empty fixwfs); (* Get the interesting evars, those that were not instantiated *) let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env sigma in (* Solve remaining evars *) let sigma = Evarutil.nf_evar_map_undefined sigma in let fixdefs = List.map out_def fixdefs in (* An early check of guardedness before working on the obligations *) let () = let fixdecls =
Array.of_list (List.map2 (fun x r -> Context.make_annot (Name x.CAst.v) r) fixnames fixrs),
Array.of_list fixtypes,
Array.of_list fixdefs in
ignore (Pretyping.esearch_guard env sigma possible_guard fixdecls) in List.split3 (List.map3 (collect_evars env sigma rec_sign) fixnames fixdefs fixtypes)
let finish_obligations env sigma rec_sign possible_guard poly udecl = function
| {fixnames=[recname];fixrs;fixdefs=[body];fixtypes=[ccl];fixctxs=[ctx];fiximps=[imps];fixntns;fixwfs=[Some wf]} -> let sigma = Evarutil.nf_evar_map sigma in(* use nf_evar_map_undefined?? *) let sigma, recname, body, ccl, impls, obls, hook = build_wellfounded env sigma poly udecl recname ctx (Option.get body) ccl imps wf in let fixrs = List.map (EConstr.ERelevance.kind sigma) fixrs in
sigma, {fixnames=[recname];fixrs;fixdefs=[Some body];fixtypes=[ccl];fixctxs=[ctx];fiximps=[impls];fixntns;fixwfs=[Some wf]}, [obls], hook
| {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs} -> let fixdefs, fixtypes, obls = build_program_fixpoint env sigma rec_sign possible_guard fixnames fixrs fixdefs fixtypes fixwfs in let fixrs = List.map (EConstr.ERelevance.kind sigma) fixrs in
sigma, {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs}, obls, None
let finish_regular env sigma use_inference_hook fix = let inference_hook = if use_inference_hook then Some Declare.Obls.program_inference_hook else None in let sigma = Pretyping.(solve_remaining_evars ?hook:inference_hook all_no_fail_flags env sigma) in
sigma, ground_fixpoint env sigma fix, [], None
let do_mutually_recursive ?pm ~refine ~program_mode ?(use_inference_hook=false) ?scope ?clearbody ~kind ~poly ?typing_flags ?user_warns ?using (rec_order, fixl)
: Declare.OblState.t option * Declare.Proof.t option = let env = Global.env () in let env = Environ.update_typing_flags ?typing_flags env in let (env,rec_sign,sigma),(fix,possible_guard,udecl) = interp_mutual_definition env ~program_mode ~function_mode:false rec_order fixl in
check_recursive ~kind env sigma fix;
if refine then let info = Declare.Info.make ?scope ?clearbody ~kind ~poly ~udecl ?typing_flags ?user_warns ~ntns:fix.fixntns () in let cinfo = build_recthms fix in let possible_guard = (possible_guard, fix.fixrs) in let lemma = Declare.Proof.start_mutual_definitions_refine ~info ~cinfo ~bodies:fix.fixdefs ~possible_guard ?using sigma in
None, Some lemma else
(* Instantiate evars and check all are resolved *) let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in let sigma = Evd.minimize_universes sigma in
let sigma, ({fixdefs=bodies;fixrs;fixtypes;fixwfs} as fix), obls, hook = match pm with
| Some pm -> finish_obligations env sigma rec_sign possible_guard poly udecl fix
| None -> finish_regular env sigma use_inference_hook fix in let info = Declare.Info.make ?scope ?clearbody ~kind ~poly ~udecl ?hook ?typing_flags ?user_warns ~ntns:fix.fixntns () in let cinfo = build_recthms fix in match pm with
| Some pm -> (* Program Fixpoint struct *) let bodies = List.mapOption.get bodies in
Evd.check_univ_decl_early ~poly ~with_obls:true sigma udecl (bodies @ fixtypes); let sigma = if poly then sigma else Evd.fix_undefined_variables sigma in let uctx = Evd.ustate sigma in
(match fixwfs, bodies, cinfo, obls with
| [Some _], [body], [cinfo], [obls] -> (* Program Fixpoint wf/measure *) let pm, _ = Declare.Obls.add_definition ~pm ~cinfo ~info ~opaque:false ~body ~uctx ?using obls in
Some pm, None
| _ -> let possible_guard = (possible_guard, fixrs) in
Some (Declare.Obls.add_mutual_definitions ~pm ~cinfo ~info ~opaque:false ~uctx ~bodies ~possible_guard ?using obls), None)
| None -> try let bodies = List.mapOption.get bodies in let uctx = Evd.ustate sigma in (* All bodies are defined *) let possible_guard = (possible_guard, fixrs) in let _ : GlobRef.t list =
Declare.declare_mutual_definitions ~cinfo ~info ~opaque:false ~uctx ~possible_guard ~bodies ?using () in
None, None withOption.IsNone -> (* At least one undefined body *)
Evd.check_univ_decl_early ~poly ~with_obls:false sigma udecl (Option.List.flatten bodies @ fixtypes); let possible_guard = (possible_guard, fixrs) in let lemma = Declare.Proof.start_mutual_definitions ~info ~cinfo ~bodies ~possible_guard ?using sigma in
None, Some lemma
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
