Mod -- has checking -- for top level Compose

- begin-type.error.i
- begin-type-nested.error.i

TODO.md

@@ -1,8 +1,3 @@
-top level env has checking -- for top level `Compose`
-
-- begin-type.error.i
-- begin-type-nested.error.i
-
 # books
 
 反应网编程

src/lang/mod/Mod.ts

@@ -1,4 +1,5 @@
 import { Loader } from "../../loader"
+import { Checking } from "../checking"
 import { Definition } from "../definition"
 import { Env } from "../env/Env.js"
 import { Rule } from "../rule"
@@ -7,6 +8,7 @@ import { Stmt } from "../stmt/Stmt.js"
 export type Mod = {
   loader: Loader
   env: Env
+  checking: Checking
   url: URL
   text: string
   stmts: Array<Stmt>

src/lang/mod/createMod.ts

@@ -1,5 +1,6 @@
 import { Loader } from "../../loader"
 import { defineBuiltinOperators } from "../builtins/defineBuiltinOperators"
+import { createChecking } from "../checking/createChecking"
 import { createEnv } from "../env/createEnv.js"
 import { Stmt } from "../stmt/Stmt.js"
 import { Mod } from "./Mod"
@@ -21,6 +22,7 @@ export function createMod(options: {
   } as Mod
 
   mod.env = createEnv(mod)
+  mod.checking = createChecking()
 
   defineBuiltinOperators(mod)
 

src/lang/stmts/Compose.ts

@@ -14,7 +14,9 @@ export class Compose implements Stmt {
 
   async execute(mod: Mod): Promise<void> {
     try {
-      compose(mod, mod.env, this.word, {})
+      compose(mod, mod.env, this.word, {
+        checking: mod.checking,
+      })
     } catch (error) {
       throw appendReport(error, {
         message: [

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

@@ -16,5 +16,3 @@ node cons
 end
 
 sole sole cons
-
-TODO

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

@@ -1,25 +1,24 @@
-[lookupDefinitionOrFail] I meet undefined name.
+[unifyTypes] I fail to unify types.
 
-  name: TODO
+  left: Trivial
+  right: Trivial List
 
 [compose] I fail compose word.
 
-  word: TODO
+  word: cons
 
+ 15 |  'A List :value!
  16 |end
  17 |
  18 |sole sole cons
  19 |
- 20 |TODO
- 21 |
 
 [Compose.execute] I fail to compose word.
 
-  word: TODO
+  word: cons
 
+ 15 |  'A List :value!
  16 |end
  17 |
  18 |sole sole cons
  19 |
- 20 |TODO
- 21 |

tests/checking/begin-type.error.i

@@ -6,5 +6,3 @@ type Trivial -- Type end
 node sole -- Trivial :value! end
 
 sole add1
-
-TODO

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

@@ -1,25 +1,24 @@
-[lookupDefinitionOrFail] I meet undefined name.
+[unifyTypes] I fail to unify types.
 
-  name: TODO
+  left: Trivial
+  right: Nat
 
 [compose] I fail compose word.
 
-  word: TODO
+  word: add1
 
+  5 |type Trivial -- Type end
   6 |node sole -- Trivial :value! end
   7 |
   8 |sole add1
   9 |
- 10 |TODO
- 11 |
 
 [Compose.execute] I fail to compose word.
 
-  word: TODO
+  word: add1
 
+  5 |type Trivial -- Type end
   6 |node sole -- Trivial :value! end
   7 |
   8 |sole add1
   9 |
- 10 |TODO
- 11 |