diff options
| author | Vincent Laporte | 2018-09-07 12:22:17 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2018-09-14 07:51:17 +0000 |
| commit | 42bed627c4a1c5a1ecf59d4865fc872b5eee7290 (patch) | |
| tree | e70eab9f85e1f0c7d3818ac4d7c4712ffcc85483 /kernel/retroknowledge.ml | |
| parent | ab2560233f2e6fc8c26853af6991533d8d335e16 (diff) | |
Retroknowledge: simpler parsing rules
Diffstat (limited to 'kernel/retroknowledge.ml')
| -rw-r--r-- | kernel/retroknowledge.ml | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 0d1bb1e586..2ed846d852 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -55,6 +55,33 @@ type int31_field = type field = | KInt31 of int31_field +let int31_field_of_string = + function + | "bits" -> Int31Bits + | "type" -> Int31Type + | "twice" -> Int31Twice + | "twice_plus_one" -> Int31TwicePlusOne + | "phi" -> Int31Phi + | "phi_inv" -> Int31PhiInv + | "plus" -> Int31Plus + | "plusc" -> Int31PlusC + | "pluscarryc" -> Int31PlusCarryC + | "minus" -> Int31Minus + | "minusc" -> Int31MinusC + | "minuscarryc" -> Int31MinusCarryC + | "times" -> Int31Times + | "timesc" -> Int31TimesC + | "div21" -> Int31Div21 + | "div" -> Int31Div + | "diveucl" -> Int31Diveucl + | "addmuldiv" -> Int31AddMulDiv + | "compare" -> Int31Compare + | "head0" -> Int31Head0 + | "tail0" -> Int31Tail0 + | "lor" -> Int31Lor + | "land" -> Int31Land + | "lxor" -> Int31Lxor + | s -> CErrors.user_err Pp.(str "Registering unknown int31 operator " ++ str s) (* record representing all the flags of the internal state of the kernel *) type flags = {fastcomputation : bool} |