aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/glob_termops.mli
blob: b6d2c4543794ca164b2728ecdc51f7d1b04204fe (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
open API
open Names
open Glob_term
open Misctypes

(* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *)
val get_pattern_id : cases_pattern -> Id.t list

(* [pattern_to_term pat] returns a glob_constr corresponding to [pat].
   [pat] must not contain occurrences of anonymous pattern
*)
val pattern_to_term : cases_pattern -> glob_constr

(*
   Some basic functions to rebuild glob_constr
   In each of them the location is Util.Loc.ghost
*)
val mkGRef : Globnames.global_reference -> glob_constr
val mkGVar : Id.t -> glob_constr
val mkGApp  : glob_constr*(glob_constr list) -> glob_constr
val mkGLambda : Name.t * glob_constr * glob_constr -> glob_constr
val mkGProd : Name.t * glob_constr * glob_constr -> glob_constr
val mkGLetIn : Name.t * glob_constr * glob_constr option * glob_constr -> glob_constr
val mkGCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr
val mkGSort : glob_sort -> glob_constr
val mkGHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *)
val mkGCast : glob_constr* glob_constr -> glob_constr
(*
  Some basic functions to decompose glob_constrs
  These are analogous to the ones constrs
*)
val glob_decompose_prod : glob_constr -> (Name.t*glob_constr) list * glob_constr
val glob_decompose_prod_or_letin :
  glob_constr -> (Name.t*glob_constr option*glob_constr option) list * glob_constr
val glob_decompose_prod_n : int -> glob_constr -> (Name.t*glob_constr) list * glob_constr
val glob_decompose_prod_or_letin_n : int -> glob_constr ->
  (Name.t*glob_constr option*glob_constr option) list * glob_constr
val glob_compose_prod : glob_constr -> (Name.t*glob_constr) list  ->  glob_constr
val glob_compose_prod_or_letin: glob_constr ->
  (Name.t*glob_constr option*glob_constr option) list  ->  glob_constr
val glob_decompose_app : glob_constr -> glob_constr*(glob_constr list)


(* [glob_make_eq t1 t2] build the glob_constr corresponding to [t2 = t1] *)
val  glob_make_eq : ?typ:glob_constr -> glob_constr -> glob_constr -> glob_constr
(* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *)
val  glob_make_neq : glob_constr -> glob_constr -> glob_constr
(* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *)
val  glob_make_or : glob_constr -> glob_constr -> glob_constr

(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding
   to [P1 \/ ( .... \/ Pn)]
*)
val  glob_make_or_list : glob_constr list -> glob_constr


(* alpha_conversion functions *)



(* Replace the var mapped in the glob_constr/context *)
val change_vars : Id.t Id.Map.t -> glob_constr -> glob_constr



(* [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 occurrence 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 :
    Id.Map.key list ->
    Glob_term.cases_pattern ->
    Glob_term.cases_pattern * Id.Map.key list *
      Id.t Id.Map.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 : Id.t list -> glob_constr -> glob_constr

(* same as alpha_rt but for case branches *)
val alpha_br : Id.t list ->
  Glob_term.cases_clause ->
  Glob_term.cases_clause

(* Reduction function *)
val replace_var_by_term  :
  Id.t ->
  Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constr



(*
   [is_free_in id rt] checks if [id] is a free variable in [rt]
*)
val is_free_in : Id.t -> glob_constr -> bool


val are_unifiable : cases_pattern -> cases_pattern -> bool
val eq_cases_pattern : cases_pattern -> cases_pattern -> bool



(*
   ids_of_pat : cases_pattern -> Id.Set.t
   returns the set of variables appearing in a pattern
*)
val   ids_of_pat : cases_pattern -> Id.Set.t

(* TODO: finish this function (Fix not treated) *)
val ids_of_glob_constr: glob_constr -> Id.Set.t

(*
   removing let_in construction in a glob_constr
*)
val zeta_normalize : Glob_term.glob_constr -> Glob_term.glob_constr


val expand_as : glob_constr -> glob_constr


(* [resolve_and_replace_implicits ?expected_type env sigma rt] solves implicits of [rt] w.r.t. [env] and [sigma] and then replace them by their solution 
 *)
val resolve_and_replace_implicits :
      ?flags:Pretyping.inference_flags -> 
      ?expected_type:Pretyping.typing_constraint -> Environ.env -> Evd.evar_map -> glob_constr -> glob_constr