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

Incrementat type checking #68

Open
wants to merge 71 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
71 commits
Select commit Hold shift + click to select a range
f4cc377
start incremental
CrowdHailer Apr 5, 2023
464ed77
ziping trees for incremental
CrowdHailer Apr 6, 2023
dd86f6c
and the hash test
CrowdHailer Apr 6, 2023
d0ba4b4
fix unzipping
CrowdHailer Apr 6, 2023
2fcb361
incremental w
CrowdHailer Apr 6, 2023
a8282d0
extract free calc
CrowdHailer Apr 7, 2023
8d1811f
free with previous
CrowdHailer Apr 7, 2023
e687b5e
cached
CrowdHailer Apr 7, 2023
df12d1d
rest of type checking
CrowdHailer Apr 7, 2023
4265552
extract incremental files
CrowdHailer Apr 7, 2023
ac12fcb
update app
CrowdHailer Apr 7, 2023
b05cb0c
more timing for improvements
CrowdHailer Apr 7, 2023
2d0d9d0
more timing
CrowdHailer Apr 7, 2023
94381e0
start incremental store
CrowdHailer Apr 7, 2023
beb9ba8
typecheck in store
CrowdHailer Apr 7, 2023
f381fee
dont know why partial types
CrowdHailer Apr 7, 2023
f9da53b
test application
CrowdHailer Apr 7, 2023
4eef9fc
reuse language type def
CrowdHailer Apr 7, 2023
55c6632
just log failure
CrowdHailer Apr 7, 2023
8aa27dd
fix map cursor build
CrowdHailer Apr 7, 2023
081556f
store replace
CrowdHailer Apr 7, 2023
ca19adc
time store in browser
CrowdHailer Apr 7, 2023
ccbb1bb
show that free mem is empty sometimes
CrowdHailer Apr 7, 2023
572138e
give up
CrowdHailer Apr 7, 2023
6e05067
fix subs
CrowdHailer Apr 8, 2023
7916808
fix all warnings
CrowdHailer Apr 8, 2023
9b62399
remove spike of test
CrowdHailer Apr 8, 2023
9eccb98
better tests
CrowdHailer Apr 8, 2023
5659fd1
try looking up the double ref
CrowdHailer Apr 8, 2023
8c955d1
merge main
CrowdHailer Apr 9, 2023
fa193d3
0.28.1 map version
CrowdHailer Apr 10, 2023
6768508
Merge branch 'main' into incrementatl
CrowdHailer Apr 10, 2023
c42a533
clean up store map type
CrowdHailer Apr 10, 2023
2b9a569
undo debug info
CrowdHailer Apr 10, 2023
5b25232
mutable store
CrowdHailer Apr 10, 2023
031d919
Merge branch 'main' into incrementatl
CrowdHailer Apr 10, 2023
b0a22e0
Merge branch 'main' into incrementatl
CrowdHailer Apr 10, 2023
fdde149
clean up cursor
CrowdHailer Apr 18, 2023
e23fc08
update docker
CrowdHailer Apr 18, 2023
876860f
fix store load
CrowdHailer Apr 18, 2023
afeccc8
clean up tests
CrowdHailer Apr 18, 2023
dee5132
messing with monads
CrowdHailer Apr 18, 2023
7dd9b24
messing with algorithm j
CrowdHailer Apr 20, 2023
138bfde
unificationfix
CrowdHailer Apr 21, 2023
6f569d9
gleam notes
CrowdHailer Apr 22, 2023
21e6253
crash on recursion
CrowdHailer Apr 22, 2023
82b9f5e
fix recursion to be tail recursive
CrowdHailer Apr 22, 2023
35d93d1
start notes
CrowdHailer Apr 22, 2023
77bb529
extract env and scheme
CrowdHailer Apr 22, 2023
4220b64
standard error
CrowdHailer Apr 22, 2023
577f068
extract tree and incremental inference
CrowdHailer Apr 22, 2023
db75b4a
add builtins
CrowdHailer Apr 22, 2023
4b50bb5
fix type application
CrowdHailer Apr 22, 2023
b547269
some notes
CrowdHailer Apr 22, 2023
11bdbf6
tiny notes
CrowdHailer Apr 24, 2023
e5ac8e0
fix recursive check
CrowdHailer Apr 24, 2023
2ad1c4c
more tests
CrowdHailer Apr 24, 2023
d8743bc
debug this equal
CrowdHailer Apr 24, 2023
324d21f
formatting
CrowdHailer Apr 24, 2023
282909b
notes
CrowdHailer Apr 24, 2023
bc27f47
chase out bug in apply
CrowdHailer Apr 25, 2023
bae1459
typ rendering for new types
CrowdHailer Apr 27, 2023
592d66f
tidy up jm inference
CrowdHailer Apr 27, 2023
14c3c92
add builtins to j
CrowdHailer Apr 27, 2023
b734f41
run formatter
CrowdHailer Apr 27, 2023
6d56bc2
Merge branch 'main' into incrementatl
CrowdHailer Apr 27, 2023
e6ba896
Merge branch 'main' into incrementatl
CrowdHailer Apr 27, 2023
dc88467
Merge branch 'main' into incrementatl
CrowdHailer Apr 27, 2023
576be9e
Merge branch 'main' into incrementatl
CrowdHailer Apr 27, 2023
e7f969f
remove really useless tests
CrowdHailer Apr 27, 2023
6e05da2
Merge branch 'main' into incrementatl
CrowdHailer Apr 27, 2023
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
784 changes: 454 additions & 330 deletions eyg/src/atelier/app.gleam

Large diffs are not rendered by default.

117 changes: 70 additions & 47 deletions eyg/src/atelier/view/pallet.gleam
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
// command pallet
import gleam/io
import gleam/dynamic
import gleam/list
import gleam/map
Expand All @@ -8,19 +9,22 @@ import lustre/element.{div, input, span, text, textarea}
import lustre/event.{on_click}
import lustre/attribute.{class, classes}
import eyg/analysis/inference
import eyg/incremental/cursor
import eyg/analysis/jm/error
import eyg/analysis/jm/type_ as t
import atelier/app.{ClickOption, SelectNode}
import atelier/view/typ
import atelier/view/type_
import atelier/inventory

pub fn render(state: app.WorkSpace, inferred) {
pub fn render(state: app.WorkSpace) {
div(
[class("cover bg-gray-100")],
case state.mode {
app.WriteLabel(value, _) -> render_label(value)
app.WriteTerm(value, _) -> render_variable(value, inferred, state)
app.WriteTerm(value, _) -> render_variable(value, state)
app.WriteNumber(number, _) -> render_number(number)
app.WriteText(value, _) -> render_text(value)
_ -> render_navigate(inferred, state)
_ -> render_navigate(state)
},
)
}
Expand All @@ -36,39 +40,35 @@ fn render_label(value) {
]
}

fn render_variable(
value,
inferred: option.Option(inference.Infered),
state: app.WorkSpace,
) {
fn render_variable(value, state: app.WorkSpace) {
[
div(
[],
case inferred {
Some(inferred) ->
case inventory.variables_at(inferred.environments, state.selection) {
// using spaces because we are in pre tag and text based
// not in pre tag here
Ok(options) ->
list.map(
options,
fn(option) {
let #(t, term) = option
span(
[
class("rounded bg-blue-100 p-1"),
on_click(ClickOption(term)),
],
[text(t)],
)
},
)
|> list.intersperse(text(" "))
Error(_) -> [text("no env")]
}
None -> []
},
),
div([], []),
// case inferred {
// Some(inferred) ->
// // TODO use inferred but we dont have the whole env map.
// []
// // case inventory.variables_at(inferred.environments, state.selection) {
// // // using spaces because we are in pre tag and text based
// // // not in pre tag here
// // Ok(options) ->
// // list.map(
// // options,
// // fn(option) {
// // let #(t, term) = option
// // span(
// // [
// // class("rounded bg-blue-100 p-1"),
// // on_click(ClickOption(term)),
// // ],
// // [text(t)],
// // )
// // },
// // )
// // |> list.intersperse(text(" "))
// // Error(_) -> [text("no env")]
// // }
// None -> []
// },
input([
class("border w-full"),
attribute.autofocus(True),
Expand Down Expand Up @@ -114,10 +114,11 @@ fn render_text(value) {
]
}

fn render_navigate(inferred, state: app.WorkSpace) {
fn render_navigate(state: app.WorkSpace) {
let #(sub, _next, types) = state.inferred
[
case inferred {
Some(inferred) -> render_errors(inferred)
case types {
Some(types) -> render_errors(types)
None -> span([], [])
},
div(
Expand All @@ -126,13 +127,25 @@ fn render_navigate(inferred, state: app.WorkSpace) {
span(
[],
[
case inferred {
Some(inferred) ->
case types {
Some(types) ->
text(string.append(
":",
inferred
|> inference.type_of(state.selection)
|> typ.render(),
{
let assert Ok(c) =
cursor.at(state.selection, state.root, state.source)
let id = cursor.inner(c)
let assert Ok(type_) = map.get(types, id)
case type_ {
Ok(type_) -> type_.render_type(t.resolve(type_, sub))
Error(#(reason, t1, t2)) ->
type_.render_failure(
reason,
t.resolve(t1, sub),
t.resolve(t2, sub),
)
}
},
))
None -> span([], [text("type checking")])
},
Expand All @@ -151,10 +164,10 @@ fn render_navigate(inferred, state: app.WorkSpace) {
]
}

fn render_errors(inferred: inference.Infered) {
fn render_errors(types) {
let errors =
list.filter_map(
map.to_list(inferred.types),
map.to_list(types),
fn(el) {
let #(k, v) = el
case v {
Expand All @@ -173,12 +186,22 @@ fn render_errors(inferred: inference.Infered) {
errors,
fn(err) {
let #(path, reason) = err
// TODO real path
let path = []
div(
[classes([#("cursor-pointer", True)]), on_click(SelectNode(path))],
[text(typ.render_failure(reason))],
[text(render_failure(reason))],
)
},
),
)
}
}

pub fn render_failure(reason) {
let #(reason, _, _) = reason
case reason {
error.RecursiveType -> "recursive type"
_ -> "other error"
}
}
8 changes: 6 additions & 2 deletions eyg/src/atelier/view/root.gleam
Original file line number Diff line number Diff line change
@@ -1,13 +1,16 @@
import gleam/io
import gleam/option
import lustre/element.{div}
import lustre/attribute.{attribute, autofocus, class}
import lustre/event.{on_keydown}
import eyg/incremental/source
import atelier/app
import atelier/view/projection
import atelier/view/pallet

// maybe belongs in procejection .render
pub fn render(state: app.WorkSpace) {
let assert Ok(tree) = source.to_tree(state.source, state.root)
div(
[
on_keydown(app.Keypress),
Expand All @@ -19,9 +22,10 @@ pub fn render(state: app.WorkSpace) {
],
[
div([class("expand")], []),
projection.render(state.source, state.selection, state.inferred),
// pass through inferred
projection.render(tree, state.selection, option.None),
div([class("expand")], []),
pallet.render(state, state.inferred),
pallet.render(state),
],
)
}
1 change: 1 addition & 0 deletions eyg/src/atelier/view/typ.gleam
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ import eyg/analysis/typ as t
import eyg/analysis/unification
import eyg/analysis/substitutions as sub

// Keep for old kinded version
// Do we have a general need for type debug functionality
pub fn render(type_info) {
case type_info {
Expand Down
95 changes: 95 additions & 0 deletions eyg/src/atelier/view/type_.gleam
Original file line number Diff line number Diff line change
@@ -0,0 +1,95 @@
// for flat types
import gleam/int
import gleam/list
import gleam/string
import eyg/analysis/jm/type_ as t
import eyg/analysis/jm/error

pub fn render_failure(reason, t1, t2) {
case reason {
error.TypeMismatch(a, b) ->
// need to shrink errors together
string.concat(["Type Missmatch: ", render_type(a), " vs ", render_type(b)])
error.RowMismatch(label) -> string.append("Row Missmatch: ", label)
error.MissingVariable(x) -> string.append("missing variable: ", x)
error.RecursiveType -> "Recursive type"
error.InvalidTail(_) -> "invalid tail"
}
}

pub fn render_type(typ) {
case typ {
t.Var(i) -> int.to_string(i)
t.Integer -> "Integer"
t.String -> "String"
t.LinkedList(el) -> string.concat(["List(", render_type(el), ")"])
t.Fun(from, effects, to) ->
string.concat([
"(",
render_type(from),
") ->",
render_effects(effects),
" ",
render_type(to),
])
t.Union(row) ->
string.concat([
"[",
string.concat(
render_row(row)
|> list.intersperse(" | "),
),
"]",
])
t.Record(row) ->
string.concat([
"{",
string.concat(
render_row(row)
|> list.intersperse(", "),
),
"}",
])
_ -> "invalid should not be raw type"
}
}

fn render_row(r) -> List(String) {
case r {
t.Empty -> []
t.Var(i) -> [string.append("..", int.to_string(i))]
t.RowExtend(label, value, tail) -> {
let field = string.concat([label, ": ", render_type(value)])
[field, ..render_row(tail)]
}
_ -> ["not a valid row"]
}
}

fn render_effects(effects) {
case effects {
t.Var(_) | t.Empty -> ""
t.EffectExtend(label, #(lift, resume), tail) ->
string.concat([
" <",
string.join(
collect_effect(tail, [render_effect(label, lift, resume)]),
", ",
),
">",
])
_ -> "not a valid effect"
}
}

fn render_effect(label, lift, resume) {
string.concat([label, "(", render_type(lift), ", ", render_type(resume), ")"])
}

fn collect_effect(eff, acc) {
case eff {
t.EffectExtend(label, #(lift, resume), tail) ->
collect_effect(tail, [render_effect(label, lift, resume), ..acc])
_ -> acc
}
}
Loading