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
|
open Rawterm
(* Ocaml 3.06 Map.S does not handle is_empty *)
val idmap_is_empty : 'a Names.Idmap.t -> bool
(* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *)
val get_pattern_id : cases_pattern -> Names.identifier list
(* [pattern_to_term pat] returns a rawconstr corresponding to [pat].
[pat] must not contain occurences of anonymous pattern
*)
val pattern_to_term : cases_pattern -> rawconstr
(*
Some basic functions to rebuild rawconstr
In each of them the location is Util.dummy_loc
*)
val mkRRef : Libnames.global_reference -> rawconstr
val mkRVar : Names.identifier -> rawconstr
val mkRApp : rawconstr*(rawconstr list) -> rawconstr
val mkRLambda : Names.name*rawconstr*rawconstr -> rawconstr
val mkRProd : Names.name*rawconstr*rawconstr -> rawconstr
val mkRLetIn : Names.name*rawconstr*rawconstr -> rawconstr
val mkRCases : rawconstr option * tomatch_tuples * cases_clauses -> rawconstr
val mkRSort : rawsort -> rawconstr
val mkRHole : unit -> rawconstr (* we only build Evd.BinderType Anonymous holes *)
val mkRCast : rawconstr* rawconstr -> rawconstr
(*
Some basic functions to decompose rawconstrs
These are analogous to the ones constrs
*)
val raw_decompose_prod : rawconstr -> (Names.name*rawconstr) list * rawconstr
val raw_decompose_prod_or_letin :
rawconstr -> (Names.name*rawconstr option*rawconstr option) list * rawconstr
val raw_decompose_prod_n : int -> rawconstr -> (Names.name*rawconstr) list * rawconstr
val raw_decompose_prod_or_letin_n : int -> rawconstr ->
(Names.name*rawconstr option*rawconstr option) list * rawconstr
val raw_compose_prod : rawconstr -> (Names.name*rawconstr) list -> rawconstr
val raw_compose_prod_or_letin: rawconstr ->
(Names.name*rawconstr option*rawconstr option) list -> rawconstr
val raw_decompose_app : rawconstr -> rawconstr*(rawconstr list)
(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *)
val raw_make_eq : ?typ:rawconstr -> rawconstr -> rawconstr -> rawconstr
(* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *)
val raw_make_neq : rawconstr -> rawconstr -> rawconstr
(* [raw_make_or P1 P2] build the rawconstr corresponding to [P1 \/ P2] *)
val raw_make_or : rawconstr -> rawconstr -> rawconstr
(* [raw_make_or_list [P1;...;Pn]] build the rawconstr corresponding
to [P1 \/ ( .... \/ Pn)]
*)
val raw_make_or_list : rawconstr list -> rawconstr
(* alpha_conversion functions *)
(* Replace the var mapped in the rawconstr/context *)
val change_vars : Names.identifier Names.Idmap.t -> rawconstr -> rawconstr
(* [alpha_pat avoid pat] rename all the variables present in [pat] s.t.
the result does not share variables with [avoid]. This function create
a fresh variable for each occurence of the anonymous pattern.
Also returns a mapping from old variables to new ones and the concatenation of
[avoid] with the variables appearing in the result.
*)
val alpha_pat :
Names.Idmap.key list ->
Rawterm.cases_pattern ->
Rawterm.cases_pattern * Names.Idmap.key list *
Names.identifier Names.Idmap.t
(* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt
conventions and does not share bound variables with avoid
*)
val alpha_rt : Names.identifier list -> rawconstr -> rawconstr
(* same as alpha_rt but for case branches *)
val alpha_br : Names.identifier list ->
Util.loc * Names.identifier list * Rawterm.cases_pattern list *
Rawterm.rawconstr ->
Util.loc * Names.identifier list * Rawterm.cases_pattern list *
Rawterm.rawconstr
(* Reduction function *)
val replace_var_by_term :
Names.identifier ->
Rawterm.rawconstr -> Rawterm.rawconstr -> Rawterm.rawconstr
(*
[is_free_in id rt] checks if [id] is a free variable in [rt]
*)
val is_free_in : Names.identifier -> rawconstr -> bool
val are_unifiable : cases_pattern -> cases_pattern -> bool
val eq_cases_pattern : cases_pattern -> cases_pattern -> bool
(*
ids_of_pat : cases_pattern -> Idset.t
returns the set of variables appearing in a pattern
*)
val ids_of_pat : cases_pattern -> Names.Idset.t
(* TODO: finish this function (Fix not treated) *)
val ids_of_rawterm: rawconstr -> Names.Idset.t
(*
removing let_in construction in a rawterm
*)
val zeta_normalize : Rawterm.rawconstr -> Rawterm.rawconstr
val expand_as : rawconstr -> rawconstr
|
