It should be possible to declare notations which parse terms as uconstrs

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#4728
From: @JasonGross
Reported version: 8.5
CC: coq-bugs-redist@lists.gforge.inria.fr

[coqbot]

Comment author: @JasonGross

I'd like the final [Check] in the following to work:

Ltac fin_eta_expand :=
  [ > lazymatch goal with
      | [ H : _ |- _ ] => clear H
      end..
  | lazymatch goal with
    | [ H : ?T |- ?T ]
      => exact H
    | [ |- ?G ]
      => fail 0 "No hypothesis matching" G
    end ];
  let n := numgoals in
  tryif constr_eq numgoals 0
  then idtac
  else fin_eta_expand.

Ltac pre_eta_expand x :=
  let T := type of x in
  let G := match goal with |- ?G => G end in
  unify T G;
  unshelve econstructor;
  destruct x;
  fin_eta_expand.

Ltac eta_expand x :=
  let v := constr:(ltac:(pre_eta_expand x)) in
  idtac v;
  let v := (eval cbv beta iota zeta in v) in
  exact v.

Notation eta_expand x := (ltac:(eta_expand x)) (only parsing).

Ltac partial_unify eqn :=
  lazymatch eqn with
  | ?x = ?x => idtac
  | ?f ?x = ?g ?y
    => partial_unify (f = g);
       (tryif unify x y then
           idtac
         else tryif has_evar x then
             unify x y
           else tryif has_evar y then
               unify x y
             else
               idtac)
  | ?x = ?y
    => idtac;
       (tryif unify x y then
           idtac
         else tryif has_evar x then
             unify x y
           else tryif has_evar y then
               unify x y
             else
               idtac)
  end.

Tactic Notation "{" open_constr(old_record) "with" open_constr(new_record) "}" :=
  let old_record' := eta_expand old_record in
  partial_unify (old_record = new_record);
  eexact new_record.

Set Implicit Arguments.
Record prod A B := pair { fst : A ; snd : B }.
Infix "*" := prod : type_scope.
Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.

Notation "{ old 'with' new }" := (ltac:({ old with new })) (only parsing).

Check ltac:({ (1, 1) with {| snd := 2 |} }).
Check { (1, 1) with {| snd := 2 |} }. (* Error: Cannot infer this placeholder of type "Type". *)

[JasonGross]

Here's another version of the record-updating code that would also be made slightly better with uconstr-in-notations:

Definition marker {T} (v : T) := v.                                                                                                                                                                         
Ltac apply_with_underscores f x :=                                                                                                                                                                          
  match constr:(Set) with                                                                                                                                                                                   
  | _ => constr:(f x)                                                                                                                                                                                       
  | _ => apply_with_underscores uconstr:(f _) x                                                                                                                                                             
  end.                                                                                                                                                                                                      
Ltac update_record v accessor new_value :=                                                                                                                                                                  
  let T := type of v in                                                                                                                                                                                     
  let v' := open_constr:(ltac:(econstructor) : T) in                                                                                                                                                        
  let accessed := apply_with_underscores accessor v' in                                                                                                                                                     
  let accessed := (eval hnf in accessed) in                                                                                                                                                                 
  let unif := open_constr:(eq_refl : accessed = marker _) in                                                                                                                                                
  let v'' := (eval cbv [marker] in v') in                                                                                                                                                                   
  let unif := constr:(eq_refl : v = v'') in                                                                                                                                                                 
  lazymatch v' with                                                                                                                                                                                         
  | context G[marker _] => let G' := context G[new_value] in                                                                                                                                                
                           G'                                                                                                                                                                               
  end.                                                                                                                                                                                                      
                                                                                                                                                                                                            
Tactic Notation "update!" constr(v) "setting" uconstr(accessor) "to" constr(new_value)                                                                                                                      
  := let res := update_record v accessor new_value in                                                                                                                                                       
     exact res.                                                                                                                                                                                             
                                                                                                                                                                                                            
Set Primitive Projections.                                                                                                                                                                                  
Record prod A B := pair { fst : A ; snd : B }.                                                                                                                                                              
Arguments pair {A B} _ _.                                                                                                                                                                                   
Arguments fst {A B} _.                                                                                                                                                                                      
Arguments snd {A B} _.                                                                                                                                                                                      
                                                                                                                                                                                                            
Notation "'update!' v 'setting' accessor 'to' new_value" := (ltac:(update! v setting accessor to new_value)) (only parsing, at level 90).                                                                   
Check ltac:(update! {| fst := 1 ; snd := 2 |} setting fst to 3).                                                                                                                                            
Check update! {| fst := 1 ; snd := 2 |} setting @fst to 3.