diff options
Diffstat (limited to 'toplevel/obligations.ml')
| -rw-r--r-- | toplevel/obligations.ml | 221 |
1 files changed, 114 insertions, 107 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 523134b5..9019f486 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -306,7 +306,7 @@ type fixpoint_kind = type notations = (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list -type program_info = { +type program_info_aux = { prg_name: Id.t; prg_body: constr; prg_type: constr; @@ -322,6 +322,13 @@ type program_info = { prg_opaque : bool; } +type program_info = program_info_aux Ephemeron.key + +let get_info x = + try Ephemeron.get x + with Ephemeron.InvalidKey -> + Errors.anomaly Pp.(str "Program obligation can't be accessed by a worker") + let assumption_message = Declare.assumption_message let (set_default_tactic, get_default_tactic, print_default_tactic) = @@ -452,23 +459,10 @@ let subst_deps_obl obls obl = module ProgMap = Map.Make(Id) -let map_replace k v m = ProgMap.add k v (ProgMap.remove k m) +let map_replace k v m = ProgMap.add k (Ephemeron.create v) (ProgMap.remove k m) let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] -let map_cardinal m = - let i = ref 0 in - ProgMap.iter (fun _ _ -> incr i) m; - !i - -exception Found of program_info - -let map_first m = - try - ProgMap.iter (fun _ v -> raise (Found v)) m; - assert(false) - with Found x -> x - let from_prg : program_info ProgMap.t ref = Summary.ref ProgMap.empty ~name:"program-tcc-table" @@ -514,16 +508,17 @@ let declare_definition prg = let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None) (Evd.evar_universe_context_subst prg.prg_ctx) in let opaque = prg.prg_opaque in + let fix_exn = Stm.get_fix_exn () in let ce = - definition_entry ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) - ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body) + definition_entry ~fix_exn + ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) + ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body) in progmap_remove prg; !declare_definition_ref prg.prg_name prg.prg_kind ce prg.prg_implicits - (Lemmas.mk_hook (fun l r -> - Lemmas.call_hook (fun exn -> exn) prg.prg_hook l r; r)) - + (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r; r)) + open Pp let rec lam_index n t acc = @@ -547,7 +542,7 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype = let ctx = fst (decompose_prod_n_assum m fixtype) in List.map_i (fun i _ -> i) 0 ctx -let mk_proof c = ((c, Univ.ContextSet.empty), Declareops.no_seff) +let mk_proof c = ((c, Univ.ContextSet.empty), Safe_typing.empty_private_constants) let declare_mutual_definition l = let len = List.length l in @@ -606,12 +601,17 @@ let shrink_body c = else mkLambda (n,t,b), succ i, mkRel i :: args) (b, 1, []) ctx in List.map (fun (c,t) -> (c,None,t)) ctx, b', Array.of_list args - + +let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] + +let add_hint local prg cst = + Hints.add_hints local [Id.to_string prg.prg_name] (unfold_entry cst) + let declare_obligation prg obl body ty uctx = let body = prg.prg_reduce body in let ty = Option.map prg.prg_reduce ty in match obl.obl_status with - | Evar_kinds.Expand -> { obl with obl_body = Some (TermObl body) } + | Evar_kinds.Expand -> false, { obl with obl_body = Some (TermObl body) } | Evar_kinds.Define opaque -> let opaque = if get_proofs_transparency () then false else opaque in let poly = pi2 prg.prg_kind in @@ -619,8 +619,9 @@ let declare_obligation prg obl body ty uctx = if get_shrink_obligations () && not poly then shrink_body body else [], body, [||] in + let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in let ce = - { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Declareops.no_seff); + { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body; const_entry_secctx = None; const_entry_type = if List.is_empty ctx then ty else None; const_entry_polymorphic = poly; @@ -633,11 +634,9 @@ let declare_obligation prg obl body ty uctx = let constant = Declare.declare_constant obl.obl_name ~local:true (DefinitionEntry ce,IsProof Property) in - if not opaque then - Hints.add_hints false [Id.to_string prg.prg_name] - (Hints.HintsUnfoldEntry [EvalConstRef constant]); + if not opaque then add_hint false prg constant; definition_message obl.obl_name; - { obl with obl_body = + true, { obl with obl_body = if poly then Some (DefinedObl constant) else @@ -670,17 +669,33 @@ let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls prg_hook = hook; prg_opaque = opaque; } +let map_cardinal m = + let i = ref 0 in + ProgMap.iter (fun _ v -> + if snd (Ephemeron.get v).prg_obligations > 0 then incr i) m; + !i + +exception Found of program_info + +let map_first m = + try + ProgMap.iter (fun _ v -> + if snd (Ephemeron.get v).prg_obligations > 0 then + raise (Found v)) m; + assert(false) + with Found x -> x + let get_prog name = let prg_infos = !from_prg in match name with Some n -> - (try ProgMap.find n prg_infos + (try get_info (ProgMap.find n prg_infos) with Not_found -> raise (NoObligations (Some n))) | None -> (let n = map_cardinal prg_infos in match n with 0 -> raise (NoObligations None) - | 1 -> map_first prg_infos + | 1 -> get_info (map_first prg_infos) | _ -> error ("More than one program with unsolved obligations: "^ String.concat ", " @@ -690,7 +705,7 @@ let get_prog name = let get_any_prog () = let prg_infos = !from_prg in let n = map_cardinal prg_infos in - if n > 0 then map_first prg_infos + if n > 0 then get_info (map_first prg_infos) else raise (NoObligations None) let get_prog_err n = @@ -730,7 +745,7 @@ let update_obls prg obls rem = progmap_remove prg'; Defined kn | l -> - let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in + let progs = List.map (fun x -> get_info (ProgMap.find x !from_prg)) prg'.prg_deps in if List.for_all (fun x -> obligations_solved x) progs then let kn = declare_mutual_definition progs in Defined (ConstRef kn) @@ -767,7 +782,7 @@ let not_transp_msg = str "Obligation should be transparent but was declared opaque." ++ spc () ++ str"Use 'Defined' instead." -let error_not_transp () = pperror not_transp_msg +let err_not_transp () = pperror not_transp_msg let rec string_of_list sep f = function [] -> "" @@ -783,81 +798,68 @@ let solve_by_tac name evi t poly ctx = let (entry,_,ctx') = Pfedit.build_constant_by_tactic id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in let env = Global.env () in - let entry = Term_typing.handle_entry_side_effects env entry in - let body, eff = Future.force entry.Entries.const_entry_body in - assert(Declareops.side_effects_is_empty eff); - assert(Univ.ContextSet.is_empty (snd body)); + let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in + let body, eff = Future.force entry.const_entry_body in + assert(Safe_typing.empty_private_constants = eff); + let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in Inductiveops.control_only_guard (Global.env ()) (fst body); - (fst body), entry.Entries.const_entry_type, ctx' + (fst body), entry.const_entry_type, Evd.evar_universe_context ctx' + +let obligation_hook prg obl num auto ctx' _ gr = + let obls, rem = prg.prg_obligations in + let cst = match gr with ConstRef cst -> cst | _ -> assert false in + let transparent = evaluable_constant cst (Global.env ()) in + let () = match obl.obl_status with + | Evar_kinds.Expand -> if not transparent then err_not_transp () + | Evar_kinds.Define op -> if not op && not transparent then err_not_transp () + in + let obl = { obl with obl_body = Some (DefinedObl cst) } in + let () = if transparent then add_hint true prg cst in + let obls = Array.copy obls in + let _ = obls.(num) <- obl in + let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in + let ctx' = + if not (pi2 prg.prg_kind) (* Not polymorphic *) then + (* The universe context was declared globally, we continue + from the new global environment. *) + Evd.evar_universe_context (Evd.from_env (Global.env ())) + else ctx' + in + let prg = { prg with prg_ctx = ctx' } in + let () = + try ignore (update_obls prg obls (pred rem)) + with e when Errors.noncritical e -> + let e = Errors.push e in + pperror (Errors.iprint (Cerrors.process_vernac_interp_error e)) + in + if pred rem > 0 then begin + let deps = dependencies obls num in + if not (Int.Set.is_empty deps) then + ignore (auto (Some prg.prg_name) None deps) + end let rec solve_obligation prg num tac = let user_num = succ num in let obls, rem = prg.prg_obligations in let obl = obls.(num) in + let remaining = deps_remaining obls obl.obl_deps in + let () = if not (Option.is_empty obl.obl_body) then - pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.") - else - match deps_remaining obls obl.obl_deps with - | [] -> - let obl = subst_deps_obl obls obl in - let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in - let evd = Evd.from_env ~ctx:prg.prg_ctx Environ.empty_env in - Lemmas.start_proof_univs obl.obl_name kind evd obl.obl_type - (fun ctx' -> Lemmas.mk_hook (fun strength gr -> - let cst = match gr with ConstRef cst -> cst | _ -> assert false in - let obl = - let transparent = evaluable_constant cst (Global.env ()) in - let body = - match obl.obl_status with - | Evar_kinds.Expand -> - if not transparent then error_not_transp () - else DefinedObl cst - | Evar_kinds.Define opaque -> - if not opaque && not transparent then error_not_transp () - else DefinedObl cst - in - if transparent then - Hints.add_hints true [Id.to_string prg.prg_name] - (Hints.HintsUnfoldEntry [EvalConstRef cst]); - { obl with obl_body = Some body } - in - let obls = Array.copy obls in - let _ = obls.(num) <- obl in - let ctx' = - let ctx = - match ctx' with - | None -> prg.prg_ctx - | Some ctx' -> ctx' - in - if not (pi2 prg.prg_kind) (* Not polymorphic *) then - (* This context is already declared globally, we cannot - instantiate the rigid variables anymore *) - Evd.abstract_undefined_variables ctx - else ctx - in - let res = - try update_obls - {prg with prg_body = prg.prg_body; - prg_type = prg.prg_type; - prg_ctx = ctx' } - - obls (pred rem) - with e when Errors.noncritical e -> - let e = Errors.push e in - pperror (Errors.iprint (Cerrors.process_vernac_interp_error e)) - in - match res with - | Remain n when n > 0 -> - let deps = dependencies obls num in - if not (Int.Set.is_empty deps) then - ignore(auto_solve_obligations (Some prg.prg_name) None ~oblset:deps) - | _ -> ())); - trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ - Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type); - ignore (Pfedit.by (snd (get_default_tactic ()))); - Option.iter (fun tac -> Pfedit.set_end_tac tac) tac - | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " - ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l)) + pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved."); + if not (List.is_empty remaining) then + pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " + ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining)); + in + let obl = subst_deps_obl obls obl in + let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in + let evd = Evd.from_ctx prg.prg_ctx in + let auto n tac oblset = auto_solve_obligations n ~oblset tac in + let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in + let () = Lemmas.start_proof_univs obl.obl_name kind evd obl.obl_type hook in + let () = trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ + Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type) in + let _ = Pfedit.by (snd (get_default_tactic ())) in + Option.iter (fun tac -> Pfedit.set_end_tac tac) tac and obligation (user_num, name, typ) tac = let num = pred user_num in @@ -892,8 +894,13 @@ and solve_obligation_by_tac prg obls i tac = (pi2 !prg.prg_kind) !prg.prg_ctx in let uctx = Evd.evar_context_universe_context ctx in - prg := {!prg with prg_ctx = ctx}; - obls.(i) <- declare_obligation !prg obl t ty uctx; + let () = prg := {!prg with prg_ctx = ctx} in + let def, obl' = declare_obligation !prg obl t ty uctx in + obls.(i) <- obl'; + if def && not (pi2 !prg.prg_kind) then ( + (* Declare the term constraints with the first obligation only *) + let ctx' = Evd.evar_universe_context (Evd.from_env (Global.env ())) in + prg := {!prg with prg_ctx = ctx'}); true else false with e when Errors.noncritical e -> @@ -929,7 +936,7 @@ and solve_obligations n tac = solve_prg_obligations prg tac and solve_all_obligations tac = - ProgMap.iter (fun k v -> ignore(solve_prg_obligations v tac)) !from_prg + ProgMap.iter (fun k v -> ignore(solve_prg_obligations (get_info v) tac)) !from_prg and try_solve_obligation n prg tac = let prg = get_prog prg in @@ -970,7 +977,7 @@ let show_obligations ?(msg=true) n = | Some n -> try [ProgMap.find n !from_prg] with Not_found -> raise (NoObligations (Some n)) - in List.iter (show_obligations_of_prg ~msg) progs + in List.iter (fun x -> show_obligations_of_prg ~msg (get_info x)) progs let show_term n = let prg = get_prog_err n in @@ -991,7 +998,7 @@ let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) else ( let len = Array.length obls in let _ = Flags.if_verbose msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in - progmap_add n prg; + progmap_add n (Ephemeron.create prg); let res = auto_solve_obligations (Some n) tactic in match res with | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res @@ -1004,7 +1011,7 @@ let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduc (fun (n, b, t, imps, obls) -> let prg = init_prog_info ~opaque n (Some b) t ctx deps (Some fixkind) notations obls imps kind reduce hook - in progmap_add n prg) l; + in progmap_add n (Ephemeron.create prg)) l; let _defined = List.fold_left (fun finished x -> if finished then finished |