summaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/Recdef.v2
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--plugins/funind/invfun.ml11
-rw-r--r--plugins/funind/merge.ml2
-rw-r--r--plugins/funind/rawterm_to_relation.ml79
-rw-r--r--plugins/funind/recdef.ml4
6 files changed, 85 insertions, 15 deletions
diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v
index b29b8362..763ed82f 100644
--- a/plugins/funind/Recdef.v
+++ b/plugins/funind/Recdef.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index e47f19bf..41fafdf1 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 84470a0f..aa42f6cd 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -504,6 +504,15 @@ and intros_with_rewrite_aux : tactic =
intros_with_rewrite
]
g
+ else if isVar args.(2)
+ then
+ let id = pf_get_new_id (id_of_string "y") g in
+ tclTHENSEQ [ h_intro id;
+ generalize_dependent_of (destVar args.(2)) id;
+ tclTRY (Equality.rewriteRL (mkVar id));
+ intros_with_rewrite
+ ]
+ g
else
begin
let id = pf_get_new_id (id_of_string "y") g in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 799180b7..40ee116d 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml
index 3c3a36f0..b74422a3 100644
--- a/plugins/funind/rawterm_to_relation.ml
+++ b/plugins/funind/rawterm_to_relation.ml
@@ -716,11 +716,11 @@ and build_entry_lc_from_case env funname make_discr
*)
let case_resl =
List.fold_right
- (fun (case_arg,_) ctxt_argsl ->
- let arg_res = build_entry_lc env funname avoid case_arg in
- combine_results combine_args arg_res ctxt_argsl
- )
- el
+ (fun (case_arg,_) ctxt_argsl ->
+ let arg_res = build_entry_lc env funname avoid case_arg in
+ combine_results combine_args arg_res ctxt_argsl
+ )
+ el
(mk_result [] [] avoid)
in
let types =
@@ -876,6 +876,32 @@ let is_res id =
with Invalid_argument _ -> false
+
+let same_raw_term rt1 rt2 =
+ match rt1,rt2 with
+ | RRef(_,r1), RRef (_,r2) -> r1=r2
+ | RHole _, RHole _ -> true
+ | _ -> false
+let decompose_raw_eq lhs rhs =
+ let rec decompose_raw_eq lhs rhs acc =
+ observe (str "decomposing eq for " ++ pr_rawconstr lhs ++ str " " ++ pr_rawconstr rhs);
+ let (rhd,lrhs) = raw_decompose_app rhs in
+ let (lhd,llhs) = raw_decompose_app lhs in
+ observe (str "lhd := " ++ pr_rawconstr lhd);
+ observe (str "rhd := " ++ pr_rawconstr rhd);
+ observe (str "llhs := " ++ int (List.length llhs));
+ observe (str "lrhs := " ++ int (List.length lrhs));
+ let sllhs = List.length llhs in
+ let slrhs = List.length lrhs in
+ if same_raw_term lhd rhd && sllhs = slrhs
+ then
+ (* let _ = assert false in *)
+ List.fold_right2 decompose_raw_eq llhs lrhs acc
+ else (lhs,rhs)::acc
+ in
+ decompose_raw_eq lhs rhs []
+
+
exception Continue
(*
The second phase which reconstruct the real type of the constructor.
@@ -1032,6 +1058,41 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
mkRProd(n,t,new_b),id_to_exclude
else new_b, Idset.add id id_to_exclude
*)
+ | RApp(loc1,RRef(loc2,eq_as_ref),[ty;rt1;rt2])
+ when eq_as_ref = Lazy.force Coqlib.coq_eq_ref && n = Anonymous
+ ->
+ begin
+ try
+ let l = decompose_raw_eq rt1 rt2 in
+ if List.length l > 1
+ then
+ let new_rt =
+ List.fold_left
+ (fun acc (lhs,rhs) ->
+ mkRProd(Anonymous,
+ mkRApp(mkRRef(eq_as_ref),[mkRHole ();lhs;rhs]),acc)
+ )
+ b
+ l
+ in
+ rebuild_cons env nb_args relname args crossed_types depth new_rt
+ else raise Continue
+ with Continue ->
+ observe (str "computing new type for prod : " ++ pr_rawconstr rt);
+ let t' = Pretyping.Default.understand Evd.empty env t in
+ let new_env = Environ.push_rel (n,None,t') env in
+ let new_b,id_to_exclude =
+ rebuild_cons new_env
+ nb_args relname
+ args new_crossed_types
+ (depth + 1) b
+ in
+ match n with
+ | Name id when Idset.mem id id_to_exclude && depth >= nb_args ->
+ new_b,Idset.remove id
+ (Idset.filter not_free_in_t id_to_exclude)
+ | _ -> mkRProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude
+ end
| _ ->
observe (str "computing new type for prod : " ++ pr_rawconstr rt);
let t' = Pretyping.Default.understand Evd.empty env t in
@@ -1122,12 +1183,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
(* debuging wrapper *)
let rebuild_cons env nb_args relname args crossed_types rt =
-(* observennl (str "rebuild_cons : rt := "++ pr_rawconstr rt ++ *)
-(* str "nb_args := " ++ str (string_of_int nb_args)); *)
+ observe (str "rebuild_cons : rt := "++ pr_rawconstr rt ++
+ str "nb_args := " ++ str (string_of_int nb_args));
let res =
rebuild_cons env nb_args relname args crossed_types 0 rt
in
-(* observe (str " leads to "++ pr_rawconstr (fst res)); *)
+ observe (str " leads to "++ pr_rawconstr (fst res));
res
@@ -1266,7 +1327,7 @@ let do_build_inductive
(function result (* (args',concl') *) ->
let rt = compose_raw_context result.context result.value in
let nb_args = List.length funsargs.(i) in
- (* with_full_print (fun rt -> Pp.msgnl (str "raw constr " ++ pr_rawconstr rt)) rt; *)
+ (* with_full_print (fun rt -> Pp.msgnl (str "raw constr " ++ pr_rawconstr rt)) rt; *)
fst (
rebuild_cons env_with_graphs nb_args relnames.(i)
[]
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9c4cc78a..83868da9 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: recdef.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: recdef.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Term
open Termops
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-04 07:56:35 +0000