aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/glob_term_to_relation.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/glob_term_to_relation.ml')
-rw-r--r--plugins/funind/glob_term_to_relation.ml25
1 files changed, 23 insertions, 2 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 379c83b24..8555a0b22 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -32,6 +32,14 @@ type binder_type =
type glob_context = (binder_type*glob_constr) list
+
+let rec solve_trivial_holes pat_as_term e =
+ match pat_as_term.CAst.v,e.CAst.v with
+ | GHole _,_ -> e
+ | GApp(fp,argsp),GApp(fe,argse) when glob_constr_eq fp fe ->
+ CAst.make (GApp((solve_trivial_holes fp fe),List.map2 solve_trivial_holes argsp argse))
+ | _,_ -> pat_as_term
+
(*
compose_glob_context [(bt_1,n_1,t_1);......] rt returns
b_1(n_1,t_1,.....,bn(n_k,t_k,rt)) where the b_i's are the
@@ -226,7 +234,12 @@ let combine_lam n t b =
compose_glob_context b.context b.value )
}
-
+let combine_prod2 n t b =
+ {
+ context = [];
+ value = mkGProd(n, compose_glob_context t.context t.value,
+ compose_glob_context b.context b.value )
+ }
let combine_prod n t b =
{ context = t.context@((Prod n,t.value)::b.context); value = b.value}
@@ -604,7 +617,9 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
let t_res = build_entry_lc env funnames avoid t in
let new_env = raw_push_named (n,None,t) env in
let b_res = build_entry_lc new_env funnames avoid b in
- combine_results (combine_prod n) t_res b_res
+ if List.length t_res.result = 1 && List.length b_res.result = 1
+ then combine_results (combine_prod2 n) t_res b_res
+ else combine_results (combine_prod n) t_res b_res
| GLetIn(n,v,typ,b) ->
(* we first compute the list of constructor
corresponding to the body of the function,
@@ -806,6 +821,12 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
let typ_as_constr = EConstr.of_constr typ_as_constr in
let typ = Detyping.detype false [] new_env (Evd.from_env env) typ_as_constr in
let pat_as_term = pattern_to_term pat in
+ (* removing trivial holes *)
+ let pat_as_term = solve_trivial_holes pat_as_term e in
+ (* observe (str "those_pattern_preconds" ++ spc () ++ *)
+ (* str "pat" ++ spc () ++ pr_glob_constr pat_as_term ++ spc ()++ *)
+ (* str "e" ++ spc () ++ pr_glob_constr e ++spc ()++ *)
+ (* str "typ_as_constr" ++ spc () ++ pr_lconstr typ_as_constr); *)
List.fold_right
(fun id acc ->
if Id.Set.mem id this_pat_ids