Independance de grammar.cmo vis a vis de Search; reorganisation VernacDefinition

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

4 files changed, 58 insertions, 51 deletions

diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 93baa3edf..56edd9526 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -101,8 +101,8 @@ GEXTEND Gram
         c = lconstr ->
           let bl = [] in
           VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ()))
-      | (f,d,e) = def_token; id = base_ident; b = def_body -> 
-          VernacDefinition (d, id, b, f, e)
+      | (f,d) = def_token; id = base_ident; b = def_body -> 
+          VernacDefinition (d, id, b, f)
       | stre = assumption_token; bl = assum_list -> 
 	  VernacAssumption (stre, flatten_assum bl)
       | stre = assumptions_token; bl = assum_list ->
@@ -136,21 +136,21 @@ GEXTEND Gram
     [ [ "Theorem" -> Theorem
       | IDENT "Lemma" -> Lemma
       | IDENT "Fact" -> Fact
-      | IDENT "Remark" -> Remark
-      | IDENT "Conjecture" -> Conjecture ] ]
+      | IDENT "Remark" -> Remark ] ]
   ;
   def_token:
-    [ [ "Definition" -> (fun _ _ -> ()), Global, GDefinition
-      | IDENT "Local" -> (fun _ _ -> ()), Local, LDefinition
-      | IDENT "SubClass"  -> Class.add_subclass_hook, Global, GCoercion
+    [ [ "Definition" -> (fun _ _ -> ()), (Global, Definition)
+      | IDENT "Local" -> (fun _ _ -> ()), (Local, Definition)
+      | IDENT "SubClass"  -> Class.add_subclass_hook, (Global, Coercion)
       | IDENT "Local"; IDENT "SubClass"  ->
-          Class.add_subclass_hook, Local, LCoercion ] ] 
+          Class.add_subclass_hook, (Local, Coercion) ] ] 
   ;
   assumption_token:
     [ [ "Hypothesis" -> (Local, Logical)
       | "Variable" -> (Local, Definitional)
       | "Axiom" -> (Global, Logical)
-      | "Parameter" -> (Global, Definitional) ] ]
+      | "Parameter" -> (Global, Definitional)
+      | IDENT "Conjecture" -> (Global, Conjectural) ] ]
   ;
   assumptions_token:
     [ [ IDENT "Hypotheses" -> (Local, Logical)
@@ -400,15 +400,16 @@ GEXTEND Gram
 	  VernacCanonical qid
       | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
           let s = Ast.coerce_global_to_id qid in
-	  VernacDefinition (Global,s,d,Recordobj.add_object_hook,SCanonical)
+	  VernacDefinition 
+	    ((Global,CanonicalStructure),s,d,Recordobj.add_object_hook)
 
       (* Coercions *)
       | IDENT "Coercion"; qid = global; d = def_body ->
           let s = Ast.coerce_global_to_id qid in
-	  VernacDefinition (Global,s,d,Class.add_coercion_hook,GCoercion)
+	  VernacDefinition ((Global,Coercion),s,d,Class.add_coercion_hook)
       | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
            let s = Ast.coerce_global_to_id qid in
-	  VernacDefinition (Local,s,d,Class.add_coercion_hook,LCoercion)
+	  VernacDefinition ((Local,Coercion),s,d,Class.add_coercion_hook)
       | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = base_ident;
          ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> 
 	   VernacIdentityCoercion (Local, f, s, t)
@@ -520,9 +521,9 @@ GEXTEND Gram
       | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules ->
 	  VernacSearch (SearchRewrite c, l)
       | IDENT "SearchAbout"; 
-	  sl = [ "["; l = LIST1 [ r = global -> Search.SearchRef r
-                                  | s = STRING -> Search.SearchString s ]; "]" -> l 
-   		 | qid = global -> [Search.SearchRef qid] ];
+	  sl = [ "["; l = LIST1 [ r = global -> SearchRef r
+                                  | s = STRING -> SearchString s ]; "]" -> l 
+   		 | qid = global -> [SearchRef qid] ];
 	  l = in_or_out_modules -> 
 	  VernacSearch (SearchAbout sl, l)
       | IDENT "SearchNamed"; sl = LIST1 string; l = in_or_out_modules -> 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a0137d791..82318340c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -252,7 +252,7 @@ let start_proof_and_print idopt k t hook =
   print_subgoals ();
   if !pcoq <> None then (out_some !pcoq).start_proof ()
 
-let vernac_definition local id def hook =
+let vernac_definition (local,_ as k) id def hook =
   match def with
   | ProveBody (bl,t) ->   (* local binders, typ *)
       if Lib.is_modtype () then
@@ -268,7 +268,7 @@ let vernac_definition local id def hook =
         | Some r -> 
 	    let (evc,env)= Command.get_current_context () in
 	    Some (interp_redexp env evc r) in
-      declare_definition id local bl red_option c typ_opt hook
+      declare_definition id k bl red_option c typ_opt hook
 
 let vernac_start_proof kind sopt (bl,t) lettop hook =
   if not(refining ()) then
@@ -883,8 +883,8 @@ let interp_search_restriction = function
 open Search
 
 let interp_search_about_item = function
-  | SearchRef qid -> SearchRef (Nametab.global qid)
-  | SearchString s as x -> x
+  | SearchRef qid -> GlobSearchRef (Nametab.global qid)
+  | SearchString s -> GlobSearchString s
 
 let vernac_search s r =
   let r = interp_search_restriction r in
@@ -1119,7 +1119,7 @@ let interp c = match c with
       vernac_notation local c infpl mv8 sc
 
   (* Gallina *)
-  | VernacDefinition (k,id,d,f,_) -> vernac_definition k id d f
+  | VernacDefinition (k,id,d,f) -> vernac_definition k id d f
   | VernacStartTheoremProof (k,id,t,top,f) ->
       vernac_start_proof k (Some id) t top f
   | VernacEndProof e -> vernac_end_proof e
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 76c3358a0..06dae3815 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -55,11 +55,15 @@ type printable =
   | PrintScope of string
   | PrintAbout of reference
 
+type search_about_item =
+  | SearchRef of reference
+  | SearchString of string
+
 type searchable =
   | SearchPattern of pattern_expr
   | SearchRewrite of pattern_expr
   | SearchHead of reference
-  | SearchAbout of reference Search.search_about_item list
+  | SearchAbout of search_about_item list
   | SearchNamed of string list
 
 type locatable =
@@ -92,14 +96,12 @@ type comment =
   | CommentString of string
   | CommentInt of int
 
-type raw_constr_expr = constr_expr
-
 type hints =
   | HintsResolve of (identifier option * constr_expr) list
   | HintsImmediate of (identifier option * constr_expr) list
   | HintsUnfold of (identifier option * reference) list
   | HintsConstructors of identifier option * reference list
-  | HintsExtern of identifier option * int * raw_constr_expr * raw_tactic_expr
+  | HintsExtern of identifier option * int * constr_expr * raw_tactic_expr
   | HintsDestruct of identifier *
       int * (bool,unit) location * constr_expr * raw_tactic_expr
 
@@ -178,8 +180,8 @@ type vernac_expr =
       (string * syntax_modifier list) option * scope_name option
 
   (* Gallina *)
-  | VernacDefinition of definition_kind * identifier * definition_expr *
-      declaration_hook * definitionkind
+  | VernacDefinition of definition_kind * identifier * definition_expr * 
+      declaration_hook
   | VernacStartTheoremProof of theorem_kind * identifier *
       (local_binder list * constr_expr) * bool * declaration_hook
   | VernacEndProof of proof_end
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index b8bcf8cbd..3eaaeb0ea 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -25,7 +25,7 @@ open Ast
 open Libnames
 open Ppextend
 open Topconstr
-
+open Decl_kinds
 open Tacinterp
 
 (* Copie de Nameops *)
@@ -146,8 +146,8 @@ let pr_in_out_modules = function
   | SearchOutside l -> spc() ++ str"outside" ++ spc() ++ prlist_with_sep sep pr_module l
 
 let pr_search_about = function
-  | Search.SearchRef r -> pr_reference r
-  | Search.SearchString s -> qsnew s
+  | SearchRef r -> pr_reference r
+  | SearchString s -> qsnew s
 
 let pr_search a b pr_p = match a with
   | SearchHead qid -> str"Search" ++ spc() ++ pr_reference qid ++ pr_in_out_modules b
@@ -327,14 +327,17 @@ let pr_class_rawexpr = function
   | RefClass qid -> pr_reference qid
 
 let pr_assumption_token many = function
-  | (Decl_kinds.Local,Decl_kinds.Logical) ->
+  | (Local,Logical) ->
       str (if many then "Hypotheses" else "Hypothesis")
-  | (Decl_kinds.Local,Decl_kinds.Definitional) ->
+  | (Local,Definitional) ->
       str (if many then "Variables" else "Variable")
-  | (Decl_kinds.Global,Decl_kinds.Logical) ->
+  | (Global,Logical) ->
       str (if many then "Axioms" else "Axiom")
-  | (Decl_kinds.Global,Decl_kinds.Definitional) -> 
+  | (Global,Definitional) -> 
       str (if many then "Parameters" else "Parameter")
+  | (Global,Conjectural) -> str"Conjecture"
+  | (Local,Conjectural) -> 
+      anomaly "Don't know how to translate a local conjecture"
 
 let pr_params pr_c (xl,(c,t)) =
   hov 2 (prlist_with_sep sep pr_id xl ++ spc() ++
@@ -358,11 +361,10 @@ let pr_ne_params_list pr_c l =
 *)
 
 let pr_thm_token = function
-  | Decl_kinds.Theorem -> str"Theorem"
-  | Decl_kinds.Lemma -> str"Lemma"
-  | Decl_kinds.Fact -> str"Fact"
-  | Decl_kinds.Remark -> str"Remark"
-  | Decl_kinds.Conjecture -> str"Conjecture"
+  | Theorem -> str"Theorem"
+  | Lemma -> str"Lemma"
+  | Fact -> str"Fact"
+  | Remark -> str"Remark"
 
 let pr_require_token = function
   | Some true -> str "Export"
@@ -572,15 +574,17 @@ let rec pr_vernac = function
       pr_syntax_modifiers l
 
   (* Gallina *)
-  | VernacDefinition (d,id,b,f,e) -> (* A verifier... *)
+  | VernacDefinition (d,id,b,f) -> (* A verifier... *)
       let pr_def_token = function
-        | Decl_kinds.LCoercion -> str"Coercion Local"
-        | Decl_kinds.GCoercion -> str"Coercion"
-        | Decl_kinds.LDefinition -> str"Local"
-        | Decl_kinds.GDefinition -> str"Definition"
-        | Decl_kinds.LSubClass -> str"Local SubClass"
-        | Decl_kinds.GSubClass -> str"SubClass"
-        | Decl_kinds.SCanonical -> str"Canonical Structure" in
+        | Local, Coercion -> str"Coercion Local"
+        | Global, Coercion -> str"Coercion"
+        | Local, Definition -> str"Local"
+        | Global, Definition -> str"Definition"
+        | Local, SubClass -> str"Local SubClass"
+        | Global, SubClass -> str"SubClass"
+        | Global, CanonicalStructure -> str"Canonical Structure"
+        | Local, CanonicalStructure ->
+	   anomaly "Don't know how to translate a local canonical structure" in
       let pr_reduce = function
         | None -> mt()
         | Some r ->
@@ -612,7 +616,7 @@ let rec pr_vernac = function
             (pr_and_type_binders_arg bl, str" :" ++ spc () ++ pr_type t, None)
       in
       let (binds,typ,c) = pr_def_body b in
-      hov 2 (pr_def_token e ++ spc() ++ pr_id id ++ binds ++ typ ++
+      hov 2 (pr_def_token d ++ spc() ++ pr_id id ++ binds ++ typ ++
       (match c with
         | None -> mt()
         | Some cc -> str" :=" ++ spc() ++ cc))
@@ -839,14 +843,14 @@ let rec pr_vernac = function
   | VernacCanonical q -> str"Canonical Structure" ++ spc() ++ pr_reference q
   | VernacCoercion (s,id,c1,c2) ->
       hov 1 (
-	str"Coercion" ++ (match s with | Decl_kinds.Local -> spc() ++
-	  str"Local" ++ spc() | Decl_kinds.Global -> spc()) ++
+	str"Coercion" ++ (match s with | Local -> spc() ++
+	  str"Local" ++ spc() | Global -> spc()) ++
 	pr_reference id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++
 	spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2)
   | VernacIdentityCoercion (s,id,c1,c2) ->
       hov 1 (
-	str"Identity Coercion" ++ (match s with | Decl_kinds.Local -> spc() ++
-	  str"Local" ++ spc() | Decl_kinds.Global -> spc()) ++ pr_id id ++ 
+	str"Identity Coercion" ++ (match s with | Local -> spc() ++
+	  str"Local" ++ spc() | Global -> spc()) ++ pr_id id ++ 
 	spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
 	spc() ++ pr_class_rawexpr c2)