diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/class.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 2 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 6 | ||||
| -rw-r--r-- | toplevel/ide_intf.ml | 610 | ||||
| -rw-r--r-- | toplevel/ide_intf.mli | 99 | ||||
| -rw-r--r-- | toplevel/ide_slave.ml | 32 | ||||
| -rw-r--r-- | toplevel/indschemes.ml | 2 | ||||
| -rw-r--r-- | toplevel/interface.mli | 125 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 4 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 16 |
11 files changed, 546 insertions, 354 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index 52d507a1..7e7dfd17 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -255,7 +255,7 @@ let add_new_coercion_core coef stre source target isid = in check_source (Some cls); if not (uniform_cond (llp-ind) lvs) then - warning (Pp.string_of_ppcmds (explain_coercion_error coef NotUniform)); + msg_warn (Pp.string_of_ppcmds (explain_coercion_error coef NotUniform)); let clt = try get_target tg ind diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 8f954573..85c2ca6e 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -140,6 +140,6 @@ let get_compat_version = function | "8.3" -> Flags.V8_3 | "8.2" -> Flags.V8_2 | ("8.1" | "8.0") as s -> - warning ("Compatibility with version "^s^" not supported."); + msg_warn ("Compatibility with version "^s^" not supported."); Flags.V8_2 | s -> Util.error ("Unknown compatibility version \""^s^"\".") diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index f550df16..2ef8bd2b 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -851,8 +851,8 @@ let error_same_names_overlap idl = str "names:" ++ spc () ++ prlist_with_sep pr_comma pr_id idl ++ str "." -let error_not_an_arity id = - str "The type of" ++ spc () ++ pr_id id ++ spc () ++ str "is not an arity." +let error_not_an_arity env c = + str "The type" ++ spc () ++ pr_lconstr_env env c ++ spc () ++ str "is not an arity." let error_bad_entry () = str "Bad inductive definition." @@ -888,7 +888,7 @@ let explain_inductive_error = function | SameNamesTypes id -> error_same_names_types id | SameNamesConstructors id -> error_same_names_constructors id | SameNamesOverlap idl -> error_same_names_overlap idl - | NotAnArity id -> error_not_an_arity id + | NotAnArity (env, c) -> error_not_an_arity env c | BadEntry -> error_bad_entry () | LargeNonPropInductiveNotInType -> error_large_non_prop_inductive_not_in_type () diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml index 6937eeb8..46b75339 100644 --- a/toplevel/ide_intf.ml +++ b/toplevel/ide_intf.ml @@ -10,7 +10,7 @@ (** WARNING: TO BE UPDATED WHEN MODIFIED! *) -let protocol_version = "20120710" +let protocol_version = "20130425~2" (** * Interface of calls to Coq by CoqIde *) @@ -22,76 +22,143 @@ type xml = Xml_parser.xml (** We use phantom types and GADT to protect ourselves against wild casts *) type 'a call = - | Interp of raw * verbose * string - | Rewind of int - | Goal - | Evars - | Hints - | Status - | Search of search_flags - | GetOptions - | SetOptions of (option_name * option_value) list - | InLoadPath of string - | MkCases of string - | Quit - | About - -(** The structure that coqtop should implement *) - -type handler = { - interp : raw * verbose * string -> string; - rewind : int -> int; - goals : unit -> goals option; - evars : unit -> evar list option; - hints : unit -> (hint list * hint) option; - status : unit -> status; - search : search_flags -> string coq_object list; - get_options : unit -> (option_name * option_state) list; - set_options : (option_name * option_value) list -> unit; - inloadpath : string -> bool; - mkcases : string -> string list list; - quit : unit -> unit; - about : unit -> coq_info; - handle_exn : exn -> location * string; -} + | Interp of interp_sty + | Rewind of rewind_sty + | Goal of goals_sty + | Evars of evars_sty + | Hints of hints_sty + | Status of status_sty + | Search of search_sty + | GetOptions of get_options_sty + | SetOptions of set_options_sty + | InLoadPath of inloadpath_sty + | MkCases of mkcases_sty + | Quit of quit_sty + | About of about_sty + +type unknown (** The actual calls *) -let interp (r,b,s) : string call = Interp (r,b,s) -let rewind i : int call = Rewind i -let goals : goals option call = Goal -let evars : evar list option call = Evars -let hints : (hint list * hint) option call = Hints -let status : status call = Status -let search flags : string coq_object list call = Search flags -let get_options : (option_name * option_state) list call = GetOptions -let set_options l : unit call = SetOptions l -let inloadpath s : bool call = InLoadPath s -let mkcases s : string list list call = MkCases s -let quit : unit call = Quit +let interp x : interp_rty call = Interp x +let rewind x : rewind_rty call = Rewind x +let goals x : goals_rty call = Goal x +let evars x : evars_rty call = Evars x +let hints x : hints_rty call = Hints x +let status x : status_rty call = Status x +let get_options x : get_options_rty call = GetOptions x +let set_options x : set_options_rty call = SetOptions x +let inloadpath x : inloadpath_rty call = InLoadPath x +let mkcases x : mkcases_rty call = MkCases x +let search x : search_rty call = Search x +let quit x : quit_rty call = Quit x (** * Coq answers to CoqIde *) -let abstract_eval_call handler c = +let abstract_eval_call handler (c : 'a call) = + let mkGood x : 'a value = Good (Obj.magic x) in try - let res = match c with - | Interp (r,b,s) -> Obj.magic (handler.interp (r,b,s) : string) - | Rewind i -> Obj.magic (handler.rewind i : int) - | Goal -> Obj.magic (handler.goals () : goals option) - | Evars -> Obj.magic (handler.evars () : evar list option) - | Hints -> Obj.magic (handler.hints () : (hint list * hint) option) - | Status -> Obj.magic (handler.status () : status) - | Search flags -> Obj.magic (handler.search flags : string coq_object list) - | GetOptions -> Obj.magic (handler.get_options () : (option_name * option_state) list) - | SetOptions opts -> Obj.magic (handler.set_options opts : unit) - | InLoadPath s -> Obj.magic (handler.inloadpath s : bool) - | MkCases s -> Obj.magic (handler.mkcases s : string list list) - | Quit -> Obj.magic (handler.quit () : unit) - | About -> Obj.magic (handler.about () : coq_info) - in Good res + match c with + | Interp x -> mkGood (handler.interp x) + | Rewind x -> mkGood (handler.rewind x) + | Goal x -> mkGood (handler.goals x) + | Evars x -> mkGood (handler.evars x) + | Hints x -> mkGood (handler.hints x) + | Status x -> mkGood (handler.status x) + | Search x -> mkGood (handler.search x) + | GetOptions x -> mkGood (handler.get_options x) + | SetOptions x -> mkGood (handler.set_options x) + | InLoadPath x -> mkGood (handler.inloadpath x) + | MkCases x -> mkGood (handler.mkcases x) + | Quit x -> mkGood (handler.quit x) + | About x -> mkGood (handler.about x) with any -> - let (l, str) = handler.handle_exn any in - Fail (l,str) + Fail (handler.handle_exn any) + +(* To read and typecheck the answers we give a description of the types, + and a way to statically check that the reified version is in sync *) +module ReifType : sig + + type 'a val_t + + val unit_t : unit val_t + val string_t : string val_t + val int_t : int val_t + val bool_t : bool val_t + val goals_t : goals val_t + val evar_t : evar val_t + val state_t : status val_t + val coq_info_t : coq_info val_t + val option_state_t : option_state val_t + val option_t : 'a val_t -> 'a option val_t + val list_t : 'a val_t -> 'a list val_t + val coq_object_t : 'a val_t -> 'a coq_object val_t + val pair_t : 'a val_t -> 'b val_t -> ('a * 'b) val_t + val union_t : 'a val_t -> 'b val_t -> ('a ,'b) Util.union val_t + + type value_type = private + | Unit | String | Int | Bool | Goals | Evar | State | Option_state | Coq_info + | Option of value_type + | List of value_type + | Coq_object of value_type + | Pair of value_type * value_type + | Union of value_type * value_type + + val check : 'a val_t -> value_type + +end = struct + + type value_type = + | Unit | String | Int | Bool | Goals | Evar | State | Option_state | Coq_info + | Option of value_type + | List of value_type + | Coq_object of value_type + | Pair of value_type * value_type + | Union of value_type * value_type + + type 'a val_t = value_type + let check x = x + + let unit_t = Unit + let string_t = String + let int_t = Int + let bool_t = Bool + let goals_t = Goals + let evar_t = Evar + let state_t = State + let coq_info_t = Coq_info + let option_state_t = Option_state + let option_t x = Option x + let list_t x = List x + let coq_object_t x = Coq_object x + let pair_t x y = Pair (x, y) + let union_t x y = Union (x, y) + +end + +open ReifType + +(* For every (call : 'a call), we build the reification of 'a. + * In OCaml 4 we could use GATDs to do that I guess *) +let expected_answer_type call : value_type = + let hint = list_t (pair_t string_t string_t) in + let hints = pair_t (list_t hint) hint in + let options = pair_t (list_t string_t) option_state_t in + let objs = coq_object_t string_t in + match call with + | Interp _ -> check (string_t : interp_rty val_t) + | Rewind _ -> check (int_t : rewind_rty val_t) + | Goal _ -> check (option_t goals_t : goals_rty val_t) + | Evars _ -> check (option_t (list_t evar_t) : evars_rty val_t) + | Hints _ -> check (option_t hints : hints_rty val_t) + | Status _ -> check (state_t : status_rty val_t) + | Search _ -> check (list_t objs : search_rty val_t) + | GetOptions _ -> check (list_t options : get_options_rty val_t) + | SetOptions _ -> check (unit_t : set_options_rty val_t) + | InLoadPath _ -> check (bool_t : inloadpath_rty val_t) + | MkCases _ -> check (list_t (list_t string_t) : mkcases_rty val_t) + | Quit _ -> check (unit_t : quit_rty val_t) + | About _ -> check (coq_info_t : about_rty val_t) (** * XML data marshalling *) @@ -113,10 +180,6 @@ let do_match constr t mf = match constr with else raise Marshal_error | _ -> raise Marshal_error -let pcdata = function -| PCData s -> s -| _ -> raise Marshal_error - let singleton = function | [x] -> x | _ -> raise Marshal_error @@ -132,56 +195,68 @@ let bool_arg tag b = if b then [tag, ""] else [] let of_unit () = Element ("unit", [], []) -let to_unit = function +let to_unit : xml -> unit = function | Element ("unit", [], []) -> () | _ -> raise Marshal_error -let of_bool b = +let of_bool (b : bool) : xml = if b then constructor "bool" "true" [] else constructor "bool" "false" [] -let to_bool xml = do_match xml "bool" +let to_bool xml : bool = do_match xml "bool" (fun s _ -> match s with | "true" -> true | "false" -> false | _ -> raise Marshal_error) -let of_list f l = +let of_list (f : 'a -> xml) (l : 'a list) = Element ("list", [], List.map f l) -let to_list f = function +let to_list (f : xml -> 'a) : xml -> 'a list = function | Element ("list", [], l) -> List.map f l | _ -> raise Marshal_error -let of_option f = function +let of_option (f : 'a -> xml) : 'a option -> xml = function | None -> Element ("option", ["val", "none"], []) | Some x -> Element ("option", ["val", "some"], [f x]) -let to_option f = function +let to_option (f : xml -> 'a) : xml -> 'a option = function | Element ("option", ["val", "none"], []) -> None | Element ("option", ["val", "some"], [x]) -> Some (f x) | _ -> raise Marshal_error -let of_string s = Element ("string", [], [PCData s]) +let of_string (s : string) : xml = Element ("string", [], [PCData s]) -let to_string = function +let to_string : xml -> string = function | Element ("string", [], l) -> raw_string l | _ -> raise Marshal_error -let of_int i = Element ("int", [], [PCData (string_of_int i)]) +let of_int (i : int) : xml = Element ("int", [], [PCData (string_of_int i)]) -let to_int = function +let to_int : xml -> int = function | Element ("int", [], [PCData s]) -> (try int_of_string s with Failure _ -> raise Marshal_error) | _ -> raise Marshal_error -let of_pair f g (x, y) = Element ("pair", [], [f x; g y]) +let of_pair (f : 'a -> xml) (g : 'b -> xml) : 'a * 'b -> xml = + function (x,y) -> Element ("pair", [], [f x; g y]) -let to_pair f g = function +let to_pair (f : xml -> 'a) (g : xml -> 'b) : xml -> 'a * 'b = function | Element ("pair", [], [x; y]) -> (f x, g y) | _ -> raise Marshal_error +let of_union (f : 'a -> xml) (g : 'b -> xml) : ('a,'b) Util.union -> xml = +function +| Util.Inl x -> Element ("union", ["val","in_l"], [f x]) +| Util.Inr x -> Element ("union", ["val","in_r"], [g x]) + +let to_union (f : xml -> 'a) (g : xml -> 'b) : xml -> ('a,'b) Util.union= +function +| Element ("union", ["val","in_l"], [x]) -> Util.Inl (f x) +| Element ("union", ["val","in_r"], [x]) -> Util.Inr (g x) +| _ -> raise Marshal_error + (** More elaborate types *) let of_option_value = function @@ -275,7 +350,7 @@ let to_value f = function let loc_s = int_of_string (List.assoc "loc_s" attrs) in let loc_e = int_of_string (List.assoc "loc_e" attrs) in Some (loc_s, loc_e) - with e when e <> Sys.Break -> None + with Not_found | Failure _ -> None in let msg = raw_string l in Fail (loc, msg) @@ -283,23 +358,24 @@ let to_value f = function | _ -> raise Marshal_error let of_call = function -| Interp (raw, vrb, cmd) -> +| Interp (id,raw, vrb, cmd) -> let flags = (bool_arg "raw" raw) @ (bool_arg "verbose" vrb) in - Element ("call", ("val", "interp") :: flags, [PCData cmd]) + Element ("call", ("val", "interp") :: ("id", string_of_int id) :: flags, + [PCData cmd]) | Rewind n -> Element ("call", ("val", "rewind") :: ["steps", string_of_int n], []) -| Goal -> +| Goal () -> Element ("call", ["val", "goal"], []) -| Evars -> +| Evars () -> Element ("call", ["val", "evars"], []) -| Hints -> +| Hints () -> Element ("call", ["val", "hints"], []) -| Status -> +| Status () -> Element ("call", ["val", "status"], []) | Search flags -> let args = List.map (of_pair of_search_constraint of_bool) flags in Element ("call", ["val", "search"], args) -| GetOptions -> +| GetOptions () -> Element ("call", ["val", "getoptions"], []) | SetOptions opts -> let args = List.map (of_pair (of_list of_string) of_option_value) opts in @@ -308,37 +384,40 @@ let of_call = function Element ("call", ["val", "inloadpath"], [PCData file]) | MkCases ind -> Element ("call", ["val", "mkcases"], [PCData ind]) -| Quit -> +| Quit () -> Element ("call", ["val", "quit"], []) -| About -> +| About () -> Element ("call", ["val", "about"], []) let to_call = function | Element ("call", attrs, l) -> let ans = massoc "val" attrs in begin match ans with - | "interp" -> - let raw = List.mem_assoc "raw" attrs in - let vrb = List.mem_assoc "verbose" attrs in - Interp (raw, vrb, raw_string l) + | "interp" -> begin + try + let id = List.assoc "id" attrs in + let raw = List.mem_assoc "raw" attrs in + let vrb = List.mem_assoc "verbose" attrs in + Interp (int_of_string id, raw, vrb, raw_string l) + with Not_found -> raise Marshal_error end | "rewind" -> let steps = int_of_string (massoc "steps" attrs) in Rewind steps - | "goal" -> Goal - | "evars" -> Evars - | "status" -> Status + | "goal" -> Goal () + | "evars" -> Evars () + | "status" -> Status () | "search" -> let args = List.map (to_pair to_search_constraint to_bool) l in Search args - | "getoptions" -> GetOptions + | "getoptions" -> GetOptions () | "setoptions" -> let args = List.map (to_pair (to_list to_string) to_option_value) l in SetOptions args | "inloadpath" -> InLoadPath (raw_string l) | "mkcases" -> MkCases (raw_string l) - | "hints" -> Hints - | "quit" -> Quit - | "about" -> About + | "hints" -> Hints () + | "quit" -> Quit () + | "about" -> About () | _ -> raise Marshal_error end | _ -> raise Marshal_error @@ -419,181 +498,216 @@ let to_coq_info = function } | _ -> raise Marshal_error +let of_message_level = function +| Debug s -> constructor "message_level" "debug" [PCData s] +| Info -> constructor "message_level" "info" [] +| Notice -> constructor "message_level" "notice" [] +| Warning -> constructor "message_level" "warning" [] +| Error -> constructor "message_level" "error" [] + +let to_message_level xml = do_match xml "message_level" + (fun s args -> match s with + | "debug" -> Debug (raw_string args) + | "info" -> Info + | "notice" -> Notice + | "warning" -> Warning + | "error" -> Error + | _ -> raise Marshal_error) + +let of_message msg = + let lvl = of_message_level msg.message_level in + let content = of_string msg.message_content in + Element ("message", [], [lvl; content]) + +let to_message xml = match xml with +| Element ("message", [], [lvl; content]) -> + { message_level = to_message_level lvl; message_content = to_string content } +| _ -> raise Marshal_error + +let is_message = function +| Element ("message", _, _) -> true +| _ -> false + +let of_loc loc = + let start, stop = loc in + Element ("loc",[("start",string_of_int start);("stop",string_of_int stop)],[]) + +let to_loc xml = match xml with +| Element ("loc", l,[]) -> + (try + let start = List.assoc "start" l in + let stop = List.assoc "stop" l in + (int_of_string start, int_of_string stop) + with Not_found | Invalid_argument _ -> raise Marshal_error) +| _ -> raise Marshal_error + +let to_feedback_content xml = do_match xml "feedback_content" + (fun s args -> match s with + | "addedaxiom" -> AddedAxiom + | "processed" -> Processed + | "globref" -> + (match args with + | [loc; filepath; modpath; ident; ty] -> + GlobRef(to_loc loc, to_string filepath, to_string modpath, + to_string ident, to_string ty) + | _ -> raise Marshal_error) + | _ -> raise Marshal_error) + +let of_feedback_content = function +| AddedAxiom -> constructor "feedback_content" "addedaxiom" [] +| Processed -> constructor "feedback_content" "processed" [] +| GlobRef(loc, filepath, modpath, ident, ty) -> + constructor "feedback_content" "globref" [ + of_loc loc; + of_string filepath; + of_string modpath; + of_string ident; + of_string ty + ] + +let of_feedback msg = + let content = of_feedback_content msg.content in + Element ("feedback", ["id",string_of_int msg.edit_id], [content]) + +let to_feedback xml = match xml with +| Element ("feedback", ["id",id], [content]) -> + { edit_id = int_of_string id; + content = to_feedback_content content } +| _ -> raise Marshal_error + +let is_feedback = function +| Element ("feedback", _, _) -> true +| _ -> false + (** Conversions between ['a value] and xml answers When decoding an xml answer, we dynamically check that it is compatible with the original call. For that we now rely on the fact that all sub-fonctions [to_xxx : xml -> xxx] check that the current xml element - is "xxx", and raise [Marshal_error] if anything goes wrong. -*) - -type value_type = - | Unit | String | Int | Bool | Goals | Evar | State | Option_state | Coq_info - | Option of value_type - | List of value_type - | Coq_object of value_type - | Pair of value_type * value_type - -let hint = List (Pair (String, String)) -let option_name = List String - -let expected_answer_type = function - | Interp _ -> String - | Rewind _ -> Int - | Goal -> Option Goals - | Evars -> Option (List Evar) - | Hints -> Option (Pair (List hint, hint)) - | Status -> State - | Search _ -> List (Coq_object String) - | GetOptions -> List (Pair (option_name, Option_state)) - | SetOptions _ -> Unit - | InLoadPath _ -> Bool - | MkCases _ -> List (List String) - | Quit -> Unit - | About -> Coq_info + is "xxx", and raise [Marshal_error] if anything goes wrong. *) let of_answer (q : 'a call) (r : 'a value) : xml = let rec convert ty : 'a -> xml = match ty with - | Unit -> Obj.magic of_unit - | Bool -> Obj.magic of_bool - | String -> Obj.magic of_string - | Int -> Obj.magic of_int - | State -> Obj.magic of_status - | Option_state -> Obj.magic of_option_state - | Coq_info -> Obj.magic of_coq_info - | Goals -> Obj.magic of_goals - | Evar -> Obj.magic of_evar - | List t -> Obj.magic (of_list (convert t)) - | Option t -> Obj.magic (of_option (convert t)) - | Coq_object t -> Obj.magic (of_coq_object (convert t)) - | Pair (t1,t2) -> Obj.magic (of_pair (convert t1) (convert t2)) + | Unit -> Obj.magic of_unit + | Bool -> Obj.magic of_bool + | String -> Obj.magic of_string + | Int -> Obj.magic of_int + | State -> Obj.magic of_status + | Option_state -> Obj.magic of_option_state + | Coq_info -> Obj.magic of_coq_info + | Goals -> Obj.magic of_goals + | Evar -> Obj.magic of_evar + | List t -> Obj.magic (of_list (convert t)) + | Option t -> Obj.magic (of_option (convert t)) + | Coq_object t -> Obj.magic (of_coq_object (convert t)) + | Pair (t1,t2) -> Obj.magic (of_pair (convert t1) (convert t2)) + | Union (t1,t2) -> Obj.magic (of_union (convert t1) (convert t2)) in of_value (convert (expected_answer_type q)) r let to_answer xml (c : 'a call) : 'a value = let rec convert ty : xml -> 'a = match ty with - | Unit -> Obj.magic to_unit - | Bool -> Obj.magic to_bool - | String -> Obj.magic to_string - | Int -> Obj.magic to_int - | State -> Obj.magic to_status - | Option_state -> Obj.magic to_option_state - | Coq_info -> Obj.magic to_coq_info - | Goals -> Obj.magic to_goals - | Evar -> Obj.magic to_evar - | List t -> Obj.magic (to_list (convert t)) - | Option t -> Obj.magic (to_option (convert t)) - | Coq_object t -> Obj.magic (to_coq_object (convert t)) - | Pair (t1,t2) -> Obj.magic (to_pair (convert t1) (convert t2)) + | Unit -> Obj.magic to_unit + | Bool -> Obj.magic to_bool + | String -> Obj.magic to_string + | Int -> Obj.magic to_int + | State -> Obj.magic to_status + | Option_state -> Obj.magic to_option_state + | Coq_info -> Obj.magic to_coq_info + | Goals -> Obj.magic to_goals + | Evar -> Obj.magic to_evar + | List t -> Obj.magic (to_list (convert t)) + | Option t -> Obj.magic (to_option (convert t)) + | Coq_object t -> Obj.magic (to_coq_object (convert t)) + | Pair (t1,t2) -> Obj.magic (to_pair (convert t1) (convert t2)) + | Union (t1,t2) -> Obj.magic (to_union (convert t1) (convert t2)) in to_value (convert (expected_answer_type c)) xml (** * Debug printing *) +let pr_unit () = "" +let pr_string s = Printf.sprintf "%S" s +let pr_int i = string_of_int i +let pr_bool b = Printf.sprintf "%B" b +let pr_goal (g : goals) = + if g.fg_goals = [] then + if g.bg_goals = [] then "Proof completed." + else + let rec pr_focus _ = function + | [] -> assert false + | [lg, rg] -> Printf.sprintf "%i" (List.length lg + List.length rg) + | (lg, rg) :: l -> + Printf.sprintf "%i:%a" (List.length lg + List.length rg) pr_focus l in + Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals + else + let pr_menu s = s in + let pr_goal { goal_hyp = hyps; goal_ccl = goal } = + "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^ + pr_menu goal ^ "]" in + String.concat " " (List.map pr_goal g.fg_goals) +let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]" +let pr_status (s : status) = + let path = + let l = String.concat "." s.status_path in + "path=" ^ l ^ ";" in + let name = match s.status_proofname with + | None -> "no proof;" + | Some n -> "proof = " ^ n ^ ";" in + "Status: " ^ path ^ name +let pr_coq_info (i : coq_info) = "FIXME" let pr_option_value = function -| IntValue None -> "none" -| IntValue (Some i) -> string_of_int i -| StringValue s -> s -| BoolValue b -> if b then "true" else "false" - -let rec pr_setoptions opts = - let map (key, v) = - let key = String.concat " " key in - key ^ " := " ^ (pr_option_value v) - in - String.concat "; " (List.map map opts) - -let pr_getoptions opts = - let map (key, s) = - let key = String.concat " " key in - Printf.sprintf "%s: sync := %b; depr := %b; name := %s; value := %s\n" - key s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value) - in - "\n" ^ String.concat "" (List.map map opts) + | IntValue None -> "none" + | IntValue (Some i) -> string_of_int i + | StringValue s -> s + | BoolValue b -> if b then "true" else "false" +let pr_option_state (s : option_state) = + Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n" + s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value) +let pr_list pr l = "["^String.concat ";" (List.map pr l)^"]" +let pr_option pr = function None -> "None" | Some x -> "Some("^pr x^")" +let pr_coq_object (o : 'a coq_object) = "FIXME" +let pr_pair pr1 pr2 (a,b) = "("^pr1 a^","^pr2 b^")" +let pr_union pr1 pr2 = function Util.Inl x -> pr1 x | Util.Inr x -> pr2 x let pr_call = function - | Interp (r,b,s) -> + | Interp (id,r,b,s) -> let raw = if r then "RAW" else "" in let verb = if b then "" else "SILENT" in - "INTERP"^raw^verb^" ["^s^"]" + "INTERP"^raw^verb^" "^string_of_int id^" ["^s^"]" | Rewind i -> "REWIND "^(string_of_int i) - | Goal -> "GOALS" - | Evars -> "EVARS" - | Hints -> "HINTS" - | Status -> "STATUS" + | Goal _ -> "GOALS" + | Evars _ -> "EVARS" + | Hints _ -> "HINTS" + | Status _ -> "STATUS" | Search _ -> "SEARCH" - | GetOptions -> "GETOPTIONS" - | SetOptions l -> "SETOPTIONS" ^ " [" ^ pr_setoptions l ^ "]" + | GetOptions _ -> "GETOPTIONS" + | SetOptions l -> "SETOPTIONS" ^ " [" ^ + String.concat ";" + (List.map (pr_pair (pr_list pr_string) pr_option_value) l) ^ "]" | InLoadPath s -> "INLOADPATH "^s | MkCases s -> "MKCASES "^s - | Quit -> "QUIT" - | About -> "ABOUT" - + | Quit _ -> "QUIT" + | About _ -> "ABOUT" let pr_value_gen pr = function | Good v -> "GOOD " ^ pr v | Fail (_,str) -> "FAIL ["^str^"]" - -let pr_value v = pr_value_gen (fun _ -> "") v - -let pr_string s = "["^s^"]" -let pr_bool b = if b then "true" else "false" - -let pr_status s = - let path = - let l = String.concat "." s.status_path in - "path=" ^ l ^ ";" - in - let name = match s.status_proofname with - | None -> "no proof;" - | Some n -> "proof = " ^ n ^ ";" - in - "Status: " ^ path ^ name - -let pr_mkcases l = - let l = List.map (String.concat " ") l in - "[" ^ String.concat " | " l ^ "]" - -let pr_goals_aux g = - if g.fg_goals = [] then - if g.bg_goals = [] then "Proof completed." - else - let rec pr_focus _ = function - | [] -> assert false - | [lg, rg] -> Printf.sprintf "%i" (List.length lg + List.length rg) - | (lg, rg) :: l -> - Printf.sprintf "%i:%a" (List.length lg + List.length rg) pr_focus l - in - Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals - else - let pr_menu s = s in - let pr_goal { goal_hyp = hyps; goal_ccl = goal } = - "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^ pr_menu goal ^ "]" - in - String.concat " " (List.map pr_goal g.fg_goals) - -let pr_goals = function -| None -> "No proof in progress." -| Some g -> pr_goals_aux g - -let pr_evar ev = "[" ^ ev.evar_info ^ "]" - -let pr_evars = function -| None -> "No proof in progress." -| Some evars -> String.concat " " (List.map pr_evar evars) - +let pr_value v = pr_value_gen (fun _ -> "FIXME") v let pr_full_value call value = - match call with - | Interp _ -> pr_value_gen pr_string (Obj.magic value : string value) - | Rewind i -> pr_value_gen string_of_int (Obj.magic value : int value) - | Goal -> pr_value_gen pr_goals (Obj.magic value : goals option value) - | Evars -> pr_value_gen pr_evars (Obj.magic value : evar list option value) - | Hints -> pr_value value - | Status -> pr_value_gen pr_status (Obj.magic value : status value) - | Search _ -> pr_value value - | GetOptions -> pr_value_gen pr_getoptions (Obj.magic value : (option_name * option_state) list value) - | SetOptions _ -> pr_value value - | InLoadPath s -> pr_value_gen pr_bool (Obj.magic value : bool value) - | MkCases s -> pr_value_gen pr_mkcases (Obj.magic value : string list list value) - | Quit -> pr_value value - | About -> pr_value value - + let rec pr = function + | Unit -> Obj.magic pr_unit + | Bool -> Obj.magic pr_bool + | String -> Obj.magic pr_string + | Int -> Obj.magic pr_int + | State -> Obj.magic pr_status + | Option_state -> Obj.magic pr_option_state + | Coq_info -> Obj.magic pr_coq_info + | Goals -> Obj.magic pr_goal + | Evar -> Obj.magic pr_evar + | List t -> Obj.magic (pr_list (pr t)) + | Option t -> Obj.magic (pr_option (pr t)) + | Coq_object t -> Obj.magic pr_coq_object + | Pair (t1,t2) -> Obj.magic (pr_pair (pr t1) (pr t2)) + | Union (t1,t2) -> Obj.magic (pr_union (pr t1) (pr t2)) + in + pr_value_gen (pr (expected_answer_type call)) value diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli index 7d0685b1..aa3f91bf 100644 --- a/toplevel/ide_intf.mli +++ b/toplevel/ide_intf.mli @@ -14,78 +14,20 @@ type xml = Xml_parser.xml type 'a call -(** Running a command (given as a string). - - The 1st flag indicates whether to use "raw" mode - (less sanity checks, no impact on the undo stack). - Suitable e.g. for queries, or for the Set/Unset - of display options that coqide performs all the time. - - The 2nd flag controls the verbosity. - - The returned string contains the messages produced - by this command, but not the updated goals (they are - to be fetch by a separated [current_goals]). *) -val interp : raw * verbose * string -> string call - -(** Backtracking by at least a certain number of phrases. - No finished proofs will be re-opened. Instead, - we continue backtracking until before these proofs, - and answer the amount of extra backtracking performed. - Backtracking by more than the number of phrases already - interpreted successfully (and not yet undone) will fail. *) -val rewind : int -> int call - -(** Fetching the list of current goals. Return [None] if no proof is in - progress, [Some gl] otherwise. *) -val goals : goals option call - -(** Retrieving the tactics applicable to the current goal. [None] if there is - no proof in progress. *) -val hints : (hint list * hint) option call - -(** The status, for instance "Ready in SomeSection, proving Foo" *) -val status : status call - -(** Is a directory part of Coq's loadpath ? *) -val inloadpath : string -> bool call - -(** Create a "match" template for a given inductive type. - For each branch of the match, we list the constructor name - followed by enough pattern variables. *) -val mkcases : string -> string list list call - -(** Retrieve the list of unintantiated evars in the current proof. [None] if no - proof is in progress. *) -val evars : evar list option call - -(** Retrieve the list of options of the current toplevel, together with their - state. *) -val get_options : (option_name * option_state) list call - -(** Set the options to the given value. Warning: this is not atomic, so whenever - the call fails, the option state can be messed up... This is the caller duty - to check that everything is correct. *) -val set_options : (option_name * option_value) list -> unit call - -(** Quit gracefully the interpreter. *) -val quit : unit call - -(** The structure that coqtop should implement *) - -type handler = { - interp : raw * verbose * string -> string; - rewind : int -> int; - goals : unit -> goals option; - evars : unit -> evar list option; - hints : unit -> (hint list * hint) option; - status : unit -> status; - search : search_flags -> string coq_object list; - get_options : unit -> (option_name * option_state) list; - set_options : (option_name * option_value) list -> unit; - inloadpath : string -> bool; - mkcases : string -> string list list; - quit : unit -> unit; - about : unit -> coq_info; - handle_exn : exn -> location * string; -} +type unknown + +val interp : interp_sty -> interp_rty call +val rewind : rewind_sty -> rewind_rty call +val goals : goals_sty -> goals_rty call +val hints : hints_sty -> hints_rty call +val status : status_sty -> status_rty call +val inloadpath : inloadpath_sty -> inloadpath_rty call +val mkcases : mkcases_sty -> mkcases_rty call +val evars : evars_sty -> evars_rty call +val search : search_sty -> search_rty call +val get_options : get_options_sty -> get_options_rty call +val set_options : set_options_sty -> set_options_rty call +val quit : quit_sty -> quit_rty call val abstract_eval_call : handler -> 'a call -> 'a value @@ -97,11 +39,18 @@ val protocol_version : string exception Marshal_error +val of_call : 'a call -> xml +val to_call : xml -> unknown call + +val of_message : message -> xml +val to_message : xml -> message +val is_message : xml -> bool + val of_value : ('a -> xml) -> 'a value -> xml -val to_value : (xml -> 'a) -> xml -> 'a value -val of_call : 'a call -> xml -val to_call : xml -> 'a call +val of_feedback : feedback -> xml +val to_feedback : xml -> feedback +val is_feedback : xml -> bool val of_answer : 'a call -> 'a value -> xml val to_answer : xml -> 'a call -> 'a value diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 6e9a0ee0..019f8a69 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -112,7 +112,7 @@ let coqide_cmd_checks (loc,ast) = (** Interpretation (cf. [Ide_intf.interp]) *) -let interp (raw,verbosely,s) = +let interp (id,raw,verbosely,s) = let pa = Pcoq.Gram.parsable (Stream.of_string s) in let loc_ast = Vernac.parse_sentence (pa,None) in if not raw then coqide_cmd_checks loc_ast; @@ -371,7 +371,7 @@ let eval_call c = (* Here we do send an acknowledgement message to prove everything went OK. *) let dummy = Interface.Good () in - let xml_answer = Ide_intf.of_answer Ide_intf.quit dummy in + let xml_answer = Ide_intf.of_answer (Ide_intf.quit ()) dummy in let () = Xml_utils.print_xml !orig_stdout xml_answer in let () = flush !orig_stdout in let () = pr_debug "Exiting gracefully." in @@ -392,20 +392,20 @@ let eval_call c = r in let handler = { - Ide_intf.interp = interruptible interp; - Ide_intf.rewind = interruptible Backtrack.back; - Ide_intf.goals = interruptible goals; - Ide_intf.evars = interruptible evars; - Ide_intf.hints = interruptible hints; - Ide_intf.status = interruptible status; - Ide_intf.search = interruptible search; - Ide_intf.inloadpath = interruptible inloadpath; - Ide_intf.get_options = interruptible get_options; - Ide_intf.set_options = interruptible set_options; - Ide_intf.mkcases = interruptible Vernacentries.make_cases; - Ide_intf.quit = (fun () -> raise Quit); - Ide_intf.about = interruptible about; - Ide_intf.handle_exn = handle_exn; } + Interface.interp = interruptible interp; + Interface.rewind = interruptible Backtrack.back; + Interface.goals = interruptible goals; + Interface.evars = interruptible evars; + Interface.hints = interruptible hints; + Interface.status = interruptible status; + Interface.search = interruptible search; + Interface.inloadpath = interruptible inloadpath; + Interface.get_options = interruptible get_options; + Interface.set_options = interruptible set_options; + Interface.mkcases = interruptible Vernacentries.make_cases; + Interface.quit = (fun () -> raise Quit); + Interface.about = interruptible about; + Interface.handle_exn = handle_exn; } in (* If the messages of last command are still there, we remove them *) ignore (read_stdout ()); diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index e30404e1..c8292937 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -271,7 +271,7 @@ let declare_congr_scheme ind = then ignore (define_individual_scheme congr_scheme_kind KernelVerbose None ind) else - warning "Cannot build congruence scheme because eq is not found" + msg_warn "Cannot build congruence scheme because eq is not found" end let declare_sym_scheme ind = diff --git a/toplevel/interface.mli b/toplevel/interface.mli index 7b4312a3..f2a22f22 100644 --- a/toplevel/interface.mli +++ b/toplevel/interface.mli @@ -86,8 +86,8 @@ type search_constraint = the flag should be negated. *) type search_flags = (search_constraint * bool) list -(** A named object in Coq. [coq_object_qualid] is the shortest path defined for - the user. [coq_object_prefix] is the missing part to recover the fully +(** A named object in Coq. [coq_object_qualid] is the shortest path defined for + the user. [coq_object_prefix] is the missing part to recover the fully qualified name, i.e [fully_qualified = coq_object_prefix + coq_object_qualid]. [coq_object_object] is the actual content of the object. *) type 'a coq_object = { @@ -103,10 +103,129 @@ type coq_info = { compile_date : string; } -(** * Coq answers to CoqIde *) +(** Coq unstructured messages *) + +type message_level = + | Debug of string + | Info + | Notice + | Warning + | Error + +type message = { + message_level : message_level; + message_content : string; +} + +(** Coq "semantic" infos obtained during parsing/execution *) +type edit_id = int + +type feedback_content = + | AddedAxiom + | Processed + | GlobRef of (int*int) * string * string * string * string + +type feedback = { + edit_id : edit_id; + content : feedback_content; +} + +(** Calls result *) type location = (int * int) option (* start and end of the error *) type 'a value = | Good of 'a | Fail of (location * string) + +(* Request/Reply message protocol between Coq and CoqIde *) + +(** Running a command (given as its id and its text). + "raw" mode (less sanity checks, no impact on the undo stack) + is suitable for queries, or for the Set/Unset + of display options that coqide performs all the time. + The returned string contains the messages produced + but not the updated goals (they are + to be fetch by a separated [current_goals]). *) +type interp_sty = edit_id * raw * verbose * string +type interp_rty = string + +(** Backtracking by at least a certain number of phrases. + No finished proofs will be re-opened. Instead, + we continue backtracking until before these proofs, + and answer the amount of extra backtracking performed. + Backtracking by more than the number of phrases already + interpreted successfully (and not yet undone) will fail. *) +type rewind_sty = int +type rewind_rty = int + +(** Fetching the list of current goals. Return [None] if no proof is in + progress, [Some gl] otherwise. *) +type goals_sty = unit +type goals_rty = goals option + +(** Retrieve the list of unintantiated evars in the current proof. [None] if no + proof is in progress. *) +type evars_sty = unit +type evars_rty = evar list option + +(** Retrieving the tactics applicable to the current goal. [None] if there is + no proof in progress. *) +type hints_sty = unit +type hints_rty = (hint list * hint) option + +(** The status, for instance "Ready in SomeSection, proving Foo" *) +type status_sty = unit +type status_rty = status + +(** Search for objects satisfying the given search flags. *) +type search_sty = search_flags +type search_rty = string coq_object list + +(** Retrieve the list of options of the current toplevel *) +type get_options_sty = unit +type get_options_rty = (option_name * option_state) list + +(** Set the options to the given value. Warning: this is not atomic, so whenever + the call fails, the option state can be messed up... This is the caller duty + to check that everything is correct. *) +type set_options_sty = (option_name * option_value) list +type set_options_rty = unit + +(** Is a directory part of Coq's loadpath ? *) +type inloadpath_sty = string +type inloadpath_rty = bool + +(** Create a "match" template for a given inductive type. + For each branch of the match, we list the constructor name + followed by enough pattern variables. *) +type mkcases_sty = string +type mkcases_rty = string list list + +(** Quit gracefully the interpreter. *) +type quit_sty = unit +type quit_rty = unit + +type about_sty = unit +type about_rty = coq_info + +type handle_exn_rty = location * string +type handle_exn_sty = exn + +type handler = { + interp : interp_sty -> interp_rty; + rewind : rewind_sty -> rewind_rty; + goals : goals_sty -> goals_rty; + evars : evars_sty -> evars_rty; + hints : hints_sty -> hints_rty; + status : status_sty -> status_rty; + search : search_sty -> search_rty; + get_options : get_options_sty -> get_options_rty; + set_options : set_options_sty -> set_options_rty; + inloadpath : inloadpath_sty -> inloadpath_rty; + mkcases : mkcases_sty -> mkcases_rty; + quit : quit_sty -> quit_rty; + about : about_sty -> about_rty; + handle_exn : handle_exn_sty -> handle_exn_rty; +} + diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 006dc5ec..7653bfc4 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -851,7 +851,7 @@ let check_rule_productivity l = error "A recursive notation must start with at least one symbol." let is_not_printable = function - | AVar _ -> warning "This notation will not be used for printing as it is bound to a \nsingle variable"; true + | AVar _ -> msg_warn "This notation will not be used for printing as it is bound to a \nsingle variable"; true | _ -> false let find_precedence lev etyps symbols = @@ -909,7 +909,7 @@ let remove_curly_brackets l = (match next' with | Terminal "}" as t2 :: l'' as l1 -> if l <> l0 or l' <> l1 then - warning "Skipping spaces inside curly brackets"; + msg_warn "Skipping spaces inside curly brackets"; if deb & l'' = [] then [t1;x;t2] else begin check_curly_brackets_notation_exists (); x :: aux false l'' diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index f08308d3..b6639c06 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -117,7 +117,7 @@ let dir_ml_load s = let dir_ml_use s = match !load with | WithTop t -> t.use_file s - | _ -> warning "Cannot access the ML compiler" + | _ -> msg_warn "Cannot access the ML compiler" (* Adds a path to the ML paths *) let add_ml_dir s = diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 75efe139..e7db8fac 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -801,7 +801,7 @@ let vernac_chdir = function | Some path -> begin try Sys.chdir (System.expand_path_macros path) - with Sys_error str -> warning ("Cd failed: " ^ str) + with Sys_error str -> msg_warn ("Cd failed: " ^ str) end; if_verbose message (Sys.getcwd()) @@ -883,6 +883,12 @@ let vernac_declare_arguments local r l nargs flags = | x, _ -> x in List.map (fun ns -> List.map name_anons (List.combine ns inf_names)) l in let names_decl = List.map (List.map (fun (id, _,_,_,_) -> id)) l in + let renamed_arg = ref None in + let set_renamed a b = + if !renamed_arg = None && a <> b then renamed_arg := Some(b,a) in + let pr_renamed_arg () = match !renamed_arg with None -> "" + | Some (o,n) -> + "\nArgument "^string_of_id o ^" renamed to "^string_of_id n^"." in let some_renaming_specified = try Arguments_renaming.arguments_names sr <> names_decl with Not_found -> false in @@ -894,15 +900,19 @@ let vernac_declare_arguments local r l nargs flags = | (Name x, _,_, true, _), Anonymous -> error ("Argument "^string_of_id x^" cannot be declared implicit.") | (Name iid, _,_, true, max), Name id -> + set_renamed iid id; b || iid <> id, Some (ExplByName id, max, false) - | (Name iid, _,_, _, _), Name id -> b || iid <> id, None + | (Name iid, _,_, _, _), Name id -> + set_renamed iid id; + b || iid <> id, None | _ -> b, None) sr (List.combine il inf_names) in sr || sr', Util.list_map_filter (fun x -> x) impl) some_renaming_specified l in if some_renaming_specified then if not (List.mem `Rename flags) then - error "To rename arguments the \"rename\" flag must be specified." + error ("To rename arguments the \"rename\" flag must be specified." + ^ pr_renamed_arg ()) else Arguments_renaming.rename_arguments local sr names_decl; (* All other infos are in the first item of l *) let l = List.hd l in |