diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 177 | ||||
| -rw-r--r-- | vernac/classes.mli | 1 | ||||
| -rw-r--r-- | vernac/comAssumption.ml | 182 | ||||
| -rw-r--r-- | vernac/comAssumption.mli | 34 | ||||
| -rw-r--r-- | vernac/comDefinition.ml | 131 | ||||
| -rw-r--r-- | vernac/comDefinition.mli | 30 | ||||
| -rw-r--r-- | vernac/comFixpoint.ml | 356 | ||||
| -rw-r--r-- | vernac/comFixpoint.mli | 93 | ||||
| -rw-r--r-- | vernac/comInductive.ml | 456 | ||||
| -rw-r--r-- | vernac/comInductive.mli | 65 | ||||
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 342 | ||||
| -rw-r--r-- | vernac/comProgramFixpoint.mli | 12 | ||||
| -rw-r--r-- | vernac/command.ml | 1365 | ||||
| -rw-r--r-- | vernac/command.mli | 163 | ||||
| -rw-r--r-- | vernac/declareDef.ml | 3 | ||||
| -rw-r--r-- | vernac/explainErr.ml | 3 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 101 | ||||
| -rw-r--r-- | vernac/lemmas.mli | 5 | ||||
| -rw-r--r-- | vernac/mltop.ml | 2 | ||||
| -rw-r--r-- | vernac/obligations.ml | 12 | ||||
| -rw-r--r-- | vernac/obligations.mli | 3 | ||||
| -rw-r--r-- | vernac/record.ml | 98 | ||||
| -rw-r--r-- | vernac/record.mli | 2 | ||||
| -rw-r--r-- | vernac/topfmt.ml | 17 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 6 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 50 | ||||
| -rw-r--r-- | vernac/vernacstate.ml | 28 |
27 files changed, 1974 insertions, 1763 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index b80741269..c2e9a5ab4 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -8,10 +8,7 @@ (*i*) open Names -open Term -open Constr -open Vars -open Environ +open EConstr open Nametab open CErrors open Util @@ -70,7 +67,7 @@ let existing_instance glob g info = let c = global g in let info = Option.default Hints.empty_hint_info info in let instance, _ = Global.type_of_global_in_context (Global.env ()) c in - let _, r = decompose_prod_assum instance in + let _, r = Term.decompose_prod_assum instance in match class_of_constr Evd.empty (EConstr.of_constr r) with | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob (*FIXME*) (Flags.use_polymorphic_flag ()) c) @@ -83,19 +80,20 @@ let mismatched_props env n m = mismatched_ctx_inst env Properties n m (* Declare everything in the parameters as implicit, and the class instance as well *) -let type_ctx_instance evars env ctx inst subst = - let rec aux (subst, instctx) l = function +let type_ctx_instance env sigma ctx inst subst = + let open Vars in + let rec aux (sigma, subst, instctx) l = function decl :: ctx -> let t' = substl subst (RelDecl.get_type decl) in - let c', l = + let (sigma, c'), l = match decl with - | LocalAssum _ -> EConstr.Unsafe.to_constr (interp_casted_constr_evars env evars (List.hd l) t'), List.tl l - | LocalDef (_,b,_) -> substl subst b, l + | LocalAssum _ -> interp_casted_constr_evars env sigma (List.hd l) t', List.tl l + | LocalDef (_,b,_) -> (sigma, substl subst b), l in let d = RelDecl.get_name decl, Some c', t' in - aux (c' :: subst, d :: instctx) l ctx - | [] -> subst - in aux (subst, []) inst (List.rev ctx) + aux (sigma, c' :: subst, d :: instctx) l ctx + | [] -> sigma, subst + in aux (sigma, subst, []) inst (List.rev ctx) let id_of_class cl = match cl.cl_impl with @@ -112,31 +110,31 @@ let instance_hook k info global imps ?hook cst = Typeclasses.declare_instance (Some info) (not global) cst; (match hook with Some h -> h cst | None -> ()) -let declare_instance_constant k info global imps ?hook id decl poly evm term termtype = +let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype = let kind = IsDefinition Instance in - let evm = - let levels = Univ.LSet.union (Univops.universes_of_constr termtype) - (Univops.universes_of_constr term) in - Evd.restrict_universe_context evm levels + let sigma = + let env = Global.env () in + let levels = Univ.LSet.union (Univops.universes_of_constr env termtype) + (Univops.universes_of_constr env term) in + Evd.restrict_universe_context sigma levels in - let uctx = Evd.check_univ_decl ~poly evm decl in + let uctx = Evd.check_univ_decl ~poly sigma decl in let entry = Declare.definition_entry ~types:termtype ~univs:uctx term in let cdecl = (DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in Declare.definition_message id; - Universes.register_universe_binders (ConstRef kn) (Evd.universe_binders evm); + Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma); instance_hook k info global imps ?hook (ConstRef kn); id let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) - poly ctx (instid, bk, cl) props ?(generalize=true) + ~program_mode poly ctx (instid, bk, cl) props ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in let ((loc, instid), pl) = instid in - let evd, decl = Univdecls.interp_univ_decl_opt env pl in - let evars = ref evd in + let sigma, decl = Univdecls.interp_univ_decl_opt env pl in let tclass, ids = match bk with | Decl_kinds.Implicit -> @@ -154,26 +152,26 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) else tclass in - let k, u, cty, ctx', ctx, len, imps, subst = - let impls, ((env', ctx), imps) = interp_context_evars env evars ctx in - let ctx = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) ctx in - let c', imps' = interp_type_evars_impls ~impls env' evars tclass in - let c' = EConstr.Unsafe.to_constr c' in + let sigma, k, u, cty, ctx', ctx, len, imps, subst = + let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in + let sigma, (c', imps') = interp_type_evars_impls ~impls env' sigma tclass in let len = List.length ctx in let imps = imps @ Impargs.lift_implicits len imps' in - let ctx', c = decompose_prod_assum c' in + let ctx', c = decompose_prod_assum sigma c' in let ctx'' = ctx' @ ctx in - let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) !evars (EConstr.of_constr c) in - let u = EConstr.EInstance.kind !evars u in - let cl = Typeclasses.typeclass_univ_instance (k, u) in - let _, args = + let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) sigma c in + let u_s = EInstance.kind sigma u in + let cl = Typeclasses.typeclass_univ_instance (k, u_s) in + let args = List.map of_constr args in + let cl_context = List.map (Termops.map_rel_decl of_constr) (snd cl.cl_context) in + let _, args = List.fold_right (fun decl (args, args') -> match decl with | LocalAssum _ -> (List.tl args, List.hd args :: args') - | LocalDef (_,b,_) -> (args, substl args' b :: args')) - (snd cl.cl_context) (args, []) + | LocalDef (_,b,_) -> (args, Vars.substl args' b :: args')) + cl_context (args, []) in - cl, u, c', ctx', ctx, len, imps, args + sigma, cl, u, c', ctx', ctx, len, imps, args in let id = match instid with @@ -187,9 +185,8 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) Namegen.next_global_ident_away i (Termops.vars_of_env env) in let env' = push_rel_context ctx env in - evars := Evarutil.nf_evar_map !evars; - evars := resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env !evars; - let subst = List.map (fun c -> EConstr.Unsafe.to_constr (Evarutil.nf_evar !evars (EConstr.of_constr c))) subst in + let sigma = Evarutil.nf_evar_map sigma in + let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in if abstract then begin let subst = List.fold_left2 @@ -197,18 +194,16 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) [] subst (snd k.cl_context) in let (_, ty_constr) = instance_constructor (k,u) subst in - let nf, subst = Evarutil.e_nf_evars_and_universes evars in - let termtype = - let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - nf t - in - Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype); - let univs = Evd.check_univ_decl ~poly !evars decl in + let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in + let sigma,_ = Evarutil.nf_evars_and_universes sigma in + Pretyping.check_evars env Evd.empty sigma termtype; + let univs = Evd.check_univ_decl ~poly sigma decl in + let termtype = to_constr sigma termtype in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id (ParameterEntry (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in - Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars); + Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); instance_hook k pri global imps ?hook (ConstRef cst); id end else ( @@ -220,16 +215,16 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) Some (Inl fs) | Some (_, t) -> Some (Inr t) | None -> - if Flags.is_program_mode () then Some (Inl []) + if program_mode then Some (Inl []) else None in - let subst = + let subst, sigma = match props with - | None -> if List.is_empty k.cl_props then Some (Inl subst) else None + | None -> + (if List.is_empty k.cl_props then Some (Inl subst) else None), sigma | Some (Inr term) -> - let c = interp_casted_constr_evars env' evars term cty in - let c = EConstr.Unsafe.to_constr c in - Some (Inr (c, subst)) + let sigma, c = interp_casted_constr_evars env' sigma term cty in + Some (Inr (c, subst)), sigma | Some (Inl props) -> let get_id = function @@ -266,9 +261,10 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) | (n, _) :: _ -> unbound_method env' k.cl_impl (get_id n) | _ -> - Some (Inl (type_ctx_instance evars (push_rel_context ctx' env') - k.cl_props props subst)) - in + let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in + let sigma, res = type_ctx_instance (push_rel_context ctx' env') sigma kcl_props props subst in + Some (Inl res), sigma + in let term, termtype = match subst with | None -> let termtype = it_mkProd_or_LetIn cty ctx in @@ -280,34 +276,30 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) in let (app, ty_constr) = instance_constructor (k,u) subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let term = Termops.it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in + let term = it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in Some term, termtype | Some (Inr (def, subst)) -> let termtype = it_mkProd_or_LetIn cty ctx in - let term = Termops.it_mkLambda_or_LetIn def ctx in + let term = it_mkLambda_or_LetIn def ctx in Some term, termtype in - let _ = - evars := Evarutil.nf_evar_map !evars; - evars := Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true - env !evars; - (* Try resolving fields that are typeclasses automatically. *) - evars := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false - env !evars - in - let _ = evars := Evarutil.nf_evar_map_undefined !evars in - let evm, nf = Evarutil.nf_evar_map_universes !evars in - let termtype = nf termtype in - let _ = (* Check that the type is free of evars now. *) - Pretyping.check_evars env Evd.empty evm (EConstr.of_constr termtype) - in - let term = Option.map nf term in - if not (Evd.has_undefined evm) && not (Option.is_empty term) then + let sigma = Evarutil.nf_evar_map sigma in + let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env sigma in + (* Try resolving fields that are typeclasses automatically. *) + let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false env sigma in + let sigma = Evarutil.nf_evar_map_undefined sigma in + (* Beware of this step, it is required as to minimize universes. *) + let sigma, _nf = Evarutil.nf_evar_map_universes sigma in + (* Check that the type is free of evars now. *) + Pretyping.check_evars env Evd.empty sigma termtype; + let termtype = to_constr sigma termtype in + let term = Option.map (to_constr sigma) term in + if not (Evd.has_undefined sigma) && not (Option.is_empty term) then declare_instance_constant k pri global imps ?hook id decl - poly evm (Option.get term) termtype - else if Flags.is_program_mode () || refine || Option.is_empty term then begin + poly sigma (Option.get term) termtype + else if program_mode || refine || Option.is_empty term then begin let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in - if Flags.is_program_mode () then + if program_mode then let hook vis gr _ = let cst = match gr with ConstRef kn -> kn | _ -> assert false in Impargs.declare_manual_implicits false gr ~enriching:false [imps]; @@ -317,12 +309,12 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) match term with | Some t -> let obls, _, constr, typ = - Obligations.eterm_obligations env id evm 0 t termtype + Obligations.eterm_obligations env id sigma 0 t termtype in obls, Some constr, typ | None -> [||], None, termtype in let hook = Lemmas.mk_hook hook in - let ctx = Evd.evar_universe_context evm in + let ctx = Evd.evar_universe_context sigma in ignore (Obligations.add_definition id ?term:constr ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls); id @@ -333,16 +325,16 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) the pretyping after the proof has opened. As a consequence, we use the low-level primitives to code the refinement manually.*) - let gls = List.rev (Evd.future_goals evm) in - let evm = Evd.reset_future_goals evm in - Lemmas.start_proof id ~pl:decl kind evm (EConstr.of_constr termtype) + let gls = List.rev (Evd.future_goals sigma) in + let sigma = Evd.reset_future_goals sigma in + Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype) (Lemmas.mk_hook (fun _ -> instance_hook k pri global imps ?hook)); (* spiwack: I don't know what to do with the status here. *) if not (Option.is_empty term) then let init_refine = Tacticals.New.tclTHENLIST [ - Refine.refine ~typecheck:false (fun evm -> (evm,EConstr.of_constr (Option.get term))); + Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term))); Proofview.Unsafe.tclNEWGOALS gls; Tactics.New.reduce_after_refine; ] @@ -356,6 +348,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) else CErrors.user_err Pp.(str "Unsolved obligations remaining.")) let named_of_rel_context l = + let open Vars in let acc, ctx = List.fold_right (fun decl (subst, ctx) -> @@ -369,20 +362,20 @@ let named_of_rel_context l = let context poly l = let env = Global.env() in - let evars = ref (Evd.from_env env) in - let _, ((env', fullctx), impls) = interp_context_evars env evars l in - let fullctx = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) fullctx in - let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in - let fullctx = Context.Rel.map subst fullctx in - let ce t = Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr t) in + let sigma = Evd.from_env env in + let sigma, (_, ((env', fullctx), impls)) = interp_context_evars env sigma l in + (* Note, we must use the normalized evar from now on! *) + let sigma,_ = Evarutil.nf_evars_and_universes sigma in + let ce t = Pretyping.check_evars env Evd.empty sigma t in let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in let ctx = try named_of_rel_context fullctx with e when CErrors.noncritical e -> user_err Pp.(str "Anonymous variables not allowed in contexts.") in - let uctx = ref (Evd.universe_context_set !evars) in + let uctx = ref (Evd.universe_context_set sigma) in let fn status (id, b, t) = + let b, t = Option.map (to_constr sigma) b, to_constr sigma t in if Lib.is_modtype () && not (Lib.sections_are_opened ()) then (* Declare the universe context once *) let univs = if poly @@ -398,7 +391,7 @@ let context poly l = (DefinitionEntry entry, IsAssumption Logical) in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in - match class_of_constr !evars (EConstr.of_constr t) with + match class_of_constr sigma (of_constr t) with | Some (rels, ((tc,_), args) as _cl) -> add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (*FIXME*) poly (ConstRef cst)); @@ -418,7 +411,7 @@ let context poly l = in let nstatus = match b with | None -> - pi3 (Command.declare_assumption false decl (t, univs) Universes.empty_binders [] impl + pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl Vernacexpr.NoInline (Loc.tag id)) | Some b -> let decl = (Discharge, poly, Definition) in diff --git a/vernac/classes.mli b/vernac/classes.mli index c0f03227c..d47c6a6f8 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -41,6 +41,7 @@ val new_instance : ?abstract:bool -> (** Not abstract by default. *) ?global:bool -> (** Not global by default. *) ?refine:bool -> (** Allow refinement *) + program_mode:bool -> Decl_kinds.polymorphic -> local_binder_expr list -> Vernacexpr.typeclass_constraint -> diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml new file mode 100644 index 000000000..5d7adb24a --- /dev/null +++ b/vernac/comAssumption.ml @@ -0,0 +1,182 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open CErrors +open Util +open Vars +open Environ +open Declare +open Names +open Globnames +open Constrexpr_ops +open Constrintern +open Impargs +open Decl_kinds +open Pretyping +open Vernacexpr +open Entries + +(* 2| Variable/Hypothesis/Parameter/Axiom declarations *) + +let axiom_into_instance = ref false + +let _ = + let open Goptions in + declare_bool_option + { optdepr = false; + optname = "automatically declare axioms whose type is a typeclass as instances"; + optkey = ["Typeclasses";"Axioms";"Are";"Instances"]; + optread = (fun _ -> !axiom_into_instance); + optwrite = (:=) axiom_into_instance; } + +let should_axiom_into_instance = function + | Discharge -> + (* The typeclass behaviour of Variable and Context doesn't depend + on section status *) + true + | Global | Local -> !axiom_into_instance + +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 ctx = match ctx with + | Monomorphic_const_entry ctx -> ctx + | Polymorphic_const_entry ctx -> Univ.ContextSet.of_context ctx + in + 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 && Proof_global.there_are_pending_proofs () then + Feedback.msg_info (str"Variable" ++ spc () ++ Id.print 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 do_instance = should_axiom_into_instance local in + let local = DeclareDef.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 decl = (ParameterEntry (None,(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 () = Declare.declare_univ_binders gr pl in + let () = assumption_message ident in + let () = if do_instance then Typeclasses.declare_instance None false gr in + let () = if is_coe then Class.try_add_new_coercion gr ~local p in + let inst = match ctx with + | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx + | Monomorphic_const_entry _ -> Univ.Instance.empty + in + (gr,inst,Lib.is_modtype_strict ()) + +let interp_assumption sigma env impls bl c = + let c = mkCProdN ?loc:(local_binders_loc bl) bl c in + let sigma, (ty, impls) = interp_type_evars_impls env sigma ~impls c in + let ty = EConstr.Unsafe.to_constr ty in + sigma, (ty, impls) + +(* When monomorphic the universe constraints are declared with the first declaration only. *) +let next_uctx = + let empty_uctx = Monomorphic_const_entry Univ.ContextSet.empty in + function + | Polymorphic_const_entry _ as uctx -> uctx + | Monomorphic_const_entry _ -> empty_uctx + +let declare_assumptions idl is_coe k (c,uctx) pl imps nl = + let refs, status, _ = + List.fold_left (fun (refs,status,uctx) id -> + let ref',u',status' = + declare_assumption is_coe k (c,uctx) pl imps false nl id in + (ref',u')::refs, status' && status, next_uctx uctx) + ([],true,uctx) idl + in + List.rev refs, status + + +let maybe_error_many_udecls = function + | ((loc,id), Some _) -> + user_err ?loc ~hdr:"many_universe_declarations" + Pp.(str "When declaring multiple axioms in one command, " ++ + str "only the first is allowed a universe binder " ++ + str "(which will be shared by the whole block).") + | (_, None) -> () + +let process_assumptions_udecls kind l = + let udecl, first_id = match l with + | (coe, ((id, udecl)::rest, c))::rest' -> + List.iter maybe_error_many_udecls rest; + List.iter (fun (coe, (idl, c)) -> List.iter maybe_error_many_udecls idl) rest'; + udecl, id + | (_, ([], _))::_ | [] -> assert false + in + let () = match kind, udecl with + | (Discharge, _, _), Some _ when Lib.sections_are_opened () -> + let loc = fst first_id in + let msg = Pp.str "Section variables cannot be polymorphic." in + user_err ?loc msg + | _ -> () + in + udecl, List.map (fun (coe, (idl, c)) -> coe, (List.map fst idl, c)) l + +let do_assumptions kind nl l = + let open Context.Named.Declaration in + let env = Global.env () in + let udecl, l = process_assumptions_udecls kind l in + let sigma, udecl = Univdecls.interp_univ_decl_opt env udecl in + let l = + if pi2 kind (* 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 (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) -> + let sigma,(t,imps) = interp_assumption sigma 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 + ((sigma,env,ienv),((is_coe,idl),t,imps))) + (sigma,env,empty_internalization_env) l + in + let sigma = solve_remaining_evars all_and_fail_flags env sigma Evd.empty in + (* The universe constraints come from the whole telescope. *) + let sigma = Evd.nf_constraints sigma in + let nf_evar c = EConstr.to_constr sigma (EConstr.of_constr c) in + let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) -> + let t = nf_evar t in + let uvars = Univ.LSet.union uvars (Univops.universes_of_constr env t) in + uvars, (coe,t,imps)) + Univ.LSet.empty l + in + let sigma = Evd.restrict_universe_context sigma uvars in + let uctx = Evd.check_univ_decl ~poly:(pi2 kind) sigma udecl in + let ubinders = Evd.universe_binders sigma in + pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) -> + let t = replace_vars subst t in + let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps 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, next_uctx uctx) + ([], true, uctx) l) diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli new file mode 100644 index 000000000..2fa156abd --- /dev/null +++ b/vernac/comAssumption.mli @@ -0,0 +1,34 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Constr +open Entries +open Globnames +open Vernacexpr +open Constrexpr +open Decl_kinds + +(** {6 Parameters/Assumptions} *) + +val do_assumptions : locality * polymorphic * assumption_object_kind -> + Vernacexpr.inline -> (Vernacexpr.ident_decl list * constr_expr) with_coercion list -> bool + +(************************************************************************) +(** Internal API *) +(************************************************************************) + +(** Exported for Classes *) + +(** returns [false] if the assumption is neither local to a section, + nor in a module type and meant to be instantiated. *) +val declare_assumption : coercion_flag -> assumption_kind -> + types in_constant_universes_entry -> + Universes.universe_binders -> Impargs.manual_implicits -> + bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located -> + global_reference * Univ.Instance.t * bool diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml new file mode 100644 index 000000000..883121479 --- /dev/null +++ b/vernac/comDefinition.ml @@ -0,0 +1,131 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2018 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Util +open Constr +open Environ +open Entries +open Termops +open Redexpr +open Declare +open Constrintern +open Pretyping + +open Context.Rel.Declaration + +(* Commands of the interface: Constant definitions *) + +let rec under_binders env sigma f n c = + if Int.equal n 0 then f env sigma (EConstr.of_constr c) else + match Constr.kind c with + | Lambda (x,t,c) -> + 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 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 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 poly red_option c ctypopt = + let env = Global.env() in + let evd, decl = Univdecls.interp_univ_decl_opt env pl in + let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars env evd 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 evd,imps,ce = + match ctypopt with + None -> + let evd, subst = Evd.nf_univ_variables evd in + let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in + let env_bl = push_rel_context ctx env in + let evd, (c, imps2) = interp_constr_evars_impls ~impls env_bl evd c in + let c = EConstr.Unsafe.to_constr c in + let evd,nf = Evarutil.nf_evars_and_universes evd in + let body = nf (it_mkLambda_or_LetIn c ctx) in + let vars = EConstr.universes_of_constr env evd (EConstr.of_constr body) in + let evd = Evd.restrict_universe_context evd vars in + let uctx = Evd.check_univ_decl ~poly evd decl in + evd, imps1@(Impargs.lift_implicits nb_args imps2), + definition_entry ~univs:uctx body + | Some ctyp -> + let evd, (ty, impsty) = interp_type_evars_impls ~impls env_bl evd ctyp in + let evd, subst = Evd.nf_univ_variables evd in + let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in + let env_bl = push_rel_context ctx env in + let evd, (c, imps2) = interp_casted_constr_evars_impls ~impls env_bl evd c ty in + let c = EConstr.Unsafe.to_constr c in + let evd, nf = Evarutil.nf_evars_and_universes evd 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 bodyvars = EConstr.universes_of_constr env evd (EConstr.of_constr body) in + let tyvars = EConstr.universes_of_constr env evd (EConstr.of_constr ty) in + let vars = Univ.LSet.union bodyvars tyvars in + let evd = Evd.restrict_universe_context evd vars in + let uctx = Evd.check_univ_decl ~poly evd decl in + evd, imps1@(Impargs.lift_implicits nb_args impsty), + definition_entry ~types:typ ~univs:uctx body + in + (red_constant_entry (Context.Rel.length ctx) ce evd red_option, evd, decl, imps) + +let check_definition (ce, evd, _, imps) = + check_evars_are_solved (Global.env ()) evd Evd.empty; + ce + +let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook = + let (ce, evd, univdecl, imps as def) = + interp_definition univdecl bl (pi2 k) red_option c ctypopt + in + if 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 ~univdecl ~implicits:imps ~kind:k ~hook obls) + else let ce = check_definition def in + ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps + (Lemmas.mk_hook + (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r))) diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli new file mode 100644 index 000000000..4a65c1e91 --- /dev/null +++ b/vernac/comDefinition.mli @@ -0,0 +1,30 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2018 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Entries +open Decl_kinds +open Redexpr +open Constrexpr + +(** {6 Definitions/Let} *) + +val do_definition : program_mode:bool -> + Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option -> + local_binder_expr list -> red_expr option -> constr_expr -> + constr_expr option -> unit Lemmas.declaration_hook -> unit + +(************************************************************************) +(** Internal API *) +(************************************************************************) + +(** Not used anywhere. *) +val interp_definition : + Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> + constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * + Univdecls.universe_decl * Impargs.manual_implicits diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml new file mode 100644 index 000000000..d648e293a --- /dev/null +++ b/vernac/comFixpoint.ml @@ -0,0 +1,356 @@ +open Pp +open CErrors +open Util +open Constr +open Vars +open Termops +open Declare +open Names +open Constrexpr +open Constrexpr_ops +open Constrintern +open Decl_kinds +open Pretyping +open Evarutil +open Evarconv +open Misctypes +open Vernacexpr + +module RelDecl = Context.Rel.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 (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 + 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 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 : universe_decl_expr 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 ~cofix env sigma fix = + let before, after = if not cofix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in + let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars env sigma before in + let sigma, (impl_env', ((env'', ctx'), imps')) = interp_context_evars ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after in + let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in + sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot) + +let interp_fix_ccl sigma impls (env,_) fix = + interp_type_evars_impls ~impls env sigma fix.fix_type + +let interp_fix_body env_rec sigma impls (_,ctx) fix ccl = + let open EConstr in + Option.cata (fun body -> + let env = push_rel_context ctx env_rec in + let sigma, body = interp_casted_constr_evars env sigma ~impls body ccl in + sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.fix_body + +let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx + +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 *) + +let contrib_name = "Program" +let subtac_dir = [contrib_name] +let tactics_module = subtac_dir @ ["Tactics"] + +let init_constant dir s sigma = + Evarutil.new_global sigma (Coqlib.coq_reference "Command" dir s) + +let fix_proto = init_constant tactics_module "fix_proto" + +let interp_recursive ~program_mode ~cofix 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 -> + let lsu = ls.univdecl_instance and usu = us.univdecl_instance in + if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) lsu usu) then + user_err Pp.(str "(co)-recursive definitions should all have the same universe binders"); + Some us) fixl None in + let sigma, decl = Univdecls.interp_univ_decl_opt env all_universes in + let sigma, (fixctxs, fiximppairs, fixannots) = + on_snd List.split3 @@ + List.fold_left_map (fun sigma -> interp_fix_context env sigma ~cofix) sigma fixl in + let fixctximpenvs, fixctximps = List.split fiximppairs in + let sigma, (fixccls,fixcclimps) = + on_snd List.split @@ + List.fold_left3_map interp_fix_ccl sigma fixctximpenvs fixctxs fixl in + let fixtypes = List.map2 build_fix_type fixctxs fixccls in + let fixtypes = List.map (fun c -> nf_evar sigma 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 sigma, rec_sign = + List.fold_left2 + (fun (sigma, env') id t -> + if program_mode then + let sigma, sort = Typing.type_of ~refresh:true env sigma t in + let sigma, fixprot = + try + let sigma, h_term = fix_proto sigma in + let app = mkApp (h_term, [|sort; t|]) in + let _evd = ref sigma in + let res = Typing.e_solve_evars env _evd app in + !_evd, res + with e when CErrors.noncritical e -> sigma, t + in + sigma, LocalAssum (id,fixprot) :: env' + else sigma, LocalAssum (id,t) :: env') + (sigma,[]) 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 impls = compute_internalization_env env Recursive fixnames fixtypes fiximps in + + (* Interp bodies with rollback because temp use of notations/implicit *) + let sigma, fixdefs = + Metasyntax.with_syntax_protection (fun () -> + List.iter (Metasyntax.set_notation_for_interpretation env_rec impls) notations; + List.fold_left4_map + (fun sigma fixctximpenv -> interp_fix_body env_rec sigma (Id.Map.fold Id.Map.add fixctximpenv impls)) + sigma fixctximpenvs fixctxs fixl fixccls) + () in + + (* Instantiate evars and check all are resolved *) + let sigma = solve_unif_constraints_with_heuristics env_rec sigma in + let sigma, nf = nf_evars_and_universes sigma 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,decl,sigma), (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 ~cofix l ntns = + let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l ntns in + check_recursive true 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,(EConstr.of_constr 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 pl (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 = Univops.universes_of_constr env (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 ctx = Evd.check_univ_decl ~poly evd pl in + let pl = Evd.universe_binders evd in + let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in + ignore (List.map4 (DeclareDef.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 (Global.env())) 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,(EConstr.of_constr 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 pl (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 env = Global.env () in + let vars = Univops.universes_of_constr env (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 ctx = Evd.check_univ_decl ~poly evd pl in + let pl = Evd.universe_binders evd in + ignore (List.map4 (DeclareDef.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 (Global.env())) 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 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 = + let fixl, ntns = extract_fixpoint_components true l in + let (_, _, _, info as fix) = interp_fixpoint ~cofix:false 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 + let cofix = interp_fixpoint ~cofix:true fixl ntns in + declare_cofixpoint local poly cofix ntns; + if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli new file mode 100644 index 000000000..2c84bd84d --- /dev/null +++ b/vernac/comFixpoint.mli @@ -0,0 +1,93 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2018 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Constr +open Decl_kinds +open Constrexpr +open Vernacexpr + +(** {6 Fixpoints and cofixpoints} *) + +(** Entry points for the vernacular commands Fixpoint and CoFixpoint *) + +val do_fixpoint : + (* When [false], assume guarded. *) + locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit + +val do_cofixpoint : + (* When [false], assume guarded. *) + locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit + +(************************************************************************) +(** Internal API *) +(************************************************************************) + +type structured_fixpoint_expr = { + fix_name : Id.t; + fix_univs : Vernacexpr.universe_decl_expr option; + fix_annot : Id.t Loc.located option; + fix_binders : local_binder_expr list; + fix_body : constr_expr option; + fix_type : constr_expr +} + +(** Typing global fixpoints and cofixpoint_expr *) + +(** Exported for Program *) +val interp_recursive : + (* Misc arguments *) + program_mode:bool -> cofix:bool -> + (* Notations of the fixpoint / should that be folded in the previous argument? *) + structured_fixpoint_expr list -> decl_notation list -> + + (* env / signature / univs / evar_map *) + (Environ.env * EConstr.named_context * Univdecls.universe_decl * Evd.evar_map) * + (* names / defs / types *) + (Id.t list * Constr.constr option list * Constr.types list) * + (* ctx per mutual def / implicits / struct annotations *) + (EConstr.rel_context * Impargs.manual_explicitation list * int option) list + +(** Exported for Funind *) + +(** Extracting the semantical components out of the raw syntax of + (co)fixpoints declarations *) + +val extract_fixpoint_components : bool -> + (fixpoint_expr * decl_notation list) list -> + structured_fixpoint_expr list * decl_notation list + +val extract_cofixpoint_components : + (cofixpoint_expr * decl_notation list) list -> + structured_fixpoint_expr list * decl_notation list + +type recursive_preentry = + Id.t list * constr option list * types list + +val interp_fixpoint : + cofix:bool -> + structured_fixpoint_expr list -> decl_notation list -> + recursive_preentry * Univdecls.universe_decl * UState.t * + (EConstr.rel_context * Impargs.manual_implicits * int option) list + +(** Registering fixpoints and cofixpoints in the environment *) +(** [Not used so far] *) +val declare_fixpoint : + locality -> polymorphic -> + recursive_preentry * Univdecls.universe_decl * UState.t * + (Context.Rel.t * Impargs.manual_implicits * int option) list -> + Proof_global.lemma_possible_guards -> decl_notation list -> unit + +val declare_cofixpoint : locality -> polymorphic -> + recursive_preentry * Univdecls.universe_decl * UState.t * + (Context.Rel.t * Impargs.manual_implicits * int option) list -> + decl_notation list -> unit + +(** Very private function, do not use *) +val compute_possible_guardness_evidences : + ('a, 'b) Context.Rel.pt * 'c * int option -> int list diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml new file mode 100644 index 000000000..f3f50f41d --- /dev/null +++ b/vernac/comInductive.ml @@ -0,0 +1,456 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open CErrors +open Sorts +open Util +open Constr +open Termops +open Environ +open Declare +open Names +open Libnames +open Globnames +open Nameops +open Constrexpr +open Constrexpr_ops +open Constrintern +open Nametab +open Impargs +open Reductionops +open Indtypes +open Decl_kinds +open Pretyping +open Evarutil +open Indschemes +open Misctypes +open Context.Rel.Declaration +open Entries + +module RelDecl = Context.Rel.Declaration + +(* 3b| Mutual inductive definitions *) + +let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function + | CProdN (bl,c) -> CProdN (bl,complete_conclusion a cs c) + | CLetIn (na,b,t,c) -> CLetIn (na,b,t,complete_conclusion a cs c) + | CHole (k, _, _) -> + let (has_no_args,name,params) = a in + if not has_no_args then + user_err ?loc + (strbrk"Cannot infer the non constant arguments of the conclusion of " + ++ Id.print cs ++ str "."); + let args = List.map (fun id -> CAst.make ?loc @@ CRef(Ident(loc,id),None)) params in + CAppExpl ((None,Ident(loc,name),None),List.rev args) + | c -> c + ) + +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 : Vernacexpr.universe_decl_expr 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] -> (Id.print x ++ str " is defined" ++ + if warn then str " as a non-primitive record" else mt()) + | l -> hov 0 (prlist_with_sep pr_comma Id.print 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 sigma env assums arity indname = + let is_ml_type = is_sort env sigma (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 DAst.get ind with + | GSort (GType []) -> true + | GProd ( _, _, _, e) + | GLetIn (_, _, _, e) + | GLambda (_, _, _, e) + | GApp (e, _) + | GCast (e, _) -> check_anonymous_type e + | _ -> false + +let make_conclusion_flexible sigma ty poly = + if poly && Term.isArity ty then + let _, concl = Term.destArity ty in + match concl with + | Type u -> + (match Univ.universe_level u with + | Some u -> + Evd.make_flexible_variable sigma ~algebraic:true u + | None -> sigma) + | _ -> sigma + else sigma + +let is_impredicative env u = + u = Prop Null || (is_impredicative_set env && u = Prop Pos) + +let interp_ind_arity env sigma ind = + let c = intern_gen IsType env ind.ind_arity in + let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in + let sigma,t = understand_tcc env sigma ~expected_type:IsType c in + let pseudo_poly = check_anonymous_type c in + let () = if not (Reductionops.is_arity env sigma t) then + user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity") + in + let t = EConstr.Unsafe.to_constr t in + sigma, (t, pseudo_poly, impls) + +let interp_cstrs env sigma 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 sigma, (ctyps'', cimpls) = + on_snd List.split @@ + List.fold_left_map (fun sigma l -> + on_snd (on_fst EConstr.Unsafe.to_constr) @@ + interp_type_evars_impls env sigma ~impls l) sigma ctyps' in + sigma, (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 evd 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 evd ctx in + Univ.sup ilev minlev) + else minlev + in + let clev = extract_level env evd 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)) + (evd,[]) (Array.to_list levels') destarities sizes + in 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 (loc,_) -> + Loc.raise ?loc (Stream.Error "pattern with quote not allowed here.") + +let interp_mutual_inductive (paramsl,indl) notations cum 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 sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in + let sigma, (impls, ((env_params, ctx_params), userimpls)) = + interp_context_evars env0 sigma 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 sigma, arities = List.fold_left_map (fun sigma -> interp_ind_arity env_params sigma) sigma 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 ntn_impls = compute_internalization_env env0 (Inductive (params,true)) indnames fullarities indimpls in + let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in + + let sigma, constructors = + Metasyntax.with_syntax_protection (fun () -> + (* Temporary declaration of notations and scopes *) + List.iter (Metasyntax.set_notation_for_interpretation env_params ntn_impls) notations; + (* Interpret the constructor types *) + List.fold_left3_map (fun sigma -> interp_cstrs env_ar_params sigma impls) sigma mldatas arities indl) + () in + + (* Try further to solve evars, and instantiate them *) + let sigma = solve_remaining_evars all_and_fail_flags env_params sigma Evd.empty in + (* Compute renewed arities *) + let sigma, nf = nf_evars_and_universes sigma 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 sigma = List.fold_left2 (fun sigma ty poly -> make_conclusion_flexible sigma ty poly) sigma arities aritypoly in + let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in + let sigma, nf' = nf_evars_and_universes sigma 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 uctx = Evd.check_univ_decl ~poly sigma decl in + List.iter (fun c -> check_evars env_params Evd.empty sigma (EConstr.of_constr c)) arities; + Context.Rel.iter (fun c -> check_evars env0 Evd.empty sigma (EConstr.of_constr c)) ctx_params; + List.iter (fun (_,ctyps,_) -> + List.iter (fun c -> check_evars env_ar_params Evd.empty sigma (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 + let univs = + match uctx with + | Polymorphic_const_entry uctx -> + if cum then + Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx) + else Polymorphic_ind_entry uctx + | Monomorphic_const_entry uctx -> + Monomorphic_ind_entry uctx + in + (* Build the mutual inductive entry *) + let mind_ent = + { mind_entry_params = List.map prepare_param ctx_params; + mind_entry_record = None; + mind_entry_finite = finite; + mind_entry_inds = entries; + mind_entry_private = if prv then Some false else None; + mind_entry_universes = univs; + } + in + (if poly && cum then + Inductiveops.infer_inductive_subtyping env_ar sigma mind_ent + else mind_ent), Evd.universe_binders sigma, 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 Constr.kind 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; + Declare.declare_univ_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 + Flags.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 cum 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 cum 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 (Global.env ())) 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 () diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli new file mode 100644 index 000000000..82ea131e1 --- /dev/null +++ b/vernac/comInductive.mli @@ -0,0 +1,65 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Entries +open Libnames +open Vernacexpr +open Constrexpr +open Decl_kinds + +(** {6 Inductive and coinductive types} *) + +(** Entry points for the vernacular commands Inductive and CoInductive *) + +val do_mutual_inductive : + (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> + polymorphic -> private_flag -> Declarations.recursivity_kind -> unit + +(************************************************************************) +(** Internal API *) +(************************************************************************) + +(** Exported for Record and Funind *) + +(** Registering a mutual inductive definition together with its + associated schemes *) + +type one_inductive_impls = + Impargs.manual_implicits (** for inds *)* + Impargs.manual_implicits list (** for constrs *) + +val declare_mutual_inductive_with_eliminations : + mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list -> + MutInd.t + +(** Exported for Funind *) + +(** Extracting the semantical components out of the raw syntax of mutual + inductive declarations *) + +type structured_one_inductive_expr = { + ind_name : Id.t; + ind_univs : Vernacexpr.universe_decl_expr 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 + +val extract_mutual_inductive_declaration_components : + (one_inductive_expr * decl_notation list) list -> + structured_inductive_expr * (*coercions:*) qualid list * decl_notation list + +(** Typing mutual inductive definitions *) + +val interp_mutual_inductive : + structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag -> + polymorphic -> private_flag -> Declarations.recursivity_kind -> + mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml new file mode 100644 index 000000000..a9a91e304 --- /dev/null +++ b/vernac/comProgramFixpoint.ml @@ -0,0 +1,342 @@ +open Pp +open CErrors +open Util +open Constr +open Entries +open Vars +open Declare +open Names +open Libnames +open Globnames +open Nameops +open Constrexpr +open Constrexpr_ops +open Constrintern +open Decl_kinds +open Evarutil +open Context.Rel.Declaration +open ComFixpoint + +module RelDecl = Context.Rel.Declaration + +(* 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 sigma = + Evarutil.new_global sigma (Coqlib.coq_reference "Command" dir s) + +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 sigma name typ prop = + let open EConstr in + let sigma, app_h = Evarutil.new_global sigma (delayed_force build_sigma).typ in + sigma, mkApp (app_h, [| 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 sigma l = + let open EConstr in + let open Vars in + match l with + | [] -> assert false + | [LocalAssum (n, t)] -> + sigma, t, [LocalDef (n, mkRel 1, t)], mkRel 1 + | LocalAssum (n, t) :: tl -> + let sigma, ty, tys, (k, constr) = + List.fold_left + (fun (sigma, ty, tys, (k, constr)) decl -> + let t = RelDecl.get_type decl in + let pred = mkLambda (RelDecl.get_name decl, t, ty) in + let sigma, ty = Evarutil.new_global sigma (Lazy.force sigT).typ in + let sigma, intro = Evarutil.new_global sigma (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 + (sigma, sigty, pred :: tys, (succ k, intro))) + (sigma, t, [], (2, mkRel 1)) tl + in + let sigma, last, subst = List.fold_right2 + (fun pred decl (sigma, prev, subst) -> + let t = RelDecl.get_type decl in + let sigma, p1 = Evarutil.new_global sigma (Lazy.force sigT).proj1 in + let sigma, p2 = Evarutil.new_global sigma (Lazy.force sigT).proj2 in + let proj1 = applist (p1, [t; pred; prev]) in + let proj2 = applist (p2, [t; pred; prev]) in + (sigma, lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst)) + (List.rev tys) tl (sigma, mkRel 1, []) + in sigma, ty, (LocalDef (n, last, t) :: subst), constr + + | LocalDef (n, b, t) :: tl -> + let sigma, ty, subst, term = telescope sigma tl in + sigma, 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 sigma, decl = Univdecls.interp_univ_decl_opt env pl in + let sigma, (_, ((env', binders_rel), impls)) = interp_context_evars env sigma bl in + let len = List.length binders_rel in + let top_env = push_rel_context binders_rel env in + let sigma, top_arity = interp_type_evars top_env sigma arityc in + let full_arity = it_mkProd_or_LetIn top_arity binders_rel in + let sigma, argtyp, letbinders, make = telescope sigma 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 sigma, (rel, _) = interp_constr_evars_impls env sigma r in + let relty = Typing.unsafe_type_of env sigma rel in + let relargty = + let error () = + user_err ?loc:(constr_loc r) + ~hdr:"Command.build_wellfounded" + (Printer.pr_econstr_env env sigma rel ++ str " is not an homogeneous binary relation.") + in + try + let ctx, ar = Reductionops.splay_prod_n env sigma 2 relty in + match ctx, EConstr.kind sigma ar with + | [LocalAssum (_,t); LocalAssum (_,u)], Sort s + when Sorts.is_prop (ESorts.kind sigma s) && Reductionops.is_conv env sigma t u -> t + | _, _ -> error () + with e when CErrors.noncritical e -> error () + in + let sigma, measure = interp_casted_constr_evars binders_env sigma measure relargty in + let sigma, 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 sigma, comb = Evarutil.new_global sigma (delayed_force measure_on_R_ref) 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 sigma, wf_rel, wf_rel_fun, measure + in + let sigma, wf_term = well_founded sigma in + let wf_proof = mkApp (wf_term, [| argtyp ; wf_rel |]) in + let argid' = Id.of_string (Id.to_string argname ^ "'") in + let wfarg sigma len = + let sigma, ss_term = mkSubset sigma (Name argid') argtyp (wf_rel_fun (mkRel 1) (mkRel (len + 1))) in + sigma, LocalAssum (Name argid', ss_term) + in + let sigma, intern_bl = + let sigma, wfa = wfarg sigma 1 in + sigma, wfa :: [arg] + in + let _intern_env = push_rel_context intern_bl env in + let sigma, proj = Evarutil.new_global sigma (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 sigma, wfa = wfarg sigma 1 in + let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfa] in + let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in + let sigma, curry_fun = + let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in + let sigma, intro = Evarutil.new_global sigma (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 + sigma, LocalDef (Name recname, body, ty) + in + let fun_bl = intern_fun_binder :: [arg] in + let lift_lets = lift_rel_context 1 letbinders in + let sigma, 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) sigma + ~impls:newimpls body (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 + (* XXX: Previous code did parallel evdref update, so possible old + weak ordering semantics may bite here. *) + let sigma, def = + let sigma, h_a_term = Evarutil.new_global sigma (delayed_force fix_sub_ref) in + let sigma, h_e_term = Evarutil.new_evar env sigma + ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof in + sigma, mkApp (h_a_term, [| argtyp ; wf_rel ; h_e_term; prop |]) + in + let _evd = ref sigma in + let def = Typing.e_solve_evars env _evd def in + let sigma = !_evd in + let sigma = Evarutil.nf_evar_map sigma in + let def = mkApp (def, [|intern_body_lam|]) in + let binders_rel = nf_evar_context sigma binders_rel in + let binders = nf_evar_context sigma binders in + let top_arity = Evarutil.nf_evar sigma top_arity in + let hook, recname, typ = + if List.length binders_rel > 1 then + let name = add_suffix recname "_func" in + (* XXX: Mutating the evar_map in the hook! *) + (* XXX: Likely the sigma is out of date when the hook is called .... *) + let hook sigma l gr _ = + let sigma, h_body = Evarutil.new_global sigma gr in + let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in + let ty = it_mkProd_or_LetIn top_arity binders_rel in + let ty = EConstr.Unsafe.to_constr ty in + let univs = Evd.check_univ_decl ~poly sigma decl in + (*FIXME poly? *) + let ce = definition_entry ~types:ty ~univs (EConstr.to_constr sigma body) in + (** FIXME: include locality *) + let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in + let gr = ConstRef c in + let () = Universes.register_universe_binders gr (Evd.universe_binders sigma) 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 sigma 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 + (* XXX: Capturing sigma here... bad bad *) + let hook = Lemmas.mk_hook (hook sigma) in + let fullcoqc = EConstr.to_constr sigma def in + let fullctyp = EConstr.to_constr sigma typ in + Obligations.check_evars env sigma; + let evars, _, evars_def, evars_typ = + Obligations.eterm_obligations env recname sigma 0 fullcoqc fullctyp + in + let ctx = Evd.evar_universe_context sigma in + ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl + evars_typ ctx evars ~hook) + +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 poly fixkind fixl ntns = + let cofix = fixkind = Obligations.IsCoFixpoint in + let (env, rec_sign, pl, evd), fix, info = + interp_recursive ~cofix ~program_mode:true 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 not cofix then begin + let possible_indexes = List.map ComFixpoint.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, poly, Fixpoint) + | Obligations.IsCoFixpoint -> (local, poly, CoFixpoint) + in + Obligations.add_mutual_definitions defs ~kind ~univdecl: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 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 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 = + do_program_fixpoint local poly l; + if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () + +let do_cofixpoint local poly l = + let fixl,ntns = extract_cofixpoint_components l in + do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns; + if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli new file mode 100644 index 000000000..943cb8efe --- /dev/null +++ b/vernac/comProgramFixpoint.mli @@ -0,0 +1,12 @@ +open Decl_kinds +open Vernacexpr + +(** Special Fixpoint handling when command is activated. *) + +val do_fixpoint : + (* When [false], assume guarded. *) + locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit + +val do_cofixpoint : + (* When [false], assume guarded. *) + locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit diff --git a/vernac/command.ml b/vernac/command.ml deleted file mode 100644 index 01c7f149b..000000000 --- a/vernac/command.ml +++ /dev/null @@ -1,1365 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Pp -open CErrors -open Sorts -open Util -open Constr -open Vars -open Termops -open Environ -open Redexpr -open Declare -open Names -open Libnames -open Globnames -open Nameops -open Constrexpr -open Constrexpr_ops -open Constrintern -open Nametab -open Impargs -open Reductionops -open Indtypes -open Decl_kinds -open Pretyping -open Evarutil -open Evarconv -open Indschemes -open Misctypes -open Vernacexpr -open Context.Rel.Declaration -open Entries - -module RelDecl = Context.Rel.Declaration - -let do_universe poly l = Declare.do_universe poly l -let do_constraint poly l = Declare.do_constraint poly l - -let rec under_binders env sigma f n c = - if Int.equal n 0 then f env sigma (EConstr.of_constr c) else - match Constr.kind c with - | Lambda (x,t,c) -> - 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 " - ++ Id.print 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 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 poly red_option c ctypopt = - let env = Global.env() in - let evd, decl = Univdecls.interp_univ_decl_opt env pl in - let evdref = ref evd 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 = Univops.universes_of_constr body in - let evd = Evd.restrict_universe_context !evdref vars in - let uctx = Evd.check_univ_decl ~poly evd decl in - let binders = Evd.universe_binders evd in - imps1@(Impargs.lift_implicits nb_args imps2), binders, - definition_entry ~univs:uctx 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 (Univops.universes_of_constr body) - (Univops.universes_of_constr typ) in - let ctx = Evd.restrict_universe_context !evdref vars in - let uctx = Evd.check_univ_decl ~poly ctx decl in - let binders = Evd.universe_binders evd in - imps1@(Impargs.lift_implicits nb_args impsty), binders, - definition_entry ~types:typ - ~univs:uctx body - in - red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, pl, imps - -let check_definition (ce, evd, _, _, imps) = - check_evars_are_solved (Global.env ()) evd Evd.empty; - ce - -let do_definition ident k univdecl bl red_option c ctypopt hook = - let (ce, evd, univdecl, pl', imps as def) = - interp_definition univdecl 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 ~univdecl ~implicits:imps ~kind:k ~hook obls) - else let ce = check_definition def in - ignore(DeclareDef.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 axiom_into_instance = ref false - -let _ = - let open Goptions in - declare_bool_option - { optdepr = false; - optname = "automatically declare axioms whose type is a typeclass as instances"; - optkey = ["Typeclasses";"Axioms";"Are";"Instances"]; - optread = (fun _ -> !axiom_into_instance); - optwrite = (:=) axiom_into_instance; } - -let should_axiom_into_instance = function - | Discharge -> - (* The typeclass behaviour of Variable and Context doesn't depend - on section status *) - true - | Global | Local -> !axiom_into_instance - -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 ctx = match ctx with - | Monomorphic_const_entry ctx -> ctx - | Polymorphic_const_entry ctx -> Univ.ContextSet.of_context ctx - in - 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 && Proof_global.there_are_pending_proofs () then - Feedback.msg_info (str"Variable" ++ spc () ++ Id.print 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 do_instance = should_axiom_into_instance local in - let local = DeclareDef.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 decl = (ParameterEntry (None,(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 () = if do_instance then Typeclasses.declare_instance None false gr in - let () = if is_coe then Class.try_add_new_coercion gr ~local p in - let inst = match ctx with - | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx - | Monomorphic_const_entry _ -> 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) - -(* When monomorphic the universe constraints are declared with the first declaration only. *) -let next_uctx = - let empty_uctx = Monomorphic_const_entry Univ.ContextSet.empty in - function - | Polymorphic_const_entry _ as uctx -> uctx - | Monomorphic_const_entry _ -> empty_uctx - -let declare_assumptions idl is_coe k (c,uctx) pl imps nl = - let refs, status, _ = - List.fold_left (fun (refs,status,uctx) id -> - let ref',u',status' = - declare_assumption is_coe k (c,uctx) pl imps false nl id in - (ref',u')::refs, status' && status, next_uctx uctx) - ([],true,uctx) idl - in - List.rev refs, status - - -let maybe_error_many_udecls = function - | ((loc,id), Some _) -> - user_err ?loc ~hdr:"many_universe_declarations" - Pp.(str "When declaring multiple axioms in one command, " ++ - str "only the first is allowed a universe binder " ++ - str "(which will be shared by the whole block).") - | (_, None) -> () - -let process_assumptions_udecls kind l = - let udecl, first_id = match l with - | (coe, ((id, udecl)::rest, c))::rest' -> - List.iter maybe_error_many_udecls rest; - List.iter (fun (coe, (idl, c)) -> List.iter maybe_error_many_udecls idl) rest'; - udecl, id - | (_, ([], _))::_ | [] -> assert false - in - let () = match kind, udecl with - | (Discharge, _, _), Some _ when Lib.sections_are_opened () -> - let loc = fst first_id in - let msg = Pp.str "Section variables cannot be polymorphic." in - user_err ?loc msg - | _ -> () - in - udecl, List.map (fun (coe, (idl, c)) -> coe, (List.map fst idl, c)) l - -let do_assumptions kind nl l = - let open Context.Named.Declaration in - let env = Global.env () in - let udecl, l = process_assumptions_udecls kind l in - let evdref, udecl = - let evd, udecl = Univdecls.interp_univ_decl_opt env udecl in - ref evd, udecl - in - let l = - if pi2 kind (* 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_left_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 nf_evar c = EConstr.to_constr evd (EConstr.of_constr c) in - let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) -> - let t = nf_evar t in - let uvars = Univ.LSet.union uvars (Univops.universes_of_constr t) in - uvars, (coe,t,imps)) - Univ.LSet.empty l - in - let evd = Evd.restrict_universe_context evd uvars in - let uctx = Evd.check_univ_decl ~poly:(pi2 kind) evd udecl in - let ubinders = Evd.universe_binders evd in - pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) -> - let t = replace_vars subst t in - let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps 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, next_uctx uctx) - ([], true, uctx) 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 : Vernacexpr.universe_decl_expr 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] -> (Id.print x ++ str " is defined" ++ - if warn then str " as a non-primitive record" else mt()) - | l -> hov 0 (prlist_with_sep pr_comma Id.print 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 DAst.get ind 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 && Term.isArity ty then - let _, concl = Term.destArity ty in - match concl with - | Type u -> - (match Univ.universe_level u with - | Some u -> - evdref := Evd.make_flexible_variable !evdref ~algebraic: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 impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in - let (evd,t) = understand_tcc env !evdref ~expected_type:IsType c in - evdref := evd; - 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 (loc,_) -> - Loc.raise ?loc (Stream.Error "pattern with quote not allowed here.") - -let interp_mutual_inductive (paramsl,indl) notations cum 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 evd, decl = Univdecls.interp_univ_decl_opt env0 pl in - let evdref = ref evd 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 ntn_impls = compute_internalization_env env0 (Inductive (params,true)) 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 env_params ntn_impls) 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 uctx = Evd.check_univ_decl ~poly evd decl 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 - let univs = - match uctx with - | Polymorphic_const_entry uctx -> - if cum then - Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx) - else Polymorphic_ind_entry uctx - | Monomorphic_const_entry uctx -> - Monomorphic_ind_entry uctx - in - (* Build the mutual inductive entry *) - let mind_ent = - { mind_entry_params = List.map prepare_param ctx_params; - mind_entry_record = None; - mind_entry_finite = finite; - mind_entry_inds = entries; - mind_entry_private = if prv then Some false else None; - mind_entry_universes = univs; - } - in - (if poly && cum then - Inductiveops.infer_inductive_subtyping env_ar evd mind_ent - else mind_ent), Evd.universe_binders evd, 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 Constr.kind 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 - Flags.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 cum 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 cum 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 (Global.env ())) 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 - 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 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 : universe_decl_expr 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 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 evd, decl = Univdecls.interp_univ_decl_opt env pl in - let evdref = ref evd 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 univs = Evd.check_univ_decl ~poly !evdref decl in - (*FIXME poly? *) - let ce = definition_entry ~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 - let () = Universes.register_universe_binders gr (Evd.universe_binders !evdref) 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 ~univdecl:decl - 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 -> - let lsu = ls.univdecl_instance and usu = us.univdecl_instance in - if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) lsu usu) then - user_err Pp.(str "(co)-recursive definitions should all have the same universe binders"); - Some us) fixl None in - let evd, decl = Univdecls.interp_univ_decl_opt env all_universes in - let evdref = ref evd 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 env_rec 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,decl,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,(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 pl (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 = Univops.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 ctx = Evd.check_univ_decl ~poly evd pl in - let pl = Evd.universe_binders evd in - let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in - ignore (List.map4 (DeclareDef.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 (Global.env())) 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,(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 pl (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 = Univops.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 ctx = Evd.check_univ_decl ~poly evd pl in - let pl = Evd.universe_binders evd in - ignore (List.map4 (DeclareDef.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 (Global.env())) 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 ~univdecl: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 () diff --git a/vernac/command.mli b/vernac/command.mli deleted file mode 100644 index 070f3e112..000000000 --- a/vernac/command.mli +++ /dev/null @@ -1,163 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Names -open Constr -open Entries -open Libnames -open Globnames -open Vernacexpr -open Constrexpr -open Decl_kinds -open Redexpr - -(** This file is about the interpretation of raw commands into typed - ones and top-level declaration of the main Gallina objects *) - -val do_universe : polymorphic -> Id.t Loc.located list -> unit -val do_constraint : polymorphic -> - (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> unit - -(** {6 Definitions/Let} *) - -val interp_definition : - Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> - constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * - Univdecls.universe_decl * Universes.universe_binders * Impargs.manual_implicits - -val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option -> - local_binder_expr list -> red_expr option -> constr_expr -> - constr_expr option -> unit Lemmas.declaration_hook -> unit - -(** {6 Parameters/Assumptions} *) - -(* val interp_assumption : env -> evar_map ref -> *) -(* local_binder_expr list -> constr_expr -> *) -(* types Univ.in_universe_context_set * Impargs.manual_implicits *) - -(** returns [false] if the assumption is neither local to a section, - nor in a module type and meant to be instantiated. *) -val declare_assumption : coercion_flag -> assumption_kind -> - types in_constant_universes_entry -> - Universes.universe_binders -> Impargs.manual_implicits -> - bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located -> - global_reference * Univ.Instance.t * bool - -val do_assumptions : locality * polymorphic * assumption_object_kind -> - Vernacexpr.inline -> (Vernacexpr.ident_decl list * constr_expr) with_coercion list -> bool - -(* val declare_assumptions : variable Loc.located list -> *) -(* coercion_flag -> assumption_kind -> types Univ.in_universe_context_set -> *) -(* Impargs.manual_implicits -> bool -> Vernacexpr.inline -> bool *) - -(** {6 Inductive and coinductive types} *) - -(** Extracting the semantical components out of the raw syntax of mutual - inductive declarations *) - -type structured_one_inductive_expr = { - ind_name : Id.t; - ind_univs : Vernacexpr.universe_decl_expr 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 - -val extract_mutual_inductive_declaration_components : - (one_inductive_expr * decl_notation list) list -> - structured_inductive_expr * (*coercions:*) qualid list * decl_notation list - -(** Typing mutual inductive definitions *) - -type one_inductive_impls = - Impargs.manual_implicits (** for inds *)* - Impargs.manual_implicits list (** for constrs *) - -val interp_mutual_inductive : - structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag -> - polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> - mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list - -(** Registering a mutual inductive definition together with its - associated schemes *) - -val declare_mutual_inductive_with_eliminations : - mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list -> - MutInd.t - -(** Entry points for the vernacular commands Inductive and CoInductive *) - -val do_mutual_inductive : - (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> - polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> unit - -(** {6 Fixpoints and cofixpoints} *) - -type structured_fixpoint_expr = { - fix_name : Id.t; - fix_univs : Vernacexpr.universe_decl_expr option; - fix_annot : Id.t Loc.located option; - fix_binders : local_binder_expr list; - fix_body : constr_expr option; - fix_type : constr_expr -} - -(** Extracting the semantical components out of the raw syntax of - (co)fixpoints declarations *) - -val extract_fixpoint_components : bool -> - (fixpoint_expr * decl_notation list) list -> - structured_fixpoint_expr list * decl_notation list - -val extract_cofixpoint_components : - (cofixpoint_expr * decl_notation list) list -> - structured_fixpoint_expr list * decl_notation list - -(** Typing global fixpoints and cofixpoint_expr *) - -type recursive_preentry = - Id.t list * constr option list * types list - -val interp_fixpoint : - structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * Univdecls.universe_decl * UState.t * - (EConstr.rel_context * Impargs.manual_implicits * int option) list - -val interp_cofixpoint : - structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * Univdecls.universe_decl * UState.t * - (EConstr.rel_context * Impargs.manual_implicits * int option) list - -(** Registering fixpoints and cofixpoints in the environment *) - -val declare_fixpoint : - locality -> polymorphic -> - recursive_preentry * Univdecls.universe_decl * UState.t * - (Context.Rel.t * Impargs.manual_implicits * int option) list -> - Proof_global.lemma_possible_guards -> decl_notation list -> unit - -val declare_cofixpoint : locality -> polymorphic -> - recursive_preentry * Univdecls.universe_decl * UState.t * - (Context.Rel.t * Impargs.manual_implicits * int option) list -> - decl_notation list -> unit - -(** Entry points for the vernacular commands Fixpoint and CoFixpoint *) - -val do_fixpoint : - (* When [false], assume guarded. *) - locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit - -val do_cofixpoint : - (* When [false], assume guarded. *) - locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit - -(** Utils *) - -val check_mutuality : Environ.env -> Evd.evar_map -> bool -> (Id.t * types) list -> unit diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 980db4109..dfac78c04 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -36,7 +36,7 @@ let declare_global_definition ident ce local k pl imps = 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 () = Declare.declare_univ_binders gr pl in let () = definition_message ident in gr @@ -49,6 +49,7 @@ let declare_definition ident (local, p, k) ce pl imps hook = let () = definition_message ident in let gr = VarRef ident in let () = maybe_declare_manual_implicits false gr imps in + let () = Declare.declare_univ_binders gr pl in let () = if Proof_global.there_are_pending_proofs () then warn_definition_not_visible ident in diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 3a8e8fb43..d328ad0cf 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -75,8 +75,7 @@ let process_vernac_interp_error exn = match fst exn with wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e) | Tacred.ReductionTacticError e -> wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e) - | Logic.RefinerError e -> - let sigma, env = Pfedit.get_current_context () in + | Logic.RefinerError (env, sigma, e) -> wrap_vernac_error exn (Himsg.explain_refiner_error env sigma e) | Nametab.GlobalizationError q -> wrap_vernac_error exn diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 42631a15b..27a680b9b 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -13,12 +13,10 @@ open CErrors open Util open Pp open Names -open Term open Constr open Declarations open Declareops open Entries -open Environ open Nameops open Globnames open Decls @@ -88,28 +86,28 @@ let adjust_guardness_conditions const = function (mkFix ((indexes,0),fixdecls), ctx), eff | _ -> (body, ctx), eff) } -let find_mutually_recursive_statements thms = +let find_mutually_recursive_statements sigma thms = let n = List.length thms in let inds = List.map (fun (id,(t,impls)) -> - let (hyps,ccl) = decompose_prod_assum t in + let (hyps,ccl) = EConstr.decompose_prod_assum sigma t in let x = (id,(t,impls)) in - let whnf_hyp_hds = map_rel_context_in_env - (fun env c -> EConstr.Unsafe.to_constr (fst (whd_all_stack env Evd.empty (EConstr.of_constr c)))) + let whnf_hyp_hds = EConstr.map_rel_context_in_env + (fun env c -> fst (Reductionops.whd_all_stack env sigma c)) (Global.env()) hyps in let ind_hyps = List.flatten (List.map_i (fun i decl -> let t = RelDecl.get_type decl in - match Constr.kind t with + match EConstr.kind sigma t with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in mind.mind_finite <> Decl_kinds.CoFinite -> [ind,x,i] | _ -> - []) 0 (List.rev (List.filter RelDecl.is_local_assum whnf_hyp_hds))) in + []) 0 (List.rev (List.filter Context.Rel.Declaration.is_local_assum whnf_hyp_hds))) in let ind_ccl = - let cclenv = push_rel_context hyps (Global.env()) in - let whnf_ccl,_ = whd_all_stack cclenv Evd.empty (EConstr.of_constr ccl) in - match Constr.kind (EConstr.Unsafe.to_constr whnf_ccl) with + let cclenv = EConstr.push_rel_context hyps (Global.env()) in + let whnf_ccl,_ = whd_all_stack cclenv Evd.empty ccl in + match EConstr.kind sigma whnf_ccl with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite -> @@ -163,21 +161,21 @@ let find_mutually_recursive_statements thms = in (finite,guard,None), ordered_inds -let look_for_possibly_mutual_statements = function +let look_for_possibly_mutual_statements sigma = function | [id,(t,impls)] -> (* One non recursively proved theorem *) None,[id,(t,impls)],None | _::_ as thms -> (* More than one statement and/or an explicit decreasing mark: *) (* we look for a common inductive hyp or a common coinductive conclusion *) - let recguard,ordered_inds = find_mutually_recursive_statements thms in + let recguard,ordered_inds = find_mutually_recursive_statements sigma thms in let thms = List.map pi2 ordered_inds in Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds) | [] -> anomaly (Pp.str "Empty list of theorems.") (* Saving a goal *) -let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook = +let save ?export_seff id const uctx do_guard (locality,poly,kind) hook = let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in try let const = adjust_guardness_conditions const do_guard in @@ -204,7 +202,7 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook = (locality, ConstRef kn) in definition_message id; - Universes.register_universe_binders r (Option.default Universes.empty_binders pl); + Declare.declare_univ_binders r (UState.universe_binders uctx); call_hook (fun exn -> exn) hook l r with e when CErrors.noncritical e -> let e = CErrors.push e in @@ -286,17 +284,17 @@ let save_hook = ref ignore let set_save_hook f = save_hook := f let save_named ?export_seff proof = - let id,const,(cstrs,pl),do_guard,persistence,hook = proof in - save ?export_seff id const cstrs pl do_guard persistence hook + let id,const,uctx,do_guard,persistence,hook = proof in + save ?export_seff id const uctx do_guard persistence hook let check_anonymity id save_ident = if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then user_err Pp.(str "This command can only be used for unnamed theorem.") let save_anonymous ?export_seff proof save_ident = - let id,const,(cstrs,pl),do_guard,persistence,hook = proof in + let id,const,uctx,do_guard,persistence,hook = proof in check_anonymity id save_ident; - save ?export_seff save_ident const cstrs pl do_guard persistence hook + save ?export_seff save_ident const uctx do_guard persistence hook (* Admitted *) @@ -312,7 +310,7 @@ let admit (id,k,e) pl hook () = | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id in let () = assumption_message id in - Universes.register_universe_binders (ConstRef kn) (Option.default Universes.empty_binders pl); + Declare.declare_univ_binders (ConstRef kn) pl; call_hook (fun exn -> exn) hook Global (ConstRef kn) (* Starting a goal *) @@ -330,8 +328,8 @@ let get_proof proof do_guard hook opacity = let universe_proof_terminator compute_guard hook = let open Proof_global in make_terminator begin function - | Admitted (id,k,pe,(ctx,pl)) -> - admit (id,k,pe) pl (hook (Some ctx)) (); + | Admitted (id,k,pe,ctx) -> + admit (id,k,pe) (UState.universe_binders ctx) (hook (Some ctx)) (); Feedback.feedback Feedback.AddedAxiom | Proved (opaque,idopt,proof) -> let is_opaque, export_seff = match opaque with @@ -339,7 +337,7 @@ let universe_proof_terminator compute_guard hook = | Vernacexpr.Opaque -> true, false in let proof = get_proof proof compute_guard - (hook (Some (fst proof.Proof_global.universes))) is_opaque in + (hook (Some (proof.Proof_global.universes))) is_opaque in begin match idopt with | None -> save_named ~export_seff proof | Some (_,id) -> save_anonymous ~export_seff proof id @@ -377,7 +375,7 @@ let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_ let rec_tac_initializer finite guard thms snl = if finite then - match List.map (fun (id,(t,_)) -> (id,EConstr.of_constr t)) thms with + match List.map (fun (id,(t,_)) -> (id,t)) thms with | (id,_)::l -> Tactics.mutual_cofix id l 0 | _ -> assert false else @@ -385,11 +383,11 @@ let rec_tac_initializer finite guard thms snl = let nl = match snl with | None -> List.map succ (List.map List.last guard) | Some nl -> nl - in match List.map2 (fun (id,(t,_)) n -> (id,n, EConstr.of_constr t)) thms nl with + in match List.map2 (fun (id,(t,_)) n -> (id,n, t)) thms nl with | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false -let start_proof_with_initialization kind ctx decl recguard thms snl hook = +let start_proof_with_initialization kind sigma decl recguard thms snl hook = let intro_tac (_, (_, (ids, _))) = Tacticals.New.tclMAP (function | Name id -> Tactics.intro_mustbe_force id @@ -417,23 +415,22 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook = | (id,(t,(_,imps)))::other_thms -> let hook ctx strength ref = let ctx = match ctx with - | None -> Evd.empty_evar_universe_context + | None -> UState.empty | Some ctx -> ctx in let other_thms_data = if List.is_empty other_thms then [] else (* there are several theorems defined mutually *) let body,opaq = retrieve_first_recthm ctx ref in - let subst = Evd.evar_universe_context_subst ctx in - let norm c = Universes.subst_opt_univs_constr subst c in - let ctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in - let body = Option.map norm body in - List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in + let norm c = EConstr.to_constr (Evd.from_ctx ctx) c in + let body = Option.map EConstr.of_constr body in + let uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in + List.map_i (save_remaining_recthms kind norm uctx body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in List.iter (fun (strength,ref,imps) -> maybe_declare_manual_implicits false ref imps; call_hook (fun exn -> exn) hook strength ref) thms_data in - start_proof_univs id ~pl:decl kind ctx (EConstr.of_constr t) ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard + start_proof_univs id ~pl:decl kind sigma t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard let start_proof_com ?inference_hook kind thms hook = let env0 = Global.env () in @@ -442,22 +439,24 @@ let start_proof_com ?inference_hook kind thms hook = match decl with | None -> Evd.from_env env0, Univdecls.default_univ_decl | Some decl -> - Univdecls.interp_univ_decl_opt env0 (snd decl) in - let evdref = ref evd in - let thms = List.map (fun (sopt,(bl,t)) -> - let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in - let t', imps' = interp_type_evars_impls ~impls env evdref t in + Univdecls.interp_univ_decl_opt env0 (snd decl) in + let evd, thms = List.fold_left_map (fun evd (sopt,(bl,t)) -> + let evd, (impls, ((env, ctx), imps)) = interp_context_evars env0 evd bl in + let evd, (t', imps') = interp_type_evars_impls ~impls env evd t in let flags = all_and_fail_flags in let flags = { flags with use_hook = inference_hook } in - evdref := solve_remaining_evars flags env !evdref Evd.empty; + let evd = solve_remaining_evars flags env evd Evd.empty in let ids = List.map RelDecl.get_name ctx in - (compute_proof_name (pi1 kind) sopt, - (EConstr.Unsafe.to_constr (nf_evar !evdref (EConstr.it_mkProd_or_LetIn t' ctx)), - (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps')))) - thms in - let recguard,thms,snl = look_for_possibly_mutual_statements thms in - let evd, nf = Evarutil.nf_evars_and_universes !evdref in - let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in + (* XXX: The nf_evar is critical !! *) + evd, (compute_proof_name (pi1 kind) sopt, + (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx), + (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps')))) + evd thms in + let recguard,thms,snl = look_for_possibly_mutual_statements evd thms in + let evd, _nf = Evarutil.nf_evars_and_universes evd in + (* XXX: This nf_evar is critical too!! We are normalizing twice if + you look at the previous lines... *) + let thms = List.map (fun (n, (t, info)) -> (n, (nf_evar evd t, info))) thms in let () = let open Misctypes in if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then @@ -470,7 +469,6 @@ let start_proof_com ?inference_hook kind thms hook = in start_proof_with_initialization kind evd decl recguard thms snl hook - (* Saving a proof *) let keep_admitted_vars = ref true @@ -496,7 +494,7 @@ let save_proof ?proof = function if const_entry_type = None then user_err Pp.(str "Admitted requires an explicit statement"); let typ = Option.get const_entry_type in - let ctx = UState.const_univ_entry ~poly:(pi2 k) (fst universes) in + let ctx = UState.const_univ_entry ~poly:(pi2 k) universes in let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in Admitted(id, k, (sec_vars, (typ, ctx), None), universes) | None -> @@ -518,12 +516,9 @@ let save_proof ?proof = function Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def)) | _ -> None in let decl = Proof_global.get_universe_decl () in - let evd = Evd.from_ctx universes in let poly = pi2 k in - let ctx = Evd.check_univ_decl ~poly evd decl in - let binders = if poly then Some (UState.universe_binders universes) else None in - Admitted(id,k,(sec_vars, (typ, ctx), None), - (universes, binders)) + let ctx = UState.check_univ_decl ~poly universes decl in + Admitted(id,k,(sec_vars, (typ, ctx), None), universes) in Proof_global.apply_terminator (Proof_global.get_terminator ()) pe | Vernacexpr.Proved (is_opaque,idopt) -> diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index a4854b4a6..ca92e856b 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Constr open Decl_kinds type 'a declaration_hook @@ -37,11 +36,11 @@ val start_proof_com : goal_kind -> Vernacexpr.proof_expr list -> unit declaration_hook -> unit -val start_proof_with_initialization : +val start_proof_with_initialization : goal_kind -> Evd.evar_map -> Univdecls.universe_decl -> (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option -> (Id.t (* name of thm *) * - (types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list + (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list -> int list option -> unit declaration_hook -> unit val universe_proof_terminator : diff --git a/vernac/mltop.ml b/vernac/mltop.ml index d3de10235..00554e3ba 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -378,7 +378,7 @@ let unfreeze_ml_modules x = (fun (name,path) -> trigger_ml_object false false false ?path name) x let _ = - Summary.declare_summary Summary.ml_modules + Summary.declare_ml_modules_summary { Summary.freeze_function = (fun _ -> get_loaded_modules ()); Summary.unfreeze_function = unfreeze_ml_modules; Summary.init_function = reset_loaded_modules } diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 1046d68f8..58e4b00fc 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -429,8 +429,8 @@ let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] -let from_prg : program_info ProgMap.t ref = - Summary.ref ProgMap.empty ~name:"program-tcc-table" +let from_prg, program_tcc_summary_tag = + Summary.ref_tag ProgMap.empty ~name:"program-tcc-table" let close sec = if not (ProgMap.is_empty !from_prg) then @@ -477,7 +477,10 @@ let declare_definition prg = let fix_exn = Hook.get get_fix_exn () in let typ = nf typ in let body = nf body in - let uvars = Univ.LSet.union (Univops.universes_of_constr typ) (Univops.universes_of_constr body) in + let env = Global.env () in + let uvars = Univ.LSet.union + (Univops.universes_of_constr env typ) + (Univops.universes_of_constr env body) in let uctx = UState.restrict prg.prg_ctx uvars in let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in @@ -833,7 +836,7 @@ let obligation_terminator name num guard hook auto pf = let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in let ty = entry.Entries.const_entry_type in let (body, cstr), () = Future.force entry.Entries.const_entry_body in - let sigma = Evd.from_ctx (fst uctx) in + let sigma = Evd.from_ctx uctx in let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in Inductiveops.control_only_guard (Global.env ()) body; (** Declare the obligation ourselves and drop the hook *) @@ -1182,7 +1185,6 @@ let init_program () = Coqlib.check_required_library ["Coq";"Init";"Specif"]; Coqlib.check_required_library ["Coq";"Program";"Tactics"] - let set_program_mode c = if c then if !Flags.program_mode then () diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 0602e52e9..bdc97d48c 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -104,3 +104,6 @@ exception NoObligations of Names.Id.t option val explain_no_obligations : Names.Id.t option -> Pp.t val set_program_mode : bool -> unit + +type program_info +val program_tcc_summary_tag : program_info Id.Map.t Summary.Dyn.tag diff --git a/vernac/record.ml b/vernac/record.ml index 1d255b08e..114b55cb4 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -60,23 +60,25 @@ let _ = optread = (fun () -> !typeclasses_unique); optwrite = (fun b -> typeclasses_unique := b); } -let interp_fields_evars env evars impls_env nots l = +let interp_fields_evars env sigma impls_env nots l = List.fold_left2 - (fun (env, uimpls, params, impls) no ((loc, i), b, t) -> - let t', impl = interp_type_evars_impls env evars ~impls t in - let b' = Option.map (fun x -> fst (interp_casted_constr_evars_impls env evars ~impls x t')) b in + (fun (env, sigma, uimpls, params, impls) no ((loc, i), b, t) -> + let sigma, (t', impl) = interp_type_evars_impls env sigma ~impls t in + let sigma, b' = + Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@ + interp_casted_constr_evars_impls env sigma ~impls x t') (sigma,None) b in let impls = match i with | Anonymous -> impls - | Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method (EConstr.to_constr !evars t') impl) impls + | Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method (EConstr.to_constr sigma t') impl) impls in let d = match b' with | None -> LocalAssum (i,t') | Some b' -> LocalDef (i,b',t') in List.iter (Metasyntax.set_notation_for_interpretation env impls) no; - (EConstr.push_rel d env, impl :: uimpls, d::params, impls)) - (env, [], [], impls_env) nots l + (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls)) + (env, sigma, [], [], impls_env) nots l let compute_constructor_level evars env l = List.fold_right (fun d (env, univ) -> @@ -97,10 +99,9 @@ let binders_of_decls = List.map binder_of_decl let typecheck_params_and_fields finite def id poly pl t ps nots fs = let env0 = Global.env () in - let evd, decl = Univdecls.interp_univ_decl_opt env0 pl in - let evars = ref evd in - let _ = - let error bk (loc, name) = + let sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in + let _ = + let error bk (loc, name) = match bk, name with | Default _, Anonymous -> user_err ?loc ~hdr:"record" (str "Record parameters must be named") @@ -112,63 +113,65 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = | CLocalPattern (loc,(_,_)) -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps in - let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in - let typ, sort, template = match t with + let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars env0 sigma ps in + let sigma, typ, sort, template = match t with | Some t -> let env = EConstr.push_rel_context newps env0 in let poly = match t with | { CAst.v = CSort (Misctypes.GType []) } -> true | _ -> false in - let s = interp_type_evars env evars ~impls:empty_internalization_env t in - let sred = Reductionops.whd_all env !evars s in - (match EConstr.kind !evars sred with + let sigma, s = interp_type_evars env sigma ~impls:empty_internalization_env t in + let sred = Reductionops.whd_all env sigma s in + (match EConstr.kind sigma sred with | Sort s' -> - let s' = EConstr.ESorts.kind !evars s' in + let s' = EConstr.ESorts.kind sigma s' in (if poly then - match Evd.is_sort_variable !evars s' with - | Some l -> evars := Evd.make_flexible_variable !evars ~algebraic:true l; - s, s', true - | None -> s, s', false - else s, s', false) + match Evd.is_sort_variable sigma s' with + | Some l -> + let sigma = Evd.make_flexible_variable sigma ~algebraic:true l in + sigma, s, s', true + | None -> + sigma, s, s', false + else sigma, s, s', false) | _ -> user_err ?loc:(constr_loc t) (str"Sort expected.")) | None -> let uvarkind = Evd.univ_flexible_alg in - let s = Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars in - EConstr.mkSort s, s, true + let sigma, s = Evd.new_sort_variable uvarkind sigma in + sigma, EConstr.mkSort s, s, true in let arity = EConstr.it_mkProd_or_LetIn typ newps in let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in let assums = List.filter is_local_assum newps in let params = List.map (RelDecl.get_name %> Name.get_id) assums in let ty = Inductive (params,(finite != BiFinite)) in - let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr !evars arity] [imps] in - let env2,impls,newfs,data = - interp_fields_evars env_ar evars impls_env nots (binders_of_decls fs) + let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr sigma arity] [imps] in + let env2,sigma,impls,newfs,data = + interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs) in - let evars = - Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars Evd.empty in - let typ, evars = - let _, univ = compute_constructor_level evars env_ar newfs in + let sigma = + Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma Evd.empty in + let sigma, typ = + let _, univ = compute_constructor_level sigma env_ar newfs in if not def && (Sorts.is_prop sort || (Sorts.is_set sort && is_impredicative_set env0)) then - typ, evars + sigma, typ else - let evars = Evd.set_leq_sort env_ar evars (Type univ) sort in + let sigma = Evd.set_leq_sort env_ar sigma (Type univ) sort in if Univ.is_small_univ univ && - Option.cata (Evd.is_flexible_level evars) false (Evd.is_sort_variable evars sort) then + Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then (* We can assume that the level in aritysort is not constrained and clear it, if it is flexible *) - EConstr.mkSort (Sorts.sort_of_univ univ), - Evd.set_eq_sort env_ar evars (Prop Pos) sort - else typ, evars + Evd.set_eq_sort env_ar sigma (Prop Pos) sort, + EConstr.mkSort (Sorts.sort_of_univ univ) + else sigma, typ in - let evars, nf = Evarutil.nf_evars_and_universes evars in - let newfs = List.map (EConstr.to_rel_decl evars) newfs in - let newps = List.map (EConstr.to_rel_decl evars) newps in - let typ = EConstr.to_constr evars typ in - let ce t = Pretyping.check_evars env0 Evd.empty evars (EConstr.of_constr t) in - let univs = Evd.check_univ_decl ~poly evars decl in - let ubinders = Evd.universe_binders evars in + let sigma, _ = Evarutil.nf_evars_and_universes sigma in + let newfs = List.map (EConstr.to_rel_decl sigma) newfs in + let newps = List.map (EConstr.to_rel_decl sigma) newps in + let typ = EConstr.to_constr sigma typ in + let ce t = Pretyping.check_evars env0 Evd.empty sigma (EConstr.of_constr t) in + let univs = Evd.check_univ_decl ~poly sigma decl in + let ubinders = Evd.universe_binders sigma in List.iter (iter_constr ce) (List.rev newps); List.iter (iter_constr ce) (List.rev newfs); ubinders, univs, typ, template, imps, newps, impls, newfs @@ -430,7 +433,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t | Monomorphic_const_entry _ -> mie in - let kn = Command.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in + let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name coers ubinders fieldimpls fields in @@ -613,7 +616,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf States.with_state_protection (fun () -> typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in let sign = structure_signature (fields@params) in - match kind with + let gr = match kind with | Class def -> let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in let gr = declare_class finite def cum pl univs (loc,idstruc) idbuild @@ -638,3 +641,6 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf idbuild implpars params arity template implfs fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in IndRef ind + in + Declare.declare_univ_binders gr pl; + gr diff --git a/vernac/record.mli b/vernac/record.mli index 9fdd5e1c4..e632e7bbf 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -15,7 +15,7 @@ val primitive_flag : bool ref val definition_structure : inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic * - Decl_kinds.recursivity_kind * ident_decl with_coercion * local_binder_expr list * + Declarations.recursivity_kind * ident_decl with_coercion * local_binder_expr list * (local_decl_expr with_instance with_priority with_notation) list * Id.t * constr_expr option -> global_reference diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 6a10eb43a..7e96f28de 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -288,7 +288,6 @@ let init_terminal_output ~color = *) let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning - (* This is specific to the toplevel *) let pr_loc loc = let fname = loc.Loc.fname in @@ -311,17 +310,23 @@ let print_err_exn ?extra any = std_logger ~pre_hdr Feedback.Error msg let with_output_to_file fname func input = - (* XXX FIXME: redirect std_ft *) - (* let old_logger = !logger in *) let channel = open_out (String.concat "." [fname; "out"]) in - (* logger := ft_logger old_logger (Format.formatter_of_out_channel channel); *) + let old_fmt = !std_ft, !err_ft, !deep_ft in + let new_ft = Format.formatter_of_out_channel channel in + std_ft := new_ft; + err_ft := new_ft; + deep_ft := new_ft; try let output = func input in - (* logger := old_logger; *) + std_ft := Util.pi1 old_fmt; + err_ft := Util.pi2 old_fmt; + deep_ft := Util.pi3 old_fmt; close_out channel; output with reraise -> let reraise = Backtrace.add_backtrace reraise in - (* logger := old_logger; *) + std_ft := Util.pi1 old_fmt; + err_ft := Util.pi2 old_fmt; + deep_ft := Util.pi3 old_fmt; close_out channel; Exninfo.iraise reraise diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 8673155e2..f001b572a 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -11,7 +11,11 @@ Search Indschemes DeclareDef Obligations -Command +ComDefinition +ComAssumption +ComInductive +ComFixpoint +ComProgramFixpoint Classes Record Assumptions diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f8ec05fdb..a581043ac 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -18,7 +18,6 @@ open Tacmach open Constrintern open Prettyp open Printer -open Command open Goptions open Libnames open Globnames @@ -479,6 +478,7 @@ let vernac_definition ~atts discharge kind ((loc,id as lid),pl) def = | Discharge -> Dumpglob.dump_definition lid true "var" | Local | Global -> Dumpglob.dump_definition lid false "def" in + let program_mode = Flags.is_program_mode () in (match def with | ProveBody (bl,t) -> (* local binders, typ *) start_proof_and_print (local, atts.polymorphic, DefinitionBody kind) @@ -489,7 +489,7 @@ let vernac_definition ~atts discharge kind ((loc,id as lid),pl) def = | Some r -> let sigma, env = Pfedit.get_current_context () in Some (snd (Hook.get f_interp_redexp env sigma r)) in - do_definition id (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook) + ComDefinition.do_definition ~program_mode id (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook) let vernac_start_proof ~atts kind l = let local = enforce_locality_exp atts.locality NoDischarge in @@ -520,7 +520,7 @@ let vernac_assumption ~atts discharge kind l nl = List.iter (fun (lid, _) -> if global then Dumpglob.dump_definition lid false "ax" else Dumpglob.dump_definition lid true "var") idl) l; - let status = do_assumptions kind nl l in + let status = ComAssumption.do_assumptions kind nl l in if not status then Feedback.feedback Feedback.AddedAxiom let should_treat_as_cumulative cum poly = @@ -592,18 +592,29 @@ let vernac_inductive ~atts cum lo finite indl = | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.") in let indl = List.map unpack indl in - do_mutual_inductive indl is_cumulative atts.polymorphic lo finite + ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite let vernac_fixpoint ~atts discharge l = let local = enforce_locality_exp atts.locality discharge in if Dumpglob.dump () then List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; + (* XXX: Switch to the attribute system and match on ~atts *) + let do_fixpoint = if Flags.is_program_mode () then + ComProgramFixpoint.do_fixpoint + else + ComFixpoint.do_fixpoint + in do_fixpoint local atts.polymorphic l let vernac_cofixpoint ~atts discharge l = let local = enforce_locality_exp atts.locality discharge in if Dumpglob.dump () then List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; + let do_cofixpoint = if Flags.is_program_mode () then + ComProgramFixpoint.do_cofixpoint + else + ComFixpoint.do_cofixpoint + in do_cofixpoint local atts.polymorphic l let vernac_scheme l = @@ -627,14 +638,14 @@ let vernac_universe ~atts l = user_err ?loc:atts.loc ~hdr:"vernac_universe" (str"Polymorphic universes can only be declared inside sections, " ++ str "use Monomorphic Universe instead"); - do_universe atts.polymorphic l + Declare.do_universe atts.polymorphic l let vernac_constraint ~atts l = if atts.polymorphic && not (Lib.sections_are_opened ()) then user_err ?loc:atts.loc ~hdr:"vernac_constraint" (str"Polymorphic universe constraints can only be declared" ++ str " inside sections, use Monomorphic Constraint instead"); - do_constraint atts.polymorphic l + Declare.do_constraint atts.polymorphic l (**********************) (* Modules *) @@ -831,7 +842,8 @@ let vernac_identity_coercion ~atts id qids qidt = let vernac_instance ~atts abst sup inst props pri = let global = not (make_section_locality atts.locality) in Dumpglob.dump_constraint inst false "inst"; - ignore(Classes.new_instance ~abstract:abst ~global atts.polymorphic sup inst props pri) + let program_mode = Flags.is_program_mode () in + ignore(Classes.new_instance ~program_mode ~abstract:abst ~global atts.polymorphic sup inst props pri) let vernac_context ~atts l = if not (Classes.context atts.polymorphic l) then Feedback.feedback Feedback.AddedAxiom @@ -1591,13 +1603,14 @@ let vernac_declare_reduction ~atts s r = let vernac_global_check c = let env = Global.env() in let sigma = Evd.from_env env in - let c,ctx = interp_constr env sigma c in + let c,uctx = interp_constr env sigma c in let senv = Global.safe_env() in - let cstrs = snd (UState.context_set ctx) in - let senv = Safe_typing.add_constraints cstrs senv in + let uctx = UState.context_set uctx in + let senv = Safe_typing.push_context_set false uctx senv in let j = Safe_typing.typing senv c in let env = Safe_typing.env_of_safe_env senv in - Feedback.msg_notice (print_safe_judgment env sigma j) + Feedback.msg_notice (print_safe_judgment env sigma j ++ + pr_universe_ctx_set sigma uctx) let get_nth_goal n = @@ -1656,13 +1669,13 @@ let vernac_print ~atts env sigma = | PrintMLModules -> msg_notice (Mltop.print_ml_modules ()) | PrintDebugGC -> msg_notice (Mltop.print_gc ()) | PrintName (qid,udecl) -> dump_global qid; msg_notice (print_name env sigma qid udecl) - | PrintGraph -> msg_notice (Prettyp.print_graph()) + | PrintGraph -> msg_notice (Prettyp.print_graph env sigma) | PrintClasses -> msg_notice (Prettyp.print_classes()) | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses()) | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c)) | PrintCoercions -> msg_notice (Prettyp.print_coercions env sigma) | PrintCoercionPaths (cls,clt) -> - msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)) + msg_notice (Prettyp.print_path_between env sigma (cl_of_qualid cls) (cl_of_qualid clt)) | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections env sigma) | PrintUniverses (b, dst) -> let univ = Global.universes () in @@ -1696,7 +1709,7 @@ let vernac_print ~atts env sigma = let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in let nassums = Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in - msg_notice (Printer.pr_assumptionset (Global.env ()) nassums) + msg_notice (Printer.pr_assumptionset env sigma nassums) | PrintStrategy r -> print_strategy r let global_module r = @@ -2268,5 +2281,10 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = comments on the PR *) let interp ?verbosely ?proof ~st cmd = Vernacstate.unfreeze_interp_state st; - interp ?verbosely ?proof ~st cmd; - Vernacstate.freeze_interp_state `No + try + interp ?verbosely ?proof ~st cmd; + Vernacstate.freeze_interp_state `No + with exn -> + let exn = CErrors.push exn in + Vernacstate.invalidate_cache (); + iraise exn diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 4a1ae14e3..4980333b5 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -12,18 +12,30 @@ type t = { shallow : bool (* is the state trimmed down (libstack) *) } -let s_cache = ref (States.freeze ~marshallable:`No) -let s_proof = ref (Proof_global.freeze ~marshallable:`No) +let s_cache = ref None +let s_proof = ref None let invalidate_cache () = - s_cache := Obj.magic 0; - s_proof := Obj.magic 0 + s_cache := None; + s_proof := None + +let update_cache rf v = + rf := Some v; v + +let do_if_not_cached rf f v = + match !rf with + | None -> + rf := Some v; f v + | Some vc when vc != v -> + rf := Some v; f v + | Some _ -> + () let freeze_interp_state marshallable = - { system = (s_cache := States.freeze ~marshallable; !s_cache); - proof = (s_proof := Proof_global.freeze ~marshallable; !s_proof); + { system = update_cache s_cache (States.freeze ~marshallable); + proof = update_cache s_proof (Proof_global.freeze ~marshallable); shallow = marshallable = `Shallow } let unfreeze_interp_state { system; proof } = - if (!s_cache != system) then (s_cache := system; States.unfreeze system); - if (!s_proof != proof) then (s_proof := proof; Proof_global.unfreeze proof) + do_if_not_cached s_cache States.unfreeze system; + do_if_not_cached s_proof Proof_global.unfreeze proof |