diff options
| -rw-r--r-- | interp/notation_ops.ml | 8 | ||||
| -rw-r--r-- | test-suite/output/Notations3.out | 17 | ||||
| -rw-r--r-- | test-suite/output/Notations3.v | 16 |
3 files changed, 38 insertions, 3 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index e6b5dc50b..804521345 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -287,9 +287,13 @@ let compare_recursive_parts found f f' (iterator,subc) = str "Both ends of the recursive pattern are the same.") | Some (x,y,Some lassoc) -> let newfound,x,y,lassoc = - if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) then + if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) || + List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi3 !found) + then !found,x,y,lassoc - else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi2 !found) then + else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi2 !found) || + List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi3 !found) + then !found,y,x,not lassoc else (pi1 !found, (x,y) :: pi2 !found, pi3 !found),x,y,lassoc in diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index c10c78652..950382d57 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -32,6 +32,23 @@ fun f : forall x : nat * (bool * unit), ?T => CURRY (x : nat) (y : bool), f forall (x : nat) (y : bool), ?T@{x:=(x, (y, tt))} where ?T : [x : nat * (bool * unit) |- Type] +fun f : forall x : bool * (nat * unit), ?T => +CURRYINV (x : nat) (y : bool), f + : (forall x : bool * (nat * unit), ?T) -> + forall (x : nat) (y : bool), ?T@{x:=(y, (x, tt))} +where +?T : [x : bool * (nat * unit) |- Type] +fun f : forall x : unit * nat * bool, ?T => CURRYLEFT (x : nat) (y : bool), f + : (forall x : unit * nat * bool, ?T) -> + forall (x : nat) (y : bool), ?T@{x:=(tt, x, y)} +where +?T : [x : unit * nat * bool |- Type] +fun f : forall x : unit * bool * nat, ?T => +CURRYINVLEFT (x : nat) (y : bool), f + : (forall x : unit * bool * nat, ?T) -> + forall (x : nat) (y : bool), ?T@{x:=(tt, y, x)} +where +?T : [x : unit * bool * nat |- Type] forall n : nat, {#n | 1 > n} : Prop forall x : nat, {|x | x > 0|} diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 9577d1074..9efac6508 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -34,9 +34,22 @@ Check ETA (x:nat) (y:nat), Nat.add. Set Printing Notations. Check ETA x y, le_S. -Notation "'CURRY' x .. y , f" := (fun x => .. (fun y => f (x, .. (y,tt) ..)) ..) (at level 200, x binder, y binder). +Notation "'CURRY' x .. y , f" := (fun x => .. (fun y => f (x, .. (y,tt) ..)) ..) + (at level 200, x binder, y binder). Check fun f => CURRY (x:nat) (y:bool), f. +Notation "'CURRYINV' x .. y , f" := (fun x => .. (fun y => f (y, .. (x,tt) ..)) ..) + (at level 200, x binder, y binder). +Check fun f => CURRYINV (x:nat) (y:bool), f. + +Notation "'CURRYLEFT' x .. y , f" := (fun x => .. (fun y => f (.. (tt,x) .., y)) ..) + (at level 200, x binder, y binder). +Check fun f => CURRYLEFT (x:nat) (y:bool), f. + +Notation "'CURRYINVLEFT' x .. y , f" := (fun x => .. (fun y => f (.. (tt,y) .., x)) ..) + (at level 200, x binder, y binder). +Check fun f => CURRYINVLEFT (x:nat) (y:bool), f. + (**********************************************************************) (* Notations with variables bound both as a term and as a binder *) (* This is #4592 *) @@ -101,3 +114,4 @@ Check fun n => foo4 n (fun x y z => (fun _ => x=0) z). (* Not printable: y, z not allowed to occur in P *) Check fun n => foo4 n (fun x y z => (fun _ => z=0) z). Check fun n => foo4 n (fun x y z => (fun _ => y=0) z). + |