blob: 35bed8f403eedb3fa58898ca41f72c22cd7c6fdb (
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <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 *)
(************************************************************************)
open Term
open Environ
open Evd
open Mod_subst
open Unification
open Misctypes
(** {6 The Type of Constructions clausale environments.} *)
type clausenv = {
env : env; (** the typing context *)
evd : evar_map; (** the mapping from metavar and evar numbers to their
types and values *)
templval : constr freelisted; (** the template which we are trying to fill
out *)
templtyp : constr freelisted (** its type *)}
val map_clenv : (constr -> constr) -> clausenv -> clausenv
(** subject of clenv (instantiated) *)
val clenv_value : clausenv -> constr
(** type of clenv (instantiated) *)
val clenv_type : clausenv -> types
(** substitute resolved metas *)
val clenv_nf_meta : clausenv -> constr -> constr
(** type of a meta in clenv context *)
val clenv_meta_type : clausenv -> metavariable -> types
val mk_clenv_from : Goal.goal sigma -> constr * types -> clausenv
val mk_clenv_from_n :
Goal.goal sigma -> int option -> constr * types -> clausenv
val mk_clenv_type_of : Goal.goal sigma -> constr -> clausenv
val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv
(** Refresh the universes in a clenv *)
val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst
(** {6 linking of clenvs } *)
val connect_clenv : Goal.goal sigma -> clausenv -> clausenv
val clenv_fchain :
?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
(** {6 Unification with clenvs } *)
(** Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *)
val clenv_unify :
?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
(** unifies the concl of the goal with the type of the clenv *)
val clenv_unique_resolver :
?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
val clenv_dependent : clausenv -> metavariable list
val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
(** {6 Bindings } *)
type arg_bindings = constr explicit_bindings
(** bindings where the key is the position in the template of the
clenv (dependent or not). Positions can be negative meaning to
start from the rightmost argument of the template. *)
val clenv_independent : clausenv -> metavariable list
val clenv_missing : clausenv -> metavariable list
(** for the purpose of inversion tactics *)
exception NoSuchBinding
val clenv_constrain_last_binding : constr -> clausenv -> clausenv
val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
(** start with a clenv to refine with a given term with bindings *)
(** the arity of the lemma is fixed
the optional int tells how many prods of the lemma have to be used
use all of them if None *)
val make_clenv_binding_env_apply :
env -> evar_map -> int option -> constr * constr -> constr bindings ->
clausenv
val make_clenv_binding_apply :
env -> evar_map -> int option -> constr * constr -> constr bindings ->
clausenv
val make_clenv_binding :
env -> evar_map -> constr * constr -> constr bindings -> clausenv
(** if the clause is a product, add an extra meta for this product *)
exception NotExtensibleClause
val clenv_push_prod : clausenv -> clausenv
(** {6 Pretty-print (debug only) } *)
val pr_clenv : clausenv -> Pp.std_ppcmds
|
