Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 118 insertions, 95 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 6b2f9a6ae..fc80cfda9 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -35,10 +35,7 @@ open Safe_typing
    (useful only for persistent constructions), is the length of the section
    part in [dir] *)
 
-type strength = 
-  | NotDeclare
-  | DischargeAt of dir_path * int
-  | NeverDischarge
+open Nametab
 
 let depth_of_strength = function
   | DischargeAt (sp',n) -> n
diff --git a/library/declare.mli b/library/declare.mli
index b7b305cfa..07b9d98b6 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -26,13 +26,7 @@ open Nametab
    reset works properly --- and will fill some global tables such as 
    [Nametab] and [Impargs]. *)
 
-type strength = 
-  | NotDeclare
-  | DischargeAt of dir_path * int
-  | NeverDischarge
-
-val is_less_persistent_strength : strength * strength -> bool
-val strength_min : strength * strength -> strength
+open Nametab
 
 type section_variable_entry =
   | SectionLocalDef of constr * types option
@@ -51,6 +45,10 @@ val declare_constant : identifier -> constant_declaration -> constant
 
 val redeclare_constant : constant -> Cooking.recipe * strength -> unit
 
+(*
+val declare_parameter : identifier -> constr -> constant
+*)
+
 (* [declare_mind me] declares a block of inductive types with
    their constructors in the current section; it returns the path of
    the whole block *)
@@ -61,6 +59,8 @@ val out_inductive : Libobject.obj -> mutual_inductive_entry
 val make_strength_0 : unit -> strength
 val make_strength_1 : unit -> strength
 val make_strength_2 : unit -> strength
+val is_less_persistent_strength : strength * strength -> bool
+val strength_min : strength * strength -> strength
 
 (*s Corresponding test and access functions. *)
 
diff --git a/library/goptions.ml b/library/goptions.ml
index f919b12e8..b4056472b 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -29,11 +29,11 @@ let nickname = function
   | SecondaryTable (s1,s2) -> s1^" "^s2
 
 let error_undeclared_key key =
-  error ((nickname key)^": no such table or option")
+  error ((nickname key)^": no table or option of this type")
 
 type value =
   | BoolValue   of bool
-  | IntValue    of int
+  | IntValue    of int option
   | StringValue of string
   | IdentValue  of global_reference
 
@@ -55,11 +55,10 @@ module MakeTable =
 	  type key
 	  val table : (string * key table_of_A) list ref
 	  val encode : key -> t
-          val check : t -> unit
           val printer : t -> std_ppcmds
           val key : option_name
           val title : string
-          val member_message : key -> bool -> string
+          val member_message : t -> bool -> std_ppcmds
           val synchronous : bool
         end) ->
   struct
@@ -113,18 +112,17 @@ module MakeTable =
 	   (hov 0 
 	      (if MySet.is_empty table then str "None" ++ fnl ()
                else MySet.fold
-		 (fun a b -> printer a ++ spc () ++ b) table (mt ()))))
+		 (fun a b -> printer a ++ spc () ++ b)
+		 table (mt ()) ++ fnl ())))
 
     class table_of_A () =
     object
-      method add x =
-	let c = A.encode x in
-        A.check c;
-        add_option c
+      method add x = add_option (A.encode x)
       method remove x = remove_option (A.encode x)
       method mem x = 
-        let answer = MySet.mem (A.encode x) !t in
-        msg (str (A.member_message x answer))
+	let y = A.encode x in
+        let answer = MySet.mem y !t in
+        msg (A.member_message y answer ++ fnl ())
       method print = print_table A.title A.printer !t 
     end
 
@@ -139,10 +137,9 @@ let get_string_table k = List.assoc (nickname k) !string_table
 
 module type StringConvertArg =
 sig
-  val check : string -> unit
   val key : option_name
   val title : string
-  val member_message : string -> bool -> string
+  val member_message : string -> bool -> std_ppcmds
   val synchronous : bool
 end
 
@@ -152,8 +149,7 @@ struct
   type key = string
   let table = string_table
   let encode x = x
-  let check = A.check
-  let printer s = (str s)
+  let printer = str
   let key = A.key
   let title = A.title
   let member_message = A.member_message
@@ -163,29 +159,27 @@ end
 module MakeStringTable =
   functor (A : StringConvertArg) -> MakeTable (StringConvert(A))
 
-let ident_table = ref []
+let ref_table = ref []
 
-let get_ident_table k = List.assoc (nickname k) !ident_table
+let get_ref_table k = List.assoc (nickname k) !ref_table
 
-module type IdentConvertArg =
+module type RefConvertArg =
 sig
   type t
-  val encode : global_reference -> t
-  val check : t -> unit
+  val encode : qualid located -> t
   val printer : t -> std_ppcmds
   val key : option_name
   val title : string
-  val member_message : global_reference -> bool -> string
+  val member_message : t -> bool -> std_ppcmds
   val synchronous : bool
 end
 
-module IdentConvert = functor (A : IdentConvertArg) -> 
+module RefConvert = functor (A : RefConvertArg) -> 
 struct
   type t = A.t
-  type key = global_reference
-  let table = ident_table
+  type key = qualid located
+  let table = ref_table
   let encode = A.encode
-  let check = A.check
   let printer = A.printer
   let key = A.key
   let title = A.title
@@ -193,8 +187,8 @@ struct
   let synchronous = A.synchronous
 end
 
-module MakeIdentTable =
-  functor (A : IdentConvertArg) -> MakeTable (IdentConvert(A))
+module MakeRefTable =
+  functor (A : RefConvertArg) -> MakeTable (RefConvert(A))
 
 (****************************************************************************)
 (* 2- Options                                                               *)
@@ -222,7 +216,7 @@ let check_key key = try
   error "Sorry, this option name is already used"
 with Not_found ->
   if List.mem_assoc (nickname key) !string_table
-    or List.mem_assoc (nickname key) !ident_table
+    or List.mem_assoc (nickname key) !ref_table
   then error "Sorry, this option name is already used"
 
 open Summary
@@ -301,7 +295,8 @@ let msg_option_value (name,v) =
   match v with
     | BoolValue true  -> str "true"
     | BoolValue false -> str "false"
-    | IntValue n      -> int n
+    | IntValue (Some n) -> int n
+    | IntValue None   -> str "undefined"
     | StringValue s   -> str s
     | IdentValue r    -> pr_global_env (Global.env()) r
 
@@ -343,7 +338,7 @@ let print_tables () =
        !string_table (mt ()) ++
      List.fold_right
        (fun (nickkey,_) p -> p ++ str ("  "^nickkey) ++ fnl ())
-       !ident_table (mt ()) ++
+       !ref_table (mt ()) ++
      fnl ()
     )
 
diff --git a/library/goptions.mli b/library/goptions.mli
index 8f810a266..d43a4283e 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -54,6 +54,7 @@
 
 (*i*)
 open Pp
+open Util
 open Names
 open Term
 open Nametab
@@ -68,26 +69,22 @@ type option_name =
 
 val error_undeclared_key : option_name -> 'a
 
-
 (*s Tables. *)
 
 (* The functor [MakeStringTable] declares a table containing objects
-   of type [string]; the function [check] is for testing if a given
-   object is allowed to be added to the table; the function
-   [member_message] say what to print when invoking the "Test Toto
-   Titi foo." command; at the end [title] is the table name printed
-   when invoking the "Print Toto Titi." command; [active] is roughly
-   the internal version of the vernacular "Test ...": it tells if a
-   given object is in the table; [elements] returns the list of
-   elements of the table *)
+   of type [string]; the function [member_message] say what to print
+   when invoking the "Test Toto Titi foo." command; at the end [title]
+   is the table name printed when invoking the "Print Toto Titi."
+   command; [active] is roughly the internal version of the vernacular
+   "Test ...": it tells if a given object is in the table; [elements]
+   returns the list of elements of the table *)
 
 module MakeStringTable :
   functor
     (A : sig
-       val check : string -> unit
        val key : option_name
        val title : string
-       val member_message : string -> bool -> string
+       val member_message : string -> bool -> std_ppcmds
        val synchronous : bool
      end) ->
 sig
@@ -95,29 +92,25 @@ sig
   val elements : unit -> string list
 end
 
-(* The functor [MakeIdentTable] declares a new table of [global_reference];
-   for generality, identifiers may be internally encode in other type
-   which is [A.t] through an encoding function [encode : global_reference ->
-   A.t] (typically, [A.t] is the persistent [global_reference] associated
-   to the currentdenotation of the [global_reference] and the encoding function
-   is the globalization function); the function [check] is for testing
-   if a given object is allowed to be added to the table; the function
+(* The functor [MakeRefTable] declares a new table of objects of type
+   [A.t] practically denoted by [qualid]; the encoding function
+   [encode : qualid -> A.t] is typically a globalization function,
+   possibly with some restriction checks; the function
    [member_message] say what to print when invoking the "Test Toto
    Titi foo." command; at the end [title] is the table name printed
    when invoking the "Print Toto Titi." command; [active] is roughly
    the internal version of the vernacular "Test ...": it tells if a
-   given object is in the table.                                            *)
+   given object is in the table.  *)
 
-module MakeIdentTable :
+module MakeRefTable :
   functor
     (A : sig
            type t
-           val encode : global_reference -> t
-           val check : t -> unit
+           val encode : qualid located -> t
            val printer : t -> std_ppcmds
            val key : option_name
            val title : string
-           val member_message : global_reference -> bool -> string
+           val member_message : t -> bool -> std_ppcmds
            val synchronous : bool
          end) ->
     sig
@@ -145,7 +138,7 @@ type 'a option_sig = {
 
 type 'a write_function = 'a -> unit
 
-val declare_int_option   : int option_sig    -> int write_function
+val declare_int_option   : int option option_sig -> int option write_function
 val declare_bool_option  : bool option_sig   -> bool write_function
 val declare_string_option: string option_sig -> string write_function
 
@@ -159,14 +152,14 @@ val get_string_table :
       mem : string -> unit;
       print : unit >
 
-val get_ident_table :
+val get_ref_table :
   option_name ->
-    < add : global_reference -> unit;
-      remove : global_reference -> unit;
-      mem : global_reference -> unit;
+    < add : qualid located -> unit;
+      remove : qualid located -> unit;
+      mem : qualid located -> unit;
       print : unit >
 
-val set_int_option_value    : option_name -> int    -> unit
+val set_int_option_value    : option_name -> int option -> unit
 val set_bool_option_value   : option_name -> bool   -> unit
 val set_string_option_value : option_name -> string -> unit
 
diff --git a/library/impargs.ml b/library/impargs.ml
index 86acf1687..af6bfd6b7 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -77,7 +77,7 @@ let with_implicits b f x =
     raise e
   end
 
-let implicitely f = with_implicits true f
+let implicitly f = with_implicits true f
 
 let using_implicits = function
   | No_impl -> with_implicits false
diff --git a/library/impargs.mli b/library/impargs.mli
index 470f3d0c3..022a38230 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -20,7 +20,7 @@ open Nametab
 
 val make_implicit_args : bool -> unit
 val is_implicit_args : unit -> bool
-val implicitely : ('a -> 'b) -> 'a -> 'b
+val implicitly : ('a -> 'b) -> 'a -> 'b
 val with_implicits : bool -> ('a -> 'b) -> 'a -> 'b
 
 (*s An [implicits_list] is a list of positions telling which arguments
diff --git a/library/library.ml b/library/library.ml
index 47beca5f3..bc25eb617 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -435,7 +435,7 @@ let locate_qualified_library qid =
     (LibInPath, extend_dirpath (find_logical_path path) base, file)
   with Not_found -> raise LibNotFound
 
-let rec_intern_qualified_library qid =
+let rec_intern_qualified_library (loc,qid) =
   try
     let (_,dir,f) = locate_qualified_library qid in
     rec_intern_module (dir,f);
@@ -443,19 +443,18 @@ let rec_intern_qualified_library qid =
   with
   | LibUnmappedDir ->
       let prefix, id = repr_qualid qid in
-      errorlabstrm "rec_intern_qualified_library"
-      (str ("Cannot load "^(string_of_id id)^":") ++ spc () ++ 
-      str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ())
+      user_err_loc (loc, "rec_intern_qualified_library",
+        str ("Cannot load "^(string_of_id id)^":") ++ spc () ++ 
+        str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++
+        fnl ())
   | LibNotFound ->
-      errorlabstrm "rec_intern_qualified_library"
-      (str"Cannot find module " ++ pr_qualid qid ++ str" in loadpath")
+      user_err_loc (loc, "rec_intern_qualified_library",
+        str"Cannot find module " ++ pr_qualid qid ++ str" in loadpath")
 
-let rec_intern_module_from_file qid f =
+let rec_intern_module_from_file idopt f =
   (* A name is specified, we have to check it contains module id *)
-  let prefix, id = repr_qualid qid in
-  assert (repr_dirpath prefix = []);
   let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in
-  rec_intern_by_filename_only (Some id) f
+  rec_intern_by_filename_only idopt f
 
 (*s [require_module] loads and opens a module. This is a synchronized
     operation. *)
@@ -493,17 +492,19 @@ let require_module spec qidl export =
   add_anonymous_leaf (in_require (modrefl,Some export));
   add_frozen_state ()
 
-let require_module_from_file spec qid file export =
-  let modref = rec_intern_module_from_file qid file in
+let require_module_from_file spec idopt file export =
+  let modref = rec_intern_module_from_file idopt file in
   add_anonymous_leaf (in_require ([modref],Some export));
   add_frozen_state ()
 
-let import_module export qid =
+let import_module export (loc,qid) =
   let modref =
     try 
       Nametab.locate_loaded_library qid
     with Not_found ->
-      error ((Nametab.string_of_qualid qid)^" not loaded") in
+      user_err_loc
+        (loc,"import_module",
+	 str ((Nametab.string_of_qualid qid)^" not loaded")) in
   add_anonymous_leaf (in_require ([modref],Some export))
 
 let read_module qid =
diff --git a/library/library.mli b/library/library.mli
index 5b51780e1..c29299331 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -9,6 +9,7 @@
 (*i $Id$ i*)
 
 (*i*)
+open Util
 open Names
 open Libobject
 (*i*)
@@ -20,9 +21,9 @@ open Libobject
    provides a high level function [require] which corresponds to the 
    vernacular command [Require]. *)
 
-val read_module : Nametab.qualid -> unit
+val read_module : Nametab.qualid located -> unit
 val read_module_from_file : System.physical_path -> unit
-val import_module : bool -> Nametab.qualid -> unit
+val import_module : bool -> Nametab.qualid located -> unit
 
 val module_is_loaded : dir_path -> bool
 val module_is_opened : dir_path -> bool
@@ -39,10 +40,10 @@ val fmt_modules_state : unit -> Pp.std_ppcmds
   exported. *)
 
 val require_module :
-  bool option -> Nametab.qualid list -> bool -> unit
+  bool option -> Nametab.qualid located list -> bool -> unit
 
 val require_module_from_file :
-  bool option -> Nametab.qualid -> string -> bool -> unit
+  bool option -> identifier option -> string -> bool -> unit
 
 (*s [save_module_to s f] saves the current environment as a module [s]
   in the file [f]. *)
diff --git a/library/nametab.ml b/library/nametab.ml
index 99524bde1..b28506f91 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -139,6 +139,8 @@ let push_idtree extract_dirpath tab n dir id o =
 
 let push_long_names_ccipath = push_idtree dirpath_of_extended_ref the_ccitab
 let push_short_name_ccipath = push_idtree dirpath_of_extended_ref the_ccitab
+let push_long_names_objpath =
+  push_idtree (fun sp -> let (p,_) = repr_path sp in p) the_objtab
 let push_short_name_objpath =
   push_idtree (fun sp -> let (p,_) = repr_path sp in p) the_objtab
 
@@ -181,6 +183,12 @@ let push_short_name_object sp =
   let _, s = repr_qualid (qualid_of_sp sp) in
   push_short_name_objpath 0 empty_dirpath s sp
 
+(* This is for tactic definition names *)
+
+let push_tactic_path sp =
+  let dir, s = repr_qualid (qualid_of_sp sp) in
+  push_long_names_objpath 0 dir s sp
+
 (* This is to remember absolute Section/Module names and to avoid redundancy *)
 let push_section fulldir =
   let dir, s = split_dirpath fulldir in
@@ -213,6 +221,10 @@ let locate_obj qid =
   let (dir,id) = repr_qualid qid in
   locate_in_tree (Idmap.find id !the_objtab) dir
 
+let locate_tactic qid =
+  let (dir,id) = repr_qualid qid in
+  locate_in_tree (Idmap.find id !the_objtab) dir
+
 (* Actually, this table has only two levels, since only basename and *)
 (* fullname are registered *)
 let push_loaded_library fulldir =
@@ -259,13 +271,13 @@ let absolute_reference sp =
 let locate_in_absolute_module dir id =
   absolute_reference (make_path dir id)
 
-let global loc qid =
+let global (loc,qid) =
   try match extended_locate qid with
     | TrueGlobal ref -> ref
     | SyntacticDef _ -> 
-        error
-          ("Unexpected reference to a syntactic definition: "
-           ^(string_of_qualid qid))
+        user_err_loc (loc,"global",
+          str "Unexpected reference to a syntactic definition: " ++
+          pr_qualid qid)
   with Not_found ->
     error_global_not_found_loc loc qid
 
@@ -299,6 +311,13 @@ let pr_global_env env ref =
   let s = string_of_qualid (shortest_qualid_of_global env ref) in
   (str s)
 
+let global_inductive (loc,qid as locqid) =
+  match global locqid with
+  | IndRef ind -> ind
+  | ref ->
+      user_err_loc (loc,"global_inductive",
+        pr_qualid qid ++ spc () ++ str "is not an inductive type")
+
 (********************************************************************)
 
 (********************************************************************)
@@ -330,3 +349,8 @@ let _ =
       Summary.unfreeze_function = unfreeze;
       Summary.init_function = init;
       Summary.survive_section = false }
+
+type strength = 
+  | NotDeclare
+  | DischargeAt of dir_path * int
+  | NeverDischarge
diff --git a/library/nametab.mli b/library/nametab.mli
index adb764fcb..d71e3e379 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -67,6 +67,10 @@ val push_syntactic_definition : section_path -> unit
 val push_short_name_syntactic_definition : section_path -> unit
 val push_short_name_object : section_path -> unit
 
+(*s Register visibility of absolute paths by short names *)
+val push_tactic_path : section_path -> unit
+val locate_tactic : qualid -> section_path
+
 (*s Register visibility by all qualifications *)
 val push_section : dir_path -> unit
 
@@ -82,7 +86,10 @@ val locate : qualid -> global_reference
 
 (* This function is used to transform a qualified identifier into a
    global reference, with a nice error message in case of failure *)
-val global : loc -> qualid -> global_reference
+val global : qualid located -> global_reference
+
+(* The same for inductive types *)
+val global_inductive : qualid located -> inductive
 
 (* This locates also syntactic definitions *)
 val extended_locate : qualid -> extended_global_reference
@@ -109,3 +116,8 @@ val locate_in_absolute_module : dir_path -> identifier -> global_reference
 
 val push_loaded_library : dir_path -> unit
 val locate_loaded_library : qualid -> dir_path
+
+type strength = 
+  | NotDeclare
+  | DischargeAt of dir_path * int
+  | NeverDischarge