← Back to branch summary

~naesten/coq/trunk

« back to all changes in this revision

Viewing changes to interp/constrintern.mli

  • Committer: herbelin
  • Date: 2009-11-08 17:31:16 UTC
  • Revision ID: svn-v4:85f007b7-540e-0410-9357-904b9bb8a0f7:trunk:12481
Restructuration of command.ml + generic infrastructure for inductive schemes
- Cleaning and uniformisation in command.ml:
  - For better modularity and better visibility, two files got isolated
    out of command.ml:
    - lemmas.ml is about starting and saving a proof
    - indschemes.ml is about declaring inductive schemes
  - Decomposition of the functions of command.ml into a functional part
    and the imperative part
- Inductive schemes:
  - New architecture in ind_tables.ml for registering scheme builders,
    and for sharing and generating on demand inductive schemes
  - Adding new automatically generated equality schemes (file eqschemes.ml)
    - "_congr" for equality types (completing here commit 12273)
    - "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep",
      "_rew_backward" (similar to eq_rect), "_rew_backward_dep" for
      rewriting schemes (warning, rew_forward_dep cannot be stated following
      the standard Coq pattern for inductive types: "t=u" cannot be the
      last argument of the scheme)
    - "_case", "_case_nodep", "_case_dep" for case analysis schemes
  - Preliminary step towards discriminate and injection working on any
    equality-like type (e.g. eq_true)
  - Restating JMeq_congr under the canonical form of congruence schemes
  - Renamed "Set Equality Scheme" into "Set Equality Schemes"
  - Added "Set Rewriting Schemes", "Set Case Analysis Schemes"
  - Activation of the automatic generation of boolean equality lemmas
  - Partial debug and error messages improvements for the generation of
    boolean equality and decidable equality
  - Added schemes for making dependent rewrite working (unfortunately with
    not a fully satisfactory design - see file eqschemes.ml)
- Some names of ML function made more regular (see dev/doc/changes.txt)
- Incidentally, added a flush to obsolete Local/Global syntax warning

Show diffs side-by-side

added added

removed removed

Lines of Context:
interp/constrintern.mli
33
33
   - insert existential variables for implicit arguments
34
34
*)
35
35
 
36
 
(* To interpret implicits and arg scopes of recursive variables in
37
 
   inductive types and recursive definitions; mention of a list of
38
 
   implicits arguments in the ``rel'' part of [env]; the second
39
 
   argument associates a list of implicit positions and scopes to
40
 
   identifiers declared in the [rel_context] of [env] *)
41
 
 
42
 
type var_internalisation_type = Inductive | Recursive | Method
43
 
 
44
 
type var_internalisation_data =
45
 
  var_internalisation_type * identifier list * Impargs.implicits_list * scope_name option list
46
 
 
47
 
type implicits_env = (identifier * var_internalisation_data) list
48
 
type full_implicits_env = identifier list * implicits_env
 
36
(* To interpret implicits and arg scopes of recursive variables while
 
37
   internalizing inductive types and recursive definitions, and also
 
38
   projection while typing records.
 
39
 
 
40
   the third and fourth arguments associate a list of implicit
 
41
   positions and scopes to identifiers declared in the [rel_context]
 
42
   of [env] *)
 
43
 
 
44
type var_internalization_type = Inductive | Recursive | Method
 
45
 
 
46
type var_internalization_data =
 
47
    var_internalization_type *
 
48
    identifier list *
 
49
    Impargs.implicits_list *
 
50
    scope_name option list
 
51
 
 
52
(* A map of free variables to their implicit arguments and scopes *)
 
53
type internalization_env =
 
54
    (identifier * var_internalization_data) list
 
55
 
 
56
(* Contains also a list of identifiers to automatically apply to the variables*)
 
57
type full_internalization_env =
 
58
    identifier list * internalization_env
 
59
 
 
60
val empty_internalization_env : full_internalization_env
 
61
 
 
62
val compute_internalization_data : env -> var_internalization_type ->
 
63
  types -> Impargs.manual_explicitation list -> var_internalization_data
 
64
 
 
65
val set_internalization_env_params :
 
66
  internalization_env -> identifier list -> full_internalization_env
 
67
 
 
68
val compute_full_internalization_env : env ->
 
69
  var_internalization_type ->
 
70
  identifier list -> identifier list -> types list ->
 
71
  Impargs.manual_explicitation list list -> full_internalization_env
49
72
 
50
73
type manual_implicits = (explicitation * (bool * bool * bool)) list
51
74
 
60
83
val intern_type : evar_map -> env -> constr_expr -> rawconstr
61
84
 
62
85
val intern_gen : bool -> evar_map -> env ->
63
 
  ?impls:full_implicits_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
 
86
  ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
64
87
  constr_expr -> rawconstr
65
88
 
66
89
val intern_pattern : env -> cases_pattern_expr ->
69
92
 
70
93
val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder list
71
94
 
72
 
(*s Composing internalisation with pretyping *)
 
95
(*s Composing internalization with pretyping *)
73
96
 
74
97
(* Main interpretation function *)
75
98
 
76
99
val interp_gen : typing_constraint -> evar_map -> env ->
77
 
  ?impls:full_implicits_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
 
100
  ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
78
101
  constr_expr -> constr
79
102
 
80
103
(* Particular instances *)
82
105
val interp_constr : evar_map -> env ->
83
106
  constr_expr -> constr
84
107
 
85
 
val interp_type : evar_map -> env -> ?impls:full_implicits_env ->
 
108
val interp_type : evar_map -> env -> ?impls:full_internalization_env ->
86
109
  constr_expr -> types
87
110
 
88
111
val interp_open_constr   : evar_map -> env -> constr_expr -> evar_map * constr
89
112
 
90
113
val interp_open_constr_patvar   : evar_map -> env -> constr_expr -> evar_map * constr
91
114
 
92
 
val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env ->
 
115
val interp_casted_constr : evar_map -> env -> ?impls:full_internalization_env ->
93
116
  constr_expr -> types -> constr
94
117
 
95
118
(* Accepting evars and giving back the manual implicits in addition. *)
96
119
 
97
120
val interp_casted_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> env ->
98
 
  ?impls:full_implicits_env -> constr_expr -> types -> constr * manual_implicits
 
121
  ?impls:full_internalization_env -> constr_expr -> types -> constr * manual_implicits
99
122
 
100
123
val interp_type_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool ->
101
 
  env -> ?impls:full_implicits_env ->
 
124
  env -> ?impls:full_internalization_env ->
102
125
  constr_expr -> types * manual_implicits
103
126
 
104
127
val interp_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool ->
105
 
  env -> ?impls:full_implicits_env ->
 
128
  env -> ?impls:full_internalization_env ->
106
129
  constr_expr -> constr * manual_implicits
107
130
 
108
131
val interp_casted_constr_evars : evar_defs ref -> env ->
109
 
  ?impls:full_implicits_env -> constr_expr -> types -> constr
 
132
  ?impls:full_internalization_env -> constr_expr -> types -> constr
110
133
 
111
 
val interp_type_evars : evar_defs ref -> env -> ?impls:full_implicits_env ->
 
134
val interp_type_evars : evar_defs ref -> env -> ?impls:full_internalization_env ->
112
135
  constr_expr -> types
113
136
 
114
137
(*s Build a judgment  *)
147
170
 
148
171
(* Interprets into a abbreviatable constr *)
149
172
 
150
 
val interp_aconstr : implicits_env -> identifier list * identifier list
151
 
  -> constr_expr -> interpretation
 
173
val interp_aconstr : ?impls:full_internalization_env ->
 
174
  identifier list * identifier list -> constr_expr -> interpretation
152
175
 
153
176
(* Globalization leak for Grammar *)
154
177
val for_grammar : ('a -> 'b) -> 'a -> 'b