summaryrefslogtreecommitdiff
path: root/interp/constrintern.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrintern.mli')
-rw-r--r--interp/constrintern.mli110
1 files changed, 52 insertions, 58 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 767ec9ff..7a4bba10 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -1,39 +1,34 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: constrintern.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
open Names
open Term
open Sign
open Evd
open Environ
open Libnames
-open Rawterm
+open Glob_term
open Pattern
open Topconstr
open Termops
open Pretyping
-(*i*)
-(*s Translation from front abstract syntax of term to untyped terms (rawconstr)
+(** Translation from front abstract syntax of term to untyped terms (glob_constr) *)
- The translation performs:
+(** The translation performs:
- resolution of names :
- check all variables are bound
- make absolute the references to global objets
- resolution of symbolic notations using scopes
- insertion of implicit arguments
-*)
-(* To interpret implicit arguments and arg scopes of recursive variables
+ To interpret implicit arguments and arg scopes of recursive variables
while internalizing inductive types and recursive definitions, and also
projection while typing records.
@@ -45,22 +40,21 @@ type var_internalization_type =
| Inductive of identifier list (* list of params *)
| Recursive
| Method
+ | Variable
type var_internalization_data =
var_internalization_type *
- (* type of the "free" variable, for coqdoc, e.g. while typing the
- constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
+ (** type of the "free" variable, for coqdoc, e.g. while typing the
+ constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
identifier list *
- (* impargs to automatically add to the variable, e.g. for "JMeq A a B b"
+ (** impargs to automatically add to the variable, e.g. for "JMeq A a B b"
in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
Impargs.implicit_status list * (** signature of impargs of the variable *)
- scope_name option list (* subscopes of the args of the variable *)
+ scope_name option list (** subscopes of the args of the variable *)
-(* A map of free variables to their implicit arguments and scopes *)
-type internalization_env =
- (identifier * var_internalization_data) list
+(** A map of free variables to their implicit arguments and scopes *)
+type internalization_env = var_internalization_data Idmap.t
-(* Contains also a list of identifiers to automatically apply to the variables*)
val empty_internalization_env : internalization_env
val compute_internalization_data : env -> var_internalization_type ->
@@ -70,43 +64,41 @@ val compute_internalization_env : env -> var_internalization_type ->
identifier list -> types list -> Impargs.manual_explicitation list list ->
internalization_env
-type manual_implicits = (explicitation * (bool * bool * bool)) list
-
type ltac_sign = identifier list * unbound_ltac_var_map
-type raw_binder = (name * binding_kind * rawconstr option * rawconstr)
+type glob_binder = (name * binding_kind * glob_constr option * glob_constr)
-(*s Internalisation performs interpretation of global names and notations *)
+(** {6 Internalization performs interpretation of global names and notations } *)
-val intern_constr : evar_map -> env -> constr_expr -> rawconstr
+val intern_constr : evar_map -> env -> constr_expr -> glob_constr
-val intern_type : evar_map -> env -> constr_expr -> rawconstr
+val intern_type : evar_map -> env -> constr_expr -> glob_constr
val intern_gen : bool -> evar_map -> env ->
?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
- constr_expr -> rawconstr
+ constr_expr -> glob_constr
val intern_pattern : env -> cases_pattern_expr ->
Names.identifier list *
- ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list
+ ((Names.identifier * Names.identifier) list * Glob_term.cases_pattern) list
-val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder list
+val intern_context : bool -> evar_map -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list
-(*s Composing internalization with pretyping *)
+(** {6 Composing internalization with pretyping } *)
-(* Main interpretation function *)
+(** Main interpretation function *)
val interp_gen : typing_constraint -> evar_map -> env ->
?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
constr_expr -> constr
-(* Particular instances *)
+(** Particular instances *)
val interp_constr : evar_map -> env ->
constr_expr -> constr
val interp_type : evar_map -> env -> ?impls:internalization_env ->
- constr_expr -> types
+ constr_expr -> types
val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr
@@ -115,18 +107,18 @@ val interp_open_constr_patvar : evar_map -> env -> constr_expr -> evar_map * c
val interp_casted_constr : evar_map -> env -> ?impls:internalization_env ->
constr_expr -> types -> constr
-(* Accepting evars and giving back the manual implicits in addition. *)
+(** Accepting evars and giving back the manual implicits in addition. *)
val interp_casted_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env ->
- ?impls:internalization_env -> constr_expr -> types -> constr * manual_implicits
+ ?impls:internalization_env -> constr_expr -> types -> constr * Impargs.manual_implicits
val interp_type_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool ->
env -> ?impls:internalization_env ->
- constr_expr -> types * manual_implicits
+ constr_expr -> types * Impargs.manual_implicits
val interp_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool ->
env -> ?impls:internalization_env ->
- constr_expr -> constr * manual_implicits
+ constr_expr -> constr * Impargs.manual_implicits
val interp_casted_constr_evars : evar_map ref -> env ->
?impls:internalization_env -> constr_expr -> types -> constr
@@ -134,58 +126,60 @@ val interp_casted_constr_evars : evar_map ref -> env ->
val interp_type_evars : evar_map ref -> env -> ?impls:internalization_env ->
constr_expr -> types
-(*s Build a judgment *)
+(** {6 Build a judgment } *)
val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment
-(* Interprets constr patterns *)
+(** Interprets constr patterns *)
val intern_constr_pattern :
evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign ->
constr_pattern_expr -> patvar list * constr_pattern
-(* Raise Not_found if syndef not bound to a name and error if unexisting ref *)
+(** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
val intern_reference : reference -> global_reference
-(* Expands abbreviations (syndef); raise an error if not existing *)
-val interp_reference : ltac_sign -> reference -> rawconstr
+(** Expands abbreviations (syndef); raise an error if not existing *)
+val interp_reference : ltac_sign -> reference -> glob_constr
-(* Interpret binders *)
+(** Interpret binders *)
val interp_binder : evar_map -> env -> name -> constr_expr -> types
val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types
-(* Interpret contexts: returns extended env and context *)
+(** Interpret contexts: returns extended env and context *)
-val interp_context_gen : (env -> rawconstr -> types) ->
- (env -> rawconstr -> unsafe_judgment) ->
- ?global_level:bool ->
- evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
+val interp_context_gen : (env -> glob_constr -> types) ->
+ (env -> glob_constr -> unsafe_judgment) ->
+ ?global_level:bool -> ?impl_env:internalization_env ->
+ evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
-val interp_context : ?global_level:bool ->
- evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
+val interp_context : ?global_level:bool -> ?impl_env:internalization_env ->
+ evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
-val interp_context_evars : ?global_level:bool ->
- evar_map ref -> env -> local_binder list -> (env * rel_context) * manual_implicits
+val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env ->
+ evar_map ref -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
-(* Locating references of constructions, possibly via a syntactic definition *)
-(* (these functions do not modify the glob file) *)
+(** Locating references of constructions, possibly via a syntactic definition
+ (these functions do not modify the glob file) *)
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 a term as the left-hand side of a notation; the boolean
- list is a set and this set is [true] for a variable occurring in
- term position, [false] for a variable occurring in binding
- position; [true;false] if in both kinds of position *)
-
+(** Interprets a term as the left-hand side of a notation; the boolean
+ list is a set and this set is [true] for a variable occurring in
+ term position, [false] for a variable occurring in binding
+ position; [true;false] if in both kinds of position *)
val interp_aconstr : ?impls:internalization_env ->
(identifier * notation_var_internalization_type) list ->
(identifier * identifier) list -> constr_expr ->
(identifier * (subscopes * notation_var_internalization_type)) list * aconstr
-(* Globalization leak for Grammar *)
+(** Globalization options *)
+val parsing_explicit : bool ref
+
+(** Globalization leak for Grammar *)
val for_grammar : ('a -> 'b) -> 'a -> 'b