diff options
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 11 | ||||
| -rw-r--r-- | grammar/q_util.ml4 | 26 | ||||
| -rw-r--r-- | grammar/q_util.mli | 2 | ||||
| -rw-r--r-- | grammar/tacextend.ml4 | 3 | ||||
| -rw-r--r-- | grammar/vernacextend.ml4 | 8 |
5 files changed, 20 insertions, 30 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 41e94914e..82bc09519 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -46,18 +46,16 @@ let has_extraarg l = let make_act loc act pil = let rec make = function | [] -> <:expr< (fun loc -> $act$) >> - | ExtNonTerminal (t, _, p) :: tl -> - <:expr< - (fun $lid:p$ -> - let _ = Genarg.in_gen $make_rawwit loc t$ $lid:p$ in $make tl$) - >> + | ExtNonTerminal (t, _, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >> | ExtTerminal _ :: tl -> <:expr< (fun _ -> $make tl$) >> in make (List.rev pil) let make_prod_item = function | ExtTerminal s -> <:expr< Pcoq.Atoken (Lexer.terminal $mlexpr_of_string s$) >> - | ExtNonTerminal (_, g, _) -> mlexpr_of_prod_entry_key g + | ExtNonTerminal (_, g, _) -> + let base s = <:expr< Pcoq.name_of_entry $lid:s$ >> in + mlexpr_of_prod_entry_key base g let rec make_prod = function | [] -> <:expr< Extend.Stop >> @@ -174,7 +172,6 @@ let declare_vernac_argument loc s pr cl = (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not wit printer")) } >> ] -open Pcoq open Pcaml open PcamlSig (* necessary for camlp4 *) diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index 3946d5d2b..c43ce15be 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -47,31 +47,23 @@ let mlexpr_of_option f = function let mlexpr_of_ident id = <:expr< Names.Id.of_string $str:id$ >> -let rec mlexpr_of_prod_entry_key = function - | Extend.Ulist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >> - | Extend.Ulist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> - | Extend.Ulist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key s$ >> - | Extend.Ulist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> - | Extend.Uopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key s$ >> - | Extend.Umodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >> - | Extend.Uentry e -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:e$) >> +let rec mlexpr_of_prod_entry_key f = function + | Extend.Ulist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key f s$ >> + | Extend.Ulist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >> + | Extend.Ulist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key f s$ >> + | Extend.Ulist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >> + | Extend.Uopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key f s$ >> + | Extend.Umodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key f s$ >> + | Extend.Uentry e -> <:expr< Pcoq.Aentry $f e$ >> | Extend.Uentryl (e, l) -> (** Keep in sync with Pcoq! *) assert (CString.equal e "tactic"); if l = 5 then <:expr< Pcoq.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >> else <:expr< Pcoq.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >> -let type_entry u e = - let Pcoq.TypedEntry (t, _) = Pcoq.get_entry u e in - Genarg.unquote t - let rec type_of_user_symbol = function | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) | Umodifiers s -> Genarg.ListArgType (type_of_user_symbol s) | Uopt s -> Genarg.OptArgType (type_of_user_symbol s) -| Uentry e | Uentryl (e, _) -> - try type_entry Pcoq.uprim e with Not_found -> - try type_entry Pcoq.uconstr e with Not_found -> - try type_entry Pcoq.utactic e with Not_found -> - Genarg.ExtraArgType e +| Uentry e | Uentryl (e, _) -> Genarg.ExtraArgType e diff --git a/grammar/q_util.mli b/grammar/q_util.mli index 837ec6fb0..712aa8509 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -28,6 +28,6 @@ val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr val mlexpr_of_ident : string -> MLast.expr -val mlexpr_of_prod_entry_key : Extend.user_symbol -> MLast.expr +val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> Extend.user_symbol -> MLast.expr val type_of_user_symbol : Extend.user_symbol -> Genarg.argument_type diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index c35fa00d2..8c85d0162 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -85,8 +85,9 @@ let make_fun_clauses loc s l = let make_prod_item = function | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> | ExtNonTerminal (nt, g, id) -> + let base s = <:expr< Pcoq.genarg_grammar $mk_extraarg loc s$ >> in <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$ - $mlexpr_of_prod_entry_key g$ >> + $mlexpr_of_prod_entry_key base g$ >> let mlexpr_of_clause cl = mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 3bb1e0907..d8c885088 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -42,7 +42,7 @@ let rec make_let e = function let make_clause { r_patt = pt; r_branch = e; } = (make_patt pt, - vala (Some (make_when (MLast.loc_of_expr e) pt)), + vala None, make_let e pt) (* To avoid warnings *) @@ -58,11 +58,11 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = match c ,cg with | Some c, _ -> (make_patt pt, - vala (Some (make_when (MLast.loc_of_expr c) pt)), + vala None, make_let (mk_ignore c pt) pt) | None, Some cg -> (make_patt pt, - vala (Some (make_when (MLast.loc_of_expr cg) pt)), + vala None, <:expr< fun () -> $cg$ $str:s$ >>) | None, None -> msg_warning (strbrk("Vernac entry \""^s^"\" misses a classifier. "^ @@ -85,7 +85,7 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = strbrk("Specific classifiers have precedence over global "^ "classifiers. Only one classifier is called.")++fnl()); (make_patt pt, - vala (Some (make_when loc pt)), + vala None, <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) let make_fun_clauses loc s l = |