Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 111 insertions, 0 deletions

diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli
new file mode 100644
index 00000000..92df0ec6
--- /dev/null
+++ b/contrib/funind/rawtermops.mli
@@ -0,0 +1,111 @@
+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 *
+  (rawconstr * (Names.name * (Util.loc * Names.inductive * Names.name list) option)) list * 
+  (Util.loc * Names.identifier list * cases_pattern list * rawconstr) list -> 
+  rawconstr
+val mkRSort : rawsort -> rawconstr 
+val mkRHole : unit -> rawconstr (* we only build Evd.BinderType Anonymous holes *)
+
+(*
+  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_compose_prod : rawconstr -> (Names.name*rawconstr) 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 : 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