From 9907e296e21fdd9dc3fab2b84fe7159b35af654c Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 2 Jun 2016 16:11:03 +0200
Subject: Remove tabulation support from pretty-printing.

This mechanism relied on functions that are deprecated in recent versions
of ocaml. It was incorrectly used for the most part anyway. The only place
that was using tabulations correctly is "print_loadpath", so there is a
minor regression there: physical paths of short logical paths are no longer
aligned.
---
 kernel/cbytecodes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index a705e3004f..09afbb5758 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -278,7 +278,7 @@ and pp_bytecodes c =
   | Ksequence (l1, l2) :: c ->
       pp_bytecodes l1 ++ pp_bytecodes l2 ++  pp_bytecodes c
   | i :: c ->
-      tab () ++ pp_instr i ++ fnl () ++ pp_bytecodes c
+      pp_instr i ++ fnl () ++ pp_bytecodes c
 
 (*spiwack: moved this type in this file  because I needed it for
   retroknowledge which can't depend from cbytegen *)
-- 
cgit v1.2.3


From 3502cc7c3bbad154dbfe76558d411d2c76109668 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 5 Mar 2017 17:30:03 +0100
Subject: [future] Remove unused parameter greedy.

It was always set to `greedy:true`.
---
 kernel/opaqueproof.ml | 2 +-
 kernel/term_typing.ml | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel')

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 130f1eb039..f147ea3433 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -136,7 +136,7 @@ let dump (otab,_) =
   let disch_table = Array.make n a_discharge in
   let f2t_map = ref FMap.empty in
   Int.Map.iter (fun n (d,cu) ->
-    let c, u = Future.split2 ~greedy:true cu in
+    let c, u = Future.split2 cu in
     Future.sink u;
     Future.sink c;
     opaque_table.(n) <- c;
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 3a0d1a2a5e..a63eb33766 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -191,7 +191,7 @@ let infer_declaration ~trust env kn dcl =
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
-        Future.chain ~greedy:true ~pure:true body (fun ((body,uctx),side_eff) ->
+        Future.chain ~pure:true body (fun ((body,uctx),side_eff) ->
           let body, uctx, signatures =
             inline_side_effects env body uctx side_eff in
           let valid_signatures = check_signatures trust signatures in
@@ -416,7 +416,7 @@ let export_side_effects mb env ce =
       let { const_entry_body = body } = c in
       let _, eff = Future.force body in
       let ce = DefinitionEntry { c with
-        const_entry_body = Future.chain ~greedy:true ~pure:true body
+        const_entry_body = Future.chain ~pure:true body
           (fun (b_ctx, _) -> b_ctx, []) } in
       let not_exists (c,_,_,_) =
         try ignore(Environ.lookup_constant c env); false
@@ -498,7 +498,7 @@ let translate_local_def mb env id centry =
 let translate_mind env kn mie = Indtypes.check_inductive env kn mie
 
 let inline_entry_side_effects env ce = { ce with
-  const_entry_body = Future.chain ~greedy:true ~pure:true
+  const_entry_body = Future.chain ~pure:true
     ce.const_entry_body (fun ((body, ctx), side_eff) ->
       let body, ctx',_ = inline_side_effects env body ctx side_eff in
       (body, ctx'), []);
-- 
cgit v1.2.3


From 3a050f305293676ccf66d415ab386d9521f0f765 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 23 Feb 2017 04:04:33 +0100
Subject: [safe_string] kernel/term_typing

No functional change, we create the new string beforehand and
`id_of_string` will become a noop with `-safe-string`.
---
 kernel/term_typing.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 3a0d1a2a5e..b9cf8101da 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -76,8 +76,7 @@ let inline_side_effects env body ctx side_eff =
     let cbl = List.filter not_exists cbl in
     let cname c = 
       let name = string_of_con c in
-      for i = 0 to String.length name - 1 do
-        if name.[i] == '.' || name.[i] == '#' then name.[i] <- '_' done;
+      let name = String.map (fun c -> if c == '.' || c == '#' then '_' else c) name in
       Name (id_of_string name) in
     let rec sub c i x = match kind_of_term x with
       | Const (c', _) when eq_constant c c' -> mkRel i
-- 
cgit v1.2.3


From 6098d329afc1e212ff866212a8f7815969a460ad Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 23 Feb 2017 13:33:39 +0100
Subject: [safe-string] kernel/nativevalues

No functional change.
---
 kernel/nativevalues.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel')

diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 8093df3044..965ed67b07 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -491,12 +491,12 @@ let str_encode expr =
 let str_decode s =
   let mshl_expr_len = String.length s / 2 in
   let mshl_expr = Buffer.create mshl_expr_len in
-  let buf = String.create 2 in
+  let buf = Bytes.create 2 in
   for i = 0 to mshl_expr_len - 1 do
-    String.blit s (2*i) buf 0 2;
-    Buffer.add_char mshl_expr (bin_of_hex buf)
+    Bytes.blit_string s (2*i) buf 0 2;
+    Buffer.add_char mshl_expr (bin_of_hex (Bytes.to_string buf))
   done;
-  Marshal.from_string (Buffer.contents mshl_expr) 0
+  Marshal.from_bytes (Buffer.to_bytes mshl_expr) 0
 
 (** Retroknowledge, to be removed when we switch to primitive integers *)
 
-- 
cgit v1.2.3


From b087d133f7d6d091cce72190c05a9a09d5b37791 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 14 Mar 2017 21:24:53 +0100
Subject: [toplevel] Remove unusable option -notop

Maxime points out that -notop cannot be used as the kernel requires
all constants to belong into a module. Indeed:

```
$ rlwrap ./bin/coqtop -notop
Coq < Definition foo := True.
Toplevel input, characters 0-23:
> Definition foo := True.
> ^^^^^^^^^^^^^^^^^^^^^^^
Error: No session module started (use -top dir)
Coq < Module M. Definition foo := True. End M.
Module M is defined
Coq < Locate foo.
Constant If you see this, it's a bug.M.foo
  (shorter name to refer to it in current context is M.foo)
```

My rationale for the removal is that this kind of incomplete features
are often confusing to newcomers ─ it has happened to me many times ─
as it can be seen for example in #397 .
---
 kernel/safe_typing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e4b3fcbf1a..2312f891c5 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -71,7 +71,7 @@ module NamedDecl = Context.Named.Declaration
   - [env] : the underlying environment (cf Environ)
   - [modpath] : the current module name
   - [modvariant] :
-    * NONE before coqtop initialization (or when -notop is used)
+    * NONE before coqtop initialization
     * LIBRARY at toplevel of a compilation or a regular coqtop session
     * STRUCT (params,oldsenv) : inside a local module, with
       module parameters [params] and earlier environment [oldsenv]
-- 
cgit v1.2.3


From 581b8d52fe93d666045d4878a1b48dad916451ec Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 23 Feb 2017 04:09:33 +0100
Subject: [safe_string] kernel/cemitcodes

The `emitcodes` string type was used in both a functional and an
imperative way, so we have to handle it with care in order to preserve
the previous optimizations and semantics.
---
 kernel/cemitcodes.ml | 39 +++++++++++++++++++++++++--------------
 1 file changed, 25 insertions(+), 14 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index ad7a41a347..a0a13174ff 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -24,33 +24,45 @@ type reloc_info =
 type patch = reloc_info * int
 
 let patch_char4 buff pos c1 c2 c3 c4 = 
-  String.unsafe_set buff pos       c1;
-  String.unsafe_set buff (pos + 1) c2;
-  String.unsafe_set buff (pos + 2) c3;
-  String.unsafe_set buff (pos + 3) c4 
+  Bytes.unsafe_set buff pos       c1;
+  Bytes.unsafe_set buff (pos + 1) c2;
+  Bytes.unsafe_set buff (pos + 2) c3;
+  Bytes.unsafe_set buff (pos + 3) c4 
   
 let patch buff (pos, n) =
   patch_char4 buff pos 
     (Char.unsafe_chr n) (Char.unsafe_chr (n asr 8))  (Char.unsafe_chr (n asr 16))
     (Char.unsafe_chr (n asr 24))
 
+(* val patch_int : emitcodes -> ((\*pos*\)int * int) list -> emitcodes *)
 let patch_int buff patches =
   (* copy code *before* patching because of nested evaluations:
      the code we are patching might be called (and thus "concurrently" patched)
      and results in wrong results. Side-effects... *)
-  let buff = String.copy buff in
+  let buff = Bytes.of_string buff in
   let () = List.iter (fun p -> patch buff p) patches in
-  buff
+  (* Note: we follow the apporach suggested by Gabriel Scherer in
+     PR#136 here, and use unsafe as we own buff.
+
+     The crux of the question that avoids defining emitcodes just as a
+     Byte.t is the call to hcons in to_memory below. Even if disabling
+     this optimization has no visible time impact, test data shows
+     that the optimization is indeed triggered quite often so we
+     choose ugliness over altering the semantics.
+
+     Handle with care.
+  *)
+  Bytes.unsafe_to_string buff
 
 (* Buffering of bytecode *)
 
-let out_buffer = ref(String.create 1024)
+let out_buffer = ref(Bytes.create 1024)
 and out_position = ref 0
 
 let out_word b1 b2 b3 b4 =
   let p = !out_position in
-  if p >= String.length !out_buffer then begin
-    let len = String.length !out_buffer in
+  if p >= Bytes.length !out_buffer then begin
+    let len = Bytes.length !out_buffer in
     let new_len =
       if len <= Sys.max_string_length / 2
       then 2 * len
@@ -58,8 +70,8 @@ let out_word b1 b2 b3 b4 =
 	if len = Sys.max_string_length
 	then invalid_arg "String.create"  (* Pas la bonne exception .... *)
 	else Sys.max_string_length in
-    let new_buffer = String.create new_len in
-    String.blit !out_buffer 0 new_buffer 0 len;
+    let new_buffer = Bytes.create new_len in
+    Bytes.blit !out_buffer 0 new_buffer 0 len;
     out_buffer := new_buffer
   end;
   patch_char4 !out_buffer p (Char.unsafe_chr b1)
@@ -305,7 +317,7 @@ let init () =
   label_table := Array.make 16 (Label_undefined []);
   reloc_info := []
 
-type emitcodes = string
+type emitcodes = String.t
 
 let length = String.length
 
@@ -369,9 +381,8 @@ let to_memory (init_code, fun_code, fv) =
   init();
   emit init_code;
   emit fun_code;
-  let code = String.create !out_position in
-  String.unsafe_blit !out_buffer 0 code 0 !out_position;
   (** Later uses of this string are all purely functional *)
+  let code = Bytes.sub_string !out_buffer 0 !out_position in
   let code = CString.hcons code in
   let reloc = List.rev !reloc_info in
   Array.iter (fun lbl ->
-- 
cgit v1.2.3


From 7601ddc3500cae2da39883b339951205be19c41d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 23 Feb 2017 03:48:50 +0100
Subject: [safe_string] library/nameops

We add a more convenient API to create identifiers from mutable
strings. We cannot solve the `String.copy` deprecation problem until
we enable `-safe-string`.
---
 kernel/names.ml  | 5 +++++
 kernel/names.mli | 1 +
 2 files changed, 6 insertions(+)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index 1f138581cc..831b6ad46e 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -50,6 +50,11 @@ struct
   | None -> true
   | Some _ -> false
 
+  let of_bytes s =
+    let s = Bytes.to_string s in
+    check_soft s;
+    String.hcons s
+
   let of_string s =
     let () = check_soft s in
     let s = String.copy s in
diff --git a/kernel/names.mli b/kernel/names.mli
index 6b0a80625b..be9b9422b7 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -43,6 +43,7 @@ sig
   (** Check that a string may be converted to an identifier.
   @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *)
 
+  val of_bytes : bytes -> t
   val of_string : string -> t
   (** Converts a string into an identifier.
       @raise UserError if the string is not valid, or echo a warning if it contains invalid identifier characters.
-- 
cgit v1.2.3


From 5e2574cbef1ba132aacc73b4a079cc0b5584f589 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 23 Feb 2017 14:57:59 +0100
Subject: [safe-string] Enable -safe-string !

We now build Coq with `-safe-string`, which enforces functional use
of the `string` datatype. Coq was pretty safe in these regard so only
a few tweaks were needed.

- coq_makefile: build plugins with -safe-string too.
- `names.ml`: we remove `String.copy` uses, as they are not needed.
---
 kernel/names.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index 831b6ad46e..ee8d838da1 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -57,15 +57,13 @@ struct
 
   let of_string s =
     let () = check_soft s in
-    let s = String.copy s in
     String.hcons s
 
   let of_string_soft s =
     let () = check_soft ~warn:false s in
-    let s = String.copy s in
     String.hcons s
 
-  let to_string id = String.copy id
+  let to_string id = id
 
   let print id = str id
 
-- 
cgit v1.2.3


From d25b1431eb73a04bdfc0f1ad2922819b69bba93a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 20 Mar 2017 15:14:01 +0100
Subject: [misc] Remove warnings about String.set

The `a.[i] <- x` notation is deprecated and we were getting a couple
of warnings.
---
 kernel/cemitcodes.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index a0a13174ff..f2c3b402b3 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -106,10 +106,10 @@ let extend_label_table needed =
 
 let backpatch (pos, orig) =
   let displ = (!out_position - orig) asr 2 in
-  !out_buffer.[pos]   <- Char.unsafe_chr displ;
-  !out_buffer.[pos+1] <- Char.unsafe_chr (displ asr 8);
-  !out_buffer.[pos+2] <- Char.unsafe_chr (displ asr 16);
-  !out_buffer.[pos+3] <- Char.unsafe_chr (displ asr 24)
+  Bytes.set !out_buffer  pos    @@ Char.unsafe_chr displ;
+  Bytes.set !out_buffer (pos+1) @@ Char.unsafe_chr (displ asr 8);
+  Bytes.set !out_buffer (pos+2) @@ Char.unsafe_chr (displ asr 16);
+  Bytes.set !out_buffer (pos+3) @@ Char.unsafe_chr (displ asr 24)
 
 let define_label lbl =
   if lbl >= Array.length !label_table then extend_label_table lbl;
-- 
cgit v1.2.3


From 76c263b5eceac313ac2cdd3a3e7e2961876d3e31 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Mon, 20 Mar 2017 12:21:12 -0400
Subject: In the Kami project, that causes a stack overflow in one of the
 example files (ProcThreeStInl.v, when the final "Defined" runs). I've
 verified that the change here fixes the stack overflow there with Coq 8.5pl2.

In this version, all the recursive calls are in tail position. Instead of
taking a single list of instructions, `emit' here takes a curent list and a remaining
list of lists of instructions. That means the two calls elsewhere in the file now
add an empty list argument. The algorithm works on the current list until it's empty,
then works on the remaining lists. The most complex case is for Ksequence, where
one of the pieces becomes the new current list, and the other pieces are consed onto
the remaining sub-lists.
---
 kernel/cemitcodes.ml | 31 +++++++++++++++++--------------
 1 file changed, 17 insertions(+), 14 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index ad7a41a347..f13620e101 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -262,41 +262,44 @@ let emit_instr = function
   | Kstop ->
       out opSTOP
 
-(* Emission of a list of instructions. Include some peephole optimization. *)
+(* Emission of a current list and remaining lists of instructions. Include some peephole optimization. *)
 
-let rec emit = function
-  | [] -> ()
+let rec emit insns remaining = match insns with
+  | [] -> 
+     (match remaining with 
+       [] -> () 
+     | (first::rest) -> emit first rest)
   (* Peephole optimizations *)
   | Kpush :: Kacc n :: c ->
       if n < 8 then out(opPUSHACC0 + n) else (out opPUSHACC; out_int n);
-      emit c
+      emit c remaining
   | Kpush :: Kenvacc n :: c ->
       if n >= 1 && n <= 4
       then out(opPUSHENVACC1 + n - 1)
       else (out opPUSHENVACC; out_int n);
-      emit c
+      emit c remaining
   | Kpush :: Koffsetclosure ofs :: c ->
       if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2
       then out(opPUSHOFFSETCLOSURE0 + ofs / 2)
       else (out opPUSHOFFSETCLOSURE; out_int ofs);
-      emit c
+      emit c remaining
   | Kpush :: Kgetglobal id :: c ->
-      out opPUSHGETGLOBAL; slot_for_getglobal id; emit c
+      out opPUSHGETGLOBAL; slot_for_getglobal id; emit c remaining
   | Kpush :: Kconst (Const_b0 i) :: c ->
       if i >= 0 && i <= 3
       then out (opPUSHCONST0 + i)
       else (out opPUSHCONSTINT; out_int i);
-      emit c
+      emit c remaining
   | Kpush :: Kconst const :: c ->
       out opPUSHGETGLOBAL; slot_for_const const;
-      emit c
+      emit c remaining
   | Kpop n :: Kjump :: c ->
-      out opRETURN; out_int n; emit c
+      out opRETURN; out_int n; emit c remaining
   | Ksequence(c1,c2)::c ->
-      emit c1; emit c2;emit c
+      emit c1 (c2::c::remaining)
   (* Default case *)
   | instr :: c ->
-      emit_instr instr; emit c
+      emit_instr instr; emit c remaining
 
 (* Initialization *)
 
@@ -367,8 +370,8 @@ let repr_body_code = function
 
 let to_memory (init_code, fun_code, fv) =
   init();
-  emit init_code;
-  emit fun_code;
+  emit init_code [];
+  emit fun_code [];
   let code = String.create !out_position in
   String.unsafe_blit !out_buffer 0 code 0 !out_position;
   (** Later uses of this string are all purely functional *)
-- 
cgit v1.2.3


From 09c856a3bcb7369244202ed94db247f7abe84dad Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 21 Mar 2017 14:29:56 +0100
Subject: Do not typecheck twice the type of opaque constants.

I believe an unwanted shadowing was introduced by a4043608f704f0.
---
 kernel/term_typing.ml | 41 +++++++++++++++++------------------------
 1 file changed, 17 insertions(+), 24 deletions(-)

(limited to 'kernel')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 749b5dbafa..2d55803475 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -22,24 +22,6 @@ open Entries
 open Typeops
 open Fast_typeops
 
-let constrain_type env j poly subst = function
-  | `None -> 
-    if not poly then (* Old-style polymorphism *)
-      make_polymorphic_if_constant_for_ind env j
-    else RegularArity (Vars.subst_univs_level_constr subst j.uj_type)
-  | `Some t ->
-      let tj = infer_type env t in
-      let _ = judge_of_cast env j DEFAULTcast tj in
-	assert (eq_constr t tj.utj_val);
-	RegularArity (Vars.subst_univs_level_constr subst t)
-  | `SomeWJ (t, tj) ->
-      let tj = infer_type env t in
-      let _ = judge_of_cast env j DEFAULTcast tj in
-	assert (eq_constr t tj.utj_val);
-	RegularArity (Vars.subst_univs_level_constr subst t)
-
-let map_option_typ = function None -> `None | Some x -> `Some x
-
 (* Insertion of constants and parameters in environment. *)
 
 let mk_pure_proof c = (c, Univ.ContextSet.empty), []
@@ -193,15 +175,16 @@ let infer_declaration ~trust env kn dcl =
           let body, uctx, signatures =
             inline_side_effects env body uctx side_eff in
           let valid_signatures = check_signatures trust signatures in
-	  let env' = push_context_set uctx env in
+	  let env = push_context_set uctx env in
           let j =
-            let body,env',ectx = skip_trusted_seff valid_signatures body env' in
-            let j = infer env' body in
+            let body,env,ectx = skip_trusted_seff valid_signatures body env in
+            let j = infer env body in
             unzip ectx j in
           let j = hcons_j j in
 	  let subst = Univ.LMap.empty in
-          let _typ = constrain_type env' j c.const_entry_polymorphic subst
-	    (`SomeWJ (typ,tyj)) in
+          let _ = judge_of_cast env j DEFAULTcast tyj in
+          assert (eq_constr typ tyj.utj_val);
+          let _typ = RegularArity (Vars.subst_univs_level_constr subst typ) in
           feedback_completion_typecheck feedback_id;
           j.uj_val, uctx) in
       let def = OpaqueDef (Opaqueproof.create proofterm) in
@@ -221,7 +204,17 @@ let infer_declaration ~trust env kn dcl =
       let usubst, univs =
 	Univ.abstract_universes abstract (Univ.ContextSet.to_context ctx) in      
       let j = infer env body in
-      let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
+      let typ = match typ with
+        | None ->
+           if not c.const_entry_polymorphic then (* Old-style polymorphism *)
+             make_polymorphic_if_constant_for_ind env j
+           else RegularArity (Vars.subst_univs_level_constr usubst j.uj_type)
+        | Some t ->
+           let tj = infer_type env t in
+           let _ = judge_of_cast env j DEFAULTcast tj in
+           assert (eq_constr t tj.utj_val);
+           RegularArity (Vars.subst_univs_level_constr usubst t)
+      in
       let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
       let def = 
 	if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
-- 
cgit v1.2.3


From 6d416ea54fd26987188858bcf80461247b002a09 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 21 Mar 2017 14:30:58 +0100
Subject: Add a few comments in term_typing.ml.

---
 kernel/term_typing.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'kernel')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 2d55803475..b7597ba7fb 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -164,6 +164,10 @@ let infer_declaration ~trust env kn dcl =
       let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in
 	Undef nl, RegularArity t, None, poly, univs, false, ctx
 
+  (** Definition [c] is opaque (Qed), non polymorphic and with a specified type,
+      so we delay the typing and hash consing of its body.
+      Remark: when the universe quantification is given explicitly, we could
+      delay even in the polymorphic case.  *)
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true;
 		       const_entry_polymorphic = false} as c) ->
@@ -192,6 +196,7 @@ let infer_declaration ~trust env kn dcl =
 	c.const_entry_universes,
 	c.const_entry_inline_code, c.const_entry_secctx
 
+  (** Other definitions have to be processed immediately. *)
   | DefinitionEntry c ->
       let { const_entry_type = typ; const_entry_opaque = opaque } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
-- 
cgit v1.2.3


From ea8185d872f242f8ebf4274ebe550ed81107150a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 12 Mar 2017 19:57:48 +0100
Subject: Making the side_effects type opaque.

We move it from Entries to Term_typing and export the few functions needed
to manipulate it in this module.
---
 kernel/entries.mli     |  2 --
 kernel/safe_typing.ml  | 12 ++++++------
 kernel/safe_typing.mli |  2 +-
 kernel/term_typing.ml  | 17 ++++++++++++-----
 kernel/term_typing.mli |  7 ++++++-
 5 files changed, 25 insertions(+), 15 deletions(-)

(limited to 'kernel')

diff --git a/kernel/entries.mli b/kernel/entries.mli
index ea7c266bcd..5287a009e5 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -113,5 +113,3 @@ type side_effect = {
   from_env : Declarations.structure_body CEphemeron.key;
   eff      : side_eff;
 }
-
-type side_effects = side_effect list
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index bc1cb63d82..e3b87bbe1a 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -206,19 +206,19 @@ let get_opaque_body env cbo =
          Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
 
 type private_constant = Entries.side_effect
-type private_constants = private_constant list
+type private_constants = Term_typing.side_effects
 
 type private_constant_role = Term_typing.side_effect_role =
   | Subproof
   | Schema of inductive * string
 
-let empty_private_constants = []
-let add_private x xs = if List.mem_f Term_typing.equal_eff x xs then xs else x :: xs
-let concat_private xs ys = List.fold_right add_private xs ys
+let empty_private_constants = Term_typing.empty_seff
+let add_private = Term_typing.add_seff
+let concat_private = Term_typing.concat_seff
 let mk_pure_proof = Term_typing.mk_pure_proof
 let inline_private_constants_in_constr = Term_typing.inline_side_effects
 let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects
-let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x)
+let side_effects_of_private_constants = Term_typing.uniq_seff
 
 let private_con_of_con env c =
   let cbo = Environ.lookup_constant c env.env in
@@ -248,7 +248,7 @@ let universes_of_private eff =
      | Entries.SEsubproof (c, cb, e) ->
 	if cb.const_polymorphic then acc
 	else Univ.ContextSet.of_context cb.const_universes :: acc)
-   [] eff
+   [] (Term_typing.uniq_seff eff)
 
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 15ebc7d880..8bc47d6ce0 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -47,7 +47,7 @@ type private_constant_role =
   | Schema of inductive * string
 
 val side_effects_of_private_constants :
-  private_constants -> Entries.side_effects
+  private_constants -> Entries.side_effect list
 
 val empty_private_constants : private_constants
 val add_private : private_constant -> private_constants -> private_constants
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index b7597ba7fb..24da308b4f 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -37,13 +37,20 @@ let equal_eff e1 e2 =
           cl1 cl2
   | _ -> false
 
-let rec uniq_seff = function
+type side_effects = side_effect list
+
+let rec uniq_seff_aux = function
   | [] -> []
-  | x :: xs -> x :: uniq_seff (List.filter (fun y -> not (equal_eff x y)) xs)
+  | x :: xs -> x :: uniq_seff_aux (List.filter (fun y -> not (equal_eff x y)) xs)
 (* The list of side effects is in reverse order (most recent first).
  * To keep the "topological" order between effects we have to uniq-ize from
  * the tail *)
-let uniq_seff l = List.rev (uniq_seff (List.rev l))
+let uniq_seff_rev l = List.rev (uniq_seff_aux (List.rev l))
+let uniq_seff l = List.rev (uniq_seff_aux l)
+
+let empty_seff = []
+let add_seff x xs = if List.mem_f equal_eff x xs then xs else x :: xs
+let concat_seff xs ys = List.fold_right add_seff xs ys
 
 let inline_side_effects env body ctx side_eff =
   let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } =
@@ -97,7 +104,7 @@ let inline_side_effects env body ctx side_eff =
     t, ctx, (mb,List.length cbl) :: sl
   in
   (* CAVEAT: we assure a proper order *)
-  List.fold_left handle_sideff (body,ctx,[]) (uniq_seff side_eff)
+  List.fold_left handle_sideff (body,ctx,[]) (uniq_seff_rev side_eff)
 
 (* Given the list of signatures of side effects, checks if they match.
  * I.e. if they are ordered descendants of the current revstruct *)
@@ -427,7 +434,7 @@ let export_side_effects mb env ce =
         let cbl = List.filter not_exists cbl in
         if cbl = [] then acc, sl
         else cbl :: acc, (mb,List.length cbl) :: sl in
-      let seff, signatures = List.fold_left aux ([],[]) (uniq_seff eff) in
+      let seff, signatures = List.fold_left aux ([],[]) (uniq_seff_rev eff) in
       let trusted = check_signatures mb signatures in
       let push_seff env = function
         | kn, cb, `Nothing, _ ->
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 89b5fc40e3..5330fb32ba 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -12,6 +12,8 @@ open Environ
 open Declarations
 open Entries
 
+type side_effects
+
 val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry ->
   constant_def * types * constant_universes
 
@@ -29,7 +31,10 @@ val inline_entry_side_effects :
     {!Entries.const_entry_body} field. It is meant to get a term out of a not
     yet type checked proof. *)
 
-val uniq_seff : side_effects -> side_effects
+val empty_seff : side_effects
+val add_seff : side_effect -> side_effects -> side_effects
+val concat_seff : side_effects -> side_effects -> side_effects
+val uniq_seff : side_effects -> side_effect list
 val equal_eff : side_effect -> side_effect -> bool
 
 val translate_constant :
-- 
cgit v1.2.3


From ee1546dc6686e888cc8da5f9442bcf788544dd0e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 12 Mar 2017 20:16:43 +0100
Subject: Using a dedicated datastructure for side effect ordering.

We were doing fishy things in the Term_typing file, where side-effects were
not considered in the right uniquization order because of the uniq_seff_rev
function. It probably did not matter after a9b76df because effects were
(mostly) uniquize upfront, but this is not clear because of the use of the
transparente API in the module.

Now everything has to go through the opaque API, so that a proper dependence
order is ensured.
---
 kernel/term_typing.ml | 66 ++++++++++++++++++++++++++++++++++++++-------------
 1 file changed, 49 insertions(+), 17 deletions(-)

(limited to 'kernel')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 24da308b4f..6ce14c853d 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -24,8 +24,6 @@ open Fast_typeops
 
 (* Insertion of constants and parameters in environment. *)
 
-let mk_pure_proof c = (c, Univ.ContextSet.empty), []
-
 let equal_eff e1 e2 =
   let open Entries in
   match e1, e2 with
@@ -37,20 +35,54 @@ let equal_eff e1 e2 =
           cl1 cl2
   | _ -> false
 
-type side_effects = side_effect list
+module SideEffects :
+sig
+  type t
+  val repr : t -> side_effect list
+  val empty : t
+  val add : side_effect -> t -> t
+  val concat : t -> t -> t
+end =
+struct
+
+let compare_seff e1 e2 = match e1, e2 with
+| SEsubproof (c1, _, _), SEsubproof (c2, _, _) -> Constant.CanOrd.compare c1 c2
+| SEscheme (cl1, _), SEscheme (cl2, _) ->
+  let cmp (_, c1, _, _) (_, c2, _, _) = Constant.CanOrd.compare c1 c2 in
+  CList.compare cmp cl1 cl2
+| SEsubproof _, SEscheme _ -> -1
+| SEscheme _, SEsubproof _ -> 1
+
+module SeffOrd = struct
+type t = side_effect
+let compare e1 e2 = compare_seff e1.eff e2.eff
+end
+
+module SeffSet = Set.Make(SeffOrd)
+
+type t = { seff : side_effect list; elts : SeffSet.t }
+(** Invariant: [seff] is a permutation of the elements of [elts] *)
+
+let repr eff = eff.seff
+let empty = { seff = []; elts = SeffSet.empty }
+let add x es =
+  if SeffSet.mem x es.elts then es
+  else { seff = x :: es.seff; elts = SeffSet.add x es.elts }
+let concat xes yes =
+  List.fold_right add xes.seff yes
+
+end
+
+type side_effects = SideEffects.t
+
+let uniq_seff_rev = SideEffects.repr
+let uniq_seff l = List.rev (SideEffects.repr l)
 
-let rec uniq_seff_aux = function
-  | [] -> []
-  | x :: xs -> x :: uniq_seff_aux (List.filter (fun y -> not (equal_eff x y)) xs)
-(* The list of side effects is in reverse order (most recent first).
- * To keep the "topological" order between effects we have to uniq-ize from
- * the tail *)
-let uniq_seff_rev l = List.rev (uniq_seff_aux (List.rev l))
-let uniq_seff l = List.rev (uniq_seff_aux l)
+let empty_seff = SideEffects.empty
+let add_seff = SideEffects.add
+let concat_seff = SideEffects.concat
 
-let empty_seff = []
-let add_seff x xs = if List.mem_f equal_eff x xs then xs else x :: xs
-let concat_seff xs ys = List.fold_right add_seff xs ys
+let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff
 
 let inline_side_effects env body ctx side_eff =
   let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } =
@@ -388,7 +420,7 @@ let constant_entry_of_side_effect cb u =
     | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty
     | _ -> assert false in
   DefinitionEntry {
-    const_entry_body = Future.from_val (pt, []);
+    const_entry_body = Future.from_val (pt, empty_seff);
     const_entry_secctx = None;
     const_entry_feedback = None;
     const_entry_type =
@@ -422,7 +454,7 @@ let export_side_effects mb env ce =
       let _, eff = Future.force body in
       let ce = DefinitionEntry { c with
         const_entry_body = Future.chain ~greedy:true ~pure:true body
-          (fun (b_ctx, _) -> b_ctx, []) } in
+          (fun (b_ctx, _) -> b_ctx, empty_seff) } in
       let not_exists (c,_,_,_) =
         try ignore(Environ.lookup_constant c env); false
         with Not_found -> true in 
@@ -507,7 +539,7 @@ let inline_entry_side_effects env ce = { ce with
   const_entry_body = Future.chain ~greedy:true ~pure:true
     ce.const_entry_body (fun ((body, ctx), side_eff) ->
       let body, ctx',_ = inline_side_effects env body ctx side_eff in
-      (body, ctx'), []);
+      (body, ctx'), empty_seff);
 }
 
 let inline_side_effects env body side_eff =
-- 
cgit v1.2.3


From 91dbe4af7b2a435142dcf40902082f90f07cc8be Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 20 Mar 2017 08:48:22 +0100
Subject: Documenting the API of side-effects.

---
 kernel/safe_typing.mli | 7 +++++++
 kernel/term_typing.mli | 5 +++++
 2 files changed, 12 insertions(+)

(limited to 'kernel')

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 8bc47d6ce0..efeb98bd25 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -48,10 +48,17 @@ type private_constant_role =
 
 val side_effects_of_private_constants :
   private_constants -> Entries.side_effect list
+(** Return the list of individual side-effects in the order of their
+    creation. *)
 
 val empty_private_constants : private_constants
 val add_private : private_constant -> private_constants -> private_constants
+(** Add a constant to a list of private constants. The former must be more
+    recent than all constants appearing in the latter, i.e. one should not
+    create a dependency cycle. *)
 val concat_private : private_constants -> private_constants -> private_constants
+(** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in
+    [e1] must be more recent than those of [e2]. *)
 
 val private_con_of_con : safe_environment -> constant -> private_constant
 val private_con_of_scheme : kind:string -> safe_environment -> (inductive * constant) list -> private_constant
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 5330fb32ba..075389ea53 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -34,7 +34,12 @@ val inline_entry_side_effects :
 val empty_seff : side_effects
 val add_seff : side_effect -> side_effects -> side_effects
 val concat_seff : side_effects -> side_effects -> side_effects
+(** [concat_seff e1 e2] adds the side-effects of [e1] to [e2], i.e. effects in
+    [e1] must be more recent than those of [e2]. *)
 val uniq_seff : side_effects -> side_effect list
+(** Return the list of individual side-effects in the order of their
+    creation. *)
+
 val equal_eff : side_effect -> side_effect -> bool
 
 val translate_constant :
-- 
cgit v1.2.3