diff --git a/TODO.md b/TODO.md index 17e0da42..82abaf61 100644 --- a/TODO.md +++ b/TODO.md @@ -1,4 +1,7 @@ -remove `begin end` syntax +top level env has checking -- for top level `Compose` + +- begin-type.error.i +- begin-type-nested.error.i # books diff --git a/src/lang/stmts/Begin.ts b/src/lang/stmts/Begin.ts deleted file mode 100644 index 1aa67082..00000000 --- a/src/lang/stmts/Begin.ts +++ /dev/null @@ -1,32 +0,0 @@ -import { createChecking } from "../checking/createChecking" -import { composeWords } from "../compose/composeWords" -import { createEnv } from "../env/createEnv" -import { appendReport } from "../errors/appendReport" -import { Mod } from "../mod" -import { Span } from "../span" -import { Stmt } from "../stmt" -import { Word } from "../word" - -export class Begin implements Stmt { - constructor( - public words: Array, - public span: Span, - ) {} - - async execute(mod: Mod): Promise { - try { - const env = createEnv(mod) - composeWords(mod, env, this.words, { - checking: createChecking(), - }) - } catch (error) { - throw appendReport(error, { - message: `[Begin.execute] I fail to begin.`, - context: { - span: this.span, - text: mod.text, - }, - }) - } - } -} diff --git a/src/lang/stmts/index.ts b/src/lang/stmts/index.ts index f30e0e35..ef15f0c4 100644 --- a/src/lang/stmts/index.ts +++ b/src/lang/stmts/index.ts @@ -1,4 +1,3 @@ -export * from "./Begin" export * from "./Check" export * from "./Claim" export * from "./Compose" diff --git a/src/lang/syntax/grammars/name.ts b/src/lang/syntax/grammars/name.ts index f850c304..b85ccf96 100644 --- a/src/lang/syntax/grammars/name.ts +++ b/src/lang/syntax/grammars/name.ts @@ -3,7 +3,7 @@ const preserved = [ ...["define", "claim"], ...["type", "node", "rule"], - ...["begin", "check"], + ...["check"], ...["import", "require"], ...["end"], ] diff --git a/src/lang/syntax/grammars/stmt.ts b/src/lang/syntax/grammars/stmt.ts index af1fcbfe..70f0ea79 100644 --- a/src/lang/syntax/grammars/stmt.ts +++ b/src/lang/syntax/grammars/stmt.ts @@ -37,7 +37,6 @@ export const stmt = { { output: "words" }, '"end"', ], - "stmt:begin": ['"begin"', { words: "words" }, '"end"'], "stmt:check": [ '"check"', { input: "words" }, diff --git a/src/lang/syntax/matchers/stmt_matcher.ts b/src/lang/syntax/matchers/stmt_matcher.ts index ded910a2..203abd08 100644 --- a/src/lang/syntax/matchers/stmt_matcher.ts +++ b/src/lang/syntax/matchers/stmt_matcher.ts @@ -35,8 +35,6 @@ export function stmt_matcher(tree: pt.Tree): Stmt { matchers.words_matcher(output), span, ), - "stmt:begin": ({ words }, { span }) => - new Stmts.Begin(matchers.words_matcher(words), span), "stmt:check": ({ input, output, words }, { span }) => new Stmts.Check( matchers.words_matcher(input), diff --git a/tests/builtin/connect-args.error.i b/tests/builtin/connect-args.error.i index 7e9386f5..59302ee2 100644 --- a/tests/builtin/connect-args.error.i +++ b/tests/builtin/connect-args.error.i @@ -1,4 +1,4 @@ type Trivial -- Type end node sole -- Trivial :value! end -begin sole connect end +sole connect diff --git a/tests/builtin/connect-args.error.i.err b/tests/builtin/connect-args.error.i.err index a8c203fb..ee3738a7 100644 --- a/tests/builtin/connect-args.error.i.err +++ b/tests/builtin/connect-args.error.i.err @@ -9,13 +9,15 @@ 1 |type Trivial -- Type end 2 |node sole -- Trivial :value! end 3 | - 4 |begin sole connect end + 4 |sole connect 5 | -[Begin.execute] I fail to begin. +[Compose.execute] I fail to compose word. + + word: connect 1 |type Trivial -- Type end 2 |node sole -- Trivial :value! end 3 | - 4 |begin sole connect end + 4 |sole connect 5 | diff --git a/tests/builtin/inspect-args.error.i b/tests/builtin/inspect-args.error.i index 955fcaa6..7c85ca2f 100644 --- a/tests/builtin/inspect-args.error.i +++ b/tests/builtin/inspect-args.error.i @@ -1 +1 @@ -begin inspect end +inspect diff --git a/tests/builtin/inspect-args.error.i.err b/tests/builtin/inspect-args.error.i.err index 27d81fe8..95de7c33 100644 --- a/tests/builtin/inspect-args.error.i.err +++ b/tests/builtin/inspect-args.error.i.err @@ -4,10 +4,12 @@ word: inspect - 1 |begin inspect end + 1 |inspect 2 | -[Begin.execute] I fail to begin. +[Compose.execute] I fail to compose word. - 1 |begin inspect end + word: inspect + + 1 |inspect 2 | diff --git a/tests/builtin/rot-args.error.i b/tests/builtin/rot-args.error.i index a09d8fc9..36c636f1 100644 --- a/tests/builtin/rot-args.error.i +++ b/tests/builtin/rot-args.error.i @@ -1,4 +1,4 @@ type Trivial -- Type end node sole -- Trivial :value! end -begin sole sole rot end \ No newline at end of file +sole sole rot diff --git a/tests/builtin/rot-args.error.i.err b/tests/builtin/rot-args.error.i.err index 5452954e..df559b40 100644 --- a/tests/builtin/rot-args.error.i.err +++ b/tests/builtin/rot-args.error.i.err @@ -10,11 +10,15 @@ 1 |type Trivial -- Type end 2 |node sole -- Trivial :value! end 3 | - 4 |begin sole sole rot end + 4 |sole sole rot + 5 | -[Begin.execute] I fail to begin. +[Compose.execute] I fail to compose word. + + word: rot 1 |type Trivial -- Type end 2 |node sole -- Trivial :value! end 3 | - 4 |begin sole sole rot end + 4 |sole sole rot + 5 | diff --git a/tests/builtin/run-only-top-port.i b/tests/builtin/run-only-top-port.i index 845563ba..a69c4b69 100644 --- a/tests/builtin/run-only-top-port.i +++ b/tests/builtin/run-only-top-port.i @@ -1,9 +1,7 @@ require "../datatype/Nat.i" -begin - one one add - one one add - run inspect - swap inspect - run inspect -end +one one add +one one add +run inspect +swap inspect +run inspect diff --git a/tests/builtin/swap-args.error.i b/tests/builtin/swap-args.error.i index dee4d1ad..d96db685 100644 --- a/tests/builtin/swap-args.error.i +++ b/tests/builtin/swap-args.error.i @@ -1,4 +1,4 @@ type Trivial -- Type end node sole -- Trivial :value! end -begin sole swap end \ No newline at end of file +sole swap diff --git a/tests/builtin/swap-args.error.i.err b/tests/builtin/swap-args.error.i.err index 13c723f7..74fb2431 100644 --- a/tests/builtin/swap-args.error.i.err +++ b/tests/builtin/swap-args.error.i.err @@ -9,11 +9,15 @@ 1 |type Trivial -- Type end 2 |node sole -- Trivial :value! end 3 | - 4 |begin sole swap end + 4 |sole swap + 5 | -[Begin.execute] I fail to begin. +[Compose.execute] I fail to compose word. + + word: swap 1 |type Trivial -- Type end 2 |node sole -- Trivial :value! end 3 | - 4 |begin sole swap end + 4 |sole swap + 5 | diff --git a/tests/checking/begin-sign.error.i b/tests/checking/begin-sign.error.i index 985c89c0..04dd213c 100644 --- a/tests/checking/begin-sign.error.i +++ b/tests/checking/begin-sign.error.i @@ -1,4 +1,4 @@ type Trivial -- Type end node sole -- Trivial :value! end -begin sole sole connect end +sole sole connect diff --git a/tests/checking/begin-sign.error.i.err b/tests/checking/begin-sign.error.i.err index feeebb29..c2f99cc8 100644 --- a/tests/checking/begin-sign.error.i.err +++ b/tests/checking/begin-sign.error.i.err @@ -11,13 +11,15 @@ 1 |type Trivial -- Type end 2 |node sole -- Trivial :value! end 3 | - 4 |begin sole sole connect end + 4 |sole sole connect 5 | -[Begin.execute] I fail to begin. +[Compose.execute] I fail to compose word. + + word: connect 1 |type Trivial -- Type end 2 |node sole -- Trivial :value! end 3 | - 4 |begin sole sole connect end + 4 |sole sole connect 5 | diff --git a/tests/checking/begin-type-nested.error.i b/tests/checking/begin-type-nested.error.i index 040ee220..f86c94ea 100644 --- a/tests/checking/begin-type-nested.error.i +++ b/tests/checking/begin-type-nested.error.i @@ -15,4 +15,6 @@ node cons 'A List :value! end -begin sole sole cons end \ No newline at end of file +sole sole cons + +TODO diff --git a/tests/checking/begin-type-nested.error.i.err b/tests/checking/begin-type-nested.error.i.err index d755ad88..e48a617d 100644 --- a/tests/checking/begin-type-nested.error.i.err +++ b/tests/checking/begin-type-nested.error.i.err @@ -1,21 +1,25 @@ -[unifyTypes] I fail to unify types. +[lookupDefinitionOrFail] I meet undefined name. - left: Trivial - right: Trivial List + name: TODO [compose] I fail compose word. - word: cons + word: TODO - 15 | 'A List :value! 16 |end 17 | - 18 |begin sole sole cons end + 18 |sole sole cons + 19 | + 20 |TODO + 21 | -[Begin.execute] I fail to begin. +[Compose.execute] I fail to compose word. + + word: TODO - 14 | -------- - 15 | 'A List :value! 16 |end 17 | - 18 |begin sole sole cons end + 18 |sole sole cons + 19 | + 20 |TODO + 21 | diff --git a/tests/checking/begin-type.error.i b/tests/checking/begin-type.error.i index b5722920..edbda2b4 100644 --- a/tests/checking/begin-type.error.i +++ b/tests/checking/begin-type.error.i @@ -5,4 +5,6 @@ node add1 Nat :prev -- Nat :value! end type Trivial -- Type end node sole -- Trivial :value! end -begin sole add1 end +sole add1 + +TODO diff --git a/tests/checking/begin-type.error.i.err b/tests/checking/begin-type.error.i.err index 659b1a42..c32b4f8c 100644 --- a/tests/checking/begin-type.error.i.err +++ b/tests/checking/begin-type.error.i.err @@ -1,23 +1,25 @@ -[unifyTypes] I fail to unify types. +[lookupDefinitionOrFail] I meet undefined name. - left: Trivial - right: Nat + name: TODO [compose] I fail compose word. - word: add1 + word: TODO - 5 |type Trivial -- Type end 6 |node sole -- Trivial :value! end 7 | - 8 |begin sole add1 end + 8 |sole add1 9 | + 10 |TODO + 11 | -[Begin.execute] I fail to begin. +[Compose.execute] I fail to compose word. + + word: TODO - 4 | - 5 |type Trivial -- Type end 6 |node sole -- Trivial :value! end 7 | - 8 |begin sole add1 end + 8 |sole add1 9 | + 10 |TODO + 11 | diff --git a/tests/checking/rearrange-duplicated-name.error.i b/tests/checking/rearrange-duplicated-name.error.i index d7e1bdff..a35395e7 100644 --- a/tests/checking/rearrange-duplicated-name.error.i +++ b/tests/checking/rearrange-duplicated-name.error.i @@ -15,4 +15,4 @@ node cons 'A List :value! end -begin sole (:head:tail cons :tail:head) end \ No newline at end of file +sole (:head:tail cons :tail:head) diff --git a/tests/checking/rearrange-duplicated-name.error.i.err b/tests/checking/rearrange-duplicated-name.error.i.err index f958f737..cf23db9a 100644 --- a/tests/checking/rearrange-duplicated-name.error.i.err +++ b/tests/checking/rearrange-duplicated-name.error.i.err @@ -9,12 +9,15 @@ 15 | 'A List :value! 16 |end 17 | - 18 |begin sole (:head:tail cons :tail:head) end + 18 |sole (:head:tail cons :tail:head) + 19 | -[Begin.execute] I fail to begin. +[Compose.execute] I fail to compose word. + + word: (:head:tail cons :tail:head) - 14 | -------- 15 | 'A List :value! 16 |end 17 | - 18 |begin sole (:head:tail cons :tail:head) end + 18 |sole (:head:tail cons :tail:head) + 19 | diff --git a/tests/checking/rearrange-undefined-name.error.i b/tests/checking/rearrange-undefined-name.error.i index 16dd9dbd..09f64b64 100644 --- a/tests/checking/rearrange-undefined-name.error.i +++ b/tests/checking/rearrange-undefined-name.error.i @@ -15,4 +15,4 @@ node cons 'A List :value! end -begin sole (:hi cons) end \ No newline at end of file +sole (:hi cons) diff --git a/tests/checking/rearrange-undefined-name.error.i.err b/tests/checking/rearrange-undefined-name.error.i.err index e9f48a07..ca6592ee 100644 --- a/tests/checking/rearrange-undefined-name.error.i.err +++ b/tests/checking/rearrange-undefined-name.error.i.err @@ -11,12 +11,15 @@ 15 | 'A List :value! 16 |end 17 | - 18 |begin sole (:hi cons) end + 18 |sole (:hi cons) + 19 | -[Begin.execute] I fail to begin. +[Compose.execute] I fail to compose word. + + word: (:hi cons) - 14 | -------- 15 | 'A List :value! 16 |end 17 | - 18 |begin sole (:hi cons) end + 18 |sole (:hi cons) + 19 | diff --git a/tests/checking/type-term-args-not-type.error.i b/tests/checking/type-term-args-not-type.error.i index 63e736b6..62e32b00 100644 --- a/tests/checking/type-term-args-not-type.error.i +++ b/tests/checking/type-term-args-not-type.error.i @@ -3,4 +3,4 @@ node sole -- Trivial :value! end type List Type -- Type end -begin sole List end +sole List diff --git a/tests/checking/type-term-args-not-type.error.i.err b/tests/checking/type-term-args-not-type.error.i.err index 24192bbc..3bf3a279 100644 --- a/tests/checking/type-term-args-not-type.error.i.err +++ b/tests/checking/type-term-args-not-type.error.i.err @@ -9,14 +9,15 @@ 3 | 4 |type List Type -- Type end 5 | - 6 |begin sole List end + 6 |sole List 7 | -[Begin.execute] I fail to begin. +[Compose.execute] I fail to compose word. + + word: List - 2 |node sole -- Trivial :value! end 3 | 4 |type List Type -- Type end 5 | - 6 |begin sole List end + 6 |sole List 7 | diff --git a/tests/datatype/DiffList.test.i b/tests/datatype/DiffList.test.i index 03ba4f61..02a49ea2 100644 --- a/tests/datatype/DiffList.test.i +++ b/tests/datatype/DiffList.test.i @@ -9,7 +9,7 @@ define one_two_soles diff_append end -begin one_two_soles inspect run inspect end +one_two_soles inspect run inspect claim two_two_soles -- Trivial DiffList end @@ -19,7 +19,7 @@ define two_two_soles diff_append end -begin two_two_soles inspect run inspect end +two_two_soles inspect run inspect claim two_two_soles_with_local -- Trivial DiffList end @@ -29,4 +29,4 @@ define two_two_soles_with_local diff_append end -begin two_two_soles_with_local inspect run inspect end +two_two_soles_with_local inspect run inspect diff --git a/tests/datatype/List.test.i b/tests/datatype/List.test.i index 4828c60a..64205747 100644 --- a/tests/datatype/List.test.i +++ b/tests/datatype/List.test.i @@ -9,4 +9,4 @@ define six_soles append end -begin six_soles inspect run inspect end +six_soles inspect run inspect diff --git a/tests/datatype/Nat.test.i b/tests/datatype/Nat.test.i index bcb0b5fa..7c8f8672 100644 --- a/tests/datatype/Nat.test.i +++ b/tests/datatype/Nat.test.i @@ -2,25 +2,25 @@ require "Nat.i" require "Nat.i" require "Nat.i" // Multiple `require` is fine. -begin zero zero add inspect run inspect end -begin two inspect run inspect end -begin four inspect run inspect end -begin zero one add inspect run inspect end +zero zero add inspect run inspect +two inspect run inspect +four inspect run inspect +zero one add inspect run inspect claim addadd Nat Nat Nat -- Nat end define addadd add add end -begin one one one addadd run inspect end +one one one addadd run inspect -begin two nat_erase zero inspect run inspect end -begin two nat_dup inspect run inspect end +two nat_erase zero inspect run inspect +two nat_dup inspect run inspect -begin two two mul inspect run inspect end -begin three three mul inspect run inspect end +two two mul inspect run inspect +three three mul inspect run inspect -begin zero two max run inspect end -begin one two max run inspect end -begin three two max run inspect end \ No newline at end of file +zero two max run inspect +one two max run inspect +three two max run inspect diff --git a/tests/module/import.i b/tests/module/import.i index 64cf2dc6..07c798a1 100644 --- a/tests/module/import.i +++ b/tests/module/import.i @@ -1,3 +1,3 @@ import zero, one, add from "../datatype/Nat.i" -begin zero one add inspect run inspect end +zero one add inspect run inspect diff --git a/tests/module/require.i b/tests/module/require.i index 2242e114..d619e2e6 100644 --- a/tests/module/require.i +++ b/tests/module/require.i @@ -1,3 +1,3 @@ require "../datatype/Nat.i" -begin zero one add inspect run inspect end +zero one add inspect run inspect diff --git a/tests/value/input-and-output-placeholders.i b/tests/value/input-and-output-placeholders.i index 2b234ed0..f8ffa1cc 100644 --- a/tests/value/input-and-output-placeholders.i +++ b/tests/value/input-and-output-placeholders.i @@ -19,4 +19,4 @@ rule add1 add (add)-return inspect connect end -begin zero add1 zero add1 add inspect end \ No newline at end of file +zero add1 zero add1 add inspect diff --git a/tests/value/labeled.i b/tests/value/labeled.i index 0c816a51..c5a4e61f 100644 --- a/tests/value/labeled.i +++ b/tests/value/labeled.i @@ -1,4 +1,2 @@ -begin - 'A :target! inspect - 'A :addend inspect -end \ No newline at end of file +'A :target! inspect +'A :addend inspect diff --git a/tests/value/type-term.i b/tests/value/type-term.i index 595c9e51..6325c8cf 100644 --- a/tests/value/type-term.i +++ b/tests/value/type-term.i @@ -1,7 +1,6 @@ type Nat -- Type end type List Type -- Type end -begin - 'A List inspect - Nat List inspect -end \ No newline at end of file + +'A List inspect +Nat List inspect diff --git a/tests/value/type-var.i b/tests/value/type-var.i index d108eec2..8d2c61c7 100644 --- a/tests/value/type-var.i +++ b/tests/value/type-var.i @@ -1,5 +1,3 @@ -begin - 'A inspect - 'B inspect inspect - 'C inspect inspect inspect -end \ No newline at end of file +'A inspect +'B inspect inspect +'C inspect inspect inspect