aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/entries.mli3
-rw-r--r--kernel/term_typing.ml65
-rw-r--r--library/declare.ml4
-rw-r--r--plugins/funind/functional_principles_types.ml17
-rw-r--r--plugins/funind/recdef.ml4
-rw-r--r--plugins/setoid_ring/newring.ml44
-rw-r--r--proofs/proof_global.ml46
-rw-r--r--proofs/proof_global.mli2
-rw-r--r--tactics/leminv.ml1
-rw-r--r--tactics/rewrite.ml5
-rw-r--r--toplevel/autoinstance.ml6
-rw-r--r--toplevel/class.ml3
-rw-r--r--toplevel/classes.ml5
-rw-r--r--toplevel/command.ml16
-rw-r--r--toplevel/ind_tables.ml3
-rw-r--r--toplevel/indschemes.ml3
-rw-r--r--toplevel/lemmas.ml6
-rw-r--r--toplevel/obligations.ml10
-rw-r--r--toplevel/record.ml14
-rw-r--r--toplevel/stm.ml3
20 files changed, 123 insertions, 97 deletions
diff --git a/kernel/entries.mli b/kernel/entries.mli
index b78372c0e..73efc7372 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -52,7 +52,10 @@ type const_entry_body = proof_output Future.computation
type definition_entry = {
const_entry_body : const_entry_body;
+ (* List of sectoin variables *)
const_entry_secctx : Context.section_context option;
+ (* State id on which the completion of type checking is reported *)
+ const_entry_feedback : Stateid.t option;
const_entry_type : types option;
const_entry_opaque : bool;
const_entry_inline_code : bool }
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 0ad03d417..554ed9f9b 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -78,45 +78,46 @@ let handle_side_effects env body side_eff =
Declareops.fold_side_effects handle_sideff body
(Declareops.uniquize_side_effects side_eff)
+let hcons_j j =
+ { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type}
+
+let feedback_completion_typecheck =
+ Option.iter (fun state_id -> Pp.feedback ~state_id Interface.Complete)
+
(* what is used for debugging only *)
let infer_declaration ?(what="UNKNOWN") env dcl =
match dcl with
- | DefinitionEntry c ->
- let ctx, entry_body = c.const_entry_secctx, c.const_entry_body in
- if c.const_entry_opaque && not (Option.is_empty c.const_entry_type) then
- let body_cst =
- Future.chain ~pure:true entry_body (fun (body, side_eff) ->
- let body = handle_side_effects env body side_eff in
- let j, cst = infer env body in
- let j =
- {uj_val = hcons_constr j.uj_val;
- uj_type = hcons_constr j.uj_type} in
- let _typ, cst = constrain_type env j cst c.const_entry_type in
- Lazyconstr.opaque_from_val j.uj_val, cst) in
- let body, cst = Future.split2 body_cst in
- let def = OpaqueDef body in
- let typ = match c.const_entry_type with
- | None -> assert false
- | Some typ -> NonPolymorphicType typ in
- def, typ, cst, c.const_entry_inline_code, ctx
- else
- let body, side_eff = Future.join entry_body in
- let body = handle_side_effects env body side_eff in
- let j, cst =
- try infer env body
- with Not_found as e ->
- prerr_endline ("infer not found " ^ what);
- raise e in
- let j =
- {uj_val = hcons_constr j.uj_val;
- uj_type = hcons_constr j.uj_type} in
- let typ, cst = constrain_type env j cst c.const_entry_type in
- let def = Def (Lazyconstr.from_val j.uj_val) in
- def, typ, Future.from_val cst, c.const_entry_inline_code, ctx
| ParameterEntry (ctx,t,nl) ->
let j, cst = infer env t in
let t = hcons_constr (Typeops.assumption_of_judgment env j) in
Undef nl, NonPolymorphicType t, Future.from_val cst, false, ctx
+ | DefinitionEntry ({ const_entry_type = Some typ;
+ const_entry_opaque = true } as c) ->
+ let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
+ let body_cst =
+ Future.chain ~greedy:true ~pure:true body (fun (body, side_eff) ->
+ let body = handle_side_effects env body side_eff in
+ let j, cst = infer env body in
+ let j = hcons_j j in
+ let _typ, cst = constrain_type env j cst (Some typ) in
+ feedback_completion_typecheck feedback_id;
+ Lazyconstr.opaque_from_val j.uj_val, cst) in
+ let body, cst = Future.split2 ~greedy:true body_cst in
+ let def = OpaqueDef body in
+ let typ = NonPolymorphicType typ in
+ def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx
+ | DefinitionEntry c ->
+ let { const_entry_type = typ; const_entry_opaque = opaque } = c in
+ let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
+ let body, side_eff = Future.join body in
+ let body = handle_side_effects env body side_eff in
+ let j, cst = infer env body in
+ let j = hcons_j j in
+ let typ, cst = constrain_type env j cst typ in
+ feedback_completion_typecheck feedback_id;
+ let def = Def (Lazyconstr.from_val j.uj_val) in
+ let cst = Future.from_val cst in
+ def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx
let global_vars_set_constant_type env = function
| NonPolymorphicType t -> global_vars_set env t
diff --git a/library/declare.ml b/library/declare.ml
index a0d0cc2ec..3bd4cdd3f 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -209,6 +209,7 @@ let declare_sideff se =
const_entry_type = ty;
const_entry_opaque = opaque;
const_entry_inline_code = false;
+ const_entry_feedback = None;
});
cst_hyps = [] ;
cst_kind = Decl_kinds.IsDefinition Decl_kinds.Definition;
@@ -254,7 +255,8 @@ let declare_definition ?(internal=UserVerbose)
const_entry_type = types;
const_entry_opaque = opaque;
const_entry_inline_code = false;
- const_entry_secctx = None }
+ const_entry_secctx = None;
+ const_entry_feedback = None }
in
declare_constant ~internal ~local id
(Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 2661a78a5..56b1a3f1c 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -339,15 +339,14 @@ let generate_functional_principle
let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
let value = change_property_sort s new_principle_type new_princ_name in
(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
- let ce =
- { const_entry_body =
- Future.from_val (value,Declareops.no_seff);
- const_entry_secctx = None;
- const_entry_type = None;
- const_entry_opaque = false;
- const_entry_inline_code = false
- }
- in
+ let ce = {
+ const_entry_body = Future.from_val (value,Declareops.no_seff);
+ const_entry_secctx = None;
+ const_entry_type = None;
+ const_entry_opaque = false;
+ const_entry_inline_code = false;
+ const_entry_feedback = None;
+ } in
ignore(
Declare.declare_constant
name
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 082d7ad51..26e1011ba 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -61,7 +61,9 @@ let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) =
const_entry_secctx = None;
const_entry_type = None;
const_entry_opaque = false;
- const_entry_inline_code = false} in
+ const_entry_inline_code = false;
+ const_entry_feedback = None;
+ } in
ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
let defined () = Lemmas.save_proof (Vernacexpr.Proved (false,None))
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index aee7efb76..b8507041f 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -152,7 +152,9 @@ let decl_constant na c =
const_entry_secctx = None;
const_entry_type = None;
const_entry_opaque = true;
- const_entry_inline_code = false},
+ const_entry_inline_code = false;
+ const_entry_feedback = None;
+ },
IsProof Lemma))
(* Calling a global tactic *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 5da216122..6e3d8f753 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -289,49 +289,45 @@ let get_open_goals () =
(List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
List.length shelf
-let close_proof ~now fpl =
- let { pid;section_vars;strength;proof;terminator } =
- cur_pstate ()
- in
+let close_proof ?feedback_id ~now fpl =
+ let { pid; section_vars; strength; proof; terminator } = cur_pstate () in
let initial_goals = Proof.initial_goals proof in
- let entries = Future.map2 (fun p (c, t) -> { Entries.
- const_entry_body = p;
- const_entry_secctx = section_vars;
- const_entry_type = Some t;
- const_entry_inline_code = false;
- const_entry_opaque = true }) fpl initial_goals in
+ let entries =
+ Future.map2 (fun p (c, t) -> { Entries.
+ const_entry_body = p;
+ const_entry_secctx = section_vars;
+ const_entry_feedback = feedback_id;
+ const_entry_type = Some t;
+ const_entry_inline_code = false;
+ const_entry_opaque = true })
+ fpl initial_goals in
if now then
List.iter (fun x -> ignore(Future.join x.Entries.const_entry_body)) entries;
- { id = pid ;
- entries = entries ;
- persistence = strength } , terminator
+ { id = pid; entries = entries; persistence = strength }, terminator
let return_proof () =
let { proof } = cur_pstate () in
let initial_goals = Proof.initial_goals proof in
let evd =
+ let error s = raise (Errors.UserError("last tactic before Qed",s)) in
try Proof.return proof with
| Proof.UnfinishedProof ->
- raise (Errors.UserError("last tactic before Qed",
- str"Attempt to save an incomplete proof"))
+ error(str"Attempt to save an incomplete proof")
| Proof.HasShelvedGoals ->
- raise (Errors.UserError("last tactic before Qed",
- str"Attempt to save a proof with shelved goals"))
+ error(str"Attempt to save a proof with shelved goals")
| Proof.HasGivenUpGoals ->
- raise (Errors.UserError("last tactic before Qed",
- str"Attempt to save a proof with given up goals"))
- | Proof.HasUnresolvedEvar ->
- raise (Errors.UserError("last tactic before Qed",
- str"Attempt to save a proof with existential " ++
- str"variables still non-instantiated"))
- in
+ error(str"Attempt to save a proof with given up goals")
+ | Proof.HasUnresolvedEvar->
+ error(str"Attempt to save a proof with existential " ++
+ str"variables still non-instantiated") in
let eff = Evd.eval_side_effects evd in
(** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
side-effects... This may explain why one need to uniquize side-effects
thereafter... *)
List.map (fun (c, _) -> (Evarutil.nf_evar evd c, eff)) initial_goals
-let close_future_proof proof = close_proof ~now:false proof
+let close_future_proof ~feedback_id proof =
+ close_proof ~feedback_id ~now:false proof
let close_proof fix_exn =
close_proof ~now:true (Future.from_val ~fix_exn (return_proof ()))
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index a8f2f2720..0519ac92b 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -96,7 +96,7 @@ val close_proof : (exn -> exn) -> closed_proof
* Both access the current proof state. The formes is supposed to be
* chained with a computation that completed the proof *)
val return_proof : unit -> Entries.proof_output list
-val close_future_proof :
+val close_future_proof : feedback_id:Stateid.t ->
Entries.proof_output list Future.computation -> closed_proof
(** Gets the current terminator without checking that the proof has
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 106205552..7af7fcb02 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -236,6 +236,7 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
const_entry_type = None;
const_entry_opaque = false;
const_entry_inline_code = false;
+ const_entry_feedback = None;
} in
let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
()
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index ca8ae67cf..2f8e0e29f 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1541,8 +1541,9 @@ let declare_projection n instance_id r =
const_entry_secctx = None;
const_entry_type = Some typ;
const_entry_opaque = false;
- const_entry_inline_code = false }
- in
+ const_entry_inline_code = false;
+ const_entry_feedback = None;
+ } in
ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
let build_morphism_signature m =
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 9ad54ac96..51d8379f5 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -191,7 +191,8 @@ let declare_record_instance gr ctx params =
const_entry_secctx = None;
const_entry_type=None;
const_entry_opaque=false;
- const_entry_inline_code = false } in
+ const_entry_inline_code = false;
+ const_entry_feedback = None } in
let decl = (DefinitionEntry ce,Decl_kinds.IsDefinition Decl_kinds.StructureComponent) in
let cst = Declare.declare_constant ident decl in
new_instance_message ident (Typeops.type_of_constant (Global.env()) cst) def
@@ -208,7 +209,8 @@ let declare_class_instance gr ctx params =
const_entry_body= Future.from_val (def,Declareops.no_seff);
const_entry_secctx = None;
const_entry_opaque = false;
- const_entry_inline_code = false } in
+ const_entry_inline_code = false;
+ const_entry_feedback = None } in
try
let cst = Declare.declare_constant ident
(ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in
diff --git a/toplevel/class.ml b/toplevel/class.ml
index f9ce75bba..a9cb6ca5e 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -222,7 +222,8 @@ let build_id_coercion idf_opt source =
const_entry_secctx = None;
const_entry_type = Some typ_f;
const_entry_opaque = false;
- const_entry_inline_code = true
+ const_entry_inline_code = true;
+ const_entry_feedback = None;
} in
let decl = (constr_entry, IsDefinition IdentityCoercion) in
let kn = declare_constant idf decl in
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index bb34323cd..220e0e050 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -107,8 +107,9 @@ let declare_instance_constant k pri global imps ?hook id term termtype =
const_entry_secctx = None;
const_entry_type = Some termtype;
const_entry_opaque = false;
- const_entry_inline_code = false }
- in
+ const_entry_inline_code = false;
+ const_entry_feedback = None;
+ } in
let cdecl = (DefinitionEntry entry, kind) in
let kn = Declare.declare_constant id cdecl in
Declare.definition_message id;
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 77219f9a2..b2e0e9736 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -89,7 +89,8 @@ let interp_definition bl red_option c ctypopt =
const_entry_secctx = None;
const_entry_type = None;
const_entry_opaque = false;
- const_entry_inline_code = false
+ const_entry_inline_code = false;
+ const_entry_feedback = None;
}
| Some ctyp ->
let ty, impsty = interp_type_evars_impls ~impls evdref env_bl ctyp in
@@ -112,7 +113,8 @@ let interp_definition bl red_option c ctypopt =
const_entry_secctx = None;
const_entry_type = Some typ;
const_entry_opaque = false;
- const_entry_inline_code = false
+ const_entry_inline_code = false;
+ const_entry_feedback = None;
}
in
red_constant_entry (rel_context_length ctx) ce red_option, !evdref, imps
@@ -536,7 +538,8 @@ let declare_fix kind f def t imps =
const_entry_secctx = None;
const_entry_type = Some t;
const_entry_opaque = false;
- const_entry_inline_code = false
+ const_entry_inline_code = false;
+ const_entry_feedback = None;
} in
declare_definition f kind ce imps (fun _ r -> r)
@@ -726,9 +729,10 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
{ const_entry_body = Future.from_val (Evarutil.nf_evar !evdref body,Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = Some ty;
- const_entry_opaque = false;
- const_entry_inline_code = false}
- in
+ const_entry_opaque = false;
+ const_entry_inline_code = false;
+ const_entry_feedback = None;
+ } in
(** FIXME: include locality *)
let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
let gr = ConstRef c in
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 4607e70eb..f5ee027f1 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -119,7 +119,8 @@ let define internal id c =
const_entry_secctx = None;
const_entry_type = None;
const_entry_opaque = false;
- const_entry_inline_code = false
+ const_entry_inline_code = false;
+ const_entry_feedback = None;
} in
let kn = fd id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
let () = match internal with
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 9eabd1df6..2cc98feea 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -121,7 +121,8 @@ let define id internal c t =
const_entry_secctx = None;
const_entry_type = t;
const_entry_opaque = false;
- const_entry_inline_code = false
+ const_entry_inline_code = false;
+ const_entry_feedback = None;
},
Decl_kinds.IsDefinition Scheme) in
definition_message id;
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 5da651120..2adc2feef 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -234,7 +234,8 @@ let save_remaining_recthms (locality,kind) body opaq i (id,(t_i,(_,imps))) =
const_entry_secctx = None;
const_entry_type = Some t_i;
const_entry_opaque = opaq;
- const_entry_inline_code = false
+ const_entry_inline_code = false;
+ const_entry_feedback = None;
} in
let c = SectionLocalDef const in
let _ = declare_variable id (Lib.cwd(), c, k) in
@@ -250,7 +251,8 @@ let save_remaining_recthms (locality,kind) body opaq i (id,(t_i,(_,imps))) =
const_entry_secctx = None;
const_entry_type = Some t_i;
const_entry_opaque = opaq;
- const_entry_inline_code = false
+ const_entry_inline_code = false;
+ const_entry_feedback = None;
} in
let kn = declare_constant id ~local (DefinitionEntry const, k) in
(locality,ConstRef kn,imps)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 54e7fbf91..6536796f4 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -514,8 +514,9 @@ let declare_definition prg =
const_entry_secctx = None;
const_entry_type = Some typ;
const_entry_opaque = false;
- const_entry_inline_code = false}
- in
+ const_entry_inline_code = false;
+ const_entry_feedback = None;
+ } in
progmap_remove prg;
!declare_definition_ref prg.prg_name
prg.prg_kind ce prg.prg_implicits
@@ -615,8 +616,9 @@ let declare_obligation prg obl body =
const_entry_secctx = None;
const_entry_type = if List.is_empty ctx then Some ty else None;
const_entry_opaque = opaque;
- const_entry_inline_code = false}
- in
+ const_entry_inline_code = false;
+ const_entry_feedback = None;
+ } in
(** ppedrot: seems legit to have obligations as local *)
let constant = Declare.declare_constant obl.obl_name ~local:true
(DefinitionEntry ce,IsProof Property)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 2ef425bf2..dc38d2519 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -194,7 +194,9 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
const_entry_secctx = None;
const_entry_type = Some projtyp;
const_entry_opaque = false;
- const_entry_inline_code = false } in
+ const_entry_inline_code = false;
+ const_entry_feedback = None;
+ } in
let k = (DefinitionEntry cie,IsDefinition kind) in
let kn = declare_constant ~internal:KernelSilent fid k in
Declare.definition_message fid;
@@ -299,8 +301,9 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
const_entry_secctx = None;
const_entry_type = class_type;
const_entry_opaque = false;
- const_entry_inline_code = false }
- in
+ const_entry_inline_code = false;
+ const_entry_feedback = None;
+ } in
let cst = Declare.declare_constant (snd id)
(DefinitionEntry class_entry, IsDefinition Definition)
in
@@ -313,8 +316,9 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
const_entry_secctx = None;
const_entry_type = Some proj_type;
const_entry_opaque = false;
- const_entry_inline_code = false }
- in
+ const_entry_inline_code = false;
+ const_entry_feedback = None;
+ } in
let proj_cst = Declare.declare_constant proj_name
(DefinitionEntry proj_entry, IsDefinition Definition)
in
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index bca2ce24c..7ea37b08c 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -1137,7 +1137,8 @@ let known_state ?(redefine_qed=false) ~cache id =
Slaves.build_proof ~exn_info:(id,eop) ~start ~stop:eop
~name:(String.concat " " (List.map Id.to_string ids)) in
qed.fproof <- Some (fp, cancel);
- let proof = Proof_global.close_future_proof fp in
+ let proof =
+ Proof_global.close_future_proof ~feedback_id:id fp in
reach view.next;
vernac_interp id ~proof x;
feedback ~state_id:id Interface.Incomplete
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 18:07:07 +0000