Merge PR #6288: Interfaces for checker and IDE.

23 files changed, 201 insertions, 139 deletions

diff --git a/Makefile.checker b/Makefile.checker
index 5b5855782f..8334b6a2a6 100644
--- a/Makefile.checker
+++ b/Makefile.checker
@@ -33,7 +33,7 @@ CHECKERDEPS := $(addsuffix .d, $(CHECKMLDFILE) $(CHECKMLLIBFILE))
 -include $(CHECKERDEPS)
 
 ifeq ($(BEST),opt)
-$(CHICKEN): checker/check.cmxa checker/main.ml
+$(CHICKEN): checker/check.cmxa checker/main.mli checker/main.ml
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^
 	$(STRIP) $@
@@ -43,7 +43,7 @@ $(CHICKEN): $(CHICKENBYTE)
 	cp $< $@
 endif
 
-$(CHICKENBYTE): checker/check.cma checker/main.ml
+$(CHICKENBYTE): checker/check.cma checker/main.mli checker/main.ml
 	$(SHOW)'OCAMLC -o $@'
 	$(HIDE)$(OCAMLC) -linkpkg $(SYSMOD) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^
 
diff --git a/Makefile.ide b/Makefile.ide
index 08829b5544..09eef1f6bb 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -45,8 +45,8 @@ IDEDEPS:=clib/clib.cma lib/lib.cma
 IDECMA:=ide/ide.cma
 IDETOPLOOPCMA=ide/coqidetop.cma
 
-LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.ml
-LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml
+LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.mli ide/coqide_main.ml
+LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.mli ide/coqide_main.ml
 
 IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map
 
diff --git a/checker/checker.mli b/checker/checker.mli
new file mode 100644
index 0000000000..ceab137747
--- /dev/null
+++ b/checker/checker.mli
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val start : unit -> unit
diff --git a/checker/main.mli b/checker/main.mli
new file mode 100644
index 0000000000..e1555ba2e2
--- /dev/null
+++ b/checker/main.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* This empty file avoids a race condition that occurs when compiling a .ml file
+   that does not have a corresponding .mli file *)
diff --git a/checker/print.mli b/checker/print.mli
new file mode 100644
index 0000000000..3b2715de92
--- /dev/null
+++ b/checker/print.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Cic
+
+val print_pure_constr : constr -> unit
diff --git a/checker/validate.ml b/checker/validate.ml
index 8200405878..2624e6d495 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -49,8 +49,6 @@ let (/) (ctx:error_context) s : error_context = s::ctx
 exception ValidObjError of string * error_context * Obj.t
 let fail ctx o s = raise (ValidObjError(s,ctx,o))
 
-type func = error_context -> Obj.t -> unit
-
 (* Check that object o is a block with tag t *)
 let val_tag t ctx o =
   if Obj.is_block o && Obj.tag o = t then ()
diff --git a/checker/validate.mli b/checker/validate.mli
new file mode 100644
index 0000000000..7eed692a0b
--- /dev/null
+++ b/checker/validate.mli
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val validate : bool -> Values.value -> 'a -> unit
diff --git a/checker/values.ml b/checker/values.ml
index 5a371164c6..4698227ff0 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -372,22 +372,3 @@ let v_lib =
 let v_opaques = Array (v_computation v_constr)
 let v_univopaques =
   Opt (Tuple ("univopaques",[|Array (v_computation v_context_set);v_context_set;v_bool|]))
-
-(** Registering dynamic values *)
-
-module IntOrd =
-struct
-  type t = int
-  let compare (x : t) (y : t) = compare x y
-end
-
-module IntMap = Map.Make(IntOrd)
-
-let dyn_table : value IntMap.t ref = ref IntMap.empty
-
-let register_dyn name t =
-  dyn_table := IntMap.add name t !dyn_table
-
-let find_dyn name =
-  try IntMap.find name !dyn_table
-  with Not_found -> Any
diff --git a/checker/values.mli b/checker/values.mli
new file mode 100644
index 0000000000..aad8fd5f45
--- /dev/null
+++ b/checker/values.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type value =
+  | Any
+  | Fail of string
+  | Tuple of string * value array
+  | Sum of string * int * value array array
+  | Array of value
+  | List of value
+  | Opt of value
+  | Int
+  | String
+  | Annot of string * value
+  | Dyn
+
+val v_univopaques : value
+val v_libsum : value
+val v_lib : value
+val v_opaques : value
+val v_stm_seg : value
diff --git a/checker/votour.ml b/checker/votour.ml
index 77c9999c42..8cb97a2b1b 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -210,7 +210,6 @@ let access_list v o pos =
 let access_block o = match Repr.repr o with
 | BLOCK (tag, os) -> (tag, os)
 | _ -> raise Exit
-let access_int o = match Repr.repr o with INT i -> i | _ -> raise Exit
 
 (** raises Exit if the object has not the expected structure *)
 exception Forbidden
@@ -249,8 +248,7 @@ let rec get_children v o pos = match v with
   |Dyn ->
     begin match Repr.repr o with
     | BLOCK (0, [|id; o|]) ->
-      let n = access_int id in
-      let tpe = find_dyn n in
+      let tpe = Any in
       [|(Int, id, 0 :: pos); (tpe, o, 1 :: pos)|]
     | _ -> raise Exit
     end
@@ -395,7 +393,7 @@ let visit_vo f =
     | None -> ()
   done
 
-let main =
+let () =
   if not !Sys.interactive then
     Arg.parse [] visit_vo
       ("votour: guided tour of a Coq .vo or .vi file\n"^
diff --git a/checker/votour.mli b/checker/votour.mli
new file mode 100644
index 0000000000..e1555ba2e2
--- /dev/null
+++ b/checker/votour.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* This empty file avoids a race condition that occurs when compiling a .ml file
+   that does not have a corresponding .mli file *)
diff --git a/ide/config_lexer.mli b/ide/config_lexer.mli
new file mode 100644
index 0000000000..0c0c5d1e74
--- /dev/null
+++ b/ide/config_lexer.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val print_file : string -> string list Util.String.Map.t -> unit
+val load_file : string -> string list Util.String.Map.t
diff --git a/ide/coq_commands.mli b/ide/coq_commands.mli
new file mode 100644
index 0000000000..53026be38b
--- /dev/null
+++ b/ide/coq_commands.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val tactics : string list list
+val commands : string list list
+val state_preserving : string list
diff --git a/ide/coq_lex.mli b/ide/coq_lex.mli
new file mode 100644
index 0000000000..417e0a76fa
--- /dev/null
+++ b/ide/coq_lex.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val delimit_sentences : (int -> GText.tag -> unit) -> string -> unit
+
+exception Unterminated
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index 8d99cc3e66..6e330c62b5 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -55,6 +55,8 @@ let os_specific_init () = ()
 
 (** Win32 *)
 
+IFDEF WIN32 THEN
+
 (* On win32, we add the directory of coqide to the PATH at launch-time
    (this used to be done in a .bat script). *)
 
@@ -86,7 +88,6 @@ let reroute_stdout_stderr () =
 
 (* We also provide specific kill and interrupt functions. *)
 
-IFDEF WIN32 THEN
 external win32_kill : int -> unit = "win32_kill"
 external win32_interrupt : int -> unit = "win32_interrupt"
 let () =
diff --git a/ide/coqide_main.mli b/ide/coqide_main.mli
new file mode 100644
index 0000000000..e1555ba2e2
--- /dev/null
+++ b/ide/coqide_main.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* This empty file avoids a race condition that occurs when compiling a .ml file
+   that does not have a corresponding .mli file *)
diff --git a/ide/coqide_ui.mli b/ide/coqide_ui.mli
new file mode 100644
index 0000000000..9f6fa5635a
--- /dev/null
+++ b/ide/coqide_ui.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val init : unit -> unit
+val ui_m : GAction.ui_manager
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml
index f0575e325a..7c0a7495a0 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/gtk_parsing.ml
@@ -7,11 +7,7 @@
 (************************************************************************)
 
 let underscore = Glib.Utf8.to_unichar "_" ~pos:(ref 0)
-let arobase = Glib.Utf8.to_unichar "@" ~pos:(ref 0)
 let prime = Glib.Utf8.to_unichar "'" ~pos:(ref 0)
-let bn = Glib.Utf8.to_unichar "\n" ~pos:(ref 0)
-let space = Glib.Utf8.to_unichar " " ~pos:(ref 0)
-let tab = Glib.Utf8.to_unichar "\t" ~pos:(ref 0)
 
 
 (* TODO: avoid num and prime at the head of a word *)
@@ -30,17 +26,6 @@ let ends_word (it:GText.iter) =
        not (is_word_char c)
   )
 
-
-let inside_word (it:GText.iter) =
-  let c = it#char in
-    not (starts_word it) &&
-      not (ends_word it) &&
-      is_word_char c
-
-
-let is_on_word_limit (it:GText.iter) = inside_word it || ends_word it
-
-
 let find_word_start (it:GText.iter) =
   let rec step_to_start it =
     Minilib.log "Find word start";
@@ -72,100 +57,6 @@ let get_word_around (it:GText.iter) =
   let stop =  find_word_end it in
     start,stop
 
-
-let rec complete_backward w (it:GText.iter) =
-  Minilib.log "Complete backward...";
-  match it#backward_search w with
-    | None -> (Minilib.log "backward_search failed";None)
-    | Some (start,stop) ->
-	Minilib.log ("complete_backward got a match:"^(string_of_int start#offset)^(string_of_int stop#offset));
-	if starts_word start then
-	  let ne = find_word_end stop in
-	    if ne#compare stop = 0
-	    then complete_backward w start
-	    else Some (start,stop,ne)
-	else complete_backward w start
-
-
-let rec complete_forward w (it:GText.iter) =
-  Minilib.log "Complete forward...";
-  match it#forward_search w with
-    | None -> None
-    | Some (start,stop) ->
-	if starts_word start then
-	  let ne = find_word_end stop in
-	    if ne#compare stop = 0 then
-	      complete_forward w stop
-	    else Some (stop,stop,ne)
-	else complete_forward w stop
-
-
-let find_comment_end (start:GText.iter) =
-  let rec find_nested_comment (search_start:GText.iter) (search_end:GText.iter) (comment_end:GText.iter) =
-    match (search_start#forward_search ~limit:search_end "(*"),(comment_end#forward_search "*)") with
-      | None,_ -> comment_end
-      | Some _, None -> raise Not_found
-      | Some (_,next_search_start),Some (next_search_end,next_comment_end) ->
-          find_nested_comment next_search_start next_search_end next_comment_end
-  in
-    match start#forward_search "*)" with
-      | None -> raise Not_found
-      | Some (search_end,comment_end) -> find_nested_comment start search_end comment_end
-
-
-let rec find_string_end (start:GText.iter) =
-  let dblquote = int_of_char '"' in
-  let rec escaped_dblquote c =
-    (c#char = dblquote) && not (escaped_dblquote c#backward_char)
-  in
-    match start#forward_search "\"" with
-      | None -> raise Not_found
-      | Some (stop,next_start) ->
-          if escaped_dblquote stop#backward_char
-          then find_string_end next_start
-          else next_start
-
-
-let rec find_next_sentence (from:GText.iter) =
-  match (from#forward_search ".") with
-    | None -> raise Not_found
-    | Some (non_vernac_search_end,next_sentence) ->
-        match from#forward_search ~limit:non_vernac_search_end "(*",from#forward_search ~limit:non_vernac_search_end "\"" with
-          | None,None ->
-              if Glib.Unichar.isspace next_sentence#char || next_sentence#compare next_sentence#forward_char == 0
-              then next_sentence else find_next_sentence next_sentence
-          | None,Some (_,string_search_start) -> find_next_sentence (find_string_end string_search_start)
-          | Some (_,comment_search_start),None -> find_next_sentence (find_comment_end comment_search_start)
-          | Some (_,comment_search_start),Some (_,string_search_start) ->
-              find_next_sentence (
-                if comment_search_start#compare string_search_start < 0
-                then find_comment_end comment_search_start
-                else find_string_end string_search_start)
-
-
-let find_nearest_forward (cursor:GText.iter) targets =
-  let fold_targets acc target =
-    match cursor#forward_search target,acc with
-      | Some (t_start,_),Some nearest when (t_start#compare nearest < 0) -> Some t_start
-      | Some (t_start,_),None -> Some t_start
-      | _ -> acc
-  in
-    match List.fold_left fold_targets None targets with
-      | None -> raise Not_found
-      | Some nearest -> nearest
-
-
-let find_nearest_backward (cursor:GText.iter) targets =
-  let fold_targets acc target =
-    match cursor#backward_search target,acc with
-      | Some (t_start,_),Some nearest when (t_start#compare nearest > 0) -> Some t_start
-      | Some (t_start,_),None -> Some t_start
-      | _ -> acc
-  in
-    match List.fold_left fold_targets None targets with
-      | None -> raise Not_found
-      | Some nearest -> nearest
-
 (** On double-click on a view, select the whole word. This is a workaround for
     a deficient word handling in TextView. *)
 let fix_double_click self =
diff --git a/ide/gtk_parsing.mli b/ide/gtk_parsing.mli
new file mode 100644
index 0000000000..b54f731b33
--- /dev/null
+++ b/ide/gtk_parsing.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val fix_double_click :
+  < buffer : < get_iter : [> `INSERT ] -> GText.iter;
+               move_mark : [> `INSERT | `SEL_BOUND ] ->
+                 where:GText.iter -> unit;
+               .. >;
+    event : < connect :
+                < button_press :
+                    callback:([> `TWO_BUTTON_PRESS ] Gdk.event ->
+                              bool) ->
+                    'a;
+                  .. >;
+              .. >;
+    .. > ->
+  unit
+val starts_word : GText.iter -> bool
+val ends_word : GText.iter -> bool
+val find_word_start : GText.iter -> GText.iter
+val find_word_end : GText.iter -> GText.iter
diff --git a/ide/ide_slave.mli b/ide/ide_slave.mli
new file mode 100644
index 0000000000..e1555ba2e2
--- /dev/null
+++ b/ide/ide_slave.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* This empty file avoids a race condition that occurs when compiling a .ml file
+   that does not have a corresponding .mli file *)
diff --git a/ide/macos_prehook.mli b/ide/macos_prehook.mli
new file mode 100644
index 0000000000..e1555ba2e2
--- /dev/null
+++ b/ide/macos_prehook.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* This empty file avoids a race condition that occurs when compiling a .ml file
+   that does not have a corresponding .mli file *)
diff --git a/ide/nanoPG.mli b/ide/nanoPG.mli
new file mode 100644
index 0000000000..3ad8435b5c
--- /dev/null
+++ b/ide/nanoPG.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val get_documentation : unit -> string
+val init : GWindow.window -> Session.session Wg_Notebook.typed_notebook ->
+           GAction.action_group list -> unit
diff --git a/ide/utf8_convert.mli b/ide/utf8_convert.mli
new file mode 100644
index 0000000000..06a131a68e
--- /dev/null
+++ b/ide/utf8_convert.mli
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val f : string -> string