diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /contrib/funind/rawtermops.mli | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'contrib/funind/rawtermops.mli')
-rw-r--r-- | contrib/funind/rawtermops.mli | 126 |
1 files changed, 0 insertions, 126 deletions
diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli deleted file mode 100644 index 358c6ba6..00000000 --- a/contrib/funind/rawtermops.mli +++ /dev/null @@ -1,126 +0,0 @@ -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 |