diff options
Diffstat (limited to 'vernac/obligations.ml')
-rw-r--r-- | vernac/obligations.ml | 1196 |
1 files changed, 1196 insertions, 0 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml new file mode 100644 index 00000000..765d6851 --- /dev/null +++ b/vernac/obligations.ml @@ -0,0 +1,1196 @@ +open Printf +open Libobject +open Entries +open Decl_kinds +open Declare + +(** + - Get types of existentials ; + - Flatten dependency tree (prefix order) ; + - Replace existentials by de Bruijn indices in term, applied to the right arguments ; + - Apply term prefixed by quantification on "existentials". +*) + +open Term +open Constr +open Vars +open Names +open Evd +open Pp +open CErrors +open Util + +module NamedDecl = Context.Named.Declaration + +let get_fix_exn, stm_get_fix_exn = Hook.make () + +let succfix (depth, fixrels) = + (succ depth, List.map succ fixrels) + +let check_evars env evm = + Evar.Map.iter + (fun key evi -> + let (loc,k) = evar_source key evm in + match k with + | Evar_kinds.QuestionMark _ + | Evar_kinds.ImplicitArg (_,_,false) -> () + | _ -> + Pretype_errors.error_unsolvable_implicit ?loc env evm key None) + (Evd.undefined_map evm) + +type oblinfo = + { ev_name: int * Id.t; + ev_hyps: Context.Named.t; + ev_status: bool * Evar_kinds.obligation_definition_status; + ev_chop: int option; + ev_src: Evar_kinds.t Loc.located; + ev_typ: types; + ev_tac: unit Proofview.tactic option; + ev_deps: Int.Set.t } + +(** Substitute evar references in t using de Bruijn indices, + where n binders were passed through. *) + +let subst_evar_constr evs n idf t = + let seen = ref Int.Set.empty in + let transparent = ref Id.Set.empty in + let evar_info id = List.assoc_f Evar.equal id evs in + let rec substrec (depth, fixrels) c = match Constr.kind c with + | Evar (k, args) -> + let { ev_name = (id, idstr) ; + ev_hyps = hyps ; ev_chop = chop } = + try evar_info k + with Not_found -> + anomaly ~label:"eterm" (Pp.str "existential variable " ++ int (Evar.repr k) ++ str " not found.") + in + seen := Int.Set.add id !seen; + (* Evar arguments are created in inverse order, + and we must not apply to defined ones (i.e. LetIn's) + *) + let args = + let n = match chop with None -> 0 | Some c -> c in + let (l, r) = List.chop n (List.rev (Array.to_list args)) in + List.rev r + in + let args = + let rec aux hyps args acc = + let open Context.Named.Declaration in + match hyps, args with + (LocalAssum _ :: tlh), (c :: tla) -> + aux tlh tla ((substrec (depth, fixrels) c) :: acc) + | (LocalDef _ :: tlh), (_ :: tla) -> + aux tlh tla acc + | [], [] -> acc + | _, _ -> acc (*failwith "subst_evars: invalid argument"*) + in aux hyps args [] + in + if List.exists + (fun x -> match Constr.kind x with + | Rel n -> Int.List.mem n fixrels + | _ -> false) args + then + transparent := Id.Set.add idstr !transparent; + mkApp (idf idstr, Array.of_list args) + | Fix _ -> + Constr.map_with_binders succfix substrec (depth, 1 :: fixrels) c + | _ -> Constr.map_with_binders succfix substrec (depth, fixrels) c + in + let t' = substrec (0, []) t in + t', !seen, !transparent + + +(** Substitute variable references in t using de Bruijn indices, + where n binders were passed through. *) +let subst_vars acc n t = + let var_index id = Util.List.index Id.equal id acc in + let rec substrec depth c = match Constr.kind c with + | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c) + | _ -> Constr.map_with_binders succ substrec depth c + in + substrec 0 t + +(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ]) + to a product : forall H1 : t1, ..., forall Hn : tn, concl. + Changes evars and hypothesis references to variable references. +*) +let etype_of_evar evs hyps concl = + let open Context.Named.Declaration in + let rec aux acc n = function + decl :: tl -> + let t', s, trans = subst_evar_constr evs n mkVar (NamedDecl.get_type decl) in + let t'' = subst_vars acc 0 t' in + let rest, s', trans' = aux (NamedDecl.get_id decl :: acc) (succ n) tl in + let s' = Int.Set.union s s' in + let trans' = Id.Set.union trans trans' in + (match decl with + | LocalDef (id,c,_) -> + let c', s'', trans'' = subst_evar_constr evs n mkVar c in + let c' = subst_vars acc 0 c' in + mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest, + Int.Set.union s'' s', + Id.Set.union trans'' trans' + | LocalAssum (id,_) -> + mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans') + | [] -> + let t', s, trans = subst_evar_constr evs n mkVar concl in + subst_vars acc 0 t', s, trans + in aux [] 0 (List.rev hyps) + +let trunc_named_context n ctx = + let len = List.length ctx in + List.firstn (len - n) ctx + +let rec chop_product n t = + let pop t = Vars.lift (-1) t in + if Int.equal n 0 then Some t + else + match Constr.kind t with + | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (pop b) else None + | _ -> None + +let evar_dependencies evm oev = + let one_step deps = + Evar.Set.fold (fun ev s -> + let evi = Evd.find evm ev in + let deps' = evars_of_filtered_evar_info evi in + if Evar.Set.mem oev deps' then + invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ Pp.string_of_ppcmds @@ Evar.print oev) + else Evar.Set.union deps' s) + deps deps + in + let rec aux deps = + let deps' = one_step deps in + if Evar.Set.equal deps deps' then deps + else aux deps' + in aux (Evar.Set.singleton oev) + +let move_after (id, ev, deps as obl) l = + let rec aux restdeps = function + | (id', _, _) as obl' :: tl -> + let restdeps' = Evar.Set.remove id' restdeps in + if Evar.Set.is_empty restdeps' then + obl' :: obl :: tl + else obl' :: aux restdeps' tl + | [] -> [obl] + in aux (Evar.Set.remove id deps) l + +let sort_dependencies evl = + let rec aux l found list = + match l with + | (id, ev, deps) as obl :: tl -> + let found' = Evar.Set.union found (Evar.Set.singleton id) in + if Evar.Set.subset deps found' then + aux tl found' (obl :: list) + else aux (move_after obl tl) found list + | [] -> List.rev list + in aux evl Evar.Set.empty [] + +open Environ + +let eterm_obligations env name evm fs ?status t ty = + (* 'Serialize' the evars *) + let nc = Environ.named_context env in + let nc_len = Context.Named.length nc in + let evm = Evarutil.nf_evar_map_undefined evm in + let evl = Evarutil.non_instantiated evm in + let evl = Evar.Map.bindings evl in + let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in + let sevl = sort_dependencies evl in + let evl = List.map (fun (id, ev, _) -> id, ev) sevl in + let evn = + let i = ref (-1) in + List.rev_map (fun (id, ev) -> incr i; + (id, (!i, Id.of_string + (Id.to_string name ^ "_obligation_" ^ string_of_int (succ !i))), + ev)) evl + in + let evts = + (* Remove existential variables in types and build the corresponding products *) + List.fold_right + (fun (id, (n, nstr), ev) l -> + let hyps = Evd.evar_filtered_context ev in + let hyps = trunc_named_context nc_len hyps in + let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in + let evtyp, hyps, chop = + match chop_product fs evtyp with + | Some t -> t, trunc_named_context fs hyps, fs + | None -> evtyp, hyps, 0 + in + let loc, k = evar_source id evm in + let status = match k with + | Evar_kinds.QuestionMark (o,_) -> o + | _ -> match status with + | Some o -> o + | None -> Evar_kinds.Define (not (Program.get_proofs_transparency ())) + in + let force_status, status, chop = match status with + | Evar_kinds.Define true as stat -> + if not (Int.equal chop fs) then true, Evar_kinds.Define false, None + else false, stat, Some chop + | s -> false, s, None + in + let info = { ev_name = (n, nstr); + ev_hyps = hyps; ev_status = force_status, status; ev_chop = chop; + ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = None } + in (id, info) :: l) + evn [] + in + let t', _, transparent = (* Substitute evar refs in the term by variables *) + subst_evar_constr evts 0 mkVar t + in + let ty, _, _ = subst_evar_constr evts 0 mkVar ty in + let evars = + List.map (fun (ev, info) -> + let { ev_name = (_, name); ev_status = force_status, status; + ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info + in + let force_status, status = match status with + | Evar_kinds.Define true when Id.Set.mem name transparent -> + true, Evar_kinds.Define false + | _ -> force_status, status + in name, typ, src, (force_status, status), deps, tac) evts + in + let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in + let evmap f c = pi1 (subst_evar_constr evts 0 f c) in + Array.of_list (List.rev evars), (evnames, evmap), t', ty + +let tactics_module = ["Program";"Tactics"] +let safe_init_constant md name () = + Coqlib.check_required_library ("Coq"::md); + Universes.constr_of_global (Coqlib.coq_reference "Obligations" md name) +let hide_obligation = safe_init_constant tactics_module "obligation" + +let pperror cmd = CErrors.user_err ~hdr:"Program" cmd +let error s = pperror (str s) + +let reduce c = + EConstr.Unsafe.to_constr (Reductionops.clos_norm_flags CClosure.betaiota (Global.env ()) Evd.empty (EConstr.of_constr c)) + +exception NoObligations of Id.t option + +let explain_no_obligations = function + Some ident -> str "No obligations for program " ++ Id.print ident + | None -> str "No obligations remaining" + +type obligation_info = + (Names.Id.t * types * Evar_kinds.t Loc.located * + (bool * Evar_kinds.obligation_definition_status) + * Int.Set.t * unit Proofview.tactic option) array + +type 'a obligation_body = + | DefinedObl of 'a + | TermObl of constr + +type obligation = + { obl_name : Id.t; + obl_type : types; + obl_location : Evar_kinds.t Loc.located; + obl_body : pconstant obligation_body option; + obl_status : bool * Evar_kinds.obligation_definition_status; + obl_deps : Int.Set.t; + obl_tac : unit Proofview.tactic option; + } + +type obligations = (obligation array * int) + +type fixpoint_kind = + | IsFixpoint of (Misctypes.lident option * Constrexpr.recursion_order_expr) list + | IsCoFixpoint + +type notations = (Misctypes.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list + +type program_info_aux = { + prg_name: Id.t; + prg_body: constr; + prg_type: constr; + prg_ctx: UState.t; + prg_univdecl: Univdecls.universe_decl; + prg_obligations: obligations; + prg_deps : Id.t list; + prg_fixkind : fixpoint_kind option ; + prg_implicits : (Constrexpr.explicitation * (bool * bool * bool)) list; + prg_notations : notations ; + prg_kind : definition_kind; + prg_reduce : constr -> constr; + prg_hook : (UState.t -> unit) Lemmas.declaration_hook; + prg_opaque : bool; + prg_sign: named_context_val; +} + +type program_info = program_info_aux CEphemeron.key + +let get_info x = + try CEphemeron.get x + with CEphemeron.InvalidKey -> + CErrors.anomaly Pp.(str "Program obligation can't be accessed by a worker.") + +let assumption_message = Declare.assumption_message + +let default_tactic = ref (Proofview.tclUNIT ()) + +(* true = hide obligations *) +let hide_obligations = ref false + +let set_hide_obligations = (:=) hide_obligations +let get_hide_obligations () = !hide_obligations + +open Goptions +let _ = + declare_bool_option + { optdepr = false; + optname = "Hidding of Program obligations"; + optkey = ["Hide";"Obligations"]; + optread = get_hide_obligations; + optwrite = set_hide_obligations; } + +let shrink_obligations = ref true + +let set_shrink_obligations = (:=) shrink_obligations +let get_shrink_obligations () = !shrink_obligations + +let _ = + declare_bool_option + { optdepr = true; (* remove in 8.8 *) + optname = "Shrinking of Program obligations"; + optkey = ["Shrink";"Obligations"]; + optread = get_shrink_obligations; + optwrite = set_shrink_obligations; } + +let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type + +let get_obligation_body expand obl = + match obl.obl_body with + | None -> None + | Some c -> + if expand && snd obl.obl_status == Evar_kinds.Expand then + match c with + | DefinedObl pc -> Some (constant_value_in (Global.env ()) pc) + | TermObl c -> Some c + else (match c with + | DefinedObl pc -> Some (mkConstU pc) + | TermObl c -> Some c) + +let obl_substitution expand obls deps = + Int.Set.fold + (fun x acc -> + let xobl = obls.(x) in + match get_obligation_body expand xobl with + | None -> acc + | Some oblb -> (xobl.obl_name, (xobl.obl_type, oblb)) :: acc) + deps [] + +let subst_deps expand obls deps t = + let osubst = obl_substitution expand obls deps in + (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t) + +let rec prod_app t n = + match Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (** FIXME *) with + | Prod (_,_,b) -> subst1 n b + | LetIn (_, b, t, b') -> prod_app (subst1 b b') n + | _ -> + user_err ~hdr:"prod_app" + (str"Needed a product, but didn't find one" ++ fnl ()) + + +(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) +let prod_applist t nL = List.fold_left prod_app t nL + +let replace_appvars subst = + let rec aux c = + let f, l = decompose_app c in + if isVar f then + try + let c' = List.map (Constr.map aux) l in + let (t, b) = Id.List.assoc (destVar f) subst in + mkApp (delayed_force hide_obligation, + [| prod_applist t c'; applistc b c' |]) + with Not_found -> Constr.map aux c + else Constr.map aux c + in Constr.map aux + +let subst_prog expand obls ints prg = + let subst = obl_substitution expand obls ints in + if get_hide_obligations () then + (replace_appvars subst prg.prg_body, + replace_appvars subst ((* Termops.refresh_universes *) prg.prg_type)) + else + let subst' = List.map (fun (n, (_, b)) -> n, b) subst in + (Vars.replace_vars subst' prg.prg_body, + Vars.replace_vars subst' ((* Termops.refresh_universes *) prg.prg_type)) + +let subst_deps_obl obls obl = + let t' = subst_deps true obls obl.obl_deps obl.obl_type in + { obl with obl_type = t' } + +module ProgMap = Id.Map + +let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) + +let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] + +let from_prg, program_tcc_summary_tag = + Summary.ref_tag ProgMap.empty ~name:"program-tcc-table" + +let close sec = + if not (ProgMap.is_empty !from_prg) then + let keys = map_keys !from_prg in + user_err ~hdr:"Program" + (str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++ + prlist_with_sep spc (fun x -> Id.print x) keys ++ + (str (if Int.equal (List.length keys) 1 then " has " else " have ") ++ + str "unsolved obligations")) + +let input : program_info ProgMap.t -> obj = + declare_object + { (default_object "Program state") with + cache_function = (fun (na, pi) -> from_prg := pi); + load_function = (fun _ (_, pi) -> from_prg := pi); + discharge_function = (fun _ -> close "section"; None); + classify_function = (fun _ -> close "module"; Dispose) } + +open Evd + +let progmap_remove prg = + Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg)) + +let progmap_add n prg = + Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg)) + +let progmap_replace prg' = + Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg)) + +let rec intset_to = function + -1 -> Int.Set.empty + | n -> Int.Set.add n (intset_to (pred n)) + +let subst_body expand prg = + let obls, _ = prg.prg_obligations in + let ints = intset_to (pred (Array.length obls)) in + subst_prog expand obls ints prg + +let declare_definition prg = + let body, typ = subst_body true prg in + let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None) + (UState.subst prg.prg_ctx) in + let opaque = prg.prg_opaque in + let fix_exn = Hook.get get_fix_exn () in + let typ = nf typ in + let body = nf body in + let env = Global.env () in + let uvars = Univ.LSet.union + (Univops.universes_of_constr env typ) + (Univops.universes_of_constr env body) in + let uctx = UState.restrict prg.prg_ctx uvars in + let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in + let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in + let () = progmap_remove prg in + let ubinders = UState.universe_binders uctx in + DeclareDef.declare_definition prg.prg_name + prg.prg_kind ce ubinders prg.prg_implicits + (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r uctx; r)) + +let rec lam_index n t acc = + match Constr.kind t with + | Lambda (Name n', _, _) when Id.equal n n' -> + acc + | Lambda (_, _, b) -> + lam_index n b (succ acc) + | _ -> raise Not_found + +let compute_possible_guardness_evidences (n,_) fixbody fixtype = + match n with + | Some { CAst.loc; v = n } -> [lam_index n fixbody 0] + | None -> + (* If recursive argument was not given by user, we try all args. + An earlier approach was to look only for inductive arguments, + but doing it properly involves delta-reduction, and it finally + doesn't seem to worth the effort (except for huge mutual + fixpoints ?) *) + let m = Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) (** FIXME *) in + 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), Safe_typing.empty_private_constants) + +let declare_mutual_definition l = + let len = List.length l in + let first = List.hd l in + let fixdefs, fixtypes, fiximps = + List.split3 + (List.map (fun x -> + let subs, typ = (subst_body true x) in + let env = Global.env () in + let sigma = Evd.from_ctx x.prg_ctx in + let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in + let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in + let term = EConstr.to_constr sigma term in + let typ = EConstr.to_constr sigma typ in + x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l) + in +(* let fixdefs = List.map reduce_fix fixdefs in *) + let fixkind = Option.get first.prg_fixkind in + let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in + let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in + let (local,poly,kind) = first.prg_kind in + let fixnames = first.prg_deps in + let opaque = first.prg_opaque in + let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in + let indexes, fixdecls = + match fixkind with + | IsFixpoint wfl -> + let possible_indexes = + List.map3 compute_possible_guardness_evidences + wfl fixdefs fixtypes in + let indexes = + Pretyping.search_guard (Global.env()) + possible_indexes fixdecls in + Some indexes, + List.map_i (fun i _ -> + mk_proof (mkFix ((indexes,i),fixdecls))) 0 l + | IsCoFixpoint -> + None, + List.map_i (fun i _ -> + mk_proof (mkCoFix (i,fixdecls))) 0 l + in + (* Declare the recursive definitions *) + let univs = UState.const_univ_entry ~poly first.prg_ctx in + let fix_exn = Hook.get get_fix_exn () in + let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders univs) + fixnames fixdecls fixtypes fiximps in + (* Declare notations *) + List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; + Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; + let gr = List.hd kns in + Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx; + List.iter progmap_remove l; gr + +let decompose_lam_prod c ty = + let open Context.Rel.Declaration in + let rec aux ctx c ty = + match Constr.kind c, Constr.kind ty with + | LetIn (x, b, t, c), LetIn (x', b', t', ty) + when Constr.equal b b' && Constr.equal t t' -> + let ctx' = Context.Rel.add (LocalDef (x,b',t')) ctx in + aux ctx' c ty + | _, LetIn (x', b', t', ty) -> + let ctx' = Context.Rel.add (LocalDef (x',b',t')) ctx in + aux ctx' (lift 1 c) ty + | LetIn (x, b, t, c), _ -> + let ctx' = Context.Rel.add (LocalDef (x,b,t)) ctx in + aux ctx' c (lift 1 ty) + | Lambda (x, b, t), Prod (x', b', t') + (* By invariant, must be convertible *) -> + let ctx' = Context.Rel.add (LocalAssum (x,b')) ctx in + aux ctx' t t' + | Cast (c, _, _), _ -> aux ctx c ty + | _, _ -> ctx, c, ty + in aux Context.Rel.empty c ty + +let shrink_body c ty = + let ctx, b, ty = + match ty with + | None -> + let ctx, b = decompose_lam_assum c in + ctx, b, None + | Some ty -> + let ctx, b, ty = decompose_lam_prod c ty in + ctx, b, Some ty + in + let b', ty', n, args = + List.fold_left (fun (b, ty, i, args) decl -> + if noccurn 1 b && Option.cata (noccurn 1) true ty then + subst1 mkProp b, Option.map (subst1 mkProp) ty, succ i, args + else + let open Context.Rel.Declaration in + let args = if is_local_assum decl then mkRel i :: args else args in + mkLambda_or_LetIn decl b, Option.map (mkProd_or_LetIn decl) ty, + succ i, args) + (b, ty, 1, []) ctx + in ctx, b', ty', 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 it_mkLambda_or_LetIn_or_clean t ctx = + let open Context.Rel.Declaration in + let fold t decl = + if is_local_assum decl then mkLambda_or_LetIn decl t + else + if noccurn 1 t then subst1 mkProp t + else mkLambda_or_LetIn decl t + in + Context.Rel.fold_inside fold ctx ~init:t + +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 -> false, { obl with obl_body = Some (TermObl body) } + | force, Evar_kinds.Define opaque -> + let opaque = not force && opaque in + let poly = pi2 prg.prg_kind in + let ctx, body, ty, args = + if get_shrink_obligations () && not poly then + shrink_body body ty else [], body, ty, [||] + in + let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in + let ce = + { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body; + const_entry_secctx = None; + const_entry_type = ty; + const_entry_universes = uctx; + const_entry_opaque = opaque; + const_entry_inline_code = false; + const_entry_feedback = None; + } in + (** ppedrot: seems legit to have obligations as local *) + let constant = Declare.declare_constant obl.obl_name ~local:true + (DefinitionEntry ce,IsProof Property) + in + if not opaque then add_hint (Locality.make_section_locality None) prg constant; + definition_message obl.obl_name; + let body = match uctx with + | Polymorphic_const_entry uctx -> + Some (DefinedObl (constant, Univ.UContext.instance uctx)) + | Monomorphic_const_entry _ -> + Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) + in + true, { obl with obl_body = body } + +let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind + notations obls impls kind reduce hook = + let obls', b = + match b with + | None -> + assert(Int.equal (Array.length obls) 0); + let n = Nameops.add_suffix n "_obligation" in + [| { obl_name = n; obl_body = None; + obl_location = Loc.tag Evar_kinds.InternalHole; obl_type = t; + obl_status = false, Evar_kinds.Expand; obl_deps = Int.Set.empty; + obl_tac = None } |], + mkVar n + | Some b -> + Array.mapi + (fun i (n, t, l, o, d, tac) -> + { obl_name = n ; obl_body = None; + obl_location = l; obl_type = t; obl_status = o; + obl_deps = d; obl_tac = tac }) + obls, b + in + let ctx = UState.make_flexible_nonalgebraic ctx in + { prg_name = n ; prg_body = b; prg_type = reduce t; + prg_ctx = ctx; prg_univdecl = udecl; + prg_obligations = (obls', Array.length obls'); + prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ; + prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; + prg_hook = hook; prg_opaque = opaque; + prg_sign = sign } + +let map_cardinal m = + let i = ref 0 in + ProgMap.iter (fun _ v -> + if snd (CEphemeron.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 (CEphemeron.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 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 -> get_info (map_first prg_infos) + | _ -> + let progs = Id.Set.elements (ProgMap.domain prg_infos) in + let prog = List.hd progs in + let progs = prlist_with_sep pr_comma Id.print progs in + user_err + (str "More than one program with unsolved obligations: " ++ progs + ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Id.print prog ++ str "\"")) + +let get_any_prog () = + let prg_infos = !from_prg in + let n = map_cardinal prg_infos in + if n > 0 then get_info (map_first prg_infos) + else raise (NoObligations None) + +let get_prog_err n = + try get_prog n with NoObligations id -> pperror (explain_no_obligations id) + +let get_any_prog_err () = + try get_any_prog () with NoObligations id -> pperror (explain_no_obligations id) + +let obligations_solved prg = Int.equal (snd prg.prg_obligations) 0 + +let all_programs () = + ProgMap.fold (fun k p l -> p :: l) !from_prg [] + +type progress = + | Remain of int + | Dependent + | Defined of global_reference + +let obligations_message rem = + if rem > 0 then + if Int.equal rem 1 then + Flags.if_verbose Feedback.msg_info (int rem ++ str " obligation remaining") + else + Flags.if_verbose Feedback.msg_info (int rem ++ str " obligations remaining") + else + Flags.if_verbose Feedback.msg_info (str "No more obligations remaining") + +let update_obls prg obls rem = + let prg' = { prg with prg_obligations = (obls, rem) } in + progmap_replace prg'; + obligations_message rem; + if rem > 0 then Remain rem + else ( + match prg'.prg_deps with + | [] -> + let kn = declare_definition prg' in + progmap_remove prg'; + Defined kn + | l -> + 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 kn + else Dependent) + +let is_defined obls x = not (Option.is_empty obls.(x).obl_body) + +let deps_remaining obls deps = + Int.Set.fold + (fun x acc -> + if is_defined obls x then acc + else x :: acc) + deps [] + +let dependencies obls n = + let res = ref Int.Set.empty in + Array.iteri + (fun i obl -> + if not (Int.equal i n) && Int.Set.mem n obl.obl_deps then + res := Int.Set.add i !res) + obls; + !res + +let goal_kind poly = Decl_kinds.Local, poly, Decl_kinds.DefinitionBody Decl_kinds.Definition + +let goal_proof_kind poly = Decl_kinds.Local, poly, Decl_kinds.Proof Decl_kinds.Lemma + +let kind_of_obligation poly o = + match o with + | Evar_kinds.Define false | Evar_kinds.Expand -> goal_kind poly + | _ -> goal_proof_kind poly + +let not_transp_msg = + str "Obligation should be transparent but was declared opaque." ++ spc () ++ + str"Use 'Defined' instead." + +let err_not_transp () = pperror not_transp_msg + +let rec string_of_list sep f = function + [] -> "" + | x :: [] -> f x + | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl + +(* Solve an obligation using tactics, return the corresponding proof term *) + +let solve_by_tac name evi t poly ctx = + let id = name in + let concl = EConstr.of_constr evi.evar_concl in + (* spiwack: the status is dropped. *) + 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 = Safe_typing.inline_private_constants_in_definition_entry env entry in + let body, () = Future.force entry.const_entry_body in + let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in + Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body)); + (fst body), entry.const_entry_type, Evd.evar_universe_context ctx' + +let obligation_terminator name num guard hook auto pf = + let open Proof_global in + let term = Lemmas.universe_proof_terminator guard hook in + match pf with + | Admitted _ -> apply_terminator term pf + | Proved (opq, id, proof) -> + let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in + let env = Global.env () in + let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in + let ty = entry.Entries.const_entry_type in + let (body, cstr), () = Future.force entry.Entries.const_entry_body in + let sigma = Evd.from_ctx uctx in + let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in + Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body); + (** Declare the obligation ourselves and drop the hook *) + let prg = get_info (ProgMap.find name !from_prg) in + (** Ensure universes are substituted properly in body and type *) + let body = EConstr.to_constr sigma (EConstr.of_constr body) in + let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in + let ctx = Evd.evar_universe_context sigma in + let obls, rem = prg.prg_obligations in + let obl = obls.(num) in + let status = + match obl.obl_status, opq with + | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp () + | (true, _), Vernacexpr.Opaque -> err_not_transp () + | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true + | (_, Evar_kinds.Define true), Vernacexpr.Transparent -> + Evar_kinds.Define false + | (_, status), Vernacexpr.Transparent -> status + in + let obl = { obl with obl_status = false, status } in + let ctx = + if pi2 prg.prg_kind then ctx + else UState.union prg.prg_ctx ctx + in + let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in + let (defined, obl) = declare_obligation prg obl body ty uctx in + let obls = Array.copy obls in + let _ = obls.(num) <- obl in + let prg_ctx = + if pi2 (prg.prg_kind) then (* Polymorphic *) + (** We merge the new universes and constraints of the + polymorphic obligation with the existing ones *) + UState.union prg.prg_ctx ctx + else + (** The first obligation, if defined, + declares the univs of the constant, + each subsequent obligation declares its own additional + universes and constraints if any *) + if defined then UState.make (Global.universes ()) + else ctx + in + let prg = { prg with prg_ctx } in + try + ignore (update_obls prg obls (pred rem)); + if pred rem > 0 then + begin + let deps = dependencies obls num in + if not (Int.Set.is_empty deps) then + ignore (auto (Some name) None deps) + end + with e when CErrors.noncritical e -> + let e = CErrors.push e in + pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) + +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 + (true, Evar_kinds.Expand) + | (true, Evar_kinds.Define true) -> + if not transparent then err_not_transp () + | _ -> () +in + let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in + let inst, ctx' = + if not (pi2 prg.prg_kind) (* Not polymorphic *) then + (* The universe context was declared globally, we continue + from the new global environment. *) + let evd = Evd.from_env (Global.env ()) in + let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in + Univ.Instance.empty, Evd.evar_universe_context ctx' + else + (* We get the right order somehow, but surely it could be enforced in a clearer way. *) + let uctx = UState.context ctx' in + Univ.UContext.instance uctx, ctx' + in + let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in + let () = if transparent then add_hint true prg cst in + let obls = Array.copy obls in + let _ = obls.(num) <- obl in + let prg = { prg with prg_ctx = ctx' } in + let () = + try ignore (update_obls prg obls (pred rem)) + with e when CErrors.noncritical e -> + let e = CErrors.push e in + pperror (CErrors.iprint (ExplainErr.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."); + 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) (snd obl.obl_status) in + let evd = Evd.from_ctx prg.prg_ctx in + let evd = Evd.update_sigma_env evd (Global.env ()) in + let auto n tac oblset = auto_solve_obligations n ~oblset tac in + let terminator guard hook = + Proof_global.make_terminator + (obligation_terminator prg.prg_name num guard hook auto) in + let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in + let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator hook in + let _ = Pfedit.by !default_tactic in + Option.iter (fun tac -> Proof_global.set_endline_tactic tac) tac + +and obligation (user_num, name, typ) tac = + let num = pred user_num in + let prg = get_prog_err name in + let obls, rem = prg.prg_obligations in + if num >= 0 && num < Array.length obls then + let obl = obls.(num) in + match obl.obl_body with + None -> solve_obligation prg num tac + | Some r -> error "Obligation already solved" + else error (sprintf "Unknown obligation number %i" (succ num)) + + +and solve_obligation_by_tac prg obls i tac = + let obl = obls.(i) in + match obl.obl_body with + | Some _ -> None + | None -> + try + if List.is_empty (deps_remaining obls obl.obl_deps) then + let obl = subst_deps_obl obls obl in + let tac = + match tac with + | Some t -> t + | None -> + match obl.obl_tac with + | Some t -> t + | None -> !default_tactic + in + let evd = Evd.from_ctx prg.prg_ctx in + let evd = Evd.update_sigma_env evd (Global.env ()) in + let t, ty, ctx = + solve_by_tac obl.obl_name (evar_of_obligation obl) tac + (pi2 prg.prg_kind) (Evd.evar_universe_context evd) + in + let uctx = if pi2 prg.prg_kind + then Polymorphic_const_entry (UState.context ctx) + else Monomorphic_const_entry (UState.context_set ctx) + in + 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 evd = Evd.from_env (Global.env ()) in + let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in + let ctx' = Evd.evar_universe_context evd in + Some {prg with prg_ctx = ctx'}) + else Some prg + else None + with e when CErrors.noncritical e -> + let (e, _) = CErrors.push e in + match e with + | Refiner.FailError (_, s) -> + user_err ?loc:(fst obl.obl_location) ~hdr:"solve_obligation" (Lazy.force s) + | e -> None (* FIXME really ? *) + +and solve_prg_obligations prg ?oblset tac = + let obls, rem = prg.prg_obligations in + let rem = ref rem in + let obls' = Array.copy obls in + let set = ref Int.Set.empty in + let p = match oblset with + | None -> (fun _ -> true) + | Some s -> set := s; + (fun i -> Int.Set.mem i !set) + in + let prgref = ref prg in + let _ = + Array.iteri (fun i x -> + if p i then + match solve_obligation_by_tac !prgref obls' i tac with + | None -> () + | Some prg' -> + prgref := prg'; + let deps = dependencies obls i in + (set := Int.Set.union !set deps; + decr rem)) + obls' + in + update_obls !prgref obls' !rem + +and solve_obligations n tac = + let prg = get_prog_err n in + solve_prg_obligations prg tac + +and solve_all_obligations tac = + 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 + let obls, rem = prg.prg_obligations in + let obls' = Array.copy obls in + match solve_obligation_by_tac prg obls' n tac with + | Some prg' -> ignore(update_obls prg' obls' (pred rem)) + | None -> () + +and try_solve_obligations n tac = + try ignore (solve_obligations n tac) with NoObligations _ -> () + +and auto_solve_obligations n ?oblset tac : progress = + Flags.if_verbose Feedback.msg_info (str "Solving obligations automatically..."); + try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent + +open Pp +let show_obligations_of_prg ?(msg=true) prg = + let n = prg.prg_name in + let obls, rem = prg.prg_obligations in + let showed = ref 5 in + if msg then Feedback.msg_info (int rem ++ str " obligation(s) remaining: "); + Array.iteri (fun i x -> + match x.obl_body with + | None -> + if !showed > 0 then ( + decr showed; + let x = subst_deps_obl obls x in + Feedback.msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ + str "of" ++ spc() ++ Id.print n ++ str ":" ++ spc () ++ + hov 1 (Printer.pr_constr_env (Global.env ()) Evd.empty x.obl_type ++ + str "." ++ fnl ()))) + | Some _ -> ()) + obls + +let show_obligations ?(msg=true) n = + let progs = match n with + | None -> all_programs () + | Some n -> + try [ProgMap.find n !from_prg] + with Not_found -> raise (NoObligations (Some n)) + 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 + let n = prg.prg_name in + (Id.print n ++ spc () ++ str":" ++ spc () ++ + Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_type ++ spc () ++ str ":=" ++ fnl () + ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body) + +let add_definition n ?term t ctx ?(univdecl=Univdecls.default_univ_decl) + ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic + ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls = + let sign = Decls.initialize_named_context_for_proof () in + let info = Id.print n ++ str " has type-checked" in + let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce hook in + let obls,_ = prg.prg_obligations in + if Int.equal (Array.length obls) 0 then ( + Flags.if_verbose Feedback.msg_info (info ++ str "."); + let cst = declare_definition prg in + Defined cst) + else ( + let len = Array.length obls in + let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in + progmap_add n (CEphemeron.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 + | _ -> res) + +let add_mutual_definitions l ctx ?(univdecl=Univdecls.default_univ_decl) ?tactic + ?(kind=Global,false,Definition) ?(reduce=reduce) + ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind = + let sign = Decls.initialize_named_context_for_proof () in + let deps = List.map (fun (n, b, t, imps, obls) -> n) l in + List.iter + (fun (n, b, t, imps, obls) -> + let prg = init_prog_info sign ~opaque n univdecl (Some b) t ctx deps (Some fixkind) + notations obls imps kind reduce hook + in progmap_add n (CEphemeron.create prg)) l; + let _defined = + List.fold_left (fun finished x -> + if finished then finished + else + let res = auto_solve_obligations (Some x) tactic in + match res with + | Defined _ -> + (* If one definition is turned into a constant, + the whole block is defined. *) true + | _ -> false) + false deps + in () + +let admit_prog prg = + let obls, rem = prg.prg_obligations in + let obls = Array.copy obls in + Array.iteri + (fun i x -> + match x.obl_body with + | None -> + let x = subst_deps_obl obls x in + let ctx = Monomorphic_const_entry (UState.context_set prg.prg_ctx) in + let kn = Declare.declare_constant x.obl_name ~local:true + (ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural) + in + assumption_message x.obl_name; + obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) } + | Some _ -> ()) + obls; + ignore(update_obls prg obls 0) + +let rec admit_all_obligations () = + let prg = try Some (get_any_prog ()) with NoObligations _ -> None in + match prg with + | None -> () + | Some prg -> + admit_prog prg; + admit_all_obligations () + +let admit_obligations n = + match n with + | None -> admit_all_obligations () + | Some _ -> + let prg = get_prog_err n in + admit_prog prg + +let next_obligation n tac = + let prg = match n with + | None -> get_any_prog_err () + | Some _ -> get_prog_err n + in + let obls, rem = prg.prg_obligations in + let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in + let i = match Array.findi is_open obls with + | Some i -> i + | None -> anomaly (Pp.str "Could not find a solvable obligation.") + in + solve_obligation prg i tac + +let init_program () = + Coqlib.check_required_library Coqlib.datatypes_module_name; + Coqlib.check_required_library ["Coq";"Init";"Specif"]; + Coqlib.check_required_library ["Coq";"Program";"Tactics"] + +let set_program_mode c = + if c then + if !Flags.program_mode then () + else begin + init_program (); + Flags.program_mode := true; + end |