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

basic stack traces #261

Open
wants to merge 23 commits into
base: main
Choose a base branch
from
Open
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
8 changes: 4 additions & 4 deletions examples/contract.golden
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
#<closure> : (Syntax → Syntax)
#<closure> : (Syntax → (Syntax → (Syntax → (Macro Syntax))))
#<closure> : (Syntax → (Syntax → (Syntax → (Macro Syntax))))
#<closure> : ∀(α : *). (α → α)
#<contract> : (Syntax → Syntax)
#<arg> : (Syntax → (Syntax → (Syntax → (Macro Syntax))))
#<args> : (Syntax → (Syntax → (Syntax → (Macro Syntax))))
#<x> : ∀(α : *). (α → α)
(true) : Bool
6 changes: 3 additions & 3 deletions examples/datatypes.golden
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,9 @@
(add1 (add1 (add1 (add1 (zero))))) : Nat
(right (true)) : ∀(α : *). (Either α Bool)
(left (:: (add1 (zero)) (nil))) : ∀(α : *). (Either (List Nat) α)
#<closure> : (Nat → (Nat → Nat))
#<n> : (Nat → (Nat → Nat))
(add1 (add1 (add1 (add1 (add1 (zero)))))) : Nat
#<closure> : (Alphabet → Integer)
#<closure> : (Alphabet → Bool)
#<letter> : (Alphabet → Integer)
#<letter> : (Alphabet → Bool)
(true) : Bool
(false) : Bool
2 changes: 1 addition & 1 deletion examples/error.golden
Original file line number Diff line number Diff line change
@@ -1 +1 @@
#<closure> : ∀(α : *). (Syntax → α)
#<msg> : ∀(α : *). (Syntax → α)
8 changes: 4 additions & 4 deletions examples/eta-case.golden
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,11 @@
#[eta-case.kl:225.13-225.20]<((eta-case-aux ...) (::))> : Syntax
#[eta-case.kl:243.19-243.22]
<(eta-case-aux (list 1 2 3) (::) (pair) ((nil) (pair 0 (nil))))> : Syntax
#<closure> : ∀(α : *). (α → ((List α) → (List α)))
#<closure> : ((List Integer) → (List Integer))
#<x> : ∀(α : *). (α → ((List α) → (List α)))
#<xs> : ((List Integer) → (List Integer))
(:: 1 (:: 2 (:: 3 (nil)))) : (List Integer)
#<closure> : ∀(α : *). (α → ((List α) → (List α)))
#<closure> : ((List Integer) → (List Integer))
#<x> : ∀(α : *). (α → ((List α) → (List α)))
#<xs> : ((List Integer) → (List Integer))
(:: 1 (:: 2 (:: 3 (nil)))) : (List Integer)
(pair 1 (:: 2 (:: 3 (nil)))) : (Pair Integer (List Integer))
(pair 1 (:: 2 (:: 3 (nil)))) : (Pair Integer (List Integer))
Expand Down
2 changes: 1 addition & 1 deletion examples/fix.golden
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(in (cons "hello" (in (cons "world" (in (nil)))))) : (Fix (ListF String))
(in (cons "hello" (in (cons "world" (in (nil)))))) : (Fix (ListF String))
(in (succ (in (succ (in (zero)))))) : (Fix NatF)
#<closure> : ∀(α : *) (β : *). ((α → β) → ((Fix (ListF α)) → (Fix (ListF β))))
#<f> : ∀(α : *) (β : *). ((α → β) → ((Fix (ListF α)) → (Fix (ListF β))))
(in (cons (in (succ (in (succ (in (zero))))))
(in (cons (in (succ (in (succ (in (succ (in (zero))))))))
(in (nil)))))) : (Fix (ListF (Fix NatF)))
6 changes: 3 additions & 3 deletions examples/higher-kinded.golden
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(of-unit #<IO action>) : (OfUnit IO)
(of-unit #<closure>) : (OfUnit (→ Unit))
(of-unit #<x>) : (OfUnit (→ Unit))
(of-unit (just (unit))) : (OfUnit Maybe)
(of-unit (pair (unit) (unit))) : (OfUnit (Pair Unit))
(of-unit-unit #<closure>) : (OfUnitUnit (→))
(of-unit-unit #<closure>) : (OfUnitUnit (→))
(of-unit-unit #<x>) : (OfUnitUnit (→))
(of-unit-unit #<x>) : (OfUnitUnit (→))
(of-unit-unit (pair (unit) (unit))) : (OfUnitUnit Pair)
2 changes: 1 addition & 1 deletion examples/implicit-conversion-test.golden
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
42 : Integer
4 : Integer
"4!" : String
#<closure> : (Integer → Integer)
#<x> : (Integer → Integer)
"31!" : String
12 changes: 6 additions & 6 deletions examples/monad.golden
Original file line number Diff line number Diff line change
@@ -1,14 +1,14 @@
#<closure> : ∀(α : *). (α → α)
#<closure> : ∀(α : (* → *)) (β : *) (γ : *). ((Functor α β γ) → ((β → γ) → ((α β) → (α γ))))
(applicative (functor #<closure>) #<closure> #<closure>) : ∀(α : *) (β : *). (Applicative Macro α β)
#<closure> : ∀(α : (* → *)) (β : *) (γ : *). ((Applicative α β γ) → (β → (α β)))
#<closure> : ∀(α : (* → *)) (β : *) (γ : *).
#<x> : ∀(α : *). (α → α)
#<inst> : ∀(α : (* → *)) (β : *) (γ : *). ((Functor α β γ) → ((β → γ) → ((α β) → (α γ))))
(applicative (functor #<f>) #<x> #<fun>) : ∀(α : *) (β : *). (Applicative Macro α β)
#<inst> : ∀(α : (* → *)) (β : *) (γ : *). ((Applicative α β γ) → (β → (α β)))
#<inst> : ∀(α : (* → *)) (β : *) (γ : *).
((Applicative α β γ) → ((α (β → γ)) → ((α β) → (α γ))))
(just "applicative notation") : (Maybe String)
(nothing) : (Maybe String)
(just "applicative notation") : (Maybe String)
(nothing) : (Maybe String)
#<closure> : ∀(α : (* → *)) (β : *) (γ : *).
#<inst> : ∀(α : (* → *)) (β : *) (γ : *).
((Monad α β γ) → ((α β) → ((β → (α γ)) → (α γ))))
(just "hey") : (Maybe String)
(just "hey") : (Maybe String)
1 change: 1 addition & 0 deletions examples/non-examples/bad-lexical-env.golden
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Unknown: #[bad-lexical-env.kl:3.24-3.25]<y>
6 changes: 6 additions & 0 deletions examples/non-examples/bad-lexical-env.kl
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
#lang kernel

(define f (lambda (ff) y))
(define g (lambda (y) (f)))

(example (g 2))
5 changes: 4 additions & 1 deletion examples/non-examples/error.golden
Original file line number Diff line number Diff line change
@@ -1 +1,4 @@
Error at phase p0: error.kl:3.18-3.34: "It went wrong."
Error at phase p0:
error.kl:3.18-3.34: "It went wrong."
stack trace:
---- Halt
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
User error; no such file: "/home/doyougnu/programming/klister/examples/non-examples/stack-traces/[email protected]:1735135986"
5 changes: 5 additions & 0 deletions examples/non-examples/stack-traces/error-in-arg.golden
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
Error at phase p0:
error-in-arg.kl:5.24-5.27: bad
stack trace:
---- with function #<thing>
---- Halt
5 changes: 5 additions & 0 deletions examples/non-examples/stack-traces/error-in-arg.kl
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
#lang "prelude.kl"

(define fail (lambda (thing) (+ thing 1)))

(example (fail (error 'bad)))
7 changes: 7 additions & 0 deletions examples/non-examples/stack-traces/error-in-bind-head.golden
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
Error at phase p0:
error-in-bind-head.kl:3.29-3.30: e
stack trace:
---- in pure macro
---- in bind macro head
λx. pure x
---- Halt
3 changes: 3 additions & 0 deletions examples/non-examples/stack-traces/error-in-bind-head.kl
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
#lang "prelude.kl"

(example (>>= (pure (error 'e)) (lambda (x) (pure x))))
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Missing newline!

Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
pure #[error-in-bind-tail.kl:4.15-4.28]<hello-go-boom> >>= #<x> : ∀(α : *). (Macro α)
8 changes: 8 additions & 0 deletions examples/non-examples/stack-traces/error-in-bind-tail.kl
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
#lang "prelude.kl"

(example
(>>= (pure 'hello-go-boom)
(lambda (x)
(>>= (pure x)
-- TODO: why doesn't this work?
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a strange error indeed!

(lambda (y) (error y))))))
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
Error at phase p0:
error-in-case-constructor.kl:12.20-12.31: Im-an-error
stack trace:
---- in data case pattern: l
---- Halt
15 changes: 15 additions & 0 deletions examples/non-examples/stack-traces/error-in-case-constructor.kl
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
#lang "prelude.kl"

(import "lambda-case.kl")

(datatype (Alphabet)
(a) (b) (c) (d) (e) (f) (g) (h) (i) (j) (k) (l) (m) (n)
(o) (p) (q) (r) (s) (t) (u) (v) (x) (y) (z) (æ) (ø) (å))
Comment on lines +5 to +7
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue

Add missing letter 'w' to the Alphabet datatype.

The Alphabet datatype is missing the letter 'w' in the sequence between 'v' and 'x'.

Apply this diff to add the missing letter:

 (datatype (Alphabet)
   (a) (b) (c) (d) (e) (f) (g) (h) (i) (j) (k) (l) (m) (n)
-  (o) (p) (q) (r) (s) (t) (u) (v) (x) (y) (z) (æ) (ø) (å))
+  (o) (p) (q) (r) (s) (t) (u) (v) (w) (x) (y) (z) (æ) (ø) (å))
📝 Committable suggestion

‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.

Suggested change
(datatype (Alphabet)
(a) (b) (c) (d) (e) (f) (g) (h) (i) (j) (k) (l) (m) (n)
(o) (p) (q) (r) (s) (t) (u) (v) (x) (y) (z) (æ) (ø) (å))
(datatype (Alphabet)
(a) (b) (c) (d) (e) (f) (g) (h) (i) (j) (k) (l) (m) (n)
(o) (p) (q) (r) (s) (t) (u) (v) (w) (x) (y) (z) (æ) (ø) (å))


(define fail
(lambda (thing)
(case thing
[(l) (error 'Im-an-error)]
[(else the-other) the-other])))

(example (fail (l)))
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Unknown: #[error-in-cons-head.kl:8.6-8.9]<car>
10 changes: 10 additions & 0 deletions examples/non-examples/stack-traces/error-in-cons-head.kl
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
#lang "prelude.kl"

(import "lambda-case.kl")

-- TODO: DYG: how to test the pairs?
(define fail
(lambda (thing)
(car '(1 2 'something-else))))

(example (fail 3))
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
Error at phase p0:
error-in-constructor.kl:17.45-17.56: Im-an-error
stack trace:
---- in constructor pair
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is really nice!

in field 2
---- in let #[error-in-constructor.kl:17.22-17.24]<go>
---- Halt
20 changes: 20 additions & 0 deletions examples/non-examples/stack-traces/error-in-constructor.kl
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
#lang "prelude.kl"

(import "lambda-case.kl")

(datatype (Pair A B)
(pair A B))

(define fst
(lambda-case
[(pair x _) x]))

(define snd
(lambda-case
[(pair _ y) y]))

(define fail (lambda (thing)
(let (go (pair thing (error 'Im-an-error)))
go)))

(example (fail 23))
6 changes: 6 additions & 0 deletions examples/non-examples/stack-traces/error-in-let.golden
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
Error at phase p0:
error-in-let.kl:4.42-4.53: Im-an-error
stack trace:
---- with function #<bir>
---- in let #[error-in-let.kl:4.22-4.24]<go>
---- Halt
7 changes: 7 additions & 0 deletions examples/non-examples/stack-traces/error-in-let.kl
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
#lang "prelude.kl"

(define fail (lambda (thing)
(let (go (+ thing (error 'Im-an-error)))
go)))

(example (fail 23))
4 changes: 4 additions & 0 deletions examples/non-examples/stack-traces/error-in-list.golden
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Error at phase p0:
error-in-list.kl:7.27-7.38: Im-an-error
stack trace:
---- Halt
13 changes: 13 additions & 0 deletions examples/non-examples/stack-traces/error-in-list.kl
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
#lang "prelude.kl"

(import "defun.kl")
(import "list.kl")

(define thing 'nothing)
(define the-error (error 'Im-an-error))

(defun fail (thing) (+ 1 thing))

-- TODO: DYG: how to test
-- (example `(list-syntax (,thing (fail the-error) ()) thing))
(example `('a 'b ,the-error))
5 changes: 5 additions & 0 deletions examples/non-examples/stack-traces/error-in-pure-macro.golden
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
Error at phase p0:
error-in-pure-macro.kl:3.24-3.38: surprise-error
stack trace:
---- in pure macro
---- Halt
3 changes: 3 additions & 0 deletions examples/non-examples/stack-traces/error-in-pure-macro.kl
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
#lang "prelude.kl"

(example (pure (error 'surprise-error)))
1 change: 1 addition & 0 deletions examples/non-examples/stack-traces/in-arg-error.golden
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Type mismatch at in-arg-error.kl:5.23-5.38. Expected Syntax but got String
5 changes: 5 additions & 0 deletions examples/non-examples/stack-traces/in-arg-error.kl
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
#lang "prelude.kl"

(define fail (lambda (something) (+ something 1)))

(example (fail (error "in-arg-error!")))
6 changes: 3 additions & 3 deletions examples/prelude-test.golden
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#[prelude-test.kl:3.18-3.19]<a> : Syntax
#<closure> : ∀(α : *) (β : *). ((α → β) → (α → β))
#<closure> : ∀(α : *). (α → α)
#<closure> : ∀(α : *). (α → α)
#<g> : ∀(α : *) (β : *). ((α → β) → (α → β))
#<x> : ∀(α : *). (α → α)
#<x> : ∀(α : *). (α → α)
68 changes: 34 additions & 34 deletions examples/primitives-documentation.golden
Original file line number Diff line number Diff line change
@@ -1,33 +1,33 @@
(pair "open-syntax" #<closure>) : (Pair String (Syntax → (Syntax-Contents Syntax)))
(pair "close-syntax" #<closure>) : (Pair String (Syntax → (Syntax → ((Syntax-Contents Syntax) → Syntax))))
(pair "+" #<closure>) : (Pair String (Integer → (Integer → Integer)))
(pair "-" #<closure>) : (Pair String (Integer → (Integer → Integer)))
(pair "*" #<closure>) : (Pair String (Integer → (Integer → Integer)))
(pair "/" #<closure>) : (Pair String (Integer → (Integer → Integer)))
(pair "abs" #<closure>) : (Pair String (Integer → Integer))
(pair "negate" #<closure>) : (Pair String (Integer → Integer))
(pair ">" #<closure>) : (Pair String (Integer → (Integer → Bool)))
(pair ">=" #<closure>) : (Pair String (Integer → (Integer → Bool)))
(pair "<" #<closure>) : (Pair String (Integer → (Integer → Bool)))
(pair "<=" #<closure>) : (Pair String (Integer → (Integer → Bool)))
(pair "=" #<closure>) : (Pair String (Integer → (Integer → Bool)))
(pair "/=" #<closure>) : (Pair String (Integer → (Integer → Bool)))
(pair "integer->string" #<closure>) : (Pair String (Integer → String))
(pair "string-append" #<closure>) : (Pair String (String → (String → String)))
(pair "substring" #<closure>) : (Pair String (Integer → (Integer → (String → (Maybe String)))))
(pair "string-length" #<closure>) : (Pair String (String → Integer))
(pair "string=?" #<closure>) : (Pair String (String → (String → Bool)))
(pair "string/=?" #<closure>) : (Pair String (String → (String → Bool)))
(pair "string<?" #<closure>) : (Pair String (String → (String → Bool)))
(pair "string<=?" #<closure>) : (Pair String (String → (String → Bool)))
(pair "string>?" #<closure>) : (Pair String (String → (String → Bool)))
(pair "string>=?" #<closure>) : (Pair String (String → (String → Bool)))
(pair "string-upcase" #<closure>) : (Pair String (String → String))
(pair "string-downcase" #<closure>) : (Pair String (String → String))
(pair "string-titlecase" #<closure>) : (Pair String (String → String))
(pair "string-foldcase" #<closure>) : (Pair String (String → String))
(pair "pure-IO" #<closure>) : ∀(α : *). (Pair String (α → (IO α)))
(pair "bind-IO" #<closure>) : ∀(α : *) (β : *). (Pair String ((IO α) → ((α → (IO β)) → (IO β))))
(pair "open-syntax" #<open-syntax>) : (Pair String (Syntax → (Syntax-Contents Syntax)))
(pair "close-syntax" #<close-syntax>) : (Pair String (Syntax → (Syntax → ((Syntax-Contents Syntax) → Syntax))))
(pair "+" #<bil>) : (Pair String (Integer → (Integer → Integer)))
(pair "-" #<bil>) : (Pair String (Integer → (Integer → Integer)))
(pair "*" #<bil>) : (Pair String (Integer → (Integer → Integer)))
(pair "/" #<bil>) : (Pair String (Integer → (Integer → Integer)))
(pair "abs" #<TODO:Jeff:WHAT-TO-PUT-HERE>) : (Pair String (Integer → Integer))
(pair "negate" #<TODO:Jeff:WHAT-TO-PUT-HERE>) : (Pair String (Integer → Integer))
(pair ">" #<bipl>) : (Pair String (Integer → (Integer → Bool)))
(pair ">=" #<bipl>) : (Pair String (Integer → (Integer → Bool)))
(pair "<" #<bipl>) : (Pair String (Integer → (Integer → Bool)))
(pair "<=" #<bipl>) : (Pair String (Integer → (Integer → Bool)))
(pair "=" #<bipl>) : (Pair String (Integer → (Integer → Bool)))
(pair "/=" #<bipl>) : (Pair String (Integer → (Integer → Bool)))
(pair "integer->string" #<integer->string>) : (Pair String (Integer → String))
(pair "string-append" #<string-append-l>) : (Pair String (String → (String → String)))
(pair "substring" #<substing>) : (Pair String (Integer → (Integer → (String → (Maybe String)))))
(pair "string-length" #<string-length>) : (Pair String (String → Integer))
(pair "string=?" #<bsp-l>) : (Pair String (String → (String → Bool)))
(pair "string/=?" #<bsp-l>) : (Pair String (String → (String → Bool)))
(pair "string<?" #<bsp-l>) : (Pair String (String → (String → Bool)))
(pair "string<=?" #<bsp-l>) : (Pair String (String → (String → Bool)))
(pair "string>?" #<bsp-l>) : (Pair String (String → (String → Bool)))
(pair "string>=?" #<bsp-l>) : (Pair String (String → (String → Bool)))
(pair "string-upcase" #<string-upcase>) : (Pair String (String → String))
(pair "string-downcase" #<string-downcase>) : (Pair String (String → String))
(pair "string-titlecase" #<string-titlecase>) : (Pair String (String → String))
(pair "string-foldcase" #<string-foldcase>) : (Pair String (String → String))
(pair "pure-IO" #<pure-IO>) : ∀(α : *). (Pair String (α → (IO α)))
(pair "bind-IO" #<action>) : ∀(α : *) (β : *). (Pair String ((IO α) → ((α → (IO β)) → (IO β))))
(flip) : ScopeAction
(add) : ScopeAction
(remove) : ScopeAction
Expand All @@ -43,8 +43,8 @@
(nil) : ∀(α : *). (List α)
make-introducer : (Macro (ScopeAction → (Syntax → Syntax)))
which-problem : (Macro Problem)
(pair "id" #<closure>) : ∀(α : *). (Pair String (α → α))
(pair "const" #<closure>) : ∀(α : *) (β : *). (Pair String (α → (β → α)))
(pair "compose" #<closure>) : ∀(α : *) (β : *) (γ : *). (Pair String ((α → β) → ((γ → α) → (γ → β))))
(pair "id" #<x>) : ∀(α : *). (Pair String (α → α))
(pair "const" #<x>) : ∀(α : *) (β : *). (Pair String (α → (β → α)))
(pair "compose" #<f>) : ∀(α : *) (β : *) (γ : *). (Pair String ((α → β) → ((γ → α) → (γ → β))))
(pair "stdout" #<output port>) : (Pair String Output-Port)
(pair "write" #<closure>) : (Pair String (Output-Port → (String → (IO Unit))))
(pair "write" #<write>) : (Pair String (Output-Port → (String → (IO Unit))))
2 changes: 1 addition & 1 deletion examples/product-type.golden
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
#[product-type.kl:12.23-12.24]<a> : Syntax
#<closure> : ∀(α : *) (β : *). ((× α β) → α)
#<x> : ∀(α : *) (β : *). ((× α β) → α)
6 changes: 3 additions & 3 deletions examples/tiny-types.golden
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,10 @@
(false) : Bool
#[tiny-types.kl:5.25-5.28]<foo> : Syntax
pure #[tiny-types.kl:6.39-6.42]<foo> : (Macro Syntax)
#<closure> : (Bool → Bool)
#<closure> : (Bool → Syntax)
#<x> : (Bool → Bool)
#<x> : (Bool → Syntax)
(free-identifier=?
#[tiny-types.kl:10.40-10.41]<a>
#[tiny-types.kl:10.43-10.44]<b>)
>>=
#<closure> : (Macro (Bool → Bool))
#<eq?> : (Macro (Bool → Bool))
4 changes: 2 additions & 2 deletions examples/unknown-type.golden
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
(nothing) : ∀(α : *). (Maybe α)
(just #[unknown-type.kl:24.33-24.37]<here>) : (Maybe Syntax)
(just #<closure>) : ∀(α : *). (Maybe (α → α))
(pair (just #<closure>) (nothing)) : ∀(α : *). (Pair (Maybe (α → α)) (Maybe (α → α)))
(just #<x>) : ∀(α : *). (Maybe (α → α))
(pair (just #<x>) (nothing)) : ∀(α : *). (Pair (Maybe (α → α)) (Maybe (α → α)))
8 changes: 4 additions & 4 deletions examples/which-problem.golden
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
(true) : Bool
(true) : Bool
#<closure> : (Bool → (Bool → (Bool → (Bool → Unit))))
#<closure> : (Bool → (Bool → (Bool → (Bool → Unit))))
(both #<closure> #<closure>) : ∀(α : *) (β : *) (γ : *). (Both (α → (β → (γ → Syntax))))
(both #<closure> #<closure>) : ∀(α : *) (β : *) (γ : *). (Both (α → (β → (γ → Syntax))))
#<_> : (Bool → (Bool → (Bool → (Bool → Unit))))
#<_> : (Bool → (Bool → (Bool → (Bool → Unit))))
(both #<x> #<_>) : ∀(α : *) (β : *) (γ : *). (Both (α → (β → (γ → Syntax))))
(both #<_> #<x>) : ∀(α : *) (β : *) (γ : *). (Both (α → (β → (γ → Syntax))))
"String" : String
"String -> String" : String
"String -> String -> String" : String
Expand Down
Loading