diff options
| author | Pierre Roux | 2019-04-02 22:39:32 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:19:59 +0100 |
| commit | f93684a412f067622a5026c406bc76032c30b6e9 (patch) | |
| tree | 94965ae5e5d454b0ebb0d4266dd8a27f5487ddf3 /kernel/cPrimitives.mli | |
| parent | 6694a1811dc4e961a81fb4464cf5aaf05f1b5752 (diff) | |
Declare type of primitives in CPrimitives
Rather than in typeops
Diffstat (limited to 'kernel/cPrimitives.mli')
| -rw-r--r-- | kernel/cPrimitives.mli | 22 |
1 files changed, 15 insertions, 7 deletions
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 6913371caf..3c825a8018 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -53,18 +53,26 @@ val kind : t -> args_red (** Special Entries for Register **) -type prim_ind = - | PIT_bool - | PIT_carry - | PIT_pair - | PIT_cmp - type prim_type = | PT_int63 +type 'a prim_ind = + | PIT_bool : unit prim_ind + | PIT_carry : prim_type prim_ind + | PIT_pair : (prim_type * prim_type) prim_ind + | PIT_cmp : unit prim_ind + +type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex + type op_or_type = | OT_op of t | OT_type of prim_type -val prim_ind_to_string : prim_ind -> string +val prim_ind_to_string : 'a prim_ind -> string val op_or_type_to_string : op_or_type -> string + +type ind_or_type = + | PITT_ind : 'a prim_ind * 'a -> ind_or_type + | PITT_type : prim_type -> ind_or_type + +val types : t -> ind_or_type list |