From e5b07b820f73be273427523d72f1e3ddf44426ac Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 18 Nov 2011 15:02:52 +0000 Subject: Now Coqtop has a richer way to answer a query about its pending goals. Answers are semantic and not simple strings anymore. Still to be ameliorated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14683 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/ideproof.ml | 19 +++++++++++++++-- toplevel/ide_intf.ml | 33 ++++++++++++++++++++++++----- toplevel/ide_intf.mli | 5 ++++- toplevel/ide_slave.ml | 58 +++++++++++++++++++++------------------------------ 4 files changed, 73 insertions(+), 42 deletions(-) diff --git a/ide/ideproof.ml b/ide/ideproof.ml index 58e7d2734..742ffc46a 100644 --- a/ide/ideproof.ml +++ b/ide/ideproof.ml @@ -97,7 +97,22 @@ let mode_cesar (proof:GText.view) = function let display mode (view:GText.view) goals = view#buffer#set_text ""; match goals with - | Ide_intf.Message msg -> + | Ide_intf.No_current_proof -> () + | Ide_intf.Proof_completed -> + view#buffer#insert "Proof Completed." + | Ide_intf.Unfocused_goals l -> + view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n"; + let iter goal = + let msg = Printf.sprintf "%s\n" goal.Ide_intf.goal_ccl in view#buffer#insert msg + in + List.iter iter l + | Ide_intf.Uninstantiated_evars el -> + view#buffer#insert "No more subgoals but non-instantiated existential variables:\n\n"; + let iter evar = + let msg = Printf.sprintf "%s\n" evar in + view#buffer#insert msg + in + List.iter iter el | Ide_intf.Goals g -> - mode view g + mode view g diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml index 6abea2ad8..18a602af2 100644 --- a/toplevel/ide_intf.ml +++ b/toplevel/ide_intf.ml @@ -20,7 +20,10 @@ type goal = { } type goals = - | Message of string + | No_current_proof + | Proof_completed + | Unfocused_goals of goal list + | Uninstantiated_evars of string list | Goals of goal list (** We use phantom types and GADT to protect ourselves against wild casts *) @@ -210,14 +213,31 @@ let to_goal = function | _ -> raise Marshal_error let of_goals = function -| Message s -> - Element ("goals", ["val", "message"], [PCData s]) +| No_current_proof -> + Element ("goals", ["val", "no_current_proof"], []) +| Proof_completed -> + Element ("goals", ["val", "proof_completed"], []) +| Unfocused_goals l -> + let xml = of_list of_goal l in + Element ("goals", ["val", "unfocused_goals"], [xml]) +| Uninstantiated_evars el -> + let xml = of_list of_string el in + Element ("goals", ["val", "uninstantiated_evars"], [xml]) | Goals l -> let xml = of_list of_goal l in Element ("goals", ["val", "goals"], [xml]) let to_goals = function -| Element ("goals", ["val", "message"], l) -> Message (raw_string l) +| Element ("goals", ["val", "no_current_proof"], []) -> + No_current_proof +| Element ("goals", ["val", "proof_completed"], []) -> + Proof_completed +| Element ("goals", ["val", "unfocused_goals"], [xml]) -> + let l = to_list to_goal xml in + Unfocused_goals l +| Element ("goals", ["val", "uninstantiated_evars"], [xml]) -> + let l = to_list to_string xml in + Uninstantiated_evars l | Element ("goals", ["val", "goals"], [xml]) -> let l = to_list to_goal xml in Goals l @@ -276,7 +296,10 @@ let pr_mkcases l = "[" ^ String.concat " | " l ^ "]" let pr_goals = function -| Message s -> "Message: " ^ s +| No_current_proof -> "No current proof." +| Proof_completed -> "Proof completed." +| Unfocused_goals gl -> Printf.sprintf "Still %i unfocused goals." (List.length gl) +| Uninstantiated_evars el -> Printf.sprintf "Still %i uninstantiated evars." (List.length el) | Goals gl -> let pr_menu s = s in let pr_goal { goal_hyp = hyps; goal_ccl = goal } = diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli index 02b852534..3752d0142 100644 --- a/toplevel/ide_intf.mli +++ b/toplevel/ide_intf.mli @@ -16,7 +16,10 @@ type goal = { } type goals = - | Message of string + | No_current_proof + | Proof_completed + | Unfocused_goals of goal list + | Uninstantiated_evars of string list | Goals of goal list type 'a call diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 95a6dcf6a..a276f3292 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -400,6 +400,20 @@ let concl_next_tac sigma concl = "right" ]) +let process_goal sigma g = + let env = Goal.V82.env sigma g in + let ccl = + let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in + string_of_ppcmds (pr_ltype_env_at_top env norm_constr) in + let process_hyp h_env d acc = + let d = Term.map_named_declaration (Reductionops.nf_evar sigma) d in + (string_of_ppcmds (pr_var_decl h_env d)) :: acc in +(* (string_of_ppcmds (pr_var_decl h_env d), hyp_next_tac sigma h_env d)::acc in *) + let hyps = + List.rev (Environ.fold_named_context process_hyp env ~init: []) in + { Ide_intf.goal_hyp = hyps; Ide_intf.goal_ccl = ccl } +(* hyps,(ccl,concl_next_tac sigma g)) *) + let goals () = try let pfts = @@ -408,42 +422,18 @@ let goals () = let { Evd.it=all_goals ; sigma=sigma } = Proof.V82.subgoals pfts in if all_goals = [] then begin - Ide_intf.Message (string_of_ppcmds ( - let { Evd.it = bgoals ; sigma = sigma } = Proof.V82.background_subgoals pfts in - match bgoals with - | [] -> - let exl = Evarutil.non_instantiated sigma in - (str (if exl = [] then "Proof Completed." else - "No more subgoals but non-instantiated existential variables:") ++ - (fnl ()) ++ (pr_evars_int 1 exl)) - | _ -> - Util.list_fold_left_i - (fun i a g -> - a ++ (Printer.pr_concl i sigma g) ++ (spc ())) 1 - (str "This subproof is complete, but there are still unfocused goals:" ++ (fnl ())) - bgoals)) + let { Evd.it = bgoals ; sigma = sigma } = Proof.V82.background_subgoals pfts in + if bgoals = [] then + let exl = Evarutil.non_instantiated sigma in + if exl = [] then Ide_intf.Proof_completed + else + let el = List.map (fun evar -> string_of_ppcmds (pr_evar evar)) exl in + Ide_intf.Uninstantiated_evars el + else Ide_intf.Unfocused_goals (List.map (process_goal sigma) bgoals) end else - begin - let process_goal g = - let env = Goal.V82.env sigma g in - let ccl = - let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in - string_of_ppcmds (pr_ltype_env_at_top env norm_constr) in - let process_hyp h_env d acc = - let d = Term.map_named_declaration (Reductionops.nf_evar sigma) d in - (string_of_ppcmds (pr_var_decl h_env d)) :: acc in -(* (string_of_ppcmds (pr_var_decl h_env d), hyp_next_tac sigma h_env d)::acc in *) - let hyps = - List.rev (Environ.fold_named_context process_hyp env ~init: []) in - { Ide_intf.goal_hyp = hyps; Ide_intf.goal_ccl = ccl } -(* hyps,(ccl,concl_next_tac sigma g)) *) - in - Ide_intf.Goals (List.map process_goal all_goals) - end - with Proof_global.NoCurrentProof -> - Ide_intf.Message "" (* quick hack to have a clean message screen *) - + Ide_intf.Goals (List.map (process_goal sigma) all_goals) + with Proof_global.NoCurrentProof -> Ide_intf.No_current_proof (** Other API calls *) -- cgit v1.2.3