aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-12-26 13:51:24 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-12-26 13:51:24 +0000
commite0f9487be5ce770117a9c9c815af8c7010ff357b (patch)
treebbbde42b0a40803a0c5f5bdb5aaf09248d9aedc0 /parsing
parent98d60ce261e7252379ced07d2934647c77efebfd (diff)
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
-rw-r--r--parsing/argextend.ml447
-rwxr-xr-xparsing/ast.ml590
-rwxr-xr-xparsing/ast.mli121
-rw-r--r--parsing/coqast.ml104
-rw-r--r--parsing/coqast.mli50
-rw-r--r--parsing/egrammar.ml380
-rw-r--r--parsing/egrammar.mli26
-rw-r--r--parsing/esyntax.ml276
-rw-r--r--parsing/esyntax.mli52
-rw-r--r--parsing/extend.ml337
-rw-r--r--parsing/extend.mli113
-rw-r--r--parsing/g_constrnew.ml418
-rw-r--r--parsing/g_ltacnew.ml47
-rw-r--r--parsing/g_natsyntax.ml130
-rw-r--r--parsing/g_prim.ml429
-rw-r--r--parsing/g_primnew.ml482
-rw-r--r--parsing/g_proofsnew.ml45
-rw-r--r--parsing/g_rsyntax.ml217
-rw-r--r--parsing/g_tacticnew.ml448
-rw-r--r--parsing/g_vernacnew.ml434
-rw-r--r--parsing/g_xml.ml43
-rw-r--r--parsing/g_zsyntax.ml176
-rw-r--r--parsing/lexer.ml4162
-rw-r--r--parsing/lexer.mli2
-rw-r--r--parsing/pcoq.ml4242
-rw-r--r--parsing/pcoq.mli52
-rw-r--r--parsing/ppconstr.ml366
-rw-r--r--parsing/ppconstr.mli30
-rw-r--r--parsing/pptactic.ml581
-rw-r--r--parsing/pptactic.mli21
-rw-r--r--parsing/prettyp.ml19
-rw-r--r--parsing/printer.ml178
-rw-r--r--parsing/q_coqast.ml4135
-rw-r--r--parsing/q_util.ml436
-rw-r--r--parsing/q_util.mli1
-rw-r--r--parsing/search.ml1
-rw-r--r--parsing/tacextend.ml493
-rw-r--r--parsing/tactic_printer.ml11
-rw-r--r--parsing/termast.ml551
-rw-r--r--parsing/termast.mli60
-rw-r--r--parsing/vernacextend.ml437
41 files changed, 484 insertions, 4939 deletions
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 66c2d3bf0..331df4c70 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -11,7 +11,6 @@
open Genarg
open Q_util
open Q_coqast
-open Ast
let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
let loc = Util.dummy_loc
@@ -25,12 +24,12 @@ let rec make_rawwit loc = function
| PreIdentArgType -> <:expr< Genarg.rawwit_pre_ident >>
| IntroPatternArgType -> <:expr< Genarg.rawwit_intro_pattern >>
| IdentArgType -> <:expr< Genarg.rawwit_ident >>
- | HypArgType -> <:expr< Genarg.rawwit_var >>
+ | VarArgType -> <:expr< Genarg.rawwit_var >>
| RefArgType -> <:expr< Genarg.rawwit_ref >>
| SortArgType -> <:expr< Genarg.rawwit_sort >>
| ConstrArgType -> <:expr< Genarg.rawwit_constr >>
| ConstrMayEvalArgType -> <:expr< Genarg.rawwit_constr_may_eval >>
- | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >>
+ | QuantVarArgType -> <:expr< Genarg.rawwit_quant_hyp >>
| TacticArgType n -> <:expr< Genarg.rawwit_tactic $mlexpr_of_int n$ >>
| RedExprArgType -> <:expr< Genarg.rawwit_red_expr >>
| OpenConstrArgType b -> <:expr< Genarg.rawwit_open_constr_gen $mlexpr_of_bool b$ >>
@@ -51,9 +50,9 @@ let rec make_globwit loc = function
| PreIdentArgType -> <:expr< Genarg.globwit_pre_ident >>
| IntroPatternArgType -> <:expr< Genarg.globwit_intro_pattern >>
| IdentArgType -> <:expr< Genarg.globwit_ident >>
- | HypArgType -> <:expr< Genarg.globwit_var >>
+ | VarArgType -> <:expr< Genarg.globwit_var >>
| RefArgType -> <:expr< Genarg.globwit_ref >>
- | QuantHypArgType -> <:expr< Genarg.globwit_quant_hyp >>
+ | QuantVarArgType -> <:expr< Genarg.globwit_quant_hyp >>
| SortArgType -> <:expr< Genarg.globwit_sort >>
| ConstrArgType -> <:expr< Genarg.globwit_constr >>
| ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >>
@@ -77,9 +76,9 @@ let rec make_wit loc = function
| PreIdentArgType -> <:expr< Genarg.wit_pre_ident >>
| IntroPatternArgType -> <:expr< Genarg.wit_intro_pattern >>
| IdentArgType -> <:expr< Genarg.wit_ident >>
- | HypArgType -> <:expr< Genarg.wit_var >>
+ | VarArgType -> <:expr< Genarg.wit_var >>
| RefArgType -> <:expr< Genarg.wit_ref >>
- | QuantHypArgType -> <:expr< Genarg.wit_quant_hyp >>
+ | QuantVarArgType -> <:expr< Genarg.wit_quant_hyp >>
| SortArgType -> <:expr< Genarg.wit_sort >>
| ConstrArgType -> <:expr< Genarg.wit_constr >>
| ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >>
@@ -111,7 +110,7 @@ let make_rule loc (prods,act) =
let (symbs,pil) = List.split prods in
<:expr< ($mlexpr_of_list (fun x -> x) symbs$,$make_act loc act pil$) >>
-let declare_tactic_argument for_v8 loc s typ pr f g h rawtyppr globtyppr cl =
+let declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr cl =
let rawtyp, rawpr = match rawtyppr with
| None -> typ,pr
| Some (t,p) -> t,p in
@@ -159,14 +158,13 @@ let declare_tactic_argument for_v8 loc s typ pr f g h rawtyppr globtyppr cl =
Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None
[(None, None, $rules$)];
Pptactic.declare_extra_genarg_pprule
- $mlexpr_of_bool for_v8$
($rawwit$, $lid:rawpr$)
($globwit$, $lid:globpr$)
($wit$, $lid:pr$);
end
>>
-let declare_vernac_argument for_v8 loc s cl =
+let declare_vernac_argument loc s cl =
let se = mlexpr_of_string s in
let rawwit = <:expr< $lid:"rawwit_"^s$ >> in
let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
@@ -235,36 +233,13 @@ EXTEND
"END" ->
if String.capitalize s = s then
failwith "Argument entry names must be lowercase";
- declare_tactic_argument true loc s typ pr f g h rawtyppr globtyppr l
+ declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr l
| "VERNAC"; "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ];
OPT "|"; l = LIST1 argrule SEP "|";
"END" ->
if String.capitalize s = s then
failwith "Argument entry names must be lowercase";
- declare_vernac_argument true loc s l
- | "V7"; "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ];
- "TYPED"; "AS"; typ = argtype;
- "PRINTED"; "BY"; pr = LIDENT;
- f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ];
- g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ];
- h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ];
- rawtyppr =
- OPT [ "GLOB_TYPED"; "AS"; t = argtype;
- "GLOB_PRINTED"; "BY"; pr = LIDENT -> (t,pr) ];
- globtyppr =
- OPT [ "GLOB_TYPED"; "AS"; t = argtype;
- "GLOB_PRINTED"; "BY"; pr = LIDENT -> (t,pr) ];
- OPT "|"; l = LIST1 argrule SEP "|";
- "END" ->
- if String.capitalize s = s then
- failwith "Argument entry names must be lowercase";
- declare_tactic_argument false loc s typ pr f g h rawtyppr globtyppr l
- | "V7"; "VERNAC"; "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ];
- OPT "|"; l = LIST1 argrule SEP "|";
- "END" ->
- if String.capitalize s = s then
- failwith "Argument entry names must be lowercase";
- declare_vernac_argument false loc s l ] ]
+ declare_vernac_argument loc s l ] ]
;
argtype:
[ "2"
@@ -285,7 +260,7 @@ EXTEND
| s = STRING ->
if String.length s > 0 && Util.is_letter s.[0] then
Pcoq.lexer.Token.using ("", s);
- (<:expr< (Gramext.Stoken (Extend.terminal $str:s$)) >>, None)
+ (<:expr< (Gramext.Stoken (Lexer.terminal $str:s$)) >>, None)
] ]
;
END
diff --git a/parsing/ast.ml b/parsing/ast.ml
deleted file mode 100755
index eef1ca4b7..000000000
--- a/parsing/ast.ml
+++ /dev/null
@@ -1,590 +0,0 @@
-(************************************************************************)
-(* 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$ *)
-
-open Pp
-open Util
-open Names
-open Libnames
-open Coqast
-open Topconstr
-open Genarg
-
-let isMeta s = String.length s <> 0 & s.[0]='$'
-
-let loc = function
- | Node (loc,_,_) -> loc
- | Nvar (loc,_) -> loc
- | Nmeta (loc,_) -> loc
- | Slam (loc,_,_) -> loc
- | Smetalam (loc,_,_) -> loc
- | Num (loc,_) -> loc
- | Id (loc,_) -> loc
- | Str (loc,_) -> loc
- | Path (loc,_) -> loc
- | ConPath (loc,_) -> loc
- | Dynamic (loc,_) -> loc
-
-(* patterns of ast *)
-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
-
-and tok_kind = Tnum | Tid | Tstr | Tpath | Tvar | Tany | Tlist
-
-type pat =
- | AstListPat of patlist
- | PureAstPat of astpat
-
-(* building a node with dummy location *)
-
-let ope(op,l) = Node(dummy_loc,op,l)
-let slam(idl,b) = Slam(dummy_loc,idl,b)
-let ide s = Id(dummy_loc,s)
-let nvar s = Nvar(dummy_loc,s)
-let num n = Num(dummy_loc,n)
-let string s = Str(dummy_loc,s)
-let path sl = Path(dummy_loc,sl)
-let conpath sl = ConPath(dummy_loc,sl)
-let dynamic d = Dynamic(dummy_loc,d)
-
-let rec set_loc loc = function
- | Node(_,op,al) -> Node(loc, op, List.map (set_loc loc) al)
- | Slam(_,idl,b) -> Slam(loc,idl, set_loc loc b)
- | Smetalam(_,idl,b) -> Smetalam(loc,idl, set_loc loc b)
- | Nvar(_,s) -> Nvar(loc,s)
- | Nmeta(_,s) -> Nmeta(loc,s)
- | Id(_,s) -> Id(loc,s)
- | Str(_,s) -> Str(loc,s)
- | Num(_,s) -> Num(loc,s)
- | Path(_,sl) -> Path(loc,sl)
- | ConPath(_,sl) -> ConPath(loc,sl)
- | Dynamic(_,d) -> Dynamic(loc,d)
-
-let path_section loc sp = Coqast.Path(loc, sp)
-let conpath_section loc sp = Coqast.ConPath(loc, sp)
-
-(* ast destructors *)
-let num_of_ast = function
- | Num(_,n) -> n
- | ast -> invalid_arg_loc (loc ast, "Ast.num_of_ast")
-
-let nvar_of_ast = function
- | Nvar(_,s) -> s
- | ast -> invalid_arg_loc (loc ast, "Ast.nvar_of_ast")
-
-let meta_of_ast = function
- | Nmeta(_,s) -> s
- | ast -> invalid_arg_loc (loc ast, "Ast.nvar_of_ast")
-
-let id_of_ast = function
- | Id(_,s) -> s
- | ast -> invalid_arg_loc (loc ast, "Ast.nvar_of_ast")
-
-(* semantic actions of grammar rules *)
-type act =
- | Act of constr_expr
- | ActCase of act * (pat * act) list
- | ActCaseList of act * (pat * act) list
-
-(* values associated to variables *)
-(*
-type typed_ast =
- | AstListNode of Coqast.t list
- | PureAstNode of Coqast.t
-*)
-type typed_ast =
- | AstListNode of Coqast.t list
- | PureAstNode of Coqast.t
-
-type ast_action_type = ETast | ETastl
-
-type dynamic_grammar =
- | ConstrNode of constr_expr
- | CasesPatternNode of cases_pattern_expr
-
-type grammar_action =
- | SimpleAction of loc * dynamic_grammar
- | CaseAction of
- loc * grammar_action * ast_action_type * (t list * grammar_action) list
-
-type env = (string * typed_ast) list
-
-let string_of_dirpath = function
- | [] -> "<empty>"
- | sl ->
- String.concat "." (List.map string_of_id (List.rev sl))
-
-let pr_id id = str (string_of_id id)
-
-let print_kn_or_con repr kn =
- let (mp,dp,l) = repr kn in
- let dpl = repr_dirpath dp in
- str (string_of_mp mp) ++ str "." ++
- prlist_with_sep (fun _ -> str".") pr_id dpl ++
- str (string_of_label l)
-
-let print_kn = print_kn_or_con repr_kn
-let print_con = print_kn_or_con repr_con
-
-(* Pretty-printing *)
-let rec print_ast ast =
- match ast with
- | Num(_,n) -> int n
- | Str(_,s) -> qs s
- | Path(_,sl) -> print_kn sl
- | ConPath(_,sl) -> print_con sl
- | Id (_,s) -> str "{" ++ str s ++ str "}"
- | Nvar(_,s) -> pr_id s
- | Nmeta(_,s) -> str s
- | Node(_,op,l) ->
- hov 3 (str "(" ++ str op ++ spc () ++ print_astl l ++ str ")")
- | Slam(_,None,ast) -> hov 1 (str "[<>]" ++ print_ast ast)
- | Slam(_,Some x,ast) ->
- hov 1
- (str "[" ++ pr_id x ++ str "]" ++ cut () ++
- print_ast ast)
- | Smetalam(_,id,ast) -> hov 1 (str id ++ print_ast ast)
- | Dynamic(_,d) ->
- hov 0 (str "<dynamic: " ++ str (Dyn.tag d) ++ str ">")
-
-and print_astl astl =
- prlist_with_sep pr_spc print_ast astl
-
-let print_ast_cast = function
- | Tany -> (mt ())
- | Tvar -> (str":var")
- | Tid -> (str":id")
- | Tstr -> (str":str")
- | Tpath -> (str":path")
- | Tnum -> (str":num")
- | Tlist -> (str":list")
-
-let rec print_astpat = function
- | Pquote ast ->
- str"'" ++ print_ast ast
- | Pmeta(s,tk) ->
- str s ++ print_ast_cast tk
- | Pmeta_slam(s,b) ->
- hov 1 (str "[" ++ str s ++ str"]" ++ cut () ++ print_astpat b)
- | Pnode(op,al) ->
- hov 2 (str"(" ++ str op ++ spc () ++ print_astlpat al ++ str")" )
- | Pslam(None,b) ->
- hov 1 (str"[<" ++ cut () ++ print_astpat b)
- | Pslam(Some id,b) ->
- hov 1
- (str"[" ++ str(string_of_id id) ++ str"]" ++ cut () ++ print_astpat b)
-
-and print_astlpat = function
- | Pnil -> mt ()
- | Pcons(h,Pnil) -> hov 1 (print_astpat h)
- | Pcons(h,t) -> hov 1 (print_astpat h ++ spc () ++ print_astlpat t)
- | Plmeta(s) -> str"| " ++ str s
-
-
-let print_val = function
- | PureAstNode a -> print_ast a
- | AstListNode al ->
- hov 1 (str"[" ++ prlist_with_sep pr_spc print_ast al ++ str"]")
-
-(* Ast values environments *)
-
-let grammar_type_error (loc,s) =
- anomaly_loc (loc,s,(str"grammar type error: " ++ str s))
-
-
-(* Coercions enforced by the user *)
-let check_cast loc a k =
- match (k,a) with
- | (Tany, _) -> ()
- | (Tid, Id _) -> ()
- | (Tvar, Nvar _) -> ()
- | (Tpath, Path _) -> ()
- | (Tpath, ConPath _) -> ()
- | (Tstr, Str _) -> ()
- | (Tnum, Num _) -> ()
- | (Tlist, _) -> grammar_type_error (loc,"Ast.cast_val")
- | _ -> user_err_loc (loc,"Ast.cast_val",
- (str"cast _" ++ print_ast_cast k ++ str"failed"))
-
-let rec coerce_to_var = function
- | Nvar(_,id) as var -> var
- | Nmeta(_,id) as var -> var
- | Node(_,"QUALID",[Nvar(_,id) as var]) -> var
- | ast -> user_err_loc
- (loc ast,"Ast.coerce_to_var",
- (str"This expression should be a simple identifier"))
-
-let coerce_to_id_ast a = match coerce_to_var a with
- | Nvar (_,id) -> id
- | ast -> user_err_loc
- (loc ast,"Ast.coerce_to_id",
- str"This expression should be a simple identifier")
-
-let coerce_to_id = function
- | CRef (Ident (loc,id)) -> (loc,id)
- | a -> user_err_loc
- (constr_loc a,"Ast.coerce_to_id",
- str"This expression should be a simple identifier")
-
-let coerce_reference_to_id = function
- | Ident (_,id) -> id
- | Qualid (loc,_) ->
- user_err_loc (loc, "Ast.coerce_reference_to_id",
- str"This expression should be a simple identifier")
-
-let coerce_global_to_id = coerce_reference_to_id
-
-(* Pattern-matching on ast *)
-
-let env_assoc_value loc v env =
- try
- List.assoc v env
- with Not_found ->
- anomaly_loc
- (loc,"Ast.env_assoc_value",
- (str"metavariable " ++ str v ++ str" is unbound"))
-
-let env_assoc_list sigma (loc,v) =
- match env_assoc_value loc v sigma with
- | AstListNode al -> al
- | PureAstNode a -> [a]
-
-let env_assoc sigma k (loc,v) =
- match env_assoc_value loc v sigma with
- | PureAstNode a -> check_cast loc a k; a
- | _ -> grammar_type_error (loc,"Ast.env_assoc: "^v^" is an ast list")
-
-let env_assoc_nvars sigma (dloc,v) =
- match env_assoc_value dloc v sigma with
- | AstListNode al -> List.map coerce_to_id_ast al
- | PureAstNode ast -> [coerce_to_id_ast ast]
-
-let build_lams dloc idl ast =
- List.fold_right (fun id lam -> Slam(dloc,Some id,lam)) idl ast
-
-(* Alpha-conversion *)
-
-let rec alpha_var id1 id2 = function
- | (i1,i2)::_ when i1=id1 -> i2 = id2
- | (i1,i2)::_ when i2=id2 -> i1 = id1
- | _::idl -> alpha_var id1 id2 idl
- | [] -> id1 = id2
-
-let rec alpha alp a1 a2 =
- match (a1,a2) with
- | (Node(_,op1,tl1),Node(_,op2,tl2)) ->
- (op1 = op2) & (List.length tl1 = List.length tl2)
- & (List.for_all2 (alpha alp) tl1 tl2)
- | (Nvar(_,id1),Nvar(_,id2)) -> alpha_var id1 id2 alp
- | (Slam(_,None,body1),Slam(_,None,body2)) -> alpha alp body1 body2
- | (Slam(_,Some s1,body1),Slam(_,Some s2,body2)) ->
- alpha ((s1,s2)::alp) body1 body2
- | (Id(_,s1),Id(_,s2)) -> s1=s2
- | (Str(_,s1),Str(_,s2)) -> s1=s2
- | (Num(_,n1),Num(_,n2)) -> n1=n2
- | (Path(_,sl1),Path(_,sl2)) -> sl1=sl2
- | (ConPath(_,sl1),ConPath(_,sl2)) -> sl1=sl2
- | ((Smetalam _ | Nmeta _ | Dynamic _), _) -> false
- | (_, (Smetalam _ | Nmeta _ | Dynamic _)) -> false
- | _ -> false
-
-let alpha_eq (a1,a2)= alpha [] a1 a2
-
-let alpha_eq_val (x,y) = x = y
-(*
-let alpha_eq_val = function
- | (Vast a1, Vast a2) -> alpha_eq (a1,a2)
- | (Vastlist al1, Vastlist al2) ->
- (List.length al1 = List.length al2)
- & List.for_all2 (fun x y -> alpha_eq (x,y)) al1 al2
- | _ -> false
-*)
-
-exception No_match of string
-
-let no_match_loc (loc,s) = Stdpp.raise_with_loc loc (No_match s)
-
-(* Binds value v to variable var. If var is already bound, checks if
- its value is alpha convertible with v. This allows non-linear patterns.
-
- Important note: The Metavariable $_ is a special case; it cannot be
- bound, which is like _ in the ML matching. *)
-
-let bind_env sigma var v =
- if var = "$_" then
- sigma
- else
- try
- let vvar = List.assoc var sigma in
- if alpha_eq_val (v,vvar) then sigma
- else raise (No_match "Ast.bind_env: values do not match")
- with Not_found ->
- (var,v)::sigma
-
-let bind_env_ast sigma var ast =
- try
- bind_env sigma var (PureAstNode ast)
- with e ->
- Stdpp.raise_with_loc (loc ast) e
-
-let alpha_define sigma loc ps s =
- try
- let _ = List.assoc ps sigma in sigma
- with Not_found ->
- if ps = "$_" then sigma else (ps, PureAstNode(Nvar(loc,s)))::sigma
-
-
-(* Match an ast with an ast pattern. Returns the new environnement. *)
-
-let rec amatch alp sigma spat ast =
- match (spat,ast) with
- | (Pquote a, _) ->
- if alpha alp a ast then
- sigma
- else
- no_match_loc (loc ast,"quote does not match")
- | (Pmeta(pv,Tany), _) -> bind_env_ast sigma pv ast
- | (Pmeta(pv,Tvar), Nvar _) -> bind_env_ast sigma pv ast
- | (Pmeta(pv,Tid), Id _) -> bind_env_ast sigma pv ast
- | (Pmeta(pv,Tnum), Num _) -> bind_env_ast sigma pv ast
- | (Pmeta(pv,Tstr), Str _) -> bind_env_ast sigma pv ast
- | (Pmeta(pv,Tpath), Path _) -> bind_env_ast sigma pv ast
- | (Pmeta(pv,Tpath), ConPath _) -> bind_env_ast sigma pv ast
- | (Pmeta(pv,Tlist),_) -> grammar_type_error (loc ast,"Ast.amatch")
- | (Pmeta_slam(pv,pb), Slam(loc, Some s, b)) ->
- amatch alp (bind_env_ast sigma pv (Nvar(loc,s))) pb b
- | (Pmeta_slam(pv,pb), Slam(loc, None, b)) ->
- amatch alp (bind_env_ast sigma pv (Nvar(loc,id_of_string "_"))) pb b
- | (Pmeta_slam(pv,pb), Smetalam(loc, s, b)) ->
- anomaly "amatch: match a pattern with an open ast"
- | (Pnode(nodp,argp), Node(loc,op,args)) when nodp = op ->
- (try amatchl alp sigma argp args
- with e -> Stdpp.raise_with_loc loc e)
- | (Pslam(None,bp), Slam(_,None,b)) -> amatch alp sigma bp b
- | (Pslam(Some ps,bp), Slam(_,Some s,b)) -> amatch ((ps,s)::alp) sigma bp b
- | _ -> no_match_loc (loc ast, "Ast.amatch")
-
-and amatchl alp sigma spatl astl =
- match (spatl,astl) with
- | (Pnil, []) -> sigma
- | (Pcons(pat,patl), ast::asttl) ->
- amatchl alp (amatch alp sigma pat ast) patl asttl
- | (Plmeta pv, _) -> bind_env sigma pv (AstListNode astl)
- | _ -> raise (No_match "Ast.amatchl")
-
-let ast_match = amatch []
-
-let typed_ast_match env p a = match (p,a) with
- | PureAstPat p, PureAstNode a -> amatch [] env p a
- | AstListPat pl, AstListNode al -> amatchl [] env pl al
- | _ -> failwith "Ast.typed_ast_match: TODO"
-
-let astl_match = amatchl []
-
-let first_match pat_of_fun env ast sl =
- let rec aux = function
- | [] -> None
- | h::t ->
- (try Some (h, ast_match env (pat_of_fun h) ast)
- with (No_match _| Stdpp.Exc_located (_,No_match _)) -> aux t)
- in
- aux sl
-
-let find_all_matches pat_of_fun env ast sl =
- let rec aux = function
- | [] -> []
- | (h::t) ->
- let l = aux t in
- (try (h, ast_match env (pat_of_fun h) ast)::l
- with (No_match _| Stdpp.Exc_located (_,No_match _)) -> l)
- in
- aux sl
-
-let first_matchl patl_of_fun env astl sl =
- let rec aux = function
- | [] -> None
- | (h::t) ->
- (try Some (h, astl_match env (patl_of_fun h) astl)
- with (No_match _| Stdpp.Exc_located (_,No_match _)) -> aux t)
- in
- aux sl
-
-let bind_patvar env loc v etyp =
- try
- if List.assoc v env = etyp then
- env
- else
- user_err_loc
- (loc,"Ast.bind_patvar",
- (str"variable " ++ str v ++
- str" is bound several times with different types"))
- with Not_found ->
- if v="$_" then env else (v,etyp)::env
-
-let make_astvar env loc v cast =
- let env' = bind_patvar env loc v ETast in
- (Pmeta(v,cast), env')
-
-(* Note: no metavar in operator position. necessary ? *)
-let rec pat_of_ast env ast =
- match ast with
- | Nmeta(loc,pv) -> make_astvar env loc pv Tany
-(* Obsolète
- | Id(loc,pv) when isMeta pv -> make_astvar env loc pv Tid
-*)
- | Smetalam(loc,s,a) ->
- let senv = bind_patvar env loc s ETast in
- let (pa,env') = pat_of_ast senv a in
- (Pmeta_slam(s, pa), env')
- | Node(_,"$VAR",[Nmeta(loc,pv)]) ->
- make_astvar env loc pv Tvar
- | Node(_,"$ID",[Nmeta(loc,pv)]) ->
- make_astvar env loc pv Tid
- | Node(_,"$NUM",[Nmeta(loc,pv)]) ->
- make_astvar env loc pv Tnum
- | Node(_,"$STR",[Nmeta(loc,pv)]) ->
- make_astvar env loc pv Tstr
- | Node(_,"$PATH",[Nmeta(loc,pv)]) ->
- make_astvar env loc pv Tpath
- | Node(_,"$QUOTE",[qast]) -> (Pquote (set_loc dummy_loc qast), env)
-
- (* This may occur when the meta is not textual but bound by coerce_to_id*)
- | Slam(loc,Some id,b) when isMeta (string_of_id id) ->
- let s = string_of_id id in
- let senv = bind_patvar env loc s ETast in
- let (pb,env') = pat_of_ast senv b in
- (Pmeta_slam(s, pb), env')
-
- | Slam(_,os,b) ->
- let (pb,env') = pat_of_ast env b in
- (Pslam(os,pb), env')
- | Node(loc,op,_) when isMeta op ->
- user_err_loc(loc,"Ast.pat_of_ast",
- (str"no patvar in operator position."))
- | Node(_,op,args) ->
- let (pargs, env') = patl_of_astl env args in
- (Pnode(op,pargs), env')
-(* Compatibility with new parsing mode *)
- | Nvar(loc,id) when (string_of_id id).[0] = '$' -> make_astvar env loc (string_of_id id) Tany
- | (Path _|ConPath _|Num _|Id _|Str _ |Nvar _) -> (Pquote (set_loc dummy_loc ast), env)
- | Dynamic(loc,_) ->
- invalid_arg_loc(loc,"pat_of_ast: dynamic")
-
-and patl_of_astl env astl =
- match astl with
- | [Node(_,"$LIST",[Nmeta(loc,pv)])] ->
- let penv = bind_patvar env loc pv ETastl in
- (Plmeta pv, penv)
- | [] -> (Pnil,env)
- | ast::asttl ->
- let (p1,env1) = pat_of_ast env ast in
- let (ptl,env2) = patl_of_astl env1 asttl in
- (Pcons (p1,ptl), env2)
-
-type entry_env = (string * ast_action_type) list
-
-let to_pat = pat_of_ast
-
-(* Substitution *)
-
-(* Locations in quoted ast are wrong (they refer to the right hand
- side of a grammar rule). A default location dloc is used whenever
- we create an ast constructor. Locations in the binding list are trusted. *)
-
-(* For old ast printer *)
-let rec pat_sub dloc sigma pat =
- match pat with
- | Pmeta(pv,c) -> env_assoc sigma c (dloc,pv)
- | Pmeta_slam(pv,p) ->
- let idl = env_assoc_nvars sigma (dloc,pv) in
- build_lams dloc idl (pat_sub dloc sigma p)
- | Pquote a -> set_loc dloc a
- | Pnode(op,pl) -> Node(dloc, op, patl_sub dloc sigma pl)
- | Pslam(os,p) -> Slam(dloc, os, pat_sub dloc sigma p)
-
-and patl_sub dloc sigma pl =
- match pl with
- | Pnil ->
- []
- | Plmeta pv ->
- env_assoc_list sigma (dloc,pv)
- | Pcons(Pmeta(pv,Tlist), ptl) ->
- (env_assoc_list sigma (dloc,pv))@(patl_sub dloc sigma ptl)
- | Pcons(p1,ptl) ->
- (pat_sub dloc sigma p1)::(patl_sub dloc sigma ptl)
-
-(* Converting and checking free meta-variables *)
-
-(* For old ast printer *)
-let type_of_meta env loc pv =
- try
- List.assoc pv env
- with Not_found ->
- user_err_loc (loc,"Ast.type_of_meta",
- (str"variable " ++ str pv ++ str" is unbound"))
-
-(* For old ast printer *)
-let check_ast_meta env loc pv =
- match type_of_meta env loc pv with
- | ETast -> ()
- | _ ->
- user_err_loc (loc,"Ast.check_ast_meta",
- (str"variable " ++ str pv ++ str" is not of ast type"))
-
-(* For old ast printer *)
-let rec val_of_ast env = function
- | Nmeta(loc,pv) ->
- check_ast_meta env loc pv;
- Pmeta(pv,Tany)
- | Node(_,"$QUOTE",[qast]) -> Pquote (set_loc dummy_loc qast)
- | Smetalam(loc,s,a) ->
- let _ = type_of_meta env loc s in (* ids are coerced to id lists *)
- Pmeta_slam(s, val_of_ast env a)
- | (Path _|ConPath _|Num _|Id _|Str _|Nvar _ as ast) -> Pquote (set_loc dummy_loc ast)
- | Slam(_,os,b) -> Pslam(os, val_of_ast env b)
- | Node(loc,op,_) when isMeta op ->
- user_err_loc(loc,"Ast.val_of_ast",
- (str"no patvar in operator position."))
- | Node(_,op,args) -> Pnode(op, vall_of_astl env args)
- | Dynamic(loc,_) ->
- invalid_arg_loc(loc,"val_of_ast: dynamic")
-
-and vall_of_astl env = function
- | (Node(loc,"$LIST",[Nmeta(locv,pv)]))::asttl ->
- if type_of_meta env locv pv = ETastl then
- if asttl = [] then
- Plmeta pv
- else
- Pcons(Pmeta(pv,Tlist), vall_of_astl env asttl)
- else
- user_err_loc
- (loc,"Ast.vall_of_astl",
- str"variable " ++ str pv ++ str" is not a List")
- | ast::asttl -> Pcons (val_of_ast env ast, vall_of_astl env asttl)
- | [] -> Pnil
-
-(* For old ast printer *)
-let rec occur_var_ast s = function
- | Node(_,"QUALID",_::_::_) -> false
- | Node(_,"QUALID",[Nvar(_,s2)]) -> s = s2
- | Nvar(_,s2) -> s = s2
- | Node(loc,op,args) -> List.exists (occur_var_ast s) args
- | Smetalam _ | Nmeta _ -> anomaly "occur_var: metas should not occur here"
- | Slam(_,sopt,body) -> (Some s <> sopt) & occur_var_ast s body
- | Id _ | Str _ | Num _ | Path _ | ConPath _ -> false
- | Dynamic _ -> (* Hum... what to do here *) false
diff --git a/parsing/ast.mli b/parsing/ast.mli
deleted file mode 100755
index 9c7eec43c..000000000
--- a/parsing/ast.mli
+++ /dev/null
@@ -1,121 +0,0 @@
-(************************************************************************)
-(* 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 *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-(*i*)
-open Pp
-open Util
-open Names
-open Libnames
-open Coqast
-open Topconstr
-open Genarg
-open Mod_subst
-(*i*)
-
-(* Abstract syntax trees. *)
-
-val loc : Coqast.t -> loc
-
-(* ast constructors with dummy location *)
-val ope : string * Coqast.t list -> Coqast.t
-val slam : identifier option * Coqast.t -> Coqast.t
-val nvar : identifier -> Coqast.t
-val ide : string -> Coqast.t
-val num : int -> Coqast.t
-val string : string -> Coqast.t
-val path : kernel_name -> Coqast.t
-val dynamic : Dyn.t -> Coqast.t
-
-val set_loc : loc -> Coqast.t -> Coqast.t
-
-val path_section : loc -> kernel_name -> Coqast.t
-val conpath_section : loc -> constant -> Coqast.t
-
-(* ast destructors *)
-val num_of_ast : Coqast.t -> int
-val id_of_ast : Coqast.t -> string
-val nvar_of_ast : Coqast.t -> identifier
-val meta_of_ast : Coqast.t -> string
-
-(* patterns of ast *)
-type astpat =
- | Pquote of Coqast.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
-
-and tok_kind = Tnum | Tid | Tstr | Tpath | Tvar | Tany | Tlist
-
-type pat =
- | AstListPat of patlist
- | PureAstPat of astpat
-
-(* semantic actions of grammar rules *)
-type act =
- | Act of constr_expr
- | ActCase of act * (pat * act) list
- | ActCaseList of act * (pat * act) list
-
-(* values associated to variables *)
-type typed_ast =
- | AstListNode of Coqast.t list
- | PureAstNode of Coqast.t
-
-type ast_action_type = ETast | ETastl
-
-type dynamic_grammar =
- | ConstrNode of constr_expr
- | CasesPatternNode of cases_pattern_expr
-
-type grammar_action =
- | SimpleAction of loc * dynamic_grammar
- | CaseAction of
- loc * grammar_action * ast_action_type * (t list * grammar_action) list
-
-type env = (string * typed_ast) list
-
-val coerce_to_id : constr_expr -> identifier located
-
-val coerce_global_to_id : reference -> identifier
-val coerce_reference_to_id : reference -> identifier
-
-exception No_match of string
-
-val isMeta : string -> bool
-
-val print_ast : Coqast.t -> std_ppcmds
-val print_astl : Coqast.t list -> std_ppcmds
-val print_astpat : astpat -> std_ppcmds
-val print_astlpat : patlist -> std_ppcmds
-
-(* Meta-syntax operations: matching and substitution *)
-
-type entry_env = (string * ast_action_type) list
-
-val grammar_type_error : loc * string -> 'a
-
-(* Converting and checking free meta-variables *)
-
-(* For old ast printer *)
-val pat_sub : loc -> env -> astpat -> Coqast.t
-val val_of_ast : entry_env -> Coqast.t -> astpat
-val alpha_eq : Coqast.t * Coqast.t -> bool
-val alpha_eq_val : typed_ast * typed_ast -> bool
-val occur_var_ast : identifier -> Coqast.t -> bool
-val find_all_matches : ('a -> astpat) -> env -> t -> 'a list -> ('a * env) list
-val first_matchl : ('a -> patlist) -> env -> Coqast.t list -> 'a list ->
- ('a * env) option
-val to_pat : entry_env -> Coqast.t -> (astpat * entry_env)
diff --git a/parsing/coqast.ml b/parsing/coqast.ml
deleted file mode 100644
index 3811dd322..000000000
--- a/parsing/coqast.ml
+++ /dev/null
@@ -1,104 +0,0 @@
-(************************************************************************)
-(* 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$ *)
-
-(*i*)
-open Util
-open Names
-open Libnames
-open Mod_subst
-(*i*)
-
-type t =
- | Node of loc * string * t list
- | Nmeta of loc * string
- | Nvar of loc * identifier
- | Slam of loc * identifier option * t
- | Smetalam of loc * string * t
- | Num of loc * int
- | Str of loc * string
- | Id of loc * string
- | Path of loc * kernel_name
- | ConPath of loc * constant
- | Dynamic of loc * Dyn.t
-
-type the_coq_ast = t
-
-let subst_meta bl ast =
- let rec aux = function
- | Node (_,"META", [Num(_, n)]) -> List.assoc n bl
- | Node(loc, node_name, args) ->
- Node(loc, node_name, List.map aux args)
- | Slam(loc, var, arg) -> Slam(loc, var, aux arg)
- | Smetalam(loc, var, arg) -> Smetalam(loc, var, aux arg)
- | other -> other
- in
- aux ast
-
-let rec collect_metas = function
- | Node (_,"META", [Num(_, n)]) -> [n]
- | Node(_, _, args) -> List.concat (List.map collect_metas args)
- | Slam(loc, var, arg) -> collect_metas arg
- | Smetalam(loc, var, arg) -> collect_metas arg
- | _ -> []
-
-(* Hash-consing *)
-module Hloc = Hashcons.Make(
- struct
- type t = loc
- type u = unit
- let equal (b1,e1) (b2,e2) = b1=b2 & e1=e2
- let hash_sub () x = x
- let hash = Hashtbl.hash
- end)
-
-module Hast = Hashcons.Make(
- struct
- type t = the_coq_ast
- type u =
- (the_coq_ast -> the_coq_ast) *
- ((loc -> loc) * (string -> string)
- * (identifier -> identifier) * (kernel_name -> kernel_name)
- * (constant -> constant))
- let hash_sub (hast,(hloc,hstr,hid,hsp,hcon)) = function
- | Node(l,s,al) -> Node(hloc l, hstr s, List.map hast al)
- | Nmeta(l,s) -> Nmeta(hloc l, hstr s)
- | Nvar(l,s) -> Nvar(hloc l, hid s)
- | Slam(l,None,t) -> Slam(hloc l, None, hast t)
- | Slam(l,Some s,t) -> Slam(hloc l, Some (hid s), hast t)
- | Smetalam(l,s,t) -> Smetalam(hloc l, hstr s, hast t)
- | Num(l,n) -> Num(hloc l, n)
- | Id(l,s) -> Id(hloc l, hstr s)
- | Str(l,s) -> Str(hloc l, hstr s)
- | Path(l,d) -> Path(hloc l, hsp d)
- | ConPath(l,d) -> ConPath(hloc l, hcon d)
- | Dynamic(l,d) -> Dynamic(hloc l, d)
- let equal a1 a2 =
- match (a1,a2) with
- | (Node(l1,s1,al1), Node(l2,s2,al2)) ->
- (l1==l2 & s1==s2 & List.length al1 = List.length al2)
- & List.for_all2 (==) al1 al2
- | (Nmeta(l1,s1), Nmeta(l2,s2)) -> l1==l2 & s1==s2
- | (Nvar(l1,s1), Nvar(l2,s2)) -> l1==l2 & s1==s2
- | (Slam(l1,None,t1), Slam(l2,None,t2)) -> l1==l2 & t1==t2
- | (Slam(l1,Some s1,t1), Slam(l2,Some s2,t2)) ->l1==l2 & s1==s2 & t1==t2
- | (Smetalam(l1,s1,t1), Smetalam(l2,s2,t2)) -> l1==l2 & s1==s2 & t1==t2
- | (Num(l1,n1), Num(l2,n2)) -> l1==l2 & n1=n2
- | (Id(l1,s1), Id(l2,s2)) -> l1==l2 & s1==s2
- | (Str(l1,s1),Str(l2,s2)) -> l1==l2 & s1==s2
- | (Path(l1,d1), Path(l2,d2)) -> (l1==l2 & d1==d2)
- | (ConPath(l1,d1), ConPath(l2,d2)) -> (l1==l2 & d1==d2)
- | _ -> false
- let hash = Hashtbl.hash
- end)
-
-let hcons_ast (hstr,hid,hpath,hconpath) =
- let hloc = Hashcons.simple_hcons Hloc.f () in
- let hast = Hashcons.recursive_hcons Hast.f (hloc,hstr,hid,hpath,hconpath) in
- (hast,hloc)
diff --git a/parsing/coqast.mli b/parsing/coqast.mli
deleted file mode 100644
index a083d09a6..000000000
--- a/parsing/coqast.mli
+++ /dev/null
@@ -1,50 +0,0 @@
-(************************************************************************)
-(* 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 *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-(*i*)
-open Util
-open Names
-open Libnames
-(*i*)
-
-(* Abstract syntax trees. *)
-
-type t =
- | Node of loc * string * t list
- | Nmeta of loc * string
- | Nvar of loc * identifier
- | Slam of loc * identifier option * t
- | Smetalam of loc * string * t
- | Num of loc * int
- | Str of loc * string
- | Id of loc * string
- | Path of loc * kernel_name
- | ConPath of loc * constant
- | Dynamic of loc * Dyn.t
-
-(* returns the list of metas occuring in the ast *)
-val collect_metas : t -> int list
-
-(* [subst_meta bl ast]: for each binding [(i,c_i)] in [bl],
- replace the metavar [?i] by [c_i] in [ast] *)
-val subst_meta : (int * t) list -> t -> t
-
-(* hash-consing function *)
-val hcons_ast:
- (string -> string) * (Names.identifier -> Names.identifier)
- * (kernel_name -> kernel_name) * (constant -> constant)
- -> (t -> t) * (loc -> loc)
-
-(*i
-val map_tactic_expr : (t -> t) -> (tactic_expr -> tactic_expr) -> tactic_expr -> tactic_expr
-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
-i*)
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index be8b1e8ad..37dc007ee 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -10,52 +10,27 @@
open Pp
open Util
-open Extend
open Pcoq
+open Extend
open Topconstr
-open Ast
open Genarg
open Libnames
open Nameops
-
-(* State of the grammar extensions *)
-
-type notation_grammar =
- int * Gramext.g_assoc option * notation * prod_item list
-
-type all_grammar_command =
- | Notation of Notation.level * notation_grammar
- | Grammar of grammar_command
- | TacticGrammar of
- (string * int * grammar_production list *
- (Names.dir_path * Tacexpr.glob_tactic_expr))
-
-let (grammar_state : all_grammar_command list ref) = ref []
-
+open Tacexpr
+open Names
+open Vernacexpr
(**************************************************************************)
-(* Interpretation of the right hand side of grammar rules *)
-
-(* When reporting errors, we add the name of the grammar rule that failed *)
-let specify_name name e =
- match e with
- | UserError(lab,strm) ->
- UserError(lab, (str"during interpretation of grammar rule " ++
- str name ++ str"," ++ spc () ++ strm))
- | Anomaly(lab,strm) ->
- Anomaly(lab, (str"during interpretation of grammar rule " ++
- str name ++ str"," ++ spc () ++ strm))
- | Failure s ->
- Failure("during interpretation of grammar rule "^name^", "^s)
- | e -> e
-
-(* Translation of environments: a production
+(*
+ * --- Note on the mapping of grammar productions to camlp4 actions ---
+ *
+ * Translation of environments: a production
* [ nt1(x1) ... nti(xi) ] -> act(x1..xi)
* is written (with camlp4 conventions):
* (fun vi -> .... (fun v1 -> act(v1 .. vi) )..)
* where v1..vi are the values generated by non-terminals nt1..nti.
* Since the actions are executed by substituting an environment,
- * make_act builds the following closure:
+ * the make_*_action family build the following closure:
*
* ((fun env ->
* (fun vi ->
@@ -69,11 +44,18 @@ let specify_name name e =
* [])
*)
-open Names
+(**********************************************************************)
+(** Declare Notations grammar rules *)
+
+type prod_item =
+ | Term of Token.pattern
+ | NonTerm of constr_production_entry *
+ (Names.identifier * constr_production_entry) option
type 'a action_env = (identifier * 'a) list
-let make_act (f : loc -> constr_expr action_env -> constr_expr) pil =
+let make_constr_action
+ (f : loc -> constr_expr action_env -> constr_expr) pil =
let rec make (env : constr_expr action_env) = function
| [] ->
Gramext.action (fun loc -> f loc env)
@@ -97,7 +79,7 @@ let make_act (f : loc -> constr_expr action_env -> constr_expr) pil =
failwith "Unexpected entry of type cases pattern" in
make [] (List.rev pil)
-let make_act_in_cases_pattern (* For Notations *)
+let make_cases_pattern_action
(f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil =
let rec make (env : cases_pattern_expr action_env) = function
| [] ->
@@ -123,238 +105,92 @@ let make_act_in_cases_pattern (* For Notations *)
failwith "Unexpected entry of type cases pattern or other" in
make [] (List.rev pil)
-(* For V7 Grammar only *)
-let make_cases_pattern_act
- (f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil =
- let rec make (env : cases_pattern_expr action_env) = function
- | [] ->
- Gramext.action (fun loc -> f loc env)
- | None :: tl -> (* parse a non-binding item *)
- Gramext.action (fun _ -> make env tl)
- | Some (p, ETPattern) :: tl -> (* non-terminal *)
- Gramext.action (fun v -> make ((p,v) :: env) tl)
- | Some (p, ETReference) :: tl -> (* non-terminal *)
- Gramext.action (fun v -> make ((p,CPatAtom(dummy_loc,Some v)) :: env)
- tl)
- | Some (p, ETBigint) :: tl -> (* non-terminal *)
- Gramext.action (fun v -> make ((p,CPatNumeral(dummy_loc,v)) :: env) tl)
- | Some (p, (ETConstrList _ | ETIdent | ETConstr _ | ETOther _)) :: tl ->
- error "ident and constr entry not admitted in patterns cases syntax extensions" in
- make [] (List.rev pil)
-
-(* Grammar extension command. Rules are assumed correct.
- * Type-checking of grammar rules is done during the translation of
- * ast to the type grammar_command. We only check that the existing
- * entries have the type assumed in the grammar command (these types
- * annotations are added when type-checking the command, function
- * Extend.of_ast) *)
-
-let symbol_of_prod_item univ assoc from forpat = function
+let make_constr_prod_item univ assoc from forpat = function
| Term tok -> (Gramext.Stoken tok, None)
| NonTerm (nt, ovar) ->
let eobj = symbol_of_production assoc from forpat nt in
(eobj, ovar)
-let coerce_to_id = function
- | CRef (Ident (_,id)) -> id
- | c ->
- user_err_loc (constr_loc c, "subst_rawconstr",
- str"This expression should be a simple identifier")
-
-let coerce_to_ref = function
- | CRef r -> r
- | c ->
- user_err_loc (constr_loc c, "subst_rawconstr",
- str"This expression should be a simple reference")
-
-let subst_ref loc subst id =
- try coerce_to_ref (List.assoc id subst) with Not_found -> Ident (loc,id)
-
-let subst_pat_id loc subst id =
- try List.assoc id subst
- with Not_found -> CPatAtom (loc,Some (Ident (loc,id)))
-
-let subst_id subst id =
- try coerce_to_id (List.assoc id subst) with Not_found -> id
-
-(*
-let subst_cases_pattern_expr a loc subs =
- let rec subst = function
- | CPatAlias (_,p,x) -> CPatAlias (loc,subst p,x)
- (* No subst in compound pattern ? *)
- | CPatCstr (_,ref,pl) -> CPatCstr (loc,ref,List.map subst pl)
- | CPatAtom (_,Some (Ident (_,id))) -> subst_pat_id loc subs id
- | CPatAtom (_,x) -> CPatAtom (loc,x)
- | CPatNotation (_,ntn,l) -> CPatNotation
- | CPatNumeral (_,n) -> CPatNumeral (loc,n)
- | CPatDelimiters (_,key,p) -> CPatDelimiters (loc,key,subst p)
- in subst a
-*)
-
-let subst_constr_expr a loc subs =
- let rec subst = function
- | CRef (Ident (_,id)) ->
- (try List.assoc id subs with Not_found -> CRef (Ident (loc,id)))
- (* Temporary: no robust treatment of substituted binders *)
- | CLambdaN (_,[],c) -> subst c
- | CLambdaN (_,([],t)::bl,c) -> subst (CLambdaN (loc,bl,c))
- | CLambdaN (_,((_,na)::bl,t)::bll,c) ->
- let na = name_app (subst_id subs) na in
- CLambdaN (loc,[[loc,na],subst t], subst (CLambdaN (loc,(bl,t)::bll,c)))
- | CProdN (_,[],c) -> subst c
- | CProdN (_,([],t)::bl,c) -> subst (CProdN (loc,bl,c))
- | CProdN (_,((_,na)::bl,t)::bll,c) ->
- let na = name_app (subst_id subs) na in
- CProdN (loc,[[loc,na],subst t], subst (CProdN (loc,(bl,t)::bll,c)))
- | CLetIn (_,(_,na),b,c) ->
- let na = name_app (subst_id subs) na in
- CLetIn (loc,(loc,na),subst b,subst c)
- | CArrow (_,a,b) -> CArrow (loc,subst a,subst b)
- | CAppExpl (_,(p,Ident (_,id)),l) ->
- CAppExpl (loc,(p,subst_ref loc subs id),List.map subst l)
- | CAppExpl (_,r,l) -> CAppExpl (loc,r,List.map subst l)
- | CApp (_,(p,a),l) ->
- CApp (loc,(p,subst a),List.map (fun (a,i) -> (subst a,i)) l)
- | CCast (_,a,k,b) -> CCast (loc,subst a,k,subst b)
- | CNotation (_,n,l) -> CNotation (loc,n,List.map subst l)
- | CDelimiters (_,s,a) -> CDelimiters (loc,s,subst a)
- | CHole _ | CEvar _ | CPatVar _ | CSort _
- | CNumeral _ | CDynamic _ | CRef _ as x -> x
- | CCases (_,(po,rtntypo),a,bl) ->
- (* TODO: apply g on the binding variables in pat... *)
- let bl = List.map (fun (_,pat,rhs) -> (loc,pat,subst rhs)) bl in
- CCases (loc,(option_app subst po,option_app subst rtntypo),
- List.map (fun (tm,x) -> subst tm,x) a,bl)
- | COrderedCase (_,s,po,a,bl) ->
- COrderedCase (loc,s,option_app subst po,subst a,List.map subst bl)
- | CLetTuple (_,nal,(na,po),a,b) ->
- let na = option_app (name_app (subst_id subs)) na in
- let nal = List.map (name_app (subst_id subs)) nal in
- CLetTuple (loc,nal,(na,option_app subst po),subst a,subst b)
- | CIf (_,c,(na,po),b1,b2) ->
- let na = option_app (name_app (subst_id subs)) na in
- CIf (loc,subst c,(na,option_app subst po),subst b1,subst b2)
- | CFix (_,id,dl) ->
- CFix (loc,id,List.map (fun (id,n,bl, t,d) ->
- (id,n,
- List.map(function
- LocalRawAssum(nal,ty) -> LocalRawAssum(nal,subst ty)
- | LocalRawDef(na,def) -> LocalRawDef(na,subst def)) bl,
- subst t,subst d)) dl)
- | CCoFix (_,id,dl) ->
- CCoFix (loc,id,List.map (fun (id,bl,t,d) ->
- (id,
- List.map(function
- LocalRawAssum(nal,ty) -> LocalRawAssum(nal,subst ty)
- | LocalRawDef(na,def) -> LocalRawDef(na,subst def)) bl,
- subst t,subst d)) dl)
- in subst a
-
-(* For V7 Grammar only *)
-let make_rule_v7 univ assoc etyp rule =
- if not !Options.v7 then anomaly "No Grammar in new syntax";
- let pil = List.map (symbol_of_prod_item univ assoc etyp false) rule.gr_production in
- let (symbs,ntl) = List.split pil in
- let act = match etyp with
- | ETPattern ->
- (* Ugly *)
- let f loc env = match rule.gr_action, env with
- | CRef (Ident(_,p)), [p',a] when p=p' -> a
- | CDelimiters (_,s,CRef (Ident(_,p))), [p',a] when p=p' ->
- CPatDelimiters (loc,s,a)
- | _ -> error "Unable to handle this grammar extension of pattern" in
- make_cases_pattern_act f ntl
- | ETConstrList _ | ETIdent | ETBigint | ETReference -> error "Cannot extend"
- | ETConstr _ | ETOther _ ->
- make_act (subst_constr_expr rule.gr_action) ntl in
- (symbs, act)
-
-(* Rules of a level are entered in reverse order, so that the first rules
- are applied before the last ones *)
-(* For V7 Grammar only *)
-let extend_entry univ (te, etyp, pos, name, ass, p4ass, rls) =
- let rules = List.rev (List.map (make_rule_v7 univ ass etyp) rls) in
- grammar_extend te pos [(name, p4ass, rules)]
-
-(* Defines new entries. If the entry already exists, check its type *)
-let define_entry univ {ge_name=typ; gl_assoc=ass; gl_rules=rls} =
- let e,lev,keepassoc = get_constr_entry false typ in
- let pos,p4ass,name = find_position false keepassoc ass lev in
- (e,typ,pos,name,ass,p4ass,rls)
-
-(* Add a bunch of grammar rules. Does not check if it is well formed *)
-(* For V7 Grammar only *)
-let extend_grammar_rules gram =
- let univ = get_univ gram.gc_univ in
- let tl = List.map (define_entry univ) gram.gc_entries in
- List.iter (extend_entry univ) tl
-
-(* Add a grammar rules for tactics *)
-type grammar_tactic_production =
- | TacTerm of string
- | TacNonTerm of loc * (Gram.te Gramext.g_symbol * argument_type) * string option
-
-let make_prod_item = function
- | TacTerm s -> (Gramext.Stoken (Extend.terminal s), None)
- | TacNonTerm (_,(nont,t), po) ->
- (nont, option_app (fun p -> (p,t)) po)
-
-let make_gen_act f pil =
- let rec make env = function
- | [] ->
- Gramext.action (fun loc -> f loc env)
- | None :: tl -> (* parse a non-binding item *)
- Gramext.action (fun _ -> make env tl)
- | Some (p, t) :: tl -> (* non-terminal *)
- Gramext.action (fun v -> make ((p,in_generic t v) :: env) tl) in
- make [] (List.rev pil)
-
-let extend_constr entry (n,assoc,pos,p4assoc,name) make_act (forpat,pt) =
+let extend_constr entry (n,assoc,pos,p4assoc,name) mkact (forpat,pt) =
let univ = get_univ "constr" in
- let pil = List.map (symbol_of_prod_item univ assoc n forpat) pt in
+ let pil = List.map (make_constr_prod_item univ assoc n forpat) pt in
let (symbs,ntl) = List.split pil in
- let act = make_act ntl in
- grammar_extend entry pos [(name, p4assoc, [symbs, act])]
+ grammar_extend entry pos [(name, p4assoc, [symbs, mkact ntl])]
let extend_constr_notation (n,assoc,ntn,rule) =
+ (* Add the notation in constr *)
let mkact loc env = CNotation (loc,ntn,List.map snd env) in
let (e,level,keepassoc) = get_constr_entry false (ETConstr (n,())) in
let pos,p4assoc,name = find_position false keepassoc assoc level in
extend_constr e (ETConstr(n,()),assoc,pos,p4assoc,name)
- (make_act mkact) (false,rule);
- if not !Options.v7 then
+ (make_constr_action mkact) (false,rule);
+ (* Add the notation in cases_pattern *)
let mkact loc env = CPatNotation (loc,ntn,List.map snd env) in
let (e,level,keepassoc) = get_constr_entry true (ETConstr (n,())) in
let pos,p4assoc,name = find_position true keepassoc assoc level in
extend_constr e (ETConstr (n,()),assoc,pos,p4assoc,name)
- (make_act_in_cases_pattern mkact) (true,rule)
+ (make_cases_pattern_action mkact) (true,rule)
+
+(**********************************************************************)
+(** Making generic actions in type generic_argument *)
+
+let make_generic_action
+ (f:loc -> ('b * raw_generic_argument) list -> 'a) pil =
+ let rec make env = function
+ | [] ->
+ Gramext.action (fun loc -> f loc env)
+ | None :: tl -> (* parse a non-binding item *)
+ Gramext.action (fun _ -> make env tl)
+ | Some (p, t) :: tl -> (* non-terminal *)
+ Gramext.action (fun v -> make ((p,in_generic t v) :: env) tl) in
+ make [] (List.rev pil)
-(* These grammars are not a removable *)
let make_rule univ f g pt =
let (symbs,ntl) = List.split (List.map g pt) in
- let act = make_gen_act f ntl in
+ let act = make_generic_action f ntl in
(symbs, act)
+(**********************************************************************)
+(** Grammar extensions declared at ML level *)
+
+type grammar_tactic_production =
+ | TacTerm of string
+ | TacNonTerm of
+ loc * (Gram.te Gramext.g_symbol * argument_type) * string option
+
+let make_prod_item = function
+ | TacTerm s -> (Gramext.Stoken (Lexer.terminal s), None)
+ | TacNonTerm (_,(nont,t), po) -> (nont, option_app (fun p -> (p,t)) po)
+
+(* Tactic grammar extensions *)
+
let tac_exts = ref []
let get_extend_tactic_grammars () = !tac_exts
let extend_tactic_grammar s gl =
tac_exts := (s,gl) :: !tac_exts;
let univ = get_univ "tactic" in
- let make_act loc l = Tacexpr.TacExtend (loc,s,List.map snd l) in
- let rules = List.map (make_rule univ make_act make_prod_item) gl in
+ let mkact loc l = Tacexpr.TacExtend (loc,s,List.map snd l) in
+ let rules = List.map (make_rule univ mkact make_prod_item) gl in
Gram.extend Tactic.simple_tactic None [(None, None, List.rev rules)]
+(* Vernac grammar extensions *)
+
let vernac_exts = ref []
let get_extend_vernac_grammars () = !vernac_exts
let extend_vernac_command_grammar s gl =
vernac_exts := (s,gl) :: !vernac_exts;
let univ = get_univ "vernac" in
- let make_act loc l = Vernacexpr.VernacExtend (s,List.map snd l) in
- let rules = List.map (make_rule univ make_act make_prod_item) gl in
+ let mkact loc l = VernacExtend (s,List.map snd l) in
+ let rules = List.map (make_rule univ mkact make_prod_item) gl in
Gram.extend Vernac_.command None [(None, None, List.rev rules)]
+(**********************************************************************)
+(** Grammar declaration for Tactic Notation (Coq level) *)
+
+(* Interpretation of the grammar entry names *)
+
let find_index s t =
let t,n = repr_ident (id_of_string t) in
if s <> t or n = None then raise Not_found;
@@ -374,23 +210,12 @@ let rec interp_entry_name up_level u s =
else
try
let i = find_index "tactic" s in
- if !Options.v7 then
- let e = match i with
- | 2 -> Tactic.tactic_expr2
- | 3 -> Tactic.tactic_expr3
- | 4 -> Tactic.tactic_expr4
- | 5 -> Tactic.tactic_expr5
- | _ -> error ("Unknown entry "^s)
- in TacticArgType i, Gramext.Snterm (Pcoq.Gram.Entry.obj e)
- else
- TacticArgType i,
- if i=up_level then Gramext.Sself else
- if i=up_level-1 then Gramext.Snext else
- Gramext.Snterml(Pcoq.Gram.Entry.obj Tactic.tactic_expr,string_of_int i)
+ TacticArgType i,
+ if i=up_level then Gramext.Sself else
+ if i=up_level-1 then Gramext.Snext else
+ Gramext.Snterml(Pcoq.Gram.Entry.obj Tactic.tactic_expr,string_of_int i)
with Not_found ->
let e =
- if !Options.v7 then get_entry (get_univ u) s
- else
(* Qualified entries are no longer in use *)
try get_entry (get_univ "tactic") s
with _ ->
@@ -403,59 +228,60 @@ let rec interp_entry_name up_level u s =
let t = type_of_typed_entry e in
t,Gramext.Snterm (Pcoq.Gram.Entry.obj o)
-let qualified_nterm current_univ = function
- | NtQual (univ, en) -> if !Options.v7 then (univ, en) else assert false
- | NtShort en -> (current_univ, en)
-
let make_vprod_item n univ = function
- | VTerm s -> (Gramext.Stoken (Extend.terminal s), None)
+ | VTerm s -> (Gramext.Stoken (Lexer.terminal s), None)
| VNonTerm (loc, nt, po) ->
- let (u,nt) = qualified_nterm univ nt in
- let (etyp, e) = interp_entry_name n u nt in
+ let (etyp, e) = interp_entry_name n univ nt in
e, option_app (fun p -> (p,etyp)) po
let get_tactic_entry n =
- if n = 0 then weaken_entry Tactic.simple_tactic, None
- else if !Options.v7 then
- let e = match n with
- | 2 -> Tactic.tactic_expr2
- | 3 -> Tactic.tactic_expr3
- | 4 -> Tactic.tactic_expr4
- | 5 -> Tactic.tactic_expr5
- | _ -> error ("Invalid v7 Tactic Notation level: "^(string_of_int n)) in
- weaken_entry e, None
- else
- if 1<=n && n<=5 then
- weaken_entry Tactic.tactic_expr, Some (Gramext.Level (string_of_int n))
- else
- error ("Invalid Tactic Notation level: "^(string_of_int n))
+ if n = 0 then
+ weaken_entry Tactic.simple_tactic, None
+ else if 1<=n && n<=5 then
+ weaken_entry Tactic.tactic_expr, Some (Gramext.Level (string_of_int n))
+ else
+ error ("Invalid Tactic Notation level: "^(string_of_int n))
-open Tacexpr
+(* Declaration of the tactic grammar rule *)
let head_is_ident = function VTerm _::_ -> true | _ -> false
let add_tactic_entry (key,lev,prods,tac) =
let univ = get_univ "tactic" in
let entry, pos = get_tactic_entry lev in
+ let mkprod = make_vprod_item lev "tactic" in
let rules =
if lev = 0 then begin
if not (head_is_ident prods) then
error "Notation for simple tactic must start with an identifier";
- let make_act s tac loc l =
+ let mkact s tac loc l =
(TacAlias(loc,s,l,tac):raw_atomic_tactic_expr) in
- make_rule univ (make_act key tac) (make_vprod_item lev "tactic") prods
+ make_rule univ (mkact key tac) mkprod prods
end
else
- let make_act s tac loc l =
+ let mkact s tac loc l =
(TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in
- make_rule univ (make_act key tac) (make_vprod_item lev "tactic") prods in
+ make_rule univ (mkact key tac) mkprod prods in
let _ = find_position true true None None (* to synchronise with remove *) in
grammar_extend entry pos [(None, None, List.rev [rules])]
+(**********************************************************************)
+(** State of the grammar extensions *)
+
+type notation_grammar =
+ int * Gramext.g_assoc option * notation * prod_item list
+
+type all_grammar_command =
+ | Notation of Notation.level * notation_grammar
+ | TacticGrammar of
+ (string * int * grammar_production list *
+ (Names.dir_path * Tacexpr.glob_tactic_expr))
+
+let (grammar_state : all_grammar_command list ref) = ref []
+
let extend_grammar gram =
(match gram with
| Notation (_,a) -> extend_constr_notation a
- | Grammar g -> extend_grammar_rules g
| TacticGrammar g -> add_tactic_entry g);
grammar_state := gram :: !grammar_state
@@ -464,7 +290,7 @@ let reset_extend_grammars_v8 () =
let tv = List.rev !vernac_exts in
tac_exts := [];
vernac_exts := [];
- List.iter (fun (s,gl) -> extend_tactic_grammar s gl) te;
+ List.iter (fun (s,gl) -> print_string ("Resinstalling "^s); flush stdout; extend_tactic_grammar s gl) te;
List.iter (fun (s,gl) -> extend_vernac_command_grammar s gl) tv
let recover_notation_grammar ntn prec =
@@ -489,11 +315,7 @@ let factorize_grams l1 l2 =
let number_of_entries gcl =
List.fold_left
(fun n -> function
- | Notation _ ->
- if !Options.v7 then n + 1
- else n + 2 (* 1 for operconstr, 1 for pattern *)
- | Grammar gc ->
- n + (List.length gc.gc_entries)
+ | Notation _ -> n + 2 (* 1 for operconstr, 1 for pattern *)
| TacticGrammar _ -> n + 1)
0 gcl
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 06ab2b42f..92efd0824 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -11,21 +11,29 @@
(*i*)
open Util
open Topconstr
-open Ast
-open Coqast
+open Pcoq
+open Extend
open Vernacexpr
open Ppextend
-open Extend
open Rawterm
open Mod_subst
(*i*)
+(** Mapping of grammar productions to camlp4 actions
+ Used for Coq-level Notation and Tactic Notation,
+ and for ML-level tactic and vernac extensions
+ *)
+
+type prod_item =
+ | Term of Token.pattern
+ | NonTerm of constr_production_entry *
+ (Names.identifier * constr_production_entry) option
+
type notation_grammar =
int * Gramext.g_assoc option * notation * prod_item list
type all_grammar_command =
| Notation of (precedence * tolerability list) * notation_grammar
- | Grammar of grammar_command
| TacticGrammar of
(string * int * grammar_production list *
(Names.dir_path * Tacexpr.glob_tactic_expr))
@@ -33,22 +41,26 @@ type all_grammar_command =
val extend_grammar : all_grammar_command -> unit
(* Add grammar rules for tactics *)
+
type grammar_tactic_production =
| TacTerm of string
- | TacNonTerm of loc * (Token.t Gramext.g_symbol * Genarg.argument_type) * string option
+ | TacNonTerm of
+ loc * (Token.t Gramext.g_symbol * Genarg.argument_type) * string option
val extend_tactic_grammar :
string -> grammar_tactic_production list list -> unit
val extend_vernac_command_grammar :
string -> grammar_tactic_production list list -> unit
-
+(*
val get_extend_tactic_grammars :
unit -> (string * grammar_tactic_production list list) list
+*)
val get_extend_vernac_grammars :
unit -> (string * grammar_tactic_production list list) list
+(*
val reset_extend_grammars_v8 : unit -> unit
-
+*)
val interp_entry_name : int -> string -> string ->
entry_type * Token.t Gramext.g_symbol
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml
deleted file mode 100644
index 1ee900dbc..000000000
--- a/parsing/esyntax.ml
+++ /dev/null
@@ -1,276 +0,0 @@
-(************************************************************************)
-(* 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$ *)
-
-open Pp
-open Util
-open Names
-open Libnames
-open Coqast
-open Ast
-open Extend
-open Ppextend
-open Names
-open Nametab
-open Topconstr
-open Notation
-
-(*** Syntax keys ***)
-
-(* We define keys for ast and astpats. This is a kind of hash
- * function. An ast may have several keys, but astpat only one. The
- * idea is that if an ast A matches a pattern P, then the key of P
- * is in the set of keys of A. Thus, we can split the syntax entries
- * according to the key of the pattern. *)
-
-type key =
- | Cst of Names.constant (* keys for global constants rules *)
- | SecVar of Names.variable
- | Ind of Names.inductive
- | Cstr of Names.constructor
- | Nod of string (* keys for other constructed asts rules *)
- | Oth (* key for other syntax rules *)
- | All (* key for catch-all rules (i.e. with a pattern such as $x .. *)
-
-let warning_verbose = ref true
-
-let ast_keys = function
- | Node(_,"APPLIST", Node(_,"CONST", [ConPath (_,sl)]) ::_) ->
- [Cst sl; Nod "APPLIST"; All]
- | Node(_,"APPLIST", Node(_,"SECVAR", [Nvar (_,s)]) ::_) ->
- [SecVar s; Nod "APPLIST"; All]
- | Node(_,"APPLIST", Node(_,"MUTIND", [Path (_,sl); Num (_,tyi)]) ::_) ->
- [Ind (sl,tyi); Nod "APPLIST"; All]
- | Node(_,"APPLIST", Node(_,"MUTCONSTRUCT",
- [Path (_,sl); Num (_,tyi); Num (_,i)]) ::_) ->
- [Cstr ((sl,tyi),i); Nod "APPLIST"; All]
- | Node(_,s,_) -> [Nod s; All]
- | _ -> [Oth; All]
-
-let spat_key astp =
- match astp with
- | Pnode("APPLIST",
- Pcons(Pnode("CONST",
- Pcons(Pquote(ConPath (_,sl)),_)), _))
- -> Cst sl
- | Pnode("APPLIST",
- Pcons(Pnode("SECVAR",
- Pcons(Pquote(Nvar (_,s)),_)), _))
- -> SecVar s
- | Pnode("APPLIST",
- Pcons(Pnode("MUTIND",
- Pcons(Pquote(Path (_,sl)),
- Pcons(Pquote(Num (_,tyi)),_))), _))
- -> Ind (sl,tyi)
- | Pnode("APPLIST",
- Pcons(Pnode("MUTCONSTRUCT",
- Pcons(Pquote(Path (_,sl)),
- Pcons(Pquote(Num (_,tyi)),
- Pcons(Pquote(Num (_,i)),_)))), _))
- -> Cstr ((sl,tyi),i)
- | Pnode(na,_) -> Nod na
- | Pquote ast -> List.hd (ast_keys ast)
- | Pmeta _ -> All
- | _ -> Oth
-
-let se_key se = spat_key se.syn_astpat
-
-(** Syntax entry tables (state of the pretty_printer) **)
-let from_name_table = ref Gmap.empty
-let from_key_table = ref Gmapl.empty
-
-(* Summary operations *)
-type frozen_t = (string * string, astpat syntax_entry) Gmap.t *
- (string * key, astpat syntax_entry) Gmapl.t
-
-let freeze () =
- (!from_name_table, !from_key_table)
-
-let unfreeze (fnm,fkm) =
- from_name_table := fnm;
- from_key_table := fkm
-
-let init () =
- from_name_table := Gmap.empty;
- from_key_table := Gmapl.empty
-
-let find_syntax_entry whatfor gt =
- let gt_keys = ast_keys gt in
- let entries =
- List.flatten
- (List.map (fun k -> Gmapl.find (whatfor,k) !from_key_table) gt_keys)
- in
- find_all_matches (fun se -> se.syn_astpat) [] gt entries
-
-let remove_with_warning name =
- if Gmap.mem name !from_name_table then begin
- let se = Gmap.find name !from_name_table in
- let key = (fst name, se_key se) in
- if !warning_verbose then
- (Options.if_verbose
- warning ("overriding syntax rule "^(fst name)^":"^(snd name)^"."));
- from_name_table := Gmap.remove name !from_name_table;
- from_key_table := Gmapl.remove key se !from_key_table
- end
-
-let add_rule whatfor se =
- let name = (whatfor,se.syn_id) in
- let key = (whatfor, se_key se) in
- remove_with_warning name;
- from_name_table := Gmap.add name se !from_name_table;
- from_key_table := Gmapl.add key se !from_key_table
-
-let add_ppobject {sc_univ=wf;sc_entries=sel} = List.iter (add_rule wf) sel
-
-
-(* Pretty-printing machinery *)
-
-type std_printer = Coqast.t -> std_ppcmds
-type unparsing_subfunction = string -> tolerability option -> std_printer
-type primitive_printer = Coqast.t -> std_ppcmds option
-
-(* Module of primitive printers *)
-module Ppprim =
- struct
- type t = std_printer -> std_printer
- let tab = ref ([] : (string * t) list)
- let map a = List.assoc a !tab
- let add (a,ppr) = tab := (a,ppr)::!tab
- end
-
-(**********************************************************************)
-(* Primitive printers (e.g. for numerals) *)
-
-(* This is the map associating to a printer the scope it belongs to *)
-(* and its ML code *)
-
-let primitive_printer_tab =
- ref (Stringmap.empty : (scope_name * primitive_printer) Stringmap.t)
-let declare_primitive_printer s sc pp =
- primitive_printer_tab := Stringmap.add s (sc,pp) !primitive_printer_tab
-let lookup_primitive_printer s =
- Stringmap.find s !primitive_printer_tab
-
-(* Register the primitive printer for "token". It is not used in syntax/PP*.v,
- * but any ast matching no PP rule is printed with it. *)
-(*
-let _ = declare_primitive_printer "token" token_printer
-*)
-
-(* A printer for the tokens. *)
-let token_printer stdpr = function
- | (Id _ | Num _ | Str _ | Path _ | ConPath _ as ast) -> print_ast ast
- | a -> stdpr a
-
-(* Unused ??
-(* A primitive printer to do "print as" (to specify a length for a string) *)
-let print_as_printer = function
- | Node (_, "AS", [Num(_,n); Str(_,s)]) -> Some (stras (n,s))
- | ast -> None
-
-let _ = declare_primitive_printer "print_as" default_scope print_as_printer
-*)
-
-(* Handle infix symbols *)
-
-let pr_parenthesis inherited se strm =
- if tolerable_prec inherited se.syn_prec then
- strm
- else
- (str"(" ++ strm ++ str")")
-
-let print_delimiters inh se strm = function
- | None -> pr_parenthesis inh se strm
- | Some key ->
- let left = "'"^key^":" and right = "'" in
- let lspace =
- if is_letter (left.[String.length left -1]) then str " " else mt () in
- let rspace =
- let c = right.[0] in
- if is_ident_tail c then str " " else mt () in
- hov 0 (str left ++ lspace ++ strm ++ rspace ++ str right)
-
-(* Print the syntax entry. In the unparsing hunks, the tokens are
- * printed using the token_printer, unless another primitive printer
- * is specified. *)
-
-let print_syntax_entry sub_pr scopes env se =
- let rec print_hunk rule_prec scopes = function
- | PH(e,externpr,reln) ->
- let node = Ast.pat_sub dummy_loc env e in
- let printer =
- match externpr with (* May branch to an other printer *)
- | Some c ->
- (try (* Test for a primitive printer *) Ppprim.map c
- with Not_found -> token_printer)
- | _ -> token_printer in
- printer (sub_pr scopes (Some(rule_prec,reln))) node
- | RO s -> str s
- | UNP_TAB -> tab ()
- | UNP_FNL -> fnl ()
- | UNP_BRK(n1,n2) -> brk(n1,n2)
- | UNP_TBRK(n1,n2) -> tbrk(n1,n2)
- | UNP_BOX (b,sub) -> ppcmd_of_box b (prlist (print_hunk rule_prec scopes) sub)
- | UNP_SYMBOLIC _ -> anomaly "handled by call_primitive_parser"
- in
- prlist (print_hunk se.syn_prec scopes) se.syn_hunks
-
-let call_primitive_parser rec_pr otherwise inherited scopes (se,env) =
- try (
- match se.syn_hunks with
- | [PH(e,Some c,reln)] ->
- (* Test for a primitive printer; may raise Not_found *)
- let sc,pr = lookup_primitive_printer c in
- (* Look if scope [sc] associated to this printer is OK *)
- (match Notation.availability_of_numeral sc scopes with
- | None -> otherwise ()
- | Some key ->
- (* We can use this printer *)
- let node = Ast.pat_sub dummy_loc env e in
- match pr node with
- | Some strm -> print_delimiters inherited se strm key
- | None -> otherwise ())
- | [UNP_SYMBOLIC (sc,pat,sub)] ->
- (match Notation.availability_of_notation (sc,pat) scopes with
- | None -> otherwise ()
- | Some (scopt,key) ->
- print_delimiters inherited se
- (print_syntax_entry rec_pr
- (option_fold_right Notation.push_scope scopt scopes) env
- {se with syn_hunks = [sub]}) key)
- | _ ->
- pr_parenthesis inherited se (print_syntax_entry rec_pr scopes env se)
- )
- with Not_found -> (* To handle old style printer *)
- pr_parenthesis inherited se (print_syntax_entry rec_pr scopes env se)
-
-(* [genprint whatfor dflt inhprec ast] prints out the ast of
- * 'universe' whatfor. If the term is not matched by any
- * pretty-printing rule, then it will call dflt on it, which is
- * responsible for printing out the term (usually #GENTERM...).
- * In the case of tactics and commands, dflt also prints
- * global constants basenames. *)
-
-let genprint dflt whatfor inhprec ast =
- let rec rec_pr scopes inherited gt =
- let entries = find_syntax_entry whatfor gt in
- let rec test_rule = function
- | se_env::rules ->
- call_primitive_parser
- rec_pr
- (fun () -> test_rule rules)
- inherited scopes se_env
- | [] -> dflt gt (* No rule found *)
- in test_rule entries
- in
- try
- rec_pr (Notation.current_scopes ()) inhprec ast
- with
- | Failure _ -> (str"<PP failure: " ++ dflt ast ++ str">")
- | Not_found -> (str"<PP search failure: " ++ dflt ast ++ str">")
diff --git a/parsing/esyntax.mli b/parsing/esyntax.mli
deleted file mode 100644
index 0344a27e2..000000000
--- a/parsing/esyntax.mli
+++ /dev/null
@@ -1,52 +0,0 @@
-(************************************************************************)
-(* 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 *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-(*i*)
-open Pp
-open Extend
-open Notation
-open Ppextend
-open Topconstr
-(*i*)
-
-(* Syntax entry tables. *)
-
-type frozen_t
-
-(* pretty-printer summary operations *)
-val init : unit -> unit
-val freeze : unit -> frozen_t
-val unfreeze : frozen_t -> unit
-
-(* Search and add a PP rule for an ast in the summary *)
-val find_syntax_entry :
- string -> Coqast.t -> (Ast.astpat syntax_entry * Ast.env) list
-val add_rule : string -> Ast.astpat syntax_entry -> unit
-val add_ppobject : Ast.astpat syntax_command -> unit
-val warning_verbose : bool ref
-
-(* Pretty-printing *)
-
-type std_printer = Coqast.t -> std_ppcmds
-type unparsing_subfunction = string -> tolerability option -> std_printer
-type primitive_printer = Coqast.t -> std_ppcmds option
-
-(* Module of constr primitive printers [old style - no scope] *)
-module Ppprim :
- sig
- type t = std_printer -> std_printer
- val add : string * t -> unit
- end
-
-val declare_primitive_printer :
- string -> scope_name -> primitive_printer -> unit
-
-(* Generic printing functions *)
-val genprint : std_printer -> unparsing_subfunction
diff --git a/parsing/extend.ml b/parsing/extend.ml
index d6587e1ec..fbea84e7b 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -13,12 +13,12 @@ open Util
open Pp
open Gramext
open Names
-open Ast
open Ppextend
open Topconstr
open Genarg
-type entry_type = argument_type
+(**********************************************************************)
+(* constr entry keys *)
type production_position =
| BorderProd of bool * Gramext.g_assoc option (* true=left; false=right *)
@@ -37,54 +37,13 @@ type ('lev,'pos) constr_entry_key =
type constr_production_entry =
(production_level,production_position) constr_entry_key
-type constr_entry = (int,unit) constr_entry_key
-type simple_constr_production_entry = (production_level,unit) constr_entry_key
-
-type nonterm_prod =
- | ProdList0 of nonterm_prod
- | ProdList1 of nonterm_prod * Token.pattern list
- | ProdOpt of nonterm_prod
- | ProdPrimitive of constr_production_entry
-
-type prod_item =
- | Term of Token.pattern
- | NonTerm of constr_production_entry *
- (Names.identifier * constr_production_entry) option
-
-type grammar_rule = {
- gr_name : string;
- gr_production : prod_item list;
- gr_action : constr_expr }
-
-type grammar_entry = {
- ge_name : constr_entry;
- gl_assoc : Gramext.g_assoc option;
- gl_rules : grammar_rule list }
-
-type grammar_command = {
- gc_univ : string;
- gc_entries : grammar_entry list }
-
-type grammar_associativity = Gramext.g_assoc option
+type constr_entry =
+ (int,unit) constr_entry_key
+type simple_constr_production_entry =
+ (production_level,unit) constr_entry_key
(**********************************************************************)
-(* Globalisation and type-checking of Grammar actions *)
-
-type entry_context = identifier list
-
-open Rawterm
-open Libnames
-
-let globalizer = ref (fun _ _ -> CHole dummy_loc)
-let set_constr_globalizer f = globalizer := f
-
-let act_of_ast vars = function
- | SimpleAction (loc,ConstrNode a) -> !globalizer vars a
- | SimpleAction (loc,CasesPatternNode a) ->
- failwith "TODO:act_of_ast: cases_pattern"
- | CaseAction _ -> failwith "case/let not supported"
-
-let to_act_check_vars = act_of_ast
+(* syntax modifiers *)
type syntax_modifier =
| SetItemLevel of string list * production_level
@@ -94,285 +53,3 @@ type syntax_modifier =
| SetOnlyParsing
| SetFormat of string located
-type nonterm =
- | NtShort of string
- | NtQual of string * string
-type grammar_production =
- | VTerm of string
- | VNonTerm of loc * nonterm * Names.identifier option
-type raw_grammar_rule = string * grammar_production list * grammar_action
-type raw_grammar_entry = string * grammar_associativity * raw_grammar_rule list
-
-(* No kernel names in Grammar's *)
-let subst_constr_expr _ a = a
-
-let subst_grammar_rule subst gr =
- { gr with gr_action = subst_constr_expr subst gr.gr_action }
-
-let subst_grammar_entry subst ge =
- { ge with gl_rules = List.map (subst_grammar_rule subst) ge.gl_rules }
-
-let subst_grammar_command subst gc =
- { gc with gc_entries = List.map (subst_grammar_entry subst) gc.gc_entries }
-
-
-(*s Terminal symbols interpretation *)
-
-let is_ident_not_keyword s =
- match s.[0] with
- | 'a'..'z' | 'A'..'Z' | '_' -> not (Lexer.is_keyword s)
- | _ -> false
-
-let is_number s =
- match s.[0] with
- | '0'..'9' -> true
- | _ -> false
-
-let strip s =
- let len =
- let rec loop i len =
- if i = String.length s then len
- else if s.[i] == ' ' then loop (i + 1) len
- else loop (i + 1) (len + 1)
- in
- loop 0 0
- in
- if len == String.length s then s
- else
- let s' = String.create len in
- let rec loop i i' =
- if i == String.length s then s'
- else if s.[i] == ' ' then loop (i + 1) i'
- else begin s'.[i'] <- s.[i]; loop (i + 1) (i' + 1) end
- in
- loop 0 0
-
-let terminal s =
- let s = strip s in
- if s = "" then failwith "empty token";
- if is_ident_not_keyword s then ("IDENT", s)
- else if is_number s then ("INT", s)
- else ("", s)
-
-(*s Non-terminal symbols interpretation *)
-
-(* For compatibility *)
-let warn nt nt' =
- warning ("'"^nt^"' grammar entry is obsolete; use name '"^nt'^"' instead");
- nt'
-
-let rename_command_entry nt =
- if String.length nt >= 7 & String.sub nt 0 7 = "command"
- then warn nt ("constr"^(String.sub nt 7 (String.length nt - 7)))
- else if nt = "lcommand" then warn nt "lconstr"
- else if nt = "lassoc_command4" then warn nt "lassoc_constr4"
- else nt
-
-(* This translates constr0, constr1, ... level into camlp4 levels of constr *)
-
-let explicitize_prod_entry inj pos univ nt =
- if univ = "prim" & nt = "var" then ETIdent else
- if univ = "prim" & nt = "bigint" then ETBigint else
- if univ <> "constr" then ETOther (univ,nt) else
- match nt with
- | "constr0" -> ETConstr (inj 0,pos)
- | "constr1" -> ETConstr (inj 1,pos)
- | "constr2" -> ETConstr (inj 2,pos)
- | "constr3" -> ETConstr (inj 3,pos)
- | "lassoc_constr4" -> ETConstr (inj 4,pos)
- | "constr5" -> ETConstr (inj 5,pos)
- | "constr6" -> ETConstr (inj 6,pos)
- | "constr7" -> ETConstr (inj 7,pos)
- | "constr8" -> ETConstr (inj 8,pos)
- | "constr" when !Options.v7 -> ETConstr (inj 8,pos)
- | "constr9" -> ETConstr (inj 9,pos)
- | "constr10" | "lconstr" -> ETConstr (inj 10,pos)
- | "pattern" -> ETPattern
- | "ident" -> ETIdent
- | "global" -> ETReference
- | _ -> ETOther (univ,nt)
-
-let explicitize_entry = explicitize_prod_entry (fun x -> x) ()
-
-(* Express border sub entries in function of the from level and an assoc *)
-(* We're cheating: not necessarily the same assoc on right and left *)
-let clever_explicitize_prod_entry pos univ from en =
- let t = explicitize_prod_entry (fun x -> NumLevel x) pos univ en in
- match from with
- | ETConstr (from,()) ->
- (match t with
- | ETConstr (n,BorderProd (left,None))
- when (n=NumLevel from & left) ->
- ETConstr (n,BorderProd (left,Some Gramext.LeftA))
- | ETConstr (NumLevel n,BorderProd (left,None))
- when (n=from-1 & not left) ->
- ETConstr
- (NumLevel (n+1),BorderProd (left,Some Gramext.LeftA))
- | ETConstr (NumLevel n,BorderProd (left,None))
- when (n=from-1 & left) ->
- ETConstr
- (NumLevel (n+1),BorderProd (left,Some Gramext.RightA))
- | ETConstr (n,BorderProd (left,None))
- when (n=NumLevel from & not left) ->
- ETConstr (n,BorderProd (left,Some Gramext.RightA))
- | t -> t)
- | _ -> t
-
-let qualified_nterm current_univ pos from = function
- | NtQual (univ, en) ->
- clever_explicitize_prod_entry pos univ from en
- | NtShort en ->
- clever_explicitize_prod_entry pos current_univ from en
-
-let check_entry check_entry_type = function
- | ETOther (u,n) -> check_entry_type (u,n)
- | _ -> ()
-
-let nterm loc (((check_entry_type,univ),from),pos) nont =
- let typ = qualified_nterm univ pos from nont in
- check_entry check_entry_type typ;
- typ
-
-let prod_item univ env = function
- | VTerm s -> env, Term (terminal s)
- | VNonTerm (loc, nt, Some p) ->
- let typ = nterm loc univ nt in
- (p :: env, NonTerm (typ, Some (p,typ)))
- | VNonTerm (loc, nt, None) ->
- let typ = nterm loc univ nt in
- env, NonTerm (typ, None)
-
-let rec prod_item_list univ penv pil current_pos =
- match pil with
- | [] -> [], penv
- | pi :: pitl ->
- let pos = if pitl=[] then (BorderProd (false,None)) else current_pos in
- let (env, pic) = prod_item (univ,pos) penv pi in
- let (pictl, act_env) = prod_item_list univ env pitl InternalProd in
- (pic :: pictl, act_env)
-
-let gram_rule univ (name,pil,act) =
- let (pilc, act_env) = prod_item_list univ [] pil (BorderProd (true,None)) in
- let a = to_act_check_vars act_env act in
- { gr_name = name; gr_production = pilc; gr_action = a }
-
-let border = function
- | NonTerm (ETConstr(_,BorderProd (_,a)),_) :: _ -> a
- | _ -> None
-
-let clever_assoc ass g =
- if g.gr_production <> [] then
- (match border g.gr_production, border (List.rev g.gr_production) with
- | Some LeftA, Some RightA -> ass (* Untractable; we cheat *)
- | Some LeftA, _ -> Some LeftA
- | _, Some RightA -> Some RightA
- | _ -> Some NonA)
- else ass
-
-let gram_entry univ (nt, ass, rl) =
- let from = explicitize_entry (snd univ) nt in
- let l = List.map (gram_rule (univ,from)) rl in
- let ass = List.fold_left clever_assoc ass l in
- { ge_name = from;
- gl_assoc = ass;
- gl_rules = l }
-
-let interp_grammar_command univ ge entryl =
- { gc_univ = univ;
- gc_entries = List.map (gram_entry (ge,univ)) entryl }
-
-(* unparsing objects *)
-
-type 'pat unparsing_hunk =
- | PH of 'pat * string option * parenRelation
- | RO of string
- | UNP_BOX of ppbox * 'pat unparsing_hunk list
- | UNP_BRK of int * int
- | UNP_TBRK of int * int
- | UNP_TAB
- | UNP_FNL
- | UNP_SYMBOLIC of string option * string * 'pat unparsing_hunk
-
-let rec subst_hunk subst_pat subst hunk = match hunk with
- | PH (pat,so,pr) ->
- let pat' = subst_pat subst pat in
- if pat'==pat then hunk else
- PH (pat',so,pr)
- | RO _ -> hunk
- | UNP_BOX (ppbox, hunkl) ->
- let hunkl' = list_smartmap (subst_hunk subst_pat subst) hunkl in
- if hunkl' == hunkl then hunk else
- UNP_BOX (ppbox, hunkl')
- | UNP_BRK _
- | UNP_TBRK _
- | UNP_TAB
- | UNP_FNL -> hunk
- | UNP_SYMBOLIC (s1, s2, pat) ->
- let pat' = subst_hunk subst_pat subst pat in
- if pat' == pat then hunk else
- UNP_SYMBOLIC (s1, s2, pat')
-
-(* Checks if the precedence of the parent printer (None means the
- highest precedence), and the child's one, follow the given
- relation. *)
-
-let tolerable_prec oparent_prec_reln child_prec =
- match oparent_prec_reln with
- | Some (pprec, L) -> child_prec < pprec
- | Some (pprec, E) -> child_prec <= pprec
- | Some (_, Prec level) -> child_prec <= level
- | _ -> true
-
-type 'pat syntax_entry = {
- syn_id : string;
- syn_prec: precedence;
- syn_astpat : 'pat;
- syn_hunks : 'pat unparsing_hunk list }
-
-let subst_syntax_entry subst_pat subst sentry =
- let syn_astpat' = subst_pat subst sentry.syn_astpat in
- let syn_hunks' = list_smartmap (subst_hunk subst_pat subst) sentry.syn_hunks
- in
- if syn_astpat' == sentry.syn_astpat
- && syn_hunks' == sentry.syn_hunks then sentry
- else
- { sentry with
- syn_astpat = syn_astpat' ;
- syn_hunks = syn_hunks' ;
- }
-
-type 'pat syntax_command = {
- sc_univ : string;
- sc_entries : 'pat syntax_entry list }
-
-let subst_syntax_command subst_pat subst scomm =
- let sc_entries' =
- list_smartmap (subst_syntax_entry subst_pat subst) scomm.sc_entries
- in
- if sc_entries' == scomm.sc_entries then scomm else
- { scomm with sc_entries = sc_entries' }
-
-type syntax_rule = string * Coqast.t * Coqast.t unparsing_hunk list
-type raw_syntax_entry = precedence * syntax_rule list
-
-let rec interp_unparsing env = function
- | PH (ast,ext,pr) -> PH (Ast.val_of_ast env ast,ext,pr)
- | UNP_BOX (b,ul) -> UNP_BOX (b,List.map (interp_unparsing env) ul)
- | UNP_BRK _ | RO _ | UNP_TBRK _ | UNP_TAB | UNP_FNL as x -> x
- | UNP_SYMBOLIC (x,y,u) -> UNP_SYMBOLIC (x,y,interp_unparsing env u)
-
-let rule_of_ast univ prec (s,spat,unp) =
- let (astpat,meta_env) = Ast.to_pat [] spat in
- let hunks = List.map (interp_unparsing meta_env) unp in
- { syn_id = s;
- syn_prec = prec;
- syn_astpat = astpat;
- syn_hunks = hunks }
-
-let level_of_ast univ (prec,rl) = List.map (rule_of_ast univ prec) rl
-
-let interp_syntax_entry univ sel =
- { sc_univ = univ;
- sc_entries = List.flatten (List.map (level_of_ast univ) sel)}
-
-
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 80a0e4448..6a51d738d 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -8,9 +8,9 @@
(*i $Id$ i*)
-(*i*)
-open Pp
open Util
+(*i
+open Pp
open Names
open Ast
open Coqast
@@ -18,9 +18,10 @@ open Ppextend
open Topconstr
open Genarg
open Mod_subst
-(*i*)
+i*)
-type entry_type = argument_type
+(**********************************************************************)
+(* constr entry keys *)
type production_position =
| BorderProd of bool * Gramext.g_assoc option (* true=left; false=right *)
@@ -39,41 +40,13 @@ type ('lev,'pos) constr_entry_key =
type constr_production_entry =
(production_level,production_position) constr_entry_key
-type constr_entry = (int,unit) constr_entry_key
-type simple_constr_production_entry = (production_level,unit) constr_entry_key
-
-type nonterm_prod =
- | ProdList0 of nonterm_prod
- | ProdList1 of nonterm_prod * Token.pattern list
- | ProdOpt of nonterm_prod
- | ProdPrimitive of constr_production_entry
-
-type prod_item =
- | Term of Token.pattern
- | NonTerm of constr_production_entry *
- (Names.identifier * constr_production_entry) option
-
-type grammar_rule = {
- gr_name : string;
- gr_production : prod_item list;
- gr_action : constr_expr }
-
-type grammar_entry = {
- ge_name : constr_entry;
- gl_assoc : Gramext.g_assoc option;
- gl_rules : grammar_rule list }
-
-type grammar_command = {
- gc_univ : string;
- gc_entries : grammar_entry list }
+type constr_entry =
+ (int,unit) constr_entry_key
+type simple_constr_production_entry =
+ (production_level,unit) constr_entry_key
-type grammar_associativity = Gramext.g_assoc option
-
-(* Globalisation and type-checking of Grammar actions *)
-type entry_context = identifier list
-
-val set_constr_globalizer :
- (entry_context -> constr_expr -> constr_expr) -> unit
+(**********************************************************************)
+(* syntax modifiers *)
type syntax_modifier =
| SetItemLevel of string list * production_level
@@ -83,67 +56,3 @@ type syntax_modifier =
| SetOnlyParsing
| SetFormat of string located
-type nonterm =
- | NtShort of string
- | NtQual of string * string
-type grammar_production =
- | VTerm of string
- | VNonTerm of loc * nonterm * Names.identifier option
-type raw_grammar_rule = string * grammar_production list * grammar_action
-type raw_grammar_entry = string * grammar_associativity * raw_grammar_rule list
-
-val terminal : string -> string * string
-
-val rename_command_entry : string -> string
-
-val explicitize_entry : string -> string -> constr_entry
-
-val subst_grammar_command :
- substitution -> grammar_command -> grammar_command
-
-(* unparsing objects *)
-
-type 'pat unparsing_hunk =
- | PH of 'pat * string option * parenRelation
- | RO of string
- | UNP_BOX of ppbox * 'pat unparsing_hunk list
- | UNP_BRK of int * int
- | UNP_TBRK of int * int
- | UNP_TAB
- | UNP_FNL
- | UNP_SYMBOLIC of string option * string * 'pat unparsing_hunk
-
-(* Checks if the precedence of the parent printer (None means the
- highest precedence), and the child's one, follow the given
- relation. *)
-
-val tolerable_prec : tolerability option -> precedence -> bool
-
-type 'pat syntax_entry = {
- syn_id : string;
- syn_prec: precedence;
- syn_astpat : 'pat;
- syn_hunks : 'pat unparsing_hunk list }
-
-val subst_syntax_entry :
- (substitution -> 'pat -> 'pat) ->
- substitution -> 'pat syntax_entry -> 'pat syntax_entry
-
-
-type 'pat syntax_command = {
- sc_univ : string;
- sc_entries : 'pat syntax_entry list }
-
-val subst_syntax_command :
- (substitution -> 'pat -> 'pat) ->
- substitution -> 'pat syntax_command -> 'pat syntax_command
-
-type syntax_rule = string * Coqast.t * Coqast.t unparsing_hunk list
-type raw_syntax_entry = precedence * syntax_rule list
-
-val interp_grammar_command :
- string -> (string * string -> unit) ->
- raw_grammar_entry list -> grammar_command
-
-val interp_syntax_entry :
- string -> raw_syntax_entry list -> Ast.astpat syntax_command
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index d2df2e144..1f8422111 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -24,12 +24,7 @@ let constr_kw =
"end"; "as"; "let"; "if"; "then"; "else"; "return";
"Prop"; "Set"; "Type"; ".("; "_"; ".." ]
-let _ =
- if not !Options.v7 then
- List.iter (fun s -> Lexer.add_token("",s)) constr_kw
-
-(* For Correctness syntax; doesn't work if in psyntax (freeze pb?) *)
-let _ = Lexer.add_token ("","!")
+let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw
let mk_cast = function
(c,(_,None)) -> c
@@ -39,9 +34,6 @@ let mk_lam = function
([],c) -> c
| (bl,c) -> CLambdaN(constr_loc c, bl,c)
-let mk_match (loc,cil,rty,br) =
- CCases(loc,(None,rty),cil,br)
-
let loc_of_binder_let = function
| LocalRawAssum ((loc,_)::_,_)::_ -> loc
| LocalRawDef ((loc,_),_)::_ -> loc
@@ -125,7 +117,6 @@ let lpar_id_coloneq =
| _ -> raise Stream.Failure)
-if not !Options.v7 then
GEXTEND Gram
GLOBAL: binder_constr lconstr constr operconstr sort global
constr_pattern lconstr_pattern Constr.ident binder binder_let pattern;
@@ -138,9 +129,6 @@ GEXTEND Gram
Prim.name:
[ [ "_" -> (loc, Anonymous) ] ]
;
- Prim.ast:
- [ [ "_" -> Coqast.Nvar(loc,id_of_string"_") ] ]
- ;
global:
[ [ r = Prim.reference -> r
@@ -259,7 +247,7 @@ GEXTEND Gram
;
match_constr:
[ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with";
- br=branches; "end" -> mk_match (loc,ci,ty,br) ] ]
+ br=branches; "end" -> CCases(loc,ty,ci,br) ] ]
;
case_item:
[ [ c=operconstr LEVEL "100"; p=pred_pattern -> (c,p) ] ]
@@ -297,7 +285,7 @@ GEXTEND Gram
| _ -> Util.user_err_loc
(cases_pattern_loc p, "compound_pattern",
Pp.str "Constructor expected"))
- | p = pattern; "as"; id = base_ident ->
+ | p = pattern; "as"; id = ident ->
CPatAlias (loc, p, id)
| c = pattern; "%"; key=IDENT ->
CPatDelimiters (loc,key,c) ]
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index 734a65174..313886e9a 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -10,12 +10,10 @@
open Pp
open Util
-open Ast
open Topconstr
open Rawterm
open Tacexpr
open Vernacexpr
-open Ast
open Pcoq
open Prim
open Tactic
@@ -39,7 +37,6 @@ let arg_of_expr = function
(* Tactics grammar rules *)
-if not !Options.v7 then
GEXTEND Gram
GLOBAL: tactic Vernac_.command tactic_expr tactic_arg constr_may_eval;
@@ -60,7 +57,7 @@ GEXTEND Gram
| IDENT "info"; tc = tactic_expr -> TacInfo tc
(*To do: put Abstract in Refiner*)
| IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None)
- | IDENT "abstract"; tc = NEXT; "using"; s = base_ident ->
+ | IDENT "abstract"; tc = NEXT; "using"; s = ident ->
TacAbstract (tc,Some s) ]
(*End of To do*)
| "2" RIGHTA
@@ -135,7 +132,7 @@ GEXTEND Gram
;
input_fun:
[ [ "_" -> None
- | l = base_ident -> Some l ] ]
+ | l = ident -> Some l ] ]
;
let_clause:
[ [ id = identref; ":="; te = tactic_expr ->
diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index 85b79d8bf..d80cc5ec3 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -8,105 +8,14 @@
(* $Id$ *)
-(* This file to allow writing (3) for (S (S (S O)))
- and still write (S y) for (S y) *)
+(* This file defines the printer for natural numbers in [nat] *)
+(*i*)
open Pcoq
open Pp
open Util
open Names
-open Coqast
-open Ast
open Coqlib
-open Termast
-open Extend
-
-let ast_O = ast_of_ref glob_O
-let ast_S = ast_of_ref glob_S
-
-(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
-let nat_of_int n dloc =
- let ast_O = set_loc dloc ast_O in
- let ast_S = set_loc dloc ast_S in
- let rec mk_nat n =
- if n <= 0 then
- ast_O
- else
- Node(dloc,"APPLIST", [ast_S; mk_nat (n-1)])
- in
- mk_nat n
-
-let pat_nat_of_int n dloc =
- let ast_O = set_loc dloc ast_O in
- let ast_S = set_loc dloc ast_S in
- let rec mk_nat n =
- if n <= 0 then
- ast_O
- else
- Node(dloc,"PATTCONSTRUCT", [ast_S; mk_nat (n-1)])
- in
- mk_nat n
-
-let nat_of_string s dloc =
- nat_of_int (int_of_string s) dloc
-
-let pat_nat_of_string s dloc =
- pat_nat_of_int (int_of_string s) dloc
-
-exception Non_closed_number
-
-let rec int_of_nat_rec astS astO p =
- match p with
- | Node (_,"APPLIST", [b; a]) when alpha_eq(b,astS) ->
- (int_of_nat_rec astS astO a)+1
- | a when alpha_eq(a,astO) -> 1
- (***** YES, 1, non 0 ... to print the successor of p *)
- | _ -> raise Non_closed_number
-
-let int_of_nat p =
- try
- Some (int_of_nat_rec ast_S ast_O p)
- with
- Non_closed_number -> None
-
-let pr_S a = hov 0 (str "S" ++ brk (1,1) ++ a)
-
-let rec pr_external_S std_pr = function
- | Node (l,"APPLIST", [b; a]) when alpha_eq (b,ast_S) ->
- str"(" ++ pr_S (pr_external_S std_pr a) ++ str")"
- | p -> std_pr p
-
-(* Declare the primitive printer *)
-
-(* Prints not p, but the SUCCESSOR of p !!!!! *)
-let nat_printer std_pr p =
- match (int_of_nat p) with
- | Some i -> str "(" ++ str (string_of_int i) ++ str ")"
- | None -> str "(" ++ pr_S (pr_external_S std_pr p) ++ str ")"
-
-let _ = Esyntax.Ppprim.add ("nat_printer", nat_printer)
-(*
-(* Declare the primitive parser *)
-
-let unat = create_univ_if_new "nat"
-
-let number = create_constr_entry unat "number"
-let pat_number = create_constr_entry unat "pat_number"
-
-let _ =
- Gram.extend number None
- [None, None,
- [[Gramext.Stoken ("INT", "")],
- Gramext.action nat_of_string]]
-
-let _ =
- Gram.extend pat_number None
- [None, None,
- [[Gramext.Stoken ("INT", "")],
- Gramext.action pat_nat_of_string]]
-*)
-
-(*i*)
open Rawterm
open Libnames
open Bigint
@@ -191,38 +100,3 @@ let _ =
(glob_nat,["Coq";"Init";"Datatypes"])
(nat_of_int,Some pat_nat_of_int)
([RRef (dummy_loc,glob_S); RRef (dummy_loc,glob_O)], uninterp_nat, None)
-
-(************************************************************************)
-(* Old ast printing *)
-
-open Coqast
-open Ast
-open Termast
-
-let _ = if !Options.v7 then
-let ast_O = ast_of_ref glob_O in
-let ast_S = ast_of_ref glob_S in
-
-let rec int_of_nat = function
- | Node (_,"APPLIST", [b; a]) when alpha_eq(b,ast_S) -> (int_of_nat a) + 1
- | a when alpha_eq(a,ast_O) -> 0
- | _ -> raise Non_closed_number
-in
-(* Prints not p, but the SUCCESSOR of p !!!!! *)
-let nat_printer_S p =
- try
- Some (int (int_of_nat p + 1))
- with
- Non_closed_number -> None
-in
-let nat_printer_O _ =
- Some (int 0)
-in
-(* Declare the primitive printers *)
-let _ =
- Esyntax.declare_primitive_printer "nat_printer_S" "nat_scope" nat_printer_S
-in
-let _ =
- Esyntax.declare_primitive_printer "nat_printer_O" "nat_scope" nat_printer_O
-in
-()
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 2bb5b0630..bbf00a489 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -33,47 +33,22 @@ let local_make_binding loc a b =
let local_append l id = l@[id]
GEXTEND Gram
- GLOBAL: bigint ident natural integer string preident ast
- astlist qualid reference dirpath identref name base_ident var
- hyp;
+ GLOBAL: bigint ident string preident ast
+ astlist qualid reference dirpath identref name base_ident var;
- (* Compatibility: Prim.var is a synonym of Prim.ident *)
- var:
- [ [ id = ident -> id ] ]
- ;
- hyp:
- [ [ id = ident -> id ] ]
- ;
metaident:
[ [ s = METAIDENT -> Nmeta (loc,s) ] ]
;
- preident:
- [ [ s = IDENT -> s ] ]
- ;
base_ident:
[ [ s = IDENT -> local_id_of_string s ] ]
;
- name:
- [ [ IDENT "_" -> (loc, Anonymous)
- | id = base_ident -> (loc, Name id) ] ]
- ;
- identref:
- [ [ id = base_ident -> (loc,id) ] ]
- ;
ident:
[ [ id = base_ident -> id ] ]
;
- natural:
- [ [ i = INT -> local_make_posint i ] ]
- ;
bigint:
[ [ i = INT -> Bigint.of_string i
| "-"; i = INT -> Bigint.neg (Bigint.of_string i) ] ]
;
- integer:
- [ [ i = INT -> local_make_posint i
- | "-"; i = INT -> local_make_negint i ] ]
- ;
field:
[ [ s = FIELD -> local_id_of_string s ] ]
;
diff --git a/parsing/g_primnew.ml4 b/parsing/g_primnew.ml4
index 667b5654e..0a3a3c92b 100644
--- a/parsing/g_primnew.ml4
+++ b/parsing/g_primnew.ml4
@@ -8,71 +8,62 @@
(*i $Id$ i*)
-open Coqast
open Pcoq
open Names
open Libnames
open Topconstr
-let _ =
- if not !Options.v7 then
- Pcoq.reset_all_grammars()
-let _ =
- if not !Options.v7 then
- let f = Gram.Unsafe.clear_entry in
- f Prim.bigint;
- f Prim.qualid;
- f Prim.ast;
- f Prim.reference
-
-let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "<>"; "<<"; ">>"; "'"]
-let _ =
- if not !Options.v7 then
- List.iter (fun s -> Lexer.add_token("",s)) prim_kw
+let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"]
+let _ = List.iter (fun s -> Lexer.add_token("",s)) prim_kw
open Prim
-
open Nametab
-let local_id_of_string = id_of_string
-let local_make_dirpath = make_dirpath
-let local_make_qualid l id' = make_qualid (local_make_dirpath l) id'
-let local_make_short_qualid id = make_short_qualid id
-let local_make_posint = int_of_string
-let local_make_negint n = - int_of_string n
-let local_make_path l a = encode_kn (local_make_dirpath l) a
-let local_make_binding loc a b =
- match a with
- | Nvar (_,id) -> Slam(loc,Some id,b)
- | Nmeta (_,s) -> Smetalam(loc,s,b)
- | _ -> failwith "Slam expects a var or a metavar"
-let local_append l id = l@[id]
-if not !Options.v7 then
+let local_make_qualid l id = make_qualid (make_dirpath l) id
+
GEXTEND Gram
- GLOBAL: bigint fullyqualid qualid reference ne_string;
+ GLOBAL:
+ bigint natural integer identref name ident var preident
+ fullyqualid qualid reference
+ ne_string;
+ preident:
+ [ [ s = IDENT -> s ] ]
+ ;
+ ident:
+ [ [ s = IDENT -> id_of_string s ] ]
+ ;
+ var: (* as identref, but interpret as a term identifier in ltac *)
+ [ [ id = ident -> (loc,id) ] ]
+ ;
+ identref:
+ [ [ id = ident -> (loc,id) ] ]
+ ;
field:
- [ [ s = FIELD -> local_id_of_string s ] ]
+ [ [ s = FIELD -> id_of_string s ] ]
;
fields:
- [ [ id = field; (l,id') = fields -> (local_append l id,id')
+ [ [ id = field; (l,id') = fields -> (l@[id],id')
| id = field -> ([],id)
] ]
;
fullyqualid:
- [ [ id = base_ident; (l,id')=fields -> loc,id::List.rev (id'::l)
- | id = base_ident -> loc,[id]
+ [ [ id = ident; (l,id')=fields -> loc,id::List.rev (id'::l)
+ | id = ident -> loc,[id]
] ]
;
basequalid:
- [ [ id = base_ident; (l,id')=fields ->
- local_make_qualid (local_append l id) id'
- | id = base_ident -> local_make_short_qualid id
+ [ [ id = ident; (l,id')=fields -> local_make_qualid (l@[id]) id'
+ | id = ident -> make_short_qualid id
] ]
;
+ name:
+ [ [ IDENT "_" -> (loc, Anonymous)
+ | id = ident -> (loc, Name id) ] ]
+ ;
reference:
- [ [ id = base_ident; (l,id') = fields ->
- Qualid (loc, local_make_qualid (local_append l id) id')
- | id = base_ident -> Ident (loc,id)
+ [ [ id = ident; (l,id') = fields ->
+ Qualid (loc, local_make_qualid (l@[id]) id')
+ | id = ident -> Ident (loc,id)
] ]
;
qualid:
@@ -83,6 +74,13 @@ GEXTEND Gram
if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string"); s
] ]
;
+ integer:
+ [ [ i = INT -> int_of_string i
+ | "-"; i = INT -> - int_of_string i ] ]
+ ;
+ natural:
+ [ [ i = INT -> int_of_string i ] ]
+ ;
bigint: (* Negative numbers are dealt with specially *)
[ [ i = INT -> (Bigint.of_string i) ] ]
;
diff --git a/parsing/g_proofsnew.ml4 b/parsing/g_proofsnew.ml4
index 4f25354b6..5cf5152a3 100644
--- a/parsing/g_proofsnew.ml4
+++ b/parsing/g_proofsnew.ml4
@@ -21,7 +21,6 @@ open Constr
let thm_token = G_vernacnew.thm_token
(* Proof commands *)
-if not !Options.v7 then
GEXTEND Gram
GLOBAL: command;
@@ -36,7 +35,7 @@ GEXTEND Gram
;
command:
[ [ IDENT "Goal"; c = Constr.lconstr -> VernacGoal c
- | IDENT "Proof" -> VernacNop
+ | IDENT "Proof" -> VernacProof (Tacexpr.TacId "")
| IDENT "Proof"; "with"; ta = tactic -> VernacProof ta
| IDENT "Abort" -> VernacAbort None
| IDENT "Abort"; IDENT "All" -> VernacAbortAll
@@ -113,7 +112,7 @@ GEXTEND Gram
tac = tactic ->
HintsExtern (None,n,c,tac)
| IDENT"Destruct";
- id = base_ident; ":=";
+ id = ident; ":=";
pri = natural;
dloc = destruct_location;
hyptyp = Constr.constr_pattern;
diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml
index 3cd6eba3a..fb5be2896 100644
--- a/parsing/g_rsyntax.ml
+++ b/parsing/g_rsyntax.ml
@@ -6,161 +6,15 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Coqast
-open Ast
open Pp
open Util
open Names
open Pcoq
-open Extend
open Topconstr
open Libnames
-(**********************************************************************)
-(* Parsing with Grammar *)
-(**********************************************************************)
-
-let get_r_sign loc =
- let mkid id =
- mkRefC (Qualid (loc,Libnames.make_short_qualid id))
- in
- ((mkid (id_of_string "R0"),
- mkid (id_of_string "R1"),
- mkid (id_of_string "Rplus"),
- mkid (id_of_string "Rmult"),
- mkid (id_of_string "NRplus"),
- mkid (id_of_string "NRmult")))
-
-let get_r_sign_ast loc =
- let mkid id =
- Termast.ast_of_ref (Nametab.locate (Libnames.make_short_qualid id))
- in
- ((mkid (id_of_string "R0"),
- mkid (id_of_string "R1"),
- mkid (id_of_string "Rplus"),
- mkid (id_of_string "Rmult"),
- mkid (id_of_string "NRplus"),
- mkid (id_of_string "NRmult")))
-
-(* We have the following interpretation:
- [| 0 |] = 0
- [| 1 |] = 1
- [| 2 |] = 1 + 1
- [| 3 |] = 1 + (1 + 1)
- [| 2n |] = 2 * [| n |] for n >= 2
- [| 2n+1 |] = 1 + 2 * [| n |] for n >= 2
- [| -n |] = - [| n |] for n >= 0
-*)
-
-open Bigint
-
-let rec int_decomp m =
- if equal m zero then [0] else
- if equal m one then [1] else
- let (m',b) = euclid m two in (if equal b zero then 0 else 1) :: int_decomp m'
-
-let _ = if !Options.v7 then
-let r_of_int n dloc =
- let (a0,a1,plus,mult,_,_) = get_r_sign dloc in
- let list_ch = int_decomp n in
- let a2 = mkAppC (plus, [a1; a1]) in
- let rec mk_r l =
- match l with
- | [] -> failwith "Error r_of_int"
- | [a] -> if a=1 then a1 else a0
- | [a;b] -> if a==1 then mkAppC (plus, [a1; a2]) else a2
- | a::l' -> if a=1 then mkAppC (plus, [a1; mkAppC (mult, [a2; mk_r l'])]) else mkAppC (mult, [a2; mk_r l'])
- in mk_r list_ch
-in
-let r_of_string s dloc =
- r_of_int (of_string s) dloc
-in
-let rsyntax_create name =
- let e =
- Pcoq.create_constr_entry (Pcoq.get_univ "rnatural") name in
- Pcoq.Gram.Unsafe.clear_entry e;
- e
-in
-let rnumber = rsyntax_create "rnumber"
-in
-let _ =
- Gram.extend rnumber None
- [None, None,
- [[Gramext.Stoken ("INT", "")],
- Gramext.action r_of_string]]
-in ()
-
-(**********************************************************************)
-(* Old ast printing *)
-(**********************************************************************)
-
exception Non_closed_number
-let _ = if !Options.v7 then
-let int_of_r p =
- let (a0,a1,plus,mult,_,_) = get_r_sign_ast dummy_loc in
- let rec int_of_r_rec p =
- match p with
- | Node (_,"APPLIST", [b;a;c]) when alpha_eq(b,plus) & alpha_eq(a,a1) & alpha_eq(c,a1) -> 2
- | Node (_,"APPLIST", [b;a;c]) when alpha_eq(b,plus) & alpha_eq(a,a1) ->
- (match c with
- | Node (_,"APPLIST", [e;d;f]) when alpha_eq(e,mult) -> 1 + int_of_r_rec c
- | Node (_,"APPLIST", [e;d;f]) when alpha_eq(e,plus) & alpha_eq(d,a1) & alpha_eq(f,a1) -> 3
- | _ -> raise Non_closed_number)
- | Node (_,"APPLIST", [b;a;c]) when alpha_eq(b,mult) ->
- (match a with
- | Node (_,"APPLIST", [e;d;f]) when alpha_eq(e,plus) & alpha_eq(d,a1) & alpha_eq(f,a1) ->
- (match c with
- | g when alpha_eq(g,a1) -> raise Non_closed_number
- | g when alpha_eq(g,a0) -> raise Non_closed_number
- | _ -> 2 * int_of_r_rec c)
- | _ -> raise Non_closed_number)
- | a when alpha_eq(a,a0) -> 0
- | a when alpha_eq(a,a1) -> 1
- | _ -> raise Non_closed_number in
- try
- Some (int_of_r_rec p)
- with
- Non_closed_number -> None
-in
-let replace_plus p =
- let (_,_,_,_,astnrplus,_) = get_r_sign_ast dummy_loc in
- ope ("REXPR",[ope("APPLIST",[astnrplus;p])])
-in
-let replace_mult p =
- let (_,_,_,_,_,astnrmult) = get_r_sign_ast dummy_loc in
- ope ("REXPR",[ope("APPLIST",[astnrmult;p])])
-in
-let rec r_printer_odd std_pr p =
- let (_,a1,plus,_,_,_) = get_r_sign_ast dummy_loc in
- match (int_of_r (ope("APPLIST",[plus;a1;p]))) with
- | Some i -> str (string_of_int i)
- | None -> std_pr (replace_plus p)
-in
-let rec r_printer_odd_outside std_pr p =
- let (_,a1,plus,_,_,_) = get_r_sign_ast dummy_loc in
- match (int_of_r (ope("APPLIST",[plus;a1;p]))) with
- | Some i -> str"``" ++ str (string_of_int i) ++ str"``"
- | None -> std_pr (replace_plus p)
-in
-let rec r_printer_even std_pr p =
- let (_,a1,plus,mult,_,_) = get_r_sign_ast dummy_loc in
- match (int_of_r (ope("APPLIST",[mult;(ope("APPLIST",[plus;a1;a1]));p]))) with
- | Some i -> str (string_of_int i)
- | None -> std_pr (replace_mult p)
-in
-let rec r_printer_even_outside std_pr p =
- let (_,a1,plus,mult,_,_) = get_r_sign_ast dummy_loc in
- match (int_of_r (ope("APPLIST",[mult;(ope("APPLIST",[plus;a1;a1]));p]))) with
- | Some i -> str"``" ++ str (string_of_int i) ++ str"``"
- | None -> std_pr (replace_mult p)
-in
-let _ = Esyntax.Ppprim.add ("r_printer_odd", r_printer_odd) in
-let _ = Esyntax.Ppprim.add ("r_printer_odd_outside", r_printer_odd_outside) in
-let _ = Esyntax.Ppprim.add ("r_printer_even", r_printer_even) in
-let _ = Esyntax.Ppprim.add ("r_printer_even_outside", r_printer_even_outside)
-in ()
-
(**********************************************************************)
(* Parsing R via scopes *)
(**********************************************************************)
@@ -182,29 +36,6 @@ let glob_Ropp = ConstRef (make_path rdefinitions "Ropp")
let glob_Rplus = ConstRef (make_path rdefinitions "Rplus")
let glob_Rmult = ConstRef (make_path rdefinitions "Rmult")
-(* V7 *)
-let r_of_posint dloc n =
- let ref_R0 = RRef (dloc, glob_R0) in
- let ref_R1 = RRef (dloc, glob_R1) in
- let ref_Rplus = RRef (dloc, glob_Rplus) in
- let ref_Rmult = RRef (dloc, glob_Rmult) in
- let a2 = RApp(dloc, ref_Rplus, [ref_R1; ref_R1]) in
- let list_ch = int_decomp n in
- let rec mk_r l =
- match l with
- | [] -> failwith "Error r_of_posint"
- | [a] -> if a=1 then ref_R1 else ref_R0
- | a::[b] -> if a==1 then RApp (dloc, ref_Rplus, [ref_R1; a2]) else a2
- | a::l' -> if a=1 then RApp (dloc, ref_Rplus, [ref_R1; RApp (dloc, ref_Rmult, [a2; mk_r l'])]) else RApp (dloc, ref_Rmult, [a2; mk_r l'])
- in mk_r list_ch
-
-let r_of_int2 dloc z =
- if is_strictly_neg z then
- RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc (neg z)])
- else
- r_of_posint dloc z
-
-(* V8 *)
let two = mult_2 one
let three = add_1 two
let four = mult_2 two
@@ -280,54 +111,8 @@ let uninterp_r p =
let _ = Notation.declare_numeral_interpreter "R_scope"
(glob_R,["Coq";"Reals";"Rdefinitions"])
- ((if !Options.v7 then r_of_int2 else r_of_int),None)
+ (r_of_int,None)
([RRef(dummy_loc,glob_Ropp);RRef(dummy_loc,glob_R0);
RRef(dummy_loc,glob_Rplus);RRef(dummy_loc,glob_Rmult);RRef(dummy_loc,glob_R1)],
uninterp_r,
None)
-
-(************************************************************************)
-(* Old ast printers via scope *)
-
-let _ = if !Options.v7 then
-let bignat_of_pos p =
- let (_,one,plus,_,_,_) = get_r_sign_ast dummy_loc in
- let rec transl = function
- | Node (_,"APPLIST",[p; o; a]) when alpha_eq(p,plus) & alpha_eq(o,one)
- -> add_1(transl a)
- | a when alpha_eq(a,one) -> Bigint.one
- | _ -> raise Non_closed_number
- in transl p
-in
-let bignat_option_of_pos p =
- try
- Some (bignat_of_pos p)
- with Non_closed_number ->
- None
-in
-let r_printer_Rplus1 p =
- match bignat_option_of_pos p with
- | Some n -> Some (str (Bigint.to_string (add_1 n)))
- | None -> None
-in
-let r_printer_Ropp p =
- match bignat_option_of_pos p with
- | Some n -> Some (str "-" ++ str (Bigint.to_string n))
- | None -> None
-in
-let r_printer_R1 _ =
- Some (int 1)
-in
-let r_printer_R0 _ =
- Some (int 0)
-in
-(* Declare pretty-printers for integers *)
-let _ =
- Esyntax.declare_primitive_printer "r_printer_Ropp" "R_scope" (r_printer_Ropp)
-in let _ =
- Esyntax.declare_primitive_printer "r_printer_Rplus1" "R_scope" (r_printer_Rplus1)
-in let _ =
- Esyntax.declare_primitive_printer "r_printer_R1" "R_scope" (r_printer_R1)
-in let _ =
- Esyntax.declare_primitive_printer "r_printer_R0" "R_scope" r_printer_R0
-in ()
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index c7fee72db..180754668 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -9,7 +9,6 @@
(* $Id$ *)
open Pp
-open Ast
open Pcoq
open Util
open Tacexpr
@@ -18,11 +17,8 @@ open Genarg
let compute = Cbv all_flags
-let tactic_kw =
- [ "->"; "<-" ]
-let _ =
- if not !Options.v7 then
- List.iter (fun s -> Lexer.add_token("",s)) tactic_kw
+let tactic_kw = [ "->"; "<-" ]
+let _ = List.iter (fun s -> Lexer.add_token("",s)) tactic_kw
(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
(* admissible notation "(x t)" *)
@@ -98,15 +94,8 @@ let induction_arg_of_constr c =
try ElimOnIdent (Topconstr.constr_loc c,snd(coerce_to_id c))
with _ -> ElimOnConstr c
-let local_compute = [FBeta;FIota;FDeltaBut [];FZeta]
-
-let error_oldelim _ = error "OldElim no longer supported"
-
-let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
-
(* Auxiliary grammar rules *)
-if not !Options.v7 then
GEXTEND Gram
GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
bindings red_expr int_or_var open_constr casted_open_constr
@@ -141,7 +130,7 @@ GEXTEND Gram
] ]
;
quantified_hypothesis:
- [ [ id = base_ident -> NamedHyp id
+ [ [ id = ident -> NamedHyp id
| n = natural -> AnonHyp n ] ]
;
conversion:
@@ -167,11 +156,11 @@ GEXTEND Gram
[ [ "["; tc = LIST1 intropatterns SEP "|" ; "]" -> IntroOrAndPattern tc
| "("; tc = LIST1 simple_intropattern SEP "," ; ")" -> IntroOrAndPattern [tc]
| "_" -> IntroWildcard
- | id = base_ident -> IntroIdentifier id
+ | id = ident -> IntroIdentifier id
] ]
;
simple_binding:
- [ [ "("; id = base_ident; ":="; c = lconstr; ")" -> (loc, NamedHyp id, c)
+ [ [ "("; id = ident; ":="; c = lconstr; ")" -> (loc, NamedHyp id, c)
| "("; n = natural; ":="; c = lconstr; ")" -> (loc, AnonHyp n, c) ] ]
;
bindings:
@@ -221,11 +210,12 @@ GEXTEND Gram
| s = IDENT -> ExtraRedExpr s ] ]
;
hypident:
- [ [ id = id_or_meta -> id,(InHyp,ref None)
+ [ [ id = id_or_meta ->
+ id,InHyp
| "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" ->
- id,(InHypTypeOnly,ref None)
+ id,InHypTypeOnly
| "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" ->
- id,(InHypValueOnly,ref None)
+ id,InHypValueOnly
] ]
;
hypident_occ:
@@ -251,7 +241,7 @@ GEXTEND Gram
| -> [] ] ]
;
fixdecl:
- [ [ "("; id = base_ident; bl=LIST0 Constr.binder; ann=fixannot;
+ [ [ "("; id = ident; bl=LIST0 Constr.binder; ann=fixannot;
":"; ty=lconstr; ")" -> (loc,id,bl,ann,ty) ] ]
;
fixannot:
@@ -275,11 +265,11 @@ GEXTEND Gram
IDENT "intros"; IDENT "until"; id = quantified_hypothesis ->
TacIntrosUntil id
| IDENT "intros"; pl = intropatterns -> TacIntroPattern pl
- | IDENT "intro"; id = base_ident; IDENT "after"; id2 = identref ->
+ | IDENT "intro"; id = ident; IDENT "after"; id2 = identref ->
TacIntroMove (Some id, Some id2)
| IDENT "intro"; IDENT "after"; id2 = identref ->
TacIntroMove (None, Some id2)
- | IDENT "intro"; id = base_ident -> TacIntroMove (Some id, None)
+ | IDENT "intro"; id = ident -> TacIntroMove (Some id, None)
| IDENT "intro" -> TacIntroMove (None, None)
| IDENT "assumption" -> TacAssumption
@@ -293,12 +283,12 @@ GEXTEND Gram
| IDENT "case"; cl = constr_with_bindings -> TacCase cl
| IDENT "casetype"; c = constr -> TacCaseType c
| "fix"; n = natural -> TacFix (None,n)
- | "fix"; id = base_ident; n = natural -> TacFix (Some id,n)
- | "fix"; id = base_ident; n = natural; "with"; fd = LIST1 fixdecl ->
+ | "fix"; id = ident; n = natural -> TacFix (Some id,n)
+ | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl ->
TacMutualFix (id,n,List.map mk_fix_tac fd)
| "cofix" -> TacCofix None
- | "cofix"; id = base_ident -> TacCofix (Some id)
- | "cofix"; id = base_ident; "with"; fd = LIST1 fixdecl ->
+ | "cofix"; id = ident -> TacCofix (Some id)
+ | "cofix"; id = ident; "with"; fd = LIST1 fixdecl ->
TacMutualCofix (id,List.map mk_cofix_tac fd)
| IDENT "cut"; c = constr -> TacCut c
@@ -330,15 +320,15 @@ GEXTEND Gram
(* Derived basic tactics *)
| IDENT "simple"; IDENT"induction"; h = quantified_hypothesis ->
- TacSimpleInduction (h,ref [])
+ TacSimpleInduction h
| IDENT "induction"; c = induction_arg; ids = with_names;
- el = OPT eliminator -> TacNewInduction (c,el,(ids,ref []))
+ el = OPT eliminator -> TacNewInduction (c,el,ids)
| IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
| IDENT "simple"; IDENT"destruct"; h = quantified_hypothesis ->
TacSimpleDestruct h
| IDENT "destruct"; c = induction_arg; ids = with_names;
- el = OPT eliminator -> TacNewDestruct (c,el,(ids,ref []))
+ el = OPT eliminator -> TacNewDestruct (c,el,ids)
| IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c
| IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c
| IDENT "decompose"; "["; l = LIST1 global; "]"; c = constr
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 21aa0c732..4a0d498d3 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -11,7 +11,6 @@
open Pp
open Util
open Names
-open Coqast
open Topconstr
open Vernacexpr
open Pcoq
@@ -27,11 +26,8 @@ open Constr
open Vernac_
open Module
-
let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ]
-let _ =
- if not !Options.v7 then
- List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw
+let _ = List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw
(* Rem: do not join the different GEXTEND into one, it breaks native *)
(* compilation on PowerPC and Sun architectures *)
@@ -41,7 +37,6 @@ let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr"
let thm_token = Gram.Entry.create "vernac:thm_token"
let def_body = Gram.Entry.create "vernac:def_body"
-if not !Options.v7 then
GEXTEND Gram
GLOBAL: vernac gallina_ext;
vernac:
@@ -87,7 +82,6 @@ let no_coercion loc (c,x) =
x
(* Gallina declarations *)
-if not !Options.v7 then
GEXTEND Gram
GLOBAL: gallina gallina_ext thm_token def_body;
@@ -210,7 +204,7 @@ GEXTEND Gram
;
(* (co)-fixpoints *)
rec_definition:
- [ [ id = base_ident; bl = LIST1 binder_let;
+ [ [ id = ident; bl = LIST1 binder_let;
annot = OPT rec_annotation; type_ = type_cstr;
":="; def = lconstr; ntn = decl_notation ->
let names = List.map snd (names_of_local_assums bl) in
@@ -230,7 +224,7 @@ GEXTEND Gram
((id, ni, bl, type_, def),ntn) ] ]
;
corec_definition:
- [ [ id = base_ident; bl = LIST0 binder_let; c = type_cstr; ":=";
+ [ [ id = ident; bl = LIST0 binder_let; c = type_cstr; ":=";
def = lconstr ->
(id,bl,c ,def) ] ]
;
@@ -301,7 +295,6 @@ END
(* Modules and Sections *)
-if not !Options.v7 then
GEXTEND Gram
GLOBAL: gallina_ext module_expr module_type;
@@ -387,7 +380,6 @@ GEXTEND Gram
END
(* Extensions: implicits, coercions, etc. *)
-if not !Options.v7 then
GEXTEND Gram
GLOBAL: gallina_ext;
@@ -400,17 +392,17 @@ GEXTEND Gram
| 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
+ let s = coerce_global_to_id qid in
VernacDefinition
((Global,CanonicalStructure),(dummy_loc,s),d,
(fun _ -> Recordops.declare_canonical_structure))
(* Coercions *)
| IDENT "Coercion"; qid = global; d = def_body ->
- let s = Ast.coerce_global_to_id qid in
+ let s = 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
+ let s = 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 ->
@@ -436,7 +428,6 @@ GEXTEND Gram
;
END
-if not !Options.v7 then
GEXTEND Gram
GLOBAL: command check_command class_rawexpr;
@@ -632,7 +623,6 @@ GEXTEND Gram
;
END;
-if not !Options.v7 then
GEXTEND Gram
command:
[ [
@@ -661,7 +651,6 @@ GEXTEND Gram
(* Grammar extensions *)
-if not !Options.v7 then
GEXTEND Gram
GLOBAL: syntax;
@@ -737,13 +726,8 @@ GEXTEND Gram
[ [ "_" -> None | sc = IDENT -> Some sc ] ]
;
production_item:
- [[ s = ne_string -> VTerm s
- | nt = IDENT; po = OPT [ "("; p = ident; ")" -> p ] ->
- VNonTerm (loc,NtShort nt,po) ]]
+ [ [ s = ne_string -> VTerm s
+ | nt = IDENT; po = OPT [ "("; p = ident; ")" -> p ] ->
+ VNonTerm (loc,nt,po) ] ]
;
END
-
-(* Reinstall tactic and vernac extensions *)
-let _ =
- if not !Options.v7 then
- Egrammar.reset_extend_grammars_v8()
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 02b35a1d8..7b7e471c6 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -135,10 +135,13 @@ let rec interp_xml_constr = function
| XmlTag (loc,"CONST",al,[]) ->
RRef (loc, ConstRef (get_xml_constant al))
| XmlTag (loc,"MUTCASE",al,x::y::yl) -> (* BUGGE *)
+ failwith "XML MUTCASE TO DO";
+(*
ROrderedCase (loc,RegularStyle,Some (interp_xml_patternsType x),
interp_xml_inductiveTerm y,
Array.of_list (List.map interp_xml_pattern yl),
ref None)
+*)
| XmlTag (loc,"MUTIND",al,[]) ->
RRef (loc, IndRef (get_xml_inductive al))
| XmlTag (loc,"MUTCONSTRUCT",al,[]) ->
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index f78373c28..9f4bba335 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -8,144 +8,16 @@
(* $Id$ *)
-open Coqast
open Pcoq
open Pp
open Util
open Names
-open Ast
-open Extend
open Topconstr
open Libnames
open Bigint
-(**********************************************************************)
-(* V7 parsing via Grammar *)
-
-let get_z_sign loc =
- let mkid id =
- mkRefC (Qualid (loc,Libnames.make_short_qualid id))
- in
- ((mkid (id_of_string "xI"),
- mkid (id_of_string "xO"),
- mkid (id_of_string "xH")),
- (mkid (id_of_string "ZERO"),
- mkid (id_of_string "POS"),
- mkid (id_of_string "NEG")))
-
-let pos_of_bignat xI xO xH x =
- let rec pos_of x =
- match div2_with_rest x with
- | (q, true) when q <> zero -> mkAppC (xI, [pos_of q])
- | (q, false) -> mkAppC (xO, [pos_of q])
- | (_, true) -> xH
- in
- pos_of x
-
-let z_of_string pos_or_neg s dloc =
- let ((xI,xO,xH),(aZERO,aPOS,aNEG)) = get_z_sign dloc in
- let v = Bigint.of_string s in
- if v <> zero then
- if pos_or_neg then
- mkAppC (aPOS, [pos_of_bignat xI xO xH v])
- else
- mkAppC (aNEG, [pos_of_bignat xI xO xH v])
- else
- aZERO
-
-(* Declare the primitive parser with Grammar and without the scope mechanism *)
-let zsyntax_create name =
- let e =
- Pcoq.create_constr_entry (Pcoq.get_univ "znatural") name in
- Pcoq.Gram.Unsafe.clear_entry e;
- e
-
-let number = zsyntax_create "number"
-
-let negnumber = zsyntax_create "negnumber"
-
-let _ =
- Gram.extend number None
- [None, None,
- [[Gramext.Stoken ("INT", "")],
- Gramext.action (z_of_string true)]]
-
-let _ =
- Gram.extend negnumber None
- [None, None,
- [[Gramext.Stoken ("INT", "")],
- Gramext.action (z_of_string false)]]
-
-(**********************************************************************)
-(* Old v7 ast printing *)
-
-open Coqlib
-
exception Non_closed_number
-let get_z_sign_ast loc =
- let ast_of_id id =
- Termast.ast_of_ref
- (global_of_constr
- (gen_constant_in_modules "Z-printer" zarith_base_modules id))
- in
- ((ast_of_id "xI",
- ast_of_id "xO",
- ast_of_id "xH"),
- (ast_of_id "ZERO",
- ast_of_id "POS",
- ast_of_id "NEG"))
-
-let _ = if !Options.v7 then
-let rec bignat_of_pos c1 c2 c3 p =
- match p with
- | Node (_,"APPLIST", [b; a]) when alpha_eq(b,c1) ->
- mult_2 (bignat_of_pos c1 c2 c3 a)
- | Node (_,"APPLIST", [b; a]) when alpha_eq(b,c2) ->
- add_1 (mult_2 (bignat_of_pos c1 c2 c3 a))
- | a when alpha_eq(a,c3) -> Bigint.one
- | _ -> raise Non_closed_number
-in
-let bignat_option_of_pos xI xO xH p =
- try
- Some (bignat_of_pos xO xI xH p)
- with Non_closed_number ->
- None
-in
-let pr_pos a = hov 0 (str "POS" ++ brk (1,1) ++ a) in
-let pr_neg a = hov 0 (str "NEG" ++ brk (1,1) ++ a) in
-
-let inside_printer posneg std_pr p =
- let ((xI,xO,xH),_) = get_z_sign_ast dummy_loc in
- match (bignat_option_of_pos xI xO xH p) with
- | Some n ->
- if posneg then
- (str (Bigint.to_string n))
- else
- (str "(-" ++ str (Bigint.to_string n) ++ str ")")
- | None ->
- let pr = if posneg then pr_pos else pr_neg in
- str "(" ++ pr (std_pr (ope("ZEXPR",[p]))) ++ str ")"
-in
-let outside_printer posneg std_pr p =
- let ((xI,xO,xH),_) = get_z_sign_ast dummy_loc in
- match (bignat_option_of_pos xI xO xH p) with
- | Some n ->
- if posneg then
- (str "`" ++ str (Bigint.to_string n) ++ str "`")
- else
- (str "`-" ++ str (Bigint.to_string n) ++ str "`")
- | None ->
- let pr = if posneg then pr_pos else pr_neg in
- str "(" ++ pr (std_pr p) ++ str ")"
-in
-(* For printing with Syntax and without the scope mechanism *)
-let _ = Esyntax.Ppprim.add ("positive_printer", (outside_printer true)) in
-let _ = Esyntax.Ppprim.add ("negative_printer", (outside_printer false)) in
-let _ = Esyntax.Ppprim.add ("positive_printer_inside", (inside_printer true))in
-let _ = Esyntax.Ppprim.add ("negative_printer_inside", (inside_printer false))
-in ()
-
(**********************************************************************)
(* Parsing positive via scopes *)
(**********************************************************************)
@@ -235,8 +107,7 @@ let _ = Notation.declare_numeral_interpreter "positive_scope"
(**********************************************************************)
let binnat_module = ["Coq";"NArith";"BinNat"]
-let n_path = make_path (make_dir binnat_module)
- (id_of_string (if !Options.v7 then "entier" else "N"))
+let n_path = make_path (make_dir binnat_module) (id_of_string "N")
let glob_n = IndRef (n_path,0)
let path_of_N0 = ((n_path,0),1)
let path_of_Npos = ((n_path,0),2)
@@ -346,48 +217,3 @@ let _ = Notation.declare_numeral_interpreter "Z_scope"
RRef (dummy_loc, glob_NEG)],
uninterp_z,
None)
-
-(************************************************************************)
-(* Old V7 ast Printers *)
-
-open Esyntax
-
-let _ = if !Options.v7 then
-let bignat_of_pos p =
- let ((xI,xO,xH),_) = get_z_sign_ast dummy_loc in
- let c1 = xO in
- let c2 = xI in
- let c3 = xH in
- let rec transl = function
- | Node (_,"APPLIST",[b; a]) when alpha_eq(b,c1) -> mult_2(transl a)
- | Node (_,"APPLIST",[b; a]) when alpha_eq(b,c2) -> add_1(mult_2(transl a))
- | a when alpha_eq(a,c3) -> Bigint.one
- | _ -> raise Non_closed_number
- in transl p
-in
-let bignat_option_of_pos p =
- try
- Some (bignat_of_pos p)
- with Non_closed_number ->
- None
-in
-let z_printer posneg p =
- match bignat_option_of_pos p with
- | Some n ->
- if posneg then
- Some (str (Bigint.to_string n))
- else
- Some (str "-" ++ str (Bigint.to_string n))
- | None -> None
-in
-let z_printer_ZERO _ =
- Some (int 0)
-in
-(* Declare pretty-printers for integers *)
-let _ =
- declare_primitive_printer "z_printer_POS" "Z_scope" (z_printer true) in
-let _ =
- declare_primitive_printer "z_printer_NEG" "Z_scope" (z_printer false) in
-let _ =
- declare_primitive_printer "z_printer_ZERO" "Z_scope" z_printer_ZERO in
-()
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 1534123f8..1708fa5eb 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -93,12 +93,9 @@ let check_ident str =
| (('\134'..'\143' | '\152'..'\155'
| '\164'..'\165' | '\168'..'\171'),_) ->
bad_token str
- | _ -> (* default to iso 8859-1 "â" *)
- if !Options.v7 then loop_id [< 'c2; 'c3; s >]
- else bad_token str)
+ | _ ->
+ bad_token str)
(* iso 8859-1 accentuated letters *)
- | [< ' ('\192'..'\214' | '\216'..'\246' | '\248'..'\255'); s >] ->
- if !Options.v7 then loop_id s else bad_token str
| [< _ = Stream.empty >] -> ()
| [< >] -> bad_token str
in
@@ -170,26 +167,13 @@ let get_buff len = String.sub !buff 0 len
(* The classical lexer: idents, numbers, quoted strings, comments *)
-let rec ident_tail len strm =
- if !Options.v7 then
- match strm with parser
- | [< ' ('a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_' | '@' as c); s >] ->
- ident_tail (store len c) s
- (* Greek utf-8 letters [CE80-CEBF and CF80-CFBF] (CE=206; BF=191) *)
- | [< ' ('\206' | '\207' as c1); ' ('\128'..'\191' as c2) ; s >] ->
- ident_tail (store (store len c1) c2) s
- (* iso 8859-1 accentuated letters *)
- | [< ' ('\192'..'\214' | '\216'..'\246' | '\248'..'\255' as c); s >] ->
- ident_tail (store len c) s
- | [< >] -> len
- else
- match strm with parser
- | [< ' ('a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_' as c); s >] ->
- ident_tail (store len c) s
- (* Greek utf-8 letters [CE80-CEBF and CF80-CFBF] (CE=206; BF=191) *)
- | [< ' ('\206' | '\207' as c1); ' ('\128'..'\191' as c2) ; s >] ->
- ident_tail (store (store len c1) c2) s
- | [< >] -> len
+let rec ident_tail len = parser
+ | [< ' ('a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_' as c); s >] ->
+ ident_tail (store len c) s
+ (* Greek utf-8 letters [CE80-CEBF and CF80-CFBF] (CE=206; BF=191) *)
+ | [< ' ('\206' | '\207' as c1); ' ('\128'..'\191' as c2) ; s >] ->
+ ident_tail (store (store len c1) c2) s
+ | [< >] -> len
let rec number len = parser
@@ -198,21 +182,11 @@ let rec number len = parser
let escape len c = store len c
-let rec string_v8 bp len = parser
+let rec string bp len = parser
| [< ''"'; esc=(parser [<''"' >] -> true | [< >] -> false); s >] ->
- if esc then string_v8 bp (store len '"') s else len
- | [< 'c; s >] -> string_v8 bp (store len c) s
- | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string
-
-let rec string_v7 bp len = parser
- | [< ''"' >] -> len
- | [< ''\\'; c = (parser [< ' ('"' | '\\' as c) >] -> c | [< >] -> '\\'); s >]
- -> string_v7 bp (escape len c) s
+ if esc then string bp (store len '"') s else len
+ | [< 'c; s >] -> string bp (store len c) s
| [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string
- | [< 'c; s >] -> string_v7 bp (store len c) s
-
-let string bp len s =
- if !Options.v7 then string_v7 bp len s else string_v8 bp len s
(* Hook for exporting comment into xml theory files *)
let xml_output_comment = ref (fun _ -> ())
@@ -359,45 +333,22 @@ let parse_226_tail tk = parser
(* Parse what follows a dot *)
-let parse_after_dot bp c strm =
- if !Options.v7 then
- match strm with parser
- | [< ' ('_' | 'a'..'z' | 'A'..'Z' as c);
- len = ident_tail (store 0 c) >] ->
- ("FIELD", get_buff len)
- (* Greek utf-8 letters [CE80-CEBF and CF80-CFBF] (CE=206; BF=191) *)
- | [< ' ('\206' | '\207' as c1); ' ('\128'..'\191' as c2);
- len = ident_tail (store (store 0 c1) c2) >] ->
- ("FIELD", get_buff len)
- (* utf-8 mathematical symbols have format E2 xx xx [E2=226] *)
- | [< ''\226'; t = parse_226_tail
- (progress_special '.' (Some !token_tree)) >] ep ->
- (match t with
- | TokSymbol (Some t) -> ("", t)
- | TokSymbol None -> err (bp, ep) Undefined_token
- | TokIdent t -> ("FIELD", t))
- (* iso 8859-1 accentuated letters *)
- | [< ' ('\192'..'\214' | '\216'..'\246' | '\248'..'\255' as c);
- len = ident_tail (store 0 c) >] ->
- ("FIELD", get_buff len)
- | [< (t,_) = process_chars bp c >] -> t
- else
- match strm with parser
- | [< ' ('a'..'z' | 'A'..'Z' | '_' as c);
- len = ident_tail (store 0 c) >] ->
- ("FIELD", get_buff len)
- (* Greek utf-8 letters [CE80-CEBF and CF80-CFBF] (CE=206; BF=191) *)
- | [< ' ('\206' | '\207' as c1); ' ('\128'..'\191' as c2);
- len = ident_tail (store (store 0 c1) c2) >] ->
- ("FIELD", get_buff len)
- (* utf-8 mathematical symbols have format E2 xx xx [E2=226] *)
- | [< ''\226'; t = parse_226_tail
- (progress_special '.' (Some !token_tree)) >] ep ->
- (match t with
- | TokSymbol (Some t) -> ("", t)
- | TokSymbol None -> err (bp, ep) Undefined_token
- | TokIdent t -> ("FIELD", t))
- | [< (t,_) = process_chars bp c >] -> t
+let parse_after_dot bp c = parser
+ | [< ' ('a'..'z' | 'A'..'Z' | '_' as c);
+ len = ident_tail (store 0 c) >] ->
+ ("FIELD", get_buff len)
+ (* Greek utf-8 letters [CE80-CEBF and CF80-CFBF] (CE=206; BF=191) *)
+ | [< ' ('\206' | '\207' as c1); ' ('\128'..'\191' as c2);
+ len = ident_tail (store (store 0 c1) c2) >] ->
+ ("FIELD", get_buff len)
+ (* utf-8 mathematical symbols have format E2 xx xx [E2=226] *)
+ | [< ''\226'; t = parse_226_tail
+ (progress_special '.' (Some !token_tree)) >] ep ->
+ (match t with
+ | TokSymbol (Some t) -> ("", t)
+ | TokSymbol None -> err (bp, ep) Undefined_token
+ | TokIdent t -> ("FIELD", t))
+ | [< (t,_) = process_chars bp c >] -> t
(* Parse a token in a char stream *)
@@ -410,7 +361,6 @@ let rec next_token = parser bp
(("METAIDENT", get_buff len), (bp,ep))
| [< ''.' as c; t = parse_after_dot bp c >] ep ->
comment_stop bp;
- if !Options.v7 & t=("",".") then between_com := true;
(t, (bp,ep))
| [< ' ('a'..'z' | 'A'..'Z' | '_' as c);
len = ident_tail (store 0 c) >] ep ->
@@ -433,20 +383,10 @@ let rec next_token = parser bp
(try ("", find_keyword id) with Not_found -> ("IDENT", id)),
(bp, ep))
(* iso 8859-1 accentuated letters *)
- | [< ' ('\192'..'\214' | '\216'..'\246' | '\248'..'\255' as c) ; s >] ->
- if !Options.v7 then
- begin
- match s with parser
- [< len = ident_tail (store 0 c) >] ep ->
- let id = get_buff len in
- comment_stop bp;
- (try ("", find_keyword id) with Not_found -> ("IDENT", id)), (bp, ep)
- end
- else
- begin
- match s with parser
- [< t = process_chars bp c >] -> comment_stop bp; t
- end
+ | [< ' ('\192'..'\214' | '\216'..'\246' | '\248'..'\255' as c) ;
+ t = process_chars bp c >] ->
+ comment_stop bp;
+ t
| [< ' ('0'..'9' as c); len = number (store 0 c) >] ep ->
comment_stop bp;
(("INT", get_buff len), (bp, ep))
@@ -534,3 +474,41 @@ let tparse (p_con, p_prm) =
else
(parser [< '(con, prm) when con = p_con && prm = p_prm >] -> prm)
i*)
+
+(* Terminal symbols interpretation *)
+
+let is_ident_not_keyword s =
+ match s.[0] with
+ | 'a'..'z' | 'A'..'Z' | '_' -> not (is_keyword s)
+ | _ -> false
+
+let is_number s =
+ match s.[0] with
+ | '0'..'9' -> true
+ | _ -> false
+
+let strip s =
+ let len =
+ let rec loop i len =
+ if i = String.length s then len
+ else if s.[i] == ' ' then loop (i + 1) len
+ else loop (i + 1) (len + 1)
+ in
+ loop 0 0
+ in
+ if len == String.length s then s
+ else
+ let s' = String.create len in
+ let rec loop i i' =
+ if i == String.length s then s'
+ else if s.[i] == ' ' then loop (i + 1) i'
+ else begin s'.[i'] <- s.[i]; loop (i + 1) (i' + 1) end
+ in
+ loop 0 0
+
+let terminal s =
+ let s = strip s in
+ if s = "" then failwith "empty token";
+ if is_ident_not_keyword s then ("IDENT", s)
+ else if is_number s then ("INT", s)
+ else ("", s)
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 2730cfea5..84f25ca5e 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -48,3 +48,5 @@ val com_state: unit -> com_state
val restore_com_state: com_state -> unit
val set_xml_output_comment : (string -> unit) -> unit
+
+val terminal : string -> string * string
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 90e93b832..0c864ba09 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -11,14 +11,13 @@
open Pp
open Util
open Names
+open Extend
open Libnames
open Rawterm
open Topconstr
-open Ast
open Genarg
open Tacexpr
open Ppextend
-open Extend
(* The lexer of Coq *)
@@ -65,8 +64,9 @@ struct
let weaken_entry e = Obj.magic e
end
+type entry_type = argument_type
type grammar_object = Gramobj.grammar_object
-type typed_entry = entry_type * grammar_object G.Entry.e
+type typed_entry = argument_type * grammar_object G.Entry.e
let in_typed_entry t e = (t,Gramobj.weaken_entry e)
let type_of_typed_entry (t,e) = t
let object_of_typed_entry (t,e) = e
@@ -311,10 +311,7 @@ module Prim =
let reference = make_gen_entry uprim rawwit_ref "reference"
(* parsed like ident but interpreted as a term *)
- let hyp = gec_gen rawwit_ident "hyp"
-
- (* synonym of hyp/ident (before semantics split) for v7 compatibility *)
- let var = gec_gen rawwit_ident "var"
+ let var = gec_gen rawwit_var "var"
let name = Gram.Entry.create "Prim.name"
let identref = Gram.Entry.create "Prim.identref"
@@ -328,12 +325,6 @@ module Prim =
let ne_string = Gram.Entry.create "Prim.ne_string"
- (* For old ast printer *)
- let astpat = Gram.Entry.create "Prim.astpat"
- let ast = Gram.Entry.create "Prim.ast"
- let astlist = Gram.Entry.create "Prim.astlist"
- let ast_eoi = eoi_entry ast
- let astact = Gram.Entry.create "Prim.astact"
end
@@ -380,8 +371,7 @@ module Tactic =
make_gen_entry utactic rawwit_constr_with_bindings "constr_with_bindings"
let bindings =
make_gen_entry utactic rawwit_bindings "bindings"
-(*v7*) let constrarg = make_gen_entry utactic rawwit_constr_may_eval "constrarg"
-(*v8*) let constr_may_eval = make_gen_entry utactic rawwit_constr_may_eval "constr_may_eval"
+ let constr_may_eval = make_gen_entry utactic rawwit_constr_may_eval "constr_may_eval"
let quantified_hypothesis =
make_gen_entry utactic rawwit_quant_hyp "quantified_hypothesis"
let int_or_var = make_gen_entry utactic rawwit_int_or_var "int_or_var"
@@ -391,13 +381,7 @@ module Tactic =
(* Main entries for ltac *)
let tactic_arg = Gram.Entry.create "tactic:tactic_arg"
- (* For v8: *)
let tactic_expr = Gram.Entry.create "tactic:tactic_expr"
- (* For v7: *)
- let tactic_expr2 = Gram.Entry.create "tactic:tactic_expr2"
- let tactic_expr3 = Gram.Entry.create "tactic:tactic_expr3"
- let tactic_expr4 = Gram.Entry.create "tactic:tactic_expr4"
- let tactic_expr5 = Gram.Entry.create "tactic:tactic_expr5"
let tactic_main_level = 5
let tactic = make_gen_entry utactic (rawwit_tactic tactic_main_level) "tactic"
@@ -422,32 +406,6 @@ module Vernac_ =
let vernac_eoi = eoi_entry vernac
end
-
-(* Prim is not re-initialized *)
-let reset_all_grammars () =
- let f = Gram.Unsafe.clear_entry in
- List.iter f
- [Constr.constr;Constr.operconstr;Constr.lconstr;Constr.annot;
- Constr.constr_pattern;Constr.lconstr_pattern];
- f Constr.ident; f Constr.global; f Constr.sort; f Constr.pattern;
- f Module.module_expr; f Module.module_type;
- f Tactic.simple_tactic;
- f Tactic.open_constr;
- f Tactic.constr_with_bindings;
- f Tactic.bindings;
- f Tactic.constrarg;
- f Tactic.quantified_hypothesis;
- f Tactic.int_or_var;
- f Tactic.red_expr;
- f Tactic.tactic_arg;
- f Tactic.tactic;
- f Vernac_.gallina;
- f Vernac_.gallina_ext;
- f Vernac_.command;
- f Vernac_.syntax;
- f Vernac_.vernac;
- Lexer.init()
-
let main_entry = Gram.Entry.create "vernac"
GEXTEND Gram
@@ -456,88 +414,6 @@ GEXTEND Gram
;
END
-(* Quotations *)
-
-open Prim
-open Constr
-open Tactic
-open Vernac_
-
-(* current file and toplevel/vernac.ml *)
-let globalizer = ref (fun x -> failwith "No globalizer")
-let set_globalizer f = globalizer := f
-
-let define_ast_quotation default s (e:Coqast.t G.Entry.e) =
- (if default then
- GEXTEND Gram
- ast: [ [ "<<"; c = e; ">>" -> c ] ];
- (* Uncomment this to keep compatibility with old grammar syntax
- constr: [ [ "<<"; c = e; ">>" -> c ] ];
- vernac: [ [ "<<"; c = e; ">>" -> c ] ];
- tactic: [ [ "<<"; c = e; ">>" -> c ] ];
- *)
- END);
- (GEXTEND Gram
- GLOBAL: ast constr command tactic;
- ast:
- [ [ "<:"; IDENT $s$; ":<"; c = e; ">>" -> c ] ];
- (* Uncomment this to keep compatibility with old grammar syntax
- constr:
- [ [ "<:"; IDENT $s$; ":<"; c = e; ">>" -> c ] ];
- command:
- [ [ "<:"; IDENT $s$; ":<"; c = e; ">>" -> c ] ];
- tactic:
- [ [ "<:"; IDENT $s$; ":<"; c = e; ">>" -> c ] ];
- *)
- END)
-
-(*
-let _ = define_ast_quotation false "ast" ast in ()
-*)
-
-let dynconstr = Gram.Entry.create "Constr.dynconstr"
-let dyncasespattern = Gram.Entry.create "Constr.dyncasespattern"
-
-GEXTEND Gram
- dynconstr:
- [ [ a = Constr.constr -> ConstrNode a
- (* For compatibility *)
- | "<<"; a = Constr.lconstr; ">>" -> ConstrNode a ] ]
- ;
- dyncasespattern: [ [ a = Constr.pattern -> CasesPatternNode a ] ];
-END
-
-(**********************************************************************)
-(* The following is to dynamically set the parser in Grammar actions *)
-(* and Syntax pattern, according to the universe of the rule defined *)
-
-type parser_type =
- | ConstrParser
- | CasesPatternParser
-
-let default_action_parser_ref = ref dynconstr
-
-let get_default_action_parser () = !default_action_parser_ref
-
-let entry_type_of_parser = function
- | ConstrParser -> Some ConstrArgType
- | CasesPatternParser -> failwith "entry_type_of_parser: cases_pattern, TODO"
-
-let parser_type_from_name = function
- | "constr" -> ConstrParser
- | "cases_pattern" -> CasesPatternParser
- | "tactic" -> assert false
- | "vernac" -> error "No longer supported"
- | s -> ConstrParser
-
-let set_default_action_parser = function
- | ConstrParser -> default_action_parser_ref := dynconstr
- | CasesPatternParser -> default_action_parser_ref := dyncasespattern
-
-let default_action_parser =
- Gram.Entry.of_parser "default_action_parser"
- (fun strm -> Gram.Entry.parse_token (get_default_action_parser ()) strm)
-
(**********************************************************************)
(* This determines (depending on the associativity of the current
level and on the expected associativity) if a reference to constr_n is
@@ -547,24 +423,9 @@ let default_action_parser =
translated in camlp4 into "constr" without level) or to another level
(to be translated into "constr LEVEL n") *)
-let assoc_level = function
- | Some Gramext.LeftA when !Options.v7 -> "L"
- | _ -> ""
-
-let constr_level = function
- | n,assoc -> (string_of_int n)^(assoc_level assoc)
-
-let constr_level2 = function
- | n,assoc -> (string_of_int n)^(assoc_level (Some assoc))
-
-let default_levels_v7 =
- [10,Gramext.RightA;
- 9,Gramext.RightA;
- 8,Gramext.RightA;
- 1,Gramext.RightA;
- 0,Gramext.RightA]
+let constr_level = string_of_int
-let default_levels_v8 =
+let default_levels =
[200,Gramext.RightA;
100,Gramext.RightA;
99,Gramext.RightA;
@@ -574,20 +435,16 @@ let default_levels_v8 =
1,Gramext.LeftA;
0,Gramext.RightA]
-let default_pattern_levels_v8 =
+let default_pattern_levels =
[10,Gramext.LeftA;
0,Gramext.RightA]
let level_stack =
- ref
- [if !Options.v7 then (default_levels_v7, default_levels_v7)
- else (default_levels_v8, default_pattern_levels_v8)]
+ ref [(default_levels, default_pattern_levels)]
(* At a same level, LeftA takes precedence over RightA and NoneA *)
(* In case, several associativity exists for a level, we make two levels, *)
(* first LeftA, then RightA and NoneA together *)
-exception Found of Gramext.g_assoc
-
open Ppextend
let admissible_assoc = function
@@ -610,48 +467,35 @@ let error_level_assoc p current expected =
pr_assoc expected ++ str " associative")
let find_position forpat other assoc lev =
- let default = if !Options.v7 then Some (10,Gramext.RightA) else None in
let ccurrent,pcurrent as current = List.hd !level_stack in
match lev with
| None ->
level_stack := current :: !level_stack;
None, (if other then assoc else None), None
| Some n ->
- if !Options.v7 & n = 8 & assoc = Some Gramext.LeftA then
- error "Left associativity not allowed at level 8";
- let after = ref default in
+ let after = ref None in
let rec add_level q = function
- | (p,_ as pa)::l when p > n -> pa :: add_level (Some pa) l
- | (p,a as pa)::l as l' when p = n ->
- if admissible_assoc (a,assoc) then raise (Found a);
- (* No duplication of levels in v8 *)
- if not !Options.v7 then error_level_assoc p a (out_some assoc);
- (* Maybe this was (p,Left) and p occurs a second time *)
- if a = Gramext.LeftA then
- match l with
- | (p,a)::_ when p = n -> raise (Found a)
- | _ -> after := Some pa; pa::(n,create_assoc assoc)::l
- else
- (* This was not (p,LeftA) hence assoc is RightA *)
- (after := q; (n,create_assoc assoc)::l')
- | l ->
- after := q; (n,create_assoc assoc)::l
+ | (p,_ as pa)::l when p > n -> pa :: add_level (Some p) l
+ | (p,a)::l when p = n ->
+ if admissible_assoc (a,assoc) then raise Exit;
+ error_level_assoc p a (out_some assoc)
+ | l -> after := q; (n,create_assoc assoc)::l
in
try
(* Create the entry *)
let updated =
- if forpat then (ccurrent, add_level default pcurrent)
- else (add_level default ccurrent, pcurrent) in
+ if forpat then (ccurrent, add_level None pcurrent)
+ else (add_level None ccurrent, pcurrent) in
level_stack := updated:: !level_stack;
let assoc = create_assoc assoc in
(if !after = None then Some Gramext.First
- else Some (Gramext.After (constr_level2 (out_some !after)))),
- Some assoc, Some (constr_level2 (n,assoc))
+ else Some (Gramext.After (constr_level (out_some !after)))),
+ Some assoc, Some (constr_level n)
with
- Found a ->
+ Exit ->
level_stack := current :: !level_stack;
(* Just inherit the existing associativity and name (None) *)
- Some (Gramext.Level (constr_level2 (n,a))), None, None
+ Some (Gramext.Level (constr_level n)), None, None
let remove_levels n =
level_stack := list_skipn n !level_stack
@@ -729,7 +573,7 @@ let compute_entry allow_create adjust forpat = function
| ETConstr (n,q) ->
(if forpat then weaken_entry Constr.pattern
else weaken_entry Constr.operconstr),
- (if forpat & !Options.v7 then None else adjust (n,q)), false
+ adjust (n,q), false
| ETIdent -> weaken_entry Constr.ident, None, false
| ETBigint -> weaken_entry Prim.bigint, None, false
| ETReference -> weaken_entry Constr.global, None, false
@@ -747,7 +591,7 @@ let compute_entry allow_create adjust forpat = function
(* This computes the name of the level where to add a new rule *)
let get_constr_entry forpat en =
match en with
- ETConstr(200,()) when not !Options.v7 & not forpat ->
+ ETConstr(200,()) when not forpat ->
snd (get_entry (get_univ "constr") "binder_constr"),
None,
false
@@ -756,25 +600,7 @@ let get_constr_entry forpat en =
(* This computes the name to give to a production knowing the name and
associativity of the level where it must be added *)
let get_constr_production_entry ass from forpat en =
- (* first 2 cases to help factorisation *)
- match en with
- | ETConstr (NumLevel 10,q) when !Options.v7 & not forpat ->
- weaken_entry Constr.lconstr, None, false
-(*
- | ETConstr (8,q) when !Options.v7 ->
- weaken_entry Constr.constr, None, false
-*)
- | _ -> compute_entry false (adjust_level ass from) forpat en
-
-let constr_prod_level assoc cur lev =
- if !Options.v7 then
- if cur then constr_level (lev,assoc) else
- match lev with
- | 4 when !Options.v7 -> "4L"
- | n -> string_of_int n
- else
- (* No duplication L/R of levels in v8 *)
- constr_level (lev,assoc)
+ compute_entry false (adjust_level ass from) forpat en
let is_self from e =
match from, e with
@@ -789,8 +615,7 @@ let is_self from e =
let is_binder_level from e =
match from, e with
ETConstr(200,()),
- ETConstr(NumLevel 200,(BorderProd(false,_)|InternalProd)) ->
- not !Options.v7
+ ETConstr(NumLevel 200,(BorderProd(false,_)|InternalProd)) -> true
| _ -> false
let rec symbol_of_production assoc from forpat typ =
@@ -814,4 +639,19 @@ let rec symbol_of_production assoc from forpat typ =
| (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj)
| (eobj,Some None,_) -> Gramext.Snext
| (eobj,Some (Some (lev,cur)),_) ->
- Gramext.Snterml (Gram.Entry.obj eobj,constr_prod_level assoc cur lev)
+ Gramext.Snterml (Gram.Entry.obj eobj,constr_level lev)
+
+let coerce_reference_to_id = function
+ | Ident (_,id) -> id
+ | Qualid (loc,_) ->
+ user_err_loc (loc, "coerce_reference_to_id",
+ str "This expression should be a simple identifier")
+
+let coerce_global_to_id = coerce_reference_to_id
+
+let coerce_to_id = function
+ | CRef (Ident (loc,id)) -> (loc,id)
+ | a -> user_err_loc
+ (constr_loc a,"coerce_to_id",
+ str "This expression should be a simple identifier")
+
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index a6aa7417e..87e0c24ba 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -11,13 +11,12 @@
open Util
open Names
open Rawterm
-open Ast
+open Extend
open Genarg
open Topconstr
open Tacexpr
open Vernacexpr
open Libnames
-open Extend
(* The lexer and parser of Coq. *)
@@ -31,16 +30,15 @@ type grammar_object
(* The type of typed grammar objects *)
type typed_entry
-val type_of_typed_entry : typed_entry -> Extend.entry_type
+type entry_type = argument_type
+
+val type_of_typed_entry : typed_entry -> entry_type
val object_of_typed_entry : typed_entry -> grammar_object Gram.Entry.e
val weaken_entry : 'a Gram.Entry.e -> grammar_object Gram.Entry.e
val get_constr_entry :
bool -> constr_entry -> grammar_object Gram.Entry.e * int option * bool
-val symbol_of_production : Gramext.g_assoc option -> constr_entry ->
- bool -> constr_production_entry -> Token.t Gramext.g_symbol
-
val grammar_extend :
grammar_object Gram.Entry.e -> Gramext.position option ->
(string option * Gramext.g_assoc option *
@@ -83,22 +81,6 @@ val create_generic_entry : string -> ('a, constr_expr,raw_tactic_expr) abstract_
val get_generic_entry : string -> grammar_object Gram.Entry.e
val get_generic_entry_type : string * gram_universe -> string -> Genarg.argument_type
-type parser_type =
- | ConstrParser
- | CasesPatternParser
-
-val entry_type_of_parser : parser_type -> entry_type option
-val parser_type_from_name : string -> parser_type
-
-(* Quotations in ast parser *)
-val define_ast_quotation : bool -> string -> (Coqast.t Gram.Entry.e) -> unit
-val set_globalizer : (constr_expr -> Coqast.t) -> unit
-
-(* The default parser for actions in grammar rules *)
-
-val default_action_parser : dynamic_grammar Gram.Entry.e
-val set_default_action_parser : parser_type -> unit
-
(* The main entry: reads an optional vernac command *)
val main_entry : (loc * vernac_expr) option Gram.Entry.e
@@ -124,13 +106,7 @@ module Prim :
val reference : reference Gram.Entry.e
val dirpath : dir_path Gram.Entry.e
val ne_string : string Gram.Entry.e
- val hyp : identifier Gram.Entry.e
- (* v7 only entries *)
- val astpat: typed_ast Gram.Entry.e
- val ast : Coqast.t Gram.Entry.e
- val astlist : Coqast.t list Gram.Entry.e
- val ast_eoi : Coqast.t Gram.Entry.e
- val var : identifier Gram.Entry.e
+ val var : identifier located Gram.Entry.e
end
module Constr :
@@ -164,8 +140,7 @@ module Tactic :
val casted_open_constr : open_constr_expr Gram.Entry.e
val constr_with_bindings : constr_expr with_bindings Gram.Entry.e
val bindings : constr_expr bindings Gram.Entry.e
-(*v7*) val constrarg : (constr_expr,reference) may_eval Gram.Entry.e
-(*v8*) val constr_may_eval : (constr_expr,reference) may_eval Gram.Entry.e
+ val constr_may_eval : (constr_expr,reference) may_eval Gram.Entry.e
val quantified_hypothesis : quantified_hypothesis Gram.Entry.e
val int_or_var : int or_var Gram.Entry.e
val red_expr : raw_red_expr Gram.Entry.e
@@ -176,12 +151,6 @@ module Tactic :
val tactic_main_level : int
val tactic : raw_tactic_expr Gram.Entry.e
val tactic_eoi : raw_tactic_expr Gram.Entry.e
-
- (* For v7 *)
- val tactic_expr2 : raw_tactic_expr Gram.Entry.e
- val tactic_expr3 : raw_tactic_expr Gram.Entry.e
- val tactic_expr4 : raw_tactic_expr Gram.Entry.e
- val tactic_expr5 : raw_tactic_expr Gram.Entry.e
end
module Vernac_ :
@@ -195,7 +164,10 @@ module Vernac_ :
val vernac_eoi : vernac_expr Gram.Entry.e
end
-val reset_all_grammars : unit -> unit
+(* Binding entry names to campl4 entries *)
+
+val symbol_of_production : Gramext.g_assoc option -> constr_entry ->
+ bool -> constr_production_entry -> Token.t Gramext.g_symbol
(* Registering/resetting the level of an entry *)
@@ -204,3 +176,7 @@ val find_position :
Gramext.position option * Gramext.g_assoc option * string option
val remove_levels : int -> unit
+
+val coerce_global_to_id : reference -> identifier
+
+val coerce_to_id : constr_expr -> identifier located
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index c47ad04c3..e6de302f6 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -9,381 +9,15 @@
(* $Id$ *)
(*i*)
-open Ast
open Util
open Pp
open Nametab
open Names
open Nameops
open Libnames
-open Coqast
open Ppextend
open Topconstr
open Term
open Pattern
(*i*)
-let latom = 0
-let lannot = 1
-let lprod = 8 (* not 1 because the scope extends to 8 on the right *)
-let llambda = 8 (* not 1 *)
-let lif = 8 (* not 1 *)
-let lletin = 8 (* not 1 *)
-let lcases = 1
-let larrow = 8
-let lcast = 9
-let lapp = 10
-let ltop = (8,E)
-
-let prec_less child (parent,assoc) = match assoc with
- | E -> child <= parent
- | L -> child < parent
- | Prec n -> child <= n
- | Any -> true
-
-let env_assoc_value v env =
- try List.nth env (v-1)
- with Not_found -> anomaly "Inconsistent environment for pretty-print rule"
-
-let decode_constrlist_value = function
- | CAppExpl (_,_,l) -> l
- | CApp (_,_,l) -> List.map fst l
- | _ -> anomaly "Ill-formed list argument of notation"
-
-let decode_patlist_value = function
- | CPatCstr (_,_,l) -> l
- | _ -> anomaly "Ill-formed list argument of notation"
-
-open Notation
-
-let rec print_hunk n decode pr env = function
- | UnpMetaVar (e,prec) -> pr (n,prec) (env_assoc_value e env)
- | UnpListMetaVar (e,prec,sl) ->
- prlist_with_sep (fun () -> prlist (print_hunk n decode pr env) sl)
- (pr (n,prec)) (decode (env_assoc_value e env))
- | UnpTerminal s -> str s
- | UnpBox (b,sub) -> ppcmd_of_box b (prlist (print_hunk n decode pr env) sub)
- | UnpCut cut -> ppcmd_of_cut cut
-
-let pr_notation_gen decode pr s env =
- let unpl, level = find_notation_printing_rule s in
- prlist (print_hunk level decode pr env) unpl, level
-
-let pr_notation = pr_notation_gen decode_constrlist_value
-let pr_patnotation = pr_notation_gen decode_patlist_value
-
-let pr_delimiters key strm =
- let left = "'"^key^":" and right = "'" in
- let lspace =
- if is_letter (left.[String.length left -1]) then str " " else mt () in
- let rspace =
- let c = right.[0] in
- if is_letter c or is_digit c or c = '\'' then str " " else mt () in
- str left ++ lspace ++ strm ++ rspace ++ str right
-
-open Rawterm
-
-let pr_opt pr = function
- | None -> mt ()
- | Some x -> spc () ++ pr x
-
-let pr_universe = Univ.pr_uni
-
-let pr_sort = function
- | RProp Term.Null -> str "Prop"
- | RProp Term.Pos -> str "Set"
- | RType u -> str "Type" ++ pr_opt pr_universe u
-
-let pr_explicitation = function
- | None -> mt ()
- | Some (_,ExplByPos n) -> int n ++ str "!"
- | Some (_,ExplByName n) -> anomaly "Argument made explicit by name"
-
-let pr_expl_args pr (a,expl) =
- pr_explicitation expl ++ pr (lapp,L) a
-
-let pr_opt_type pr = function
- | CHole _ -> mt ()
- | t -> str ":" ++ pr ltop t
-
-let pr_tight_coma () = str "," ++ cut ()
-
-let pr_located pr (loc,x) = pr x
-
-let pr_let_binder pr x a =
- hov 0 (hov 0 (pr_name x ++ brk(0,1) ++ str ":=") ++ brk(0,1) ++ pr ltop a)
-
-let pr_binder pr (nal,t) =
- hov 0 (
- prlist_with_sep pr_tight_coma (pr_located pr_name) nal ++
- pr_opt_type pr t)
-
-let pr_binders pr bl =
- hv 0 (prlist_with_sep pr_semicolon (pr_binder pr) bl)
-
-let pr_local_binder pr = function
- LocalRawAssum(nal,t) -> pr_binder pr (nal,t)
- | LocalRawDef((_,na),t) -> pr_let_binder pr na t
-
-let pr_local_binders pr bl =
- hv 0 (prlist_with_sep pr_semicolon (pr_local_binder pr) bl)
-
-let pr_global vars ref = pr_global_env vars ref
-
-let rec pr_lambda_tail pr bll = function
- | CLambdaN (_,bl,a) ->
- pr_lambda_tail pr (bll ++ pr_semicolon() ++ pr_binders pr bl) a
- | CLetIn (_,x,a,b) ->
- pr_lambda_tail pr (bll ++ pr_semicolon() ++ pr_let_binder pr (snd x) a) b
- | a ->
- bll, pr ltop a
-
-let rec pr_prod_tail pr bll = function
- | CProdN (_,bl,a) ->
- pr_prod_tail pr (bll ++ pr_semicolon () ++ pr_binders pr bl) a
- | a -> bll, pr ltop a
-
-let pr_recursive_decl pr id binders t c =
- pr_id id ++ binders ++
- brk (1,2) ++ str ": " ++ pr ltop t ++ str " :=" ++
- brk (1,2) ++ pr ltop c
-
-let split_lambda = function
- | CLambdaN (loc,[[na],t],c) -> (na,t,c)
- | CLambdaN (loc,([na],t)::bl,c) -> (na,t,CLambdaN(loc,bl,c))
- | CLambdaN (loc,(na::nal,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,t)::bl,c))
- | _ -> anomaly "ill-formed fixpoint body"
-
-let split_product = function
- | CArrow (loc,t,c) -> ((loc,Anonymous),t,c)
- | CProdN (loc,[[na],t],c) -> (na,t,c)
- | CProdN (loc,([na],t)::bl,c) -> (na,t,CProdN(loc,bl,c))
- | CProdN (loc,(na::nal,t)::bl,c) -> (na,t,CProdN(loc,(nal,t)::bl,c))
- | _ -> anomaly "ill-formed fixpoint body"
-
-let concat_binder na t = function
- | [] -> [[na],t]
- | (nal,u)::bl' as bl -> if t=u then (na::nal,t)::bl' else ([na],t)::bl
-
-let rec split_fix n typ def =
- if n = 0 then ([],typ,def)
- else
- let (na,_,def) = split_lambda def in
- let (_,t,typ) = split_product typ in
- let (bl,typ,def) = split_fix (n-1) typ def in
- (concat_binder na t bl,typ,def)
-
-let pr_fixdecl pr (id,n,bl,t,c) =
- pr_recursive_decl pr id
- (brk (1,2) ++ str "[" ++ pr_local_binders pr bl ++ str "]") t c
-
-let pr_cofixdecl pr (id,bl,t,c) =
- let b =
- if bl=[] then mt() else
- brk(1,2) ++ str"[" ++ pr_local_binders pr bl ++ str "]" in
- pr_recursive_decl pr id b t c
-
-let pr_recursive fix pr_decl id = function
- | [] -> anomaly "(co)fixpoint with no definition"
- | d1::dl ->
- hov 0 (
- str fix ++ spc () ++ pr_id id ++ brk (1,2) ++ str "{" ++
- (v 0 (
- (hov 0 (pr_decl d1)) ++
- (prlist (fun fix -> fnl () ++ hov 0 (str "with" ++ pr_decl fix))
- dl))) ++
- str "}")
-
-let pr_fix pr = pr_recursive "Fix" (pr_fixdecl pr)
-let pr_cofix pr = pr_recursive "CoFix" (pr_cofixdecl pr)
-
-let rec pr_arrow pr = function
- | CArrow (_,a,b) -> pr (larrow,L) a ++ cut () ++ str "->" ++ pr_arrow pr b
- | a -> pr (larrow,E) a
-
-let pr_annotation pr = function
- | None -> mt ()
- | Some t -> str "<" ++ pr ltop t ++ str ">" ++ brk (0,2)
-
-let rec pr_cases_pattern _inh = function
- | CPatAlias (_,p,x) ->
- pr_cases_pattern _inh p ++ spc () ++ str "as" ++ spc () ++ pr_id x
- | CPatCstr (_,c,[]) -> pr_reference c
- | CPatCstr (_,c,pl) ->
- hov 0 (
- str "(" ++ pr_reference c ++ spc () ++
- prlist_with_sep spc (pr_cases_pattern _inh) pl ++ str ")")
- | CPatAtom (_,Some c) -> pr_reference c
- | CPatAtom (_,None) -> str "_"
- | CPatOr (_,pl) ->
- str "(" ++
- hov 0 (prlist_with_sep pr_bar (pr_cases_pattern _inh) pl) ++
- str ")"
- | CPatNotation (_,"( _ )",[p]) ->
- str"("++ pr_cases_pattern _inh p ++ str")"
- | CPatNotation (_,s,env) -> fst (pr_patnotation pr_cases_pattern s env)
- | CPatNumeral (_,n) -> Bigint.pr_bigint n
- | CPatDelimiters (_,key,p) -> pr_delimiters key (pr_cases_pattern _inh p)
-
-let pr_cases_pattern = pr_cases_pattern (0,E) (* level unused *)
-
-let pr_eqn pr (_,patl,rhs) =
- hov 0 (
- prlist_with_sep spc pr_cases_pattern patl ++ spc () ++
- str "=>" ++
- brk (1,1) ++ pr ltop rhs) ++ spc ()
-
-let pr_cases pr (po,_) tml eqns =
- hov 0 (
- pr_annotation pr po ++
- hv 0 (
- hv 0 (
- str "Cases" ++ brk (1,2) ++
- prlist_with_sep spc (fun (tm,_) -> pr ltop tm) tml ++ spc() ++ str "of") ++ brk(1,2) ++
- prlist_with_sep (fun () -> str "| ") (pr_eqn pr) eqns ++
- str "end"))
-
-let pr_proj pr pr_app a f l =
- hov 0 (pr (latom,E) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")")
-
-let pr_explapp pr f l =
- hov 0 (
- str "!" ++ pr_reference f ++
- prlist (fun a -> brk (1,1) ++ pr (lapp,L) a) l)
-
-let pr_app pr a l =
- hov 0 (
- pr (lapp,L) a ++
- prlist (fun a -> brk (1,1) ++ pr_expl_args pr a) l)
-
-let rec pr inherited a =
- let (strm,prec) = match a with
- | CRef r -> pr_reference r, latom
- | CFix (_,id,fix) -> pr_fix pr (snd id) fix, latom
- | CCoFix (_,id,cofix) -> pr_cofix pr (snd id) cofix, latom
- | CArrow _ -> hv 0 (pr_arrow pr a), larrow
- | CProdN (_,bl,a) ->
- let bll, a = pr_prod_tail pr (mt()) a in
- hv 1 (
- hv 1 (str "(" ++ pr_binders pr bl ++ bll ++ str ")") ++
- brk (0,1) ++ a), lprod
- | CLambdaN (_,bl,a) ->
- let bll, a = pr_lambda_tail pr (mt()) a in
- hv 1 (
- hv 1 (str "[" ++ pr_binders pr bl ++ bll ++ str "]") ++
- brk (0,1) ++ a), llambda
- | CLetIn (_,x,a,b) ->
- let bll, b = pr_lambda_tail pr (mt()) b in
- hv 1 (
- hv 1 (str "[" ++ pr_let_binder pr (snd x) a ++ bll ++ str "]") ++
- brk (0,1) ++ b), lletin
- | CAppExpl (_,((* V7 don't know about projections *)_,f),l) ->
- pr_explapp pr f l, lapp
- | CApp (_,(_,a),l) ->
- pr_app pr a l, lapp
- | CCases (_,po,tml,eqns) ->
- pr_cases pr po tml eqns, lcases
- | COrderedCase (_,IfStyle,po,c,[b1;b2]) ->
- (* On force les parenthèses autour d'un "if" sous-terme (même si le
- parsing est lui plus tolérant) *)
- hov 0 (
- pr_annotation pr po ++
- hv 0 (
- str "if " ++ pr ltop c ++ spc () ++
- hov 0 (str "then" ++ brk (1,1) ++ pr ltop b1) ++ spc () ++
- hov 0 (str "else" ++ brk (1,1) ++ pr ltop b2))), lif
- | CLetTuple _ | CIf _ ->
- anomaly "Let tuple and If not supported in v7"
-
- | COrderedCase (_,(MatchStyle|RegularStyle as style),po,c,bl) ->
- hov 0 (
- hov 0 (
- pr_annotation pr po ++
- hov 0 (
- str (if style=RegularStyle then "Case" else "Match") ++
- brk (1,1) ++ pr ltop c ++ spc () ++
- str (if style=RegularStyle then "of" else "with") ++
- brk (1,3) ++
- fnl () ++ hov 0 (prlist (fun b -> pr ltop b ++ fnl ()) bl) ++
- str "end"))), lcases
- | COrderedCase (_,_,_,_,_) ->
- anomaly "malformed if or destructuring let"
- | CHole _ -> str "?", latom
-(*
- | CEvar (_,n) -> str "?" ++ int n, latom
-*)
- | CEvar (_,n) -> str (Evd.string_of_existential n), latom
- | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
- | CSort (_,s) -> pr_sort s, latom
- | CCast (_,a,_,b) ->
- hv 0 (pr (lcast,L) a ++ cut () ++ str "::" ++ pr (lcast,E) b), lcast
- | CNotation (_,"( _ )",[t]) ->
- str"("++ pr (max_int,E) t ++ str")", latom
- | CNotation (_,s,env) -> pr_notation pr s env
- | CNumeral (_,p) -> Bigint.pr_bigint p, latom
- | CDelimiters (_,sc,a) -> pr_delimiters sc (pr ltop a), latom
- | CDynamic _ -> str "<dynamic>", latom
- in
- if prec_less prec inherited then strm
- else str"(" ++ strm ++ str")"
-
-let pr_constr = pr ltop
-
-let pr_pattern = pr_constr
-
-let pr_qualid qid = str (string_of_qualid qid)
-
-open Rawterm
-
-let pr_arg pr x = spc () ++ pr x
-
-let pr_red_flag pr r =
- (if r.rBeta then pr_arg str "Beta" else mt ()) ++
- (if r.rIota then pr_arg str "Iota" else mt ()) ++
- (if r.rZeta then pr_arg str "Zeta" else mt ()) ++
- (if r.rConst = [] then
- if r.rDelta then pr_arg str "Delta"
- else mt ()
- else
- pr_arg str "Delta" ++ (if r.rDelta then str "-" else mt ()) ++
- hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]"))
-
-open Genarg
-
-let pr_occurrences prc (nl,c) = prlist (fun n -> int n ++ spc ()) nl ++ prc c
-
-let pr_red_expr (pr_constr,pr_ref) = function
- | Red false -> str "Red"
- | Hnf -> str "Hnf"
- | Simpl o -> str "Simpl" ++ pr_opt (pr_occurrences pr_constr) o
- | Cbv f ->
- if f = {rBeta=true;rIota=true;rZeta=true;rDelta=true;rConst=[]} then
- str "Compute"
- else
- hov 1 (str "Cbv" ++ spc () ++ pr_red_flag pr_ref f)
- | Lazy f ->
- hov 1 (str "Lazy" ++ spc () ++ pr_red_flag pr_ref f)
- | Unfold l ->
- hov 1 (str "Unfold" ++
- prlist (fun (nl,qid) ->
- prlist (pr_arg int) nl ++ spc () ++ pr_ref qid) l)
- | Fold l -> hov 1 (str "Fold" ++ prlist (pr_arg pr_constr) l)
- | Pattern l -> hov 1 (str "Pattern " ++ prlist (pr_occurrences pr_constr) l)
- | Red true -> error "Shouldn't be accessible from user"
- | ExtraRedExpr s -> str s
- | CbvVm -> str "vm_compute"
-
-
-let rec pr_may_eval pr pr2 = function
- | ConstrEval (r,c) ->
- hov 0
- (str "Eval" ++ brk (1,1) ++ pr_red_expr (pr,pr2) r ++
- spc () ++ str "in" ++ brk (1,1) ++ pr c)
- | ConstrContext ((_,id),c) ->
- hov 0
- (str "Inst " ++ brk (1,1) ++ pr_id id ++ spc () ++
- str "[" ++ pr c ++ str "]")
- | ConstrTypeOf c -> hov 0 (str "Check " ++ brk (1,1) ++ pr c)
- | ConstrTerm c -> pr c
-
-let pr_rawconstr c = pr_constr (Constrextern.extern_rawconstr Idset.empty c)
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index 3ca626121..5bbeecc2c 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -8,33 +8,3 @@
(*i $Id$ i*)
-open Pp
-open Environ
-open Term
-open Libnames
-open Pcoq
-open Rawterm
-open Extend
-open Coqast
-open Topconstr
-open Names
-open Util
-
-val split_fix : int -> constr_expr -> constr_expr ->
- (name located list * constr_expr) list * constr_expr * constr_expr
-
-val pr_global : Idset.t -> global_reference -> std_ppcmds
-
-val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
-val pr_qualid : qualid -> std_ppcmds
-val pr_red_expr :
- ('a -> std_ppcmds) * ('b -> std_ppcmds) ->
- ('a,'b) red_expr_gen -> std_ppcmds
-val pr_occurrences : ('a -> std_ppcmds) -> 'a occurrences -> std_ppcmds
-
-val pr_sort : rawsort -> std_ppcmds
-val pr_pattern : Tacexpr.pattern_expr -> std_ppcmds
-val pr_constr : constr_expr -> std_ppcmds
-val pr_cases_pattern : cases_pattern_expr -> std_ppcmds
-val pr_may_eval : ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('a,'b) may_eval -> std_ppcmds
-val pr_rawconstr : rawconstr -> std_ppcmds
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index d5c42a04d..9803c0031 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -12,7 +12,6 @@ open Pp
open Names
open Nameops
open Util
-open Extend
open Tacexpr
open Rawterm
open Topconstr
@@ -21,28 +20,21 @@ open Libnames
open Pattern
open Ppextend
-let pr_red_expr = Ppconstr.pr_red_expr
-let pr_may_eval = Ppconstr.pr_may_eval
-let pr_sort = Ppconstr.pr_sort
-let pr_global x =
- if Options.do_translate () then (* for pr_gen *)
- Ppconstrnew.pr_global Idset.empty x
- else
- Ppconstr.pr_global Idset.empty x
-let pr_opt = Ppconstr.pr_opt
-let pr_occurrences = Ppconstr.pr_occurrences
+let pr_red_expr = Ppconstrnew.pr_red_expr
+let pr_may_eval = Ppconstrnew.pr_may_eval
+let pr_sort = Ppconstrnew.pr_sort
+let pr_global x = Nametab.pr_global_env Idset.empty x
+let pr_opt = Ppconstrnew.pr_opt
type grammar_terminals = string option list
(* Extensions *)
-let prtac_tab_v7 = Hashtbl.create 17
let prtac_tab = Hashtbl.create 17
-let declare_extra_tactic_pprule for_v8 s (tags,prods) =
- Hashtbl.add prtac_tab_v7 (s,tags) prods;
- if for_v8 then Hashtbl.add prtac_tab (s,tags) prods
+let declare_extra_tactic_pprule (s,tags,prods) =
+ Hashtbl.add prtac_tab (s,tags) prods
-let exists_extra_tactic_pprule s tags = Hashtbl.mem prtac_tab_v7 (s,tags)
+let exists_extra_tactic_pprule s tags = Hashtbl.mem prtac_tab (s,tags)
type 'a raw_extra_genarg_printer =
(constr_expr -> std_ppcmds) ->
@@ -62,10 +54,9 @@ type 'a extra_genarg_printer =
(tolerability -> glob_tactic_expr -> std_ppcmds) ->
'a -> std_ppcmds
-let genarg_pprule_v7 = ref Stringmap.empty
let genarg_pprule = ref Stringmap.empty
-let declare_extra_genarg_pprule for_v8 (rawwit, f) (globwit, g) (wit, h) =
+let declare_extra_genarg_pprule (rawwit, f) (globwit, g) (wit, h) =
let s = match unquote wit with
| ExtraArgType s -> s
| _ -> error
@@ -74,9 +65,7 @@ let declare_extra_genarg_pprule for_v8 (rawwit, f) (globwit, g) (wit, h) =
let f prc prlc prtac x = f prc prlc prtac (out_gen rawwit x) in
let g prc prlc prtac x = g prc prlc prtac (out_gen globwit x) in
let h prc prlc prtac x = h prc prlc prtac (out_gen wit x) in
- genarg_pprule_v7 := Stringmap.add s (f,g,h) !genarg_pprule_v7;
- if for_v8 then
- genarg_pprule := Stringmap.add s (f,g,h) !genarg_pprule
+ genarg_pprule := Stringmap.add s (f,g,h) !genarg_pprule
let pr_arg pr x = spc () ++ pr x
@@ -92,14 +81,10 @@ let pr_and_short_name pr (c,_) = pr c
let pr_located pr (loc,x) = pr x
-let pr_ltac_constant sp = pr_qualid (Nametab.shortest_qualid_of_tactic sp)
-
let pr_evaluable_reference = function
| EvalVarRef id -> pr_id id
| EvalConstRef sp -> pr_global (Libnames.ConstRef sp)
-let pr_inductive ind = pr_global (Libnames.IndRef ind)
-
let pr_quantified_hypothesis = function
| AnonHyp n -> int n
| NamedHyp id -> pr_id id
@@ -116,12 +101,7 @@ let pr_bindings prc prlc = function
prlist_with_sep spc prc l
| ExplicitBindings l ->
brk (1,1) ++ str "with" ++ brk (1,1) ++
- prlist_with_sep spc
- (fun b -> if Options.do_translate () or not !Options.v7 then
- str"(" ++ pr_binding prlc b ++ str")"
- else
- pr_binding prc b)
- l
+ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
| NoBindings -> mt ()
let pr_bindings_no_with prc prlc = function
@@ -130,21 +110,11 @@ let pr_bindings_no_with prc prlc = function
prlist_with_sep spc prc l
| ExplicitBindings l ->
brk (1,1) ++
- prlist_with_sep spc
- (fun b -> if Options.do_translate () or not !Options.v7 then
- str"(" ++ pr_binding prlc b ++ str")"
- else
- pr_binding prc b)
- l
+ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
| NoBindings -> mt ()
let pr_with_bindings prc prlc (c,bl) =
- if Options.do_translate () then
- (* translator calls pr_with_bindings on rawconstr: we cast it! *)
- let bl' = Ppconstrnew.translate_with_bindings (fst (Obj.magic c) : rawconstr) bl in
- prc c ++ hv 0 (pr_bindings prc prlc bl')
- else
- prc c ++ hv 0 (pr_bindings prc prlc bl)
+ prc c ++ hv 0 (pr_bindings prc prlc bl)
let pr_with_constr prc = function
| None -> mt ()
@@ -154,111 +124,6 @@ let pr_with_names = function
| None -> mt ()
| Some ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
-let pr_hyp_location pr_id = function
- | id, _, (InHyp,_) -> spc () ++ pr_id id
- | id, _, (InHypTypeOnly,_) ->
- spc () ++ str "(Type of " ++ pr_id id ++ str ")"
- | id, _, _ -> error "Unsupported hyp location in v7"
-
-let pr_clause pr_id = function
- | [] -> mt ()
- | l -> spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l)
-
-let pr_clauses pr_id cls =
- match cls with
- { onhyps = Some l; onconcl = false } ->
- spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l)
- | { onhyps = Some []; onconcl = true } -> mt()
- | _ -> error "this clause has both hypothesis and conclusion"
-
-let pr_simple_clause pr_id = function
- | [] -> mt ()
- | l -> spc () ++
- hov 0 (str "in" ++ spc () ++ prlist_with_sep spc pr_id l)
-
-let pr_clause_pattern pr_id cls =
- pr_opt
- (prlist (fun (id,occs,_) ->
- prlist (pr_arg int) occs ++ spc () ++ pr_id id)) cls.onhyps ++
- if cls.onconcl then
- prlist (pr_arg int) cls.concl_occs ++ spc() ++ str"Goal"
- else mt()
-
-let pr_subterms pr occl =
- hov 0 (pr_occurrences pr occl ++ spc () ++ str "with")
-
-let pr_induction_arg prc = function
- | ElimOnConstr c -> prc c
- | ElimOnIdent (_,id) -> pr_id id
- | ElimOnAnonHyp n -> int n
-
-let pr_induction_kind = function
- | SimpleInversion -> str "Simple Inversion"
- | FullInversion -> str "Inversion"
- | FullInversionClear -> str "Inversion_clear"
-
-let pr_lazy lz = if lz then str "lazy " else mt ()
-
-let pr_match_pattern pr_pat = function
- | Term a -> pr_pat a
- | Subterm (None,a) -> str "[" ++ pr_pat a ++ str "]"
- | Subterm (Some id,a) -> pr_id id ++ str "[" ++ pr_pat a ++ str "]"
-
-let pr_match_hyps pr_pat = function
- | Hyp ((_,na),mp) -> pr_name na ++ str ":" ++ pr_match_pattern pr_pat mp
-
-let pr_match_rule m pr_pat pr = function
- | Pat ([],mp,t) when m ->
- str "[" ++ pr_match_pattern pr_pat mp ++ str "]"
- ++ spc () ++ str "->" ++ brk (1,2) ++ pr t
- | Pat (rl,mp,t) ->
- str "[" ++ prlist_with_sep pr_semicolon
- (pr_match_hyps pr_pat) rl ++ spc () ++
- str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++ str "]" ++
- spc () ++ str "->" ++ brk (1,2) ++ pr t
- | All t -> str "_" ++ spc () ++ str "->" ++ brk (1,2) ++ pr t
-
-let pr_funvar = function
- | None -> spc () ++ str "()"
- | Some id -> spc () ++ pr_id id
-
-let pr_let_clause k pr = function
- | ((_,id),None,t) -> hv 0(str k ++ pr_id id ++ str " =" ++ brk (1,1) ++ pr t)
- | ((_,id),Some c,t) -> str "TODO(LETCLAUSE)"
-
-let pr_let_clauses pr = function
- | hd::tl ->
- hv 0
- (pr_let_clause "Let " pr hd ++
- prlist (fun t -> spc () ++ pr_let_clause "And " pr t) tl)
- | [] -> anomaly "LetIn must declare at least one binding"
-
-let pr_rec_clause pr ((_,id),(l,t)) =
- pr_id id ++ prlist pr_funvar l ++ str "->" ++ spc () ++ pr t
-
-let pr_rec_clauses pr l =
- prlist_with_sep (fun () -> fnl () ++ str "And ") (pr_rec_clause pr) l
-
-let pr_hintbases = function
- | None -> spc () ++ str "with *"
- | Some [] -> mt ()
- | Some l ->
- spc () ++ str "with" ++ hv 0 (prlist (fun s -> spc () ++ str s) l)
-
-let pr_autoarg_adding = function
- | [] -> mt ()
- | l ->
- spc () ++ str "Adding [" ++
- hv 0 (prlist_with_sep spc pr_reference l) ++ str "]"
-
-let pr_autoarg_destructing = function
- | true -> spc () ++ str "Destructing"
- | false -> mt ()
-
-let pr_autoarg_usingTDB = function
- | true -> spc () ++ str "Using TDB"
- | false -> mt ()
-
let rec pr_raw_generic prc prlc prtac prref x =
match Genarg.genarg_tag x with
| BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false")
@@ -268,20 +133,18 @@ let rec pr_raw_generic prc prlc prtac prref x =
| PreIdentArgType -> pr_arg str (out_gen rawwit_pre_ident x)
| IntroPatternArgType -> pr_arg pr_intro_pattern
(out_gen rawwit_intro_pattern x)
- | IdentArgType -> pr_arg pr_id ((*Constrextern.v7_to_v8_id*) (out_gen rawwit_ident x))
- | HypArgType -> pr_arg
- (pr_located (fun id -> pr_id (Constrextern.v7_to_v8_id id))) (out_gen rawwit_var x)
+ | IdentArgType -> pr_arg pr_id (out_gen rawwit_ident x)
+ | VarArgType -> pr_arg (pr_located pr_id) (out_gen rawwit_var x)
| RefArgType -> pr_arg prref (out_gen rawwit_ref x)
| SortArgType -> pr_arg pr_sort (out_gen rawwit_sort x)
| ConstrArgType -> pr_arg prc (out_gen rawwit_constr x)
| ConstrMayEvalArgType ->
- pr_arg (pr_may_eval prc prref)
+ pr_arg (pr_may_eval prc prlc prref)
(out_gen rawwit_constr_may_eval x)
- | QuantHypArgType ->
+ | QuantVarArgType ->
pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x)
| RedExprArgType ->
- pr_arg (pr_red_expr
- (prc,prref)) (out_gen rawwit_red_expr x)
+ pr_arg (pr_red_expr (prc,prlc,prref)) (out_gen rawwit_red_expr x)
| TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (rawwit_tactic n) x)
| OpenConstrArgType b -> pr_arg prc (snd (out_gen (rawwit_open_constr_gen b) x))
| ConstrWithBindingsArgType ->
@@ -300,10 +163,7 @@ let rec pr_raw_generic prc prlc prtac prref x =
pr_raw_generic prc prlc prtac prref b)
x)
| ExtraArgType s ->
- let tab =
- if Options.do_translate() or not !Options.v7 then !genarg_pprule
- else !genarg_pprule_v7 in
- try pi1 (Stringmap.find s tab) prc prlc prtac x
+ try pi1 (Stringmap.find s !genarg_pprule) prc prlc prtac x
with Not_found -> str " [no printer for " ++ str s ++ str "] "
@@ -316,19 +176,20 @@ let rec pr_glob_generic prc prlc prtac x =
| PreIdentArgType -> pr_arg str (out_gen globwit_pre_ident x)
| IntroPatternArgType ->
pr_arg pr_intro_pattern (out_gen globwit_intro_pattern x)
- | IdentArgType -> pr_arg pr_id ((*Constrextern.v7_to_v8_id*) (out_gen globwit_ident x))
- | HypArgType -> pr_arg (pr_located (fun id -> pr_id (Constrextern.v7_to_v8_id id))) (out_gen globwit_var x)
+ | IdentArgType -> pr_arg pr_id (out_gen globwit_ident x)
+ | VarArgType -> pr_arg (pr_located pr_id) (out_gen globwit_var x)
| RefArgType -> pr_arg (pr_or_var (pr_located pr_global)) (out_gen globwit_ref x)
| SortArgType -> pr_arg pr_sort (out_gen globwit_sort x)
| ConstrArgType -> pr_arg prc (out_gen globwit_constr x)
| ConstrMayEvalArgType ->
- pr_arg (pr_may_eval prc
+ pr_arg (pr_may_eval prc prlc
(pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_constr_may_eval x)
- | QuantHypArgType ->
+ | QuantVarArgType ->
pr_arg pr_quantified_hypothesis (out_gen globwit_quant_hyp x)
| RedExprArgType ->
pr_arg (pr_red_expr
- (prc,pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_red_expr x)
+ (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference)))
+ (out_gen globwit_red_expr x)
| TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (globwit_tactic n) x)
| OpenConstrArgType b -> pr_arg prc (snd (out_gen (globwit_open_constr_gen b) x))
| ConstrWithBindingsArgType ->
@@ -347,10 +208,7 @@ let rec pr_glob_generic prc prlc prtac x =
pr_glob_generic prc prlc prtac b)
x)
| ExtraArgType s ->
- let tab =
- if Options.do_translate() or not !Options.v7 then !genarg_pprule
- else !genarg_pprule_v7 in
- try pi2 (Stringmap.find s tab) prc prlc prtac x
+ try pi2 (Stringmap.find s !genarg_pprule) prc prlc prtac x
with Not_found -> str " [no printer for " ++ str s ++ str "] "
open Closure
@@ -364,17 +222,18 @@ let rec pr_generic prc prlc prtac x =
| PreIdentArgType -> pr_arg str (out_gen wit_pre_ident x)
| IntroPatternArgType ->
pr_arg pr_intro_pattern (out_gen wit_intro_pattern x)
- | IdentArgType -> pr_arg pr_id (Constrextern.v7_to_v8_id (out_gen wit_ident x))
- | HypArgType -> pr_arg prc (out_gen wit_var x)
+ | IdentArgType -> pr_arg pr_id (out_gen wit_ident x)
+ | VarArgType -> pr_arg pr_id (out_gen wit_var x)
| RefArgType -> pr_arg pr_global (out_gen wit_ref x)
| SortArgType -> pr_arg prc (Term.mkSort (out_gen wit_sort x))
| ConstrArgType -> pr_arg prc (out_gen wit_constr x)
| ConstrMayEvalArgType ->
pr_arg prc (out_gen wit_constr_may_eval x)
- | QuantHypArgType ->
+ | QuantVarArgType ->
pr_arg pr_quantified_hypothesis (out_gen wit_quant_hyp x)
| RedExprArgType ->
- pr_arg (pr_red_expr (prc,pr_evaluable_reference)) (out_gen wit_red_expr x)
+ pr_arg (pr_red_expr (prc,prlc,pr_evaluable_reference))
+ (out_gen wit_red_expr x)
| TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (wit_tactic n) x)
| OpenConstrArgType b -> pr_arg prc (snd (out_gen (wit_open_constr_gen b) x))
| ConstrWithBindingsArgType ->
@@ -393,10 +252,7 @@ let rec pr_generic prc prlc prtac x =
pr_generic prc prlc prtac b)
x)
| ExtraArgType s ->
- let tab =
- if Options.do_translate() or not !Options.v7 then !genarg_pprule
- else !genarg_pprule_v7 in
- try pi3 (Stringmap.find s tab) prc prlc prtac x
+ try pi3 (Stringmap.find s !genarg_pprule) prc prlc prtac x
with Not_found -> str " [no printer for " ++ str s ++ str "]"
let rec pr_tacarg_using_rule pr_gen = function
@@ -408,388 +264,17 @@ let rec pr_tacarg_using_rule pr_gen = function
let surround p = hov 1 (str"(" ++ p ++ str")")
let pr_extend_gen prgen lev s l =
- let tab =
- if Options.do_translate() or not !Options.v7 then prtac_tab
- else prtac_tab_v7
- in
try
let tags = List.map genarg_tag l in
- (* Hack pour les syntaxes changeant non uniformément en passant a la V8 *)
- let s =
- let n = String.length s in
- if Options.do_translate() & n > 2 & String.sub s (n-2) 2 = "v7"
- then String.sub s 0 (n-2) ^ "v8"
- else s in
- let (lev',pl) = Hashtbl.find tab (s,tags) in
+ let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in
let p = pr_tacarg_using_rule prgen (pl,l) in
if lev' > lev then surround p else p
with Not_found ->
str s ++ prlist prgen l ++ str " (* Generic printer *)"
-let make_pr_tac (pr_tac_level,pr_constr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend) =
-
-let pr_bindings = pr_bindings pr_constr pr_constr in
-let pr_with_bindings = pr_with_bindings pr_constr pr_constr in
-let pr_eliminator cb = str "using" ++ pr_arg (pr_with_bindings) cb in
-let pr_intarg n = spc () ++ int n in
-
- (* Printing tactics as arguments *)
-let rec pr_atom0 = function
- | TacIntroPattern [] -> str "Intros"
- | TacIntroMove (None,None) -> str "Intro"
- | TacAssumption -> str "Assumption"
- | TacAnyConstructor None -> str "Constructor"
- | TacTrivial (Some []) -> str "Trivial"
- | TacAuto (None,Some []) -> str "Auto"
- | TacAutoTDB None -> str "AutoTDB"
- | TacDestructConcl -> str "DConcl"
- | TacReflexivity -> str "Reflexivity"
- | t -> str "(" ++ pr_atom1 t ++ str ")"
-
- (* Main tactic printer *)
-and pr_atom1 = function
- | TacExtend (_,s,l) -> pr_extend pr_constr pr_constr pr_tac_level 1 s l
- | TacAlias (_,s,l,_) ->
- pr_extend pr_constr pr_constr pr_tac_level 1 s (List.map snd l)
-
- (* Basic tactics *)
- | TacIntroPattern [] as t -> pr_atom0 t
- | TacIntroPattern (_::_ as p) ->
- hov 1 (str "Intros" ++ spc () ++ prlist_with_sep spc pr_intro_pattern p)
- | TacIntrosUntil h ->
- hv 1 (str "Intros until" ++ pr_arg pr_quantified_hypothesis h)
- | TacIntroMove (None,None) as t -> pr_atom0 t
- | TacIntroMove (Some id1,None) -> str "Intro " ++ pr_id id1
- | TacIntroMove (ido1,Some (_,id2)) ->
- hov 1
- (str "Intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++ pr_id id2)
- | TacAssumption as t -> pr_atom0 t
- | TacExact c -> hov 1 (str "Exact" ++ pr_arg pr_constr c)
- | TacExactNoCheck c -> hov 1 (str "Exact_no_check" ++ pr_arg pr_constr c)
- | TacApply cb -> hov 1 (str "Apply" ++ spc () ++ pr_with_bindings cb)
- | TacElim (cb,cbo) ->
- hov 1 (str "Elim" ++ pr_arg pr_with_bindings cb ++
- pr_opt pr_eliminator cbo)
- | TacElimType c -> hov 1 (str "ElimType" ++ pr_arg pr_constr c)
- | TacCase cb -> hov 1 (str "Case" ++ spc () ++ pr_with_bindings cb)
- | TacCaseType c -> hov 1 (str "CaseType" ++ pr_arg pr_constr c)
- | TacFix (ido,n) -> hov 1 (str "Fix" ++ pr_opt pr_id ido ++ pr_intarg n)
- | TacMutualFix (id,n,l) ->
- hov 1 (str "Fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc () ++
- hov 0 (str "with" ++ brk (1,1) ++
- prlist_with_sep spc
- (fun (id,n,c) ->
- spc () ++ pr_id id ++ pr_intarg n ++ pr_arg pr_constr c)
- l))
- | TacCofix ido -> hov 1 (str "Cofix" ++ pr_opt pr_id ido)
- | TacMutualCofix (id,l) ->
- hov 1 (str "Cofix" ++ spc () ++ pr_id id ++ spc () ++
- hov 0 (str "with" ++ brk (1,1) ++
- prlist (fun (id,c) -> spc () ++ pr_id id ++ pr_arg pr_constr c)
- l))
- | TacCut c -> hov 1 (str "Cut" ++ pr_arg pr_constr c)
- | TacTrueCut (Anonymous,c) ->
- hov 1 (str "Assert" ++ pr_arg pr_constr c)
- | TacTrueCut (Name id,c) ->
- hov 1 (str "Assert" ++ spc () ++ pr_id id ++ str ":" ++ pr_constr c)
- | TacForward (false,na,c) ->
- hov 1 (str "Assert" ++ pr_arg pr_name na ++ str ":=" ++ pr_constr c)
- | TacForward (true,na,c) ->
- hov 1 (str "Pose" ++ pr_arg pr_name na ++ str ":=" ++ pr_constr c)
- | TacGeneralize l ->
- hov 1 (str "Generalize" ++ spc () ++ prlist_with_sep spc pr_constr l)
- | TacGeneralizeDep c ->
- hov 1 (str "Generalize" ++ spc () ++ str "Dependent" ++ spc () ++
- pr_constr c)
- | TacLetTac (na,c,cl) ->
- let pcl = match cl with
- {onhyps=None;onconcl=true;concl_occs=[]} -> mt()
- | _ -> pr_clauses pr_ident cl in
- hov 1 (str "LetTac" ++ spc () ++ pr_name na ++ str ":=" ++
- pr_constr c ++ pcl)
- (* | TacInstantiate (n,c,ConclLocation ()) ->
- hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c )
- | TacInstantiate (n,c,HypLocation (id,hloc)) ->
- hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c ++
- str "in" ++ pr_hyp_location pr_ident (id,[],(hloc,ref None)))
- *)
- (* Derived basic tactics *)
- | TacSimpleInduction (h,_) ->
- hov 1 (str "Induction" ++ pr_arg pr_quantified_hypothesis h)
- | TacNewInduction (h,e,(ids,_)) ->
- hov 1 (str "NewInduction" ++ spc () ++ pr_induction_arg pr_constr h ++
- pr_opt pr_eliminator e ++ pr_with_names ids)
- | TacSimpleDestruct h ->
- hov 1 (str "Destruct" ++ pr_arg pr_quantified_hypothesis h)
- | TacNewDestruct (h,e,(ids,_)) ->
- hov 1 (str "NewDestruct" ++ spc () ++ pr_induction_arg pr_constr h ++
- pr_opt pr_eliminator e ++ pr_with_names ids)
- | TacDoubleInduction (h1,h2) ->
- hov 1
- (str "Double Induction" ++
- pr_arg pr_quantified_hypothesis h1 ++
- pr_arg pr_quantified_hypothesis h2)
- | TacDecomposeAnd c ->
- hov 1 (str "Decompose Record" ++ pr_arg pr_constr c)
- | TacDecomposeOr c ->
- hov 1 (str "Decompose Sum" ++ pr_arg pr_constr c)
- | TacDecompose (l,c) ->
- hov 1 (str "Decompose" ++ spc () ++
- hov 0 (str "[" ++ prlist_with_sep spc pr_ind l
- ++ str "]" ++ pr_arg pr_constr c))
- | TacSpecialize (n,c) ->
- hov 1 (str "Specialize" ++ pr_opt int n ++ pr_with_bindings c)
- | TacLApply c ->
- hov 1 (str "LApply" ++ pr_constr c)
-
- (* Automation tactics *)
- | TacTrivial (Some []) as x -> pr_atom0 x
- | TacTrivial db -> hov 0 (str "Trivial" ++ pr_hintbases db)
- | TacAuto (None,Some []) as x -> pr_atom0 x
- | TacAuto (n,db) ->
- hov 0 (str "Auto" ++ pr_opt (pr_or_var int) n ++ pr_hintbases db)
- | TacAutoTDB None as x -> pr_atom0 x
- | TacAutoTDB (Some n) -> hov 0 (str "AutoTDB" ++ spc () ++ int n)
- | TacDestructHyp (true,(_,id)) -> hov 0 (str "CDHyp" ++ spc () ++ pr_id id)
- | TacDestructHyp (false,(_,id)) -> hov 0 (str "DHyp" ++ spc () ++ pr_id id)
- | TacDestructConcl as x -> pr_atom0 x
- | TacSuperAuto (n,l,b1,b2) ->
- hov 1 (str "SuperAuto" ++ pr_opt int n ++ pr_autoarg_adding l ++
- pr_autoarg_destructing b1 ++ pr_autoarg_usingTDB b2)
- | TacDAuto (n,p) ->
- hov 1 (str "Auto" ++ pr_opt (pr_or_var int) n ++ str "Decomp" ++ pr_opt int p)
-
- (* Context management *)
- | TacClear (keep,l) ->
- hov 1 (str "Clear" ++ spc () ++ (if keep then str "- " else mt ()) ++
- prlist_with_sep spc pr_ident l)
- | TacClearBody l ->
- hov 1 (str "ClearBody" ++ spc () ++ prlist_with_sep spc pr_ident l)
- | TacMove (b,id1,id2) ->
- (* Rem: only b = true is available for users *)
- assert b;
- hov 1
- (str "Move" ++ brk (1,1) ++ pr_ident id1 ++ spc () ++
- str "after" ++ brk (1,1) ++ pr_ident id2)
- | TacRename (id1,id2) ->
- hov 1
- (str "Rename" ++ brk (1,1) ++ pr_ident id1 ++ spc () ++
- str "into" ++ brk (1,1) ++ pr_ident id2)
-
- (* Constructors *)
- | TacLeft l -> hov 1 (str "Left" ++ pr_bindings l)
- | TacRight l -> hov 1 (str "Right" ++ pr_bindings l)
- | TacSplit (_,l) -> hov 1 (str "Split" ++ pr_bindings l)
- | TacAnyConstructor (Some t) ->
- hov 1 (str "Constructor" ++ pr_arg (pr_tac_level (0,E)) t)
- | TacAnyConstructor None as t -> pr_atom0 t
- | TacConstructor (n,l) ->
- hov 1 (str "Constructor" ++ pr_or_metaid pr_intarg n ++ pr_bindings l)
-
- (* Conversion *)
- | TacReduce (r,h) ->
- hov 1 (pr_red_expr (pr_constr,pr_cst) r ++ pr_clauses pr_ident h)
- | TacChange (occl,c,h) ->
- hov 1 (str "Change" ++ pr_opt (pr_subterms pr_constr) occl ++
- brk (1,1) ++ pr_constr c ++ pr_clauses pr_ident h)
-
- (* Equivalence relations *)
- | TacReflexivity as x -> pr_atom0 x
- | TacSymmetry cls -> str "Symmetry " ++ pr_clauses pr_ident cls
- | TacTransitivity c -> str "Transitivity" ++ pr_arg pr_constr c
-
- (* Equality and inversion *)
- | TacInversion (DepInversion (k,c,ids),hyp) ->
- hov 1 (str "Dependent " ++ pr_induction_kind k ++
- pr_quantified_hypothesis hyp ++
- pr_with_names ids ++ pr_with_constr pr_constr c)
- | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
- hov 1 (pr_induction_kind k ++ spc () ++
- pr_quantified_hypothesis hyp ++
- pr_with_names ids ++ pr_simple_clause pr_ident cl)
- | TacInversion (InversionUsing (c,cl),hyp) ->
- hov 1 (str "Inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++
- str "using" ++ spc () ++ pr_constr c ++
- pr_simple_clause pr_ident cl)
-
-and pr_tactic_seq_body tl =
- hv 0 (str "[ " ++
- prlist_with_sep (fun () -> spc () ++ str "| ") prtac tl ++ str " ]")
-
- (* Strictly closed atomic tactic expressions *)
-and pr0 = function
- | TacFirst tl -> str "First" ++ spc () ++ pr_tactic_seq_body tl
- | TacSolve tl -> str "Solve" ++ spc () ++ pr_tactic_seq_body tl
- | TacId "" -> str "Idtac"
- | TacFail (ArgArg 0,"") -> str "Fail"
- | TacAtom (_,t) -> pr_atom0 t
- | TacArg c -> pr_tacarg c
- | t -> str "(" ++ prtac t ++ str ")"
-
- (* Semi-closed atomic tactic expressions *)
-and pr1 = function
- | TacAtom (_,t) -> pr_atom1 t
- | TacId s -> str "Idtac \"" ++ str s ++ str "\""
- | TacFail (ArgArg 0,s) -> str "Fail \"" ++ str s ++ str "\""
- | TacFail (n,"") -> str "Fail " ++ pr_or_var int n
- | TacFail (n,s) -> str "Fail " ++ pr_or_var int n ++ str " \"" ++ str s ++ str "\""
- | t -> pr0 t
-
- (* Orelse tactic expressions (printed as if parsed associating on the right
- though the semantics is purely associative) *)
-and pr2 = function
- | TacOrelse (t1,t2) ->
- hov 1 (pr1 t1 ++ str " Orelse" ++ brk (1,1) ++ pr3 t2)
- | TacAtom (_,TacAlias (_,s,l,_)) ->
- pr_extend pr_constr pr_constr pr_tac_level 2 s (List.map snd l)
- | t -> pr1 t
-
- (* Non closed prefix tactic expressions *)
-and pr3 = function
- | TacTry t -> hov 1 (str "Try" ++ spc () ++ pr3 t)
- | TacDo (n,t) -> hov 1 (str "Do " ++ pr_or_var int n ++ spc () ++ pr3 t)
- | TacRepeat t -> hov 1 (str "Repeat" ++ spc () ++ pr3 t)
- | TacProgress t -> hov 1 (str "Progress" ++ spc () ++ pr3 t)
- | TacInfo t -> hov 1 (str "Info" ++ spc () ++ pr3 t)
- | TacAtom (_,TacAlias (_,s,l,_)) ->
- pr_extend pr_constr pr_constr pr_tac_level 3 s (List.map snd l)
- | t -> pr2 t
-
-and pr4 = function
- | TacAtom (_,TacAlias (_,s,l,_)) ->
- pr_extend pr_constr pr_constr pr_tac_level 4 s (List.map snd l)
- | t -> pr3 t
-
- (* THEN and THENS tactic expressions (printed as if parsed
- associating on the left though the semantics is purely associative) *)
-and pr5 = function
- | TacThens (t,tl) ->
- hov 1 (pr5 t ++ str ";" ++ spc () ++ pr_tactic_seq_body tl)
- | TacThen (t1,t2) ->
- hov 1 (pr5 t1 ++ str ";" ++ spc () ++ pr4 t2)
- | TacAtom (_,TacAlias (_,s,l,_)) ->
- pr_extend pr_constr pr_constr pr_tac_level 5 s (List.map snd l)
- | t -> pr4 t
-
- (* Ltac tactic expressions *)
-and pr6 = function
- |(TacAtom _
- | TacThen _
- | TacThens _
- | TacFirst _
- | TacSolve _
- | TacTry _
- | TacOrelse _
- | TacDo _
- | TacRepeat _
- | TacProgress _
- | TacId _
- | TacFail _
- | TacInfo _) as t -> pr5 t
-
- | TacAbstract (t,None) -> str "Abstract " ++ pr6 t
- | TacAbstract (t,Some s) ->
- hov 0
- (str "Abstract " ++ pr6 t ++ spc () ++ str "using" ++ spc () ++ pr_id s)
- | TacLetRecIn (l,t) ->
- hv 0
- (str "Rec " ++ pr_rec_clauses prtac l ++
- spc () ++ str "In" ++ fnl () ++ prtac t)
- | TacLetIn (llc,u) ->
- v 0
- (hv 0 (pr_let_clauses pr_tacarg0 llc ++ spc () ++ str "In") ++ fnl () ++ prtac u)
- | TacMatch (lz,t,lrul) ->
- hov 0 (pr_lazy lz ++ str "Match" ++ spc () ++ pr6 t ++ spc()
- ++ str "With"
- ++ prlist
- (fun r -> fnl () ++ str "|" ++ spc () ++
- pr_match_rule true pr_pat prtac r)
- lrul)
- | TacMatchContext (lz,lr,lrul) ->
- hov 0 (pr_lazy lz ++
- str (if lr then "Match Reverse Context With" else "Match Context With")
- ++ prlist
- (fun r -> fnl () ++ str "|" ++ spc () ++
- pr_match_rule false pr_pat prtac r)
- lrul)
- | TacFun (lvar,body) ->
- hov 0 (str "Fun" ++
- prlist pr_funvar lvar ++ spc () ++ str "->" ++ spc () ++ prtac body)
-
- | TacArg c -> pr_tacarg c
-
-and pr_tacarg0 = function
- | TacDynamic (_,t) -> str ("<dynamic ["^(Dyn.tag t)^"]>")
- | MetaIdArg (_,s) -> str ("$" ^ s)
- | IntroPattern ipat -> pr_intro_pattern ipat
- | TacVoid -> str "()"
- | Reference r -> pr_ref r
- | ConstrMayEval (ConstrTerm c) -> str "'" ++ pr_constr c
- | ConstrMayEval c -> pr_may_eval pr_constr pr_cst c
- | Integer n -> int n
- | TacFreshId sopt -> str "FreshId" ++ pr_opt qstring sopt
- | TacExternal _ -> failwith "Not supported in v7 syntax"
- | (TacCall _ | Tacexp _) as t -> str "(" ++ pr_tacarg1 t ++ str ")"
-
-and pr_tacarg1 = function
- | TacCall (_,f,l) ->
- hov 0 (pr_ref f ++ spc () ++ prlist_with_sep spc pr_tacarg0 l)
- | Tacexp t -> pr_tac_level (6,E) t
- | t -> pr_tacarg0 t
-
-and pr_tacarg x = pr_tacarg1 x
-
-and prtac x = pr6 x
-
-and prtac_level (n,p) =
- let n = match p with E -> n | L -> n-1 | Prec n -> n | Any -> 6 in
- match n with
- | 0 -> pr0
- | 1 -> pr1
- | 2 -> pr2
- | 3 -> pr3
- | 4 -> pr4
- | 5 -> pr5
- | 6 -> pr6
- | _ -> anomaly "Unknown tactic level"
-
-in (prtac_level,pr_match_rule false pr_pat (pr_tac_level (6,E)))
-
let pr_raw_extend prc prlc prtac =
pr_extend_gen (pr_raw_generic prc prlc prtac Ppconstrnew.pr_reference)
let pr_glob_extend prc prlc prtac =
pr_extend_gen (pr_glob_generic prc prlc prtac)
let pr_extend prc prlc prtac =
pr_extend_gen (pr_generic prc prlc prtac)
-
-let pr_and_constr_expr pr (c,_) = pr c
-
-let rec glob_printers =
- (pr_glob_tactic_level,
- pr_and_constr_expr Printer.pr_rawterm,
- Printer.pr_pattern,
- pr_or_var (pr_and_short_name pr_evaluable_reference),
- pr_or_var pr_inductive,
- pr_or_var (pr_located pr_ltac_constant),
- pr_located pr_id,
- pr_glob_extend)
-
-and pr_glob_tactic_level n (t:glob_tactic_expr) =
- fst (make_pr_tac glob_printers) n t
-
-and pr_glob_match_context t =
- snd (make_pr_tac glob_printers) t
-
-let (pr_tactic_level,_) =
- make_pr_tac
- (pr_glob_tactic_level,
- Printer.prterm,
- Printer.pr_pattern,
- pr_evaluable_reference,
- pr_inductive,
- pr_ltac_constant,
- pr_id,
- pr_extend)
-
-let pr_glob_tactic = pr_glob_tactic_level (6,E)
-let pr_tactic = pr_tactic_level (6,E)
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index bd42a1ffe..fa835fff1 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -20,7 +20,6 @@ open Ppextend
val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
val pr_or_metaid : ('a -> std_ppcmds) -> 'a or_metaid -> std_ppcmds
val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
-val pr_located : ('a -> std_ppcmds) -> 'a Util.located -> std_ppcmds
type 'a raw_extra_genarg_printer =
(constr_expr -> std_ppcmds) ->
@@ -42,7 +41,6 @@ type 'a extra_genarg_printer =
(* if the boolean is false then the extension applies only to old syntax *)
val declare_extra_genarg_pprule :
- bool ->
('c raw_abstract_argument_type * 'c raw_extra_genarg_printer) ->
('a glob_abstract_argument_type * 'a glob_extra_genarg_printer) ->
('b closed_abstract_argument_type * 'b extra_genarg_printer) -> unit
@@ -50,26 +48,11 @@ val declare_extra_genarg_pprule :
type grammar_terminals = string option list
(* if the boolean is false then the extension applies only to old syntax *)
-val declare_extra_tactic_pprule : bool -> string ->
- argument_type list * (int * grammar_terminals) -> unit
+val declare_extra_tactic_pprule :
+ string * argument_type list * (int * grammar_terminals) -> unit
val exists_extra_tactic_pprule : string -> argument_type list -> bool
-val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
-
-val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
- ('a,'b) match_rule -> std_ppcmds
-
-val pr_glob_tactic : glob_tactic_expr -> std_ppcmds
-
-val pr_tactic : Proof_type.tactic_expr -> std_ppcmds
-
-val pr_glob_generic:
- (rawconstr_and_expr -> std_ppcmds) ->
- (rawconstr_and_expr -> std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
- glob_generic_argument -> std_ppcmds
-
val pr_raw_generic :
(constr_expr -> std_ppcmds) ->
(constr_expr -> std_ppcmds) ->
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 5092601fb..76c87f2c8 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -58,8 +58,7 @@ let print_impl_args_by_name = function
str" are implicit" ++ fnl()
let print_impl_args l =
- if !Options.v7 then print_impl_args_by_pos (positions_of_implicits l)
- else print_impl_args_by_name (List.filter is_status_implicit l)
+ print_impl_args_by_name (List.filter is_status_implicit l)
(*********************)
(** Printing Scopes *)
@@ -183,8 +182,7 @@ let pr_located_qualid = function
| VarRef _ -> "Variable" in
str ref_str ++ spc () ++ pr_sp (Nametab.sp_of_global ref)
| Syntactic kn ->
- str (if !Options.v7 then "Syntactic Definition" else "Notation") ++
- spc () ++ pr_sp (Nametab.sp_of_syntactic_definition kn)
+ str "Notation" ++ spc () ++ pr_sp (Nametab.sp_of_syntactic_definition kn)
| Dir dir ->
let s,dir = match dir with
| DirOpenModule (dir,_) -> "Open Module", dir
@@ -269,13 +267,7 @@ let assumptions_for_print lna =
(* *)
let print_params env params =
- if params = [] then
- (mt ())
- else
- if !Options.v7 then
- (str "[" ++ pr_rel_context env params ++ str "]" ++ brk(1,2))
- else
- (pr_rel_context env params ++ brk(1,2))
+ if params = [] then mt () else pr_rel_context env params ++ brk(1,2)
let print_constructors envpar names types =
let pc =
@@ -356,9 +348,8 @@ let print_inductive sp = (print_mutual sp)
let print_syntactic_def sep kn =
let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn in
let c = Syntax_def.search_syntactic_definition dummy_loc kn in
- (str (if !Options.v7 then "Syntactic Definition " else "Notation ")
- ++ pr_qualid qid ++ str sep ++
- Constrextern.without_symbols pr_rawterm c ++ fnl ())
+ str "Notation " ++ pr_qualid qid ++ str sep ++
+ Constrextern.without_symbols pr_rawterm c ++ fnl ()
let print_leaf_entry with_values sep ((sp,kn as oname),lobj) =
let tag = object_tag lobj in
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 355bf6c94..a87415d95 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -18,11 +18,7 @@ open Sign
open Environ
open Global
open Declare
-open Coqast
-open Ast
-open Termast
open Libnames
-open Extend
open Nametab
open Ppconstr
open Evd
@@ -33,97 +29,25 @@ open Pfedit
let emacs_str s = if !Options.print_emacs then s else ""
(**********************************************************************)
-(* Old Ast printing *)
-
-let constr_syntax_universe = "constr"
-(* This is starting precedence for printing constructions or tactics *)
-(* Level 9 means no parentheses except for applicative terms (at level 10) *)
-let constr_initial_prec_v7 = Some (9,Ppextend.L)
-let constr_initial_prec = Some (200,Ppextend.E)
-
-let dfltpr ast = (str"#GENTERM " ++ print_ast ast);;
-
-let global_const_name kn =
- try pr_global Idset.empty (ConstRef kn)
- with Not_found -> (* May happen in debug *)
- (str ("CONST("^(string_of_con kn)^")"))
-
-let global_var_name id =
- try pr_global Idset.empty (VarRef id)
- with Not_found -> (* May happen in debug *)
- (str ("SECVAR("^(string_of_id id)^")"))
-
-let global_ind_name (kn,tyi) =
- try pr_global Idset.empty (IndRef (kn,tyi))
- with Not_found -> (* May happen in debug *)
- (str ("IND("^(string_of_kn kn)^","^(string_of_int tyi)^")"))
-
-let global_constr_name ((kn,tyi),i) =
- try pr_global Idset.empty (ConstructRef ((kn,tyi),i))
- with Not_found -> (* May happen in debug *)
- (str ("CONSTRUCT("^(string_of_kn kn)^","^(string_of_int tyi)
- ^","^(string_of_int i)^")"))
-
-let globpr gt = match gt with
- | Nvar(_,s) -> (pr_id s)
- | Node(_,"EVAR", [Num (_,ev)]) -> (str ("?" ^ (string_of_int ev)))
- | Node(_,"CONST",[ConPath(_,sl)]) ->
- global_const_name sl
- | Node(_,"SECVAR",[Nvar(_,s)]) ->
- global_var_name s
- | Node(_,"MUTIND",[Path(_,sl); Num(_,tyi)]) ->
- global_ind_name (sl, tyi)
- | Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) ->
- global_constr_name ((sl, tyi), i)
- | Dynamic(_,d) ->
- if (Dyn.tag d) = "constr" then (str"<dynamic [constr]>")
- else dfltpr gt
- | gt -> dfltpr gt
-
-
-let wrap_exception = function
- Anomaly (s1,s2) ->
- warning ("Anomaly ("^s1^")"); pp s2;
- str"<PP error: non-printable term>"
- | Failure _ | UserError _ | Not_found ->
- str"<PP error: non-printable term>"
- | s -> raise s
-
-let gentermpr_fail gt =
- let prec =
- if !Options.v7 then constr_initial_prec_v7 else constr_initial_prec in
- Esyntax.genprint globpr constr_syntax_universe prec gt
-
-let gentermpr gt =
- try gentermpr_fail gt
- with s -> wrap_exception s
-
-(**********************************************************************)
(* Generic printing: choose old or new printers *)
(* [at_top] means ids of env must be avoided in bound variables *)
-let gentermpr_core at_top env t =
- if !Options.v7 then gentermpr (Termast.ast_of_constr at_top env t)
- else Ppconstrnew.pr_lconstr (Constrextern.extern_constr at_top env t)
-let gentypepr_core at_top env t =
- if !Options.v7 then gentermpr (Termast.ast_of_constr at_top env t)
- else Ppconstrnew.pr_lconstr (Constrextern.extern_type at_top env t)
+let prterm_core at_top env t =
+ Ppconstrnew.pr_lconstr (Constrextern.extern_constr at_top env t)
+let prtype_core at_top env t =
+ Ppconstrnew.pr_lconstr (Constrextern.extern_type at_top env t)
let pr_cases_pattern t =
- if !Options.v7 then gentermpr (Termast.ast_of_cases_pattern t)
- else Ppconstrnew.pr_cases_pattern
- (Constrextern.extern_cases_pattern Idset.empty t)
+ Ppconstrnew.pr_cases_pattern (Constrextern.extern_cases_pattern Idset.empty t)
let pr_pattern_env tenv env t =
- if !Options.v7 then gentermpr (Termast.ast_of_pattern tenv env t)
- else Ppconstrnew.pr_constr
- (Constrextern.extern_pattern tenv env t)
+ Ppconstrnew.pr_constr (Constrextern.extern_pattern tenv env t)
(**********************************************************************)
(* Derived printers *)
-let prterm_env_at_top env = gentermpr_core true env
-let prterm_env env = gentermpr_core false env
-let prtype_env_at_top env = gentypepr_core true env
-let prtype_env env = gentypepr_core false env
+let prterm_env_at_top env = prterm_core true env
+let prterm_env env = prterm_core false env
+let prtype_env_at_top env = prtype_core true env
+let prtype_env env = prtype_core false env
let prjudge_env env j =
(prterm_env env j.uj_val, prterm_env env j.uj_type)
@@ -134,13 +58,11 @@ let prjudge j = prjudge_env (Global.env()) j
let _ = Termops.set_print_constr prterm_env
-(*let _ = Tactic_debug.set_pattern_printer pr_pattern_env*)
-
let pr_constant env cst = prterm_env env (mkConst cst)
let pr_existential env ev = prterm_env env (mkEvar ev)
let pr_inductive env ind = prterm_env env (mkInd ind)
let pr_constructor env cstr = prterm_env env (mkConstruct cstr)
-let pr_global = pr_global Idset.empty
+let pr_global = pr_global_env Idset.empty
let pr_evaluable_reference ref =
let ref' = match ref with
| EvalConstRef const -> ConstRef const
@@ -148,8 +70,7 @@ let pr_evaluable_reference ref =
pr_global ref'
let pr_rawterm t =
- if !Options.v7 then gentermpr (Termast.ast_of_rawconstr t)
- else Ppconstrnew.pr_lconstr (Constrextern.extern_rawconstr Idset.empty t)
+ Ppconstrnew.pr_lconstr (Constrextern.extern_rawconstr Idset.empty t)
open Pattern
@@ -197,16 +118,11 @@ let pr_named_context env ne_context =
let pr_rel_context env rel_context =
let rec prec env = function
| [] -> (mt ())
- | [b] ->
- if !Options.v7 then pr_rel_decl env b
- else str "(" ++ pr_rel_decl env b ++ str")"
+ | [b] -> str "(" ++ pr_rel_decl env b ++ str")"
| b::rest ->
let pb = pr_rel_decl env b in
let penvtl = prec (push_rel b env) rest in
- if !Options.v7 then
- (pb ++ str";" ++ spc () ++ penvtl)
- else
- (str "(" ++ pb ++ str")" ++ spc () ++ penvtl)
+ str "(" ++ pb ++ str")" ++ spc () ++ penvtl
in
hov 0 (prec env (List.rev rel_context))
@@ -367,74 +283,13 @@ let pr_nth_open_subgoal n =
(* Elementary tactics *)
-let pr_prim_rule_v7 = function
- | Intro id ->
- str"Intro " ++ pr_id id
-
- | Intro_replacing id ->
- (str"intro replacing " ++ pr_id id)
-
- | Cut (b,id,t) ->
- if b then
- (str"Assert " ++ print_constr t)
- else
- (str"Cut " ++ print_constr t ++ str ";[Intro " ++ pr_id id ++ str "|Idtac]")
-
- | FixRule (f,n,[]) ->
- (str"Fix " ++ pr_id f ++ str"/" ++ int n)
-
- | FixRule (f,n,others) ->
- let rec print_mut = function
- | (f,n,ar)::oth ->
- pr_id f ++ str"/" ++ int n ++ str" : " ++ print_constr ar ++ print_mut oth
- | [] -> mt () in
- (str"Fix " ++ pr_id f ++ str"/" ++ int n ++
- str" with " ++ print_mut others)
-
- | Cofix (f,[]) ->
- (str"Cofix " ++ pr_id f)
-
- | Cofix (f,others) ->
- let rec print_mut = function
- | (f,ar)::oth ->
- (pr_id f ++ str" : " ++ print_constr ar ++ print_mut oth)
- | [] -> mt () in
- (str"Cofix " ++ pr_id f ++ str" with " ++ print_mut others)
-
- | Refine c ->
- str(if occur_meta c then "Refine " else "Exact ") ++
- Constrextern.with_meta_as_hole print_constr c
-
- | Convert_concl (c,_) ->
- (str"Change " ++ print_constr c)
-
- | Convert_hyp (id,None,t) ->
- (str"Change " ++ print_constr t ++ spc () ++ str"in " ++ pr_id id)
-
- | Convert_hyp (id,Some c,t) ->
- (str"Change " ++ print_constr c ++ spc () ++ str"in "
- ++ pr_id id ++ str" (Type of " ++ pr_id id ++ str ")")
-
- | Thin ids ->
- (str"Clear " ++ prlist_with_sep pr_spc pr_id ids)
-
- | ThinBody ids ->
- (str"ClearBody " ++ prlist_with_sep pr_spc pr_id ids)
-
- | Move (withdep,id1,id2) ->
- (str (if withdep then "Dependent " else "") ++
- str"Move " ++ pr_id id1 ++ str " after " ++ pr_id id2)
-
- | Rename (id1,id2) ->
- (str "Rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
-
let print_constr8 t =
Ppconstrnew.pr_constr (Constrextern.extern_constr false (Global.env()) t)
let print_lconstr8 t =
Ppconstrnew.pr_lconstr (Constrextern.extern_constr false (Global.env()) t)
-let pr_prim_rule_v8 = function
+let pr_prim_rule = function
| Intro id ->
str"intro " ++ pr_id id
@@ -494,6 +349,3 @@ let pr_prim_rule_v8 = function
| Rename (id1,id2) ->
(str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
-
-let pr_prim_rule t =
- if! Options.v7 then pr_prim_rule_v7 t else pr_prim_rule_v8 t
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 9a5e43feb..d28b36924 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -30,95 +30,6 @@ let anti loc x =
in
<:expr< $anti:e$ >>
-(* [mlexpr_of_ast] contributes to translate g_*.ml4 files into g_*.ppo *)
-(* This is where $id's (and macros) in ast are translated in ML variables *)
-(* which will bind their actual ast value *)
-
-let rec mlexpr_of_ast = function
- | Coqast.Nmeta (loc, id) -> anti loc id
- | Coqast.Id (loc, id) when is_meta id -> <:expr< Coqast.Id loc $anti loc id$ >>
- | Coqast.Node (_, "$VAR", [Coqast.Nmeta (loc, x)]) ->
- <:expr< let s = $anti loc x$ in
- if String.length s > 0 && String.sub s 0 1 = "$" then
- failwith "Wrong ast: $VAR should not be bound to a meta variable"
- else
- Coqast.Nvar loc (Names.id_of_string s) >>
- | Coqast.Node (_, "$PATH", [Coqast.Nmeta (loc, x)]) ->
- <:expr< Coqast.Path loc $anti loc x$ >>
- | Coqast.Node (_, "$ID", [Coqast.Nmeta (loc, x)]) ->
- <:expr< Coqast.Id loc $anti loc x$ >>
- | Coqast.Node (_, "$STR", [Coqast.Nmeta (loc, x)]) ->
- <:expr< Coqast.Str loc $anti loc x$ >>
-(* Obsolète
- | Coqast.Node _ "$SLAM" [Coqast.Nmeta loc idl; y] ->
- <:expr<
- List.fold_right (Pcoq.slam_ast loc) $anti loc idl$ $mlexpr_of_ast y$ >>
-*)
- | Coqast.Node (loc, "$ABSTRACT", [Coqast.Str (_, s); x; y]) ->
- let x = mlexpr_of_ast x in
- let y = mlexpr_of_ast y in
- <:expr< Ast.abstract_binders_ast loc $str:s$ $x$ $y$ >>
- | Coqast.Node (loc, nn, al) ->
- let e = expr_list_of_ast_list al in
- <:expr< Coqast.Node loc $str:nn$ $e$ >>
- | Coqast.Nvar (loc, id) ->
- <:expr< Coqast.Nvar loc (Names.id_of_string $str:Names.string_of_id id$) >>
- | Coqast.Slam (loc, None, a) ->
- <:expr< Coqast.Slam loc None $mlexpr_of_ast a$ >>
- | Coqast.Smetalam (loc, s, a) ->
- <:expr<
- match $anti loc s$ with
- [ Coqast.Nvar _ id -> Coqast.Slam loc (Some id) $mlexpr_of_ast a$
- | Coqast.Nmeta _ s -> Coqast.Smetalam loc s $mlexpr_of_ast a$
- | _ -> failwith "Slam expects a var or a metavar" ] >>
- | Coqast.Slam (loc, Some s, a) ->
- let se = <:expr< Names.id_of_string $str:Names.string_of_id s$ >> in
- <:expr< Coqast.Slam loc (Some $se$) $mlexpr_of_ast a$ >>
- | Coqast.Num (loc, i) -> <:expr< Coqast.Num loc $int:string_of_int i$ >>
- | Coqast.Id (loc, id) -> <:expr< Coqast.Id loc $str:id$ >>
- | Coqast.Str (loc, str) -> <:expr< Coqast.Str loc $str:str$ >>
- | Coqast.Path (loc, kn) ->
- let l,a = Libnames.decode_kn kn in
- let mlexpr_of_modid id =
- <:expr< Names.id_of_string $str:string_of_id id$ >> in
- let e = List.map mlexpr_of_modid (repr_dirpath l) in
- let e = expr_list_of_var_list e in
- <:expr< Coqast.Path loc (Libnames.encode_kn (Names.make_dirpath $e$)
- (Names.id_of_string $str:Names.string_of_id a$)) >>
- | Coqast.ConPath (loc, kn) ->
- let l,a = Libnames.decode_con kn in
- let mlexpr_of_modid id =
- <:expr< Names.id_of_string $str:string_of_id id$ >> in
- let e = List.map mlexpr_of_modid (repr_dirpath l) in
- let e = expr_list_of_var_list e in
- <:expr< Coqast.Path loc (Libnames.encode_kn (Names.make_dirpath $e$)
- (Names.id_of_string $str:Names.string_of_id a$)) >>
- | Coqast.Dynamic (_, _) ->
- failwith "Q_Coqast: dynamic: not implemented"
-
-and expr_list_of_ast_list al =
- List.fold_right
- (fun a e2 -> match a with
- | (Coqast.Node (_, "$LIST", [Coqast.Nmeta (locv, pv)])) ->
- let e1 = anti locv pv in
- let loc = (fst(MLast.loc_of_expr e1), snd(MLast.loc_of_expr e2)) in
- if e2 = (let loc = dummy_loc in <:expr< [] >>)
- then <:expr< $e1$ >>
- else <:expr< ( $lid:"@"$ $e1$ $e2$) >>
- | _ ->
- let e1 = mlexpr_of_ast a in
- let loc = (fst(MLast.loc_of_expr e1), snd(MLast.loc_of_expr e2)) in
- <:expr< [$e1$ :: $e2$] >> )
- al (let loc = dummy_loc in <:expr< [] >>)
-
-and expr_list_of_var_list sl =
- let loc = dummy_loc in
- List.fold_right
- (fun e1 e2 ->
- let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in
- <:expr< [$e1$ :: $e2$] >>)
- sl <:expr< [] >>
-
(* We don't give location for tactic quotation! *)
let loc = dummy_loc
@@ -173,12 +84,12 @@ let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident)
let mlexpr_of_occs = mlexpr_of_list mlexpr_of_int
let mlexpr_of_hyp_location = function
- | id, occs, (Tacexpr.InHyp,_) ->
- <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, (Tacexpr.InHyp, ref None)) >>
- | id, occs, (Tacexpr.InHypTypeOnly,_) ->
- <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, (Tacexpr.InHypTypeOnly, ref None)) >>
- | id, occs, (Tacexpr.InHypValueOnly,_) ->
- <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, (Tacexpr.InHypValueOnly,ref None)) >>
+ | id, occs, Tacexpr.InHyp ->
+ <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, Tacexpr.InHyp) >>
+ | id, occs, Tacexpr.InHypTypeOnly ->
+ <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, Tacexpr.InHypTypeOnly) >>
+ | id, occs, Tacexpr.InHypValueOnly ->
+ <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, Tacexpr.InHypValueOnly) >>
let mlexpr_of_clause cl =
<:expr< {Tacexpr.onhyps=
@@ -187,13 +98,6 @@ let mlexpr_of_clause cl =
Tacexpr.onconcl= $mlexpr_of_bool cl.Tacexpr.onconcl$;
Tacexpr.concl_occs= $mlexpr_of_occs cl.Tacexpr.concl_occs$} >>
-(*
-let mlexpr_of_red_mode = function
- | Closure.UNIFORM -> <:expr< Closure.UNIFORM >>
- | Closure.SIMPL -> <:expr< Closure.SIMPL >>
- | Closure.WITHBACK -> <:expr< Closure.WITHBACK >>
-*)
-
let mlexpr_of_red_flags {
Rawterm.rBeta = bb;
Rawterm.rIota = bi;
@@ -226,7 +130,6 @@ let rec mlexpr_of_constr = function
| Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
| Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >>
| Topconstr.CCases (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
- | Topconstr.COrderedCase (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO"
| Topconstr.CHole loc -> <:expr< Topconstr.CHole $dloc$ >>
| Topconstr.CNotation(_,ntn,l) ->
<:expr< Topconstr.CNotation $dloc$ $mlexpr_of_string ntn$
@@ -268,9 +171,9 @@ let rec mlexpr_of_argtype loc = function
| Genarg.PreIdentArgType -> <:expr< Genarg.PreIdentArgType >>
| Genarg.IntroPatternArgType -> <:expr< Genarg.IntroPatternArgType >>
| Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >>
- | Genarg.HypArgType -> <:expr< Genarg.HypArgType >>
+ | Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
| Genarg.StringArgType -> <:expr< Genarg.StringArgType >>
- | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>
+ | Genarg.QuantVarArgType -> <:expr< Genarg.QuantVarArgType >>
| Genarg.OpenConstrArgType b -> <:expr< Genarg.OpenConstrArgType $mlexpr_of_bool b$ >>
| Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >>
| Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >>
@@ -409,18 +312,18 @@ let rec mlexpr_of_atomic_tactic = function
<:expr< Tacexpr.TacLetTac $na$ $mlexpr_of_constr c$ $cl$ >>
(* Derived basic tactics *)
- | Tacexpr.TacSimpleInduction (h,_) ->
- <:expr< Tacexpr.TacSimpleInduction ($mlexpr_of_quantified_hypothesis h$,ref []) >>
+ | Tacexpr.TacSimpleInduction h ->
+ <:expr< Tacexpr.TacSimpleInduction ($mlexpr_of_quantified_hypothesis h$) >>
| Tacexpr.TacNewInduction (c,cbo,ids) ->
let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
- let ids = mlexpr_of_option mlexpr_of_intro_pattern (fst ids) in
- <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ ($ids$,ref [])>>
+ let ids = mlexpr_of_option mlexpr_of_intro_pattern ids in
+ <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ $ids$>>
| Tacexpr.TacSimpleDestruct h ->
<:expr< Tacexpr.TacSimpleDestruct $mlexpr_of_quantified_hypothesis h$ >>
| Tacexpr.TacNewDestruct (c,cbo,ids) ->
let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
- let ids = mlexpr_of_option mlexpr_of_intro_pattern (fst ids) in
- <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ ($ids$,ref []) >>
+ let ids = mlexpr_of_option mlexpr_of_intro_pattern ids in
+ <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ $ids$ >>
(* Context management *)
| Tacexpr.TacClear (b,l) ->
@@ -551,14 +454,6 @@ and mlexpr_of_tactic_arg = function
<:expr< Tacexpr.Reference $mlexpr_of_reference r$ >>
| _ -> failwith "mlexpr_of_tactic_arg: TODO"
-let f e =
- let ee s =
- mlexpr_of_ast (Pcoq.Gram.Entry.parse e
- (Pcoq.Gram.parsable (Stream.of_string s)))
- in
- let ep s = patt_of_expr (ee s) in
- Quotation.ExAst (ee, ep)
-
let fconstr e =
let ee s =
mlexpr_of_constr (Pcoq.Gram.Entry.parse e
@@ -578,6 +473,4 @@ let ftac e =
let _ =
Quotation.add "constr" (fconstr Pcoq.Constr.constr_eoi);
Quotation.add "tactic" (ftac Pcoq.Tactic.tactic_eoi);
-(* Quotation.add "vernac" (f Pcoq.Vernac_.vernac_eoi);*)
-(* Quotation.add "ast" (f Pcoq.Prim.ast_eoi);*)
Quotation.default := "constr"
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index 991982211..16943d925 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -66,3 +66,39 @@ let mlexpr_of_string s = <:expr< $str:s$ >>
let mlexpr_of_option f = function
| None -> <:expr< None >>
| Some e -> <:expr< Some $f e$ >>
+
+open Vernacexpr
+open Pcoq
+open Genarg
+
+let rec interp_entry_name loc s =
+ let l = String.length s in
+ if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then
+ let t, g = interp_entry_name loc (String.sub s 3 (l-8)) in
+ List1ArgType t, <:expr< Gramext.Slist1 $g$ >>
+ else if l > 5 & String.sub s (l-5) 5 = "_list" then
+ let t, g = interp_entry_name loc (String.sub s 0 (l-5)) in
+ List0ArgType t, <:expr< Gramext.Slist0 $g$ >>
+ else if l > 4 & String.sub s (l-4) 4 = "_opt" then
+ let t, g = interp_entry_name loc (String.sub s 0 (l-4)) in
+ OptArgType t, <:expr< Gramext.Sopt $g$ >>
+ else
+ let s = if s = "hyp" then "var" else s in
+ let t, se =
+ match Pcoq.entry_type (Pcoq.get_univ "prim") s with
+ | Some _ as x -> x, <:expr< Prim. $lid:s$ >>
+ | None ->
+ match Pcoq.entry_type (Pcoq.get_univ "constr") s with
+ | Some _ as x -> x, <:expr< Constr. $lid:s$ >>
+ | None ->
+ match Pcoq.entry_type (Pcoq.get_univ "tactic") s with
+ | Some _ as x -> x, <:expr< Tactic. $lid:s$ >>
+ | None -> None, <:expr< $lid:s$ >> in
+ let t =
+ match t with
+ | Some t -> t
+ | None ->
+(* Pp.warning_with Pp_control.err_ft
+ ("Unknown primitive grammar entry: "^s);*)
+ ExtraArgType s
+ in t, <:expr< Gramext.Snterm (Pcoq.Gram.Entry.obj $se$) >>
diff --git a/parsing/q_util.mli b/parsing/q_util.mli
index 8ed0f9d21..4418c6376 100644
--- a/parsing/q_util.mli
+++ b/parsing/q_util.mli
@@ -28,3 +28,4 @@ val mlexpr_of_string : string -> MLast.expr
val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr
+val interp_entry_name : Util.loc -> string -> Pcoq.entry_type * MLast.expr
diff --git a/parsing/search.ml b/parsing/search.ml
index 82829337a..42b5cef5c 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -17,7 +17,6 @@ open Rawterm
open Declarations
open Libobject
open Declare
-open Coqast
open Environ
open Pattern
open Matching
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index a8e47aa9b..4601b0db4 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -120,34 +120,13 @@ let rec make_tags loc = function
<:expr< [ $t$ :: $l$ ] >>
| _::l -> make_tags loc l
-let make_one_printing_rule (pt,e) =
+let make_one_printing_rule se (pt,e) =
let level = mlexpr_of_int 0 in (* only level 0 supported here *)
let loc = MLast.loc_of_expr e in
let prods = mlexpr_of_list mlexpr_terminals_of_grammar_production pt in
- <:expr< ($make_tags loc pt$, ($level$, $prods$)) >>
+ <:expr< ($se$, $make_tags loc pt$, ($level$, $prods$)) >>
-let make_printing_rule = mlexpr_of_list make_one_printing_rule
-
-let new_tac_ext (s,cl) =
- (String.lowercase s, List.map
- (fun (l,e) ->
- (List.map (function
- | TacTerm s -> TacTerm (String.lowercase s)
- | t -> t) l,
- e))
- cl)
-
-let declare_tactic_v7 loc s cl =
- let pp = make_printing_rule cl in
- let gl = mlexpr_of_clause cl in
- let se = mlexpr_of_string s in
- <:str_item<
- declare
- open Pcoq;
- Egrammar.extend_tactic_grammar $se$ $gl$;
- List.iter (Pptactic.declare_extra_tactic_pprule False $se$) $pp$;
- end
- >>
+let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se)
let rec contains_epsilon = function
| List0ArgType _ -> true
@@ -165,81 +144,41 @@ let is_atomic = function
| _ -> []
let declare_tactic loc s cl =
- let (s',cl') = new_tac_ext (s,cl) in
- let pp' = make_printing_rule cl' in
- let gl' = mlexpr_of_clause cl' in
- let se' = mlexpr_of_string s' in
- let pp = make_printing_rule cl in
+ let se = mlexpr_of_string s in
+ let pp = make_printing_rule se cl in
let gl = mlexpr_of_clause cl in
let hide_tac (p,e) =
(* reste a definir les fonctions cachees avec des noms frais *)
- let stac = "h_"^s' in
+ let stac = "h_"^s in
let e =
make_fun
<:expr<
- Refiner.abstract_extended_tactic $mlexpr_of_string s'$ $make_args p$ $make_eval_tactic e p$
+ Refiner.abstract_extended_tactic $mlexpr_of_string s$ $make_args p$ $make_eval_tactic e p$
>>
p in
<:str_item< value $lid:stac$ = $e$ >>
in
- let hidden = if List.length cl = 1 then List.map hide_tac cl' else [] in
+ let hidden = if List.length cl = 1 then List.map hide_tac cl else [] in
let atomic_tactics =
mlexpr_of_list mlexpr_of_string
- (List.flatten (List.map (fun (al,_) -> is_atomic al) cl')) in
+ (List.flatten (List.map (fun (al,_) -> is_atomic al) cl)) in
<:str_item<
declare
open Pcoq;
declare $list:hidden$ end;
try
- let _=Refiner.add_tactic $se'$ (fun [ $list:make_clauses s' cl'$ ]) in
+ let _=Refiner.add_tactic $se$ (fun [ $list:make_clauses s cl$ ]) in
List.iter
(fun s -> Tacinterp.add_primitive_tactic s
(Tacexpr.TacAtom($default_loc$,
Tacexpr.TacExtend($default_loc$,s,[]))))
$atomic_tactics$
with e -> Pp.pp (Cerrors.explain_exn e);
- if Options.v7.val then Egrammar.extend_tactic_grammar $se'$ $gl$
- else Egrammar.extend_tactic_grammar $se'$ $gl'$;
- List.iter (Pptactic.declare_extra_tactic_pprule True $se'$) $pp'$;
- List.iter (Pptactic.declare_extra_tactic_pprule False $se'$) $pp$;
+ Egrammar.extend_tactic_grammar $se$ $gl$;
+ List.iter Pptactic.declare_extra_tactic_pprule $pp$;
end
>>
-open Vernacexpr
-open Pcoq
-
-let rec interp_entry_name loc s =
- let l = String.length s in
- if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then
- let t, g = interp_entry_name loc (String.sub s 3 (l-8)) in
- List1ArgType t, <:expr< Gramext.Slist1 $g$ >>
- else if l > 5 & String.sub s (l-5) 5 = "_list" then
- let t, g = interp_entry_name loc (String.sub s 0 (l-5)) in
- List0ArgType t, <:expr< Gramext.Slist0 $g$ >>
- else if l > 4 & String.sub s (l-4) 4 = "_opt" then
- let t, g = interp_entry_name loc (String.sub s 0 (l-4)) in
- OptArgType t, <:expr< Gramext.Sopt $g$ >>
- else
-
- let t, se =
- match Pcoq.entry_type (Pcoq.get_univ "prim") s with
- | Some _ as x -> x, <:expr< Prim. $lid:s$ >>
- | None ->
- match Pcoq.entry_type (Pcoq.get_univ "constr") s with
- | Some _ as x -> x, <:expr< Constr. $lid:s$ >>
- | None ->
- match Pcoq.entry_type (Pcoq.get_univ "tactic") s with
- | Some _ as x -> x, <:expr< Tactic. $lid:s$ >>
- | None -> None, <:expr< $lid:s$ >> in
- let t =
- match t with
- | Some t -> t
- | None ->
-(* Pp.warning_with Pp_control.err_ft
- ("Unknown primitive grammar entry: "^s);*)
- ExtraArgType s
- in t, <:expr< Gramext.Snterm (Pcoq.Gram.Entry.obj $se$) >>
-
open Pcaml
EXTEND
@@ -248,11 +187,7 @@ EXTEND
[ [ "TACTIC"; "EXTEND"; s = [ UIDENT | LIDENT ];
OPT "|"; l = LIST1 tacrule SEP "|";
"END" ->
- declare_tactic loc s l
- | "V7"; "TACTIC"; "EXTEND"; s = [ UIDENT | LIDENT ];
- OPT "|"; l = LIST1 tacrule SEP "|";
- "END" ->
- declare_tactic_v7 loc s l ] ]
+ declare_tactic loc s l ] ]
;
tacrule:
[ [ "["; l = LIST1 tacargs; "]"; "->"; "["; e = Pcaml.expr; "]"
@@ -265,7 +200,7 @@ EXTEND
;
tacargs:
[ [ e = LIDENT; "("; s = LIDENT; ")" ->
- let t, g = interp_entry_name loc e in
+ let t, g = Q_util.interp_entry_name loc e in
TacNonTerm (loc, t, g, Some s)
| s = STRING ->
if s = "" then Util.user_err_loc (loc,"",Pp.str "Empty terminal");
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index 6b5b35dd2..32a673cdc 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -20,15 +20,10 @@ open Printer
let pr_tactic = function
| TacArg (Tacexp t) ->
- if !Options.v7 then
- Pptactic.pr_glob_tactic t (*top tactic from tacinterp*)
- else
- Pptacticnew.pr_glob_tactic (Global.env()) t
+ (*top tactic from tacinterp*)
+ Pptacticnew.pr_glob_tactic (Global.env()) t
| t ->
- if !Options.v7 then
- Pptactic.pr_tactic t
- else
- Pptacticnew.pr_tactic (Global.env()) t
+ Pptacticnew.pr_tactic (Global.env()) t
let pr_rule = function
| Prim r -> hov 0 (pr_prim_rule r)
diff --git a/parsing/termast.ml b/parsing/termast.ml
deleted file mode 100644
index 3d191d4a9..000000000
--- a/parsing/termast.ml
+++ /dev/null
@@ -1,551 +0,0 @@
-(************************************************************************)
-(* 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$ *)
-
-open Pp
-open Util
-open Univ
-open Names
-open Nameops
-open Term
-open Termops
-open Inductive
-open Sign
-open Environ
-open Libnames
-open Declare
-open Impargs
-open Coqast
-open Ast
-open Rawterm
-open Pattern
-open Nametab
-open Mod_subst
-
-(* In this file, we translate rawconstr to ast, in order to print constr *)
-
-(**********************************************************************)
-(* Parametrization *)
-open Constrextern
-(*
-(* This governs printing of local context of references *)
-let print_arguments = ref false
-
-(* If true, prints local context of evars, whatever print_arguments *)
-let print_evar_arguments = ref false
-*)
-
-(* This forces printing of cast nodes *)
-let print_casts = ref true
-
-(*
-(* This governs printing of implicit arguments. When
- [print_implicits] is on then [print_implicits_explicit_args] tells
- how implicit args are printed. If on, implicit args are printed
- prefixed by "!" otherwise the function and not the arguments is
- prefixed by "!" *)
-let print_implicits = ref false
-*)
-let print_implicits_explicit_args = ref false
-
-(*
-(* This forces printing of coercions *)
-let print_coercions = ref false
-
-(* This forces printing universe names of Type{.} *)
-let print_universes = ref false
-
-
-let with_option o f x =
- let old = !o in o:=true;
- try let r = f x in o := old; r
- with e -> o := old; raise e
-
-let with_arguments f = with_option print_arguments f
-let with_casts f = with_option print_casts f
-let with_implicits f = with_option print_implicits f
-let with_coercions f = with_option print_coercions f
-let with_universes f = with_option print_universes f
-*)
-(**********************************************************************)
-(* conversion of references *)
-
-let ids_of_ctxt ctxt =
- Array.to_list
- (Array.map
- (function c -> match kind_of_term c with
- | Var id -> id
- | _ ->
- error
- "Termast: arbitrary substitution of references not yet implemented")
- ctxt)
-
-let ast_of_ident id = nvar id
-
-let ast_of_name = function
- | Name id -> nvar id
- | Anonymous -> nvar wildcard
-
-let idopt_of_name = function
- | Name id -> Some id
- | Anonymous -> None
-
-let ast_of_binders bl =
- List.map (fun (nal,isdef,ty) ->
- if isdef then ope("LETBINDER",ty::List.map ast_of_name nal)
- else ope("BINDER",ty::List.map ast_of_name nal)) bl
-
-let ast_type_of_binder bl t =
- List.fold_right (fun (nal,isdef,ty) ast ->
- if isdef then
- ope("LETIN",[ty;slam(idopt_of_name (List.hd nal),ast)])
- else
- ope("PROD",[ty;List.fold_right
- (fun na ast -> slam(idopt_of_name na,ast)) nal ast]))
- bl t
-
-let ast_body_of_binder bl t =
- List.fold_right (fun (nal,isdef,ty) ast ->
- if isdef then
- ope("LETIN",[ty;slam(idopt_of_name (List.hd nal),ast)])
- else
- ope("LAMBDA",[ty;List.fold_right
- (fun na ast -> slam(idopt_of_name na,ast)) nal ast]))
- bl t
-
-let ast_of_constant_ref sp =
- ope("CONST", [conpath_section dummy_loc sp])
-
-let ast_of_existential_ref ev =
-(*
- let ev =
- try int_of_string (string_of_id ev)
- with _ -> warning "cannot find existential variable number"; 0 in
-*)
- ope("EVAR", [num ev])
-
-let ast_of_constructor_ref ((sp,tyi),n) =
- ope("MUTCONSTRUCT",[path_section dummy_loc sp; num tyi; num n])
-
-let ast_of_inductive_ref (sp,tyi) =
- ope("MUTIND", [path_section dummy_loc sp; num tyi])
-
-let ast_of_section_variable_ref s =
- ope("SECVAR", [nvar s])
-
-let ast_of_qualid p =
- let dir, s = repr_qualid p in
- let args = List.map nvar ((List.rev(repr_dirpath dir))@[s]) in
- ope ("QUALID", args)
-
-let ast_of_ref = function
- | ConstRef sp -> ast_of_constant_ref sp
- | IndRef sp -> ast_of_inductive_ref sp
- | ConstructRef sp -> ast_of_constructor_ref sp
- | VarRef id -> ast_of_section_variable_ref id
-
-(**********************************************************************)
-(* conversion of patterns *)
-
-let rec ast_of_cases_pattern = function (* loc is thrown away for printing *)
- | PatVar (loc,Name id) -> nvar id
- | PatVar (loc,Anonymous) -> nvar wildcard
- | PatCstr(loc,cstrsp,args,Name id) ->
- let args = List.map ast_of_cases_pattern args in
- ope("PATTAS",
- [nvar id;
- ope("PATTCONSTRUCT", (ast_of_constructor_ref cstrsp)::args)])
- | PatCstr(loc,cstrsp,args,Anonymous) ->
- ope("PATTCONSTRUCT",
- (ast_of_constructor_ref cstrsp)
- :: List.map ast_of_cases_pattern args)
-
-let ast_dependent na aty =
- match na with
- | Name id -> occur_var_ast id aty
- | Anonymous -> false
-
-let decompose_binder = function
- | RProd(_,na,ty,c) -> Some (BProd,na,ty,c)
- | RLambda(_,na,ty,c) -> Some (BLambda,na,ty,c)
- | RLetIn(_,na,b,c) -> Some (BLetIn,na,b,c)
- | _ -> None
-
-(* Implicit args indexes are in ascending order *)
-let explicitize impl args =
- let n = List.length args in
- let rec exprec q = function
- | a::args, imp::impl when is_status_implicit imp ->
- let tail = exprec (q+1) (args,impl) in
- let visible =
- (!print_implicits & !print_implicits_explicit_args)
- or not (is_inferable_implicit false n imp) in
- if visible then ope("EXPL", [num q; a]) :: tail else tail
- | a::args, _::impl -> a :: exprec (q+1) (args,impl)
- | args, [] -> args (* In case of polymorphism *)
- | [], _ -> []
- in exprec 1 (args,impl)
-
-let rec skip_coercion dest_ref (f,args as app) =
- if !print_coercions then app
- else
- try
- match dest_ref f with
- | Some r ->
- (match Classops.hide_coercion r with
- | Some n ->
- if n >= List.length args then app
- else (* We skip a coercion *)
- let fargs = list_skipn n args in
- skip_coercion dest_ref (List.hd fargs,List.tl fargs)
- | None -> app)
- | None -> app
- with Not_found -> app
-
-let ast_of_app impl f args =
- if !print_implicits & not !print_implicits_explicit_args then
- ope("APPLISTEXPL", f::args)
- else
- let args = explicitize impl args in
- if args = [] then f else ope("APPLIST", f::args)
-
-let rec ast_of_raw = function
- | RRef (_,ref) -> ast_of_ref ref
- | RVar (_,id) -> ast_of_ident id
- | REvar (_,n,_) -> (* we drop args *) ast_of_existential_ref n
- | RPatVar (_,(_,n)) -> ope("META",[ast_of_ident n])
- | RApp (_,f,args) ->
- let (f,args) =
- skip_coercion (function RRef(_,r) -> Some r | _ -> None) (f,args) in
- let astf = ast_of_raw f in
- let astargs = List.map ast_of_raw args in
- (match f with
- | RRef (_,ref) -> ast_of_app (implicits_of_global ref) astf astargs
- | _ -> ast_of_app [] astf astargs)
-
- | RProd (_,Anonymous,t,c) ->
- (* Anonymous product are never factorized *)
- ope("ARROW",[ast_of_raw t; slam(None,ast_of_raw c)])
-
- | RLetIn (_,na,t,c) ->
- ope("LETIN",[ast_of_raw t; slam(idopt_of_name na,ast_of_raw c)])
-
- | RProd (_,na,t,c) ->
- let (n,a) = factorize_binder 1 BProd na (ast_of_raw t) c in
- (* PROD et PRODLIST doivent être distingués à cause du cas *)
- (* non dépendant, pour isoler l'implication; peut-être un *)
- (* constructeur ARROW serait-il plus justifié ? *)
- let tag = if n=1 then "PROD" else "PRODLIST" in
- ope(tag,[ast_of_raw t;a])
-
- | RLambda (_,na,t,c) ->
- let (n,a) = factorize_binder 1 BLambda na (ast_of_raw t) c in
- (* LAMBDA et LAMBDALIST se comportent pareil ... Non ! *)
- (* Pour compatibilité des theories, il faut LAMBDALIST partout *)
- ope("LAMBDALIST",[ast_of_raw t;a])
-
- | RCases (_,(typopt,_),tml,eqns) ->
- let pred = ast_of_rawopt typopt in
- let tag = "CASES" in
- let asttomatch =
- ope("TOMATCH", List.map (fun (tm,_) -> ast_of_raw tm) tml) in
- let asteqns = List.map ast_of_eqn eqns in
- ope(tag,pred::asttomatch::asteqns)
-
- | ROrderedCase (_,LetStyle,typopt,tm,[|bv|],_) ->
- let nvar' = function Anonymous -> nvar wildcard | Name id -> nvar id in
- let rec f l = function
- | RLambda (_,na,RHole _,c) -> f (nvar' na :: l) c
- | c -> List.rev l, ast_of_raw c in
- let l,c = f [] bv in
- let eqn = ope ("EQN", [c;ope ("PATTCONSTRUCT",(nvar wildcard)::l)]) in
- ope ("FORCELET",[(ast_of_rawopt typopt);(ast_of_raw tm);eqn])
-
- | ROrderedCase (_,st,typopt,tm,bv,_) ->
- let tag = match st with
- | IfStyle -> "FORCEIF"
- | RegularStyle -> "CASE"
- | MatchStyle | LetStyle -> "MATCH"
- in
-
- (* warning "Old Case syntax"; *)
- ope(tag,(ast_of_rawopt typopt)
- ::(ast_of_raw tm)
- ::(Array.to_list (Array.map ast_of_raw bv)))
-
- | RLetTuple _ | RIf _ ->
- anomaly "Let tuple and If not supported in v7"
-
- | RRec (_,fk,idv,blv,tyv,bv) ->
- let alfi = Array.map ast_of_ident idv in
- (match fk with
- | RFix (nv,n) ->
- let rec split_lambda binds = function
- | (0, t) -> (List.rev binds,ast_of_raw t)
- | (n, RLetIn (_,na,b,c)) ->
- let bind = ope("LETBINDER",[ast_of_raw b;ast_of_name na]) in
- split_lambda (bind::binds) (n,c)
- | (n, RLambda (_,na,t,b)) ->
- let bind = ope("BINDER",[ast_of_raw t;ast_of_name na]) in
- split_lambda (bind::binds) (n-1,b)
- | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint body" in
- let rec split_product = function
- | (0, t) -> ast_of_raw t
- | (n, RLetIn (_,na,_,c)) -> split_product (n,c)
- | (n, RProd (_,na,t,b)) -> split_product (n-1,b)
- | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint type" in
- let listdecl =
- Array.mapi
- (fun i fi ->
- if List.length blv.(i) >= nv.(i)+1 then
- let (oldfixp,factb) = list_chop (nv.(i)+1) blv.(i) in
- let bl = factorize_local_binder oldfixp in
- let factb = factorize_local_binder factb in
- let asttyp = ast_type_of_binder factb
- (ast_of_raw tyv.(i)) in
- let astdef = ast_body_of_binder factb
- (ast_of_raw bv.(i)) in
- ope("FDECL",[fi;ope("BINDERS",ast_of_binders bl);
- asttyp; astdef])
- else
- let n = nv.(i)+1 - List.length blv.(i) in
- let (lparams,astdef) =
- split_lambda [] (n,bv.(i)) in
- let bl = factorize_local_binder blv.(i) in
- let lparams = ast_of_binders bl @ lparams in
- let asttyp = split_product (n,tyv.(i)) in
- ope("FDECL",
- [fi; ope ("BINDERS",lparams);
- asttyp; astdef]))
- alfi
- in
- ope("FIX", alfi.(n)::(Array.to_list listdecl))
- | RCoFix n ->
- let listdecl =
- Array.mapi
- (fun i fi ->
- let bl = factorize_local_binder blv.(i) in
- let asttyp = ast_type_of_binder bl (ast_of_raw tyv.(i)) in
- let astdef = ast_body_of_binder bl (ast_of_raw bv.(i)) in
- ope("CFDECL",[fi; asttyp; astdef]))
- alfi
- in
- ope("COFIX", alfi.(n)::(Array.to_list listdecl)))
-
- | RSort (_,s) ->
- (match s with
- | RProp Null -> ope("PROP",[])
- | RProp Pos -> ope("SET",[])
- | RType _ -> ope("TYPE",[]))
- | RHole _ -> ope("ISEVAR",[])
- | RCast (_,c,_,t) -> ope("CAST",[ast_of_raw c;ast_of_raw t])
- | RDynamic (loc,d) -> Dynamic (loc,d)
-
-and ast_of_eqn (_,ids,pl,c) =
- ope("EQN", (ast_of_raw c)::(List.map ast_of_cases_pattern pl))
-
-and ast_of_rawopt = function
- | None -> (string "SYNTH")
- | Some p -> ast_of_raw p
-
-and factorize_binder n oper na aty c =
- let (p,body) = match decompose_binder c with
- | Some (oper',na',ty',c')
- when (oper = oper') & (aty = ast_of_raw ty')
- & not (ast_dependent na aty) (* To avoid na in ty' escapes scope *)
- & not (na' = Anonymous & oper = BProd)
- -> factorize_binder (n+1) oper na' aty c'
- | _ -> (n,ast_of_raw c)
- in
- (p,slam(idopt_of_name na, body))
-
-and factorize_local_binder = function
- [] -> []
- | (na,Some bd,ty)::l ->
- ([na],true,ast_of_raw bd) :: factorize_local_binder l
- | (na,None,ty)::l ->
- let ty = ast_of_raw ty in
- (match factorize_local_binder l with
- (lna,false,ty') :: l when ty=ty' ->
- (na::lna,false,ty') :: l
- | l -> ([na],false,ty) :: l)
-
-
-let ast_of_rawconstr = ast_of_raw
-
-(******************************************************************)
-(* Main translation function from constr -> ast *)
-
-let ast_of_constr at_top env t =
- let t' =
- if !print_casts then t
- else Reductionops.local_strong strip_outer_cast t in
- let avoid = if at_top then ids_of_context env else [] in
- ast_of_raw
- (Detyping.detype (at_top,env) avoid (names_of_rel_context env) t')
-
-(**********************************************************************)
-(* Object substitution in modules *)
-
-let rec subst_ast subst ast = match ast with
- | Node (l,s,astl) ->
- let astl' = Util.list_smartmap (subst_ast subst) astl in
- if astl' == astl then ast else
- Node (l,s,astl')
- | Slam (l,ido,ast1) ->
- let ast1' = subst_ast subst ast1 in
- if ast1' == ast1 then ast else
- Slam (l,ido,ast1')
- | Smetalam (l,s,ast1) ->
- let ast1' = subst_ast subst ast1 in
- if ast1' == ast1 then ast else
- Smetalam (l,s,ast1')
- | Path (loc,kn) ->
- let kn' = subst_kn subst kn in
- if kn' == kn then ast else
- Path(loc,kn')
- | ConPath (loc,kn) ->
- let kn',t = subst_con subst kn in
- if kn' == kn then ast else
- ast_of_constr false (Global.env ()) t
- | Nmeta _
- | Nvar _ -> ast
- | Num _
- | Str _
- | Id _
- | Dynamic _ -> ast
-
-let rec subst_astpat subst = function
-(*CSC: this is wrong since I am not recompiling the whole pattern.
- However, this is V7-syntax code that is doomed to disappear. Hence I
- prefer to be lazy and to not fix the bug. *)
- | Pquote a -> Pquote (subst_ast subst a)
- | Pmeta _ as p -> p
- | Pnode (s,pl) -> Pnode (s,subst_astpatlist subst pl)
- | Pslam (ido,p) -> Pslam (ido,subst_astpat subst p)
- | Pmeta_slam (s,p) -> Pmeta_slam (s,subst_astpat subst p)
-
-and subst_astpatlist subst = function
- | Pcons (p,pl) -> Pcons (subst_astpat subst p, subst_astpatlist subst pl)
- | (Plmeta _ | Pnil) as pl -> pl
-
-let subst_pat subst = function
- | AstListPat pl -> AstListPat (subst_astpatlist subst pl)
- | PureAstPat p -> PureAstPat (subst_astpat subst p)
-
-let ast_of_constant env sp =
- let a = ast_of_constant_ref sp in
- a
-
-let ast_of_existential env (ev,ids) =
- let a = ast_of_existential_ref ev in
- if !print_arguments or !print_evar_arguments then
- ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids))
- else a
-
-let ast_of_constructor env cstr_sp =
- let a = ast_of_constructor_ref cstr_sp in
- a
-
-let ast_of_inductive env ind_sp =
- let a = ast_of_inductive_ref ind_sp in
- a
-
-let decompose_binder_pattern = function
- | PProd(na,ty,c) -> Some (BProd,na,ty,c)
- | PLambda(na,ty,c) -> Some (BLambda,na,ty,c)
- | PLetIn(na,b,c) -> Some (BLetIn,na,b,c)
- | _ -> None
-
-let rec ast_of_pattern tenv env = function
- | PRef ref -> ast_of_ref ref
-
- | PVar id -> ast_of_ident id
-
- | PEvar (n,_) -> ast_of_existential_ref n
-
- | PRel n ->
- (try match lookup_name_of_rel n env with
- | Name id -> ast_of_ident id
- | Anonymous ->
- anomaly "ast_of_pattern: index to an anonymous variable"
- with Not_found ->
- nvar (id_of_string ("[REL "^(string_of_int n)^"]")))
-
- | PApp (f,args) ->
- let (f,args) =
- skip_coercion (function PRef r -> Some r | _ -> None)
- (f,Array.to_list args) in
- let astf = ast_of_pattern tenv env f in
- let astargs = List.map (ast_of_pattern tenv env) args in
- (match f with
- | PRef ref -> ast_of_app (implicits_of_global ref) astf astargs
- | _ -> ast_of_app [] astf astargs)
-
- | PSoApp (n,args) ->
- ope("SOAPP",(ope ("META",[ast_of_ident n]))::
- (List.map (ast_of_pattern tenv env) args))
-
- | PLetIn (na,b,c) ->
- let c' = ast_of_pattern tenv (add_name na env) c in
- ope("LETIN",[ast_of_pattern tenv env b;slam(idopt_of_name na,c')])
-
- | PProd (Anonymous,t,c) ->
- ope("PROD",[ast_of_pattern tenv env t;
- slam(None,ast_of_pattern tenv env c)])
- | PProd (na,t,c) ->
- let env' = add_name na env in
- let (n,a) =
- factorize_binder_pattern tenv env' 1 BProd na
- (ast_of_pattern tenv env t) c in
- (* PROD et PRODLIST doivent être distingués à cause du cas *)
- (* non dépendant, pour isoler l'implication; peut-être un *)
- (* constructeur ARROW serait-il plus justifié ? *)
- let tag = if n=1 then "PROD" else "PRODLIST" in
- ope(tag,[ast_of_pattern tenv env t;a])
- | PLambda (na,t,c) ->
- let env' = add_name na env in
- let (n,a) =
- factorize_binder_pattern tenv env' 1 BLambda na
- (ast_of_pattern tenv env t) c in
- (* LAMBDA et LAMBDALIST se comportent pareil *)
- let tag = if n=1 then "LAMBDA" else "LAMBDALIST" in
- ope(tag,[ast_of_pattern tenv env t;a])
-
- | PCase (st,typopt,tm,bv) ->
- warning "Old Case syntax";
- ope("MUTCASE",(ast_of_patopt tenv env typopt)
- ::(ast_of_pattern tenv env tm)
- ::(Array.to_list (Array.map (ast_of_pattern tenv env) bv)))
-
- | PSort s ->
- (match s with
- | RProp Null -> ope("PROP",[])
- | RProp Pos -> ope("SET",[])
- | RType _ -> ope("TYPE",[]))
-
- | PMeta (Some n) -> ope("META",[ast_of_ident n])
- | PMeta None -> ope("ISEVAR",[])
- | PFix f -> ast_of_raw (Detyping.detype (false,tenv) [] env (mkFix f))
- | PCoFix c -> ast_of_raw (Detyping.detype (false,tenv) [] env (mkCoFix c))
-
-and ast_of_patopt tenv env = function
- | None -> (string "SYNTH")
- | Some p -> ast_of_pattern tenv env p
-
-and factorize_binder_pattern tenv env n oper na aty c =
- let (p,body) = match decompose_binder_pattern c with
- | Some (oper',na',ty',c')
- when (oper = oper') & (aty = ast_of_pattern tenv env ty')
- & not (na' = Anonymous & oper = BProd)
- ->
- factorize_binder_pattern tenv (add_name na' env) (n+1) oper na' aty c'
- | _ -> (n,ast_of_pattern tenv env c)
- in
- (p,slam(idopt_of_name na, body))
diff --git a/parsing/termast.mli b/parsing/termast.mli
deleted file mode 100644
index da7e476be..000000000
--- a/parsing/termast.mli
+++ /dev/null
@@ -1,60 +0,0 @@
-(************************************************************************)
-(* 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 *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-(*i*)
-open Names
-open Term
-open Termops
-open Sign
-open Environ
-open Libnames
-open Nametab
-open Rawterm
-open Pattern
-open Mod_subst
-(*i*)
-
-(* Translation of pattern, cases pattern, rawterm and term into syntax
- trees for printing *)
-
-val ast_of_cases_pattern : cases_pattern -> Coqast.t
-val ast_of_rawconstr : rawconstr -> Coqast.t
-val ast_of_pattern : env -> names_context -> constr_pattern -> Coqast.t
-
-(* If [b=true] in [ast_of_constr b env c] then the variables in the first
- level of quantification clashing with the variables in [env] are renamed *)
-
-val ast_of_constr : bool -> env -> constr -> Coqast.t
-
-(* Object substitution in modules *)
-val subst_ast: substitution -> Coqast.t -> Coqast.t
-val subst_astpat : substitution -> Ast.astpat -> Ast.astpat
-
-val ast_of_constant : env -> constant -> Coqast.t
-val ast_of_existential : env -> existential -> Coqast.t
-val ast_of_constructor : env -> constructor -> Coqast.t
-val ast_of_inductive : env -> inductive -> Coqast.t
-val ast_of_ref : global_reference -> Coqast.t
-val ast_of_qualid : qualid -> Coqast.t
-
-(*i Now in constrextern.mli
-val print_implicits : bool ref
-val print_casts : bool ref
-val print_arguments : bool ref
-val print_evar_arguments : bool ref
-val print_coercions : bool ref
-val print_universes : bool ref
-
-val with_casts : ('a -> 'b) -> 'a -> 'b
-val with_implicits : ('a -> 'b) -> 'a -> 'b
-val with_arguments : ('a -> 'b) -> 'a -> 'b
-val with_coercions : ('a -> 'b) -> 'a -> 'b
-val with_universes : ('a -> 'b) -> 'a -> 'b
-i*)
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 6e2f5fe3a..b478e37d9 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -11,7 +11,6 @@
open Genarg
open Q_util
open Q_coqast
-open Ast
open Argextend
let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
@@ -96,40 +95,6 @@ let declare_command loc s cl =
end
>>
-open Vernacexpr
-open Pcoq
-
-let rec interp_entry_name loc s =
- let l = String.length s in
- if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then
- let t, g = interp_entry_name loc (String.sub s 3 (l-8)) in
- List1ArgType t, <:expr< Gramext.Slist1 $g$ >>
- else if l > 5 & String.sub s (l-5) 5 = "_list" then
- let t, g = interp_entry_name loc (String.sub s 0 (l-5)) in
- List0ArgType t, <:expr< Gramext.Slist0 $g$ >>
- else if l > 4 & String.sub s (l-4) 4 = "_opt" then
- let t, g = interp_entry_name loc (String.sub s 0 (l-4)) in
- OptArgType t, <:expr< Gramext.Sopt $g$ >>
- else
- let t, se =
- match Pcoq.entry_type (Pcoq.get_univ "prim") s with
- | Some _ as x -> x, <:expr< Prim. $lid:s$ >>
- | None ->
- match Pcoq.entry_type (Pcoq.get_univ "constr") s with
- | Some _ as x -> x, <:expr< Constr. $lid:s$ >>
- | None ->
- match Pcoq.entry_type (Pcoq.get_univ "tactic") s with
- | Some _ as x -> x, <:expr< Tactic. $lid:s$ >>
- | None -> None, <:expr< $lid:s$ >> in
- let t =
- match t with
- | Some t -> t
- | None ->
-(* Pp.warning_with Pp_control.err_ft
- ("Unknown primitive grammar entry: "^s);*)
- ExtraArgType s
- in t, <:expr< Gramext.Snterm (Pcoq.Gram.Entry.obj $se$) >>
-
open Pcaml
EXTEND
@@ -149,7 +114,7 @@ EXTEND
;
args:
[ [ e = LIDENT; "("; s = LIDENT; ")" ->
- let t, g = interp_entry_name loc e in
+ let t, g = Q_util.interp_entry_name loc e in
VernacNonTerm (loc, t, g, Some s)
| s = STRING ->
VernacTerm s