aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml3
-rw-r--r--vernac/classes.ml24
-rw-r--r--vernac/classes.mli3
-rw-r--r--vernac/comAssumption.ml11
-rw-r--r--vernac/comDefinition.ml27
-rw-r--r--vernac/comDefinition.mli3
-rw-r--r--vernac/comPrimitive.ml59
-rw-r--r--vernac/comPrimitive.mli7
-rw-r--r--vernac/comProgramFixpoint.ml29
-rw-r--r--vernac/comProgramFixpoint.mli15
-rw-r--r--vernac/declare.ml330
-rw-r--r--vernac/declare.mli70
-rw-r--r--vernac/g_vernac.mlg2
-rw-r--r--vernac/ppvernac.ml2372
-rw-r--r--vernac/vernacentries.ml65
-rw-r--r--vernac/vernacexpr.ml2
-rw-r--r--vernac/vernacextend.ml6
-rw-r--r--vernac/vernacextend.mli6
-rw-r--r--vernac/vernacinterp.ml65
-rw-r--r--vernac/vernacstate.ml23
-rw-r--r--vernac/vernacstate.mli4
21 files changed, 1603 insertions, 1523 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index ef6f8652e9..f47cdd8bf0 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -155,7 +155,7 @@ let build_beq_scheme_deps kn =
| None -> accu)
| Rel _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | Proj _
| Construct _ | Case _ | CoFix _ | Fix _ | Meta _ | Evar _ | Int _
- | Float _ -> accu
+ | Float _ | Array _ -> accu
in
let u = Univ.Instance.empty in
let constrs n = get_constructors env (make_ind_family (((kn, i), u),
@@ -293,6 +293,7 @@ let build_beq_scheme mode kn =
| Evar _ -> raise (EqUnknown "existential variable")
| Int _ -> raise (EqUnknown "int")
| Float _ -> raise (EqUnknown "float")
+ | Array _ -> raise (EqUnknown "array")
in
aux t
in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index ba08aa2b94..f454c389dc 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -334,7 +334,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst
Impargs.maybe_declare_manual_implicits false cst impargs;
instance_hook pri global cst
-let declare_instance_program env sigma ~global ~poly name pri impargs udecl term termtype =
+let declare_instance_program pm env sigma ~global ~poly name pri impargs udecl term termtype =
let hook { Declare.Hook.S.scope; dref; _ } =
let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in
let pri = intern_info pri in
@@ -349,9 +349,9 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term
Decls.IsDefinition Decls.Instance in
let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
let info = Declare.Info.make ~udecl ~scope ~poly ~kind ~hook () in
- let _ : Declare.Obls.progress =
- Declare.Obls.add_definition ~cinfo ~info ~term ~uctx obls
- in ()
+ let pm, _ =
+ Declare.Obls.add_definition ~pm ~cinfo ~info ~term ~uctx obls
+ in pm
let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl ids term termtype =
(* spiwack: it is hard to reorder the actions to do
@@ -493,7 +493,7 @@ let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imp
Pretyping.check_evars_are_solved ~program_mode:false env sigma;
declare_instance_constant pri global imps ?hook id decl poly sigma term termtype
-let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props =
+let do_instance_program ~pm env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props =
let term, termtype, sigma =
match opt_props with
| Some props ->
@@ -506,9 +506,10 @@ let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri
term, termtype, sigma in
let termtype, sigma = do_instance_resolve_TC termtype sigma env in
if not (Evd.has_undefined sigma) && not (Option.is_empty opt_props) then
- declare_instance_constant pri global imps ?hook id decl poly sigma term termtype
+ let () = declare_instance_constant pri global imps ?hook id decl poly sigma term termtype in
+ pm
else
- declare_instance_program env sigma ~global ~poly id pri imps decl term termtype
+ declare_instance_program pm env sigma ~global ~poly id pri imps decl term termtype
let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
@@ -564,15 +565,16 @@ let new_instance_interactive ?(global=false)
id, do_instance_interactive env env' sigma ?hook ~tac ~global ~poly
cty k u ctx ctx' pri decl imps subst id opt_props
-let new_instance_program ?(global=false)
+let new_instance_program ?(global=false) ~pm
~poly instid ctx cl opt_props
?(generalize=true) ?hook pri =
let env = Global.env() in
let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
new_instance_common ~program_mode:true ~generalize env instid ctx cl in
- do_instance_program env env' sigma ?hook ~global ~poly
- cty k u ctx ctx' pri decl imps subst id opt_props;
- id
+ let pm =
+ do_instance_program ~pm env env' sigma ?hook ~global ~poly
+ cty k u ctx ctx' pri decl imps subst id opt_props in
+ pm, id
let new_instance ?(global=false)
~poly instid ctx cl props
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 07695b5bef..e1816fb138 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -52,6 +52,7 @@ val new_instance
val new_instance_program
: ?global:bool (** Not global by default. *)
+ -> pm:Declare.OblState.t
-> poly:bool
-> name_decl
-> local_binder_expr list
@@ -60,7 +61,7 @@ val new_instance_program
-> ?generalize:bool
-> ?hook:(GlobRef.t -> unit)
-> Vernacexpr.hint_info_expr
- -> Id.t
+ -> Declare.OblState.t * Id.t
val declare_new_instance
: ?global:bool (** Not global by default. *)
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index d8475126ca..401ba0fba4 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -268,11 +268,14 @@ let context ~poly l =
in
let b = Option.map (EConstr.to_constr sigma) b in
let t = EConstr.to_constr sigma t in
- let test x = match x.CAst.v with
- | Some (Name id',_) -> Id.equal name id'
- | _ -> false
+ let impl = let open Glob_term in
+ let search x = match x.CAst.v with
+ | Some (Name id',max) when Id.equal name id' ->
+ Some (if max then MaxImplicit else NonMaxImplicit)
+ | _ -> None
+ in
+ try CList.find_map search impls with Not_found -> Explicit
in
- let impl = Glob_term.(if List.exists test impls then MaxImplicit else Explicit) in (* ??? *)
name,b,t,impl)
ctx
in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index b9ed4f838d..37b7106856 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -29,14 +29,17 @@ let warn_implicits_in_term =
let check_imps ~impsty ~impsbody =
let rec aux impsty impsbody =
- match impsty, impsbody with
- | a1 :: impsty, a2 :: impsbody ->
- (match a1.CAst.v, a2.CAst.v with
- | None , None -> aux impsty impsbody
- | Some _ , Some _ -> aux impsty impsbody
- | _, _ -> warn_implicits_in_term ?loc:a2.CAst.loc ())
- | _ :: _, [] | [], _ :: _ -> (* Information only on one side *) ()
- | [], [] -> () in
+ match impsty, impsbody with
+ | a1 :: impsty, a2 :: impsbody ->
+ let () = match a1.CAst.v, a2.CAst.v with
+ | None , None | Some _, None -> ()
+ | Some (_,b1) , Some (_,b2) ->
+ if not ((b1:bool) = b2) then warn_implicits_in_term ?loc:a2.CAst.loc ()
+ | None, Some _ -> warn_implicits_in_term ?loc:a2.CAst.loc ()
+ in
+ aux impsty impsbody
+ | _ :: _, [] | [], _ :: _ -> (* Information only on one side *) ()
+ | [], [] -> () in
aux impsty impsbody
let protect_pattern_in_binder bl c ctypopt =
@@ -122,14 +125,14 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
Declare.declare_definition ~info ~cinfo ~opaque:false ~body evd
in ()
-let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
+let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
let program_mode = true in
let (body, types), evd, udecl, impargs =
interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
in
let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in
- let _ : Declare.Obls.progress =
+ let pm, _ =
let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook () in
- Declare.Obls.add_definition ~cinfo ~info ~term ~uctx obls
- in ()
+ Declare.Obls.add_definition ~pm ~cinfo ~info ~term ~uctx obls
+ in pm
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index e3417d0062..d95e64a85f 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -29,6 +29,7 @@ val do_definition
val do_definition_program
: ?hook:Declare.Hook.t
+ -> pm:Declare.OblState.t
-> name:Id.t
-> scope:Locality.locality
-> poly:bool
@@ -38,4 +39,4 @@ val do_definition_program
-> red_expr option
-> constr_expr
-> constr_expr option
- -> unit
+ -> Declare.OblState.t
diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml
index bcfbc049fa..110dcdc98a 100644
--- a/vernac/comPrimitive.ml
+++ b/vernac/comPrimitive.ml
@@ -8,30 +8,45 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-let do_primitive id prim typopt =
+open Names
+
+let declare id entry =
+ let _ : Constant.t =
+ Declare.declare_constant ~name:id ~kind:Decls.IsPrimitive (Declare.PrimitiveEntry entry)
+ in
+ Flags.if_verbose Feedback.msg_info Pp.(Id.print id ++ str " is declared")
+
+let do_primitive id udecl prim typopt =
if Global.sections_are_opened () then
CErrors.user_err Pp.(str "Declaring a primitive is not allowed in sections.");
if Dumpglob.dump () then Dumpglob.dump_definition id false "ax";
- let env = Global.env () in
- let evd = Evd.from_env env in
- let evd, typopt = Option.fold_left_map
- Constrintern.(interp_type_evars_impls ~impls:empty_internalization_env env)
- evd typopt
- in
- let evd = Evd.minimize_universes evd in
- let uvars, impls, typopt = match typopt with
- | None -> Univ.LSet.empty, [], None
- | Some (ty,impls) ->
- EConstr.universes_of_constr evd ty, impls, Some (EConstr.to_constr evd ty)
- in
- let evd = Evd.restrict_universe_context evd uvars in
- let uctx = UState.check_mono_univ_decl (Evd.evar_universe_context evd) UState.default_univ_decl in
- let entry = Entries.{
- prim_entry_type = typopt;
- prim_entry_univs = uctx;
+ let loc = id.CAst.loc in
+ let id = id.CAst.v in
+ match typopt with
+ | None ->
+ if Option.has_some udecl then
+ CErrors.user_err ?loc
+ Pp.(strbrk "Cannot use a universe declaration without a type when declaring primitives.");
+ declare id {Entries.prim_entry_type = None; prim_entry_content = prim}
+ | Some typ ->
+ let env = Global.env () in
+ let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
+ let auctx = CPrimitives.op_or_type_univs prim in
+ let evd, u = Evd.with_context_set UState.univ_flexible evd (UnivGen.fresh_instance auctx) in
+ let expected_typ = EConstr.of_constr @@ Typeops.type_of_prim_or_type env u prim in
+ let evd, (typ,impls) =
+ Constrintern.(interp_type_evars_impls ~impls:empty_internalization_env)
+ env evd typ
+ in
+ let evd = Evarconv.unify_delay env evd typ expected_typ in
+ let evd = Evd.minimize_universes evd in
+ let uvars = EConstr.universes_of_constr evd typ in
+ let evd = Evd.restrict_universe_context evd uvars in
+ let typ = EConstr.to_constr evd typ in
+ let univs = Evd.check_univ_decl ~poly:(not (Univ.AUContext.is_empty auctx)) evd udecl in
+ let entry = {
+ Entries.prim_entry_type = Some (typ,univs);
prim_entry_content = prim;
}
- in
- let _kn : Names.Constant.t =
- Declare.declare_constant ~name:id.CAst.v ~kind:Decls.IsPrimitive (Declare.PrimitiveEntry entry) in
- Flags.if_verbose Feedback.msg_info Pp.(Names.Id.print id.CAst.v ++ str " is declared")
+ in
+ declare id entry
diff --git a/vernac/comPrimitive.mli b/vernac/comPrimitive.mli
index 588eb7fdea..4d468f97b1 100644
--- a/vernac/comPrimitive.mli
+++ b/vernac/comPrimitive.mli
@@ -8,4 +8,9 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-val do_primitive : Names.lident -> CPrimitives.op_or_type -> Constrexpr.constr_expr option -> unit
+val do_primitive
+ : Names.lident
+ -> Constrexpr.universe_decl_expr option
+ -> CPrimitives.op_or_type
+ -> Constrexpr.constr_expr option
+ -> unit
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 37615fa09c..55901fd604 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -109,7 +109,7 @@ let telescope env sigma l =
let nf_evar_context sigma ctx =
List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx
-let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
+let build_wellfounded pm (recname,pl,bl,arityc,body) poly r measure notation =
let open EConstr in
let open Vars in
let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
@@ -262,9 +262,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
let uctx = Evd.evar_universe_context sigma in
let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ () in
let info = Declare.Info.make ~udecl ~poly ~hook () in
- let _ : Declare.Obls.progress =
- Declare.Obls.add_definition ~cinfo ~info ~term:evars_def ~uctx evars in
- ()
+ let pm, _ =
+ Declare.Obls.add_definition ~pm ~cinfo ~info ~term:evars_def ~uctx evars in
+ pm
let out_def = function
| Some def -> def
@@ -275,7 +275,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 ~scope ~poly fixkind fixl =
+let do_program_recursive ~pm ~scope ~poly fixkind fixl =
let cofix = fixkind = Declare.Obls.IsCoFixpoint in
let (env, rec_sign, udecl, evd), fix, info =
interp_recursive ~cofix ~program_mode:true fixl
@@ -323,15 +323,15 @@ let do_program_recursive ~scope ~poly fixkind fixl =
in
let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in
let info = Declare.Info.make ~poly ~scope ~kind ~udecl () in
- Declare.Obls.add_mutual_definitions defs ~info ~uctx ~ntns fixkind
+ Declare.Obls.add_mutual_definitions ~pm defs ~info ~uctx ~ntns fixkind
-let do_fixpoint ~scope ~poly l =
+let do_fixpoint ~pm ~scope ~poly l =
let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in
match g, l with
| [Some { CAst.v = CWfRec (n,r) }],
[ Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations} ] ->
let recarg = mkIdentC n.CAst.v in
- build_wellfounded (id, univs, binders, rtype, out_def body_def) poly r recarg notations
+ build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly r recarg notations
| [Some { CAst.v = CMeasureRec (n, m, r) }],
[Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations }] ->
@@ -344,7 +344,7 @@ let do_fixpoint ~scope ~poly l =
user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.")
| _, _ -> r
in
- build_wellfounded (id, univs, binders, rtype, out_def body_def) poly
+ build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly
(Option.default (CAst.make @@ CRef (lt_ref,None)) r) m notations
| _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g ->
@@ -352,12 +352,11 @@ let do_fixpoint ~scope ~poly l =
Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in
let fixkind = Declare.Obls.IsFixpoint annots in
let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in
- do_program_recursive ~scope ~poly fixkind l
-
+ do_program_recursive ~pm ~scope ~poly fixkind l
| _, _ ->
- user_err ~hdr:"do_fixpoint"
- (str "Well-founded fixpoints not allowed in mutually recursive blocks")
+ CErrors.user_err ~hdr:"do_fixpoint"
+ (str "Well-founded fixpoints not allowed in mutually recursive blocks")
-let do_cofixpoint ~scope ~poly fixl =
+let do_cofixpoint ~pm ~scope ~poly fixl =
let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in
- do_program_recursive ~scope ~poly Declare.Obls.IsCoFixpoint fixl
+ do_program_recursive ~pm ~scope ~poly Declare.Obls.IsCoFixpoint fixl
diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli
index e39f62c348..7935cf27fb 100644
--- a/vernac/comProgramFixpoint.mli
+++ b/vernac/comProgramFixpoint.mli
@@ -11,11 +11,16 @@
open Vernacexpr
(** Special Fixpoint handling when command is activated. *)
-
val do_fixpoint :
- (* When [false], assume guarded. *)
- scope:Locality.locality -> poly:bool -> fixpoint_expr list -> unit
+ pm:Declare.OblState.t
+ -> scope:Locality.locality
+ -> poly:bool
+ -> fixpoint_expr list
+ -> Declare.OblState.t
val do_cofixpoint :
- (* When [false], assume guarded. *)
- scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> unit
+ pm:Declare.OblState.t
+ -> scope:Locality.locality
+ -> poly:bool
+ -> cofixpoint_expr list
+ -> Declare.OblState.t
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 85359d5b62..df75e121d8 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -33,11 +33,14 @@ module Hook = struct
}
end
- type t = (S.t -> unit) CEphemeron.key
+ type 'a g = (S.t -> 'a -> 'a) CEphemeron.key
+ type t = unit g
- let make hook = CEphemeron.create hook
+ let make_g hook = CEphemeron.create hook
+ let make (hook : S.t -> unit) : t = CEphemeron.create (fun x () -> hook x)
- let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x) hook
+ let call_g ?hook x s = Option.cata (fun hook -> CEphemeron.get hook x s) s hook
+ let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x ()) hook
end
@@ -653,9 +656,10 @@ let declare_definition_core ~info ~cinfo ~opaque ~obls ~body sigma =
let { CInfo.name; impargs; typ; _ } = cinfo in
let entry, uctx = prepare_definition ~info ~opaque ~body ~typ sigma in
let { Info.scope; kind; hook; _ } = info in
- declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry
+ declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry, uctx
-let declare_definition = declare_definition_core ~obls:[]
+let declare_definition ~info ~cinfo ~opaque ~body sigma =
+ declare_definition_core ~obls:[] ~info ~cinfo ~opaque ~body sigma |> fst
let prepare_obligation ~name ~types ~body sigma =
let env = Global.env () in
@@ -683,14 +687,6 @@ let prepare_parameter ~poly ~udecl ~types sigma =
type progress = Remain of int | Dependent | Defined of GlobRef.t
-type obligation_resolver =
- Id.t option
- -> Int.Set.t
- -> unit Proofview.tactic option
- -> progress
-
-type obligation_qed_info = {name : Id.t; num : int; auto : obligation_resolver}
-
module Obls_ = struct
open Constr
@@ -716,10 +712,11 @@ type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint
module ProgramDecl = struct
- type t =
+ type 'a t =
{ prg_cinfo : constr CInfo.t
; prg_info : Info.t
; prg_opaque : bool
+ ; prg_hook : 'a Hook.g option
; prg_body : constr
; prg_uctx : UState.t
; prg_obligations : obligations
@@ -731,7 +728,7 @@ module ProgramDecl = struct
open Obligation
- let make ~info ~cinfo ~opaque ~ntns ~reduce ~deps ~uctx ~body ~fixpoint_kind obls =
+ let make ~info ~cinfo ~opaque ~ntns ~reduce ~deps ~uctx ~body ~fixpoint_kind ?obl_hook obls =
let obls', body =
match body with
| None ->
@@ -761,6 +758,7 @@ module ProgramDecl = struct
let prg_uctx = UState.make_flexible_nonalgebraic uctx in
{ prg_cinfo = { cinfo with CInfo.typ = reduce cinfo.CInfo.typ }
; prg_info = info
+ ; prg_hook = obl_hook
; prg_opaque = opaque
; prg_body = body
; prg_uctx
@@ -923,11 +921,11 @@ let err_not_transp () =
module ProgMap = Id.Map
-module StateFunctional = struct
+module State = struct
- type t = ProgramDecl.t CEphemeron.key ProgMap.t
+ type t = t ProgramDecl.t CEphemeron.key ProgMap.t
- let _empty = ProgMap.empty
+ let empty = ProgMap.empty
let pending pm =
ProgMap.filter
@@ -965,30 +963,12 @@ module StateFunctional = struct
let find m t = ProgMap.find_opt t m |> Option.map CEphemeron.get
end
-module State = struct
-
- type t = StateFunctional.t
-
- open StateFunctional
-
- let prg_ref, prg_tag =
- Summary.ref_tag ProgMap.empty ~name:"program-tcc-table"
-
- let first_pending () = first_pending !prg_ref
- let get_unique_open_prog id = get_unique_open_prog !prg_ref id
- let add id prg = prg_ref := add !prg_ref id prg
- let fold ~f ~init = fold !prg_ref ~f ~init
- let all () = all !prg_ref
- let find id = find !prg_ref id
-
-end
-
(* In all cases, the use of the map is read-only so we don't expose the ref *)
let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
-let check_solved_obligations ~what_for : unit =
- if not (ProgMap.is_empty !State.prg_ref) then
- let keys = map_keys !State.prg_ref in
+let check_solved_obligations ~pm ~what_for : unit =
+ if not (ProgMap.is_empty pm) then
+ let keys = map_keys pm in
let have_string = if Int.equal (List.length keys) 1 then " has " else " have " in
CErrors.user_err ~hdr:"Program"
Pp.(
@@ -1084,7 +1064,7 @@ let subst_prog subst prg =
( Vars.replace_vars subst' prg.prg_body
, Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_cinfo.CInfo.typ )
-let declare_definition prg =
+let declare_definition ~pm prg =
let varsubst = obligation_substitution true prg in
let sigma = Evd.from_ctx prg.prg_uctx in
let body, types = subst_prog varsubst prg in
@@ -1093,10 +1073,13 @@ let declare_definition prg =
let name, info, opaque = prg.prg_cinfo.CInfo.name, prg.prg_info, prg.prg_opaque in
let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in
(* XXX: This is doing normalization twice *)
- let kn = declare_definition_core ~cinfo ~info ~obls ~body ~opaque sigma in
- let pm = progmap_remove !State.prg_ref prg in
- State.prg_ref := pm;
- kn
+ let kn, uctx = declare_definition_core ~cinfo ~info ~obls ~body ~opaque sigma in
+ (* XXX: We call the obligation hook here, by consistency with the
+ previous imperative behaviour, however I'm not sure this is right *)
+ let pm = Hook.call_g ?hook:prg.prg_hook
+ { Hook.S.uctx; obls; scope = prg.prg_info.Info.scope; dref = kn} pm in
+ let pm = progmap_remove pm prg in
+ pm, kn
let rec lam_index n t acc =
match Constr.kind t with
@@ -1117,7 +1100,7 @@ let compute_possible_guardness_evidences n fixbody fixtype =
let ctx = fst (Term.decompose_prod_n_assum m fixtype) in
List.map_i (fun i _ -> i) 0 ctx
-let declare_mutual_definition l =
+let declare_mutual_definition ~pm l =
let len = List.length l in
let first = List.hd l in
let defobl x =
@@ -1181,34 +1164,33 @@ let declare_mutual_definition l =
in
(* Only for the first constant *)
let dref = List.hd kns in
- Hook.(
- call ?hook:first.prg_info.Info.hook {S.uctx = first.prg_uctx; obls; scope; dref});
- let pm = List.fold_left progmap_remove !State.prg_ref l in
- State.prg_ref := pm;
- dref
-
-let update_obls prg obls rem =
+ let s_hook = {Hook.S.uctx = first.prg_uctx; obls; scope; dref} in
+ Hook.call ?hook:first.prg_info.Info.hook s_hook;
+ (* XXX: We call the obligation hook here, by consistency with the
+ previous imperative behaviour, however I'm not sure this is right *)
+ let pm = Hook.call_g ?hook:first.prg_hook s_hook pm in
+ let pm = List.fold_left progmap_remove pm l in
+ pm, dref
+
+let update_obls ~pm prg obls rem =
let prg_obligations = {obls; remaining = rem} in
let prg' = {prg with prg_obligations} in
- let pm = progmap_replace prg' !State.prg_ref in
- State.prg_ref := pm;
+ let pm = progmap_replace prg' pm in
obligations_message rem;
- if rem > 0 then Remain rem
+ if rem > 0 then pm, Remain rem
else
match prg'.prg_deps with
| [] ->
- let kn = declare_definition prg' in
- let pm = progmap_remove !State.prg_ref prg' in
- State.prg_ref := pm;
- Defined kn
+ let pm, kn = declare_definition ~pm prg' in
+ pm, Defined kn
| l ->
let progs =
List.map (fun x -> CEphemeron.get (ProgMap.find x pm)) prg'.prg_deps
in
if List.for_all (fun x -> obligations_solved x) progs then
- let kn = declare_mutual_definition progs in
- Defined kn
- else Dependent
+ let pm, kn = declare_mutual_definition ~pm progs in
+ pm, Defined kn
+ else pm, Dependent
let dependencies obls n =
let res = ref Int.Set.empty in
@@ -1219,23 +1201,32 @@ let dependencies obls n =
obls;
!res
-let update_program_decl_on_defined prg obls num obl ~uctx rem ~auto =
+let update_program_decl_on_defined ~pm prg obls num obl ~uctx rem ~auto =
let obls = Array.copy obls in
let () = obls.(num) <- obl in
let prg = {prg with prg_uctx = uctx} in
- let _progress = update_obls prg obls (pred rem) in
- let () =
+ let pm, _progress = update_obls ~pm prg obls (pred rem) in
+ let pm =
if pred rem > 0 then
let deps = dependencies obls num in
if not (Int.Set.is_empty deps) then
- let _progress = auto (Some prg.prg_cinfo.CInfo.name) deps None in
- ()
- else ()
- else ()
+ let pm, _progress = auto ~pm (Some prg.prg_cinfo.CInfo.name) deps None in
+ pm
+ else pm
+ else pm
in
- ()
+ pm
+
+type obligation_resolver =
+ pm:State.t
+ -> Id.t option
+ -> Int.Set.t
+ -> unit Proofview.tactic option
+ -> State.t * progress
+
+type obligation_qed_info = {name : Id.t; num : int; auto : obligation_resolver}
-let obligation_terminator ~entry ~uctx ~oinfo:{name; num; auto} =
+let obligation_terminator ~pm ~entry ~uctx ~oinfo:{name; num; auto} =
let env = Global.env () in
let ty = entry.proof_entry_type in
let body, uctx = inline_private_constants ~uctx env entry in
@@ -1243,7 +1234,7 @@ let obligation_terminator ~entry ~uctx ~oinfo:{name; num; auto} =
Inductiveops.control_only_guard (Global.env ()) sigma
(EConstr.of_constr body);
(* Declare the obligation ourselves and drop the hook *)
- let prg = Option.get (State.find name) in
+ let prg = Option.get (State.find pm name) in
let {obls; remaining = rem} = prg.prg_obligations in
let obl = obls.(num) in
let status =
@@ -1274,16 +1265,17 @@ let obligation_terminator ~entry ~uctx ~oinfo:{name; num; auto} =
UState.from_env (Global.env ())
else uctx
in
- update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto;
- cst
+ let pm =
+ update_program_decl_on_defined ~pm prg obls num obl ~uctx:prg_ctx rem ~auto in
+ pm, cst
(* Similar to the terminator but for the admitted path; this assumes
the admitted constant was already declared.
FIXME: There is duplication of this code with obligation_terminator
and Obligations.admit_obligations *)
-let obligation_admitted_terminator {name; num; auto} ctx' dref =
- let prg = Option.get (State.find name) in
+let obligation_admitted_terminator ~pm {name; num; auto} ctx' dref =
+ let prg = Option.get (State.find pm name) in
let {obls; remaining = rem} = prg.prg_obligations in
let obl = obls.(num) in
let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in
@@ -1308,7 +1300,7 @@ let obligation_admitted_terminator {name; num; auto} ctx' dref =
in
let obl = {obl with obl_body = Some (DefinedObl (cst, inst))} in
let () = if transparent then add_hint true prg cst in
- update_program_decl_on_defined prg obls num obl ~uctx:ctx' rem ~auto
+ update_program_decl_on_defined ~pm prg obls num obl ~uctx:ctx' rem ~auto
end
@@ -1322,10 +1314,10 @@ module Proof_ending = struct
type t =
| Regular
- | End_obligation of obligation_qed_info
+ | End_obligation of Obls_.obligation_qed_info
| End_derive of { f : Id.t; name : Id.t }
| End_equations of
- { hook : Constant.t list -> Evd.evar_map -> unit
+ { hook : pm:Obls_.State.t -> Constant.t list -> Evd.evar_map -> Obls_.State.t
; i : Id.t
; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list
; sigma : Evd.evar_map
@@ -1951,15 +1943,15 @@ let compute_proof_using_for_admitted proof typ pproofs =
Some (Environ.really_needed env (Id.Set.union ids_typ ids_def))
| _ -> None
-let finish_admitted ~pinfo ~uctx pe =
+let finish_admitted ~pm ~pinfo ~uctx pe =
let cst = MutualEntry.declare_variable ~pinfo ~uctx pe in
(* If the constant was an obligation we need to update the program map *)
match CEphemeron.get pinfo.Proof_info.proof_ending with
| Proof_ending.End_obligation oinfo ->
- Obls_.obligation_admitted_terminator oinfo uctx (List.hd cst)
- | _ -> ()
+ Obls_.obligation_admitted_terminator ~pm oinfo uctx (List.hd cst)
+ | _ -> pm
-let save_admitted ~proof =
+let save_admitted ~pm ~proof =
let udecl = get_universe_decl proof in
let Proof.{ poly; entry } = Proof.data (get proof) in
let typ = match Proofview.initial_goals entry with
@@ -1972,7 +1964,7 @@ let save_admitted ~proof =
let sec_vars = compute_proof_using_for_admitted proof typ pproofs in
let uctx = get_initial_euctx proof in
let univs = UState.check_univ_decl ~poly uctx udecl in
- finish_admitted ~pinfo:proof.pinfo ~uctx (sec_vars, (typ, univs), None)
+ finish_admitted ~pm ~pinfo:proof.pinfo ~uctx (sec_vars, (typ, univs), None)
(************************************************************************)
(* Saving a lemma-like constant *)
@@ -2013,7 +2005,7 @@ let finish_derived ~f ~name ~entries =
let ct = declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in
[GlobRef.ConstRef ct]
-let finish_proved_equations ~kind ~hook i proof_obj types sigma0 =
+let finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma0 =
let obls = ref 1 in
let sigma, recobls =
@@ -2030,8 +2022,8 @@ let finish_proved_equations ~kind ~hook i proof_obj types sigma0 =
sigma, cst) sigma0
types proof_obj.entries
in
- hook recobls sigma;
- List.map (fun cst -> GlobRef.ConstRef cst) recobls
+ let pm = hook ~pm recobls sigma in
+ pm, List.map (fun cst -> GlobRef.ConstRef cst) recobls
let check_single_entry { entries; uctx } label =
match entries with
@@ -2039,20 +2031,20 @@ let check_single_entry { entries; uctx } label =
| _ ->
CErrors.anomaly ~label Pp.(str "close_proof returned more than one proof term")
-let finalize_proof proof_obj proof_info =
+let finalize_proof ~pm proof_obj proof_info =
let open Proof_ending in
match CEphemeron.default proof_info.Proof_info.proof_ending Regular with
| Regular ->
let entry, uctx = check_single_entry proof_obj "Proof.save" in
- MutualEntry.declare_mutdef ~entry ~uctx ~pinfo:proof_info
+ pm, MutualEntry.declare_mutdef ~entry ~uctx ~pinfo:proof_info
| End_obligation oinfo ->
let entry, uctx = check_single_entry proof_obj "Obligation.save" in
- Obls_.obligation_terminator ~entry ~uctx ~oinfo
+ Obls_.obligation_terminator ~pm ~entry ~uctx ~oinfo
| End_derive { f ; name } ->
- finish_derived ~f ~name ~entries:proof_obj.entries
+ pm, finish_derived ~f ~name ~entries:proof_obj.entries
| End_equations { hook; i; types; sigma } ->
let kind = proof_info.Proof_info.info.Info.kind in
- finish_proved_equations ~kind ~hook i proof_obj types sigma
+ finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma
let err_save_forbidden_in_place_of_qed () =
CErrors.user_err (Pp.str "Cannot use Save with more than one constant or in this proof mode")
@@ -2070,16 +2062,24 @@ let process_idopt_for_save ~idopt info =
err_save_forbidden_in_place_of_qed ()
in { info with Proof_info.cinfo }
-let save ~proof ~opaque ~idopt =
+let save ~pm ~proof ~opaque ~idopt =
(* Env and sigma are just used for error printing in save_remaining_recthms *)
let proof_obj = close_proof ~opaque ~keep_body_ucst_separate:false proof in
let proof_info = process_idopt_for_save ~idopt proof.pinfo in
- finalize_proof proof_obj proof_info
+ finalize_proof ~pm proof_obj proof_info
+
+let save_regular ~proof ~opaque ~idopt =
+ let open Proof_ending in
+ match CEphemeron.default proof.pinfo.Proof_info.proof_ending Regular with
+ | Regular ->
+ let (_, grs) : Obls_.State.t * _ = save ~pm:Obls_.State.empty ~proof ~opaque ~idopt in
+ grs
+ | _ -> CErrors.anomaly Pp.(str "save_regular: unexpected proof ending")
(***********************************************************************)
(* Special case to close a lemma without forcing a proof *)
(***********************************************************************)
-let save_lemma_admitted_delayed ~proof ~pinfo =
+let save_lemma_admitted_delayed ~pm ~proof ~pinfo =
let { entries; uctx } = proof in
if List.length entries <> 1 then
CErrors.user_err Pp.(str "Admitted does not support multiple statements");
@@ -2092,18 +2092,18 @@ let save_lemma_admitted_delayed ~proof ~pinfo =
| Some typ -> typ in
let ctx = UState.univ_entry ~poly uctx in
let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
- finish_admitted ~uctx ~pinfo (sec_vars, (typ, ctx), None)
+ finish_admitted ~pm ~uctx ~pinfo (sec_vars, (typ, ctx), None)
-let save_lemma_proved_delayed ~proof ~pinfo ~idopt =
+let save_lemma_proved_delayed ~pm ~proof ~pinfo ~idopt =
(* vio2vo calls this but with invalid info, we have to workaround
that to add the name to the info structure *)
if CList.is_empty pinfo.Proof_info.cinfo then
let name = get_po_name proof in
let info = Proof_info.add_first_thm ~pinfo ~name ~typ:EConstr.mkSet ~impargs:[] in
- finalize_proof proof info
+ finalize_proof ~pm proof info
else
let info = process_idopt_for_save ~idopt pinfo in
- finalize_proof proof info
+ finalize_proof ~pm proof info
end (* Proof module *)
@@ -2217,8 +2217,8 @@ let solve_by_tac ?loc name evi t ~poly ~uctx =
warn_solve_errored ?loc err;
None
-let get_unique_prog prg =
- match State.get_unique_open_prog prg with
+let get_unique_prog ~pm prg =
+ match State.get_unique_open_prog pm prg with
| Ok prg -> prg
| Error [] ->
Error.no_obligations None
@@ -2241,7 +2241,7 @@ let rec solve_obligation prg num tac =
let kind = kind_of_obligation (snd obl.obl_status) in
let evd = Evd.from_ctx (Internal.get_uctx prg) in
let evd = Evd.update_sigma_env evd (Global.env ()) in
- let auto n oblset tac = auto_solve_obligations n ~oblset tac in
+ let auto ~pm n oblset tac = auto_solve_obligations ~pm n ~oblset tac in
let proof_ending =
let name = Internal.get_name prg in
Proof_ending.End_obligation {name; num; auto}
@@ -2254,9 +2254,9 @@ let rec solve_obligation prg num tac =
let lemma = Option.cata (fun tac -> Proof.set_endline_tactic tac lemma) lemma tac in
lemma
-and obligation (user_num, name, typ) tac =
+and obligation (user_num, name, typ) ~pm tac =
let num = pred user_num in
- let prg = get_unique_prog name in
+ let prg = get_unique_prog ~pm name in
let { obls; remaining } = Internal.get_obligations prg in
if num >= 0 && num < Array.length obls then
let obl = obls.(num) in
@@ -2297,7 +2297,7 @@ and solve_obligation_by_tac prg obls i tac =
else Some prg
else None
-and solve_prg_obligations prg ?oblset tac =
+and solve_prg_obligations ~pm prg ?oblset tac =
let { obls; remaining } = Internal.get_obligations prg in
let rem = ref remaining in
let obls' = Array.copy obls in
@@ -2307,49 +2307,48 @@ and solve_prg_obligations prg ?oblset tac =
| Some s -> set := s;
(fun i -> Int.Set.mem i !set)
in
- let (), prg =
+ let prg =
Array.fold_left_i
- (fun i ((), prg) x ->
+ (fun i prg x ->
if p i then (
match solve_obligation_by_tac prg obls' i tac with
- | None -> (), prg
+ | None -> prg
| Some prg ->
let deps = dependencies obls i in
set := Int.Set.union !set deps;
decr rem;
- (), prg)
- else (), prg)
- ((), prg) obls'
+ prg)
+ else prg)
+ prg obls'
in
- update_obls prg obls' !rem
+ update_obls ~pm prg obls' !rem
-and solve_obligations n tac =
- let prg = get_unique_prog n in
- solve_prg_obligations prg tac
+and solve_obligations ~pm n tac =
+ let prg = get_unique_prog ~pm n in
+ solve_prg_obligations ~pm prg tac
-and solve_all_obligations tac =
- State.fold ~init:() ~f:(fun k v () ->
- let _ = solve_prg_obligations v tac in ())
+and solve_all_obligations ~pm tac =
+ State.fold pm ~init:pm ~f:(fun k v pm ->
+ solve_prg_obligations ~pm v tac |> fst)
-and try_solve_obligation n prg tac =
- let prg = get_unique_prog prg in
+and try_solve_obligation ~pm n prg tac =
+ let prg = get_unique_prog ~pm prg in
let {obls; remaining} = Internal.get_obligations prg in
let obls' = Array.copy obls in
match solve_obligation_by_tac prg obls' n tac with
| Some prg' ->
- let _r = update_obls prg' obls' (pred remaining) in
- ()
- | None -> ()
+ let pm, _ = update_obls ~pm prg' obls' (pred remaining) in
+ pm
+ | None -> pm
-and try_solve_obligations n tac =
- let _ = solve_obligations n tac in
- ()
+and try_solve_obligations ~pm n tac =
+ solve_obligations ~pm n tac |> fst
-and auto_solve_obligations n ?oblset tac : progress =
+and auto_solve_obligations ~pm n ?oblset tac : State.t * progress =
Flags.if_verbose Feedback.msg_info
(str "Solving obligations automatically...");
- let prg = get_unique_prog n in
- solve_prg_obligations prg ?oblset tac
+ let prg = get_unique_prog ~pm n in
+ solve_prg_obligations ~pm prg ?oblset tac
let show_single_obligation i n obls x =
let x = subst_deps_obl obls x in
@@ -2379,20 +2378,20 @@ let show_obligations_of_prg ?(msg = true) prg =
| Some _ -> ())
obls
-let show_obligations ?(msg = true) n =
+let show_obligations ~pm ?(msg = true) n =
let progs =
match n with
| None ->
- State.all ()
+ State.all pm
| Some n ->
- (match State.find n with
+ (match State.find pm n with
| Some prg -> [prg]
| None -> Error.no_obligations (Some n))
in
List.iter (fun x -> show_obligations_of_prg ~msg x) progs
-let show_term n =
- let prg = get_unique_prog n in
+let show_term ~pm n =
+ let prg = get_unique_prog ~pm n in
ProgramDecl.show prg
let msg_generating_obl name obls =
@@ -2404,46 +2403,46 @@ let msg_generating_obl name obls =
info ++ str ", generating " ++ int len ++
str (String.plural len " obligation"))
-let add_definition ~cinfo ~info ?term ~uctx
+let add_definition ~pm ~cinfo ~info ?obl_hook ?term ~uctx
?tactic ?(reduce = reduce) ?(opaque = false) obls =
let prg =
- ProgramDecl.make ~info ~cinfo ~body:term ~opaque ~uctx ~reduce ~ntns:[] ~deps:[] ~fixpoint_kind:None obls
+ ProgramDecl.make ~info ~cinfo ~body:term ~opaque ~uctx ~reduce ~ntns:[] ~deps:[] ~fixpoint_kind:None ?obl_hook obls
in
let name = CInfo.get_name cinfo in
let {obls;_} = Internal.get_obligations prg in
if Int.equal (Array.length obls) 0 then (
Flags.if_verbose (msg_generating_obl name) obls;
- let cst = Obls_.declare_definition prg in
- Defined cst)
+ let pm, cst = Obls_.declare_definition ~pm prg in
+ pm, Defined cst)
else
let () = Flags.if_verbose (msg_generating_obl name) obls in
- let () = State.add name prg in
- let res = auto_solve_obligations (Some name) tactic in
+ let pm = State.add pm name prg in
+ let pm, res = auto_solve_obligations ~pm (Some name) tactic in
match res with
| Remain rem ->
- Flags.if_verbose (show_obligations ~msg:false) (Some name);
- res
- | _ -> res
+ Flags.if_verbose (show_obligations ~pm ~msg:false) (Some name);
+ pm, res
+ | _ -> pm, res
-let add_mutual_definitions l ~info ~uctx
+let add_mutual_definitions l ~pm ~info ?obl_hook ~uctx
?tactic ?(reduce = reduce) ?(opaque = false) ~ntns fixkind =
let deps = List.map (fun (ci,_,_) -> CInfo.get_name ci) l in
let pm =
List.fold_left
- (fun () (cinfo, b, obls) ->
+ (fun pm (cinfo, b, obls) ->
let prg =
ProgramDecl.make ~info ~cinfo ~opaque ~body:(Some b) ~uctx ~deps
- ~fixpoint_kind:(Some fixkind) ~ntns obls ~reduce
+ ~fixpoint_kind:(Some fixkind) ~ntns ~reduce ?obl_hook obls
in
- State.add (CInfo.get_name cinfo) prg)
- () l
+ State.add pm (CInfo.get_name cinfo) prg)
+ pm l
in
let pm, _defined =
List.fold_left
(fun (pm, finished) x ->
if finished then (pm, finished)
else
- let res = auto_solve_obligations (Some x) tactic in
+ let pm, res = auto_solve_obligations ~pm (Some x) tactic in
match res with
| Defined _ ->
(* If one definition is turned into a constant,
@@ -2454,7 +2453,7 @@ let add_mutual_definitions l ~info ~uctx
in
pm
-let admit_prog prg =
+let admit_prog ~pm prg =
let {obls; remaining} = Internal.get_obligations prg in
let obls = Array.copy obls in
Array.iteri
@@ -2471,29 +2470,29 @@ let admit_prog prg =
obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x
| Some _ -> ())
obls;
- Obls_.update_obls prg obls 0
+ Obls_.update_obls ~pm prg obls 0
(* get_any_prog *)
-let rec admit_all_obligations () =
- let prg = State.first_pending () in
+let rec admit_all_obligations ~pm =
+ let prg = State.first_pending pm in
match prg with
- | None -> ()
+ | None -> pm
| Some prg ->
- let _prog = admit_prog prg in
- admit_all_obligations ()
+ let pm, _prog = admit_prog ~pm prg in
+ admit_all_obligations ~pm
-let admit_obligations n =
+let admit_obligations ~pm n =
match n with
- | None -> admit_all_obligations ()
+ | None -> admit_all_obligations ~pm
| Some _ ->
- let prg = get_unique_prog n in
- let _ = admit_prog prg in
- ()
+ let prg = get_unique_prog ~pm n in
+ let pm, _ = admit_prog ~pm prg in
+ pm
-let next_obligation n tac =
+let next_obligation ~pm n tac =
let prg = match n with
- | None -> State.first_pending () |> Option.get
- | Some _ -> get_unique_prog n
+ | None -> State.first_pending pm |> Option.get
+ | Some _ -> get_unique_prog ~pm n
in
let {obls; remaining} = Internal.get_obligations prg in
let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in
@@ -2509,7 +2508,6 @@ let check_program_libraries () =
Coqlib.check_required_library ["Coq";"Program";"Tactics"]
(* aliases *)
-module State = Obls_.State
let prepare_obligation = prepare_obligation
let check_solved_obligations = Obls_.check_solved_obligations
type fixpoint_kind = Obls_.fixpoint_kind =
@@ -2518,3 +2516,5 @@ type nonrec progress = progress =
| Remain of int | Dependent | Defined of GlobRef.t
end
+
+module OblState = Obls_.State
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 4891e66803..adb5bd026f 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -40,7 +40,9 @@ open Names
care, as imperative effects may become not supported in the
future. *)
module Hook : sig
- type t
+ type 'a g
+
+ type t = unit g
(** Hooks allow users of the API to perform arbitrary actions at
proof/definition saving time. For example, to register a constant
@@ -61,6 +63,7 @@ module Hook : sig
}
end
+ val make_g : (S.t -> 'a -> 'a) -> 'a g
val make : (S.t -> unit) -> t
val call : ?hook:t -> S.t -> unit
end
@@ -147,6 +150,13 @@ val declare_mutually_recursive
(** {2 Declaration of interactive constants } *)
+(** [save] / [save_admitted] can update obligations state, so we need
+ to expose the state here *)
+module OblState : sig
+ type t
+ val empty : t
+end
+
(** [Declare.Proof.t] Construction of constants using interactive proofs. *)
module Proof : sig
@@ -172,7 +182,7 @@ module Proof : sig
val start_equations :
name:Id.t
-> info:Info.t
- -> hook:(Constant.t list -> Evd.evar_map -> unit)
+ -> hook:(pm:OblState.t -> Constant.t list -> Evd.evar_map -> OblState.t)
-> types:(Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list
-> Evd.evar_map
-> Proofview.telescope
@@ -198,13 +208,21 @@ module Proof : sig
(** Qed a proof *)
val save
+ : pm:OblState.t
+ -> proof:t
+ -> opaque:Vernacexpr.opacity_flag
+ -> idopt:Names.lident option
+ -> OblState.t * GlobRef.t list
+
+ (** For proofs known to have [Regular] ending, no need to touch program state. *)
+ val save_regular
: proof:t
-> opaque:Vernacexpr.opacity_flag
-> idopt:Names.lident option
-> GlobRef.t list
(** Admit a proof *)
- val save_admitted : proof:t -> unit
+ val save_admitted : pm:OblState.t -> proof:t -> OblState.t
(** [by tac] applies tactic [tac] to the 1st subgoal of the current
focused proof.
@@ -287,15 +305,17 @@ module Proof : sig
(** Special cases for delayed proofs, in this case we must provide the
proof information so the proof won't be forced. *)
val save_lemma_admitted_delayed :
- proof:proof_object
+ pm:OblState.t
+ -> proof:proof_object
-> pinfo:Proof_info.t
- -> unit
+ -> OblState.t
val save_lemma_proved_delayed
- : proof:proof_object
+ : pm:OblState.t
+ -> proof:proof_object
-> pinfo:Proof_info.t
-> idopt:Names.lident option
- -> GlobRef.t list
+ -> OblState.t * GlobRef.t list
(** Used by the STM only to store info, should go away *)
val get_po_name : proof_object -> Id.t
@@ -446,16 +466,9 @@ module Obls : sig
type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint
-module State : sig
- (* Internal *)
- type t
- val prg_tag : t Summary.Dyn.tag
-end
-
(** Check obligations are properly solved before closing the
[what_for] section / module *)
-val check_solved_obligations : what_for:Pp.t -> unit
-
+val check_solved_obligations : pm:OblState.t -> what_for:Pp.t -> unit
val default_tactic : unit Proofview.tactic ref
(** Resolution status of a program *)
@@ -478,15 +491,17 @@ val prepare_obligation
will return whether all the obligations were solved; if so, it will
also register [c] with the kernel. *)
val add_definition :
- cinfo:Constr.types CInfo.t
+ pm:OblState.t
+ -> cinfo:Constr.types CInfo.t
-> info:Info.t
+ -> ?obl_hook: OblState.t Hook.g
-> ?term:Constr.t
-> uctx:UState.t
-> ?tactic:unit Proofview.tactic
-> ?reduce:(Constr.t -> Constr.t)
-> ?opaque:bool
-> RetrieveObl.obligation_info
- -> progress
+ -> OblState.t * progress
(* XXX: unify with MutualEntry *)
@@ -494,41 +509,44 @@ val add_definition :
except it takes a list now. *)
val add_mutual_definitions :
(Constr.t CInfo.t * Constr.t * RetrieveObl.obligation_info) list
+ -> pm:OblState.t
-> info:Info.t
+ -> ?obl_hook: OblState.t Hook.g
-> uctx:UState.t
-> ?tactic:unit Proofview.tactic
-> ?reduce:(Constr.t -> Constr.t)
-> ?opaque:bool
-> ntns:Vernacexpr.decl_notation list
-> fixpoint_kind
- -> unit
+ -> OblState.t
(** Implementation of the [Obligation] command *)
val obligation :
int * Names.Id.t option * Constrexpr.constr_expr option
+ -> pm:OblState.t
-> Genarg.glob_generic_argument option
-> Proof.t
(** Implementation of the [Next Obligation] command *)
val next_obligation :
- Names.Id.t option -> Genarg.glob_generic_argument option -> Proof.t
+ pm:OblState.t -> Names.Id.t option -> Genarg.glob_generic_argument option -> Proof.t
(** Implementation of the [Solve Obligation] command *)
val solve_obligations :
- Names.Id.t option -> unit Proofview.tactic option -> progress
+ pm:OblState.t -> Names.Id.t option -> unit Proofview.tactic option -> OblState.t * progress
-val solve_all_obligations : unit Proofview.tactic option -> unit
+val solve_all_obligations : pm:OblState.t -> unit Proofview.tactic option -> OblState.t
(** Number of remaining obligations to be solved for this program *)
val try_solve_obligation :
- int -> Names.Id.t option -> unit Proofview.tactic option -> unit
+ pm:OblState.t -> int -> Names.Id.t option -> unit Proofview.tactic option -> OblState.t
val try_solve_obligations :
- Names.Id.t option -> unit Proofview.tactic option -> unit
+ pm:OblState.t -> Names.Id.t option -> unit Proofview.tactic option -> OblState.t
-val show_obligations : ?msg:bool -> Names.Id.t option -> unit
-val show_term : Names.Id.t option -> Pp.t
-val admit_obligations : Names.Id.t option -> unit
+val show_obligations : pm:OblState.t -> ?msg:bool -> Names.Id.t option -> unit
+val show_term : pm:OblState.t -> Names.Id.t option -> Pp.t
+val admit_obligations : pm:OblState.t -> Names.Id.t option -> OblState.t
val check_program_libraries : unit -> unit
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index e1f1affb2f..e0550fd744 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -234,7 +234,7 @@ GRAMMAR EXTEND Gram
{ VernacRegister(g, RegisterCoqlib quid) }
| IDENT "Register"; IDENT "Inline"; g = global ->
{ VernacRegister(g, RegisterInline) }
- | IDENT "Primitive"; id = identref; typopt = OPT [ ":"; typ = lconstr -> { typ } ]; ":="; r = register_token ->
+ | IDENT "Primitive"; id = ident_decl; typopt = OPT [ ":"; typ = lconstr -> { typ } ]; ":="; r = register_token ->
{ VernacPrimitive(id, r, typopt) }
| IDENT "Universe"; l = LIST1 identref -> { VernacUniverse l }
| IDENT "Universes"; l = LIST1 identref -> { VernacUniverse l }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 7af6a6a405..e0974ac027 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -22,93 +22,93 @@ open Vernacexpr
open Declaremods
open Pputils
- open Ppconstr
+open Ppconstr
- let do_not_tag _ x = x
- let tag_keyword = do_not_tag ()
- let tag_vernac = do_not_tag
+let do_not_tag _ x = x
+let tag_keyword = do_not_tag ()
+let tag_vernac = do_not_tag
- let keyword s = tag_keyword (str s)
+let keyword s = tag_keyword (str s)
- let pr_constr = pr_constr_expr
- let pr_lconstr = pr_lconstr_expr
- let pr_spc_lconstr =
- let env = Global.env () in
- let sigma = Evd.from_env env in
- pr_sep_com spc @@ pr_lconstr_expr env sigma
+let pr_constr = pr_constr_expr
+let pr_lconstr = pr_lconstr_expr
+let pr_spc_lconstr =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ pr_sep_com spc @@ pr_lconstr_expr env sigma
- let pr_uconstraint (l, d, r) =
- pr_glob_sort_name l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
- pr_glob_sort_name r
+let pr_uconstraint (l, d, r) =
+ pr_glob_sort_name l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
+ pr_glob_sort_name r
- let pr_univ_name_list = function
- | None -> mt ()
- | Some l ->
- str "@{" ++ prlist_with_sep spc pr_lname l ++ str"}"
+let pr_univ_name_list = function
+ | None -> mt ()
+ | Some l ->
+ str "@{" ++ prlist_with_sep spc pr_lname l ++ str"}"
- let pr_univdecl_instance l extensible =
- prlist_with_sep spc pr_lident l ++
- (if extensible then str"+" else mt ())
+let pr_univdecl_instance l extensible =
+ prlist_with_sep spc pr_lident l ++
+ (if extensible then str"+" else mt ())
- let pr_univdecl_constraints l extensible =
- if List.is_empty l && extensible then mt ()
- else str"|" ++ spc () ++ prlist_with_sep (fun () -> str",") pr_uconstraint l ++
- (if extensible then str"+" else mt())
+let pr_univdecl_constraints l extensible =
+ if List.is_empty l && extensible then mt ()
+ else str"|" ++ spc () ++ prlist_with_sep (fun () -> str",") pr_uconstraint l ++
+ (if extensible then str"+" else mt())
- let pr_universe_decl l =
- let open UState in
- match l with
- | None -> mt ()
- | Some l ->
- str"@{" ++ pr_univdecl_instance l.univdecl_instance l.univdecl_extensible_instance ++
- pr_univdecl_constraints l.univdecl_constraints l.univdecl_extensible_constraints ++ str "}"
+let pr_universe_decl l =
+ let open UState in
+ match l with
+ | None -> mt ()
+ | Some l ->
+ str"@{" ++ pr_univdecl_instance l.univdecl_instance l.univdecl_extensible_instance ++
+ pr_univdecl_constraints l.univdecl_constraints l.univdecl_extensible_constraints ++ str "}"
- let pr_ident_decl (lid, l) =
- pr_lident lid ++ pr_universe_decl l
+let pr_ident_decl (lid, l) =
+ pr_lident lid ++ pr_universe_decl l
- let string_of_fqid fqid =
- String.concat "." (List.map Id.to_string fqid)
+let string_of_fqid fqid =
+ String.concat "." (List.map Id.to_string fqid)
- let pr_fqid fqid = str (string_of_fqid fqid)
+let pr_fqid fqid = str (string_of_fqid fqid)
- let pr_lfqid {CAst.loc;v=fqid} =
- match loc with
- | None -> pr_fqid fqid
- | Some loc -> let (b,_) = Loc.unloc loc in
- pr_located pr_fqid @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (string_of_fqid fqid))) fqid
+let pr_lfqid {CAst.loc;v=fqid} =
+ match loc with
+ | None -> pr_fqid fqid
+ | Some loc -> let (b,_) = Loc.unloc loc in
+ pr_located pr_fqid @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (string_of_fqid fqid))) fqid
- let pr_lname_decl (n, u) =
- pr_lname n ++ pr_universe_decl u
+let pr_lname_decl (n, u) =
+ pr_lname n ++ pr_universe_decl u
- let pr_smart_global = Pputils.pr_or_by_notation pr_qualid
+let pr_smart_global = Pputils.pr_or_by_notation pr_qualid
- let pr_ltac_ref = Libnames.pr_qualid
+let pr_ltac_ref = Libnames.pr_qualid
- let pr_module = Libnames.pr_qualid
+let pr_module = Libnames.pr_qualid
- let pr_one_import_filter_name (q,etc) =
- Libnames.pr_qualid q ++ if etc then str "(..)" else mt()
+let pr_one_import_filter_name (q,etc) =
+ Libnames.pr_qualid q ++ if etc then str "(..)" else mt()
- let pr_import_module (m,f) =
- Libnames.pr_qualid m ++ match f with
- | ImportAll -> mt()
- | ImportNames ns -> surround (prlist_with_sep pr_comma pr_one_import_filter_name ns)
+let pr_import_module (m,f) =
+ Libnames.pr_qualid m ++ match f with
+ | ImportAll -> mt()
+ | ImportNames ns -> surround (prlist_with_sep pr_comma pr_one_import_filter_name ns)
- let sep_end = function
- | VernacBullet _
- | VernacSubproof _
- | VernacEndSubproof -> str""
- | _ -> str"."
+let sep_end = function
+ | VernacBullet _
+ | VernacSubproof _
+ | VernacEndSubproof -> str""
+ | _ -> str"."
- let pr_gen t =
- let env = Global.env () in
- let sigma = Evd.from_env env in
- Pputils.pr_raw_generic env sigma t
+let pr_gen t =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ Pputils.pr_raw_generic env sigma t
- let sep = fun _ -> spc()
- let sep_v2 = fun _ -> str"," ++ spc()
+let sep = fun _ -> spc()
+let sep_v2 = fun _ -> str"," ++ spc()
- let string_of_theorem_kind = let open Decls in function
+let string_of_theorem_kind = let open Decls in function
| Theorem -> "Theorem"
| Lemma -> "Lemma"
| Fact -> "Fact"
@@ -117,7 +117,7 @@ open Pputils
| Proposition -> "Proposition"
| Corollary -> "Corollary"
- let string_of_definition_object_kind = let open Decls in function
+let string_of_definition_object_kind = let open Decls in function
| Definition -> "Definition"
| Example -> "Example"
| Coercion -> "Coercion"
@@ -128,313 +128,313 @@ open Pputils
| (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) ->
CErrors.anomaly (Pp.str "Internal definition kind.")
- let string_of_assumption_kind = let open Decls in function
+let string_of_assumption_kind = let open Decls in function
| Definitional -> "Parameter"
| Logical -> "Axiom"
| Conjectural -> "Conjecture"
| Context -> "Context"
- let string_of_logical_kind = let open Decls in function
+let string_of_logical_kind = let open Decls in function
| IsAssumption k -> string_of_assumption_kind k
| IsDefinition k -> string_of_definition_object_kind k
| IsProof k -> string_of_theorem_kind k
| IsPrimitive -> "Primitive"
- let pr_notation_entry = function
- | InConstrEntry -> keyword "constr"
- | InCustomEntry s -> keyword "custom" ++ spc () ++ str s
+let pr_notation_entry = function
+ | InConstrEntry -> keyword "constr"
+ | InCustomEntry s -> keyword "custom" ++ spc () ++ str s
- let pr_at_level = function
- | NumLevel n -> spc () ++ keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n
- | NextLevel -> spc () ++ keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level"
- | DefaultLevel -> mt ()
+let pr_at_level = function
+ | NumLevel n -> spc () ++ keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n
+ | NextLevel -> spc () ++ keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level"
+ | DefaultLevel -> mt ()
- let level_of_pattern_level = function None -> DefaultLevel | Some n -> NumLevel n
+let level_of_pattern_level = function None -> DefaultLevel | Some n -> NumLevel n
- let pr_constr_as_binder_kind = let open Notation_term in function
+let pr_constr_as_binder_kind = let open Notation_term in function
| AsIdent -> spc () ++ keyword "as ident"
| AsIdentOrPattern -> spc () ++ keyword "as pattern"
| AsStrictPattern -> spc () ++ keyword "as strict pattern"
- let pr_strict b = if b then str "strict " else mt ()
-
- let pr_set_entry_type pr = function
- | ETIdent -> str"ident"
- | ETGlobal -> str"global"
- | ETPattern (b,n) -> pr_strict b ++ str"pattern" ++ pr_at_level (level_of_pattern_level n)
- | ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko
- | ETBigint -> str "bigint"
- | ETBinder true -> str "binder"
- | ETBinder false -> str "closed binder"
-
- let pr_set_simple_entry_type =
- pr_set_entry_type pr_at_level
-
- let pr_comment pr_c = function
- | CommentConstr c -> pr_c c
- | CommentString s -> qs s
- | CommentInt n -> int n
-
- let pr_in_out_modules = function
- | SearchInside l -> spc() ++ keyword "inside" ++ spc() ++ prlist_with_sep sep pr_module l
- | SearchOutside [] -> mt()
- | SearchOutside l -> spc() ++ keyword "outside" ++ spc() ++ prlist_with_sep sep pr_module l
-
- let pr_search_where = function
- | Anywhere, false -> mt ()
- | Anywhere, true -> str "head:"
- | InHyp, true -> str "headhyp:"
- | InHyp, false -> str "hyp:"
- | InConcl, true -> str "headconcl:"
- | InConcl, false -> str "concl:"
-
- let pr_search_item = function
- | SearchSubPattern (where,p) ->
- let env = Global.env () in
- let sigma = Evd.from_env env in
- pr_search_where where ++ pr_constr_pattern_expr env sigma p
- | SearchString (where,s,sc) -> pr_search_where where ++ qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
- | SearchKind kind -> str "is:" ++ str (string_of_logical_kind kind)
-
- let rec pr_search_request = function
- | SearchLiteral a -> pr_search_item a
- | SearchDisjConj l -> str "[" ++ prlist_with_sep spc (prlist_with_sep pr_bar pr_search_default) l ++ str "]"
-
- and pr_search_default (b, s) =
- (if b then mt() else str "-") ++ pr_search_request s
-
- let pr_search a gopt b pr_p =
- pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt
- ++
- match a with
- | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
- | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b
- | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
- | Search sl ->
- keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_default sl ++ pr_in_out_modules b
-
- let pr_option_ref_value = function
- | Goptions.QualidRefValue id -> pr_qualid id
- | Goptions.StringRefValue s -> qs s
-
- let pr_printoption table b =
- prlist_with_sep spc str table ++
- pr_opt (prlist_with_sep sep pr_option_ref_value) b
-
- let pr_set_option a b =
- pr_printoption a None ++ (match b with
- | OptionUnset | OptionSetTrue -> mt()
- | OptionSetInt n -> spc() ++ int n
- | OptionSetString s -> spc() ++ quote (str s))
-
- let pr_opt_hintbases l = match l with
- | [] -> mt()
- | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z
-
- let pr_reference_or_constr pr_c = function
- | HintsReference r -> pr_qualid r
- | HintsConstr c -> pr_c c
-
- let pr_hint_mode = let open Hints in function
+let pr_strict b = if b then str "strict " else mt ()
+
+let pr_set_entry_type pr = function
+ | ETIdent -> str"ident"
+ | ETGlobal -> str"global"
+ | ETPattern (b,n) -> pr_strict b ++ str"pattern" ++ pr_at_level (level_of_pattern_level n)
+ | ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko
+ | ETBigint -> str "bigint"
+ | ETBinder true -> str "binder"
+ | ETBinder false -> str "closed binder"
+
+let pr_set_simple_entry_type =
+ pr_set_entry_type pr_at_level
+
+let pr_comment pr_c = function
+ | CommentConstr c -> pr_c c
+ | CommentString s -> qs s
+ | CommentInt n -> int n
+
+let pr_in_out_modules = function
+ | SearchInside l -> spc() ++ keyword "inside" ++ spc() ++ prlist_with_sep sep pr_module l
+ | SearchOutside [] -> mt()
+ | SearchOutside l -> spc() ++ keyword "outside" ++ spc() ++ prlist_with_sep sep pr_module l
+
+let pr_search_where = function
+ | Anywhere, false -> mt ()
+ | Anywhere, true -> str "head:"
+ | InHyp, true -> str "headhyp:"
+ | InHyp, false -> str "hyp:"
+ | InConcl, true -> str "headconcl:"
+ | InConcl, false -> str "concl:"
+
+let pr_search_item = function
+ | SearchSubPattern (where,p) ->
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ pr_search_where where ++ pr_constr_pattern_expr env sigma p
+ | SearchString (where,s,sc) -> pr_search_where where ++ qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+ | SearchKind kind -> str "is:" ++ str (string_of_logical_kind kind)
+
+let rec pr_search_request = function
+ | SearchLiteral a -> pr_search_item a
+ | SearchDisjConj l -> str "[" ++ prlist_with_sep spc (prlist_with_sep pr_bar pr_search_default) l ++ str "]"
+
+and pr_search_default (b, s) =
+ (if b then mt() else str "-") ++ pr_search_request s
+
+let pr_search a gopt b pr_p =
+ pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt
+ ++
+ match a with
+ | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
+ | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b
+ | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
+ | Search sl ->
+ keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_default sl ++ pr_in_out_modules b
+
+let pr_option_ref_value = function
+ | Goptions.QualidRefValue id -> pr_qualid id
+ | Goptions.StringRefValue s -> qs s
+
+let pr_printoption table b =
+ prlist_with_sep spc str table ++
+ pr_opt (prlist_with_sep sep pr_option_ref_value) b
+
+let pr_set_option a b =
+ pr_printoption a None ++ (match b with
+ | OptionUnset | OptionSetTrue -> mt()
+ | OptionSetInt n -> spc() ++ int n
+ | OptionSetString s -> spc() ++ quote (str s))
+
+let pr_opt_hintbases l = match l with
+ | [] -> mt()
+ | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z
+
+let pr_reference_or_constr pr_c = function
+ | HintsReference r -> pr_qualid r
+ | HintsConstr c -> pr_c c
+
+let pr_hint_mode = let open Hints in function
| ModeInput -> str"+"
| ModeNoHeadEvar -> str"!"
| ModeOutput -> str"-"
- let pr_hint_info pr_pat { Typeclasses.hint_priority = pri; hint_pattern = pat } =
- pr_opt (fun x -> str"|" ++ int x) pri ++
- pr_opt (fun y -> (if Option.is_empty pri then str"| " else mt()) ++ pr_pat y) pat
-
- let pr_hints db h pr_c pr_pat =
- let opth = pr_opt_hintbases db in
- let pph =
- let open Hints in
- match h with
- | HintsResolve l ->
- keyword "Resolve " ++ prlist_with_sep sep
- (fun (info, _, c) -> pr_reference_or_constr pr_c c ++ pr_hint_info pr_pat info)
- l
- | HintsResolveIFF (l2r, l, n) ->
- keyword "Resolve " ++ str (if l2r then "->" else "<-")
- ++ prlist_with_sep sep pr_qualid l
- | HintsImmediate l ->
- keyword "Immediate" ++ spc() ++
- prlist_with_sep sep (fun c -> pr_reference_or_constr pr_c c) l
- | HintsUnfold l ->
- keyword "Unfold" ++ spc () ++ prlist_with_sep sep pr_qualid l
- | HintsTransparency (l, b) ->
- keyword (if b then "Transparent" else "Opaque")
- ++ spc ()
- ++ (match l with
- | HintsVariables -> keyword "Variables"
- | HintsConstants -> keyword "Constants"
- | HintsReferences l -> prlist_with_sep sep pr_qualid l)
- | HintsMode (m, l) ->
- keyword "Mode"
- ++ spc ()
- ++ pr_qualid m ++ spc() ++
- prlist_with_sep spc pr_hint_mode l
- | HintsConstructors c ->
- keyword "Constructors"
- ++ spc() ++ prlist_with_sep spc pr_qualid c
- | HintsExtern (n,c,tac) ->
- let pat = match c with None -> mt () | Some pat -> pr_pat pat in
- let env = Global.env () in
- let sigma = Evd.from_env env in
- keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
- spc() ++ Pputils.pr_raw_generic env sigma tac
- in
- hov 2 (keyword "Hint "++ pph ++ opth)
-
- let pr_with_declaration pr_c = function
- | CWith_Definition (id,udecl,c) ->
- let p = pr_c c in
- keyword "Definition" ++ spc() ++ pr_lfqid id ++ pr_universe_decl udecl ++ str" := " ++ p
- | CWith_Module (id,qid) ->
- keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++
- pr_qualid qid
-
- let rec pr_module_ast leading_space pr_c = function
- | { loc ; v = CMident qid } ->
- if leading_space then
- spc () ++ pr_located pr_qualid (loc, qid)
- else
- pr_located pr_qualid (loc,qid)
- | { v = CMwith (mty,decl) } ->
- let m = pr_module_ast leading_space pr_c mty in
- let p = pr_with_declaration pr_c decl in
- m ++ spc() ++ keyword "with" ++ spc() ++ p
- | { v = CMapply (me1, ( { v = CMident _ } as me2 ) ) } ->
- pr_module_ast leading_space pr_c me1 ++ spc() ++ pr_module_ast false pr_c me2
- | { v = CMapply (me1,me2) } ->
- pr_module_ast leading_space pr_c me1 ++ spc() ++
- hov 1 (str"(" ++ pr_module_ast false pr_c me2 ++ str")")
-
- let pr_inline = function
- | DefaultInline -> mt ()
- | NoInline -> str "[no inline]"
- | InlineAt i -> str "[inline at level " ++ int i ++ str "]"
-
- let pr_assumption_inline = function
- | DefaultInline -> str "Inline"
- | NoInline -> mt ()
- | InlineAt i -> str "Inline(" ++ int i ++ str ")"
-
- let pr_module_ast_inl leading_space pr_c (mast,inl) =
- pr_module_ast leading_space pr_c mast ++ pr_inline inl
-
- let pr_of_module_type prc = function
- | Enforce mty -> str ":" ++ pr_module_ast_inl true prc mty
- | Check mtys ->
- prlist_strict (fun m -> str "<:" ++ pr_module_ast_inl true prc m) mtys
-
- let pr_require_token = function
- | Some true ->
- keyword "Export" ++ spc ()
- | Some false ->
- keyword "Import" ++ spc ()
- | None -> mt()
-
- let pr_module_vardecls pr_c (export,idl,(mty,inl)) =
- let m = pr_module_ast true pr_c mty in
- spc() ++
- hov 1 (str"(" ++ pr_require_token export ++
- prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")")
-
- let pr_module_binders l pr_c =
- prlist_strict (pr_module_vardecls pr_c) l
-
- let pr_type_option pr_c = function
- | { v = CHole (k, Namegen.IntroAnonymous, _) } -> mt()
- | _ as c -> brk(0,2) ++ str" :" ++ pr_c c
-
- let pr_binders_arg =
- let env = Global.env () in
- let sigma = Evd.from_env env in
- pr_non_empty_arg @@ pr_binders env sigma
-
- let pr_and_type_binders_arg bl =
- pr_binders_arg bl
-
- let pr_onescheme (idop,schem) =
- match schem with
- | InductionScheme (dep,ind,s) ->
- (match idop with
- | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
- | None -> spc ()
- ) ++
- hov 0 ((if dep then keyword "Induction for" else keyword "Minimality for")
- ++ spc() ++ pr_smart_global ind) ++ spc() ++
- hov 0 (keyword "Sort" ++ spc() ++ Sorts.pr_sort_family s)
- | CaseScheme (dep,ind,s) ->
- (match idop with
- | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
- | None -> spc ()
- ) ++
- hov 0 ((if dep then keyword "Elimination for" else keyword "Case for")
- ++ spc() ++ pr_smart_global ind) ++ spc() ++
- hov 0 (keyword "Sort" ++ spc() ++ Sorts.pr_sort_family s)
- | EqualityScheme ind ->
- (match idop with
- | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
- | None -> spc()
- ) ++
- hov 0 (keyword "Equality for")
- ++ spc() ++ pr_smart_global ind
-
- let begin_of_inductive = function
- | [] -> 0
- | (_,({loc},_))::_ -> Option.cata (fun loc -> fst (Loc.unloc loc)) 0 loc
-
- let pr_class_rawexpr = function
- | FunClass -> keyword "Funclass"
- | SortClass -> keyword "Sortclass"
- | RefClass qid -> pr_smart_global qid
-
- let pr_assumption_token many discharge kind =
- match discharge, kind with
- | (NoDischarge,Decls.Logical) ->
- keyword (if many then "Axioms" else "Axiom")
- | (NoDischarge,Decls.Definitional) ->
- keyword (if many then "Parameters" else "Parameter")
- | (NoDischarge,Decls.Conjectural) -> str"Conjecture"
- | (DoDischarge,Decls.Logical) ->
- keyword (if many then "Hypotheses" else "Hypothesis")
- | (DoDischarge,Decls.Definitional) ->
- keyword (if many then "Variables" else "Variable")
- | (DoDischarge,Decls.Conjectural) ->
- anomaly (Pp.str "Don't know how to beautify a local conjecture.")
- | (_,Decls.Context) ->
- anomaly (Pp.str "Context is used only internally.")
-
- let pr_params pr_c (xl,(c,t)) =
- hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++
- (if c then str":>" else str":" ++
- spc() ++ pr_c t))
-
- let rec factorize = function
- | [] -> []
- | (c,(idl,t))::l ->
- match factorize l with
- | (xl,((c', t') as r))::l'
- when (c : bool) == c' && (=) t t' ->
- (* FIXME: we need equality on constr_expr *)
- (idl@xl,r)::l'
- | l' -> (idl,(c,t))::l'
-
- let pr_ne_params_list pr_c l =
+let pr_hint_info pr_pat { Typeclasses.hint_priority = pri; hint_pattern = pat } =
+ pr_opt (fun x -> str"|" ++ int x) pri ++
+ pr_opt (fun y -> (if Option.is_empty pri then str"| " else mt()) ++ pr_pat y) pat
+
+let pr_hints db h pr_c pr_pat =
+ let opth = pr_opt_hintbases db in
+ let pph =
+ let open Hints in
+ match h with
+ | HintsResolve l ->
+ keyword "Resolve " ++ prlist_with_sep sep
+ (fun (info, _, c) -> pr_reference_or_constr pr_c c ++ pr_hint_info pr_pat info)
+ l
+ | HintsResolveIFF (l2r, l, n) ->
+ keyword "Resolve " ++ str (if l2r then "->" else "<-")
+ ++ prlist_with_sep sep pr_qualid l
+ | HintsImmediate l ->
+ keyword "Immediate" ++ spc() ++
+ prlist_with_sep sep (fun c -> pr_reference_or_constr pr_c c) l
+ | HintsUnfold l ->
+ keyword "Unfold" ++ spc () ++ prlist_with_sep sep pr_qualid l
+ | HintsTransparency (l, b) ->
+ keyword (if b then "Transparent" else "Opaque")
+ ++ spc ()
+ ++ (match l with
+ | HintsVariables -> keyword "Variables"
+ | HintsConstants -> keyword "Constants"
+ | HintsReferences l -> prlist_with_sep sep pr_qualid l)
+ | HintsMode (m, l) ->
+ keyword "Mode"
+ ++ spc ()
+ ++ pr_qualid m ++ spc() ++
+ prlist_with_sep spc pr_hint_mode l
+ | HintsConstructors c ->
+ keyword "Constructors"
+ ++ spc() ++ prlist_with_sep spc pr_qualid c
+ | HintsExtern (n,c,tac) ->
+ let pat = match c with None -> mt () | Some pat -> pr_pat pat in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
+ spc() ++ Pputils.pr_raw_generic env sigma tac
+ in
+ hov 2 (keyword "Hint "++ pph ++ opth)
+
+let pr_with_declaration pr_c = function
+ | CWith_Definition (id,udecl,c) ->
+ let p = pr_c c in
+ keyword "Definition" ++ spc() ++ pr_lfqid id ++ pr_universe_decl udecl ++ str" := " ++ p
+ | CWith_Module (id,qid) ->
+ keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++
+ pr_qualid qid
+
+let rec pr_module_ast leading_space pr_c = function
+ | { loc ; v = CMident qid } ->
+ if leading_space then
+ spc () ++ pr_located pr_qualid (loc, qid)
+ else
+ pr_located pr_qualid (loc,qid)
+ | { v = CMwith (mty,decl) } ->
+ let m = pr_module_ast leading_space pr_c mty in
+ let p = pr_with_declaration pr_c decl in
+ m ++ spc() ++ keyword "with" ++ spc() ++ p
+ | { v = CMapply (me1, ( { v = CMident _ } as me2 ) ) } ->
+ pr_module_ast leading_space pr_c me1 ++ spc() ++ pr_module_ast false pr_c me2
+ | { v = CMapply (me1,me2) } ->
+ pr_module_ast leading_space pr_c me1 ++ spc() ++
+ hov 1 (str"(" ++ pr_module_ast false pr_c me2 ++ str")")
+
+let pr_inline = function
+ | DefaultInline -> mt ()
+ | NoInline -> str "[no inline]"
+ | InlineAt i -> str "[inline at level " ++ int i ++ str "]"
+
+let pr_assumption_inline = function
+ | DefaultInline -> str "Inline"
+ | NoInline -> mt ()
+ | InlineAt i -> str "Inline(" ++ int i ++ str ")"
+
+let pr_module_ast_inl leading_space pr_c (mast,inl) =
+ pr_module_ast leading_space pr_c mast ++ pr_inline inl
+
+let pr_of_module_type prc = function
+ | Enforce mty -> str ":" ++ pr_module_ast_inl true prc mty
+ | Check mtys ->
+ prlist_strict (fun m -> str "<:" ++ pr_module_ast_inl true prc m) mtys
+
+let pr_require_token = function
+ | Some true ->
+ keyword "Export" ++ spc ()
+ | Some false ->
+ keyword "Import" ++ spc ()
+ | None -> mt()
+
+let pr_module_vardecls pr_c (export,idl,(mty,inl)) =
+ let m = pr_module_ast true pr_c mty in
+ spc() ++
+ hov 1 (str"(" ++ pr_require_token export ++
+ prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")")
+
+let pr_module_binders l pr_c =
+ prlist_strict (pr_module_vardecls pr_c) l
+
+let pr_type_option pr_c = function
+ | { v = CHole (k, Namegen.IntroAnonymous, _) } -> mt()
+ | _ as c -> brk(0,2) ++ str" :" ++ pr_c c
+
+let pr_binders_arg =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ pr_non_empty_arg @@ pr_binders env sigma
+
+let pr_and_type_binders_arg bl =
+ pr_binders_arg bl
+
+let pr_onescheme (idop,schem) =
+ match schem with
+ | InductionScheme (dep,ind,s) ->
+ (match idop with
+ | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
+ | None -> spc ()
+ ) ++
+ hov 0 ((if dep then keyword "Induction for" else keyword "Minimality for")
+ ++ spc() ++ pr_smart_global ind) ++ spc() ++
+ hov 0 (keyword "Sort" ++ spc() ++ Sorts.pr_sort_family s)
+ | CaseScheme (dep,ind,s) ->
+ (match idop with
+ | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
+ | None -> spc ()
+ ) ++
+ hov 0 ((if dep then keyword "Elimination for" else keyword "Case for")
+ ++ spc() ++ pr_smart_global ind) ++ spc() ++
+ hov 0 (keyword "Sort" ++ spc() ++ Sorts.pr_sort_family s)
+ | EqualityScheme ind ->
+ (match idop with
+ | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
+ | None -> spc()
+ ) ++
+ hov 0 (keyword "Equality for")
+ ++ spc() ++ pr_smart_global ind
+
+let begin_of_inductive = function
+ | [] -> 0
+ | (_,({loc},_))::_ -> Option.cata (fun loc -> fst (Loc.unloc loc)) 0 loc
+
+let pr_class_rawexpr = function
+ | FunClass -> keyword "Funclass"
+ | SortClass -> keyword "Sortclass"
+ | RefClass qid -> pr_smart_global qid
+
+let pr_assumption_token many discharge kind =
+ match discharge, kind with
+ | (NoDischarge,Decls.Logical) ->
+ keyword (if many then "Axioms" else "Axiom")
+ | (NoDischarge,Decls.Definitional) ->
+ keyword (if many then "Parameters" else "Parameter")
+ | (NoDischarge,Decls.Conjectural) -> str"Conjecture"
+ | (DoDischarge,Decls.Logical) ->
+ keyword (if many then "Hypotheses" else "Hypothesis")
+ | (DoDischarge,Decls.Definitional) ->
+ keyword (if many then "Variables" else "Variable")
+ | (DoDischarge,Decls.Conjectural) ->
+ anomaly (Pp.str "Don't know how to beautify a local conjecture.")
+ | (_,Decls.Context) ->
+ anomaly (Pp.str "Context is used only internally.")
+
+let pr_params pr_c (xl,(c,t)) =
+ hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++
+ (if c then str":>" else str":" ++
+ spc() ++ pr_c t))
+
+let rec factorize = function
+ | [] -> []
+ | (c,(idl,t))::l ->
match factorize l with
- | [p] -> pr_params pr_c p
- | l ->
- prlist_with_sep spc
- (fun p -> hov 1 (str "(" ++ pr_params pr_c p ++ str ")")) l
+ | (xl,((c', t') as r))::l'
+ when (c : bool) == c' && (=) t t' ->
+ (* FIXME: we need equality on constr_expr *)
+ (idl@xl,r)::l'
+ | l' -> (idl,(c,t))::l'
+
+let pr_ne_params_list pr_c l =
+ match factorize l with
+ | [p] -> pr_params pr_c p
+ | l ->
+ prlist_with_sep spc
+ (fun p -> hov 1 (str "(" ++ pr_params pr_c p ++ str ")")) l
(*
prlist_with_sep pr_semicolon (pr_params pr_c)
*)
- let pr_thm_token k = keyword (string_of_theorem_kind k)
+let pr_thm_token k = keyword (string_of_theorem_kind k)
- let pr_syntax_modifier = let open Gramlib.Gramext in function
+let pr_syntax_modifier = let open Gramlib.Gramext in function
| SetItemLevel (l,bko,n) ->
prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n ++
pr_opt pr_constr_as_binder_kind bko
@@ -449,861 +449,861 @@ open Pputils
| SetFormat("text",s) -> keyword "format " ++ pr_ast qs s
| SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_ast qs s
- let pr_syntax_modifiers = function
- | [] -> mt()
- | l -> spc() ++
- hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
-
- let pr_only_parsing_clause onlyparsing =
- pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])
-
- let pr_decl_notation prc decl_ntn =
- let open Vernacexpr in
- let
- { decl_ntn_string = {CAst.loc;v=ntn};
- decl_ntn_interp = c;
- decl_ntn_modifiers = modifiers;
- decl_ntn_scope = scopt } = decl_ntn in
- fnl () ++ keyword "where " ++ qs ntn ++ str " := "
- ++ Flags.without_option Flags.beautify prc c
- ++ pr_syntax_modifiers modifiers
- ++ pr_opt (fun sc -> str ": " ++ str sc) scopt
-
- let pr_rec_definition { fname; univs; rec_order; binders; rtype; body_def; notations } =
- let env = Global.env () in
- let sigma = Evd.from_env env in
- let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in
- let annot = pr_guard_annot (pr_lconstr_expr env sigma) binders rec_order in
- pr_ident_decl (fname,univs) ++ pr_binders_arg binders ++ annot
- ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr env sigma c) rtype
- ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr env sigma def) body_def
- ++ prlist (pr_decl_notation @@ pr_constr env sigma) notations
-
- let pr_statement head (idpl,(bl,c)) =
- let env = Global.env () in
- let sigma = Evd.from_env env in
- hov 2
- (head ++ spc() ++ pr_ident_decl idpl ++ spc() ++
- (match bl with [] -> mt() | _ -> pr_binders env sigma bl ++ spc()) ++
- str":" ++ pr_spc_lconstr c)
+let pr_syntax_modifiers = function
+ | [] -> mt()
+ | l -> spc() ++
+ hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
+
+let pr_only_parsing_clause onlyparsing =
+ pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])
+
+let pr_decl_notation prc decl_ntn =
+ let open Vernacexpr in
+ let
+ { decl_ntn_string = {CAst.loc;v=ntn};
+ decl_ntn_interp = c;
+ decl_ntn_modifiers = modifiers;
+ decl_ntn_scope = scopt } = decl_ntn in
+ fnl () ++ keyword "where " ++ qs ntn ++ str " := "
+ ++ Flags.without_option Flags.beautify prc c
+ ++ pr_syntax_modifiers modifiers
+ ++ pr_opt (fun sc -> str ": " ++ str sc) scopt
+
+let pr_rec_definition { fname; univs; rec_order; binders; rtype; body_def; notations } =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in
+ let annot = pr_guard_annot (pr_lconstr_expr env sigma) binders rec_order in
+ pr_ident_decl (fname,univs) ++ pr_binders_arg binders ++ annot
+ ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr env sigma c) rtype
+ ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr env sigma def) body_def
+ ++ prlist (pr_decl_notation @@ pr_constr env sigma) notations
+
+let pr_statement head (idpl,(bl,c)) =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ hov 2
+ (head ++ spc() ++ pr_ident_decl idpl ++ spc() ++
+ (match bl with [] -> mt() | _ -> pr_binders env sigma bl ++ spc()) ++
+ str":" ++ pr_spc_lconstr c)
(**************************************)
(* Pretty printer for vernac commands *)
(**************************************)
- let pr_constrarg c =
- let env = Global.env () in
- let sigma = Evd.from_env env in
- spc () ++ pr_constr env sigma c
- let pr_lconstrarg c =
- let env = Global.env () in
- let sigma = Evd.from_env env in
- spc () ++ pr_lconstr env sigma c
- let pr_intarg n = spc () ++ int n
-
- let pr_oc = function
- | None -> str" :"
- | Some true -> str" :>"
- | Some false -> str" :>>"
-
- let pr_record_field (x, { rf_subclass = oc ; rf_priority = pri ; rf_notation = ntn }) =
- let env = Global.env () in
- let sigma = Evd.from_env env in
- let prx = match x with
- | AssumExpr (id,t) ->
- hov 1 (pr_lname id ++
+let pr_constrarg c =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ spc () ++ pr_constr env sigma c
+let pr_lconstrarg c =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ spc () ++ pr_lconstr env sigma c
+let pr_intarg n = spc () ++ int n
+
+let pr_oc = function
+ | None -> str" :"
+ | Some true -> str" :>"
+ | Some false -> str" :>>"
+
+let pr_record_field (x, { rf_subclass = oc ; rf_priority = pri ; rf_notation = ntn }) =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let prx = match x with
+ | AssumExpr (id,t) ->
+ hov 1 (pr_lname id ++
+ pr_oc oc ++ spc() ++
+ pr_lconstr_expr env sigma t)
+ | DefExpr(id,b,opt) -> (match opt with
+ | Some t ->
+ hov 1 (pr_lname id ++
pr_oc oc ++ spc() ++
- pr_lconstr_expr env sigma t)
- | DefExpr(id,b,opt) -> (match opt with
- | Some t ->
- hov 1 (pr_lname id ++
- pr_oc oc ++ spc() ++
- pr_lconstr_expr env sigma t ++ str" :=" ++ pr_lconstr env sigma b)
- | None ->
- hov 1 (pr_lname id ++ str" :=" ++ spc() ++
- pr_lconstr env sigma b)) in
- let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in
- prx ++ prpri ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn
-
- let pr_record_decl c fs =
- pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++
- hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")
-
- let pr_printable = function
- | PrintFullContext ->
- keyword "Print All"
- | PrintSectionContext s ->
- keyword "Print Section" ++ spc() ++ Libnames.pr_qualid s
- | PrintGrammar ent ->
- keyword "Print Grammar" ++ spc() ++ str ent
- | PrintCustomGrammar ent ->
- keyword "Print Custom Grammar" ++ spc() ++ str ent
- | PrintLoadPath dir ->
- keyword "Print LoadPath" ++ pr_opt DirPath.print dir
- | PrintModules ->
- keyword "Print Modules"
- | PrintMLLoadPath ->
- keyword "Print ML Path"
- | PrintMLModules ->
- keyword "Print ML Modules"
- | PrintDebugGC ->
- keyword "Print ML GC"
- | PrintGraph ->
- keyword "Print Graph"
- | PrintClasses ->
- keyword "Print Classes"
- | PrintTypeClasses ->
- keyword "Print TypeClasses"
- | PrintInstances qid ->
- keyword "Print Instances" ++ spc () ++ pr_smart_global qid
- | PrintCoercions ->
- keyword "Print Coercions"
- | PrintCoercionPaths (s,t) ->
- keyword "Print Coercion Paths" ++ spc()
- ++ pr_class_rawexpr s ++ spc()
- ++ pr_class_rawexpr t
- | PrintCanonicalConversions qids ->
- keyword "Print Canonical Structures" ++ prlist pr_smart_global qids
- | PrintTypingFlags ->
- keyword "Print Typing Flags"
- | PrintTables ->
- keyword "Print Tables"
- | PrintHintGoal ->
- keyword "Print Hint"
- | PrintHint qid ->
- keyword "Print Hint" ++ spc () ++ pr_smart_global qid
- | PrintHintDb ->
- keyword "Print Hint *"
- | PrintHintDbName s ->
- keyword "Print HintDb" ++ spc () ++ str s
- | PrintUniverses (b, g, fopt) ->
- let cmd =
- if b then "Print Sorted Universes"
- else "Print Universes"
- in
- let pr_subgraph = prlist_with_sep spc pr_qualid in
- keyword cmd ++ pr_opt pr_subgraph g ++ pr_opt str fopt
- | PrintName (qid,udecl) ->
- keyword "Print" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list udecl
- | PrintModuleType qid ->
- keyword "Print Module Type" ++ spc() ++ pr_qualid qid
- | PrintModule qid ->
- keyword "Print Module" ++ spc() ++ pr_qualid qid
- | PrintInspect n ->
- keyword "Inspect" ++ spc() ++ int n
- | PrintScopes ->
- keyword "Print Scopes"
- | PrintScope s ->
- keyword "Print Scope" ++ spc() ++ str s
- | PrintVisibility s ->
- keyword "Print Visibility" ++ pr_opt str s
- | PrintAbout (qid,l,gopt) ->
- pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt
- ++ keyword "About" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list l
- | PrintImplicit qid ->
- keyword "Print Implicit" ++ spc() ++ pr_smart_global qid
- (* spiwack: command printing all the axioms and section variables used in a
- term *)
- | PrintAssumptions (b, t, qid) ->
- let cmd = match b, t with
- | true, true -> "Print All Dependencies"
- | true, false -> "Print Opaque Dependencies"
- | false, true -> "Print Transparent Dependencies"
- | false, false -> "Print Assumptions"
- in
- keyword cmd ++ spc() ++ pr_smart_global qid
- | PrintNamespace dp ->
- keyword "Print Namespace" ++ DirPath.print dp
- | PrintStrategy None ->
- keyword "Print Strategies"
- | PrintStrategy (Some qid) ->
- keyword "Print Strategy" ++ pr_smart_global qid
- | PrintRegistered ->
- keyword "Print Registered"
-
- let pr_using e =
- let rec aux = function
- | SsEmpty -> "()"
- | SsType -> "(Type)"
- | SsSingl { v=id } -> "("^Id.to_string id^")"
- | SsCompl e -> "-" ^ aux e^""
- | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")"
- | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")"
- | SsFwdClose e -> "("^aux e^")*"
- in Pp.str (aux e)
-
- let pr_extend s cl =
- let pr_arg a =
- try pr_gen a
- with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in
- try
- let rl = Egramml.get_extend_vernac_rule s in
- let rec aux rl cl =
- match rl, cl with
- | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl
- | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl
- | [], [] -> []
- | _ -> assert false in
- hov 1 (pr_sequence identity (aux rl cl))
- with Not_found ->
- hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")
-
- let pr_vernac_expr v =
- let return = tag_vernac v in
- let env = Global.env () in
- let sigma = Evd.from_env env in
- match v with
- | VernacLoad (f,s) ->
- return (
- keyword "Load"
- ++ if f then
- (spc() ++ keyword "Verbose" ++ spc())
- else
- spc() ++ qs s
- )
-
- (* Proof management *)
- | VernacAbortAll ->
- return (keyword "Abort All")
- | VernacRestart ->
- return (keyword "Restart")
- | VernacUnfocus ->
- return (keyword "Unfocus")
- | VernacUnfocused ->
- return (keyword "Unfocused")
- | VernacAbort id ->
- return (keyword "Abort" ++ pr_opt pr_lident id)
- | VernacUndo i ->
- return (
- if Int.equal i 1 then keyword "Undo" else keyword "Undo" ++ pr_intarg i
- )
- | VernacUndoTo i ->
- return (keyword "Undo" ++ spc() ++ keyword "To" ++ pr_intarg i)
- | VernacFocus i ->
- return (keyword "Focus" ++ pr_opt int i)
- | VernacShow s ->
- let pr_goal_reference = function
- | OpenSubgoals -> mt ()
- | NthGoal n -> spc () ++ int n
- | GoalId id -> spc () ++ pr_id id
- in
- let pr_showable = function
- | ShowGoal n -> keyword "Show" ++ pr_goal_reference n
- | ShowProof -> keyword "Show Proof"
- | ShowExistentials -> keyword "Show Existentials"
- | ShowUniverses -> keyword "Show Universes"
- | ShowProofNames -> keyword "Show Conjectures"
- | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro")
- | ShowMatch id -> keyword "Show Match " ++ pr_qualid id
- in
- return (pr_showable s)
- | VernacCheckGuard ->
- return (keyword "Guarded")
-
- (* Resetting *)
- | VernacResetName id ->
- return (keyword "Reset" ++ spc() ++ pr_lident id)
- | VernacResetInitial ->
- return (keyword "Reset Initial")
- | VernacBack i ->
- return (
- if Int.equal i 1 then keyword "Back" else keyword "Back" ++ pr_intarg i
- )
-
- (* State management *)
- | VernacWriteState s ->
- return (keyword "Write State" ++ spc () ++ qs s)
- | VernacRestoreState s ->
- return (keyword "Restore State" ++ spc() ++ qs s)
-
- (* Syntax *)
- | VernacOpenCloseScope (opening,sc) ->
- return (
- keyword (if opening then "Open " else "Close ") ++
- keyword "Scope" ++ spc() ++ str sc
- )
- | VernacDeclareScope sc ->
- return (
- keyword "Declare Scope" ++ spc () ++ str sc
- )
- | VernacDelimiters (sc,Some key) ->
- return (
- keyword "Delimit Scope" ++ spc () ++ str sc ++
- spc() ++ keyword "with" ++ spc () ++ str key
- )
- | VernacDelimiters (sc, None) ->
- return (
- keyword "Undelimit Scope" ++ spc () ++ str sc
- )
- | VernacBindScope (sc,cll) ->
- return (
- keyword "Bind Scope" ++ spc () ++ str sc ++
- spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_class_rawexpr cll
- )
- | VernacInfix (({v=s},mv),q,sn) -> (* A Verifier *)
- return (
- hov 0 (hov 0 (keyword "Infix "
- ++ qs s ++ str " :=" ++ pr_constrarg q) ++
- pr_syntax_modifiers mv ++
- (match sn with
- | None -> mt()
- | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
- )
- | VernacNotation (c,({v=s},l),opt) ->
- return (
- hov 2 (keyword "Notation" ++ spc() ++ qs s ++
- str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++
- (match opt with
- | None -> mt()
- | Some sc -> str" :" ++ spc() ++ str sc))
- )
- | VernacSyntaxExtension (_, (s, l)) ->
- return (
- keyword "Reserved Notation" ++ spc() ++ pr_ast qs s ++
- pr_syntax_modifiers l
- )
- | VernacNotationAddFormat(s,k,v) ->
- return (
- keyword "Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v
- )
- | VernacDeclareCustomEntry s ->
- return (
- keyword "Declare Custom Entry " ++ str s
- )
-
- (* Gallina *)
- | VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *)
- let pr_def_token dk =
- keyword (
- if Name.is_anonymous (fst id).v
- then "Goal"
- else string_of_definition_object_kind dk)
- in
- let pr_reduce = function
- | None -> mt()
- | Some r ->
- keyword "Eval" ++ spc() ++
- Ppred.pr_red_expr_env env sigma (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++
- keyword " in" ++ spc()
- in
- let pr_def_body = function
- | DefineBody (bl,red,body,d) ->
- let ty = match d with
+ pr_lconstr_expr env sigma t ++ str" :=" ++ pr_lconstr env sigma b)
+ | None ->
+ hov 1 (pr_lname id ++ str" :=" ++ spc() ++
+ pr_lconstr env sigma b)) in
+ let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in
+ prx ++ prpri ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn
+
+let pr_record_decl c fs =
+ pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++
+ hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")
+
+let pr_printable = function
+ | PrintFullContext ->
+ keyword "Print All"
+ | PrintSectionContext s ->
+ keyword "Print Section" ++ spc() ++ Libnames.pr_qualid s
+ | PrintGrammar ent ->
+ keyword "Print Grammar" ++ spc() ++ str ent
+ | PrintCustomGrammar ent ->
+ keyword "Print Custom Grammar" ++ spc() ++ str ent
+ | PrintLoadPath dir ->
+ keyword "Print LoadPath" ++ pr_opt DirPath.print dir
+ | PrintModules ->
+ keyword "Print Modules"
+ | PrintMLLoadPath ->
+ keyword "Print ML Path"
+ | PrintMLModules ->
+ keyword "Print ML Modules"
+ | PrintDebugGC ->
+ keyword "Print ML GC"
+ | PrintGraph ->
+ keyword "Print Graph"
+ | PrintClasses ->
+ keyword "Print Classes"
+ | PrintTypeClasses ->
+ keyword "Print TypeClasses"
+ | PrintInstances qid ->
+ keyword "Print Instances" ++ spc () ++ pr_smart_global qid
+ | PrintCoercions ->
+ keyword "Print Coercions"
+ | PrintCoercionPaths (s,t) ->
+ keyword "Print Coercion Paths" ++ spc()
+ ++ pr_class_rawexpr s ++ spc()
+ ++ pr_class_rawexpr t
+ | PrintCanonicalConversions qids ->
+ keyword "Print Canonical Structures" ++ prlist pr_smart_global qids
+ | PrintTypingFlags ->
+ keyword "Print Typing Flags"
+ | PrintTables ->
+ keyword "Print Tables"
+ | PrintHintGoal ->
+ keyword "Print Hint"
+ | PrintHint qid ->
+ keyword "Print Hint" ++ spc () ++ pr_smart_global qid
+ | PrintHintDb ->
+ keyword "Print Hint *"
+ | PrintHintDbName s ->
+ keyword "Print HintDb" ++ spc () ++ str s
+ | PrintUniverses (b, g, fopt) ->
+ let cmd =
+ if b then "Print Sorted Universes"
+ else "Print Universes"
+ in
+ let pr_subgraph = prlist_with_sep spc pr_qualid in
+ keyword cmd ++ pr_opt pr_subgraph g ++ pr_opt str fopt
+ | PrintName (qid,udecl) ->
+ keyword "Print" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list udecl
+ | PrintModuleType qid ->
+ keyword "Print Module Type" ++ spc() ++ pr_qualid qid
+ | PrintModule qid ->
+ keyword "Print Module" ++ spc() ++ pr_qualid qid
+ | PrintInspect n ->
+ keyword "Inspect" ++ spc() ++ int n
+ | PrintScopes ->
+ keyword "Print Scopes"
+ | PrintScope s ->
+ keyword "Print Scope" ++ spc() ++ str s
+ | PrintVisibility s ->
+ keyword "Print Visibility" ++ pr_opt str s
+ | PrintAbout (qid,l,gopt) ->
+ pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt
+ ++ keyword "About" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list l
+ | PrintImplicit qid ->
+ keyword "Print Implicit" ++ spc() ++ pr_smart_global qid
+ (* spiwack: command printing all the axioms and section variables used in a
+ term *)
+ | PrintAssumptions (b, t, qid) ->
+ let cmd = match b, t with
+ | true, true -> "Print All Dependencies"
+ | true, false -> "Print Opaque Dependencies"
+ | false, true -> "Print Transparent Dependencies"
+ | false, false -> "Print Assumptions"
+ in
+ keyword cmd ++ spc() ++ pr_smart_global qid
+ | PrintNamespace dp ->
+ keyword "Print Namespace" ++ DirPath.print dp
+ | PrintStrategy None ->
+ keyword "Print Strategies"
+ | PrintStrategy (Some qid) ->
+ keyword "Print Strategy" ++ pr_smart_global qid
+ | PrintRegistered ->
+ keyword "Print Registered"
+
+let pr_using e =
+ let rec aux = function
+ | SsEmpty -> "()"
+ | SsType -> "(Type)"
+ | SsSingl { v=id } -> "("^Id.to_string id^")"
+ | SsCompl e -> "-" ^ aux e^""
+ | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")"
+ | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")"
+ | SsFwdClose e -> "("^aux e^")*"
+ in Pp.str (aux e)
+
+let pr_extend s cl =
+ let pr_arg a =
+ try pr_gen a
+ with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in
+ try
+ let rl = Egramml.get_extend_vernac_rule s in
+ let rec aux rl cl =
+ match rl, cl with
+ | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl
+ | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl
+ | [], [] -> []
+ | _ -> assert false in
+ hov 1 (pr_sequence identity (aux rl cl))
+ with Not_found ->
+ hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")
+
+let pr_vernac_expr v =
+ let return = tag_vernac v in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ match v with
+ | VernacLoad (f,s) ->
+ return (
+ keyword "Load"
+ ++ if f then
+ (spc() ++ keyword "Verbose" ++ spc())
+ else
+ spc() ++ qs s
+ )
+
+ (* Proof management *)
+ | VernacAbortAll ->
+ return (keyword "Abort All")
+ | VernacRestart ->
+ return (keyword "Restart")
+ | VernacUnfocus ->
+ return (keyword "Unfocus")
+ | VernacUnfocused ->
+ return (keyword "Unfocused")
+ | VernacAbort id ->
+ return (keyword "Abort" ++ pr_opt pr_lident id)
+ | VernacUndo i ->
+ return (
+ if Int.equal i 1 then keyword "Undo" else keyword "Undo" ++ pr_intarg i
+ )
+ | VernacUndoTo i ->
+ return (keyword "Undo" ++ spc() ++ keyword "To" ++ pr_intarg i)
+ | VernacFocus i ->
+ return (keyword "Focus" ++ pr_opt int i)
+ | VernacShow s ->
+ let pr_goal_reference = function
+ | OpenSubgoals -> mt ()
+ | NthGoal n -> spc () ++ int n
+ | GoalId id -> spc () ++ pr_id id
+ in
+ let pr_showable = function
+ | ShowGoal n -> keyword "Show" ++ pr_goal_reference n
+ | ShowProof -> keyword "Show Proof"
+ | ShowExistentials -> keyword "Show Existentials"
+ | ShowUniverses -> keyword "Show Universes"
+ | ShowProofNames -> keyword "Show Conjectures"
+ | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro")
+ | ShowMatch id -> keyword "Show Match " ++ pr_qualid id
+ in
+ return (pr_showable s)
+ | VernacCheckGuard ->
+ return (keyword "Guarded")
+
+ (* Resetting *)
+ | VernacResetName id ->
+ return (keyword "Reset" ++ spc() ++ pr_lident id)
+ | VernacResetInitial ->
+ return (keyword "Reset Initial")
+ | VernacBack i ->
+ return (
+ if Int.equal i 1 then keyword "Back" else keyword "Back" ++ pr_intarg i
+ )
+
+ (* State management *)
+ | VernacWriteState s ->
+ return (keyword "Write State" ++ spc () ++ qs s)
+ | VernacRestoreState s ->
+ return (keyword "Restore State" ++ spc() ++ qs s)
+
+ (* Syntax *)
+ | VernacOpenCloseScope (opening,sc) ->
+ return (
+ keyword (if opening then "Open " else "Close ") ++
+ keyword "Scope" ++ spc() ++ str sc
+ )
+ | VernacDeclareScope sc ->
+ return (
+ keyword "Declare Scope" ++ spc () ++ str sc
+ )
+ | VernacDelimiters (sc,Some key) ->
+ return (
+ keyword "Delimit Scope" ++ spc () ++ str sc ++
+ spc() ++ keyword "with" ++ spc () ++ str key
+ )
+ | VernacDelimiters (sc, None) ->
+ return (
+ keyword "Undelimit Scope" ++ spc () ++ str sc
+ )
+ | VernacBindScope (sc,cll) ->
+ return (
+ keyword "Bind Scope" ++ spc () ++ str sc ++
+ spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_class_rawexpr cll
+ )
+ | VernacInfix (({v=s},mv),q,sn) -> (* A Verifier *)
+ return (
+ hov 0 (hov 0 (keyword "Infix "
+ ++ qs s ++ str " :=" ++ pr_constrarg q) ++
+ pr_syntax_modifiers mv ++
+ (match sn with
| None -> mt()
- | Some ty -> spc() ++ str":" ++ pr_spc_lconstr ty
- in
- (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr env sigma body))
- | ProveBody (bl,t) ->
- let typ u = if (fst id).v = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in
- (pr_binders_arg bl, typ (pr_spc_lconstr t), None) in
- let (binds,typ,c) = pr_def_body b in
- return (
- hov 2 (
- pr_def_token kind ++ spc()
- ++ pr_lname_decl id ++ binds ++ typ
- ++ (match c with
+ | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
+ )
+ | VernacNotation (c,({v=s},l),opt) ->
+ return (
+ hov 2 (keyword "Notation" ++ spc() ++ qs s ++
+ str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++
+ (match opt with
| None -> mt()
- | Some cc -> str" :=" ++ spc() ++ cc))
- )
-
- | VernacStartTheoremProof (ki,l) ->
- return (
- hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
- prlist (pr_statement (spc () ++ keyword "with")) (List.tl l))
- )
-
- | VernacEndProof Admitted ->
- return (keyword "Admitted")
-
- | VernacEndProof (Proved (opac,o)) -> return (
- match o with
- | None -> (match opac with
- | Transparent -> keyword "Defined"
- | Opaque -> keyword "Qed")
- | Some id -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
- )
- | VernacExactProof c ->
- return (hov 2 (keyword "Proof" ++ pr_lconstrarg c))
- | VernacAssumption ((discharge,kind),t,l) ->
- let n = List.length (List.flatten (List.map fst (List.map snd l))) in
- let pr_params (c, (xl, t)) =
- hov 2 (prlist_with_sep sep pr_ident_decl xl ++ spc() ++
- (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr env sigma t)) in
- let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in
- return (hov 2 (pr_assumption_token (n > 1) discharge kind ++
- pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions))
- | VernacInductive (f,l) ->
- let pr_constructor (coe,(id,c)) =
- hov 2 (pr_lident id ++ str" " ++
- (if coe then str":>" else str":") ++
- Flags.without_option Flags.beautify pr_spc_lconstr c)
- in
- let pr_constructor_list l = match l with
- | Constructors [] -> mt()
- | Constructors l ->
- let fst_sep = match l with [_] -> " " | _ -> " | " in
- pr_com_at (begin_of_inductive l) ++
- fnl() ++ str fst_sep ++
- prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l
- | RecordDecl (c,fs) ->
- pr_record_decl c fs
- in
- let pr_oneind key (((coe,iddecl),(indupar,indpar),s,lc),ntn) =
- hov 0 (
- str key ++ spc() ++
- (if coe then str"> " else str"") ++ pr_ident_decl iddecl ++
- pr_and_type_binders_arg indupar ++
- pr_opt (fun p -> str "|" ++ spc() ++ pr_and_type_binders_arg p) indpar ++
- pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr env sigma s) s ++
- str" :=") ++ pr_constructor_list lc ++
- prlist (pr_decl_notation @@ pr_constr env sigma) ntn
- in
- let kind =
- match f with
- | Record -> "Record" | Structure -> "Structure"
- | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
- | Class _ -> "Class" | Variant -> "Variant"
- in
- return (
- hov 1 (pr_oneind kind (List.hd l)) ++
- (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
- )
-
- | VernacFixpoint (local, recs) ->
- let local = match local with
- | DoDischarge -> "Let "
- | NoDischarge -> ""
- in
- return (
- hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++
- prlist_with_sep (fun _ -> fnl () ++ keyword "with"
- ++ spc ()) pr_rec_definition recs)
- )
-
- | VernacCoFixpoint (local, corecs) ->
- let local = match local with
- | DoDischarge -> keyword "Let" ++ spc ()
- | NoDischarge -> str ""
- in
- let pr_onecorec {fname; univs; binders; rtype; body_def; notations } =
- pr_ident_decl (fname,univs) ++ spc() ++ pr_binders env sigma binders ++ spc() ++ str":" ++
- spc() ++ pr_lconstr_expr env sigma rtype ++
- pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr env sigma def) body_def ++
- prlist (pr_decl_notation @@ pr_constr env sigma) notations
- in
- return (
- hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++
- prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs)
- )
- | VernacScheme l ->
- return (
- hov 2 (keyword "Scheme" ++ spc() ++
- prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onescheme l)
- )
- | VernacCombinedScheme (id, l) ->
- return (
- hov 2 (keyword "Combined Scheme" ++ spc() ++
- pr_lident id ++ spc() ++ keyword "from" ++ spc() ++
- prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l)
- )
- | VernacUniverse v ->
- return (
- hov 2 (keyword "Universe" ++ spc () ++
- prlist_with_sep (fun _ -> str",") pr_lident v)
- )
- | VernacConstraint v ->
- return (
- hov 2 (keyword "Constraint" ++ spc () ++
- prlist_with_sep (fun _ -> str",") pr_uconstraint v)
- )
-
- (* Gallina extensions *)
- | VernacBeginSection id ->
- return (hov 2 (keyword "Section" ++ spc () ++ pr_lident id))
- | VernacEndSegment id ->
- return (hov 2 (keyword "End" ++ spc() ++ pr_lident id))
- | VernacNameSectionHypSet (id,set) ->
- return (hov 2 (keyword "Package" ++ spc() ++ pr_lident id ++ spc()++
- str ":="++spc()++pr_using set))
- | VernacRequire (from, exp, l) ->
- let from = match from with
- | None -> mt ()
- | Some r -> keyword "From" ++ spc () ++ pr_module r ++ spc ()
+ | Some sc -> str" :" ++ spc() ++ str sc))
+ )
+ | VernacSyntaxExtension (_, (s, l)) ->
+ return (
+ keyword "Reserved Notation" ++ spc() ++ pr_ast qs s ++
+ pr_syntax_modifiers l
+ )
+ | VernacNotationAddFormat(s,k,v) ->
+ return (
+ keyword "Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v
+ )
+ | VernacDeclareCustomEntry s ->
+ return (
+ keyword "Declare Custom Entry " ++ str s
+ )
+
+ (* Gallina *)
+ | VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *)
+ let pr_def_token dk =
+ keyword (
+ if Name.is_anonymous (fst id).v
+ then "Goal"
+ else string_of_definition_object_kind dk)
+ in
+ let pr_reduce = function
+ | None -> mt()
+ | Some r ->
+ keyword "Eval" ++ spc() ++
+ Ppred.pr_red_expr_env env sigma (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++
+ keyword " in" ++ spc()
+ in
+ let pr_def_body = function
+ | DefineBody (bl,red,body,d) ->
+ let ty = match d with
+ | None -> mt()
+ | Some ty -> spc() ++ str":" ++ pr_spc_lconstr ty
in
- return (
- hov 2
- (from ++ keyword "Require" ++ spc() ++ pr_require_token exp ++
- prlist_with_sep sep pr_module l)
- )
- | VernacImport (f,l) ->
- return (
- (if f then keyword "Export" else keyword "Import") ++ spc() ++
- prlist_with_sep sep pr_import_module l
- )
- | VernacCanonical q ->
- return (
- keyword "Canonical Structure" ++ spc() ++ pr_smart_global q
- )
- | VernacCoercion (id,c1,c2) ->
- return (
- hov 1 (
- keyword "Coercion" ++ spc() ++
- pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++
- spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2)
- )
- | VernacIdentityCoercion (id,c1,c2) ->
- return (
- hov 1 (
- keyword "Identity Coercion" ++ spc() ++ pr_lident id ++
- spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
- spc() ++ pr_class_rawexpr c2)
- )
-
- | VernacInstance (instid, sup, cl, props, info) ->
- return (
- hov 1 (
- keyword "Instance" ++
- (match instid with
- | {loc; v = Name id}, l -> spc () ++ pr_ident_decl (CAst.(make ?loc id),l) ++ spc ()
- | { v = Anonymous }, _ -> mt ()) ++
- pr_and_type_binders_arg sup ++
- str":" ++ spc () ++
- pr_constr env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info ++
- (match props with
- | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}"
- | Some (true,_) -> assert false
- | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr env sigma p
- | None -> mt()))
- )
-
- | VernacDeclareInstance (instid, sup, cl, info) ->
- return (
- hov 1 (
- keyword "Declare Instance" ++ spc () ++ pr_ident_decl instid ++ spc () ++
- pr_and_type_binders_arg sup ++
- str":" ++ spc () ++
- pr_constr env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info)
- )
-
- | VernacContext l ->
- return (
- hov 1 (
- keyword "Context" ++ pr_and_type_binders_arg l)
- )
-
- | VernacExistingInstance insts ->
- let pr_inst (id, info) =
- pr_qualid id ++ pr_hint_info (pr_constr_pattern_expr env sigma) info
- in
- return (
- hov 1 (keyword "Existing" ++ spc () ++
- keyword(String.plural (List.length insts) "Instance") ++
- spc () ++ prlist_with_sep (fun () -> str", ") pr_inst insts)
- )
-
- | VernacExistingClass id ->
- return (
- hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_qualid id)
- )
-
- (* Modules and Module Types *)
- | VernacDefineModule (export,m,bl,tys,bd) ->
- let b = pr_module_binders bl (pr_lconstr env sigma) in
- return (
- hov 2 (keyword "Module" ++ spc() ++ pr_require_token export ++
- pr_lident m ++ b ++
- pr_of_module_type (pr_lconstr env sigma) tys ++
- (if List.is_empty bd then mt () else str ":= ") ++
- prlist_with_sep (fun () -> str " <+")
- (pr_module_ast_inl true (pr_lconstr env sigma)) bd)
- )
- | VernacDeclareModule (export,id,bl,m1) ->
- let b = pr_module_binders bl (pr_lconstr env sigma) in
- return (
- hov 2 (keyword "Declare Module" ++ spc() ++ pr_require_token export ++
- pr_lident id ++ b ++ str " :" ++
- pr_module_ast_inl true (pr_lconstr env sigma) m1)
- )
- | VernacDeclareModuleType (id,bl,tyl,m) ->
- let b = pr_module_binders bl (pr_lconstr env sigma) in
- let pr_mt = pr_module_ast_inl true (pr_lconstr env sigma) in
- return (
- hov 2 (keyword "Module Type " ++ pr_lident id ++ b ++
- prlist_strict (fun m -> str " <:" ++ pr_mt m) tyl ++
- (if List.is_empty m then mt () else str ":= ") ++
- prlist_with_sep (fun () -> str " <+ ") pr_mt m)
- )
- | VernacInclude (mexprs) ->
- let pr_m = pr_module_ast_inl false (pr_lconstr env sigma) in
- return (
- hov 2 (keyword "Include" ++ spc() ++
- prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
- )
- (* Solving *)
- | VernacSolveExistential (i,c) ->
- return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c)
-
- (* Auxiliary file and library management *)
- | VernacAddLoadPath { implicit; physical_path; logical_path } ->
- return (
- hov 2
- (keyword "Add" ++
- (if implicit then spc () ++ keyword "Rec" ++ spc () else spc()) ++
- keyword "LoadPath" ++ spc() ++ qs physical_path ++
- spc() ++ keyword "as" ++ spc() ++ DirPath.print logical_path))
- | VernacRemoveLoadPath s ->
- return (keyword "Remove LoadPath" ++ qs s)
- | VernacAddMLPath (s) ->
- return (
- keyword "Add"
- ++ keyword "ML Path"
- ++ qs s
- )
- | VernacDeclareMLModule (l) ->
- return (
- hov 2 (keyword "Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
- )
- | VernacChdir s ->
- return (keyword "Cd" ++ pr_opt qs s)
-
- (* Commands *)
- | VernacCreateHintDb (dbname,b) ->
- return (
- hov 1 (keyword "Create HintDb" ++ spc () ++
- str dbname ++ (if b then str" discriminated" else mt ()))
- )
- | VernacRemoveHints (dbnames, ids) ->
- return (
- hov 1 (keyword "Remove Hints" ++ spc () ++
- prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++
- pr_opt_hintbases dbnames)
- )
- | VernacHints (dbnames,h) ->
- return (pr_hints dbnames h (pr_constr env sigma) (pr_constr_pattern_expr env sigma))
- | VernacSyntacticDefinition (id,(ids,c),{onlyparsing}) ->
- return (
- hov 2
- (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++
- prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++
- pr_only_parsing_clause onlyparsing)
- )
- | VernacArguments (q, args, more_implicits, mods) ->
- return (
- hov 2 (
- keyword "Arguments" ++ spc() ++
- pr_smart_global q ++
- let pr_s = function None -> str"" | Some {v=s} -> str "%" ++ str s in
- let pr_if b x = if b then x else str "" in
- let pr_one_arg (x,k) = pr_if k (str"!") ++ Name.print x in
- let pr_br imp force x =
- let left,right =
- match imp with
- | Glob_term.NonMaxImplicit -> str "[", str "]"
- | Glob_term.MaxImplicit -> str "{", str "}"
- | Glob_term.Explicit -> if force then str"(",str")" else mt(),mt()
- in
- left ++ x ++ right
- in
- let get_arguments_like s imp tl =
- if s = None && imp = Glob_term.Explicit then [], tl
- else
- let rec fold extra = function
- | RealArg arg :: tl when
- Option.equal (fun a b -> String.equal a.CAst.v b.CAst.v) arg.notation_scope s
- && arg.implicit_status = imp ->
- fold ((arg.name,arg.recarg_like) :: extra) tl
- | args -> List.rev extra, args
- in
- fold [] tl
- in
- let rec print_arguments = function
- | [] -> mt()
- | VolatileArg :: l -> spc () ++ str"/" ++ print_arguments l
- | BidiArg :: l -> spc () ++ str"&" ++ print_arguments l
- | RealArg { name = id; recarg_like = k;
- notation_scope = s;
- implicit_status = imp } :: tl ->
- let extra, tl = get_arguments_like s imp tl in
- spc() ++ pr_br imp (extra<>[]) (prlist_with_sep spc pr_one_arg ((id,k)::extra)) ++
- pr_s s ++ print_arguments tl
- in
- let rec print_implicits = function
- | [] -> mt ()
- | (name, impl) :: rest ->
- spc() ++ pr_br impl false (Name.print name) ++ print_implicits rest
- in
- print_arguments args ++
- if not (List.is_empty more_implicits) then
- prlist (fun l -> str"," ++ print_implicits l) more_implicits
- else (mt ()) ++
- (if not (List.is_empty mods) then str" : " else str"") ++
- prlist_with_sep (fun () -> str", " ++ spc()) (function
- | `ReductionDontExposeCase -> keyword "simpl nomatch"
- | `ReductionNeverUnfold -> keyword "simpl never"
- | `DefaultImplicits -> keyword "default implicits"
- | `Rename -> keyword "rename"
- | `Assert -> keyword "assert"
- | `ExtraScopes -> keyword "extra scopes"
- | `ClearImplicits -> keyword "clear implicits"
- | `ClearScopes -> keyword "clear scopes"
- | `ClearBidiHint -> keyword "clear bidirectionality hint")
- mods)
- )
- | VernacReserve bl ->
- let n = List.length (List.flatten (List.map fst bl)) in
- return (
- hov 2 (tag_keyword (str"Implicit Type" ++ str (if n > 1 then "s " else " "))
- ++ pr_ne_params_list (pr_lconstr_expr env sigma) (List.map (fun sb -> false,sb) bl))
- )
- | VernacGeneralizable g ->
- return (
- hov 1 (tag_keyword (
- str"Generalizable Variable" ++
- match g with
- | None -> str "s none"
- | Some [] -> str "s all"
- | Some idl ->
- str (if List.length idl > 1 then "s " else " ") ++
- prlist_with_sep spc pr_lident idl)
- ))
- | VernacSetOpacity(k,l) when Conv_oracle.is_transparent k ->
- return (
- hov 1 (keyword "Transparent" ++
- spc() ++ prlist_with_sep sep pr_smart_global l)
- )
- | VernacSetOpacity(Conv_oracle.Opaque,l) ->
- return (
- hov 1 (keyword "Opaque" ++
- spc() ++ prlist_with_sep sep pr_smart_global l)
- )
- | VernacSetOpacity _ ->
- return (
- CErrors.anomaly (keyword "VernacSetOpacity used to set something else.")
- )
- | VernacSetStrategy l ->
- let pr_lev = function
- | Conv_oracle.Opaque -> keyword "opaque"
- | Conv_oracle.Expand -> keyword "expand"
- | l when Conv_oracle.is_transparent l -> keyword "transparent"
- | Conv_oracle.Level n -> int n
+ (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr env sigma body))
+ | ProveBody (bl,t) ->
+ let typ u = if (fst id).v = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in
+ (pr_binders_arg bl, typ (pr_spc_lconstr t), None) in
+ let (binds,typ,c) = pr_def_body b in
+ return (
+ hov 2 (
+ pr_def_token kind ++ spc()
+ ++ pr_lname_decl id ++ binds ++ typ
+ ++ (match c with
+ | None -> mt()
+ | Some cc -> str" :=" ++ spc() ++ cc))
+ )
+
+ | VernacStartTheoremProof (ki,l) ->
+ return (
+ hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
+ prlist (pr_statement (spc () ++ keyword "with")) (List.tl l))
+ )
+
+ | VernacEndProof Admitted ->
+ return (keyword "Admitted")
+
+ | VernacEndProof (Proved (opac,o)) -> return (
+ match o with
+ | None -> (match opac with
+ | Transparent -> keyword "Defined"
+ | Opaque -> keyword "Qed")
+ | Some id -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
+ )
+ | VernacExactProof c ->
+ return (hov 2 (keyword "Proof" ++ pr_lconstrarg c))
+ | VernacAssumption ((discharge,kind),t,l) ->
+ let n = List.length (List.flatten (List.map fst (List.map snd l))) in
+ let pr_params (c, (xl, t)) =
+ hov 2 (prlist_with_sep sep pr_ident_decl xl ++ spc() ++
+ (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr env sigma t)) in
+ let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in
+ return (hov 2 (pr_assumption_token (n > 1) discharge kind ++
+ pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions))
+ | VernacInductive (f,l) ->
+ let pr_constructor (coe,(id,c)) =
+ hov 2 (pr_lident id ++ str" " ++
+ (if coe then str":>" else str":") ++
+ Flags.without_option Flags.beautify pr_spc_lconstr c)
+ in
+ let pr_constructor_list l = match l with
+ | Constructors [] -> mt()
+ | Constructors l ->
+ let fst_sep = match l with [_] -> " " | _ -> " | " in
+ pr_com_at (begin_of_inductive l) ++
+ fnl() ++ str fst_sep ++
+ prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l
+ | RecordDecl (c,fs) ->
+ pr_record_decl c fs
+ in
+ let pr_oneind key (((coe,iddecl),(indupar,indpar),s,lc),ntn) =
+ hov 0 (
+ str key ++ spc() ++
+ (if coe then str"> " else str"") ++ pr_ident_decl iddecl ++
+ pr_and_type_binders_arg indupar ++
+ pr_opt (fun p -> str "|" ++ spc() ++ pr_and_type_binders_arg p) indpar ++
+ pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr env sigma s) s ++
+ str" :=") ++ pr_constructor_list lc ++
+ prlist (pr_decl_notation @@ pr_constr env sigma) ntn
+ in
+ let kind =
+ match f with
+ | Record -> "Record" | Structure -> "Structure"
+ | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
+ | Class _ -> "Class" | Variant -> "Variant"
+ in
+ return (
+ hov 1 (pr_oneind kind (List.hd l)) ++
+ (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
+ )
+
+ | VernacFixpoint (local, recs) ->
+ let local = match local with
+ | DoDischarge -> "Let "
+ | NoDischarge -> ""
+ in
+ return (
+ hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++
+ prlist_with_sep (fun _ -> fnl () ++ keyword "with"
+ ++ spc ()) pr_rec_definition recs)
+ )
+
+ | VernacCoFixpoint (local, corecs) ->
+ let local = match local with
+ | DoDischarge -> keyword "Let" ++ spc ()
+ | NoDischarge -> str ""
+ in
+ let pr_onecorec {fname; univs; binders; rtype; body_def; notations } =
+ pr_ident_decl (fname,univs) ++ spc() ++ pr_binders env sigma binders ++ spc() ++ str":" ++
+ spc() ++ pr_lconstr_expr env sigma rtype ++
+ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr env sigma def) body_def ++
+ prlist (pr_decl_notation @@ pr_constr env sigma) notations
+ in
+ return (
+ hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++
+ prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs)
+ )
+ | VernacScheme l ->
+ return (
+ hov 2 (keyword "Scheme" ++ spc() ++
+ prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onescheme l)
+ )
+ | VernacCombinedScheme (id, l) ->
+ return (
+ hov 2 (keyword "Combined Scheme" ++ spc() ++
+ pr_lident id ++ spc() ++ keyword "from" ++ spc() ++
+ prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l)
+ )
+ | VernacUniverse v ->
+ return (
+ hov 2 (keyword "Universe" ++ spc () ++
+ prlist_with_sep (fun _ -> str",") pr_lident v)
+ )
+ | VernacConstraint v ->
+ return (
+ hov 2 (keyword "Constraint" ++ spc () ++
+ prlist_with_sep (fun _ -> str",") pr_uconstraint v)
+ )
+
+ (* Gallina extensions *)
+ | VernacBeginSection id ->
+ return (hov 2 (keyword "Section" ++ spc () ++ pr_lident id))
+ | VernacEndSegment id ->
+ return (hov 2 (keyword "End" ++ spc() ++ pr_lident id))
+ | VernacNameSectionHypSet (id,set) ->
+ return (hov 2 (keyword "Package" ++ spc() ++ pr_lident id ++ spc()++
+ str ":="++spc()++pr_using set))
+ | VernacRequire (from, exp, l) ->
+ let from = match from with
+ | None -> mt ()
+ | Some r -> keyword "From" ++ spc () ++ pr_module r ++ spc ()
+ in
+ return (
+ hov 2
+ (from ++ keyword "Require" ++ spc() ++ pr_require_token exp ++
+ prlist_with_sep sep pr_module l)
+ )
+ | VernacImport (f,l) ->
+ return (
+ (if f then keyword "Export" else keyword "Import") ++ spc() ++
+ prlist_with_sep sep pr_import_module l
+ )
+ | VernacCanonical q ->
+ return (
+ keyword "Canonical Structure" ++ spc() ++ pr_smart_global q
+ )
+ | VernacCoercion (id,c1,c2) ->
+ return (
+ hov 1 (
+ keyword "Coercion" ++ spc() ++
+ pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++
+ spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2)
+ )
+ | VernacIdentityCoercion (id,c1,c2) ->
+ return (
+ hov 1 (
+ keyword "Identity Coercion" ++ spc() ++ pr_lident id ++
+ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
+ spc() ++ pr_class_rawexpr c2)
+ )
+
+ | VernacInstance (instid, sup, cl, props, info) ->
+ return (
+ hov 1 (
+ keyword "Instance" ++
+ (match instid with
+ | {loc; v = Name id}, l -> spc () ++ pr_ident_decl (CAst.(make ?loc id),l) ++ spc ()
+ | { v = Anonymous }, _ -> mt ()) ++
+ pr_and_type_binders_arg sup ++
+ str":" ++ spc () ++
+ pr_constr env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info ++
+ (match props with
+ | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}"
+ | Some (true,_) -> assert false
+ | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr env sigma p
+ | None -> mt()))
+ )
+
+ | VernacDeclareInstance (instid, sup, cl, info) ->
+ return (
+ hov 1 (
+ keyword "Declare Instance" ++ spc () ++ pr_ident_decl instid ++ spc () ++
+ pr_and_type_binders_arg sup ++
+ str":" ++ spc () ++
+ pr_constr env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info)
+ )
+
+ | VernacContext l ->
+ return (
+ hov 1 (
+ keyword "Context" ++ pr_and_type_binders_arg l)
+ )
+
+ | VernacExistingInstance insts ->
+ let pr_inst (id, info) =
+ pr_qualid id ++ pr_hint_info (pr_constr_pattern_expr env sigma) info
+ in
+ return (
+ hov 1 (keyword "Existing" ++ spc () ++
+ keyword(String.plural (List.length insts) "Instance") ++
+ spc () ++ prlist_with_sep (fun () -> str", ") pr_inst insts)
+ )
+
+ | VernacExistingClass id ->
+ return (
+ hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_qualid id)
+ )
+
+ (* Modules and Module Types *)
+ | VernacDefineModule (export,m,bl,tys,bd) ->
+ let b = pr_module_binders bl (pr_lconstr env sigma) in
+ return (
+ hov 2 (keyword "Module" ++ spc() ++ pr_require_token export ++
+ pr_lident m ++ b ++
+ pr_of_module_type (pr_lconstr env sigma) tys ++
+ (if List.is_empty bd then mt () else str ":= ") ++
+ prlist_with_sep (fun () -> str " <+")
+ (pr_module_ast_inl true (pr_lconstr env sigma)) bd)
+ )
+ | VernacDeclareModule (export,id,bl,m1) ->
+ let b = pr_module_binders bl (pr_lconstr env sigma) in
+ return (
+ hov 2 (keyword "Declare Module" ++ spc() ++ pr_require_token export ++
+ pr_lident id ++ b ++ str " :" ++
+ pr_module_ast_inl true (pr_lconstr env sigma) m1)
+ )
+ | VernacDeclareModuleType (id,bl,tyl,m) ->
+ let b = pr_module_binders bl (pr_lconstr env sigma) in
+ let pr_mt = pr_module_ast_inl true (pr_lconstr env sigma) in
+ return (
+ hov 2 (keyword "Module Type " ++ pr_lident id ++ b ++
+ prlist_strict (fun m -> str " <:" ++ pr_mt m) tyl ++
+ (if List.is_empty m then mt () else str ":= ") ++
+ prlist_with_sep (fun () -> str " <+ ") pr_mt m)
+ )
+ | VernacInclude (mexprs) ->
+ let pr_m = pr_module_ast_inl false (pr_lconstr env sigma) in
+ return (
+ hov 2 (keyword "Include" ++ spc() ++
+ prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
+ )
+ (* Solving *)
+ | VernacSolveExistential (i,c) ->
+ return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c)
+
+ (* Auxiliary file and library management *)
+ | VernacAddLoadPath { implicit; physical_path; logical_path } ->
+ return (
+ hov 2
+ (keyword "Add" ++
+ (if implicit then spc () ++ keyword "Rec" ++ spc () else spc()) ++
+ keyword "LoadPath" ++ spc() ++ qs physical_path ++
+ spc() ++ keyword "as" ++ spc() ++ DirPath.print logical_path))
+ | VernacRemoveLoadPath s ->
+ return (keyword "Remove LoadPath" ++ qs s)
+ | VernacAddMLPath (s) ->
+ return (
+ keyword "Add"
+ ++ keyword "ML Path"
+ ++ qs s
+ )
+ | VernacDeclareMLModule (l) ->
+ return (
+ hov 2 (keyword "Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
+ )
+ | VernacChdir s ->
+ return (keyword "Cd" ++ pr_opt qs s)
+
+ (* Commands *)
+ | VernacCreateHintDb (dbname,b) ->
+ return (
+ hov 1 (keyword "Create HintDb" ++ spc () ++
+ str dbname ++ (if b then str" discriminated" else mt ()))
+ )
+ | VernacRemoveHints (dbnames, ids) ->
+ return (
+ hov 1 (keyword "Remove Hints" ++ spc () ++
+ prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++
+ pr_opt_hintbases dbnames)
+ )
+ | VernacHints (dbnames,h) ->
+ return (pr_hints dbnames h (pr_constr env sigma) (pr_constr_pattern_expr env sigma))
+ | VernacSyntacticDefinition (id,(ids,c),{onlyparsing}) ->
+ return (
+ hov 2
+ (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++
+ prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++
+ pr_only_parsing_clause onlyparsing)
+ )
+ | VernacArguments (q, args, more_implicits, mods) ->
+ return (
+ hov 2 (
+ keyword "Arguments" ++ spc() ++
+ pr_smart_global q ++
+ let pr_s = function None -> str"" | Some {v=s} -> str "%" ++ str s in
+ let pr_if b x = if b then x else str "" in
+ let pr_one_arg (x,k) = pr_if k (str"!") ++ Name.print x in
+ let pr_br imp force x =
+ let left,right =
+ match imp with
+ | Glob_term.NonMaxImplicit -> str "[", str "]"
+ | Glob_term.MaxImplicit -> str "{", str "}"
+ | Glob_term.Explicit -> if force then str"(",str")" else mt(),mt()
+ in
+ left ++ x ++ right
in
- let pr_line (l,q) =
- hov 2 (pr_lev l ++ spc() ++
- str"[" ++ prlist_with_sep sep pr_smart_global q ++ str"]")
+ let get_arguments_like s imp tl =
+ if s = None && imp = Glob_term.Explicit then [], tl
+ else
+ let rec fold extra = function
+ | RealArg arg :: tl when
+ Option.equal (fun a b -> String.equal a.CAst.v b.CAst.v) arg.notation_scope s
+ && arg.implicit_status = imp ->
+ fold ((arg.name,arg.recarg_like) :: extra) tl
+ | args -> List.rev extra, args
+ in
+ fold [] tl
in
- return (
- hov 1 (keyword "Strategy" ++ spc() ++
- hv 0 (prlist_with_sep sep pr_line l))
- )
- | VernacSetOption (export, na,v) ->
- let export = if export then keyword "Export" ++ spc () else mt () in
- let set = if v == OptionUnset then "Unset" else "Set" in
- return (
- hov 2 (export ++ keyword set ++ spc() ++ pr_set_option na v)
- )
- | VernacAddOption (na,l) ->
- return (
- hov 2 (keyword "Add" ++ spc() ++ pr_printoption na (Some l))
- )
- | VernacRemoveOption (na,l) ->
- return (
- hov 2 (keyword "Remove" ++ spc() ++ pr_printoption na (Some l))
- )
- | VernacMemOption (na,l) ->
- return (
- hov 2 (keyword "Test" ++ spc() ++ pr_printoption na (Some l))
- )
- | VernacPrintOption na ->
- return (
- hov 2 (keyword "Test" ++ spc() ++ pr_printoption na None)
- )
- | VernacCheckMayEval (r,io,c) ->
- let pr_mayeval r c = match r with
- | Some r0 ->
- hov 2 (keyword "Eval" ++ spc() ++
- Ppred.pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++
- spc() ++ keyword "in" ++ spc () ++ pr_lconstr env sigma c)
- | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr env sigma c)
+ let rec print_arguments = function
+ | [] -> mt()
+ | VolatileArg :: l -> spc () ++ str"/" ++ print_arguments l
+ | BidiArg :: l -> spc () ++ str"&" ++ print_arguments l
+ | RealArg { name = id; recarg_like = k;
+ notation_scope = s;
+ implicit_status = imp } :: tl ->
+ let extra, tl = get_arguments_like s imp tl in
+ spc() ++ pr_br imp (extra<>[]) (prlist_with_sep spc pr_one_arg ((id,k)::extra)) ++
+ pr_s s ++ print_arguments tl
in
- let pr_i = match io with None -> mt ()
- | Some i -> Goal_select.pr_goal_selector i ++ str ": " in
- return (pr_i ++ pr_mayeval r c)
- | VernacGlobalCheck c ->
- return (hov 2 (keyword "Type" ++ pr_constrarg c))
- | VernacDeclareReduction (s,r) ->
- return (
- keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++
- Ppred.pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r
- )
- | VernacPrint p ->
- return (pr_printable p)
- | VernacSearch (sea,g,sea_r) ->
- return (pr_search sea g sea_r @@ pr_constr_pattern_expr env sigma)
- | VernacLocate loc ->
- let pr_locate =function
- | LocateAny qid -> pr_smart_global qid
- | LocateTerm qid -> keyword "Term" ++ spc() ++ pr_smart_global qid
- | LocateFile f -> keyword "File" ++ spc() ++ qs f
- | LocateLibrary qid -> keyword "Library" ++ spc () ++ pr_module qid
- | LocateModule qid -> keyword "Module" ++ spc () ++ pr_module qid
- | LocateOther (s, qid) -> keyword s ++ spc () ++ pr_ltac_ref qid
+ let rec print_implicits = function
+ | [] -> mt ()
+ | (name, impl) :: rest ->
+ spc() ++ pr_br impl false (Name.print name) ++ print_implicits rest
in
- return (keyword "Locate" ++ spc() ++ pr_locate loc)
- | VernacRegister (qid, RegisterCoqlib name) ->
- return (
- hov 2
- (keyword "Register" ++ spc() ++ pr_qualid qid ++ spc () ++ str "as"
- ++ spc () ++ pr_qualid name)
- )
- | VernacRegister (qid, RegisterInline) ->
- return (
- hov 2
- (keyword "Register Inline" ++ spc() ++ pr_qualid qid)
- )
- | VernacPrimitive(id,r,typopt) ->
- hov 2
- (keyword "Primitive" ++ spc() ++ pr_lident id ++
- (Option.cata (fun ty -> spc() ++ str":" ++ pr_spc_lconstr ty) (mt()) typopt) ++ spc() ++
- str ":=" ++ spc() ++
- str (CPrimitives.op_or_type_to_string r))
- | VernacComments l ->
- return (
- hov 2
- (keyword "Comments" ++ spc()
- ++ prlist_with_sep sep (pr_comment (pr_constr env sigma)) l)
- )
-
- (* For extension *)
- | VernacExtend (s,c) ->
- return (pr_extend s c)
- | VernacProof (None, None) ->
- return (keyword "Proof")
- | VernacProof (None, Some e) ->
- return (keyword "Proof " ++ spc () ++
+ print_arguments args ++
+ if not (List.is_empty more_implicits) then
+ prlist (fun l -> str"," ++ print_implicits l) more_implicits
+ else (mt ()) ++
+ (if not (List.is_empty mods) then str" : " else str"") ++
+ prlist_with_sep (fun () -> str", " ++ spc()) (function
+ | `ReductionDontExposeCase -> keyword "simpl nomatch"
+ | `ReductionNeverUnfold -> keyword "simpl never"
+ | `DefaultImplicits -> keyword "default implicits"
+ | `Rename -> keyword "rename"
+ | `Assert -> keyword "assert"
+ | `ExtraScopes -> keyword "extra scopes"
+ | `ClearImplicits -> keyword "clear implicits"
+ | `ClearScopes -> keyword "clear scopes"
+ | `ClearBidiHint -> keyword "clear bidirectionality hint")
+ mods)
+ )
+ | VernacReserve bl ->
+ let n = List.length (List.flatten (List.map fst bl)) in
+ return (
+ hov 2 (tag_keyword (str"Implicit Type" ++ str (if n > 1 then "s " else " "))
+ ++ pr_ne_params_list (pr_lconstr_expr env sigma) (List.map (fun sb -> false,sb) bl))
+ )
+ | VernacGeneralizable g ->
+ return (
+ hov 1 (tag_keyword (
+ str"Generalizable Variable" ++
+ match g with
+ | None -> str "s none"
+ | Some [] -> str "s all"
+ | Some idl ->
+ str (if List.length idl > 1 then "s " else " ") ++
+ prlist_with_sep spc pr_lident idl)
+ ))
+ | VernacSetOpacity(k,l) when Conv_oracle.is_transparent k ->
+ return (
+ hov 1 (keyword "Transparent" ++
+ spc() ++ prlist_with_sep sep pr_smart_global l)
+ )
+ | VernacSetOpacity(Conv_oracle.Opaque,l) ->
+ return (
+ hov 1 (keyword "Opaque" ++
+ spc() ++ prlist_with_sep sep pr_smart_global l)
+ )
+ | VernacSetOpacity _ ->
+ return (
+ CErrors.anomaly (keyword "VernacSetOpacity used to set something else.")
+ )
+ | VernacSetStrategy l ->
+ let pr_lev = function
+ | Conv_oracle.Opaque -> keyword "opaque"
+ | Conv_oracle.Expand -> keyword "expand"
+ | l when Conv_oracle.is_transparent l -> keyword "transparent"
+ | Conv_oracle.Level n -> int n
+ in
+ let pr_line (l,q) =
+ hov 2 (pr_lev l ++ spc() ++
+ str"[" ++ prlist_with_sep sep pr_smart_global q ++ str"]")
+ in
+ return (
+ hov 1 (keyword "Strategy" ++ spc() ++
+ hv 0 (prlist_with_sep sep pr_line l))
+ )
+ | VernacSetOption (export, na,v) ->
+ let export = if export then keyword "Export" ++ spc () else mt () in
+ let set = if v == OptionUnset then "Unset" else "Set" in
+ return (
+ hov 2 (export ++ keyword set ++ spc() ++ pr_set_option na v)
+ )
+ | VernacAddOption (na,l) ->
+ return (
+ hov 2 (keyword "Add" ++ spc() ++ pr_printoption na (Some l))
+ )
+ | VernacRemoveOption (na,l) ->
+ return (
+ hov 2 (keyword "Remove" ++ spc() ++ pr_printoption na (Some l))
+ )
+ | VernacMemOption (na,l) ->
+ return (
+ hov 2 (keyword "Test" ++ spc() ++ pr_printoption na (Some l))
+ )
+ | VernacPrintOption na ->
+ return (
+ hov 2 (keyword "Test" ++ spc() ++ pr_printoption na None)
+ )
+ | VernacCheckMayEval (r,io,c) ->
+ let pr_mayeval r c = match r with
+ | Some r0 ->
+ hov 2 (keyword "Eval" ++ spc() ++
+ Ppred.pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++
+ spc() ++ keyword "in" ++ spc () ++ pr_lconstr env sigma c)
+ | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr env sigma c)
+ in
+ let pr_i = match io with None -> mt ()
+ | Some i -> Goal_select.pr_goal_selector i ++ str ": " in
+ return (pr_i ++ pr_mayeval r c)
+ | VernacGlobalCheck c ->
+ return (hov 2 (keyword "Type" ++ pr_constrarg c))
+ | VernacDeclareReduction (s,r) ->
+ return (
+ keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++
+ Ppred.pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r
+ )
+ | VernacPrint p ->
+ return (pr_printable p)
+ | VernacSearch (sea,g,sea_r) ->
+ return (pr_search sea g sea_r @@ pr_constr_pattern_expr env sigma)
+ | VernacLocate loc ->
+ let pr_locate =function
+ | LocateAny qid -> pr_smart_global qid
+ | LocateTerm qid -> keyword "Term" ++ spc() ++ pr_smart_global qid
+ | LocateFile f -> keyword "File" ++ spc() ++ qs f
+ | LocateLibrary qid -> keyword "Library" ++ spc () ++ pr_module qid
+ | LocateModule qid -> keyword "Module" ++ spc () ++ pr_module qid
+ | LocateOther (s, qid) -> keyword s ++ spc () ++ pr_ltac_ref qid
+ in
+ return (keyword "Locate" ++ spc() ++ pr_locate loc)
+ | VernacRegister (qid, RegisterCoqlib name) ->
+ return (
+ hov 2
+ (keyword "Register" ++ spc() ++ pr_qualid qid ++ spc () ++ str "as"
+ ++ spc () ++ pr_qualid name)
+ )
+ | VernacRegister (qid, RegisterInline) ->
+ return (
+ hov 2
+ (keyword "Register Inline" ++ spc() ++ pr_qualid qid)
+ )
+ | VernacPrimitive(id,r,typopt) ->
+ hov 2
+ (keyword "Primitive" ++ spc() ++ pr_ident_decl id ++
+ (Option.cata (fun ty -> spc() ++ str":" ++ pr_spc_lconstr ty) (mt()) typopt) ++ spc() ++
+ str ":=" ++ spc() ++
+ str (CPrimitives.op_or_type_to_string r))
+ | VernacComments l ->
+ return (
+ hov 2
+ (keyword "Comments" ++ spc()
+ ++ prlist_with_sep sep (pr_comment (pr_constr env sigma)) l)
+ )
+
+ (* For extension *)
+ | VernacExtend (s,c) ->
+ return (pr_extend s c)
+ | VernacProof (None, None) ->
+ return (keyword "Proof")
+ | VernacProof (None, Some e) ->
+ return (keyword "Proof " ++ spc () ++
keyword "using" ++ spc() ++ pr_using e)
- | VernacProof (Some te, None) ->
- return (keyword "Proof with" ++ spc() ++ Pputils.pr_raw_generic env sigma te)
- | VernacProof (Some te, Some e) ->
- return (
- keyword "Proof" ++ spc () ++
- keyword "using" ++ spc() ++ pr_using e ++ spc() ++
- keyword "with" ++ spc() ++ Pputils.pr_raw_generic env sigma te
- )
- | VernacProofMode s ->
- return (keyword "Proof Mode" ++ str s)
- | VernacBullet b ->
- (* XXX: Redundant with Proof_bullet.print *)
- return (let open Proof_bullet in begin match b with
- | Dash n -> str (String.make n '-')
- | Star n -> str (String.make n '*')
- | Plus n -> str (String.make n '+')
- end)
- | VernacSubproof None ->
- return (str "{")
- | VernacSubproof (Some i) ->
- return (Goal_select.pr_goal_selector i ++ str ":" ++ spc () ++ str "{")
- | VernacEndSubproof ->
- return (str "}")
+ | VernacProof (Some te, None) ->
+ return (keyword "Proof with" ++ spc() ++ Pputils.pr_raw_generic env sigma te)
+ | VernacProof (Some te, Some e) ->
+ return (
+ keyword "Proof" ++ spc () ++
+ keyword "using" ++ spc() ++ pr_using e ++ spc() ++
+ keyword "with" ++ spc() ++ Pputils.pr_raw_generic env sigma te
+ )
+ | VernacProofMode s ->
+ return (keyword "Proof Mode" ++ str s)
+ | VernacBullet b ->
+ (* XXX: Redundant with Proof_bullet.print *)
+ return (let open Proof_bullet in begin match b with
+ | Dash n -> str (String.make n '-')
+ | Star n -> str (String.make n '*')
+ | Plus n -> str (String.make n '+')
+ end)
+ | VernacSubproof None ->
+ return (str "{")
+ | VernacSubproof (Some i) ->
+ return (Goal_select.pr_goal_selector i ++ str ":" ++ spc () ++ str "{")
+ | VernacEndSubproof ->
+ return (str "}")
let pr_control_flag (p : control_flag) =
let w = match p with
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index b0e483ee74..d540e7f93d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -579,7 +579,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
let name = vernac_definition_name lid local in
start_lemma_com ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?hook [(name, pl), (bl, t)]
-let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt =
+let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_opt =
let open DefAttributes in
let scope = enforce_locality_exp atts.locality discharge in
let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in
@@ -593,13 +593,13 @@ let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt
Some (snd (Hook.get f_interp_redexp env sigma r)) in
if program_mode then
let kind = Decls.IsDefinition kind in
- ComDefinition.do_definition_program ~name:name.v
+ ComDefinition.do_definition_program ~pm ~name:name.v
~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook
else
let () =
ComDefinition.do_definition ~name:name.v
~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook in
- ()
+ pm
(* NB: pstate argument to use combinators easily *)
let vernac_start_proof ~atts kind l =
@@ -609,19 +609,20 @@ let vernac_start_proof ~atts kind l =
List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
start_lemma_com ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) l
-let vernac_end_proof ~lemma = let open Vernacexpr in function
+let vernac_end_proof ~lemma ~pm = let open Vernacexpr in function
| Admitted ->
- Declare.Proof.save_admitted ~proof:lemma
+ Declare.Proof.save_admitted ~pm ~proof:lemma
| Proved (opaque,idopt) ->
- let _ : Names.GlobRef.t list = Declare.Proof.save ~proof:lemma ~opaque ~idopt
- in ()
+ let pm, _ = Declare.Proof.save ~pm ~proof:lemma ~opaque ~idopt
+ in pm
-let vernac_exact_proof ~lemma c =
+let vernac_exact_proof ~lemma ~pm c =
(* spiwack: for simplicity I do not enforce that "Proof proof_term" is
called only at the beginning of a proof. *)
let lemma, status = Declare.Proof.by (Tactics.exact_proof c) lemma in
- let _ : _ list = Declare.Proof.save ~proof:lemma ~opaque:Opaque ~idopt:None in
- if not status then Feedback.feedback Feedback.AddedAxiom
+ let pm, _ = Declare.Proof.save ~pm ~proof:lemma ~opaque:Opaque ~idopt:None in
+ if not status then Feedback.feedback Feedback.AddedAxiom;
+ pm
let vernac_assumption ~atts discharge kind l nl =
let open DefAttributes in
@@ -837,14 +838,15 @@ let vernac_fixpoint_interactive ~atts discharge l =
CErrors.user_err Pp.(str"Program Fixpoint requires a body");
ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic l
-let vernac_fixpoint ~atts discharge l =
+let vernac_fixpoint ~atts ~pm discharge l =
let open DefAttributes in
let scope = vernac_fixpoint_common ~atts discharge l in
if atts.program then
(* XXX: Switch to the attribute system and match on ~atts *)
- ComProgramFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic l
+ ComProgramFixpoint.do_fixpoint ~pm ~scope ~poly:atts.polymorphic l
else
- ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic l
+ let () = ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic l in
+ pm
let vernac_cofixpoint_common ~atts discharge l =
if Dumpglob.dump () then
@@ -858,13 +860,14 @@ let vernac_cofixpoint_interactive ~atts discharge l =
CErrors.user_err Pp.(str"Program CoFixpoint requires a body");
ComFixpoint.do_cofixpoint_interactive ~scope ~poly:atts.polymorphic l
-let vernac_cofixpoint ~atts discharge l =
+let vernac_cofixpoint ~atts ~pm discharge l =
let open DefAttributes in
let scope = vernac_cofixpoint_common ~atts discharge l in
if atts.program then
- ComProgramFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic l
+ ComProgramFixpoint.do_cofixpoint ~pm ~scope ~poly:atts.polymorphic l
else
- ComFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic l
+ let () = ComFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic l in
+ pm
let vernac_scheme l =
if Dumpglob.dump () then
@@ -1085,10 +1088,10 @@ let msg_of_subsection ss id =
in
Pp.str kind ++ spc () ++ Id.print id
-let vernac_end_segment ({v=id} as lid) =
+let vernac_end_segment ~pm ({v=id} as lid) =
let ss = Lib.find_opening_node id in
let what_for = msg_of_subsection ss lid.v in
- Declare.Obls.check_solved_obligations ~what_for;
+ Declare.Obls.check_solved_obligations ~pm ~what_for;
match ss with
| Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid
| Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid
@@ -1147,14 +1150,14 @@ let vernac_identity_coercion ~atts id qids qidt =
(* Type classes *)
-let vernac_instance_program ~atts name bl t props info =
+let vernac_instance_program ~atts ~pm name bl t props info =
Dumpglob.dump_constraint (fst name) false "inst";
let locality, poly =
Attributes.(parse (Notations.(locality ++ polymorphic))) atts
in
let global = not (make_section_locality locality) in
- let _id : Id.t = Classes.new_instance_program ~global ~poly name bl t props info in
- ()
+ let pm, _id = Classes.new_instance_program ~pm ~global ~poly name bl t props info in
+ pm
let vernac_instance_interactive ~atts name bl t info props =
Dumpglob.dump_constraint (fst name) false "inst";
@@ -1991,9 +1994,9 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
(* Gallina *)
| VernacDefinition (discharge,lid,DefineBody (bl,red_option,c,typ)) ->
- VtDefault (fun () ->
+ VtModifyProgram (fun ~pm ->
with_def_attributes ~atts
- vernac_definition discharge lid bl red_option c typ)
+ vernac_definition ~pm discharge lid bl red_option c typ)
| VernacDefinition (discharge,lid,ProveBody(bl,typ)) ->
VtOpenProof(fun () ->
with_def_attributes ~atts
@@ -2028,14 +2031,14 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
VtOpenProof (fun () ->
with_def_attributes ~atts vernac_fixpoint_interactive discharge l)
else
- VtDefault (fun () ->
- with_def_attributes ~atts vernac_fixpoint discharge l)
+ VtModifyProgram (fun ~pm ->
+ with_def_attributes ~atts (vernac_fixpoint ~pm) discharge l)
| VernacCoFixpoint (discharge, l) ->
let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in
if opens then
VtOpenProof(fun () -> with_def_attributes ~atts vernac_cofixpoint_interactive discharge l)
else
- VtDefault(fun () -> with_def_attributes ~atts vernac_cofixpoint discharge l)
+ VtModifyProgram(fun ~pm -> with_def_attributes ~atts (vernac_cofixpoint ~pm) discharge l)
| VernacScheme l ->
VtDefault(fun () ->
@@ -2064,9 +2067,9 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
VtNoProof(fun () ->
vernac_begin_section ~poly:(only_polymorphism atts) lid)
| VernacEndSegment lid ->
- VtNoProof(fun () ->
+ VtReadProgram(fun ~pm ->
unsupported_attributes atts;
- vernac_end_segment lid)
+ vernac_end_segment ~pm lid)
| VernacNameSectionHypSet (lid, set) ->
VtDefault(fun () ->
unsupported_attributes atts;
@@ -2091,7 +2094,7 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
| VernacInstance (name, bl, t, props, info) ->
let atts, program = Attributes.(parse_with_extra program) atts in
if program then
- VtDefault (fun () -> vernac_instance_program ~atts name bl t props info)
+ VtModifyProgram (vernac_instance_program ~atts name bl t props info)
else begin match props with
| None ->
VtOpenProof (fun () ->
@@ -2221,10 +2224,10 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
VtNoProof(fun () ->
unsupported_attributes atts;
vernac_register qid r)
- | VernacPrimitive (id, prim, typopt) ->
+ | VernacPrimitive ((id, udecl), prim, typopt) ->
VtDefault(fun () ->
unsupported_attributes atts;
- ComPrimitive.do_primitive id prim typopt)
+ ComPrimitive.do_primitive id udecl prim typopt)
| VernacComments l ->
VtDefault(fun () ->
unsupported_attributes atts;
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 06ac7f8d48..d8e17d00e3 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -438,7 +438,7 @@ type nonrec vernac_expr =
| VernacSearch of searchable * Goal_select.t option * search_restriction
| VernacLocate of locatable
| VernacRegister of qualid * register_kind
- | VernacPrimitive of lident * CPrimitives.op_or_type * constr_expr option
+ | VernacPrimitive of ident_decl * CPrimitives.op_or_type * constr_expr option
| VernacComments of comment list
(* Proof management *)
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index f8a80e8feb..496b1a43d1 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -55,11 +55,15 @@ and proof_block_name = string (** open type of delimiters *)
type typed_vernac =
| VtDefault of (unit -> unit)
| VtNoProof of (unit -> unit)
- | VtCloseProof of (lemma:Declare.Proof.t -> unit)
+ | VtCloseProof of (lemma:Declare.Proof.t -> pm:Declare.OblState.t -> Declare.OblState.t)
| VtOpenProof of (unit -> Declare.Proof.t)
| VtModifyProof of (pstate:Declare.Proof.t -> Declare.Proof.t)
| VtReadProofOpt of (pstate:Declare.Proof.t option -> unit)
| VtReadProof of (pstate:Declare.Proof.t -> unit)
+ | VtReadProgram of (pm:Declare.OblState.t -> unit)
+ | VtModifyProgram of (pm:Declare.OblState.t -> Declare.OblState.t)
+ | VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t)
+ | VtOpenProofProgram of (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t)
type vernac_command = atts:Attributes.vernac_flags -> typed_vernac
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 103e24233b..5ef137cfc0 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -73,11 +73,15 @@ and proof_block_name = string (** open type of delimiters *)
type typed_vernac =
| VtDefault of (unit -> unit)
| VtNoProof of (unit -> unit)
- | VtCloseProof of (lemma:Declare.Proof.t -> unit)
+ | VtCloseProof of (lemma:Declare.Proof.t -> pm:Declare.OblState.t -> Declare.OblState.t)
| VtOpenProof of (unit -> Declare.Proof.t)
| VtModifyProof of (pstate:Declare.Proof.t -> Declare.Proof.t)
| VtReadProofOpt of (pstate:Declare.Proof.t option -> unit)
| VtReadProof of (pstate:Declare.Proof.t -> unit)
+ | VtReadProgram of (pm:Declare.OblState.t -> unit)
+ | VtModifyProgram of (pm:Declare.OblState.t -> Declare.OblState.t)
+ | VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t)
+ | VtOpenProofProgram of (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t)
type vernac_command = atts:Attributes.vernac_flags -> typed_vernac
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 1b977b8e10..6be2fb0d43 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -22,32 +22,41 @@ let vernac_require_open_lemma ~stack f =
| None ->
CErrors.user_err (Pp.str "Command not supported (No proof-editing in progress)")
-let interp_typed_vernac c ~stack =
+let interp_typed_vernac c ~pm ~stack =
let open Vernacextend in
match c with
- | VtDefault f -> f (); stack
+ | VtDefault f -> f (); stack, pm
| VtNoProof f ->
if Option.has_some stack then
CErrors.user_err (Pp.str "Command not supported (Open proofs remain)");
let () = f () in
- stack
+ stack, pm
| VtCloseProof f ->
vernac_require_open_lemma ~stack (fun stack ->
let lemma, stack = Vernacstate.LemmaStack.pop stack in
- f ~lemma;
- stack)
+ let pm = f ~lemma ~pm in
+ stack, pm)
| VtOpenProof f ->
- Some (Vernacstate.LemmaStack.push stack (f ()))
+ Some (Vernacstate.LemmaStack.push stack (f ())), pm
| VtModifyProof f ->
- Option.map (Vernacstate.LemmaStack.map_top ~f:(fun pstate -> f ~pstate)) stack
+ Option.map (Vernacstate.LemmaStack.map_top ~f:(fun pstate -> f ~pstate)) stack, pm
| VtReadProofOpt f ->
let pstate = Option.map (Vernacstate.LemmaStack.with_top ~f:(fun x -> x)) stack in
f ~pstate;
- stack
+ stack, pm
| VtReadProof f ->
vernac_require_open_lemma ~stack
(Vernacstate.LemmaStack.with_top ~f:(fun pstate -> f ~pstate));
- stack
+ stack, pm
+ | VtReadProgram f -> f ~pm; stack, pm
+ | VtModifyProgram f ->
+ let pm = f ~pm in stack, pm
+ | VtDeclareProgram f ->
+ let lemma = f ~pm in
+ Some (Vernacstate.LemmaStack.push stack lemma), pm
+ | VtOpenProofProgram f ->
+ let pm, lemma = f ~pm in
+ Some (Vernacstate.LemmaStack.push stack lemma), pm
(* Default proof mode, to be set at the beginning of proofs for
programs that cannot be statically classified. *)
@@ -123,11 +132,11 @@ let mk_time_header =
fun vernac -> Lazy.from_fun (fun () -> pr_time_header vernac)
let interp_control_flag ~time_header (f : control_flag) ~st
- (fn : st:Vernacstate.t -> Vernacstate.LemmaStack.t option) =
+ (fn : st:Vernacstate.t -> Vernacstate.LemmaStack.t option * Declare.OblState.t) =
match f with
| ControlFail ->
with_fail ~st (fun () -> fn ~st);
- st.Vernacstate.lemmas
+ st.Vernacstate.lemmas, st.Vernacstate.program
| ControlTimeout timeout ->
vernac_timeout ~timeout (fun () -> fn ~st) ()
| ControlTime batch ->
@@ -142,6 +151,7 @@ let interp_control_flag ~time_header (f : control_flag) ~st
* loc is the Loc.t of the vernacular command being interpreted. *)
let rec interp_expr ~atts ~st c =
let stack = st.Vernacstate.lemmas in
+ let program = st.Vernacstate.program in
vernac_pperr_endline Pp.(fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
match c with
@@ -163,7 +173,7 @@ let rec interp_expr ~atts ~st c =
vernac_load ~verbosely fname
| v ->
let fv = Vernacentries.translate_vernac ~atts v in
- interp_typed_vernac ~stack fv
+ interp_typed_vernac ~pm:program ~stack fv
and vernac_load ~verbosely fname =
(* Note that no proof should be open here, so the state here is just token for now *)
@@ -180,19 +190,19 @@ and vernac_load ~verbosely fname =
let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing
(Pcoq.Entry.parse (Pvernac.main_entry proof_mode))
in
- let rec load_loop ~stack =
+ let rec load_loop ~pm ~stack =
let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in
match parse_sentence proof_mode input with
- | None -> stack
+ | None -> stack, pm
| Some stm ->
- let stack = v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack }) stm in
- (load_loop [@ocaml.tailcall]) ~stack
+ let stack, pm = v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack; program = pm }) stm in
+ (load_loop [@ocaml.tailcall]) ~stack ~pm
in
- let stack = load_loop ~stack:st.Vernacstate.lemmas in
+ let stack, pm = load_loop ~pm:st.Vernacstate.program ~stack:st.Vernacstate.lemmas in
(* If Load left a proof open, we fail too. *)
if Option.has_some stack then
CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.");
- stack
+ stack, pm
and interp_control ~st ({ CAst.v = cmd } as vernac) =
let time_header = mk_time_header vernac in
@@ -200,9 +210,9 @@ and interp_control ~st ({ CAst.v = cmd } as vernac) =
cmd.control
(fun ~st ->
let before_univs = Global.universes () in
- let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in
- if before_univs == Global.universes () then pstack
- else Option.map (Vernacstate.LemmaStack.map_top ~f:Declare.Proof.update_global_env) pstack)
+ let pstack, pm = interp_expr ~atts:cmd.attrs ~st cmd.expr in
+ if before_univs == Global.universes () then pstack, pm
+ else Option.map (Vernacstate.LemmaStack.map_top ~f:Declare.Proof.update_global_env) pstack, pm)
~st
(* XXX: This won't properly set the proof mode, as of today, it is
@@ -213,17 +223,18 @@ and interp_control ~st ({ CAst.v = cmd } as vernac) =
*)
(* Interpreting a possibly delayed proof *)
-let interp_qed_delayed ~proof ~pinfo ~st pe : Vernacstate.LemmaStack.t option =
+let interp_qed_delayed ~proof ~pinfo ~st pe : Vernacstate.LemmaStack.t option * Declare.OblState.t =
let stack = st.Vernacstate.lemmas in
+ let pm = st.Vernacstate.program in
let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in
- let () = match pe with
+ let pm = match pe with
| Admitted ->
- Declare.Proof.save_lemma_admitted_delayed ~proof ~pinfo
+ Declare.Proof.save_lemma_admitted_delayed ~pm ~proof ~pinfo
| Proved (_,idopt) ->
- let _ : _ list = Declare.Proof.save_lemma_proved_delayed ~proof ~pinfo ~idopt in
- ()
+ let pm, _ = Declare.Proof.save_lemma_proved_delayed ~pm ~proof ~pinfo ~idopt in
+ pm
in
- stack
+ stack, pm
let interp_qed_delayed_control ~proof ~pinfo ~st ~control { CAst.loc; v=pe } =
let time_header = mk_time_header (CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe }) in
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 073ef1c2d7..ee06205427 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -113,15 +113,18 @@ type t = {
parsing : Parser.t;
system : System.t; (* summary + libstack *)
lemmas : LemmaStack.t option; (* proofs of lemmas currently opened *)
+ program : Declare.OblState.t; (* obligations table *)
shallow : bool (* is the state trimmed down (libstack) *)
}
let s_cache = ref None
let s_lemmas = ref None
+let s_program = ref Declare.OblState.empty
let invalidate_cache () =
s_cache := None;
- s_lemmas := None
+ s_lemmas := None;
+ s_program := Declare.OblState.empty
let update_cache rf v =
rf := Some v; v
@@ -138,20 +141,24 @@ let do_if_not_cached rf f v =
let freeze_interp_state ~marshallable =
{ system = update_cache s_cache (System.freeze ~marshallable);
lemmas = !s_lemmas;
+ program = !s_program;
shallow = false;
parsing = Parser.cur_state ();
}
-let unfreeze_interp_state { system; lemmas; parsing } =
+let unfreeze_interp_state { system; lemmas; program; parsing } =
do_if_not_cached s_cache System.unfreeze system;
s_lemmas := lemmas;
+ s_program := program;
Pcoq.unfreeze parsing
(* Compatibility module *)
module Declare_ = struct
let get () = !s_lemmas
- let set x = s_lemmas := x
+ let set (pstate,pm) =
+ s_lemmas := pstate;
+ s_program := pm
let get_pstate () =
Option.map (LemmaStack.with_top ~f:(fun x -> x)) !s_lemmas
@@ -237,18 +244,16 @@ module Stm = struct
type nonrec pstate =
LemmaStack.t option *
int * (* Evarutil.meta_counter_summary_tag *)
- int * (* Evd.evar_counter_summary_tag *)
- Declare.Obls.State.t
+ int (* Evd.evar_counter_summary_tag *)
(* Parts of the system state that are morally part of the proof state *)
let pstate { lemmas; system } =
let st = System.Stm.summary system in
lemmas,
Summary.project_from_summary st Evarutil.meta_counter_summary_tag,
- Summary.project_from_summary st Evd.evar_counter_summary_tag,
- Summary.project_from_summary st Declare.Obls.State.prg_tag
+ Summary.project_from_summary st Evd.evar_counter_summary_tag
- let set_pstate ({ lemmas; system } as s) (pstate,c1,c2,c3) =
+ let set_pstate ({ lemmas; system } as s) (pstate,c1,c2) =
{ s with
lemmas =
Declare_.copy_terminators ~src:s.lemmas ~tgt:pstate
@@ -258,7 +263,6 @@ module Stm = struct
let st = System.Stm.summary s.system in
let st = Summary.modify_summary st Evarutil.meta_counter_summary_tag c1 in
let st = Summary.modify_summary st Evd.evar_counter_summary_tag c2 in
- let st = Summary.modify_summary st Declare.Obls.State.prg_tag c3 in
st
end
}
@@ -267,7 +271,6 @@ module Stm = struct
let st = System.Stm.summary system in
let st = Summary.remove_from_summary st Evarutil.meta_counter_summary_tag in
let st = Summary.remove_from_summary st Evd.evar_counter_summary_tag in
- let st = Summary.remove_from_summary st Declare.Obls.State.prg_tag in
st, System.Stm.lib system
let same_env { system = s1 } { system = s2 } =
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 8c23ac0698..16fab3782b 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -52,6 +52,8 @@ type t =
(** summary + libstack *)
; lemmas : LemmaStack.t option
(** proofs of lemmas currently opened *)
+ ; program : Declare.OblState.t
+ (** program mode table *)
; shallow : bool
(** is the state trimmed down (libstack) *)
}
@@ -112,7 +114,7 @@ module Declare : sig
(* Low-level stuff *)
val get : unit -> LemmaStack.t option
- val set : LemmaStack.t option -> unit
+ val set : LemmaStack.t option * Declare.OblState.t -> unit
val get_pstate : unit -> Declare.Proof.t option
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 16:24:17 +0000