Première proposition d'un type ML exprimant la syntaxe de constr; nettoyage

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

7 files changed, 145 insertions, 158 deletions

diff --git a/parsing/coqast.ml b/parsing/coqast.ml
index e9b9e3c147..cce1dba1ec 100644
--- a/parsing/coqast.ml
+++ b/parsing/coqast.ml
@@ -123,151 +123,83 @@ let rec subst_ast subst ast = match ast with
   | Id _
   | Dynamic _ -> ast
 
-   
-
-(*
-type 'vernac_ast raw_typed_ast =
-  | PureAstNode of t
-  | AstListNode of t list
-  | PureAstNode of t
-  | TacticAstNode of tactic_expr
-  | VernacAstNode of 'vernac_ast
-
-type entry_type =
-  | PureAstType
-  | AstListType
-  | VernacAstType
-  | TacticAstType
-  | VernacAtomAstType
-  | DynamicAstType
-  | QualidAstType
-  | ConstrAstType
-  | BinderAstType
-  | ThmTokAstType
-  | BindingListAstType
-
-type astpat =
-  | Pquote of t
-  | Pmeta of string * tok_kind
-  | Pnode of string * patlist
-  | Pslam of identifier option * astpat
-  | Pmeta_slam of string * astpat
-
-and patlist =
-  | Pcons of astpat * patlist
-  | Plmeta of string
-  | Pnil
-
-type 'a syntax_rule = string * 'a raw_typed_ast * t unparsing_hunk list
-type 'a raw_syntax_entry_ast = precedence * 'a syntax_rule list
-
-type grammar_associativity = Gramext.g_assoc option
-type 'a raw_grammar_action =
-  | SimpleAction of loc * 'a raw_typed_ast
-  | CaseAction of loc *
-     'a raw_grammar_action * entry_type option
-      * (t list * 'a raw_grammar_action) list
-type grammar_production =
-    VTerm of string | VNonTerm of loc * nonterm * string option
-type 'a grammar_rule = string * grammar_production list * 'a raw_grammar_action
-type 'a raw_grammar_entry_ast = 
-    (loc * string) * entry_type option * grammar_associativity * 'a grammar_rule list
-
-type evaluable_global_reference_ast =
-  | AEvalVarRef of identifier
-  | AEvalConstRef of section_path
-
-type flags_ast = int
-
-type red_expr_ast = (t,t,t) Rawterm.red_expr_gen
-
-type vernac_arg = 
-  | VARG_VARGLIST of vernac_arg list
-  | VARG_STRING of string
-  | VARG_NUMBER of int
-  | VARG_NUMBERLIST of int list
-  | VARG_IDENTIFIER of identifier
-  | VARG_QUALID of Nametab.qualid
-  | VCALL of string * vernac_arg list
-  | VARG_CONSTR of t
-  | VARG_CONSTRLIST of t list
-  | VARG_TACTIC of tactic_expr
-  | VARG_REDEXP of red_expr_ast
-  | VARG_BINDER of identifier list * t
-  | VARG_BINDERLIST of (identifier list * t) list
-  | VARG_AST of t
-  | VARG_ASTLIST of t list
-  | VARG_UNIT
-  | VARG_DYN of Dyn.t
-
-type def_kind = DEFINITION | LET | LOCAL | THEOREM | LETTOP | DECL | REMARK
-  | FACT | LEMMA
-  | COERCION | LCOERCION | OBJECT | LOBJECT | OBJCOERCION | LOBJCOERCION
-  | SUBCLASS | LSUBCLASS
-
-open Nametab
-
-type declaration_hook = strength -> global_reference -> unit
-let add_coercion = ref (fun _ _ -> ())
-let add_subclass = ref (fun _ _ -> ())
-let add_object = ref (fun _ _ -> ())
-
-type constr_ast = t
-type sort_expr = t
-
-type simple_binders = identifier * constr_ast
-type constructor_ast = identifier * constr_ast
-type inductive_ast =
-    identifier *  simple_binders list * constr_ast * constructor_ast list
-type fixpoint_ast =
-    identifier * simple_binders list * constr_ast * constr_ast
-type cofixpoint_ast =
-    identifier * constr_ast * constr_ast
-
-type local_decl_expr =
-  | AssumExpr of identifier * constr_ast
-  | DefExpr of identifier * constr_ast * constr_ast option
-
-type vernac_atom_ast =
-  (* Syntax *) 
-  | VernacGrammar of string * vernac_ast raw_grammar_entry_ast list
-  | VernacSyntax of string * vernac_ast raw_syntax_entry_ast list
-  | VernacInfix of grammar_associativity * int * string * t
-  | VernacDistfix of grammar_associativity * int * string * t
-  (* Gallina *)
-  | VernacDefinition of (bool * strength) * identifier * t option * constr_ast * constr_ast option * declaration_hook
-  | VernacStartProof of (bool * strength) * identifier * constr_ast * bool * declaration_hook
-  | VernacEndProof of bool * strength option * identifier option
-  | VernacAssumption of strength * (identifier list * constr_ast) list
-  | VernacInductive of bool * inductive_ast list
-  | VernacFixpoint of fixpoint_ast list
-  | VernacCoFixpoint of cofixpoint_ast list
-  (* Gallina extensions *)
-  | VernacRecord of bool * identifier * simple_binders list * sort_expr * identifier option * (bool * local_decl_expr) list
-
-  (* Commands *)
-  | TacticDefinition of loc * (identifier * tactic_expr) list
-  | VernacSetOpacity of bool * (loc * identifier list) list
-  | VernacSolve of int * tactic_expr
-  (* For temporary compatibility *)
-  | ExtraVernac of t
-  (* For extension *)
-  | VernacExtend of string * vernac_arg list
-  (* For actions in Grammar and patterns in Syntax rules *)
-  | VernacMeta of loc * string
-
-and located_vernac_atom_ast = loc * vernac_atom_ast
-
-and vernac_ast =
-  | VTime of located_vernac_atom_ast
-  | VLoad of bool * string
-  | VernacList of located_vernac_atom_ast list
-  | VernacVar of identifier
-
-type pat = vernac_ast raw_pat
-type typed_ast = vernac_ast raw_typed_ast
-type grammar_action = vernac_ast raw_grammar_action
-type grammar_entry_ast = vernac_ast raw_grammar_entry_ast
-type syntax_entry_ast = vernac_ast raw_syntax_entry_ast
-
-*)
+open Util
+open Rawterm
+open Term
+
+type scope_name = string
+
+type reference_expr = 
+  | RQualid of qualid located
+  | RIdent of identifier located
+
+type explicitation = int
+
+type cases_pattern =
+  | CPatAlias of loc * cases_pattern * identifier
+  | CPatCstr of loc * reference_expr * cases_pattern list
+  | CPatAtom of loc * reference_expr option
+  | CPatNumeral of loc * Bignat.bigint
+
+type ordered_case_style = CIf | CLet | CMatch | CCase
+
+type constr_ast =
+  | CRef of reference_expr
+  | CFix of loc * identifier located * fixpoint_expr list
+  | CCoFix of loc * identifier located * cofixpoint_expr list
+  | CArrow of loc * constr_ast * constr_ast
+  | CProdN of loc * (name located list * constr_ast) list * constr_ast
+  | CLambdaN of loc * (name located list * constr_ast) list * constr_ast
+  | CLetIn of loc * identifier located * constr_ast * constr_ast
+  | CAppExpl of loc * reference_expr * constr_ast list
+  | CApp of loc * constr_ast * (constr_ast * explicitation option) list
+  | CCases of loc * case_style * constr_ast option * constr_ast list *
+      (loc * cases_pattern list * constr_ast) list
+  | COrderedCase of loc * ordered_case_style * constr_ast option * constr_ast * constr_ast list
+  | CHole of loc
+  | CMeta of loc * int
+  | CSort of loc * rawsort
+  | CCast of loc * constr_ast * constr_ast
+  | CNotation of loc * string * constr_ast list
+  | CNumeral of loc * Bignat.bigint
+  | CDelimiters of loc * scope_name * constr_ast
+  | CDynamic of loc * Dyn.t
+
+and local_binder = name located list * constr_ast 
+
+and fixpoint_expr = identifier * local_binder list * constr_ast * constr_ast
+
+and cofixpoint_expr = identifier * constr_ast * constr_ast
+
+let constr_loc = function
+  | CRef (RIdent (loc,_)) -> loc
+  | CRef (RQualid (loc,_)) -> loc
+  | CFix (loc,_,_) -> loc
+  | CCoFix (loc,_,_) -> loc
+  | CArrow (loc,_,_) -> loc
+  | CProdN (loc,_,_) -> loc
+  | CLambdaN (loc,_,_) -> loc
+  | CLetIn (loc,_,_,_) -> loc
+  | CAppExpl (loc,_,_) -> loc
+  | CApp (loc,_,_) -> loc
+  | CCases (loc,_,_,_,_) -> loc
+  | COrderedCase (loc,_,_,_,_) -> loc
+  | CHole loc -> loc
+  | CMeta (loc,_) -> loc
+  | CSort (loc,_) -> loc
+  | CCast (loc,_,_) -> loc
+  | CNotation (loc,_,_) -> loc
+  | CNumeral (loc,_) -> loc
+  | CDelimiters (loc,_,_) -> loc
+  | CDynamic _ -> dummy_loc
+
+let cases_pattern_loc = function
+  | CPatAlias (loc,_,_) -> loc
+  | CPatCstr (loc,_,_) -> loc
+  | CPatAtom (loc,_) -> loc
+  | CPatNumeral (loc,_) -> loc
+
+let replace_vars_constr_ast l t =
+  if l = [] then t else failwith "replace_constr_ast: TODO"
+
+let occur_var_constr_ast id t = Pp.warning "occur_var_constr_ast:TODO"; true
diff --git a/parsing/coqast.mli b/parsing/coqast.mli
index a304aa06b3..817ccb5cd3 100644
--- a/parsing/coqast.mli
+++ b/parsing/coqast.mli
@@ -50,3 +50,61 @@ val fold_tactic_expr :
   ('a -> t -> 'a) -> ('a -> tactic_expr -> 'a) -> 'a -> tactic_expr -> 'a
 val iter_tactic_expr : (tactic_expr -> unit) -> tactic_expr -> unit
 *)
+
+
+open Util
+open Rawterm
+open Term
+
+type scope_name = string
+
+type reference_expr = 
+  | RQualid of qualid located
+  | RIdent of identifier located
+
+type explicitation = int
+
+type cases_pattern =
+  | CPatAlias of loc * cases_pattern * identifier
+  | CPatCstr of loc * reference_expr * cases_pattern list
+  | CPatAtom of loc * reference_expr option
+  | CPatNumeral of loc * Bignat.bigint
+
+type ordered_case_style = CIf | CLet | CMatch | CCase
+
+type constr_ast =
+  | CRef of reference_expr
+  | CFix of loc * identifier located * fixpoint_expr list
+  | CCoFix of loc * identifier located * cofixpoint_expr list
+  | CArrow of loc * constr_ast * constr_ast
+  | CProdN of loc * (name located list * constr_ast) list * constr_ast
+  | CLambdaN of loc * (name located list * constr_ast) list * constr_ast
+  | CLetIn of loc * identifier located * constr_ast * constr_ast
+  | CAppExpl of loc * reference_expr * constr_ast list
+  | CApp of loc * constr_ast * (constr_ast * explicitation option) list
+  | CCases of loc * case_style * constr_ast option * constr_ast list *
+      (loc * cases_pattern list * constr_ast) list
+  | COrderedCase of loc * ordered_case_style * constr_ast option * constr_ast * constr_ast list
+  | CHole of loc
+  | CMeta of loc * int
+  | CSort of loc * rawsort
+  | CCast of loc * constr_ast * constr_ast
+  | CNotation of loc * string * constr_ast list
+  | CNumeral of loc * Bignat.bigint
+  | CDelimiters of loc * scope_name * constr_ast
+  | CDynamic of loc * Dyn.t
+
+and local_binder = name located list * constr_ast 
+
+and fixpoint_expr = identifier * local_binder list * constr_ast * constr_ast
+
+and cofixpoint_expr = identifier * constr_ast * constr_ast
+
+val constr_loc : constr_ast -> loc
+
+val cases_pattern_loc : cases_pattern -> loc
+
+val replace_vars_constr_ast :
+  (identifier * identifier) list -> constr_ast -> constr_ast
+
+val occur_var_constr_ast : identifier -> constr_ast -> bool
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index ddea9997dd..2d7c966ecc 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -79,7 +79,7 @@ sig
   val inTacticAtomAstType : raw_atomic_tactic_expr G.Entry.e -> typed_entry
   val inThmTokenAstType : theorem_kind G.Entry.e -> typed_entry
   val inDynamicAstType : typed_ast G.Entry.e -> typed_entry
-  val inReferenceAstType : reference_expr G.Entry.e -> typed_entry
+  val inReferenceAstType : Coqast.reference_expr G.Entry.e -> typed_entry
   val inPureAstType : constr_ast G.Entry.e -> typed_entry
   val inGenAstType : 'a raw_abstract_argument_type ->
       'a G.Entry.e -> typed_entry
@@ -362,7 +362,6 @@ module Prim =
     let ast_eoi = eoi_entry ast
     let astact = gec "astact"
     let metaident = gec "metaident"
-    let numarg = gec "numarg"
     let var = gec "var"
   end
 
@@ -397,6 +396,7 @@ module Constr =
     let pattern = gec "pattern"
     let constr_pattern = gec "constr_pattern"
     let ne_binders_list = gec_list "ne_binders_list"
+    let numarg = gec "numarg"
   end
 
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 9acf97078e..f6bd506375 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -110,7 +110,7 @@ module Prim :
     val integer : int Gram.Entry.e
     val string : string Gram.Entry.e
     val qualid : qualid located Gram.Entry.e
-    val reference : reference_expr Gram.Entry.e
+    val reference : Coqast.reference_expr Gram.Entry.e
     val dirpath : dir_path Gram.Entry.e
     val astpat: typed_ast Gram.Entry.e
     val ast : Coqast.t Gram.Entry.e
@@ -118,7 +118,6 @@ module Prim :
     val ast_eoi : Coqast.t Gram.Entry.e
     val astact : Coqast.t Gram.Entry.e
     val metaident : Coqast.t Gram.Entry.e
-    val numarg : Coqast.t Gram.Entry.e
     val var : Coqast.t Gram.Entry.e
   end
 
@@ -148,6 +147,7 @@ module Constr :
     val pattern : Coqast.t Gram.Entry.e
     val constr_pattern : Coqast.t Gram.Entry.e
     val ne_binders_list : Coqast.t list Gram.Entry.e
+    val numarg : Coqast.t Gram.Entry.e
   end
 
 module Module : 
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 8fa2326c45..28e51dcd12 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -19,6 +19,7 @@ open Extend
 open Ppconstr
 open Tacexpr
 open Rawterm
+open Coqast
 open Genarg
 
   (* Extensions *)
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 6b7eb89a36..4126250710 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -127,8 +127,8 @@ let mlexpr_of_qualid qid =
   <:expr< make_qualid $mlexpr_of_dirpath dir$ $mlexpr_of_ident id$ >>
 
 let mlexpr_of_reference = function
-  | Tacexpr.RQualid (loc,qid) -> <:expr< Tacexpr.RQualid loc $mlexpr_of_qualid qid$ >>
-  | Tacexpr.RIdent (loc,id) -> <:expr< Tacexpr.RIdent loc $mlexpr_of_ident id$ >>
+  | Coqast.RQualid (loc,qid) -> <:expr< Coqast.RQualid loc $mlexpr_of_qualid qid$ >>
+  | Coqast.RIdent (loc,id) -> <:expr< Coqast.RIdent loc $mlexpr_of_ident id$ >>
 
 let mlexpr_of_bool = function
   | true -> <:expr< True >>
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 2e8d581ae6..eefee41f5f 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -18,10 +18,6 @@ open Genarg
 
 type 'a or_metaid = AI of 'a | MetaId of loc * string
 
-type reference_expr = 
-  | RQualid of qualid located
-  | RIdent of identifier located
-
 type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
 
 type raw_red_flag =