Nettoyage de code en vue de la release. Plus de Warning: Unused

Variable, et plus de trucs useless qui traînaient par ma faute (y 
compris dans le noyau, la honte).



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

kernel/cbytecodes.ml

@@ -235,7 +235,3 @@ type block =
 
 let draw_instr c =
   fprintf std_formatter "@[<v 0>%a@]" instruction_list c
-
-let string_of_instr c =
-  fprintf str_formatter "@[<v 0>%a@]" instruction_list c;
-  flush_str_formatter ()

kernel/cbytecodes.mli

@@ -132,8 +132,6 @@ type comp_env = {
 
 val draw_instr : bytecodes -> unit
 
-val string_of_instr : bytecodes -> string
-
 
 
 (*spiwack: moved this here because I needed it for retroknowledge *)

kernel/cbytegen.ml

@@ -335,7 +335,7 @@ let rec str_const c =
   | App(f,args) -> 
       begin
 	match kind_of_term f with
-	| Construct(((kn,j),i) as cstr) -> 
+	| Construct((kn,j),i) -> (* arnaud: Construct(((kn,j),i) as cstr) -> *)
             begin
 	    let oib = lookup_mind kn !global_env in
 	    let oip = oib.mind_packets.(j) in
@@ -405,7 +405,7 @@ let rec str_const c =
 	| _ -> Bconstr c
       end
   | Ind ind -> Bstrconst (Const_ind ind)
-  | Construct ((kn,j),i as cstr) ->  
+  | Construct ((kn,j),i) ->  (*arnaud: Construct ((kn,j),i as cstr) ->  *)
       begin
       (* spiwack: tries first to apply the run-time compilation 
            behavior of the constructor, as in 2/ above *)
@@ -664,19 +664,19 @@ and compile_str_cst reloc sc sz cont =
 (* spiwack : compilation of constants with their arguments. 
    Makes a special treatment with 31-bit integer addition *)
 and compile_const =
-  let code_construct kn cont = 
+(*arnaud:  let code_construct kn cont = 
      let f_cont = 
          let else_lbl = Label.create () in
          Kareconst(2, else_lbl):: Kacc 0:: Kpop 1::
           Kaddint31:: Kreturn 0:: Klabel else_lbl::
          (* works as comp_app with nargs = 2 and tailcall cont [Kreturn 0]*)
           Kgetglobal (get_allias !global_env kn)::
           Kappterm(2, 2):: [] (* = discard_dead_code [Kreturn 0] *)
-     in
+     in 
      let lbl = Label.create () in 
      fun_code := [Ksequence (add_grab 2 lbl f_cont, !fun_code)];
      Kclosure(lbl, 0)::cont
-  in
+  in *)
   fun reloc-> fun  kn -> fun args -> fun sz -> fun cont ->
   let nargs = Array.length args in
   (* spiwack: checks if there is a specific way to compile the constant

kernel/cbytegen.mli

@@ -14,7 +14,6 @@ val compile_constant_body :
                                  (* opaque *) (* boxed *)
 
 
-(* arnaud : a commenter *)
 (* spiwack: this function contains the information needed to perform
             the static compilation of int31 (trying and obtaining
             a 31-bit integer in processor representation at compile time) *)

kernel/names.ml

@@ -330,43 +330,3 @@ type inv_rel_key = int (* index in the [rel_context] part of environment
 
 type id_key = inv_rel_key tableKey
 
-
-
-(* spiwack : internal representation printing *)
-
-let string_of_identifier id = id
-let string_of_module_ident id = id
-let string_of_label lbl = lbl (* not public *)
-let string_of_dir_path path = "["^String.concat "; " (List.map string_of_module_ident path)^"]"
-let string_of_name =
-  function
-  | Name id -> "Name "^id
-  | Anonymous -> "Anonymous"
-
-let rec string_of_module_path = (* not public *)
-  function
-  | MPfile path -> "MPfile "^string_of_dir_path path
-  | MPbound _ -> "MPbound "^"?" (*of mod_bound_id*)
-  | MPself _ -> "MPself "^"?" (* of mod_self_id *)
-  | MPdot (mpath, lbl) -> 
-         "MPdot ("^string_of_module_path mpath^", "^string_of_label lbl^")"
-          (* of module_path * label *)
-
-let string_of_kernel_name = (* not public *)
-   function
-   |(mpath, path, lbl) -> 
-         "("^string_of_module_path mpath^", "^
-             string_of_dir_path path^", "^
-             string_of_label lbl ^")"
-
-let string_of_constant = string_of_kernel_name
-let string_of_mutual_inductive = string_of_kernel_name
-let string_of_inductive = 
-   function
-   | (mind, i) -> "("^string_of_mutual_inductive mind^", "^string_of_int i^")"
-let string_of_constructor =
-   function
-   | (ind, i) -> "("^string_of_inductive ind^", "^string_of_int i^")"
-
-
-(* /spiwack *)

kernel/names.mli

@@ -174,15 +174,3 @@ type inv_rel_key = int (* index in the [rel_context] part of environment
 			  of de Bruijn indice *)
 
 type id_key = inv_rel_key tableKey
-
-
-
-(* spiwack : function used for printing identifiers *)
-val string_of_identifier : identifier-> string
-val string_of_module_ident : module_ident-> string
-val string_of_dir_path : dir_path -> string
-val string_of_name : name -> string
-val string_of_constant : constant -> string
-val string_of_mutual_inductive : mutual_inductive -> string
-val string_of_inductive : inductive -> string
-val string_of_constructor : constructor -> string

kernel/term.ml

@@ -1177,52 +1177,3 @@ let (hcons1_constr, hcons1_types) = hcons_constr (hcons_names())
 (*******)
 (* Type of abstract machine values *)
 type values
-
-
-
-(* spiwack : internal representation printing *)
-let string_of_sorts =
-  function 
-  | Prop Pos -> "Prop Pos"
-  | Prop Null -> "Prop Null"
-  | Type u -> "Type "^string_of_universe u
-
-let string_of_cast_kind = 
-  function
-  |VMcast -> "VMcast"
-  | DEFAULTcast -> "DEFAULTcast"
-
-let rec string_of_constr = 
-  let string_of_term string_of_expr string_of_type = function
-  | Rel i -> "Rel "^string_of_int i
-  | Var id -> "Var "^string_of_identifier id
-  | Meta mv -> "Meta "^"mv?" (* need a function for printing metavariables *)
-  | Evar ev -> "Evar "^"ev?" (* ??     of 'constr pexistential *)
-  | Sort s -> "Sort "^string_of_sorts s
-  | Cast (e,ck,t) -> 
-         "Cast ("^string_of_expr e^", "^string_of_cast_kind ck^", "^
-                 string_of_type t^")" 
-  | Prod (n, t1, t2) -> 
-          "Prod ("^string_of_name n^", "^string_of_type t1^", "^
-                   string_of_type t2^")"  
-  | Lambda (n,t,e) ->
-          "Lambda ("^string_of_name n^", "^string_of_type t^", "^
-                    string_of_expr e^")"
-  | LetIn (n, e1, t, e2) -> 
-           "LetIn ("^string_of_name n^", "^string_of_expr e1^", "^
-           string_of_type t^", "^string_of_expr e2^")"
-  | App   (e, args) ->  "App ("^string_of_expr e^", [|"^
-          String.concat "; " (Array.to_list (Array.map string_of_expr args)) ^
-          "|])"
-  | Const c ->  "Const "^string_of_constant c
-  | Ind   ind ->  "Ind "^string_of_inductive ind
-  | Construct ctr -> "Construct "^string_of_constructor ctr
-  | Case(_,_,_,_)  -> "Case ..."    
-             (*    of case_info * 'constr * 'constr * 'constr array   *)
-  | Fix _  -> "Fix ..."  (*    of ('constr, 'types) pfixpoint *)
-  | CoFix _ -> "CoFix ..."  (*     of ('constr, 'types) pcofixpoint *)
-in 
-fun x -> string_of_term string_of_constr string_of_constr x
-
-
-(* /spiwack *)

kernel/term.mli

@@ -543,9 +543,3 @@ val hcons1_types : types -> types
 (**************************************)
 
 type values
-
-
-(*************************************************************)
-
-(* spiwack: printing of internal representation of constr *)
-val string_of_constr : constr -> string

kernel/univ.ml

@@ -578,17 +578,3 @@ let hcons1_univ u =
   let _,_,hdir,_,_,_ = Names.hcons_names() in
   Hashcons.simple_hcons Huniv.f hdir u
 
-
-
-(* spiwack: function for internal representation printing *)
-let string_of_universe =
-  let string_of_universe_level = function
-  | Base -> "Base"
-  | Level (path,i) -> "Level ("^Names.string_of_dir_path path^", "^string_of_int i^")"
-in
-function 
-  | Atom u -> "Atom "^string_of_universe_level u
-  | Max (l1,l2) -> "Max (["^
-               String.concat "; " (List.map string_of_universe_level l1)^"], ["^
-               String.concat "; " (List.map string_of_universe_level l2)
-               ^"])"

kernel/univ.mli

@@ -79,7 +79,3 @@ val pr_universes : universes -> Pp.std_ppcmds
 val dump_universes : out_channel -> universes -> unit
 
 val hcons1_univ : universe -> universe
-
-
-(* spiwack: function for internal representation printing *)
-val string_of_universe : universe -> string

parsing/printer.ml

@@ -486,7 +486,7 @@ let pr_assumptionset env s =
       str "Section Variables:" ++
       (Environ.AssumptionSet.fold 
          (function Variable (id,typ ) -> 
-	    (fun b -> b++str (string_of_identifier id)
+	    (fun b -> b++str (string_of_id id)
 	               ++str " : "
 	               ++pr_ltype typ
 	               ++fnl ())

pretyping/vnorm.ml

@@ -52,42 +52,7 @@ let type_constructor mind mib typ params =
     let _,ctyp = decompose_prod_n nparams ctyp in   
     substl (List.rev (Array.to_list params)) ctyp
 
-(* arnaud: to clean 
-(* spiwack: auxiliary fonction for decompiling 31-bit integers
-   into their corresponding constr *)
-let constr_of_int31 =
-  let nth_digit_plus_one i n = (* calculates the nth (starting with 0)
-                                  digit of i and adds 1 to it 
-                                  (nth_digit_plus_one 1 3 = 2) *)
-      if (land) i ((lsl) 1 n) = 0 then
-         1
-      else
-         2
-  in
-  fun tag -> fun ind->
-  let digit_ind = Retroknowledge.digits_of_int31 ind 
-  in
-  let array_of_int i =
-    Array.init 31 (fun n -> mkConstruct(digit_ind, nth_digit_plus_one i (30-n)))
-  in
-    mkApp(mkConstruct(ind, 1), array_of_int tag) *)
 
-(* /spiwack *)
-(* arnaud
-let construct_of_constr_const env tag typ =
-  let ind,params = find_rectype env typ in
-  (* arnaud:improve comment ? *)
-  (* spiwack: branching for 31-bits integers *)
-(* arnaud:
-  if Retroknowledge.isInt31t ind then
-    constr_of_int31 tag ind
-  else *)
-  try 
-    retroknowledge Retroknowledge.get_vm_decompile_constant_info env (Ind ind) tag
-  with Not_found ->
-    let (_,mip) = lookup_mind_specif env ind in
-    let i = invert_tag true tag mip.mind_reloc_tbl in
-    applistc (mkConstruct(ind,i))  params *)
 
 let construct_of_constr const env tag typ =
   let (mind,_ as ind), allargs = find_rectype_a env typ in

tactics/extratactics.ml4

@@ -413,23 +413,6 @@ VERNAC COMMAND EXTEND RetroknowledgeRegister
              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

toplevel/auto_ind_decl.ml

@@ -331,9 +331,18 @@ let do_replace_lb aavoid narg gls p q =
     let u,v = destruct_ind type_of_pq
     in let lb_type_of_p = 
         try find_lb_proof u 
-        with Not_found -> error 
-          ("Leibniz->boolean:You have to declare the decidability over "^
-          (string_of_constr type_of_pq)^" first.")
+        with Not_found -> 
+          (* spiwack: the format of this error message should probably
+	              be improved. *)
+          let err_msg = msg_with Format.str_formatter 
+	                              (str "Leibniz->boolean:" ++
+                                       str "You have to declare the" ++ 
+				       str "decidability over " ++
+				       Printer.pr_constr type_of_pq ++ 
+				       str " first.");
+	                Format.flush_str_formatter ()
+          in
+          error err_msg
     in let lb_args = Array.append (Array.append 
                           (Array.map (fun x -> x) v)
                           (Array.map (fun x -> do_arg x 1) v))
@@ -381,9 +390,18 @@ let do_replace_bl ind gls aavoid narg lft rgt =
              else (
                let bl_t1 = 
                try find_bl_proof u 
-               with Not_found -> error 
-                 ("boolean->Leibniz:You have to declare the decidability over "^
-                 (string_of_constr tt1)^" first.")
+               with Not_found -> 
+		 (* spiwack: the format of this error message should probably
+	                     be improved. *)
+		 let err_msg = msg_with Format.str_formatter 
+	                                (str "boolean->Leibniz:" ++
+                                         str "You have to declare the" ++ 
+			   	         str "decidability over " ++
+				         Printer.pr_constr tt1 ++ 
+				         str " first.");
+ 	                       Format.flush_str_formatter ()
+		 in
+		 error err_msg
                in let bl_args = 
                         Array.append (Array.append 
                           (Array.map (fun x -> x) v)