Merge PR #6584: Implement the strategy mechanism in the checker

15 files changed, 94 insertions, 22 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 4a0e706aa..95dd18f5f 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -170,6 +170,17 @@ type set_predicativity = ImpredicativeSet | PredicativeSet
 
 type engagement = set_predicativity
 
+(** {6 Conversion oracle} *)
+
+type level = Expand | Level of int | Opaque
+
+type oracle = {
+  var_opacity : level Id.Map.t;
+  cst_opacity : level Cmap.t;
+  var_trstate : Id.Pred.t;
+  cst_trstate : Cpred.t;
+}
+
 (** {6 Representation of constants (Definition/Axiom) } *)
 
 
@@ -219,6 +230,7 @@ type typing_flags = {
   check_guarded : bool; (** If [false] then fixed points and co-fixed
                             points are assumed to be total. *)
   check_universes : bool; (** If [false] universe constraints are not checked *)
+  conv_oracle : oracle; (** Unfolding strategies for conversion *)
 }
 
 type constant_body = {
diff --git a/checker/closure.ml b/checker/closure.ml
index 3a56bba01..98f8c4a82 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -822,6 +822,7 @@ type clos_infos = fconstr infos
 
 let infos_env x = x.i_env
 let infos_flags x = x.i_flags
+let oracle_of_infos x = x.i_env.env_conv_oracle
 
 let create_clos_infos flgs env =
   create (fun _ -> inject) flgs env
diff --git a/checker/closure.mli b/checker/closure.mli
index 02d8b22fa..ce8c64e30 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -147,6 +147,8 @@ type clos_infos
 val create_clos_infos : reds -> env -> clos_infos
 val infos_env : clos_infos -> env
 val infos_flags : clos_infos -> reds
+val oracle_of_infos : clos_infos -> oracle
+
 
 (* Reduction function *)
 
diff --git a/checker/environ.ml b/checker/environ.ml
index 9db0d60e8..3830cd0dc 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -21,7 +21,15 @@ type env = {
     env_globals       : globals;
     env_rel_context   : rel_context;
     env_stratification : stratification;
-    env_imports : Cic.vodigest MPmap.t }
+    env_imports : Cic.vodigest MPmap.t;
+    env_conv_oracle : oracle; }
+
+let empty_oracle = {
+  var_opacity = Id.Map.empty;
+  cst_opacity = Cmap.empty;
+  var_trstate = Id.Pred.empty;
+  cst_trstate = Cpred.empty;
+}
 
 let empty_env = {
   env_globals =
@@ -34,7 +42,8 @@ let empty_env = {
   env_stratification =
   { env_universes = Univ.initial_universes;
     env_engagement = PredicativeSet };
-  env_imports = MPmap.empty }
+  env_imports = MPmap.empty;
+  env_conv_oracle = empty_oracle }
 
 let engagement env = env.env_stratification.env_engagement
 let universes env = env.env_stratification.env_universes
@@ -51,6 +60,8 @@ let set_engagement (impr_set as c) env =
   { env with env_stratification =
       { env.env_stratification with env_engagement = c } }
 
+let set_oracle env oracle = { env with env_conv_oracle = oracle }
+
 (* Digests *)
 
 let add_digest env dp digest =
diff --git a/checker/environ.mli b/checker/environ.mli
index 6bda838f8..ba62ed519 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -18,6 +18,7 @@ type env = {
   env_rel_context : rel_context;
   env_stratification : stratification;
   env_imports : Cic.vodigest MPmap.t;
+  env_conv_oracle : Cic.oracle;
 }
 val empty_env : env
 
@@ -25,6 +26,10 @@ val empty_env : env
 val engagement : env -> Cic.engagement
 val set_engagement : Cic.engagement -> env -> env
 
+(** Oracle *)
+
+val set_oracle : env -> Cic.oracle -> env
+
 (* Digests *)
 val add_digest : env -> DirPath.t -> Cic.vodigest -> env
 val lookup_digest : env -> DirPath.t -> Cic.vodigest
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 22c843812..bb0db8cfe 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -586,6 +586,8 @@ let check_inductive env kn mib =
       Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi)
   in
   let env = Environ.push_context ind_ctx env in
+  (** Locally set the oracle for further typechecking *)
+  let env0 = Environ.set_oracle env mib.mind_typing_flags.conv_oracle in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
   (* check mind_finite : always OK *)
   (* check mind_ntypes *)
@@ -593,13 +595,13 @@ let check_inductive env kn mib =
     user_err Pp.(str "not the right number of packets");
   (* check mind_params_ctxt *)
   let params = mib.mind_params_ctxt in
-  let _ = check_ctxt env params in
+  let _ = check_ctxt env0 params in
   (* check mind_nparams *)
   if rel_context_nhyps params <> mib.mind_nparams then
     user_err Pp.(str "number the right number of parameters");
   (* mind_packets *)
   (*  - check arities *)
-  let env_ar = typecheck_arity env params mib.mind_packets in
+  let env_ar = typecheck_arity env0 params mib.mind_packets in
   (*  - check constructor types *)
   Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets;
   (* check the inferred subtyping relation *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 4357a690e..7685863ea 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -26,6 +26,9 @@ let refresh_arity ar =
 
 let check_constant_declaration env kn cb =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ prcon kn);
+  (** Locally set the oracle for further typechecking *)
+  let oracle = env.env_conv_oracle in
+  let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in
   (** [env'] contains De Bruijn universe variables *)
   let env' =
     match cb.const_universes with
@@ -53,8 +56,12 @@ let check_constant_declaration env kn cb =
 	  conv_leq envty j ty)
     | None -> ()
   in
-  if constant_is_polymorphic cb then add_constant kn cb env
-  else add_constant kn cb env'
+  let env =
+    if constant_is_polymorphic cb then add_constant kn cb env
+    else add_constant kn cb env'
+  in
+  (** Reset the value of the oracle *)
+  Environ.set_oracle env oracle
 
 (** {6 Checking modules } *)
 
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 9b8eac04c..d4b258f58 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -276,11 +276,29 @@ let in_whnf (t,stk) =
     | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _ | FProj _) -> true
     | FLOCKED -> assert false
 
-let oracle_order fl1 fl2 =
-  match fl1,fl2 with
-      ConstKey c1, ConstKey c2 -> (*height c1 > height c2*)false
-    | _, ConstKey _ -> true
-    | _ -> false
+let default_level = Level 0
+
+let get_strategy { var_opacity; cst_opacity } = function
+  | VarKey id ->
+      (try Names.Id.Map.find id var_opacity
+      with Not_found -> default_level)
+  | ConstKey (c, _) ->
+      (try Names.Cmap.find c cst_opacity
+      with Not_found -> default_level)
+  | RelKey _ -> Expand
+
+let oracle_order infos l2r k1 k2 =
+  let o = Closure.oracle_of_infos infos in
+  match get_strategy o k1, get_strategy o k2 with
+  | Expand, Expand -> l2r
+  | Expand, (Opaque | Level _) -> true
+  | (Opaque | Level _), Expand -> false
+  | Opaque, Opaque -> l2r
+  | Level _, Opaque -> true
+  | Opaque, Level _ -> false
+  | Level n1, Level n2 ->
+     if Int.equal n1 n2 then l2r
+     else n1 < n2
 
 let unfold_projection infos p c =
   let pb = lookup_projection p (infos_env infos) in
@@ -339,7 +357,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
         with NotConvertible ->
           (* else the oracle tells which constant is to be expanded *)
           let (app1,app2) =
-            if oracle_order fl1 fl2 then
+            if oracle_order infos false fl1 fl2 then
               match unfold_reference infos fl1 with
               | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
               | None ->
diff --git a/checker/values.ml b/checker/values.ml
index 4698227ff..313067cb6 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 56ac4cade33eff3d26ed5cdadb580c7e checker/cic.mli
+MD5 483493b20fe91cc1bea4350a2db2f82d checker/cic.mli
 
 *)
 
@@ -70,6 +70,8 @@ let v_map vk vd =
 let v_hset v = v_map Int (v_set v)
 let v_hmap vk vd = v_map Int (v_map vk vd)
 
+let v_pred v = v_pair v_bool (v_set v)
+
 (* lib/future *)
 let v_computation f =
   Annot ("Future.computation",
@@ -199,6 +201,17 @@ let v_lazy_constr =
 let v_impredicative_set = v_enum "impr-set" 2
 let v_engagement = v_impredicative_set
 
+let v_conv_level =
+  v_sum "conv_level" 2 [|[|Int|]|]
+
+let v_oracle =
+  v_tuple "oracle" [|
+    v_map v_id v_conv_level;
+    v_hmap v_cst v_conv_level;
+    v_pred v_id;
+    v_pred v_cst;
+  |]
+
 let v_pol_arity =
   v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
 
@@ -213,7 +226,7 @@ let v_projbody =
 	    v_constr|]
 
 let v_typing_flags =
-  v_tuple "typing_flags" [|v_bool; v_bool|]
+  v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|]
 
 let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 7f4b85fd0..5b9e1a141 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -74,6 +74,7 @@ type typing_flags = {
   check_guarded : bool; (** If [false] then fixed points and co-fixed
                             points are assumed to be total. *)
   check_universes : bool; (** If [false] universe constraints are not checked *)
+  conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *)
 }
 
 (* some contraints are in constant_constraints, some other may be in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index d8768a0fc..9eed9efcb 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -15,9 +15,10 @@ module RelDecl = Context.Rel.Declaration
 (** Operations concernings types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
 
-let safe_flags = {
+let safe_flags oracle = {
   check_guarded = true;
   check_universes = true;
+  conv_oracle = oracle;
 }
 
 (** {6 Arities } *)
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 198831848..0eed11f49 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -67,7 +67,7 @@ val inductive_is_cumulative : mutual_inductive_body -> bool
 (** {6 Kernel flags} *)
 
 (** A default, safe set of flags for kernel type-checking *)
-val safe_flags : typing_flags
+val safe_flags : Conv_oracle.oracle -> typing_flags
 
 (** {6 Hash-consing} *)
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 1afab453a..3c86129fe 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -37,8 +37,10 @@ type env = Pre_env.env
 
 let pre_env env = env
 let env_of_pre_env env = env
-let oracle env = env.env_conv_oracle
-let set_oracle env o = { env with env_conv_oracle = o }
+let oracle env = env.env_typing_flags.conv_oracle
+let set_oracle env o =
+  let env_typing_flags = { env.env_typing_flags with conv_oracle = o } in
+  { env with env_typing_flags }
 
 let empty_named_context_val = empty_named_context_val
 
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index c5254b453..4ef89f8c0 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -75,7 +75,6 @@ type env = {
   env_nb_rel        : int;
   env_stratification : stratification;
   env_typing_flags  : typing_flags;
-  env_conv_oracle   : Conv_oracle.oracle;
   retroknowledge : Retroknowledge.retroknowledge;
   indirect_pterms : Opaqueproof.opaquetab;
 }
@@ -98,8 +97,7 @@ let empty_env = {
   env_stratification = {
     env_universes = UGraph.initial_universes;
     env_engagement = PredicativeSet };
-  env_typing_flags = Declareops.safe_flags;
-  env_conv_oracle = Conv_oracle.empty;
+  env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
   retroknowledge = Retroknowledge.initial_retroknowledge;
   indirect_pterms = Opaqueproof.empty_opaquetab }
 
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 054ae1743..fef530c87 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -53,7 +53,6 @@ type env = {
     env_nb_rel        : int;
     env_stratification : stratification;
     env_typing_flags  : typing_flags;
-    env_conv_oracle   : Conv_oracle.oracle;
     retroknowledge : Retroknowledge.retroknowledge;
     indirect_pterms : Opaqueproof.opaquetab;
 }