diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 26 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 13 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.ml | 45 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.mli | 7 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 25 |
6 files changed, 63 insertions, 55 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 1db8be0818..bd2ac8c67b 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -22,26 +22,10 @@ open Pltac DECLARE PLUGIN "recdef_plugin" -let pr_binding prc = function - | loc, (NamedHyp id, c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) - | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) - -let pr_bindings prc prlc = function - | ImplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ - pr_sequence prc l - | ExplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ - pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | NoBindings -> mt () - -let pr_with_bindings prc prlc (c,bl) = - prc c ++ hv 0 (pr_bindings prc prlc bl) - let pr_fun_ind_using prc prlc _ opt_c = match opt_c with | None -> mt () - | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc b) + | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b) (* Duplication of printing functions because "'a with_bindings" is (internally) not uniform in 'a: indeed constr_with_bindings at the @@ -49,17 +33,12 @@ let pr_fun_ind_using prc prlc _ opt_c = "constr with_bindings"; hence, its printer cannot be polymorphic in (prc,prlc)... *) -let pr_with_bindings_typed prc prlc (c,bl) = - prc c ++ - hv 0 (pr_bindings prc prlc bl) - let pr_fun_ind_using_typed prc prlc _ opt_c = match opt_c with | None -> mt () | Some b -> let (b, _) = Tactics.run_delayed (Global.env ()) Evd.empty b in - spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b) - + spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b) ARGUMENT EXTEND fun_ind_using TYPED AS constr_with_bindings option @@ -80,7 +59,6 @@ TACTIC EXTEND newfuninv ] END - let pr_intro_as_pat _prc _ _ pat = match pat with | Some pat -> diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index aa8f918ae3..785633e256 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1288,17 +1288,20 @@ let do_build_inductive let t = EConstr.Unsafe.to_constr t in evd, Environ.push_named (LocalAssum (id,t)) - (* try *) - (* Typing.e_type_of env evd (mkConstU c) *) - (* with Not_found -> *) - (* raise (UserError("do_build_inductive", str "Cannot handle partial fixpoint")) *) env ) funnames (Array.of_list funconstants) (evd,Global.env ()) in - let resa = Array.map (build_entry_lc env funnames_as_set []) rta in + (* we solve and replace the implicits *) + let rta = + Array.mapi (fun i rt -> + let _,t = Typing.type_of env evd (EConstr.of_constr (mkConstU ((Array.of_list funconstants).(i)))) in + resolve_and_replace_implicits ~expected_type:(Pretyping.OfType t) env evd rt + ) rta + in + let resa = Array.map (build_entry_lc env funnames_as_set []) rta in let env_with_graphs = let rel_arity i funargs = (* Rebuilding arities (with parameters) *) let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list = diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index b99f5a923c..6fd496f508 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 diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 25d79582f3..99a258de98 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -119,3 +119,10 @@ val zeta_normalize : Glob_term.glob_constr -> Glob_term.glob_constr val expand_as : glob_constr -> glob_constr + + +(* [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 + *) +val resolve_and_replace_implicits : + ?flags:Pretyping.inference_flags -> + ?expected_type:Pretyping.typing_constraint -> Environ.env -> Evd.evar_map -> glob_constr -> glob_constr diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 143ce82886..a23c51495c 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -142,7 +142,7 @@ let rec abstract_glob_constr c = function let interp_casted_constr_with_implicits env sigma impls c = Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls - ~allow_patvar:false c + c (* Construct a fixpoint as a Glob_term diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index f373e486cf..bcfa6b9316 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -26,31 +26,6 @@ open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration -(* Some pretty printing function for debugging purpose *) - -let pr_binding prc = - function - | loc, (NamedHyp id, c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) - | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) - -let pr_bindings prc prlc = function - | ImplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ - pr_sequence prc l - | ExplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ - pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | NoBindings -> mt () - - -let pr_with_bindings prc prlc (c,bl) = - prc c ++ hv 0 (pr_bindings prc prlc bl) - - - -let pr_constr_with_binding prc (c,bl) : Pp.std_ppcmds = - pr_with_bindings prc prc (c,bl) - (* The local debugging mechanism *) (* let msgnl = Pp.msgnl *) |