aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/analyze.ml39
-rw-r--r--checker/analyze.mli2
-rw-r--r--checker/checkInductive.ml17
-rw-r--r--checker/checker.ml10
-rw-r--r--checker/mod_checking.ml5
-rw-r--r--checker/safe_checking.ml1
-rw-r--r--checker/validate.ml5
-rw-r--r--checker/values.ml37
-rw-r--r--checker/values.mli2
-rw-r--r--checker/votour.ml4
10 files changed, 96 insertions, 26 deletions
diff --git a/checker/analyze.ml b/checker/analyze.ml
index 63324bff20..77e70318dd 100644
--- a/checker/analyze.ml
+++ b/checker/analyze.ml
@@ -106,6 +106,7 @@ end
type repr =
| RInt of int
+| RInt63 of Uint63.t
| RBlock of (int * int) (* tag × len *)
| RString of string
| RPointer of int
@@ -119,6 +120,7 @@ type data =
type obj =
| Struct of int * data array (* tag × data *)
+| Int63 of Uint63.t (* Primitive integer *)
| String of string
module type Input =
@@ -255,6 +257,28 @@ let input_header64 chan =
in
(tag, len)
+let input_cstring chan : string =
+ let buff = Buffer.create 17 in
+ let rec loop () =
+ match input_char chan with
+ | '\o000' -> Buffer.contents buff
+ | c -> Buffer.add_char buff c |> loop
+ in loop ()
+
+let input_intL chan : int64 =
+ let i = input_byte chan in
+ let j = input_byte chan in
+ let k = input_byte chan in
+ let l = input_byte chan in
+ let m = input_byte chan in
+ let n = input_byte chan in
+ let o = input_byte chan in
+ let p = input_byte chan in
+ let ( lsl ) x y = Int64.(shift_left (of_int x) y) in
+ let ( lor ) = Int64.logor in
+ (i lsl 56) lor (j lsl 48) lor (k lsl 40) lor (l lsl 32) lor
+ (m lsl 24) lor (n lsl 16) lor (o lsl 8) lor (Int64.of_int p)
+
let parse_object chan =
let data = input_byte chan in
if prefix_small_block <= data then
@@ -297,6 +321,11 @@ let parse_object chan =
let addr = input_int32u chan in
for _i = 0 to 15 do ignore (input_byte chan); done;
RCode addr
+ | CODE_CUSTOM ->
+ begin match input_cstring chan with
+ | "_j" -> RInt63 (Uint63.of_int64 (input_intL chan))
+ | s -> Printf.eprintf "Unhandled custom code: %s" s; assert false
+ end
| CODE_DOUBLE_ARRAY32_LITTLE
| CODE_DOUBLE_BIG
| CODE_DOUBLE_LITTLE
@@ -304,8 +333,7 @@ let parse_object chan =
| CODE_DOUBLE_ARRAY8_LITTLE
| CODE_DOUBLE_ARRAY32_BIG
| CODE_INFIXPOINTER
- | CODE_CUSTOM ->
- Printf.eprintf "Unhandled code %04x\n%!" data; assert false
+ -> Printf.eprintf "Unhandled code %04x\n%!" data; assert false
let parse chan =
let (magic, len, _, _, size) = parse_header chan in
@@ -337,6 +365,11 @@ let parse chan =
| RCode addr ->
let data = Fun addr in
data, None
+ | RInt63 i ->
+ let data = Ptr !current_object in
+ let () = LargeArray.set memory !current_object (Int63 i) in
+ let () = incr current_object in
+ data, None
in
let rec fill block off accu =
@@ -400,6 +433,7 @@ let instantiate (p, mem) =
for i = 0 to len - 1 do
let obj = match LargeArray.get mem i with
| Struct (tag, blk) -> Obj.new_block tag (Array.length blk)
+ | Int63 i -> Obj.repr i
| String str -> Obj.repr str
in
LargeArray.set ans i obj
@@ -418,6 +452,7 @@ let instantiate (p, mem) =
for k = 0 to Array.length blk - 1 do
Obj.set_field obj k (get_data blk.(k))
done
+ | Int63 _
| String _ -> ()
done;
get_data p
diff --git a/checker/analyze.mli b/checker/analyze.mli
index d7770539df..029f595959 100644
--- a/checker/analyze.mli
+++ b/checker/analyze.mli
@@ -1,3 +1,4 @@
+(** Representation of data allocated on the OCaml heap. *)
type data =
| Int of int
| Ptr of int
@@ -6,6 +7,7 @@ type data =
type obj =
| Struct of int * data array (* tag × data *)
+| Int63 of Uint63.t (* Primitive integer *)
| String of string
module LargeArray :
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index c823db956d..4329b2d743 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -28,11 +28,8 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
| PrimRecord data -> Some (Some (Array.map pi1 data))
in
let mind_entry_universes = match mb.mind_universes with
- | Monomorphic_ind univs -> Monomorphic_ind_entry univs
- | Polymorphic_ind auctx -> Polymorphic_ind_entry (AUContext.names auctx, AUContext.repr auctx)
- | Cumulative_ind auctx ->
- Cumulative_ind_entry (AUContext.names (ACumulativityInfo.univ_context auctx),
- ACumulativityInfo.repr auctx)
+ | Monomorphic univs -> Monomorphic_entry univs
+ | Polymorphic auctx -> Polymorphic_entry (AUContext.names auctx, AUContext.repr auctx)
in
let mind_entry_inds = Array.map_to_list (fun ind ->
let mind_entry_arity, mind_entry_template = match ind.mind_arity with
@@ -64,6 +61,7 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
mind_entry_params = mb.mind_params_ctxt;
mind_entry_inds;
mind_entry_universes;
+ mind_entry_variance = mb.mind_variance;
mind_entry_private = mb.mind_private;
}
@@ -77,6 +75,9 @@ 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
+
(* Use [eq_ind_chk] because when we rebuild the recargs we have lost
the knowledge of who is the canonical version.
Try with to see test-suite/coqchk/include.v *)
@@ -102,7 +103,7 @@ let check_packet env mind ind
check "mind_user_lc" (Array.equal Constr.equal ind.mind_user_lc mind_user_lc);
check "mind_nrealargs" Int.(equal ind.mind_nrealargs mind_nrealargs);
check "mind_nrealdecls" Int.(equal ind.mind_nrealdecls mind_nrealdecls);
- check "mind_kelim" (List.equal Sorts.family_equal ind.mind_kelim mind_kelim);
+ check "mind_kelim" (check_kelim ind.mind_kelim mind_kelim);
check "mind_nf_lc" (Array.equal Constr.equal ind.mind_nf_lc mind_nf_lc);
(* NB: here syntactic equality is not just an optimisation, we also
@@ -132,7 +133,8 @@ let check_same_record r1 r2 = match r1, r2 with
let check_inductive env mind mb =
let entry = to_entry mb in
let { mind_packets; mind_record; mind_finite; mind_ntypes; mind_hyps;
- mind_nparams; mind_nparams_rec; mind_params_ctxt; mind_universes;
+ mind_nparams; mind_nparams_rec; mind_params_ctxt;
+ mind_universes; mind_variance;
mind_private; mind_typing_flags; }
=
(* Locally set the oracle for further typechecking *)
@@ -154,6 +156,7 @@ let check_inductive env mind mb =
check "mind_params_ctxt" (Context.Rel.equal Constr.equal mb.mind_params_ctxt mind_params_ctxt);
ignore mind_universes; (* Indtypes did the necessary checking *)
+ ignore mind_variance; (* Indtypes did the necessary checking *)
ignore mind_private; (* passed through Indtypes *)
ignore mind_typing_flags;
diff --git a/checker/checker.ml b/checker/checker.ml
index d97ab5409e..3db7ccdcae 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -319,6 +319,8 @@ let explain_exn = function
let deprecated flag =
Feedback.msg_warning (str "Deprecated flag " ++ quote (str flag))
+let boot_opt = ref false
+
let parse_args argv =
let rec parse = function
| [] -> ()
@@ -348,14 +350,14 @@ let parse_args argv =
| "-debug" :: rem -> set_debug (); parse rem
| "-where" :: _ ->
- Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
- print_endline (Envars.coqlib ());
- exit 0
+ Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
+ print_endline (Envars.coqlib ());
+ exit 0
| ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
| ("-v"|"--version") :: _ -> version ()
- | "-boot" :: rem -> Flags.boot := true; parse rem
+ | "-boot" :: rem -> boot_opt := true; parse rem
| ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem
| ("-o" | "--output-context") :: rem ->
Check_stat.output_context := true; parse rem
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 086dd17e39..b86d491d72 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -16,8 +16,8 @@ let check_constant_declaration env kn cb =
(* [env'] contains De Bruijn universe variables *)
let poly, env' =
match cb.const_universes with
- | Monomorphic_const ctx -> false, push_context_set ~strict:true ctx env
- | Polymorphic_const auctx ->
+ | Monomorphic ctx -> false, push_context_set ~strict:true ctx env
+ | Polymorphic auctx ->
let ctx = Univ.AUContext.repr auctx in
let env = push_context ~strict:false ctx env in
true, env
@@ -66,6 +66,7 @@ let mk_mtb mp sign delta =
let rec check_module env mp mb =
Flags.if_verbose Feedback.msg_notice (str " checking module: " ++ str (ModPath.to_string mp));
+ let env = Modops.add_retroknowledge mb.mod_retroknowledge env in
let (_:module_signature) =
check_signature env mb.mod_type mb.mod_mp mb.mod_delta
in
diff --git a/checker/safe_checking.ml b/checker/safe_checking.ml
index 6dc2953060..4a64039e30 100644
--- a/checker/safe_checking.ml
+++ b/checker/safe_checking.ml
@@ -16,6 +16,7 @@ let import senv clib univs digest =
let env = Safe_typing.env_of_safe_env senv in
let env = push_context_set ~strict:true mb.mod_constraints env in
let env = push_context_set ~strict:true univs env in
+ let env = Modops.add_retroknowledge mb.mod_retroknowledge env in
Mod_checking.check_module env mb.mod_mp mb;
let (_,senv) = Safe_typing.import clib univs digest senv in senv
diff --git a/checker/validate.ml b/checker/validate.ml
index b85944f94f..72cf38ebe6 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -86,6 +86,7 @@ let rec val_gen v ctx o = match v with
| Annot (s,v) -> val_gen v (ctx/CtxAnnot s) o
| Dyn -> val_dyn ctx o
| Proxy { contents = v } -> val_gen v ctx o
+ | Uint63 -> val_uint63 ctx o
(* Check that an object is a tuple (or a record). vs is an array of
value representation for each field. Its size corresponds to the
@@ -133,6 +134,10 @@ and val_array v ctx o =
val_gen v ctx (Obj.field o i)
done
+and val_uint63 ctx o =
+ if not (Uint63.is_uint63 o) then
+ fail ctx o "not a 63-bit unsigned integer"
+
let print_frame = function
| CtxType t -> t
| CtxAnnot t -> t
diff --git a/checker/values.ml b/checker/values.ml
index 1afe764ca4..66467fa8f5 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -34,6 +34,7 @@ type value =
| Dyn
| Proxy of value ref
+ | Uint63
let fix (f : value -> value) : value =
let self = ref Any in
@@ -111,7 +112,6 @@ let v_variance = v_enum "variance" 3
let v_instance = Annot ("instance", Array v_level)
let v_abs_context = v_tuple "abstract_universe_context" [|Array v_name; v_cstrs|]
-let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; Array v_variance|]
let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
(** kernel/term *)
@@ -151,7 +151,8 @@ let rec v_constr =
[|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *)
[|v_fix|]; (* Fix *)
[|v_cofix|]; (* CoFix *)
- [|v_proj;v_constr|] (* Proj *)
+ [|v_proj;v_constr|]; (* Proj *)
+ [|Uint63|] (* Int *)
|])
and v_prec = Tuple ("prec_declaration",
@@ -214,21 +215,24 @@ let v_oracle =
let v_pol_arity =
v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
+let v_primitive =
+ v_enum "primitive" 25
+
let v_cst_def =
v_sum "constant_def" 0
- [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
+ [|[|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|]
-let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
+let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
let v_cb = v_tuple "constant_body"
[|v_section_ctxt;
v_cst_def;
v_constr;
Any;
- v_const_univs;
+ v_univs;
Opt v_context_set;
v_bool;
v_typing_flags|]
@@ -271,10 +275,6 @@ let v_record_info =
v_sum "record_info" 2
[| [| Array (v_tuple "record" [| v_id; Array v_id; Array v_constr |]) |] |]
-let v_ind_pack_univs =
- v_sum "abstract_inductive_universes" 0
- [|[|v_context_set|]; [|v_abs_context|]; [|v_abs_cum_info|]|]
-
let v_ind_pack = v_tuple "mutual_inductive_body"
[|Array v_one_ind;
v_record_info;
@@ -284,10 +284,25 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
Int;
Int;
v_rctxt;
- v_ind_pack_univs; (* universes *)
+ v_univs; (* universes *)
+ Opt (Array v_variance);
Opt v_bool;
v_typing_flags|]
+let v_prim_ind = v_enum "prim_ind" 4
+
+let v_prim_type = v_enum "prim_type" 1
+
+let v_retro_action =
+ v_sum "retro_action" 0 [|
+ [|v_prim_ind; v_ind|];
+ [|v_prim_type; v_cst|];
+ [|v_cst|];
+ |]
+
+let v_retroknowledge =
+ v_sum "module_retroknowledge" 1 [|[|List v_retro_action|]|]
+
let rec v_mae =
Sum ("module_alg_expr",0,
[|[|v_mp|]; (* SEBident *)
@@ -318,7 +333,7 @@ and v_impl =
and v_noimpl = v_unit
and v_module =
Tuple ("module_body",
- [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|])
+ [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_retroknowledge|])
and v_modtype =
Tuple ("module_type_body",
[|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_unit|])
diff --git a/checker/values.mli b/checker/values.mli
index 616b69907f..2ab8da1928 100644
--- a/checker/values.mli
+++ b/checker/values.mli
@@ -38,6 +38,8 @@ type value =
| Proxy of value ref
(** Same as the inner value, used to define recursive types *)
+ | Uint63
+
(** NB: List and Opt have their own constructors to make it easy to
define eg [let rec foo = List foo]. *)
diff --git a/checker/votour.ml b/checker/votour.ml
index 3c088b59b5..36014cde73 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -100,6 +100,7 @@ struct
init_size seen (fun n -> fold (succ i) (accu + 1 + n) k) os.(i)
in
fold 0 1 (fun size -> let () = LargeArray.set !sizes p size in k size)
+ | Int63 _ -> k 0
| String s ->
let size = 2 + (String.length s / ws) in
let () = LargeArray.set !sizes p size in
@@ -116,6 +117,7 @@ struct
| Ptr p ->
match LargeArray.get !memory p with
| Struct (tag, os) -> BLOCK (tag, os)
+ | Int63 _ -> OTHER (* TODO: pretty-print int63 values *)
| String s -> STRING s
let input ch =
@@ -153,6 +155,7 @@ let rec get_name ?(extra=false) = function
|Annot (s,v) -> s^"/"^get_name ~extra v
|Dyn -> "<dynamic>"
| Proxy v -> get_name ~extra !v
+ | Uint63 -> "Uint63"
(** For tuples, its quite handy to display the inner 1st string (if any).
Cf. [structure_body] for instance *)
@@ -257,6 +260,7 @@ let rec get_children v o pos = match v with
end
|Fail s -> raise Forbidden
| Proxy v -> get_children !v o pos
+ | Uint63 -> raise Exit
let get_children v o pos =
try get_children v o pos
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 17:56:23 +0000