Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

10 files changed, 185 insertions, 78 deletions

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