Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: obligations.ml Sprache: SML

Original von: Coq^©

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 Context
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 ->
       if Evd.is_obligation_evar evm key then ()
       else
         let (loc,k) = evar_source key evm in
         Pretype_errors.error_unsolvable_implicit ?loc env evm key None)
  (Evd.undefined_map evm)

type oblinfo =
  { ev_name: int * Id.t;
    ev_hyps: Constr.named_context;
    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 hyps = EConstr.Unsafe.to_named_context hyps in
         let concl = EConstr.Unsafe.to_constr ev.evar_concl in
         let evtyp, deps, transp = etype_of_evar l hyps 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 { Evar_kinds.qm_obligation=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 hide_obligation () =
  Coqlib.check_required_library ["Coq";"Program";"Tactics"];
  UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "program.tactics.obligation")

let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
let error s = pperror (str s)

let reduce c =
  let env = Global.env () in
  let sigma = Evd.from_env env in
  EConstr.Unsafe.to_constr (Reductionops.clos_norm_flags CClosure.betaiota env sigma (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 lident option list
  | IsCoFixpoint

type notations = (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: UState.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 : Lemmas.declaration_hook option;
  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 get_hide_obligations =
  Goptions.declare_bool_option_and_ref
    ~depr:false
    ~name:"Hiding of Program obligations"
    ~key:["Hide";"Obligations"]
    ~value:false

let get_shrink_obligations =
  Goptions.declare_bool_option_and_ref
    ~depr:true (* remove in 8.8 *)
    ~name:"Shrinking of Program obligations"
    ~key:["Shrink";"Obligations"]
    ~value:true

let evar_of_obligation o = make_evar (Global.named_context_val ()) (EConstr.of_constr 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_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_prog subst prg =
  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 obligation_substitution expand prg =
  let obls, _ = prg.prg_obligations in
  let ints = intset_to (pred (Array.length obls)) in
  obl_substitution expand obls ints

let declare_definition ~ontop prg =
  let varsubst = obligation_substitution true prg in
  let body, typ = subst_prog varsubst prg in
  let nf = UnivSubst.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 obls = List.map (fun (id, (_, c)) -> (id, nf c)) varsubst in
  let uvars = Univ.LSet.union
      (Vars.universes_of_constr typ)
      (Vars.universes_of_constr 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
  let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in
  DeclareDef.declare_definition ~ontop prg.prg_name
    prg.prg_kind ce ubinders prg.prg_implicits ?hook_data

let rec lam_index n t acc =
  match Constr.kind t with
    | Lambda ({binder_name=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 defobl x =
    let oblsubst = obligation_substitution true x in
    let subs, typ = subst_prog oblsubst x in
    let env = Global.env () in
    let sigma = Evd.from_ctx x.prg_ctx in
    let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) 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
    let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_implicits) in
    let oblsubst = List.map (fun (id, (_, c)) -> id, c) oblsubst in
    def, oblsubst
  in
  let defs, obls =
    List.fold_right (fun x (defs, obls) ->
        let xdef, xobls = defobl x in
        (xdef :: defs, xobls @ obls)) l ([], [])
  in
(*   let fixdefs = List.map reduce_fix fixdefs in *)
  let fixdefs, fixrs, fixtypes, fiximps = List.split4 defs in
  let fixkind = Option.get first.prg_fixkind in
  let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
  let rvec = Array.of_list fixrs in
  let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in
  let fixdecls = (Array.map2 make_annot namevec rvec, 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.univ_entry ~poly first.prg_ctx in
  let fix_exn = Hook.get get_fix_exn () in
  let kns = List.map4 (DeclareDef.declare_fix ~ontop:None ~opaque (local, poly, kind) UnivNames.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 ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr;
    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_entry (_, uctx) ->
          Some (DefinedObl (constant, Univ.UContext.instance uctx))
        | Monomorphic_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) ?hook sign n udecl b t ctx deps fixkind
                   notations obls impls kind reduce =
  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 GlobRef.t

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 ~ontop:None 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 warn_solve_errored = CWarnings.create ~name:"solve_obligation_error" ~category:"tactics" (fun err ->
    Pp.seq [str "Solve Obligations tactic returned error: "; err; fnl ();
            str "This will become an error in the future"])

let solve_by_tac ?loc name evi t poly ctx =
  let id = name in
  (* spiwack: the status is dropped. *)
  try
    let (entry,_,ctx') =
      Pfedit.build_constant_by_tactic
        id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl 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));
    Some (fst body, entry.const_entry_type, Evd.evar_universe_context ctx')
  with
  | Refiner.FailError (_, s) as exn ->
    let _ = CErrors.push exn in
    user_err ?loc ~hdr:"solve_obligation" (Lazy.force s)
  (* If the proof is open we absorb the error and leave the obligation open *)
  | Proof.OpenProof _ ->
    None
  | e when CErrors.noncritical e ->
    let err = CErrors.print e in
    warn_solve_errored ?loc err;
    None

let obligation_terminator ?hook name num guard auto pf =
  let open Proof_global in
  let term = Lemmas.standard_proof_terminator ?hook guard in
  match pf with
  | Admitted _ -> apply_terminator term pf
  | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin
    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), Opaque -> err_not_transp ()
      | (true, _), Opaque -> err_not_transp ()
      | (false, _), Opaque -> Evar_kinds.Define true
      | (_, Evar_kinds.Define true), Transparent ->
        Evar_kinds.Define false
      | (_, status), 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.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 ~lbound:(Global.universes_lbound ()) (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))
  end
  | Proved (_, _, _ ) ->
    CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term")

let obligation_hook prg obl num auto ctx' _ _ gr =
  let obls, rem = prg.prg_obligations in
  let cst = match gr with GlobRef.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 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 ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
      let ctx' = UState.merge_subst ctx (UState.subst ctx') in
      Univ.Instance.empty, 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 ~ontop 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 ?hook guard =
    Proof_global.make_terminator
      (obligation_terminator prg.prg_name num guard ?hook auto) in
  let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in
  let pstate = Lemmas.start_proof ~ontop ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in
  let pstate = fst @@ Pfedit.by !default_tactic pstate in
  let pstate = Option.cata (fun tac -> Proof_global.set_endline_tactic tac pstate) pstate tac in
  pstate

and obligation ~ontop (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 ~ontop 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 ->
      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
        match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac
                (pi2 prg.prg_kind) (Evd.evar_universe_context evd) with
        | None -> None
        | Some (t, ty, ctx) ->
          let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) 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

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
                         let env = Global.env () in
                         let sigma = Evd.from_env env 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 env sigma 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
  let env = Global.env () in
  let sigma = Evd.from_env env in
    (Id.print n ++ spc () ++ str":" ++ spc () ++
             Printer.pr_constr_env env sigma prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
            ++ Printer.pr_constr_env env sigma prg.prg_body)

let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
                   ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
    ?(reduce=reduce) ?hook ?(opaque = false) obls =
  let sign = Lemmas.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 ~ontop:None 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=UState.default_univ_decl) ?tactic
                           ?(kind=Global,false,Definition) ?(reduce=reduce)
    ?hook ?(opaque = false) notations fixkind =
  let sign = Lemmas.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. *)
     | _ -> 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 = UState.univ_entry ~poly:false 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 ~ontop 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 ~ontop prg i tac

let check_program_libraries () =
  Coqlib.check_required_library Coqlib.datatypes_module_name;
  Coqlib.check_required_library ["Coq";"Init";"Specif"];
  Coqlib.check_required_library ["Coq";"Program";"Tactics"]

¤ Dauer der Verarbeitung: 0.79 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.