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

3 files changed, 146 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
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 6534163bbb..a1da9d2b31 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -50,3 +50,11 @@ val glob_in_arg_hyp_to_clause :  (Names.identifier list option * bool)  -> Tacti
 val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.Entry.e
 val rawwit_by_arg_tac :  raw_tactic_expr option raw_abstract_argument_type
 val wit_by_arg_tac : glob_tactic_expr option closed_abstract_argument_type
+
+
+
+(* Spiwack: Primitive for retroknowledge registration *)
+
+val retroknowledge_field : Retroknowledge.field Pcoq.Gram.Entry.e
+val rawwit_retroknowledge_field :  Retroknowledge.field raw_abstract_argument_type
+val wit_retroknowledge_field : Retroknowledge.field closed_abstract_argument_type
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 4ee02e0b82..d51d17aaf4 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -400,14 +400,47 @@ VERNAC COMMAND EXTEND ImplicitTactic
     [ Tacinterp.declare_implicit_tactic (Tacinterp.interp tac) ]
 END
 
+
+
+
+(*spiwack : Vernac commands for retroknowledge *)
+
+VERNAC COMMAND EXTEND RetroknowledgeRegister
+ | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] -> 
+           [ let tc = Constrintern.interp_constr Evd.empty (Global.env ()) c in
+             let tb = Constrintern.interp_constr Evd.empty (Global.env ()) b in
+             Global.register f tc tb ]
+END
+
+(* spiwack : Vernac commands for developement *)
+
+(* arnaud : comment out/clear ? *)
+VERNAC COMMAND EXTEND InternalRepresentation (* Prints internal representation of the argument *)
+| [ "Internal" "Representation" "of" constr(t) ] -> 
+    [ let t' = Constrintern.interp_constr Evd.empty (Global.env ()) t in
+      pp (str (string_of_constr t'))]
+END
+
+VERNAC COMMAND EXTEND Bytecode (* Prints Bytecode representation of the argument *)
+| [ "Bytecode" "of" constr(t) ] -> 
+    [ let t' = Constrintern.interp_constr Evd.empty (Global.env ()) t in
+      let (bc,_,_) = Cbytegen.compile (Environ.pre_env (Global.env ())) t' in
+      pp (str (Cbytecodes.string_of_instr bc))]
+END
+
+(* /spiwack *)
+
+
 TACTIC EXTEND apply_in
 | ["apply" constr_with_bindings(c) "in" hyp(id) ] -> [ apply_in false id [c] ]
 | ["apply" constr_with_bindings(c) "," constr_with_bindings_list_sep(cl,",") 
    "in" hyp(id) ] -> [ apply_in false id (c::cl) ]
 END
 
+
 TACTIC EXTEND eapply_in
 | ["eapply" constr_with_bindings(c) "in" hyp(id) ] -> [ apply_in true id [c] ]
 | ["epply" constr_with_bindings(c) "," constr_with_bindings_list_sep(cl,",") 
    "in" hyp(id) ] -> [ apply_in true id (c::cl) ]
 END
+