aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/g_ltac.ml427
-rw-r--r--parsing/g_ltacnew.ml427
-rw-r--r--parsing/g_prim.ml438
-rw-r--r--parsing/g_primnew.ml480
-rw-r--r--parsing/g_tactic.ml422
-rw-r--r--parsing/g_tacticnew.ml437
6 files changed, 1 insertions, 230 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index e60095a0a6..c39e6f7fdf 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -16,39 +16,15 @@ open Rawterm
open Tacexpr
open Vernacexpr
open Ast
-
-ifdef Quotify then
-open Qast
-else
open Pcoq
-
open Prim
open Tactic
-ifdef Quotify then
-open Q
-
type let_clause_kind =
| LETTOPCLAUSE of Names.identifier * constr_expr
| LETCLAUSE of
(Names.identifier Util.located * raw_tactic_expr option * raw_tactic_arg)
-ifdef Quotify then
-module Prelude = struct
-let fail_default_value = Qast.Int "0"
-
-let out_letin_clause loc = function
- | Qast.Node ("LETTOPCLAUSE", _) -> user_err_loc (loc, "", (str "Syntax Error"))
- | Qast.Node ("LETCLAUSE", [id;c;d]) ->
- Qast.Tuple [id;c;d]
- | _ -> anomaly "out_letin_clause"
-
-let make_letin_clause _ = function
- | Qast.List l -> Qast.List (List.map (out_letin_clause dummy_loc) l)
- | _ -> anomaly "make_letin_clause"
-end
-else
-module Prelude = struct
let fail_default_value = Genarg.ArgArg 0
let out_letin_clause loc = function
@@ -56,9 +32,6 @@ let out_letin_clause loc = function
| LETCLAUSE (id,c,d) -> (id,c,d)
let make_letin_clause loc = List.map (out_letin_clause loc)
-end
-
-open Prelude
let arg_of_expr = function
TacArg a -> a
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index c32c0988df..578ab250d3 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -16,39 +16,15 @@ open Rawterm
open Tacexpr
open Vernacexpr
open Ast
-
-ifdef Quotify then
-open Qast
-else
open Pcoq
-
open Prim
open Tactic
-ifdef Quotify then
-open Q
-
type let_clause_kind =
| LETTOPCLAUSE of Names.identifier * constr_expr
| LETCLAUSE of
(Names.identifier Util.located * raw_tactic_expr option * raw_tactic_arg)
-ifdef Quotify then
-module Prelude = struct
-let fail_default_value = Qast.Int "0"
-
-let out_letin_clause loc = function
- | Qast.Node ("LETTOPCLAUSE", _) -> user_err_loc (loc, "", (str "Syntax Error"))
- | Qast.Node ("LETCLAUSE", [id;c;d]) ->
- Qast.Tuple [id;c;d]
- | _ -> anomaly "out_letin_clause"
-
-let make_letin_clause _ = function
- | Qast.List l -> Qast.List (List.map (out_letin_clause dummy_loc) l)
- | _ -> anomaly "make_letin_clause"
-end
-else
-module Prelude = struct
let fail_default_value = Genarg.ArgArg 0
let out_letin_clause loc = function
@@ -56,14 +32,11 @@ let out_letin_clause loc = function
| LETCLAUSE (id,c,d) -> (id,c,d)
let make_letin_clause loc = List.map (out_letin_clause loc)
-end
let arg_of_expr = function
TacArg a -> a
| e -> Tacexp (e:raw_tactic_expr)
-open Prelude
-
(* Tactics grammar rules *)
let tactic_expr = Gram.Entry.create "tactic:tactic_expr"
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 31712d23a3..6973a551d6 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -13,42 +13,10 @@ open Pcoq
open Names
open Libnames
open Topconstr
-
-ifdef Quotify then
-open Qast
-
open Prim
let _ = reset_all_grammars()
-(* camlp4o pa_extend.cmo pa_extend_m.cmo pr_o.cmo q_prim.ml *)
-
-ifdef Quotify then
-module Prelude = struct
-let local_id_of_string s = Apply ("Names","id_of_string", [s])
-let local_make_dirpath l = Qast.Apply ("Names","make_dirpath",[l])
-let local_make_posint s = s
-let local_make_negint s = Apply ("Pervasives","~-", [s])
-let local_make_qualid l id' =
- Qast.Apply ("Nametab","make_qualid", [local_make_dirpath l;id'])
-let local_make_short_qualid id =
- Qast.Apply ("Nametab","make_short_qualid",[id])
-let local_make_path l id' =
- Qast.Apply ("Libnames","encode_kn", [local_make_dirpath l;id'])
-let local_make_binding loc a b =
- match a with
- | Qast.Node ("Nvar", [_;id]) ->
- Qast.Node ("Slam", [Qast.Loc; Qast.Option (Some id); b])
- | Qast.Node ("Nmeta", [_;s]) ->
- Qast.Node ("Smetalam", [Qast.Loc;s;b])
- | _ ->
- Qast.Apply ("Pervasives", "failwith", [Qast.Str "Slam expects a var or a metavar"])
-let local_append l id = Qast.Apply ("List","append", [l; Qast.List [id]])
-end
-
-else
-
-module Prelude = struct
open Nametab
let local_id_of_string = id_of_string
let local_make_dirpath = make_dirpath
@@ -63,12 +31,6 @@ let local_make_binding loc a b =
| Nmeta (_,s) -> Smetalam(loc,s,b)
| _ -> failwith "Slam expects a var or a metavar"
let local_append l id = l@[id]
-end
-
-open Prelude
-
-ifdef Quotify then
-open Q
GEXTEND Gram
GLOBAL: ident natural integer bigint string preident ast
diff --git a/parsing/g_primnew.ml4 b/parsing/g_primnew.ml4
index 2418b6ee56..b3863b4585 100644
--- a/parsing/g_primnew.ml4
+++ b/parsing/g_primnew.ml4
@@ -30,37 +30,8 @@ let _ =
if not !Options.v7 then
List.iter (fun s -> Lexer.add_token("",s)) prim_kw
-ifdef Quotify then
-open Qast
-
open Prim
-ifdef Quotify then
-module Prelude = struct
-let local_id_of_string s = Apply ("Names","id_of_string", [s])
-let local_make_dirpath l = Qast.Apply ("Names","make_dirpath",[l])
-let local_make_posint s = s
-let local_make_negint s = Apply ("Pervasives","~-", [s])
-let local_make_qualid l id' =
- Qast.Apply ("Nametab","make_qualid", [local_make_dirpath l;id'])
-let local_make_short_qualid id =
- Qast.Apply ("Nametab","make_short_qualid",[id])
-let local_make_path l id' =
- Qast.Apply ("Libnames","encode_kn", [local_make_dirpath l;id'])
-let local_make_binding loc a b =
- match a with
- | Qast.Node ("Nvar", [_;id]) ->
- Qast.Node ("Slam", [Qast.Loc; Qast.Option (Some id); b])
- | Qast.Node ("Nmeta", [_;s]) ->
- Qast.Node ("Smetalam", [Qast.Loc;s;b])
- | _ ->
- Qast.Apply ("Pervasives", "failwith", [Qast.Str "Slam expects a var or a metavar"])
-let local_append l id = Qast.Apply ("List","append", [l; Qast.List [id]])
-end
-
-else
-
-module Prelude = struct
open Nametab
let local_id_of_string = id_of_string
let local_make_dirpath = make_dirpath
@@ -75,21 +46,10 @@ let local_make_binding loc a b =
| Nmeta (_,s) -> Smetalam(loc,s,b)
| _ -> failwith "Slam expects a var or a metavar"
let local_append l id = l@[id]
-end
-
-open Prelude
-
-ifdef Quotify then
-open Q
if not !Options.v7 then
GEXTEND Gram
- GLOBAL: (*ast*) bigint qualid reference ne_string;
-(*
- metaident:
- [ [ s = METAIDENT -> Nmeta (loc,s) ] ]
- ;
-*)
+ GLOBAL: bigint qualid reference ne_string;
field:
[ [ s = FIELD -> local_id_of_string s ] ]
;
@@ -98,14 +58,6 @@ GEXTEND Gram
| id = field -> ([],id)
] ]
;
-(*
- astpath:
- [ [ id = base_ident; (l,a) = fields ->
- Path(loc, local_make_path (local_append l id) a)
- | id = base_ident -> Nvar(loc, id)
- ] ]
- ;
-*)
basequalid:
[ [ id = base_ident; (l,id')=fields ->
local_make_qualid (local_append l id) id'
@@ -126,37 +78,7 @@ GEXTEND Gram
if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string"); s
] ]
;
-(*
- ast:
- [ [ id = metaident -> id
- | p = astpath -> p
- | s = INT -> Num(loc, local_make_posint s)
- | s = STRING -> Str(loc, s)
- | "{"; s = METAIDENT; "}" -> Id(loc,s)
- | "("; nname = IDENT; l = LIST0 ast; ")" -> Node(loc,nname,l)
- | "("; METAIDENT "$LIST"; id = metaident; ")" -> Node(loc,"$LIST",[id])
- | "("; METAIDENT "$STR"; id = metaident; ")" -> Node(loc,"$STR",[id])
- | "("; METAIDENT "$VAR"; id = metaident; ")" -> Node(loc,"$VAR",[id])
- | "("; METAIDENT "$ID"; id = metaident; ")" -> Node(loc,"$ID",[id])
- | "("; METAIDENT "$ABSTRACT"; l = LIST0 ast;")"->Node(loc,"$ABSTRACT",l)
- | "("; METAIDENT "$PATH"; id = metaident; ")" -> Node(loc,"$PATH",[id])
- | "("; METAIDENT "$NUM"; id = metaident; ")" -> Node(loc,"$NUM",[id])
- | "["; "<>"; "]"; b = ast -> Slam(loc,None,b)
- | "["; a = ast; "]"; b = ast -> local_make_binding loc a b
- | "'"; a = ast -> Node(loc,"$QUOTE",[a]) ] ]
- ;
-*)
bigint: (* Negative numbers are dealt with specially *)
[ [ i = INT -> Bignat.POS (Bignat.of_string i) ] ]
;
END
-
-(*
-let constr_to_ast a =
- Termast.ast_of_rawconstr
- (Constrintern.interp_rawconstr Evd.empty (Global.env()) a)
-
-let constr_parser_with_glob = Pcoq.map_entry constr_to_ast Constr.constr
-
-let _ = define_ast_quotation true "constr" constr_parser_with_glob
-*)
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 3d1d8eea65..7c4fa0d5bc 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -15,10 +15,6 @@ open Util
open Tacexpr
open Rawterm
open Genarg
-
-(* open grammar entries, possibly in quotified form *)
-ifdef Quotify then open Qast
-
open Constr
open Prim
open Tactic
@@ -39,24 +35,6 @@ let local_compute = [FBeta;FIota;FDeltaBut [];FZeta]
let error_oldelim _ = error "OldElim no longer supported"
-ifdef Quotify then
- let induction_arg_of_constr = function
- | Qast.Node ("Nvar", [_;id]) -> Qast.Node ("ElimOnIdent", [id])
- | c -> Qast.Node ("ElimOnConstr", [c])
-
-ifdef Quotify then
-let make_red_flag s = Qast.Apply ("make_red_flag", [s])
-
-ifdef Quotify then
-let local_compute =
- Qast.List [
- Qast.Node ("FBeta", []);
- Qast.Node ("FDeltaBut", [Qast.List []]);
- Qast.Node ("FIota", []);
- Qast.Node ("FZeta", [])]
-
-ifdef Quotify then open Q
-
let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
(* Auxiliary grammar rules *)
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 33cfab4d92..b0ea9d8352 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -71,9 +71,6 @@ let lpar_id_colon =
| _ -> raise Stream.Failure)
| _ -> raise Stream.Failure)
-(* open grammar entries, possibly in quotified form *)
-ifdef Quotify then open Qast
-
open Constr
open Prim
open Tactic
@@ -105,24 +102,6 @@ let local_compute = [FBeta;FIota;FDeltaBut [];FZeta]
let error_oldelim _ = error "OldElim no longer supported"
-ifdef Quotify then
- let induction_arg_of_constr = function
- | Qast.Node ("Nvar", [_;id]) -> Qast.Node ("ElimOnIdent", [id])
- | c -> Qast.Node ("ElimOnConstr", [c])
-
-ifdef Quotify then
-let make_red_flag s = Qast.Apply ("make_red_flag", [s])
-
-ifdef Quotify then
-let local_compute =
- Qast.List [
- Qast.Node ("FBeta", []);
- Qast.Node ("FDeltaBut", [Qast.List []]);
- Qast.Node ("FIota", []);
- Qast.Node ("FZeta", [])]
-
-ifdef Quotify then open Q
-
let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
(* Auxiliary grammar rules *)
@@ -136,22 +115,6 @@ GEXTEND Gram
[ [ n = integer -> Genarg.ArgArg n
| id = identref -> Genarg.ArgVar id ] ]
;
-(* autoarg_depth:
- [ [ n = OPT natural -> n ] ]
- ;
- autoarg_adding:
- [ [ IDENT "adding" ; "["; l = LIST1 global; "]" -> l | -> [] ] ]
- ;
- autoarg_destructing:
- [ [ IDENT "destructing" -> true | -> false ] ]
- ;
- autoarg_usingTDB:
- [ [ "using"; IDENT "tdb" -> true | -> false ] ]
- ;
- autoargs:
- [ [ a0 = autoarg_depth; l = autoarg_adding;
- a2 = autoarg_destructing; a3 = autoarg_usingTDB -> (a0,l,a2,a3) ] ]
- ;*)
(* An identifier or a quotation meta-variable *)
id_or_meta:
[ [ id = identref -> AI id
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 17:58:05 +0000