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 --- plugins/ltac/extraargs.ml4 | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) (limited to 'plugins') 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 -- 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 --- plugins/ltac/extratactics.ml4 | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'plugins') 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 -- 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 --- plugins/ltac/extraargs.ml4 | 68 ------------------------------------------- plugins/ltac/extraargs.mli | 5 ---- plugins/ltac/extratactics.ml4 | 3 +- 3 files changed, 2 insertions(+), 74 deletions(-) (limited to 'plugins') 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 --- plugins/ltac/extratactics.ml4 | 15 --------------- 1 file changed, 15 deletions(-) (limited to 'plugins') 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 *) -- cgit v1.2.3