diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 3 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 25 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.ml | 27 | ||||
| -rw-r--r-- | plugins/funind/indfun.mli | 4 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 9 |
5 files changed, 55 insertions, 13 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 e3010e3b5..8cf5e8442 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 diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 7a60da44f..93e03852e 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,8 +1,8 @@ open Misctypes -val warn_cannot_define_graph : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit +val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit -val warn_cannot_define_principle : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit +val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit val do_generate_principle : bool -> diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 5e425cd18..2e2ced790 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -1,5 +1,4 @@ open Names -open Pp (* The mk_?_id function build different name w.r.t. a function @@ -11,7 +10,7 @@ val mk_complete_id : Id.t -> Id.t val mk_equation_id : Id.t -> Id.t -val msgnl : std_ppcmds -> unit +val msgnl : Pp.t -> unit val fresh_id : Id.t list -> string -> Id.t val fresh_name : Id.t list -> string -> Name.t @@ -24,7 +23,7 @@ val id_of_name : Name.t -> Id.t val locate_ind : Libnames.reference -> inductive val locate_constant : Libnames.reference -> Constant.t val locate_with_msg : - Pp.std_ppcmds -> (Libnames.reference -> 'a) -> + Pp.t -> (Libnames.reference -> 'a) -> Libnames.reference -> 'a val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list @@ -89,8 +88,8 @@ val update_Function : function_info -> unit (** debugging *) -val pr_info : function_info -> Pp.std_ppcmds -val pr_table : unit -> Pp.std_ppcmds +val pr_info : function_info -> Pp.t +val pr_table : unit -> Pp.t (* val function_debug : bool ref *) |