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

open Serlib

open Ppx_compare_lib.Builtin
open Ppx_hash_lib.Std.Hash.Builtin
open Sexplib.Conv

module CAst       = Ser_cAst
module Names      = Ser_names
module Sorts      = Ser_sorts
module Libnames   = Ser_libnames
module Constrexpr = Ser_constrexpr
module Tactypes   = Ser_tactypes
module Genintern  = Ser_genintern
module EConstr    = Ser_eConstr
module Tacexpr    = Serlib_ltac.Ser_tacexpr

module A1 = struct

type h1 = Constrexpr.constr_expr Tactypes.intro_pattern_expr CAst.t option
[@@deriving sexp,hash,compare]
type h2 = Genintern.glob_constr_and_expr Tactypes.intro_pattern_expr CAst.t option
[@@deriving sexp,hash,compare]
type h3 = Tacexpr.intro_pattern option
[@@deriving sexp,hash,compare]

end

let ser_wit_with_names =
  let open A1 in
  Ser_genarg.{
    raw_ser = sexp_of_h1
  ; raw_des = h1_of_sexp
  ; raw_hash = hash_fold_h1
  ; raw_compare = compare_h1

  ; glb_ser = sexp_of_h2
  ; glb_des = h2_of_sexp
  ; glb_hash = hash_fold_h2
  ; glb_compare = compare_h2

  ; top_ser = sexp_of_h3
  ; top_des = h3_of_sexp
  ; top_hash = hash_fold_h3
  ; top_compare = compare_h3
  }

module WitFI = struct
  type raw = Constrexpr.constr_expr Tactypes.with_bindings option
  [@@deriving sexp,hash,compare]
  type glb = Genintern.glob_constr_and_expr Tactypes.with_bindings option
  [@@deriving sexp,hash,compare]
  type top = EConstr.t Tactypes.with_bindings Ser_tactypes.delayed_open option
  [@@deriving sexp,hash,compare]
end

let ser_wit_fun_ind_using = let module M = Ser_genarg.GS(WitFI) in M.genser

module WitFS = struct
  type t = Names.variable * Libnames.qualid * Sorts.family
  [@@deriving sexp,hash,compare]
end

let ser_wit_fun_scheme_arg = let module M = Ser_genarg.GSV(WitFS) in M.genser

module Loc = Ser_loc
module Vernacexpr = Ser_vernacexpr

module WFFD = struct
  type t = Vernacexpr.fixpoint_expr Loc.located
  [@@deriving sexp,hash,compare]
end

let ser_wit_function_fix_definition =
  let module M = Ser_genarg.GS0(WFFD) in M.genser

module WAU = struct
  type raw = Constrexpr.constr_expr list
  [@@deriving sexp,hash,compare]
  type glb = Genintern.glob_constr_and_expr list
  [@@deriving sexp,hash,compare]
  type top = EConstr.constr list
  [@@deriving sexp,hash,compare]
end

let ser_wit_auto_using' = let module M = Ser_genarg.GS(WAU) in M.genser

let register () =
  Ser_genarg.register_genser Funind_plugin.G_indfun.wit_auto_using' ser_wit_auto_using';
  Ser_genarg.register_genser Funind_plugin.G_indfun.wit_constr_comma_sequence' ser_wit_auto_using';
  Ser_genarg.register_genser Funind_plugin.G_indfun.wit_with_names ser_wit_with_names;
  Ser_genarg.register_genser Funind_plugin.G_indfun.wit_fun_ind_using ser_wit_fun_ind_using;
  Ser_genarg.register_genser Funind_plugin.G_indfun.wit_fun_scheme_arg ser_wit_fun_scheme_arg;
  Ser_genarg.register_genser Funind_plugin.G_indfun.wit_function_fix_definition ser_wit_function_fix_definition;
  ()

let _ = register ()