aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
diff options
context:
space:
mode:
authorGravatar Julien Forest <forest@ensiie.fr>2017-06-16 16:45:47 +0200
committerGravatar Julien Forest <forest@ensiie.fr>2017-07-29 10:28:07 +0200
commit3810a76a85a83242a739bacdfd2c8485a8e4c9da (patch)
treef9c3b50a86f44c06e16aa74907e4050c5a609ecf /plugins/funind
parent17f37f42792b3150fcebb6236b9896845957b89d (diff)
closing bug 5315
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml3
-rw-r--r--plugins/funind/glob_term_to_relation.ml25
-rw-r--r--plugins/funind/glob_termops.ml27
3 files changed, 49 insertions, 6 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 15ab396e3..5f6d78359 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -821,8 +821,9 @@ let build_proof
| Fix _ | CoFix _ ->
user_err Pp.(str ( "Anonymous local (co)fixpoints are not handled yet"))
+
| Proj _ -> user_err Pp.(str "Prod")
- | Prod _ -> user_err Pp.(str "Prod")
+ | Prod _ -> do_finalize dyn_infos g
| LetIn _ ->
let new_infos =
{ dyn_infos with
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
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 7cb35838c..003bb4e30 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -708,9 +708,6 @@ let expand_as =
in
expand_as Id.Map.empty
-
-
-
(* [resolve_and_replace_implicits ?expected_type env sigma rt] solves implicits of [rt] w.r.t. [env] and [sigma] and then replace them by their solution
*)
@@ -749,6 +746,30 @@ If someone knows how to prevent solved existantial removal in understand, pleas
Detyping.detype false [] env ctx (EConstr.of_constr (f c))
| Evar_empty -> rt (* the hole was not solved : we do nothing *)
)
+ | (GHole(BinderType na,_,_)) -> (* we only want to deal with implicit arguments *)
+ (
+ let res =
+ try (* we scan the new evar map to find the evar corresponding to this hole (by looking the source *)
+ Evd.fold (* to simulate an iter *)
+ (fun _ evi _ ->
+ match evi.evar_source with
+ | (loc_evi,BinderType na') ->
+ if Name.equal na na' && rt.CAst.loc = loc_evi then raise (Found evi)
+ | _ -> ()
+ )
+ ctx
+ ();
+ (* the hole was not solved : we do nothing *)
+ rt
+ with Found evi -> (* we found the evar corresponding to this hole *)
+ match evi.evar_body with
+ | Evar_defined c ->
+ (* we just have to lift the solution in glob_term *)
+ Detyping.detype false [] env ctx (EConstr.of_constr (f c))
+ | Evar_empty -> rt (* the hole was not solved : we d when falseo nothing *)
+ in
+ res
+ )
| _ -> Glob_ops.map_glob_constr change rt
in
change rt