aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/classops.mli
blob: 07f1623f8317af21d2fab6b1b7b70c2fa0725324 (plain)
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
(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(*i $Id$ i*)

(*i*)
open Names
open Decl_kinds
open Term
open Evd
open Environ
open Nametab
(*i*)

(*s This is the type of class kinds *)
type cl_typ = 
  | CL_SORT 
  | CL_FUN 
  | CL_SECVAR of variable
  | CL_CONST of constant
  | CL_IND of inductive

val subst_cl_typ : substitution -> cl_typ -> cl_typ

(* This is the type of infos for declared classes *)
type cl_info_typ = {
  cl_strength : strength;
  cl_param : int }

(* This is the type of coercion kinds *)
type coe_typ = Libnames.global_reference

(* This is the type of infos for declared coercions *)
type coe_info_typ 

(* [cl_index] is the type of class keys *)
type cl_index

(* [coe_index] is the type of coercion keys *)
type coe_index

(* This is the type of paths from a class to another *)
type inheritance_path = coe_index list

(*s [declare_class] adds a class to the set of declared classes *)
val declare_class : cl_typ * strength * int -> unit

(*s Access to classes infos *)
val class_info : cl_typ -> (cl_index * cl_info_typ)
val class_exists : cl_typ -> bool
val class_info_from_index : cl_index -> cl_typ * cl_info_typ

(* [find_class_type c] returns the head reference of c and its
   arguments *)
val find_class_type : constr -> cl_typ * constr list

(* raises [Not_found] if not convertible to a class *)
val class_of : env -> evar_map -> constr -> constr * cl_index

(* raises [Not_found] if not mapped to a class *)
val inductive_class_of : inductive -> cl_index

val class_args_of : constr -> constr list

(*s [declare_coercion] adds a coercion in the graph of coercion paths *)
val declare_coercion : 
  coe_typ -> unsafe_judgment -> strength -> isid:bool ->
      src:cl_typ -> target:cl_typ -> params:int -> unit

(*s Access to coercions infos *)
val coercion_exists : coe_typ -> bool

val coercion_value : coe_index -> (unsafe_judgment * bool)

(*s Lookup functions for coercion paths *)
val lookup_path_between : cl_index * cl_index -> inheritance_path
val lookup_path_to_fun_from : cl_index -> inheritance_path
val lookup_path_to_sort_from : cl_index -> inheritance_path
val lookup_pattern_path_between :
  cl_index * cl_index -> (constructor * int) list

(*i Pour le discharge *)
type coercion = coe_typ * coe_info_typ * cl_typ * cl_typ

open Libobject
val inClass : (cl_typ * cl_info_typ) -> Libobject.obj
val outClass : Libobject.obj -> (cl_typ * cl_info_typ)
val inCoercion : coercion -> Libobject.obj
val outCoercion : Libobject.obj -> coercion
val coercion_strength : coe_info_typ -> strength
val coercion_identity : coe_info_typ -> bool
val coercion_params : coe_info_typ -> int
(*i*)

(*i Crade *)
open Pp
val install_path_printer : 
  ((cl_index * cl_index) * inheritance_path -> std_ppcmds) -> unit
(*i*)

(*s This is for printing purpose *)
val string_of_class : cl_typ -> string
val pr_class : cl_typ -> std_ppcmds
val get_coercion_value : coe_index -> constr
val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list
val classes : unit -> cl_typ list
val coercions : unit -> coe_index list

(* [hide_coercion] returns the number of params to skip if the coercion must
   be hidden, [None] otherwise; it raises [Not_found] if not a coercion *)
val hide_coercion : coe_typ -> int option