More functional implementation of locality_flag and program_mode

This commit introduces 2 new vernac_expr constructors:
- VernacLocal (b,v)  that represents a vernacular v with the "Local" modifier
- VernacProgram v    that represents a vernacular v with the "Program" modifier

This allows the parser to avoid using side effects to model the two
modifiers, that are now represented in the AST.  This also decouples the
parsing phase from the interpretation phase, since parsing a second
phrase does not alter the locality flag for the first phrase.

As a consequence all the locality_flag components of vernac_expr have
been removed, but for the ones that (for retro compatibility) allow
an "infix" Local flag.  In these cases the boolean is renamed
obsolete_locality (as the grammar entry that parses it), and during
interpretation we check that at most one locality flag is specified,
using the idiom (where the input local is the obsolete one):

  let local = enforce_XXX_locality locality local in

Another improvement is that the default locality is not chosen in the
parser, but in the interpreter where the idiom

  let local = make_XXX_locality locality in

is used to default the locality to XXX (module/section/whatever).

Unfortunately not all side effects have been removed:
- Flags.program_mode is still used to signal that we are in program mode
- Locality.LocalityFixme.* functions are used in commands that do not
  have an AST, but are parsed as VernacExtend (see vernacinterp.ml)

I guess one could fix the latter case systematically adding an extra
argument "locality" to commands attached using VERNAC COMMAND EXTEND.

Fixing plugins adding commands that honour "Local" should look like this:

 VERNAC COMMAND EXTEND Set_Solver
 | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
     set_default_tactic
-      (Locality.use_section_locality ())
+      (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
       (Tacintern.glob_tactic t) ]
 END

In any case the side effects are set/consumed within then interpretation
phase, and not set during the parsing phase and consumed during the
interpretation phase.

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

1 files changed, 69 insertions, 67 deletions

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 572876e5b..415d70316 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -177,7 +177,7 @@ let pr_reference_or_constr pr_c = function
   | HintsReference r -> pr_reference r
   | HintsConstr c -> pr_c c
 
-let pr_hints local db h pr_c pr_pat =
+let pr_hints db h pr_c pr_pat =
   let opth = pr_opt_hintbases db  in
   let pph =
     match h with
@@ -200,7 +200,7 @@ let pr_hints local db h pr_c pr_pat =
           str "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
           spc() ++ pr_raw_tactic tac
   in
-  hov 2 (str"Hint "++pr_locality local ++ pph ++ opth)
+  hov 2 (str"Hint "++ pph ++ opth)
 
 let pr_with_declaration pr_c = function
   | CWith_Definition (id,c) ->
@@ -306,7 +306,9 @@ let pr_class_rawexpr = function
   | SortClass -> str"Sortclass"
   | RefClass qid -> pr_smart_global qid
 
-let pr_assumption_token many = function
+let pr_assumption_token many (l,a) =
+  let l = match l with Some x -> x | None -> Decl_kinds.Global in
+  match l, a with
   | (Discharge,Logical) ->
       str (if many then "Hypotheses" else "Hypothesis")
   | (Discharge,Definitional) ->
@@ -475,6 +477,8 @@ let pr_printable = function
 in
 
 let rec pr_vernac = function
+  | VernacProgram v -> str"Program" ++ spc() ++ pr_vernac v
+  | VernacLocal (local, v) -> pr_locality local ++ spc() ++ pr_vernac v
 
   (* Proof management *)
   | VernacAbortAll -> str "Abort All"
@@ -530,10 +534,9 @@ let rec pr_vernac = function
   | VernacFail v -> str"Fail" ++ spc() ++ pr_vernac v
 
   (* Syntax *)
-  | VernacTacticNotation (local,n,r,e) ->
-      pr_locality local ++ pr_grammar_tactic_rule n ("",r,e)
-  | VernacOpenCloseScope (local,opening,sc) ->
-      pr_section_locality local ++
+  | VernacTacticNotation (n,r,e) ->
+      pr_grammar_tactic_rule n ("",r,e)
+  | VernacOpenCloseScope (_,(opening,sc)) ->
       str (if opening then "Open " else "Close ") ++
       str "Scope" ++ spc() ++ str sc
   | VernacDelimiters (sc,key) ->
@@ -542,20 +545,20 @@ let rec pr_vernac = function
   | VernacBindScope (sc,cll) ->
       str"Bind Scope" ++ spc () ++ str sc ++
       spc() ++ str "with " ++ prlist_with_sep spc pr_smart_global cll
-  | VernacArgumentsScope (local,q,scl) -> let pr_opt_scope = function
+  | VernacArgumentsScope (q,scl) -> let pr_opt_scope = function
       |	None -> str"_"
       |	Some sc -> str sc in
-    pr_section_locality local ++ str"Arguments Scope" ++ spc() ++
+    str"Arguments Scope" ++ spc() ++
     pr_smart_global q
     ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
-  | VernacInfix (local,((_,s),mv),q,sn) -> (* A Verifier *)
-      hov 0 (hov 0 (pr_locality local ++ str"Infix "
+  | VernacInfix (_,((_,s),mv),q,sn) -> (* A Verifier *)
+      hov 0 (hov 0 (str"Infix "
       ++ qs s ++ str " :=" ++ pr_constrarg q) ++
       pr_syntax_modifiers mv ++
       (match sn with
     | None -> mt()
     | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
-  | VernacNotation (local,c,((_,s),l),opt) ->
+  | VernacNotation (_,c,((_,s),l),opt) ->
       let ps =
 	let n = String.length s in
 	if n > 2 && s.[0] == '\'' && s.[n-1] == '\''
@@ -563,18 +566,20 @@ let rec pr_vernac = function
           let s' = String.sub s 1 (n-2) in
           if String.contains s' '\'' then qs s else str s'
 	else qs s in
-      hov 2 (pr_locality local ++ str"Notation" ++ spc() ++ ps ++
+      hov 2 (str"Notation" ++ spc() ++ ps ++
       str " :=" ++ pr_constrarg c ++ pr_syntax_modifiers l ++
       (match opt with
         | None -> mt()
         | Some sc -> str" :" ++ spc() ++ str sc))
-  | VernacSyntaxExtension (local,(s,l)) ->
-      pr_locality local ++ str"Reserved Notation" ++ spc() ++ pr_located qs s ++
+  | VernacSyntaxExtension (_,(s,l)) ->
+      str"Reserved Notation" ++ spc() ++ pr_located qs s ++
       pr_syntax_modifiers l
 
   (* Gallina *)
   | VernacDefinition (d,id,b) -> (* A verifier... *)
-      let pr_def_token dk = str (Kindops.string_of_definition_kind dk) in
+      let pr_def_token (l,dk) =
+        let l = match l with Some x -> x | None -> Decl_kinds.Global in
+        str (Kindops.string_of_definition_kind (l,dk)) in
       let pr_reduce = function
         | None -> mt()
         | Some r ->
@@ -650,9 +655,9 @@ let rec pr_vernac = function
 
   | VernacFixpoint (local, recs) ->
       let local = match local with
-      | Discharge -> "Let "
-      | Local -> "Local "
-      | Global -> ""
+      | Some Discharge -> "Let "
+      | Some Local -> "Local "
+      | None | Some Global -> ""
       in
       let pr_onerec = function
         | ((loc,id),ro,bl,type_,def),ntn ->
@@ -667,9 +672,9 @@ let rec pr_vernac = function
 
   | VernacCoFixpoint (local, corecs) ->
       let local = match local with
-      | Discharge -> "Let "
-      | Local -> "Local "
-      | Global -> ""
+      | Some Discharge -> "Let "
+      | Some Local -> "Local "
+      | None | Some Global -> ""
       in
       let pr_onecorec (((loc,id),bl,c,def),ntn) =
         pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
@@ -698,22 +703,19 @@ let rec pr_vernac = function
       (if f then str"Export" else str"Import") ++ spc() ++
       prlist_with_sep sep pr_import_module l
   | VernacCanonical q -> str"Canonical Structure" ++ spc() ++ pr_smart_global q
-  | VernacCoercion (s,id,c1,c2) ->
+  | VernacCoercion (_,id,c1,c2) ->
       hov 1 (
-	str"Coercion" ++ (if s then spc() ++
-	  str"Local" ++ spc() else spc()) ++
+	str"Coercion" ++
 	pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++
 	spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2)
-  | VernacIdentityCoercion (s,id,c1,c2) ->
+  | VernacIdentityCoercion (_,id,c1,c2) ->
       hov 1 (
-	str"Identity Coercion" ++ (if s then spc() ++
-	  str"Local" ++ spc() else spc()) ++ pr_lident id ++
+	str"Identity Coercion" ++ pr_lident id ++
 	spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
 	spc() ++ pr_class_rawexpr c2)
 
- | VernacInstance (abst,glob, sup, (instid, bk, cl), props, pri) ->
+ | VernacInstance (abst, sup, (instid, bk, cl), props, pri) ->
      hov 1 (
-       pr_non_locality (not glob) ++
        (if abst then str"Declare " else mt ()) ++
        str"Instance" ++
        (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () |
@@ -730,10 +732,10 @@ let rec pr_vernac = function
        str"Context" ++ spc () ++ pr_and_type_binders_arg l)
 
 
- | VernacDeclareInstances (glob, ids) ->
-     hov 1 (pr_non_locality (not glob) ++
-               str"Existing" ++ spc () ++ str(String.plural (List.length ids) "Instance") ++
-               spc () ++ prlist_with_sep spc pr_reference ids)
+ | VernacDeclareInstances ids ->
+     hov 1 ( str"Existing" ++ spc () ++ 
+             str(String.plural (List.length ids) "Instance") ++
+             spc () ++ prlist_with_sep spc pr_reference ids)
 
  | VernacDeclareClass id ->
      hov 1 (str"Existing" ++ spc () ++ str"Class" ++ spc () ++ pr_reference id)
@@ -784,13 +786,12 @@ let rec pr_vernac = function
   | VernacRemoveLoadPath s -> str"Remove LoadPath" ++ qs s
   | VernacAddMLPath (fl,s) ->
       str"Add" ++ (if fl then str" Rec " else spc()) ++ str"ML Path" ++ qs s
-  | VernacDeclareMLModule (local, l) ->
-      pr_locality local ++
+  | VernacDeclareMLModule (l) ->
       hov 2 (str"Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
   | VernacChdir s -> str"Cd" ++ pr_opt qs s
 
   (* Commands *)
-  | VernacDeclareTacticDefinition (local,rc,l) ->
+  | VernacDeclareTacticDefinition (rc,l) ->
       let pr_tac_body (id, redef, body) =
         let idl, body =
           match body with
@@ -803,34 +804,33 @@ let rec pr_vernac = function
         pr_raw_tactic body
       in
       hov 1
-        (pr_locality local ++ str "Ltac " ++
+        (str "Ltac " ++
         prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l)
-  | VernacCreateHintDb (local,dbname,b) ->
-      hov 1 (pr_locality local ++ str "Create HintDb " ++
+  | VernacCreateHintDb (dbname,b) ->
+      hov 1 (str "Create HintDb " ++
 		str dbname ++ (if b then str" discriminated" else mt ()))
-  | VernacRemoveHints (local, dbnames, ids) ->
-      hov 1 (pr_locality local ++ str "Remove Hints " ++
+  | VernacRemoveHints (dbnames, ids) ->
+      hov 1 (str "Remove Hints " ++
 	       prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++
 	       pr_opt_hintbases dbnames)
-  | VernacHints (local,dbnames,h) ->
-      pr_hints local dbnames h pr_constr pr_constr_pattern_expr
-  | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) ->
+  | VernacHints (_, dbnames,h) ->
+      pr_hints dbnames h pr_constr pr_constr_pattern_expr
+  | VernacSyntacticDefinition (id,(ids,c),_,onlyparsing) ->
       hov 2
-        (pr_locality local ++ str"Notation " ++ pr_lident id ++ spc () ++
+        (str"Notation " ++ pr_lident id ++ spc () ++
 	 prlist (fun x -> spc() ++ pr_id x) ids ++ str":=" ++ pr_constrarg c ++
          pr_syntax_modifiers
 	   (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v]))
-  | VernacDeclareImplicits (local,q,[]) ->
-      hov 2 (pr_section_locality local ++ str"Implicit Arguments" ++ spc() ++
-	pr_smart_global q)
-  | VernacDeclareImplicits (local,q,impls) ->
-      hov 1 (pr_section_locality local ++ str"Implicit Arguments " ++
+  | VernacDeclareImplicits (q,[]) ->
+      hov 2 (str"Implicit Arguments" ++ spc() ++ pr_smart_global q)
+  | VernacDeclareImplicits (q,impls) ->
+      hov 1 (str"Implicit Arguments " ++
 	spc() ++ pr_smart_global q ++ spc() ++
 	prlist_with_sep spc (fun imps ->
 	  str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
 	  impls)
-  | VernacArguments (local, q, impl, nargs, mods) ->
-      hov 2 (pr_section_locality local ++ str"Arguments" ++ spc() ++
+  | VernacArguments (q, impl, nargs, mods) ->
+      hov 2 (str"Arguments" ++ spc() ++
         pr_smart_global q ++
       let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in
       let pr_if b x = if b then x else str "" in
@@ -861,21 +861,23 @@ let rec pr_vernac = function
       hov 2 (str"Implicit Type" ++
         str (if n > 1 then "s " else " ") ++
         pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl))
-  | VernacGeneralizable (local, g) ->
-      hov 1 (pr_locality local ++ str"Generalizable Variable" ++
+  | VernacGeneralizable g ->
+      hov 1 (str"Generalizable Variable" ++
 		match g with
 		| None -> str "s none"
 		| Some [] -> str "s all"
 		| Some idl ->
 		    str (if List.length idl > 1 then "s " else " ") ++
 		      prlist_with_sep spc pr_lident idl)
-  | VernacSetOpacity(b,[k,l]) when Conv_oracle.is_transparent k ->
-      hov 1 (pr_non_locality b ++ str "Transparent" ++
+  | VernacSetOpacity(k,l) when Conv_oracle.is_transparent k ->
+      hov 1 (str "Transparent" ++
              spc() ++ prlist_with_sep sep pr_smart_global l)
-  | VernacSetOpacity(b,[Conv_oracle.Opaque,l]) ->
-      hov 1 (pr_non_locality b ++ str "Opaque" ++
+  | VernacSetOpacity(Conv_oracle.Opaque,l) ->
+      hov 1 (str "Opaque" ++
              spc() ++ prlist_with_sep sep pr_smart_global l)
-  | VernacSetOpacity (local,l) ->
+  | VernacSetOpacity _ ->
+      Errors.anomaly (str "VernacSetOpacity used to set something else")
+  | VernacSetStrategy l ->
       let pr_lev = function
           Conv_oracle.Opaque -> str"opaque"
         | Conv_oracle.Expand -> str"expand"
@@ -884,12 +886,12 @@ let rec pr_vernac = function
       let pr_line (l,q) =
         hov 2 (pr_lev l ++ spc() ++
                str"[" ++ prlist_with_sep sep pr_smart_global q ++ str"]") in
-      hov 1 (pr_locality local ++ str "Strategy" ++ spc() ++
+      hov 1 (str "Strategy" ++ spc() ++
              hv 0 (prlist_with_sep sep pr_line l))
-  | VernacUnsetOption (l,na) ->
-      hov 1 (pr_locality_full l ++ str"Unset" ++ spc() ++ pr_printoption na None)
-  | VernacSetOption (l,na,v) ->
-      hov 2 (pr_locality_full l ++ str"Set" ++ spc() ++ pr_set_option na v)
+  | VernacUnsetOption (na) ->
+      hov 1 (str"Unset" ++ spc() ++ pr_printoption na None)
+  | VernacSetOption (na,v) ->
+      hov 2 (str"Set" ++ spc() ++ pr_set_option na v)
   | VernacAddOption (na,l) -> hov 2 (str"Add" ++ spc() ++ pr_printoption na (Some l))
   | VernacRemoveOption (na,l) -> hov 2 (str"Remove" ++ spc() ++ pr_printoption na (Some l))
   | VernacMemOption (na,l) -> hov 2 (str"Test" ++ spc() ++ pr_printoption na (Some l))
@@ -905,8 +907,8 @@ let rec pr_vernac = function
       let pr_i = match io with None -> mt () | Some i -> int i ++ str ": " in
       pr_i ++ pr_mayeval r c
   | VernacGlobalCheck c -> hov 2 (str"Type" ++ pr_constrarg c)
-  | VernacDeclareReduction (b,s,r) ->
-     pr_locality b ++ str "Declare Reduction " ++ str s ++ str " := " ++
+  | VernacDeclareReduction (s,r) ->
+     str "Declare Reduction " ++ str s ++ str " := " ++
      pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r
   | VernacPrint p -> pr_printable p
   | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr