aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/analyze.ml48
-rw-r--r--checker/analyze.mli3
-rw-r--r--checker/check.ml26
-rw-r--r--checker/checkInductive.ml2
-rw-r--r--checker/checker.ml22
-rw-r--r--checker/dune1
-rw-r--r--checker/mod_checking.ml2
-rw-r--r--checker/validate.ml7
-rw-r--r--checker/values.ml14
-rw-r--r--checker/values.mli1
-rw-r--r--checker/votour.ml8
11 files changed, 90 insertions, 44 deletions
diff --git a/checker/analyze.ml b/checker/analyze.ml
index e145988b4f..91137a0ce2 100644
--- a/checker/analyze.ml
+++ b/checker/analyze.ml
@@ -106,7 +106,8 @@ end
type repr =
| RInt of int
-| RInt63 of Uint63.t
+| Rint64 of Int64.t
+| RFloat64 of float
| RBlock of (int * int) (* tag × len *)
| RString of string
| RPointer of int
@@ -120,7 +121,8 @@ type data =
type obj =
| Struct of int * data array (* tag × data *)
-| Int63 of Uint63.t (* Primitive integer *)
+| Int64 of Int64.t (* Primitive integer *)
+| Float64 of float (* Primitive float *)
| String of string
module type Input =
@@ -279,6 +281,25 @@ let input_intL chan : int64 =
(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 input_double_big chan : float =
+ Int64.float_of_bits (input_intL chan)
+
+let input_double_little chan : float =
+ 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
+ let bits =
+ (p lsl 56) lor (o lsl 48) lor (n lsl 40) lor (m lsl 32) lor
+ (l lsl 24) lor (k lsl 16) lor (j lsl 8) lor (Int64.of_int i) in
+ Int64.float_of_bits bits
+
let parse_object chan =
let data = input_byte chan in
if prefix_small_block <= data then
@@ -323,12 +344,14 @@ let parse_object chan =
RCode addr
| CODE_CUSTOM ->
begin match input_cstring chan with
- | "_j" -> RInt63 (Uint63.of_int64 (input_intL chan))
+ | "_j" -> Rint64 (input_intL chan)
| s -> Printf.eprintf "Unhandled custom code: %s" s; assert false
end
+ | CODE_DOUBLE_BIG ->
+ RFloat64 (input_double_big chan)
+ | CODE_DOUBLE_LITTLE ->
+ RFloat64 (input_double_little chan)
| CODE_DOUBLE_ARRAY32_LITTLE
- | CODE_DOUBLE_BIG
- | CODE_DOUBLE_LITTLE
| CODE_DOUBLE_ARRAY8_BIG
| CODE_DOUBLE_ARRAY8_LITTLE
| CODE_DOUBLE_ARRAY32_BIG
@@ -365,9 +388,14 @@ let parse chan =
| RCode addr ->
let data = Fun addr in
data, None
- | RInt63 i ->
+ | Rint64 i ->
+ let data = Ptr !current_object in
+ let () = LargeArray.set memory !current_object (Int64 i) in
+ let () = incr current_object in
+ data, None
+ | RFloat64 f ->
let data = Ptr !current_object in
- let () = LargeArray.set memory !current_object (Int63 i) in
+ let () = LargeArray.set memory !current_object (Float64 f) in
let () = incr current_object in
data, None
in
@@ -433,7 +461,8 @@ 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
+ | Int64 i -> Obj.repr i
+ | Float64 f -> Obj.repr f
| String str -> Obj.repr str
in
LargeArray.set ans i obj
@@ -452,7 +481,8 @@ let instantiate (p, mem) =
for k = 0 to Array.length blk - 1 do
Obj.set_field obj k (get_data blk.(k))
done
- | Int63 _
+ | Int64 _
+ | Float64 _
| String _ -> ()
done;
get_data p
diff --git a/checker/analyze.mli b/checker/analyze.mli
index 029f595959..6626d1dff7 100644
--- a/checker/analyze.mli
+++ b/checker/analyze.mli
@@ -7,7 +7,8 @@ type data =
type obj =
| Struct of int * data array (* tag × data *)
-| Int63 of Uint63.t (* Primitive integer *)
+| Int64 of Int64.t (* Primitive integer *)
+| Float64 of float (* Primitive float *)
| String of string
module LargeArray :
diff --git a/checker/check.ml b/checker/check.ml
index 09ecd675f7..ffb2928d55 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -155,24 +155,24 @@ let add_load_path (phys_path,coq_path) =
let physical, logical = !load_paths in
match List.filter2 (fun p d -> p = phys_path) physical logical with
| _,[dir] ->
- if coq_path <> dir
+ if coq_path <> dir
(* If this is not the default -I . to coqtop *)
&& not
(phys_path = CUnix.canonical_path_name Filename.current_dir_name
- && coq_path = default_root_prefix)
- then
- begin
+ && coq_path = default_root_prefix)
+ then
+ begin
(* Assume the user is concerned by library naming *)
- if dir <> default_root_prefix then
- Feedback.msg_warning
- (str phys_path ++ strbrk " was previously bound to " ++
- pr_dirpath dir ++ strbrk "; it is remapped to " ++
- pr_dirpath coq_path);
- remove_load_path phys_path;
- load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths)
- end
+ if dir <> default_root_prefix then
+ Feedback.msg_warning
+ (str phys_path ++ strbrk " was previously bound to " ++
+ pr_dirpath dir ++ strbrk "; it is remapped to " ++
+ pr_dirpath coq_path);
+ remove_load_path phys_path;
+ load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths)
+ end
| _,[] ->
- load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
+ load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
| _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path^"."))
let load_paths_of_dir_path dir =
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index d20eea7874..06ee4fcc7a 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -61,7 +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_cumulative= Option.has_some mb.mind_variance;
mind_entry_private = mb.mind_private;
}
diff --git a/checker/checker.ml b/checker/checker.ml
index d08e9e698d..5f93148be6 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -29,7 +29,7 @@ let parse_dir s =
if n>=len then dirs else
let pos =
try
- String.index_from s n '.'
+ String.index_from s n '.'
with Not_found -> len
in
let dir = String.sub s n (pos-n) in
@@ -241,8 +241,8 @@ let explain_exn = function
hov 0 (str "Stack overflow")
| Match_failure(filename,pos1,pos2) ->
hov 1 (anomaly_string () ++ str "Match failure in file " ++
- guill filename ++ str " at line " ++ int pos1 ++
- str " character " ++ int pos2 ++ report ())
+ guill filename ++ str " at line " ++ int pos1 ++
+ str " character " ++ int pos2 ++ report ())
| Not_found ->
hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report ())
| Failure s ->
@@ -312,12 +312,12 @@ let explain_exn = function
| Assert_failure (s,b,e) ->
hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
- (if s = "" then mt ()
- else
- (str "(file \"" ++ str s ++ str "\", line " ++ int b ++
- str ", characters " ++ int e ++ str "-" ++
- int (e+6) ++ str ")")) ++
- report ())
+ (if s = "" then mt ()
+ else
+ (str "(file \"" ++ str s ++ str "\", line " ++ int b ++
+ str ", characters " ++ int e ++ str "-" ++
+ int (e+6) ++ str ")")) ++
+ report ())
| e -> CErrors.print e (* for anomalies and other uncaught exceptions *)
let deprecated flag =
@@ -333,8 +333,8 @@ let parse_args argv =
indices_matter:=true; parse rem
| "-coqlib" :: s :: rem ->
- if not (exists_dir s) then
- fatal_error (str "Directory '" ++ str s ++ str "' does not exist") false;
+ if not (exists_dir s) then
+ fatal_error (str "Directory '" ++ str s ++ str "' does not exist") false;
Envars.set_user_coqlib s;
parse rem
diff --git a/checker/dune b/checker/dune
index 73cbbc8d19..af7d4f2923 100644
--- a/checker/dune
+++ b/checker/dune
@@ -12,6 +12,7 @@
(executable
(name coqchk)
(public_name coqchk)
+ (modes exe byte)
(package coq)
(modules coqchk)
(flags :standard -open Coq_checklib)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 3128e125dd..44b7089fd0 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -163,6 +163,6 @@ and check_signature env sign mp_mse res = match sign with
MoreFunctor(arg_id,mtb,body)
| NoFunctor struc ->
let (_:env) = List.fold_left (fun env (lab,mb) ->
- check_structure_field env mp_mse lab res mb) env struc
+ check_structure_field env mp_mse lab res mb) env struc
in
NoFunctor struc
diff --git a/checker/validate.ml b/checker/validate.ml
index 178bb4c527..070a112bb6 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -87,6 +87,7 @@ let rec val_gen v ctx o = match v with
| Dyn -> val_dyn ctx o
| Proxy { contents = v } -> val_gen v ctx o
| Uint63 -> val_uint63 ctx o
+ | Float64 -> val_float64 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
@@ -104,7 +105,7 @@ and val_tuple ?name vs ctx o =
else
fail ctx o
("tuple size: found "^string_of_int (Obj.size o)^
- ", expected "^string_of_int n)
+ ", expected "^string_of_int n)
(* Check that the object is either a constant constructor of tag < cc,
or a constructed variant. each element of vv is an array of
@@ -138,6 +139,10 @@ and val_uint63 ctx o =
if not (Uint63.is_uint63 o) then
fail ctx o "not a 63-bit unsigned integer"
+and val_float64 ctx o =
+ if not (Float64.is_float64 o) then
+ fail ctx o "not a 64-bit float"
+
let print_frame = function
| CtxType t -> t
| CtxAnnot t -> t
diff --git a/checker/values.ml b/checker/values.ml
index 9a2028a96b..56321a27ff 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -35,6 +35,7 @@ type value =
| Proxy of value ref
| Uint63
+ | Float64
let fix (f : value -> value) : value =
let self = ref Any in
@@ -116,7 +117,7 @@ let v_binder_annot x = v_tuple "binder_annot" [|x;v_relevance|]
let v_puniverses v = v_tuple "punivs" [|v;v_instance|]
-let v_boollist = List v_bool
+let v_boollist = List v_bool
let v_caseinfo =
let v_cstyle = v_enum "case_style" 5 in
@@ -147,7 +148,8 @@ let rec v_constr =
[|v_fix|]; (* Fix *)
[|v_cofix|]; (* CoFix *)
[|v_proj;v_constr|]; (* Proj *)
- [|Uint63|] (* Int *)
+ [|Uint63|]; (* Int *)
+ [|Float64|] (* Int *)
|])
and v_prec = Tuple ("prec_declaration",
@@ -226,7 +228,7 @@ let v_pol_arity =
v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
let v_primitive =
- v_enum "primitive" 25
+ v_enum "primitive" 44 (* Number of "Primitive" in Int63.v and PrimFloat.v *)
let v_cst_def =
v_sum "constant_def" 0
@@ -300,9 +302,11 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
Opt v_bool;
v_typing_flags|]
-let v_prim_ind = v_enum "prim_ind" 4
+let v_prim_ind = v_enum "prim_ind" 6
+(* Number of "Register ... as kernel.ind_..." in Int63.v and PrimFloat.v *)
-let v_prim_type = v_enum "prim_type" 1
+let v_prim_type = v_enum "prim_type" 2
+(* Number of constructors of prim_type in "kernel/cPrimitives.ml" *)
let v_retro_action =
v_sum "retro_action" 0 [|
diff --git a/checker/values.mli b/checker/values.mli
index db6b0be250..ec3b91d5dd 100644
--- a/checker/values.mli
+++ b/checker/values.mli
@@ -39,6 +39,7 @@ type value =
(** Same as the inner value, used to define recursive types *)
| Uint63
+ | Float64
(** 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 97584831e5..9adcc874ac 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -100,7 +100,8 @@ 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
+ | Int64 _ -> k 0
+ | Float64 _ -> k 0
| String s ->
let size = 2 + (String.length s / ws) in
let () = LargeArray.set !sizes p size in
@@ -117,7 +118,8 @@ struct
| Ptr p ->
match LargeArray.get !memory p with
| Struct (tag, os) -> BLOCK (tag, os)
- | Int63 _ -> OTHER (* TODO: pretty-print int63 values *)
+ | Int64 _ -> OTHER (* TODO: pretty-print int63 values *)
+ | Float64 _ -> OTHER (* TODO: pretty-print float64 values *)
| String s -> STRING s
let input ch =
@@ -156,6 +158,7 @@ let rec get_name ?(extra=false) = function
|Dyn -> "<dynamic>"
| Proxy v -> get_name ~extra !v
| Uint63 -> "Uint63"
+ | Float64 -> "Float64"
(** For tuples, its quite handy to display the inner 1st string (if any).
Cf. [structure_body] for instance *)
@@ -261,6 +264,7 @@ let rec get_children v o pos = match v with
|Fail s -> raise Forbidden
| Proxy v -> get_children !v o pos
| Uint63 -> raise Exit
+ | Float64 -> 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 09:10:20 +0000