From 20481a3f3405f04b47c7865ca2788a6f63660443 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 14 Jan 2018 02:20:42 +0100 Subject: Actually use the strategy information in the checker. --- checker/closure.ml | 1 + checker/closure.mli | 2 ++ checker/environ.ml | 15 +++++++++++++-- checker/environ.mli | 5 +++++ checker/indtypes.ml | 6 ++++-- checker/mod_checking.ml | 11 +++++++++-- checker/reduction.ml | 30 ++++++++++++++++++++++++------ 7 files changed, 58 insertions(+), 12 deletions(-) (limited to 'checker') 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 -> -- cgit v1.2.3