aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/check.ml26
-rw-r--r--checker/cic.mli10
-rw-r--r--checker/values.ml7
-rw-r--r--checker/votour.ml1
-rw-r--r--kernel/cbytecodes.ml178
-rw-r--r--kernel/cbytecodes.mli4
-rw-r--r--kernel/cbytegen.ml22
-rw-r--r--kernel/univ.ml25
-rw-r--r--lib/flags.ml4
-rw-r--r--lib/flags.mli9
-rw-r--r--library/library.ml65
-rw-r--r--library/library.mli5
-rw-r--r--printing/ppconstr.ml8
-rw-r--r--proofs/pfedit.ml2
-rw-r--r--stm/vio_checking.ml4
-rw-r--r--tactics/rewrite.ml206
-rw-r--r--tactics/tacintern.ml12
-rw-r--r--tactics/tacinterp.ml14
-rw-r--r--test-suite/success/simpl.v7
-rw-r--r--toplevel/coqtop.ml30
-rw-r--r--toplevel/obligations.ml27
-rw-r--r--toplevel/usage.ml8
-rw-r--r--toplevel/vernac.ml4
-rw-r--r--toplevel/vernacentries.ml8
24 files changed, 419 insertions, 267 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 3e22c4b18..c835cec82 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -291,12 +291,12 @@ let with_magic_number_check f a =
open Cic
-let mk_library md f table digest cst = {
- library_name = md.md_name;
+let mk_library sd md f table digest cst = {
+ library_name = sd.md_name;
library_filename = f;
library_compiled = md.md_compiled;
library_opaques = table;
- library_deps = md.md_deps;
+ library_deps = sd.md_deps;
library_digest = digest;
library_extra_univs = cst }
@@ -310,10 +310,11 @@ let depgraph = ref LibraryMap.empty
let intern_from_file (dir, f) =
Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush ();
- let (md,table,opaque_csts,digest) =
+ let (sd,md,table,opaque_csts,digest) =
try
let ch = with_magic_number_check raw_intern_library f in
- let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in
+ let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in
+ let (md:Cic.library_disk), _, _ = System.marshal_in_segment f ch in
let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in
let (discharging:'a option), _, _ = System.marshal_in_segment f ch in
let (tasks:'a option), _, _ = System.marshal_in_segment f ch in
@@ -325,9 +326,9 @@ let intern_from_file (dir, f) =
if not (String.equal (Digest.channel ch pos) checksum) then
errorlabstrm "intern_from_file" (str "Checksum mismatch");
let () = close_in ch in
- if dir <> md.md_name then
+ if dir <> sd.md_name then
errorlabstrm "intern_from_file"
- (name_clash_message dir md.md_name f);
+ (name_clash_message dir sd.md_name f);
if tasks <> None || discharging <> None then
errorlabstrm "intern_from_file"
(str "The file "++str f++str " contains unfinished tasks");
@@ -340,25 +341,26 @@ let intern_from_file (dir, f) =
Validate.validate !Flags.debug Values.v_univopaques opaque_csts;
end;
(* Verification of the unmarshalled values *)
+ Validate.validate !Flags.debug Values.v_libsum sd;
Validate.validate !Flags.debug Values.v_lib md;
Validate.validate !Flags.debug Values.v_opaques table;
Flags.if_verbose ppnl (str" done]"); pp_flush ();
let digest =
if opaque_csts <> None then Cic.Dviovo (digest,udg)
else (Cic.Dvo digest) in
- md,table,opaque_csts,digest
+ sd,md,table,opaque_csts,digest
with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in
- depgraph := LibraryMap.add md.md_name md.md_deps !depgraph;
- opaque_tables := LibraryMap.add md.md_name table !opaque_tables;
+ depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph;
+ opaque_tables := LibraryMap.add sd.md_name table !opaque_tables;
Option.iter (fun (opaque_csts,_,_) ->
opaque_univ_tables :=
- LibraryMap.add md.md_name opaque_csts !opaque_univ_tables)
+ LibraryMap.add sd.md_name opaque_csts !opaque_univ_tables)
opaque_csts;
let extra_cst =
Option.default Univ.empty_constraint
(Option.map (fun (_,cs,_) ->
Univ.ContextSet.constraints cs) opaque_csts) in
- mk_library md f table digest extra_cst
+ mk_library sd md f table digest extra_cst
let get_deps (dir, f) =
try LibraryMap.find dir !depgraph
diff --git a/checker/cic.mli b/checker/cic.mli
index 90a0e9feb..e875e40f0 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -417,12 +417,16 @@ type compiled_library = {
type library_objects
-type library_disk = {
+type summary_disk = {
md_name : compilation_unit_name;
+ md_imports : compilation_unit_name array;
+ md_deps : library_deps;
+}
+
+type library_disk = {
md_compiled : compiled_library;
md_objects : library_objects;
- md_deps : library_deps;
- md_imports : compilation_unit_name array }
+}
type opaque_table = constr Future.computation array
type univ_table =
diff --git a/checker/values.ml b/checker/values.ml
index cf93466b0..b2d74821d 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 0a174243f8b06535c9eecbbe8d339fe1 checker/cic.mli
+MD5 f5fd749af797e08efee22122742bc740 checker/cic.mli
*)
@@ -350,8 +350,11 @@ let v_stm_seg = v_pair v_tasks v_counters
(** Toplevel structures in a vo (see Cic.mli) *)
+let v_libsum =
+ Tuple ("summary", [|v_dp;Array v_dp;v_deps|])
+
let v_lib =
- Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps;Array v_dp|])
+ Tuple ("library",[|v_compiled_lib;v_libraryobjs|])
let v_opaques = Array (v_computation v_constr)
let v_univopaques =
diff --git a/checker/votour.ml b/checker/votour.ml
index 01965bb4b..bb8e06702 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -249,6 +249,7 @@ let visit_vo f =
Printf.printf
"At prompt, <n> enters the <n>-th child, u goes up 1 level, x exits\n\n%!";
let segments = [|
+ make_seg "summary" Values.v_libsum;
make_seg "library" Values.v_lib;
make_seg "univ constraints of opaque proofs" Values.v_univopaques;
make_seg "discharging info" (Opt Any);
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 700de5020..93fd61f02 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -155,92 +155,117 @@ type comp_env = {
(* --- Pretty print *)
-open Format
-let rec instruction ppf = function
- | Klabel lbl -> fprintf ppf "L%i:" lbl
- | Kacc n -> fprintf ppf "\tacc %i" n
- | Kenvacc n -> fprintf ppf "\tenvacc %i" n
- | Koffsetclosure n -> fprintf ppf "\toffsetclosure %i" n
- | Kpush -> fprintf ppf "\tpush"
- | Kpop n -> fprintf ppf "\tpop %i" n
- | Kpush_retaddr lbl -> fprintf ppf "\tpush_retaddr L%i" lbl
- | Kapply n -> fprintf ppf "\tapply %i" n
+open Pp
+open Util
+
+let pp_sort s =
+ match family_of_sort s with
+ | InSet -> str "Set"
+ | InProp -> str "Prop"
+ | InType -> str "Type"
+
+let rec pp_struct_const = function
+ | Const_sorts s -> pp_sort s
+ | Const_ind ((mind, i), u) -> pr_mind mind ++ str"#" ++ int i
+ | Const_b0 i -> int i
+ | Const_bn (i,t) ->
+ int i ++ surround (prvect_with_sep pr_comma pp_struct_const t)
+
+let pp_lbl lbl = str "L" ++ int lbl
+
+let rec pp_instr i =
+ match i with
+ | Klabel _ | Ksequence _ -> assert false
+ | Kacc n -> str "acc " ++ int n
+ | Kenvacc n -> str "envacc " ++ int n
+ | Koffsetclosure n -> str "offsetclosure " ++ int n
+ | Kpush -> str "push"
+ | Kpop n -> str "pop " ++ int n
+ | Kpush_retaddr lbl -> str "push_retaddr " ++ pp_lbl lbl
+ | Kapply n -> str "apply " ++ int n
| Kappterm(n, m) ->
- fprintf ppf "\tappterm %i, %i" n m
- | Kreturn n -> fprintf ppf "\treturn %i" n
- | Kjump -> fprintf ppf "\tjump"
- | Krestart -> fprintf ppf "\trestart"
- | Kgrab n -> fprintf ppf "\tgrab %i" n
- | Kgrabrec n -> fprintf ppf "\tgrabrec %i" n
+ str "appterm " ++ int n ++ str ", " ++ int m
+ | Kreturn n -> str "return " ++ int n
+ | Kjump -> str "jump"
+ | Krestart -> str "restart"
+ | Kgrab n -> str "grab " ++ int n
+ | Kgrabrec n -> str "grabrec " ++ int n
| Kclosure(lbl, n) ->
- fprintf ppf "\tclosure L%i, %i" lbl n
+ str "closure " ++ pp_lbl lbl ++ str ", " ++ int n
| Kclosurerec(fv,init,lblt,lblb) ->
- fprintf ppf "\tclosurerec";
- fprintf ppf "%i , %i, " fv init;
- print_string "types = ";
- Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
- print_string " bodies = ";
- Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
+ h 1 (str "closurerec " ++
+ int fv ++ str ", " ++ int init ++
+ str " types = " ++
+ prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
+ str " bodies = " ++
+ prlist_with_sep spc pp_lbl (Array.to_list lblb))
| Kclosurecofix (fv,init,lblt,lblb) ->
- fprintf ppf "\tclosurecofix";
- fprintf ppf " %i , %i, " fv init;
- print_string "types = ";
- Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
- print_string " bodies = ";
- Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
- | Kgetglobal (id,u) -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id)
- | Kconst cst ->
- fprintf ppf "\tconst"
+ h 1 (str "closurecofix " ++
+ int fv ++ str ", " ++ int init ++
+ str " types = " ++
+ prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
+ str " bodies = " ++
+ prlist_with_sep spc pp_lbl (Array.to_list lblb))
+ | Kgetglobal (id,u) -> str "getglobal " ++ pr_con id
+ | Kconst sc ->
+ str "const " ++ pp_struct_const sc
| Kmakeblock(n, m) ->
- fprintf ppf "\tmakeblock %i, %i" n m
- | Kmakeprod -> fprintf ppf "\tmakeprod"
+ str "makeblock " ++ int n ++ str ", " ++ int m
+ | Kmakeprod -> str "makeprod"
| Kmakeswitchblock(lblt,lbls,_,sz) ->
- fprintf ppf "\tmakeswitchblock %i, %i, %i" lblt lbls sz
+ str "makeswitchblock " ++ pp_lbl lblt ++ str ", " ++
+ pp_lbl lbls ++ str ", " ++ int sz
| Kswitch(lblc,lblb) ->
- fprintf ppf "\tswitch";
- Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblc;
- Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
- | Kpushfields n -> fprintf ppf "\tpushfields %i" n
- | Ksetfield n -> fprintf ppf "\tsetfield %i" n
- | Kfield n -> fprintf ppf "\tgetfield %i" n
- | Kstop -> fprintf ppf "\tstop"
- | Ksequence (c1,c2) ->
- fprintf ppf "%a@ %a" instruction_list c1 instruction_list c2
-(* spiwack *)
- | Kbranch lbl -> fprintf ppf "\tbranch %i" lbl
- | Kaddint31 -> fprintf ppf "\taddint31"
- | Kaddcint31 -> fprintf ppf "\taddcint31"
- | Kaddcarrycint31 -> fprintf ppf "\taddcarrycint31"
- | Ksubint31 -> fprintf ppf "\tsubint31"
- | Ksubcint31 -> fprintf ppf "\tsubcint31"
- | Ksubcarrycint31 -> fprintf ppf "\tsubcarrycint31"
- | Kmulint31 -> fprintf ppf "\tmulint31"
- | Kmulcint31 -> fprintf ppf "\tmulcint31"
- | Kdiv21int31 -> fprintf ppf "\tdiv21int31"
- | Kdivint31 -> fprintf ppf "\tdivint31"
- | Kcompareint31 -> fprintf ppf "\tcompareint31"
- | Khead0int31 -> fprintf ppf "\thead0int31"
- | Ktail0int31 -> fprintf ppf "\ttail0int31"
- | Kaddmuldivint31 -> fprintf ppf "\taddmuldivint31"
- | Kisconst lbl -> fprintf ppf "\tisconst %i" lbl
- | Kareconst(n,lbl) -> fprintf ppf "\tareconst %i %i" n lbl
- | Kcompint31 -> fprintf ppf "\tcompint31"
- | Kdecompint31 -> fprintf ppf "\tdecompint"
- | Klorint31 -> fprintf ppf "\tlorint31"
- | Klandint31 -> fprintf ppf "\tlandint31"
- | Klxorint31 -> fprintf ppf "\tlxorint31"
+ h 1 (str "switch " ++
+ prlist_with_sep spc pp_lbl (Array.to_list lblc) ++
+ str " | " ++
+ prlist_with_sep spc pp_lbl (Array.to_list lblb))
+ | Kpushfields n -> str "pushfields " ++ int n
+ | Kfield n -> str "field " ++ int n
+ | Ksetfield n -> str "set field" ++ int n
-(* /spiwack *)
+ | Kstop -> str "stop"
+ | Kbranch lbl -> str "branch " ++ pp_lbl lbl
-and instruction_list ppf = function
- [] -> ()
- | Klabel lbl :: il ->
- fprintf ppf "L%i:%a" lbl instruction_list il
- | instr :: il ->
- fprintf ppf "%a@ %a" instruction instr instruction_list il
+ | Kaddint31 -> str "addint31"
+ | Kaddcint31 -> str "addcint31"
+ | Kaddcarrycint31 -> str "addcarrycint31"
+ | Ksubint31 -> str "subint31"
+ | Ksubcint31 -> str "subcint31"
+ | Ksubcarrycint31 -> str "subcarrycint31"
+ | Kmulint31 -> str "mulint31"
+ | Kmulcint31 -> str "mulcint31"
+ | Kdiv21int31 -> str "div21int31"
+ | Kdivint31 -> str "divint31"
+ | Kcompareint31 -> str "compareint31"
+ | Khead0int31 -> str "head0int31"
+ | Ktail0int31 -> str "tail0int31"
+ | Kaddmuldivint31 -> str "addmuldivint31"
+ | Kisconst lbl -> str "isconst " ++ int lbl
+ | Kareconst(n,lbl) -> str "areconst " ++ int n ++ spc () ++ int lbl
+ | Kcompint31 -> str "compint31"
+ | Kdecompint31 -> str "decompint"
+ | Klorint31 -> str "lorint31"
+ | Klandint31 -> str "landint31"
+ | Klxorint31 -> str "lxorint31"
+and pp_bytecodes c =
+ match c with
+ | [] -> str ""
+ | Klabel lbl :: c ->
+ str "L" ++ int lbl ++ str ":" ++ str "\n" ++
+ pp_bytecodes c
+ | Ksequence (l1, l2) :: c ->
+ pp_bytecodes l1 ++ pp_bytecodes l2 ++ pp_bytecodes c
+ | i :: c ->
+ str "\t" ++ pp_instr i ++ str "\n" ++ pp_bytecodes c
+
+let dump_bytecode c =
+ pperrnl (pp_bytecodes c);
+ flush_all()
+
(*spiwack: moved this type in this file because I needed it for
retroknowledge which can't depend from cbytegen *)
type block =
@@ -253,8 +278,3 @@ type block =
(* spiwack: compilation given by a function *)
(* compilation function (see get_vm_constant_dynamic_info in
retroknowledge.mli for more info) , argument array *)
-
-
-
-let draw_instr c =
- fprintf std_formatter "@[<v 0>%a@]" instruction_list c
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index fbb40ffd1..d9998c89e 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -143,9 +143,7 @@ type comp_env = {
in_env : vm_env ref
}
-val draw_instr : bytecodes -> unit
-
-
+val dump_bytecode : bytecodes -> unit
(*spiwack: moved this here because I needed it for retroknowledge *)
type block =
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 07fab06a4..ac46dc583 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -772,16 +772,18 @@ let compile fail_on_error env c =
try
let init_code = compile_constr reloc c 0 [Kstop] in
let fv = List.rev (!(reloc.in_env).fv_rev) in
-(* draw_instr init_code;
- draw_instr !fun_code;
- Format.print_string "fv = ";
- List.iter (fun v ->
- match v with
- | FVnamed id -> Format.print_string ((Id.to_string id)^"; ")
- | FVrel i -> Format.print_string ((string_of_int i)^"; ")) fv; Format
- .print_string "\n";
- Format.print_flush(); *)
- Some (init_code,!fun_code, Array.of_list fv)
+ let pp_v v =
+ match v with
+ | FVnamed id -> Pp.str (Id.to_string id)
+ | FVrel i -> Pp.str (string_of_int i)
+ in
+ let open Pp in
+ if !Flags.dump_bytecode then
+ (dump_bytecode init_code;
+ dump_bytecode !fun_code;
+ Pp.msg_debug (Pp.str "fv = " ++
+ Pp.prlist_with_sep (fun () -> Pp.str "; ") pp_v fv ++ Pp.fnl ()));
+ Some (init_code,!fun_code, Array.of_list fv)
with TooLargeInductive tname ->
let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in
(Pp.(fn
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 763c0822f..4af7fe7c1 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -723,29 +723,26 @@ let enter_arc ca g =
(* repr : universes -> Level.t -> canonical_arc *)
(* canonical representative : we follow the Equiv links *)
-let repr g u =
- let rec repr_rec u =
- let a =
- try UMap.find u g
- with Not_found -> anomaly ~label:"Univ.repr"
- (str"Universe " ++ Level.pr u ++ str" undefined")
- in
- match a with
- | Equiv v -> repr_rec v
- | Canonical arc -> arc
+let rec repr g u =
+ let a =
+ try UMap.find u g
+ with Not_found -> anomaly ~label:"Univ.repr"
+ (str"Universe " ++ Level.pr u ++ str" undefined")
in
- repr_rec u
+ match a with
+ | Equiv v -> repr g v
+ | Canonical arc -> arc
(* [safe_repr] also search for the canonical representative, but
if the graph doesn't contain the searched universe, we add it. *)
let safe_repr g u =
- let rec safe_repr_rec u =
+ let rec safe_repr_rec g u =
match UMap.find u g with
- | Equiv v -> safe_repr_rec v
+ | Equiv v -> safe_repr_rec g v
| Canonical arc -> arc
in
- try g, safe_repr_rec u
+ try g, safe_repr_rec g u
with Not_found ->
let can = terminal u in
enter_arc can g, can
diff --git a/lib/flags.ml b/lib/flags.ml
index fe580b7ff..9a0d4b5ec 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -215,3 +215,7 @@ let native_compiler = ref false
let print_mod_uid = ref false
let tactic_context_compat = ref false
+
+let dump_bytecode = ref false
+let set_dump_bytecode = (:=) dump_bytecode
+let get_dump_bytecode () = !dump_bytecode
diff --git a/lib/flags.mli b/lib/flags.mli
index bdb8159ad..29a0bbef0 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -130,12 +130,17 @@ val set_inline_level : int -> unit
val get_inline_level : unit -> int
val default_inline_level : int
-(* Native code compilation for conversion and normalization *)
+(** Native code compilation for conversion and normalization *)
val native_compiler : bool ref
-(* Print the mod uid associated to a vo file by the native compiler *)
+(** Print the mod uid associated to a vo file by the native compiler *)
val print_mod_uid : bool ref
val tactic_context_compat : bool ref
(** Set to [true] to trigger the compatibility bugged context matching (old
context vs. appcontext) is set. *)
+
+(** Dump the bytecode after compilation (for debugging purposes) *)
+val dump_bytecode : bool ref
+val set_dump_bytecode : bool -> unit
+val get_dump_bytecode : unit -> bool
diff --git a/library/library.ml b/library/library.ml
index 0296d7b90..a8fbe0841 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -76,19 +76,22 @@ open Delayed
type compilation_unit_name = DirPath.t
type library_disk = {
- md_name : compilation_unit_name;
md_compiled : Safe_typing.compiled_library;
md_objects : Declaremods.library_objects;
+}
+
+type summary_disk = {
+ md_name : compilation_unit_name;
+ md_imports : compilation_unit_name array;
md_deps : (compilation_unit_name * Safe_typing.vodigest) array;
- md_imports : compilation_unit_name array }
+}
(*s Modules loaded in memory contain the following informations. They are
kept in the global table [libraries_table]. *)
type library_t = {
library_name : compilation_unit_name;
- library_compiled : Safe_typing.compiled_library;
- library_objects : Declaremods.library_objects;
+ library_data : library_disk delayed;
library_deps : (compilation_unit_name * Safe_typing.vodigest) array;
library_imports : compilation_unit_name array;
library_digests : Safe_typing.vodigest;
@@ -406,19 +409,19 @@ let () =
(************************************************************************)
(* Internalise libraries *)
+type seg_sum = summary_disk
type seg_lib = library_disk
type seg_univ = (* true = vivo, false = vi *)
Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool
type seg_discharge = Opaqueproof.cooking_info list array
type seg_proofs = Term.constr Future.computation array
-let mk_library md digests univs =
+let mk_library sd md digests univs =
{
- library_name = md.md_name;
- library_compiled = md.md_compiled;
- library_objects = md.md_objects;
- library_deps = md.md_deps;
- library_imports = md.md_imports;
+ library_name = sd.md_name;
+ library_data = md;
+ library_deps = sd.md_deps;
+ library_imports = sd.md_imports;
library_digests = digests;
library_extra_univs = univs;
}
@@ -431,23 +434,24 @@ let mk_summary m = {
let intern_from_file f =
let ch = System.with_magic_number_check raw_intern_library f in
- let (lmd : seg_lib), pos, digest_lmd = System.marshal_in_segment f ch in
+ let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in
+ let (lmd : seg_lib delayed) = in_delayed f ch in
let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in
let _ = System.skip_in_segment f ch in
let _ = System.skip_in_segment f ch in
let (del_opaque : seg_proofs delayed) = in_delayed f ch in
close_in ch;
- register_library_filename lmd.md_name f;
- add_opaque_table lmd.md_name (ToFetch del_opaque);
+ register_library_filename lsd.md_name f;
+ add_opaque_table lsd.md_name (ToFetch del_opaque);
let open Safe_typing in
match univs with
- | None -> mk_library lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
+ | None -> mk_library lsd lmd (Dvo_or_vi digest_lsd) Univ.ContextSet.empty
| Some (utab,uall,true) ->
- add_univ_table lmd.md_name (Fetched utab);
- mk_library lmd (Dvivo (digest_lmd,digest_u)) uall
+ add_univ_table lsd.md_name (Fetched utab);
+ mk_library lsd lmd (Dvivo (digest_lsd,digest_u)) uall
| Some (utab,_,false) ->
- add_univ_table lmd.md_name (Fetched utab);
- mk_library lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
+ add_univ_table lsd.md_name (Fetched utab);
+ mk_library lsd lmd (Dvo_or_vi digest_lsd) Univ.ContextSet.empty
module DPMap = Map.Make(DirPath)
@@ -510,7 +514,7 @@ let rec_intern_by_filename_only id f =
let native_name_from_filename f =
let ch = System.with_magic_number_check raw_intern_library f in
- let (lmd : seg_lib), pos, digest_lmd = System.marshal_in_segment f ch in
+ let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in
Nativecode.mod_uid_of_dirpath lmd.md_name
let rec_intern_library_from_file idopt f =
@@ -538,10 +542,11 @@ let rec_intern_library_from_file idopt f =
*)
let register_library m =
+ let l = fetch_delayed m.library_data in
Declaremods.register_library
m.library_name
- m.library_compiled
- m.library_objects
+ l.md_compiled
+ l.md_objects
m.library_digests
m.library_extra_univs;
register_loaded_library (mk_summary m)
@@ -695,6 +700,7 @@ let load_library_todo f =
System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
let f = longf^"io" in
let ch = System.with_magic_number_check raw_intern_library f in
+ let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in
let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in
let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in
let (s3 : seg_discharge option), _, _ = System.marshal_in_segment f ch in
@@ -705,7 +711,7 @@ let load_library_todo f =
if s2 = None then errorlabstrm "restart" (str"not a .vio file");
if s3 = None then errorlabstrm "restart" (str"not a .vio file");
if pi3 (Option.get s2) then errorlabstrm "restart" (str"not a .vio file");
- longf, s1, Option.get s2, Option.get s3, Option.get tasks, s5
+ longf, s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5
(************************************************************************)
(*s [save_library dir] ends library [dir] and save it to the disk. *)
@@ -769,18 +775,22 @@ let save_library_to ?todo dir f otab =
if not(is_done_or_todo i x) then Errors.errorlabstrm "library"
Pp.(str"Proof object "++int i++str" is not checked nor to be checked"))
opaque_table;
- let md = {
+ let sd = {
md_name = dir;
+ md_deps = Array.of_list (current_deps ());
+ md_imports = Array.of_list (current_reexports ());
+ } in
+ let md = {
md_compiled = cenv;
md_objects = seg;
- md_deps = Array.of_list (current_deps ());
- md_imports = Array.of_list (current_reexports ()) } in
- if Array.exists (fun (d,_) -> DirPath.equal d dir) md.md_deps then
+ } in
+ if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then
error_recursively_dependent_library dir;
(* Open the vo file and write the magic number *)
let (f',ch) = raw_extern_library f in
try
(* Writing vo payload *)
+ System.marshal_out_segment f' ch (sd : seg_sum);
System.marshal_out_segment f' ch (md : seg_lib);
System.marshal_out_segment f' ch (utab : seg_univ option);
System.marshal_out_segment f' ch (dtab : seg_discharge option);
@@ -799,8 +809,9 @@ let save_library_to ?todo dir f otab =
let () = Sys.remove f' in
iraise reraise
-let save_library_raw f lib univs proofs =
+let save_library_raw f sum lib univs proofs =
let (f',ch) = raw_extern_library (f^"o") in
+ System.marshal_out_segment f' ch (sum : seg_sum);
System.marshal_out_segment f' ch (lib : seg_lib);
System.marshal_out_segment f' ch (Some univs : seg_univ option);
System.marshal_out_segment f' ch (None : seg_discharge option);
diff --git a/library/library.mli b/library/library.mli
index 350670680..967a54e4c 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -28,6 +28,7 @@ val require_library_from_file :
(** {6 ... } *)
(** Segments of a library *)
+type seg_sum
type seg_lib
type seg_univ = (* cst, all_cst, finished? *)
Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool
@@ -47,8 +48,8 @@ val save_library_to :
DirPath.t -> string -> Opaqueproof.opaquetab -> unit
val load_library_todo :
- string -> string * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
-val save_library_raw : string -> seg_lib -> seg_univ -> seg_proofs -> unit
+ string -> string * seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
+val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit
(** {6 Interrogate the status of libraries } *)
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index d9d8af66b..650b8f726 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -676,11 +676,11 @@ end) = struct
return (pr_glob_sort s, latom)
| CCast (_,a,b) ->
return (
- hv 0 (pr mt (lcast,L) a ++ cut () ++
+ hv 0 (pr mt (lcast,L) a ++ spc () ++
match b with
- | CastConv b -> str ":" ++ pr mt (-lcast,E) b
- | CastVM b -> str "<:" ++ pr mt (-lcast,E) b
- | CastNative b -> str "<<:" ++ pr mt (-lcast,E) b
+ | CastConv b -> str ":" ++ ws 1 ++ pr mt (-lcast,E) b
+ | CastVM b -> str "<:" ++ ws 1 ++ pr mt (-lcast,E) b
+ | CastNative b -> str "<<:" ++ ws 1 ++ pr mt (-lcast,E) b
| CastCoerce -> str ":>"),
lcast
)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index d1b6afe22..9c041d72c 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -108,7 +108,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
let () =
match info_lvl with
| None -> ()
- | Some i -> Pp.ppnl (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
+ | Some i -> Pp.msg_notice (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
in
(p,status)
with
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index b20722211..4df9603dc 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -10,7 +10,7 @@ open Util
let check_vio (ts,f) =
Dumpglob.noglob ();
- let long_f_dot_v, _, _, _, tasks, _ = Library.load_library_todo f in
+ let long_f_dot_v, _, _, _, _, tasks, _ = Library.load_library_todo f in
Stm.set_compilation_hints long_f_dot_v;
List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts
@@ -30,7 +30,7 @@ let schedule_vio_checking j fs =
let f =
if Filename.check_suffix f ".vio" then Filename.chop_extension f
else f in
- let long_f_dot_v, _,_,_, tasks, _ = Library.load_library_todo f in
+ let long_f_dot_v, _,_,_,_, tasks, _ = Library.load_library_todo f in
Stm.set_compilation_hints long_f_dot_v;
let infos = Stm.info_tasks tasks in
let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 6d26e91c6..719cc7c98 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -631,13 +631,19 @@ let poly_inverse sort =
type rewrite_proof =
| RewPrf of constr * constr
+ (** A Relation (R : rew_car -> rew_car -> Prop) and a proof of R rew_from rew_to *)
| RewCast of cast_kind
+ (** A proof of convertibility (with casts) *)
type rewrite_result_info = {
- rew_car : constr;
- rew_from : constr;
- rew_to : constr;
- rew_prf : rewrite_proof;
+ rew_car : constr ;
+ (** A type *)
+ rew_from : constr ;
+ (** A term of type rew_car *)
+ rew_to : constr ;
+ (** A term of type rew_car *)
+ rew_prf : rewrite_proof ;
+ (** A proof of rew_from == rew_to *)
rew_evars : evars;
}
@@ -646,9 +652,17 @@ type rewrite_result =
| Identity
| Success of rewrite_result_info
-type 'a pure_strategy = 'a -> Environ.env -> Id.t list -> constr -> types ->
- (bool (* prop *) * constr option) -> evars ->
- 'a * rewrite_result
+type 'a strategy_input = { state : 'a ; (* a parameter: for instance, a state *)
+ env : Environ.env ;
+ unfresh : Id.t list ; (* Unfresh names *)
+ term1 : constr ;
+ ty1 : types ; (* first term and its type (convertible to rew_from) *)
+ cstr : (bool (* prop *) * constr option) ;
+ evars : evars }
+
+type 'a pure_strategy = { strategy :
+ 'a strategy_input ->
+ 'a * rewrite_result (* the updated state and the "result" *) }
type strategy = unit pure_strategy
@@ -820,7 +834,8 @@ let apply_rule unify loccs : int pure_strategy =
then List.mem occ occs
else not (List.mem occ occs)
in
- fun occ env avoid t ty cstr evars ->
+ { strategy = fun { state = occ ; env ; unfresh ;
+ term1 = t ; ty1 = ty ; cstr ; evars } ->
let unif = if isEvar t then None else unify env evars t in
match unif with
| None -> (occ, Fail)
@@ -831,11 +846,12 @@ let apply_rule unify loccs : int pure_strategy =
else
let res = { rew with rew_car = ty } in
let rel, prf = get_rew_prf res in
- let res = Success (apply_constraint env avoid rew.rew_car rel prf cstr res) in
+ let res = Success (apply_constraint env unfresh rew.rew_car rel prf cstr res) in
(occ, res)
+ }
-let apply_lemma l2r flags oc by loccs : strategy =
- fun () env avoid t ty cstr (sigma, cstrs) ->
+let apply_lemma l2r flags oc by loccs : strategy = { strategy =
+ fun ({ state = () ; env ; term1 = t ; evars = (sigma, cstrs) } as input) ->
let sigma, c = oc sigma in
let sigma, hypinfo = decompose_applied_relation env sigma c in
let { c1; c2; car; rel; prf; sort; holes } = hypinfo in
@@ -847,8 +863,11 @@ let apply_lemma l2r flags oc by loccs : strategy =
| None -> None
| Some rew -> Some rew
in
- let _, res = apply_rule unify loccs 0 env avoid t ty cstr evars in
+ let _, res = (apply_rule unify loccs).strategy { input with
+ state = 0 ;
+ evars } in
(), res
+ }
let e_app_poly env evars f args =
let evars', c = app_poly_nocheck env !evars f args in
@@ -928,7 +947,8 @@ let unfold_match env sigma sk app =
let is_rew_cast = function RewCast _ -> true | _ -> false
let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
- let rec aux state env avoid t ty (prop, cstr) evars =
+ let rec aux { state ; env ; unfresh ;
+ term1 = t ; ty1 = ty ; cstr = (prop, cstr) ; evars } =
let cstr' = Option.map (fun c -> (ty, Some c)) cstr in
match kind_of_term t with
| App (m, args) ->
@@ -940,7 +960,11 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
state, (None :: acc, evars, progress)
else
let argty = Retyping.get_type_of env (goalevars evars) arg in
- let state, res = s state env avoid arg argty (prop,None) evars in
+ let state, res = s.strategy { state ; env ;
+ unfresh ;
+ term1 = arg ; ty1 = argty ;
+ cstr = (prop,None) ;
+ evars } in
let res' =
match res with
| Identity ->
@@ -964,7 +988,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| Some r -> not (is_rew_cast r.rew_prf)) args'
then
let evars', prf, car, rel, c1, c2 =
- resolve_morphism env avoid t m args args' (prop, cstr') evars'
+ resolve_morphism env unfresh t m args args' (prop, cstr') evars'
in
let res = { rew_car = ty; rew_from = c1;
rew_to = c2; rew_prf = RewPrf (rel, prf);
@@ -992,7 +1016,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
evars, Some cstr', m, mty, args, Array.of_list args
| None -> evars, None, m, mty, argsl, args
in
- let state, m' = s state env avoid m mty (prop, cstr') evars in
+ let state, m' = s.strategy { state ; env ; unfresh ;
+ term1 = m ; ty1 = mty ;
+ cstr = (prop, cstr') ; evars } in
match m' with
| Fail -> rewrite_args state None (* Standard path, try rewrite on arguments *)
| Identity -> rewrite_args state (Some false)
@@ -1015,7 +1041,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let res =
match prf with
| RewPrf (rel, prf) ->
- Success (apply_constraint env avoid res.rew_car
+ Success (apply_constraint env unfresh res.rew_car
rel prf (prop,cstr) res)
| _ -> Success res
in state, res
@@ -1029,7 +1055,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
else TypeGlobal.arrow_morphism
in
let (evars', mor), unfold = arr env evars tx tb x b in
- let state, res = aux state env avoid mor ty (prop,cstr) evars' in
+ let state, res = aux { state ; env ; unfresh ;
+ term1 = mor ; ty1 = ty ;
+ cstr = (prop,cstr) ; evars = evars' } in
let res =
match res with
| Success r -> Success { r with rew_to = unfold r.rew_to }
@@ -1059,7 +1087,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let forall = if prop then PropGlobal.coq_forall else TypeGlobal.coq_forall in
(app_poly_sort prop env evars forall [| dom; lam |]), TypeGlobal.unfold_forall
in
- let state, res = aux state env avoid app ty (prop,cstr) evars' in
+ let state, res = aux { state ; env ; unfresh ;
+ term1 = app ; ty1 = ty ;
+ cstr = (prop,cstr) ; evars = evars' } in
let res =
match res with
| Success r -> Success { r with rew_to = unfold r.rew_to }
@@ -1095,11 +1125,14 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
(* | _ -> b') *)
| Lambda (n, t, b) when flags.under_lambdas ->
- let n' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n in
+ let n' = name_app (fun id -> Tactics.fresh_id_in_env unfresh id env) n in
let env' = Environ.push_rel (n', None, t) env in
let bty = Retyping.get_type_of env' (goalevars evars) b in
let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in
- let state, b' = s state env' avoid b bty (prop, unlift env evars cstr) evars in
+ let state, b' = s.strategy { state ; env = env' ; unfresh ;
+ term1 = b ; ty1 = bty ;
+ cstr = (prop, unlift env evars cstr) ;
+ evars } in
let res =
match b' with
| Success r ->
@@ -1124,13 +1157,15 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let cty = Retyping.get_type_of env (goalevars evars) c in
let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in
let cstr' = Some eqty in
- let state, c' = s state env avoid c cty (prop, cstr') evars' in
+ let state, c' = s.strategy { state ; env ; unfresh ;
+ term1 = c ; ty1 = cty ;
+ cstr = (prop, cstr') ; evars = evars' } in
let state, res =
match c' with
| Success r ->
let case = mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs) in
let res = make_leibniz_proof env case ty r in
- state, Success (coerce env avoid (prop,cstr) res)
+ state, Success (coerce env unfresh (prop,cstr) res)
| Fail | Identity ->
if Array.for_all (Int.equal 0) ci.ci_cstr_ndecls then
let evars', eqty = app_poly_sort prop env evars coq_eq [| ty |] in
@@ -1140,7 +1175,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
if not (Option.is_empty found) then
(state, found, fun x -> lift 1 br :: acc x)
else
- let state, res = s state env avoid br ty (prop,cstr) evars in
+ let state, res = s.strategy { state ; env ; unfresh ;
+ term1 = br ; ty1 = ty ;
+ cstr = (prop,cstr) ; evars } in
match res with
| Success r -> (state, Some r, fun x -> mkRel 1 :: acc x)
| Fail | Identity -> (state, None, fun x -> lift 1 br :: acc x))
@@ -1155,7 +1192,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
match try Some (fold_match env (goalevars evars) t) with Not_found -> None with
| None -> state, c'
| Some (cst, _, t', eff (*FIXME*)) ->
- let state, res = aux state env avoid t' ty (prop,cstr) evars in
+ let state, res = aux { state ; env ; unfresh ;
+ term1 = t' ; ty1 = ty ;
+ cstr = (prop,cstr) ; evars } in
let res =
match res with
| Success prf ->
@@ -1169,11 +1208,11 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
match res with
| Success r ->
let rel, prf = get_rew_prf r in
- Success (apply_constraint env avoid r.rew_car rel prf (prop,cstr) r)
+ Success (apply_constraint env unfresh r.rew_car rel prf (prop,cstr) r)
| Fail | Identity -> res
in state, res
| _ -> state, Fail
- in aux
+ in { strategy = aux }
let all_subterms = subterm true default_flags
let one_subterm = subterm false default_flags
@@ -1181,11 +1220,13 @@ let one_subterm = subterm false default_flags
(** Requires transitivity of the rewrite step, if not a reduction.
Not tail-recursive. *)
-let transitivity state env avoid prop (res : rewrite_result_info) (next : 'a pure_strategy) :
+let transitivity state env unfresh prop (res : rewrite_result_info) (next : 'a pure_strategy) :
'a * rewrite_result =
let state, nextres =
- next state env avoid res.rew_to res.rew_car
- (prop, get_opt_rew_rel res.rew_prf) res.rew_evars
+ next.strategy { state ; env ; unfresh ;
+ term1 = res.rew_to ; ty1 = res.rew_car ;
+ cstr = (prop, get_opt_rew_rel res.rew_prf) ;
+ evars = res.rew_evars }
in
let res =
match nextres with
@@ -1222,15 +1263,16 @@ module Strategies =
struct
let fail : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
- state, Fail
+ { strategy = fun { state } -> state, Fail }
let id : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
- state, Identity
+ { strategy = fun { state } -> state, Identity }
let refl : 'a pure_strategy =
- fun state env avoid t ty (prop,cstr) evars ->
+ { strategy =
+ fun { state ; env ;
+ term1 = t ; ty1 = ty ;
+ cstr = (prop,cstr) ; evars } ->
let evars, rel = match cstr with
| None ->
let mkr = if prop then PropGlobal.mk_relation else TypeGlobal.mk_relation in
@@ -1249,38 +1291,43 @@ module Strategies =
let res = Success { rew_car = ty; rew_from = t; rew_to = t;
rew_prf = RewPrf (rel, proof); rew_evars = evars }
in state, res
+ }
- let progress (s : 'a pure_strategy) : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
- let state, res = s state env avoid t ty cstr evars in
+ let progress (s : 'a pure_strategy) : 'a pure_strategy = { strategy =
+ fun input ->
+ let state, res = s.strategy input in
match res with
| Fail -> state, Fail
| Identity -> state, Fail
| Success r -> state, Success r
+ }
- let seq first snd : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
- let state, res = first state env avoid t ty cstr evars in
+ let seq first snd : 'a pure_strategy = { strategy =
+ fun ({ env ; unfresh ; cstr } as input) ->
+ let state, res = first.strategy input in
match res with
| Fail -> state, Fail
- | Identity -> snd state env avoid t ty cstr evars
- | Success res -> transitivity state env avoid (fst cstr) res snd
+ | Identity -> snd.strategy { input with state }
+ | Success res -> transitivity state env unfresh (fst cstr) res snd
+ }
- let choice fst snd : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
- let state, res = fst state env avoid t ty cstr evars in
+ let choice fst snd : 'a pure_strategy = { strategy =
+ fun input ->
+ let state, res = fst.strategy input in
match res with
- | Fail -> snd state env avoid t ty cstr evars
+ | Fail -> snd.strategy { input with state }
| Identity | Success _ -> state, res
+ }
let try_ str : 'a pure_strategy = choice str id
- let check_interrupt str s e l c t r ev =
+ let check_interrupt str input =
Control.check_for_interrupt ();
- str s e l c t r ev
-
+ str input
+
let fix (f : 'a pure_strategy -> 'a pure_strategy) : 'a pure_strategy =
- let rec aux state = f (fun state -> check_interrupt aux state) state in aux
+ let rec aux input = (f { strategy = fun input -> check_interrupt aux input }).strategy input in
+ { strategy = aux }
let any (s : 'a pure_strategy) : 'a pure_strategy =
fix (fun any -> try_ (seq s any))
@@ -1316,16 +1363,17 @@ module Strategies =
(List.map (fun hint -> (inj_open hint, hint.Autorewrite.rew_l2r,
hint.Autorewrite.rew_tac)) rules)
- let hints (db : string) : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
+ let hints (db : string) : 'a pure_strategy = { strategy =
+ fun ({ term1 = t } as input) ->
let rules = Autorewrite.find_matches db t in
let lemma hint = (inj_open hint, hint.Autorewrite.rew_l2r,
hint.Autorewrite.rew_tac) in
let lems = List.map lemma rules in
- lemmas lems state env avoid t ty cstr evars
+ (lemmas lems).strategy input
+ }
- let reduce (r : Redexpr.red_expr) : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
+ let reduce (r : Redexpr.red_expr) : 'a pure_strategy = { strategy =
+ fun { state = state ; env = env ; term1 = t ; ty1 = ty ; cstr = cstr ; evars = evars } ->
let rfn, ckind = Redexpr.reduction_of_red_expr env r in
let evars', t' = rfn env (goalevars evars) t in
if eq_constr t' t then
@@ -1334,9 +1382,10 @@ module Strategies =
state, Success { rew_car = ty; rew_from = t; rew_to = t';
rew_prf = RewCast ckind;
rew_evars = evars', cstrevars evars }
+ }
- let fold_glob c : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
+ let fold_glob c : 'a pure_strategy = { strategy =
+ fun { state ; env ; term1 = t ; ty1 = ty ; cstr ; evars } ->
(* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in
let unfolded =
@@ -1351,6 +1400,7 @@ module Strategies =
rew_prf = RewCast DEFAULTcast;
rew_evars = (sigma, snd evars) }
with e when Errors.noncritical e -> state, Fail
+ }
end
@@ -1361,8 +1411,8 @@ end
even finding a first application of the rewriting lemma, in setoid_rewrite
mode *)
-let rewrite_with l2r flags c occs : strategy =
- fun () env avoid t ty cstr (sigma, cstrs) ->
+let rewrite_with l2r flags c occs : strategy = { strategy =
+ fun ({ state = () } as input) ->
let unify env evars t =
let (sigma, cstrs) = evars in
let ans =
@@ -1382,12 +1432,15 @@ let rewrite_with l2r flags c occs : strategy =
Strategies.fix (fun aux ->
Strategies.choice app (subterm true default_flags aux))
in
- let _, res = strat 0 env avoid t ty cstr (sigma, cstrs) in
- ((), res)
+ let _, res = strat.strategy { input with state = 0 } in
+ ((), res)
+ }
-let apply_strategy (s : strategy) env avoid concl (prop, cstr) evars =
+let apply_strategy (s : strategy) env unfresh concl (prop, cstr) evars =
let ty = Retyping.get_type_of env (goalevars evars) concl in
- let _, res = s () env avoid concl ty (prop, Some cstr) evars in
+ let _, res = s.strategy { state = () ; env ; unfresh ;
+ term1 = concl ; ty1 = ty ;
+ cstr = (prop, Some cstr) ; evars } in
res
let solve_constraints env (evars,cstrs) =
@@ -1566,13 +1619,13 @@ let cl_rewrite_clause l left2right occs clause gl =
let strat = rewrite_with left2right (general_rewrite_unif_flags ()) l occs in
cl_rewrite_clause_strat strat clause gl
-let apply_glob_constr c l2r occs = (); fun () env avoid t ty cstr evars ->
+let apply_glob_constr c l2r occs = (); fun ({ state = () ; env = env } as input) ->
let c sigma =
let (sigma, c) = Pretyping.understand_tcc env sigma c in
(sigma, (c, NoBindings))
in
let flags = general_rewrite_unif_flags () in
- apply_lemma l2r flags c None occs () env avoid t ty cstr evars
+ (apply_lemma l2r flags c None occs).strategy input
let interp_glob_constr_list env =
let make c = (); fun sigma ->
@@ -1636,16 +1689,18 @@ let rec strategy_of_ast = function
| Compose -> Strategies.seq
| Choice -> Strategies.choice
in f' s' t'
- | StratConstr (c, b) -> apply_glob_constr (fst c) b AllOccurrences
+ | StratConstr (c, b) -> { strategy = apply_glob_constr (fst c) b AllOccurrences }
| StratHints (old, id) -> if old then Strategies.old_hints id else Strategies.hints id
- | StratTerms l ->
- (fun () env avoid t ty cstr evars ->
+ | StratTerms l -> { strategy =
+ (fun ({ state = () ; env } as input) ->
let l' = interp_glob_constr_list env (List.map fst l) in
- Strategies.lemmas l' () env avoid t ty cstr evars)
- | StratEval r ->
- (fun () env avoid t ty cstr evars ->
+ (Strategies.lemmas l').strategy input)
+ }
+ | StratEval r -> { strategy =
+ (fun ({ state = () ; env ; evars } as input) ->
let (sigma,r_interp) = Tacinterp.interp_redexp env (goalevars evars) r in
- Strategies.reduce r_interp () env avoid t ty cstr (sigma,cstrevars evars))
+ (Strategies.reduce r_interp).strategy { input with
+ evars = (sigma,cstrevars evars) }) }
| StratFold c -> Strategies.fold_glob (fst c)
@@ -1954,9 +2009,10 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
let app = apply_rule unify occs in
let recstrat aux = Strategies.choice app (subterm true general_rewrite_flags aux) in
let substrat = Strategies.fix recstrat in
- let strat () env avoid t ty cstr evars =
- let _, res = substrat 0 env avoid t ty cstr evars in
+ let strat = { strategy = fun ({ state = () } as input) ->
+ let _, res = substrat.strategy { input with state = 0 } in
(), res
+ }
in
let origsigma = project gl in
init_setoid ();
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index d4c67b90f..fb22da83a 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -341,7 +341,7 @@ let intern_typed_pattern ist p =
let rec intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
let interp_ref r =
- try l, Inl (intern_evaluable ist r)
+ try Inl (intern_evaluable ist r)
with e when Logic.catchable_exception e ->
(* Compatibility. In practice, this means that the code above
is useless. Still the idea of having either an evaluable
@@ -356,19 +356,19 @@ let rec intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
let c = Constrintern.interp_reference sign r in
match c with
| GRef (_,r,None) ->
- l, Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
+ Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
| GVar (_,id) ->
let r = evaluable_of_global_reference ist.genv (VarRef id) in
- l, Inl (ArgArg (r,None))
+ Inl (ArgArg (r,None))
| _ ->
- l, Inr ((c,None),dummy_pat) in
- match p with
+ Inr ((c,None),dummy_pat) in
+ (l, match p with
| Inl r -> interp_ref r
| Inr (CAppExpl(_,(None,r,None),[])) ->
(* We interpret similarly @ref and ref *)
interp_ref (AN r)
| Inr c ->
- l, Inr (intern_typed_pattern ist c)
+ Inr (intern_typed_pattern ist c))
(* This seems fairly hacky, but it's the first way I've found to get proper
globalization of [unfold]. --adamc *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 374c7c736..593e46b05 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -678,7 +678,19 @@ let interp_constr_with_occurrences ist env sigma (occs,c) =
let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
let p = match a with
- | Inl b -> Inl (interp_evaluable ist env sigma b)
+ | Inl (ArgVar (loc,id)) ->
+ (* This is the encoding of an ltac var supposed to be bound
+ prioritary to an evaluable reference and otherwise to a constr
+ (it is an encoding to satisfy the "union" type given to Simpl) *)
+ let coerce_eval_ref_or_constr x =
+ try Inl (coerce_to_evaluable_ref env x)
+ with CannotCoerceTo _ ->
+ let c = coerce_to_closed_constr env x in
+ Inr (pi3 (pattern_of_constr env sigma c)) in
+ (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id)
+ with Not_found ->
+ error_global_not_found_loc loc (qualid_of_ident id))
+ | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
| Inr c -> Inr (pi3 (interp_typed_pattern ist env sigma c)) in
interp_occurrences ist occs, p
diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v
index e540ae5f3..5b87e877b 100644
--- a/test-suite/success/simpl.v
+++ b/test-suite/success/simpl.v
@@ -98,3 +98,10 @@ Fail simpl (unbox _ (unbox _ _)) at 3 4. (* Nested and even overlapping *)
simpl (unbox _ (unbox _ _)) at 2 4.
match goal with |- unbox _ (Box _ True) = unbox _ (Box _ True) => idtac end.
Abort.
+
+(* Check interpretation of ltac variables (was broken in 8.5 beta 1 and 2 *)
+
+Goal 2=1+1.
+match goal with |- (_ = ?c) => simpl c end.
+match goal with |- 2 = 2 => idtac end. (* Check that it reduced *)
+Abort.
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a04678a1b..c92c8fff7 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -94,9 +94,21 @@ let output_context = ref false
let memory_stat = ref false
let print_memory_stat () =
- if !memory_stat then
+ begin (* -m|--memory from the command-line *)
+ if !memory_stat then
ppnl
- (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes")
+ (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes");
+ end;
+ begin
+ (* operf-macro interface:
+ https://github.com/OCamlPro/operf-macro *)
+ try
+ let fn = Sys.getenv "OCAML_GC_STATS" in
+ let oc = open_out fn in
+ Gc.print_stat oc;
+ close_out oc
+ with _ -> ()
+ end
let _ = at_exit print_memory_stat
@@ -111,10 +123,15 @@ let set_hierarchy () = if !type_in_type then Global.set_type_in_type ()
let set_batch_mode () = batch_mode := true
-let set_warning = function
-| "all" -> make_warn true
-| "none" -> make_warn false
-| _ -> prerr_endline ("Error: all/none expected after option w"); exit 1
+let user_warning = ref false
+(** User explicitly set warning *)
+
+let set_warning p =
+ let () = user_warning := true in
+ match p with
+ | "all" -> make_warn true
+ | "none" -> make_warn false
+ | _ -> prerr_endline ("Error: all/none expected after option w"); exit 1
let toplevel_default_name = DirPath.make [Id.of_string "Top"]
let toplevel_name = ref (Some toplevel_default_name)
@@ -630,6 +647,7 @@ let start () =
let () = init_toplevel (List.tl (Array.to_list Sys.argv)) in
(* In batch mode, Coqtop has already exited at this point. In interactive one,
dump glob is nothing but garbage ... *)
+ if not !user_warning then make_warn true;
!toploop_run ();
exit 1
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 523134b50..9df5a411b 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -306,7 +306,7 @@ type fixpoint_kind =
type notations = (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
-type program_info = {
+type program_info_aux = {
prg_name: Id.t;
prg_body: constr;
prg_type: constr;
@@ -322,6 +322,13 @@ type program_info = {
prg_opaque : bool;
}
+type program_info = program_info_aux Ephemeron.key
+
+let get_info x =
+ try Ephemeron.get x
+ with Ephemeron.InvalidKey ->
+ Errors.anomaly Pp.(str "Program obligation can't be accessed by a worker")
+
let assumption_message = Declare.assumption_message
let (set_default_tactic, get_default_tactic, print_default_tactic) =
@@ -452,7 +459,7 @@ let subst_deps_obl obls obl =
module ProgMap = Map.Make(Id)
-let map_replace k v m = ProgMap.add k v (ProgMap.remove k m)
+let map_replace k v m = ProgMap.add k (Ephemeron.create v) (ProgMap.remove k m)
let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
@@ -674,13 +681,13 @@ let get_prog name =
let prg_infos = !from_prg in
match name with
Some n ->
- (try ProgMap.find n prg_infos
+ (try get_info (ProgMap.find n prg_infos)
with Not_found -> raise (NoObligations (Some n)))
| None ->
(let n = map_cardinal prg_infos in
match n with
0 -> raise (NoObligations None)
- | 1 -> map_first prg_infos
+ | 1 -> get_info (map_first prg_infos)
| _ ->
error ("More than one program with unsolved obligations: "^
String.concat ", "
@@ -690,7 +697,7 @@ let get_prog name =
let get_any_prog () =
let prg_infos = !from_prg in
let n = map_cardinal prg_infos in
- if n > 0 then map_first prg_infos
+ if n > 0 then get_info (map_first prg_infos)
else raise (NoObligations None)
let get_prog_err n =
@@ -730,7 +737,7 @@ let update_obls prg obls rem =
progmap_remove prg';
Defined kn
| l ->
- let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in
+ let progs = List.map (fun x -> get_info (ProgMap.find x !from_prg)) prg'.prg_deps in
if List.for_all (fun x -> obligations_solved x) progs then
let kn = declare_mutual_definition progs in
Defined (ConstRef kn)
@@ -929,7 +936,7 @@ and solve_obligations n tac =
solve_prg_obligations prg tac
and solve_all_obligations tac =
- ProgMap.iter (fun k v -> ignore(solve_prg_obligations v tac)) !from_prg
+ ProgMap.iter (fun k v -> ignore(solve_prg_obligations (get_info v) tac)) !from_prg
and try_solve_obligation n prg tac =
let prg = get_prog prg in
@@ -970,7 +977,7 @@ let show_obligations ?(msg=true) n =
| Some n ->
try [ProgMap.find n !from_prg]
with Not_found -> raise (NoObligations (Some n))
- in List.iter (show_obligations_of_prg ~msg) progs
+ in List.iter (fun x -> show_obligations_of_prg ~msg (get_info x)) progs
let show_term n =
let prg = get_prog_err n in
@@ -991,7 +998,7 @@ let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition)
else (
let len = Array.length obls in
let _ = Flags.if_verbose msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in
- progmap_add n prg;
+ progmap_add n (Ephemeron.create prg);
let res = auto_solve_obligations (Some n) tactic in
match res with
| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
@@ -1004,7 +1011,7 @@ let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduc
(fun (n, b, t, imps, obls) ->
let prg = init_prog_info ~opaque n (Some b) t ctx deps (Some fixkind)
notations obls imps kind reduce hook
- in progmap_add n prg) l;
+ in progmap_add n (Ephemeron.create prg)) l;
let _defined =
List.fold_left (fun finished x ->
if finished then finished
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index c7d77de8c..281fb7ef7 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -52,7 +52,7 @@ let print_usage_channel co command =
\n proofs in each fi.vio\
\n\
\n -where print Coq's standard library location and exit\
-\n -config print Coq's configuration information and exit\
+\n -config, --config print Coq's configuration information and exit\
\n -v print Coq version and exit\
\n -list-tags print highlight color tags known by Coq and exit\
\n\
@@ -74,8 +74,12 @@ let print_usage_channel co command =
\n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\
\n -type-in-type disable universe consistency checking\
\n -time display the time taken by each command\
+\n -m, --memory display total heap size at program exit\
+\n (use environment variable\
+\n OCAML_GC_STATS=\"/tmp/gclog.txt\"\
+\n for full Gc stats dump)
\n -native-compiler precompile files for the native_compute machinery\
-\n -h, -help print this list of options\
+\n -h, -help, --help print this list of options\
\n";
List.iter (fun (name, text) ->
output_string co
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 7d84ecf6c..bc8aa2fff 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -344,10 +344,10 @@ let compile verbosely f =
let open Library in
Dumpglob.noglob ();
let f = if check_suffix f ".vio" then chop_extension f else f in
- let lfdv, lib, univs, disch, tasks, proofs = load_library_todo f in
+ let lfdv, sum, lib, univs, disch, tasks, proofs = load_library_todo f in
Stm.set_compilation_hints lfdv;
let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
- Library.save_library_raw lfdv lib univs proofs
+ Library.save_library_raw lfdv sum lib univs proofs
let compile v f =
ignore(CoqworkmgrApi.get 1);
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 80fe26a81..8d9f8f52c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1435,10 +1435,10 @@ let _ =
declare_bool_option
{ optsync = true;
optdepr = false;
- optname = "printing of universes";
- optkey = ["Printing";"Universes"];
- optread = (fun () -> !Constrextern.print_universes);
- optwrite = (fun b -> Constrextern.print_universes:=b) }
+ optname = "dumping bytecode after compilation";
+ optkey = ["Dump";"Bytecode"];
+ optread = Flags.get_dump_bytecode;
+ optwrite = Flags.set_dump_bytecode }
let vernac_debug b =
set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 15:15:37 +0000