diff options
| author | Jason Gross | 2018-11-07 21:19:05 -0500 |
|---|---|---|
| committer | Jason Gross | 2018-11-28 15:01:17 -0500 |
| commit | e30e864d61431a0145853fcf90b5f16b781f4a46 (patch) | |
| tree | af7733b501fb880d16ba6986748ac82e2a629dd7 | |
| parent | 320f8c4503293b37c852548e4d19ff4dd1c191cb (diff) | |
Add `String Notation` vernacular like `Numeral Notation`
Users can now register string notations for custom inductives.
Much of the code and documentation was copied from numeral notations.
I chose to use a 256-constructor inductive for primitive string syntax
because (a) it is easy to convert between character codes and
constructors, and (b) it is more efficient than the existing `ascii`
type.
Some choices about proofs of the new `byte` type were made based on
efficiency. For example, https://github.com/coq/coq/issues/8517 means
that we cannot simply use `Scheme Equality` for this type, and I have
taken some care to ensure that the proofs of decidable equality and
conversion are fast. (Unfortunately, the `Init/Byte.v` file is the
slowest one in the prelude (it takes a couple of seconds to build), and
I'm not sure where the slowness is.)
In String.v, some uses of `0` as a `nat` were replaced by `O`, because
the file initially refused to check interactively otherwise (it
complained that `0` could not be interpreted in `string_scope` before
loading `Coq.Strings.String`).
There is unfortunately a decent amount of code duplication between
numeral notations and string notations.
I have not put too much thought into chosing names; most names have been
chosen to be similar to numeral notations, though I chose the name
`byte` from
https://github.com/coq/coq/issues/8483#issuecomment-421671785.
Unfortunately, this feature does not support declaring string syntax for
`list ascii`, unless that type is wrapped in a record or other inductive
type. This is not a fundamental limitation; it should be relatively
easy for someone who knows the API of the reduction machinery in Coq to
extend both this and numeral notations to support any type whose hnf
starts with an inductive type. (The reason for needing an inductive
type to bottom out at is that this is how the plugin determines what
constructors are the entry points for printing the given notation.
However, see also https://github.com/coq/coq/issues/8964 for
complications that are more likely to arise if inductive type families
are supported.)
N.B. I generated the long lists of constructors for the `byte` type with
short python scripts.
Closes #8853
29 files changed, 3466 insertions, 260 deletions
diff --git a/CHANGES.md b/CHANGES.md index 1f88b77b51..85094ac205 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -46,6 +46,9 @@ Notations `Bind Scope`, `Delimit Scope`, `Undelimit Scope`, or `Notation` is deprecated. +- New command `String Notation` to register string syntax for custom + inductive types. + Plugins - The quote plugin (https://coq.inria.fr/distrib/V8.8.1/refman/proof-engine/detailed-tactic-examples.html#quote) diff --git a/META.coq.in b/META.coq.in index 181887bc3d..03f3fdf852 100644 --- a/META.coq.in +++ b/META.coq.in @@ -459,28 +459,16 @@ package "plugins" ( archive(native) = "int31_syntax_plugin.cmx" ) - package "asciisyntax" ( + package "string_notation" ( - description = "Coq asciisyntax plugin" + description = "Coq string_notation plugin" version = "8.10" requires = "" directory = "syntax" - archive(byte) = "ascii_syntax_plugin.cmo" - archive(native) = "ascii_syntax_plugin.cmx" - ) - - package "stringsyntax" ( - - description = "Coq stringsyntax plugin" - version = "8.10" - - requires = "coq.plugins.asciisyntax" - directory = "syntax" - - archive(byte) = "string_syntax_plugin.cmo" - archive(native) = "string_syntax_plugin.cmx" + archive(byte) = "string_notation_plugin.cmo" + archive(native) = "string_notation_plugin.cmx" ) package "derive" ( diff --git a/Makefile.common b/Makefile.common index ca2cb8fee6..2ee3fa6547 100644 --- a/Makefile.common +++ b/Makefile.common @@ -140,9 +140,8 @@ RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo SYNTAXCMO:=$(addprefix plugins/syntax/, \ r_syntax_plugin.cmo \ int31_syntax_plugin.cmo \ - ascii_syntax_plugin.cmo \ - string_syntax_plugin.cmo \ - numeral_notation_plugin.cmo) + numeral_notation_plugin.cmo \ + string_notation_plugin.cmo) DERIVECMO:=plugins/derive/derive_plugin.cmo LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 65df89da6c..55508f04f2 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1522,6 +1522,104 @@ Numeral notations As noted above, the :n:`(abstract after @num)` directive has no effect when :n:`@ident__2` lands in an :g:`option` type. +String notations +----------------- + +.. cmd:: String Notation @ident__1 @ident__2 @ident__3 : @scope. + :name: String Notation + + This command allows the user to customize the way strings are parsed + and printed. + + The token :n:`@ident__1` should be the name of an inductive type, + while :n:`@ident__2` and :n:`@ident__3` should be the names of the + parsing and printing functions, respectively. The parsing function + :n:`@ident__2` should have one of the following types: + + * :n:`Byte.byte -> @ident__1` + * :n:`Byte.byte -> option @ident__1` + * :n:`list Byte.byte -> @ident__1` + * :n:`list Byte.byte -> option @ident__1` + + And the printing function :n:`@ident__3` should have one of the + following types: + + * :n:`@ident__1 -> Byte.byte` + * :n:`@ident__1 -> option Byte.byte` + * :n:`@ident__1 -> list Byte.byte` + * :n:`@ident__1 -> option (list Byte.byte)` + + When parsing, the application of the parsing function + :n:`@ident__2` to the string will be fully reduced, and universes + of the resulting term will be refreshed. + + .. exn:: Cannot interpret this string as a value of type @type + + The string notation registered for :token:`type` does not support + the given string. This error is given when the interpretation + function returns :g:`None`. + + .. exn:: @ident should go from Byte.byte or (list Byte.byte) to @type or (option @type). + + The parsing function given to the :cmd:`String Notation` + vernacular is not of the right type. + + .. exn:: @ident should go from @type to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)). + + The printing function given to the :cmd:`String Notation` + vernacular is not of the right type. + + .. exn:: @type is not an inductive type. + + String notations can only be declared for inductive types with no + arguments. + + .. exn:: Unexpected term @term while parsing a string notation. + + Parsing functions must always return ground terms, made up of + applications of constructors and inductive types. Parsing + functions may not return terms containing axioms, bare + (co)fixpoints, lambdas, etc. + + .. exn:: Unexpected non-option term @term while parsing a string notation. + + Parsing functions expected to return an :g:`option` must always + return a concrete :g:`Some` or :g:`None` when applied to a + concrete string expressed as a decimal. They may not return + opaque constants. + + .. exn:: Cannot interpret in @scope because @ident could not be found in the current environment. + + The inductive type used to register the string notation is no + longer available in the environment. Most likely, this is because + the string notation was declared inside a functor for an + inductive type inside the functor. This use case is not currently + supported. + + Alternatively, you might be trying to use a primitive token + notation from a plugin which forgot to specify which module you + must :g:`Require` for access to that notation. + + .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). + + The type passed to :cmd:`String Notation` must be a single + identifier. + + .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). + + Both functions passed to :cmd:`String Notation` must be single + identifiers. + + .. exn:: The reference @ident was not found in the current environment. + + Identifiers passed to :cmd:`String Notation` must exist in the + global environment. + + .. exn:: @ident is bound to a notation that does not denote a reference. + + Identifiers passed to :cmd:`String Notation` must be global + references, or notations which denote to single identifiers. + .. _TacticNotation: Tactic Notations diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 4fc9bf9e19..51f94d7e5a 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -17,6 +17,7 @@ through the <tt>Require Import</tt> command.</p> theories/Init/Datatypes.v theories/Init/Logic.v theories/Init/Logic_Type.v + theories/Init/Byte.v theories/Init/Nat.v theories/Init/Decimal.v theories/Init/Peano.v @@ -497,6 +498,7 @@ through the <tt>Require Import</tt> command.</p> Implementation of string as list of ascii characters </dt> <dd> + theories/Strings/Byte.v theories/Strings/Ascii.v theories/Strings/String.v theories/Strings/BinaryString.v diff --git a/interp/notation.ml b/interp/notation.ml index db8ee5bc18..b6322c7441 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -395,11 +395,12 @@ let prim_token_uninterpreters = (*******************************************************) (* Numeral notation interpretation *) -type numeral_notation_error = +type numeral_or_string_notation_error = | UnexpectedTerm of Constr.t | UnexpectedNonOptionTerm of Constr.t -exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error +exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_or_string_notation_error +exception StringNotationError of Environ.env * Evd.evar_map * numeral_or_string_notation_error type numnot_option = | Nop @@ -419,8 +420,13 @@ type target_kind = | UInt of Names.inductive (* Coq.Init.Decimal.uint *) | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) +type string_target_kind = + | ListByte + | Byte + type option_kind = Option | Direct type conversion_kind = target_kind * option_kind +type string_conversion_kind = string_target_kind * option_kind type numeral_notation_obj = { to_kind : conversion_kind; @@ -430,6 +436,13 @@ type numeral_notation_obj = num_ty : Libnames.qualid; (* for warnings / error messages *) warning : numnot_option } +type string_notation_obj = + { sto_kind : string_conversion_kind; + sto_ty : GlobRef.t; + sof_kind : string_conversion_kind; + sof_ty : GlobRef.t; + string_ty : Libnames.qualid (* for warnings / error messages *) } + module Numeral = struct (** * Numeral notation *) @@ -707,6 +720,185 @@ let uninterp o (Glob_term.AnyGlobConstr n) = | NotANumber -> None (* all other functions except big2raw *) end +module Strings = struct +(** * String notation *) + +(** Reduction + + The constr [c] below isn't necessarily well-typed, since we + built it via an [mkApp] of a conversion function on a term + that starts with the right constructor but might be partially + applied. + + At least [c] is known to be evar-free, since it comes from + our own ad-hoc [constr_of_glob] or from conversions such + as [coqint_of_rawnum]. +*) + +let eval_constr env sigma (c : Constr.t) = + let c = EConstr.of_constr c in + let sigma,t = Typing.type_of env sigma c in + let c' = Vnorm.cbv_vm env sigma c t in + EConstr.Unsafe.to_constr c' + +(* For testing with "compute" instead of "vm_compute" : +let eval_constr env sigma (c : Constr.t) = + let c = EConstr.of_constr c in + let c' = Tacred.compute env sigma c in + EConstr.Unsafe.to_constr c' +*) + +let eval_constr_app env sigma c1 c2 = + eval_constr env sigma (mkApp (c1,[| c2 |])) + +exception NotAString + +let qualid_of_ref n = + n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty + +let q_list () = qualid_of_ref "core.list.type" +let q_byte () = qualid_of_ref "core.byte.type" + +let unsafe_locate_ind q = + match Nametab.locate q with + | IndRef i -> i + | _ -> raise Not_found + +let locate_list () = unsafe_locate_ind (q_list ()) +let locate_byte () = unsafe_locate_ind (q_byte ()) + +(***********************************************************************) + +(** ** Conversion between Coq [list Byte.byte] and internal raw string *) + +let coqbyte_of_char_code byte c = + mkConstruct (byte, 1 + c) + +let coqbyte_of_string ?loc byte 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 ~hdr:"coqbyte_of_string" + (str "Expects a single character or a three-digits ascii code.") in + coqbyte_of_char_code byte p + +let coqbyte_of_char byte c = coqbyte_of_char_code byte (Char.code c) + +let make_ascii_string n = + if n>=32 && n<=126 then String.make 1 (char_of_int n) + else Printf.sprintf "%03d" n + +let char_code_of_coqbyte c = + match Constr.kind c with + | Construct ((_,c), _) -> c - 1 + | _ -> raise NotAString + +let string_of_coqbyte c = make_ascii_string (char_code_of_coqbyte c) + +let coqlist_byte_of_string byte_ty list_ty str = + let cbyte = mkInd byte_ty in + let nil = mkApp (mkConstruct (list_ty, 1), [|cbyte|]) in + let cons x xs = mkApp (mkConstruct (list_ty, 2), [|cbyte; x; xs|]) in + let rec do_chars s i acc = + if i < 0 then acc + else + let b = coqbyte_of_char byte_ty s.[i] in + do_chars s (i-1) (cons b acc) + in + do_chars str (String.length str - 1) nil + +(* N.B. We rely on the fact that [nil] is the first constructor and [cons] is the second constructor, for [list] *) +let string_of_coqlist_byte c = + let rec of_coqlist_byte_loop c buf = + match Constr.kind c with + | App (_nil, [|_ty|]) -> () + | App (_cons, [|_ty;b;c|]) -> + let () = Buffer.add_char buf (Char.chr (char_code_of_coqbyte b)) in + of_coqlist_byte_loop c buf + | _ -> raise NotAString + in + let buf = Buffer.create 64 in + let () = of_coqlist_byte_loop c buf in + Buffer.contents buf + +(** The uninterp function below work at the level of [glob_constr] + which is too low for us here. So here's a crude conversion back + to [constr] for the subset that concerns us. *) + +let rec constr_of_glob env sigma g = match DAst.get g with + | Glob_term.GRef (ConstructRef c, _) -> + let sigma,c = Evd.fresh_constructor_instance env sigma c in + sigma,mkConstructU c + | Glob_term.GApp (gc, gcl) -> + let sigma,c = constr_of_glob env sigma gc in + let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in + sigma,mkApp (c, Array.of_list cl) + | _ -> + raise NotAString + +let rec glob_of_constr ?loc env sigma c = match Constr.kind c with + | App (c, ca) -> + let c = glob_of_constr ?loc env sigma c in + let cel = List.map (glob_of_constr ?loc env sigma) (Array.to_list ca) in + DAst.make ?loc (Glob_term.GApp (c, cel)) + | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None)) + | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None)) + | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None)) + | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None)) + | _ -> Loc.raise ?loc (StringNotationError(env,sigma,UnexpectedTerm c)) + +let no_such_string ?loc ty = + CErrors.user_err ?loc + (str "Cannot interpret this string as a value of type " ++ + pr_qualid ty) + +let interp_option ty ?loc env sigma c = + match Constr.kind c with + | App (_Some, [| _; c |]) -> glob_of_constr ?loc env sigma c + | App (_None, [| _ |]) -> no_such_string ?loc ty + | x -> Loc.raise ?loc (StringNotationError(env,sigma,UnexpectedNonOptionTerm c)) + +let uninterp_option c = + match Constr.kind c with + | App (_Some, [| _; x |]) -> x + | _ -> raise NotAString + +let interp o ?loc n = + let byte_ty = locate_byte () in + let list_ty = locate_list () in + let c = match fst o.sto_kind with + | ListByte -> coqlist_byte_of_string byte_ty list_ty n + | Byte -> coqbyte_of_string ?loc byte_ty n + in + let env = Global.env () in + let sigma = Evd.from_env env in + let sigma,to_ty = Evd.fresh_global env sigma o.sto_ty in + let to_ty = EConstr.Unsafe.to_constr to_ty in + let res = eval_constr_app env sigma to_ty c in + match snd o.sto_kind with + | Direct -> glob_of_constr ?loc env sigma res + | Option -> interp_option o.string_ty ?loc env sigma res + +let uninterp o (Glob_term.AnyGlobConstr n) = + let env = Global.env () in + let sigma = Evd.from_env env in + let sigma,of_ty = Evd.fresh_global env sigma o.sof_ty in + let of_ty = EConstr.Unsafe.to_constr of_ty in + try + let sigma,n = constr_of_glob env sigma n in + let c = eval_constr_app env sigma of_ty n in + let c = if snd o.sof_kind == Direct then c else uninterp_option c in + match fst o.sof_kind with + | ListByte -> Some (string_of_coqlist_byte c) + | Byte -> Some (string_of_coqbyte c) + with + | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *) + | NotAString -> None (* all other functions except big2raw *) +end + (* A [prim_token_infos], which is synchronized with the document state, either contains a unique id pointing to an unsynchronized prim token function, or a numeral notation object describing how to @@ -718,6 +910,7 @@ end type prim_token_interp_info = Uid of prim_token_uid | NumeralNotation of numeral_notation_obj + | StringNotation of string_notation_obj type prim_token_infos = { pt_local : bool; (** Is this interpretation local? *) @@ -942,6 +1135,7 @@ let find_prim_token check_allowed ?loc p sc = let interp = match info with | Uid uid -> Hashtbl.find prim_token_interpreters uid | NumeralNotation o -> InnerPrimToken.RawNumInterp (Numeral.interp o) + | StringNotation o -> InnerPrimToken.StringInterp (Strings.interp o) in let pat = InnerPrimToken.do_interp ?loc interp p in check_allowed pat; @@ -1122,6 +1316,7 @@ let uninterp_prim_token c = let uninterp = match info with | Uid uid -> Hashtbl.find prim_token_uninterpreters uid | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o) + | StringNotation o -> InnerPrimToken.StringUninterp (Strings.uninterp o) in match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with | None -> raise Notation_ops.No_match @@ -1141,6 +1336,8 @@ let availability_of_prim_token n printer_scope local_scopes = match n, uid with | Numeral _, NumeralNotation _ -> true | _, NumeralNotation _ -> false + | String _, StringNotation _ -> true + | _, StringNotation _ -> false | _, Uid uid -> let interp = Hashtbl.find prim_token_interpreters uid in match n, interp with diff --git a/interp/notation.mli b/interp/notation.mli index 734198bbf6..6880b9a2cd 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -104,11 +104,12 @@ val register_string_interpretation : (** * Numeral notation *) -type numeral_notation_error = +type numeral_or_string_notation_error = | UnexpectedTerm of Constr.t | UnexpectedNonOptionTerm of Constr.t -exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error +exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_or_string_notation_error +exception StringNotationError of Environ.env * Evd.evar_map * numeral_or_string_notation_error type numnot_option = | Nop @@ -128,8 +129,13 @@ type target_kind = | UInt of Names.inductive (* Coq.Init.Decimal.uint *) | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) +type string_target_kind = + | ListByte + | Byte + type option_kind = Option | Direct type conversion_kind = target_kind * option_kind +type string_conversion_kind = string_target_kind * option_kind type numeral_notation_obj = { to_kind : conversion_kind; @@ -139,9 +145,17 @@ type numeral_notation_obj = num_ty : Libnames.qualid; (* for warnings / error messages *) warning : numnot_option } +type string_notation_obj = + { sto_kind : string_conversion_kind; + sto_ty : GlobRef.t; + sof_kind : string_conversion_kind; + sof_ty : GlobRef.t; + string_ty : Libnames.qualid (* for warnings / error messages *) } + type prim_token_interp_info = Uid of prim_token_uid | NumeralNotation of numeral_notation_obj + | StringNotation of string_notation_obj type prim_token_infos = { pt_local : bool; (** Is this interpretation local? *) diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml deleted file mode 100644 index 94255bab6c..0000000000 --- a/plugins/syntax/ascii_syntax.ml +++ /dev/null @@ -1,100 +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) *) -(************************************************************************) - - -(* Poor's man DECLARE PLUGIN *) -let __coq_plugin_name = "ascii_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -open Pp -open CErrors -open Util -open Names -open Glob_term -open Globnames -open Coqlib - -exception Non_closed_ascii - -let make_dir l = DirPath.make (List.rev_map Id.of_string l) -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, _) -> GlobRef.equal r gr -| _ -> false - -let ascii_module = ["Coq";"Strings";"Ascii"] -let ascii_modpath = MPfile (make_dir ascii_module) - -let ascii_path = make_path ascii_module "ascii" - -let ascii_label = Label.make "ascii" -let ascii_kn = MutInd.make2 ascii_modpath ascii_label -let path_of_Ascii = ((ascii_kn,0),1) -let static_glob_Ascii = ConstructRef path_of_Ascii - -let glob_Ascii = lazy (lib_ref "plugins.syntax.Ascii") - -open Lazy - -let interp_ascii ?loc p = - let rec aux n p = - if Int.equal n 0 then [] else - let mp = p mod 2 in - (DAst.make ?loc @@ GRef (lib_ref (if Int.equal mp 0 then "core.bool.false" else "core.bool.true"),None)) - :: (aux (n-1) (p/2)) in - DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p) - -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 ~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 - | r::l when is_gr r (lib_ref "core.bool.true") -> 1+2*(uninterp_bool_list (n-1) l) - | r::l when is_gr r (lib_ref "core.bool.false") -> 2*(uninterp_bool_list (n-1) l) - | _ -> raise Non_closed_ascii in - try - 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 - Non_closed_ascii -> None - -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 (AnyGlobConstr r) = Option.map make_ascii_string (uninterp_ascii r) - -open Notation - -let at_declare_ml_module f x = - Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name - -let _ = - let sc = "char_scope" in - register_string_interpretation sc (interp_ascii_string,uninterp_ascii_string); - at_declare_ml_module enable_prim_token_interpretation - { pt_local = false; - pt_scope = sc; - pt_interp_info = Uid sc; - pt_required = (ascii_path,ascii_module); - pt_refs = [static_glob_Ascii]; - pt_in_match = true } diff --git a/plugins/syntax/ascii_syntax_plugin.mlpack b/plugins/syntax/ascii_syntax_plugin.mlpack deleted file mode 100644 index 7b9213a0e2..0000000000 --- a/plugins/syntax/ascii_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -Ascii_syntax diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg new file mode 100644 index 0000000000..1e06cd8ddb --- /dev/null +++ b/plugins/syntax/g_string.mlg @@ -0,0 +1,25 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +DECLARE PLUGIN "string_notation_plugin" + +{ + +open String_notation +open Names +open Stdarg + +} + +VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF + | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":" + ident(sc) ] -> + { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) } +END diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune index bfdd480fe9..1ab16c700d 100644 --- a/plugins/syntax/plugin_base.dune +++ b/plugins/syntax/plugin_base.dune @@ -6,6 +6,13 @@ (libraries coq.plugins.ltac)) (library + (name string_notation_plugin) + (public_name coq.plugins.string_notation) + (synopsis "Coq string notation plugin") + (modules g_string string_notation) + (libraries coq.vernac)) + +(library (name r_syntax_plugin) (public_name coq.plugins.r_syntax) (synopsis "Coq syntax plugin: reals") @@ -13,23 +20,8 @@ (libraries coq.vernac)) (library - (name ascii_syntax_plugin) - (public_name coq.plugins.ascii_syntax) - (synopsis "Coq syntax plugin: ASCII") - (modules ascii_syntax) - (libraries coq.vernac)) - -(library - (name string_syntax_plugin) - (public_name coq.plugins.string_syntax) - (synopsis "Coq syntax plugin: strings") - (modules string_syntax) - (libraries coq.plugins.ascii_syntax)) - -(library (name int31_syntax_plugin) (public_name coq.plugins.int31_syntax) (synopsis "Coq syntax plugin: int31") (modules int31_syntax) (libraries coq.vernac)) - diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml new file mode 100644 index 0000000000..fff8e928c3 --- /dev/null +++ b/plugins/syntax/string_notation.ml @@ -0,0 +1,97 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +open Pp +open Util +open Names +open Libnames +open Globnames +open Constrexpr +open Constrexpr_ops +open Notation + +(** * String notation *) + +let get_constructors ind = + let mib,oib = Global.lookup_inductive ind in + let mc = oib.Declarations.mind_consnames in + Array.to_list + (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc) + +let qualid_of_ref n = + n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty + +let q_option () = qualid_of_ref "core.option.type" +let q_list () = qualid_of_ref "core.list.type" +let q_byte () = qualid_of_ref "core.byte.type" + +let has_type f ty = + let (sigma, env) = Pfedit.get_current_context () in + let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in + try let _ = Constrintern.interp_constr env sigma c in true + with Pretype_errors.PretypeError _ -> false + +let type_error_to f ty = + CErrors.user_err + (pr_qualid f ++ str " should go from Byte.byte or (list Byte.byte) to " ++ + pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ").") + +let type_error_of g ty = + CErrors.user_err + (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ + str " to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)).") + +let vernac_string_notation local ty f g scope = + let app x y = mkAppC (x,[y]) in + let cref q = mkRefC q in + let cbyte = cref (q_byte ()) in + let clist = cref (q_list ()) in + let coption = cref (q_option ()) in + let opt r = app coption r in + let clist_byte = app clist cbyte in + let tyc = Smartlocate.global_inductive_with_alias ty in + let to_ty = Smartlocate.global_with_alias f in + let of_ty = Smartlocate.global_with_alias g in + let cty = cref ty in + let arrow x y = + mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) + in + let constructors = get_constructors tyc in + (* Check the type of f *) + let to_kind = + if has_type f (arrow clist_byte cty) then ListByte, Direct + else if has_type f (arrow clist_byte (opt cty)) then ListByte, Option + else if has_type f (arrow cbyte cty) then Byte, Direct + else if has_type f (arrow cbyte (opt cty)) then Byte, Option + else type_error_to f ty + in + (* Check the type of g *) + let of_kind = + if has_type g (arrow cty clist_byte) then ListByte, Direct + else if has_type g (arrow cty (opt clist_byte)) then ListByte, Option + else if has_type g (arrow cty cbyte) then Byte, Direct + else if has_type g (arrow cty (opt cbyte)) then Byte, Option + else type_error_of g ty + in + let o = { sto_kind = to_kind; + sto_ty = to_ty; + sof_kind = of_kind; + sof_ty = of_ty; + string_ty = ty } + in + let i = + { pt_local = local; + pt_scope = scope; + pt_interp_info = StringNotation o; + pt_required = Nametab.path_of_global (IndRef tyc),[]; + pt_refs = constructors; + pt_in_match = true } + in + enable_prim_token_interpretation i diff --git a/plugins/syntax/string_notation.mli b/plugins/syntax/string_notation.mli new file mode 100644 index 0000000000..9a0174abf2 --- /dev/null +++ b/plugins/syntax/string_notation.mli @@ -0,0 +1,16 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +open Libnames +open Vernacexpr + +(** * String notation *) + +val vernac_string_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> unit diff --git a/plugins/syntax/string_notation_plugin.mlpack b/plugins/syntax/string_notation_plugin.mlpack new file mode 100644 index 0000000000..6aa081dab4 --- /dev/null +++ b/plugins/syntax/string_notation_plugin.mlpack @@ -0,0 +1,2 @@ +String_notation +G_string diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml deleted file mode 100644 index 59e65a0672..0000000000 --- a/plugins/syntax/string_syntax.ml +++ /dev/null @@ -1,81 +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) *) -(************************************************************************) - -open Names -open Globnames -open Ascii_syntax_plugin.Ascii_syntax -open Glob_term -open Coqlib - -(* Poor's man DECLARE PLUGIN *) -let __coq_plugin_name = "string_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -exception Non_closed_string - -(* make a string term from the string s *) - -let string_module = ["Coq";"Strings";"String"] - -let string_modpath = MPfile (make_dir string_module) -let string_path = make_path string_module "string" - -let string_kn = MutInd.make2 string_modpath @@ Label.make "string" -let static_glob_EmptyString = ConstructRef ((string_kn,0),1) -let static_glob_String = ConstructRef ((string_kn,0),2) - -let glob_String = lazy (lib_ref "plugins.syntax.String") -let glob_EmptyString = lazy (lib_ref "plugins.syntax.EmptyString") - -let is_gr c gr = match DAst.get c with -| GRef (r, _) -> GlobRef.equal r gr -| _ -> false - -open Lazy - -let interp_string ?loc s = - let le = String.length s in - let rec aux n = - if n = le then DAst.make ?loc @@ GRef (force glob_EmptyString, None) else - DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef (force glob_String, None), - [interp_ascii ?loc (int_of_char s.[n]); aux (n+1)]) - in aux 0 - -let uninterp_string (AnyGlobConstr r) = - try - let b = Buffer.create 16 in - let rec aux c = match DAst.get c with - | GApp (k,[a;s]) when is_gr k (force glob_String) -> - (match uninterp_ascii a with - | Some c -> Buffer.add_char b (Char.chr c); aux s - | _ -> raise Non_closed_string) - | GRef (z,_) when GlobRef.equal z (force glob_EmptyString) -> - Some (Buffer.contents b) - | _ -> - raise Non_closed_string - in aux r - with - Non_closed_string -> None - -open Notation - -let at_declare_ml_module f x = - Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name - -let _ = - let sc = "string_scope" in - register_string_interpretation sc (interp_string,uninterp_string); - at_declare_ml_module enable_prim_token_interpretation - { pt_local = false; - pt_scope = sc; - pt_interp_info = Uid sc; - pt_required = (string_path,["Coq";"Strings";"String"]); - pt_refs = [static_glob_String; static_glob_EmptyString]; - pt_in_match = true } diff --git a/plugins/syntax/string_syntax_plugin.mlpack b/plugins/syntax/string_syntax_plugin.mlpack deleted file mode 100644 index 45d6e0fa23..0000000000 --- a/plugins/syntax/string_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -String_syntax diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 7446c17d98..1d0485ecd4 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -25,29 +25,30 @@ xorb: bool -> bool -> bool Nat.even: nat -> bool Nat.odd: nat -> bool BoolSpec: Prop -> Prop -> bool -> Prop -Nat.eqb: nat -> nat -> bool +Byte.byte_beq: Byte.byte -> Byte.byte -> bool Nat.testbit: nat -> nat -> bool -Nat.ltb: nat -> nat -> bool +Nat.eqb: nat -> nat -> bool Nat.leb: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat +eq_true_rect: + forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b -eq_true_rec: - forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b -eq_true_ind: - forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b eq_true_rect_r: forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true +eq_true_ind: + forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b +eq_true_rec: + forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b eq_true_rec_r: forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true -eq_true_rect: - forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b -bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b eq_true_ind_r: forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true +bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true andb_true_intro: forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true -andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true BoolSpec_ind: forall (P Q : Prop) (P0 : bool -> Prop), (P -> P0 true) -> diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out index 7038eac22c..04cd7c6c91 100644 --- a/test-suite/output/SearchHead.out +++ b/test-suite/output/SearchHead.out @@ -17,6 +17,7 @@ Nat.leb: nat -> nat -> bool Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool +Byte.byte_beq: Byte.byte -> Byte.byte -> bool mult_n_O: forall n : nat, 0 = n * 0 plus_O_n: forall n : nat, 0 + n = n plus_n_O: forall n : nat, n = n + 0 diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index b0ac9ea29f..5f63b3343d 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -11,6 +11,7 @@ Nat.leb: nat -> nat -> bool Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool +Byte.byte_beq: Byte.byte -> Byte.byte -> bool Nat.two: nat Nat.one: nat Nat.zero: nat diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out new file mode 100644 index 0000000000..2f307bef88 --- /dev/null +++ b/test-suite/output/StringSyntax.out @@ -0,0 +1,1083 @@ +Monomorphic byte_rect = +fun (P : byte -> Type) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") + (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") + (f130 : P "131") (f131 : P "132") (f132 : P "133") (f133 : P "134") (f134 : P "135") (f135 : P "136") (f136 : P "137") (f137 : P "138") (f138 : P "139") (f139 : P "140") (f140 : P "141") (f141 : P "142") (f142 : P "143") (f143 : P "144") (f144 : P "145") (f145 : P "146") (f146 : P "147") (f147 : P "148") (f148 : P "149") (f149 : P "150") (f150 : P "151") (f151 : P "152") (f152 : P "153") (f153 : P "154") (f154 : P "155") (f155 : P "156") (f156 : P "157") (f157 : P "158") (f158 : P "159") (f159 : P "160") (f160 : P "161") (f161 : P "162") (f162 : P "163") (f163 : P "164") (f164 : P "165") (f165 : P "166") (f166 : P "167") (f167 : P "168") (f168 : P "169") (f169 : P "170") (f170 : P "171") (f171 : P "172") (f172 : P "173") (f173 : P "174") (f174 : P "175") (f175 : P "176") (f176 : P "177") (f177 : P "178") (f178 : P "179") (f179 : P "180") (f180 : P "181") (f181 : P "182") (f182 : P "183") (f183 : P "184") (f184 : P "185") (f185 : P "186") (f186 : P "187") + (f187 : P "188") (f188 : P "189") (f189 : P "190") (f190 : P "191") (f191 : P "192") (f192 : P "193") (f193 : P "194") (f194 : P "195") (f195 : P "196") (f196 : P "197") (f197 : P "198") (f198 : P "199") (f199 : P "200") (f200 : P "201") (f201 : P "202") (f202 : P "203") (f203 : P "204") (f204 : P "205") (f205 : P "206") (f206 : P "207") (f207 : P "208") (f208 : P "209") (f209 : P "210") (f210 : P "211") (f211 : P "212") (f212 : P "213") (f213 : P "214") (f214 : P "215") (f215 : P "216") (f216 : P "217") (f217 : P "218") (f218 : P "219") (f219 : P "220") (f220 : P "221") (f221 : P "222") (f222 : P "223") (f223 : P "224") (f224 : P "225") (f225 : P "226") (f226 : P "227") (f227 : P "228") (f228 : P "229") (f229 : P "230") (f230 : P "231") (f231 : P "232") (f232 : P "233") (f233 : P "234") (f234 : P "235") (f235 : P "236") (f236 : P "237") (f237 : P "238") (f238 : P "239") (f239 : P "240") (f240 : P "241") (f241 : P "242") (f242 : P "243") (f243 : P "244") + (f244 : P "245") (f245 : P "246") (f246 : P "247") (f247 : P "248") (f248 : P "249") (f249 : P "250") (f250 : P "251") (f251 : P "252") (f252 : P "253") (f253 : P "254") (f254 : P "255") (b : byte) => +match b as b0 return (P b0) with +| "000" => f +| "001" => f0 +| "002" => f1 +| "003" => f2 +| "004" => f3 +| "005" => f4 +| "006" => f5 +| "007" => f6 +| "008" => f7 +| "009" => f8 +| "010" => f9 +| "011" => f10 +| "012" => f11 +| "013" => f12 +| "014" => f13 +| "015" => f14 +| "016" => f15 +| "017" => f16 +| "018" => f17 +| "019" => f18 +| "020" => f19 +| "021" => f20 +| "022" => f21 +| "023" => f22 +| "024" => f23 +| "025" => f24 +| "026" => f25 +| "027" => f26 +| "028" => f27 +| "029" => f28 +| "030" => f29 +| "031" => f30 +| " " => f31 +| "!" => f32 +| """" => f33 +| "#" => f34 +| "$" => f35 +| "%" => f36 +| "&" => f37 +| "'" => f38 +| "(" => f39 +| ")" => f40 +| "*" => f41 +| "+" => f42 +| "," => f43 +| "-" => f44 +| "." => f45 +| "/" => f46 +| "0" => f47 +| "1" => f48 +| "2" => f49 +| "3" => f50 +| "4" => f51 +| "5" => f52 +| "6" => f53 +| "7" => f54 +| "8" => f55 +| "9" => f56 +| ":" => f57 +| ";" => f58 +| "<" => f59 +| "=" => f60 +| ">" => f61 +| "?" => f62 +| "@" => f63 +| "A" => f64 +| "B" => f65 +| "C" => f66 +| "D" => f67 +| "E" => f68 +| "F" => f69 +| "G" => f70 +| "H" => f71 +| "I" => f72 +| "J" => f73 +| "K" => f74 +| "L" => f75 +| "M" => f76 +| "N" => f77 +| "O" => f78 +| "P" => f79 +| "Q" => f80 +| "R" => f81 +| "S" => f82 +| "T" => f83 +| "U" => f84 +| "V" => f85 +| "W" => f86 +| "X" => f87 +| "Y" => f88 +| "Z" => f89 +| "[" => f90 +| "\" => f91 +| "]" => f92 +| "^" => f93 +| "_" => f94 +| "`" => f95 +| "a" => f96 +| "b" => f97 +| "c" => f98 +| "d" => f99 +| "e" => f100 +| "f" => f101 +| "g" => f102 +| "h" => f103 +| "i" => f104 +| "j" => f105 +| "k" => f106 +| "l" => f107 +| "m" => f108 +| "n" => f109 +| "o" => f110 +| "p" => f111 +| "q" => f112 +| "r" => f113 +| "s" => f114 +| "t" => f115 +| "u" => f116 +| "v" => f117 +| "w" => f118 +| "x" => f119 +| "y" => f120 +| "z" => f121 +| "{" => f122 +| "|" => f123 +| "}" => f124 +| "~" => f125 +| "127" => f126 +| "128" => f127 +| "129" => f128 +| "130" => f129 +| "131" => f130 +| "132" => f131 +| "133" => f132 +| "134" => f133 +| "135" => f134 +| "136" => f135 +| "137" => f136 +| "138" => f137 +| "139" => f138 +| "140" => f139 +| "141" => f140 +| "142" => f141 +| "143" => f142 +| "144" => f143 +| "145" => f144 +| "146" => f145 +| "147" => f146 +| "148" => f147 +| "149" => f148 +| "150" => f149 +| "151" => f150 +| "152" => f151 +| "153" => f152 +| "154" => f153 +| "155" => f154 +| "156" => f155 +| "157" => f156 +| "158" => f157 +| "159" => f158 +| "160" => f159 +| "161" => f160 +| "162" => f161 +| "163" => f162 +| "164" => f163 +| "165" => f164 +| "166" => f165 +| "167" => f166 +| "168" => f167 +| "169" => f168 +| "170" => f169 +| "171" => f170 +| "172" => f171 +| "173" => f172 +| "174" => f173 +| "175" => f174 +| "176" => f175 +| "177" => f176 +| "178" => f177 +| "179" => f178 +| "180" => f179 +| "181" => f180 +| "182" => f181 +| "183" => f182 +| "184" => f183 +| "185" => f184 +| "186" => f185 +| "187" => f186 +| "188" => f187 +| "189" => f188 +| "190" => f189 +| "191" => f190 +| "192" => f191 +| "193" => f192 +| "194" => f193 +| "195" => f194 +| "196" => f195 +| "197" => f196 +| "198" => f197 +| "199" => f198 +| "200" => f199 +| "201" => f200 +| "202" => f201 +| "203" => f202 +| "204" => f203 +| "205" => f204 +| "206" => f205 +| "207" => f206 +| "208" => f207 +| "209" => f208 +| "210" => f209 +| "211" => f210 +| "212" => f211 +| "213" => f212 +| "214" => f213 +| "215" => f214 +| "216" => f215 +| "217" => f216 +| "218" => f217 +| "219" => f218 +| "220" => f219 +| "221" => f220 +| "222" => f221 +| "223" => f222 +| "224" => f223 +| "225" => f224 +| "226" => f225 +| "227" => f226 +| "228" => f227 +| "229" => f228 +| "230" => f229 +| "231" => f230 +| "232" => f231 +| "233" => f232 +| "234" => f233 +| "235" => f234 +| "236" => f235 +| "237" => f236 +| "238" => f237 +| "239" => f238 +| "240" => f239 +| "241" => f240 +| "242" => f241 +| "243" => f242 +| "244" => f243 +| "245" => f244 +| "246" => f245 +| "247" => f246 +| "248" => f247 +| "249" => f248 +| "250" => f249 +| "251" => f250 +| "252" => f251 +| "253" => f252 +| "254" => f253 +| "255" => f254 +end + : forall P : byte -> Type, + P "000" -> + P "001" -> + P "002" -> + P "003" -> + P "004" -> + P "005" -> + P "006" -> + P "007" -> + P "008" -> + P "009" -> + P "010" -> + P "011" -> + P "012" -> + P "013" -> + P "014" -> + P "015" -> + P "016" -> + P "017" -> + P "018" -> + P "019" -> + P "020" -> + P "021" -> + P "022" -> + P "023" -> + P "024" -> + P "025" -> + P "026" -> + P "027" -> + P "028" -> + P "029" -> + P "030" -> + P "031" -> + P " " -> + P "!" -> + P """" -> + P "#" -> + P "$" -> + P "%" -> + P "&" -> + P "'" -> + P "(" -> + P ")" -> + P "*" -> + P "+" -> + P "," -> + P "-" -> + P "." -> + P "/" -> + P "0" -> + P "1" -> + P "2" -> + P "3" -> + P "4" -> + P "5" -> + P "6" -> + P "7" -> + P "8" -> + P "9" -> + P ":" -> + P ";" -> + P "<" -> + P "=" -> + P ">" -> + P "?" -> + P "@" -> + P "A" -> + P "B" -> + P "C" -> + P "D" -> + P "E" -> + P "F" -> + P "G" -> + P "H" -> + P "I" -> + P "J" -> + P "K" -> + P "L" -> + P "M" -> + P "N" -> + P "O" -> + P "P" -> + P "Q" -> + P "R" -> + P "S" -> + P "T" -> + P "U" -> + P "V" -> + P "W" -> + P "X" -> + P "Y" -> + P "Z" -> + P "[" -> + P "\" -> + P "]" -> + P "^" -> + P "_" -> + P "`" -> + P "a" -> + P "b" -> + P "c" -> + P "d" -> + P "e" -> + P "f" -> + P "g" -> + P "h" -> + P "i" -> + P "j" -> + P "k" -> + P "l" -> + P "m" -> + P "n" -> + P "o" -> + P "p" -> + P "q" -> + P "r" -> + P "s" -> + P "t" -> + P "u" -> + P "v" -> + P "w" -> + P "x" -> + P "y" -> + P "z" -> + P "{" -> + P "|" -> + P "}" -> + P "~" -> + P "127" -> + P "128" -> + P "129" -> + P "130" -> + P "131" -> + P "132" -> + P "133" -> + P "134" -> + P "135" -> + P "136" -> + P "137" -> + P "138" -> + P "139" -> + P "140" -> + P "141" -> + P "142" -> + P "143" -> + P "144" -> + P "145" -> + P "146" -> + P "147" -> + P "148" -> + P "149" -> + P "150" -> + P "151" -> + P "152" -> + P "153" -> + P "154" -> + P "155" -> + P "156" -> + P "157" -> + P "158" -> + P "159" -> + P "160" -> + P "161" -> + P "162" -> + P "163" -> + P "164" -> + P "165" -> + P "166" -> + P "167" -> + P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b + +byte_rect is not universe polymorphic +Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +Monomorphic byte_rec = +fun P : byte -> Set => byte_rect P + : forall P : byte -> Set, + P "000" -> + P "001" -> + P "002" -> + P "003" -> + P "004" -> + P "005" -> + P "006" -> + P "007" -> + P "008" -> + P "009" -> + P "010" -> + P "011" -> + P "012" -> + P "013" -> + P "014" -> + P "015" -> + P "016" -> + P "017" -> + P "018" -> + P "019" -> + P "020" -> + P "021" -> + P "022" -> + P "023" -> + P "024" -> + P "025" -> + P "026" -> + P "027" -> + P "028" -> + P "029" -> + P "030" -> + P "031" -> + P " " -> + P "!" -> + P """" -> + P "#" -> + P "$" -> + P "%" -> + P "&" -> + P "'" -> + P "(" -> + P ")" -> + P "*" -> + P "+" -> + P "," -> + P "-" -> + P "." -> + P "/" -> + P "0" -> + P "1" -> + P "2" -> + P "3" -> + P "4" -> + P "5" -> + P "6" -> + P "7" -> + P "8" -> + P "9" -> + P ":" -> + P ";" -> + P "<" -> + P "=" -> + P ">" -> + P "?" -> + P "@" -> + P "A" -> + P "B" -> + P "C" -> + P "D" -> + P "E" -> + P "F" -> + P "G" -> + P "H" -> + P "I" -> + P "J" -> + P "K" -> + P "L" -> + P "M" -> + P "N" -> + P "O" -> + P "P" -> + P "Q" -> + P "R" -> + P "S" -> + P "T" -> + P "U" -> + P "V" -> + P "W" -> + P "X" -> + P "Y" -> + P "Z" -> + P "[" -> + P "\" -> + P "]" -> + P "^" -> + P "_" -> + P "`" -> + P "a" -> + P "b" -> + P "c" -> + P "d" -> + P "e" -> + P "f" -> + P "g" -> + P "h" -> + P "i" -> + P "j" -> + P "k" -> + P "l" -> + P "m" -> + P "n" -> + P "o" -> + P "p" -> + P "q" -> + P "r" -> + P "s" -> + P "t" -> + P "u" -> + P "v" -> + P "w" -> + P "x" -> + P "y" -> + P "z" -> + P "{" -> + P "|" -> + P "}" -> + P "~" -> + P "127" -> + P "128" -> + P "129" -> + P "130" -> + P "131" -> + P "132" -> + P "133" -> + P "134" -> + P "135" -> + P "136" -> + P "137" -> + P "138" -> + P "139" -> + P "140" -> + P "141" -> + P "142" -> + P "143" -> + P "144" -> + P "145" -> + P "146" -> + P "147" -> + P "148" -> + P "149" -> + P "150" -> + P "151" -> + P "152" -> + P "153" -> + P "154" -> + P "155" -> + P "156" -> + P "157" -> + P "158" -> + P "159" -> + P "160" -> + P "161" -> + P "162" -> + P "163" -> + P "164" -> + P "165" -> + P "166" -> + P "167" -> + P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b + +byte_rec is not universe polymorphic +Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +Monomorphic byte_ind = +fun (P : byte -> Prop) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") + (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") + (f130 : P "131") (f131 : P "132") (f132 : P "133") (f133 : P "134") (f134 : P "135") (f135 : P "136") (f136 : P "137") (f137 : P "138") (f138 : P "139") (f139 : P "140") (f140 : P "141") (f141 : P "142") (f142 : P "143") (f143 : P "144") (f144 : P "145") (f145 : P "146") (f146 : P "147") (f147 : P "148") (f148 : P "149") (f149 : P "150") (f150 : P "151") (f151 : P "152") (f152 : P "153") (f153 : P "154") (f154 : P "155") (f155 : P "156") (f156 : P "157") (f157 : P "158") (f158 : P "159") (f159 : P "160") (f160 : P "161") (f161 : P "162") (f162 : P "163") (f163 : P "164") (f164 : P "165") (f165 : P "166") (f166 : P "167") (f167 : P "168") (f168 : P "169") (f169 : P "170") (f170 : P "171") (f171 : P "172") (f172 : P "173") (f173 : P "174") (f174 : P "175") (f175 : P "176") (f176 : P "177") (f177 : P "178") (f178 : P "179") (f179 : P "180") (f180 : P "181") (f181 : P "182") (f182 : P "183") (f183 : P "184") (f184 : P "185") (f185 : P "186") (f186 : P "187") + (f187 : P "188") (f188 : P "189") (f189 : P "190") (f190 : P "191") (f191 : P "192") (f192 : P "193") (f193 : P "194") (f194 : P "195") (f195 : P "196") (f196 : P "197") (f197 : P "198") (f198 : P "199") (f199 : P "200") (f200 : P "201") (f201 : P "202") (f202 : P "203") (f203 : P "204") (f204 : P "205") (f205 : P "206") (f206 : P "207") (f207 : P "208") (f208 : P "209") (f209 : P "210") (f210 : P "211") (f211 : P "212") (f212 : P "213") (f213 : P "214") (f214 : P "215") (f215 : P "216") (f216 : P "217") (f217 : P "218") (f218 : P "219") (f219 : P "220") (f220 : P "221") (f221 : P "222") (f222 : P "223") (f223 : P "224") (f224 : P "225") (f225 : P "226") (f226 : P "227") (f227 : P "228") (f228 : P "229") (f229 : P "230") (f230 : P "231") (f231 : P "232") (f232 : P "233") (f233 : P "234") (f234 : P "235") (f235 : P "236") (f236 : P "237") (f237 : P "238") (f238 : P "239") (f239 : P "240") (f240 : P "241") (f241 : P "242") (f242 : P "243") (f243 : P "244") + (f244 : P "245") (f245 : P "246") (f246 : P "247") (f247 : P "248") (f248 : P "249") (f249 : P "250") (f250 : P "251") (f251 : P "252") (f252 : P "253") (f253 : P "254") (f254 : P "255") (b : byte) => +match b as b0 return (P b0) with +| "000" => f +| "001" => f0 +| "002" => f1 +| "003" => f2 +| "004" => f3 +| "005" => f4 +| "006" => f5 +| "007" => f6 +| "008" => f7 +| "009" => f8 +| "010" => f9 +| "011" => f10 +| "012" => f11 +| "013" => f12 +| "014" => f13 +| "015" => f14 +| "016" => f15 +| "017" => f16 +| "018" => f17 +| "019" => f18 +| "020" => f19 +| "021" => f20 +| "022" => f21 +| "023" => f22 +| "024" => f23 +| "025" => f24 +| "026" => f25 +| "027" => f26 +| "028" => f27 +| "029" => f28 +| "030" => f29 +| "031" => f30 +| " " => f31 +| "!" => f32 +| """" => f33 +| "#" => f34 +| "$" => f35 +| "%" => f36 +| "&" => f37 +| "'" => f38 +| "(" => f39 +| ")" => f40 +| "*" => f41 +| "+" => f42 +| "," => f43 +| "-" => f44 +| "." => f45 +| "/" => f46 +| "0" => f47 +| "1" => f48 +| "2" => f49 +| "3" => f50 +| "4" => f51 +| "5" => f52 +| "6" => f53 +| "7" => f54 +| "8" => f55 +| "9" => f56 +| ":" => f57 +| ";" => f58 +| "<" => f59 +| "=" => f60 +| ">" => f61 +| "?" => f62 +| "@" => f63 +| "A" => f64 +| "B" => f65 +| "C" => f66 +| "D" => f67 +| "E" => f68 +| "F" => f69 +| "G" => f70 +| "H" => f71 +| "I" => f72 +| "J" => f73 +| "K" => f74 +| "L" => f75 +| "M" => f76 +| "N" => f77 +| "O" => f78 +| "P" => f79 +| "Q" => f80 +| "R" => f81 +| "S" => f82 +| "T" => f83 +| "U" => f84 +| "V" => f85 +| "W" => f86 +| "X" => f87 +| "Y" => f88 +| "Z" => f89 +| "[" => f90 +| "\" => f91 +| "]" => f92 +| "^" => f93 +| "_" => f94 +| "`" => f95 +| "a" => f96 +| "b" => f97 +| "c" => f98 +| "d" => f99 +| "e" => f100 +| "f" => f101 +| "g" => f102 +| "h" => f103 +| "i" => f104 +| "j" => f105 +| "k" => f106 +| "l" => f107 +| "m" => f108 +| "n" => f109 +| "o" => f110 +| "p" => f111 +| "q" => f112 +| "r" => f113 +| "s" => f114 +| "t" => f115 +| "u" => f116 +| "v" => f117 +| "w" => f118 +| "x" => f119 +| "y" => f120 +| "z" => f121 +| "{" => f122 +| "|" => f123 +| "}" => f124 +| "~" => f125 +| "127" => f126 +| "128" => f127 +| "129" => f128 +| "130" => f129 +| "131" => f130 +| "132" => f131 +| "133" => f132 +| "134" => f133 +| "135" => f134 +| "136" => f135 +| "137" => f136 +| "138" => f137 +| "139" => f138 +| "140" => f139 +| "141" => f140 +| "142" => f141 +| "143" => f142 +| "144" => f143 +| "145" => f144 +| "146" => f145 +| "147" => f146 +| "148" => f147 +| "149" => f148 +| "150" => f149 +| "151" => f150 +| "152" => f151 +| "153" => f152 +| "154" => f153 +| "155" => f154 +| "156" => f155 +| "157" => f156 +| "158" => f157 +| "159" => f158 +| "160" => f159 +| "161" => f160 +| "162" => f161 +| "163" => f162 +| "164" => f163 +| "165" => f164 +| "166" => f165 +| "167" => f166 +| "168" => f167 +| "169" => f168 +| "170" => f169 +| "171" => f170 +| "172" => f171 +| "173" => f172 +| "174" => f173 +| "175" => f174 +| "176" => f175 +| "177" => f176 +| "178" => f177 +| "179" => f178 +| "180" => f179 +| "181" => f180 +| "182" => f181 +| "183" => f182 +| "184" => f183 +| "185" => f184 +| "186" => f185 +| "187" => f186 +| "188" => f187 +| "189" => f188 +| "190" => f189 +| "191" => f190 +| "192" => f191 +| "193" => f192 +| "194" => f193 +| "195" => f194 +| "196" => f195 +| "197" => f196 +| "198" => f197 +| "199" => f198 +| "200" => f199 +| "201" => f200 +| "202" => f201 +| "203" => f202 +| "204" => f203 +| "205" => f204 +| "206" => f205 +| "207" => f206 +| "208" => f207 +| "209" => f208 +| "210" => f209 +| "211" => f210 +| "212" => f211 +| "213" => f212 +| "214" => f213 +| "215" => f214 +| "216" => f215 +| "217" => f216 +| "218" => f217 +| "219" => f218 +| "220" => f219 +| "221" => f220 +| "222" => f221 +| "223" => f222 +| "224" => f223 +| "225" => f224 +| "226" => f225 +| "227" => f226 +| "228" => f227 +| "229" => f228 +| "230" => f229 +| "231" => f230 +| "232" => f231 +| "233" => f232 +| "234" => f233 +| "235" => f234 +| "236" => f235 +| "237" => f236 +| "238" => f237 +| "239" => f238 +| "240" => f239 +| "241" => f240 +| "242" => f241 +| "243" => f242 +| "244" => f243 +| "245" => f244 +| "246" => f245 +| "247" => f246 +| "248" => f247 +| "249" => f248 +| "250" => f249 +| "251" => f250 +| "252" => f251 +| "253" => f252 +| "254" => f253 +| "255" => f254 +end + : forall P : byte -> Prop, + P "000" -> + P "001" -> + P "002" -> + P "003" -> + P "004" -> + P "005" -> + P "006" -> + P "007" -> + P "008" -> + P "009" -> + P "010" -> + P "011" -> + P "012" -> + P "013" -> + P "014" -> + P "015" -> + P "016" -> + P "017" -> + P "018" -> + P "019" -> + P "020" -> + P "021" -> + P "022" -> + P "023" -> + P "024" -> + P "025" -> + P "026" -> + P "027" -> + P "028" -> + P "029" -> + P "030" -> + P "031" -> + P " " -> + P "!" -> + P """" -> + P "#" -> + P "$" -> + P "%" -> + P "&" -> + P "'" -> + P "(" -> + P ")" -> + P "*" -> + P "+" -> + P "," -> + P "-" -> + P "." -> + P "/" -> + P "0" -> + P "1" -> + P "2" -> + P "3" -> + P "4" -> + P "5" -> + P "6" -> + P "7" -> + P "8" -> + P "9" -> + P ":" -> + P ";" -> + P "<" -> + P "=" -> + P ">" -> + P "?" -> + P "@" -> + P "A" -> + P "B" -> + P "C" -> + P "D" -> + P "E" -> + P "F" -> + P "G" -> + P "H" -> + P "I" -> + P "J" -> + P "K" -> + P "L" -> + P "M" -> + P "N" -> + P "O" -> + P "P" -> + P "Q" -> + P "R" -> + P "S" -> + P "T" -> + P "U" -> + P "V" -> + P "W" -> + P "X" -> + P "Y" -> + P "Z" -> + P "[" -> + P "\" -> + P "]" -> + P "^" -> + P "_" -> + P "`" -> + P "a" -> + P "b" -> + P "c" -> + P "d" -> + P "e" -> + P "f" -> + P "g" -> + P "h" -> + P "i" -> + P "j" -> + P "k" -> + P "l" -> + P "m" -> + P "n" -> + P "o" -> + P "p" -> + P "q" -> + P "r" -> + P "s" -> + P "t" -> + P "u" -> + P "v" -> + P "w" -> + P "x" -> + P "y" -> + P "z" -> + P "{" -> + P "|" -> + P "}" -> + P "~" -> + P "127" -> + P "128" -> + P "129" -> + P "130" -> + P "131" -> + P "132" -> + P "133" -> + P "134" -> + P "135" -> + P "136" -> + P "137" -> + P "138" -> + P "139" -> + P "140" -> + P "141" -> + P "142" -> + P "143" -> + P "144" -> + P "145" -> + P "146" -> + P "147" -> + P "148" -> + P "149" -> + P "150" -> + P "151" -> + P "152" -> + P "153" -> + P "154" -> + P "155" -> + P "156" -> + P "157" -> + P "158" -> + P "159" -> + P "160" -> + P "161" -> + P "162" -> + P "163" -> + P "164" -> + P "165" -> + P "166" -> + P "167" -> + P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b + +byte_ind is not universe polymorphic +Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +"000" + : byte +"a" + : byte +"127" + : byte +The command has indeed failed with message: +Expects a single character or a three-digits ascii code. +"000" + : ascii +"a" + : ascii +"127" + : ascii +The command has indeed failed with message: +Expects a single character or a three-digits ascii code. +"000" + : string +"a" + : string +"127" + : string +"€" + : string +"" + : string + = "a"%char + : ascii + = "a"%byte + : byte + = "a"%string + : string + = ["a"%byte] + : list byte diff --git a/test-suite/output/StringSyntax.v b/test-suite/output/StringSyntax.v new file mode 100644 index 0000000000..477a4dd1c6 --- /dev/null +++ b/test-suite/output/StringSyntax.v @@ -0,0 +1,39 @@ +Require Import Coq.Lists.List. +Require Import Coq.Strings.String Coq.Strings.Byte Coq.Strings.Ascii. +Import ListNotations. + +Set Printing Depth 100000. +Set Printing Width 1000. + +Close Scope char_scope. +Close Scope string_scope. + +Open Scope byte_scope. +Print byte_rect. +Print byte_rec. +Print byte_ind. +Check "000". +Check "a". +Check "127". +Fail Check "€". +Close Scope byte_scope. + +Open Scope char_scope. +Check "000". +Check "a". +Check "127". +Fail Check "€". +Close Scope char_scope. + +Open Scope string_scope. +Check "000". +Check "a". +Check "127". +Check "€". +Check String "001" EmptyString. +Close Scope string_scope. + +Compute ascii_of_byte "a". +Compute byte_of_ascii "a". +Compute string_of_list_byte ("a"::nil)%byte. +Compute list_byte_of_string "a". diff --git a/theories/Init/Byte.v b/theories/Init/Byte.v new file mode 100644 index 0000000000..2d8ee30a43 --- /dev/null +++ b/theories/Init/Byte.v @@ -0,0 +1,302 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +(** * Bytes *) + +Require Import Coq.Init.Datatypes. +Require Import Coq.Init.Logic. +Require Import Coq.Init.Specif. +Require Coq.Init.Nat. + +Declare ML Module "string_notation_plugin". + +(** We define an inductive for use with the [String Notation] command + which contains all ascii characters. We use 256 constructors for + efficiency and ease of conversion. *) + +Local Set Boolean Equality Schemes. +Declare Scope byte_scope. +Delimit Scope byte_scope with byte. + +Inductive byte := +| x00 +| x01 +| x02 +| x03 +| x04 +| x05 +| x06 +| x07 +| x08 +| x09 +| x0a +| x0b +| x0c +| x0d +| x0e +| x0f +| x10 +| x11 +| x12 +| x13 +| x14 +| x15 +| x16 +| x17 +| x18 +| x19 +| x1a +| x1b +| x1c +| x1d +| x1e +| x1f +| x20 +| x21 +| x22 +| x23 +| x24 +| x25 +| x26 +| x27 +| x28 +| x29 +| x2a +| x2b +| x2c +| x2d +| x2e +| x2f +| x30 +| x31 +| x32 +| x33 +| x34 +| x35 +| x36 +| x37 +| x38 +| x39 +| x3a +| x3b +| x3c +| x3d +| x3e +| x3f +| x40 +| x41 +| x42 +| x43 +| x44 +| x45 +| x46 +| x47 +| x48 +| x49 +| x4a +| x4b +| x4c +| x4d +| x4e +| x4f +| x50 +| x51 +| x52 +| x53 +| x54 +| x55 +| x56 +| x57 +| x58 +| x59 +| x5a +| x5b +| x5c +| x5d +| x5e +| x5f +| x60 +| x61 +| x62 +| x63 +| x64 +| x65 +| x66 +| x67 +| x68 +| x69 +| x6a +| x6b +| x6c +| x6d +| x6e +| x6f +| x70 +| x71 +| x72 +| x73 +| x74 +| x75 +| x76 +| x77 +| x78 +| x79 +| x7a +| x7b +| x7c +| x7d +| x7e +| x7f +| x80 +| x81 +| x82 +| x83 +| x84 +| x85 +| x86 +| x87 +| x88 +| x89 +| x8a +| x8b +| x8c +| x8d +| x8e +| x8f +| x90 +| x91 +| x92 +| x93 +| x94 +| x95 +| x96 +| x97 +| x98 +| x99 +| x9a +| x9b +| x9c +| x9d +| x9e +| x9f +| xa0 +| xa1 +| xa2 +| xa3 +| xa4 +| xa5 +| xa6 +| xa7 +| xa8 +| xa9 +| xaa +| xab +| xac +| xad +| xae +| xaf +| xb0 +| xb1 +| xb2 +| xb3 +| xb4 +| xb5 +| xb6 +| xb7 +| xb8 +| xb9 +| xba +| xbb +| xbc +| xbd +| xbe +| xbf +| xc0 +| xc1 +| xc2 +| xc3 +| xc4 +| xc5 +| xc6 +| xc7 +| xc8 +| xc9 +| xca +| xcb +| xcc +| xcd +| xce +| xcf +| xd0 +| xd1 +| xd2 +| xd3 +| xd4 +| xd5 +| xd6 +| xd7 +| xd8 +| xd9 +| xda +| xdb +| xdc +| xdd +| xde +| xdf +| xe0 +| xe1 +| xe2 +| xe3 +| xe4 +| xe5 +| xe6 +| xe7 +| xe8 +| xe9 +| xea +| xeb +| xec +| xed +| xee +| xef +| xf0 +| xf1 +| xf2 +| xf3 +| xf4 +| xf5 +| xf6 +| xf7 +| xf8 +| xf9 +| xfa +| xfb +| xfc +| xfd +| xfe +| xff +. + +Bind Scope byte_scope with byte. + +Register byte as core.byte.type. + +Notation eqb := byte_beq. + +Definition byte_of_byte (b : byte) : byte := b. + +Module Export ByteSyntaxNotations. + String Notation byte byte_of_byte byte_of_byte : byte_scope. +End ByteSyntaxNotations. + +Module Export ByteNotations. + Export ByteSyntaxNotations. + Infix "=?" := eqb (at level 70) : byte_scope. +End ByteNotations. diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 6d98bcb34a..5e29f854e8 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -13,6 +13,7 @@ Require Export Logic. Require Export Logic_Type. Require Export Datatypes. Require Export Specif. +Require Coq.Init.Byte. Require Coq.Init.Decimal. Require Coq.Init.Nat. Require Export Peano. @@ -26,6 +27,7 @@ Require Export Coq.Init.Tauto. Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". Declare ML Module "numeral_notation_plugin". +Declare ML Module "string_notation_plugin". (* Parsing / printing of decimal numbers *) Arguments Nat.of_uint d%dec_uint_scope. @@ -38,5 +40,8 @@ Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int (* Parsing / printing of [nat] numbers *) Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5000). +(* Printing/Parsing of bytes *) +Export Byte.ByteSyntaxNotations. + (* Default substrings not considered by queries like SearchAbout *) Add Search Blacklist "_subproof" "_subterm" "Private_". diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index b7c1eaa788..13757c6007 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -12,7 +12,7 @@ (** Contributed by Laurent Théry (INRIA); Adapted to Coq V8 by the Coq Development Team *) -Require Import Bool BinPos BinNat PeanoNat Nnat. +Require Import Bool BinPos BinNat PeanoNat Nnat Coq.Strings.Byte. (** * Definition of ascii characters *) @@ -20,10 +20,7 @@ Require Import Bool BinPos BinNat PeanoNat Nnat. Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool). -Register Ascii as plugins.syntax.Ascii. - Declare Scope char_scope. -Module Export AsciiSyntax. Declare ML Module "ascii_syntax_plugin". End AsciiSyntax. Delimit Scope char_scope with char. Bind Scope char_scope with ascii. @@ -140,6 +137,12 @@ do 8 (destruct p; [ | | intros; vm_compute; reflexivity ]); intro H; vm_compute in H; destruct p; discriminate. Qed. +Theorem N_ascii_bounded : + forall a : ascii, (N_of_ascii a < 256)%N. +Proof. + destruct a as [[|][|][|][|][|][|][|][|]]; vm_compute; reflexivity. +Qed. + Theorem ascii_nat_embedding : forall a : ascii, ascii_of_nat (nat_of_ascii a) = a. Proof. @@ -158,6 +161,15 @@ Proof. now apply Nat.compare_lt_iff. Qed. +Theorem nat_ascii_bounded : + forall a : ascii, nat_of_ascii a < 256. +Proof. + intro a; unfold nat_of_ascii. + change 256 with (N.to_nat 256). + rewrite <- Nat.compare_lt_iff, <- N2Nat.inj_compare, N.compare_lt_iff. + apply N_ascii_bounded. +Qed. + (** * Concrete syntax *) @@ -175,7 +187,44 @@ Qed. stand-alone utf8 characters so that only the notation "nnn" is available for them (unless your terminal is able to represent them, which is typically not the case in coqide). -*) + *) + +Definition ascii_of_byte (b : byte) : ascii + := ascii_of_N (Byte.to_N b). + +Definition byte_of_ascii (a : ascii) : byte + := match Byte.of_N (N_of_ascii a) with + | Some v => v + | None => x00 (* can't happen *) + end. + +Lemma ascii_of_byte_of_ascii x : ascii_of_byte (byte_of_ascii x) = x. +Proof. + cbv [ascii_of_byte byte_of_ascii]. + pose proof (to_of_N (N_of_ascii x)). + destruct (of_N (N_of_ascii x)) as [x'|] eqn:H1. + { specialize (H x' eq_refl); rewrite H. + apply ascii_N_embedding. } + { exfalso. + rewrite of_N_None_iff in H1. + pose proof (N_ascii_bounded x) as H2. + rewrite N.lt_nge in H1, H2. + destruct (N.le_gt_cases (N_of_ascii x) 255) as [H3|H3]. + { apply H1, H3. } + { rewrite <- N.le_succ_l in H3; apply H2, H3. } } +Qed. + +Lemma byte_of_ascii_of_byte x : byte_of_ascii (ascii_of_byte x) = x. +Proof. + cbv [ascii_of_byte byte_of_ascii]. + rewrite N_ascii_embedding, of_to_N; [ reflexivity | ]. + pose proof (to_N_bounded x) as H. + rewrite <- N.lt_succ_r in H; exact H. +Qed. + +Module Export AsciiSyntax. + String Notation ascii ascii_of_byte byte_of_ascii : char_scope. +End AsciiSyntax. Local Open Scope char_scope. diff --git a/theories/Strings/Byte.v b/theories/Strings/Byte.v new file mode 100644 index 0000000000..581094a8b5 --- /dev/null +++ b/theories/Strings/Byte.v @@ -0,0 +1,1425 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +Require Import Coq.Arith.EqNat. +Require Import Coq.NArith.BinNat. +Require Export Coq.Init.Byte. + +Local Set Implicit Arguments. + +Lemma byte_dec_lb x y : x = y -> Byte.eqb x y = true. +Proof. intro; subst y; destruct x; reflexivity. Defined. + +Definition byte_dec_bl x y (H : Byte.eqb x y = true) : x = y + := match H in (_ = tr) return if tr then x = y else True with + | eq_refl + => match x, y return if Byte.eqb x y then x = y else True with + | x00, x00 => eq_refl + | x01, x01 => eq_refl + | x02, x02 => eq_refl + | x03, x03 => eq_refl + | x04, x04 => eq_refl + | x05, x05 => eq_refl + | x06, x06 => eq_refl + | x07, x07 => eq_refl + | x08, x08 => eq_refl + | x09, x09 => eq_refl + | x0a, x0a => eq_refl + | x0b, x0b => eq_refl + | x0c, x0c => eq_refl + | x0d, x0d => eq_refl + | x0e, x0e => eq_refl + | x0f, x0f => eq_refl + | x10, x10 => eq_refl + | x11, x11 => eq_refl + | x12, x12 => eq_refl + | x13, x13 => eq_refl + | x14, x14 => eq_refl + | x15, x15 => eq_refl + | x16, x16 => eq_refl + | x17, x17 => eq_refl + | x18, x18 => eq_refl + | x19, x19 => eq_refl + | x1a, x1a => eq_refl + | x1b, x1b => eq_refl + | x1c, x1c => eq_refl + | x1d, x1d => eq_refl + | x1e, x1e => eq_refl + | x1f, x1f => eq_refl + | x20, x20 => eq_refl + | x21, x21 => eq_refl + | x22, x22 => eq_refl + | x23, x23 => eq_refl + | x24, x24 => eq_refl + | x25, x25 => eq_refl + | x26, x26 => eq_refl + | x27, x27 => eq_refl + | x28, x28 => eq_refl + | x29, x29 => eq_refl + | x2a, x2a => eq_refl + | x2b, x2b => eq_refl + | x2c, x2c => eq_refl + | x2d, x2d => eq_refl + | x2e, x2e => eq_refl + | x2f, x2f => eq_refl + | x30, x30 => eq_refl + | x31, x31 => eq_refl + | x32, x32 => eq_refl + | x33, x33 => eq_refl + | x34, x34 => eq_refl + | x35, x35 => eq_refl + | x36, x36 => eq_refl + | x37, x37 => eq_refl + | x38, x38 => eq_refl + | x39, x39 => eq_refl + | x3a, x3a => eq_refl + | x3b, x3b => eq_refl + | x3c, x3c => eq_refl + | x3d, x3d => eq_refl + | x3e, x3e => eq_refl + | x3f, x3f => eq_refl + | x40, x40 => eq_refl + | x41, x41 => eq_refl + | x42, x42 => eq_refl + | x43, x43 => eq_refl + | x44, x44 => eq_refl + | x45, x45 => eq_refl + | x46, x46 => eq_refl + | x47, x47 => eq_refl + | x48, x48 => eq_refl + | x49, x49 => eq_refl + | x4a, x4a => eq_refl + | x4b, x4b => eq_refl + | x4c, x4c => eq_refl + | x4d, x4d => eq_refl + | x4e, x4e => eq_refl + | x4f, x4f => eq_refl + | x50, x50 => eq_refl + | x51, x51 => eq_refl + | x52, x52 => eq_refl + | x53, x53 => eq_refl + | x54, x54 => eq_refl + | x55, x55 => eq_refl + | x56, x56 => eq_refl + | x57, x57 => eq_refl + | x58, x58 => eq_refl + | x59, x59 => eq_refl + | x5a, x5a => eq_refl + | x5b, x5b => eq_refl + | x5c, x5c => eq_refl + | x5d, x5d => eq_refl + | x5e, x5e => eq_refl + | x5f, x5f => eq_refl + | x60, x60 => eq_refl + | x61, x61 => eq_refl + | x62, x62 => eq_refl + | x63, x63 => eq_refl + | x64, x64 => eq_refl + | x65, x65 => eq_refl + | x66, x66 => eq_refl + | x67, x67 => eq_refl + | x68, x68 => eq_refl + | x69, x69 => eq_refl + | x6a, x6a => eq_refl + | x6b, x6b => eq_refl + | x6c, x6c => eq_refl + | x6d, x6d => eq_refl + | x6e, x6e => eq_refl + | x6f, x6f => eq_refl + | x70, x70 => eq_refl + | x71, x71 => eq_refl + | x72, x72 => eq_refl + | x73, x73 => eq_refl + | x74, x74 => eq_refl + | x75, x75 => eq_refl + | x76, x76 => eq_refl + | x77, x77 => eq_refl + | x78, x78 => eq_refl + | x79, x79 => eq_refl + | x7a, x7a => eq_refl + | x7b, x7b => eq_refl + | x7c, x7c => eq_refl + | x7d, x7d => eq_refl + | x7e, x7e => eq_refl + | x7f, x7f => eq_refl + | x80, x80 => eq_refl + | x81, x81 => eq_refl + | x82, x82 => eq_refl + | x83, x83 => eq_refl + | x84, x84 => eq_refl + | x85, x85 => eq_refl + | x86, x86 => eq_refl + | x87, x87 => eq_refl + | x88, x88 => eq_refl + | x89, x89 => eq_refl + | x8a, x8a => eq_refl + | x8b, x8b => eq_refl + | x8c, x8c => eq_refl + | x8d, x8d => eq_refl + | x8e, x8e => eq_refl + | x8f, x8f => eq_refl + | x90, x90 => eq_refl + | x91, x91 => eq_refl + | x92, x92 => eq_refl + | x93, x93 => eq_refl + | x94, x94 => eq_refl + | x95, x95 => eq_refl + | x96, x96 => eq_refl + | x97, x97 => eq_refl + | x98, x98 => eq_refl + | x99, x99 => eq_refl + | x9a, x9a => eq_refl + | x9b, x9b => eq_refl + | x9c, x9c => eq_refl + | x9d, x9d => eq_refl + | x9e, x9e => eq_refl + | x9f, x9f => eq_refl + | xa0, xa0 => eq_refl + | xa1, xa1 => eq_refl + | xa2, xa2 => eq_refl + | xa3, xa3 => eq_refl + | xa4, xa4 => eq_refl + | xa5, xa5 => eq_refl + | xa6, xa6 => eq_refl + | xa7, xa7 => eq_refl + | xa8, xa8 => eq_refl + | xa9, xa9 => eq_refl + | xaa, xaa => eq_refl + | xab, xab => eq_refl + | xac, xac => eq_refl + | xad, xad => eq_refl + | xae, xae => eq_refl + | xaf, xaf => eq_refl + | xb0, xb0 => eq_refl + | xb1, xb1 => eq_refl + | xb2, xb2 => eq_refl + | xb3, xb3 => eq_refl + | xb4, xb4 => eq_refl + | xb5, xb5 => eq_refl + | xb6, xb6 => eq_refl + | xb7, xb7 => eq_refl + | xb8, xb8 => eq_refl + | xb9, xb9 => eq_refl + | xba, xba => eq_refl + | xbb, xbb => eq_refl + | xbc, xbc => eq_refl + | xbd, xbd => eq_refl + | xbe, xbe => eq_refl + | xbf, xbf => eq_refl + | xc0, xc0 => eq_refl + | xc1, xc1 => eq_refl + | xc2, xc2 => eq_refl + | xc3, xc3 => eq_refl + | xc4, xc4 => eq_refl + | xc5, xc5 => eq_refl + | xc6, xc6 => eq_refl + | xc7, xc7 => eq_refl + | xc8, xc8 => eq_refl + | xc9, xc9 => eq_refl + | xca, xca => eq_refl + | xcb, xcb => eq_refl + | xcc, xcc => eq_refl + | xcd, xcd => eq_refl + | xce, xce => eq_refl + | xcf, xcf => eq_refl + | xd0, xd0 => eq_refl + | xd1, xd1 => eq_refl + | xd2, xd2 => eq_refl + | xd3, xd3 => eq_refl + | xd4, xd4 => eq_refl + | xd5, xd5 => eq_refl + | xd6, xd6 => eq_refl + | xd7, xd7 => eq_refl + | xd8, xd8 => eq_refl + | xd9, xd9 => eq_refl + | xda, xda => eq_refl + | xdb, xdb => eq_refl + | xdc, xdc => eq_refl + | xdd, xdd => eq_refl + | xde, xde => eq_refl + | xdf, xdf => eq_refl + | xe0, xe0 => eq_refl + | xe1, xe1 => eq_refl + | xe2, xe2 => eq_refl + | xe3, xe3 => eq_refl + | xe4, xe4 => eq_refl + | xe5, xe5 => eq_refl + | xe6, xe6 => eq_refl + | xe7, xe7 => eq_refl + | xe8, xe8 => eq_refl + | xe9, xe9 => eq_refl + | xea, xea => eq_refl + | xeb, xeb => eq_refl + | xec, xec => eq_refl + | xed, xed => eq_refl + | xee, xee => eq_refl + | xef, xef => eq_refl + | xf0, xf0 => eq_refl + | xf1, xf1 => eq_refl + | xf2, xf2 => eq_refl + | xf3, xf3 => eq_refl + | xf4, xf4 => eq_refl + | xf5, xf5 => eq_refl + | xf6, xf6 => eq_refl + | xf7, xf7 => eq_refl + | xf8, xf8 => eq_refl + | xf9, xf9 => eq_refl + | xfa, xfa => eq_refl + | xfb, xfb => eq_refl + | xfc, xfc => eq_refl + | xfd, xfd => eq_refl + | xfe, xfe => eq_refl + | xff, xff => eq_refl + | _, _ => I + end + end. + +Lemma eqb_false x y : Byte.eqb x y = false -> x <> y. +Proof. intros H H'; pose proof (byte_dec_lb H'); congruence. Qed. + +Definition byte_eq_dec (x y : byte) : {x = y} + {x <> y} + := (if Byte.eqb x y as beq return Byte.eqb x y = beq -> _ + then fun pf => left (byte_dec_bl x y pf) + else fun pf => right (eqb_false pf)) + eq_refl. + +Section nat. + Definition to_nat (x : byte) : nat + := match x with + | x00 => 0 + | x01 => 1 + | x02 => 2 + | x03 => 3 + | x04 => 4 + | x05 => 5 + | x06 => 6 + | x07 => 7 + | x08 => 8 + | x09 => 9 + | x0a => 10 + | x0b => 11 + | x0c => 12 + | x0d => 13 + | x0e => 14 + | x0f => 15 + | x10 => 16 + | x11 => 17 + | x12 => 18 + | x13 => 19 + | x14 => 20 + | x15 => 21 + | x16 => 22 + | x17 => 23 + | x18 => 24 + | x19 => 25 + | x1a => 26 + | x1b => 27 + | x1c => 28 + | x1d => 29 + | x1e => 30 + | x1f => 31 + | x20 => 32 + | x21 => 33 + | x22 => 34 + | x23 => 35 + | x24 => 36 + | x25 => 37 + | x26 => 38 + | x27 => 39 + | x28 => 40 + | x29 => 41 + | x2a => 42 + | x2b => 43 + | x2c => 44 + | x2d => 45 + | x2e => 46 + | x2f => 47 + | x30 => 48 + | x31 => 49 + | x32 => 50 + | x33 => 51 + | x34 => 52 + | x35 => 53 + | x36 => 54 + | x37 => 55 + | x38 => 56 + | x39 => 57 + | x3a => 58 + | x3b => 59 + | x3c => 60 + | x3d => 61 + | x3e => 62 + | x3f => 63 + | x40 => 64 + | x41 => 65 + | x42 => 66 + | x43 => 67 + | x44 => 68 + | x45 => 69 + | x46 => 70 + | x47 => 71 + | x48 => 72 + | x49 => 73 + | x4a => 74 + | x4b => 75 + | x4c => 76 + | x4d => 77 + | x4e => 78 + | x4f => 79 + | x50 => 80 + | x51 => 81 + | x52 => 82 + | x53 => 83 + | x54 => 84 + | x55 => 85 + | x56 => 86 + | x57 => 87 + | x58 => 88 + | x59 => 89 + | x5a => 90 + | x5b => 91 + | x5c => 92 + | x5d => 93 + | x5e => 94 + | x5f => 95 + | x60 => 96 + | x61 => 97 + | x62 => 98 + | x63 => 99 + | x64 => 100 + | x65 => 101 + | x66 => 102 + | x67 => 103 + | x68 => 104 + | x69 => 105 + | x6a => 106 + | x6b => 107 + | x6c => 108 + | x6d => 109 + | x6e => 110 + | x6f => 111 + | x70 => 112 + | x71 => 113 + | x72 => 114 + | x73 => 115 + | x74 => 116 + | x75 => 117 + | x76 => 118 + | x77 => 119 + | x78 => 120 + | x79 => 121 + | x7a => 122 + | x7b => 123 + | x7c => 124 + | x7d => 125 + | x7e => 126 + | x7f => 127 + | x80 => 128 + | x81 => 129 + | x82 => 130 + | x83 => 131 + | x84 => 132 + | x85 => 133 + | x86 => 134 + | x87 => 135 + | x88 => 136 + | x89 => 137 + | x8a => 138 + | x8b => 139 + | x8c => 140 + | x8d => 141 + | x8e => 142 + | x8f => 143 + | x90 => 144 + | x91 => 145 + | x92 => 146 + | x93 => 147 + | x94 => 148 + | x95 => 149 + | x96 => 150 + | x97 => 151 + | x98 => 152 + | x99 => 153 + | x9a => 154 + | x9b => 155 + | x9c => 156 + | x9d => 157 + | x9e => 158 + | x9f => 159 + | xa0 => 160 + | xa1 => 161 + | xa2 => 162 + | xa3 => 163 + | xa4 => 164 + | xa5 => 165 + | xa6 => 166 + | xa7 => 167 + | xa8 => 168 + | xa9 => 169 + | xaa => 170 + | xab => 171 + | xac => 172 + | xad => 173 + | xae => 174 + | xaf => 175 + | xb0 => 176 + | xb1 => 177 + | xb2 => 178 + | xb3 => 179 + | xb4 => 180 + | xb5 => 181 + | xb6 => 182 + | xb7 => 183 + | xb8 => 184 + | xb9 => 185 + | xba => 186 + | xbb => 187 + | xbc => 188 + | xbd => 189 + | xbe => 190 + | xbf => 191 + | xc0 => 192 + | xc1 => 193 + | xc2 => 194 + | xc3 => 195 + | xc4 => 196 + | xc5 => 197 + | xc6 => 198 + | xc7 => 199 + | xc8 => 200 + | xc9 => 201 + | xca => 202 + | xcb => 203 + | xcc => 204 + | xcd => 205 + | xce => 206 + | xcf => 207 + | xd0 => 208 + | xd1 => 209 + | xd2 => 210 + | xd3 => 211 + | xd4 => 212 + | xd5 => 213 + | xd6 => 214 + | xd7 => 215 + | xd8 => 216 + | xd9 => 217 + | xda => 218 + | xdb => 219 + | xdc => 220 + | xdd => 221 + | xde => 222 + | xdf => 223 + | xe0 => 224 + | xe1 => 225 + | xe2 => 226 + | xe3 => 227 + | xe4 => 228 + | xe5 => 229 + | xe6 => 230 + | xe7 => 231 + | xe8 => 232 + | xe9 => 233 + | xea => 234 + | xeb => 235 + | xec => 236 + | xed => 237 + | xee => 238 + | xef => 239 + | xf0 => 240 + | xf1 => 241 + | xf2 => 242 + | xf3 => 243 + | xf4 => 244 + | xf5 => 245 + | xf6 => 246 + | xf7 => 247 + | xf8 => 248 + | xf9 => 249 + | xfa => 250 + | xfb => 251 + | xfc => 252 + | xfd => 253 + | xfe => 254 + | xff => 255 + end. + + Definition of_nat (x : nat) : option byte + := match x with + | 0 => Some x00 + | 1 => Some x01 + | 2 => Some x02 + | 3 => Some x03 + | 4 => Some x04 + | 5 => Some x05 + | 6 => Some x06 + | 7 => Some x07 + | 8 => Some x08 + | 9 => Some x09 + | 10 => Some x0a + | 11 => Some x0b + | 12 => Some x0c + | 13 => Some x0d + | 14 => Some x0e + | 15 => Some x0f + | 16 => Some x10 + | 17 => Some x11 + | 18 => Some x12 + | 19 => Some x13 + | 20 => Some x14 + | 21 => Some x15 + | 22 => Some x16 + | 23 => Some x17 + | 24 => Some x18 + | 25 => Some x19 + | 26 => Some x1a + | 27 => Some x1b + | 28 => Some x1c + | 29 => Some x1d + | 30 => Some x1e + | 31 => Some x1f + | 32 => Some x20 + | 33 => Some x21 + | 34 => Some x22 + | 35 => Some x23 + | 36 => Some x24 + | 37 => Some x25 + | 38 => Some x26 + | 39 => Some x27 + | 40 => Some x28 + | 41 => Some x29 + | 42 => Some x2a + | 43 => Some x2b + | 44 => Some x2c + | 45 => Some x2d + | 46 => Some x2e + | 47 => Some x2f + | 48 => Some x30 + | 49 => Some x31 + | 50 => Some x32 + | 51 => Some x33 + | 52 => Some x34 + | 53 => Some x35 + | 54 => Some x36 + | 55 => Some x37 + | 56 => Some x38 + | 57 => Some x39 + | 58 => Some x3a + | 59 => Some x3b + | 60 => Some x3c + | 61 => Some x3d + | 62 => Some x3e + | 63 => Some x3f + | 64 => Some x40 + | 65 => Some x41 + | 66 => Some x42 + | 67 => Some x43 + | 68 => Some x44 + | 69 => Some x45 + | 70 => Some x46 + | 71 => Some x47 + | 72 => Some x48 + | 73 => Some x49 + | 74 => Some x4a + | 75 => Some x4b + | 76 => Some x4c + | 77 => Some x4d + | 78 => Some x4e + | 79 => Some x4f + | 80 => Some x50 + | 81 => Some x51 + | 82 => Some x52 + | 83 => Some x53 + | 84 => Some x54 + | 85 => Some x55 + | 86 => Some x56 + | 87 => Some x57 + | 88 => Some x58 + | 89 => Some x59 + | 90 => Some x5a + | 91 => Some x5b + | 92 => Some x5c + | 93 => Some x5d + | 94 => Some x5e + | 95 => Some x5f + | 96 => Some x60 + | 97 => Some x61 + | 98 => Some x62 + | 99 => Some x63 + | 100 => Some x64 + | 101 => Some x65 + | 102 => Some x66 + | 103 => Some x67 + | 104 => Some x68 + | 105 => Some x69 + | 106 => Some x6a + | 107 => Some x6b + | 108 => Some x6c + | 109 => Some x6d + | 110 => Some x6e + | 111 => Some x6f + | 112 => Some x70 + | 113 => Some x71 + | 114 => Some x72 + | 115 => Some x73 + | 116 => Some x74 + | 117 => Some x75 + | 118 => Some x76 + | 119 => Some x77 + | 120 => Some x78 + | 121 => Some x79 + | 122 => Some x7a + | 123 => Some x7b + | 124 => Some x7c + | 125 => Some x7d + | 126 => Some x7e + | 127 => Some x7f + | 128 => Some x80 + | 129 => Some x81 + | 130 => Some x82 + | 131 => Some x83 + | 132 => Some x84 + | 133 => Some x85 + | 134 => Some x86 + | 135 => Some x87 + | 136 => Some x88 + | 137 => Some x89 + | 138 => Some x8a + | 139 => Some x8b + | 140 => Some x8c + | 141 => Some x8d + | 142 => Some x8e + | 143 => Some x8f + | 144 => Some x90 + | 145 => Some x91 + | 146 => Some x92 + | 147 => Some x93 + | 148 => Some x94 + | 149 => Some x95 + | 150 => Some x96 + | 151 => Some x97 + | 152 => Some x98 + | 153 => Some x99 + | 154 => Some x9a + | 155 => Some x9b + | 156 => Some x9c + | 157 => Some x9d + | 158 => Some x9e + | 159 => Some x9f + | 160 => Some xa0 + | 161 => Some xa1 + | 162 => Some xa2 + | 163 => Some xa3 + | 164 => Some xa4 + | 165 => Some xa5 + | 166 => Some xa6 + | 167 => Some xa7 + | 168 => Some xa8 + | 169 => Some xa9 + | 170 => Some xaa + | 171 => Some xab + | 172 => Some xac + | 173 => Some xad + | 174 => Some xae + | 175 => Some xaf + | 176 => Some xb0 + | 177 => Some xb1 + | 178 => Some xb2 + | 179 => Some xb3 + | 180 => Some xb4 + | 181 => Some xb5 + | 182 => Some xb6 + | 183 => Some xb7 + | 184 => Some xb8 + | 185 => Some xb9 + | 186 => Some xba + | 187 => Some xbb + | 188 => Some xbc + | 189 => Some xbd + | 190 => Some xbe + | 191 => Some xbf + | 192 => Some xc0 + | 193 => Some xc1 + | 194 => Some xc2 + | 195 => Some xc3 + | 196 => Some xc4 + | 197 => Some xc5 + | 198 => Some xc6 + | 199 => Some xc7 + | 200 => Some xc8 + | 201 => Some xc9 + | 202 => Some xca + | 203 => Some xcb + | 204 => Some xcc + | 205 => Some xcd + | 206 => Some xce + | 207 => Some xcf + | 208 => Some xd0 + | 209 => Some xd1 + | 210 => Some xd2 + | 211 => Some xd3 + | 212 => Some xd4 + | 213 => Some xd5 + | 214 => Some xd6 + | 215 => Some xd7 + | 216 => Some xd8 + | 217 => Some xd9 + | 218 => Some xda + | 219 => Some xdb + | 220 => Some xdc + | 221 => Some xdd + | 222 => Some xde + | 223 => Some xdf + | 224 => Some xe0 + | 225 => Some xe1 + | 226 => Some xe2 + | 227 => Some xe3 + | 228 => Some xe4 + | 229 => Some xe5 + | 230 => Some xe6 + | 231 => Some xe7 + | 232 => Some xe8 + | 233 => Some xe9 + | 234 => Some xea + | 235 => Some xeb + | 236 => Some xec + | 237 => Some xed + | 238 => Some xee + | 239 => Some xef + | 240 => Some xf0 + | 241 => Some xf1 + | 242 => Some xf2 + | 243 => Some xf3 + | 244 => Some xf4 + | 245 => Some xf5 + | 246 => Some xf6 + | 247 => Some xf7 + | 248 => Some xf8 + | 249 => Some xf9 + | 250 => Some xfa + | 251 => Some xfb + | 252 => Some xfc + | 253 => Some xfd + | 254 => Some xfe + | 255 => Some xff + | _ => None + end. + + Lemma of_to_nat x : of_nat (to_nat x) = Some x. + Proof. destruct x; reflexivity. Qed. + + Lemma to_of_nat x y : of_nat x = Some y -> to_nat y = x. + Proof. + do 256 try destruct x as [|x]; cbv [of_nat]; intro. + all: repeat match goal with + | _ => reflexivity + | _ => progress subst + | [ H : Some ?a = Some ?b |- _ ] => assert (a = b) by refine match H with eq_refl => eq_refl end; clear H + | [ H : None = Some _ |- _ ] => solve [ inversion H ] + end. + Qed. + + Lemma to_of_nat_iff x y : of_nat x = Some y <-> to_nat y = x. + Proof. split; intro; subst; (apply of_to_nat || apply to_of_nat); assumption. Qed. + + Lemma to_of_nat_option_map x : option_map to_nat (of_nat x) = if Nat.leb x 255 then Some x else None. + Proof. do 256 try destruct x as [|x]; reflexivity. Qed. + + Lemma to_nat_bounded x : to_nat x <= 255. + Proof. + generalize (to_of_nat_option_map (to_nat x)). + rewrite of_to_nat; cbn [option_map]. + destruct (Nat.leb (to_nat x) 255) eqn:H; [ | congruence ]. + rewrite (PeanoNat.Nat.leb_le (to_nat x) 255) in H. + intro; assumption. + Qed. + + Lemma of_nat_None_iff x : of_nat x = None <-> 255 < x. + Proof. + generalize (to_of_nat_option_map x). + destruct (of_nat x), (Nat.leb x 255) eqn:H; cbn [option_map]; try congruence. + { rewrite PeanoNat.Nat.leb_le in H; split; [ congruence | ]. + rewrite PeanoNat.Nat.lt_nge; intro H'; exfalso; apply H'; assumption. } + { rewrite PeanoNat.Nat.leb_nle in H; split; [ | reflexivity ]. + rewrite PeanoNat.Nat.lt_nge; intro; assumption. } + Qed. +End nat. + +Section N. + Local Open Scope N_scope. + + Definition to_N (x : byte) : N + := match x with + | x00 => 0 + | x01 => 1 + | x02 => 2 + | x03 => 3 + | x04 => 4 + | x05 => 5 + | x06 => 6 + | x07 => 7 + | x08 => 8 + | x09 => 9 + | x0a => 10 + | x0b => 11 + | x0c => 12 + | x0d => 13 + | x0e => 14 + | x0f => 15 + | x10 => 16 + | x11 => 17 + | x12 => 18 + | x13 => 19 + | x14 => 20 + | x15 => 21 + | x16 => 22 + | x17 => 23 + | x18 => 24 + | x19 => 25 + | x1a => 26 + | x1b => 27 + | x1c => 28 + | x1d => 29 + | x1e => 30 + | x1f => 31 + | x20 => 32 + | x21 => 33 + | x22 => 34 + | x23 => 35 + | x24 => 36 + | x25 => 37 + | x26 => 38 + | x27 => 39 + | x28 => 40 + | x29 => 41 + | x2a => 42 + | x2b => 43 + | x2c => 44 + | x2d => 45 + | x2e => 46 + | x2f => 47 + | x30 => 48 + | x31 => 49 + | x32 => 50 + | x33 => 51 + | x34 => 52 + | x35 => 53 + | x36 => 54 + | x37 => 55 + | x38 => 56 + | x39 => 57 + | x3a => 58 + | x3b => 59 + | x3c => 60 + | x3d => 61 + | x3e => 62 + | x3f => 63 + | x40 => 64 + | x41 => 65 + | x42 => 66 + | x43 => 67 + | x44 => 68 + | x45 => 69 + | x46 => 70 + | x47 => 71 + | x48 => 72 + | x49 => 73 + | x4a => 74 + | x4b => 75 + | x4c => 76 + | x4d => 77 + | x4e => 78 + | x4f => 79 + | x50 => 80 + | x51 => 81 + | x52 => 82 + | x53 => 83 + | x54 => 84 + | x55 => 85 + | x56 => 86 + | x57 => 87 + | x58 => 88 + | x59 => 89 + | x5a => 90 + | x5b => 91 + | x5c => 92 + | x5d => 93 + | x5e => 94 + | x5f => 95 + | x60 => 96 + | x61 => 97 + | x62 => 98 + | x63 => 99 + | x64 => 100 + | x65 => 101 + | x66 => 102 + | x67 => 103 + | x68 => 104 + | x69 => 105 + | x6a => 106 + | x6b => 107 + | x6c => 108 + | x6d => 109 + | x6e => 110 + | x6f => 111 + | x70 => 112 + | x71 => 113 + | x72 => 114 + | x73 => 115 + | x74 => 116 + | x75 => 117 + | x76 => 118 + | x77 => 119 + | x78 => 120 + | x79 => 121 + | x7a => 122 + | x7b => 123 + | x7c => 124 + | x7d => 125 + | x7e => 126 + | x7f => 127 + | x80 => 128 + | x81 => 129 + | x82 => 130 + | x83 => 131 + | x84 => 132 + | x85 => 133 + | x86 => 134 + | x87 => 135 + | x88 => 136 + | x89 => 137 + | x8a => 138 + | x8b => 139 + | x8c => 140 + | x8d => 141 + | x8e => 142 + | x8f => 143 + | x90 => 144 + | x91 => 145 + | x92 => 146 + | x93 => 147 + | x94 => 148 + | x95 => 149 + | x96 => 150 + | x97 => 151 + | x98 => 152 + | x99 => 153 + | x9a => 154 + | x9b => 155 + | x9c => 156 + | x9d => 157 + | x9e => 158 + | x9f => 159 + | xa0 => 160 + | xa1 => 161 + | xa2 => 162 + | xa3 => 163 + | xa4 => 164 + | xa5 => 165 + | xa6 => 166 + | xa7 => 167 + | xa8 => 168 + | xa9 => 169 + | xaa => 170 + | xab => 171 + | xac => 172 + | xad => 173 + | xae => 174 + | xaf => 175 + | xb0 => 176 + | xb1 => 177 + | xb2 => 178 + | xb3 => 179 + | xb4 => 180 + | xb5 => 181 + | xb6 => 182 + | xb7 => 183 + | xb8 => 184 + | xb9 => 185 + | xba => 186 + | xbb => 187 + | xbc => 188 + | xbd => 189 + | xbe => 190 + | xbf => 191 + | xc0 => 192 + | xc1 => 193 + | xc2 => 194 + | xc3 => 195 + | xc4 => 196 + | xc5 => 197 + | xc6 => 198 + | xc7 => 199 + | xc8 => 200 + | xc9 => 201 + | xca => 202 + | xcb => 203 + | xcc => 204 + | xcd => 205 + | xce => 206 + | xcf => 207 + | xd0 => 208 + | xd1 => 209 + | xd2 => 210 + | xd3 => 211 + | xd4 => 212 + | xd5 => 213 + | xd6 => 214 + | xd7 => 215 + | xd8 => 216 + | xd9 => 217 + | xda => 218 + | xdb => 219 + | xdc => 220 + | xdd => 221 + | xde => 222 + | xdf => 223 + | xe0 => 224 + | xe1 => 225 + | xe2 => 226 + | xe3 => 227 + | xe4 => 228 + | xe5 => 229 + | xe6 => 230 + | xe7 => 231 + | xe8 => 232 + | xe9 => 233 + | xea => 234 + | xeb => 235 + | xec => 236 + | xed => 237 + | xee => 238 + | xef => 239 + | xf0 => 240 + | xf1 => 241 + | xf2 => 242 + | xf3 => 243 + | xf4 => 244 + | xf5 => 245 + | xf6 => 246 + | xf7 => 247 + | xf8 => 248 + | xf9 => 249 + | xfa => 250 + | xfb => 251 + | xfc => 252 + | xfd => 253 + | xfe => 254 + | xff => 255 + end. + + Definition of_N (x : N) : option byte + := match x with + | 0 => Some x00 + | 1 => Some x01 + | 2 => Some x02 + | 3 => Some x03 + | 4 => Some x04 + | 5 => Some x05 + | 6 => Some x06 + | 7 => Some x07 + | 8 => Some x08 + | 9 => Some x09 + | 10 => Some x0a + | 11 => Some x0b + | 12 => Some x0c + | 13 => Some x0d + | 14 => Some x0e + | 15 => Some x0f + | 16 => Some x10 + | 17 => Some x11 + | 18 => Some x12 + | 19 => Some x13 + | 20 => Some x14 + | 21 => Some x15 + | 22 => Some x16 + | 23 => Some x17 + | 24 => Some x18 + | 25 => Some x19 + | 26 => Some x1a + | 27 => Some x1b + | 28 => Some x1c + | 29 => Some x1d + | 30 => Some x1e + | 31 => Some x1f + | 32 => Some x20 + | 33 => Some x21 + | 34 => Some x22 + | 35 => Some x23 + | 36 => Some x24 + | 37 => Some x25 + | 38 => Some x26 + | 39 => Some x27 + | 40 => Some x28 + | 41 => Some x29 + | 42 => Some x2a + | 43 => Some x2b + | 44 => Some x2c + | 45 => Some x2d + | 46 => Some x2e + | 47 => Some x2f + | 48 => Some x30 + | 49 => Some x31 + | 50 => Some x32 + | 51 => Some x33 + | 52 => Some x34 + | 53 => Some x35 + | 54 => Some x36 + | 55 => Some x37 + | 56 => Some x38 + | 57 => Some x39 + | 58 => Some x3a + | 59 => Some x3b + | 60 => Some x3c + | 61 => Some x3d + | 62 => Some x3e + | 63 => Some x3f + | 64 => Some x40 + | 65 => Some x41 + | 66 => Some x42 + | 67 => Some x43 + | 68 => Some x44 + | 69 => Some x45 + | 70 => Some x46 + | 71 => Some x47 + | 72 => Some x48 + | 73 => Some x49 + | 74 => Some x4a + | 75 => Some x4b + | 76 => Some x4c + | 77 => Some x4d + | 78 => Some x4e + | 79 => Some x4f + | 80 => Some x50 + | 81 => Some x51 + | 82 => Some x52 + | 83 => Some x53 + | 84 => Some x54 + | 85 => Some x55 + | 86 => Some x56 + | 87 => Some x57 + | 88 => Some x58 + | 89 => Some x59 + | 90 => Some x5a + | 91 => Some x5b + | 92 => Some x5c + | 93 => Some x5d + | 94 => Some x5e + | 95 => Some x5f + | 96 => Some x60 + | 97 => Some x61 + | 98 => Some x62 + | 99 => Some x63 + | 100 => Some x64 + | 101 => Some x65 + | 102 => Some x66 + | 103 => Some x67 + | 104 => Some x68 + | 105 => Some x69 + | 106 => Some x6a + | 107 => Some x6b + | 108 => Some x6c + | 109 => Some x6d + | 110 => Some x6e + | 111 => Some x6f + | 112 => Some x70 + | 113 => Some x71 + | 114 => Some x72 + | 115 => Some x73 + | 116 => Some x74 + | 117 => Some x75 + | 118 => Some x76 + | 119 => Some x77 + | 120 => Some x78 + | 121 => Some x79 + | 122 => Some x7a + | 123 => Some x7b + | 124 => Some x7c + | 125 => Some x7d + | 126 => Some x7e + | 127 => Some x7f + | 128 => Some x80 + | 129 => Some x81 + | 130 => Some x82 + | 131 => Some x83 + | 132 => Some x84 + | 133 => Some x85 + | 134 => Some x86 + | 135 => Some x87 + | 136 => Some x88 + | 137 => Some x89 + | 138 => Some x8a + | 139 => Some x8b + | 140 => Some x8c + | 141 => Some x8d + | 142 => Some x8e + | 143 => Some x8f + | 144 => Some x90 + | 145 => Some x91 + | 146 => Some x92 + | 147 => Some x93 + | 148 => Some x94 + | 149 => Some x95 + | 150 => Some x96 + | 151 => Some x97 + | 152 => Some x98 + | 153 => Some x99 + | 154 => Some x9a + | 155 => Some x9b + | 156 => Some x9c + | 157 => Some x9d + | 158 => Some x9e + | 159 => Some x9f + | 160 => Some xa0 + | 161 => Some xa1 + | 162 => Some xa2 + | 163 => Some xa3 + | 164 => Some xa4 + | 165 => Some xa5 + | 166 => Some xa6 + | 167 => Some xa7 + | 168 => Some xa8 + | 169 => Some xa9 + | 170 => Some xaa + | 171 => Some xab + | 172 => Some xac + | 173 => Some xad + | 174 => Some xae + | 175 => Some xaf + | 176 => Some xb0 + | 177 => Some xb1 + | 178 => Some xb2 + | 179 => Some xb3 + | 180 => Some xb4 + | 181 => Some xb5 + | 182 => Some xb6 + | 183 => Some xb7 + | 184 => Some xb8 + | 185 => Some xb9 + | 186 => Some xba + | 187 => Some xbb + | 188 => Some xbc + | 189 => Some xbd + | 190 => Some xbe + | 191 => Some xbf + | 192 => Some xc0 + | 193 => Some xc1 + | 194 => Some xc2 + | 195 => Some xc3 + | 196 => Some xc4 + | 197 => Some xc5 + | 198 => Some xc6 + | 199 => Some xc7 + | 200 => Some xc8 + | 201 => Some xc9 + | 202 => Some xca + | 203 => Some xcb + | 204 => Some xcc + | 205 => Some xcd + | 206 => Some xce + | 207 => Some xcf + | 208 => Some xd0 + | 209 => Some xd1 + | 210 => Some xd2 + | 211 => Some xd3 + | 212 => Some xd4 + | 213 => Some xd5 + | 214 => Some xd6 + | 215 => Some xd7 + | 216 => Some xd8 + | 217 => Some xd9 + | 218 => Some xda + | 219 => Some xdb + | 220 => Some xdc + | 221 => Some xdd + | 222 => Some xde + | 223 => Some xdf + | 224 => Some xe0 + | 225 => Some xe1 + | 226 => Some xe2 + | 227 => Some xe3 + | 228 => Some xe4 + | 229 => Some xe5 + | 230 => Some xe6 + | 231 => Some xe7 + | 232 => Some xe8 + | 233 => Some xe9 + | 234 => Some xea + | 235 => Some xeb + | 236 => Some xec + | 237 => Some xed + | 238 => Some xee + | 239 => Some xef + | 240 => Some xf0 + | 241 => Some xf1 + | 242 => Some xf2 + | 243 => Some xf3 + | 244 => Some xf4 + | 245 => Some xf5 + | 246 => Some xf6 + | 247 => Some xf7 + | 248 => Some xf8 + | 249 => Some xf9 + | 250 => Some xfa + | 251 => Some xfb + | 252 => Some xfc + | 253 => Some xfd + | 254 => Some xfe + | 255 => Some xff + | _ => None + end. + + Lemma of_to_N x : of_N (to_N x) = Some x. + Proof. destruct x; reflexivity. Qed. + + Lemma to_of_N x y : of_N x = Some y -> to_N y = x. + Proof. + cbv [of_N]; + repeat match goal with + | [ |- context[match ?x with _ => _ end] ] => is_var x; destruct x + | _ => intro + | _ => reflexivity + | _ => progress subst + | [ H : Some ?a = Some ?b |- _ ] => assert (a = b) by refine match H with eq_refl => eq_refl end; clear H + | [ H : None = Some _ |- _ ] => solve [ inversion H ] + end. + Qed. + + Lemma to_of_N_iff x y : of_N x = Some y <-> to_N y = x. + Proof. split; intro; subst; (apply of_to_N || apply to_of_N); assumption. Qed. + + Lemma to_of_N_option_map x : option_map to_N (of_N x) = if N.leb x 255 then Some x else None. + Proof. + cbv [of_N]; + repeat match goal with + | [ |- context[match ?x with _ => _ end] ] => is_var x; destruct x + end; + reflexivity. + Qed. + + Lemma to_N_bounded x : to_N x <= 255. + Proof. + generalize (to_of_N_option_map (to_N x)). + rewrite of_to_N; cbn [option_map]. + destruct (N.leb (to_N x) 255) eqn:H; [ | congruence ]. + rewrite (N.leb_le (to_N x) 255) in H. + intro; assumption. + Qed. + + Lemma of_N_None_iff x : of_N x = None <-> 255 < x. + Proof. + generalize (to_of_N_option_map x). + destruct (of_N x), (N.leb x 255) eqn:H; cbn [option_map]; try congruence. + { rewrite N.leb_le in H; split; [ congruence | ]. + rewrite N.lt_nge; intro H'; exfalso; apply H'; assumption. } + { rewrite N.leb_nle in H; split; [ | reflexivity ]. + rewrite N.lt_nge; intro; assumption. } + Qed. +End N. diff --git a/theories/Strings/String.v b/theories/Strings/String.v index a09d518892..08ccfac877 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -15,6 +15,7 @@ Require Import Arith. Require Import Ascii. Require Import Bool. +Require Import Coq.Strings.Byte. (** *** Definition of strings *) @@ -25,7 +26,6 @@ Inductive string : Set := | String : ascii -> string -> string. Declare Scope string_scope. -Module Export StringSyntax. Declare ML Module "string_syntax_plugin". End StringSyntax. Delimit Scope string_scope with string. Bind Scope string_scope with string. Local Open Scope string_scope. @@ -114,12 +114,12 @@ Theorem get_correct : Proof. intros s1; elim s1; simpl. intros s2; case s2; simpl; split; auto. -intros H; generalize (H 0); intros H1; inversion H1. +intros H; generalize (H O); intros H1; inversion H1. intros; discriminate. intros a s1' Rec s2; case s2; simpl; split; auto. -intros H; generalize (H 0); intros H1; inversion H1. +intros H; generalize (H O); intros H1; inversion H1. intros; discriminate. -intros H; generalize (H 0); simpl; intros H1; inversion H1. +intros H; generalize (H O); simpl; intros H1; inversion H1. case (Rec s). intros H0; rewrite H0; auto. intros n; exact (H (S n)). @@ -150,7 +150,7 @@ Proof. intros s1; elim s1; simpl; auto. intros s2 n; rewrite plus_comm; simpl; auto. intros a s1' Rec s2 n; case n; simpl; auto. -generalize (Rec s2 0); simpl; auto. intros. +generalize (Rec s2 O); simpl; auto. intros. rewrite <- Plus.plus_Snm_nSm; auto. Qed. @@ -162,9 +162,9 @@ Qed. Fixpoint substring (n m : nat) (s : string) : string := match n, m, s with - | 0, 0, _ => EmptyString - | 0, S m', EmptyString => s - | 0, S m', String c s' => String c (substring 0 m' s') + | O, O, _ => EmptyString + | O, S m', EmptyString => s + | O, S m', String c s' => String c (substring 0 m' s') | S n', _, EmptyString => s | S n', _, String c s' => substring n' m s' end. @@ -257,16 +257,16 @@ Qed. Fixpoint index (n : nat) (s1 s2 : string) : option nat := match s2, n with - | EmptyString, 0 => + | EmptyString, O => match s1 with - | EmptyString => Some 0 + | EmptyString => Some O | String a s1' => None end | EmptyString, S n' => None - | String b s2', 0 => - if prefix s1 s2 then Some 0 + | String b s2', O => + if prefix s1 s2 then Some O else - match index 0 s1 s2' with + match index O s1 s2' with | Some n => Some (S n) | None => None end @@ -300,8 +300,8 @@ generalize (prefix_correct s1 (String b s2')); intros H0 H; injection H as <-; auto. case H0; simpl; auto. case m; simpl; auto. -case (index 0 s1 s2'); intros; discriminate. -intros m'; generalize (Rec 0 m' s1); case (index 0 s1 s2'); auto. +case (index O s1 s2'); intros; discriminate. +intros m'; generalize (Rec O m' s1); case (index O s1 s2'); auto. intros x H H0 H1; apply H; injection H1; auto. intros; discriminate. intros n'; case m; simpl; auto. @@ -335,7 +335,7 @@ intros H0 H; injection H as <-; auto. intros p H2 H3; inversion H3. case m; simpl; auto. case (index 0 s1 s2'); intros; discriminate. -intros m'; generalize (Rec 0 m' s1); case (index 0 s1 s2'); auto. +intros m'; generalize (Rec O m' s1); case (index 0 s1 s2'); auto. intros x H H0 H1 p; try case p; simpl; auto. intros H2 H3; red; intros H4; case H0. intros H5 H6; absurd (false = true); auto with bool. @@ -383,7 +383,7 @@ intros H4 H5; absurd (false = true); auto with bool. case s1; simpl; auto. intros a s n0 H H0 H1 H2; change (substring n0 (length (String a s)) s2' <> String a s); - apply (Rec 0); auto. + apply (Rec O); auto. generalize H0; case (index 0 (String a s) s2'); simpl; auto; intros; discriminate. apply Le.le_O_n. @@ -423,9 +423,53 @@ Qed. Definition findex n s1 s2 := match index n s1 s2 with | Some n => n - | None => 0 + | None => O end. +(** *** Conversion to/from [list ascii] and [list byte] *) + +Fixpoint string_of_list_ascii (s : list ascii) : string + := match s with + | nil => EmptyString + | cons ch s => String ch (string_of_list_ascii s) + end. + +Fixpoint list_ascii_of_string (s : string) : list ascii + := match s with + | EmptyString => nil + | String ch s => cons ch (list_ascii_of_string s) + end. + +Lemma string_of_list_ascii_of_string s : string_of_list_ascii (list_ascii_of_string s) = s. +Proof. + induction s as [|? ? IHs]; [ reflexivity | cbn; apply f_equal, IHs ]. +Defined. + +Lemma list_ascii_of_string_of_list_ascii s : list_ascii_of_string (string_of_list_ascii s) = s. +Proof. + induction s as [|? ? IHs]; [ reflexivity | cbn; apply f_equal, IHs ]. +Defined. + +Definition string_of_list_byte (s : list byte) : string + := string_of_list_ascii (List.map ascii_of_byte s). + +Definition list_byte_of_string (s : string) : list byte + := List.map byte_of_ascii (list_ascii_of_string s). + +Lemma string_of_list_byte_of_string s : string_of_list_byte (list_byte_of_string s) = s. +Proof. + cbv [string_of_list_byte list_byte_of_string]. + erewrite List.map_map, List.map_ext, List.map_id, string_of_list_ascii_of_string; [ reflexivity | intro ]. + apply ascii_of_byte_of_ascii. +Qed. + +Lemma list_byte_of_string_of_list_byte s : list_byte_of_string (string_of_list_byte s) = s. +Proof. + cbv [string_of_list_byte list_byte_of_string]. + erewrite list_ascii_of_string_of_list_ascii, List.map_map, List.map_ext, List.map_id; [ reflexivity | intro ]. + apply byte_of_ascii_of_byte. +Qed. + (** *** Concrete syntax *) (** @@ -438,7 +482,11 @@ Definition findex n s1 s2 := part of a valid utf8 sequence of characters are not representable using the Coq string notation (use explicitly the String constructor with the ascii codes of the characters). -*) + *) + +Module Export StringSyntax. + String Notation string string_of_list_byte list_byte_of_string : string_scope. +End StringSyntax. Example HelloWorld := " ""Hello world!"" ". diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index befb4d7ccf..b238c96913 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -65,7 +65,9 @@ let process_vernac_interp_error exn = match fst exn with | PretypeError(ctx,sigma,te) -> wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te) | Notation.NumeralNotationError(ctx,sigma,te) -> - wrap_vernac_error exn (Himsg.explain_numeral_notation_error ctx sigma te) + wrap_vernac_error exn (Himsg.explain_numeral_or_string_notation_error "numeral" ctx sigma te) + | Notation.StringNotationError(ctx,sigma,te) -> + wrap_vernac_error exn (Himsg.explain_numeral_or_string_notation_error "string" ctx sigma te) | Typeclasses_errors.TypeClassError(env, te) -> wrap_vernac_error exn (Himsg.explain_typeclass_error env te) | Implicit_quantifiers.MismatchedContextInstance(e,c,l,x) -> diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 6c7117b513..bf3bd70f09 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1326,12 +1326,12 @@ let explain_reduction_tactic_error = function spc () ++ str "is not well typed." ++ fnl () ++ explain_type_error env' (Evd.from_env env') e -let explain_numeral_notation_error env sigma = function +let explain_numeral_or_string_notation_error numeral_or_string env sigma = function | Notation.UnexpectedTerm c -> (strbrk "Unexpected term " ++ pr_constr_env env sigma c ++ - strbrk " while parsing a numeral notation.") + strbrk (" while parsing a "^numeral_or_string^" notation.")) | Notation.UnexpectedNonOptionTerm c -> (strbrk "Unexpected non-option term " ++ pr_constr_env env sigma c ++ - strbrk " while parsing a numeral notation.") + strbrk (" while parsing a "^numeral_or_string^" notation.")) diff --git a/vernac/himsg.mli b/vernac/himsg.mli index db05aaa125..ecb69bef1e 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -47,4 +47,4 @@ val explain_module_internalization_error : val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error -val explain_numeral_notation_error : env -> Evd.evar_map -> Notation.numeral_notation_error -> Pp.t +val explain_numeral_or_string_notation_error : string -> env -> Evd.evar_map -> Notation.numeral_or_string_notation_error -> Pp.t |