diff options
-rw-r--r-- | kernel/declarations.mli | 6 | ||||
-rw-r--r-- | kernel/declareops.ml | 4 | ||||
-rw-r--r-- | kernel/safe_typing.ml | 18 | ||||
-rw-r--r-- | kernel/term_typing.ml | 17 | ||||
-rw-r--r-- | library/declare.ml | 26 | ||||
-rw-r--r-- | stm/lemmas.ml | 4 | ||||
-rw-r--r-- | stm/stm.ml | 8 |
7 files changed, 44 insertions, 39 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index d908bcbe2..4f1672884 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -76,9 +76,11 @@ type constant_body = { const_proj : projection_body option; const_inline_code : bool } +type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] + type side_effect = - | SEsubproof of constant * constant_body - | SEscheme of (inductive * constant * constant_body) list * string + | SEsubproof of constant * constant_body * seff_env + | SEscheme of (inductive * constant * constant_body * seff_env) list * string (** {6 Representation of mutual inductive types in the kernel } *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index d99382129..e13fb4f08 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -298,9 +298,9 @@ let join_constant_body otab cb = | _ -> () let string_of_side_effect = function - | SEsubproof (c,_) -> Names.string_of_con c + | SEsubproof (c,_,_) -> Names.string_of_con c | SEscheme (cl,_) -> - String.concat ", " (List.map (fun (_,c,_) -> Names.string_of_con c) cl) + String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) type side_effects = side_effect list let no_seff = ([] : side_effects) let iter_side_effects f l = List.iter f (List.rev l) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 9aca7727b..11079d25b 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -195,10 +195,24 @@ let set_type_in_type senv = (** {6 Stm machinery } *) -let sideff_of_con env c = SEsubproof (c, Environ.lookup_constant c env.env) +let get_opauqe_body env cbo = + match cbo.const_body with + | Undef _ -> assert false + | Def _ -> `Nothing + | OpaqueDef opaque -> + `Opaque + (Opaqueproof.force_proof (Environ.opaque_tables env) opaque, + Opaqueproof.force_constraints (Environ.opaque_tables env) opaque) + +let sideff_of_con env c = + let cbo = Environ.lookup_constant c env.env in + SEsubproof (c, cbo, get_opauqe_body env.env cbo) let sideff_of_scheme kind env cl = SEscheme( - List.map (fun (i,c) -> i, c, Environ.lookup_constant c env.env) cl,kind) + List.map (fun (i,c) -> + let cbo = Environ.lookup_constant c env.env in + i, c, cbo, get_opauqe_body env.env cbo) cl, + kind) let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 415e91f70..8f41f356d 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -49,9 +49,9 @@ let mk_pure_proof c = (c, Univ.ContextSet.empty), Declareops.no_seff let handle_side_effects env body side_eff = let handle_sideff t se = let cbl = match se with - | SEsubproof (c,cb) -> [c,cb] - | SEscheme (cl,_) -> List.map (fun (_,c,cb) -> c,cb) cl in - let not_exists (c,_) = + | SEsubproof (c,cb,b) -> [c,cb,b] + | SEscheme (cl,_) -> List.map (fun (_,c,cb,b) -> c,cb,b) cl in + let not_exists (c,_,_) = try ignore(Environ.lookup_constant c env); false with Not_found -> true in let cbl = List.filter not_exists cbl in @@ -72,10 +72,9 @@ let handle_side_effects env body side_eff = (* Vars.subst_univs_level_constr subst b *) Vars.subst_instance_constr u' b | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub_body c u b i x) i x in - let fix_body (c,cb) t = - match cb.const_body with - | Undef _ -> assert false - | Def b -> + let fix_body (c,cb,b) t = + match cb.const_body, b with + | Def b, _ -> let b = Mod_subst.force_constr b in let poly = cb.const_polymorphic in if not poly then @@ -85,8 +84,7 @@ let handle_side_effects env body side_eff = else let univs = cb.const_universes in sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t) - | OpaqueDef b -> - let b = Opaqueproof.force_proof (opaque_tables env) b in + | OpaqueDef _, `Opaque (b,_) -> let poly = cb.const_polymorphic in if not poly then let b_ty = Typeops.type_of_constant_type env cb.const_type in @@ -95,6 +93,7 @@ let handle_side_effects env body side_eff = else let univs = cb.const_universes in sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t) + | _ -> assert false in List.fold_right fix_body cbl t in diff --git a/library/declare.ml b/library/declare.ml index 4ec81c49f..fb6e1c9b8 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -200,24 +200,22 @@ let declare_scheme = ref (fun _ _ -> assert false) let set_declare_scheme f = declare_scheme := f let declare_sideff env fix_exn se = let cbl, scheme = match se with - | SEsubproof (c, cb) -> [c, cb], None + | SEsubproof (c, cb, pt) -> [c, cb, pt], None | SEscheme (cbl, k) -> - List.map (fun (_,c,cb) -> c,cb) cbl, Some (cbl,k) in + List.map (fun (_,c,cb,pt) -> c,cb,pt) cbl, Some (cbl,k) in let id_of c = Names.Label.to_id (Names.Constant.label c) in - let pt_opaque_of cb = - match cb with - | { const_body = Def sc } -> (Mod_subst.force_constr sc, Univ.ContextSet.empty), false - | { const_body = OpaqueDef fc } -> - (Opaqueproof.force_proof (Environ.opaque_tables env) fc, - Opaqueproof.force_constraints (Environ.opaque_tables env) fc), true - | { const_body = Undef _ } -> anomaly(str"Undefined side effect") + let pt_opaque_of cb pt = + match cb, pt with + | { const_body = Def sc }, _ -> (Mod_subst.force_constr sc, Univ.ContextSet.empty), false + | { const_body = OpaqueDef _ }, `Opaque(pt,univ) -> (pt, univ), true + | _ -> assert false in let ty_of cb = match cb.Declarations.const_type with | Declarations.RegularArity t -> Some t | Declarations.TemplateArity _ -> None in - let cst_of cb = - let pt, opaque = pt_opaque_of cb in + let cst_of cb pt = + let pt, opaque = pt_opaque_of cb pt in let univs, subst = if cb.const_polymorphic then let univs = Univ.instantiate_univ_context cb.const_universes in @@ -244,15 +242,15 @@ let declare_sideff env fix_exn se = try ignore(Environ.lookup_constant c env); true with Not_found -> false in let knl = - CList.map_filter (fun (c,cb) -> + CList.map_filter (fun (c,cb,pt) -> if exists c then None - else Some (c,declare_constant_common (id_of c) (cst_of cb))) cbl in + else Some (c,declare_constant_common (id_of c) (cst_of cb pt))) cbl in match scheme with | None -> () | Some (inds_consts,kind) -> !declare_scheme kind (Array.of_list (List.map (fun (c,kn) -> - CList.find_map (fun (x,c',_) -> + CList.find_map (fun (x,c',_,_) -> if Constant.equal c c' then Some (x,kn) else None) inds_consts) knl)) diff --git a/stm/lemmas.ml b/stm/lemmas.ml index b0fea5916..0bcefc0e6 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -71,9 +71,9 @@ let adjust_guardness_conditions const = function with Not_found -> false in if exists c e then e else Environ.add_constant c cb e in let env = Declareops.fold_side_effects (fun env -> function - | SEsubproof (c, cb) -> add c cb env + | SEsubproof (c, cb,_) -> add c cb env | SEscheme (l,_) -> - List.fold_left (fun e (_,c,cb) -> add c cb e) env l) + List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l) env (Declareops.uniquize_side_effects eff) in let indexes = search_guard Loc.ghost env diff --git a/stm/stm.ml b/stm/stm.ml index b68ef9496..5349b85a8 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -802,14 +802,6 @@ module Task = struct let rc, time = let wall_clock = Unix.gettimeofday () in let l = Future.force (build_proof_here r_exn_info r_loc eop) in - List.iter (fun (_,se) -> Declareops.iter_side_effects (function - | Declarations.SEsubproof(_, - { Declarations.const_body = Declarations.OpaqueDef f; - const_universes = univs } ) -> - (* They are Direct *) - Opaqueproof.join_opaque Opaqueproof.empty_opaquetab f - | _ -> ()) - se) (fst l); l, Unix.gettimeofday () -. wall_clock in VCS.print (); RespBuiltProof(rc,time) |