-
Notifications
You must be signed in to change notification settings - Fork 3
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
4 changed files
with
129 additions
and
3 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,3 @@ | ||
export * from "./presentNodeAsNet" | ||
// export * from "./presentRuleInitialAsNet" | ||
// export * from "./presentRuleFinalAsNet" | ||
// export * from "./presentWordAsEnv" | ||
export * from "./presentRuleAsNets" | ||
export * from "./presentWordAsEnv" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,71 @@ | ||
import { expect, test } from "vitest" | ||
import { Fetcher } from "../../fetcher" | ||
import { Loader } from "../../loader" | ||
import { formatNet } from "../net/formatNet" | ||
import { presentWordAsEnv } from "./presentWordAsEnv" | ||
|
||
test("presentWordAsEnv", async () => { | ||
const text = ` | ||
type Nat -- Type end | ||
node zero | ||
------ | ||
Nat :value! | ||
end | ||
node add1 | ||
Nat :prev | ||
---------- | ||
Nat :value! | ||
end | ||
node add | ||
Nat :target! | ||
Nat :addend | ||
-------- | ||
Nat :return | ||
end | ||
rule zero add | ||
(add)-addend | ||
return-(add) | ||
end | ||
rule add1 add | ||
(add)-addend | ||
(add1)-prev add | ||
add1 return-(add) | ||
end | ||
claim one -- Nat end | ||
define one zero add1 end | ||
claim two -- Nat end | ||
define two one one add end | ||
claim addadd Nat Nat Nat -- Nat end | ||
define addadd add add end | ||
` | ||
|
||
const fetcher = new Fetcher() | ||
const loader = new Loader({ fetcher }) | ||
const url = new URL("test://presentNodeAsNet") | ||
const mod = await loader.load(url, { text }) | ||
|
||
expect(formatNet(presentWordAsEnv(mod, "two").net)).toMatchInlineSnapshot(` | ||
"(zero₄)-value prev-(add1₅) | ||
(add1₅)-value addend-(add₆) | ||
(zero₅)-value prev-(add1₆) | ||
(add1₆)-value!target-(add₆)" | ||
`) | ||
|
||
expect(formatNet(presentWordAsEnv(mod, "addadd").net)).toMatchInlineSnapshot(` | ||
"(@type_cap₃)-covering addend-(add₈) | ||
(@type_cap₄)-covering addend-(add₇) | ||
(@type_cap₅)-covering!target-(add₇) | ||
(add₇)-return target-(add₈)" | ||
`) | ||
}) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,52 @@ | ||
import { capType } from "../cap" | ||
import { collectWords } from "../compose/collectWords" | ||
import { compose } from "../compose/compose" | ||
import { Env } from "../env" | ||
import { createEnv } from "../env/createEnv" | ||
import { Mod, lookupDefinitionOrFail } from "../mod" | ||
import { formatWord } from "../word" | ||
|
||
export function presentWordAsEnv(mod: Mod, name: string): Env { | ||
const definition = lookupDefinitionOrFail(mod, name) | ||
|
||
if (definition["@kind"] !== "WordDefinition") { | ||
throw new Error( | ||
[ | ||
`[presentWordAsEnv] I expect to find a WordDefinition from the name.`, | ||
``, | ||
` name: ${name}`, | ||
` definition kind: ${definition["@kind"]}`, | ||
].join("\n"), | ||
) | ||
} | ||
|
||
const { input, output, words } = definition | ||
|
||
if (words === undefined) { | ||
throw new Error( | ||
[ | ||
`[presentWordAsEnv] I expect the word to be not only claimed but also defined.`, | ||
``, | ||
` name: ${name}`, | ||
` input: ${input.map(formatWord).join(" ")}`, | ||
` output: ${output.map(formatWord).join(" ")}`, | ||
].join("\n"), | ||
) | ||
} | ||
|
||
const env = createEnv(mod) | ||
|
||
const inputValues = collectWords(mod, env, input, {}) | ||
|
||
const capOutputPorts = inputValues | ||
.reverse() | ||
.map((t) => capType(mod, env.net, t)) | ||
|
||
env.stack.push(...capOutputPorts) | ||
|
||
for (const word of words) { | ||
compose(mod, env, word, {}) | ||
} | ||
|
||
return env | ||
} |