calculus-of-constructions - npm Package Compare versions

Comparing version 0.1.1 to 0.1.2

package.json

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

README.md

 ## Calculus of Constructions
 
-A lightweight implementation of the Calculus of Constructions in JavaScript. CoC is both a minimalistic programming language, similar to the Lambda Calculus, but with a very powerful type system, and a constructive foundation for mathematics.
+A lightweight implementation of the [Calculus of Constructions](https://en.wikipedia.org/wiki/Calculus_of_constructions) in JavaScript. CoC is both a minimalistic programming language (similar to the [Lambda Calculus](https://en.wikipedia.org/wiki/Lambda_calculus), but with a very powerful type system) and a constructive foundation for mathematics, serving as the basis of proof assistants such as [Coq](https://en.wikipedia.org/wiki/Coq).
 
 ## Features
 
-- Core calculus with Lambda, Forall, Application, Variables and, as you love paradoxes, Fix and Type in Type.
+- Core lang with `Lambda`, `Forall`, `Application`, `Variables` and, as you love paradoxes, `Fix` and `Type in Type`.
 
-- Let bindings as syntax sugars.
+- `Let` bindings as syntax sugars.
 
@@ -15,3 +15,3 @@ - Extremelly minimalistic, unbloated, pure ASCII syntax.
 
-- A robust parser, which allows arbitrary grammar nestings, including of `let`s.
+- A robust parser, which allows arbitrary grammar nestings, including of `Let`s.
 
@@ -24,26 +24,32 @@ - A smart stringifier which names vars so that [combinators](https://en.wikipedia.org/wiki/Combinatory_logic) are stringified uniquely, regardless of the context.
 
-- All that in less than 400 lines of code, ang a gziped minified size of laughable `2.3kb`.
+- Can deal with files, solves devs recursively, auto-imports missing names.
 
+- Can pretty-print terms showing names for known combinators.
+
+- All that in less than 400 lines of code, ang a gziped minified size of just `2.3kb`.
+
 ## Syntax
 
-- Lambda: `name:Type Body`
+- **Lambda:** `name:Type Body`
 
     A function that receives `name` of type `Type` and returns `Body`.
 
-- Forall: `name.ArgType BodyType`
+- **Forall:** `name.ArgType BodyType`
 
     The type of functions that receive `name` of type `ArgType` and return `BodyType`.
 
-- Fix: `self@ Term`
+- **Fix:** `self@ Term`
 
     The term `Term` with all instances of `self` replaced by itself.
 
-- Apply: `(f x y z)`
+- **Apply:** `(f x y z)`
 
     The application of the function `f` to `x`, `y` and `z`.
 
-- Let: `name=Term Body`
+- **Let:** `name=Term Body`
 
     Let `name` be the term `Term` inside the term `Body`.
 
+The name can be omitted from `Lambda` and `Forall`, so, for example, the equivalent of `Int -> Int` is just `.Int Int`. All other special characters are ignored, so you could write `λ a: Type -> Body` if that is more pleasing to you.
+
 ## Usage
@@ -75,2 +81,4 @@
 
+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:
@@ -104,3 +112,3 @@
 
-To aid you grasp the minimalist syntax, it is equivalent to this Idris program:
+To aid you grasp the minimalist syntax, it is equivalent to this [Idris](https://www.idris-lang.org/) program:
 
@@ -136,1 +144,40 @@ ```haskell
 ```
+
+## 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

@@ -8,33 +8,51 @@ #!/usr/bin/env node
 var CoC = require("./main.js");
+var path = require("path");
+var args = process.argv.slice(2);
 
-var path = process.cwd();
-var call = process.argv[2];
-var file = process.argv[3] || "main";
+var files = {__main: args.pop()};
+fs.readdirSync(process.cwd()).forEach(function(name) {
+  if (name.slice(-4) === ".coc")
+    files[name.slice(0, -4)] = fs.readFileSync(path.join(process.cwd(), name), "utf8");
+});
 
-var main = fs.existsSync(file) ? fs.readFileSync(file, "utf8") : file;
-var term = CoC.read(main);
+var terms = CoC.read(files);
 
-switch (process.argv[2]) {
-  case "type":
-  console.log(CoC.show(CoC.type(term)));
-  break;
+var nameOf = {};
+for (var name in terms)
+  nameOf[CoC.show(terms[name])] = name;
 
-  case "norm":
-  console.log(CoC.show(CoC.norm(term)));
-  break;
+function print(map, term, pretty) {
+  return CoC.show(map(terms[term]||CoC.read(term)), function(comb) {
+    return pretty && nameOf[comb] !== term && nameOf[comb];
+  });
+}
 
-  case "eval":
-  console.log("Type:");
-  console.log(CoC.show(CoC.type(term)));
-  console.log("")
-  console.log("Norm:");
-  console.log(CoC.show(CoC.norm(term)));
-  break;
+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");
+}
 
-  case "help":
-  console.log("Usage:")
-  console.log("$ coc eval main # evaluates term on file named `main`")
-  console.log("$ coc type main # infers type of term on file named `main`")
-  console.log("$ coc type main # normalizes term on file named `main`")
-  break;
+var pretty = false;
+if (args[0] === "pretty") {
+  pretty = true;
+  args.shift();
 }
+
+var map = function(x) { return x; };
+if (args[0] === "type") {
+  map = CoC.type;
+  args.shift();
+}
+if (args[0] === "norm") {
+  map = CoC.norm;
+  args.shift;
+};
+
+console.log(CoC.show(map(terms.__main), function(comb) {
+  return pretty && nameOf[CoC.show(comb)] !== "__main" && nameOf[CoC.show(comb)];
+}));

src/lang.js

@@ -7,122 +7,146 @@ // Syntax (parser and stringifier).
 
-  // String * Int -> {term: Term, deps: [String], index: Int}
-  // Parses a source string to a Sol term. May receive a list of types for free
-  // vars. Returns the term and a list of free vars.
-  function parse(source, index) {
-    var index = index || 0;
-    var deps = [];
-    var used = {};
+  // (s : Either String (Map String String)) -> case s of { Left s => String, Right s => Map String String }
+  //   Receives a source or an object mapping names to sources,
+  //   returns either a term of a map of names and terms.
+  function read(sources) {
+    if (typeof sources !== "object")
+      sources = {"$": sources};
 
-    var term = (function parse() {
-      while (/[^a-zA-Z\(\)_0-9\.@:\-\*\%\#\{\}\[\]]/.test(source[index]||""))
-        ++index;
+    var terms = {};
 
-      if (source[index] === "(") {
-        ++index;
-        var app = parse();
-        var arg = [];
-        while (source[index] !== ")") {
-          arg.push(parse());
-          while (/\s/.test(source[index])) ++index;
-        };
-        ++index;
-        return function(depth, binders, aliases) {
-          var appTerm = app(depth, binders, aliases);
-          for (var i=0, l=arg.length; i<l; ++i)
-            appTerm = Core.App(appTerm, arg[i](depth, binders, aliases));
-          return appTerm; 
-        };
+    function parseTerm(name) {
+      var source = sources[name];
+      var index = 0;
 
-      } else if (source[index] === "*") {
-        ++index;
-        return function(depth, binders, aliases) {
-          return Core.Set;
-        };
+      if (!source)
+        return Core.Set;
 
-      } else {
-        var binder = "";
-        while (/[a-zA-Z0-9_]/.test(source[index]||""))
-          binder += source[index++];
-        if (source[index] === ":") {
+      if (terms[name])
+        return terms[name];
+
+      // Recursive parser
+      var term = (function parse() {
+        // Skip special characters
+        while (/[^a-zA-Z\(\)_0-9\.@:\-\*\%\#\{\}\[\]]/.test(source[index]||""))
           ++index;
-          var type = parse();
-          var body = parse();
-          return function(depth, binders, aliases) {
-            return Core.Lam(
-              type(depth, binders, aliases),
-              body(depth+1, binders.concat(binder), aliases));
-          };
-        } else if (source[index] === ".") {
+
+        // Application
+        if (source[index] === "(") {
           ++index;
-          var type = parse();
-          var body = parse();
-          return function(depth, binders, aliases) {
-            return Core.For(
-              type(depth, binders, aliases),
-              body(depth+1, binders.concat(binder), aliases));
+          var app = parse();
+          var arg = [];
+          while (source[index] !== ")") {
+            arg.push(parse());
+            while (/\s/.test(source[index])) ++index;
           };
-        } else if (source[index] === "@") {
           ++index;
-          var body = parse();
           return function(depth, binders, aliases) {
-            return Core.Fix(body(depth+1, binders.concat(binder), aliases));
+            var appTerm = app(depth, binders, aliases);
+            for (var i=0, l=arg.length; i<l; ++i)
+              appTerm = Core.App(appTerm, arg[i](depth, binders, aliases));
+            return appTerm; 
           };
-        } else if (source[index] === "=") {
+
+        // Set
+        } else if (source[index] === "*") {
           ++index;
-          var value = parse();
-          var context = parse();
           return function(depth, binders, aliases) {
-            var newAliases = {};
-            for (var key in aliases)
-              newAliases[key] = aliases[key];
-            newAliases[binder] = value;
-            return context(depth, binders, newAliases);
+            return Core.Set;
           };
 
-        } else{
-          return function(depth, binders, aliases) {
-            var binderIndex = binders.lastIndexOf(binder);
-            if (binderIndex === -1) {
-              if (aliases[binder]) {
-                return aliases[binder](depth, binders, aliases);
-              };
-              if (!(used[binder] < 0)) {
-                deps.push(binder);
-                binderIndex = -deps.length;
-                used[binder] = binderIndex;
-              } else {
-                binderIndex = used[binder];
+        // Either a binder or a binding expression
+        } else {
+          var binder = "";
+
+          while (/[a-zA-Z0-9_]/.test(source[index]||""))
+            binder += source[index++];
+
+          // Lambda
+          if (source[index] === ":") {
+            ++index;
+            var type = parse();
+            var body = parse();
+            return function(depth, binders, aliases) {
+              return Core.Lam(
+                type(depth, binders, aliases),
+                body(depth+1, binders.concat(binder), aliases));
+            };
+
+          // Forall
+          } else if (source[index] === ".") {
+            ++index;
+            var type = parse();
+            var body = parse();
+            return function(depth, binders, aliases) {
+              return Core.For(
+                type(depth, binders, aliases),
+                body(depth+1, binders.concat(binder), aliases));
+            };
+
+          // Fix
+          } else if (source[index] === "@") {
+            ++index;
+            var body = parse();
+            return function(depth, binders, aliases) {
+              return Core.Fix(body(depth+1, binders.concat(binder), aliases));
+            };
+
+          // Let
+          } else if (source[index] === "=") {
+            ++index;
+            var value = parse();
+            var context = parse();
+            return function(depth, binders, aliases) {
+              var newAliases = {};
+              for (var key in aliases)
+                newAliases[key] = aliases[key];
+              newAliases[binder] = value;
+              return context(depth, binders, newAliases);
+            };
+
+          // Binder
+          } else {
+            return function(depth, binders, aliases) {
+              var binderIndex = binders.lastIndexOf(binder);
+              if (binderIndex === -1) {
+                if (aliases[binder]) {
+                  return aliases[binder](depth, binders, aliases);
+                } else {
+                  return parseTerm(binder);
+                }
               }
-            }
-            return Core.Var(depth - binderIndex - 1);
+              return Core.Var(depth - binderIndex - 1);
+            };
           };
-        };
-      }
-    })()(0, [], []);
-    return {term: term, deps: deps, index: index};
-  };
+        }
+      })()(0, [], []);
 
-  // String -> Term
-  function read(source) {
-    return parse(source).term;
-  };
+      return terms[name] = term;
+    };
 
-  // Number -> String
-  // Turns a number into a var name (a, b, c... aa, ab...).
-  function toName(nat) {
-    var alphabet = "abcdefghijklmnopqrstuvwxyz";
-    var name = "";
-    do {
-      name += alphabet[nat % alphabet.length];
-      nat = Math.floor(nat / alphabet.length);
-    } while (nat > 0);
-    return name;
+    for (var name in sources)
+      parseTerm(name);
+
+    return terms["$"] || terms;
   };
 
-  // Term, (Term -> Maybe String) -> String
-  // Stringifies a term. `combinatorName` is called on each combinator and may
-  // return a name for it.
-  function format(term, combinatorName) {
+  // Term, Maybe (Either (Map String String) (Term -> Maybe String)) -> String
+  //   Stringifies a term. `combinatorName` is called on each
+  //   combinator and may return a name for it.
+  function show(term, combinatorName) {
     if (!term) return "E";
 
+    if (!combinatorName)
+      combinatorName = function(){ return null };
+
+    function toName(nat) {
+      var alphabet = "abcdefghijklmnopqrstuvwxyz";
+      var name = "";
+      do {
+        name += alphabet[nat % alphabet.length];
+        nat = Math.floor(nat / alphabet.length);
+      } while (nat > 0);
+      return name;
+    };
+
     function extend(a,b) {
@@ -191,4 +215,6 @@ var c = {};
     return (function go(term, args) {
-      if (term.isCombinator && combinatorName && combinatorName(term))
-        return combinatorName(term);
+      if (term.isCombinator && combinatorName) {
+        var name = combinatorName(term);
+        if (name) return name;
+      };
       switch (term.ctor) {
@@ -221,19 +247,6 @@ case Core.VAR: return args[args.length-term.idx-1] || (term.idx>0?"v"+term.idx:"f"+(-term.idx));
 
-  // Term -> String
-  function show(term) {
-    return format(term, function(term) { return null; });
-  };
-
-  // Term -> IO
-  function print(term) {
-    console.log(show(term));
-  };
-
   return {
-    parse: parse,
-    format: format,
     read: read,
-    show: show,
-    print: print
+    show: show
   }
 })();

test/test.js

@@ -42,1 +42,27 @@ const CoC = require("./../src/main.js");
 
+describe("Files", () => {
+  it("Should be able to solve dependencies and stringify combinator names", () => {
+    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))"
+    }
+
+    var terms = CoC.read(files);
+
+    var nameOf = {}
+    for (var name in files)
+      nameOf[CoC.show(terms[name])] = name;
+
+    var shown = CoC.show(
+      terms.PAIR,
+
+      comb => {
+        if (nameOf[CoC.show(comb)] !== "PAIR")
+          return nameOf[CoC.show(comb)]
+      });
+
+    assert(shown === "(a:* (a:(.NAT (.NAT a)) (a C0 C1)))");
+  });
+});

No alert changes

Improved metrics

Total package byte prevSize

23909

increased by34.58%

Number of package files

15

increased by87.5%

Lines of code

475

increased by15.85%

Number of lines in readme file

179

increased by35.61%

No dependency changes