Source file `refine.ml`

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
134
135
136
137
138
139
(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \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 Proofview.Notations
open Context.Named.Declaration

module NamedDecl = Context.Named.Declaration

let extract_prefix env info =
  let ctx1 = List.rev (EConstr.named_context env) in
  let ctx2 = List.rev (Evd.evar_context info) in
  let rec share l1 l2 = match l1, l2 with
  | d1 :: l1, d2 :: l2 ->
    if d1 == d2 then share l1 l2
    else 1 + List.length l2
  | _ -> List.length l2
  in
  share ctx1 ctx2

let rec recheck_hyps n env sigma sign =
  if n = 0 then sigma
  else match EConstr.match_named_context_val sign with
    | None -> assert false
    | Some (_, decl, sign') ->
      let sigma = recheck_hyps (n-1) env sigma sign' in
      let env = Environ.reset_with_named_context sign' env in
      let t = NamedDecl.get_type decl in
      let sigma, _ = Typing.sort_of env sigma t in
      let sigma = match decl with
        | LocalAssum _ -> sigma
        | LocalDef (_,body,_) -> Typing.check env sigma body t
      in
      sigma

let typecheck_evar ev env sigma =
  let info = Evd.find_undefined sigma ev in
  (* optim: avoid checking unchanged hyps *)
  let changed = extract_prefix env info in
  (* Typecheck the hypotheses. *)
  let sign = Evd.evar_hyps info in
  let sigma = recheck_hyps changed env sigma sign in
  (* Typecheck the conclusion *)
  let env = Environ.reset_with_named_context sign env in
  let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in
  sigma

let generic_refine ~typecheck f gl =
  let sigma = Proofview.Goal.sigma gl in
  let env = Proofview.Goal.env gl in
  let concl = Proofview.Goal.concl gl in
  let state = Proofview.Goal.state gl in
  (* Save the [future_goals] state to restore them after the
     refinement. *)
  let sigma = Evd.push_future_goals sigma in
  (* Create the refinement term *)
  Proofview.Unsafe.tclEVARS sigma >>= fun () ->
  f >>= fun (v, c, principal) ->
  Proofview.tclEVARMAP >>= fun sigma ->
  Proofview.wrap_exceptions begin fun () ->
  (* Check that the introduced evars are well-typed *)
  let fold accu ev = typecheck_evar ev env accu in
  let sigma = if typecheck then Evd.fold_future_goals fold sigma else sigma in
  (* Check that the refined term is typesafe *)
  let sigma = if typecheck then Typing.check env sigma c concl else sigma in
  (* Check that the goal itself does not appear in the refined term *)
  let self = Proofview.Goal.goal gl in
  let _ =
    if not (Evarutil.occur_evar_upto sigma self c) then ()
    else Pretype_errors.error_occur_check env sigma self c
  in
  (* Restore the [future goals] state. *)
  let future_goals, sigma = Evd.pop_future_goals sigma in
  (* Select the goals *)
  let future_goals = Evd.FutureGoals.map_filter (Proofview.Unsafe.advance sigma) future_goals in
  let future_goals = Evd.FutureGoals.filter (fun ev -> not @@ Evd.mem_shelf ev sigma) future_goals in
  (* Proceed to the refinement *)
  let sigma = match Proofview.Unsafe.advance sigma self with
  | None ->
    (* Nothing to do, the goal has been solved by side-effect *)
    sigma
  | Some self ->
     let sigma = match principal with
     | None -> sigma
     | Some evk -> Evd.transfer_name self evk sigma
     in Evd.define self c sigma
  in
  (* Mark goals *)
  let sigma = Proofview.Unsafe.mark_as_goals sigma (Evd.FutureGoals.comb future_goals) in
  let comb = CList.rev_map (fun x -> Proofview.goal_with_state x state) (Evd.FutureGoals.comb future_goals) in
  let trace () = Pp.(hov 2 (str"simple refine"++spc()++
                                   Termops.Internal.print_constr_env env sigma c)) in
  Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v ->
  Proofview.Unsafe.tclEVARS sigma <*>
  Proofview.Unsafe.tclSETGOALS comb <*>
  Proofview.tclUNIT v
  end

let lift c =
  Proofview.tclEVARMAP >>= fun sigma ->
  Proofview.wrap_exceptions begin fun () ->
  let (sigma, c) = c sigma in
  Proofview.Unsafe.tclEVARS sigma >>= fun () ->
  Proofview.tclUNIT c
  end

let make_refine_enter ~typecheck f gl = generic_refine ~typecheck (lift f) gl

let refine ~typecheck f =
  let f evd =
    let (evd,c) = f evd in (evd,((), c, None))
  in
  Proofview.Goal.enter (make_refine_enter ~typecheck f)

let refine_with_principal ~typecheck f =
  let f evd =
    let (evd,c, principal) = f evd in (evd,((), c, principal))
  in
  Proofview.Goal.enter (make_refine_enter ~typecheck f)

(** {7 solve_constraints}

  Ensure no remaining unification problems are left. Run at every "." by default. *)

let solve_constraints =
  let open Proofview in
  tclENV >>= fun env -> tclEVARMAP >>= fun sigma ->
   try let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
       Unsafe.tclEVARSADVANCE sigma
   with e when CErrors.noncritical e ->
     let e, info = Exninfo.capture e in
     tclZERO ~info e