(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* mkLambda (x,t,under_binders (push_rel (LocalAssum (x,t)) env) sigma f (n-1) c) | LetIn (x,b,t,c) -> mkLetIn (x,b,t,under_binders (push_rel (LocalDef (x,b,t)) env) sigma f (n-1) c) | _ -> assert false 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 " ++ pr_id cs ++ str "."); let args = List.map (fun id -> CAst.make ?loc @@ CRef(Ident(loc,id),None)) params in CAppExpl ((None,Ident(loc,name),None),List.rev args) | c -> c ) (* Commands of the interface *) (* 1| Constant definitions *) let red_constant_entry n ce sigma = function | None -> ce | Some red -> let proof_out = ce.const_entry_body in let env = Global.env () in let (redfun, _) = reduction_of_red_expr env red in let redfun env sigma c = let (_, c) = redfun env sigma c in EConstr.Unsafe.to_constr c in { ce with const_entry_body = Future.chain ~pure:true proof_out (fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) } let warn_implicits_in_term = CWarnings.create ~name:"implicits-in-term" ~category:"implicits" (fun () -> strbrk "Implicit arguments declaration relies on type." ++ spc () ++ strbrk "The term declares more implicits than the type here.") let interp_definition pl bl p red_option c ctypopt = let env = Global.env() in let ctx = Evd.make_evar_universe_context env pl in let evdref = ref (Evd.from_ctx ctx) in let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in let nb_args = Context.Rel.nhyps ctx in let imps,pl,ce = match ctypopt with None -> let subst = evd_comb0 Evd.nf_univ_variables evdref in let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in let env_bl = push_rel_context ctx env in let c, imps2 = interp_constr_evars_impls ~impls env_bl evdref c in let c = EConstr.Unsafe.to_constr c in let nf,subst = Evarutil.e_nf_evars_and_universes evdref in let body = nf (it_mkLambda_or_LetIn c ctx) in let vars = Universes.universes_of_constr body in let evd = Evd.restrict_universe_context !evdref vars in let pl, uctx = Evd.universe_context ?names:pl evd in imps1@(Impargs.lift_implicits nb_args imps2), pl, definition_entry ~univs:uctx ~poly:p body | Some ctyp -> let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in let subst = evd_comb0 Evd.nf_univ_variables evdref in let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in let env_bl = push_rel_context ctx env in let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in let c = EConstr.Unsafe.to_constr c in let nf, subst = Evarutil.e_nf_evars_and_universes evdref in let body = nf (it_mkLambda_or_LetIn c ctx) in let ty = EConstr.Unsafe.to_constr ty in let typ = nf (Term.it_mkProd_or_LetIn ty ctx) in let beq b1 b2 = if b1 then b2 else not b2 in let impl_eq (x,y,z) (x',y',z') = beq x x' && beq y y' && beq z z' in (* Check that all implicit arguments inferable from the term are inferable from the type *) let chk (key,va) = impl_eq (List.assoc_f Pervasives.(=) key impsty) va (* FIXME *) in if not (try List.for_all chk imps2 with Not_found -> false) then warn_implicits_in_term (); let vars = Univ.LSet.union (Universes.universes_of_constr body) (Universes.universes_of_constr typ) in let ctx = Evd.restrict_universe_context !evdref vars in let pl, uctx = Evd.universe_context ?names:pl ctx in imps1@(Impargs.lift_implicits nb_args impsty), pl, definition_entry ~types:typ ~poly:p ~univs:uctx body in red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, pl, imps let check_definition (ce, evd, _, imps) = check_evars_are_solved (Global.env ()) evd Evd.empty; ce let warn_local_declaration = CWarnings.create ~name:"local-declaration" ~category:"scope" (fun (id,kind) -> pr_id id ++ strbrk " is declared as a local " ++ str kind) let get_locality id ~kind = function | Discharge -> (** If a Let is defined outside a section, then we consider it as a local definition *) warn_local_declaration (id,kind); true | Local -> true | Global -> false let declare_global_definition ident ce local k pl imps = let local = get_locality ident ~kind:"definition" local in let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in let () = Universes.register_universe_binders gr pl in let () = definition_message ident in gr let declare_definition_hook = ref ignore let set_declare_definition_hook = (:=) declare_definition_hook let get_declare_definition_hook () = !declare_definition_hook let warn_definition_not_visible = CWarnings.create ~name:"definition-not-visible" ~category:"implicits" (fun ident -> strbrk "Section definition " ++ pr_id ident ++ strbrk " is not visible from current goals") let declare_definition ident (local, p, k) ce pl imps hook = let fix_exn = Future.fix_exn_of ce.const_entry_body in let () = !declare_definition_hook ce in let r = match local with | Discharge when Lib.sections_are_opened () -> let c = SectionLocalDef ce in let _ = declare_variable ident (Lib.cwd(), c, IsDefinition k) in let () = definition_message ident in let gr = VarRef ident in let () = maybe_declare_manual_implicits false gr imps in let () = if Pfedit.refining () then warn_definition_not_visible ident in gr | Discharge | Local | Global -> declare_global_definition ident ce local k pl imps in Lemmas.call_hook fix_exn hook local r let _ = Obligations.declare_definition_ref := (fun i k c imps hook -> declare_definition i k c [] imps hook) let do_definition ident k pl bl red_option c ctypopt hook = let (ce, evd, pl', imps as def) = interp_definition pl bl (pi2 k) red_option c ctypopt in if Flags.is_program_mode () then let env = Global.env () in let (c,ctx), sideff = Future.force ce.const_entry_body in assert(Safe_typing.empty_private_constants = sideff); assert(Univ.ContextSet.is_empty ctx); let typ = match ce.const_entry_type with | Some t -> t | None -> EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr c)) in Obligations.check_evars env evd; let obls, _, c, cty = Obligations.eterm_obligations env ident evd 0 c typ in let ctx = Evd.evar_universe_context evd in let hook = Lemmas.mk_hook (fun l r _ -> Lemmas.call_hook (fun exn -> exn) hook l r) in ignore(Obligations.add_definition ident ~term:c cty ctx ?pl ~implicits:imps ~kind:k ~hook obls) else let ce = check_definition def in ignore(declare_definition ident k ce pl' imps (Lemmas.mk_hook (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r))) (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl (_,ident) = match local with | Discharge when Lib.sections_are_opened () -> let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in let _ = declare_variable ident decl in let () = assumption_message ident in let () = if not !Flags.quiet && Pfedit.refining () then Feedback.msg_info (str"Variable" ++ spc () ++ pr_id ident ++ strbrk " is not visible from current goals") in let r = VarRef ident in let () = Typeclasses.declare_instance None true r in let () = if is_coe then Class.try_add_new_coercion r ~local:true false in (r,Univ.Instance.empty,true) | Global | Local | Discharge -> let local = get_locality ident ~kind:"axiom" local in let inl = match nl with | NoInline -> None | DefaultInline -> Some (Flags.get_inline_level()) | InlineAt i -> Some i in let ctx = Univ.ContextSet.to_context ctx in let decl = (ParameterEntry (None,p,(c,ctx),inl), IsAssumption kind) in let kn = declare_constant ident ~local decl in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in let () = Universes.register_universe_binders gr pl in let () = assumption_message ident in let () = Typeclasses.declare_instance None false gr in let () = if is_coe then Class.try_add_new_coercion gr ~local p in let inst = if p (* polymorphic *) then Univ.UContext.instance ctx else Univ.Instance.empty in (gr,inst,Lib.is_modtype_strict ()) let interp_assumption evdref env impls bl c = let c = mkCProdN ?loc:(local_binders_loc bl) bl c in let ty, impls = interp_type_evars_impls env evdref ~impls c in let ty = EConstr.Unsafe.to_constr ty in (ty, impls) let declare_assumptions idl is_coe k (c,ctx) pl imps impl_is_on nl = let refs, status, _ = List.fold_left (fun (refs,status,ctx) id -> let ref',u',status' = declare_assumption is_coe k (c,ctx) pl imps impl_is_on nl id in (ref',u')::refs, status' && status, Univ.ContextSet.empty) ([],true,ctx) idl in List.rev refs, status let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = let open Context.Named.Declaration in let env = Global.env () in let evdref = ref (Evd.from_env env) in let l = if poly then (* Separate declarations so that A B : Type puts A and B in different levels. *) List.fold_right (fun (is_coe,(idl,c)) acc -> List.fold_right (fun id acc -> (is_coe, ([id], c)) :: acc) idl acc) l [] else l in (* We intepret all declarations in the same evar_map, i.e. as a telescope. *) let _,l = List.fold_map (fun (env,ienv) (is_coe,(idl,c)) -> let t,imps = interp_assumption evdref env ienv [] c in let env = push_named_context (List.map (fun (_,id) -> LocalAssum (id,t)) idl) env in let ienv = List.fold_right (fun (_,id) ienv -> let impls = compute_internalization_data env Variable t imps in Id.Map.add id impls ienv) idl ienv in ((env,ienv),((is_coe,idl),t,imps))) (env,empty_internalization_env) l in let evd = solve_remaining_evars all_and_fail_flags env !evdref Evd.empty in (* The universe constraints come from the whole telescope. *) let evd = Evd.nf_constraints evd in let ctx = Evd.universe_context_set evd in let nf_evar c = EConstr.Unsafe.to_constr (nf_evar evd (EConstr.of_constr c)) in let l = List.map (on_pi2 nf_evar) l in pi2 (List.fold_left (fun (subst,status,ctx) ((is_coe,idl),t,imps) -> let t = replace_vars subst t in let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in let subst' = List.map2 (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u))) idl refs in (subst'@subst, status' && status, (* The universe constraints are declared with the first declaration only. *) Univ.ContextSet.empty)) ([],true,ctx) l) let do_assumptions_bound_univs coe kind nl id pl c = let env = Global.env () in let ctx = Evd.make_evar_universe_context env pl in let evdref = ref (Evd.from_ctx ctx) in let ty, impls = interp_type_evars_impls env evdref c in let nf, subst = Evarutil.e_nf_evars_and_universes evdref in let ty = EConstr.Unsafe.to_constr ty in let ty = nf ty in let vars = Universes.universes_of_constr ty in let evd = Evd.restrict_universe_context !evdref vars in let pl, uctx = Evd.universe_context ?names:pl evd in let uctx = Univ.ContextSet.of_context uctx in let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls false nl id in st let do_assumptions kind nl l = match l with | [coe, ([id, Some pl], c)] -> let () = match kind with | (Discharge, _, _) when Lib.sections_are_opened () -> let loc = fst id in let msg = Pp.str "Section variables cannot be polymorphic." in user_err ?loc msg | _ -> () in do_assumptions_bound_univs coe kind nl id (Some pl) c | _ -> let map (coe, (idl, c)) = let map (id, univs) = match univs with | None -> id | Some _ -> let loc = fst id in let msg = Pp.str "Assumptions with bound universes can only be defined one at a time." in user_err ?loc msg in (coe, (List.map map idl, c)) in let l = List.map map l in do_assumptions_unbound_univs kind nl l (* 3a| Elimination schemes for mutual inductive definitions *) (* 3b| Mutual inductive definitions *) let push_types env idl tl = List.fold_left2 (fun env id t -> Environ.push_rel (LocalAssum (Name id,t)) env) env idl tl type structured_one_inductive_expr = { ind_name : Id.t; ind_univs : lident list option; ind_arity : constr_expr; ind_lc : (Id.t * constr_expr) list } type structured_inductive_expr = local_binder_expr list * structured_one_inductive_expr list let minductive_message warn = function | [] -> user_err Pp.(str "No inductive definition.") | [x] -> (pr_id x ++ str " is defined" ++ if warn then str " as a non-primitive record" else mt()) | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++ spc () ++ str "are defined") let check_all_names_different indl = let ind_names = List.map (fun ind -> ind.ind_name) indl in let cstr_names = List.map_append (fun ind -> List.map fst ind.ind_lc) indl in let l = List.duplicates Id.equal ind_names in let () = match l with | [] -> () | t :: _ -> raise (InductiveError (SameNamesTypes t)) in let l = List.duplicates Id.equal cstr_names in let () = match l with | [] -> () | c :: _ -> raise (InductiveError (SameNamesConstructors (List.hd l))) in let l = List.intersect Id.equal ind_names cstr_names in match l with | [] -> () | _ -> raise (InductiveError (SameNamesOverlap l)) let mk_mltype_data evdref env assums arity indname = let is_ml_type = is_sort env !evdref (EConstr.of_constr arity) in (is_ml_type,indname,assums) let prepare_param = function | LocalAssum (na,t) -> Name.get_id na, LocalAssumEntry t | LocalDef (na,b,_) -> Name.get_id na, LocalDefEntry b (** 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 inductives which are recognized when a "Type" appears at the end of the conlusion in the source syntax. *) let rec check_anonymous_type ind = let open Glob_term in match ind.CAst.v with | GSort (GType []) -> true | GProd ( _, _, _, e) | GLetIn (_, _, _, e) | GLambda (_, _, _, e) | GApp (e, _) | GCast (e, _) -> check_anonymous_type e | _ -> false let make_conclusion_flexible evdref ty poly = if poly && isArity ty then let _, concl = destArity ty in match concl with | Type u -> (match Univ.universe_level u with | Some u -> evdref := Evd.make_flexible_variable !evdref true u | None -> ()) | _ -> () else () let is_impredicative env u = u = Prop Null || (is_impredicative_set env && u = Prop Pos) let interp_ind_arity env evdref ind = let c = intern_gen IsType env ind.ind_arity in let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in let t, impls = understand_tcc_evars env evdref ~expected_type:IsType c, imps in let pseudo_poly = check_anonymous_type c in let () = if not (Reductionops.is_arity env !evdref t) then user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity") in let t = EConstr.Unsafe.to_constr t in t, pseudo_poly, impls let interp_cstrs evdref env impls mldata arity ind = 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 (* Interpret the constructor types *) let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls evdref env ~impls %> on_fst EConstr.Unsafe.to_constr) ctyps') in (cnames, ctyps'', cimpls) let sign_level env evd sign = fst (List.fold_right (fun d (lev,env) -> match d with | LocalDef _ -> lev, push_rel d env | LocalAssum _ -> let s = destSort (Reduction.whd_all env (EConstr.Unsafe.to_constr (nf_evar evd (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d)))))) in let u = univ_of_sort s in (Univ.sup u lev, push_rel d env)) sign (Univ.type0m_univ,env)) let sup_list min = List.fold_left Univ.sup min let extract_level env evd min tys = let sorts = List.map (fun ty -> let ctx, concl = Reduction.dest_prod_assum env ty in sign_level env evd (LocalAssum (Anonymous, concl) :: ctx)) tys in sup_list min sorts let is_flexible_sort evd u = match Univ.Universe.level u with | Some l -> Evd.is_flexible_level evd l | None -> false let inductive_levels env evdref poly arities inds = let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in let levels = List.map (fun (x,(ctx,a)) -> if a = Prop Null then None else Some (univ_of_sort a)) destarities in let cstrs_levels, min_levels, sizes = CList.split3 (List.map2 (fun (_,tys,_) (arity,(ctx,du)) -> let len = List.length tys in let minlev = Sorts.univ_of_sort du in let minlev = if len > 1 && not (is_impredicative env du) then Univ.sup minlev Univ.type0_univ else minlev in let minlev = (** Indices contribute. *) if Indtypes.is_indices_matter () && List.length ctx > 0 then ( let ilev = sign_level env !evdref ctx in Univ.sup ilev minlev) else minlev in let clev = extract_level env !evdref minlev tys in (clev, minlev, len)) inds destarities) in (* Take the transitive closure of the system of constructors *) (* level constraints and remove the recursive dependencies *) let levels' = Universes.solve_constraints_system (Array.of_list levels) (Array.of_list cstrs_levels) (Array.of_list min_levels) in let evd, arities = CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len -> if is_impredicative env du then (** Any product is allowed here. *) evd, arity :: arities else (** If in a predicative sort, or asked to infer the type, we take the max of: - indices (if in indices-matter mode) - constructors - Type(1) if there is more than 1 constructor *) (** Constructors contribute. *) let evd = if Sorts.is_set du then if not (Evd.check_leq evd cu Univ.type0_univ) then raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType) else evd else evd (* Evd.set_leq_sort env evd (Type cu) du *) in let evd = if len >= 2 && Univ.is_type0m_univ cu then (** "Polymorphic" type constraint and more than one constructor, should not land in Prop. Add constraint only if it would land in Prop directly (no informative arguments as well). *) Evd.set_leq_sort env evd (Prop Pos) du else evd in let duu = Sorts.univ_of_sort du in let evd = if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then Evd.set_eq_sort env evd (Prop Null) du else evd else Evd.set_eq_sort env evd (Type cu) du in (evd, arity :: arities)) (!evdref,[]) (Array.to_list levels') destarities sizes in evdref := evd; List.rev arities let check_named (loc, na) = match na with | Name _ -> () | Anonymous -> let msg = str "Parameters must be named." in user_err ?loc msg let check_param = function | CLocalDef (na, _, _) -> check_named na | CLocalAssum (nas, Default _, _) -> List.iter check_named nas | CLocalAssum (nas, Generalized _, _) -> () | CLocalPattern _ -> assert false let interp_mutual_inductive (paramsl,indl) notations poly prv finite = check_all_names_different indl; List.iter check_param paramsl; let env0 = Global.env() in let pl = (List.hd indl).ind_univs in let ctx = Evd.make_evar_universe_context env0 pl in let evdref = ref Evd.(from_ctx ctx) in let impls, ((env_params, ctx_params), userimpls) = interp_context_evars env0 evdref paramsl in let ctx_params = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx_params in let indnames = List.map (fun ind -> ind.ind_name) indl in (* Names of parameters as arguments of the inductive type (defs removed) *) let assums = List.filter is_local_assum ctx_params in let params = List.map (RelDecl.get_name %> Name.get_id) assums in (* Interpret the arities *) let arities = List.map (interp_ind_arity env_params evdref) indl in let fullarities = List.map (fun (c, _, _) -> Term.it_mkProd_or_LetIn c ctx_params) arities in let env_ar = push_types env0 indnames fullarities in let env_ar_params = push_rel_context ctx_params env_ar in (* Compute interpretation metadatas *) let indimpls = List.map (fun (_, _, impls) -> userimpls @ lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in let impls = compute_internalization_env env0 ~impls (Inductive (params,true)) indnames fullarities indimpls in let implsforntn = compute_internalization_env env0 Variable indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = Metasyntax.with_syntax_protection (fun () -> (* Temporary declaration of notations and scopes *) List.iter (Metasyntax.set_notation_for_interpretation implsforntn) notations; (* Interpret the constructor types *) List.map3 (interp_cstrs env_ar_params evdref impls) mldatas arities indl) () in (* Try further to solve evars, and instantiate them *) let sigma = solve_remaining_evars all_and_fail_flags env_params !evdref Evd.empty in evdref := sigma; (* Compute renewed arities *) let nf,_ = e_nf_evars_and_universes evdref in let arities = List.map nf arities in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in let _ = List.iter2 (fun ty poly -> make_conclusion_flexible evdref ty poly) arities aritypoly in let arities = inductive_levels env_ar_params evdref poly arities constructors in let nf',_ = e_nf_evars_and_universes evdref in let nf x = nf' (nf x) in let arities = List.map nf' arities in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in let ctx_params = Context.Rel.map nf ctx_params in let evd = !evdref in let pl, uctx = Evd.universe_context ?names:pl evd in List.iter (fun c -> check_evars env_params Evd.empty evd (EConstr.of_constr c)) arities; Context.Rel.iter (fun c -> check_evars env0 Evd.empty evd (EConstr.of_constr c)) ctx_params; List.iter (fun (_,ctyps,_) -> List.iter (fun c -> check_evars env_ar_params Evd.empty evd (EConstr.of_constr c)) ctyps) constructors; (* Build the inductive entries *) let entries = List.map4 (fun ind arity template (cnames,ctypes,cimpls) -> { mind_entry_typename = ind.ind_name; mind_entry_arity = arity; mind_entry_template = template; mind_entry_consnames = cnames; mind_entry_lc = ctypes }) indl arities aritypoly constructors in let impls = let len = Context.Rel.nhyps ctx_params in List.map2 (fun indimpls (_,_,cimpls) -> indimpls, List.map (fun impls -> userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors in (* Build the mutual inductive entry *) { mind_entry_params = List.map prepare_param ctx_params; mind_entry_record = None; mind_entry_finite = finite; mind_entry_inds = entries; mind_entry_polymorphic = poly; mind_entry_private = if prv then Some false else None; mind_entry_universes = uctx; }, pl, impls (* Very syntactical equality *) let eq_local_binders bl1 bl2 = List.equal local_binder_eq bl1 bl2 let extract_coercions indl = let mkqid (_,((_,id),_)) = qualid_of_ident id in let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in List.map mkqid (List.flatten(List.map (fun (_,_,_,lc) -> extract lc) indl)) let extract_params indl = let paramsl = List.map (fun (_,params,_,_) -> params) indl in match paramsl with | [] -> anomaly (Pp.str "empty list of inductive types.") | params::paramsl -> if not (List.for_all (eq_local_binders params) paramsl) then user_err Pp.(str "Parameters should be syntactically the same for each inductive type."); params let extract_inductive indl = List.map (fun (((_,indname),pl),_,ar,lc) -> { ind_name = indname; ind_univs = pl; ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (GType [])) ar; ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc }) indl let extract_mutual_inductive_declaration_components indl = let indl,ntnl = List.split indl in let params = extract_params indl in let coes = extract_coercions indl in let indl = extract_inductive indl in (params,indl), coes, List.flatten ntnl let is_recursive mie = let rec is_recursive_constructor lift typ = match Term.kind_of_term typ with | Prod (_,arg,rest) -> not (EConstr.Vars.noccurn Evd.empty (** FIXME *) lift (EConstr.of_constr arg)) || is_recursive_constructor (lift+1) rest | LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest | _ -> false in match mie.mind_entry_inds with | [ind] -> let nparams = List.length mie.mind_entry_params in List.exists (fun t -> is_recursive_constructor (nparams+1) t) ind.mind_entry_lc | _ -> false let declare_mutual_inductive_with_eliminations mie pl impls = (* spiwack: raises an error if the structure is supposed to be non-recursive, but isn't *) begin match mie.mind_entry_finite with | BiFinite when is_recursive mie -> if Option.has_some mie.mind_entry_record then user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.") else user_err Pp.(str ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.")) | _ -> () end; let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in let (_, kn), prim = declare_mind mie in let mind = Global.mind_of_delta_kn kn in List.iteri (fun i (indimpls, constrimpls) -> let ind = (mind,i) in let gr = IndRef ind in maybe_declare_manual_implicits false gr indimpls; Universes.register_universe_binders gr pl; List.iteri (fun j impls -> maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls) constrimpls) impls; let warn_prim = match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false in if_verbose Feedback.msg_info (minductive_message warn_prim names); if mie.mind_entry_private == None then declare_default_schemes mind; mind type one_inductive_impls = Impargs.manual_explicitation list (* for inds *)* Impargs.manual_explicitation list list (* for constrs *) let do_mutual_inductive indl poly prv finite = let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) let mie,pl,impls = interp_mutual_inductive indl ntns poly prv finite in (* Declare the mutual inductive block with its associated schemes *) ignore (declare_mutual_inductive_with_eliminations mie pl impls); (* Declare the possible notations of inductive types *) List.iter Metasyntax.add_notation_interpretation ntns; (* Declare the coercions *) List.iter (fun qid -> Class.try_add_new_coercion (locate qid) ~local:false poly) coes; (* If positivity is assumed declares itself as unsafe. *) if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else () (* 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 (List.remove cmp x 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 non_full_mutual_message x xge y yge isfix rest = let reason = if Id.List.mem x yge then pr_id y ++ str " depends on " ++ pr_id x ++ strbrk " but not conversely" else if Id.List.mem y xge then pr_id x ++ str " depends on " ++ pr_id y ++ strbrk " but not conversely" else pr_id y ++ str " and " ++ pr_id x ++ strbrk " are not mutually dependent" in let e = if List.is_empty rest then reason else strbrk "e.g., " ++ reason in let k = if isfix then "fixpoint" else "cofixpoint" in let w = if isfix then strbrk "Well-foundedness check may fail unexpectedly." ++ fnl() else mt () in strbrk "Not a fully mutually defined " ++ str k ++ fnl () ++ str "(" ++ e ++ str ")." ++ fnl () ++ w let warn_non_full_mutual = CWarnings.create ~name:"non-full-mutual" ~category:"fixpoints" (fun (x,xge,y,yge,isfix,rest) -> non_full_mutual_message x xge y yge isfix rest) let check_mutuality env evd isfix fixl = let names = List.map fst fixl in let preorder = List.map (fun (id,def) -> (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env evd id' (EConstr.of_constr def)) 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,isfix,rest) | _ -> () type structured_fixpoint_expr = { fix_name : Id.t; fix_univs : lident list option; fix_annot : Id.t Loc.located option; fix_binders : local_binder_expr list; fix_body : constr_expr option; fix_type : constr_expr } let interp_fix_context env evdref isfix fix = let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in let impl_env, ((env', ctx), imps) = interp_context_evars env evdref before in let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env ~shift:(Context.Rel.nhyps ctx) env' evdref after in let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot) let interp_fix_ccl evdref impls (env,_) fix = let (c, impl) = interp_type_evars_impls ~impls env evdref fix.fix_type in (c, impl) let interp_fix_body env_rec evdref impls (_,ctx) fix ccl = let open EConstr in Option.map (fun body -> let env = push_rel_context ctx env_rec in let body = interp_casted_constr_evars env evdref ~impls body ccl in it_mkLambda_or_LetIn body ctx) fix.fix_body let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps = let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r)) let _ = Obligations.declare_fix_ref := (fun ?opaque k ctx f d t imps -> declare_fix ?opaque k [] ctx f d t imps) let prepare_recursive_declaration fixnames fixtypes fixdefs = let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in let names = List.map (fun id -> Name id) fixnames in (Array.of_list names, Array.of_list fixtypes, Array.of_list defs) (* Jump over let-bindings. *) let compute_possible_guardness_evidences (ctx,_,recindex) = (* A recursive index is characterized by the number of lambdas to skip before finding the relevant inductive argument *) match recindex with | Some i -> [i] | None -> (* 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 ?) *) List.interval 0 (Context.Rel.nhyps ctx - 1) type recursive_preentry = Id.t list * constr option list * types list (* Wellfounded definition *) open Coqlib let contrib_name = "Program" let subtac_dir = [contrib_name] let fixsub_module = subtac_dir @ ["Wf"] let tactics_module = subtac_dir @ ["Tactics"] let init_reference dir s () = Coqlib.coq_reference "Command" dir s let init_constant dir s evdref = let (sigma, c) = Evarutil.new_global !evdref (Coqlib.coq_reference "Command" dir s) in evdref := sigma; c let make_ref l s = init_reference l s let fix_proto = init_constant tactics_module "fix_proto" let fix_sub_ref = make_ref fixsub_module "Fix_sub" let measure_on_R_ref = make_ref fixsub_module "MR" let well_founded = init_constant ["Init"; "Wf"] "well_founded" let mkSubset evdref name typ prop = let open EConstr in mkApp (Evarutil.e_new_global evdref (delayed_force build_sigma).typ, [| typ; mkLambda (name, typ, prop) |]) let sigT = Lazy.from_fun build_sigma_type let make_qref s = Qualid (Loc.tag @@ qualid_of_string s) let lt_ref = make_qref "Init.Peano.lt" let rec telescope evdref l = let open EConstr in let open Vars in match l with | [] -> assert false | [LocalAssum (n, t)] -> t, [LocalDef (n, mkRel 1, t)], mkRel 1 | LocalAssum (n, t) :: tl -> let ty, tys, (k, constr) = List.fold_left (fun (ty, tys, (k, constr)) decl -> let t = RelDecl.get_type decl in let pred = mkLambda (RelDecl.get_name decl, t, ty) in let ty = Evarutil.e_new_global evdref (Lazy.force sigT).typ in let intro = Evarutil.e_new_global evdref (Lazy.force sigT).intro in let sigty = mkApp (ty, [|t; pred|]) in let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in (sigty, pred :: tys, (succ k, intro))) (t, [], (2, mkRel 1)) tl in let (last, subst) = List.fold_right2 (fun pred decl (prev, subst) -> let t = RelDecl.get_type decl in let p1 = Evarutil.e_new_global evdref (Lazy.force sigT).proj1 in let p2 = Evarutil.e_new_global evdref (Lazy.force sigT).proj2 in let proj1 = applist (p1, [t; pred; prev]) in let proj2 = applist (p2, [t; pred; prev]) in (lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst)) (List.rev tys) tl (mkRel 1, []) in ty, (LocalDef (n, last, t) :: subst), constr | LocalDef (n, b, t) :: tl -> let ty, subst, term = telescope evdref tl in ty, (LocalDef (n, b, t) :: subst), lift 1 term let nf_evar_context sigma ctx = List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx let build_wellfounded (recname,pl,n,bl,arityc,body) poly 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 Coqlib.check_required_library ["Coq";"Program";"Wf"]; let env = Global.env() in let ctx = Evd.make_evar_universe_context env pl in let evdref = ref (Evd.from_ctx ctx) in let _, ((env', binders_rel), impls) = interp_context_evars env evdref bl in let len = List.length binders_rel in let top_env = push_rel_context binders_rel env in let top_arity = interp_type_evars top_env evdref arityc in let full_arity = it_mkProd_or_LetIn top_arity binders_rel in let argtyp, letbinders, make = telescope evdref binders_rel in let argname = Id.of_string "recarg" in let arg = LocalAssum (Name argname, argtyp) in let binders = letbinders @ [arg] in let binders_env = push_rel_context binders_rel env in let rel, _ = interp_constr_evars_impls env evdref r in let relty = Typing.unsafe_type_of env !evdref rel in let relargty = let error () = user_err ?loc:(constr_loc r) ~hdr:"Command.build_wellfounded" (Printer.pr_econstr_env env !evdref rel ++ str " is not an homogeneous binary relation.") in try let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in match ctx, EConstr.kind !evdref ar with | [LocalAssum (_,t); LocalAssum (_,u)], Sort s when Sorts.is_prop (ESorts.kind !evdref s) && Reductionops.is_conv env !evdref t u -> t | _, _ -> error () with e when CErrors.noncritical e -> error () in let relargty = EConstr.Unsafe.to_constr relargty in let measure = interp_casted_constr_evars binders_env evdref measure relargty in let wf_rel, wf_rel_fun, measure_fn = let measure_body, measure = it_mkLambda_or_LetIn measure letbinders, it_mkLambda_or_LetIn measure binders in let comb = Evarutil.e_new_global evdref (delayed_force measure_on_R_ref) in let relargty = EConstr.of_constr relargty in let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in let wf_rel_fun x y = mkApp (rel, [| subst1 x measure_body; subst1 y measure_body |]) in wf_rel, wf_rel_fun, measure in let wf_proof = mkApp (well_founded evdref, [| argtyp ; wf_rel |]) in let argid' = Id.of_string (Id.to_string argname ^ "'") in let wfarg len = LocalAssum (Name argid', mkSubset evdref (Name argid') argtyp (wf_rel_fun (mkRel 1) (mkRel (len + 1)))) in let intern_bl = wfarg 1 :: [arg] in let _intern_env = push_rel_context intern_bl env in let proj = Evarutil.e_new_global evdref (delayed_force build_sigma).Coqlib.proj1 in let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in let projection = (* in wfarg :: arg :: before *) mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |]) in let top_arity_let = it_mkLambda_or_LetIn top_arity letbinders in let intern_arity = substl [projection] top_arity_let in (* substitute the projection of wfarg for something, now intern_arity is in wfarg :: arg *) let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in let curry_fun = let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in let intro = Evarutil.e_new_global evdref (delayed_force build_sigma).Coqlib.intro in let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in let rcurry = mkApp (rel, [| measure; lift len measure |]) in let lam = LocalAssum (Name (Id.of_string "recproof"), rcurry) in let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in LocalDef (Name recname, body, ty) in let fun_bl = intern_fun_binder :: [arg] in let lift_lets = lift_rel_context 1 letbinders in let intern_body = let ctx = LocalAssum (Name recname, get_type curry_fun) :: binders_rel in let (r, l, impls, scopes) = Constrintern.compute_internalization_data env Constrintern.Recursive (EConstr.Unsafe.to_constr full_arity) impls in let newimpls = Id.Map.singleton recname (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))], scopes @ [None]) in interp_casted_constr_evars (push_rel_context ctx env) evdref ~impls:newimpls body (EConstr.Unsafe.to_constr (lift 1 top_arity)) in let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in let prop = mkLambda (Name argname, argtyp, top_arity_let) in let def = mkApp (Evarutil.e_new_global evdref (delayed_force fix_sub_ref), [| argtyp ; wf_rel ; Evarutil.e_new_evar env evdref ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof; prop |]) in let def = Typing.e_solve_evars env evdref def in let _ = evdref := Evarutil.nf_evar_map !evdref in let def = mkApp (def, [|intern_body_lam|]) in let binders_rel = nf_evar_context !evdref binders_rel in let binders = nf_evar_context !evdref binders in let top_arity = Evarutil.nf_evar !evdref top_arity in let hook, recname, typ = if List.length binders_rel > 1 then let name = add_suffix recname "_func" in let hook l gr _ = let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let ty = EConstr.Unsafe.to_constr ty in let pl, univs = Evd.universe_context ?names:pl !evdref in (*FIXME poly? *) let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in (** FIXME: include locality *) let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in let gr = ConstRef c in if Impargs.is_implicit_args () || not (List.is_empty impls) then Impargs.declare_manual_implicits false gr [impls] in let typ = it_mkProd_or_LetIn top_arity binders in hook, name, typ else let typ = it_mkProd_or_LetIn top_arity binders_rel in let hook l gr _ = if Impargs.is_implicit_args () || not (List.is_empty impls) then Impargs.declare_manual_implicits false gr [impls] in hook, recname, typ in let hook = Lemmas.mk_hook hook in let fullcoqc = EConstr.to_constr !evdref def in let fullctyp = EConstr.to_constr !evdref typ in Obligations.check_evars env !evdref; let evars, _, evars_def, evars_typ = Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp in let ctx = Evd.evar_universe_context !evdref in ignore(Obligations.add_definition recname ~term:evars_def ?pl evars_typ ctx evars ~hook) let interp_recursive isfix fixl notations = let open Context.Named.Declaration in let open EConstr in let env = Global.env() in let fixnames = List.map (fun fix -> fix.fix_name) fixl in (* Interp arities allowing for unresolved types *) let all_universes = List.fold_right (fun sfe acc -> match sfe.fix_univs , acc with | None , acc -> acc | x , None -> x | Some ls , Some us -> if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) ls us) then user_err Pp.(str "(co)-recursive definitions should all have the same universe binders"); Some us) fixl None in let ctx = Evd.make_evar_universe_context env all_universes in let evdref = ref (Evd.from_ctx ctx) in let fixctxs, fiximppairs, fixannots = List.split3 (List.map (interp_fix_context env evdref isfix) fixl) in let fixctximpenvs, fixctximps = List.split fiximppairs in let fixccls,fixcclimps = List.split (List.map3 (interp_fix_ccl evdref) fixctximpenvs fixctxs fixl) in let fixtypes = List.map2 build_fix_type fixctxs fixccls in let fixtypes = List.map (fun c -> nf_evar !evdref c) fixtypes in let fiximps = List.map3 (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (Context.Rel.nhyps ctx) cclimps)) fixctximps fixcclimps fixctxs in let rec_sign = List.fold_left2 (fun env' id t -> if Flags.is_program_mode () then let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref t in let fixprot = try let app = mkApp (fix_proto evdref, [|sort; t|]) in Typing.e_solve_evars env evdref app with e when CErrors.noncritical e -> t in LocalAssum (id,fixprot) :: env' else LocalAssum (id,t) :: env') [] fixnames fixtypes in let env_rec = push_named_context rec_sign env in (* Get interpretation metadatas *) let fixtypes = List.map EConstr.Unsafe.to_constr fixtypes in let fixccls = List.map EConstr.Unsafe.to_constr fixccls in let impls = compute_internalization_env env Recursive fixnames fixtypes fiximps in (* Interp bodies with rollback because temp use of notations/implicit *) let fixdefs = Metasyntax.with_syntax_protection (fun () -> List.iter (Metasyntax.set_notation_for_interpretation impls) notations; List.map4 (fun fixctximpenv -> interp_fix_body env_rec evdref (Id.Map.fold Id.Map.add fixctximpenv impls)) fixctximpenvs fixctxs fixl fixccls) () in (* Instantiate evars and check all are resolved *) let evd = solve_unif_constraints_with_heuristics env_rec !evdref in let evd, nf = nf_evars_and_universes evd in let fixdefs = List.map (fun c -> Option.map EConstr.Unsafe.to_constr c) fixdefs in let fixdefs = List.map (Option.map nf) fixdefs in let fixtypes = List.map nf fixtypes in let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in (* Build the fix declaration block *) (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots let check_recursive isfix env evd (fixnames,fixdefs,_) = check_evars_are_solved env evd Evd.empty; if List.for_all Option.has_some fixdefs then begin let fixdefs = List.map Option.get fixdefs in check_mutuality env evd isfix (List.combine fixnames fixdefs) end let interp_fixpoint l ntns = let (env,_,pl,evd),fix,info = interp_recursive true l ntns in check_recursive true env evd fix; (fix,pl,Evd.evar_universe_context evd,info) let interp_cofixpoint l ntns = let (env,_,pl,evd),fix,info = interp_recursive false l ntns in check_recursive false env evd fix; (fix,pl,Evd.evar_universe_context evd,info) let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = List.map3 (fun id t (ctx,imps,_) -> ((id,pl),(t,(List.map RelDecl.get_name ctx,imps)))) fixnames fixtypes fiximps in let init_tac = Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in let evd = Evd.from_ctx ctx in Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint) evd (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) else begin (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let env = Global.env() in let indexes = search_guard env indexes fixdecls in let fiximps = List.map (fun (n,r,p) -> r) fiximps in let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let pl, ctx = Evd.universe_context ?names:pl evd in ignore (List.map4 (declare_fix (local, poly, Fixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) fixpoint_message (Some indexes) fixnames; end; (* Declare notations *) List.iter Metasyntax.add_notation_interpretation ntns let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns = if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = List.map3 (fun id t (ctx,imps,_) -> ((id,pl),(t,(List.map RelDecl.get_name ctx,imps)))) fixnames fixtypes fiximps in let init_tac = Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in let evd = Evd.from_ctx ctx in Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint) evd (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) else begin (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in let vars = Universes.universes_of_constr (List.hd fixdecls) in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in let pl, ctx = Evd.universe_context ?names:pl evd in ignore (List.map4 (declare_fix (local, poly, CoFixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) cofixpoint_message fixnames end; (* Declare notations *) List.iter Metasyntax.add_notation_interpretation ntns let extract_decreasing_argument limit = function | (na,CStructRec) -> na | (na,_) when not limit -> na | _ -> user_err Pp.(str "Only structural decreasing is supported for a non-Program Fixpoint") let extract_fixpoint_components limit l = let fixl, ntnl = List.split l in let fixl = List.map (fun (((_,id),pl),ann,bl,typ,def) -> let ann = extract_decreasing_argument limit ann in {fix_name = id; fix_annot = ann; fix_univs = pl; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in fixl, List.flatten ntnl let extract_cofixpoint_components l = let fixl, ntnl = List.split l in List.map (fun (((_,id),pl),bl,typ,def) -> {fix_name = id; fix_annot = None; fix_univs = pl; fix_binders = bl; fix_body = def; fix_type = typ}) fixl, List.flatten ntnl let out_def = function | Some def -> def | None -> user_err Pp.(str "Program Fixpoint needs defined bodies.") let collect_evars_of_term evd c ty = let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in 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 local p fixkind fixl ntns = let isfix = fixkind != Obligations.IsCoFixpoint in let (env, rec_sign, pl, evd), fix, info = interp_recursive isfix fixl ntns in (* Program-specific code *) (* Get the interesting evars, those that were not instanciated *) 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 = (* Generalize by the recursive prototypes *) let def = EConstr.to_constr evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign) and typ = EConstr.to_constr evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign) in let evm = collect_evars_of_term evd def typ in let evars, _, def, typ = Obligations.eterm_obligations env id evm (List.length rec_sign) def typ in (id, def, typ, imps, evars) in let (fixnames,fixdefs,fixtypes) = fix in let fiximps = List.map pi2 info in let fixdefs = List.map out_def fixdefs in let defs = List.map4 collect_evars fixnames fixdefs fixtypes fiximps in let () = if isfix then begin let possible_indexes = List.map compute_possible_guardness_evidences info in let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames), Array.of_list fixtypes, Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs) in let indexes = Pretyping.search_guard (Global.env ()) possible_indexes fixdecls in List.iteri (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) fixl end in let ctx = Evd.evar_universe_context evd in let kind = match fixkind with | Obligations.IsFixpoint _ -> (local, p, Fixpoint) | Obligations.IsCoFixpoint -> (local, p, CoFixpoint) in Obligations.add_mutual_definitions defs ~kind ?pl ctx ntns fixkind let do_program_fixpoint local poly l = let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in match g, l with | [(n, CWfRec r)], [((((_,id),pl),_,bl,typ,def),ntn)] -> let recarg = match n with | Some n -> mkIdentC (snd n) | None -> user_err ~hdr:"do_program_fixpoint" (str "Recursive argument required for well-founded fixpoints") in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn | [(n, CMeasureRec (m, r))], [((((_,id),pl),_,bl,typ,def),ntn)] -> build_wellfounded (id, pl, n, bl, typ, out_def def) poly (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn | _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g -> let fixl,ntns = extract_fixpoint_components true l in let fixkind = Obligations.IsFixpoint g in do_program_recursive local poly fixkind fixl ntns | _, _ -> user_err ~hdr:"do_program_fixpoint" (str "Well-founded fixpoints not allowed in mutually recursive blocks") let check_safe () = let open Declarations in let flags = Environ.typing_flags (Global.env ()) in flags.check_universes && flags.check_guarded let do_fixpoint local poly l = if Flags.is_program_mode () then do_program_fixpoint local poly l else let fixl, ntns = extract_fixpoint_components true l in let (_, _, _, info as fix) = interp_fixpoint fixl ntns in let possible_indexes = List.map compute_possible_guardness_evidences info in declare_fixpoint local poly fix possible_indexes ntns; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () let do_cofixpoint local poly l = let fixl,ntns = extract_cofixpoint_components l in if Flags.is_program_mode () then do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns else let cofix = interp_cofixpoint fixl ntns in declare_cofixpoint local poly cofix ntns; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()