From 4785156d31eb513b6e7fcb8dbab1c219da83612b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 24 Apr 2019 15:42:45 +0200 Subject: Cleanup of Logic.convert_hyp. --- proofs/logic.ml | 40 ++++++++++++++++------------------------ 1 file changed, 16 insertions(+), 24 deletions(-) (limited to 'proofs') diff --git a/proofs/logic.ml b/proofs/logic.ml index a01ddf2388..f51f2ea5bc 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -78,14 +78,6 @@ let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoS let check = ref false let with_check = Flags.with_option check -(* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and - returns [tail::(f head (id,_,_) (rev tail))] *) -let apply_to_hyp env sigma check sign id f = - try apply_to_hyp sign id f - with Hyp_not_found -> - if check then error_no_such_hypothesis env sigma id - else sign - let check_typability env sigma c = if !check then let _ = unsafe_type_of env sigma (EConstr.of_constr c) in () @@ -559,22 +551,22 @@ and treat_case sigma goal ci lbrty lf acc' = let convert_hyp check sign sigma d = let id = NamedDecl.get_id d in let b = NamedDecl.get_value d in - let env = Global.env () in - let reorder = ref [] in - let sign' = - apply_to_hyp env sigma check sign id - (fun _ d' _ -> - let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in - let env = Global.env_of_context sign in - if check && not (is_conv env sigma (NamedDecl.get_type d) (EConstr.of_constr (NamedDecl.get_type d'))) then - user_err ~hdr:"Logic.convert_hyp" - (str "Incorrect change of the type of " ++ Id.print id ++ str "."); - if check && not (Option.equal (is_conv env sigma) b c) then - user_err ~hdr:"Logic.convert_hyp" - (str "Incorrect change of the body of "++ Id.print id ++ str "."); - if check then reorder := check_decl_position env sigma sign d; - map_named_decl EConstr.Unsafe.to_constr d) in - reorder_val_context env sigma sign' !reorder + let env = Global.env_of_context sign in + match lookup_named_ctxt id sign with + | exception Not_found -> + if check then error_no_such_hypothesis env sigma id + else sign + | d' -> + let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in + if check && not (is_conv env sigma (NamedDecl.get_type d) (EConstr.of_constr (NamedDecl.get_type d'))) then + user_err ~hdr:"Logic.convert_hyp" + (str "Incorrect change of the type of " ++ Id.print id ++ str "."); + if check && not (Option.equal (is_conv env sigma) b c) then + user_err ~hdr:"Logic.convert_hyp" + (str "Incorrect change of the body of "++ Id.print id ++ str "."); + let sign' = apply_to_hyp sign id (fun _ _ _ -> EConstr.Unsafe.to_named_decl d) in + if check then reorder_val_context env sigma sign' (check_decl_position env sigma sign d) + else sign' (************************************************************************) (************************************************************************) -- cgit v1.2.3 From a5a89e8b623cd5822f59b854a45efc8236ae0087 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 24 Apr 2019 16:03:06 +0200 Subject: Logic.convert_hyp now takes an environment as an argument. This prevents having to call global functions, for no good reason. We also seize the opportunity to name the check argument. --- proofs/logic.ml | 4 ++-- proofs/logic.mli | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'proofs') diff --git a/proofs/logic.ml b/proofs/logic.ml index f51f2ea5bc..3fcde56e76 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -548,10 +548,10 @@ and treat_case sigma goal ci lbrty lf acc' = (lacc,sigma,fi::bacc)) (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags -let convert_hyp check sign sigma d = +let convert_hyp ~check env sigma d = let id = NamedDecl.get_id d in let b = NamedDecl.get_value d in - let env = Global.env_of_context sign in + let sign = Environ.named_context_val env in match lookup_named_ctxt id sign with | exception Not_found -> if check then error_no_such_hypothesis env sigma id diff --git a/proofs/logic.mli b/proofs/logic.mli index f99076db23..163d71f69c 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -62,7 +62,7 @@ type 'id move_location = val pr_move_location : ('a -> Pp.t) -> 'a move_location -> Pp.t -val convert_hyp : bool -> Environ.named_context_val -> evar_map -> +val convert_hyp : check:bool -> Environ.env -> evar_map -> EConstr.named_declaration -> Environ.named_context_val val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move_location -> -- cgit v1.2.3 From d313bc5c1439f1881b4c77b9d92400579d2168ce Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 1 May 2019 17:22:42 +0200 Subject: Split the hypothesis conversion check in a conversion + ordering check. --- proofs/logic.ml | 4 ++-- proofs/logic.mli | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'proofs') diff --git a/proofs/logic.ml b/proofs/logic.ml index 3fcde56e76..76eb79df39 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -548,7 +548,7 @@ and treat_case sigma goal ci lbrty lf acc' = (lacc,sigma,fi::bacc)) (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags -let convert_hyp ~check env sigma d = +let convert_hyp ~check ~reorder env sigma d = let id = NamedDecl.get_id d in let b = NamedDecl.get_value d in let sign = Environ.named_context_val env in @@ -565,7 +565,7 @@ let convert_hyp ~check env sigma d = user_err ~hdr:"Logic.convert_hyp" (str "Incorrect change of the body of "++ Id.print id ++ str "."); let sign' = apply_to_hyp sign id (fun _ _ _ -> EConstr.Unsafe.to_named_decl d) in - if check then reorder_val_context env sigma sign' (check_decl_position env sigma sign d) + if reorder then reorder_val_context env sigma sign' (check_decl_position env sigma sign d) else sign' (************************************************************************) diff --git a/proofs/logic.mli b/proofs/logic.mli index 163d71f69c..406fe57985 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -62,7 +62,7 @@ type 'id move_location = val pr_move_location : ('a -> Pp.t) -> 'a move_location -> Pp.t -val convert_hyp : check:bool -> Environ.env -> evar_map -> +val convert_hyp : check:bool -> reorder:bool -> Environ.env -> evar_map -> EConstr.named_declaration -> Environ.named_context_val val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move_location -> -- cgit v1.2.3 From 1c4a11ee8b5b48b85911689e1bb93757359cdfca Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 1 May 2019 17:55:04 +0200 Subject: Fast-path for reordering of a single closed variable. Doesn't seem to matter in practice, but it doesn't hurt either. --- proofs/logic.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'proofs') diff --git a/proofs/logic.ml b/proofs/logic.ml index 76eb79df39..b79e1e6024 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -153,12 +153,14 @@ let reorder_context env sigma sign ord = step ord ords sign mt_q [] let reorder_val_context env sigma sign ord = +match ord with +| [] | [_] -> + (* Single variable-free definitions need not be reordered *) + sign +| _ :: _ :: _ -> let open EConstr in val_of_named_context (reorder_context env sigma (named_context_of_val sign) ord) - - - let check_decl_position env sigma sign d = let open EConstr in let x = NamedDecl.get_id d in -- cgit v1.2.3