diff options
Diffstat (limited to 'plugins/syntax/ascii_syntax.ml')
| -rw-r--r-- | plugins/syntax/ascii_syntax.ml | 47 |
1 files changed, 27 insertions, 20 deletions
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index e18d19ce..acb297dd 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -1,10 +1,13 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * 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) *) +(************************************************************************) + (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "ascii_syntax_plugin" @@ -24,6 +27,10 @@ let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false + let ascii_module = ["Coq";"Strings";"Ascii"] let ascii_path = make_path ascii_module "ascii" @@ -37,34 +44,34 @@ let glob_Ascii = lazy (make_reference "Ascii") open Lazy -let interp_ascii dloc p = +let interp_ascii ?loc p = let rec aux n p = if Int.equal n 0 then [] else let mp = p mod 2 in - GRef (dloc,(if Int.equal mp 0 then glob_false else glob_true),None) + (DAst.make ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None)) :: (aux (n-1) (p/2)) in - GApp (dloc,GRef(dloc,force glob_Ascii,None), aux 8 p) + DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p) -let interp_ascii_string dloc s = +let interp_ascii_string ?loc s = let p = if Int.equal (String.length s) 1 then int_of_char s.[0] else if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2] then int_of_string s else - user_err_loc (dloc,"interp_ascii_string", - str "Expects a single character or a three-digits ascii code.") in - interp_ascii dloc p + user_err ?loc ~hdr:"interp_ascii_string" + (str "Expects a single character or a three-digits ascii code.") in + interp_ascii ?loc p let uninterp_ascii r = let rec uninterp_bool_list n = function | [] when Int.equal n 0 -> 0 - | GRef (_,k,_)::l when Globnames.eq_gr k glob_true -> 1+2*(uninterp_bool_list (n-1) l) - | GRef (_,k,_)::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l) + | r::l when is_gr r glob_true -> 1+2*(uninterp_bool_list (n-1) l) + | r::l when is_gr r glob_false -> 2*(uninterp_bool_list (n-1) l) | _ -> raise Non_closed_ascii in try - let aux = function - | GApp (_,GRef (_,k,_),l) when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l + let aux c = match DAst.get c with + | GApp (r, l) when is_gr r (force glob_Ascii) -> uninterp_bool_list 8 l | _ -> raise Non_closed_ascii in Some (aux r) with @@ -74,10 +81,10 @@ let make_ascii_string n = if n>=32 && n<=126 then String.make 1 (char_of_int n) else Printf.sprintf "%03d" n -let uninterp_ascii_string r = Option.map make_ascii_string (uninterp_ascii r) +let uninterp_ascii_string (AnyGlobConstr r) = Option.map make_ascii_string (uninterp_ascii r) let _ = Notation.declare_string_interpreter "char_scope" (ascii_path,ascii_module) interp_ascii_string - ([GRef (Loc.ghost,static_glob_Ascii,None)], uninterp_ascii_string, true) + ([DAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true) |