diff options
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 28 |
1 files changed, 18 insertions, 10 deletions
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 55901fd604..c2e07c4fd5 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -109,7 +109,7 @@ let telescope env sigma l = let nf_evar_context sigma ctx = List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx -let build_wellfounded pm (recname,pl,bl,arityc,body) poly r measure notation = +let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?using r measure notation = let open EConstr in let open Vars in let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in @@ -259,8 +259,12 @@ let build_wellfounded pm (recname,pl,bl,arityc,body) poly r measure notation = let evars, _, evars_def, evars_typ = RetrieveObl.retrieve_obligations env recname sigma 0 def typ in + let using = using |> Option.map (fun expr -> + let terms = List.map EConstr.of_constr [evars_def; evars_typ] in + let l = Proof_using.process_expr env sigma expr terms in + Names.Id.Set.(List.fold_right add l empty)) in let uctx = Evd.evar_universe_context sigma in - let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ () in + let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ ?using () in let info = Declare.Info.make ~udecl ~poly ~hook () in let pm, _ = Declare.Obls.add_definition ~pm ~cinfo ~info ~term:evars_def ~uctx evars in @@ -275,7 +279,7 @@ let collect_evars_of_term evd c ty = Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) evars (Evd.from_ctx (Evd.evar_universe_context evd)) -let do_program_recursive ~pm ~scope ~poly fixkind fixl = +let do_program_recursive ~pm ~scope ~poly ?using fixkind fixl = let cofix = fixkind = Declare.Obls.IsCoFixpoint in let (env, rec_sign, udecl, evd), fix, info = interp_recursive ~cofix ~program_mode:true fixl @@ -287,13 +291,17 @@ let do_program_recursive ~pm ~scope ~poly fixkind fixl = let evd = nf_evar_map_undefined evd in let collect_evars name def typ impargs = (* Generalize by the recursive prototypes *) + let using = using |> Option.map (fun expr -> + let terms = [def; typ] in + let l = Proof_using.process_expr env evd expr terms in + Names.Id.Set.(List.fold_right add l empty)) in 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 = RetrieveObl.retrieve_obligations env name evm (List.length rec_sign) def typ in - let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in + let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in (cinfo, def, evars) in let (fixnames,fixrs,fixdefs,fixtypes) = fix in @@ -325,13 +333,13 @@ let do_program_recursive ~pm ~scope ~poly fixkind fixl = let info = Declare.Info.make ~poly ~scope ~kind ~udecl () in Declare.Obls.add_mutual_definitions ~pm defs ~info ~uctx ~ntns fixkind -let do_fixpoint ~pm ~scope ~poly l = +let do_fixpoint ~pm ~scope ~poly ?using l = let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in match g, l with | [Some { CAst.v = CWfRec (n,r) }], [ Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations} ] -> let recarg = mkIdentC n.CAst.v in - build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly r recarg notations + build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?using r recarg notations | [Some { CAst.v = CMeasureRec (n, m, r) }], [Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations }] -> @@ -344,7 +352,7 @@ let do_fixpoint ~pm ~scope ~poly l = user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.") | _, _ -> r in - build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly + build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?using (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m notations | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g -> @@ -352,11 +360,11 @@ let do_fixpoint ~pm ~scope ~poly l = Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in let fixkind = Declare.Obls.IsFixpoint annots in let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in - do_program_recursive ~pm ~scope ~poly fixkind l + do_program_recursive ~pm ~scope ~poly ?using fixkind l | _, _ -> CErrors.user_err ~hdr:"do_fixpoint" (str "Well-founded fixpoints not allowed in mutually recursive blocks") -let do_cofixpoint ~pm ~scope ~poly fixl = +let do_cofixpoint ~pm ~scope ~poly ?using fixl = let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in - do_program_recursive ~pm ~scope ~poly Declare.Obls.IsCoFixpoint fixl + do_program_recursive ~pm ~scope ~poly ?using Declare.Obls.IsCoFixpoint fixl |