remove begin ... end syntax

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
 

src/lang/stmts/index.ts

@@ -1,4 +1,3 @@
-export * from "./Begin"
 export * from "./Check"
 export * from "./Claim"
 export * from "./Compose"

src/lang/syntax/grammars/name.ts

@@ -3,7 +3,7 @@
 const preserved = [
   ...["define", "claim"],
   ...["type", "node", "rule"],
-  ...["begin", "check"],
+  ...["check"],
   ...["import", "require"],
   ...["end"],
 ]

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" },

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),

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

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 |

tests/builtin/inspect-args.error.i

@@ -1 +1 @@
-begin inspect end
+inspect

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 |

tests/builtin/rot-args.error.i

@@ -1,4 +1,4 @@
 type Trivial -- Type end
 node sole -- Trivial :value! end
 
-begin sole sole rot end
+sole sole rot

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 |

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

tests/builtin/swap-args.error.i

@@ -1,4 +1,4 @@
 type Trivial -- Type end
 node sole -- Trivial :value! end
 
-begin sole swap end
+sole swap

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 |

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

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 |

tests/checking/begin-type-nested.error.i

@@ -15,4 +15,6 @@ node cons
   'A List :value!
 end
 
-begin sole sole cons end
+sole sole cons
+
+TODO

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 |

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

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 |

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
+sole (:head:tail cons :tail:head)

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 |

tests/checking/rearrange-undefined-name.error.i

@@ -15,4 +15,4 @@ node cons
   'A List :value!
 end
 
-begin sole (:hi cons) end
+sole (:hi cons)

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 |

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

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 |