Quelle comFixpoint.ml Sprache: SML

(************************************************************************)
(*         *      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

module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration

(* 3c| Fixpoints and co-fixpoints *)

(* 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 =
        try match List.assoc_f cmp y res with
        | Inl z -> link z
        | Inr yge ->
          if List.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) ->
                  if List.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"
    else if 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 = if List.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 warn_non_recursive =
  CWarnings.create ~name:"non-recursive" ~category:CWarnings.CoreCategories.fixpoints
         (fun (x,kind) ->
          strbrk "Not a truly recursive " ++ str (string_of_kind kind) ++ str ".")

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
  match List.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 =
  let open 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)] *)
  let open 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
    let app =
      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 =
  let open 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
    let app = EConstr.mkApp (h_term, [|sort; t|]) in
    let sigma, app = Typing.solve_evars env sigma app in
    sigma, fix_proto_relevance, app
  with e when CErrors.noncritical e -> sigma, r, t

type ('constr, 'relevance) fix_data = {
  fixnames : Names.lident list;
  fixrs    : 'relevance list;
  fixdefs  : 'constr option list;
  fixtypes : 'constr list;
  fixctxs  :  EConstr.rel_context list;
  fiximps  : (Names.Name.t * bool) option CAst.t list list;
  fixntns  : Metasyntax.notation_interpretation_decl list;
  fixwfs   : (rel_declaration * EConstr.t * EConstr.t * EConstr.t) option list;
}

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 =
  let open Context.Named.Declaration in
  let open 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? *)
  if List.for_all Option.has_some fixdefs && List.for_all Option.is_empty fixwfs then begin
    let fixdefs = List.map Option.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.map Option.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.map Option.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
    with Option.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

quality100%

¤ Dauer der Verarbeitung: 0.15 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.