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/environ.ml | 4 ++-- kernel/retroknowledge.ml | 2 +- kernel/retroknowledge.mli | 2 +- kernel/safe_typing.ml | 40 +++++++++++++++++------------------ plugins/ltac/extraargs.ml4 | 11 ++-------- theories/Numbers/Cyclic/Int31/Int31.v | 38 ++++++++++++++++----------------- 6 files changed, 45 insertions(+), 52 deletions(-) diff --git a/kernel/environ.ml b/kernel/environ.ml index e7efa5e2c9..64c93a2607 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -695,10 +695,10 @@ let register_one env field entry = (* [register env field entry] may register several fields when needed *) let register env field entry = match field with - | KInt31 (grp, Int31Type) -> + | KInt31 Int31Type -> let i31c = match kind entry with | Ind i31t -> mkConstructUi (i31t, 1) | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.") in - register_one (register_one env (KInt31 (grp,Int31Constructor)) i31c) field entry + register_one (register_one env (KInt31 Int31Constructor) i31c) field entry | field -> register_one env field entry 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 *) diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 02d961d893..6b2c74e9df 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -46,7 +46,7 @@ type int31_field = | Int31Lxor type field = - | KInt31 of string*int31_field + | KInt31 of int31_field (** This type represent an atomic action of the retroknowledge. It is stored in the compiled libraries diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 6c87ff570f..15f972afcf 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -992,12 +992,12 @@ fun rk value field -> let int31_binop_from_const op prim = int31_op_from_const 2 op prim in let int31_unop_from_const op prim = int31_op_from_const 1 op prim in match field with - | KInt31 (grp, Int31Type) -> + | KInt31 Int31Type -> let int31bit = (* invariant : the type of bits is registered, otherwise the function would raise Not_found. The invariant is enforced in safe_typing.ml *) match field with - | KInt31 (grp, Int31Type) -> Retroknowledge.find rk (KInt31 (grp,Int31Bits)) + | KInt31 Int31Type -> Retroknowledge.find rk (KInt31 Int31Bits) | _ -> anomaly ~label:"Environ.register" (Pp.str "add_int31_decompilation_from_type called with an abnormal field.") in @@ -1019,46 +1019,46 @@ fun rk value field -> vm_before_match = Some Clambda.int31_escape_before_match; native_before_match = Some (Nativelambda.before_match_int31 i31bit_type); } - | KInt31 (_, Int31Constructor) -> + | KInt31 Int31Constructor -> { empty_reactive_info with vm_constant_static = Some Clambda.compile_structured_int31; vm_constant_dynamic = Some Clambda.dynamic_int31_compilation; native_constant_static = Some Nativelambda.compile_static_int31; native_constant_dynamic = Some Nativelambda.compile_dynamic_int31; } - | KInt31 (_, Int31Plus) -> int31_binop_from_const Cbytecodes.Kaddint31 + | KInt31 Int31Plus -> int31_binop_from_const Cbytecodes.Kaddint31 CPrimitives.Int31add - | KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31 + | KInt31 Int31PlusC -> int31_binop_from_const Cbytecodes.Kaddcint31 CPrimitives.Int31addc - | KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31 + | KInt31 Int31PlusCarryC -> int31_binop_from_const Cbytecodes.Kaddcarrycint31 CPrimitives.Int31addcarryc - | KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31 + | KInt31 Int31Minus -> int31_binop_from_const Cbytecodes.Ksubint31 CPrimitives.Int31sub - | KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31 + | KInt31 Int31MinusC -> int31_binop_from_const Cbytecodes.Ksubcint31 CPrimitives.Int31subc - | KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const + | KInt31 Int31MinusCarryC -> int31_binop_from_const Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc - | KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31 + | KInt31 Int31Times -> int31_binop_from_const Cbytecodes.Kmulint31 CPrimitives.Int31mul - | KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31 + | KInt31 Int31TimesC -> int31_binop_from_const Cbytecodes.Kmulcint31 CPrimitives.Int31mulc - | KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31 + | KInt31 Int31Div21 -> int31_op_from_const 3 Cbytecodes.Kdiv21int31 CPrimitives.Int31div21 - | KInt31 (_, Int31Diveucl) -> int31_binop_from_const Cbytecodes.Kdivint31 + | KInt31 Int31Diveucl -> int31_binop_from_const Cbytecodes.Kdivint31 CPrimitives.Int31diveucl - | KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31 + | KInt31 Int31AddMulDiv -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31 CPrimitives.Int31addmuldiv - | KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31 + | KInt31 Int31Compare -> int31_binop_from_const Cbytecodes.Kcompareint31 CPrimitives.Int31compare - | KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31 + | KInt31 Int31Head0 -> int31_unop_from_const Cbytecodes.Khead0int31 CPrimitives.Int31head0 - | KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31 + | KInt31 Int31Tail0 -> int31_unop_from_const Cbytecodes.Ktail0int31 CPrimitives.Int31tail0 - | KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31 + | KInt31 Int31Lor -> int31_binop_from_const Cbytecodes.Klorint31 CPrimitives.Int31lor - | KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31 + | KInt31 Int31Land -> int31_binop_from_const Cbytecodes.Klandint31 CPrimitives.Int31land - | KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31 + | KInt31 Int31Lxor -> int31_binop_from_const Cbytecodes.Klxorint31 CPrimitives.Int31lxor | _ -> empty_reactive_info diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 38600695dc..a9133512e0 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -345,11 +345,7 @@ let pr_r_int31_field i31f = let pr_retroknowledge_field f = match f with - (* | Retroknowledge.KEq -> str "equality" - | Retroknowledge.KNat natf -> pr_r_nat_field () () () natf - | Retroknowledge.KN nf -> pr_r_n_field () () () nf *) - | Retroknowledge.KInt31 (group, i31f) -> (pr_r_int31_field i31f) ++ - spc () ++ str "in " ++ qs group + | Retroknowledge.KInt31 i31f -> pr_r_int31_field i31f VERNAC ARGUMENT EXTEND retroknowledge_int31 PRINTED BY pr_r_int31_field @@ -381,8 +377,5 @@ END VERNAC ARGUMENT EXTEND retroknowledge_field PRINTED BY pr_retroknowledge_field -(*| [ "equality" ] -> [ Retroknowledge.KEq ] -| [ retroknowledge_nat(n)] -> [ Retroknowledge.KNat n ] -| [ retroknowledge_binary_n (n)] -> [ Retroknowledge.KN n ]*) -| [ retroknowledge_int31 (i) "in" string(g)] -> [ Retroknowledge.KInt31(g,i) ] +| [ retroknowledge_int31 (i) ] -> [ Retroknowledge.KInt31 i ] END diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 77ab624ca5..5c1c5d794d 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -45,8 +45,8 @@ Inductive int31 : Type := I31 : digits31 int31. (* spiwack: Registration of the type of integers, so that the matchs in the functions below perform dynamic decompilation (otherwise some segfault occur when they are applied to one non-closed term and one closed term). *) -Register digits as int31 bits in "coq_int31" by True. -Register int31 as int31 type in "coq_int31" by True. +Register digits as int31 bits by True. +Register int31 as int31 type by True. Declare Scope int31_scope. Declare ML Module "int31_syntax_plugin". @@ -345,21 +345,21 @@ Definition lor31 n m := phi_inv (Z.lor (phi n) (phi m)). Definition land31 n m := phi_inv (Z.land (phi n) (phi m)). Definition lxor31 n m := phi_inv (Z.lxor (phi n) (phi m)). -Register add31 as int31 plus in "coq_int31" by True. -Register add31c as int31 plusc in "coq_int31" by True. -Register add31carryc as int31 pluscarryc in "coq_int31" by True. -Register sub31 as int31 minus in "coq_int31" by True. -Register sub31c as int31 minusc in "coq_int31" by True. -Register sub31carryc as int31 minuscarryc in "coq_int31" by True. -Register mul31 as int31 times in "coq_int31" by True. -Register mul31c as int31 timesc in "coq_int31" by True. -Register div3121 as int31 div21 in "coq_int31" by True. -Register div31 as int31 diveucl in "coq_int31" by True. -Register compare31 as int31 compare in "coq_int31" by True. -Register addmuldiv31 as int31 addmuldiv in "coq_int31" by True. -Register lor31 as int31 lor in "coq_int31" by True. -Register land31 as int31 land in "coq_int31" by True. -Register lxor31 as int31 lxor in "coq_int31" by True. +Register add31 as int31 plus by True. +Register add31c as int31 plusc by True. +Register add31carryc as int31 pluscarryc by True. +Register sub31 as int31 minus by True. +Register sub31c as int31 minusc by True. +Register sub31carryc as int31 minuscarryc by True. +Register mul31 as int31 times by True. +Register mul31c as int31 timesc by True. +Register div3121 as int31 div21 by True. +Register div31 as int31 diveucl by True. +Register compare31 as int31 compare by True. +Register addmuldiv31 as int31 addmuldiv by True. +Register lor31 as int31 lor by True. +Register land31 as int31 land by True. +Register lxor31 as int31 lxor by True. Definition lnot31 n := lxor31 Tn n. Definition ldiff31 n m := land31 n (lnot31 m). @@ -485,5 +485,5 @@ Definition tail031 (i:int31) := end) i On. -Register head031 as int31 head0 in "coq_int31" by True. -Register tail031 as int31 tail0 in "coq_int31" by True. +Register head031 as int31 head0 by True. +Register tail031 as int31 tail0 by True. -- cgit v1.2.3 From ab2560233f2e6fc8c26853af6991533d8d335e16 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Fri, 7 Sep 2018 11:34:32 +0200 Subject: Retroknowledge: remove the (unused) by clause --- kernel/safe_typing.ml | 4 ++-- kernel/safe_typing.mli | 2 +- library/global.ml | 4 ++-- library/global.mli | 2 +- plugins/ltac/extratactics.ml4 | 6 ++---- theories/Numbers/Cyclic/Int31/Int31.v | 38 +++++++++++++++++------------------ 6 files changed, 27 insertions(+), 29 deletions(-) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 15f972afcf..95eea2d6b0 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -892,8 +892,8 @@ let retroknowledge f senv = Environ.retroknowledge f (env_of_senv senv) [@@@ocaml.warning "+3"] -let register field value by_clause senv = - (* todo : value closed, by_clause safe, by_clause of the proper type*) +let register field value senv = + (* todo : value closed *) (* spiwack : updates the safe_env with the information that the register action has to be performed (again) when the environment is imported *) { senv with diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 502e2970a1..2f83e71726 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -215,7 +215,7 @@ val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a [@@ocaml.deprecated "Use the projection of Environ.env"] val register : - field -> Retroknowledge.entry -> Constr.constr -> safe_transformer0 + field -> Retroknowledge.entry -> safe_transformer0 val register_inline : Constant.t -> safe_transformer0 diff --git a/library/global.ml b/library/global.ml index e833f71142..5872126a12 100644 --- a/library/global.ml +++ b/library/global.ml @@ -271,8 +271,8 @@ let with_global f = push_context_set false ctx; a (* spiwack: register/unregister functions for retroknowledge *) -let register field value by_clause = - globalize0 (Safe_typing.register field value by_clause) +let register field value = + globalize0 (Safe_typing.register field value) let register_inline c = globalize0 (Safe_typing.register_inline c) diff --git a/library/global.mli b/library/global.mli index 2819c187ed..1708976222 100644 --- a/library/global.mli +++ b/library/global.mli @@ -148,7 +148,7 @@ val universes_of_global : GlobRef.t -> Univ.AUContext.t (** {6 Retroknowledge } *) val register : - Retroknowledge.field -> Constr.constr -> Constr.constr -> unit + Retroknowledge.field -> Constr.constr -> unit val register_inline : Constant.t -> unit diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index dc027c4041..2e932dd059 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -548,14 +548,12 @@ END (*spiwack : Vernac commands for retroknowledge *) VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF - | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] -> + | [ "Register" constr(c) "as" retroknowledge_field(f) ] -> [ let env = Global.env () in let evd = Evd.from_env env in let tc,_ctx = Constrintern.interp_constr env evd c in - let tb,_ctx(*FIXME*) = Constrintern.interp_constr env evd b in let tc = EConstr.to_constr evd tc in - let tb = EConstr.to_constr evd tb in - Global.register f tc tb ] + Global.register f tc ] END diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 5c1c5d794d..f1b02759c5 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -45,8 +45,8 @@ Inductive int31 : Type := I31 : digits31 int31. (* spiwack: Registration of the type of integers, so that the matchs in the functions below perform dynamic decompilation (otherwise some segfault occur when they are applied to one non-closed term and one closed term). *) -Register digits as int31 bits by True. -Register int31 as int31 type by True. +Register digits as int31 bits. +Register int31 as int31 type. Declare Scope int31_scope. Declare ML Module "int31_syntax_plugin". @@ -345,21 +345,21 @@ Definition lor31 n m := phi_inv (Z.lor (phi n) (phi m)). Definition land31 n m := phi_inv (Z.land (phi n) (phi m)). Definition lxor31 n m := phi_inv (Z.lxor (phi n) (phi m)). -Register add31 as int31 plus by True. -Register add31c as int31 plusc by True. -Register add31carryc as int31 pluscarryc by True. -Register sub31 as int31 minus by True. -Register sub31c as int31 minusc by True. -Register sub31carryc as int31 minuscarryc by True. -Register mul31 as int31 times by True. -Register mul31c as int31 timesc by True. -Register div3121 as int31 div21 by True. -Register div31 as int31 diveucl by True. -Register compare31 as int31 compare by True. -Register addmuldiv31 as int31 addmuldiv by True. -Register lor31 as int31 lor by True. -Register land31 as int31 land by True. -Register lxor31 as int31 lxor by True. +Register add31 as int31 plus. +Register add31c as int31 plusc. +Register add31carryc as int31 pluscarryc. +Register sub31 as int31 minus. +Register sub31c as int31 minusc. +Register sub31carryc as int31 minuscarryc. +Register mul31 as int31 times. +Register mul31c as int31 timesc. +Register div3121 as int31 div21. +Register div31 as int31 diveucl. +Register compare31 as int31 compare. +Register addmuldiv31 as int31 addmuldiv. +Register lor31 as int31 lor. +Register land31 as int31 land. +Register lxor31 as int31 lxor. Definition lnot31 n := lxor31 Tn n. Definition ldiff31 n m := land31 n (lnot31 m). @@ -485,5 +485,5 @@ Definition tail031 (i:int31) := end) i On. -Register head031 as int31 head0 by True. -Register tail031 as int31 tail0 by True. +Register head031 as int31 head0. +Register tail031 as int31 tail0. -- 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 +++++++++++++++++ kernel/retroknowledge.mli | 2 ++ plugins/ltac/extraargs.ml4 | 68 ------------------------------------------- plugins/ltac/extraargs.mli | 5 ---- plugins/ltac/extratactics.ml4 | 3 +- 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 -- 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/clambda.ml | 13 +++++++------ kernel/environ.ml | 16 ++++++++-------- kernel/environ.mli | 2 +- kernel/modops.ml | 2 +- kernel/nativelambda.ml | 33 +++++++++++++++++---------------- kernel/retroknowledge.ml | 17 ++++------------- kernel/retroknowledge.mli | 29 +++++++++++++---------------- kernel/safe_typing.ml | 16 ++++++++-------- kernel/safe_typing.mli | 2 +- library/global.mli | 2 +- plugins/ltac/extratactics.ml4 | 15 --------------- pretyping/nativenorm.ml | 2 +- pretyping/vnorm.ml | 2 +- vernac/g_vernac.mlg | 6 ++++-- vernac/ppvernac.ml | 6 +++++- vernac/vernacentries.ml | 14 +++++++++----- vernac/vernacexpr.ml | 3 ++- 17 files changed, 83 insertions(+), 97 deletions(-) diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 961036d3c5..75cf6b747d 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -659,11 +659,11 @@ let rec lambda_of_constr env c = (* translation of the argument *) let la = lambda_of_constr env a in - let entry = mkInd ind in + let gr = GlobRef.IndRef ind in let la = try Retroknowledge.get_vm_before_match_info env.global_env.retroknowledge - entry la + gr la with Not_found -> la in (* translation of the type *) @@ -721,7 +721,7 @@ and lambda_of_app env f args = (try (* We delay the compilation of arguments to avoid an exponential behavior *) let f = Retroknowledge.get_vm_compiling_info env.global_env.retroknowledge - (mkConstU (kn,u)) in + (GlobRef.ConstRef kn) in let args = lambda_of_args env 0 args in f args with Not_found -> @@ -734,6 +734,7 @@ and lambda_of_app env f args = | Construct (c,_) -> let tag, nparams, arity = Renv.get_construct_info env c in let nargs = Array.length args in + let gr = GlobRef.ConstructRef c in if Int.equal (nparams + arity) nargs then (* fully applied *) (* spiwack: *) (* 1/ tries to compile the constructor in an optimal way, @@ -748,7 +749,7 @@ and lambda_of_app env f args = try Retroknowledge.get_vm_constant_static_info env.global_env.retroknowledge - f args + gr args with NotClosed -> (* 2/ if the arguments are not all closed (this is expectingly (and it is currently the case) the only @@ -769,7 +770,7 @@ and lambda_of_app env f args = let args = lambda_of_args env nparams rargs in Retroknowledge.get_vm_constant_dynamic_info env.global_env.retroknowledge - f args + gr args with Not_found -> (* 3/ if no special behavior is available, then the compiler falls back to the normal behavior *) @@ -782,7 +783,7 @@ and lambda_of_app env f args = (try (Retroknowledge.get_vm_constant_dynamic_info env.global_env.retroknowledge - f) args + gr) args with Not_found -> if nparams <= nargs then (* got all parameters *) makeblock tag 0 arity args diff --git a/kernel/environ.ml b/kernel/environ.ml index 64c93a2607..62c14f6f07 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -693,12 +693,12 @@ let register_one env field entry = { env with retroknowledge = Retroknowledge.add_field env.retroknowledge field entry } (* [register env field entry] may register several fields when needed *) -let register env field entry = +let register env field gr = match field with - | KInt31 Int31Type -> - let i31c = match kind entry with - | Ind i31t -> mkConstructUi (i31t, 1) - | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.") - in - register_one (register_one env (KInt31 Int31Constructor) i31c) field entry - | field -> register_one env field entry + | KInt31 Int31Type -> + let i31c = match gr with + | GlobRef.IndRef i31t -> GlobRef.ConstructRef (i31t, 1) + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.") + in + register_one (register_one env (KInt31 Int31Constructor) i31c) field gr + | field -> register_one env field gr diff --git a/kernel/environ.mli b/kernel/environ.mli index f45b7be821..1343b9029b 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -325,7 +325,7 @@ val retroknowledge : (retroknowledge->'a) -> env -> 'a val registered : env -> field -> bool -val register : env -> field -> Retroknowledge.entry -> env +val register : env -> field -> GlobRef.t -> env (** Native compiler *) val no_link_info : link_info diff --git a/kernel/modops.ml b/kernel/modops.ml index 98a9973117..9435f46c6b 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -267,7 +267,7 @@ let subst_structure subst = subst_structure subst do_delta_codom (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *) let add_retroknowledge = let perform rkaction env = match rkaction with - | Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) -> + | Retroknowledge.RKRegister (f, ((GlobRef.ConstRef _ | GlobRef.IndRef _) as e)) -> Environ.register env f e | _ -> CErrors.anomaly ~label:"Modops.add_retroknowledge" diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 122fe95df4..ab40c643f9 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -373,14 +373,14 @@ let is_lazy env prefix t = | App (f,args) -> begin match kind f with | Construct (c,_) -> - let entry = mkInd (fst c) in - (try - let _ = - Retroknowledge.get_native_before_match_info env.retroknowledge - entry prefix c Llazy; - in + let gr = GlobRef.IndRef (fst c) in + (try + let _ = + Retroknowledge.get_native_before_match_info env.retroknowledge + gr prefix c Llazy; + in false - with Not_found -> true) + with Not_found -> true) | _ -> true end | LetIn _ | Case _ | Proj _ -> true @@ -482,12 +482,12 @@ let rec lambda_of_constr cache env sigma c = in (* translation of the argument *) let la = lambda_of_constr cache env sigma a in - let entry = mkInd ind in + let gr = GlobRef.IndRef ind in let la = - try - Retroknowledge.get_native_before_match_info (env).retroknowledge - entry prefix (ind,1) la - with Not_found -> la + try + Retroknowledge.get_native_before_match_info (env).retroknowledge + gr prefix (ind,1) la + with Not_found -> la in (* translation of the type *) let lt = lambda_of_constr cache env sigma t in @@ -536,7 +536,7 @@ and lambda_of_app cache env sigma f args = let prefix = get_const_prefix env kn in (* We delay the compilation of arguments to avoid an exponential behavior *) let f = Retroknowledge.get_native_compiling_info - (env).retroknowledge (mkConst kn) prefix in + (env).retroknowledge (GlobRef.ConstRef kn) prefix in let args = lambda_of_args cache env sigma 0 args in f args with Not_found -> @@ -561,17 +561,18 @@ and lambda_of_app cache env sigma f args = let expected = nparams + arity in let nargs = Array.length args in let prefix = get_mind_prefix env (fst (fst c)) in + let gr = GlobRef.ConstructRef c in if Int.equal nargs expected then try try Retroknowledge.get_native_constant_static_info (env).retroknowledge - f args + gr args with NotClosed -> assert (Int.equal nparams 0); (* should be fine for int31 *) let args = lambda_of_args cache env sigma nparams args in Retroknowledge.get_native_constant_dynamic_info - (env).retroknowledge f prefix c args + (env).retroknowledge gr prefix c args with Not_found -> let args = lambda_of_args cache env sigma nparams args in makeblock env c u tag args @@ -579,7 +580,7 @@ and lambda_of_app cache env sigma f args = let args = lambda_of_args cache env sigma 0 args in (try Retroknowledge.get_native_constant_dynamic_info - (env).retroknowledge f prefix c args + (env).retroknowledge gr prefix c args with Not_found -> mkLapp (Lconstruct (prefix, (c,u))) args) | _ -> 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*) diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 1436f23739..1fc3cfb817 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -13,9 +13,6 @@ open Constr type retroknowledge -(** aliased type for clarity purpose*) -type entry = Constr.t - (** the following types correspond to the different "things" the kernel can learn about.*) type int31_field = @@ -55,7 +52,7 @@ val int31_field_of_string : string -> int31_field 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 (** initial value for retroknowledge *) @@ -66,7 +63,7 @@ val initial_retroknowledge : retroknowledge and the continuation cont of the bytecode compilation returns the compilation of id in cont if it has a specific treatment or raises Not_found if id should be compiled as usual *) -val get_vm_compiling_info : retroknowledge -> entry -> +val get_vm_compiling_info : retroknowledge -> GlobRef.t -> Cinstr.lambda array -> Cinstr.lambda (*Given an identifier id (usually Construct _) and its argument array, returns a function that tries an ad-hoc optimisated @@ -75,7 +72,7 @@ val get_vm_compiling_info : retroknowledge -> entry -> raises Not_found if id should be compiled as usual, and expectingly CBytecodes.NotClosed if the term is not a closed constructor pattern (a constant for the compiler) *) -val get_vm_constant_static_info : retroknowledge -> entry -> +val get_vm_constant_static_info : retroknowledge -> GlobRef.t -> constr array -> Cinstr.lambda (*Given an identifier id (usually Construct _ ) @@ -83,45 +80,45 @@ val get_vm_constant_static_info : retroknowledge -> entry -> of id+args+cont when id has a specific treatment (in the case of 31-bit integers, that would be the dynamic compilation into integers) or raises Not_found if id should be compiled as usual *) -val get_vm_constant_dynamic_info : retroknowledge -> entry -> +val get_vm_constant_dynamic_info : retroknowledge -> GlobRef.t -> Cinstr.lambda array -> Cinstr.lambda (** Given a type identifier, this function is used before compiling a match over this type. In the case of 31-bit integers for instance, it is used to add the instruction sequence which would perform a dynamic decompilation in case the argument of the match is not in coq representation *) -val get_vm_before_match_info : retroknowledge -> entry -> Cinstr.lambda +val get_vm_before_match_info : retroknowledge -> GlobRef.t -> Cinstr.lambda -> Cinstr.lambda (** Given a type identifier, this function is used by pretyping/vnorm.ml to recover the elements of that type from their compiled form if it's non standard (it is used (and can be used) only when the compiled form is not a block *) -val get_vm_decompile_constant_info : retroknowledge -> entry -> int -> constr +val get_vm_decompile_constant_info : retroknowledge -> GlobRef.t -> int -> constr -val get_native_compiling_info : retroknowledge -> entry -> Nativeinstr.prefix -> +val get_native_compiling_info : retroknowledge -> GlobRef.t -> Nativeinstr.prefix -> Nativeinstr.lambda array -> Nativeinstr.lambda -val get_native_constant_static_info : retroknowledge -> entry -> +val get_native_constant_static_info : retroknowledge -> GlobRef.t -> constr array -> Nativeinstr.lambda -val get_native_constant_dynamic_info : retroknowledge -> entry -> +val get_native_constant_dynamic_info : retroknowledge -> GlobRef.t -> Nativeinstr.prefix -> constructor -> Nativeinstr.lambda array -> Nativeinstr.lambda -val get_native_before_match_info : retroknowledge -> entry -> +val get_native_before_match_info : retroknowledge -> GlobRef.t -> Nativeinstr.prefix -> constructor -> Nativeinstr.lambda -> Nativeinstr.lambda (** the following functions are solely used in Environ and Safe_typing to implement the functions register and unregister (and mem) of Environ *) -val add_field : retroknowledge -> field -> entry -> retroknowledge +val add_field : retroknowledge -> field -> GlobRef.t -> retroknowledge val mem : retroknowledge -> field -> bool (* val remove : retroknowledge -> field -> retroknowledge *) -val find : retroknowledge -> field -> entry +val find : retroknowledge -> field -> GlobRef.t (** Dispatching type for the above [get_*] functions. *) @@ -163,4 +160,4 @@ val empty_reactive_info : reactive_info (** Hook to be set after the compiler are installed to dispatch fields into the above [get_*] functions. *) -val dispatch_hook : (retroknowledge -> entry -> field -> reactive_info) Hook.t +val dispatch_hook : (retroknowledge -> GlobRef.t -> field -> reactive_info) Hook.t diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 95eea2d6b0..9d302c69fb 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -977,16 +977,16 @@ let dispatch = it to the name of the coq definition in the reactive retroknowledge) *) let int31_op n op prim kn = { empty_reactive_info with - vm_compiling = Some (Clambda.compile_prim n op kn); - native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn)); + vm_compiling = Some (Clambda.compile_prim n op (kn, Univ.Instance.empty)); (*XXX: FIXME universes? *) + native_compiling = Some (Nativelambda.compile_prim prim kn); } in fun rk value field -> (* subfunction which shortens the (very common) dispatch of operations *) let int31_op_from_const n op prim = - match Constr.kind value with - | Constr.Const kn -> int31_op n op prim kn + match value with + | GlobRef.ConstRef kn -> int31_op n op prim kn | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.") in let int31_binop_from_const op prim = int31_op_from_const 2 op prim in @@ -1002,14 +1002,14 @@ fun rk value field -> (Pp.str "add_int31_decompilation_from_type called with an abnormal field.") in let i31bit_type = - match Constr.kind int31bit with - | Constr.Ind (i31bit_type,_) -> i31bit_type + match int31bit with + | GlobRef.IndRef i31bit_type -> i31bit_type | _ -> anomaly ~label:"Environ.register" (Pp.str "Int31Bits should be an inductive type.") in let int31_decompilation = - match Constr.kind value with - | Constr.Ind (i31t,_) -> + match value with + | GlobRef.IndRef i31t -> constr_of_int31 i31t i31bit_type | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.") diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 2f83e71726..08b97b718e 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -215,7 +215,7 @@ val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a [@@ocaml.deprecated "Use the projection of Environ.env"] val register : - field -> Retroknowledge.entry -> safe_transformer0 + field -> GlobRef.t -> safe_transformer0 val register_inline : Constant.t -> safe_transformer0 diff --git a/library/global.mli b/library/global.mli index 1708976222..6aeae9fd02 100644 --- a/library/global.mli +++ b/library/global.mli @@ -148,7 +148,7 @@ val universes_of_global : GlobRef.t -> Univ.AUContext.t (** {6 Retroknowledge } *) val register : - Retroknowledge.field -> Constr.constr -> unit + Retroknowledge.field -> GlobRef.t -> unit val register_inline : Constant.t -> unit diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 9538abcb18..8dad6260ae 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -544,21 +544,6 @@ END -(**********************************************************************) -(*spiwack : Vernac commands for retroknowledge *) - -VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF - | [ "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 - - - (**********************************************************************) (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as defined by Conor McBride *) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 246acfc92e..20185363e6 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -123,7 +123,7 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs = try if const then let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(0)) params in - Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkInd ind) tag, ctyp + Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (GlobRef.IndRef ind) tag, ctyp else raise Not_found with Not_found -> diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 255707dc7b..266e94b34d 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -79,7 +79,7 @@ let construct_of_constr const env tag typ = (* spiwack : here be a branch for specific decompilation handled by retroknowledge *) try if const then - ((Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkIndU indu) tag), + ((Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (GlobRef.IndRef ind) tag), typ) (*spiwack: this may need to be changed in case there are parameters in the type which may cause a constant value to have an arity. (type_constructor seems to be all about parameters actually) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 44c0159d1b..42d9239f36 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -212,8 +212,10 @@ GRAMMAR EXTEND Gram | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> { VernacScheme l } | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; l = LIST1 identref SEP "," -> { VernacCombinedScheme (id, l) } - | IDENT "Register"; IDENT "Inline"; id = identref -> - { VernacRegister(id, RegisterInline) } + | IDENT "Register"; g = global; "as"; IDENT "int31"; quid = qualid -> + { VernacRegister(g, RegisterRetroknowledge quid) } + | IDENT "Register"; IDENT "Inline"; g = global -> + { VernacRegister(g, RegisterInline) } | IDENT "Universe"; l = LIST1 identref -> { VernacUniverse l } | IDENT "Universes"; l = LIST1 identref -> { VernacUniverse l } | IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> { VernacConstraint l } diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 63e9e4fe49..9a356bbaef 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1161,7 +1161,11 @@ open Pputils | VernacRegister (id, RegisterInline) -> return ( hov 2 - (keyword "Register Inline" ++ spc() ++ pr_lident id) + (keyword "Register Inline" ++ spc() ++ pr_qualid id) + ) + | VernacRegister (id, RegisterRetroknowledge n) -> + return ( + hov 2 (keyword "Register" ++ spc () ++ pr_qualid id ++ spc () ++ keyword "as" ++ str "int31" ++ pr_qualid n) ) | VernacComments l -> return ( diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e6b3721134..2b4dfd19a6 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1950,14 +1950,18 @@ let vernac_locate = function | LocateOther (s, qid) -> print_located_other s qid | LocateFile f -> locate_file f -let vernac_register id r = +let vernac_register qid r = + let gr = Smartlocate.global_with_alias qid in if Proof_global.there_are_pending_proofs () then user_err Pp.(str "Cannot register a primitive while in proof editing mode."); - let kn = Constrintern.global_reference id.v in - if not (isConstRef kn) then - user_err Pp.(str "Register inline: a constant is expected"); match r with - | RegisterInline -> Global.register_inline (destConstRef kn) + | RegisterInline -> + if not (isConstRef gr) then + user_err Pp.(str "Register inline: a constant is expected"); + Global.register_inline (destConstRef gr) + | RegisterRetroknowledge n -> + let f = Retroknowledge.(KInt31 (int31_field_of_string (Libnames.string_of_qualid n))) in + Global.register f gr (********************) (* Proof management *) diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 11b2a7d802..ea69ed59a3 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -278,6 +278,7 @@ type extend_name = It will be extended with primitive inductive types and operators *) type register_kind = | RegisterInline + | RegisterRetroknowledge of qualid type bullet = Proof_bullet.t [@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"] @@ -438,7 +439,7 @@ type nonrec vernac_expr = | VernacPrint of printable | VernacSearch of searchable * Goal_select.t option * search_restriction | VernacLocate of locatable - | VernacRegister of lident * register_kind + | VernacRegister of qualid * register_kind | VernacComments of comment list (* Proof management *) -- 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 ++ kernel/retroknowledge.mli | 2 ++ theories/Numbers/Cyclic/Int31/Int31.v | 38 +++++++++++++++++------------------ vernac/g_vernac.mlg | 2 +- vernac/ppvernac.ml | 2 +- vernac/vernacentries.ml | 9 +++++++-- 6 files changed, 32 insertions(+), 23 deletions(-) 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} diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 1fc3cfb817..0a2ef5300e 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -47,6 +47,8 @@ type field = val int31_field_of_string : string -> int31_field +val int31_path : DirPath.t + (** 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/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index f1b02759c5..ca7d3ec074 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -45,8 +45,8 @@ Inductive int31 : Type := I31 : digits31 int31. (* spiwack: Registration of the type of integers, so that the matchs in the functions below perform dynamic decompilation (otherwise some segfault occur when they are applied to one non-closed term and one closed term). *) -Register digits as int31 bits. -Register int31 as int31 type. +Register digits as int31.bits. +Register int31 as int31.type. Declare Scope int31_scope. Declare ML Module "int31_syntax_plugin". @@ -345,21 +345,21 @@ Definition lor31 n m := phi_inv (Z.lor (phi n) (phi m)). Definition land31 n m := phi_inv (Z.land (phi n) (phi m)). Definition lxor31 n m := phi_inv (Z.lxor (phi n) (phi m)). -Register add31 as int31 plus. -Register add31c as int31 plusc. -Register add31carryc as int31 pluscarryc. -Register sub31 as int31 minus. -Register sub31c as int31 minusc. -Register sub31carryc as int31 minuscarryc. -Register mul31 as int31 times. -Register mul31c as int31 timesc. -Register div3121 as int31 div21. -Register div31 as int31 diveucl. -Register compare31 as int31 compare. -Register addmuldiv31 as int31 addmuldiv. -Register lor31 as int31 lor. -Register land31 as int31 land. -Register lxor31 as int31 lxor. +Register add31 as int31.plus. +Register add31c as int31.plusc. +Register add31carryc as int31.pluscarryc. +Register sub31 as int31.minus. +Register sub31c as int31.minusc. +Register sub31carryc as int31.minuscarryc. +Register mul31 as int31.times. +Register mul31c as int31.timesc. +Register div3121 as int31.div21. +Register div31 as int31.diveucl. +Register compare31 as int31.compare. +Register addmuldiv31 as int31.addmuldiv. +Register lor31 as int31.lor. +Register land31 as int31.land. +Register lxor31 as int31.lxor. Definition lnot31 n := lxor31 Tn n. Definition ldiff31 n m := land31 n (lnot31 m). @@ -485,5 +485,5 @@ Definition tail031 (i:int31) := end) i On. -Register head031 as int31 head0. -Register tail031 as int31 tail0. +Register head031 as int31.head0. +Register tail031 as int31.tail0. diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 42d9239f36..650b28ea67 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -212,7 +212,7 @@ GRAMMAR EXTEND Gram | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> { VernacScheme l } | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; l = LIST1 identref SEP "," -> { VernacCombinedScheme (id, l) } - | IDENT "Register"; g = global; "as"; IDENT "int31"; quid = qualid -> + | IDENT "Register"; g = global; "as"; quid = qualid -> { VernacRegister(g, RegisterRetroknowledge quid) } | IDENT "Register"; IDENT "Inline"; g = global -> { VernacRegister(g, RegisterInline) } diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 9a356bbaef..e15e57a003 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1165,7 +1165,7 @@ open Pputils ) | VernacRegister (id, RegisterRetroknowledge n) -> return ( - hov 2 (keyword "Register" ++ spc () ++ pr_qualid id ++ spc () ++ keyword "as" ++ str "int31" ++ pr_qualid n) + hov 2 (keyword "Register" ++ spc () ++ pr_qualid id ++ spc () ++ keyword "as" ++ pr_qualid n) ) | VernacComments l -> return ( diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 2b4dfd19a6..28abd1e6ef 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1960,8 +1960,13 @@ let vernac_register qid r = user_err Pp.(str "Register inline: a constant is expected"); Global.register_inline (destConstRef gr) | RegisterRetroknowledge n -> - let f = Retroknowledge.(KInt31 (int31_field_of_string (Libnames.string_of_qualid n))) in - Global.register f gr + let path, id = Libnames.repr_qualid n in + if DirPath.equal path Retroknowledge.int31_path + then + let f = Retroknowledge.(KInt31 (int31_field_of_string (Id.to_string id))) in + Global.register f gr + else + user_err Pp.(str "Register in unknown namespace: " ++ str (DirPath.to_string path)) (********************) (* Proof management *) -- cgit v1.2.3