diff options
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index a6a14efc87..8cb423051a 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -387,6 +387,37 @@ let prim_token_interpreters = let prim_token_uninterpreters = (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.uninterpreter) Hashtbl.t) +(*******************************************************) +(* Numeral notation interpretation *) +type numnot_option = + | Nop + | Warning of raw_natural_number + | Abstract of raw_natural_number + +type int_ty = + { uint : Names.inductive; + int : Names.inductive } + +type z_pos_ty = + { z_ty : Names.inductive; + pos_ty : Names.inductive } + +type target_kind = + | Int of int_ty (* Coq.Init.Decimal.int + uint *) + | UInt of Names.inductive (* Coq.Init.Decimal.uint *) + | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) + +type option_kind = Option | Direct +type conversion_kind = target_kind * option_kind + +type numeral_notation_obj = + { to_kind : conversion_kind; + to_ty : GlobRef.t; + of_kind : conversion_kind; + of_ty : GlobRef.t; + num_ty : Libnames.qualid; (* for warnings / error messages *) + warning : numnot_option } + (* Table from scope_name to backtrack-able informations about interpreters (in particular interpreter unique id). *) let prim_token_interp_infos = |