From ad33c77bdff669a74f872f48af4d27e4bf18bd7d Mon Sep 17 00:00:00 2001 From: coq Date: Fri, 3 Feb 2006 21:35:08 +0000 Subject: added mli 's for the nex functional induction (forgotten last time). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7980 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/funind/indfun_common.mli | 39 ++++++++++++ contrib/funind/new_arg_principle.mli | 18 ++++++ contrib/funind/rawterm_to_relation.mli | 15 +++++ contrib/funind/rawtermops.mli | 107 +++++++++++++++++++++++++++++++++ 4 files changed, 179 insertions(+) create mode 100644 contrib/funind/indfun_common.mli create mode 100644 contrib/funind/new_arg_principle.mli create mode 100644 contrib/funind/rawterm_to_relation.mli create mode 100644 contrib/funind/rawtermops.mli (limited to 'contrib') diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli new file mode 100644 index 000000000..639063faf --- /dev/null +++ b/contrib/funind/indfun_common.mli @@ -0,0 +1,39 @@ +open Names +open Pp + +val mk_rel_id : identifier -> identifier + +val msgnl : std_ppcmds -> unit + +val invalid_argument : string -> 'a + +val fresh_id : identifier list -> string -> identifier +val fresh_name : identifier list -> string -> name +val get_name : identifier list -> ?default:string -> name -> name + +val array_get_start : 'a array -> 'a array + +val id_of_name : name -> identifier + +val locate_ind : Libnames.reference -> inductive +val locate_constant : Libnames.reference -> constant +val locate_with_msg : + Pp.std_ppcmds -> (Libnames.reference -> 'a) -> + Libnames.reference -> 'a + +val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list +val list_union_eq : + ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list +val list_add_set_eq : + ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list + +val chop_rlambda_n : int -> Rawterm.rawconstr -> + (name*Rawterm.rawconstr) list * Rawterm.rawconstr + +val chop_rprod_n : int -> Rawterm.rawconstr -> + (name*Rawterm.rawconstr) list * Rawterm.rawconstr + +val def_of_const : Term.constr -> Term.constr +val eq : Term.constr Lazy.t +val refl_equal : Term.constr Lazy.t +val const_of_id: identifier -> constant diff --git a/contrib/funind/new_arg_principle.mli b/contrib/funind/new_arg_principle.mli new file mode 100644 index 000000000..dd3630a0d --- /dev/null +++ b/contrib/funind/new_arg_principle.mli @@ -0,0 +1,18 @@ + +val generate_new_structural_principle : + (* induction principle on rel *) + Names.constant -> + (* the elimination sort *) + Term.sorts -> + (* Name of the new principle *) + (Names.identifier) option -> + (* do we want to use a principle with conclusion *) + bool -> + (* the compute functions to use *) + Names.constant array -> + int -> + unit + + + +val my_reflexivity : Tacmach.tactic diff --git a/contrib/funind/rawterm_to_relation.mli b/contrib/funind/rawterm_to_relation.mli new file mode 100644 index 000000000..51977e33d --- /dev/null +++ b/contrib/funind/rawterm_to_relation.mli @@ -0,0 +1,15 @@ + +(* val new_build_entry_lc : *) +(* Names.identifier list -> *) +(* (Names.name*Rawterm.rawconstr) list list -> *) +(* Topconstr.constr_expr list -> *) +(* Rawterm.rawconstr list -> *) +(* unit *) + +val build_inductive : + Names.identifier list -> + (Names.name*Rawterm.rawconstr) list list -> + Topconstr.constr_expr list -> + Rawterm.rawconstr list -> + unit + diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli new file mode 100644 index 000000000..fe8a4b6ce --- /dev/null +++ b/contrib/funind/rawtermops.mli @@ -0,0 +1,107 @@ +open Rawterm + +(* [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 [t1 = t2] *) +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 + +val change_vars_in_binder : + Names.identifier Names.Idmap.t -> ('a*Names.name*rawconstr) list -> + ('a*Names.name*rawconstr) list + + +(* [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 +val replace_var_by_term_in_binder : + Names.identifier -> + Rawterm.rawconstr -> + ('a * Names.name * Rawterm.rawconstr) list -> + ('a * Names.name * Rawterm.rawconstr) list + + + +(* + [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 -- cgit v1.2.3