summaryrefslogtreecommitdiff
path: root/interp/constrintern.mli
blob: d88a058d3a3ff4092f0d52799ac5ee9846a738c5 (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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
(************************************************************************)
(*  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 9154 2006-09-20 17:18:18Z corbinea $ 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

val intern_pattern : env -> cases_pattern_expr ->
  Names.identifier list *
    ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list

val intern_pattern : env -> cases_pattern_expr ->
  Names.identifier list *
    ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list

(*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

val interp_casted_constr_evars : evar_defs ref -> env -> 
  ?impls:full_implicits_env -> constr_expr -> types -> constr

val interp_type_evars : evar_defs ref -> env -> ?impls:full_implicits_env ->
  constr_expr -> types

(*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

val interp_context_evars : 
  evar_defs ref -> 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