From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2015 10:36:12 +0200 Subject: Imported Upstream version 8.5~beta2+dfsg --- checker/check.ml | 2 +- checker/checker.ml | 3 +- checker/cic.mli | 2 +- checker/declarations.ml | 2 +- checker/indtypes.ml | 1 - checker/reduction.ml | 10 +++- checker/safe_typing.ml | 3 +- checker/univ.ml | 43 ++++++++------ checker/values.ml | 43 +++++++++++--- checker/votour.ml | 154 ++++++++++++++++++++++++++++++++++-------------- 10 files changed, 185 insertions(+), 78 deletions(-) (limited to 'checker') diff --git a/checker/check.ml b/checker/check.ml index 9a750858..3e22c4b1 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -321,7 +321,7 @@ let intern_from_file (dir, f) = System.marshal_in_segment f ch in (* Verification of the final checksum *) let () = close_in ch in - let ch = open_in f in + let ch = open_in_bin f in if not (String.equal (Digest.channel ch pos) checksum) then errorlabstrm "intern_from_file" (str "Checksum mismatch"); let () = close_in ch in diff --git a/checker/checker.ml b/checker/checker.ml index ffe15531..9a1007ac 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -181,8 +181,7 @@ let print_usage_channel co command = " -I dir -as coqdir map physical dir to logical coqdir\ \n -I dir map directory dir to the empty logical path\ \n -include dir (idem)\ -\n -R dir -as coqdir recursively map physical dir to logical coqdir\ -\n -R dir coqdir (idem)\ +\n -R dir coqdir recursively map physical dir to logical coqdir\ \n\ \n -admit module load module and dependencies without checking\ \n -norec module check module but admit dependencies without checking\ diff --git a/checker/cic.mli b/checker/cic.mli index a793fefa..90a0e9fe 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -333,7 +333,7 @@ type ('ty,'a) functorize = type with_declaration = | WithMod of Id.t list * module_path - | WithDef of Id.t list * constr + | WithDef of Id.t list * (constr * Univ.universe_context) type module_alg_expr = | MEident of module_path diff --git a/checker/declarations.ml b/checker/declarations.ml index c6709a78..8d913475 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -583,7 +583,7 @@ let implem_map fs fa = function let subst_with_body sub = function | WithMod(id,mp) -> WithMod(id,subst_mp sub mp) - | WithDef(id,c) -> WithDef(id,subst_mps sub c) + | WithDef(id,(c,ctx)) -> WithDef(id,(subst_mps sub c,ctx)) let rec subst_expr sub = function | MEident mp -> MEident (subst_mp sub mp) diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 2ce9f038..050c33e6 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -230,7 +230,6 @@ let compute_elim_sorts env_ar params mib arity lc = let infos = Array.map (sorts_of_constr_args env_params) lc in let (small,unit) = small_unit infos in (* We accept recursive unit types... *) - let unit = unit && mib.mind_ntypes = 1 in (* compute the max of the sorts of the products of the constructor type *) let level = max_inductive_sort (Array.concat (Array.to_list (Array.map Array.of_list infos))) in diff --git a/checker/reduction.ml b/checker/reduction.ml index 185c6edf..28fdb130 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -169,7 +169,15 @@ let sort_cmp univ pb s0 s1 = (match pb with | CONV -> Univ.check_eq univ u1 u2 | CUMUL -> Univ.check_leq univ u1 u2) - then raise NotConvertible + then begin + if !Flags.debug then begin + let op = match pb with CONV -> "=" | CUMUL -> "<=" in + Printf.eprintf "cort_cmp: %s\n%!" Pp.(string_of_ppcmds + (str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut() + ++ Univ.pr_universes univ)) + end; + raise NotConvertible + end | (_, _) -> raise NotConvertible let rec no_arg_available = function diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index 35f7f14b..810d6e0b 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -83,6 +83,7 @@ let import file clib univs digest = (* When the module is admitted, digests *must* match *) let unsafe_import file clib univs digest = let env = !genv in - check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps; + if !Flags.debug then check_imports msg_warning clib.comp_name env clib.comp_deps + else check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps; check_engagement env clib.comp_enga; full_add_module clib.comp_name clib.comp_mod univs digest diff --git a/checker/univ.ml b/checker/univ.ml index 5fed6dcd..3bcb3bc9 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -174,6 +174,16 @@ struct | _, Level _ -> 1 | Var n, Var m -> Int.compare n m + let hequal x y = + x == y || + match x, y with + | Prop, Prop -> true + | Set, Set -> true + | Level (n,d), Level (n',d') -> + n == n' && d == d' + | Var n, Var n' -> n == n' + | _ -> false + let hcons = function | Prop as x -> x | Set as x -> x @@ -211,27 +221,26 @@ module Level = struct let hash x = x.hash - let hcons x = - let data' = RawLevel.hcons x.data in - if data' == x.data then x - else { x with data = data' } - let data x = x.data (** Hashcons on levels + their hash *) - let make = - let module Self = struct - type _t = t - type t = _t - let equal = equal - let hash = hash - end in - let module WH = Weak.Make(Self) in - let pool = WH.create 4910 in fun x -> - let x = { hash = RawLevel.hash x; data = x } in - try WH.find pool x - with Not_found -> WH.add pool x; x + module Self = struct + type _t = t + type t = _t + type u = unit + let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data + let hash x = x.hash + let hashcons () x = + let data' = RawLevel.hcons x.data in + if x.data == data' then x else { x with data = data' } + end + + let hcons = + let module H = Hashcons.Make(Self) in + Hashcons.simple_hcons H.generate H.hcons () + + let make l = hcons { hash = RawLevel.hash l; data = l } let set = make Set let prop = make Prop diff --git a/checker/values.ml b/checker/values.ml index 3ca44b7d..cf93466b 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 0fbea8efeae581d87d977faa9eb2f421 checker/cic.mli +MD5 0a174243f8b06535c9eecbbe8d339fe1 checker/cic.mli *) @@ -270,7 +270,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body" let v_with = Sum ("with_declaration_body",0, [|[|List v_id;v_mp|]; - [|List v_id;v_constr|]|]) + [|List v_id;v_tuple "with_def" [|v_constr;v_context|]|]|]) let rec v_mae = Sum ("module_alg_expr",0, @@ -321,6 +321,33 @@ let v_libobj = Tuple ("libobj", [|v_id;v_obj|]) let v_libobjs = List v_libobj let v_libraryobjs = Tuple ("library_objects",[|v_libobjs;v_libobjs|]) +(** STM objects *) + +let v_frozen = Tuple ("frozen", [|List (v_pair Int Dyn); Opt Dyn|]) +let v_states = v_pair Any v_frozen +let v_state = Tuple ("state", [|v_states; Any; v_bool|]) + +let v_vcs = + let data = Opt Any in + let vcs = + Tuple ("vcs", + [|Any; Any; + Tuple ("dag", + [|Any; Any; v_map Any (Tuple ("state_info", + [|Any; Any; Opt v_state; v_pair data Any|])) + |]) + |]) + in + let () = Obj.set_field (Obj.magic data) 0 (Obj.magic vcs) in + vcs + +let v_uuid = Any +let v_request id doc = + Tuple ("request", [|Any; Any; doc; Any; id; String|]) +let v_tasks = List (v_pair (v_request v_uuid v_vcs) v_bool) +let v_counters = Any +let v_stm_seg = v_pair v_tasks v_counters + (** Toplevel structures in a vo (see Cic.mli) *) let v_lib = @@ -332,19 +359,19 @@ let v_univopaques = (** Registering dynamic values *) -module StringOrd = +module IntOrd = struct - type t = string + type t = int let compare (x : t) (y : t) = compare x y end -module StringMap = Map.Make(StringOrd) +module IntMap = Map.Make(IntOrd) -let dyn_table : value StringMap.t ref = ref StringMap.empty +let dyn_table : value IntMap.t ref = ref IntMap.empty let register_dyn name t = - dyn_table := StringMap.add name t !dyn_table + dyn_table := IntMap.add name t !dyn_table let find_dyn name = - try StringMap.find name !dyn_table + try IntMap.find name !dyn_table with Not_found -> Any diff --git a/checker/votour.ml b/checker/votour.ml index 29593cb7..7c954d6f 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -10,11 +10,44 @@ open Values (** {6 Interactive visit of a vo} *) -(** Name of a value *) - -type dyn = { dyn_tag : string; dyn_obj : Obj.t; } +type 'a repr = +| INT of int +| STRING of string +| BLOCK of int * 'a array +| OTHER + +module type S = +sig + type obj + val input : in_channel -> obj + val repr : obj -> obj repr + val size : int list -> int +end + +module Repr : S = +struct + type obj = Obj.t + + let input chan = + let obj = input_value chan in + let () = CObj.register_shared_size obj in + obj + + let repr obj = + if Obj.is_block obj then + let tag = Obj.tag obj in + if tag = Obj.string_tag then STRING (Obj.magic obj) + else if tag < Obj.no_scan_tag then + let data = Obj.dup obj in + let () = Obj.set_tag data 0 in + BLOCK (tag, Obj.magic data) + else OTHER + else INT (Obj.magic obj) + + let size p = CObj.shared_size_of_pos p +end -let to_dyn obj = (Obj.magic obj : dyn) +(** Name of a value *) let rec get_name ?(extra=false) = function |Any -> "?" @@ -32,69 +65,101 @@ let rec get_name ?(extra=false) = function (** For tuples, its quite handy to display the inner 1st string (if any). Cf. [structure_body] for instance *) -let get_string_in_tuple v o = +let get_string_in_tuple o = try - for i = 0 to Array.length v - 1 do - if v.(i) = String then - failwith (" [.."^(Obj.magic (Obj.field o i) : string)^"..]"); + for i = 0 to Array.length o - 1 do + match Repr.repr o.(i) with + | STRING s -> + failwith (Printf.sprintf " [..%s..]" s) + | _ -> () done; "" with Failure s -> s (** Some details : tags, integer value for non-block, etc etc *) -let rec get_details v o = match v with - |String | Any when (Obj.is_block o && Obj.tag o = Obj.string_tag) -> - " [" ^ String.escaped (Obj.magic o : string) ^"]" - |Tuple (_,v) -> get_string_in_tuple v o - |(Sum _|Any) when Obj.is_block o -> - " [tag=" ^ string_of_int (Obj.tag o) ^"]" - |(Sum _|Any) -> - " [imm=" ^ string_of_int (Obj.magic o : int) ^"]" - |Int -> " [" ^ string_of_int (Obj.magic o : int) ^"]" - |Annot (s,v) -> get_details v o +let rec get_details v o = match v, Repr.repr o with + | (String | Any), STRING s -> + Printf.sprintf " [%s]" (String.escaped s) + |Tuple (_,v), BLOCK (_, o) -> get_string_in_tuple o + |(Sum _|Any), BLOCK (tag, _) -> + Printf.sprintf " [tag=%i]" tag + |(Sum _|Any), INT i -> + Printf.sprintf " [imm=%i]" i + |Int, INT i -> Printf.sprintf " [imm=%i]" i + |Annot (s,v), _ -> get_details v o |_ -> "" let node_info (v,o,p) = get_name ~extra:true v ^ get_details v o ^ - " (size "^ string_of_int (CObj.shared_size_of_pos p)^"w)" + " (size "^ string_of_int (Repr.size p)^"w)" (** Children of a block : type, object, position. For lists, we collect all elements of the list at once *) -let access_children vs o pos = - Array.mapi (fun i v -> v, Obj.field o i, i::pos) vs - +let access_children vs os pos = + if Array.length os = Array.length vs then + Array.mapi (fun i v -> v, os.(i), i::pos) vs + else raise Exit + +let access_list v o pos = + let rec loop o pos = match Repr.repr o with + | INT 0 -> [] + | BLOCK (0, [|hd; tl|]) -> + (v, hd, 0 :: pos) :: loop tl (1 :: pos) + | _ -> raise Exit + in + Array.of_list (loop o pos) + +let access_block o = match Repr.repr o with +| BLOCK (tag, os) -> (tag, os) +| _ -> raise Exit +let access_int o = match Repr.repr o with INT i -> i | _ -> raise Exit + +(** raises Exit if the object has not the expected structure *) let rec get_children v o pos = match v with - |Tuple (_,v) -> access_children v o pos - |Sum (_,_,vv) -> - if Obj.is_block o then access_children vv.(Obj.tag o) o pos - else [||] - |Array v -> access_children (Array.make (Obj.size o) v) o pos - |List v -> - let rec loop pos = function - | [] -> [] - | o :: ol -> (v,o,0::pos) :: loop (1::pos) ol - in - Array.of_list (loop pos (Obj.magic o : Obj.t list)) + |Tuple (_, v) -> + let (_, os) = access_block o in + access_children v os pos + |Sum (_, _, vv) -> + begin match Repr.repr o with + | BLOCK (tag, os) -> access_children vv.(tag) os pos + | INT _ -> [||] + | _ -> raise Exit + end + |Array v -> + let (_, os) = access_block o in + access_children (Array.make (Array.length os) v) os pos + |List v -> access_list v o pos |Opt v -> - if Obj.is_block o then [|v,Obj.field o 0,0::pos|] else [||] + begin match Repr.repr o with + | INT 0 -> [||] + | BLOCK (0, [|x|]) -> [|(v, x, 0 :: pos)|] + | _ -> raise Exit + end |String | Int -> [||] |Annot (s,v) -> get_children v o pos - |Any -> - if Obj.is_block o && Obj.tag o < Obj.no_scan_tag then - Array.init (Obj.size o) (fun i -> (Any,Obj.field o i,i::pos)) - else [||] + |Any -> raise Exit |Dyn -> - let t = to_dyn o in - let tpe = find_dyn t.dyn_tag in - [|(String, Obj.repr t.dyn_tag, 0 :: pos); (tpe, t.dyn_obj, 1 :: pos)|] + begin match Repr.repr o with + | BLOCK (0, [|id; o|]) -> + let n = access_int id in + let tpe = find_dyn n in + [|(Int, id, 0 :: pos); (tpe, o, 1 :: pos)|] + | _ -> raise Exit + end |Fail s -> failwith "forbidden" +let get_children v o pos = + try get_children v o pos + with Exit -> match Repr.repr o with + | BLOCK (_, os) -> Array.mapi (fun i o -> Any, o, i :: pos) os + | _ -> [||] + type info = { nam : string; typ : value; - obj : Obj.t; + obj : Repr.obj; pos : int list } @@ -154,7 +219,7 @@ let visit_vo f = {name="library"; pos=0; typ=Values.v_lib}; {name="univ constraints of opaque proofs"; pos=0;typ=Values.v_univopaques}; {name="discharging info"; pos=0; typ=Opt Any}; - {name="STM tasks"; pos=0; typ=Opt Any}; + {name="STM tasks"; pos=0; typ=Opt Values.v_stm_seg}; {name="opaque proofs"; pos=0; typ=Values.v_opaques}; |] in while true do @@ -176,8 +241,7 @@ let visit_vo f = let l = read_line () in let seg = int_of_string l in seek_in ch segments.(seg).pos; - let o = (input_value ch : Obj.t) in - let () = CObj.register_shared_size o in + let o = Repr.input ch in let () = init () in visit segments.(seg).typ o [] done -- cgit v1.2.3