package coq-serapi

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

Source file ser_pretype_errors.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
(************************************************************************)
(*         *   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)         *)
(************************************************************************)

(************************************************************************)
(* SerAPI: Coq interaction protocol with bidirectional serialization    *)
(************************************************************************)
(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+             *)
(* Copyright 2019-2023 Inria           -- License LGPL 2.1+             *)
(* Written by: Emilio J. Gallego Arias and others                       *)
(************************************************************************)

let ee = Environ.empty_env

open Sexplib.Std

module Names = Ser_names

module Term        = Ser_constr
module Evd         = Ser_evd
module Evar        = Ser_evar
module Environ     = Ser_environ
module EConstr     = Ser_eConstr
module Univ        = Ser_univ
module UGraph      = Ser_uGraph
module Type_errors = Ser_type_errors
module Locus       = Ser_locus
module Evar_kinds  = Ser_evar_kinds

type unification_error =
  [%import: Pretype_errors.unification_error]
  [@@deriving sexp]

(* workaround env being embedded in the exn, see bug #250 *)
let rec filter_ue (ue : unification_error) = match ue with
  | NotClean (e, _, c) ->
    NotClean (e, ee, c)
  | ConversionFailed (_, c1, c2) ->
    ConversionFailed (ee, c1, c2)
  | IncompatibleInstances (_, e, c1, c2) ->
    IncompatibleInstances (ee, e, c1, c2)
  | InstanceNotSameType (e, _, t1, t2) ->
    InstanceNotSameType (e, ee, t1, t2)
  | CannotSolveConstraint (e, ue) ->
    CannotSolveConstraint (e, (filter_ue ue))
  | ue -> ue

let sexp_of_unification_error ue =
  filter_ue ue |> sexp_of_unification_error

type position =
  [%import: Pretype_errors.position]
  [@@deriving sexp]

type position_reporting =
  [%import: Pretype_errors.position_reporting]
  [@@deriving sexp]

type subterm_unification_error =
  [%import: Pretype_errors.subterm_unification_error]
  [@@deriving sexp]

type type_error =
  [%import: Pretype_errors.type_error]
  [@@deriving sexp]

type pretype_error =
  [%import: Pretype_errors.pretype_error]
  [@@deriving sexp]