diff options
Diffstat (limited to 'grammar/q_util.mlp')
| -rw-r--r-- | grammar/q_util.mlp | 150 |
1 files changed, 0 insertions, 150 deletions
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp deleted file mode 100644 index a2007d258c..0000000000 --- a/grammar/q_util.mlp +++ /dev/null @@ -1,150 +0,0 @@ -(************************************************************************) -(* * 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 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* This file defines standard combinators to build ml expressions *) - -type argument_type = -| ListArgType of argument_type -| OptArgType of argument_type -| PairArgType of argument_type * argument_type -| ExtraArgType of string - -type user_symbol = -| Ulist1 of user_symbol -| Ulist1sep of user_symbol * string -| Ulist0 of user_symbol -| Ulist0sep of user_symbol * string -| Uopt of user_symbol -| Uentry of string -| Uentryl of string * int - -type extend_token = -| ExtTerminal of 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 = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in - <:expr< [$e1$ :: $e2$] >>) - 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 = 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 = Ploc.dummy - - -let mlexpr_of_bool = function - | true -> <:expr< True >> - | false -> <:expr< False >> - -let mlexpr_of_int n = <:expr< $int:string_of_int n$ >> - -let mlexpr_of_string s = <:expr< $str:s$ >> - -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 - | Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >> - | Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> - | 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$) >> - | Uentryl (e, l) -> - (** Keep in sync with Pcoq! *) - assert (e = "tactic"); - if l = 5 then <:expr< Extend.Aentry Pltac.binder_tactic >> - else <:expr< Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_string (string_of_int l)$ >> - -let rec type_of_user_symbol = function -| Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) -> - ListArgType (type_of_user_symbol s) -| Uopt s -> - OptArgType (type_of_user_symbol s) -| Uentry e | Uentryl (e, _) -> ExtraArgType e - -let coincide s pat off = - let len = String.length pat in - let break = ref true in - let i = ref 0 in - while !break && !i < len do - let c = Char.code s.[off + !i] in - let d = Char.code pat.[!i] in - break := c = d; - incr i - 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 - let entry = parse_user_entry (String.sub s 3 (l-12)) "" in - 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 - -let rec mlexpr_of_symbol = function -| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >> -| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >> -| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >> -| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >> -| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >> -| Uentry e -> - let wit = <:expr< $lid:"wit_"^e$ >> in - <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >> -| Uentryl (e, l) -> - assert (e = "tactic"); - let wit = <:expr< $lid:"wit_"^e$ >> in - <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>> - -let rec binders_of_tokens e = function -| [] -> e -| ExtNonTerminal(_,None) :: cl -> <:expr< fun _ -> $binders_of_tokens e cl$ >> -| ExtNonTerminal(_,Some id) :: cl -> <:expr< fun $lid:id$ -> $binders_of_tokens e cl$ >> -| ExtTerminal _ :: cl -> binders_of_tokens e cl |