Merge remote-tracking branch 'upstream/trunk' into trunk

11 files changed, 116 insertions, 29 deletions

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index a6972c9500..54db58c01f 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -28,11 +28,11 @@
 ########################################################################
 # Mathclasses + Corn
 ########################################################################
-: ${math_classes_CI_BRANCH:=v8.6}
-: ${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git}
+: ${math_classes_CI_BRANCH:=external-bignums}
+: ${math_classes_CI_GITURL:=https://github.com/letouzey/math-classes.git}
 
-: ${Corn_CI_BRANCH:=v8.6}
-: ${Corn_CI_GITURL:=https://github.com/c-corn/corn.git}
+: ${Corn_CI_BRANCH:=external-bignums}
+: ${Corn_CI_GITURL:=https://github.com/letouzey/corn.git}
 
 ########################################################################
 # Iris
@@ -46,8 +46,8 @@
 ########################################################################
 # HoTT
 ########################################################################
-# Temporal overlay
-: ${HoTT_CI_BRANCH:=mz-8.7}
+# Temporary overlay
+: ${HoTT_CI_BRANCH:=ocaml.4.02.3}
 : ${HoTT_CI_GITURL:=https://github.com/ejgallego/HoTT.git}
 # : ${HoTT_CI_BRANCH:=master}
 # : ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git}
@@ -85,8 +85,8 @@
 ########################################################################
 # fiat_parsers
 ########################################################################
-: ${fiat_parsers_CI_BRANCH:=master}
-: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git}
+: ${fiat_parsers_CI_BRANCH:=trunk__API}
+: ${fiat_parsers_CI_GITURL:=https://github.com/matejkosik/fiat.git}
 
 ########################################################################
 # fiat_crypto
@@ -97,14 +97,14 @@
 ########################################################################
 # bedrock_src
 ########################################################################
-: ${bedrock_src_CI_BRANCH:=master}
-: ${bedrock_src_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
+: ${bedrock_src_CI_BRANCH:=trunk__API}
+: ${bedrock_src_CI_GITURL:=https://github.com/matejkosik/bedrock.git}
 
 ########################################################################
 # bedrock_facade
 ########################################################################
-: ${bedrock_facade_CI_BRANCH:=master}
-: ${bedrock_facade_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
+: ${bedrock_facade_CI_BRANCH:=trunk__API}
+: ${bedrock_facade_CI_GITURL:=https://github.com/matejkosik/bedrock.git}
 
 ########################################################################
 # formal-topology
@@ -113,6 +113,12 @@
 : ${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology.git}
 
 ########################################################################
+# coq-dpdgraph
+########################################################################
+: ${coq_dpdgraph_CI_BRANCH:=coq-trunk}
+: ${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git}
+
+########################################################################
 # CoLoR
 ########################################################################
 : ${Color_CI_SVNURL:=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color}
@@ -127,3 +133,9 @@
 ########################################################################
 : ${tlc_CI_BRANCH:=master}
 : ${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git}
+
+########################################################################
+# Bignums
+########################################################################
+: ${bignums_CI_BRANCH:=master}
+: ${bignums_CI_GITURL:=https://github.com/coq/bignums.git}
diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh
new file mode 100755
index 0000000000..ff5935d4c7
--- /dev/null
+++ b/dev/ci/ci-bignums.sh
@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+
+# This script could be included inside other ones
+# Let's avoid to source ci-common twice in this case
+if [ -z "${CI_BUILD_DIR}"];
+then
+    source ${ci_dir}/ci-common.sh
+fi
+
+bignums_CI_DIR=${CI_BUILD_DIR}/Bignums
+
+git_checkout ${bignums_CI_BRANCH} ${bignums_CI_GITURL} ${bignums_CI_DIR}
+
+( cd ${bignums_CI_DIR} && make -j ${NJOBS} && make install)
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index 3f0716511d..57f569858b 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -5,6 +5,17 @@ source ${ci_dir}/ci-common.sh
 
 Color_CI_DIR=${CI_BUILD_DIR}/color
 
+# Setup Bignums
+
+source ${ci_dir}/ci-bignums.sh
+
+# Compiles CoLoR
+
 svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR}
 
+sed -i -e "s/From Coq Require Import BigN/From Bignums Require Import BigN/" ${Color_CI_DIR}/Util/*/*.v
+sed -i -e "s/From Coq Require Export BigN/From Bignums Require Export BigN/" ${Color_CI_DIR}/Util/*/*.v
+sed -i -e "s/From Coq Require Import BigZ/From Bignums Require Import BigZ/" ${Color_CI_DIR}/Util/*/*.v
+sed -i -e "s/From Coq Require Export BigZ/From Bignums Require Export BigZ/" ${Color_CI_DIR}/Util/*/*.v
+
 ( cd ${Color_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh
new file mode 100755
index 0000000000..e8018158bf
--- /dev/null
+++ b/dev/ci/ci-coq-dpdgraph.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+coq_dpdgraph_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph
+
+git_checkout ${coq_dpdgraph_CI_BRANCH} ${coq_dpdgraph_CI_GITURL} ${coq_dpdgraph_CI_DIR}
+
+( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make -j ${NJOBS} && make tests && (make tests | tee tmp.log) && (if grep DIFFERENCES tmp.log ; then exit 1 ; else exit 0 ; fi) )
diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh
index ecb36349fb..64b78c0396 100755
--- a/dev/ci/ci-formal-topology.sh
+++ b/dev/ci/ci-formal-topology.sh
@@ -9,6 +9,10 @@ Corn_CI_DIR=${CI_BUILD_DIR}/corn
 
 formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology
 
+# Setup Bignums
+
+source ${ci_dir}/ci-bignums.sh
+
 # Setup Math-Classes
 
 git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index beb75773b7..46581c6381 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -7,6 +7,10 @@ math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes
 
 Corn_CI_DIR=${CI_BUILD_DIR}/corn
 
+# Setup Bignums
+
+source ${ci_dir}/ci-bignums.sh
+
 # Setup Math-Classes
 
 git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 195ede6d00..200d431bcb 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -30,3 +30,20 @@ if [ $TRAVIS_PULL_REQUEST == "669" ] || [ $TRAVIS_BRANCH == "ssr-merge" ]; then
     mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
 fi
 
+echo "DEBUG: ci-user-overlay.sh 0"
+if [ $TRAVIS_PULL_REQUEST = "707" ] || [ $TRAVIS_BRANCH == "trunk__API__coq_makefile" ]; then
+    echo "DEBUG: ci-user-overlay.sh 1"
+    bedrock_src_CI_BRANCH=trunk__API
+    bedrock_src_CI_GITURL=https://github.com/matejkosik/bedrock.git
+    bedrock_facade_CI_BRANCH=trunk__API
+    bedrock_facade_CI_GITURL=https://github.com/matejkosik/bedrock.git
+    fiat_parsers_CI_BRANCH=trunk__API
+    fiat_parsers_CI_GITURL=https://github.com/matejkosik/fiat.git
+fi
+
+if [ $TRAVIS_PULL_REQUEST == "498" ] || [ $TRAVIS_BRANCH == "outsource-bignums" ]; then
+    math_classes_CI_BRANCH=external-bignums
+    math_classes_CI_GITURL=https://github.com/letouzey/math-classes.git
+    Corn_CI_BRANCH=external-bignums
+    Corn_CI_GITURL=https://github.com/letouzey/corn.git
+fi
diff --git a/dev/core.dbg b/dev/core.dbg
index 6acdd01528..71d06cdb0a 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -17,4 +17,6 @@ load_printer vernac.cma
 load_printer stm.cma
 load_printer toplevel.cma
 load_printer highparsing.cma
+load_printer intf.cma
+load_printer API.cma
 load_printer ltac_plugin.cmo
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index bcda4ff50a..631b5f5aaf 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -10,6 +10,16 @@ will fail to compile now. They should switch to `Bytes.t`
 
 * ML API *
 
+Added two functions for declaring hooks to be executed in reduction
+functions when some given constants are traversed:
+
+  declare_reduction_effect: to declare a hook to be applied when some
+  constant are visited during the execution of some reduction functions
+  (primarily cbv).
+
+  set_reduction_effect: to declare a constant on which a given effect
+  hook should be called.
+
 We renamed the following functions:
 
   Context.Rel.Declaration.fold   -> Context.Rel.Declaration.fold_constr
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 3850c05fd9..f4799f7b2c 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -23,6 +23,7 @@ exec $OCAMLDEBUG \
 	-I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \
         -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
 	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \
+        -I $COQTOP/API \
         -I $COQTOP/plugins/cc         -I $COQTOP/plugins/dp \
         -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \
         -I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index a1b3c81b9a..6ae5125f6d 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -37,7 +37,7 @@ let pp   x = Pp.pp_with !Topfmt.std_ft x
 let ppfuture kx = pp (Future.print (fun _ -> str "_") kx)
 
 (* name printers *)
-let ppid id = pp (pr_id id)
+let ppid id = pp (Id.print id)
 let pplab l = pp (pr_lab l)
 let ppmbid mbid = pp (str (MBId.debug_to_string mbid))
 let ppdir dir = pp (pr_dirpath dir)
@@ -79,12 +79,12 @@ let ppbigint n = pp (str (Bigint.to_string n));;
 
 let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]"
 let ppintset l = pp (prset int (Int.Set.elements l))
-let ppidset l = pp (prset pr_id (Id.Set.elements l))
+let ppidset l = pp (prset Id.print (Id.Set.elements l))
 
 let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]"
 
 let pridmap pr l =
-  let pr (id,b) = pr_id id ++ str "=>" ++ pr id b in
+  let pr (id,b) = Id.print id ++ str "=>" ++ pr id b in
   prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l [])
 
 let ppidmap pr l = pp (pridmap pr l)
@@ -95,10 +95,10 @@ let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) ->
    (match copt with None -> mt () | Some c -> spc () ++ str "<expanded: " ++
     Termops.print_constr (EConstr.of_constr c) ++ str">") ++
    (if id = id0 then mt ()
-    else spc () ++ str "<canonical: " ++ pr_id id ++ str ">"))))
+    else spc () ++ str "<canonical: " ++ Id.print id ++ str ">"))))
 
-let prididmap = pridmap (fun _ -> pr_id)
-let ppididmap = ppidmap (fun _ -> pr_id)
+let prididmap = pridmap (fun _ -> Id.print)
+let ppididmap = ppidmap (fun _ -> Id.print)
 
 let prconstrunderbindersidmap = pridmap (fun _ (l,c) ->
   hov 1 (str"[" ++  prlist_with_sep spc Id.print l ++ str"]")
@@ -132,15 +132,15 @@ let safe_pr_global = function
 			  int i ++ str ")")
   | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ debug_pr_mind kn ++ str "," ++
 				      int i ++ str "," ++ int j ++ str ")")
-  | VarRef id -> pp (str "VARREF(" ++ pr_id id ++ str ")")
+  | VarRef id -> pp (str "VARREF(" ++ Id.print id ++ str ")")
 
 let ppglobal x = try pp(pr_global x) with _ -> safe_pr_global x
 
 let ppconst (sp,j) =
-    pp (str"#" ++ pr_kn sp ++ str"=" ++ pr_lconstr j.uj_val)
+    pp (str"#" ++ KerName.print sp ++ str"=" ++ pr_lconstr j.uj_val)
 
 let ppvar ((id,a)) =
-    pp (str"#" ++ pr_id id ++ str":" ++ pr_lconstr a)
+    pp (str"#" ++ Id.print id ++ str":" ++ pr_lconstr a)
 
 let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t)
 
@@ -538,21 +538,21 @@ let encode_path ?loc prefix mpdir suffix id =
   let dir = match mpdir with
     | None -> []
     | Some (mp,dir) ->
-	(DirPath.repr (dirpath_of_string (string_of_mp mp))@
+	(DirPath.repr (dirpath_of_string (ModPath.to_string mp))@
 	DirPath.repr dir) in
   Qualid (Loc.tag ?loc @@ make_qualid
     (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id)
 
 let raw_string_of_ref ?loc _ = function
   | ConstRef cst ->
-      let (mp,dir,id) = repr_con cst in
+      let (mp,dir,id) = Constant.repr3 cst in
       encode_path ?loc "CST" (Some (mp,dir)) [] (Label.to_id id)
   | IndRef (kn,i) ->
-      let (mp,dir,id) = repr_mind kn in
+      let (mp,dir,id) = MutInd.repr3 kn in
       encode_path ?loc "IND" (Some (mp,dir)) [Label.to_id id]
 	(Id.of_string ("_"^string_of_int i))
   | ConstructRef ((kn,i),j) ->
-      let (mp,dir,id) = repr_mind kn in
+      let (mp,dir,id) = MutInd.repr3 kn in
       encode_path ?loc "CSTR" (Some (mp,dir))
 	[Label.to_id id;Id.of_string ("_"^string_of_int i)]
 	(Id.of_string ("_"^string_of_int j))
@@ -561,14 +561,14 @@ let raw_string_of_ref ?loc _ = function
 
 let short_string_of_ref ?loc _ = function
   | VarRef id -> Ident (Loc.tag ?loc id)
-  | ConstRef cst -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (repr_con cst)))
-  | IndRef (kn,0) -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (repr_mind kn)))
+  | ConstRef cst -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (Constant.repr3 cst)))
+  | IndRef (kn,0) -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (MutInd.repr3 kn)))
   | IndRef (kn,i) ->
-      encode_path ?loc "IND" None [Label.to_id (pi3 (repr_mind kn))]
+      encode_path ?loc "IND" None [Label.to_id (pi3 (MutInd.repr3 kn))]
         (Id.of_string ("_"^string_of_int i))
   | ConstructRef ((kn,i),j) ->
       encode_path ?loc "CSTR" None
-        [Label.to_id (pi3 (repr_mind kn));Id.of_string ("_"^string_of_int i)]
+        [Label.to_id (pi3 (MutInd.repr3 kn));Id.of_string ("_"^string_of_int i)]
         (Id.of_string ("_"^string_of_int j))
 
 (* Anticipate that printers can be used from ocamldebug and that