summaryrefslogtreecommitdiff
path: root/parsing/tacextend.ml4
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-03-27 07:43:43 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-03-27 07:45:11 +0200
commit6e34b272d789455a9be589e27ad3a998cf25496b (patch)
tree57b74c7cbafd705a1ebce7d16cdaec02b704fb44 /parsing/tacextend.ml4
parent5fe4ac437bed43547b3695664974f492b55cb553 (diff)
parent2bdcd093b357adb2185518dabbafd1a0b9279044 (diff)
Remove non-DFSG contentsupstream/8.3.pl4+dfsg
Diffstat (limited to 'parsing/tacextend.ml4')
-rw-r--r--parsing/tacextend.ml444
1 files changed, 26 insertions, 18 deletions
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 0d7a9cfe..2fbe3f44 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
-(* $Id: tacextend.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: tacextend.ml4 15043 2012-03-18 13:57:01Z herbelin $ *)
open Util
open Genarg
@@ -131,19 +131,27 @@ let make_one_printing_rule se (pt,e) =
let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se)
-let rec contains_epsilon = function
- | List0ArgType _ -> true
- | List1ArgType t -> contains_epsilon t
- | OptArgType _ -> true
- | PairArgType(t1,t2) -> contains_epsilon t1 && contains_epsilon t2
- | ExtraArgType("hintbases") -> true
- | _ -> false
-let is_atomic = function
- | GramTerminal s :: l when
- List.for_all (function
- GramTerminal _ -> false
- | GramNonTerminal(_,t,_,_) -> contains_epsilon t) l
- -> [s]
+let rec contains_epsilon loc = function
+ | List0ArgType _ as t ->
+ <:expr< Genarg.in_gen $make_globwit loc t$ [] >>
+ | List1ArgType t' as t ->
+ <:expr< Genarg.in_gen $make_globwit loc t$
+ [out_gen $make_globwit loc t'$ $contains_epsilon loc t'$] >>
+ | OptArgType _ as t ->
+ <:expr< Genarg.in_gen $make_globwit loc t$ None >>
+(* | PairArgType(t1,t2) -> contains_epsilon t1 && contains_epsilon t2*)
+ | ExtraArgType("hintbases") as t ->
+ <:expr< Genarg.in_gen $make_globwit loc t$ (Some []) >> (* fragile *)
+ | _ -> raise Exit
+
+let is_atomic loc = function
+ | GramTerminal s :: l ->
+ (try
+ let l = List.map (function
+ GramTerminal _ -> raise Exit
+ | GramNonTerminal(_,t,_,_) -> contains_epsilon loc t) l
+ in [<:expr< ($str:s$, $mlexpr_of_list (fun x -> x) l$) >>]
+ with Exit -> [])
| _ -> []
let declare_tactic loc s cl =
@@ -163,8 +171,8 @@ let declare_tactic loc s cl =
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
+ mlexpr_of_list (fun x -> x)
+ (List.flatten (List.map (fun (al,_) -> is_atomic loc al) cl)) in
<:str_item<
declare
open Pcoq;
@@ -173,9 +181,9 @@ let declare_tactic loc s cl =
try
let _=Tacinterp.add_tactic $se$ (fun [ $list:make_clauses s cl$ ]) in
List.iter
- (fun s -> Tacinterp.add_primitive_tactic s
+ (fun (s,l) -> Tacinterp.add_primitive_tactic s
(Tacexpr.TacAtom($default_loc$,
- Tacexpr.TacExtend($default_loc$,s,[]))))
+ Tacexpr.TacExtend($default_loc$,$se$,l))))
$atomic_tactics$
with e -> Pp.pp (Cerrors.explain_exn e);
Egrammar.extend_tactic_grammar $se$ $gl$;