aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/cbytecodes.ml4
-rw-r--r--kernel/cbytecodes.mli2
-rw-r--r--kernel/cbytegen.ml10
-rw-r--r--kernel/cbytegen.mli1
-rw-r--r--kernel/names.ml40
-rw-r--r--kernel/names.mli12
-rw-r--r--kernel/term.ml49
-rw-r--r--kernel/term.mli6
-rw-r--r--kernel/univ.ml14
-rw-r--r--kernel/univ.mli4
-rw-r--r--parsing/printer.ml2
-rw-r--r--pretyping/vnorm.ml35
-rw-r--r--tactics/extratactics.ml417
-rw-r--r--toplevel/auto_ind_decl.ml30
14 files changed, 30 insertions, 196 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 84d04d67e..ceba6e82a 100644
--- a/kernel/cbytecodes.ml
+++ b/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 ()
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 86b465543..c24b5a530 100644
--- a/kernel/cbytecodes.mli
+++ b/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 *)
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 2664abe1f..721134252 100644
--- a/kernel/cbytegen.ml
+++ b/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,7 +664,7 @@ 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::
@@ -672,11 +672,11 @@ and compile_const =
(* 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
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 829ac46e2..dfdcb0747 100644
--- a/kernel/cbytegen.mli
+++ b/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) *)
diff --git a/kernel/names.ml b/kernel/names.ml
index c153169ab..46a44a9b2 100644
--- a/kernel/names.ml
+++ b/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 *)
diff --git a/kernel/names.mli b/kernel/names.mli
index dee798da0..64edf1702 100644
--- a/kernel/names.mli
+++ b/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
diff --git a/kernel/term.ml b/kernel/term.ml
index b09bd4aea..ad4bd2bda 100644
--- a/kernel/term.ml
+++ b/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 *)
diff --git a/kernel/term.mli b/kernel/term.mli
index b0387417c..b5304b651 100644
--- a/kernel/term.mli
+++ b/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
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 7a7e0bb5a..a127fd5c0 100644
--- a/kernel/univ.ml
+++ b/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)
- ^"])"
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 6c709bc83..52af808e3 100644
--- a/kernel/univ.mli
+++ b/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
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 6bd11af9f..218ba4150 100644
--- a/parsing/printer.ml
+++ b/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 ())
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 8103bdafb..c746e4199 100644
--- a/pretyping/vnorm.ml
+++ b/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
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ef6ac60f4..0fff16cf9 100644
--- a/tactics/extratactics.ml4
+++ b/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
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 89569453a..b7e1900b1 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/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)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 10:13:27 +0000