1 files changed, 126 insertions, 0 deletions
diff --git a/plugins/funind/rawtermops.mli b/plugins/funind/rawtermops.mli
new file mode 100644
index 00000000..455e7c89
--- /dev/null
+++ b/plugins/funind/rawtermops.mli
@@ -0,0 +1,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