diff options
Diffstat (limited to 'parsing/tacextend.ml4')
| -rw-r--r-- | parsing/tacextend.ml4 | 59 |
1 files changed, 25 insertions, 34 deletions
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 0d7a9cfe..2fe1fdda 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -1,14 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) - -(* $Id: tacextend.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) +(*i camlp4deps: "tools/compat5b.cmo" i*) open Util open Genarg @@ -18,6 +16,7 @@ open Argextend open Pcoq open Extrawit open Egrammar +open Compat let rec make_patt = function | [] -> <:patt< [] >> @@ -43,20 +42,9 @@ let rec make_let e = function let loc = join_loc loc (MLast.loc_of_expr e) in let e = make_let e l in let v = <:expr< Genarg.out_gen $make_wit loc t$ $lid:p$ >> in - let v = - (* Special case for tactics which must be stored in algebraic - form to avoid marshalling closures and to be reprinted *) - if is_tactic_genarg t then - <:expr< ($v$, Tacinterp.eval_tactic $v$) >> - else v in <:expr< let $lid:p$ = $v$ in $e$ >> | _::l -> make_let e l -let add_clause s (pt,e) l = - let p = make_patt pt in - let w = Some (make_when (MLast.loc_of_expr e) pt) in - (p, <:vala< w >>, make_let e pt)::l - let rec extract_signature = function | [] -> [] | GramNonTerminal (_,t,_,_) :: l -> t :: extract_signature l @@ -69,12 +57,14 @@ let check_unicity s l = ("Two distinct rules of tactic entry "^s^" have the same\n"^ "non-terminals in the same order: put them in distinct tactic entries") -let make_clauses s l = +let make_clause (pt,e) = + (make_patt pt, + vala (Some (make_when (MLast.loc_of_expr e) pt)), + make_let e pt) + +let make_fun_clauses loc s l = check_unicity s l; - let default = - (<:patt< _ >>,<:vala<None>>, - <:expr< failwith "Tactic extension: cannot occur" >>) in - List.fold_right (add_clause s) l [default] + Compat.make_fun loc (List.map make_clause l) let rec make_args = function | [] -> <:expr< [] >> @@ -89,9 +79,7 @@ let rec make_eval_tactic e = function let p = Names.string_of_id p in let loc = join_loc loc (MLast.loc_of_expr e) in let e = make_eval_tactic e l in - (* Special case for tactics which must be stored in algebraic - form to avoid marshalling closures and to be reprinted *) - <:expr< let $lid:p$ = ($lid:p$,Tacinterp.eval_tactic $lid:p$) in $e$ >> + <:expr< let $lid:p$ = $lid:p$ in $e$ >> | _::l -> make_eval_tactic e l let rec make_fun e = function @@ -165,30 +153,28 @@ let declare_tactic loc s cl = let atomic_tactics = mlexpr_of_list mlexpr_of_string (List.flatten (List.map (fun (al,_) -> is_atomic al) cl)) in - <:str_item< - declare - open Pcoq; - open Extrawit; - declare $list:hidden$ end; + declare_str_items loc + (hidden @ + [ <:str_item< do { try - let _=Tacinterp.add_tactic $se$ (fun [ $list:make_clauses s cl$ ]) in + let _=Tacinterp.add_tactic $se$ $make_fun_clauses loc 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); + with e -> Pp.pp (Errors.print e); Egrammar.extend_tactic_grammar $se$ $gl$; - List.iter Pptactic.declare_extra_tactic_pprule $pp$; - end - >> + List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >> + ]) open Pcaml +open PcamlSig EXTEND GLOBAL: str_item; str_item: - [ [ "TACTIC"; "EXTEND"; s = [ UIDENT | LIDENT ]; + [ [ "TACTIC"; "EXTEND"; s = tac_name; OPT "|"; l = LIST1 tacrule SEP "|"; "END" -> declare_tactic loc s l ] ] @@ -214,5 +200,10 @@ EXTEND GramTerminal s ] ] ; + tac_name: + [ [ s = LIDENT -> s + | s = UIDENT -> s + ] ] + ; END |