diff options
Diffstat (limited to 'grammar/q_util.mlp')
| -rw-r--r-- | grammar/q_util.mlp | 40 |
1 files changed, 26 insertions, 14 deletions
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp index 2d5c4089..6cdd2ec1 100644 --- a/grammar/q_util.mlp +++ b/grammar/q_util.mlp @@ -1,15 +1,15 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* This file defines standard combinators to build ml expressions *) -open GramCompat - type argument_type = | ListArgType of argument_type | OptArgType of argument_type @@ -27,23 +27,23 @@ type user_symbol = type extend_token = | ExtTerminal of string -| ExtNonTerminal of user_symbol * string +| ExtNonTerminal of user_symbol * string option let mlexpr_of_list f l = List.fold_right (fun e1 e2 -> let e1 = f e1 in - let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in + let loc = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in <:expr< [$e1$ :: $e2$] >>) - l (let loc = CompatLoc.ghost in <:expr< [] >>) + l (let loc = Ploc.dummy in <:expr< [] >>) let mlexpr_of_pair m1 m2 (a1,a2) = let e1 = m1 a1 and e2 = m2 a2 in - let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in + let loc = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in <:expr< ($e1$, $e2$) >> (* We don't give location for tactic quotation! *) -let loc = CompatLoc.ghost +let loc = Ploc.dummy let mlexpr_of_bool = function @@ -58,6 +58,10 @@ let mlexpr_of_option f = function | None -> <:expr< None >> | Some e -> <:expr< Some $f e$ >> +let mlexpr_of_name f = function + | None -> <:expr< Names.Name.Anonymous >> + | Some e -> <:expr< Names.Name.Name $f e$ >> + let symbol_of_string s = <:expr< Extend.Atoken (CLexer.terminal $str:s$) >> let rec mlexpr_of_prod_entry_key f = function @@ -66,12 +70,12 @@ let rec mlexpr_of_prod_entry_key f = function | Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >> | Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> | Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >> - | Uentry e -> <:expr< Extend.Aentry $f e$ >> + | Uentry e -> <:expr< Extend.Aentry ($f e$) >> | Uentryl (e, l) -> (** Keep in sync with Pcoq! *) assert (e = "tactic"); - if l = 5 then <:expr< Extend.Aentry (Pcoq.Tactic.binder_tactic) >> - else <:expr< Extend.Aentryl (Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >> + if l = 5 then <:expr< Extend.Aentry Pltac.binder_tactic >> + else <:expr< Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_int l$ >> let rec type_of_user_symbol = function | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) -> @@ -92,10 +96,14 @@ let coincide s pat off = done; !break +let check_separator sep = + if sep <> "" then failwith "Separator is only for arguments with suffix _list_sep." + let rec parse_user_entry s sep = let l = String.length s in if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then let entry = parse_user_entry (String.sub s 3 (l-8)) "" in + check_separator sep; Ulist1 entry else if l > 12 && coincide s "ne_" 0 && coincide s "_list_sep" (l-9) then @@ -103,16 +111,20 @@ let rec parse_user_entry s sep = Ulist1sep (entry, sep) else if l > 5 && coincide s "_list" (l-5) then let entry = parse_user_entry (String.sub s 0 (l-5)) "" in + check_separator sep; Ulist0 entry else if l > 9 && coincide s "_list_sep" (l-9) then let entry = parse_user_entry (String.sub s 0 (l-9)) "" in Ulist0sep (entry, sep) else if l > 4 && coincide s "_opt" (l-4) then let entry = parse_user_entry (String.sub s 0 (l-4)) "" in + check_separator sep; Uopt entry else if l = 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then let n = Char.code s.[6] - 48 in + check_separator sep; Uentryl ("tactic", n) else let s = match s with "hyp" -> "var" | _ -> s in + check_separator sep; Uentry s |