Processor integers + Print assumption (see coqdev mailing list for the

details).




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 105 insertions, 0 deletions

diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 498afee99e..327bd24f79 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -236,3 +236,108 @@ let raw_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause snd
 let glob_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause (fun x -> x) 
 
 
+(* spiwack argument for the commands of the retroknowledge *)
+
+let (wit_r_nat_field, globwit_r_nat_field, rawwit_r_nat_field) =
+  Genarg.create_arg "r_nat_field"
+let (wit_r_n_field, globwit_r_n_field, rawwit_r_n_field) =
+  Genarg.create_arg "r_n_field"
+let (wit_r_int31_field, globwit_r_int31_field, rawwit_r_int31_field) =
+  Genarg.create_arg "r_int31_field"
+let (wit_r_field, globwit_r_field, rawwit_r_field) =
+  Genarg.create_arg "r_field"
+
+(* spiwack: the print functions are incomplete, but I don't know what they are
+	used for *)
+let pr_r_nat_field _ _ _ natf = 
+  str "nat " ++
+  match natf with
+    | Retroknowledge.NatType -> str "type"
+    | Retroknowledge.NatPlus -> str "plus"
+    | Retroknowledge.NatTimes -> str "times"
+
+let pr_r_n_field _ _ _ nf =
+  str "binary N " ++
+  match nf with
+    | Retroknowledge.NPositive -> str "positive"
+    | Retroknowledge.NType -> str "type"
+    | Retroknowledge.NTwice -> str "twice"
+    | Retroknowledge.NTwicePlusOne -> str "twice plus one"
+    | Retroknowledge.NPhi -> str "phi"
+    | Retroknowledge.NPhiInv -> str "phi inv"
+    | Retroknowledge.NPlus -> str "plus"
+    | Retroknowledge.NTimes -> str "times"
+
+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"
+
+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) ++
+                                           str "in " ++ str group 
+
+ARGUMENT EXTEND retroknowledge_nat
+TYPED AS r_nat_field
+PRINTED BY pr_r_nat_field
+| [ "nat" "type" ] -> [ Retroknowledge.NatType ]
+| [ "nat" "plus" ] -> [ Retroknowledge.NatPlus ]
+| [ "nat" "times" ] -> [ Retroknowledge.NatTimes ]
+END
+
+
+ARGUMENT EXTEND retroknowledge_binary_n
+TYPED AS r_n_field 
+PRINTED BY pr_r_n_field
+| [ "binary" "N" "positive" ] -> [ Retroknowledge.NPositive ]
+| [ "binary" "N" "type" ] -> [ Retroknowledge.NType ]
+| [ "binary" "N" "twice" ] -> [ Retroknowledge.NTwice ]
+| [ "binary" "N" "twice" "plus" "one" ] -> [ Retroknowledge.NTwicePlusOne ]
+| [ "binary" "N" "phi" ] -> [ Retroknowledge.NPhi ]
+| [ "binary" "N" "phi" "inv" ] -> [ Retroknowledge.NPhiInv ]
+| [ "binary" "N" "plus" ] -> [ Retroknowledge.NPlus ]
+| [ "binary" "N" "times" ] -> [ Retroknowledge.NTimes ]
+END
+
+ARGUMENT EXTEND retroknowledge_int31
+TYPED AS r_int31_field 
+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" "addmuldiv" ] -> [ Retroknowledge.Int31AddMulDiv ]
+| [ "int31" "compare" ] -> [ Retroknowledge.Int31Compare ]
+END
+
+ARGUMENT EXTEND retroknowledge_field 
+TYPED AS r_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) ]
+END
\ No newline at end of file