diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 50 | ||||
| -rw-r--r-- | proofs/logic.mli | 2 | ||||
| -rw-r--r-- | proofs/proof.ml | 62 | ||||
| -rw-r--r-- | proofs/proof.mli | 47 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 4 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 2 |
6 files changed, 39 insertions, 128 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index a01ddf2388..b79e1e6024 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 () @@ -161,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 @@ -556,25 +550,25 @@ 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 ~reorder env 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 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 + 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 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 f99076db23..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 : bool -> Environ.named_context_val -> 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 -> diff --git a/proofs/proof.ml b/proofs/proof.ml index 978b1f6f78..778d98b2cd 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -126,9 +126,6 @@ type t = (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *) } -let initial_goals pf = Proofview.initial_goals pf.entry -let initial_euctx pf = pf.initial_euctx - (*** General proof functions ***) let proof p = @@ -147,33 +144,6 @@ let proof p = let given_up = p.given_up in (goals,stack,shelf,given_up,sigma) -type 'a pre_goals = { - fg_goals : 'a list; - (** List of the focussed goals *) - bg_goals : ('a list * 'a list) list; - (** Zipper representing the unfocussed background goals *) - shelved_goals : 'a list; - (** List of the goals on the shelf. *) - given_up_goals : 'a list; - (** List of the goals that have been given up *) -} - -let map_structured_proof pfts process_goal: 'a pre_goals = - let (goals, zipper, shelf, given_up, sigma) = proof pfts in - let fg = List.map (process_goal sigma) goals in - let map_zip (lg, rg) = - let lg = List.map (process_goal sigma) lg in - let rg = List.map (process_goal sigma) rg in - (lg, rg) - in - let bg = List.map map_zip zipper in - let shelf = List.map (process_goal sigma) shelf in - let given_up = List.map (process_goal sigma) given_up in - { fg_goals = fg; - bg_goals = bg; - shelved_goals = shelf; - given_up_goals = given_up; } - let rec unroll_focus pv = function | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk | [] -> pv @@ -441,22 +411,6 @@ let in_proof p k = k (Proofview.return p.proofview) let unshelve p = { p with proofview = Proofview.unshelve (p.shelf) (p.proofview) ; shelf = [] } -let pr_proof p = - let p = map_structured_proof p (fun _sigma g -> g) in - Pp.( - let pr_goal_list = prlist_with_sep spc Goal.pr_goal in - let rec aux acc = function - | [] -> acc - | (before,after)::stack -> - aux (pr_goal_list before ++ spc () ++ str "{" ++ acc ++ str "}" ++ spc () ++ - pr_goal_list after) stack in - str "[" ++ str "focus structure: " ++ - aux (pr_goal_list p.fg_goals) p.bg_goals ++ str ";" ++ spc () ++ - str "shelved: " ++ pr_goal_list p.shelved_goals ++ str ";" ++ spc () ++ - str "given up: " ++ pr_goal_list p.given_up_goals ++ - str "]" - ) - (*** Compatibility layer with <=v8.2 ***) module V82 = struct @@ -554,3 +508,19 @@ let data { proofview; focus_stack; entry; shelf; given_up; initial_euctx; name; let stack = map_minus_one (fun (_,_,c) -> Proofview.focus_context c) focus_stack in { sigma; goals; entry; stack; shelf; given_up; initial_euctx; name; poly } + +let pr_proof p = + let { goals=fg_goals; stack=bg_goals; shelf; given_up; _ } = data p in + Pp.( + let pr_goal_list = prlist_with_sep spc Goal.pr_goal in + let rec aux acc = function + | [] -> acc + | (before,after)::stack -> + aux (pr_goal_list before ++ spc () ++ str "{" ++ acc ++ str "}" ++ spc () ++ + pr_goal_list after) stack in + str "[" ++ str "focus structure: " ++ + aux (pr_goal_list fg_goals) bg_goals ++ str ";" ++ spc () ++ + str "shelved: " ++ pr_goal_list shelf ++ str ";" ++ spc () ++ + str "given up: " ++ pr_goal_list given_up ++ + str "]" + ) diff --git a/proofs/proof.mli b/proofs/proof.mli index defef57a8d..1f4748141a 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -34,30 +34,6 @@ (* Type of a proof. *) type t -(* Returns a stylised view of a proof for use by, for instance, - ide-s. *) -(* spiwack: the type of [proof] will change as we push more refined - functions to ide-s. This would be better than spawning a new nearly - identical function everytime. Hence the generic name. *) -(* In this version: returns the focused goals, a representation of the - focus stack (the goals at each level), a representation of the - shelf (the list of goals on the shelf), a representation of the - given up goals (the list of the given up goals) and the underlying - evar_map *) -val proof : t -> - Goal.goal list - * (Goal.goal list * Goal.goal list) list - * Goal.goal list - * Goal.goal list - * Evd.evar_map -[@@ocaml.deprecated "use [Proof.data]"] - -val initial_goals : t -> (EConstr.constr * EConstr.types) list -[@@ocaml.deprecated "use [Proof.data]"] - -val initial_euctx : t -> UState.t -[@@ocaml.deprecated "use [Proof.data]"] - type data = { sigma : Evd.evar_map (** A representation of the evar_map [EJGA wouldn't it better to just return the proofview?] *) @@ -81,29 +57,6 @@ type data = val data : t -> data -(* Generic records structured like the return type of proof *) -type 'a pre_goals = { - fg_goals : 'a list; - [@ocaml.deprecated "use [Proof.data]"] - (** List of the focussed goals *) - bg_goals : ('a list * 'a list) list; - [@ocaml.deprecated "use [Proof.data]"] - (** Zipper representing the unfocussed background goals *) - shelved_goals : 'a list; - [@ocaml.deprecated "use [Proof.data]"] - (** List of the goals on the shelf. *) - given_up_goals : 'a list; - [@ocaml.deprecated "use [Proof.data]"] - (** List of the goals that have been given up *) -} -[@@ocaml.deprecated "use [Proof.data]"] - -(* needed in OCaml 4.05.0, not needed in newer ones *) -[@@@ocaml.warning "-3"] -val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) [@ocaml.warning "-3"] -[@@ocaml.deprecated "use [Proof.data]"] -[@@@ocaml.warning "+3"] - (*** General proof functions ***) val start : name:Names.Id.t diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 7b3d9e534b..93031c2202 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -104,10 +104,6 @@ let db_pr_goal sigma g = let pr_gls gls = hov 0 (pr_evar_map (Some 2) (pf_env gls) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls)) -let pr_glls glls = - hov 0 (pr_evar_map (Some 2) (Global.env()) (sig_sig glls) ++ fnl () ++ - prlist_with_sep fnl (db_pr_goal (project glls)) (sig_it glls)) - (* Variants of [Tacmach] functions built with the new proof engine *) module New = struct diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 218011c316..23e1e6f566 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -68,8 +68,6 @@ val pf_conv_x_leq : Goal.goal sigma -> constr -> constr -> bool (** {6 Pretty-printing functions (debug only). } *) val pr_gls : Goal.goal sigma -> Pp.t -val pr_glls : Goal.goal list sigma -> Pp.t -[@@ocaml.deprecated "Please move to \"new\" proof engine"] (** Variants of [Tacmach] functions built with the new proof engine *) module New : sig |