Add interfaces for checker and remove dead code.

9 files changed, 77 insertions, 25 deletions

diff --git a/checker/checker.mli b/checker/checker.mli
new file mode 100644
index 000000000..ceab13774
--- /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 000000000..e1555ba2e
--- /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 000000000..3b2715de9
--- /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 820040587..2624e6d49 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 000000000..7eed692a0
--- /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 5a371164c..4698227ff 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 000000000..aad8fd5f4
--- /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 77c9999c4..8cb97a2b1 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 000000000..e1555ba2e
--- /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 *)