diff options
| author | Gaëtan Gilbert | 2018-11-17 21:07:44 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 15:46:16 +0100 |
| commit | ab8c27c589ea90ac86518cc7c1b513b740190cdc (patch) | |
| tree | aea236e67ca897ab208ae95e352b29c9d3b28a58 /kernel | |
| parent | 456919dd31f2f4bda15c6b37e4f1217bc085fc41 (diff) | |
Put [@inline] on CClosure.Mark functions
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cClosure.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 922fce957e..412637c4b6 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -307,32 +307,32 @@ module Mark : sig end = struct type t = int - let of_state = function + let[@inline] of_state = function | Norm -> 0b00 | Cstr -> 0b01 | Whnf -> 0b10 | Red -> 0b11 - let of_relevance = function + let[@inline] of_relevance = function | Unknown -> 0 | KnownR -> 0b01 | KnownI -> 0b10 - let mark state relevance = (of_state state) * 4 + (of_relevance relevance) + let[@inline] mark state relevance = (of_state state) * 4 + (of_relevance relevance) - let relevance x = match x land 0b11 with + let[@inline] relevance x = match x land 0b11 with | 0b00 -> Unknown | 0b01 -> KnownR | 0b10 -> KnownI | _ -> assert false - let red_state x = match x land 0b1100 with + let[@inline] red_state x = match x land 0b1100 with | 0b0000 -> Norm | 0b0100 -> Cstr | 0b1000 -> Whnf | 0b1100 -> Red | _ -> assert false - let neutr x = x lor 0b1000 (* Whnf|Norm -> Whnf | Red|Cstr -> Red *) + let[@inline] neutr x = x lor 0b1000 (* Whnf|Norm -> Whnf | Red|Cstr -> Red *) - let set_norm x = x land 0b0011 + let[@inline] set_norm x = x land 0b0011 end let mark = Mark.mark |
