Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier devenu tros gros pour la compilation en PowerPC

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

2 files changed, 189 insertions, 170 deletions

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
new file mode 100644
index 000000000..3f1087c67
--- /dev/null
+++ b/parsing/g_proofs.ml4
@@ -0,0 +1,160 @@
+
+(* $Id$ *)
+
+open Pcoq
+open Pp
+open Tactic
+open Util
+open Vernac
+
+(* Proof commands *)
+GEXTEND Gram
+  GLOBAL: command ne_constrarg_list;
+
+  destruct_location :
+  [ [ IDENT "Conclusion"  -> <:ast< (CONCL)>>
+    | IDENT "Discardable"; "Hypothesis"  -> <:ast< (DiscardableHYP)>>
+    | "Hypothesis"   -> <:ast< (PreciousHYP)>> ]]
+  ;
+  ne_constrarg_list:
+  [ [ l = LIST1 constrarg -> l ] ]
+  ;
+  opt_identarg_list:
+  [ [ -> []
+    | ":"; l = LIST1 identarg -> l ] ]
+  ;
+  vrec_clause:
+    [ [ name=identarg; it=LIST1 input_fun; ":="; body=tactic_expr ->
+          <:ast<(RECCLAUSE $name (FUNVAR ($LIST $it)) $body)>> ] ]
+  ;
+  command:
+    [ [ IDENT "Goal"; c = constrarg; "." -> <:ast< (GOAL $c) >>
+      | IDENT "Goal"; "." -> <:ast< (GOAL) >>
+      | "Proof"; "." -> <:ast< (GOAL) >>
+      | IDENT "Abort"; "." -> <:ast< (ABORT) >>
+      | "Qed"; "." -> <:ast< (SaveNamed) >>
+      | IDENT "Save"; "." -> <:ast< (SaveNamed) >>
+      | IDENT "Defined"; "." -> <:ast< (DefinedNamed) >>
+      | IDENT "Save"; IDENT "Remark"; id = identarg; "." ->
+          <:ast< (SaveAnonymousRmk $id) >>
+      | IDENT "Save"; IDENT "Theorem"; id = identarg; "." ->
+          <:ast< (SaveAnonymousThm $id) >>
+      | IDENT "Save"; id = identarg; "." -> <:ast< (SaveAnonymousThm $id) >>
+      | IDENT "Suspend"; "." -> <:ast< (SUSPEND) >>
+      | IDENT "Resume"; "." -> <:ast< (RESUME) >>
+      | IDENT "Resume"; id = identarg; "." -> <:ast< (RESUME $id) >>
+      | IDENT "Abort"; IDENT "All"; "." -> <:ast< (ABORTALL) >>
+      | IDENT "Abort"; id = identarg; "." -> <:ast< (ABORT $id) >>
+      | IDENT "Restart"; "." -> <:ast< (RESTART) >>
+      | "Proof"; c = constrarg; "." -> <:ast< (PROOF $c) >>
+      | IDENT "Undo"; "." -> <:ast< (UNDO 1) >>
+      | IDENT "Undo"; n = numarg; "." -> <:ast< (UNDO $n) >>
+      | IDENT "Show"; n = numarg; "." -> <:ast< (SHOW $n) >>
+      | IDENT "Show"; IDENT "Implicits"; n = numarg; "." ->
+          <:ast< (SHOWIMPL $n) >>
+      | IDENT "Focus"; "." -> <:ast< (FOCUS) >>
+      | IDENT "Focus"; n = numarg; "." -> <:ast< (FOCUS $n) >>
+      | IDENT "Unfocus"; "." -> <:ast< (UNFOCUS) >>
+      | IDENT "Show"; "." -> <:ast< (SHOW) >>
+      | IDENT "Show"; IDENT "Implicits"; "." -> <:ast< (SHOWIMPL) >>
+      | IDENT "Show"; IDENT "Node"; "." -> <:ast< (ShowNode) >>
+      | IDENT "Show"; IDENT "Script"; "." -> <:ast< (ShowScript) >>
+      | IDENT "Show"; IDENT "Existentials"; "." -> <:ast< (ShowEx) >>
+      | IDENT "Existential"; n = numarg; ":="; c = constrarg; "." ->
+          <:ast< (EXISTENTIAL $n $c) >>
+      | IDENT "Existential"; n = numarg; ":="; c1 = Constr.constr; ":";
+        c2 = Constr.constr; "." ->
+          <:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >>
+      | IDENT "Existential"; n = numarg; ":"; c2 = Constr.constr; ":=";
+        c1 = Constr.constr; "." ->
+          <:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >>
+      | IDENT "Explain"; "Proof"; l = numarg_list; "." ->
+          <:ast< (ExplainProof ($LIST $l)) >>
+      | IDENT "Explain"; "Proof"; IDENT "Tree"; l = numarg_list; "." ->
+          <:ast< (ExplainProofTree ($LIST $l)) >>
+      | IDENT "Go"; n = numarg; "." -> <:ast< (Go $n) >>
+      | IDENT "Go"; IDENT "top"; "." -> <:ast< (Go "top") >>
+      | IDENT "Go"; IDENT "prev"; "." -> <:ast< (Go "prev") >>
+      | IDENT "Go"; IDENT "next"; "." -> <:ast< (Go "next") >>
+      | IDENT "Show"; "Proof"; "." -> <:ast< (ShowProof) >>
+      | IDENT "Guarded"; "." -> <:ast< (CheckGuard) >>
+      | IDENT "Show"; IDENT "Tree"; "." -> <:ast< (ShowTree) >>
+      | IDENT "Show"; IDENT "Conjectures"; "." -> <:ast< (ShowProofs) >>
+
+(* Tactic Definition *)
+
+      |IDENT "Tactic"; "Definition"; name=identarg; ":="; body=Tactic.tactic;
+        "." -> <:ast<(TACDEF $name (AST $body))>>
+      |IDENT "Tactic"; "Definition"; name=identarg; largs=LIST1 input_fun;
+        ":="; body=Tactic.tactic; "." ->
+        <:ast<(TACDEF $name (AST (FUN (FUNVAR ($LIST $largs)) $body)))>>
+      |IDENT "Recursive"; IDENT "Tactic"; "Definition"; vc=vrec_clause ; "." ->
+        (match vc with
+            Coqast.Node(_,"RECCLAUSE",nme::tl) ->
+              <:ast<(TACDEF $nme (AST (REC $vc)))>>
+           |_ ->
+             anomalylabstrm "Gram.vernac" [<'sTR "Not a correct RECCLAUSE">])
+      |IDENT "Recursive"; IDENT "Tactic"; "Definition"; vc=vrec_clause;
+        IDENT "And"; vcl=LIST1 vrec_clause SEP IDENT "And"; "." ->
+        let nvcl=
+          List.fold_right
+            (fun e b -> match e with
+                Coqast.Node(_,"RECCLAUSE",nme::_) ->
+                  nme::<:ast<(AST (REC $e))>>::b
+               |_ ->
+                 anomalylabstrm "Gram.vernac" [<'sTR
+                   "Not a correct RECCLAUSE">]) (vc::vcl) []
+        in
+          <:ast<(TACDEF ($LIST $nvcl))>>
+
+(* Hints for Auto and EAuto *)
+
+      | IDENT "Hint"; hintname = identarg; dbname = opt_identarg_list; ":=";
+	IDENT "Resolve"; c = constrarg; "." ->
+	  <:ast<(HintResolve $hintname (VERNACARGLIST ($LIST $dbname)) $c)>>
+	  
+      | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
+	IDENT "Immediate"; c = constrarg; "." ->
+	  <:ast<(HintImmediate $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
+	  
+      | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
+	IDENT "Unfold"; c = identarg; "." ->
+	  <:ast<(HintUnfold $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
+	  
+      | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
+	IDENT "Constructors"; c = identarg;  "." ->
+	  <:ast<(HintConstructors $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
+	  
+      | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
+	IDENT "Extern"; n = numarg; c = constrarg ; tac = tacarg; "." ->
+	  <:ast<(HintExtern $hintname (VERNACARGLIST ($LIST $dbnames)) 
+		   $n $c (TACTIC $tac))>>
+	  
+      | IDENT "Hints"; IDENT "Resolve"; l = ne_identarg_list; 
+	dbnames = opt_identarg_list; "." ->
+          <:ast< (HintsResolve (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
+	  
+      | IDENT "Hints"; IDENT "Immediate"; l = ne_identarg_list; 
+	dbnames = opt_identarg_list; "." ->
+          <:ast< (HintsImmediate (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
+	  
+      | IDENT "Hints"; IDENT "Unfold"; l = ne_identarg_list;
+	dbnames = opt_identarg_list; "." ->
+          <:ast< (HintsUnfold (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
+	  
+      | IDENT "HintDestruct"; 
+                dloc = destruct_location;
+                na  = identarg;
+                hyptyp = constrarg;
+                pri = numarg;
+                tac = Prim.astact; "." -> 
+          <:ast< (HintDestruct $na (AST $dloc) $hyptyp $pri (AST $tac))>>
+
+      | n = numarg; ":"; tac = tacarg; "." ->
+          <:ast< (SOLVE $n (TACTIC $tac)) >> 
+
+(*This entry is not commented, only for debug*)
+      | IDENT "PrintConstr"; com = constrarg; "." ->
+          <:ast< (PrintConstr $com)>>
+      ] ];
+  END
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f10a81d27..a3145ca04 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -9,6 +9,9 @@ open Tactic
 open Util
 open Vernac
 
+(* Rem: do not join the different GEXTEND into one, it breaks native *)
+(* compilation on PowerPC and Sun architectures *)
+
 GEXTEND Gram
   GLOBAL: vernac;
   vernac:
@@ -356,6 +359,7 @@ GEXTEND Gram
   ;
 END
 
+(* Modules management *)   
 GEXTEND Gram
   GLOBAL: command;
 
@@ -370,24 +374,7 @@ GEXTEND Gram
       |  -> <:ast< "UNSPECIFIED" >> ] ]
   ;
   command:
-    [ [ 
-
-(* State management *)
-        IDENT "Write"; IDENT "State"; id = identarg; "." ->
-          <:ast< (WriteState $id) >>
-      | IDENT "Write"; IDENT "State"; s = stringarg; "." ->
-          <:ast< (WriteState $s) >>
-      | IDENT "Restore";  IDENT "State"; id = identarg; "." ->
-          <:ast< (RestoreState $id) >>
-      | IDENT "Restore";  IDENT "State"; s = stringarg; "." ->
-          <:ast< (RestoreState $s) >>
-      | IDENT "Reset"; id = identarg; "." -> <:ast< (ResetName $id) >>
-      | IDENT "Reset"; IDENT "Initial"; "." -> <:ast< (ResetInitial) >>
-      | IDENT "Reset"; IDENT "Section"; id = identarg; "." ->
-          <:ast< (ResetSection $id) >>
-
-(* Modules management *)   
-      | "Load"; verbosely = [ IDENT "Verbose" -> "Verbose" | -> "" ];
+    [ [ "Load"; verbosely = [ IDENT "Verbose" -> "Verbose" | -> "" ];
 	s = [ s = STRING -> s | s = IDENT -> s ]; "." ->
           <:ast< (LoadFile ($STR $verbosely) ($STR $s)) >>
       | "Compile";
@@ -419,6 +406,29 @@ GEXTEND Gram
       | IDENT "Declare"; IDENT "ML"; IDENT "Module";
         l = ne_stringarg_list; "." -> <:ast< (DeclareMLModule ($LIST $l)) >>
       | IDENT "Import"; id = identarg; "." -> <:ast< (ImportModule $id) >>
+  ] ]
+  ;
+END
+
+GEXTEND Gram
+  GLOBAL: command;
+
+  command:
+    [ [ 
+
+(* State management *)
+        IDENT "Write"; IDENT "State"; id = identarg; "." ->
+          <:ast< (WriteState $id) >>
+      | IDENT "Write"; IDENT "State"; s = stringarg; "." ->
+          <:ast< (WriteState $s) >>
+      | IDENT "Restore";  IDENT "State"; id = identarg; "." ->
+          <:ast< (RestoreState $id) >>
+      | IDENT "Restore";  IDENT "State"; s = stringarg; "." ->
+          <:ast< (RestoreState $s) >>
+      | IDENT "Reset"; id = identarg; "." -> <:ast< (ResetName $id) >>
+      | IDENT "Reset"; IDENT "Initial"; "." -> <:ast< (ResetInitial) >>
+      | IDENT "Reset"; IDENT "Section"; id = identarg; "." ->
+          <:ast< (ResetSection $id) >>
       
 (* Extraction *)
       | IDENT "Extraction"; id = identarg; "." ->
@@ -431,155 +441,4 @@ GEXTEND Gram
 
  ] ];
     END
-
-(* Proof commands *)
-GEXTEND Gram
-  GLOBAL: command ne_constrarg_list;
-
-  destruct_location :
-  [ [ IDENT "Conclusion"  -> <:ast< (CONCL)>>
-    | IDENT "Discardable"; "Hypothesis"  -> <:ast< (DiscardableHYP)>>
-    | "Hypothesis"   -> <:ast< (PreciousHYP)>> ]]
-  ;
-  ne_constrarg_list:
-  [ [ l = LIST1 constrarg -> l ] ]
-  ;
-  opt_identarg_list:
-  [ [ -> []
-    | ":"; l = LIST1 identarg -> l ] ]
-  ;
-  vrec_clause:
-    [ [ name=identarg; it=LIST1 input_fun; ":="; body=tactic_expr ->
-          <:ast<(RECCLAUSE $name (FUNVAR ($LIST $it)) $body)>> ] ]
-  ;
-  command:
-    [ [ IDENT "Goal"; c = constrarg; "." -> <:ast< (GOAL $c) >>
-      | IDENT "Goal"; "." -> <:ast< (GOAL) >>
-      | "Proof"; "." -> <:ast< (GOAL) >>
-      | IDENT "Abort"; "." -> <:ast< (ABORT) >>
-      | "Qed"; "." -> <:ast< (SaveNamed) >>
-      | IDENT "Save"; "." -> <:ast< (SaveNamed) >>
-      | IDENT "Defined"; "." -> <:ast< (DefinedNamed) >>
-      | IDENT "Save"; IDENT "Remark"; id = identarg; "." ->
-          <:ast< (SaveAnonymousRmk $id) >>
-      | IDENT "Save"; IDENT "Theorem"; id = identarg; "." ->
-          <:ast< (SaveAnonymousThm $id) >>
-      | IDENT "Save"; id = identarg; "." -> <:ast< (SaveAnonymousThm $id) >>
-      | IDENT "Suspend"; "." -> <:ast< (SUSPEND) >>
-      | IDENT "Resume"; "." -> <:ast< (RESUME) >>
-      | IDENT "Resume"; id = identarg; "." -> <:ast< (RESUME $id) >>
-      | IDENT "Abort"; IDENT "All"; "." -> <:ast< (ABORTALL) >>
-      | IDENT "Abort"; id = identarg; "." -> <:ast< (ABORT $id) >>
-      | IDENT "Restart"; "." -> <:ast< (RESTART) >>
-      | "Proof"; c = constrarg; "." -> <:ast< (PROOF $c) >>
-      | IDENT "Undo"; "." -> <:ast< (UNDO 1) >>
-      | IDENT "Undo"; n = numarg; "." -> <:ast< (UNDO $n) >>
-      | IDENT "Show"; n = numarg; "." -> <:ast< (SHOW $n) >>
-      | IDENT "Show"; IDENT "Implicits"; n = numarg; "." ->
-          <:ast< (SHOWIMPL $n) >>
-      | IDENT "Focus"; "." -> <:ast< (FOCUS) >>
-      | IDENT "Focus"; n = numarg; "." -> <:ast< (FOCUS $n) >>
-      | IDENT "Unfocus"; "." -> <:ast< (UNFOCUS) >>
-      | IDENT "Show"; "." -> <:ast< (SHOW) >>
-      | IDENT "Show"; IDENT "Implicits"; "." -> <:ast< (SHOWIMPL) >>
-      | IDENT "Show"; IDENT "Node"; "." -> <:ast< (ShowNode) >>
-      | IDENT "Show"; IDENT "Script"; "." -> <:ast< (ShowScript) >>
-      | IDENT "Show"; IDENT "Existentials"; "." -> <:ast< (ShowEx) >>
-      | IDENT "Existential"; n = numarg; ":="; c = constrarg; "." ->
-          <:ast< (EXISTENTIAL $n $c) >>
-      | IDENT "Existential"; n = numarg; ":="; c1 = Constr.constr; ":";
-        c2 = Constr.constr; "." ->
-          <:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >>
-      | IDENT "Existential"; n = numarg; ":"; c2 = Constr.constr; ":=";
-        c1 = Constr.constr; "." ->
-          <:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >>
-      | IDENT "Explain"; "Proof"; l = numarg_list; "." ->
-          <:ast< (ExplainProof ($LIST $l)) >>
-      | IDENT "Explain"; "Proof"; IDENT "Tree"; l = numarg_list; "." ->
-          <:ast< (ExplainProofTree ($LIST $l)) >>
-      | IDENT "Go"; n = numarg; "." -> <:ast< (Go $n) >>
-      | IDENT "Go"; IDENT "top"; "." -> <:ast< (Go "top") >>
-      | IDENT "Go"; IDENT "prev"; "." -> <:ast< (Go "prev") >>
-      | IDENT "Go"; IDENT "next"; "." -> <:ast< (Go "next") >>
-      | IDENT "Show"; "Proof"; "." -> <:ast< (ShowProof) >>
-      | IDENT "Guarded"; "." -> <:ast< (CheckGuard) >>
-      | IDENT "Show"; IDENT "Tree"; "." -> <:ast< (ShowTree) >>
-      | IDENT "Show"; IDENT "Conjectures"; "." -> <:ast< (ShowProofs) >>
-
-(* Tactic Definition *)
-
-      |IDENT "Tactic"; "Definition"; name=identarg; ":="; body=Tactic.tactic;
-        "." -> <:ast<(TACDEF $name (AST $body))>>
-      |IDENT "Tactic"; "Definition"; name=identarg; largs=LIST1 input_fun;
-        ":="; body=Tactic.tactic; "." ->
-        <:ast<(TACDEF $name (AST (FUN (FUNVAR ($LIST $largs)) $body)))>>
-      |IDENT "Recursive"; IDENT "Tactic"; "Definition"; vc=vrec_clause ; "." ->
-        (match vc with
-            Coqast.Node(_,"RECCLAUSE",nme::tl) ->
-              <:ast<(TACDEF $nme (AST (REC $vc)))>>
-           |_ ->
-             anomalylabstrm "Gram.vernac" [<'sTR "Not a correct RECCLAUSE">])
-      |IDENT "Recursive"; IDENT "Tactic"; "Definition"; vc=vrec_clause;
-        IDENT "And"; vcl=LIST1 vrec_clause SEP IDENT "And"; "." ->
-        let nvcl=
-          List.fold_right
-            (fun e b -> match e with
-                Coqast.Node(_,"RECCLAUSE",nme::_) ->
-                  nme::<:ast<(AST (REC $e))>>::b
-               |_ ->
-                 anomalylabstrm "Gram.vernac" [<'sTR
-                   "Not a correct RECCLAUSE">]) (vc::vcl) []
-        in
-          <:ast<(TACDEF ($LIST $nvcl))>>
-
-(* Hints for Auto and EAuto *)
-
-      | IDENT "Hint"; hintname = identarg; dbname = opt_identarg_list; ":=";
-	IDENT "Resolve"; c = constrarg; "." ->
-	  <:ast<(HintResolve $hintname (VERNACARGLIST ($LIST $dbname)) $c)>>
-	  
-      | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
-	IDENT "Immediate"; c = constrarg; "." ->
-	  <:ast<(HintImmediate $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
-	  
-      | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
-	IDENT "Unfold"; c = identarg; "." ->
-	  <:ast<(HintUnfold $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
-	  
-      | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
-	IDENT "Constructors"; c = identarg;  "." ->
-	  <:ast<(HintConstructors $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
-	  
-      | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
-	IDENT "Extern"; n = numarg; c = constrarg ; tac = tacarg; "." ->
-	  <:ast<(HintExtern $hintname (VERNACARGLIST ($LIST $dbnames)) 
-		   $n $c (TACTIC $tac))>>
-	  
-      | IDENT "Hints"; IDENT "Resolve"; l = ne_identarg_list; 
-	dbnames = opt_identarg_list; "." ->
-          <:ast< (HintsResolve (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
-	  
-      | IDENT "Hints"; IDENT "Immediate"; l = ne_identarg_list; 
-	dbnames = opt_identarg_list; "." ->
-          <:ast< (HintsImmediate (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
-	  
-      | IDENT "Hints"; IDENT "Unfold"; l = ne_identarg_list;
-	dbnames = opt_identarg_list; "." ->
-          <:ast< (HintsUnfold (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
-	  
-      | IDENT "HintDestruct"; 
-                dloc = destruct_location;
-                na  = identarg;
-                hyptyp = constrarg;
-                pri = numarg;
-                tac = Prim.astact; "." -> 
-          <:ast< (HintDestruct $na (AST $dloc) $hyptyp $pri (AST $tac))>>
-
-      | n = numarg; ":"; tac = tacarg; "." ->
-          <:ast< (SOLVE $n (TACTIC $tac)) >> 
-
-(*This entry is not commented, only for debug*)
-      | IDENT "PrintConstr"; com = constrarg; "." ->
-          <:ast< (PrintConstr $com)>>
-      ] ];
-  END
+;;