Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Replace right squiggle arrow with thick arrow #53

Merged
merged 1 commit into from
Aug 30, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion emacs/polytt-mode.el
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@
"Symbols for binders.")

(defconst polytt-expression-symbols
'("→" "←" "×" "⇝" "⇜" "∘" "⇒")
'("→" "←" "×" "⇜" "∘" "⇒")
"Expression symbols.")

(defconst polytt-mode-font-lock-keywords
Expand Down
28 changes: 14 additions & 14 deletions examples/prelude.poly
Original file line number Diff line number Diff line change
Expand Up @@ -57,29 +57,29 @@ def tensor : Poly → Poly → Poly :=


def id : Π (P : Poly), P ⇒ P :=
λ P → λ a⁺ ⇜ a⁻
λ P → λ a⁺ ⇜ a⁻
return a⁺ ⇜ a⁻

#print (λ P → P) : Poly → Poly

#print (λ P → λ a⁺ ⇜ a⁻ return a⁺ ⇜ a⁻) : Π (P : Poly), P ⇒ P
#print (λ P → λ a⁺ ⇜ a⁻ return a⁺ ⇜ a⁻) : Π (P : Poly), P ⇒ P

def nyan-hom : ℕ → nyan ⇒ nyan :=
λ n → λ a⁺ ⇜ a⁻
λ n → λ a⁺ ⇜ a⁻
let (b⁺ ⇜ b⁻) := (id nyan) (a⁺ ⇜ a⁻);
return n ⇜ (b⁻ ∘ succ ∘ succ)

#normalize nyan-hom 42 1

def nyan-hom2 : nyan ⇒ nyan :=
λ a⁺ ⇜ a⁻
λ a⁺ ⇜ a⁻
let (b⁺ ⇜ b⁻) := (nyan-hom 12) (a⁺ ⇜ a⁻);
return b⁺ ⇜ b⁻

#normalize nyan-hom2 1

def compose : Π (P Q R : Poly), Q ⇒ R → P ⇒ Q → P ⇒ R :=
λ P Q R f g → λ p⁺ ⇜ p⁻
λ P Q R f g → λ p⁺ ⇜ p⁻
let (q⁺ ⇜ q⁻) := g (p⁺ ⇜ p⁻);
let (r⁺ ⇜ r⁻) := f (q⁺ ⇜ q⁻);
return r⁺ ⇜ r⁻
Expand All @@ -89,7 +89,7 @@ def compose : Π (P Q R : Poly), Q ⇒ R → P ⇒ Q → P ⇒ R :=
#normalize compose nyan nyan nyan nyan-hom2 nyan-hom2 1

def counter : (ℕ × ℕ) ⇒ (ℕ × #{ .single }) :=
λ n⁺ ⇜ n⁻
λ n⁺ ⇜ n⁻
n⁻ ← succ n⁺;
return n⁺ ⇜ λ⁻ _ → done

Expand All @@ -101,21 +101,21 @@ def Moore : Type → Type → Type → Type :=
λ S I O → (S × S) ⇒ (O × I)

def mds : Π (A B : Type), (A → B) → Moore B A B :=
λ A B f → λ b⁺ ⇜ b⁻
λ A B f → λ b⁺ ⇜ b⁻
return b⁺ ⇜ b⁻ ∘ f

def Gate : Type → Type → Type :=
λ I O → Moore O I O

def test-pair : nyan ⇒ tensor nyan nyan :=
λ n⁺ ⇜ n⁻
λ n⁺ ⇜ n⁻
let (b⁺ ⇜ b⁻) := (nyan-hom 12) (n⁺ ⇜ n⁻);
return (n⁺ , b⁺) ⇜ (! , b⁻ ∘ succ)

#normalize (test-pair 1)

def swap : Π (P Q : Poly), tensor P Q ⇒ tensor Q P :=
λ P Q → λ (p⁺ ⇜ p⁻) (q⁺ ⇜ q⁻)
λ P Q → λ (p⁺ ⇜ p⁻) (q⁺ ⇜ q⁻)
return (q⁺ ⇜ q⁻) (p⁺ ⇜ p⁻)

#normalize swap nyan nyan (1, 2)
Expand All @@ -136,7 +136,7 @@ def internal-hom : Poly → Poly → Poly :=

-- Π Σ Π Σ

-- λ a⁺ ⇜ a⁻
-- λ a⁺ ⇜ a⁻
-- p⁻ ← p⁺;
-- return (base f) a⁺ ⇜ λ r →
-- p⁻ ← p⁺;
Expand All @@ -147,9 +147,9 @@ def internal-hom : Poly → Poly → Poly :=
--def eval (P Q : Poly) : tensor P (internal-hom P Q) ⇒ Q :=
-- -- These two lines are equivalent:
-- -- either we take one (tensored) box, and deconstruct its bases (p⁺ , f⁺) and fibers (p₁⁻ , (p₂⁻ , q⁻))
-- -- λ (p⁺ , f⁺) ⇜ (p₁⁻ , (p₂⁻ , q⁻))
-- -- λ (p⁺ , f⁺) ⇜ (p₁⁻ , (p₂⁻ , q⁻))
-- -- or we take two boxes (implicitly tensored), and deconstruct each base and fiber separately
-- λ (p⁺ ⇜ p₁⁻) (f⁺ ⇜ (p₂⁻ , q⁻))
-- λ (p⁺ ⇜ p₁⁻) (f⁺ ⇜ (p₂⁻ , q⁻))
-- let (q⁺ , bwd) := f⁺ p⁺;
-- p₂⁻ ← p⁺;
-- return
Expand All @@ -176,7 +176,7 @@ def eval : Π (P Q : Poly), tensor P (internal-hom P Q) ⇒ Q :=
-- p⁻ : fib P p⁺
-- p_base⁻ : base P
-- fq⁻ : fib Q (fst (f⁺ (borrow p_base⁻)))
λ P Q → λ (p⁺ ⇜ p⁻) (f⁺ ⇜ (p_base⁻ , fq⁻))
λ P Q → λ (p⁺ ⇜ p⁻) (f⁺ ⇜ (p_base⁻ , fq⁻))
p_base⁻ ← p⁺;
-- q⁺ : base Q
-- f_fib_p⁺ : fib Q q⁺ → fib P p⁺
Expand All @@ -191,7 +191,7 @@ def compose : Poly → Poly → Poly :=
λ P Q → Σ ((p , f) : Σ (p : base P), fib P p → base Q), Σ (i : fib P p), fib Q (f i)

def tensor-to-compose : Π (P Q : Poly), tensor P Q ⇒ compose P Q :=
λ P Q → λ (p⁺ , q⁺) ⇜ pq⁻
λ P Q → λ (p⁺ , q⁺) ⇜ pq⁻
return (p⁺ , λ _ → q⁺) ⇜ pq⁻

#normalize tensor-to-compose
Expand Down
2 changes: 1 addition & 1 deletion lib/core/Syntax.ml
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ type t = Data.syn =
Fib of t * t
| (* p ⇒ q *)
Hom of t * t
| (* λ a⁺ a⁻ p *)
| (* λ a⁺ a⁻ p *)
HomLam of t
| (* x y *)
HomElim of t * t
Expand Down
4 changes: 2 additions & 2 deletions lib/parser/Grammar.mly
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ let rec fold_pat = fun t ->
%token TIMES FST SND
%token NAT ZERO SUCC NAT_ELIM
%token POLY BASE FIB RIGHT_THICK_ARROW
%token LEFT_SQUIGGLY_ARROW RIGHT_SQUIGGLY_ARROW CIRC
%token LEFT_SQUIGGLY_ARROW CIRC
%token HASH
(* Delimiters *)
%token LPR RPR LSQ RSQ LBR RBR
Expand Down Expand Up @@ -206,7 +206,7 @@ arrow:
{ CS.Pi (quantifiers, fam) }
| base = term; RIGHT_ARROW; fam = term
{ CS.Pi ([[Var `Anon], base], fam) }
| LAMBDA; binders = boxes(pattern, pattern); RIGHT_SQUIGGLY_ARROW; body = hom_body
| LAMBDA; binders = boxes(pattern, pattern); RIGHT_THICK_ARROW; body = hom_body
{ CS.HomLam(Ident.join (fst binders), Ident.join (snd binders), body) }
| p = term; RIGHT_THICK_ARROW; q = term
{ CS.Hom (p, q) }
Expand Down
2 changes: 0 additions & 2 deletions lib/parser/Lex.mll
Original file line number Diff line number Diff line change
Expand Up @@ -123,8 +123,6 @@ and real_token = parse
{ RIGHT_THICK_ARROW }
| "." | "∘"
{ CIRC }
| "~>" | "⇝"
{ RIGHT_SQUIGGLY_ARROW }
| "<~" | "⇜"
{ LEFT_SQUIGGLY_ARROW }
| "*" | "×"
Expand Down
14 changes: 7 additions & 7 deletions std-lib/Data/Polynomial.poly
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ def constantₚ : Type → Poly :=
-- └─────────┘
--
def idₚ (P : Poly) : P ⇒ P :=
λ p⁺ ⇜ p⁻
λ p⁺ ⇜ p⁻
return p⁺ ⇜ p⁻

-- | Composition of polynomials
Expand All @@ -46,7 +46,7 @@ def idₚ (P : Poly) : P ⇒ P :=
-- └───────────────┘
--
def compose (P Q R : Poly) : Q ⇒ R → P ⇒ Q → P ⇒ R :=
λ f g → λ p⁺ ⇜ p⁻
λ f g → λ p⁺ ⇜ p⁻
let (q⁺ ⇜ q⁻) := g (p⁺ ⇜ p⁻);
let (r⁺ ⇜ r⁻) := f (q⁺ ⇜ q⁻);
return r⁺ ⇜ r⁻
Expand Down Expand Up @@ -89,11 +89,11 @@ def tensor-⊗ : Poly → Poly → Poly :=
λ P Q → Σ ((p , q) : base P × base Q), fib P p × fib Q q

def swap-⊗ : Π (P Q : Poly), tensor-⊗ P Q ⇒ tensor-⊗ Q P :=
λ P Q → λ (p⁺ , q⁺) ⇜ (p⁻ , q⁻)
λ P Q → λ (p⁺ , q⁺) ⇜ (p⁻ , q⁻)
return (q⁺ , p⁺) ⇜ (q⁻ , p⁻)

def dupe-⊗ : Π (P : Poly), P ⇒ tensor-⊗ P P :=
λ P → λ p⁺ ⇜ p⁻
λ P → λ p⁺ ⇜ p⁻
return (p⁺ , p⁺) ⇜ ( p⁻ , ! )

--------------------------------------------------------------------------------
Expand All @@ -105,15 +105,15 @@ def tensor-× : Poly → Poly → Poly :=
λ P Q → Σ ((i , j) : base P × base Q), Either (fib P i) (fib Q j)

def fst-× (P Q : Poly) : tensor-× P Q ⇒ P :=
λ (p⁺ , q⁺) ⇜ pq⁻
λ (p⁺ , q⁺) ⇜ pq⁻
return p⁺ ⇜ λ⁻ p → pq⁻ ← Left (fib P p⁺) (fib Q q⁺) p; done

def snd-× (P Q : Poly) : tensor-× P Q ⇒ Q :=
λ (p⁺ , q⁺) ⇜ pq⁻
λ (p⁺ , q⁺) ⇜ pq⁻
return q⁺ ⇜ λ⁻ q → pq⁻ ← Right (fib P p⁺) (fib Q q⁺) q; done

def dupe-× (P : Poly) : P ⇒ tensor-× P P :=
λ p⁺ ⇜ p⁻
λ p⁺ ⇜ p⁻
return (p⁺ , p⁺) ⇜ p⁻ ∘ (from-either (fib P p⁺))

--------------------------------------------------------------------------------
Expand Down
4 changes: 2 additions & 2 deletions std-lib/Data/Polynomial/Lens.poly
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ def set : Π (S T A B : Type), Lens S T A B → B → S → T :=

def lens : Π (S T A B : Type), (S → A) → (S → B → T) → Lens S T A B :=
λ S T A B get set →
λ s⁺ ⇜ t⁻
λ s⁺ ⇜ t⁻
return (get s⁺) ⇜ λ⁻ (b : B) → t⁻ ← set s⁺ b; done

--------------------------------------------------------------------------------
Expand All @@ -34,4 +34,4 @@ def proj₂ : Π (A B : Type), Lens (A × B) (A × B) B B :=
λ A B → lens (A × B) (A × B) B B (λ ab → snd ab) (λ ab b → (fst ab , b))

def example₁ : Bool :=
view (Bool × Bool) (Bool × Bool) Bool Bool (proj₁ Bool Bool) (.true , .false)
view (Bool × Bool) (Bool × Bool) Bool Bool (proj₁ Bool Bool) (.true , .false)
8 changes: 4 additions & 4 deletions std-lib/Data/Polynomial/Machines.poly
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ def Moore : Type → Type → Type → Type :=

def moore : Π (S I O : Type), (S → O) → (S → I → S) → Moore S I O :=
λ S I O output transition →
λ s⁺ ⇜ s⁻
λ s⁺ ⇜ s⁻
return (output s⁺) ⇜ s⁻ ∘ (transition s⁺)

def disassemble-moore : Π (S I O : Type), Moore S I O → (S → O) × (S → I → S) :=
Expand All @@ -38,7 +38,7 @@ def DFSA : Type → Type → Type :=
-- B × B ⇒ B × A
def mds : Π (A B : Type), (A → B) → Moore B A B :=
λ A B f →
λ b⁺ ⇜ b⁻
λ b⁺ ⇜ b⁻
return b⁺ ⇜ b⁻ ∘ f

-- | An MDS given a partial function.
Expand All @@ -48,7 +48,7 @@ def mds-partial : Π (A B : Type),
(A → Either Unit B) →
Moore (Either Unit B) A (Either Unit B) :=
λ A B f →
λ b⁺ ⇜ b⁻
λ b⁺ ⇜ b⁻
return b⁺ ⇜ λ⁻ (a : A) → b⁻ ← (bind-either Unit B B (λ _ → f a) b⁺); done

-- | Delay receives a ℕ as input, sets the state to it, and outputs
Expand Down Expand Up @@ -103,4 +103,4 @@ def counter : Moore ℕ #{ .unit } ℕ :=
--
-- ℕ × ℕ ⇒ ℕ × #{ .unit }
def repeater : Moore ℕ #{ .unit } ℕ :=
moore ℕ #{ .unit } ℕ (λ x → x) (λ n _ → n)
moore ℕ #{ .unit } ℕ (λ x → x) (λ n _ → n)
20 changes: 10 additions & 10 deletions std-lib/Tutorial.poly
Original file line number Diff line number Diff line change
Expand Up @@ -136,7 +136,7 @@ def idₚ : Π (P : Poly), P ⇒ P :=
-- Here we bind the base and fiber-sink of the inner Poly:
-- inner⁺ : base P
-- inner⁻ : fib P inner⁺
λ inner⁺ ⇜ inner⁻
λ inner⁺ ⇜ inner⁻
-- And here we define the base and fiber-sink of the outer
-- Poly. In this case we map the base to the base and the
-- fiber-sink to the fiber-sink.
Expand Down Expand Up @@ -165,7 +165,7 @@ def idₚ≡idₚ' : idₚ = idₚ' := refl
-- └─────────────────┘

def two-chainₚ (A B C : Type) : (tensor-⊗ (B × A) (C × B)) ⇒ (C × A) :=
λ (p⁺ , q⁺) ⇜ pq⁻
λ (p⁺ , q⁺) ⇜ pq⁻
let- (p⁻ , q⁻) := pq⁻;
q⁻ ← p⁺;
return q⁺ ⇜ p⁻
Expand Down Expand Up @@ -212,7 +212,7 @@ def counterₚ : (ℕ × ℕ) ⇒ (ℕ × #{ .unit }) :=
-- Bind the base and fiber-sink of the inner Poly:
-- n⁺ : base (ℕ × ℕ)
-- n⁻ : fib (ℕ × ℕ) n⁺
λ n⁺ ⇜ n⁻
λ n⁺ ⇜ n⁻

-- Apply 'succ' to n⁺ and connect it back to n⁻ to create the
-- feedback loop:
Expand Down Expand Up @@ -292,7 +292,7 @@ def counterₚ : (ℕ × ℕ) ⇒ (ℕ × #{ .unit }) :=

def composeₚ : Π (P Q R : Poly), (Q ⇒ R) → (P ⇒ Q) → (P ⇒ R) :=
λ P Q R f g →
λ p⁺ ⇜ p⁻
λ p⁺ ⇜ p⁻
let (q⁺ , g⁻) := g p⁺;
let- q⁻ := p⁻ ∘ g⁻;

Expand All @@ -315,7 +315,7 @@ def composeₚ : Π (P Q R : Poly), (Q ⇒ R) → (P ⇒ Q) → (P ⇒ R) :=
-- We can simplify composeₚ as such:

def composeₚ' : Π (P Q R : Poly), (Q ⇒ R) → (P ⇒ Q) → (P ⇒ R) :=
λ P Q R f g → λ p⁺ ⇜ p⁻
λ P Q R f g → λ p⁺ ⇜ p⁻
let (q⁺ ⇜ q⁻) := g (p⁺ ⇜ p⁻);
let (r⁺ ⇜ r⁻) := f (q⁺ ⇜ q⁻);
return r⁺ ⇜ r⁻
Expand Down Expand Up @@ -347,7 +347,7 @@ def compose-equiv : composeₚ = composeₚ' := refl
-- └──────────────┘

def swapₚ (P Q : Poly) : (tensor-⊗ P Q) ⇒ (tensor-⊗ Q P) :=
λ pq⁺ ⇜ pq⁻
λ pq⁺ ⇜ pq⁻
-- Case on the tensored fiber-sinks. Note that because
-- fiber-sinks are linear obligations we can no longer reference
-- pq⁻ after this point.
Expand All @@ -373,7 +373,7 @@ def swapₚ (P Q : Poly) : (tensor-⊗ P Q) ⇒ (tensor-⊗ Q P) :=
--

def f : (ℕ × ℕ) ⇒ (ℕ × ℕ) :=
λ n⁺ ⇜ n⁻
λ n⁺ ⇜ n⁻
return n⁺ ⇜ λ⁻ (m : ℕ) → n⁻ ← add m n⁺; done

--------------------------------------------------------------------------------
Expand Down Expand Up @@ -407,7 +407,7 @@ def counterₚ-is-a-machine : Moore ℕ #{ .unit } ℕ := counterₚ

def moore (S I O : Type) : (S → O) → (S → I → S) → Moore S I O :=
λ output transition →
λ s⁺ ⇜ s⁻
λ s⁺ ⇜ s⁻
return (output s⁺) ⇜ λ⁻ (i : I) → s⁻ ← transition s⁺ i; done

-- We can also define counterₚ using the 'moore' function:
Expand Down Expand Up @@ -441,7 +441,7 @@ def three-state-dfsa : DFSA #{ .A, .B, .C} #{ .a₀, .a₁ } :=
, .C = { .a₀ = .A, .a₁ = .A }
}
in
λ s⁺ ⇜ s⁻ return (check s⁺) ⇜ (s⁻ ∘ (step s⁺))
λ s⁺ ⇜ s⁻ return (check s⁺) ⇜ (s⁻ ∘ (step s⁺))

-- | Memoryless Dynamical System
--
Expand All @@ -452,7 +452,7 @@ def three-state-dfsa : DFSA #{ .A, .B, .C} #{ .a₀, .a₁ } :=

def mds (A B : Type) : (A → B) → Moore B A B :=
λ f →
λ b⁺ ⇜ b⁻
λ b⁺ ⇜ b⁻
return b⁺ ⇜ λ⁻ (a : A) → b⁻ ← f a; done

-- With 'mds' we can build the delay line and summation examples:
Expand Down
Loading