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

4 files changed, 179 insertions, 0 deletions

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