Skip to content

Commit

Permalink
Better default patterns for depelim.
Browse files Browse the repository at this point in the history 
[dependent elimination] should now be able to produce default
patterns in every case that should succeed.
  • Loading branch information
@cmangin
cmangin committed Jan 26, 2018
1 parent 55f1270 commit 7f0df04
Show file tree
Hide file tree
Showing 3 changed files with 65 additions and 56 deletions.
23 changes: 23 additions & 0 deletions src/covering.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -161,6 +161,29 @@ and pat_of_constr sigma c =
| _ -> PInac c


let rec pat_to_user_pat ?(avoid = ref Id.Set.empty) ?loc ctx = function
| PRel i ->
let decl = List.nth ctx (pred i) in
let name = Context.Rel.Declaration.get_name decl in
let id = Namegen.next_name_away name !avoid in
avoid := Id.Set.add id !avoid;
Some (loc, Syntax.PUVar (id, false))
| PCstr (((ind, _ as cstr), _), pats) ->
let n = Inductiveops.inductive_nparams ind in
let _, pats = List.chop n pats in
Some (loc, Syntax.PUCstr (cstr, n, pats_to_lhs ~avoid ?loc ctx pats))
| PInac c ->
let id = Namegen.next_ident_away (Id.of_string "wildcard") !avoid in
avoid := Id.Set.add id !avoid;
Some (loc, Syntax.PUVar (id, true))
| PHide i -> None
and pats_to_lhs ?(avoid = ref Id.Set.empty) ?loc ctx pats =
List.map_filter (pat_to_user_pat ~avoid ?loc ctx) pats

let context_map_to_lhs ?(avoid = Id.Set.empty) ?loc (ctx, pats, _) =
let avoid = ref avoid in
List.rev (pats_to_lhs ~avoid ?loc ctx pats)

(** Pretty-printing *)

let pr_constr_pat env sigma c =
Expand Down
3 changes: 3 additions & 0 deletions src/covering.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,9 @@ val inaccs_of_constrs : constr list -> pat list
val pats_of_constrs : Evd.evar_map -> constr list -> pat list
val pat_of_constr : Evd.evar_map -> constr -> pat

(** Translating back to user patterns. *)
val context_map_to_lhs : ?avoid:Id.Set.t -> ?loc:Loc.t -> context_map -> Syntax.lhs

(** Pretty-printing *)
val pr_constr_pat : env -> Evd.evar_map -> constr -> Pp.t
val pr_pat : env -> Evd.evar_map -> pat -> Pp.t
Expand Down
95 changes: 39 additions & 56 deletions src/depelim.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -492,31 +492,6 @@ let specialize_eqs id gl =
tclFAIL 0 (str "Specialization not allowed on dependent hypotheses") gl
else specialize_eqs id gl

(* Produce a list of default patterns to eliminate an inductive value in [ind]. *)
let default_patterns env sigma ?(avoid = ref Id.Set.empty) ind : (Syntax.user_pat Loc.located) list =
let nparams = Inductiveops.inductive_nparams ind in
let mib, oib = Inductive.lookup_mind_specif env ind in
let make_pattern (i : int) : Syntax.user_pat Loc.located =
let construct = Names.ith_constructor_of_inductive ind (succ i) in
let args =
let arity = oib.mind_nf_lc.(i) in
let params, arity = EConstr.decompose_prod_n_assum sigma nparams (of_constr arity) in
let ctx, _ = EConstr.decompose_prod_assum sigma arity in
(* Make an identifier for each argument of the constructor. *)
List.rev_map (fun decl ->
let id =
match Context.Rel.Declaration.get_name decl with
| Names.Name id -> Namegen.next_ident_away id !avoid
| Names.Anonymous ->
let ty = Context.Rel.Declaration.get_type decl in
let hd = Namegen.hdchar env sigma ty in
Namegen.next_ident_away (Names.Id.of_string hd) !avoid
in avoid := Id.Set.add id !avoid;
None, Syntax.PUVar (id, true)) ctx
in
None, Syntax.PUCstr (construct, nparams, args)
in List.init (Array.length oib.mind_consnames) make_pattern

(* Dependent elimination using Equations. *)
let dependent_elim_tac ?patterns id : unit Proofview.tactic =
let open Proofview.Notations in
Expand All @@ -532,10 +507,15 @@ let dependent_elim_tac ?patterns id : unit Proofview.tactic =
let env = push_named_context sec_hyps env in

(* Check that [id] exists in the current context. *)
begin try ignore (Context.Named.lookup id loc_hyps); Proofview.tclUNIT ()
begin try
let rec lookup k = function
| decl :: _ when Id.equal id (Context.Named.Declaration.get_id decl) -> k
| _ :: sign -> lookup (succ k) sign
| [] -> raise Not_found
in Proofview.tclUNIT (lookup 1 loc_hyps)
with Not_found ->
Tacticals.New.tclZEROMSG (str "No such hypothesis: " ++ Id.print id)
end >>= fun () ->
end >>= fun rel ->

(* We want to work in a [rel_context], not a [named_context]. *)
let ctx, subst = Equations_common.rel_of_named_context loc_hyps in
Expand All @@ -547,37 +527,40 @@ let dependent_elim_tac ?patterns id : unit Proofview.tactic =
(* We also need to convert the goal for it to be well-typed in
* the [rel_context]. *)
let ty = Vars.subst_vars subst concl in
let patterns : (Syntax.user_pat Loc.located) list =
match patterns with
| None ->
(* Produce directly a user_pat. *)
let decl = Context.Named.lookup id loc_hyps in
let ty = Context.Named.Declaration.get_type decl in
let indf, _ = find_rectype env sigma ty in
let ((ind,_), _) = dest_ind_family indf in
default_patterns env sigma ind
| Some p ->
(* Interpret each pattern. *)
let avoid = ref Id.Set.empty in
List.map (Syntax.interp_pat env ~avoid) p
let rhs =
let prog = Constrexpr.CHole (None, Misctypes.IntroAnonymous, None) in
Syntax.Program (CAst.make prog, [])
in

(* For each pattern, produce a clause. *)
let make_clause : (Syntax.user_pat Loc.located) -> Syntax.clause =
fun (loc, pat) ->
let lhs =
List.rev_map (fun decl ->
let decl_id = Context.Named.Declaration.get_id decl in
if Names.Id.equal decl_id id then loc, pat
else None, Syntax.PUVar (decl_id, false)) loc_hyps
in
let rhs =
let prog = Constrexpr.CHole (None, Misctypes.IntroAnonymous, None) in
Syntax.Program (CAst.make prog, [])
begin match patterns with
| None ->
(* Produce default clauses from the variable to split. *)
let evd = ref sigma in
begin match Covering.split_var (env, evd) rel ctx with
| None -> Tacticals.New.tclZEROMSG (str "Could not eliminate variable " ++ Id.print id)
| Some (_, newctx, brs) ->
let brs = Option.List.flatten (Array.to_list brs) in
let clauses_lhs = List.map Covering.context_map_to_lhs brs in
let clauses = List.map (fun lhs -> (default_loc, lhs, rhs)) clauses_lhs in
Proofview.tclUNIT clauses
end
| Some p ->
(* Interpret each pattern to then produce clauses. *)
let patterns : (Syntax.user_pat Loc.located) list =
let avoid = ref Id.Set.empty in
List.map (Syntax.interp_pat env ~avoid) p
in
(Option.default default_loc loc, lhs, rhs)
in
let clauses : Syntax.clause list = List.map make_clause patterns in
(* For each pattern, produce a clause. *)
let make_clause : (Syntax.user_pat Loc.located) -> Syntax.clause =
fun (loc, pat) ->
let lhs =
List.rev_map (fun decl ->
let decl_id = Context.Named.Declaration.get_id decl in
if Names.Id.equal decl_id id then loc, pat
else None, Syntax.PUVar (decl_id, false)) loc_hyps
in
(Option.default default_loc loc, lhs, rhs)
in Proofview.tclUNIT (List.map make_clause patterns)
end >>= fun clauses ->
if !debug then
Feedback.msg_info (str "Generated clauses: " ++ fnl() ++ Syntax.pr_clauses env clauses);

Expand Down

0 comments on commit 7f0df04

Please sign in to comment.