From 0f706b470c83a957b600496c2bca652c2cfe65e3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 7 Oct 2015 13:36:03 +0200 Subject: term_typing: strengthen discharging code Given the way Lib.extract_hyps is coded if the const_hyps field of a constant declaration contains a named_context that does not have the same order of the one in Environment.env, discharging is broken (as in some section variables are not discharged). If const_hyps is computed by the kernel, then the order is correct by construction. If such list is provided by the user, the order is not granted. We now systematically sort the list of user provided section hyps. The code of Proof using is building the named_context in the right order, but the API was not enforcing/checking it. Now it does. --- kernel/term_typing.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'kernel') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 926b387942..8eb920fb78 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -204,6 +204,10 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) str " " ++ str (String.conjugate_verb_to_be n) ++ str " used but not declared:" ++ fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in + let sort evn l = + List.filter (fun (id,_,_) -> + List.exists (fun (id',_,_) -> Names.Id.equal id id') l) + (named_context env) in (* We try to postpone the computation of used section variables *) let hyps, def = let context_ids = List.map pi1 (named_context env) in @@ -233,7 +237,7 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) [], def (* Empty section context: no need to check *) | Some declared -> (* We use the declared set and chain a check of correctness *) - declared, + sort env declared, match def with | Undef _ as x -> x (* nothing to check *) | Def cs as x -> -- cgit v1.2.3 From 9ea8867a0fa8f2a52df102732fdc1a931c659826 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 30 Sep 2015 22:12:25 +0200 Subject: Proof using: let-in policy, optional auto-clear, forward closure* - "Proof using p*" means: use p and any section var about p. - Simplify the grammar/parser for proof using . - Section variables with a body (let-in) are pulled in automatically since they are safe to be used (add no extra quantification) - automatic clear of "unused" section variables made optional: Set Proof Using Clear Unused. since clearing section hypotheses does not "always work" (e.g. hint databases are not really cleaned) - term_typing: trigger a "suggest proof using" message also for Let theorems. --- kernel/term_typing.ml | 35 +++++++++++++++++++++++++++-------- kernel/term_typing.mli | 2 +- 2 files changed, 28 insertions(+), 9 deletions(-) (limited to 'kernel') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 8eb920fb78..b6df8f454b 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -182,14 +182,17 @@ let global_vars_set_constant_type env = function (fun t c -> Id.Set.union (global_vars_set env t) c)) ctx ~init:Id.Set.empty -let record_aux env s1 s2 = +let record_aux env s_ty s_bo suggested_expr = + let in_ty = keep_hyps env s_ty in let v = String.concat " " - (List.map (fun (id, _,_) -> Id.to_string id) - (keep_hyps env (Id.Set.union s1 s2))) in - Aux_file.record_in_aux "context_used" v + (CList.map_filter (fun (id, _,_) -> + if List.exists (fun (id',_,_) -> Id.equal id id') in_ty then None + else Some (Id.to_string id)) + (keep_hyps env s_bo)) in + Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr) -let suggest_proof_using = ref (fun _ _ _ _ _ -> ()) +let suggest_proof_using = ref (fun _ _ _ _ _ -> "") let set_suggest_proof_using f = suggest_proof_using := f let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) = @@ -225,15 +228,17 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) (Opaqueproof.force_proof (opaque_tables env) lc) in (* we force so that cst are added to the env immediately after *) ignore(Opaqueproof.force_constraints (opaque_tables env) lc); - !suggest_proof_using kn env vars ids_typ context_ids; + let expr = + !suggest_proof_using (Constant.to_string kn) + env vars ids_typ context_ids in if !Flags.compilation_mode = Flags.BuildVo then - record_aux env ids_typ vars; + record_aux env ids_typ vars expr; vars in keep_hyps env (Idset.union ids_typ ids_def), def | None -> if !Flags.compilation_mode = Flags.BuildVo then - record_aux env Id.Set.empty Id.Set.empty; + record_aux env Id.Set.empty Id.Set.empty ""; [], def (* Empty section context: no need to check *) | Some declared -> (* We use the declared set and chain a check of correctness *) @@ -307,6 +312,20 @@ let translate_local_def env id centry = let def,typ,proj,poly,univs,inline_code,ctx = infer_declaration env None (DefinitionEntry centry) in let typ = type_of_constant_type env typ in + if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin + match def with + | Undef _ -> () + | Def _ -> () + | OpaqueDef lc -> + let context_ids = List.map pi1 (named_context env) in + let ids_typ = global_vars_set env typ in + let ids_def = global_vars_set env + (Opaqueproof.force_proof (opaque_tables env) lc) in + let expr = + !suggest_proof_using (Id.to_string id) + env ids_def ids_typ context_ids in + record_aux env ids_typ ids_def expr + end; def, typ, univs (* Insertion of inductive types. *) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 1b54b1ea1e..8d92bcc68f 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -44,4 +44,4 @@ val build_constant_declaration : constant -> env -> Cooking.result -> constant_body val set_suggest_proof_using : - (constant -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> unit) -> unit + (string -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> string) -> unit -- cgit v1.2.3 From b6edcae7b61ea6ccc0e65223cecb71cab0dd55cc Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 8 Oct 2015 16:00:06 +0200 Subject: Univs: fix bug #3807 Add a flag to disallow minimization to set --- kernel/univ.ml | 3 +++ kernel/univ.mli | 1 + 2 files changed, 4 insertions(+) (limited to 'kernel') diff --git a/kernel/univ.ml b/kernel/univ.ml index 34eb283d73..c0bd3bacd7 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1797,6 +1797,9 @@ struct let empty = (LSet.empty, Constraint.empty) let is_empty (univs, cst) = LSet.is_empty univs && Constraint.is_empty cst + let equal (univs, cst as x) (univs', cst' as y) = + x == y || (LSet.equal univs univs' && Constraint.equal cst cst') + let of_set s = (s, Constraint.empty) let singleton l = of_set (LSet.singleton l) let of_instance i = of_set (Instance.levels i) diff --git a/kernel/univ.mli b/kernel/univ.mli index 4cc8a2528f..cbaf7e546a 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -360,6 +360,7 @@ sig val of_instance : Instance.t -> t val of_set : universe_set -> t + val equal : t -> t -> bool val union : t -> t -> t val append : t -> t -> t -- cgit v1.2.3