aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/analyze.ml86
-rw-r--r--checker/analyze.mli21
-rw-r--r--checker/check.ml21
-rw-r--r--checker/check.mllib1
-rw-r--r--checker/closure.ml25
-rw-r--r--checker/closure.mli2
-rw-r--r--checker/reduction.ml16
-rw-r--r--checker/votour.ml22
8 files changed, 139 insertions, 55 deletions
diff --git a/checker/analyze.ml b/checker/analyze.ml
index df75d5b93..7047d8a14 100644
--- a/checker/analyze.ml
+++ b/checker/analyze.ml
@@ -55,6 +55,55 @@ let magic_number = "\132\149\166\190"
(** Memory reification *)
+module LargeArray :
+sig
+ type 'a t
+ val empty : 'a t
+ val length : 'a t -> int
+ val make : int -> 'a -> 'a t
+ val get : 'a t -> int -> 'a
+ val set : 'a t -> int -> 'a -> unit
+end =
+struct
+
+ let max_length = Sys.max_array_length
+
+ type 'a t = 'a array array * 'a array
+ (** Invariants:
+ - All subarrays of the left array have length [max_length].
+ - The right array has length < [max_length].
+ *)
+
+ let empty = [||], [||]
+
+ let length (vl, vr) =
+ (max_length * Array.length vl) + Array.length vr
+
+ let make n x =
+ let k = n / max_length in
+ let r = n mod max_length in
+ let vl = Array.init k (fun _ -> Array.make max_length x) in
+ let vr = Array.make r x in
+ (vl, vr)
+
+ let get (vl, vr) n =
+ let k = n / max_length in
+ let r = n mod max_length in
+ let len = Array.length vl in
+ if k < len then vl.(k).(r)
+ else if k == len then vr.(r)
+ else invalid_arg "index out of bounds"
+
+ let set (vl, vr) n x =
+ let k = n / max_length in
+ let r = n mod max_length in
+ let len = Array.length vl in
+ if k < len then vl.(k).(r) <- x
+ else if k == len then vr.(r) <- x
+ else invalid_arg "index out of bounds"
+
+end
+
type repr =
| RInt of int
| RBlock of (int * int) (* tag × len *)
@@ -82,7 +131,7 @@ end
module type S =
sig
type input
- val parse : input -> (data * obj array)
+ val parse : input -> (data * obj LargeArray.t)
end
module Make(M : Input) =
@@ -261,7 +310,7 @@ let parse_object chan =
let parse chan =
let (magic, len, _, _, size) = parse_header chan in
let () = assert (magic = magic_number) in
- let memory = Array.make size (Struct ((-1), [||])) in
+ let memory = LargeArray.make size (Struct ((-1), [||])) in
let current_object = ref 0 in
let fill_obj = function
| RPointer n ->
@@ -272,7 +321,7 @@ let parse chan =
data, None
| RString s ->
let data = Ptr !current_object in
- let () = memory.(!current_object) <- String s in
+ let () = LargeArray.set memory !current_object (String s) in
let () = incr current_object in
data, None
| RBlock (tag, 0) ->
@@ -282,7 +331,7 @@ let parse chan =
| RBlock (tag, len) ->
let data = Ptr !current_object in
let nblock = Array.make len (Atm (-1)) in
- let () = memory.(!current_object) <- Struct (tag, nblock) in
+ let () = LargeArray.set memory !current_object (Struct (tag, nblock)) in
let () = incr current_object in
data, Some nblock
| RCode addr ->
@@ -343,3 +392,32 @@ module PString = Make(IString)
let parse_channel = PChannel.parse
let parse_string s = PString.parse (s, ref 0)
+
+let instantiate (p, mem) =
+ let len = LargeArray.length mem in
+ let ans = LargeArray.make len (Obj.repr 0) in
+ (** First pass: initialize the subobjects *)
+ 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)
+ | String str -> Obj.repr str
+ in
+ LargeArray.set ans i obj
+ done;
+ let get_data = function
+ | Int n -> Obj.repr n
+ | Ptr p -> LargeArray.get ans p
+ | Atm tag -> Obj.new_block tag 0
+ | Fun _ -> assert false (** We shouldn't serialize closures *)
+ in
+ (** Second pass: set the pointers *)
+ for i = 0 to len - 1 do
+ match LargeArray.get mem i with
+ | Struct (_, blk) ->
+ let obj = LargeArray.get ans i in
+ for k = 0 to Array.length blk - 1 do
+ Obj.set_field obj k (get_data blk.(k))
+ done
+ | String _ -> ()
+ done;
+ get_data p
diff --git a/checker/analyze.mli b/checker/analyze.mli
index 42efcf01d..9c837643f 100644
--- a/checker/analyze.mli
+++ b/checker/analyze.mli
@@ -8,8 +8,20 @@ type obj =
| Struct of int * data array (* tag × data *)
| String of string
-val parse_channel : in_channel -> (data * obj array)
-val parse_string : string -> (data * obj array)
+module LargeArray :
+sig
+ type 'a t
+ val empty : 'a t
+ val length : 'a t -> int
+ val make : int -> 'a -> 'a t
+ val get : 'a t -> int -> 'a
+ val set : 'a t -> int -> 'a -> unit
+end
+(** A data structure similar to arrays but allowing to overcome the 2^22 length
+ limitation on 32-bit architecture. *)
+
+val parse_channel : in_channel -> (data * obj LargeArray.t)
+val parse_string : string -> (data * obj LargeArray.t)
(** {6 Functorized version} *)
@@ -26,10 +38,13 @@ end
module type S =
sig
type input
- val parse : input -> (data * obj array)
+ val parse : input -> (data * obj LargeArray.t)
(** Return the entry point and the reification of the memory out of a
marshalled structure. *)
end
module Make (M : Input) : S with type input = M.t
(** Functorized version of the previous code. *)
+
+val instantiate : data * obj LargeArray.t -> Obj.t
+(** Create the OCaml object out of the reified representation. *)
diff --git a/checker/check.ml b/checker/check.ml
index a00ec3b0e..82341ad9b 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -301,18 +301,27 @@ let name_clash_message dir mdir f =
(* Dependency graph *)
let depgraph = ref LibraryMap.empty
+let marshal_in_segment f ch =
+ try
+ let stop = input_binary_int ch in
+ let v = Analyze.instantiate (Analyze.parse_channel ch) in
+ let digest = Digest.input ch in
+ Obj.obj v, stop, digest
+ with _ ->
+ user_err (str "Corrupted file " ++ quote (str f))
+
let intern_from_file (dir, f) =
Flags.if_verbose chk_pp (str"[intern "++str f++str" ...");
let (sd,md,table,opaque_csts,digest) =
try
let ch = System.with_magic_number_check raw_intern_library f in
- let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in
- let (md:Cic.library_disk), _, digest = 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
+ let (sd:Cic.summary_disk), _, digest = marshal_in_segment f ch in
+ let (md:Cic.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 (tasks:'a option), _, _ = marshal_in_segment f ch in
let (table:Cic.opaque_table), pos, checksum =
- System.marshal_in_segment f ch in
+ marshal_in_segment f ch in
(* Verification of the final checksum *)
let () = close_in ch in
let ch = open_in_bin f in
diff --git a/checker/check.mllib b/checker/check.mllib
index 488507a13..f79ba66e3 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -1,5 +1,6 @@
Coq_config
+Analyze
Hook
Terminal
Canary
diff --git a/checker/closure.ml b/checker/closure.ml
index 7982ffa7a..3a56bba01 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -279,7 +279,6 @@ and fterm =
| FProj of projection * fconstr
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
- | FCase of case_info * fconstr * fconstr * fconstr array
| FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
| FLambda of int * (Name.t * constr) list * constr * fconstr subs
| FProd of Name.t * fconstr * fconstr
@@ -306,7 +305,6 @@ let update v1 (no,t) =
type stack_member =
| Zapp of fconstr array
- | Zcase of case_info * fconstr * fconstr array
| ZcaseT of case_info * constr * constr array * fconstr subs
| Zproj of int * int * projection
| Zfix of fconstr * stack
@@ -456,13 +454,10 @@ let rec to_constr constr_fun lfts v =
| FFlex (ConstKey op) -> Const op
| FInd op -> Ind op
| FConstruct op -> Construct op
- | FCase (ci,p,c,ve) ->
- Case (ci, constr_fun lfts p,
- constr_fun lfts c,
- Array.map (constr_fun lfts) ve)
- | FCaseT (ci,p,c,ve,e) -> (* TODO: enable sharing, cf FCLOS below ? *)
- to_constr constr_fun lfts
- {norm=Red;term=FCase(ci,mk_clos2 e p,c,mk_clos_vect e ve)}
+ | FCaseT (ci,p,c,ve,e) ->
+ let fp = mk_clos2 e p in
+ let fve = mk_clos_vect e ve in
+ Case (ci, constr_fun lfts fp, constr_fun lfts c, Array.map (constr_fun lfts) fve)
| FFix ((op,(lna,tys,bds)),e) ->
let n = Array.length bds in
let ftys = Array.map (mk_clos e) tys in
@@ -532,9 +527,6 @@ let rec zip m stk =
match stk with
| [] -> m
| Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s
- | Zcase(ci,p,br)::s ->
- let t = FCase(ci, p, m, br) in
- zip {norm=neutr m.norm; term=t} s
| ZcaseT(ci,p,br,e)::s ->
let t = FCaseT(ci, p, m, br, e) in
zip {norm=neutr m.norm; term=t} s
@@ -616,7 +608,7 @@ let rec get_args n tys f e stk =
(* Eta expansion: add a reference to implicit surrounding lambda at end of stack *)
let rec eta_expand_stack = function
- | (Zapp _ | Zfix _ | Zcase _ | ZcaseT _ | Zproj _
+ | (Zapp _ | Zfix _ | ZcaseT _ | Zproj _
| Zshift _ | Zupdate _ as e) :: s ->
e :: eta_expand_stack s
| [] ->
@@ -720,7 +712,6 @@ let rec knh info m stk =
| FCLOS(t,e) -> knht info e t (zupdate m stk)
| FLOCKED -> assert false
| FApp(a,b) -> knh info a (append_stack b (zupdate m stk))
- | FCase(ci,p,t,br) -> knh info t (Zcase(ci,p,br)::zupdate m stk)
| FCaseT(ci,p,t,br,env) -> knh info t (ZcaseT(ci,p,br,env)::zupdate m stk)
| FFix(((ri,n),(_,_,_)),_) ->
(match get_nth_arg m ri.(n) stk with
@@ -778,10 +769,6 @@ let rec knr info m stk =
| None -> (set_norm m; (m,stk)))
| FConstruct((ind,c),u) when red_set info.i_flags fIOTA ->
(match strip_update_shift_app m stk with
- (depth, args, Zcase(ci,_,br)::s) ->
- assert (ci.ci_npar>=0);
- let rargs = drop_parameters depth ci.ci_npar args in
- kni info br.(c-1) (rargs@s)
| (depth, args, ZcaseT(ci,_,br,env)::s) ->
assert (ci.ci_npar>=0);
let rargs = drop_parameters depth ci.ci_npar args in
@@ -798,7 +785,7 @@ let rec knr info m stk =
| (_,args,s) -> (m,args@s))
| FCoFix _ when red_set info.i_flags fIOTA ->
(match strip_update_shift_app m stk with
- (_, args, (((Zcase _|ZcaseT _)::_) as stk')) ->
+ (_, args, (((ZcaseT _)::_) as stk')) ->
let (fxe,fxbd) = contract_fix_vect m.term in
knit info fxe fxbd (args@stk')
| (_,args,s) -> (m,args@s))
diff --git a/checker/closure.mli b/checker/closure.mli
index 957cc4adb..02d8b22fa 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -98,7 +98,6 @@ type fterm =
| FProj of projection * fconstr
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
- | FCase of case_info * fconstr * fconstr * fconstr array
| FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
| FLambda of int * (Name.t * constr) list * constr * fconstr subs
| FProd of Name.t * fconstr * fconstr
@@ -115,7 +114,6 @@ type fterm =
type stack_member =
| Zapp of fconstr array
- | Zcase of case_info * fconstr * fconstr array
| ZcaseT of case_info * constr * constr array * fconstr subs
| Zproj of int * int * projection
| Zfix of fconstr * stack
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 6d8783d7e..9b8eac04c 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -42,8 +42,8 @@ let compare_stack_shape stk1 stk2 =
| (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2
| (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) ->
Int.equal bal 0 && compare_rec 0 s1 s2
- | ((Zcase(c1,_,_)|ZcaseT(c1,_,_,_))::s1,
- (Zcase(c2,_,_)|ZcaseT(c2,_,_,_))::s2) ->
+ | ((ZcaseT(c1,_,_,_))::s1,
+ (ZcaseT(c2,_,_,_))::s2) ->
bal=0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2
| (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
bal=0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
@@ -78,8 +78,7 @@ let pure_stack lfts stk =
(l, Zlfix((lfx,fx),pa)::pstk)
| (ZcaseT(ci,p,br,env),(l,pstk)) ->
(l,Zlcase(ci,l,mk_clos env p,mk_clos_vect env br)::pstk)
- | (Zcase(ci,p,br),(l,pstk)) ->
- (l,Zlcase(ci,l,p,br)::pstk)) in
+ ) in
snd (pure_rec lfts stk)
(****************************************************************************)
@@ -243,7 +242,6 @@ let rec no_arg_available = function
| Zshift _ :: stk -> no_arg_available stk
| Zapp v :: stk -> Array.length v = 0 && no_arg_available stk
| Zproj _ :: _ -> true
- | Zcase _ :: _ -> true
| ZcaseT _ :: _ -> true
| Zfix _ :: _ -> true
@@ -256,7 +254,6 @@ let rec no_nth_arg_available n = function
if n >= k then no_nth_arg_available (n-k) stk
else false
| Zproj _ :: _ -> true
- | Zcase _ :: _ -> true
| ZcaseT _ :: _ -> true
| Zfix _ :: _ -> true
@@ -266,13 +263,12 @@ let rec no_case_available = function
| Zshift _ :: stk -> no_case_available stk
| Zapp _ :: stk -> no_case_available stk
| Zproj (_,_,_) :: _ -> false
- | Zcase _ :: _ -> false
| ZcaseT _ :: _ -> false
| Zfix _ :: _ -> true
let in_whnf (t,stk) =
match fterm_of t with
- | (FLetIn _ | FCase _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false
+ | (FLetIn _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false
| FLambda _ -> no_arg_available stk
| FConstruct _ -> no_case_available stk
| FCoFix _ -> no_case_available stk
@@ -504,8 +500,8 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
else raise NotConvertible
(* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
- | ( (FLetIn _, _) | (FCase _,_) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
- | (_, FLetIn _) | (_,FCase _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
+ | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
+ | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
| (FLOCKED,_) | (_,FLOCKED) ) -> assert false
(* In all other cases, terms are not convertible *)
diff --git a/checker/votour.ml b/checker/votour.ml
index b7c898232..77c9999c4 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -77,8 +77,8 @@ struct
type obj = data
- let memory = ref [||]
- let sizes = ref [||]
+ let memory = ref LargeArray.empty
+ let sizes = ref LargeArray.empty
(** size, in words *)
let ws = Sys.word_size / 8
@@ -86,10 +86,10 @@ struct
let rec init_size seen k = function
| Int _ | Atm _ | Fun _ -> k 0
| Ptr p ->
- if seen.(p) then k 0
+ if LargeArray.get seen p then k 0
else
- let () = seen.(p) <- true in
- match (!memory).(p) with
+ let () = LargeArray.set seen p true in
+ match LargeArray.get !memory p with
| Struct (tag, os) ->
let len = Array.length os in
let rec fold i accu k =
@@ -97,30 +97,30 @@ struct
else
init_size seen (fun n -> fold (succ i) (accu + 1 + n) k) os.(i)
in
- fold 0 1 (fun size -> let () = (!sizes).(p) <- size in k size)
+ fold 0 1 (fun size -> let () = LargeArray.set !sizes p size in k size)
| String s ->
let size = 2 + (String.length s / ws) in
- let () = (!sizes).(p) <- size in
+ let () = LargeArray.set !sizes p size in
k size
let size = function
| Int _ | Atm _ | Fun _ -> 0
- | Ptr p -> (!sizes).(p)
+ | Ptr p -> LargeArray.get !sizes p
let repr = function
| Int i -> INT i
| Atm t -> BLOCK (t, [||])
| Fun _ -> OTHER
| Ptr p ->
- match (!memory).(p) with
+ match LargeArray.get !memory p with
| Struct (tag, os) -> BLOCK (tag, os)
| String s -> STRING s
let input ch =
let obj, mem = parse_channel ch in
let () = memory := mem in
- let () = sizes := Array.make (Array.length mem) (-1) in
- let seen = Array.make (Array.length mem) false in
+ let () = sizes := LargeArray.make (LargeArray.length mem) (-1) in
+ let seen = LargeArray.make (LargeArray.length mem) false in
let () = init_size seen ignore obj in
obj
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 18:22:44 +0000