diff options
Diffstat (limited to 'grammar/tacextend.ml4')
-rw-r--r-- | grammar/tacextend.ml4 | 234 |
1 files changed, 234 insertions, 0 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 new file mode 100644 index 000000000..3a47ade0d --- /dev/null +++ b/grammar/tacextend.ml4 @@ -0,0 +1,234 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <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 camlp4deps: "tools/compat5b.cmo" i*) + +open Util +open Pp +open Genarg +open Q_util +open Q_coqast +open Argextend +open Pcoq +open Extrawit +open Egramml +open Compat + +let rec make_patt = function + | [] -> <:patt< [] >> + | GramNonTerminal(loc',_,_,Some p)::l -> + let p = Names.string_of_id p in + <:patt< [ $lid:p$ :: $make_patt l$ ] >> + | _::l -> make_patt l + +let rec make_when loc = function + | [] -> <:expr< True >> + | GramNonTerminal(loc',t,_,Some p)::l -> + let p = Names.string_of_id p in + let l = make_when loc l in + let loc = join_loc loc' loc in + let t = mlexpr_of_argtype loc' t in + <:expr< Genarg.genarg_tag $lid:p$ = $t$ && $l$ >> + | _::l -> make_when loc l + +let rec make_let e = function + | [] -> e + | GramNonTerminal(loc,t,_,Some p)::l -> + let p = Names.string_of_id p in + 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 + <:expr< let $lid:p$ = $v$ in $e$ >> + | _::l -> make_let e l + +let rec extract_signature = function + | [] -> [] + | GramNonTerminal (_,t,_,_) :: l -> t :: extract_signature l + | _::l -> extract_signature l + +let check_unicity s l = + let l' = List.map (fun (l,_) -> extract_signature l) l in + if not (Util.list_distinct l') then + Pp.warning_with !Pp_control.err_ft + ("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_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; + Compat.make_fun loc (List.map make_clause l) + +let rec make_args = function + | [] -> <:expr< [] >> + | GramNonTerminal(loc,t,_,Some p)::l -> + let p = Names.string_of_id p in + <:expr< [ Genarg.in_gen $make_wit loc t$ $lid:p$ :: $make_args l$ ] >> + | _::l -> make_args l + +let rec make_eval_tactic e = function + | [] -> e + | GramNonTerminal(loc,tag,_,Some p)::l when is_tactic_genarg tag -> + 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 + <:expr< let $lid:p$ = $lid:p$ in $e$ >> + | _::l -> make_eval_tactic e l + +let rec make_fun e = function + | [] -> e + | GramNonTerminal(loc,_,_,Some p)::l -> + let p = Names.string_of_id p in + <:expr< fun $lid:p$ -> $make_fun e l$ >> + | _::l -> make_fun e l + +let mlexpr_terminals_of_grammar_tactic_prod_item_expr = function + | GramTerminal s -> <:expr< Some $mlexpr_of_string s$ >> + | GramNonTerminal (loc,nt,_,sopt) -> <:expr< None >> + +let make_prod_item = function + | GramTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> + | GramNonTerminal (loc,nt,g,sopt) -> + <:expr< Egramml.GramNonTerminal $default_loc$ $mlexpr_of_argtype loc nt$ + $mlexpr_of_prod_entry_key g$ $mlexpr_of_option mlexpr_of_ident sopt$ >> + +let mlexpr_of_clause = + mlexpr_of_list (fun (a,b) -> mlexpr_of_list make_prod_item a) + +let rec make_tags loc = function + | [] -> <:expr< [] >> + | GramNonTerminal(loc',t,_,Some p)::l -> + let l = make_tags loc l in + let loc = join_loc loc' loc in + let t = mlexpr_of_argtype loc' t in + <:expr< [ $t$ :: $l$ ] >> + | _::l -> make_tags loc l + +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_tactic_prod_item_expr pt in + <:expr< ($se$, $make_tags loc pt$, ($level$, $prods$)) >> + +let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se) + +let rec possibly_empty_subentries loc = function + | [] -> [] + | (s,prodsl) :: l -> + let rec aux = function + | [] -> (false,<:expr< None >>) + | prods :: rest -> + try + let l = List.map (function + | GramNonTerminal(_,(List0ArgType _| + OptArgType _| + ExtraArgType _ as t),_,_)-> + (* This possibly parses epsilon *) + let rawwit = make_rawwit loc t in + <:expr< match Genarg.default_empty_value $rawwit$ with + [ None -> failwith "" + | Some v -> + Tacinterp.intern_genarg Tacinterp.fully_empty_glob_sign + (Genarg.in_gen $rawwit$ v) ] >> + | GramTerminal _ | GramNonTerminal(_,_,_,_) -> + (* This does not parse epsilon (this Exit is static time) *) + raise Exit) prods in + if has_extraarg prods then + (true,<:expr< try Some $mlexpr_of_list (fun x -> x) l$ + with [ Failure "" -> $snd (aux rest)$ ] >>) + else + (true, <:expr< Some $mlexpr_of_list (fun x -> x) l$ >>) + with Exit -> aux rest in + let (nonempty,v) = aux prodsl in + if nonempty then (s,v) :: possibly_empty_subentries loc l + else possibly_empty_subentries loc l + +let possibly_atomic loc prods = + let l = list_map_filter (function + | GramTerminal s :: l, _ -> Some (s,l) + | _ -> None) prods in + possibly_empty_subentries loc (list_factorize_left l) + +let declare_tactic loc s cl = + 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 e = + make_fun + <:expr< + 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 atomic_tactics = + mlexpr_of_list (mlexpr_of_pair mlexpr_of_string (fun x -> x)) + (possibly_atomic loc cl) in + declare_str_items loc + (hidden @ + [ <:str_item< do { + try + let _=Tacinterp.add_tactic $se$ $make_fun_clauses loc s cl$ in + List.iter + (fun (s,l) -> match l with + [ Some l -> + Tacinterp.add_primitive_tactic s + (Tacexpr.TacAtom($default_loc$, + Tacexpr.TacExtend($default_loc$,$se$,l))) + | None -> () ]) + $atomic_tactics$ + with e -> Pp.pp (Errors.print e); + Egramml.extend_tactic_grammar $se$ $gl$; + List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >> + ]) + +open Pcaml +open PcamlSig + +EXTEND + GLOBAL: str_item; + str_item: + [ [ "TACTIC"; "EXTEND"; s = tac_name; + OPT "|"; l = LIST1 tacrule SEP "|"; + "END" -> + declare_tactic loc s l ] ] + ; + tacrule: + [ [ "["; l = LIST1 tacargs; "]"; "->"; "["; e = Pcaml.expr; "]" + -> + if match List.hd l with GramNonTerminal _ -> true | _ -> false then + (* En attendant la syntaxe de tacticielles *) + failwith "Tactic syntax must start with an identifier"; + (l,e) + ] ] + ; + tacargs: + [ [ e = LIDENT; "("; s = LIDENT; ")" -> + let t, g = interp_entry_name false None e "" in + GramNonTerminal (loc, t, g, Some (Names.id_of_string s)) + | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> + let t, g = interp_entry_name false None e sep in + GramNonTerminal (loc, t, g, Some (Names.id_of_string s)) + | s = STRING -> + if s = "" then Errors.user_err_loc (loc,"",Pp.str "Empty terminal."); + GramTerminal s + ] ] + ; + tac_name: + [ [ s = LIDENT -> s + | s = UIDENT -> s + ] ] + ; + END |