From 4be2dd481c783bed7c09086b647d860e42b7ea9f Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 7 Sep 2018 11:18:28 +0200
Subject: Retroknowledge.KInt31: remove the (unused) group parameter

---
 kernel/retroknowledge.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/retroknowledge.ml')

diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 34f62defb8..0d1bb1e586 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -53,7 +53,7 @@ type int31_field =
   | Int31Lxor
 
 type field =
-  | KInt31 of string*int31_field
+  | KInt31 of int31_field
 
 
 (* record representing all the flags of the internal state of the kernel *)
-- 
cgit v1.2.3


From 42bed627c4a1c5a1ecf59d4865fc872b5eee7290 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 7 Sep 2018 12:22:17 +0200
Subject: Retroknowledge: simpler parsing rules

---
 kernel/retroknowledge.ml | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

(limited to 'kernel/retroknowledge.ml')

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}
-- 
cgit v1.2.3


From 2ec78477c720ba3a5343b49f25cfa9c1639adbba Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 7 Sep 2018 17:34:11 +0200
Subject: Retroknowledge: use GlobRef.t instead of Constr.t as entry

---
 kernel/retroknowledge.ml | 17 ++++-------------
 1 file changed, 4 insertions(+), 13 deletions(-)

(limited to 'kernel/retroknowledge.ml')

diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 2ed846d852..c1a8820bf0 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -19,12 +19,9 @@ open Names
 open Constr
 
 (* The retroknowledge defines a bijective correspondance between some
-   [entry]-s (which are, in fact, merely terms) and [field]-s which
+   [entry]-s (which are, in fact, merely names) and [field]-s which
    are roles assigned to these entries. *)
 
-(* aliased type for clarity purpose*)
-type entry = Constr.t
-
 type int31_field =
   | Int31Bits
   | Int31Type
@@ -95,19 +92,13 @@ type flags = {fastcomputation : bool}
 module Proactive =
   Map.Make (struct type t = field let compare = Pervasives.compare end)
 
-type proactive = entry Proactive.t
+type proactive = GlobRef.t Proactive.t
 
 (* The [reactive] knowledge contains the mapping
    [entry->field]. Fields are later to be interpreted as a
    [reactive_info]. *)
 
-module EntryOrd =
-struct
-  type t = entry
-  let compare = Constr.compare
-end
-
-module Reactive = Map.Make (EntryOrd)
+module Reactive = GlobRef.Map
 
 type reactive_info = {(*information required by the compiler of the VM *)
   vm_compiling :
@@ -154,7 +145,7 @@ and retroknowledge = {flags : flags; proactive : proactive; reactive : reactive}
 (* As per now, there is only the possibility of registering things
    the possibility of unregistering or changing the flag is under study *)
 type action =
-    | RKRegister of field*entry
+    | RKRegister of field * GlobRef.t
 
 
 (*initialisation*)
-- 
cgit v1.2.3


From 736842d4cde09c667837dee8a633ff98ecf6a820 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 10 Sep 2018 13:20:39 +0200
Subject: Register: simpler syntax

---
 kernel/retroknowledge.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/retroknowledge.ml')

diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index c1a8820bf0..e51c25c06b 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -80,6 +80,8 @@ let int31_field_of_string =
   | "lxor" -> Int31Lxor
   | s -> CErrors.user_err Pp.(str "Registering unknown int31 operator " ++ str s)
 
+let int31_path = DirPath.make [ Id.of_string "int31" ]
+
 (* record representing all the flags of the internal state of the kernel *)
 type flags = {fastcomputation : bool}
 
-- 
cgit v1.2.3