Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 524 insertions, 0 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
new file mode 100644
index 00000000..e2eecf55
--- /dev/null
+++ b/parsing/g_vernac.ml4
@@ -0,0 +1,524 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: g_vernac.ml4,v 1.93.2.2 2004/07/16 20:51:12 herbelin Exp $ *)
+
+open Names
+open Topconstr
+open Vernacexpr
+open Pcoq
+open Pp
+open Tactic
+open Util
+open Constr
+open Vernac_
+open Prim
+open Decl_kinds
+
+open Genarg
+
+let evar_constr loc = CHole loc
+
+let class_rawexpr = G_basevernac.class_rawexpr
+let thm_token = G_proofs.thm_token
+
+(* Rem: do not join the different GEXTEND into one, it breaks native *)
+(* compilation on PowerPC and Sun architectures *)
+
+let filter_com (b,e) =
+  let (b,e) = unloc (b,e) in
+  Pp.comments := List.filter (fun ((b',e'),s) -> b'<b || e'>e) !Pp.comments 
+
+if !Options.v7 then
+GEXTEND Gram
+  GLOBAL: vernac gallina_ext;
+  vernac:
+    (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
+    (* "." is still in the stream and discard_to_dot works correctly         *)
+    [ [ g = gallina; "." -> g 
+      | g = gallina_ext; "." -> g
+      | c = command; "." -> c 
+      | c = syntax; "." -> c
+      | n = natural; ":"; tac = Tactic.tactic; "." -> VernacSolve (n,tac,true) 
+      | n = natural; ":"; tac = Tactic.tactic; "!!" -> VernacSolve (n,tac,false)
+      | n = natural; ":"; v = check_command; "." -> v (Some n)
+      | "["; l = vernac_list_tail -> VernacList l
+
+      (* For translation from V7 to V8 *)
+      | IDENT "V7only"; v = vernac ->
+          filter_com loc; VernacV7only v
+      | IDENT "V8only"; v = vernac -> VernacV8only v
+
+(*
+      (* This is for "Grammar vernac" rules *)
+      | id = METAIDENT -> VernacVar (Names.id_of_string id)
+*)
+    ] ]
+  ;
+    
+  check_command:
+    [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = constr ->
+          fun g -> VernacCheckMayEval (Some r, g, c)
+      | IDENT "Check"; c = constr ->
+	  fun g -> VernacCheckMayEval (None, g, c) ] ]
+  ;
+  vernac: FIRST
+    [ [ IDENT "Time"; v = vernac  -> VernacTime v ] ]
+  ;
+  vernac: LAST
+    [ [ tac = Tactic.tactic; "." -> VernacSolve (1,tac,true)
+      | tac = Tactic.tactic; "!!" -> VernacSolve (1,tac,false)
+      | IDENT "Existential"; n = natural; c = constr_body ->
+	  VernacSolveExistential (n,c)
+    ] ]
+  ;
+  constr_body:
+    [ [ ":="; c = constr; ":"; t = constr -> CCast(loc,c,t)
+      | ":"; t = constr; ":="; c = constr -> CCast(loc,c,t)
+      | ":="; c = constr -> c ] ]
+  ;
+  vernac_list_tail:
+    [ [ v = located_vernac; l = vernac_list_tail -> v :: l
+      | "]"; "." -> [] ] ]
+  ;
+  located_vernac:
+    [ [ v = vernac -> loc, v ] ]
+  ;
+END
+
+let test_plurial_form = function
+  | [_,([_],_)] ->
+      Options.if_verbose warning
+      "Keywords Variables/Hypotheses/Parameters expect more than one assumption"
+  | _ -> ()
+
+(* Gallina declarations *)
+if !Options.v7 then
+GEXTEND Gram
+  GLOBAL: gallina gallina_ext thm_token;
+
+  thm_token:
+    [ [ "Theorem" -> Theorem
+      | IDENT "Lemma" -> Lemma
+      | IDENT "Fact" -> Fact
+      | IDENT "Remark" -> Remark ] ]
+  ;
+  def_token:
+    [ [ "Definition" -> (fun _ _ -> ()), (Global, Definition)
+      | IDENT "Local" -> (fun _ _ -> ()), (Local, Definition)
+      | IDENT "SubClass"  -> Class.add_subclass_hook, (Global, SubClass)
+      | IDENT "Local"; IDENT "SubClass"  ->
+	  Class.add_subclass_hook, (Local, SubClass) ] ] 
+  ;
+  assumption_token:
+    [ [ "Hypothesis" -> (Local, Logical)
+      | "Variable" -> (Local, Definitional)
+      | "Axiom" -> (Global, Logical)
+      | "Parameter" -> (Global, Definitional)
+      | IDENT "Conjecture" -> (Global,Conjectural) ] ]
+  ;
+  assumptions_token:
+    [ [ IDENT "Hypotheses" -> (Local, Logical)
+      | IDENT "Variables" -> (Local, Definitional)
+      | IDENT "Parameters" -> (Global, Definitional) ] ]
+  ;
+  of_type_with_opt_coercion:
+    [ [ ":>" -> true
+      | ":"; ">" -> true
+      | ":" -> false ] ]
+  ;
+  params:
+    [ [ idl = LIST1 identref SEP ","; coe = of_type_with_opt_coercion; 
+        c = constr -> (coe,(idl,c))
+    ] ]
+  ;
+  ne_params_list:
+    [ [ ll = LIST1 params SEP ";" -> ll ] ]
+  ;
+  name_comma_list_tail:
+    [ [ ","; nal = LIST1 name SEP "," -> nal | -> [] ] ]
+  ;
+  ident_comma_list_tail:
+    [ [ ","; nal = LIST1 identref SEP "," -> nal | -> [] ] ]
+  ;
+  decl_notation:
+    [ [ "where"; ntn = STRING; ":="; c = constr; 
+         scopt = OPT [ ":"; sc = IDENT -> sc] -> (ntn,c,scopt) ] ]
+  ;
+  type_option:
+    [ [ ":"; c = constr -> c 
+      | -> evar_constr loc ] ]
+  ;
+  opt_casted_constr:
+    [ [ c = constr;  ":"; t = constr -> CCast(loc,c,t)
+      | c = constr -> c ] ]
+  ;
+  vardecls:
+    [ [ na = name; nal = name_comma_list_tail; c = type_option
+          -> LocalRawAssum (na::nal,c)
+      | na = name; "="; c = opt_casted_constr ->
+          LocalRawDef (na,c)
+      | na = name; ":="; c = opt_casted_constr ->
+          LocalRawDef (na,c)
+    ] ]
+  ;
+  binders:
+    [ [ "["; bl = LIST1 vardecls SEP ";"; "]" -> bl ] ]
+  ;
+  binders_list:
+    [ [ bls = LIST0 binders -> List.flatten bls ] ]
+  ;
+  reduce:
+    [ [ IDENT "Eval"; r = Tactic.red_expr; "in" -> Some r
+      | -> None ] ]
+  ;
+  def_body:
+    [ [ bl = binders_list; ":="; red = reduce; c = constr; ":"; t = constr ->
+          DefineBody (bl, red, c, Some t)
+      | bl = binders_list; ":"; t = constr; ":="; red = reduce; c = constr ->
+          DefineBody (bl, red, c, Some t)
+      | bl = binders_list; ":="; red = reduce; c = constr ->
+          DefineBody (bl, red, c, None)
+      | bl = binders_list; ":"; t = constr ->
+          ProveBody (bl, t) ] ]
+  ;
+  gallina:
+    (* Definition, Theorem, Variable, Axiom, ... *)
+    [ [ thm = thm_token; id = identref; ":"; c = constr ->
+         VernacStartTheoremProof (thm, id, ([], c), false, (fun _ _ -> ()))
+      | (f,d) = def_token; id = identref; b = def_body -> 
+          VernacDefinition (d, id, b, f)
+      | stre = assumption_token; bl = ne_params_list -> 
+	  VernacAssumption (stre, bl)
+      | stre = assumptions_token; bl = ne_params_list ->
+	  test_plurial_form bl;
+	  VernacAssumption (stre, bl)
+      ] ]
+  ;
+  (* Gallina inductive declarations *)
+  finite_token:
+    [ [ "Inductive" -> true
+      | "CoInductive" -> false ] ]
+  ;
+  record_token:
+    [ [ IDENT "Record" -> true | IDENT "Structure" -> false ] ]
+  ;
+  constructor:
+    [ [ idl = LIST1 identref SEP ","; coe = of_type_with_opt_coercion;
+        c = constr -> List.map (fun id -> (coe,(id,c))) idl ] ]
+  ;
+  constructor_list:
+    [ [ "|"; l = LIST1 constructor SEP "|" -> List.flatten l
+      | l = LIST1 constructor SEP "|" -> List.flatten l
+      |  -> [] ] ]
+  ;
+  block_old_style:
+    [ [ ind = oneind_old_style; "with"; indl = block_old_style -> ind :: indl
+      | ind = oneind_old_style -> [ind] ] ]
+  ;
+  oneind_old_style:
+    [ [ id = identref; ":"; c = constr; ":="; lc = constructor_list ->
+          (id,c,lc) ] ]
+  ;
+  oneind:
+    [ [ id = identref; indpar = simple_binders_list; ":"; c = constr; 
+        ":="; lc = constructor_list; ntn = OPT decl_notation ->
+	  (id,ntn,indpar,c,lc) ] ]
+  ;
+  simple_binders_list:
+    [ [ bl = ne_simple_binders_list -> bl
+      |  -> [] ] ]
+  ;
+  opt_coercion:
+    [ [ ">" -> true
+      |  -> false ] ]
+  ;
+  onescheme:
+    [ [ id = identref; ":="; dep = dep; ind = global; IDENT "Sort";
+        s = sort -> (id,dep,ind,s) ] ]
+  ;
+  schemes:
+    [ [ recl = LIST1 onescheme SEP "with" -> recl ] ]
+  ;
+  dep:
+    [ [ IDENT "Induction"; IDENT "for" -> true
+      | IDENT "Minimality"; IDENT "for" -> false ] ]
+  ;
+  onerec:
+    [ [ id = base_ident; bl = ne_fix_binders; ":"; type_ = constr;
+        ":="; def = constr; ntn = OPT decl_notation ->
+          let ni = List.length (List.flatten (List.map fst bl)) - 1 in
+          let bl = List.map (fun(nal,ty)->LocalRawAssum(nal,ty)) bl in
+	  ((id, ni, bl, type_, def), ntn) ] ]
+  ;
+  specifrec:
+    [ [ l = LIST1 onerec SEP "with" -> l ] ]
+  ;
+  onecorec:
+    [ [ id = base_ident; ":"; c = constr; ":="; def = constr ->
+          (id,[],c,def) ] ]
+  ;
+  specifcorec:
+    [ [ l = LIST1 onecorec SEP "with" -> l ] ]
+  ;
+  record_field:
+    [ [ id = name; oc = of_type_with_opt_coercion; t = constr ->
+          (oc,AssumExpr (id,t))
+      | id = name; oc = of_type_with_opt_coercion; t = constr;
+	":="; b = constr ->
+	  (oc,DefExpr (id,b,Some t))
+      | id = name; ":="; b = constr ->
+	  (false,DefExpr (id,b,None)) ] ]
+  ;
+  fields:
+    [ [ fs = LIST0 record_field SEP ";" -> fs ] ]
+  ;
+  simple_binders:
+    [ [ "["; bll = LIST1 vardecls SEP ";"; "]" -> bll ] ]
+  ;
+  ne_simple_binders_list:
+    [ [ bll = LIST1 simple_binders -> (List.flatten bll) ] ]
+  ;
+  fix_params:
+    [ [ idl = LIST1 name SEP ","; ":"; c = constr -> (idl, c)
+      | idl = LIST1 name SEP "," -> (idl, evar_constr dummy_loc)
+    ] ]
+  ;
+  fix_binders:
+    [ [ "["; bll = LIST1 fix_params SEP ";"; "]" -> bll ] ]
+  ;
+  ne_fix_binders:
+    [ [ bll = LIST1 fix_binders -> List.flatten bll ] ]
+  ;
+  rec_constructor:
+    [ [ c = identref -> Some c
+      |  -> None ] ]
+  ;
+  gallina_ext:
+    [ [ IDENT "Mutual"; bl = ne_simple_binders_list ; f = finite_token;
+        indl = block_old_style ->
+	  let indl' = List.map (fun (id,ar,c) -> (id,None,bl,ar,c)) indl in
+	  VernacInductive (f,indl')
+      | b = record_token; oc = opt_coercion; name = identref;
+	ps = simple_binders_list; ":";
+	s = constr; ":="; c = rec_constructor; "{"; fs = fields; "}" ->
+	  VernacRecord (b,(oc,name),ps,s,c,fs)
+    ] ]
+  ;
+  gallina:
+    [ [ IDENT "Mutual"; f = finite_token; indl = LIST1 oneind SEP "with" ->
+          VernacInductive (f,indl)
+      | f = finite_token; indl = LIST1 oneind SEP "with" ->
+          VernacInductive (f,indl)
+      | "Fixpoint"; recs = specifrec -> VernacFixpoint recs
+      | "CoFixpoint"; corecs = specifcorec -> VernacCoFixpoint corecs
+      | IDENT "Scheme"; l = schemes -> VernacScheme l
+      | f = finite_token; s = csort; id = identref;
+	indpar = simple_binders_list; ":="; lc = constructor_list -> 
+          VernacInductive (f,[id,None,indpar,s,lc]) ] ]
+  ;
+  csort:
+    [ [ s = sort -> CSort (loc,s) ] ]
+  ;
+  gallina_ext:
+    [ [ 
+(* Sections *)
+	IDENT "Section"; id = identref -> VernacBeginSection id
+      | IDENT "Chapter"; id = identref -> VernacBeginSection id ] ]
+  ;
+  module_vardecls:
+    [ [ id = identref; idl = ident_comma_list_tail; ":";
+        mty = Module.module_type -> (id::idl,mty) ] ]
+  ;
+  module_binders:
+    [ [ "["; bl = LIST1 module_vardecls SEP ";"; "]" -> bl ] ]
+  ;
+  module_binders_list:
+    [ [ bls = LIST0 module_binders -> List.flatten bls ] ]
+  ;
+  of_module_type:
+    [ [ ":"; mty = Module.module_type -> (mty, true) 
+      | "<:"; mty = Module.module_type -> (mty, false) ] ]
+  ;
+  is_module_type:
+    [ [ ":="; mty = Module.module_type -> mty ] ]
+  ;
+  is_module_expr:
+    [ [ ":="; mexpr = Module.module_expr -> mexpr ] ]
+  ;
+  gallina_ext:
+    [ [ 
+	  (* Interactive module declaration *)
+	IDENT "Module"; id = identref; 
+	bl = module_binders_list; mty_o = OPT of_module_type; 
+	mexpr_o = OPT is_module_expr ->
+	  VernacDefineModule (id, bl, mty_o, mexpr_o)
+	  
+      | IDENT "Module"; "Type"; id = identref; 
+	bl = module_binders_list; mty_o = OPT is_module_type ->
+	  VernacDeclareModuleType (id, bl, mty_o)
+	  
+      | IDENT "Declare"; IDENT "Module"; id = identref; 
+	bl = module_binders_list; mty_o = OPT of_module_type; 
+	mexpr_o = OPT is_module_expr ->
+	  VernacDeclareModule (id, bl, mty_o, mexpr_o)
+
+	  (* This end a Section a Module or a Module Type *)
+
+      | IDENT "End"; id = identref -> VernacEndSegment id
+
+
+(* Transparent and Opaque *)
+      | IDENT "Transparent"; l = LIST1 global -> VernacSetOpacity (false, l)
+      | IDENT "Opaque"; l = LIST1 global -> VernacSetOpacity (true, l)
+
+(* Canonical structure *)
+      | IDENT "Canonical"; IDENT "Structure"; qid = global ->
+	  VernacCanonical qid
+      | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
+          let s = Ast.coerce_global_to_id qid in
+	  VernacDefinition 
+	    ((Global,CanonicalStructure),(dummy_loc,s),d,Recordobj.add_object_hook)
+      (* Rem: LOBJECT, OBJCOERCION, LOBJCOERCION have been removed
+         (they were unused and undocumented) *)
+
+(* Coercions *)
+      | IDENT "Coercion"; qid = global; d = def_body ->
+          let s = Ast.coerce_global_to_id qid in
+	  VernacDefinition ((Global,Coercion),(dummy_loc,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,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
+      | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
+         ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> 
+	   VernacIdentityCoercion (Local, f, s, t)
+      | IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
+         s = class_rawexpr; ">->"; t = class_rawexpr -> 
+	   VernacIdentityCoercion (Global, f, s, t)
+      | IDENT "Coercion"; IDENT "Local"; qid = global; ":";
+	 s = class_rawexpr; ">->"; t = class_rawexpr -> 
+	  VernacCoercion (Local, qid, s, t)
+      | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->";
+         t = class_rawexpr ->
+	  VernacCoercion (Global, qid, s, t)
+      | IDENT "Class"; IDENT "Local"; c = global ->
+	  Pp.warning "Class is obsolete"; VernacNop
+      | IDENT "Class"; c = global ->
+	  Pp.warning "Class is obsolete"; VernacNop
+
+(* Implicit *)
+(*
+      | IDENT "Syntactic"; "Definition"; id = identref; ":="; c = constr;
+         n = OPT [ "|"; n = natural -> n ] ->
+	   VernacSyntacticDefinition (id,c,n)
+*)
+      | IDENT "Syntactic"; "Definition"; id = ident; ":="; c = constr;
+         n = OPT [ "|"; n = natural -> n ] ->
+	   let c = match n with
+	     | Some n ->
+		 let l = list_tabulate (fun _ -> (CHole (loc),None)) n in
+		 CApp (loc,(None,c),l)
+	     | None -> c in
+	   VernacSyntacticDefinition (id,c,false,true)
+      | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
+	  let l = List.map (fun n -> ExplByPos n) l in
+	  VernacDeclareImplicits (qid,Some l)
+      | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None)
+
+      | IDENT "Implicit"; ["Variable"; "Type" | IDENT "Variables"; "Type"];
+	   idl = LIST1 identref SEP ","; ":"; c = constr -> VernacReserve (idl,c)
+
+      (* For compatibility *)
+      | IDENT "Implicit"; IDENT "Arguments"; IDENT "On" ->
+	  VernacSetOption
+	    (Goptions.SecondaryTable ("Implicit","Arguments"), BoolValue true)
+      | IDENT "Implicit"; IDENT "Arguments"; IDENT "Off" ->
+	  VernacSetOption
+	    (Goptions.SecondaryTable ("Implicit","Arguments"), BoolValue false)
+  ] ]
+  ;
+END
+
+(* Modules management *)   
+if !Options.v7 then
+GEXTEND Gram
+  GLOBAL: command;
+
+  export_token:
+    [ [ IDENT "Import" -> false
+      | IDENT "Export" -> true
+      |  -> false ] ]
+  ;
+  specif_token:
+    [ [ IDENT "Implementation" -> Some false
+      | IDENT "Specification" -> Some true
+      |  -> None ] ]
+  ;
+  command:
+    [ [ "Load"; verbosely = [ IDENT "Verbose" -> true | -> false ];
+	s = [ s = STRING -> s | s = IDENT -> s ] ->
+	  VernacLoad (verbosely, s)
+(*      | "Compile";
+	verbosely =
+          [ IDENT "Verbose" -> "Verbose"
+          | -> "" ];
+	IDENT "Module";
+	only_spec =
+          [ IDENT "Specification" -> "Specification"
+          | -> "" ];
+	mname = [ s = STRING -> s | s = IDENT -> s ];
+	fname = OPT [ s = STRING -> s | s = IDENT -> s ] -> ExtraVernac
+          let fname = match fname with Some s -> s | None -> mname in
+            <:ast< (CompileFile ($STR $verbosely) ($STR $only_spec)
+                      ($STR $mname) ($STR $fname))>>
+*)
+      | IDENT "Read"; IDENT "Module"; qidl = LIST1 global ->
+	  VernacRequire (None, None, qidl)
+      | IDENT "Require"; export = export_token; specif = specif_token;
+        qidl = LIST1 global -> VernacRequire (Some export, specif, qidl)
+(*      | IDENT "Require"; export = export_token; specif = specif_token;
+        id = identref; filename = STRING -> 
+	  VernacRequireFrom (export, specif, id, filename) *)
+      | IDENT "Require"; export = export_token; specif = specif_token;
+        filename = STRING -> 
+	  VernacRequireFrom (Some export, specif, filename)
+      | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 STRING ->
+	  VernacDeclareMLModule l
+      | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl)
+      | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl)
+  ] 
+]
+  ;
+END
+
+if !Options.v7 then
+GEXTEND Gram
+  GLOBAL: command;
+
+  command:
+    [ [ 
+
+(* State management *)
+        IDENT "Write"; IDENT "State"; s = IDENT -> VernacWriteState s
+      | IDENT "Write"; IDENT "State"; s = STRING -> VernacWriteState s
+      | IDENT "Restore"; IDENT "State"; s = IDENT -> VernacRestoreState s
+      | IDENT "Restore"; IDENT "State"; s = STRING -> VernacRestoreState s
+
+(* Resetting *)
+      | IDENT "Reset"; id = identref -> VernacResetName id
+      | IDENT "Reset"; IDENT "Initial" -> VernacResetInitial
+      | IDENT "Back" -> VernacBack 1
+      | IDENT "Back"; n = natural -> VernacBack n
+
+(* Tactic Debugger *)
+      |	IDENT "Debug"; IDENT "On" -> VernacDebug true
+      |	IDENT "Debug"; IDENT "Off" -> VernacDebug false
+
+ ] ];
+    END
+;;