calculus-of-constructions - npm Package Compare versions

Comparing version 0.1.2 to 0.1.4

package.json

 {
   "name": "calculus-of-constructions",
-  "version": "0.1.2",
+  "version": "0.1.4",
   "description": "Minimal, fast, robust implementation of the Calculus of Constructions on JavaScript",
@@ -5,0 +5,0 @@ "main": "src/main.js",

README.md

@@ -23,3 +23,3 @@ ## Calculus of Constructions
 
-- Can deal with files, solves devs recursively, auto-imports missing names.
+- Can deal with files, solve devs recursively, auto-imports missing names.
 
@@ -30,2 +30,42 @@ - Can pretty-print terms showing names for known combinators.
 
+## Usage
+
+Install:
+
+    $ npm install -g calculus-of-constructions
+
+### From command line:
+
+The command line can be used to print the base form, the normal form, and the type of a term. It auto-includes undefined variables by detecting them on the same directory. It can either print the full form, or a short form with known names.
+
+```bash
+$ coc two                         # (a:* (b:(.a a) (a:a (b (b a)))))
+$ coc type "(exp two two)"        # Nat
+$ coc norm "(exp two two)"        # four
+$ coc full "(exp two two)"        # ((c:(a.* (.(.a a) (.a a))) (b:(a.* (.(.a a) (.a a))) (a:* (b (.a a) (c a))))) (a:* (b:(.a a) (a:a (b (b a))))) (a:* (b:(.a a) (a:a (b (b a))))))
+$ coc full type "(exp two two)"   # (a.* (.(.a a) (.a a)))
+$ coc full norm "(exp two two)"   # (a:* (b:(.a a) (a:a (b (b (b (b a)))))))
+```
+
+Check out the [examples](https://github.com/MaiaVictor/calculus-of-constructions/tree/master/examples) for that usage.
+
+### From JavaScript:
+
+```javascript
+const coc = require("calculus-of-constructions");
+
+const main = `T:* x:T x`; // id function
+
+const term = CoC.read(main); // parses source, could be an object {name: source, ...}
+const type = CoC.type(term); // infers type
+const norm = CoC.norm(term); // normalizes
+
+console.log(CoC.show(term)); // prints original term
+console.log(CoC.show(type)); // prints inferred type
+console.log(CoC.show(norm)); // prints normal form
+
+// CoC.show can receive, optionally, a function that
+// receives a combinator and returns a name of it. 
+```
+
 ## Syntax
@@ -55,30 +95,2 @@
 
-## Usage
-
-Install:
-
-    npm install -g calculus-of-constructions
-
-Use from command line:
-
-    coc eval my_file.coc
-
-Use from JavaScript:
-
-```javascript
-const coc = require("calculus-of-constructions");
-
-const main = `T:* x:T x`; // id function
-
-const term = CoC.read(main); // parses source
-const type = CoC.type(term); // infers type
-const norm = CoC.norm(term); // normalizes
-
-console.log(CoC.show(term)); // prints original term
-console.log(CoC.show(type)); // prints inferred type
-console.log(CoC.show(norm)); // prints normal form
-```
-
-Check out the [example](https://github.com/MaiaVictor/calculus-of-constructions/tree/master/example) directory for cool examples of the command-line interface usage.
-
 ## Example:
@@ -143,40 +155,1 @@
 ```
-
-## Parsing files, solving dependencies and pretty-printing names
-
-This library allows you to parse files. It solves dependencies recursively. Imports are implicit (any unbound variable is imported). Example:
-
-```javascript
-// A list of files where terms can reference on each-other.
-var files = {
-  "NAT": "(Nat. * Succ. (.Nat Nat) Zero. Nat Nat)",
-  "C0": "(N:* S:(.N N) Z:N Z)",
-  "C1": "(N:* S:(.N N) Z:N (S Z))",
-  "PAIR": "(T:* P:(.NAT .NAT T) (P C0 C1))"
-}
-
-// Parses those files, returns the resulting terms.
-var terms = CoC.read(files);
-```
-
-It also has a name-aware pretty-printer. That is, sometimes the normal form of a term is huge, and `CoC.show(term)` will be hard to read. You can make this output much better by letting the library name combinators inside the normal form. Study this example:
-
-```javascript
-// Name of combinators we know.
-var nameOf = {}
-for (var name in files)
-  nameOf[CoC.show(terms[name])] = name;
-
-// Stringifies the PAIR term, naming combinators inside it.
-var PAIR = CoC.show(
-  terms.PAIR,
-
-  comb => {
-    if (nameOf[CoC.show(comb)] !== "PAIR")
-      return nameOf[CoC.show(comb)]
-  });
-
-// Notice that here we didn't return the full normal form
-// of PAIR. Instead, NAT, C0 and C1 were pretty-printed.
-console.log(PAIR === "(a:* (a:(.NAT (.NAT a)) (a C0 C1)))");
-```

src/cmds.js

@@ -11,3 +11,3 @@ #!/usr/bin/env node
 
-var files = {__main: args.pop()};
+var files = {"$main$": args.pop()};
 fs.readdirSync(process.cwd()).forEach(function(name) {
@@ -24,21 +24,15 @@ if (name.slice(-4) === ".coc")
 
-function print(map, term, pretty) {
-  return CoC.show(map(terms[term]||CoC.read(term)), function(comb) {
-    return pretty && nameOf[comb] !== term && nameOf[comb];
-  });
-}
-
 if (args[0] === "help") {
   console.log("Usage:");
-  console.log("$ coc term             # shows the base form of term.coc");
-  console.log("$ coc type term        # shows the type of term.coc");
-  console.log("$ coc norm term        # shows the normal form of term.coc");
-  console.log("$ coc pretty term      # pretty-prints the base form of term.coc");
-  console.log("$ coc pretty type term # pretty-prints the type of term.coc");
-  console.log("$ coc pretty norm term # pretty-prints the normal form of term.coc");
+  console.log("$ coc term           # shows the base form of term.coc");
+  console.log("$ coc type term      # shows the type of term.coc");
+  console.log("$ coc norm term      # shows the normal form of term.coc");
+  console.log("$ coc full term      # fully shows the base form of term.coc");
+  console.log("$ coc full type term # fully shows the type of term.coc");
+  console.log("$ coc full norm term # fully shows the normal form of term.coc");
 }
 
-var pretty = false;
-if (args[0] === "pretty") {
-  pretty = true;
+var full = false;
+if (args[0] === "full") {
+  full = true;
   args.shift();
@@ -57,4 +51,4 @@ }
 
-console.log(CoC.show(map(terms.__main), function(comb) {
-  return pretty && nameOf[CoC.show(comb)] !== "__main" && nameOf[CoC.show(comb)];
+console.log(CoC.show(map(terms["$main$"]), function(comb) {
+  return !full && nameOf[CoC.show(comb)] !== "$main$" && nameOf[CoC.show(comb)];
 }));

No alert changes

Worsened metrics

Total package byte prevSize

22880

decreased by-4.3%

Lines of code

470

decreased by-1.05%

Number of lines in readme file

152

decreased by-15.08%

No dependency changes