Retroknowledge: simpler parsing rules

5 files changed, 31 insertions, 74 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}
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 6b2c74e9df..1436f23739 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -48,6 +48,8 @@ type int31_field =
 type field =
   | KInt31 of int31_field
 
+val int31_field_of_string : string -> int31_field
+
 (** This type represent an atomic action of the retroknowledge. It
    is stored in the compiled libraries 
    As per now, there is only the possibility of registering things
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index a9133512e0..f4555509cc 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -311,71 +311,3 @@ let pr_lpar_id_colon _ _ _ _ = mt ()
 ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon
 | [ local_test_lpar_id_colon(x) ] -> [ () ]
 END
-
-(* spiwack: the print functions are incomplete, but I don't know what they are
-	used for *)
-let pr_r_int31_field i31f =
-  str "int31 " ++
-  match i31f with
-    | Retroknowledge.Int31Bits -> str "bits"
-    | Retroknowledge.Int31Type -> str "type"
-    | Retroknowledge.Int31Twice -> str "twice"
-    | Retroknowledge.Int31TwicePlusOne -> str "twice plus one"
-    | Retroknowledge.Int31Phi -> str "phi"
-    | Retroknowledge.Int31PhiInv -> str "phi inv"
-    | Retroknowledge.Int31Plus -> str "plus"
-    | Retroknowledge.Int31Times -> str "times"
-    | Retroknowledge.Int31Constructor -> assert false
-    | Retroknowledge.Int31PlusC -> str "plusc"
-    | Retroknowledge.Int31PlusCarryC -> str "pluscarryc"
-    | Retroknowledge.Int31Minus -> str "minus"
-    | Retroknowledge.Int31MinusC -> str "minusc"
-    | Retroknowledge.Int31MinusCarryC -> str "minuscarryc"
-    | Retroknowledge.Int31TimesC -> str "timesc"
-    | Retroknowledge.Int31Div21 -> str "div21"
-    | Retroknowledge.Int31Div -> str "div"
-    | Retroknowledge.Int31Diveucl -> str "diveucl"
-    | Retroknowledge.Int31AddMulDiv -> str "addmuldiv"
-    | Retroknowledge.Int31Compare -> str "compare"
-    | Retroknowledge.Int31Head0 -> str "head0"
-    | Retroknowledge.Int31Tail0 -> str "tail0"
-    | Retroknowledge.Int31Lor -> str "lor"
-    | Retroknowledge.Int31Land -> str "land"
-    | Retroknowledge.Int31Lxor -> str "lxor"
-
-let pr_retroknowledge_field f =
-  match f with
-  | Retroknowledge.KInt31 i31f -> pr_r_int31_field i31f
-
-VERNAC ARGUMENT EXTEND retroknowledge_int31
-PRINTED BY pr_r_int31_field
-| [ "int31" "bits" ] -> [ Retroknowledge.Int31Bits ]
-| [ "int31" "type" ] -> [ Retroknowledge.Int31Type ]
-| [ "int31" "twice" ] -> [ Retroknowledge.Int31Twice ]
-| [ "int31" "twice" "plus" "one" ] -> [ Retroknowledge.Int31TwicePlusOne ]
-| [ "int31" "phi" ] -> [ Retroknowledge.Int31Phi ]
-| [ "int31" "phi" "inv" ] -> [ Retroknowledge.Int31PhiInv ]
-| [ "int31" "plus" ] -> [ Retroknowledge.Int31Plus ]
-| [ "int31" "plusc" ] -> [ Retroknowledge.Int31PlusC ]
-| [ "int31" "pluscarryc" ] -> [ Retroknowledge.Int31PlusCarryC ]
-| [ "int31" "minus" ] -> [ Retroknowledge.Int31Minus ]
-| [ "int31" "minusc" ] -> [ Retroknowledge.Int31MinusC ]
-| [ "int31" "minuscarryc" ] -> [ Retroknowledge.Int31MinusCarryC ]
-| [ "int31" "times" ] -> [ Retroknowledge.Int31Times ]
-| [ "int31" "timesc" ] -> [ Retroknowledge.Int31TimesC ]
-| [ "int31" "div21" ] -> [ Retroknowledge.Int31Div21 ]
-| [ "int31" "div" ] -> [ Retroknowledge.Int31Div ]
-| [ "int31" "diveucl" ] -> [ Retroknowledge.Int31Diveucl ]
-| [ "int31" "addmuldiv" ] -> [ Retroknowledge.Int31AddMulDiv ]
-| [ "int31" "compare" ] -> [ Retroknowledge.Int31Compare ]
-| [ "int31" "head0" ] -> [ Retroknowledge.Int31Head0 ]
-| [ "int31" "tail0" ] -> [ Retroknowledge.Int31Tail0 ]
-| [ "int31" "lor" ] -> [ Retroknowledge.Int31Lor ]
-| [ "int31" "land" ] -> [ Retroknowledge.Int31Land ]
-| [ "int31" "lxor" ] -> [ Retroknowledge.Int31Lxor ]
-END
-
-VERNAC ARGUMENT EXTEND retroknowledge_field
-PRINTED BY pr_retroknowledge_field
-| [ retroknowledge_int31 (i) ] -> [ Retroknowledge.KInt31 i ]
-END
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index e477b12cd3..fa70235975 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -72,11 +72,6 @@ val test_lpar_id_colon : unit Pcoq.Entry.t
 
 val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type
 
-(** Spiwack: Primitive for retroknowledge registration *)
-
-val retroknowledge_field : Retroknowledge.field Pcoq.Entry.t
-val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type
-
 val wit_in_clause :
   (lident Locus.clause_expr,
    lident Locus.clause_expr,
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 2e932dd059..9538abcb18 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -548,11 +548,12 @@ END
 (*spiwack : Vernac commands for retroknowledge                        *)
 
 VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF
- | [ "Register" constr(c) "as" retroknowledge_field(f) ] ->
+ | [ "Register" constr(c) "as" "int31" pre_ident(n) ] ->
            [ let env = Global.env () in
              let evd = Evd.from_env env in
              let tc,_ctx = Constrintern.interp_constr env evd c in
              let tc = EConstr.to_constr evd tc in
+             let f = Retroknowledge.(KInt31 (int31_field_of_string n)) in
              Global.register f tc ]
 END