diff options
Diffstat (limited to 'vernac')
35 files changed, 1033 insertions, 950 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 6711b14da..d22024568 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -18,7 +18,7 @@ open Pp open CErrors open Util open Names -open Term +open Constr open Declarations open Mod_subst open Globnames @@ -89,7 +89,7 @@ and fields_of_mp mp = let mb = lookup_module_in_impl mp in let fields,inner_mp,subs = fields_of_mb empty_subst mb [] in let subs = - if mp_eq inner_mp mp then subs + if ModPath.equal inner_mp mp then subs else add_mp inner_mp mp mb.mod_delta subs in Modops.subst_structure subs fields @@ -118,7 +118,7 @@ and fields_of_expression x = fields_of_functor fields_of_expr x let lookup_constant_in_impl cst fallback = try - let mp,dp,lab = repr_kn (canonical_con cst) in + let mp,dp,lab = KerName.repr (Constant.canonical cst) in let fields = memoize_fields_of_mp mp in (* A module found this way is necessarily closed, in particular our constant cannot be in an opened section : *) @@ -131,7 +131,7 @@ let lookup_constant_in_impl cst fallback = - The label has not been found in the structure. This is an error *) match fallback with | Some cb -> cb - | None -> anomaly (str "Print Assumption: unknown constant " ++ pr_con cst ++ str ".") + | None -> anomaly (str "Print Assumption: unknown constant " ++ Constant.print cst ++ str ".") let lookup_constant cst = try @@ -142,7 +142,7 @@ let lookup_constant cst = let lookup_mind_in_impl mind = try - let mp,dp,lab = repr_kn (canonical_mind mind) in + let mp,dp,lab = KerName.repr (MutInd.canonical mind) in let fields = memoize_fields_of_mp mp in search_mind_label lab fields with Not_found -> @@ -156,14 +156,14 @@ let lookup_mind mind = traversed objects *) let label_of = function - | ConstRef kn -> pi3 (repr_con kn) + | ConstRef kn -> pi3 (Constant.repr3 kn) | IndRef (kn,_) - | ConstructRef ((kn,_),_) -> pi3 (repr_mind kn) + | ConstructRef ((kn,_),_) -> pi3 (MutInd.repr3 kn) | VarRef id -> Label.of_id id let fold_constr_with_full_binders g f n acc c = let open Context.Rel.Declaration in - match kind_of_term c with + match Constr.kind c with | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> acc | Cast (c,_, t) -> f n (f n acc c) t | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c @@ -182,7 +182,7 @@ let fold_constr_with_full_binders g f n acc c = let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd -let rec traverse current ctx accu t = match kind_of_term t with +let rec traverse current ctx accu t = match Constr.kind t with | Var id -> let body () = id |> Global.lookup_named |> NamedDecl.get_value in traverse_object accu body (VarRef id) diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli index 46730f824..afe932ead 100644 --- a/vernac/assumptions.mli +++ b/vernac/assumptions.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Globnames open Printer @@ -21,11 +21,11 @@ open Printer val traverse : Label.t -> constr -> (Refset_env.t * Refset_env.t Refmap_env.t * - (label * Context.Rel.t * types) list Refmap_env.t) + (Label.t * Context.Rel.t * types) list Refmap_env.t) (** Collects all the assumptions (optionally including opaque definitions) on which a term relies (together with their type). The above warning of {!traverse} also applies. *) val assumptions : ?add_opaque:bool -> ?add_transparent:bool -> transparent_state -> - global_reference -> constr -> Term.types ContextObjectMap.t + global_reference -> constr -> types ContextObjectMap.t diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 66a4a2e49..51dd5cd4f 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -13,12 +13,12 @@ open CErrors open Util open Pp open Term +open Constr open Vars open Termops open Declarations open Names open Globnames -open Nameops open Inductiveops open Tactics open Ind_tables @@ -199,7 +199,7 @@ let build_beq_scheme mode kn = | Cast (x,_,_) -> aux (EConstr.applist (x,a)) | App _ -> assert false | Ind ((kn',i as ind'),u) (*FIXME: universes *) -> - if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants + if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants else begin try let eq, eff = @@ -360,15 +360,15 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = if Id.equal avoid.(n-i) s then avoid.(n-i-x) else (if i<n then find (i+1) else user_err ~hdr:"AutoIndDecl.do_replace_lb" - (str "Var " ++ pr_id s ++ str " seems unknown.") + (str "Var " ++ Id.print s ++ str " seems unknown.") ) in mkVar (find 1) with e when CErrors.noncritical e -> (* if this happen then the args have to be already declared as a Parameter*) ( - let mp,dir,lbl = repr_con (fst (destConst sigma v)) in - mkConst (make_con mp dir (mk_label ( + let mp,dir,lbl = Constant.repr3 (fst (destConst sigma v)) in + mkConst (Constant.make3 mp dir (Label.make ( if Int.equal offset 1 then ("eq_"^(Label.to_string lbl)) else ((Label.to_string lbl)^"_lb") ))) @@ -377,6 +377,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = Proofview.Goal.enter begin fun gl -> let type_of_pq = Tacmach.New.pf_unsafe_type_of gl p in let sigma = Tacmach.New.project gl in + let env = Tacmach.New.pf_env gl in let u,v = destruct_ind sigma type_of_pq in let lb_type_of_p = try @@ -389,7 +390,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = (str "Leibniz->boolean:" ++ str "You have to declare the" ++ str "decidability over " ++ - Printer.pr_econstr type_of_pq ++ + Printer.pr_econstr_env env sigma type_of_pq ++ str " first.") in Tacticals.New.tclZEROMSG err_msg @@ -421,15 +422,15 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = if Id.equal avoid.(n-i) s then avoid.(n-i-x) else (if i<n then find (i+1) else user_err ~hdr:"AutoIndDecl.do_replace_bl" - (str "Var " ++ pr_id s ++ str " seems unknown.") + (str "Var " ++ Id.print s ++ str " seems unknown.") ) in mkVar (find 1) with e when CErrors.noncritical e -> (* if this happen then the args have to be already declared as a Parameter*) ( - let mp,dir,lbl = repr_con (fst (destConst sigma v)) in - mkConst (make_con mp dir (mk_label ( + let mp,dir,lbl = Constant.repr3 (fst (destConst sigma v)) in + mkConst (Constant.make3 mp dir (Label.make ( if Int.equal offset 1 then ("eq_"^(Label.to_string lbl)) else ((Label.to_string lbl)^"_bl") ))) @@ -442,6 +443,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = Proofview.Goal.enter begin fun gl -> let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in let sigma = Tacmach.New.project gl in + let env = Tacmach.New.pf_env gl in if EConstr.eq_constr sigma t1 t2 then aux q1 q2 else ( let u,v = try destruct_ind sigma tt1 @@ -461,7 +463,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = (str "boolean->Leibniz:" ++ str "You have to declare the" ++ str "decidability over " ++ - Printer.pr_econstr tt1 ++ + Printer.pr_econstr_env env sigma tt1 ++ str " first.") in user_err err_msg @@ -504,7 +506,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.") end end >>= fun (sp2,i2) -> - if not (eq_mind sp1 sp2) || not (Int.equal i1 i2) + if not (MutInd.equal sp1 sp2) || not (Int.equal i1 i2) then Tacticals.New.tclZEROMSG (str "Eq should be on the same type") else aux (Array.to_list ca1) (Array.to_list ca2) @@ -531,8 +533,8 @@ let eqI ind l = and e, eff = try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff with Not_found -> user_err ~hdr:"AutoIndDecl.eqI" - (str "The boolean equality on " ++ pr_mind (fst ind) ++ str " is needed."); - in (if Array.equal Term.eq_constr eA [||] then e else mkApp(e,eA)), eff + (str "The boolean equality on " ++ MutInd.print (fst ind) ++ str " is needed."); + in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA)), eff (**********************************************************************) (* Boolean->Leibniz *) diff --git a/vernac/class.ml b/vernac/class.ml index 3915148a0..943da8fa8 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -11,6 +11,7 @@ open Util open Pp open Names open Term +open Constr open Vars open Termops open Entries @@ -83,16 +84,9 @@ let check_target clt = function (* condition d'heritage uniforme *) -let uniform_cond sigma nargs lt = - let open EConstr in - let rec aux = function - | (0,[]) -> true - | (n,t::l) -> - let t = strip_outer_cast sigma t in - isRel sigma t && Int.equal (destRel sigma t) n && aux ((n-1),l) - | _ -> false - in - aux (nargs,lt) +let uniform_cond sigma ctx lt = + List.for_all2eq (EConstr.eq_constr sigma) + lt (Context.Rel.to_extended_list EConstr.mkRel 0 ctx) let class_of_global = function | ConstRef sp -> @@ -118,24 +112,29 @@ l'indice de la classe source dans la liste lp *) let get_source lp source = + let open Context.Rel.Declaration in match source with | None -> - let (cl1,u1,lv1) = - match lp with - | [] -> raise Not_found - | t1::_ -> find_class_type Evd.empty (EConstr.of_constr t1) - in - (cl1,u1,lv1,1) + (* Take the latest non let-in argument *) + let rec aux = function + | [] -> raise Not_found + | LocalDef _ :: lt -> aux lt + | LocalAssum (_,t1) :: lt -> + let cl1,u1,lv1 = find_class_type Evd.empty (EConstr.of_constr t1) in + cl1,lt,lv1,1 + in aux lp | Some cl -> - let rec aux = function - | [] -> raise Not_found - | t1::lt -> - try - let cl1,u1,lv1 = find_class_type Evd.empty (EConstr.of_constr t1) in - if cl_typ_eq cl cl1 then cl1,u1,lv1,(List.length lt+1) - else raise Not_found - with Not_found -> aux lt - in aux (List.rev lp) + (* Take the first argument that matches *) + let rec aux acc = function + | [] -> raise Not_found + | LocalDef _ as decl :: lt -> aux (decl::acc) lt + | LocalAssum (_,t1) as decl :: lt -> + try + let cl1,u1,lv1 = find_class_type Evd.empty (EConstr.of_constr t1) in + if cl_typ_eq cl cl1 then cl1,acc,lv1,Context.Rel.nhyps lt+1 + else raise Not_found + with Not_found -> aux (decl::acc) lt + in aux [] (List.rev lp) let get_target t ind = if (ind > 1) then @@ -146,15 +145,6 @@ let get_target t ind = CL_PROJ p | x -> x - -let prods_of t = - let rec aux acc d = match kind_of_term d with - | Prod (_,c1,c2) -> aux (c1::acc) c2 - | Cast (c,_,_) -> aux acc c - | _ -> (d,acc) - in - aux [] t - let strength_of_cl = function | CL_CONST kn -> `GLOBAL | CL_SECVAR id -> `LOCAL @@ -173,8 +163,8 @@ let get_strength stre ref cls clt = let ident_key_of_class = function | CL_FUN -> "Funclass" | CL_SORT -> "Sortclass" - | CL_CONST sp | CL_PROJ sp -> Label.to_string (con_label sp) - | CL_IND (sp,_) -> Label.to_string (mind_label sp) + | CL_CONST sp | CL_PROJ sp -> Label.to_string (Constant.label sp) + | CL_IND (sp,_) -> Label.to_string (MutInd.label sp) | CL_SECVAR id -> Id.to_string id (* Identity coercion *) @@ -222,10 +212,10 @@ let build_id_coercion idf_opt source poly = Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) in - let univs = (snd (Evd.universe_context ~names:[] ~extensible:true sigma)) in + let univs = Evd.const_univ_entry ~poly sigma in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry - (definition_entry ~types:typ_f ~poly ~univs + (definition_entry ~types:typ_f ~univs ~inline:true (mkCast (val_f, DEFAULTcast, typ_f))) in let decl = (constr_entry, IsDefinition IdentityCoercion) in @@ -257,17 +247,18 @@ let add_new_coercion_core coef stre poly source target isid = check_source source; let t, _ = Global.type_of_global_in_context (Global.env ()) coef in if coercion_exists coef then raise (CoercionError AlreadyExists); - let tg,lp = prods_of t in + let lp,tg = decompose_prod_assum t in let llp = List.length lp in if Int.equal llp 0 then raise (CoercionError NotAFunction); - let (cls,us,lvs,ind) = + let (cls,ctx,lvs,ind) = try get_source lp source with Not_found -> raise (CoercionError (NoSource source)) in check_source (Some cls); - if not (uniform_cond Evd.empty (** FIXME *) (llp-ind) lvs) then + if not (uniform_cond Evd.empty (** FIXME - for when possibly called with unresolved evars in the future *) + ctx lvs) then warn_uniform_inheritance coef; let clt = try diff --git a/vernac/classes.ml b/vernac/classes.ml index 0926c93e5..3e47f881c 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -9,6 +9,7 @@ (*i*) open Names open Term +open Constr open Vars open Environ open Nametab @@ -98,7 +99,7 @@ let type_ctx_instance evars env ctx inst subst = let id_of_class cl = match cl.cl_impl with - | ConstRef kn -> let _,_,l = repr_con kn in Label.to_id l + | ConstRef kn -> let _,_,l = Constant.repr3 kn in Label.to_id l | IndRef (kn,i) -> let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in mip.(0).Declarations.mind_typename @@ -113,19 +114,20 @@ let instance_hook k info global imps ?hook cst = let declare_instance_constant k info global imps ?hook id decl poly evm 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 + let evm = + 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 evm levels in - let pl, uctx = Evd.check_univ_decl evm decl in + let uctx = Evd.check_univ_decl ~poly evm decl in let entry = - Declare.definition_entry ~types:termtype ~poly ~univs:uctx term + 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) pl; + Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders evm); instance_hook k info global imps ?hook (ConstRef kn); id @@ -179,7 +181,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) Name id -> let sp = Lib.make_path id in if Nametab.exists_cci sp then - user_err ~hdr:"new_instance" (Nameops.pr_id id ++ Pp.str " already exists."); + user_err ~hdr:"new_instance" (Id.print id ++ Pp.str " already exists."); id | Anonymous -> let i = Nameops.add_suffix (id_of_class k) "_instance_0" in @@ -199,16 +201,16 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) 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 pl, ctx = Evd.check_univ_decl !evars decl in - let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id - (ParameterEntry - (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) - in - Universes.register_universe_binders (ConstRef cst) pl; - instance_hook k pri global imps ?hook (ConstRef cst); id + 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 cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id + (ParameterEntry + (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical) + in + Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders !evars); + instance_hook k pri global imps ?hook (ConstRef cst); id end else ( let props = @@ -383,14 +385,17 @@ let context poly l = let uctx = ref (Evd.universe_context_set !evars) in let fn status (id, b, t) = if Lib.is_modtype () && not (Lib.sections_are_opened ()) then - let ctx = Univ.ContextSet.to_context !uctx in (* Declare the universe context once *) + let univs = if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx) + else Monomorphic_const_entry !uctx + in let () = uctx := Univ.ContextSet.empty in let decl = match b with | None -> - (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical) + (ParameterEntry (None,(t,univs),None), IsAssumption Logical) | Some b -> - let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in + let entry = Declare.definition_entry ~univs ~types:t b in (DefinitionEntry entry, IsAssumption Logical) in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in @@ -408,16 +413,19 @@ let context poly l = in let impl = List.exists test impls in let decl = (Discharge, poly, Definitional) in + let univs = if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx) + else Monomorphic_const_entry !uctx + in let nstatus = match b with | None -> - pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl + pi3 (Command.declare_assumption false decl (t, univs) Universes.empty_binders [] impl Vernacexpr.NoInline (Loc.tag id)) | Some b -> - let ctx = Univ.ContextSet.to_context !uctx in let decl = (Discharge, poly, Definition) in - let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in + let entry = Declare.definition_entry ~univs ~types:t b in let hook = Lemmas.mk_hook (fun _ gr -> gr) in - let _ = DeclareDef.declare_definition id decl entry [] [] hook in + let _ = DeclareDef.declare_definition id decl entry Universes.empty_binders [] hook in Lib.sections_are_opened () || Lib.is_modtype_strict () in status && nstatus diff --git a/vernac/classes.mli b/vernac/classes.mli index fcdb5c3bc..c0f03227c 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -34,7 +34,7 @@ val declare_instance_constant : bool -> (* polymorphic *) Evd.evar_map -> (* Universes *) Constr.t -> (** body *) - Term.types -> (** type *) + Constr.types -> (** type *) Names.Id.t val new_instance : diff --git a/vernac/command.ml b/vernac/command.ml index f58ed065c..23be2c308 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -8,8 +8,9 @@ open Pp open CErrors +open Sorts open Util -open Term +open Constr open Vars open Termops open Environ @@ -21,7 +22,6 @@ open Globnames open Nameops open Constrexpr open Constrexpr_ops -open Topconstr open Constrintern open Nametab open Impargs @@ -44,7 +44,7 @@ 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 kind_of_term c with + 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) -> @@ -59,7 +59,7 @@ let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function if not has_no_args then user_err ?loc (strbrk"Cannot infer the non constant arguments of the conclusion of " - ++ pr_id cs ++ str "."); + ++ 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 @@ -88,14 +88,14 @@ let warn_implicits_in_term = strbrk "Implicit arguments declaration relies on type." ++ spc () ++ strbrk "The term declares more implicits than the type here.") -let interp_definition pl bl p red_option c ctypopt = +let 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 = + let imps,ce = match ctypopt with None -> let subst = evd_comb0 Evd.nf_univ_variables evdref in @@ -105,14 +105,14 @@ let interp_definition pl bl p red_option c ctypopt = 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 pl, uctx = Evd.check_univ_decl evd decl in - imps1@(Impargs.lift_implicits nb_args imps2), pl, - definition_entry ~univs:uctx ~poly:p body + let vars = EConstr.universes_of_constr env !evdref (EConstr.of_constr body) in + let () = evdref := Evd.restrict_universe_context !evdref vars in + let uctx = Evd.check_univ_decl ~poly !evdref decl in + imps1@(Impargs.lift_implicits nb_args imps2), + 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 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 @@ -130,22 +130,22 @@ let interp_definition pl bl p red_option c ctypopt = 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 pl, uctx = Evd.check_univ_decl ctx decl in - imps1@(Impargs.lift_implicits nb_args impsty), pl, - definition_entry ~types:typ ~poly:p - ~univs:uctx body + let bodyvars = EConstr.universes_of_constr env !evdref (EConstr.of_constr body) in + let tyvars = EConstr.universes_of_constr env !evdref (EConstr.of_constr ty) in + let vars = Univ.LSet.union bodyvars tyvars in + let () = evdref := Evd.restrict_universe_context !evdref vars in + let uctx = Evd.check_univ_decl ~poly !evdref decl in + imps1@(Impargs.lift_implicits nb_args impsty), + definition_entry ~types:typ ~univs:uctx body in - red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, pl, imps + (red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, imps) -let check_definition (ce, evd, _, _, 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) = + let (ce, evd, univdecl, imps as def) = interp_definition univdecl bl (pi2 k) red_option c ctypopt in if Flags.is_program_mode () then @@ -166,21 +166,43 @@ let do_definition ident k univdecl bl red_option c ctypopt hook = 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 + 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))) (* 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 () ++ pr_id ident ++ + Feedback.msg_info (str"Variable" ++ spc () ++ Id.print ident ++ strbrk " is not visible from current goals") in let r = VarRef ident in @@ -189,24 +211,24 @@ match local with (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 ctx = Univ.ContextSet.to_context ctx in - let decl = (ParameterEntry (None,p,(c,ctx),inl), IsAssumption kind) 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 () = Declare.declare_univ_binders gr pl in let () = assumption_message ident in - let () = Typeclasses.declare_instance None false gr 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 = - if p (* polymorphic *) then Univ.UContext.instance ctx - else Univ.Instance.empty + 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 ()) @@ -216,26 +238,63 @@ let interp_assumption evdref env impls bl c = let ty = EConstr.Unsafe.to_constr ty in (ty, impls) -let declare_assumptions idl is_coe k (c,ctx) pl imps impl_is_on nl = +(* 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,ctx) id -> + List.fold_left (fun (refs,status,uctx) id -> let ref',u',status' = - declare_assumption is_coe k (c,ctx) pl imps impl_is_on nl id in - (ref',u')::refs, status' && status, Univ.ContextSet.empty) - ([],true,ctx) idl + 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 do_assumptions_unbound_univs (_, poly, _ as kind) nl l = + +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 evdref = ref (Evd.from_env env) in - let l = - if poly then + 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) + List.fold_right (fun id acc -> + (is_coe, ([id], c)) :: acc) idl acc) l [] else l in @@ -247,65 +306,31 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = 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,ienv),((is_coe,idl),t,imps))) (env,empty_internalization_env) l in let evd = solve_remaining_evars all_and_fail_flags env !evdref Evd.empty in (* The universe constraints come from the whole telescope. *) let evd = Evd.nf_constraints evd in - let ctx = Evd.universe_context_set evd in - let nf_evar c = EConstr.Unsafe.to_constr (nf_evar evd (EConstr.of_constr c)) in - let l = List.map (on_pi2 nf_evar) l in - pi2 (List.fold_left (fun (subst,status,ctx) ((is_coe,idl),t,imps) -> - let t = replace_vars subst t in - let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in - let subst' = List.map2 - (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u))) - idl refs - in - (subst'@subst, status' && status, - (* The universe constraints are declared with the first declaration only. *) - Univ.ContextSet.empty)) ([],true,ctx) l) - -let do_assumptions_bound_univs coe kind nl id pl c = - let env = Global.env () in - let evd, decl = Univdecls.interp_univ_decl_opt env pl in - let evdref = ref evd in - let ty, impls = interp_type_evars_impls env evdref c in - let nf, subst = Evarutil.e_nf_evars_and_universes evdref in - let ty = EConstr.Unsafe.to_constr ty in - let ty = nf ty in - let vars = Univops.universes_of_constr ty in - let evd = Evd.restrict_universe_context !evdref vars in - let pl, uctx = Evd.check_univ_decl evd decl in - let uctx = Univ.ContextSet.of_context uctx in - let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls false nl id in - st - -let do_assumptions kind nl l = match l with -| [coe, ([id, Some pl], c)] -> - let () = match kind with - | (Discharge, _, _) when Lib.sections_are_opened () -> - let loc = fst id in - let msg = Pp.str "Section variables cannot be polymorphic." in - user_err ?loc msg - | _ -> () + 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 env t) in + uvars, (coe,t,imps)) + Univ.LSet.empty l in - do_assumptions_bound_univs coe kind nl id (Some pl) c -| _ -> - let map (coe, (idl, c)) = - let map (id, univs) = match univs with - | None -> id - | Some _ -> - let loc = fst id in - let msg = - Pp.str "Assumptions with bound universes can only be defined one at a time." in - user_err ?loc msg - in - (coe, (List.map map idl, c)) - in - let l = List.map map l in - do_assumptions_unbound_univs kind nl l + 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 *) @@ -327,9 +352,9 @@ type structured_inductive_expr = let minductive_message warn = function | [] -> user_err Pp.(str "No inductive definition.") - | [x] -> (pr_id x ++ str " is defined" ++ + | [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 pr_id l ++ + | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ spc () ++ str "are defined") let check_all_names_different indl = @@ -376,8 +401,8 @@ let rec check_anonymous_type ind = | _ -> false let make_conclusion_flexible evdref ty poly = - if poly && isArity ty then - let _, concl = destArity ty in + if poly && Term.isArity ty then + let _, concl = Term.destArity ty in match concl with | Type u -> (match Univ.universe_level u with @@ -550,12 +575,13 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = 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 impls) notations; + 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 @@ -575,7 +601,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in let ctx_params = Context.Rel.map nf ctx_params in let evd = !evdref in - let pl, uctx = Evd.check_univ_decl evd decl 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,_) -> @@ -597,11 +623,12 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors in let univs = - if poly then + 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 - else + | Monomorphic_const_entry uctx -> Monomorphic_ind_entry uctx in (* Build the mutual inductive entry *) @@ -616,7 +643,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = in (if poly && cum then Inductiveops.infer_inductive_subtyping env_ar evd mind_ent - else mind_ent), pl, impls + else mind_ent), Evd.universe_binders evd, impls (* Very syntactical equality *) let eq_local_binders bl1 bl2 = @@ -652,7 +679,7 @@ let extract_mutual_inductive_declaration_components indl = let is_recursive mie = let rec is_recursive_constructor lift typ = - match Term.kind_of_term typ with + 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 @@ -683,7 +710,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls = let ind = (mind,i) in let gr = IndRef ind in maybe_declare_manual_implicits false gr indimpls; - Universes.register_universe_binders gr pl; + Declare.declare_univ_binders gr pl; List.iteri (fun j impls -> maybe_declare_manual_implicits false @@ -763,11 +790,11 @@ let rec partial_order cmp = function let non_full_mutual_message x xge y yge isfix rest = let reason = if Id.List.mem x yge then - pr_id y ++ str " depends on " ++ pr_id x ++ strbrk " but not conversely" + Id.print y ++ str " depends on " ++ Id.print x ++ strbrk " but not conversely" else if Id.List.mem y xge then - pr_id x ++ str " depends on " ++ pr_id y ++ strbrk " but not conversely" + Id.print x ++ str " depends on " ++ Id.print y ++ strbrk " but not conversely" else - pr_id y ++ str " and " ++ pr_id x ++ strbrk " are not mutually dependent" in + 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 = @@ -1018,23 +1045,22 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = 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 pl, plext = Option.cata - (fun d -> d.univdecl_instance, d.univdecl_extensible_instance) ([],true) pl in let hook, recname, typ = if List.length binders_rel > 1 then let name = add_suffix recname "_func" in let hook l gr _ = - let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in - let ty = it_mkProd_or_LetIn top_arity binders_rel in - let ty = EConstr.Unsafe.to_constr ty in - let pl, univs = Evd.universe_context ~names:pl ~extensible:plext !evdref in - (*FIXME poly? *) - let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in - (** FIXME: include locality *) - let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in - let gr = ConstRef c in - if Impargs.is_implicit_args () || not (List.is_empty impls) then - Impargs.declare_manual_implicits false gr [impls] + 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 @@ -1162,12 +1188,13 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind 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 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 pl, ctx = Evd.check_univ_decl evd pl 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); @@ -1194,12 +1221,14 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n 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 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 pl, ctx = Evd.check_univ_decl evd pl 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 *) @@ -1238,7 +1267,7 @@ let collect_evars_of_term evd c ty = Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) evars (Evd.from_ctx (Evd.evar_universe_context evd)) -let do_program_recursive local p fixkind fixl ntns = +let do_program_recursive local poly fixkind fixl ntns = let isfix = fixkind != Obligations.IsCoFixpoint in let (env, rec_sign, pl, evd), fix, info = interp_recursive isfix fixl ntns @@ -1280,8 +1309,8 @@ let do_program_recursive local p fixkind fixl ntns = 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) + | Obligations.IsFixpoint _ -> (local, poly, Fixpoint) + | Obligations.IsCoFixpoint -> (local, poly, CoFixpoint) in Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind diff --git a/vernac/command.mli b/vernac/command.mli index afa97aa24..c7342e6da 100644 --- a/vernac/command.mli +++ b/vernac/command.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Entries open Libnames open Globnames @@ -28,7 +28,7 @@ val do_constraint : polymorphic -> 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 + Univdecls.universe_decl * Impargs.manual_implicits val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option -> local_binder_expr list -> red_expr option -> constr_expr -> @@ -43,7 +43,7 @@ val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr opt (** 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 Univ.in_universe_context_set -> + types in_constant_universes_entry -> Universes.universe_binders -> Impargs.manual_implicits -> bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located -> global_reference * Univ.Instance.t * bool @@ -82,7 +82,7 @@ type one_inductive_impls = val interp_mutual_inductive : structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag -> - polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> + polymorphic -> private_flag -> Declarations.recursivity_kind -> mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list (** Registering a mutual inductive definition together with its @@ -90,13 +90,13 @@ val interp_mutual_inductive : val declare_mutual_inductive_with_eliminations : mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list -> - mutual_inductive + 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 + polymorphic -> private_flag -> Declarations.recursivity_kind -> unit (** {6 Fixpoints and cofixpoints} *) @@ -127,24 +127,24 @@ type recursive_preentry = val interp_fixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context * + 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 * Evd.evar_universe_context * + 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 * Evd.evar_universe_context * + 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 * Evd.evar_universe_context * + recursive_preentry * Univdecls.universe_decl * UState.t * (Context.Rel.t * Impargs.manual_implicits * int option) list -> decl_notation list -> unit diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index d7a4fcca3..dfac78c04 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -11,18 +11,17 @@ open Declare open Entries open Globnames open Impargs -open Nameops let warn_definition_not_visible = CWarnings.create ~name:"definition-not-visible" ~category:"implicits" Pp.(fun ident -> strbrk "Section definition " ++ - pr_id ident ++ strbrk " is not visible from current goals") + Names.Id.print ident ++ strbrk " is not visible from current goals") let warn_local_declaration = CWarnings.create ~name:"local-declaration" ~category:"scope" Pp.(fun (id,kind) -> - pr_id id ++ strbrk " is declared as a local " ++ str kind) + Names.Id.print id ++ strbrk " is declared as a local " ++ str kind) let get_locality id ~kind = function | Discharge -> @@ -37,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 @@ -50,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 @@ -58,7 +58,7 @@ let declare_definition ident (local, p, k) ce pl imps hook = declare_global_definition ident ce local k pl imps in Lemmas.call_hook fix_exn hook local r -let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps = - let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in +let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps = + let ce = definition_entry ~opaque ~types:t ~univs ~eff def in declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r)) diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 5dea0ba27..55f7c7861 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -15,5 +15,8 @@ val declare_definition : Id.t -> definition_kind -> Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits -> Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference -val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t -> - Safe_typing.private_constants Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> Globnames.global_reference +val declare_fix : ?opaque:bool -> definition_kind -> + Universes.universe_binders -> Entries.constant_universes_entry -> + Id.t -> Safe_typing.private_constants Entries.proof_output -> + Constr.types -> Impargs.manual_implicits -> + Globnames.global_reference diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 2178a7caa..d328ad0cf 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -75,8 +75,8 @@ 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 -> - wrap_vernac_error exn (Himsg.explain_refiner_error e) + | Logic.RefinerError (env, sigma, e) -> + wrap_vernac_error exn (Himsg.explain_refiner_error env sigma e) | Nametab.GlobalizationError q -> wrap_vernac_error exn (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 189c47aab..e8c5aeedd 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -11,7 +11,7 @@ open Util open Names open Nameops open Namegen -open Term +open Constr open Termops open Indtypes open Environ @@ -92,9 +92,7 @@ let jv_nf_betaiotaevar sigma jl = (** Printers *) -let pr_lconstr c = quote (pr_lconstr c) let pr_lconstr_env e s c = quote (pr_lconstr_env e s c) -let pr_leconstr c = quote (pr_leconstr c) let pr_leconstr_env e s c = quote (pr_leconstr_env e s c) let pr_ljudge_env e s c = let v,t = pr_ljudge_env e s c in (quote v,quote t) @@ -159,7 +157,7 @@ let pr_explicit env sigma t1 t2 = let pr_db env i = try match env |> lookup_rel i |> get_name with - | Name id -> pr_id id + | Name id -> Id.print id | Anonymous -> str "<>" with Not_found -> str "UNBOUND_REL_" ++ int i @@ -169,7 +167,7 @@ let explain_unbound_rel env sigma n = str "The reference " ++ int n ++ str " is free." let explain_unbound_var env v = - let var = pr_id v in + let var = Id.print v in str "No such section variable or assumption: " ++ var ++ str "." let explain_not_type env sigma j = @@ -189,7 +187,7 @@ let explain_bad_assumption env sigma j = let explain_reference_variables sigma id c = (* c is intended to be a global reference *) let pc = pr_global (fst (Termops.global_of_constr sigma c)) in - pc ++ strbrk " depends on the variable " ++ pr_id id ++ + pc ++ strbrk " depends on the variable " ++ Id.print id ++ strbrk " which is not declared in the context." let rec pr_disjunction pr = function @@ -407,7 +405,7 @@ let explain_not_product env sigma c = let pr = pr_lconstr_env env sigma c in str "The type of this term is a product" ++ spc () ++ str "while it is expected to be" ++ - (if Term.is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "." + (if Constr.is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "." (* TODO: use the names *) (* (co)fixpoints *) @@ -415,7 +413,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj = let pr_lconstr_env env sigma c = pr_leconstr_env env sigma c in let prt_name i = match names.(i) with - Name id -> str "Recursive definition of " ++ pr_id id + Name id -> str "Recursive definition of " ++ Id.print id | Anonymous -> str "The " ++ pr_nth i ++ str " definition" in let st = match err with @@ -430,7 +428,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj = let arg_env = make_all_name_different arg_env sigma in let called = match names.(j) with - Name id -> pr_id id + Name id -> Id.print id | Anonymous -> str "the " ++ pr_nth i ++ str " definition" in let pr_db x = quote (pr_db env x) in let vars = @@ -450,7 +448,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj = | NotEnoughArgumentsForFixCall j -> let called = match names.(j) with - Name id -> pr_id id + Name id -> Id.print id | Anonymous -> str "the " ++ pr_nth i ++ str " definition" in str "Recursive call to " ++ called ++ str " has not enough arguments" @@ -528,7 +526,7 @@ let pr_trailing_ne_context_of env sigma = let rec explain_evar_kind env sigma evk ty = function | Evar_kinds.NamedHole id -> - strbrk "the existential variable named " ++ pr_id id + strbrk "the existential variable named " ++ Id.print id | Evar_kinds.QuestionMark _ -> strbrk "this placeholder of type " ++ ty | Evar_kinds.CasesType false -> @@ -537,12 +535,12 @@ let rec explain_evar_kind env sigma evk ty = function strbrk "a subterm of type " ++ ty ++ strbrk " in the type of this pattern-matching problem" | Evar_kinds.BinderType (Name id) -> - strbrk "the type of " ++ Nameops.pr_id id + strbrk "the type of " ++ Id.print id | Evar_kinds.BinderType Anonymous -> strbrk "the type of this anonymous binder" | Evar_kinds.ImplicitArg (c,(n,ido),b) -> let id = Option.get ido in - strbrk "the implicit parameter " ++ pr_id id ++ spc () ++ str "of" ++ + strbrk "the implicit parameter " ++ Id.print id ++ spc () ++ str "of" ++ spc () ++ Nametab.pr_global_env Id.Set.empty c ++ strbrk " whose type is " ++ ty | Evar_kinds.InternalHole -> strbrk "an internal placeholder of type " ++ ty @@ -558,7 +556,7 @@ let rec explain_evar_kind env sigma evk ty = function assert false | Evar_kinds.VarInstance id -> strbrk "an instance of type " ++ ty ++ - str " for the variable " ++ pr_id id + str " for the variable " ++ Id.print id | Evar_kinds.SubEvar evk' -> let evi = Evd.find sigma evk' in let pc = match evi.evar_body with @@ -598,7 +596,7 @@ let explain_unsolvable_implicit env sigma evk explain = explain_placeholder_kind env sigma evi.evar_concl explain ++ pe let explain_var_not_found env id = - str "The variable" ++ spc () ++ pr_id id ++ + str "The variable" ++ spc () ++ Id.print id ++ spc () ++ str "was not found" ++ spc () ++ str "in the current" ++ spc () ++ str "environment" ++ str "." @@ -638,7 +636,7 @@ let explain_no_occurrence_found env sigma c id = str "Found no subterm matching " ++ pr_lconstr_env env sigma c ++ str " in " ++ (match id with - | Some id -> pr_id id + | Some id -> Id.print id | None -> str"the current goal") ++ str "." let explain_cannot_unify_binding_type env sigma m n = @@ -660,7 +658,7 @@ let explain_wrong_abstraction_type env sigma na abs expected result = let abs = EConstr.to_constr sigma abs in let expected = EConstr.to_constr sigma expected in let result = EConstr.to_constr sigma result in - let ppname = match na with Name id -> pr_id id ++ spc () | _ -> mt () in + let ppname = match na with Name id -> Id.print id ++ spc () | _ -> mt () in str "Cannot instantiate metavariable " ++ ppname ++ strbrk "of type " ++ pr_lconstr_env env sigma expected ++ strbrk " with abstraction " ++ pr_lconstr_env env sigma abs ++ strbrk " of incompatible type " ++ @@ -723,9 +721,9 @@ let explain_type_error env sigma err = let pr_position (cl,pos) = let clpos = match cl with | None -> str " of the goal" - | Some (id,Locus.InHyp) -> str " of hypothesis " ++ pr_id id - | Some (id,Locus.InHypTypeOnly) -> str " of the type of hypothesis " ++ pr_id id - | Some (id,Locus.InHypValueOnly) -> str " of the body of hypothesis " ++ pr_id id in + | Some (id,Locus.InHyp) -> str " of hypothesis " ++ Id.print id + | Some (id,Locus.InHypTypeOnly) -> str " of the type of hypothesis " ++ Id.print id + | Some (id,Locus.InHypValueOnly) -> str " of the body of hypothesis " ++ Id.print id in int pos ++ clpos let explain_cannot_unify_occurrences env sigma nested ((cl2,pos2),t2) ((cl1,pos1),t1) e = @@ -844,7 +842,7 @@ let explain_not_match_error = function | ModuleTypeFieldExpected -> strbrk "a module type is expected" | NotConvertibleInductiveField id | NotConvertibleConstructorField id -> - str "types given to " ++ pr_id id ++ str " differ" + str "types given to " ++ Id.print id ++ str " differ" | NotConvertibleBodyField -> str "the body of definitions differs" | NotConvertibleTypeField (env, typ1, typ2) -> @@ -869,7 +867,7 @@ let explain_not_match_error = function | RecordProjectionsExpected nal -> (if List.length nal >= 2 then str "expected projection names are " else str "expected projection name is ") ++ - pr_enum (function Name id -> pr_id id | _ -> str "_") nal + pr_enum (function Name id -> Id.print id | _ -> str "_") nal | NotEqualInductiveAliases -> str "Aliases to inductive types do not match" | NoTypeConstraintExpected -> @@ -899,11 +897,11 @@ let explain_not_match_error = function quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst) let explain_signature_mismatch l spec why = - str "Signature components for label " ++ pr_label l ++ + str "Signature components for label " ++ Label.print l ++ str " do not match:" ++ spc () ++ explain_not_match_error why ++ str "." let explain_label_already_declared l = - str "The label " ++ pr_label l ++ str " is already declared." + str "The label " ++ Label.print l ++ str " is already declared." let explain_application_to_not_path _ = strbrk "A module cannot be applied to another module application or " ++ @@ -933,11 +931,11 @@ let explain_not_equal_module_paths mp1 mp2 = str "Non equal modules." let explain_no_such_label l = - str "No such label " ++ pr_label l ++ str "." + str "No such label " ++ Label.print l ++ str "." let explain_incompatible_labels l l' = str "Opening and closing labels are not the same: " ++ - pr_label l ++ str " <> " ++ pr_label l' ++ str "!" + Label.print l ++ str " <> " ++ Label.print l' ++ str "!" let explain_not_a_module s = quote (str s) ++ str " is not a module." @@ -946,19 +944,19 @@ let explain_not_a_module_type s = quote (str s) ++ str " is not a module type." let explain_not_a_constant l = - quote (pr_label l) ++ str " is not a constant." + quote (Label.print l) ++ str " is not a constant." let explain_incorrect_label_constraint l = str "Incorrect constraint for label " ++ - quote (pr_label l) ++ str "." + quote (Label.print l) ++ str "." let explain_generative_module_expected l = - str "The module " ++ pr_label l ++ str " is not generative." ++ + str "The module " ++ Label.print l ++ str " is not generative." ++ strbrk " Only components of generative modules can be changed" ++ strbrk " using the \"with\" construct." let explain_label_missing l s = - str "The field " ++ pr_label l ++ str " is missing in " + str "The field " ++ Label.print l ++ str " is missing in " ++ str s ++ str "." let explain_include_restricted_functor mp = @@ -1016,7 +1014,7 @@ let explain_not_a_class env c = pr_constr_env env Evd.empty c ++ str" is not a declared type class." let explain_unbound_method env cid id = - str "Unbound method name " ++ Nameops.pr_id (snd id) ++ spc () ++ + str "Unbound method name " ++ Id.print (snd id) ++ spc () ++ str"of class" ++ spc () ++ pr_global cid ++ str "." let pr_constr_exprs exprs = @@ -1037,52 +1035,52 @@ let explain_typeclass_error env = function (* Refiner errors *) -let explain_refiner_bad_type arg ty conclty = +let explain_refiner_bad_type env sigma arg ty conclty = str "Refiner was given an argument" ++ brk(1,1) ++ - pr_lconstr arg ++ spc () ++ - str "of type" ++ brk(1,1) ++ pr_lconstr ty ++ spc () ++ - str "instead of" ++ brk(1,1) ++ pr_lconstr conclty ++ str "." + pr_lconstr_env env sigma arg ++ spc () ++ + str "of type" ++ brk(1,1) ++ pr_lconstr_env env sigma ty ++ spc () ++ + str "instead of" ++ brk(1,1) ++ pr_lconstr_env env sigma conclty ++ str "." let explain_refiner_unresolved_bindings l = str "Unable to find an instance for the " ++ str (String.plural (List.length l) "variable") ++ spc () ++ prlist_with_sep pr_comma Name.print l ++ str"." -let explain_refiner_cannot_apply t harg = +let explain_refiner_cannot_apply env sigma t harg = str "In refiner, a term of type" ++ brk(1,1) ++ - pr_lconstr t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++ - pr_lconstr harg ++ str "." + pr_lconstr_env env sigma t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++ + pr_lconstr_env env sigma harg ++ str "." -let explain_refiner_not_well_typed c = - str "The term " ++ pr_lconstr c ++ str " is not well-typed." +let explain_refiner_not_well_typed env sigma c = + str "The term " ++ pr_lconstr_env env sigma c ++ str " is not well-typed." let explain_intro_needs_product () = str "Introduction tactics needs products." -let explain_does_not_occur_in c hyp = - str "The term" ++ spc () ++ pr_lconstr c ++ spc () ++ - str "does not occur in" ++ spc () ++ pr_id hyp ++ str "." +let explain_does_not_occur_in env sigma c hyp = + str "The term" ++ spc () ++ pr_lconstr_env env sigma c ++ spc () ++ + str "does not occur in" ++ spc () ++ Id.print hyp ++ str "." -let explain_non_linear_proof c = - str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++ +let explain_non_linear_proof env sigma c = + str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr_env env sigma c ++ spc () ++ str "because a metavariable has several occurrences." -let explain_meta_in_type c = - str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_leconstr c ++ +let explain_meta_in_type env sigma c = + str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_leconstr_env env sigma c ++ str " of another meta" let explain_no_such_hyp id = - str "No such hypothesis: " ++ pr_id id + str "No such hypothesis: " ++ Id.print id -let explain_refiner_error = function - | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty +let explain_refiner_error env sigma = function + | BadType (arg,ty,conclty) -> explain_refiner_bad_type env sigma arg ty conclty | UnresolvedBindings t -> explain_refiner_unresolved_bindings t - | CannotApply (t,harg) -> explain_refiner_cannot_apply t harg - | NotWellTyped c -> explain_refiner_not_well_typed c + | CannotApply (t,harg) -> explain_refiner_cannot_apply env sigma t harg + | NotWellTyped c -> explain_refiner_not_well_typed env sigma c | IntroNeedsProduct -> explain_intro_needs_product () - | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp - | NonLinearProof c -> explain_non_linear_proof c - | MetaInType c -> explain_meta_in_type c + | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in env sigma c hyp + | NonLinearProof c -> explain_non_linear_proof env sigma c + | MetaInType c -> explain_meta_in_type env sigma c | NoSuchHyp id -> explain_no_such_hyp id (* Inductive errors *) @@ -1102,7 +1100,7 @@ let error_ill_formed_inductive env c v = let error_ill_formed_constructor env id c v nparams nargs = let pv = pr_lconstr_env env Evd.empty v in let atomic = Int.equal (nb_prod Evd.empty (EConstr.of_constr c)) (** FIXME *) 0 in - str "The type of constructor" ++ brk(1,1) ++ pr_id id ++ brk(1,1) ++ + str "The type of constructor" ++ brk(1,1) ++ Id.print id ++ brk(1,1) ++ str "is not valid;" ++ brk(1,1) ++ strbrk (if atomic then "it must be " else "its conclusion must be ") ++ pv ++ @@ -1130,17 +1128,17 @@ let error_bad_ind_parameters env c n v1 v2 = str " as " ++ pr_nth n ++ str " argument in" ++ brk(1,1) ++ pc ++ str "." let error_same_names_types id = - str "The name" ++ spc () ++ pr_id id ++ spc () ++ + str "The name" ++ spc () ++ Id.print id ++ spc () ++ str "is used more than once." let error_same_names_constructors id = - str "The constructor name" ++ spc () ++ pr_id id ++ spc () ++ + str "The constructor name" ++ spc () ++ Id.print id ++ spc () ++ str "is used more than once." let error_same_names_overlap idl = strbrk "The following names are used both as type names and constructor " ++ str "names:" ++ spc () ++ - prlist_with_sep pr_comma pr_id idl ++ str "." + prlist_with_sep pr_comma Id.print idl ++ str "." let error_not_an_arity env c = str "The type" ++ spc () ++ pr_lconstr_env env Evd.empty c ++ spc () ++ diff --git a/vernac/himsg.mli b/vernac/himsg.mli index 5b91f9e68..8945ebadb 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -27,7 +27,7 @@ val explain_typeclass_error : env -> typeclass_error -> Pp.t val explain_recursion_scheme_error : recursion_scheme_error -> Pp.t -val explain_refiner_error : refiner_error -> Pp.t +val explain_refiner_error : env -> Evd.evar_map -> refiner_error -> Pp.t val explain_pattern_matching_error : env -> Evd.evar_map -> pattern_matching_error -> Pp.t diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 90168843a..e4ca98749 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -21,6 +21,7 @@ open Names open Declarations open Entries open Term +open Constr open Inductive open Decl_kinds open Indrec @@ -108,10 +109,10 @@ let _ = let define id internal ctx c t = let f = declare_constant ~internal in - let _, univs = Evd.universe_context ~names:[] ~extensible:true ctx in let univs = - if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs - else Monomorphic_const_entry univs + if Flags.is_universe_polymorphism () + then Polymorphic_const_entry (Evd.to_universe_context ctx) + else Monomorphic_const_entry (Evd.universe_context_set ctx) in let kn = f id (DefinitionEntry @@ -407,7 +408,7 @@ let do_mutual_induction_scheme lnamedepindsort = let get_common_underlying_mutual_inductive = function | [] -> assert false | (id,(mind,i as ind))::l as all -> - match List.filter (fun (_,(mind',_)) -> not (eq_mind mind mind')) l with + match List.filter (fun (_,(mind',_)) -> not (MutInd.equal mind mind')) l with | (_,ind')::_ -> raise (RecursionSchemeError (NotMutualInScheme (ind,ind'))) | [] -> @@ -458,7 +459,7 @@ let build_combined_scheme env schemes = let find_inductive ty = let (ctx, arity) = decompose_prod ty in let (_, last) = List.hd ctx in - match kind_of_term last with + match Constr.kind last with | App (ind, args) -> let ind = destInd ind in let (_,spec) = Inductive.lookup_mind_specif env (fst ind) in diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli index 91c4c5825..4b31389ab 100644 --- a/vernac/indschemes.mli +++ b/vernac/indschemes.mli @@ -8,7 +8,7 @@ open Loc open Names -open Term +open Constr open Environ open Vernacexpr @@ -16,9 +16,9 @@ open Vernacexpr (** Build and register the boolean equalities associated to an inductive type *) -val declare_beq_scheme : mutual_inductive -> unit +val declare_beq_scheme : MutInd.t -> unit -val declare_eq_decidability : mutual_inductive -> unit +val declare_eq_decidability : MutInd.t -> unit (** Build and register a congruence scheme for an equality-like inductive type *) @@ -39,10 +39,10 @@ val do_scheme : (Id.t located option * scheme) list -> unit (** Combine a list of schemes into a conjunction of them *) -val build_combined_scheme : env -> constant list -> Evd.evar_map * constr * types +val build_combined_scheme : env -> Constant.t list -> Evd.evar_map * constr * types val do_combined_scheme : Id.t located -> Id.t located list -> unit (** Hook called at each inductive type definition *) -val declare_default_schemes : mutual_inductive -> unit +val declare_default_schemes : MutInd.t -> unit diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index dbf7fec66..200c2260e 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -14,6 +14,7 @@ open Util open Pp open Names open Term +open Constr open Declarations open Declareops open Entries @@ -48,7 +49,8 @@ let retrieve_first_recthm uctx = function (NamedDecl.get_value (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in - let (_, uctx) = UState.universe_context ~names:[] ~extensible:true uctx in + (* we get the right order somehow but surely it could be enforced in a better way *) + let uctx = UState.context uctx in let inst = Univ.UContext.instance uctx in let map (c, ctx) = Vars.subst_instance_constr inst c in (Option.map map (Global.body_of_constant_body cb), is_opaque cb) @@ -62,7 +64,7 @@ let adjust_guardness_conditions const = function { const with const_entry_body = Future.chain const.const_entry_body (fun ((body, ctx), eff) -> - match kind_of_term body with + match Constr.kind body with | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> (* let possible_indexes = List.map2 (fun i c -> match i with Some i -> i | None -> @@ -97,7 +99,7 @@ let find_mutually_recursive_statements thms = let ind_hyps = List.flatten (List.map_i (fun i decl -> let t = RelDecl.get_type decl in - match kind_of_term t with + match Constr.kind t with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in mind.mind_finite <> Decl_kinds.CoFinite -> @@ -107,7 +109,7 @@ let find_mutually_recursive_statements thms = 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 kind_of_term (EConstr.Unsafe.to_constr whnf_ccl) with + match Constr.kind (EConstr.Unsafe.to_constr 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 -> @@ -116,7 +118,7 @@ let find_mutually_recursive_statements thms = [] in ind_hyps,ind_ccl) thms in let inds_hyps,ind_ccls = List.split inds in - let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> eq_mind kn kn' in + let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> MutInd.equal kn kn' in (* Check if all conclusions are coinductive in the same type *) (* (degenerated cartesian product since there is at most one coind ccl) *) let same_indccl = @@ -175,7 +177,7 @@ let look_for_possibly_mutual_statements = function (* 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 @@ -202,7 +204,7 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook = (locality, ConstRef kn) in definition_message id; - Option.iter (Universes.register_universe_binders r) 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 @@ -216,13 +218,13 @@ let compute_proof_name locality = function if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || locality == Global && Nametab.exists_cci (Lib.make_path_except_section id) then - user_err ?loc (pr_id id ++ str " already exists."); + user_err ?loc (Id.print id ++ str " already exists."); id | None -> let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in next_global_ident_away default_thm_id avoid -let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t_i,(_,imps))) = +let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,imps))) = let t_i = norm t_i in match body with | None -> @@ -230,7 +232,13 @@ let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t | Discharge -> let impl = false in (* copy values from Vernacentries *) let k = IsAssumption Conjectural in - let c = SectionLocalAssum ((t_i,Univ.ContextSet.of_context ctx),p,impl) in + let univs = match univs with + | Polymorphic_const_entry univs -> + (* What is going on here? *) + Univ.ContextSet.of_context univs + | Monomorphic_const_entry univs -> univs + in + let c = SectionLocalAssum ((t_i, univs),p,impl) in let _ = declare_variable id (Lib.cwd(),c,k) in (Discharge, VarRef id,imps) | Local | Global -> @@ -240,24 +248,25 @@ let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t | Global -> false | Discharge -> assert false in - let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in + let decl = (ParameterEntry (None,(t_i,univs),None), k) in let kn = declare_constant id ~local decl in (locality,ConstRef kn,imps)) | Some body -> let body = norm body in let k = Kindops.logical_kind_of_goal_kind kind in - let rec body_i t = match kind_of_term t with + let rec body_i t = match Constr.kind t with | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) | CoFix (0,decls) -> mkCoFix (i,decls) | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2) | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t) | App (t, args) -> mkApp (body_i t, args) - | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body ++ str ".") in + | _ -> + let sigma, env = Pfedit.get_current_context () in + anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in let body_i = body_i body in match locality with | Discharge -> - let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p - ~univs:ctx body_i in + let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in let c = SectionLocalDef const in let _ = declare_variable id (Lib.cwd(), c, k) in (Discharge,VarRef id,imps) @@ -268,7 +277,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t | Discharge -> assert false in let const = - Declare.definition_entry ~types:t_i ~poly:p ~univs:ctx ~opaque:opaq body_i + Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in let kn = declare_constant id ~local (DefinitionEntry const, k) in (locality,ConstRef kn,imps) @@ -277,23 +286,23 @@ 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 *) let warn_let_as_axiom = CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" - (fun id -> strbrk "Let definition" ++ spc () ++ pr_id id ++ + (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++ spc () ++ strbrk "declared as an axiom.") let admit (id,k,e) pl hook () = @@ -303,7 +312,7 @@ let admit (id,k,e) pl hook () = | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id in let () = assumption_message id in - Option.iter (Universes.register_universe_binders (ConstRef kn)) pl; + Declare.declare_univ_binders (ConstRef kn) pl; call_hook (fun exn -> exn) hook Global (ConstRef kn) (* Starting a goal *) @@ -321,8 +330,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 @@ -330,7 +339,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 @@ -408,7 +417,7 @@ 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 = @@ -417,9 +426,9 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook = 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 binders, ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in - let body = Option.map norm body in - List.map_i (save_remaining_recthms kind norm ctx binders body opaq) 1 other_thms in + let body = Option.map norm 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; @@ -450,9 +459,9 @@ let start_proof_com ?inference_hook kind thms hook = let evd, nf = Evarutil.nf_evars_and_universes !evdref in let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in let () = - if not decl.Misctypes.univdecl_extensible_instance then - ignore (Evd.universe_context evd ~names:decl.Misctypes.univdecl_instance ~extensible:false) - else () + let open Misctypes in + if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then + ignore (Evd.check_univ_decl ~poly:(pi2 kind) evd decl) in let evd = if pi2 kind then evd @@ -487,9 +496,9 @@ 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 = Evd.evar_context_universe_context (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, pi2 k, (typ, ctx), None), universes) + Admitted(id, k, (sec_vars, (typ, ctx), None), universes) | None -> let pftree = Proof_global.give_me_the_proof () in let id, k, typ = Pfedit.current_proof_statement () in @@ -509,12 +518,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 binders, ctx = Evd.check_univ_decl evd decl in let poly = pi2 k in - let binders = if poly then Some binders else None in - Admitted(id,k,(sec_vars, poly, (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) -> @@ -529,7 +535,5 @@ let save_proof ?proof = function Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj))) (* Miscellaneous *) +let get_current_context () = Pfedit.get_current_context () -let get_current_context () = - Pfedit.get_current_context () - diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 1e23c7314..a4854b4a6 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Decl_kinds type 'a declaration_hook @@ -27,10 +27,10 @@ val start_proof : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_m unit declaration_hook -> unit val start_proof_univs : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> - ?terminator:(Proof_global.lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) -> + ?terminator:(Proof_global.lemma_possible_guards -> (UState.t option -> unit declaration_hook) -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> - (Evd.evar_universe_context option -> unit declaration_hook) -> unit + (UState.t option -> unit declaration_hook) -> unit val start_proof_com : ?inference_hook:Pretyping.inference_hook -> @@ -46,7 +46,7 @@ val start_proof_with_initialization : val universe_proof_terminator : Proof_global.lemma_possible_guards -> - (Evd.evar_universe_context option -> unit declaration_hook) -> + (UState.t option -> unit declaration_hook) -> Proof_global.proof_terminator val standard_proof_terminator : @@ -56,7 +56,7 @@ val standard_proof_terminator : (** {6 ... } *) (** A hook the next three functions pass to cook_proof *) -val set_save_hook : (Proof.proof -> unit) -> unit +val set_save_hook : (Proof.t -> unit) -> unit val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit @@ -66,3 +66,4 @@ val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> uni and the current global env *) val get_current_context : unit -> Evd.evar_map * Environ.env +[@@ocaml.deprecated "please use [Pfedit.get_current_context]"] diff --git a/vernac/locality.ml b/vernac/locality.ml index 054a451a4..87b411625 100644 --- a/vernac/locality.ml +++ b/vernac/locality.ml @@ -6,46 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp +open Decl_kinds (** * Managing locality *) let local_of_bool = function - | true -> Decl_kinds.Local - | false -> Decl_kinds.Global - -let check_locality locality_flag = - match locality_flag with - | Some b -> - let s = if b then "Local" else "Global" in - CErrors.user_err ~hdr:"Locality.check_locality" - (str "This command does not support the \"" ++ str s ++ str "\" prefix.") - | None -> () - -(** Extracting the locality flag *) - -(* Commands which supported an inlined Local flag *) - -let warn_deprecated_local_syntax = - CWarnings.create ~name:"deprecated-local-syntax" ~category:"deprecated" - (fun () -> - Pp.strbrk "Deprecated syntax: use \"Local\" as a prefix.") - -let enforce_locality_full locality_flag local = - let local = - match locality_flag with - | Some false when local -> - CErrors.user_err Pp.(str "Cannot be simultaneously Local and Global.") - | Some true when local -> - CErrors.user_err Pp.(str "Use only prefix \"Local\".") - | None -> - if local then begin - warn_deprecated_local_syntax (); - Some true - end else - None - | Some b -> Some b in - local + | true -> Local + | false -> Global + (** Positioning locality for commands supporting discharging and export outside of modules *) @@ -58,15 +26,16 @@ let make_non_locality = function Some false -> false | _ -> true let make_locality = function Some true -> true | _ -> false -let enforce_locality locality_flag local = - make_locality (enforce_locality_full locality_flag local) +let enforce_locality_exp locality_flag discharge = + match locality_flag, discharge with + | Some b, NoDischarge -> local_of_bool b + | None, NoDischarge -> Global + | None, DoDischarge -> Discharge + | Some true, DoDischarge -> CErrors.user_err Pp.(str "Local not allowed in this case") + | Some false, DoDischarge -> CErrors.user_err Pp.(str "Global not allowed in this case") -let enforce_locality_exp locality_flag local = - match locality_flag, local with - | None, Some local -> local - | Some b, None -> local_of_bool b - | None, None -> Decl_kinds.Global - | Some _, Some _ -> CErrors.user_err Pp.(str "Local non allowed in this case") +let enforce_locality locality_flag = + make_locality locality_flag (* For commands whose default is to not discharge but to export: Global in sections forces discharge, Global not in section is the default; @@ -75,8 +44,8 @@ let enforce_locality_exp locality_flag local = let make_section_locality = function Some b -> b | None -> Lib.sections_are_opened () -let enforce_section_locality locality_flag local = - make_section_locality (enforce_locality_full locality_flag local) +let enforce_section_locality locality_flag = + make_section_locality locality_flag (** Positioning locality for commands supporting export but not discharge *) @@ -93,15 +62,5 @@ let make_module_locality = function | Some true -> true | None -> false -let enforce_module_locality locality_flag local = - make_module_locality (enforce_locality_full locality_flag local) - -module LocalityFixme = struct - let locality = ref None - let set l = locality := l - let consume () = - let l = !locality in - locality := None; - l - let assert_consumed () = check_locality !locality -end +let enforce_module_locality locality_flag = + make_module_locality locality_flag diff --git a/vernac/locality.mli b/vernac/locality.mli index c1c45d6b0..922538b23 100644 --- a/vernac/locality.mli +++ b/vernac/locality.mli @@ -8,10 +8,6 @@ (** * Managing locality *) -(** Commands which supported an inlined Local flag *) - -val enforce_locality_full : bool option -> bool -> bool option - (** * Positioning locality for commands supporting discharging and export outside of modules *) @@ -22,16 +18,15 @@ val enforce_locality_full : bool option -> bool -> bool option val make_locality : bool option -> bool val make_non_locality : bool option -> bool -val enforce_locality : bool option -> bool -> bool -val enforce_locality_exp : - bool option -> Decl_kinds.locality option -> Decl_kinds.locality +val enforce_locality_exp : bool option -> Decl_kinds.discharge -> Decl_kinds.locality +val enforce_locality : bool option -> bool (** For commands whose default is to not discharge but to export: Global in sections forces discharge, Global not in section is the default; Local in sections is the default, Local not in section forces non-export *) val make_section_locality : bool option -> bool -val enforce_section_locality : bool option -> bool -> bool +val enforce_section_locality : bool option -> bool (** * Positioning locality for commands supporting export but not discharge *) @@ -40,12 +35,4 @@ val enforce_section_locality : bool option -> bool -> bool Local in sections is the default, Local not in section forces non-export *) val make_module_locality : bool option -> bool -val enforce_module_locality : bool option -> bool -> bool - -(* This is the old imperative interface that is still used for - * VernacExtend vernaculars. Time permitting this could be trashed too *) -module LocalityFixme : sig - val set : bool option -> unit - val consume : unit -> bool option - val assert_consumed : unit -> unit -end +val enforce_module_locality : bool option -> bool diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 9376afa8c..6c3dfec7d 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -310,7 +310,7 @@ let rec get_notation_vars onlyprint = function (* don't check for nonlinearity if printing only, see Bug 5526 *) if not onlyprint && Id.List.mem id vars then user_err ~hdr:"Metasyntax.get_notation_vars" - (str "Variable " ++ pr_id id ++ str " occurs more than once.") + (str "Variable " ++ Id.print id ++ str " occurs more than once.") else id::vars | (Terminal _ | Break _) :: sl -> get_notation_vars onlyprint sl | SProdList _ :: _ -> assert false @@ -323,7 +323,7 @@ let analyze_notation_tokens ~onlyprint l = let error_not_same_scope x y = user_err ~hdr:"Metasyntax.error_not_name_scope" - (str "Variables " ++ pr_id x ++ str " and " ++ pr_id y ++ str " must be in the same scope.") + (str "Variables " ++ Id.print x ++ str " and " ++ Id.print y ++ str " must be in the same scope.") (**********************************************************************) (* Build pretty-printing rules *) @@ -398,7 +398,7 @@ let check_open_binder isopen sl m = | _ -> assert false in if isopen && not (List.is_empty sl) then - user_err (str "as " ++ pr_id m ++ + user_err (str "as " ++ Id.print m ++ str " is a non-closed binder, no such \"" ++ prlist_with_sep spc pr_token sl ++ strbrk "\" is allowed to occur.") @@ -865,7 +865,7 @@ let check_useless_entry_types recvars mainvars etyps = let vars = let (l1,l2) = List.split recvars in l1@l2@mainvars in match List.filter (fun (x,etyp) -> not (List.mem x vars)) etyps with | (x,_)::_ -> user_err ~hdr:"Metasyntax.check_useless_entry_types" - (pr_id x ++ str " is unbound in the notation.") + (Id.print x ++ str " is unbound in the notation.") | _ -> () let check_binder_type recvars etyps = @@ -922,7 +922,7 @@ let join_auxiliary_recursive_types recvars etyps = | Some xtyp, Some ytyp when Pervasives.(=) xtyp ytyp -> typs (* FIXME *) | Some xtyp, Some ytyp -> user_err - (strbrk "In " ++ pr_id x ++ str " .. " ++ pr_id y ++ + (strbrk "In " ++ Id.print x ++ str " .. " ++ Id.print y ++ strbrk ", both ends have incompatible types.")) recvars etyps 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 785c842ba..181068089 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -13,6 +13,7 @@ open Declare *) open Term +open Constr open Vars open Names open Evd @@ -55,7 +56,7 @@ let subst_evar_constr evs n idf t = let seen = ref Int.Set.empty in let transparent = ref Id.Set.empty in let evar_info id = List.assoc_f Evar.equal id evs in - let rec substrec (depth, fixrels) c = match kind_of_term c with + let rec substrec (depth, fixrels) c = match Constr.kind c with | Evar (k, args) -> let { ev_name = (id, idstr) ; ev_hyps = hyps ; ev_chop = chop } = @@ -85,15 +86,15 @@ let subst_evar_constr evs n idf t = in aux hyps args [] in if List.exists - (fun x -> match kind_of_term x with + (fun x -> match Constr.kind x with | Rel n -> Int.List.mem n fixrels | _ -> false) args then transparent := Id.Set.add idstr !transparent; mkApp (idf idstr, Array.of_list args) | Fix _ -> - map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c - | _ -> map_constr_with_binders succfix substrec (depth, fixrels) c + Constr.map_with_binders succfix substrec (depth, 1 :: fixrels) c + | _ -> Constr.map_with_binders succfix substrec (depth, fixrels) c in let t' = substrec (0, []) t in t', !seen, !transparent @@ -103,9 +104,9 @@ let subst_evar_constr evs n idf t = where n binders were passed through. *) let subst_vars acc n t = let var_index id = Util.List.index Id.equal id acc in - let rec substrec depth c = match kind_of_term c with + let rec substrec depth c = match Constr.kind c with | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c) - | _ -> map_constr_with_binders succ substrec depth c + | _ -> Constr.map_with_binders succ substrec depth c in substrec 0 t @@ -144,7 +145,7 @@ let rec chop_product n t = let pop t = Vars.lift (-1) t in if Int.equal n 0 then Some t else - match kind_of_term t with + match Constr.kind t with | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (pop b) else None | _ -> None @@ -154,7 +155,7 @@ let evar_dependencies evm oev = let evi = Evd.find evm ev in let deps' = evars_of_filtered_evar_info evi in if Evar.Set.mem oev deps' then - invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ string_of_existential oev) + invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ Pp.string_of_ppcmds @@ Evar.print oev) else Evar.Set.union deps' s) deps deps in @@ -163,7 +164,7 @@ let evar_dependencies evm oev = if Evar.Set.equal deps deps' then deps else aux deps' in aux (Evar.Set.singleton oev) - + let move_after (id, ev, deps as obl) l = let rec aux restdeps = function | (id', _, _) as obl' :: tl -> @@ -273,7 +274,7 @@ let explain_no_obligations = function | None -> str "No obligations remaining" type obligation_info = - (Names.Id.t * Term.types * Evar_kinds.t Loc.located * + (Names.Id.t * types * Evar_kinds.t Loc.located * (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array @@ -303,7 +304,7 @@ type program_info_aux = { prg_name: Id.t; prg_body: constr; prg_type: constr; - prg_ctx: Evd.evar_universe_context; + prg_ctx: UState.t; prg_univdecl: Univdecls.universe_decl; prg_obligations: obligations; prg_deps : Id.t list; @@ -312,7 +313,7 @@ type program_info_aux = { prg_notations : notations ; prg_kind : definition_kind; prg_reduce : constr -> constr; - prg_hook : (Evd.evar_universe_context -> unit) Lemmas.declaration_hook; + prg_hook : (UState.t -> unit) Lemmas.declaration_hook; prg_opaque : bool; prg_sign: named_context_val; } @@ -384,7 +385,7 @@ let subst_deps expand obls deps t = (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t) let rec prod_app t n = - match kind_of_term (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (** FIXME *) with + match Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (** FIXME *) with | Prod (_,_,b) -> subst1 n b | LetIn (_, b, t, b') -> prod_app (subst1 b b') n | _ -> @@ -400,13 +401,13 @@ let replace_appvars subst = let f, l = decompose_app c in if isVar f then try - let c' = List.map (map_constr aux) l in + let c' = List.map (Constr.map aux) l in let (t, b) = Id.List.assoc (destVar f) subst in mkApp (delayed_force hide_obligation, [| prod_applist t c'; applistc b c' |]) - with Not_found -> map_constr aux c - else map_constr aux c - in map_constr aux + with Not_found -> Constr.map aux c + else Constr.map aux c + in Constr.map aux let subst_prog expand obls ints prg = let subst = obl_substitution expand obls ints in @@ -428,15 +429,15 @@ 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 let keys = map_keys !from_prg in user_err ~hdr:"Program" (str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++ - prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++ + prlist_with_sep spc (fun x -> Id.print x) keys ++ (str (if Int.equal (List.length keys) 1 then " has " else " have ") ++ str "unsolved obligations")) @@ -474,23 +475,23 @@ let declare_definition prg = (Evd.evar_universe_context_subst prg.prg_ctx) in let opaque = prg.prg_opaque in let fix_exn = Hook.get get_fix_exn () in - let pl, ctx = Evd.check_univ_decl (Evd.from_ctx prg.prg_ctx) prg.prg_univdecl in - let ce = - definition_entry ~fix_exn - ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) - ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body) - in + let typ = nf typ in + let body = nf 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 let () = progmap_remove prg in - let cst = - DeclareDef.declare_definition prg.prg_name - prg.prg_kind ce [] prg.prg_implicits - (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r)) - in - Universes.register_universe_binders cst pl; - cst + let ubinders = UState.universe_binders uctx in + DeclareDef.declare_definition prg.prg_name + prg.prg_kind ce ubinders prg.prg_implicits + (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r uctx; r)) let rec lam_index n t acc = - match kind_of_term t with + match Constr.kind t with | Lambda (Name n', _, _) when Id.equal n n' -> acc | Lambda (_, _, b) -> @@ -551,9 +552,9 @@ let declare_mutual_definition l = mk_proof (mkCoFix (i,fixdecls))) 0 l in (* Declare the recursive definitions *) - let ctx = Evd.evar_context_universe_context first.prg_ctx in + let univs = UState.const_univ_entry ~poly first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in - let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) [] ctx) + let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders univs) fixnames fixdecls fixtypes fiximps in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; @@ -566,9 +567,9 @@ let declare_mutual_definition l = let decompose_lam_prod c ty = let open Context.Rel.Declaration in let rec aux ctx c ty = - match kind_of_term c, kind_of_term ty with + match Constr.kind c, Constr.kind ty with | LetIn (x, b, t, c), LetIn (x', b', t', ty) - when eq_constr b b' && eq_constr t t' -> + when Constr.equal b b' && Constr.equal t t' -> let ctx' = Context.Rel.add (LocalDef (x,b',t')) ctx in aux ctx' c ty | _, LetIn (x', b', t', ty) -> @@ -635,12 +636,11 @@ let declare_obligation prg obl body ty uctx = shrink_body body ty else [], body, ty, [||] in let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in - let univs = if poly then Polymorphic_const_entry uctx else Monomorphic_const_entry uctx in let ce = { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body; const_entry_secctx = None; const_entry_type = ty; - const_entry_universes = univs; + const_entry_universes = uctx; const_entry_opaque = opaque; const_entry_inline_code = false; const_entry_feedback = None; @@ -649,13 +649,15 @@ let declare_obligation prg obl body ty uctx = let constant = Declare.declare_constant obl.obl_name ~local:true (DefinitionEntry ce,IsProof Property) in - if not opaque then add_hint (Locality.make_section_locality None) prg constant; - definition_message obl.obl_name; - true, { obl with obl_body = - if poly then - Some (DefinedObl (constant, Univ.UContext.instance uctx)) - else - Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) } + if not opaque then add_hint (Locality.make_section_locality None) prg constant; + definition_message obl.obl_name; + let body = match uctx with + | Polymorphic_const_entry uctx -> + Some (DefinedObl (constant, Univ.UContext.instance uctx)) + | Monomorphic_const_entry _ -> + Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) + in + true, { obl with obl_body = body } let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind notations obls impls kind reduce hook = @@ -677,6 +679,7 @@ let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind obl_deps = d; obl_tac = tac }) obls, b in + let ctx = UState.make_flexible_nonalgebraic ctx in { prg_name = n ; prg_body = b; prg_type = reduce t; prg_ctx = ctx; prg_univdecl = udecl; prg_obligations = (obls', Array.length obls'); @@ -715,10 +718,10 @@ let get_prog name = | _ -> let progs = Id.Set.elements (ProgMap.domain prg_infos) in let prog = List.hd progs in - let progs = prlist_with_sep pr_comma Nameops.pr_id progs in + let progs = prlist_with_sep pr_comma Id.print progs in user_err (str "More than one program with unsolved obligations: " ++ progs - ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Nameops.pr_id prog ++ str "\"")) + ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Id.print prog ++ str "\"")) let get_any_prog () = let prg_infos = !from_prg in @@ -828,46 +831,63 @@ let obligation_terminator name num guard hook auto pf = match pf with | Admitted _ -> apply_terminator term pf | Proved (opq, id, proof) -> - if not !shrink_obligations then apply_terminator term pf - else - let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in - let env = Global.env () in - 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.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 *) - let prg = get_info (ProgMap.find name !from_prg) in - let ctx = Evd.evar_universe_context sigma in - let prg = { prg with prg_ctx = ctx } in - let obls, rem = prg.prg_obligations in - let obl = obls.(num) in - let status = - match obl.obl_status, opq with - | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp () - | (true, _), Vernacexpr.Opaque -> err_not_transp () - | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true - | (_, Evar_kinds.Define true), Vernacexpr.Transparent -> Evar_kinds.Define false - | (_, status), Vernacexpr.Transparent -> status - in - let obl = { obl with obl_status = false, status } in - let uctx = Evd.evar_context_universe_context ctx in - let (_, obl) = declare_obligation prg obl body ty uctx in - let obls = Array.copy obls in - let _ = obls.(num) <- obl in - try + let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in + let env = Global.env () in + 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 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 *) + let prg = get_info (ProgMap.find name !from_prg) in + (** Ensure universes are substituted properly in body and type *) + let body = EConstr.to_constr sigma (EConstr.of_constr body) in + let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in + let ctx = Evd.evar_universe_context sigma in + let obls, rem = prg.prg_obligations in + let obl = obls.(num) in + let status = + match obl.obl_status, opq with + | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp () + | (true, _), Vernacexpr.Opaque -> err_not_transp () + | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true + | (_, Evar_kinds.Define true), Vernacexpr.Transparent -> + Evar_kinds.Define false + | (_, status), Vernacexpr.Transparent -> status + in + let obl = { obl with obl_status = false, status } in + let ctx = + if pi2 prg.prg_kind then ctx + else UState.union prg.prg_ctx ctx + in + let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in + let (_, obl) = declare_obligation prg obl body ty uctx in + let obls = Array.copy obls in + let _ = obls.(num) <- obl in + let prg_ctx = + if pi2 (prg.prg_kind) then (* Polymorphic *) + (** We merge the new universes and constraints of the + polymorphic obligation with the existing ones *) + UState.union prg.prg_ctx ctx + else + (** The first obligation declares the univs of the constant, + each subsequent obligation declares its own additional + universes and constraints if any *) + UState.make (Global.universes ()) + in + let prg = { prg with prg_ctx } in + try ignore (update_obls prg obls (pred rem)); if pred rem > 0 then begin - let deps = dependencies obls num in - if not (Int.Set.is_empty deps) then - ignore (auto (Some name) None deps) - end - with e when CErrors.noncritical e -> - let e = CErrors.push e in - pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) + let deps = dependencies obls num in + if not (Int.Set.is_empty deps) then + ignore (auto (Some name) None deps) + end + with e when CErrors.noncritical e -> + let e = CErrors.push e in + pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) let obligation_hook prg obl num auto ctx' _ gr = let obls, rem = prg.prg_obligations in @@ -888,7 +908,8 @@ in let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in Univ.Instance.empty, Evd.evar_universe_context ctx' else - let (_, uctx) = UState.universe_context ~names:[] ~extensible:true ctx' in + (* We get the right order somehow, but surely it could be enforced in a clearer way. *) + let uctx = UState.context ctx' in Univ.UContext.instance uctx, ctx' in let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in @@ -964,13 +985,16 @@ and solve_obligation_by_tac prg obls i tac = let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in let t, ty, ctx = - solve_by_tac obl.obl_name (evar_of_obligation obl) tac - (pi2 prg.prg_kind) (Evd.evar_universe_context evd) - in - let uctx = Evd.evar_context_universe_context ctx in - let prg = {prg with prg_ctx = ctx} in - let def, obl' = declare_obligation prg obl t ty uctx in - obls.(i) <- obl'; + solve_by_tac obl.obl_name (evar_of_obligation obl) tac + (pi2 prg.prg_kind) (Evd.evar_universe_context evd) + in + let uctx = if pi2 prg.prg_kind + then Polymorphic_const_entry (UState.context ctx) + else Monomorphic_const_entry (UState.context_set ctx) + in + let prg = {prg with prg_ctx = ctx} in + let def, obl' = declare_obligation prg obl t ty uctx in + obls.(i) <- obl'; if def && not (pi2 prg.prg_kind) then ( (* Declare the term constraints with the first obligation only *) let evd = Evd.from_env (Global.env ()) in @@ -1118,9 +1142,9 @@ let admit_prog prg = match x.obl_body with | None -> let x = subst_deps_obl obls x in - let ctx = Evd.evar_context_universe_context prg.prg_ctx in + let ctx = Monomorphic_const_entry (UState.context_set prg.prg_ctx) in let kn = Declare.declare_constant x.obl_name ~local:true - (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural) + (ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural) in assumption_message x.obl_name; obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) } diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 11c2553ae..bdc97d48c 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -7,7 +7,7 @@ (************************************************************************) open Environ -open Term +open Constr open Evd open Names open Globnames @@ -32,14 +32,14 @@ val eterm_obligations : env -> Id.t -> evar_map -> int -> (* Existential key, obl. name, type as product, location of the original evar, associated tactic, status and dependencies as indexes into the array *) - * ((existential_key * Id.t) list * ((Id.t -> constr) -> constr -> constr)) * + * ((Evar.t * Id.t) list * ((Id.t -> constr) -> constr -> constr)) * constr * types (* Translations from existential identifiers to obligation identifiers and for terms with existentials to closed terms, given a translation from obligation identifiers to constrs, new term, new type *) type obligation_info = - (Id.t * Term.types * Evar_kinds.t Loc.located * + (Id.t * types * Evar_kinds.t Loc.located * (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array (* ident, type, location, (opaque or transparent, expand or define), dependencies, tactic to solve it *) @@ -51,14 +51,14 @@ type progress = (* Resolution status of a program *) val default_tactic : unit Proofview.tactic ref -val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types -> - Evd.evar_universe_context -> +val add_definition : Names.Id.t -> ?term:constr -> types -> + UState.t -> ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *) ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list -> ?kind:Decl_kinds.definition_kind -> ?tactic:unit Proofview.tactic -> - ?reduce:(Term.constr -> Term.constr) -> - ?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress + ?reduce:(constr -> constr) -> + ?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress type notations = (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list @@ -68,14 +68,14 @@ type fixpoint_kind = | IsCoFixpoint val add_mutual_definitions : - (Names.Id.t * Term.constr * Term.types * + (Names.Id.t * constr * types * (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list -> - Evd.evar_universe_context -> + UState.t -> ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *) ?tactic:unit Proofview.tactic -> ?kind:Decl_kinds.definition_kind -> - ?reduce:(Term.constr -> Term.constr) -> - ?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook -> ?opaque:bool -> + ?reduce:(constr -> constr) -> + ?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool -> notations -> fixpoint_kind -> unit @@ -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 5533fe5b3..1cdc538b5 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -8,11 +8,13 @@ open Pp open CErrors +open Term +open Sorts open Util open Names open Globnames open Nameops -open Term +open Constr open Vars open Environ open Declarations @@ -93,7 +95,7 @@ let binder_of_decl = function let binders_of_decls = List.map binder_of_decl -let typecheck_params_and_fields finite def id pl t ps nots fs = +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 @@ -137,7 +139,7 @@ let typecheck_params_and_fields finite def id pl t ps nots fs = 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 %> out_name) assums 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 = @@ -165,10 +167,11 @@ let typecheck_params_and_fields finite def id pl t ps nots fs = 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 evars decl in + let univs = Evd.check_univ_decl ~poly evars decl in + let ubinders = Evd.universe_binders evars in List.iter (iter_constr ce) (List.rev newps); List.iter (iter_constr ce) (List.rev newfs); - univs, typ, template, imps, newps, impls, newfs + ubinders, univs, typ, template, imps, newps, impls, newfs let degenerate_decl decl = let id = match RelDecl.get_name decl with @@ -193,24 +196,24 @@ let warning_or_error coe indsp err = let st = match err with | MissingProj (fi,projs) -> let s,have = if List.length projs > 1 then "s","were" else "","was" in - (pr_id fi ++ + (Id.print fi ++ strbrk" cannot be defined because the projection" ++ str s ++ spc () ++ - prlist_with_sep pr_comma pr_id projs ++ spc () ++ str have ++ + prlist_with_sep pr_comma Id.print projs ++ spc () ++ str have ++ strbrk " not defined.") | BadTypedProj (fi,ctx,te) -> match te with | ElimArity (_,_,_,_,Some (_,_,NonInformativeToInformative)) -> - (pr_id fi ++ + (Id.print fi ++ strbrk" cannot be defined because it is informative and " ++ Printer.pr_inductive (Global.env()) indsp ++ strbrk " is not.") | ElimArity (_,_,_,_,Some (_,_,StrongEliminationOnNonSmallType)) -> - (pr_id fi ++ + (Id.print fi ++ strbrk" cannot be defined because it is large and " ++ Printer.pr_inductive (Global.env()) indsp ++ strbrk " is not.") | _ -> - (pr_id fi ++ strbrk " cannot be defined because it is not typable.") + (Id.print fi ++ strbrk " cannot be defined because it is not typable.") in if coe then user_err ~hdr:"structure" st; warn_cannot_define_projection (hov 0 st) @@ -229,7 +232,7 @@ exception NotDefinable of record_error let subst_projection fid l c = let lv = List.length l in let bad_projs = ref [] in - let rec substrec depth c = match kind_of_term c with + let rec substrec depth c = match Constr.kind c with | Rel k -> (* We are in context [[params;fields;x:ind;...depth...]] *) if k <= depth+1 then @@ -239,12 +242,12 @@ let subst_projection fid l c = | Projection t -> lift depth t | NoProjection (Name id) -> bad_projs := id :: !bad_projs; mkRel k | NoProjection Anonymous -> - user_err (str "Field " ++ pr_id fid ++ + user_err (str "Field " ++ Id.print fid ++ str " depends on the " ++ pr_nth (k-depth-1) ++ str " field which has no name.") else mkRel (k-lv) - | _ -> map_constr_with_binders succ substrec depth c + | _ -> Constr.map_with_binders succ substrec depth c in let c' = lift 1 c in (* to get [c] defined in ctxt [[params;fields;x:ind]] *) let c'' = substrec 0 c' in @@ -263,12 +266,14 @@ let warn_non_primitive_record = strbrk" could not be defined as a primitive record"))) (* We build projections *) -let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields = +let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers ubinders fieldimpls fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in let poly = Declareops.inductive_is_polymorphic mib in - let ctx = Univ.AUContext.repr (Declareops.inductive_polymorphic_context mib) in - let u = Univ.UContext.instance ctx in + let u = match ctx with + | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx + | Monomorphic_const_entry ctx -> Univ.Instance.empty + in let paramdecls = Inductive.inductive_paramdecls (mib, u) in let indu = indsp, u in let r = mkIndU (indsp,u) in @@ -302,9 +307,11 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field let kn, term = if is_local_assum decl && primitive then (** Already defined in the kernel silently *) - let kn = destConstRef (Nametab.locate (Libnames.qualid_of_ident fid)) in - Declare.definition_message fid; - kn, mkProj (Projection.make kn false,mkRel 1) + let gr = Nametab.locate (Libnames.qualid_of_ident fid) in + let kn = destConstRef gr in + Declare.definition_message fid; + Universes.register_universe_binders gr ubinders; + kn, mkProj (Projection.make kn false,mkRel 1) else let ccl = subst_projection fid subst ti in let body = match decl with @@ -323,16 +330,12 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in try - let univs = - if poly then Polymorphic_const_entry ctx - else Monomorphic_const_entry ctx - in let entry = { const_entry_body = Future.from_val (Safe_typing.mk_pure_proof proj); const_entry_secctx = None; const_entry_type = Some projtyp; - const_entry_universes = univs; + const_entry_universes = ctx; const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None } in @@ -341,8 +344,9 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field let constr_fip = let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in applist (mkConstU (kn,u),proj_args) - in - Declare.definition_message fid; + in + Declare.definition_message fid; + Universes.register_universe_binders (ConstRef kn) ubinders; kn, constr_fip with Type_errors.TypeError (ctx,te) -> raise (NotDefinable (BadTypedProj (fid,ctx,te))) @@ -380,17 +384,20 @@ let structure_signature ctx = open Typeclasses -let declare_structure finite univs id idbuild paramimpls params arity template +let declare_structure finite ubinders univs id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign = let nparams = List.length params and nfields = List.length fields in let args = Context.Rel.to_extended_list mkRel nfields params in let ind = applist (mkRel (1+nparams+nfields), args) in let type_constructor = it_mkProd_or_LetIn ind fields in - let poly, ctx = + let template, ctx = match univs with - | Monomorphic_ind_entry ctx -> false, ctx - | Polymorphic_ind_entry ctx -> true, ctx - | Cumulative_ind_entry cumi -> true, (Univ.CumulativityInfo.univ_context cumi) + | Monomorphic_ind_entry ctx -> + template, Monomorphic_const_entry Univ.ContextSet.empty + | Polymorphic_ind_entry ctx -> + false, Polymorphic_const_entry ctx + | Cumulative_ind_entry cumi -> + false, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi) in let binder_name = match name with @@ -400,7 +407,7 @@ let declare_structure finite univs id idbuild paramimpls params arity template let mie_ind = { mind_entry_typename = id; mind_entry_arity = arity; - mind_entry_template = not poly && template; + mind_entry_template = template; mind_entry_consnames = [idbuild]; mind_entry_lc = [type_constructor] } in @@ -414,27 +421,21 @@ let declare_structure finite univs id idbuild paramimpls params arity template } in let mie = - if poly then - begin + match ctx with + | Polymorphic_const_entry ctx -> let env = Global.env () in let env' = Environ.push_context ctx env in let evd = Evd.from_env env' in Inductiveops.infer_inductive_subtyping env' evd mie - end - else + | Monomorphic_const_entry _ -> mie in - let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in + let kn = Command.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 fields = - if poly then - let subst, _ = Univ.abstract_universes ctx in - Context.Rel.map (fun c -> Vars.subst_univs_level_constr subst c) fields - else fields - in - let kinds,sp_projs = declare_projections rsp ~kind binder_name coers fieldimpls fields in + let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name coers ubinders fieldimpls fields in let build = ConstructRef cstr in + let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs); rsp @@ -448,7 +449,7 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) -let declare_class finite def cum poly ctx id idbuild paramimpls params arity +let declare_class finite def cum ubinders univs id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) @@ -463,27 +464,29 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity let class_body = it_mkLambda_or_LetIn field params in let class_type = it_mkProd_or_LetIn arity params in let class_entry = - Declare.definition_entry ~types:class_type ~poly ~univs:ctx class_body in + Declare.definition_entry ~types:class_type ~univs class_body in let cst = Declare.declare_constant (snd id) (DefinitionEntry class_entry, IsDefinition Definition) in - let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in + let cstu = (cst, match univs with + | Polymorphic_const_entry univs -> Univ.UContext.instance univs + | Monomorphic_const_entry _ -> Univ.Instance.empty) + in let inst_type = appvectc (mkConstU cstu) (Termops.rel_vect 0 (List.length params)) in let proj_type = it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in let proj_body = it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in - let proj_entry = - Declare.definition_entry ~types:proj_type ~poly - ~univs:(if poly then ctx else Univ.UContext.empty) proj_body - in + let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in let proj_cst = Declare.declare_constant proj_name (DefinitionEntry proj_entry, IsDefinition Definition) in let cref = ConstRef cst in Impargs.declare_manual_implicits false cref [paramimpls]; + Universes.register_universe_binders cref ubinders; Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; + Universes.register_universe_binders (ConstRef proj_cst) ubinders; Classes.set_typeclass_transparency (EvalConstRef cst) false false; let sub = match List.hd coers with | Some b -> Some ((if b then Backward else Forward), List.hd priorities) @@ -492,15 +495,16 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity cref, [Name proj_name, sub, Some proj_cst] | _ -> let univs = - if poly then + match univs with + | Polymorphic_const_entry univs -> if cum then - Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx) + Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) else - Polymorphic_ind_entry ctx - else - Monomorphic_ind_entry ctx + Polymorphic_ind_entry univs + | Monomorphic_const_entry univs -> + Monomorphic_ind_entry univs in - let ind = declare_structure BiFinite univs (snd id) idbuild paramimpls + let ind = declare_structure BiFinite ubinders univs (snd id) idbuild paramimpls params arity template fieldimpls fields ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign in @@ -521,13 +525,15 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity params, params in let univs, ctx_context, fields = - if poly then - let usubst, auctx = Univ.abstract_universes ctx in + match univs with + | Polymorphic_const_entry univs -> + let usubst, auctx = Univ.abstract_universes univs in let map c = Vars.subst_univs_level_constr usubst c in let fields = Context.Rel.map map fields in let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in auctx, ctx_context, fields - else Univ.AUContext.empty, ctx_context, fields + | Monomorphic_const_entry _ -> + Univ.AUContext.empty, ctx_context, fields in let k = { cl_univs = univs; @@ -603,14 +609,14 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then user_err Pp.(str "Priorities only allowed for type class substructures"); (* Now, younger decl in params and fields is on top *) - let (pl, ctx), arity, template, implpars, params, implfs, fields = + let pl, univs, arity, template, implpars, params, implfs, fields = States.with_state_protection (fun () -> - typecheck_params_and_fields finite (kind = Class true) idstruc pl s ps notations fs) () in + typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in let sign = structure_signature (fields@params) in 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 poly ctx (loc,idstruc) idbuild + let gr = declare_class finite def cum pl univs (loc,idstruc) idbuild implpars params arity template implfs fields is_coe coers priorities sign in gr | _ -> @@ -619,18 +625,19 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf (succ (List.length params)) impls) implfs in let univs = - if poly then + match univs with + | Polymorphic_const_entry univs -> if cum then - Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx) + Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) else - Polymorphic_ind_entry ctx - else - Monomorphic_ind_entry ctx + Polymorphic_ind_entry univs + | Monomorphic_const_entry univs -> + Monomorphic_ind_entry univs in - let ind = declare_structure finite univs idstruc + let ind = declare_structure finite pl univs idstruc idbuild implpars params arity template implfs fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in IndRef ind in - Universes.register_universe_binders gr pl; + Declare.declare_univ_binders gr pl; gr diff --git a/vernac/record.mli b/vernac/record.mli index aea474581..e632e7bbf 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -7,39 +7,15 @@ (************************************************************************) open Names -open Term open Vernacexpr open Constrexpr -open Impargs open Globnames val primitive_flag : bool ref -(** [declare_projections ref name coers params fields] declare projections of - record [ref] (if allowed) using the given [name] as argument, and put them - as coercions accordingly to [coers]; it returns the absolute names of projections *) - -val declare_projections : - inductive -> ?kind:Decl_kinds.definition_object_kind -> Id.t -> - coercion_flag list -> manual_explicitation list list -> Context.Rel.t -> - (Name.t * bool) list * constant option list - -val declare_structure : - Decl_kinds.recursivity_kind -> - Entries.inductive_universes -> - Id.t -> Id.t -> - manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *) - bool (** template arity ? *) -> - Impargs.manual_explicitation list list -> Context.Rel.t -> (** fields *) - ?kind:Decl_kinds.definition_object_kind -> ?name:Id.t -> - bool -> (** coercion? *) - bool list -> (** field coercions *) - Evd.evar_map -> - inductive - 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/search.ml b/vernac/search.ml index 0f56f81e7..6da6a0c2d 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -9,7 +9,7 @@ open Pp open Util open Names -open Term +open Constr open Declarations open Libobject open Environ diff --git a/vernac/search.mli b/vernac/search.mli index db54d732b..2eda3980a 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Environ open Pattern open Globnames 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 850902d6b..8673155e2 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -15,6 +15,7 @@ Command Classes Record Assumptions +Vernacstate Vernacinterp Mltop Topfmt diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 41f63644d..161e0c535 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -29,6 +29,7 @@ open Redexpr open Lemmas open Misctypes open Locality +open Vernacinterp module NamedDecl = Context.Named.Declaration @@ -56,20 +57,19 @@ let scope_class_of_qualid qid = let show_proof () = (* spiwack: this would probably be cooler with a bit of polishing. *) let p = Proof_global.give_me_the_proof () in + let sigma, env = Pfedit.get_current_context () in let pprf = Proof.partial_proof p in - Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_econstr pprf) + Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) let show_top_evars () = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) let pfts = Proof_global.give_me_the_proof () in - let gls = Proof.V82.subgoals pfts in - let sigma = gls.Evd.sigma in + let gls,_,_,_,sigma = Proof.proof pfts in Feedback.msg_notice (pr_evars_int sigma 1 (Evd.undefined_map sigma)) let show_universes () = let pfts = Proof_global.give_me_the_proof () in - let gls = Proof.V82.subgoals pfts in - let sigma = gls.Evd.sigma in + let gls,_,_,_,sigma = Proof.proof pfts in let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in Feedback.msg_notice (Termops.pr_evar_universe_context (Evd.evar_universe_context sigma)); Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx) @@ -78,16 +78,16 @@ let show_universes () = let show_intro all = let open EConstr in let pf = Proof_global.give_me_the_proof() in - let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in + let gls,_,_,_,sigma = Proof.proof pf in if not (List.is_empty gls) then begin let gl = {Evd.it=List.hd gls ; sigma = sigma; } in let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in if all then let lid = Tactics.find_intro_names l gl in - Feedback.msg_notice (hov 0 (prlist_with_sep spc pr_id lid)) + Feedback.msg_notice (hov 0 (prlist_with_sep spc Id.print lid)) else if not (List.is_empty l) then let n = List.last l in - Feedback.msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl))) + Feedback.msg_notice (Id.print (List.hd (Tactics.find_intro_names [n] gl))) end (** Prepare a "match" template for a given inductive type. @@ -153,8 +153,8 @@ let show_match id = (* "Print" commands *) let print_path_entry p = - let dir = pr_dirpath (Loadpath.logical p) in - let path = str (Loadpath.physical p) in + let dir = DirPath.print (Loadpath.logical p) in + let path = str (CUnix.escaped_string_of_physical_path (Loadpath.physical p)) in Pp.hov 2 (dir ++ spc () ++ path) let print_loadpath dir = @@ -176,9 +176,9 @@ let print_modules () = let loaded_opened = List.intersect DirPath.equal opened loaded and only_loaded = List.subtract DirPath.equal loaded opened in str"Loaded and imported library files: " ++ - pr_vertical_list pr_dirpath loaded_opened ++ fnl () ++ + pr_vertical_list DirPath.print loaded_opened ++ fnl () ++ str"Loaded and not imported library files: " ++ - pr_vertical_list pr_dirpath only_loaded + pr_vertical_list DirPath.print only_loaded let print_module r = @@ -186,8 +186,8 @@ let print_module r = try let globdir = Nametab.locate_dir qid in match globdir with - DirModule (dirpath,(mp,_)) -> - Feedback.msg_notice (Printmod.print_module (Printmod.printable_body dirpath) mp) + DirModule { obj_dir; obj_mp; _ } -> + Feedback.msg_notice (Printmod.print_module (Printmod.printable_body obj_dir) obj_mp) | _ -> raise Not_found with Not_found -> Feedback.msg_error (str"Unknown Module " ++ pr_qualid qid) @@ -250,14 +250,15 @@ let print_namespace ns = let print_list pr l = prlist_with_sep (fun () -> str".") pr l in let print_kn kn = (* spiwack: I'm ignoring the dirpath, is that bad? *) - let (mp,_,lbl) = Names.repr_kn kn in + let (mp,_,lbl) = Names.KerName.repr kn in let qn = (qualified_minus (List.length ns) mp)@[Names.Label.to_id lbl] in - print_list pr_id qn + print_list Id.print qn in let print_constant k body = (* FIXME: universes *) let t = body.Declarations.const_type in - print_kn k ++ str":" ++ spc() ++ Printer.pr_type t + let sigma, env = Pfedit.get_current_context () in + print_kn k ++ str":" ++ spc() ++ Printer.pr_type_env env sigma t in let matches mp = match match_modulepath ns mp with | Some [] -> true @@ -265,14 +266,14 @@ let print_namespace ns = let constants = (Environ.pre_env (Global.env ())).Pre_env.env_globals.Pre_env.env_constants in let constants_in_namespace = Cmap_env.fold (fun c (body,_) acc -> - let kn = user_con c in - if matches (modpath kn) then + let kn = Constant.user c in + if matches (KerName.modpath kn) then acc++fnl()++hov 2 (print_constant kn body) else acc ) constants (str"") in - Feedback.msg_notice ((print_list pr_id ns)++str":"++fnl()++constants_in_namespace) + Feedback.msg_notice ((print_list Id.print ns)++str":"++fnl()++constants_in_namespace) let print_strategy r = let open Conv_oracle in @@ -361,29 +362,29 @@ let locate_file f = let msg_found_library = function | Library.LibLoaded, fulldir, file -> Feedback.msg_info (hov 0 - (pr_dirpath fulldir ++ strbrk " has been loaded from file " ++ + (DirPath.print fulldir ++ strbrk " has been loaded from file " ++ str file)) | Library.LibInPath, fulldir, file -> Feedback.msg_info (hov 0 - (pr_dirpath fulldir ++ strbrk " is bound to file " ++ str file)) + (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file)) let err_unmapped_library ?loc ?from qid = let dir = fst (repr_qualid qid) in let prefix = match from with | None -> str "." | Some from -> - str " and prefix " ++ pr_dirpath from ++ str "." + str " and prefix " ++ DirPath.print from ++ str "." in user_err ?loc ~hdr:"locate_library" (strbrk "Cannot find a physical path bound to logical path matching suffix " ++ - pr_dirpath dir ++ prefix) + DirPath.print dir ++ prefix) let err_notfound_library ?loc ?from qid = let prefix = match from with | None -> str "." | Some from -> - str " with prefix " ++ pr_dirpath from ++ str "." + str " with prefix " ++ DirPath.print from ++ str "." in user_err ?loc ~hdr:"locate_library" (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) @@ -408,8 +409,8 @@ let dump_global r = (**********) (* Syntax *) -let vernac_syntax_extension locality local infix l = - let local = enforce_module_locality locality local in +let vernac_syntax_extension atts infix l = + let local = enforce_module_locality atts.locality in if infix then Metasyntax.check_infix_modifiers (snd l); Metasyntax.add_syntax_extension local l @@ -420,20 +421,20 @@ let vernac_delimiters sc = function let vernac_bind_scope sc cll = Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll) -let vernac_open_close_scope locality local (b,s) = - let local = enforce_section_locality locality local in +let vernac_open_close_scope ~atts (b,s) = + let local = enforce_section_locality atts.locality in Notation.open_close_scope (local,b,s) -let vernac_arguments_scope locality r scl = - let local = make_section_locality locality in +let vernac_arguments_scope ~atts r scl = + let local = make_section_locality atts.locality in Notation.declare_arguments_scope local (smart_global r) scl -let vernac_infix locality local = - let local = enforce_module_locality locality local in +let vernac_infix ~atts = + let local = enforce_module_locality atts.locality in Metasyntax.add_infix local (Global.env()) -let vernac_notation locality local = - let local = enforce_module_locality locality local in +let vernac_notation ~atts = + let local = enforce_module_locality atts.locality in Metasyntax.add_notation local (Global.env()) (***********) @@ -471,33 +472,33 @@ let vernac_definition_hook p = function | SubClass -> Class.add_subclass_hook p | _ -> no_hook -let vernac_definition locality p (local,k) ((loc,id as lid),pl) def = - let local = enforce_locality_exp locality local in - let hook = vernac_definition_hook p k in +let vernac_definition ~atts discharge kind ((loc,id as lid),pl) def = + let local = enforce_locality_exp atts.locality discharge in + let hook = vernac_definition_hook atts.polymorphic kind in let () = match local with | Discharge -> Dumpglob.dump_definition lid true "var" | Local | Global -> Dumpglob.dump_definition lid false "def" in (match def with | ProveBody (bl,t) -> (* local binders, typ *) - start_proof_and_print (local,p,DefinitionBody k) + start_proof_and_print (local, atts.polymorphic, DefinitionBody kind) [Some (lid,pl), (bl,t)] hook | DefineBody (bl,red_option,c,typ_opt) -> - let red_option = match red_option with + let red_option = match red_option with | None -> None | Some r -> - let (evc,env)= get_current_context () in - Some (snd (Hook.get f_interp_redexp env evc r)) in - do_definition id (local,p,k) pl bl red_option c typ_opt hook) + 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) -let vernac_start_proof locality p kind l = - let local = enforce_locality_exp locality None in +let vernac_start_proof ~atts kind l = + let local = enforce_locality_exp atts.locality NoDischarge in if Dumpglob.dump () then List.iter (fun (id, _) -> match id with | Some (lid,_) -> Dumpglob.dump_definition lid false "prf" | None -> ()) l; - start_proof_and_print (local, p, Proof kind) l no_hook + start_proof_and_print (local, atts.polymorphic, Proof kind) l no_hook let vernac_end_proof ?proof = function | Admitted -> save_proof ?proof Admitted @@ -510,10 +511,10 @@ let vernac_exact_proof c = save_proof (Vernacexpr.(Proved(Opaque,None))); if not status then Feedback.feedback Feedback.AddedAxiom -let vernac_assumption locality poly (local, kind) l nl = - let local = enforce_locality_exp locality local in +let vernac_assumption ~atts discharge kind l nl = + let local = enforce_locality_exp atts.locality discharge in let global = local == Global in - let kind = local, poly, kind in + let kind = local, atts.polymorphic, kind in List.iter (fun (is_coe,(idl,c)) -> if Dumpglob.dump () then List.iter (fun (lid, _) -> @@ -553,8 +554,8 @@ let vernac_record cum k poly finite struc binders sort nameopt cfs = then the type is declared private (as per the [Private] keyword). [finite] indicates whether the type is inductive, co-inductive or neither. *) -let vernac_inductive cum poly lo finite indl = - let is_cumulative = should_treat_as_cumulative cum poly in +let vernac_inductive ~atts cum lo finite indl = + let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in if Dumpglob.dump () then List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) -> match cstrs with @@ -571,13 +572,13 @@ let vernac_inductive cum poly lo finite indl = user_err Pp.(str "The Variant keyword does not support syntax { ... }.") | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] -> vernac_record cum (match b with Class _ -> Class false | _ -> b) - poly finite id bl c oc fs + atts.polymorphic finite id bl c oc fs | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> let f = let (coe, ((loc, id), ce)) = l in let coe' = if coe then Some true else None in (((coe', AssumExpr ((loc, Name id), ce)), None), []) - in vernac_record cum (Class true) poly finite id bl c None [f] + in vernac_record cum (Class true) atts.polymorphic finite id bl c None [f] | [ ( _ , _, _, Class _, Constructors _), [] ] -> user_err Pp.(str "Inductive classes not supported") | [ ( id , bl , c , Class _, _), _ :: _ ] -> @@ -591,19 +592,19 @@ let vernac_inductive cum poly 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 poly lo finite + do_mutual_inductive indl is_cumulative atts.polymorphic lo finite -let vernac_fixpoint locality poly local l = - let local = enforce_locality_exp locality local in +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; - do_fixpoint local poly l + do_fixpoint local atts.polymorphic l -let vernac_cofixpoint locality poly local l = - let local = enforce_locality_exp locality local in +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; - do_cofixpoint local poly l + do_cofixpoint local atts.polymorphic l let vernac_scheme l = if Dumpglob.dump () then @@ -621,19 +622,19 @@ let vernac_combined_scheme lid l = List.iter (fun lid -> dump_global (Misctypes.AN (Ident lid))) l); Indschemes.do_combined_scheme lid l -let vernac_universe loc poly l = - if poly && not (Lib.sections_are_opened ()) then - user_err ?loc ~hdr:"vernac_universe" +let vernac_universe ~atts l = + if atts.polymorphic && not (Lib.sections_are_opened ()) then + user_err ?loc:atts.loc ~hdr:"vernac_universe" (str"Polymorphic universes can only be declared inside sections, " ++ str "use Monomorphic Universe instead"); - do_universe poly l + do_universe atts.polymorphic l -let vernac_constraint loc poly l = - if poly && not (Lib.sections_are_opened ()) then - user_err ?loc ~hdr:"vernac_constraint" +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 poly l + do_constraint atts.polymorphic l (**********************) (* Modules *) @@ -656,7 +657,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast = id binders_ast (Enforce mty_ast) [] in Dumpglob.dump_moddef ?loc mp "mod"; - Flags.if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is declared"); + Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared"); Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = @@ -678,7 +679,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = in Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info - (str "Interactive Module " ++ pr_id id ++ str " started"); + (str "Interactive Module " ++ Id.print id ++ str " started"); List.iter (fun (export,id) -> Option.iter @@ -696,14 +697,14 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = in Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info - (str "Module " ++ pr_id id ++ str " is defined"); + (str "Module " ++ Id.print id ++ str " is defined"); Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export let vernac_end_module export (loc,id as lid) = let mp = Declaremods.end_module () in Dumpglob.dump_modref ?loc mp "mod"; - Flags.if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined"); + Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined"); Option.iter (fun export -> vernac_import export [Ident lid]) export let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = @@ -725,7 +726,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = in Dumpglob.dump_moddef ?loc mp "modtype"; Flags.if_verbose Feedback.msg_info - (str "Interactive Module Type " ++ pr_id id ++ str " started"); + (str "Interactive Module Type " ++ Id.print id ++ str " started"); List.iter (fun (export,id) -> Option.iter @@ -744,12 +745,12 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = in Dumpglob.dump_moddef ?loc mp "modtype"; Flags.if_verbose Feedback.msg_info - (str "Module Type " ++ pr_id id ++ str " is defined") + (str "Module Type " ++ Id.print id ++ str " is defined") let vernac_end_modtype (loc,id) = let mp = Declaremods.end_modtype () in Dumpglob.dump_modref ?loc mp "modtype"; - Flags.if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined") + Flags.if_verbose Feedback.msg_info (str "Module Type " ++ Id.print id ++ str " is defined") let vernac_include l = Declaremods.declare_include Modintern.interp_module_ast l @@ -811,32 +812,32 @@ let vernac_require from import qidl = let vernac_canonical r = Recordops.declare_canonical_structure (smart_global r) -let vernac_coercion locality poly local ref qids qidt = - let local = enforce_locality locality local in +let vernac_coercion ~atts ref qids qidt = + let local = enforce_locality atts.locality in let target = cl_of_qualid qidt in let source = cl_of_qualid qids in let ref' = smart_global ref in - Class.try_add_new_coercion_with_target ref' ~local poly ~source ~target; + Class.try_add_new_coercion_with_target ref' ~local atts.polymorphic ~source ~target; Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion") -let vernac_identity_coercion locality poly local id qids qidt = - let local = enforce_locality locality local in +let vernac_identity_coercion ~atts id qids qidt = + let local = enforce_locality atts.locality in let target = cl_of_qualid qidt in let source = cl_of_qualid qids in - Class.try_add_new_identity_coercion id ~local poly ~source ~target + Class.try_add_new_identity_coercion id ~local atts.polymorphic ~source ~target (* Type classes *) -let vernac_instance abst locality poly sup inst props pri = - let global = not (make_section_locality locality) in +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 poly sup inst props pri) + ignore(Classes.new_instance ~abstract:abst ~global atts.polymorphic sup inst props pri) -let vernac_context poly l = - if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom +let vernac_context ~atts l = + if not (Classes.context atts.polymorphic l) then Feedback.feedback Feedback.AddedAxiom -let vernac_declare_instances locality insts = - let glob = not (make_section_locality locality) in +let vernac_declare_instances ~atts insts = + let glob = not (make_section_locality atts.locality) in List.iter (fun (id, info) -> Classes.existing_instance glob id (Some info)) insts let vernac_declare_class id = @@ -874,7 +875,7 @@ let vernac_set_used_variables e = List.iter (fun id -> if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then user_err ~hdr:"vernac_set_used_variables" - (str "Unknown variable: " ++ pr_id id)) + (str "Unknown variable: " ++ Id.print id)) l; let _, to_clear = Proof_global.set_used_variables l in let to_clear = List.map snd to_clear in @@ -893,7 +894,7 @@ let expand filename = let vernac_add_loadpath implicit pdir ldiropt = let pdir = expand pdir in - let alias = Option.default Nameops.default_root_prefix ldiropt in + let alias = Option.default Libnames.default_root_prefix ldiropt in Mltop.add_rec_path Mltop.AddTopML ~unix_path:pdir ~coq_root:alias ~implicit let vernac_remove_loadpath path = @@ -904,8 +905,8 @@ let vernac_remove_loadpath path = let vernac_add_ml_path isrec path = (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) (expand path) -let vernac_declare_ml_module locality l = - let local = make_locality locality in +let vernac_declare_ml_module ~atts l = + let local = make_locality atts.locality in Mltop.declare_ml_modules local (List.map expand l) let vernac_chdir = function @@ -938,25 +939,25 @@ let vernac_restore_state file = (************) (* Commands *) -let vernac_create_hintdb locality id b = - let local = make_module_locality locality in +let vernac_create_hintdb ~atts id b = + let local = make_module_locality atts.locality in Hints.create_hint_db local id full_transparent_state b -let vernac_remove_hints locality dbs ids = - let local = make_module_locality locality in +let vernac_remove_hints ~atts dbs ids = + let local = make_module_locality atts.locality in Hints.remove_hints local dbs (List.map Smartlocate.global_with_alias ids) -let vernac_hints locality poly local lb h = - let local = enforce_module_locality locality local in - Hints.add_hints local lb (Hints.interp_hints poly h) +let vernac_hints ~atts lb h = + let local = enforce_module_locality atts.locality in + Hints.add_hints local lb (Hints.interp_hints atts.polymorphic h) -let vernac_syntactic_definition locality lid x local y = +let vernac_syntactic_definition ~atts lid x y = Dumpglob.dump_definition lid false "syndef"; - let local = enforce_module_locality locality local in + let local = enforce_module_locality atts.locality in Metasyntax.add_syntactic_definition (Global.env()) (snd lid) x local y -let vernac_declare_implicits locality r l = - let local = make_section_locality locality in +let vernac_declare_implicits ~atts r l = + let local = make_section_locality atts.locality in match l with | [] -> Impargs.declare_implicits local (smart_global r) @@ -976,7 +977,7 @@ let warn_arguments_assert = (* [nargs_for_red] is the number of arguments required to trigger reduction, [args] is the main list of arguments statuses, [more_implicits] is a list of extra lists of implicit statuses *) -let vernac_arguments locality reference args more_implicits nargs_for_red flags = +let vernac_arguments ~atts reference args more_implicits nargs_for_red flags = let assert_flag = List.mem `Assert flags in let rename_flag = List.mem `Rename flags in let clear_scopes_flag = List.mem `ClearScopes flags in @@ -1184,7 +1185,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags (* Actions *) if renaming_specified then begin - let local = make_section_locality locality in + let local = make_section_locality atts.locality in Arguments_renaming.rename_arguments local sr names end; @@ -1194,20 +1195,20 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags with UserError _ -> Notation.find_delimiters_scope ?loc k)) scopes in - vernac_arguments_scope locality reference scopes + vernac_arguments_scope ~atts reference scopes end; if implicits_specified || clear_implicits_flag then - vernac_declare_implicits locality reference implicits; + vernac_declare_implicits ~atts reference implicits; if default_implicits_flag then - vernac_declare_implicits locality reference []; + vernac_declare_implicits ~atts reference []; if red_modifiers_specified then begin match sr with | ConstRef _ as c -> Reductionops.ReductionBehaviour.set - (make_section_locality locality) c + (make_section_locality atts.locality) c (rargs, Option.default ~-1 nargs_for_red, red_flags) | _ -> user_err (strbrk "Modifiers of the behavior of the simpl tactic "++ @@ -1235,8 +1236,8 @@ let vernac_reserve bl = Reserve.declare_reserved_type idl t) in List.iter sb_decl bl -let vernac_generalizable locality = - let local = make_non_locality locality in +let vernac_generalizable ~atts = + let local = make_non_locality atts.locality in Implicit_quantifiers.declare_generalizable local let _ = @@ -1473,8 +1474,8 @@ let _ = optread = Nativenorm.get_profiling_enabled; optwrite = Nativenorm.set_profiling_enabled } -let vernac_set_strategy locality l = - let local = make_locality locality in +let vernac_set_strategy ~atts l = + let local = make_locality atts.locality in let glob_ref r = match smart_global r with | ConstRef sp -> EvalConstRef sp @@ -1484,8 +1485,8 @@ let vernac_set_strategy locality l = let l = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) l in Redexpr.set_strategy local l -let vernac_set_opacity locality (v,l) = - let local = make_non_locality locality in +let vernac_set_opacity ~atts (v,l) = + let local = make_non_locality atts.locality in let glob_ref r = match smart_global r with | ConstRef sp -> EvalConstRef sp @@ -1495,18 +1496,18 @@ let vernac_set_opacity locality (v,l) = let l = List.map glob_ref l in Redexpr.set_strategy local [v,l] -let vernac_set_option locality key = function - | StringValue s -> set_string_option_value_gen locality key s - | StringOptValue (Some s) -> set_string_option_value_gen locality key s - | StringOptValue None -> unset_option_value_gen locality key - | IntValue n -> set_int_option_value_gen locality key n - | BoolValue b -> set_bool_option_value_gen locality key b +let vernac_set_option ~atts key = function + | StringValue s -> set_string_option_value_gen atts.locality key s + | StringOptValue (Some s) -> set_string_option_value_gen atts.locality key s + | StringOptValue None -> unset_option_value_gen atts.locality key + | IntValue n -> set_int_option_value_gen atts.locality key n + | BoolValue b -> set_bool_option_value_gen atts.locality key b -let vernac_set_append_option locality key s = - set_string_option_append_value_gen locality key s +let vernac_set_append_option ~atts key s = + set_string_option_append_value_gen atts.locality key s -let vernac_unset_option locality key = - unset_option_value_gen locality key +let vernac_unset_option ~atts key = + unset_option_value_gen atts.locality key let vernac_add_option key lv = let f = function @@ -1539,7 +1540,7 @@ let vernac_print_option key = let get_current_context_of_args = function | Some n -> Pfedit.get_goal_context n - | None -> get_current_context () + | None -> Pfedit.get_current_context () let query_command_selector ?loc = function | None -> None @@ -1547,16 +1548,16 @@ let query_command_selector ?loc = function | _ -> user_err ?loc ~hdr:"query_command_selector" (str "Query commands only support the single numbered goal selector.") -let vernac_check_may_eval ?loc redexp glopt rc = - let glopt = query_command_selector ?loc glopt in +let vernac_check_may_eval ~atts redexp glopt rc = + let glopt = query_command_selector ?loc:atts.loc glopt in let (sigma, env) = get_current_context_of_args glopt in let sigma', c = interp_open_constr env sigma rc in let c = EConstr.Unsafe.to_constr c in let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in Evarconv.check_problems_are_solved env sigma'; let sigma',nf = Evarutil.nf_evars_and_universes sigma' in - let pl, uctx = Evd.universe_context ~names:[] ~extensible:true sigma' in - let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in + let uctx = Evd.universe_context_set sigma' in + let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma' env) in let c = nf c in let j = if Evarutil.has_undefined_evars sigma' (EConstr.of_constr c) then @@ -1572,7 +1573,7 @@ let vernac_check_may_eval ?loc redexp glopt rc = let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in Feedback.msg_notice (print_judgment env sigma' j ++ pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ - Printer.pr_universe_ctx sigma uctx) + Printer.pr_universe_ctx_set sigma uctx) | Some r -> let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in let redfun env evm c = @@ -1582,26 +1583,27 @@ let vernac_check_may_eval ?loc redexp glopt rc = in Feedback.msg_notice (print_eval redfun env sigma' rc j) -let vernac_declare_reduction locality s r = - let local = make_locality locality in +let vernac_declare_reduction ~atts s r = + let local = make_locality atts.locality in declare_red_expr local s (snd (Hook.get f_interp_redexp (Global.env()) Evd.empty r)) (* The same but avoiding the current goal context if any *) 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 = let pf = Proof_global.give_me_the_proof() in - let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in + let gls,_,_,_,sigma = Proof.proof pf in let gl = {Evd.it=List.nth gls (n-1) ; sigma = sigma; } in gl @@ -1609,9 +1611,10 @@ exception NoHyp (* Printing "About" information of a hypothesis of the current goal. We only print the type and a small statement to this comes from the goal. Precondition: there must be at least one current goal. *) -let print_about_hyp_globs ?loc ref_or_by_not glopt = +let print_about_hyp_globs ?loc ref_or_by_not udecl glopt = let open Context.Named.Declaration in try + (* FIXME error on non None udecl if we find the hyp. *) let glnumopt = query_command_selector ?loc glopt in let gl,id = match glnumopt,ref_or_by_not with @@ -1628,17 +1631,22 @@ let print_about_hyp_globs ?loc ref_or_by_not glopt = let natureofid = match decl with | LocalAssum _ -> "Hypothesis" | LocalDef (_,bdy,_) ->"Constant (let in)" in - v 0 (pr_id id ++ str":" ++ pr_econstr (NamedDecl.get_type decl) ++ fnl() ++ fnl() + let sigma, env = Pfedit.get_current_context () in + v 0 (Id.print id ++ str":" ++ pr_econstr_env env sigma (NamedDecl.get_type decl) ++ fnl() ++ fnl() ++ str natureofid ++ str " of the goal context.") with (* fallback to globals *) - | NoHyp | Not_found -> print_about ref_or_by_not + | NoHyp | Not_found -> + let sigma, env = Pfedit.get_current_context () in + print_about env sigma ref_or_by_not udecl - -let vernac_print ?loc = let open Feedback in function +let vernac_print ~atts env sigma = + let open Feedback in + let loc = atts.loc in + function | PrintTables -> msg_notice (print_tables ()) - | PrintFullContext-> msg_notice (print_full_context_typ ()) - | PrintSectionContext qid -> msg_notice (print_sec_context_typ qid) - | PrintInspect n -> msg_notice (inspect n) + | PrintFullContext-> msg_notice (print_full_context_typ env sigma) + | PrintSectionContext qid -> msg_notice (print_sec_context_typ env sigma qid) + | PrintInspect n -> msg_notice (inspect env sigma n) | PrintGrammar ent -> msg_notice (Metasyntax.pr_grammar ent) | PrintLoadPath dir -> (* For compatibility ? *) msg_notice (print_loadpath dir) | PrintModules -> msg_notice (print_modules ()) @@ -1648,15 +1656,15 @@ let vernac_print ?loc = let open Feedback in function | PrintMLLoadPath -> msg_notice (Mltop.print_ml_path ()) | PrintMLModules -> msg_notice (Mltop.print_ml_modules ()) | PrintDebugGC -> msg_notice (Mltop.print_gc ()) - | PrintName qid -> dump_global qid; msg_notice (print_name qid) - | PrintGraph -> msg_notice (Prettyp.print_graph()) + | PrintName (qid,udecl) -> dump_global qid; msg_notice (print_name env sigma qid udecl) + | 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()) + | 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)) - | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ()) + 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 let univ = if b then UGraph.sort_universes univ else univ in @@ -1668,18 +1676,18 @@ let vernac_print ?loc = let open Feedback in function | None -> msg_notice (UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining) | Some s -> dump_universes_gen univ s end - | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r)) + | PrintHint r -> msg_notice (Hints.pr_hint_ref env sigma (smart_global r)) | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ()) - | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name s) - | PrintHintDb -> msg_notice (Hints.pr_searchtable ()) + | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name env sigma s) + | PrintHintDb -> msg_notice (Hints.pr_searchtable env sigma) | PrintScopes -> - msg_notice (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr)) + msg_notice (Notation.pr_scopes (Constrextern.without_symbols (pr_lglob_constr_env env))) | PrintScope s -> - msg_notice (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s) + msg_notice (Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s) | PrintVisibility s -> - msg_notice (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s) - | PrintAbout (ref_or_by_not,glnumopt) -> - msg_notice (print_about_hyp_globs ?loc ref_or_by_not glnumopt) + msg_notice (Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s) + | PrintAbout (ref_or_by_not,udecl,glnumopt) -> + msg_notice (print_about_hyp_globs ?loc ref_or_by_not udecl glnumopt) | PrintImplicit qid -> dump_global qid; msg_notice (print_impargs qid) | PrintAssumptions (o,t,r) -> @@ -1689,7 +1697,7 @@ let vernac_print ?loc = let open Feedback in function 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 = @@ -1743,8 +1751,8 @@ let _ = optread = (fun () -> !search_output_name_only); optwrite = (:=) search_output_name_only } -let vernac_search ?loc s gopt r = - let gopt = query_command_selector ?loc gopt in +let vernac_search ~atts s gopt r = + let gopt = query_command_selector ?loc:atts.loc gopt in let r = interp_search_restriction r in let env,gopt = match gopt with | None -> @@ -1780,9 +1788,10 @@ let vernac_locate = let open Feedback in function | LocateTerm (AN qid) -> msg_notice (print_located_term qid) | LocateAny (ByNotation (_, (ntn, sc))) (** TODO : handle Ltac notations *) | LocateTerm (ByNotation (_, (ntn, sc))) -> - msg_notice - (Notation.locate_notation - (Constrextern.without_symbols pr_lglob_constr) ntn sc) + let _, env = Pfedit.get_current_context () in + msg_notice + (Notation.locate_notation + (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc) | LocateLibrary qid -> print_located_library qid | LocateModule qid -> msg_notice (print_located_module qid) | LocateOther (s, qid) -> msg_notice (print_located_other s qid) @@ -1849,17 +1858,18 @@ let vernac_bullet (bullet : Proof_bullet.t) = let vernac_show = let open Feedback in function | ShowScript -> assert false (* Only the stm knows the script *) | ShowGoal goalref -> + let proof = Proof_global.give_me_the_proof () in let info = match goalref with - | OpenSubgoals -> pr_open_subgoals () - | NthGoal n -> pr_nth_open_subgoal n - | GoalId id -> pr_goal_by_id id + | OpenSubgoals -> pr_open_subgoals ~proof + | NthGoal n -> pr_nth_open_subgoal ~proof n + | GoalId id -> pr_goal_by_id ~proof id in msg_notice info | ShowProof -> show_proof () | ShowExistentials -> show_top_evars () | ShowUniverses -> show_universes () | ShowProofNames -> - msg_notice (pr_sequence pr_id (Proof_global.get_all_proof_names())) + msg_notice (pr_sequence Id.print (Proof_global.get_all_proof_names())) | ShowIntros all -> show_intro all | ShowMatch id -> show_match id @@ -1909,7 +1919,8 @@ let vernac_load interp fname = * is the outdated/deprecated "Local" attribute of some vernacular commands * still parsed as the obsolete_locality grammar entry for retrocompatibility. * loc is the Loc.t of the vernacular command being interpreted. *) -let interp ?proof ?loc locality poly c = +let interp ?proof ~atts ~st c = + let open Vernacinterp in vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c); match c with (* The below vernac are candidates for removal from the main type @@ -1948,31 +1959,33 @@ let interp ?proof ?loc locality poly c = | VernacLocal _ -> assert false (* Syntax *) - | VernacSyntaxExtension (infix, local,sl) -> - vernac_syntax_extension locality local infix sl + | VernacSyntaxExtension (infix, sl) -> + vernac_syntax_extension atts infix sl | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl - | VernacOpenCloseScope (local, s) -> vernac_open_close_scope locality local s - | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope locality qid scl - | VernacInfix (local,mv,qid,sc) -> vernac_infix locality local mv qid sc - | VernacNotation (local,c,infpl,sc) -> - vernac_notation locality local c infpl sc + | VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s) + | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope ~atts qid scl + | VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc + | VernacNotation (c,infpl,sc) -> + vernac_notation ~atts c infpl sc | VernacNotationAddFormat(n,k,v) -> Metasyntax.add_notation_extra_printing_rule n k v (* Gallina *) - | VernacDefinition (k,lid,d) -> vernac_definition locality poly k lid d - | VernacStartTheoremProof (k,l) -> vernac_start_proof locality poly k l + | VernacDefinition ((discharge,kind),lid,d) -> + vernac_definition ~atts discharge kind lid d + | VernacStartTheoremProof (k,l) -> vernac_start_proof ~atts k l | VernacEndProof e -> vernac_end_proof ?proof e | VernacExactProof c -> vernac_exact_proof c - | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl - | VernacInductive (cum, priv,finite,l) -> vernac_inductive cum poly priv finite l - | VernacFixpoint (local, l) -> vernac_fixpoint locality poly local l - | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l + | VernacAssumption ((discharge,kind),nl,l) -> + vernac_assumption ~atts discharge kind l nl + | VernacInductive (cum, priv,finite,l) -> vernac_inductive ~atts cum priv finite l + | VernacFixpoint (discharge, l) -> vernac_fixpoint ~atts discharge l + | VernacCoFixpoint (discharge, l) -> vernac_cofixpoint ~atts discharge l | VernacScheme l -> vernac_scheme l | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l - | VernacUniverse l -> vernac_universe loc poly l - | VernacConstraint l -> vernac_constraint loc poly l + | VernacUniverse l -> vernac_universe ~atts l + | VernacConstraint l -> vernac_constraint ~atts l (* Modules *) | VernacDeclareModule (export,lid,bl,mtyo) -> @@ -1993,15 +2006,15 @@ let interp ?proof ?loc locality poly c = | VernacRequire (from, export, qidl) -> vernac_require from export qidl | VernacImport (export,qidl) -> vernac_import export qidl | VernacCanonical qid -> vernac_canonical qid - | VernacCoercion (local,r,s,t) -> vernac_coercion locality poly local r s t - | VernacIdentityCoercion (local,(_,id),s,t) -> - vernac_identity_coercion locality poly local id s t + | VernacCoercion (r,s,t) -> vernac_coercion ~atts r s t + | VernacIdentityCoercion ((_,id),s,t) -> + vernac_identity_coercion ~atts id s t (* Type classes *) | VernacInstance (abst, sup, inst, props, info) -> - vernac_instance abst locality poly sup inst props info - | VernacContext sup -> vernac_context poly sup - | VernacDeclareInstances insts -> vernac_declare_instances locality insts + vernac_instance ~atts abst sup inst props info + | VernacContext sup -> vernac_context ~atts sup + | VernacDeclareInstances insts -> vernac_declare_instances ~atts insts | VernacDeclareClass id -> vernac_declare_class id (* Solving *) @@ -2011,7 +2024,7 @@ let interp ?proof ?loc locality poly c = | VernacAddLoadPath (isrec,s,alias) -> vernac_add_loadpath isrec s alias | VernacRemoveLoadPath s -> vernac_remove_loadpath s | VernacAddMLPath (isrec,s) -> vernac_add_ml_path isrec s - | VernacDeclareMLModule l -> vernac_declare_ml_module locality l + | VernacDeclareMLModule l -> vernac_declare_ml_module ~atts l | VernacChdir s -> vernac_chdir s (* State management *) @@ -2019,38 +2032,40 @@ let interp ?proof ?loc locality poly c = | VernacRestoreState s -> vernac_restore_state s (* Commands *) - | VernacCreateHintDb (dbname,b) -> vernac_create_hintdb locality dbname b - | VernacRemoveHints (dbnames,ids) -> vernac_remove_hints locality dbnames ids - | VernacHints (local,dbnames,hints) -> - vernac_hints locality poly local dbnames hints - | VernacSyntacticDefinition (id,c,local,b) -> - vernac_syntactic_definition locality id c local b + | VernacCreateHintDb (dbname,b) -> vernac_create_hintdb ~atts dbname b + | VernacRemoveHints (dbnames,ids) -> vernac_remove_hints ~atts dbnames ids + | VernacHints (dbnames,hints) -> + vernac_hints ~atts dbnames hints + | VernacSyntacticDefinition (id,c,b) -> + vernac_syntactic_definition ~atts id c b | VernacDeclareImplicits (qid,l) -> - vernac_declare_implicits locality qid l + vernac_declare_implicits ~atts qid l | VernacArguments (qid, args, more_implicits, nargs, flags) -> - vernac_arguments locality qid args more_implicits nargs flags + vernac_arguments ~atts qid args more_implicits nargs flags | VernacReserve bl -> vernac_reserve bl - | VernacGeneralizable gen -> vernac_generalizable locality gen - | VernacSetOpacity qidl -> vernac_set_opacity locality qidl - | VernacSetStrategy l -> vernac_set_strategy locality l - | VernacSetOption (key,v) -> vernac_set_option locality key v - | VernacSetAppendOption (key,v) -> vernac_set_append_option locality key v - | VernacUnsetOption key -> vernac_unset_option locality key + | VernacGeneralizable gen -> vernac_generalizable ~atts gen + | VernacSetOpacity qidl -> vernac_set_opacity ~atts qidl + | VernacSetStrategy l -> vernac_set_strategy ~atts l + | VernacSetOption (key,v) -> vernac_set_option ~atts key v + | VernacSetAppendOption (key,v) -> vernac_set_append_option ~atts key v + | VernacUnsetOption key -> vernac_unset_option ~atts key | VernacRemoveOption (key,v) -> vernac_remove_option key v | VernacAddOption (key,v) -> vernac_add_option key v | VernacMemOption (key,v) -> vernac_mem_option key v | VernacPrintOption key -> vernac_print_option key - | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ?loc r g c - | VernacDeclareReduction (s,r) -> vernac_declare_reduction locality s r + | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ~atts r g c + | VernacDeclareReduction (s,r) -> vernac_declare_reduction ~atts s r | VernacGlobalCheck c -> vernac_global_check c - | VernacPrint p -> vernac_print ?loc p - | VernacSearch (s,g,r) -> vernac_search ?loc s g r + | VernacPrint p -> + let sigma, env = Pfedit.get_current_context () in + vernac_print ~atts env sigma p + | VernacSearch (s,g,r) -> vernac_search ~atts s g r | VernacLocate l -> vernac_locate l | VernacRegister (id, r) -> vernac_register id r | VernacComments l -> Flags.if_verbose Feedback.msg_info (str "Comments ok\n") (* Proof management *) - | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t)] + | VernacGoal t -> vernac_start_proof ~atts Theorem [None,([],t)] | VernacFocus n -> vernac_focus n | VernacUnfocus -> vernac_unfocus () | VernacUnfocused -> vernac_unfocused () @@ -2063,13 +2078,16 @@ let interp ?proof ?loc locality poly c = let using = Option.append using (Proof_using.get_default_proof_using ()) in let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in let usings = if Option.is_empty using then "using:no" else "using:yes" in - Aux_file.record_in_aux_at ?loc "VernacProof" (tacs^" "^usings); + Aux_file.record_in_aux_at ?loc:atts.loc "VernacProof" (tacs^" "^usings); Option.iter vernac_set_end_tac tac; Option.iter vernac_set_used_variables using | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"] (* Extensions *) - | VernacExtend (opn,args) -> Vernacinterp.call ?locality ?loc (opn,args) + | VernacExtend (opn,args) -> + (* XXX: Here we are returning the state! :) *) + let _st : Vernacstate.t = Vernacinterp.call ~atts opn args ~st in + () (* Vernaculars that take a locality flag *) let check_vernac_supports_locality c l = @@ -2100,7 +2118,7 @@ let check_vernac_supports_polymorphism c p = | None, _ -> () | Some _, ( VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _ - | VernacAssumption _ | VernacInductive _ + | VernacAssumption _ | VernacInductive _ | VernacStartTheoremProof _ | VernacCoercion _ | VernacIdentityCoercion _ | VernacInstance _ | VernacDeclareInstances _ @@ -2109,7 +2127,7 @@ let check_vernac_supports_polymorphism c p = | Some _, _ -> user_err Pp.(str "This command does not support Polymorphism") let enforce_polymorphism = function - | None -> Flags.is_universe_polymorphism () + | None -> Flags.is_universe_polymorphism () | Some b -> Flags.make_polymorphic_flag b; b (** A global default timeout, controlled by option "Set Default Timeout n". @@ -2134,7 +2152,7 @@ let vernac_timeout f = match !current_timeout, !default_timeout with | Some n, _ | None, Some n -> let f () = f (); current_timeout := None in - Control.timeout n f Timeout + Control.timeout n f () Timeout | None, None -> f () let restore_timeout () = current_timeout := None @@ -2147,28 +2165,6 @@ let locate_if_not_already ?loc (e, info) = exception HasNotFailed exception HasFailed of Pp.t -type interp_state = { (* TODO: inline records in OCaml 4.03 *) - system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) - 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 invalidate_cache () = - s_cache := Obj.magic 0; - s_proof := Obj.magic 0 - -let freeze_interp_state marshallable = - { system = (s_cache := States.freeze ~marshallable; !s_cache); - proof = (s_proof := Proof_global.freeze ~marshallable; !s_proof); - 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) - (* XXX STATE: this type hints that restoring the state should be the caller's responsibility *) let with_fail st b f = @@ -2187,8 +2183,8 @@ let with_fail st b f = (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e))) with e when CErrors.noncritical e -> (* Restore the previous state XXX Careful here with the cache! *) - invalidate_cache (); - unfreeze_interp_state st; + Vernacstate.invalidate_cache (); + Vernacstate.unfreeze_interp_state st; let (e, _) = CErrors.push e in match e with | HasNotFailed -> @@ -2199,42 +2195,57 @@ let with_fail st b f = | _ -> assert false end -let interp ?(verbosely=true) ?proof st (loc,c) = +let interp ?(verbosely=true) ?proof ~st (loc,c) = let orig_program_mode = Flags.is_program_mode () in - let rec aux ?locality ?polymorphism isprogcmd = function - - | VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c - | VernacProgram _ -> user_err Pp.(str "Program mode specified twice") - | VernacLocal (b, c) when Option.is_empty locality -> - aux ~locality:b ?polymorphism isprogcmd c - | VernacPolymorphic (b, c) when polymorphism = None -> - aux ?locality ~polymorphism:b isprogcmd c - | VernacPolymorphic (b, c) -> user_err Pp.(str "Polymorphism specified twice") - | VernacLocal _ -> user_err Pp.(str "Locality specified twice") + let rec aux ?polymorphism ~atts isprogcmd = function + + | VernacProgram c when not isprogcmd -> + aux ?polymorphism ~atts true c + + | VernacProgram _ -> + user_err Pp.(str "Program mode specified twice") + + | VernacPolymorphic (b, c) when polymorphism = None -> + aux ~polymorphism:b ~atts:atts isprogcmd c + + | VernacPolymorphic (b, c) -> + user_err Pp.(str "Polymorphism specified twice") + + | VernacLocal (b, c) when Option.is_empty atts.locality -> + aux ?polymorphism ~atts:{atts with locality = Some b} isprogcmd c + + | VernacLocal _ -> + user_err Pp.(str "Locality specified twice") + | VernacFail v -> - with_fail st true (fun () -> aux ?locality ?polymorphism isprogcmd v) + with_fail st true (fun () -> aux ?polymorphism ~atts isprogcmd v) + | VernacTimeout (n,v) -> - current_timeout := Some n; - aux ?locality ?polymorphism isprogcmd v + current_timeout := Some n; + aux ?polymorphism ~atts isprogcmd v + | VernacRedirect (s, (_,v)) -> - Topfmt.with_output_to_file s (aux ?locality ?polymorphism isprogcmd) v + Topfmt.with_output_to_file s (aux ?polymorphism ~atts isprogcmd) v + | VernacTime (_,v) -> - System.with_time !Flags.time - (aux ?locality ?polymorphism isprogcmd) v; - | VernacLoad (_,fname) -> vernac_load (aux false) fname - | c -> - check_vernac_supports_locality c locality; - check_vernac_supports_polymorphism c polymorphism; - let poly = enforce_polymorphism polymorphism in - Obligations.set_program_mode isprogcmd; - try - vernac_timeout begin fun () -> + System.with_time !Flags.time (aux ?polymorphism ~atts isprogcmd) v; + + | VernacLoad (_,fname) -> vernac_load (aux ?polymorphism ~atts false) fname + + | c -> + check_vernac_supports_locality c atts.locality; + check_vernac_supports_polymorphism c polymorphism; + let polymorphic = enforce_polymorphism polymorphism in + Obligations.set_program_mode isprogcmd; + try + vernac_timeout begin fun () -> + let atts = { atts with polymorphic } in if verbosely - then Flags.verbosely (interp ?proof ?loc locality poly) c - else Flags.silently (interp ?proof ?loc locality poly) c; + then Flags.verbosely (interp ?proof ~atts ~st) c + else Flags.silently (interp ?proof ~atts ~st) c; if orig_program_mode || not !Flags.program_mode || isprogcmd then Flags.program_mode := orig_program_mode; - ignore (Flags.use_polymorphic_flag ()) + ignore (Flags.use_polymorphic_flag ()) end with | reraise when @@ -2249,10 +2260,19 @@ let interp ?(verbosely=true) ?proof st (loc,c) = ignore (Flags.use_polymorphic_flag ()); iraise e in - if verbosely then Flags.verbosely (aux false) c - else aux false c - -let interp ?verbosely ?proof st cmd = - unfreeze_interp_state st; - interp ?verbosely ?proof st cmd; - freeze_interp_state `No + let atts = { loc; locality = None; polymorphic = false; } in + if verbosely + then Flags.verbosely (aux ~atts orig_program_mode) c + else aux ~atts orig_program_mode c + +(* XXX: There is a bug here in case of an exception, see @gares + comments on the PR *) +let interp ?verbosely ?proof ~st cmd = + Vernacstate.unfreeze_interp_state st; + 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/vernacentries.mli b/vernac/vernacentries.mli index 56635c801..a559912a0 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -14,21 +14,11 @@ val dump_global : Libnames.reference or_by_notation -> unit val vernac_require : Libnames.reference option -> bool option -> Libnames.reference list -> unit -type interp_state = { (* TODO: inline records in OCaml 4.03 *) - system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) - shallow : bool (* is the state trimmed down (libstack) *) -} - -val freeze_interp_state : Summary.marshallable -> interp_state -val unfreeze_interp_state : interp_state -> unit - (** The main interpretation function of vernacular expressions *) val interp : ?verbosely:bool -> ?proof:Proof_global.closed_proof -> - interp_state -> - Vernacexpr.vernac_expr Loc.located -> interp_state + st:Vernacstate.t -> Vernacexpr.vernac_expr Loc.located -> Vernacstate.t (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name @@ -40,7 +30,7 @@ val make_cases : string -> string list list (* XXX STATE: this type hints that restoring the state should be the caller's responsibility *) -val with_fail : interp_state -> bool -> (unit -> unit) -> unit +val with_fail : Vernacstate.t -> bool -> (unit -> unit) -> unit val command_focus : unit Proof.focus_kind diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 41fee6bd0..c0b93c163 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -11,12 +11,21 @@ open Pp open CErrors type deprecation = bool -type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit + +type atts = { + loc : Loc.t option; + locality : bool option; + polymorphic : bool; +} + +type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t + +type plugin_args = Genarg.raw_generic_argument list (* Table of vernac entries *) let vernac_tab = - (Hashtbl.create 51 : - (Vernacexpr.extend_name, deprecation * vernac_command) Hashtbl.t) + (Hashtbl.create 211 : + (Vernacexpr.extend_name, deprecation * plugin_args vernac_command) Hashtbl.t) let vinterp_add depr s f = try @@ -49,7 +58,7 @@ let warn_deprecated_command = (* Interpretation of a vernac command *) -let call ?locality ?loc (opn,converted_args) = +let call opn converted_args ~atts ~st = let phase = ref "Looking up command" in try let depr, callback = vinterp_map opn in @@ -65,9 +74,7 @@ let call ?locality ?loc (opn,converted_args) = phase := "Checking arguments"; let hunk = callback converted_args in phase := "Executing command"; - Locality.LocalityFixme.set locality; - hunk loc; - Locality.LocalityFixme.assert_consumed() + hunk ~atts ~st with | Drop -> raise Drop | reraise -> diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli index 84370fdc2..ab3d4bfc5 100644 --- a/vernac/vernacinterp.mli +++ b/vernac/vernacinterp.mli @@ -9,12 +9,19 @@ (** Interpretation of extended vernac phrases. *) type deprecation = bool -type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit -val vinterp_add : deprecation -> Vernacexpr.extend_name -> - vernac_command -> unit -val overwriting_vinterp_add : - Vernacexpr.extend_name -> vernac_command -> unit +type atts = { + loc : Loc.t option; + locality : bool option; + polymorphic : bool; +} + +type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t + +type plugin_args = Genarg.raw_generic_argument list val vinterp_init : unit -> unit -val call : ?locality:bool -> ?loc:Loc.t -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit +val vinterp_add : deprecation -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit +val overwriting_vinterp_add : Vernacexpr.extend_name -> plugin_args vernac_command -> unit + +val call : Vernacexpr.extend_name -> plugin_args -> atts:atts -> st:Vernacstate.t -> Vernacstate.t diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml new file mode 100644 index 000000000..4980333b5 --- /dev/null +++ b/vernac/vernacstate.ml @@ -0,0 +1,41 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +type t = { + system : States.state; (* summary + libstack *) + proof : Proof_global.t; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) +} + +let s_cache = ref None +let s_proof = ref None + +let invalidate_cache () = + 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 = 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 } = + do_if_not_cached s_cache States.unfreeze system; + do_if_not_cached s_proof Proof_global.unfreeze proof diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli new file mode 100644 index 000000000..3ed27ddb7 --- /dev/null +++ b/vernac/vernacstate.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +type t = { + system : States.state; (* summary + libstack *) + proof : Proof_global.t; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) +} + +val freeze_interp_state : Summary.marshallable -> t +val unfreeze_interp_state : t -> unit + +(* WARNING: Do not use, it will go away in future releases *) +val invalidate_cache : unit -> unit |