diff --git a/base/Lit/Core.kind b/base/Lit/Core.kind index d7c2b1c9..540d0d6f 100644 --- a/base/Lit/Core.kind +++ b/base/Lit/Core.kind @@ -52,8 +52,9 @@ type Lit.Core.Term { ) // The monadic effect binder bind( - name: String - effe: Lit.Core.Effect + name: Maybe + otype: Lit.Core.Type + effect: Lit.Core.Effect cont: Lit.Core.Term ) // The monadic effect return @@ -71,7 +72,6 @@ type Lit.Core.Effect { call( func: String args: List - cont: Lit.Core.Term ) // Gets the name of the nth caller get_caller( @@ -232,6 +232,8 @@ Lit.Core.Type.find_ctor(name: String, type: Lit.Core.Type): Maybe @@ -352,7 +382,7 @@ Lit.Core.World.check.many( case terms types { cons cons: let type = Lit.Core.World.get_type(types.head, context@world) abort false - let head = Lit.Core.World.check.term(context, terms.head, type) + let head = Lit.Core.check.term(context, terms.head, type) let tail = Lit.Core.World.check.many(context, terms.tail, types.tail) head && tail nil nil: @@ -381,7 +411,7 @@ Lit.Core.World.check.match.cases( context.caller ext_variables ) - let case_ok = Lit.Core.World.check.term(new_context, cases.head, type) + let case_ok = Lit.Core.check.term(new_context, cases.head, type) let rest_ok = Lit.Core.World.check.match.cases(new_context, cases.tail, type, ctors.tail, name) case_ok && rest_ok nil nil: @@ -469,6 +499,8 @@ Lit.Core.World.run.statement( else log("error: cannot redefine built-in type named 'U64'") none } default log("error: type redefinition: " | type.name) none + effect: + _ // TODO } bond: use func = statement.entry.value @@ -500,7 +532,7 @@ Lit.Core.World.run.statement( some(func.name) ctx.value ) - let term_ok = Lit.Core.World.check.term( + let term_ok = Lit.Core.check.term( new_context func.main otyp @@ -520,23 +552,23 @@ Lit.Core.World.run.statement( // duplicating the typechecking function. let call_type = Lit.Core.Type.word let context = Lit.Core.Check.Context.from_world(world) - let term_ok = Lit.Core.World.check.term(context, exec_term, call_type) + let term_ok = Lit.Core.check.term(context, exec_term, call_type) if term_ok then use ctx = Lit.Core.World.run.term(exec_term, world, {}, 0) // TODO - log("- ext_exec: " - | Lit.Lang.show.term(ctx.term, world) - | " (gas:\n" - | let ops = List.reverse!(["var", "create", "match", "match_substitution", "word", "compare", "operate", "call", "bind"]) - let str = String.pad_left(TempWidth*9, '0', Nat.show(ctx.gas)) - let str_list = List.zip!!(ops, String.chunks_of(TempWidth, str)) - let fin = "" - for os in str_list with fin: - let {op, s} = os - fin | " " | op | ": " | s | "\n" - fin - | ")" - ) + // log("- ext_exec: " // DEBUG + // | Lit.Lang.show.term(ctx.term, world) + // | " (gas:\n" + // | let ops = List.reverse!(["var", "create", "match", "match_substitution", "word", "compare", "operate", "call", "bind"]) + // let str = String.pad_left(TempWidth*9, '0', Nat.show(ctx.gas)) + // let str_list = List.zip!!(ops, String.chunks_of(TempWidth, str)) + // let fin = "" + // for os in str_list with fin: + // let {op, s} = os + // fin | " " | op | ": " | s | "\n" + // fin + // | ")" + // ) some(ctx.world) else log("error: exec failed in typecheck") none @@ -582,10 +614,14 @@ Lit.Core.World.run.term( log("call!") // DEBUG let gas = gas + Lit.Core.Costs.default@call Lit.Core.World.run.term.call(world, vars, term.name, term.func, term.args, term.cont, gas) + // bind: + // log("bind!") // DEBUG + // let gas = gas + Lit.Core.Costs.default@bind + // Lit.Core.World.run.term.bind(world, vars, term.name, term.main, term.cont, gas) bind: - log("bind!") // DEBUG - let gas = gas + Lit.Core.Costs.default@bind - Lit.Core.World.run.term.bind(world, vars, term.name, term.main, term.cont, gas) + _ // TODO + return: + _ // TODO } Lit.Core.World.run.terms( @@ -613,7 +649,8 @@ Lit.Core.World.run.term.call( ): Lit.Core.run.Context case world{func} as got { none: - {Lit.Core.Term.call(name, func, args, cont), world, gas} + // {Lit.Core.Term.call(name, func, args, cont), world, gas} + _ // TODO some: case got.value as entry { bond: @@ -642,7 +679,8 @@ Lit.Core.World.run.term.call( let vars = vars{name} <- ctx.term Lit.Core.World.run.term(cont, ctx.world, vars, ctx.gas) } default - {Lit.Core.Term.call(name, func, args, cont), world, gas} + // {Lit.Core.Term.call(name, func, args, cont), world, gas} + _ // TODO } Lit.Core.World.run.term.compare( @@ -758,28 +796,35 @@ Lit.Core.World.run.term.operate( log("error: operand didn't reduce to word") {Lit.Core.Term.operate(oper, val0, val1), world, gas} -Lit.Core.World.run.term.bind( - world: Lit.Core.World - vars: Map - name: String - main: Lit.Core.Term +// Lit.Core.World.run.term.bind( +// world: Lit.Core.World +// vars: Map +// name: String +// main: Lit.Core.Term +// cont: Lit.Core.Term +// gas: Nat +// ): Lit.Core.run.Context +// case world{name} as got { +// none: +// {Lit.Core.Term.bind(name, main, cont), world, gas} +// some: +// case got.value as entry { +// bond: +// // TODO calculate gas based upon size of bound term? +// use func = entry.value +// use ctx = Lit.Core.World.run.term(main, world, vars, gas) +// let world = ctx.world{name} <- Lit.Core.Entry.bond(func@main <- ctx.term) +// Lit.Core.World.run.term(cont, world, vars, ctx.gas) +// } default +// {Lit.Core.Term.bind(name, main, cont), world, gas} +// } + +Lit.Core.run.term.bind( + context: Lit.Core.run.Context + effect: Lit.Core.Effect cont: Lit.Core.Term - gas: Nat ): Lit.Core.run.Context - case world{name} as got { - none: - {Lit.Core.Term.bind(name, main, cont), world, gas} - some: - case got.value as entry { - bond: - // TODO calculate gas based upon size of bound term? - use func = entry.value - use ctx = Lit.Core.World.run.term(main, world, vars, gas) - let world = ctx.world{name} <- Lit.Core.Entry.bond(func@main <- ctx.term) - Lit.Core.World.run.term(cont, world, vars, ctx.gas) - } default - {Lit.Core.Term.bind(name, main, cont), world, gas} - } + _ // TODO: I think we can actually remove this, I believe we're safe Lit.Core.run.term.check_sanity(term: Lit.Core.Term): Bool @@ -816,8 +861,11 @@ Lit.Core.run.term.check_sanity(term: Lit.Core.Term): Bool valid && Lit.Core.run.term.check_sanity(arg) valid && Lit.Core.run.term.check_sanity(term.cont) bind: - Lit.Core.run.term.check_sanity(term.main) - && Lit.Core.run.term.check_sanity(term.cont) + // Lit.Core.run.term.check_sanity(term.main) + // && Lit.Core.run.term.check_sanity(term.cont) + _ // TODO + return: + _ // TODO } // Serialization @@ -876,102 +924,102 @@ Lit.Bits.serialize.name.go(size: Nat, name: String): Bits // Tests // ----- -Lit.Core: _ - let world = {} +// Lit.Core: _ +// let world = {} - let code = "" +// let code = "" - let code = code | - Lit.Lang.Type - | Lit.Lang.Cmp - | Lit.Lang.Nat - | Lit.Lang.Bits - | Lit.Lang.BitsMap - | Lit.Lang.Voting - //| Lit.Lang.Test +// let code = code | +// Lit.Lang.Type +// | Lit.Lang.Cmp +// | Lit.Lang.Nat +// | Lit.Lang.Bits +// | Lit.Lang.BitsMap +// | Lit.Lang.Voting +// //| Lit.Lang.Test -// let code = code | -// ` -// GiveUnit(): Unit -// Unit/new -// -// TakeUnit(x: Unit): U64 -// 42 -// -// do { -// call a1 = GiveUnit() -// call a2 = GiveUnit() -// call b = TakeUnit(a1) -// call c = TakeUnit(a2) -// (+ b c) -// } -// ` +// // let code = code | +// // ` +// // GiveUnit(): Unit +// // Unit/new +// // +// // TakeUnit(x: Unit): U64 +// // 42 +// // +// // do { +// // call a1 = GiveUnit() +// // call a2 = GiveUnit() +// // call b = TakeUnit(a1) +// // call c = TakeUnit(a2) +// // (+ b c) +// // } +// // ` - let code = code | - ` -// type Lit.Core.Costs { -// new( -// var: Nat -// create: Nat -// match: Nat -// match_substitution: Nat -// word: Nat -// compare: Nat -// operate: Nat -// call: Nat -// bind: Nat -// ) -// } +// let code = code | +// ` +// // type Lit.Core.Costs { +// // new( +// // var: Nat +// // create: Nat +// // match: Nat +// // match_substitution: Nat +// // word: Nat +// // compare: Nat +// // operate: Nat +// // call: Nat +// // bind: Nat +// // ) +// // } - candidates(): Candidates - Candidates/cons{ - count: Nat/zero, tail: Candidates/cons{ - count: Nat/zero, tail: Candidates/cons{ - count: Nat/zero, tail: Candidates/nil }}} +// candidates(): Candidates +// Candidates/cons{ +// count: Nat/zero, tail: Candidates/cons{ +// count: Nat/zero, tail: Candidates/cons{ +// count: Nat/zero, tail: Candidates/nil }}} - key1(): Bits - Bits/o{pred: Bits/e} +// key1(): Bits +// Bits/o{pred: Bits/e} - key2(): Bits - Bits/i{pred: Bits/e} +// key2(): Bits +// Bits/i{pred: Bits/e} - do { - call cand = candidates() - call joao = key1() - call maria = key2() +// do { +// call cand = candidates() +// call joao = key1() +// call maria = key2() - call m = VotingMap.add(VotingMap/new, joao) - call new_m = VotingMap.add(m, maria) +// call m = VotingMap.add(VotingMap/new, joao) +// call new_m = VotingMap.add(m, maria) - call new_m = VotingMap.allow_vote(new_m, joao) - call new_m = VotingMap.allow_vote(new_m, maria) +// call new_m = VotingMap.allow_vote(new_m, joao) +// call new_m = VotingMap.allow_vote(new_m, maria) - call result = VotingMap.vote(new_m, joao, Nat/succ{pred: Nat/zero}, cand) - case result : VoteResult { - new: - call new_result = VotingMap.vote(result.map, maria, Nat/zero, result.candidates) - case new_result : VoteResult { - new: - call winner = Candidates.get_winner(new_result.candidates) - 0 - } - } - } - ` +// call result = VotingMap.vote(new_m, joao, Nat/succ{pred: Nat/zero}, cand) +// case result : VoteResult { +// new: +// call new_result = VotingMap.vote(result.map, maria, Nat/zero, result.candidates) +// case new_result : VoteResult { +// new: +// call winner = Candidates.get_winner(new_result.candidates) +// 0 +// } +// } +// } +// ` - let page = Parser.run!(Lit.Lang.parser.page(world), code) abort IO.print("parse error") +// let page = Parser.run!(Lit.Lang.parser.page(world), code) abort IO.print("parse error") - log("PARSED:") // DEBUG - log(Lit.Lang.show.page(page, world)) // DEBUG +// log("PARSED:") // DEBUG +// log(Lit.Lang.show.page(page, world)) // DEBUG - case Lit.Core.World.run.page(page, world) as result { - none: - IO.print("FAILURE") - some: - IO { - // log("PAGE:") // DEBUG - // let new_world = result.value // DEBUG - // log(Lit.Lang.show.page(page, new_world)) // DEBUG - IO.print("SUCCESS") - } - } +// case Lit.Core.World.run.page(page, world) as result { +// none: +// IO.print("FAILURE") +// some: +// IO { +// // log("PAGE:") // DEBUG +// // let new_world = result.value // DEBUG +// // log(Lit.Lang.show.page(page, new_world)) // DEBUG +// IO.print("SUCCESS") +// } +// } diff --git a/base/Lit/Lang.kind b/base/Lit/Lang.kind index 7ce58b17..a69e722b 100644 --- a/base/Lit/Lang.kind +++ b/base/Lit/Lang.kind @@ -47,6 +47,8 @@ Lit.Lang.show.type(type: Lit.Core.Type, world: Lit.Core.World): String | "}" )) | " }" + effect: + _ // TODO } Lit.Lang.show.bond(bond: Lit.Core.Bond, world: Lit.Core.World): String @@ -102,6 +104,8 @@ Lit.Lang.show.term(term: Lit.Core.Term, world: Lit.Core.World): String let vals = if List.is_empty!(vals) then "" else "{" | String.join(",",vals) | "}" return type.name | "/" | ctor.name | vals } + effect: + _ // TODO } } <> "CREATE" match: Maybe { @@ -121,6 +125,8 @@ Lit.Lang.show.term(term: Lit.Core.Term, world: Lit.Core.World): String term.cses) return "case " | name | " : " | type.name | " = " | expr | " { " | String.join(", ",vals) | " }" } + effect: + _ // TODO } } <> "MATCH" call: Maybe { @@ -180,8 +186,12 @@ Lit.Lang.parser.page(world: Lit.Core.World): Parser define: case head.entry as entry { type: case entry.value { - word: world - data: world{entry.value.name} <- Lit.Core.Entry.type(entry.value) + word: + world + data: + world{entry.value.name} <- Lit.Core.Entry.type(entry.value) + effect: + _ // TODO } } default world } default world @@ -460,6 +470,8 @@ Lit.Lang.parser.term.match(world: Lit.Core.World): Parser Lit.Lang.parser.text("}") return Lit.Core.Term.match(name, type_name, expr, cses) } + effect: + _ // TODO } } }