1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Util
open Pp

module NamedDecl = Context.Named.Declaration

(* This module implements the abstract interface to goals *)
(* A general invariant of the module, is that a goal whose associated
   evar is defined in the current evar_map, should not be accessed. *)

(* type of the goals *)
type goal = Evar.t

let pr_goal e = str "GOAL:" ++ Pp.int (Evar.repr e)

let uid e = string_of_int (Evar.repr e)

(* Layer to implement v8.2 tactic engine ontop of the new architecture.
   Types are different from what they used to be due to a change of the
   internal types. *)
module V82 = struct

  (* Old style env primitive *)
  let env evars gl =
    let evi = Evd.find evars gl in
    Evd.evar_filtered_env evi

  (* Old style hyps primitive *)
  let hyps evars gl =
    let evi = Evd.find evars gl in
    Evd.evar_filtered_hyps evi

  (* same as [hyps], but ensures that existential variables are
     normalised. *)
  let nf_hyps evars gl =
    let hyps = Environ.named_context_of_val (hyps evars gl) in
    Environ.val_of_named_context (Evarutil.nf_named_context_evar evars hyps)

  (* Access to ".evar_concl" *)
  let concl evars gl =
    let evi = Evd.find evars gl in
    evi.Evd.evar_concl

  (* Old style mk_goal primitive *)
  let mk_goal evars hyps concl =
    (* A goal created that way will not be used by refine and will not
       be shelved. It must not appear as a future_goal, so the future
       goals are restored to their initial value after the evar is
       created. *)
    let prev_future_goals = Evd.save_future_goals evars in
    let evi = { Evd.evar_hyps = hyps;
                Evd.evar_concl = concl;
                Evd.evar_filter = Evd.Filter.identity;
                Evd.evar_abstract_arguments = Evd.Abstraction.identity;
                Evd.evar_body = Evd.Evar_empty;
                Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar);
                Evd.evar_candidates = None }
    in
    let (evars, evk) = Evarutil.new_pure_evar_full evars ~typeclass_candidate:false evi in
    let evars = Evd.restore_future_goals evars prev_future_goals in
    let ctxt = Environ.named_context_of_val hyps in
    let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in
    let ev = EConstr.mkEvar (evk,inst) in
    (evk, ev, evars)

  (* Instantiates a goal with an open term *)
  let partial_solution env sigma evk c =
    (* Check that the goal itself does not appear in the refined term *)
    let _ =
      if not (Evarutil.occur_evar_upto sigma evk c) then ()
      else Pretype_errors.error_occur_check env sigma evk c
    in
    Evd.define evk c sigma

  (* Instantiates a goal with an open term, using name of goal for evk' *)
  let partial_solution_to env sigma evk evk' c =
    let id = Evd.evar_ident evk sigma in
    let sigma = partial_solution env sigma evk c in
    match id with
    | None -> sigma
    | Some id -> Evd.rename evk' id sigma

  let weak_progress glss gls =
    match glss.Evd.it with
    | [ g ] -> not (Proofview.Progress.goal_equal ~evd:gls.Evd.sigma
                      ~extended_evd:glss.Evd.sigma gls.Evd.it g)
    | _ -> true

  let progress glss gls =
    weak_progress glss gls
    (* spiwack: progress normally goes like this:
    (Evd.progress_evar_map gls.Evd.sigma glss.Evd.sigma) || (weak_progress glss gls)
       This is immensly slow in the current implementation. Maybe we could
       reimplement progress_evar_map with restricted folds like "fold_undefined",
       with a good implementation of them.
    *)

  (* Used by the compatibility layer and typeclasses *)
  let nf_evar sigma gl =
    let evi = Evd.find sigma gl in
    let evi = Evarutil.nf_evar_info sigma evi in
    let sigma = Evd.add sigma gl evi in
    (gl, sigma)

  (* Goal represented as a type, doesn't take into account section variables *)
  let abstract_type sigma gl =
    let open EConstr in
    let (gl,sigma) = nf_evar sigma gl in
    let env = env sigma gl in
    let genv = Global.env () in
    let is_proof_var decl =
      try ignore (Environ.lookup_named (NamedDecl.get_id decl) genv); false
      with Not_found -> true in
    Environ.fold_named_context_reverse (fun t decl ->
                                          if is_proof_var decl then
                                            let decl = Termops.map_named_decl EConstr.of_constr decl in
                                            mkNamedProd_or_LetIn decl t
                                          else
                                            t
                                       ) ~init:(concl sigma gl) env

end

module Set = Set.Make(struct type t = goal let compare = Evar.compare end)