preliminary lens notations

_CoqProject

@@ -1,4 +1,5 @@
 -Q theories Lens
 
-theories/Lens.v
+theories/lens.v
+theories/notation.v
 theories/TC/TC.v

test-suite/demo.v

@@ -1,7 +1,13 @@
-Require Import Coq.Strings.String.
-Require Import Lens.Lens.
+(*
+ * Copyright (C) BedRock Systems Inc. 2019-2020 Gregory Malecha
+ *
+ * SPDX-License-Identifier: LGPL-2.1 WITH BedRock Exception for use over network, see repository root for details.
+ *)
+Require Import Lens.notation.
 Require Import Lens.TC.TC.
 
+Set Default Proof Using "Type".
+
 Record Oops : Set :=
 { oops1 : nat }.
 
@@ -19,12 +25,16 @@ Run TemplateProgram (genLens Foo).
 About _foo.
 About _bar.
 
-Goal view _foo {| foo := 3 ; bar := true |} = 3.
+Goal {| foo := 3 ; bar := true |} .^ _foo = 3.
 Proof. reflexivity. Qed.
 
-Goal view _bar {| foo := 3 ; bar := true |} = true.
+Goal {| foo := 3 ; bar := true |} .^ _bar = true.
 Proof. reflexivity. Qed.
 
+Goal {| foo := 3 ; bar := true |} & _bar .= false = {| foo := 3 ; bar := false |}.
+Proof. reflexivity. Qed.
 
-Goal set _bar  false {| foo := 3 ; bar := true |} = {| foo := 3 ; bar := false |}.
+Goal forall a b,
+    {| foo := a ; bar := b |} & _bar .= false
+                              & _foo .= 21 = {| foo := 21 ; bar := false |}.
 Proof. reflexivity. Qed.

theories/TC/TC.v

@@ -7,7 +7,7 @@ From MetaCoq.Template Require Import
      monad_utils Ast Loader TemplateMonad.
 Import MonadNotation.
 
-Require Import Lens.Lens.
+Require Import Lens.lens.
 
 Set Primitive Projections.
 

theories/Lens.v → theories/lens.v

@@ -1,4 +1,10 @@
+(*
+ * Copyright (C) BedRock Systems Inc. 2019-2020 Gregory Malecha
+ *
+ * SPDX-License-Identifier: LGPL-2.1 WITH BedRock Exception for use over network, see repository root for details.
+ *)
 Set Primitive Projections.
+(* Set Universe Polymorphism. *)
 
 Record Lens (a b c d : Type) : Type :=
 { view : a -> c
@@ -8,7 +14,7 @@ Record Lens (a b c d : Type) : Type :=
 Arguments over {_ _ _ _} _ _ _.
 Arguments view {_ _ _ _} _ _.
 
-Definition lens_compose {a b c d e f : Type}
+Definition compose {a b c d e f : Type}
            (l1 : Lens a b c d) (l2 : Lens c d e f)
 : Lens a b e f :=
 {| view := fun x : a => view l2 (view l1 x)

theories/notation.v

@@ -0,0 +1,20 @@
+(*
+ * Copyright (C) BedRock Systems Inc. 2019-2020 Gregory Malecha
+ *
+ * SPDX-License-Identifier: LGPL-2.1 WITH BedRock Exception for use over network, see repository root for details.
+ *)
+Require Export Lens.lens.
+
+Declare Scope lens_scope.
+Delimit Scope lens_scope with lens.
+Bind Scope lens_scope with Lens.
+
+(* not sure about these levels *)
+Notation "a & b" := (b a) (at level 50, only parsing, left associativity) : lens_scope.
+Notation "a %= f" := (lens.over a f) (at level 45, left associativity) : lens_scope.
+Notation "a .= b" := (lens.set a b) (at level 45, left associativity) : lens_scope.
+Notation "a .^ f" := (lens.view f a) (at level 44, left associativity) : lens_scope.
+(* level 19 to be compatible with Iris .@ *)
+Notation "a .@ b" := (lens.compose a b) (at level 19, left associativity) : lens_scope.
+
+Global Open Scope lens_scope.