diff options
| author | Maxime Dénès | 2020-05-09 12:53:20 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-05-09 12:53:20 +0200 |
| commit | 3a7ff44f1ffaff3a8bb8c5a9c95a9b102e31c476 (patch) | |
| tree | 9476ed11d9d31912c85760e185e1410513fc4824 /kernel/cPrimitives.mli | |
| parent | 1bf9ba682e74391cf853e9b87ae40fac5b3b17b3 (diff) | |
| parent | 1322e8356087d4ad19bbec13968f456222667ab2 (diff) | |
Merge PR #12122: Avoid registering as keywords the #... in Primitive
Ack-by: SkySkimmer
Reviewed-by: maximedenes
Diffstat (limited to 'kernel/cPrimitives.mli')
| -rw-r--r-- | kernel/cPrimitives.mli | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 2a0399f1f7..a5db51111f 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -52,6 +52,10 @@ type t = | Float64next_up | Float64next_down +(** Can raise [Not_found]. + Beware that this is not exactly the reverse of [to_string] below. *) +val parse : string -> t + val equal : t -> t -> bool type arg_kind = @@ -75,6 +79,10 @@ type prim_type = | PT_int63 | PT_float64 +(** Can raise [Not_found] *) +val prim_type_of_string : string -> prim_type +val prim_type_to_string : prim_type -> string + type 'a prim_ind = | PIT_bool : unit prim_ind | PIT_carry : prim_type prim_ind @@ -90,8 +98,13 @@ type op_or_type = | OT_type of prim_type val prim_ind_to_string : 'a prim_ind -> string + +(** Can raise [Not_found] *) +val op_or_type_of_string : string -> op_or_type val op_or_type_to_string : op_or_type -> string +val parse_op_or_type : ?loc:Loc.t -> string -> op_or_type + type ind_or_type = | PITT_ind : 'a prim_ind * 'a -> ind_or_type | PITT_type : prim_type -> ind_or_type |