aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/analyze.ml4
-rw-r--r--checker/check.ml40
-rw-r--r--checker/check.mli2
-rw-r--r--checker/checkInductive.ml13
-rw-r--r--checker/checkInductive.mli2
-rw-r--r--checker/checkTypes.ml2
-rw-r--r--checker/checkTypes.mli2
-rw-r--r--checker/check_stat.ml34
-rw-r--r--checker/check_stat.mli2
-rw-r--r--checker/checker.ml2
-rw-r--r--checker/checker.mli2
-rw-r--r--checker/coqchk.mli2
-rw-r--r--checker/include2
-rw-r--r--checker/mod_checking.ml66
-rw-r--r--checker/mod_checking.mli4
-rw-r--r--checker/safe_checking.ml2
-rw-r--r--checker/safe_checking.mli2
-rw-r--r--checker/validate.ml2
-rw-r--r--checker/validate.mli2
-rw-r--r--checker/values.ml64
-rw-r--r--checker/values.mli2
-rw-r--r--checker/votour.ml2
-rw-r--r--checker/votour.mli2
23 files changed, 163 insertions, 94 deletions
diff --git a/checker/analyze.ml b/checker/analyze.ml
index 77e70318dd..e145988b4f 100644
--- a/checker/analyze.ml
+++ b/checker/analyze.ml
@@ -395,8 +395,8 @@ end
module IChannel =
struct
type t = in_channel
- let input_byte = Pervasives.input_byte
- let input_binary_int = Pervasives.input_binary_int
+ let input_byte = input_byte
+ let input_binary_int = input_binary_int
end
module IString =
diff --git a/checker/check.ml b/checker/check.ml
index a2c8a0f25d..69de2536c5 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -50,7 +50,8 @@ let pr_path sp =
type compilation_unit_name = DirPath.t
-type seg_proofs = Constr.constr Future.computation array
+type seg_univ = Univ.ContextSet.t * bool
+type seg_proofs = Opaqueproof.opaque_proofterm array
type library_t = {
library_name : compilation_unit_name;
@@ -65,7 +66,7 @@ module LibraryOrdered =
struct
type t = DirPath.t
let compare d1 d2 =
- Pervasives.compare
+ compare
(List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2))
end
@@ -90,7 +91,6 @@ let register_loaded_library m =
(* Map from library names to table of opaque terms *)
let opaque_tables = ref LibraryMap.empty
-let opaque_univ_tables = ref LibraryMap.empty
let access_opaque_table dp i =
let t =
@@ -100,16 +100,14 @@ let access_opaque_table dp i =
assert (i < Array.length t);
t.(i)
-let access_opaque_univ_table dp i =
- try
- let t = LibraryMap.find dp !opaque_univ_tables in
- assert (i < Array.length t);
- Some t.(i)
- with Not_found -> None
+let access_discharge = Cooking.cook_constr
+
+let indirect_accessor = {
+ Opaqueproof.access_proof = access_opaque_table;
+ Opaqueproof.access_discharge = access_discharge;
+}
-let () =
- Opaqueproof.set_indirect_opaque_accessor access_opaque_table;
- Opaqueproof.set_indirect_univ_accessor access_opaque_univ_table
+let () = Mod_checking.set_indirect_accessor indirect_accessor
let check_one_lib admit senv (dir,m) =
let md = m.library_compiled in
@@ -264,7 +262,6 @@ let raw_intern_library f =
type summary_disk = {
md_name : compilation_unit_name;
- md_imports : compilation_unit_name array;
md_deps : (compilation_unit_name * Safe_typing.vodigest) array;
}
@@ -335,8 +332,7 @@ let intern_from_file ~intern_mode (dir, f) =
let ch = System.with_magic_number_check raw_intern_library f in
let (sd:summary_disk), _, digest = marshal_in_segment f ch in
let (md:library_disk), _, digest = marshal_in_segment f ch in
- let (opaque_csts:'a option), _, udg = marshal_in_segment f ch in
- let (discharging:'a option), _, _ = marshal_in_segment f ch in
+ let (opaque_csts:seg_univ option), _, udg = marshal_in_segment f ch in
let (tasks:'a option), _, _ = marshal_in_segment f ch in
let (table:seg_proofs option), pos, checksum =
marshal_or_skip ~intern_mode f ch in
@@ -349,12 +345,12 @@ let intern_from_file ~intern_mode (dir, f) =
if dir <> sd.md_name then
user_err ~hdr:"intern_from_file"
(name_clash_message dir sd.md_name f);
- if tasks <> None || discharging <> None then
+ if tasks <> None then
user_err ~hdr:"intern_from_file"
(str "The file "++str f++str " contains unfinished tasks");
if opaque_csts <> None then begin
Flags.if_verbose chk_pp (str " (was a vio file) ");
- Option.iter (fun (_,_,b) -> if not b then
+ Option.iter (fun (_,b) -> if not b then
user_err ~hdr:"intern_from_file"
(str "The file "++str f++str " is still a .vio"))
opaque_csts;
@@ -372,19 +368,15 @@ let intern_from_file ~intern_mode (dir, f) =
with e -> Flags.if_verbose chk_pp (str" failed!]" ++ fnl ()); raise e in
depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph;
Option.iter (fun table -> opaque_tables := LibraryMap.add sd.md_name table !opaque_tables) table;
- Option.iter (fun (opaque_csts,_,_) ->
- opaque_univ_tables :=
- LibraryMap.add sd.md_name opaque_csts !opaque_univ_tables)
- opaque_csts;
let extra_cst =
Option.default Univ.ContextSet.empty
- (Option.map (fun (_,cs,_) -> cs) opaque_csts) in
+ (Option.map (fun (cs,_) -> cs) opaque_csts) in
mk_library sd md f table digest extra_cst
let get_deps (dir, f) =
try LibraryMap.find dir !depgraph
with Not_found ->
- let _ = intern_from_file (dir,f) in
+ let _ = intern_from_file ~intern_mode:Dep (dir,f) in
LibraryMap.find dir !depgraph
(* Read a compiled library and all dependencies, in reverse order.
diff --git a/checker/check.mli b/checker/check.mli
index 39cc93c060..7f0340b193 100644
--- a/checker/check.mli
+++ b/checker/check.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index 4f4527ca12..d20eea7874 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -75,8 +75,7 @@ let check_arity env ar1 ar2 = match ar1, ar2 with
(* template_level is inferred by indtypes, so functor application can produce a smaller one *)
| (RegularArity _ | TemplateArity _), _ -> false
-let check_kelim k1 k2 =
- List.for_all (fun x -> List.mem_f Sorts.family_equal x k2) k1
+let check_kelim k1 k2 = Sorts.family_leq k1 k2
(* Use [eq_ind_chk] because when we rebuild the recargs we have lost
the knowledge of who is the canonical version.
@@ -143,8 +142,12 @@ let check_inductive env mind mb =
mind_universes; mind_variance;
mind_private; mind_typing_flags; }
=
- (* Locally set the oracle for further typechecking *)
- let env = Environ.set_oracle env mb.mind_typing_flags.conv_oracle in
+ (* Locally set typing flags for further typechecking *)
+ let mb_flags = mb.mind_typing_flags in
+ let env = Environ.set_typing_flags {env.env_typing_flags with check_guarded = mb_flags.check_guarded;
+ check_positive = mb_flags.check_positive;
+ check_universes = mb_flags.check_universes;
+ conv_oracle = mb_flags.conv_oracle} env in
Indtypes.check_inductive env mind entry
in
let check = check mind in
diff --git a/checker/checkInductive.mli b/checker/checkInductive.mli
index ab54190967..c5f8dec1a4 100644
--- a/checker/checkInductive.mli
+++ b/checker/checkInductive.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/checker/checkTypes.ml b/checker/checkTypes.ml
index 7eaa5eedd5..2f1c690aca 100644
--- a/checker/checkTypes.ml
+++ b/checker/checkTypes.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/checker/checkTypes.mli b/checker/checkTypes.mli
index 022f9bc603..ac9ea2fb31 100644
--- a/checker/checkTypes.mli
+++ b/checker/checkTypes.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 57adc79475..a67945ae94 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -31,14 +31,31 @@ let pr_engagement env =
| PredicativeSet -> str "Theory: Set is predicative"
end
-let is_ax _ cb = not (Declareops.constant_has_body cb)
-let pr_ax env =
- let axs = fold_constants (fun c ce acc -> if is_ax c ce then c::acc else acc) env [] in
+let pr_assumptions ass axs =
if axs = [] then
- str "Axioms: <none>"
+ str ass ++ str ": <none>"
else
- hv 2 (str "Axioms:" ++ fnl() ++ prlist_with_sep fnl Constant.print axs)
+ hv 2 (str ass ++ str ":" ++ fnl() ++ prlist_with_sep fnl str axs)
+
+let pr_axioms env =
+ let csts = fold_constants (fun c cb acc -> if not (Declareops.constant_has_body cb) then Constant.to_string c :: acc else acc) env [] in
+ pr_assumptions "Axioms" csts
+
+let pr_type_in_type env =
+ let csts = fold_constants (fun c cb acc -> if not cb.const_typing_flags.check_universes then Constant.to_string c :: acc else acc) env [] in
+ let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_universes then MutInd.to_string c :: acc else acc) env csts in
+ pr_assumptions "Constants/Inductives relying on type-in-type" csts
+
+let pr_unguarded env =
+ let csts = fold_constants (fun c cb acc -> if not cb.const_typing_flags.check_guarded then Constant.to_string c :: acc else acc) env [] in
+ let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_guarded then MutInd.to_string c :: acc else acc) env csts in
+ pr_assumptions "Constants/Inductives relying on unsafe (co)fixpoints" csts
+
+let pr_nonpositive env =
+ let inds = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_positive then MutInd.to_string c :: acc else acc) env [] in
+ pr_assumptions "Inductives whose positivity is assumed" inds
+
let print_context env =
if !output_context then begin
@@ -47,7 +64,10 @@ let print_context env =
(fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
str"===============" ++ fnl() ++ fnl() ++
str "* " ++ hov 0 (pr_engagement env ++ fnl()) ++ fnl() ++
- str "* " ++ hov 0 (pr_ax env)));
+ str "* " ++ hov 0 (pr_axioms env ++ fnl()) ++ fnl() ++
+ str "* " ++ hov 0 (pr_type_in_type env ++ fnl()) ++ fnl() ++
+ str "* " ++ hov 0 (pr_unguarded env ++ fnl()) ++ fnl() ++
+ str "* " ++ hov 0 (pr_nonpositive env)))
end
let stats env =
diff --git a/checker/check_stat.mli b/checker/check_stat.mli
index b094da1c44..c636327553 100644
--- a/checker/check_stat.mli
+++ b/checker/check_stat.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/checker/checker.ml b/checker/checker.ml
index cbac9cb570..d08e9e698d 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/checker/checker.mli b/checker/checker.mli
index 582f42589c..bbfefb22c0 100644
--- a/checker/checker.mli
+++ b/checker/checker.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/checker/coqchk.mli b/checker/coqchk.mli
index 9db9ecd12e..d0712f8075 100644
--- a/checker/coqchk.mli
+++ b/checker/coqchk.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/checker/include b/checker/include
index 3ffc301724..411321cb3e 100644
--- a/checker/include
+++ b/checker/include
@@ -3,7 +3,7 @@
(* Caml script to include for debugging the checker.
Usage: from the checker/ directory launch ocaml toplevel and then
type #use"include";;
- This command loads the relevent modules, defines some pretty
+ This command loads the relevant modules, defines some pretty
printers, and provides functions to interactively check modules
(mainly run_l and norec).
*)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index b86d491d72..3128e125dd 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -8,40 +8,64 @@ open Environ
(** {6 Checking constants } *)
+let indirect_accessor = ref {
+ Opaqueproof.access_proof = (fun _ _ -> assert false);
+ Opaqueproof.access_discharge = (fun _ _ -> assert false);
+}
+
+let set_indirect_accessor f = indirect_accessor := f
+
let check_constant_declaration env kn cb =
Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ Constant.print kn);
- (* Locally set the oracle for further typechecking *)
- let oracle = env.env_typing_flags.conv_oracle in
- let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in
- (* [env'] contains De Bruijn universe variables *)
- let poly, env' =
+ let cb_flags = cb.const_typing_flags in
+ let env = Environ.set_typing_flags
+ {env.env_typing_flags with
+ check_guarded = cb_flags.check_guarded;
+ check_universes = cb_flags.check_universes;
+ conv_oracle = cb_flags.conv_oracle;}
+ env
+ in
+ let poly, env =
match cb.const_universes with
- | Monomorphic ctx -> false, push_context_set ~strict:true ctx env
+ | Monomorphic ctx ->
+ (* Monomorphic universes are stored at the library level, the
+ ones in const_universes should not be needed *)
+ false, env
| Polymorphic auctx ->
let ctx = Univ.AUContext.repr auctx in
+ (* [env] contains De Bruijn universe variables *)
let env = push_context ~strict:false ctx env in
true, env
in
- let env' = match cb.const_private_poly_univs, (cb.const_body, poly) with
- | None, _ -> env'
- | Some local, (OpaqueDef _, true) -> push_subgraph local env'
- | Some _, _ -> assert false
- in
let ty = cb.const_type in
- let _ = infer_type env' ty in
+ let _ = infer_type env ty in
+ let otab = Environ.opaque_tables env in
+ let body, env = match cb.const_body with
+ | Undef _ | Primitive _ -> None, env
+ | Def c -> Some (Mod_subst.force_constr c), env
+ | OpaqueDef o ->
+ let c, u = Opaqueproof.force_proof !indirect_accessor otab o in
+ let env = match u, cb.const_universes with
+ | Opaqueproof.PrivateMonomorphic (), Monomorphic _ -> env
+ | Opaqueproof.PrivatePolymorphic (_, local), Polymorphic _ ->
+ push_subgraph local env
+ | _ -> assert false
+ in
+ Some c, env
+ in
let () =
- match Environ.body_of_constant_body env cb with
+ match body with
| Some bd ->
- let j = infer env' (fst bd) in
- conv_leq env' j.uj_type ty
+ let j = infer env bd in
+ (try conv_leq env j.uj_type ty
+ with NotConvertible -> Type_errors.error_actual_type env j ty)
| None -> ()
in
- let env =
- if poly then add_constant kn cb env
- else add_constant kn cb env'
- in
- (* Reset the value of the oracle *)
- Environ.set_oracle env oracle
+ ()
+
+let check_constant_declaration env kn cb =
+ let () = check_constant_declaration env kn cb in
+ Environ.add_constant kn cb env
(** {6 Checking modules } *)
diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli
index 6cff3e6b8c..d29d1861f4 100644
--- a/checker/mod_checking.mli
+++ b/checker/mod_checking.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -8,4 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+val set_indirect_accessor : Opaqueproof.indirect_accessor -> unit
+
val check_module : Environ.env -> Names.ModPath.t -> Declarations.module_body -> unit
diff --git a/checker/safe_checking.ml b/checker/safe_checking.ml
index 4a64039e30..a913d53bd6 100644
--- a/checker/safe_checking.ml
+++ b/checker/safe_checking.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/checker/safe_checking.mli b/checker/safe_checking.mli
index 44cd2b3a2e..205777272d 100644
--- a/checker/safe_checking.mli
+++ b/checker/safe_checking.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/checker/validate.ml b/checker/validate.ml
index 72cf38ebe6..178bb4c527 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/checker/validate.mli b/checker/validate.mli
index 6c2ab8d348..fbcea3121b 100644
--- a/checker/validate.mli
+++ b/checker/validate.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/checker/values.ml b/checker/values.ml
index 5cbf0ff298..6b340635d7 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -53,7 +53,6 @@ let v_enum name n = Sum(name,n,[||])
let v_pair v1 v2 = v_tuple "*" [|v1; v2|]
let v_bool = v_enum "bool" 2
let v_unit = v_enum "unit" 1
-let v_ref v = v_tuple "ref" [|v|]
let v_set v =
let rec s = Sum ("Set.t",1,
@@ -70,13 +69,6 @@ let v_hmap vk vd = v_map Int (v_map vk vd)
let v_pred v = v_pair v_bool (v_set v)
-(* lib/future *)
-let v_computation f =
- Annot ("Future.computation",
- v_ref
- (v_sum "Future.comput" 0
- [| [| Fail "Future.ongoing" |]; [| f |] |]))
-
(** kernel/names *)
let v_id = String
@@ -139,7 +131,7 @@ let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|]
let rec v_constr =
Sum ("constr",0,[|
[|Int|]; (* Rel *)
- [|Fail "Var"|]; (* Var *)
+ [|v_id|]; (* Var *)
[|Fail "Meta"|]; (* Meta *)
[|Fail "Evar"|]; (* Evar *)
[|v_sort|]; (* Sort *)
@@ -227,7 +219,7 @@ let v_cst_def =
[|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]; [|v_primitive|]|]
let v_typing_flags =
- v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|]
+ v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool; v_bool|]
let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
@@ -238,7 +230,6 @@ let v_cb = v_tuple "constant_body"
v_relevance;
Any;
v_univs;
- Opt v_context_set;
v_bool;
v_typing_flags|]
@@ -265,7 +256,7 @@ let v_one_ind = v_tuple "one_inductive_body"
Array v_constr;
Int;
Int;
- List v_sortfam;
+ v_sortfam;
Array (v_pair v_rctxt v_constr);
Array Int;
Array Int;
@@ -354,8 +345,26 @@ let v_compiled_lib =
(** Library objects *)
let v_obj = Dyn
-let v_libobj = Tuple ("libobj", [|v_id;v_obj|])
-let v_libobjs = List v_libobj
+
+let rec v_aobjs = Sum("algebraic_objects", 0,
+ [| [|v_libobjs|];
+ [|v_mp;v_subst|]
+ |])
+and v_substobjs =
+ Tuple("*", [|List v_uid;v_aobjs|])
+and v_libobjt = Sum("Libobject.t",0,
+ [| [| v_substobjs |];
+ [| v_substobjs |];
+ [| v_aobjs |];
+ [| v_libobjs |];
+ [| List v_mp |];
+ [| v_obj |]
+ |])
+
+and v_libobj = Tuple ("libobj", [|v_id;v_libobjt|])
+
+and v_libobjs = List v_libobj
+
let v_libraryobjs = Tuple ("library_objects",[|v_libobjs;v_libobjs|])
(** STM objects *)
@@ -386,11 +395,30 @@ 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|])
+ Tuple ("summary", [|v_dp;v_deps|])
let v_lib =
Tuple ("library",[|v_compiled_lib;v_libraryobjs|])
-let v_opaques = Array (v_computation v_constr)
+let v_ndecl = v_sum "named_declaration" 0
+ [| [|v_binder_annot v_id; v_constr|]; (* LocalAssum *)
+ [|v_binder_annot v_id; v_constr; v_constr|] |] (* LocalDef *)
+
+let v_nctxt = List v_ndecl
+
+let v_work_list =
+ let v_abstr = v_pair v_instance (Array v_id) in
+ Tuple ("work_list", [|v_hmap v_cst v_abstr; v_hmap v_cst v_abstr|])
+
+let v_abstract =
+ Tuple ("abstract", [| v_nctxt; v_instance; v_abs_context |])
+
+let v_cooking_info =
+ Tuple ("cooking_info", [|v_work_list; v_abstract|])
+
+let v_delayed_universes =
+ Sum ("delayed_universes", 0, [| [| v_unit |]; [| Int; v_context_set |] |])
+
+let v_opaques = Array (Tuple ("opaque", [| List v_cooking_info; Opt (v_pair v_constr v_delayed_universes) |]))
let v_univopaques =
- Opt (Tuple ("univopaques",[|Array (v_computation v_context_set);v_context_set;v_bool|]))
+ Opt (Tuple ("univopaques",[|v_context_set;v_bool|]))
diff --git a/checker/values.mli b/checker/values.mli
index 2ab8da1928..93983eb700 100644
--- a/checker/values.mli
+++ b/checker/values.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/checker/votour.ml b/checker/votour.ml
index 36014cde73..f0e0cf22ab 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/checker/votour.mli b/checker/votour.mli
index 9db9ecd12e..d0712f8075 100644
--- a/checker/votour.mli
+++ b/checker/votour.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 04:02:13 +0000