blob: cdd87a7c15017a4f27e6ce1572e4bd365adc25f1 (
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
117
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: constrintern.mli 7732 2005-12-26 13:51:24Z herbelin $ i*)
(*i*)
open Names
open Term
open Sign
open Evd
open Environ
open Libnames
open Rawterm
open Pattern
open Topconstr
open Termops
open Pretyping
(*i*)
(*s Translation from front abstract syntax of term to untyped terms (rawconstr)
The translation performs:
- resolution of names :
- check all variables are bound
- make absolute the references to global objets
- resolution of symbolic notations using scopes
- insert existential variables for implicit arguments
*)
(* To interpret implicits and arg scopes of recursive variables in
inductive types and recursive definitions; mention of a list of
implicits arguments in the ``rel'' part of [env]; the second
argument associates a list of implicit positions and scopes to
identifiers declared in the [rel_context] of [env] *)
type var_internalisation_data =
identifier list * Impargs.implicits_list * scope_name option list
type implicits_env = (identifier * var_internalisation_data) list
type full_implicits_env = identifier list * implicits_env
type ltac_sign = identifier list * unbound_ltac_var_map
(*s Internalisation performs interpretation of global names and notations *)
val intern_constr : evar_map -> env -> constr_expr -> rawconstr
val intern_gen : bool -> evar_map -> env ->
?impls:full_implicits_env -> ?allow_soapp:bool -> ?ltacvars:ltac_sign ->
constr_expr -> rawconstr
(*s Composing internalisation with pretyping *)
(* Main interpretation function *)
val interp_gen : typing_constraint -> evar_map -> env ->
?impls:full_implicits_env -> ?allow_soapp:bool -> ?ltacvars:ltac_sign ->
constr_expr -> constr
(* Particular instances *)
val interp_constr : evar_map -> env ->
constr_expr -> constr
val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env ->
constr_expr -> types -> constr
val interp_type : evar_map -> env -> ?impls:full_implicits_env ->
constr_expr -> types
val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr
(*s Build a judgment *)
val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment
(* Interprets constr patterns *)
val interp_constrpattern :
evar_map -> env -> constr_expr -> patvar list * constr_pattern
val interp_reference : ltac_sign -> reference -> rawconstr
(* Interpret binders *)
val interp_binder : evar_map -> env -> name -> constr_expr -> types
(* Interpret contexts: returns extended env and context *)
val interp_context : evar_map -> env -> local_binder list -> env * rel_context
(* Locating references of constructions, possibly via a syntactic definition *)
val locate_reference : qualid -> global_reference
val is_global : identifier -> bool
val construct_reference : named_context -> identifier -> constr
val global_reference : identifier -> constr
val global_reference_in_absolute_module : dir_path -> identifier -> constr
(* Interprets into a abbreviatable constr *)
val interp_aconstr : implicits_env -> identifier list -> constr_expr ->
interpretation
(* Globalization leak for Grammar *)
val for_grammar : ('a -> 'b) -> 'a -> 'b
(* Coqdoc utility functions *)
type coqdoc_state
val coqdoc_freeze : unit -> coqdoc_state
val coqdoc_unfreeze : coqdoc_state -> unit
|
