diff options
author | 2017-03-30 17:24:45 +0200 | |
---|---|---|
committer | 2017-06-01 20:02:43 +0200 | |
commit | c643a4c20b033c27b153d186128093791b687b77 (patch) | |
tree | ac76687d94f5411a533b2aa3d689a339b31e077c /plugins/funind/glob_termops.ml | |
parent | 11c1d469fc12e617d0840700bc01caf2a1d5276c (diff) |
solving implicit resolution in Function
Diffstat (limited to 'plugins/funind/glob_termops.ml')
-rw-r--r-- | plugins/funind/glob_termops.ml | 45 |
1 files changed, 45 insertions, 0 deletions
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 0361e8cb1..416e196e8 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -707,3 +707,48 @@ let expand_as = (loc,(idl,cpl, expand_as (List.fold_left add_as map cpl) rt)) 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 + *) + +exception Found of Evd.evar_info +let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expected_type=Pretyping.WithoutTypeConstraint) env sigma rt = + let open Evd in + let open Evar_kinds in + (* we first (pseudo) understand [rt] and get back the computed evar_map *) + (* FIXME : JF (30/03/2017) I'm not completely sure to have split understand as needed. +If someone knows how to prevent solved existantial removal in understand, please do not hesitate to change the computation of [ctx] here *) + let ctx,_ = Pretyping.ise_pretype_gen flags env sigma Pretyping.empty_lvar expected_type rt in + let ctx, f = Evarutil.nf_evars_and_universes ctx in + + (* then we map [rt] to replace the implicit holes by their values *) + let rec change rt = + match rt.CAst.v with + | GHole(ImplicitArg(grk,pk,bk),_,_) -> (* we only want to deal with implicit arguments *) + ( + 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,ImplicitArg(gr_evi,p_evi,b_evi)) -> + if Globnames.eq_gr grk gr_evi && pk=p_evi && bk=b_evi && 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 do nothing *) + ) + | _ -> Glob_ops.map_glob_constr change rt + in + change rt |