Add ∏ as a synonym for Π

It's easier for Mac users to type (option-shift-P).

Author: david-christiansen

basics.rkt

@@ -39,7 +39,7 @@
 (define-type Pie-Keyword
   (U 'U
      'Nat 'zero 'add1 'which-Nat 'iter-Nat 'rec-Nat 'ind-Nat
-     '-> '→ 'Π 'λ 'Pi 'lambda
+     '-> '→ 'Π 'λ 'Pi '∏ 'lambda
      'quote 'Atom
      'car 'cdr 'cons 'Σ 'Sigma 'Pair
      'Trivial 'sole
@@ -377,7 +377,7 @@
   (not (or (eqv? x 'U) (eqv? x 'Nat) (eqv? x 'zero)
            (eqv? x 'add1) (eqv? x 'which-Nat) (eqv? x 'ind-Nat)
            (eqv? x 'rec-Nat) (eqv? x 'iter-Nat)
-           (eqv? x '->) (eqv? x '→) (eqv? x 'Π) (eqv? x 'Pi) (eqv? x 'λ) (eqv? x 'lambda)
+           (eqv? x '->) (eqv? x '→) (eqv? x 'Π) (eqv? x 'Pi) (eqv? x '∏) (eqv? x 'λ) (eqv? x 'lambda)
            (eqv? x 'quote) (eqv? x 'Atom) (eqv? x 'Σ) (eqv? x 'Sigma) (eqv? x 'Pair)
            (eqv? x 'cons) (eqv? x 'car) (eqv? x 'cdr)
            (eqv? x 'Trivial) (eqv? x 'sole)

gui/pie-lexer.rkt

@@ -396,7 +396,7 @@
                "car" "cdr" "cong" "trans" "symm" "replace")
               'keyword]
              [("U"
-               "Π" "Pi" "->" "→"
+               "Π" "Pi" "∏" "->" "→"
                "Σ" "Sigma" "Pair"
                "Either"
                "Atom"

main.rkt

@@ -32,7 +32,7 @@
          match norm
          (rename-out [kw:U U]
                      [kw:Nat Nat] [kw:zero zero] [kw:add1 add1] [kw:which-Nat which-Nat] [kw:iter-Nat iter-Nat] [kw:rec-Nat rec-Nat] [kw:ind-Nat ind-Nat]
-                     [kw:-> ->] [kw:→ →] [kw:Π Π] [kw:λ λ] [kw:Pi Pi] [kw:lambda lambda]
+                     [kw:-> ->] [kw:→ →] [kw:Π Π] [kw:λ λ] [kw:Pi Pi] [kw:∏ ∏] [kw:lambda lambda]
                      [kw:quote quote] [kw:Atom Atom]
                      [kw:car car] [kw:cdr cdr] [kw:cons cons] [kw:Σ Σ] [kw:Sigma Sigma] [kw:Pair Pair]
                      [kw:Trivial Trivial] [kw:sole sole]
@@ -276,13 +276,14 @@
                                        [grand-op-end (send txt get-forward-sexp (add1 grandparent-sexp-start))]
                                        [grand-op-start (send txt get-backward-sexp grand-op-end)]
                                        [grand-op (send txt get-text grand-op-start grand-op-end)])
-                                      (if (member grand-op '("Pi" "Π" "Sigma" "Σ"))
+                                      (if (member grand-op '("Pi" "Π" "∏" "Sigma" "Σ"))
                                           #t
                                           #f)))
                           (define real-op
                             (match op
                               ['lambda 'λ]
                               ['Pi 'Π]
+                              ['∏ 'Π]
                               ['Sigma 'Σ]
                               ['-> '→]
                               [other other]))

parser.rkt

@@ -237,7 +237,7 @@
     #:datum-literals (U
                       Nat zero add1
                       which-Nat iter-Nat rec-Nat ind-Nat
-                      → -> Pi Π the lambda λ Atom quote
+                      → -> Pi Π ∏ the lambda λ Atom quote
                       cons car cdr Sigma Σ Pair
                       Trivial sole
                       List :: nil ind-List rec-List
@@ -280,6 +280,8 @@
                   (parse-pie #'b))]
     [(Pi ~! more ...)
      (parse-pie #'(Π more ...))]
+    [(∏ ~! more ...)
+     (parse-pie #'(Π more ...))]
     [(Π ~! (~describe "argument names and types"
                       ((x0:pie-id A0) (x:pie-id A) ...))
         (~describe "result type" B))
@@ -436,7 +438,7 @@
     #:datum-literals (U
                       Nat zero add1
                       which-Nat iter-Nat rec-Nat ind-Nat
-                      → -> Pi Π the lambda λ  Atom quote
+                      → -> Pi Π ∏ the lambda λ  Atom quote
                       cons car cdr Sigma Σ Pair
                       Trivial sole
                       List :: nil ind-List rec-List
@@ -490,20 +492,28 @@
                                   b/bindings)))
                         (car (syntax-e stx))))]
     [(Pi ~! ((x0:id A0) (x:id A) ...) B)
-     (with-syntax ([pi/loc (syntax/loc (car (syntax-e stx)) kw:Pi)]
+     (with-syntax ([sig/loc (syntax/loc (car (syntax-e stx)) kw:Pi)]
                    [A0* #'(pie->binders A0)]
                    [(A* ...) #'((pie->binders A) ...)]
                    [B* #'(pie->binders B)])
        (add-disappeared (syntax/loc stx
-                          (void pi/loc (let* ([x0 A0*] [x A*] ...) B*)))
+                          (void sig/loc (let* ([x0 A0*] [x A*] ...) B*)))
                         (car (syntax-e stx))))]
     [(Π ~! ((x0:id A0) (x:id A) ...) B)
-     (with-syntax ([pi/loc (syntax/loc (car (syntax-e stx)) kw:Π)]
+     (with-syntax ([sig/loc (syntax/loc (car (syntax-e stx)) kw:Π)]
                    [A0* #'(pie->binders A0)]
                    [(A* ...) #'((pie->binders A) ...)]
                    [B* #'(pie->binders B)])
        (add-disappeared (syntax/loc stx
-                          (void pi/loc (let* ([x0 A0*] [x A*] ...) B*)))
+                          (void sig/loc (let* ([x0 A0*] [x A*] ...) B*)))
+                        (car (syntax-e stx))))]
+    [(∏ ~! ((x0:id A0) (x:id A) ...) B)
+     (with-syntax ([sig/loc (syntax/loc (car (syntax-e stx)) kw:∏)]
+                   [A0* #'(pie->binders A0)]
+                   [(A* ...) #'((pie->binders A) ...)]
+                   [B* #'(pie->binders B)])
+       (add-disappeared (syntax/loc stx
+                          (void sig/loc (let* ([x0 A0*] [x A*] ...) B*)))
                         (car (syntax-e stx))))]
     [(Sigma ~! ((x0:id A0) (x:id A) ...) B)
      (with-syntax ([sig/loc (syntax/loc (car (syntax-e stx)) kw:Sigma)]

pie-info.rkt

@@ -22,7 +22,7 @@
 (define-pie-keywords
   U
   Nat zero add1 which-Nat iter-Nat rec-Nat ind-Nat
-  -> → Π λ Pi lambda
+  -> → Π Pi ∏ λ lambda
   quote Atom
   car cdr cons Σ Sigma Pair
   Trivial sole

pie.scrbl

@@ -233,6 +233,9 @@ The second projection of a pair. If @pie[p] is a @pie[(Σ ((_x _A)) _D)], then
 @def-type-constructor[(Pi ((x X1) (y X2) ...) B)]{
  @pie[Pi] is an alias for @pie[Π].
 }
+@def-type-constructor[(∏ ((x X1) (y X2) ...) B)]{
+ @pie[∏] is an alias for @pie[Π] that is easier to type on some keyboards.
+}
 @def-type-constructor[(→ X1 X2 ... B)]{
  @pie[→], pronounced "arrow", is shorter way of writing @pie[(Π ((x X1) (x X2) ...) B)] when the identifiers @racket[x ...] are not used.}
 @def-type-constructor[(-> X1 X2 ... B)]{@pie[->] is an alias for @pie[→].}

tests.rkt

@@ -1637,3 +1637,17 @@
                            (λ (p)
                              ((C to) p)))
                          b)))))))))))
+
+;;; Check that ∏ works as a way of writing Π
+(check-equal?
+ (rep init-ctx
+     (parse-pie #'((the (∏ ((A U) (B U))
+                    (-> (Either A B)
+                        (Either B A)))
+                (lambda (A B e)
+                  (ind-Either e
+                              (lambda (_) (Either B A))
+                              (lambda (x) (right x))
+                              (lambda (x) (left x)))))
+           Nat Trivial (left 2))))
+ (go '(the (Either Trivial Nat) (right (add1 (add1 zero))))))