package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file logic.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
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq 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 Pp
open CErrors
open Util
open Names
open Nameops
open Termops
open Environ
open Reductionops

module NamedDecl = Context.Named.Declaration

type refiner_error =

  (* Errors raised by the refiner *)
  | UnresolvedBindings of Name.t list
  | CannotApply of EConstr.t * EConstr.t
  | NonLinearProof of EConstr.t

  (* Errors raised by the tactics *)
  | IntroNeedsProduct
  | NoSuchHyp of Id.t

exception RefinerError of Environ.env * Evd.evar_map * refiner_error


let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoSuchHyp id))

(************************************************************************)
(************************************************************************)
(* Implementation of the structural rules (moving and deleting
   hypotheses around) *)

(* The ClearBody tactic *)

(* Reordering of the context *)

(* faire le minimum d'echanges pour que l'ordre donne soit un *)
(* sous-ordre du resultat. Par exemple, 2 hyps non mentionnee ne sont *)
(* pas echangees. Choix: les hyps mentionnees ne peuvent qu'etre *)
(* reculees par rapport aux autres (faire le contraire!) *)

let mt_q = (Id.Map.empty,[])
let push_val y = function
    (_,[] as q) -> q
  | (m, (x,l)::q) -> (m, (x,Id.Set.add y l)::q)
let push_item x v (m,l) =
  (Id.Map.add x v m, (x,Id.Set.empty)::l)
let mem_q x (m,_) = Id.Map.mem x m
let find_q x (m,q) =
  let v = Id.Map.find x m in
  let m' = Id.Map.remove x m in
  let rec find accs acc = function
      [] -> raise Not_found
    | [(x',l)] ->
        if Id.equal x x' then ((v,Id.Set.union accs l),(m',List.rev acc))
        else raise Not_found
    | (x',l as i)::((x'',l'')::q as itl) ->
        if Id.equal x x' then
          ((v,Id.Set.union accs l),
           (m',List.rev acc@(x'',Id.Set.add x (Id.Set.union l l''))::q))
        else find (Id.Set.union l accs) (i::acc) itl in
  find Id.Set.empty [] q

let occur_vars_in_decl env sigma hyps d =
  if Id.Set.is_empty hyps then false else
    let ohyps = global_vars_set_of_decl env sigma d in
    Id.Set.exists (fun h -> Id.Set.mem h ohyps) hyps

let reorder_context env sigma sign ord =
  let ords = List.fold_right Id.Set.add ord Id.Set.empty in
  if not (Int.equal (List.length ord) (Id.Set.cardinal ords)) then
    user_err Pp.(str "Order list has duplicates");
  let rec step ord expected ctxt_head moved_hyps ctxt_tail =
    match ord with
      | [] -> List.rev ctxt_tail @ ctxt_head
      | top::ord' when mem_q top moved_hyps ->
          let ((d,h),mh) = find_q top moved_hyps in
          if occur_vars_in_decl env sigma h d then
            user_err
              (str "Cannot move declaration " ++ Id.print top ++ spc() ++
              str "before " ++
              pr_sequence Id.print
                (Id.Set.elements (Id.Set.inter h
                  (global_vars_set_of_decl env sigma d))) ++ str ".");
          step ord' expected ctxt_head mh (d::ctxt_tail)
      | _ ->
          (match ctxt_head with
            | [] -> error_no_such_hypothesis env sigma (List.hd ord)
            | d :: ctxt ->
                let x = NamedDecl.get_id d in
                if Id.Set.mem x expected then
                  step ord (Id.Set.remove x expected)
                    ctxt (push_item x d moved_hyps) ctxt_tail
                else
                  step ord expected
                    ctxt (push_val x moved_hyps) (d::ctxt_tail)) in
  step ord ords sign mt_q []

let reorder_val_context env sigma sign ord =
match ord with
| [] | [_] ->
  (* Single variable-free definitions need not be reordered *)
  sign
| _ :: _ :: _ ->
  let open EConstr in
  val_of_named_context (reorder_context env sigma (named_context_of_val sign) ord)

let check_decl_position env sigma sign d =
  let open EConstr in
  let x = NamedDecl.get_id d in
  let needed = global_vars_set_of_decl env sigma d in
  let deps = dependency_closure env sigma (named_context_of_val sign) needed in
  if Id.List.mem x deps then
    user_err
      (str "Cannot create self-referring hypothesis " ++ Id.print x ++ str ".");
  x::deps

(* Auxiliary functions for primitive MOVE tactic
 *
 * [move_hyp with_dep toleft (left,(hfrom,typfrom),right) hto] moves
 * hyp [hfrom] at location [hto] which belongs to the hyps on the
 * left side [left] of the full signature if [toleft=true] or to the hyps
 * on the right side [right] if [toleft=false].
 * If [with_dep] then dependent hypotheses are moved accordingly. *)

(** Move destination for hypothesis *)

type 'id move_location =
  | MoveAfter of 'id
  | MoveBefore of 'id
  | MoveFirst
  | MoveLast (** can be seen as "no move" when doing intro *)

(** Printing of [move_location] *)

let pr_move_location pr_id = function
  | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id
  | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
  | MoveFirst -> str " at top"
  | MoveLast -> str " at bottom"

let move_location_eq m1 m2 = match m1, m2 with
| MoveAfter id1, MoveAfter id2 -> Id.equal id1 id2
| MoveBefore id1, MoveBefore id2 -> Id.equal id1 id2
| MoveLast, MoveLast -> true
| MoveFirst, MoveFirst -> true
| _ -> false

let mem_id_context id ctx = Id.Map.mem id ctx.Environ.env_named_map

let split_sign env sigma hfrom l =
  let () = if not (mem_id_context hfrom l) then error_no_such_hypothesis env sigma hfrom in
  let rec splitrec left sign = match EConstr.match_named_context_val sign with
  | None -> assert false
  | Some (d, right) ->
    let hyp = NamedDecl.get_id d in
    if Id.equal hyp hfrom then (left, right, d)
    else splitrec (d :: left) right
  in
  splitrec [] l

(* ocaml/ocaml#10027 triggered if inline record *)
type cannot_move_hyp = { from : Id.t; hto : Id.t move_location; hyp : Id.t }
exception CannotMoveHyp of cannot_move_hyp

let () = CErrors.register_handler (function
    | CannotMoveHyp { from; hto; hyp } ->
      Some Pp.(str "Cannot move " ++ Id.print from ++
               pr_move_location Id.print hto ++
               str ": it occurs in the declaration of " ++
               Id.print hyp ++ str ".")
    | _ -> None)

let move_hyp env sigma toleft (left,declfrom,right) hto =
  let open EConstr in
  let push prefix sign = List.fold_right push_named_context_val prefix sign in
  let push_rev prefix sign = List.fold_left (fun accu d -> push_named_context_val d accu) sign prefix in
  let rec moverec_toleft ans first middle midvars = function
    | [] -> push middle @@ push first ans
    | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) ->
      push_rev right @@ push middle @@ push first ans
    | d :: right ->
        let hyp = NamedDecl.get_id d in
        let (first', middle', midvars') =
          if occur_vars_in_decl env sigma midvars d then
            if not (move_location_eq hto (MoveAfter hyp)) then
              (first, d :: middle, Id.Set.add hyp midvars)
            else raise (CannotMoveHyp {from = NamedDecl.get_id declfrom; hto; hyp})
          else
            (d::first, middle, midvars)
        in
        if move_location_eq hto (MoveAfter hyp) then
          push_rev right @@ push middle' @@ push first' ans
        else
          moverec_toleft ans first' middle' midvars' right
  in
  let rec moverec_toright first middle depvars right = match EConstr.match_named_context_val right with
    | None -> push_rev first @@ push_rev middle right
    | Some (d, _) when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) ->
        push_rev first @@ push_rev middle @@ right
    | Some (d, right) ->
        let hyp = NamedDecl.get_id d in
        let (first', middle', depvars') =
          if Id.Set.mem hyp depvars then
            if not (move_location_eq hto (MoveAfter hyp)) then
              let vars = global_vars_set_of_decl env sigma d in
              let depvars = Id.Set.union vars depvars in
              (first, d::middle, depvars)
            else raise (CannotMoveHyp {from = NamedDecl.get_id declfrom; hto; hyp})
          else
            (d::first, middle, depvars)
        in
        if move_location_eq hto (MoveAfter hyp) then
          push_rev first' @@ push_rev middle' @@ right
        else
          moverec_toright first' middle' depvars' right
  in
  if toleft then
    let id = NamedDecl.get_id declfrom in
    moverec_toleft right [] [declfrom] (Id.Set.singleton id) left
  else
    let depvars = global_vars_set_of_decl env sigma declfrom in
    let right = moverec_toright [] [declfrom] depvars right in
    push_rev left @@ right

let move_hyp_in_named_context env sigma hfrom hto sign =
  let (left, right, declfrom) = split_sign env sigma hfrom sign in
  let toleft = match hto with
  | MoveLast -> true
  | MoveAfter id | MoveBefore id ->
    if mem_id_context id right then false
    else if mem_id_context id sign then true
    else error_no_such_hypothesis env sigma id
  | MoveFirst -> false
  in
  move_hyp env sigma toleft (left,declfrom,right) hto

let insert_decl_in_named_context env sigma decl hto sign =
  move_hyp env sigma false ([],decl,sign) hto

let convert_hyp ~check ~reorder env sigma d =
  let id = NamedDecl.get_id d in
  let b = NamedDecl.get_value d in
  let sign = Environ.named_context_val env in
  match lookup_named_ctxt id sign with
  | exception Not_found ->
    if check then error_no_such_hypothesis env sigma id
    else sign
  | d' ->
    let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in
    if check && not (is_conv env sigma (NamedDecl.get_type d) (EConstr.of_constr (NamedDecl.get_type d'))) then
      user_err
        (str "Incorrect change of the type of " ++ Id.print id ++ str ".");
    if check && not (Option.equal (is_conv env sigma) b c) then
      user_err
        (str "Incorrect change of the body of "++ Id.print id ++ str ".");
    let sign' = apply_to_hyp sign id (fun _ _ _ -> EConstr.Unsafe.to_named_decl d) in
    if reorder then reorder_val_context env sigma sign' (check_decl_position env sigma sign d)
    else sign'
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct