commit

Author: Hakerh400

frontend/projects/main/math.js

@@ -7,31 +7,54 @@ const O = require('omikron');
 const Expr = require('./expr');
 
 const pidents = {
-  'a.': '\\varphi',
-  'b.': '\\psi',
-  'c.': '\\chi',
-  'd.': '\\theta',
+  'phi': '\\varphi',
+  'psi': '\\psi',
+  'chi': '\\chi',
+  'theta': '\\theta',
 };
 
-const precs = {
-  impl: 10,
-  neg: 10,
+const idents = {
+  'a.': 'a',
+  'b.': 'b',
+  'c.': 'c',
+  'd.': 'd',
 };
 
+const ops = [
+  'impl',
+  'pnot',
+  'pelem',
+  'forall',
+];
+
+const precs = O.obj();
+
+ops.forEach((op, index) => {
+  precs[op] = index << 1;
+});
+
+const precMin = -1;
+const precMax = O.N;
+
 const expr2math = expr => {
-  const expr2math = function*(expr, prec=-1){
+  const expr2math = function*(expr, prec=precMin){
     if(expr.isSym){
       const {name} = expr;
 
       if(O.has(pidents, name))
         return pidents[name];
 
+      if(O.has(idents, name))
+        return idents[name];
+
       assert.fail();
       return;
     }
 
-    const {baseSym} = expr;
-    const prec1 = precs[baseSym];
+    const op = expr.baseSym
+    assert(O.has(precs, op), op);
+
+    const prec1 = precs[op];
     const args = Expr.expr2args(expr);
     const argsNum = args.length;
 
@@ -40,23 +63,29 @@ const expr2math = expr => {
         return str;
     };
 
-    if(baseSym === 'impl'){
-      assert(argsNum === 2);
+    if(op === 'impl')
       return disambiguate(`${
         yield [expr2math, args[0], prec1 + 1]} \\to ${
         yield [expr2math, args[1], prec1]}`);
-    }
 
-    if(baseSym === 'pnot'){
-      assert(argsNum === 1);
+    if(op === 'pnot')
       return disambiguate(`\\lnot ${
         yield [expr2math, args[0], prec1]}`);
-    }
 
-    assert.fail();
+    if(op === 'forall')
+      return disambiguate(`\\forall ${
+        yield [expr2math, args[0], precMax]} ${
+        yield [expr2math, args[1], prec1]}`);
+
+    if(op === 'pelem')
+      return disambiguate(`${
+        yield [expr2math, args[0], precMax]} \\in ${
+        yield [expr2math, args[1], precMax]}`);
+
+    assert.fail(op);
   };
 
-  return O.rec(expr2math, expr);
+  return log(O.rec(expr2math, expr));
 };
 
 const str2math = str => {

local-test/main.js

@@ -9,7 +9,7 @@ const drift = require('..');
 const {Database} = drift;
 
 const main = () => {
-  drift.verifyAll();
+  drift.verifyAll(1);
 };
 
 main();

package.json

@@ -15,7 +15,7 @@
     "test": "node test"
   },
   "dependencies": {
-    "omikron": "~1.2.54",
+    "omikron": "~1.2.55",
     "@hakerh400/list": "~1.0.6",
     "@hakerh400/fs-rec": "~1.0.4"
   },

src/index.js

@@ -43,8 +43,18 @@ const verifyAll = (force=0) => {
     saveVerified();
   }
 
-  for(const thName of O.keys(ths))
-    verify(thName);
+  for(const thName of O.keys(ths)){
+    log(thName);
+    log.inc();
+
+    if(prog.hasIdent(thName)){
+      verify(thName);
+    }else{
+      log('Skip');
+    }
+
+    log.dec();
+  }
 };
 
 const verify = (thName, force=0) => {
@@ -57,8 +67,6 @@ const verify = (thName, force=0) => {
     update(0);
   }
 
-  log(thName);
-
   const db = new database.OperativeDatabase();
 
   const reduceIdent = function*(ident){

system/core/consts/idents.txt

@@ -0,0 +1,6 @@
+a. = zero
+b. = nextIdent a.
+c. = nextIdent b.
+d. = nextIdent c.
+
+nextIdent = succ

system/core/consts/pidents.txt

@@ -0,0 +1,6 @@
+phi = pident zero
+psi = nextPident phi
+chi = nextPident psi
+theta = nextPident chi
+
+nextPident (Pident a) = pident (succ a)

system/funcs/assert.txt system/core/funcs/assert.txt

@@ -0,0 +1,14 @@
+id a = a
+
+dot a b c = a (b c)
+dot2 a b c d = a (b c d)
+
+b1 a * = a
+b0 * a = a
+
+extract (* a) = a
+
+const a * = a
+
+const2 = dot const const
+const3 = dot const const2

system/core/funcs/basic.txt

@@ -0,0 +1,48 @@
+head (Pair * a *) = a
+tail (Pair * * a) = a
+
+singleton a = pair a nil
+
+map f Nil = nil
+map f (Pair x xs) = pair (f x) (map f xs)
+
+foldl f z Nil = z
+foldl f z (Pair x xs) = foldl f (f z x) xs
+
+foldr f z Nil = z
+foldr f z (Pair x xs) = f x (foldr f z xs)
+
+all f list = foldl (all_ f) true list
+all_ f a b = and a (f b)
+
+any f list = foldl (any_ f) false list
+any_ f a b = or a (f b)
+
+rawList = rawList_ nil
+rawList_ list Nil = list
+rawList_ list a = rawList_ (pair a list)
+
+length = foldl (dot2 succ b1) zero
+
+empty = eq nil
+
+nempty = dot not empty
+
+elem e Nil = False
+elem e (Pair e *) = True
+elem e (Pair * rest) = elem e rest
+
+reverse list = reverse_ list nil
+reverse_ Nil list = list
+reverse_ (Pair x xs) list = reverse_ xs (pair x list)
+
+takeWhile f Nil = nil
+takeWhile f (Pair x xs) = ite (f x)
+  takeWhile_ (const3 nil) f x xs
+takeWhile_ f x xs = pair x (takeWhile f xs)
+
+dropWhile f Nil = nil
+dropWhile f y:(Pair x xs) = ite (f x)
+  dropWhile_1 dropWhile_2 f x xs
+dropWhile_1 f x xs = dropWhile f xs
+dropWhile_2 f x xs = pair x xs

system/core/funcs/list.txt

@@ -0,0 +1,13 @@
+natSet.empty = nil
+
+natSet.has = elem
+
+natSet.insert Zero Nil = singleton true
+natSet.insert Zero (Pair * xs) = pair true xs
+natSet.insert (Succ n) Nil = pair false (natSet.insert n nil)
+natSet.insert (Succ n) (Pair x xs) = pair x (natSet.insert n xs)
+
+natSet.remove n set = reverse (dropWhile not (natSet.remove_ n (reverse set)))
+natSet.remove_ * Nil = nil
+natSet.remove_ Zero (Pair * xs) = pair false xs
+natSet.remove_ (Succ n) (Pair x xs) = pair x (natSet.remove_ n xs)

system/core/funcs/nat-set.txt

@@ -1,3 +1,7 @@
+Bool:
+  bool a:True = Bool a
+  bool a:False = Bool a
+
 True:
   true = True
 

system/core/nat.txt

@@ -0,0 +1,13 @@
+Nat:
+  nat a:Zero = Nat a
+  nat a:(Succ *) = Nat a
+
+Zero:
+  zero = Zero
+
+Succ:
+  succ a:Zero = Succ a
+  succ a:(Succ *) = Succ a
+
+for f z Zero = z
+for f z (Succ a) = f (for f z a)

system/core/proof.txt

@@ -6,7 +6,7 @@ Pred:
   pred a:(Pelem * *) = Pred a
 
 Pident:
-  pident_ (Strict.Nat a) = Pident a
+  pident_ (Nat a) = Pident a
 
 Impl:
   impl_ (Pred a) (Pred b) = Impl a b
@@ -15,13 +15,13 @@ Pnot:
   pnot_ (Pred a) = Pnot a
 
 Forall:
-  forall_ (Strict.Nat a) (Pred b) = Forall a b
+  forall_ (Nat a) (Pred b) = Forall a b
 
 Pelem:
-  pelem_ (Strict.Nat a) (Strict.Nat b) = Pelem a b
+  pelem_ (Nat a) (Nat b) = Pelem a b
 
-pident a = pident_ (strict.nat a)
+pident a = pident_ (nat a)
 impl a b = impl_ (pred a) (pred b)
 pnot a = pnot_ (pred a)
-forall a b = forall_ (strict.nat a) (pred b)
-pelem a b = pelem_ (strict.nat a) (strict.nat b)
+forall a b = forall_ (nat a) (pred b)
+pelem a b = pelem_ (nat a) (nat b)

system/types/bool.txt system/core/types/bool.txt

@@ -0,0 +1,34 @@
+Proof:
+  rule.inst_ (Proof phi) a:(Pident *) (Pred p) = assert (noFreeIdents p)
+    (Proof (substPident a p phi))
+  rule.mp (Proof (Impl a b)) (Proof a) = Proof b
+
+  ax.prop.1 = Proof (impl phi (impl psi phi))
+  ax.prop.2 = Proof (impl (impl phi (impl psi chi)) (impl (impl phi psi) (impl phi chi)))
+  ax.prop.3 = Proof (impl (impl (pnot phi) (pnot psi)) (impl psi phi))
+
+rule.inst a b c = rule.inst_ a b (pred c)
+
+substPident pident:(Pident *) p pident = p
+substPident pident:(Pident *) p a:(Pident *) = a
+substPident pident:(Pident *) p (Impl a b) = impl (substPident pident p a) (substPident pident p b)
+substPident pident:(Pident *) p (Pnot a) = pnot (substPident pident p a)
+substPident pident:(Pident *) p (Forall a b) = forall a (substPident pident p b)
+substPident pident:(Pident *) p a:(Pelem * *) = a
+
+substIdent ident1 ident2 (Impl a b) = impl (substIdent ident1 ident2 a) (substIdent ident1 ident2 b)
+substIdent ident1 ident2 (Pnot a) = pnot (substIdent ident1 ident2 a)
+substIdent ident1 ident2 x:(Forall ident1 b) = x
+substIdent ident1 ident2 (Forall a b) = forall a (substIdent ident1 ident2 b)
+substIdent ident1 ident2 (Pelem a b) = pelem (replaceIdent ident1 ident2 a) (replaceIdent ident1 ident2 b)
+
+getFreeIdents p = getFreeIdents_ p natSet.empty
+getFreeIdents_ (Pident *) set = set
+getFreeIdents_ (Impl a b) set = getFreeIdents_ b (getFreeIdents_ a set)
+getFreeIdents_ (Pnot a) set = getFreeIdents_ a set
+getFreeIdents_ (Forall ident a) set = natSet.remove ident (getFreeIdents_ a set)
+getFreeIdents_ (Pelem a b) set = natSet.insert b (natSet.insert a set)
+
+hasFreeIdents = dot nempty getFreeIdents
+
+noFreeIdents = dot empty getFreeIdents