Library SSProve.Crypt.package.pkg_notation
Package notations
In this module we define a functor to export user-friendly notations for
packages and package codes.
The user doesn't need to instantiate the functor here, and should only rely
on the Package functor which exports the notations as well.
Scope of the notations: package_scope
delimited with
From Coq Require Import Utf8 Lia.
Set Warnings "-notation-overridden,-ambiguous-paths".
From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool ssrnum eqtype
choice seq.
Set Warnings "notation-overridden,ambiguous-paths".
From extructures Require Import ord fset fmap.
From SSProve.Crypt Require Import Prelude Axioms ChoiceAsOrd RulesStateProb
choice_type pkg_core_definition pkg_composition.
#[local] Open Scope fset.
#[local] Open Scope fset_scope.
Declare Custom Entry pack_type.
Declare Custom Entry interface.
Declare Custom Entry package.
Declare Custom Entry pack_op.
Module PackageNotation.
The `custom entry` engine does not allow a name to be a symbol without
it being a symbol in the global grammar.
As a workaround, we define 'bool and such to avoid making it impossible
to refer to bool by making it a keyword.
Notation " 'nat " := (chNat) (in custom pack_type at level 2).
Notation " 'int " := (chInt) (in custom pack_type at level 2).
Notation " 'bool " := (chBool) (in custom pack_type at level 2).
Notation " 'unit " := (chUnit) (in custom pack_type at level 2).
Notation " 'word n " := (chWord n) (in custom pack_type at level 2).
Notation " 'option x " := (chOption x) (in custom pack_type at level 2).
Notation " 'fin n " :=
(chFin (mkpos n))
(in custom pack_type at level 2, n constr).
Notation "{map x → y }" :=
(chMap x y)
(in custom pack_type at level 2, format "{map x → y }").
Notation " x × y " := (chProd x y) (in custom pack_type at level 2).
Notation " x ∐ y " := (chSum x y) (in custom pack_type at level 2).
Notation "( x )" := x (in custom pack_type, x at level 2).
Repeat the above notations here for package_scope.
Notation " 'nat " := (chNat) (at level 2) : package_scope.
Notation " 'int " := (chInt) (at level 2) : package_scope.
Notation " 'bool " := (chBool) (at level 2) : package_scope.
Notation " 'unit " := (chUnit) (at level 2) : package_scope.
Notation " 'word n " := (chWord n) (at level 2) : package_scope.
Notation " 'option x " := (chOption x) (at level 2) : package_scope.
Notation " 'fin x " :=
(chFin (mkpos x))
(at level 2) : package_scope.
(* Conflicts with this one. *)
(* Notation "{map x → y }" :=
(chMap x y)
(at level 80, format "{map x → y }") : package_scope. *)
Notation " x × y " := (chProd x y) (at level 80) : package_scope.
Notation " x ∐ y " := (chSum x y) (at level 80) : package_scope.
Notation "[ 'interface' ]" :=
(mkfmap [::])
(at level 0, only parsing)
: package_scope.
Notation "[ 'interface' x1 ]" :=
(mkfmap [:: x1 ])
(at level 0, x1 custom interface at level 2,
format "[ interface x1 ]")
: package_scope.
Notation "[ 'interface' x1 ; x2 ; .. ; xn ]" :=
(mkfmap (x1 :: x2 :: .. [:: xn] ..))
(at level 0,
x1 custom interface at level 2,
x2 custom interface at level 2,
xn custom interface at level 2,
format "[ interface '[' x1 ; '/' x2 ; '/' .. ; '/' xn ']' ]")
: package_scope.
Notation "'#val' #[ f ] : A → B" :=
(f, (A, B))
(in custom interface at level 0,
f constr, A custom pack_type, B custom pack_type,
format "#val #[ f ] : A → B").
Notation "[ 'package' L ]" :=
(mkpackage L (mkfmap [::]) _)
(at level 0, only parsing)
: package_scope.
Notation "[ 'package' L ; x1 ]" :=
(mkpackage L (mkfmap (x1 :: [::])) _)
(at level 0, x1 custom package at level 2, format "[ package L ; x1 ]")
: package_scope.
Notation "[ 'package' L ; x1 ; x2 ; .. ; xn ]" :=
(mkpackage L (mkfmap (x1 :: x2 :: .. [:: xn] ..)) _)
(at level 0,
x1 custom package at level 2,
x2 custom package at level 2,
xn custom package at level 2,
format "[ package '[' L ; '/' x1 ; '/' x2 ; '/' .. ; '/' xn ']' ]")
: package_scope.
Notation " '#def' #[ f ] ( x : A ) : B { e }" :=
((f, mkdef A B (λ x, e)))
(in custom package at level 0,
f constr, e constr, x name, A custom pack_type, B custom pack_type,
format "#def #[ f ] ( x : A ) : B { '[' '/' e '/' ']' }")
: package_scope.
Notation " '#def' #[ f ] ( ' p : A ) : B { e }" :=
((f, mkdef A B (λ p, e)))
(in custom package at level 0,
f constr, e constr, p pattern, A custom pack_type, B custom pack_type,
format "#def #[ f ] ( ' p : A ) : B { '[' '/' e '/' ']' }")
: package_scope.
Notation "#[ f ] : A → B" :=
(mkopsig f A B)
(in custom pack_op at level 0,
f constr, A custom pack_type, B custom pack_type,
format "#[ f ] : A → B").
Notation "{ 'sig' o }" :=
(o)
(at level 0, o custom pack_op at level 2, format "{ sig o }")
: package_scope.
Notation "x ← c1 ;; c2" :=
(bind c1 (λ x, c2))
(at level 100, c1 at next level, right associativity,
format "x ← c1 ;; '//' c2")
: package_scope.
Notation "' p ← c1 ;; c2" :=
(bind c1 (λ x, let p := x in c2))
(at level 100, p pattern, c1 at next level, right associativity,
format "' p ← c1 ;; '//' c2")
: package_scope.
Notation "e1 ;; e2" :=
(_ ← e1 ;; e2)%pack
(at level 100, right associativity,
format "e1 ;; '//' e2")
: package_scope.
Notation "'#put' n ':=' u ;; c" :=
(putr n u c)
(at level 100, u at next level, right associativity,
format "#put n := u ;; '//' c")
: package_scope.
Notation "x ← 'get' n ;; c" :=
(getr n (λ x, c))
(at level 100, n at next level, right associativity,
format "x ← get n ;; '//' c")
: package_scope.
Notation "' p ← 'get' n ;; c" :=
(getr n (λ x, let p := x in c))
(at level 100, p pattern, n at next level, right associativity,
format "' p ← get n ;; '//' c")
: package_scope.
Notation "x ← 'op' o ⋅ n ;; c" :=
(opr o n (λ x, c))
(at level 100, n at next level, o at next level,
right associativity,
format "x ← op o ⋅ n ;; '//' c")
: package_scope.
Notation "' p ← 'op' o ⋅ n ;; c" :=
(opr o n (λ x, let p := x in c))
(at level 100, p pattern, n at next level, o at next level,
right associativity,
format "' p ← op o ⋅ n ;; '//' c")
: package_scope.
Notation "x ← 'sample' o ;; c" :=
(sampler o (λ x, c))
(at level 100, o at next level, right associativity,
format "x ← sample o ;; '//' c")
: package_scope.
Notation "' p ← 'sample' o ;; c" :=
(sampler o (λ x, let p := x in c))
(at level 100, p pattern, o at next level, right associativity,
format "' p ← sample o ;; '//' c")
: package_scope.
Notation "x <$ o ;; c" :=
(x ← sample o ;; c)%pack
(at level 100, o at next level, right associativity,
(* format "x <*) only parsing)
: package_scope.
Notation "x ← 'cmd' o ;; c" :=
(cmd_bind o (λ x, c))
(at level 100, o at next level, right associativity,
format "x ← cmd o ;; '//' c")
: package_scope.
Notation "' p ← 'cmd' o ;; c" :=
(cmd_bind o (λ x, let p := x in c))
(at level 100, p pattern, o at next level, right associativity,
format "' p ← cmd o ;; '//' c")
: package_scope.
(* TODO Use ;; for this, and a longer notation or none at all for
bind. Bind is just a tool to compose codes while this is to compose
commands and code, much more practical.
*)
Notation "e1 ;' e2" :=
(_ ← cmd e1 ;; e2)%pack
(at level 100, right associativity,
format "e1 ;' '//' e2")
: package_scope.
Notation "'#import' s 'as' id ;; t" :=
(let id := λ x, opr s x (λ y, ret y) in t)
(at level 100, id name, s at next level, right associativity,
format "#import s as id ;; '//' t")
: package_scope.
Notation " 'int " := (chInt) (at level 2) : package_scope.
Notation " 'bool " := (chBool) (at level 2) : package_scope.
Notation " 'unit " := (chUnit) (at level 2) : package_scope.
Notation " 'word n " := (chWord n) (at level 2) : package_scope.
Notation " 'option x " := (chOption x) (at level 2) : package_scope.
Notation " 'fin x " :=
(chFin (mkpos x))
(at level 2) : package_scope.
(* Conflicts with this one. *)
(* Notation "{map x → y }" :=
(chMap x y)
(at level 80, format "{map x → y }") : package_scope. *)
Notation " x × y " := (chProd x y) (at level 80) : package_scope.
Notation " x ∐ y " := (chSum x y) (at level 80) : package_scope.
Notation "[ 'interface' ]" :=
(mkfmap [::])
(at level 0, only parsing)
: package_scope.
Notation "[ 'interface' x1 ]" :=
(mkfmap [:: x1 ])
(at level 0, x1 custom interface at level 2,
format "[ interface x1 ]")
: package_scope.
Notation "[ 'interface' x1 ; x2 ; .. ; xn ]" :=
(mkfmap (x1 :: x2 :: .. [:: xn] ..))
(at level 0,
x1 custom interface at level 2,
x2 custom interface at level 2,
xn custom interface at level 2,
format "[ interface '[' x1 ; '/' x2 ; '/' .. ; '/' xn ']' ]")
: package_scope.
Notation "'#val' #[ f ] : A → B" :=
(f, (A, B))
(in custom interface at level 0,
f constr, A custom pack_type, B custom pack_type,
format "#val #[ f ] : A → B").
Notation "[ 'package' L ]" :=
(mkpackage L (mkfmap [::]) _)
(at level 0, only parsing)
: package_scope.
Notation "[ 'package' L ; x1 ]" :=
(mkpackage L (mkfmap (x1 :: [::])) _)
(at level 0, x1 custom package at level 2, format "[ package L ; x1 ]")
: package_scope.
Notation "[ 'package' L ; x1 ; x2 ; .. ; xn ]" :=
(mkpackage L (mkfmap (x1 :: x2 :: .. [:: xn] ..)) _)
(at level 0,
x1 custom package at level 2,
x2 custom package at level 2,
xn custom package at level 2,
format "[ package '[' L ; '/' x1 ; '/' x2 ; '/' .. ; '/' xn ']' ]")
: package_scope.
Notation " '#def' #[ f ] ( x : A ) : B { e }" :=
((f, mkdef A B (λ x, e)))
(in custom package at level 0,
f constr, e constr, x name, A custom pack_type, B custom pack_type,
format "#def #[ f ] ( x : A ) : B { '[' '/' e '/' ']' }")
: package_scope.
Notation " '#def' #[ f ] ( ' p : A ) : B { e }" :=
((f, mkdef A B (λ p, e)))
(in custom package at level 0,
f constr, e constr, p pattern, A custom pack_type, B custom pack_type,
format "#def #[ f ] ( ' p : A ) : B { '[' '/' e '/' ']' }")
: package_scope.
Notation "#[ f ] : A → B" :=
(mkopsig f A B)
(in custom pack_op at level 0,
f constr, A custom pack_type, B custom pack_type,
format "#[ f ] : A → B").
Notation "{ 'sig' o }" :=
(o)
(at level 0, o custom pack_op at level 2, format "{ sig o }")
: package_scope.
Notation "x ← c1 ;; c2" :=
(bind c1 (λ x, c2))
(at level 100, c1 at next level, right associativity,
format "x ← c1 ;; '//' c2")
: package_scope.
Notation "' p ← c1 ;; c2" :=
(bind c1 (λ x, let p := x in c2))
(at level 100, p pattern, c1 at next level, right associativity,
format "' p ← c1 ;; '//' c2")
: package_scope.
Notation "e1 ;; e2" :=
(_ ← e1 ;; e2)%pack
(at level 100, right associativity,
format "e1 ;; '//' e2")
: package_scope.
Notation "'#put' n ':=' u ;; c" :=
(putr n u c)
(at level 100, u at next level, right associativity,
format "#put n := u ;; '//' c")
: package_scope.
Notation "x ← 'get' n ;; c" :=
(getr n (λ x, c))
(at level 100, n at next level, right associativity,
format "x ← get n ;; '//' c")
: package_scope.
Notation "' p ← 'get' n ;; c" :=
(getr n (λ x, let p := x in c))
(at level 100, p pattern, n at next level, right associativity,
format "' p ← get n ;; '//' c")
: package_scope.
Notation "x ← 'op' o ⋅ n ;; c" :=
(opr o n (λ x, c))
(at level 100, n at next level, o at next level,
right associativity,
format "x ← op o ⋅ n ;; '//' c")
: package_scope.
Notation "' p ← 'op' o ⋅ n ;; c" :=
(opr o n (λ x, let p := x in c))
(at level 100, p pattern, n at next level, o at next level,
right associativity,
format "' p ← op o ⋅ n ;; '//' c")
: package_scope.
Notation "x ← 'sample' o ;; c" :=
(sampler o (λ x, c))
(at level 100, o at next level, right associativity,
format "x ← sample o ;; '//' c")
: package_scope.
Notation "' p ← 'sample' o ;; c" :=
(sampler o (λ x, let p := x in c))
(at level 100, p pattern, o at next level, right associativity,
format "' p ← sample o ;; '//' c")
: package_scope.
Notation "x <$ o ;; c" :=
(x ← sample o ;; c)%pack
(at level 100, o at next level, right associativity,
(* format "x <*) only parsing)
: package_scope.
Notation "x ← 'cmd' o ;; c" :=
(cmd_bind o (λ x, c))
(at level 100, o at next level, right associativity,
format "x ← cmd o ;; '//' c")
: package_scope.
Notation "' p ← 'cmd' o ;; c" :=
(cmd_bind o (λ x, let p := x in c))
(at level 100, p pattern, o at next level, right associativity,
format "' p ← cmd o ;; '//' c")
: package_scope.
(* TODO Use ;; for this, and a longer notation or none at all for
bind. Bind is just a tool to compose codes while this is to compose
commands and code, much more practical.
*)
Notation "e1 ;' e2" :=
(_ ← cmd e1 ;; e2)%pack
(at level 100, right associativity,
format "e1 ;' '//' e2")
: package_scope.
Notation "'#import' s 'as' id ;; t" :=
(let id := λ x, opr s x (λ y, ret y) in t)
(at level 100, id name, s at next level, right associativity,
format "#import s as id ;; '//' t")
: package_scope.
Utility for fin types
m : 'fin n