Sat May 4 15:34:38 EDT 2024

--- /fd/5
+++ /sys/src/cmd/eqn/mkfile
@@ -23,7 +23,7 @@
	size.$O\
	sqrt.$O\
	text.$O\
- eqn.$O\
+ y.tab.$O\

 YFILES=eqn.y\

@@ -39,8 +39,7 @@
 YFLAGS=-d -S
 CFLAGS=-c

-eqn.c: y.tab.c prevy.tab.h
- cp y.tab.c $target
+y.tab.c: prevy.tab.h

 prevy.tab.h: y.tab.h
	rc -c 'cmp -s y.tab.h prevy.tab.h || cp y.tab.h prevy.tab.h'

mk eqn
pcc -c main.c
pcc -c tuning.c
pcc -c diacrit.c
pcc -c eqnbox.c
pcc -c font.c
pcc -c fromto.c
pcc -c funny.c
pcc -c glob.c
pcc -c integral.c
pcc -c input.c
pcc -c lex.c
pcc -c lookup.c
pcc -c mark.c
pcc -c matrix.c
pcc -c move.c
pcc -c over.c
pcc -c paren.c
pcc -c pile.c
pcc -c shift.c
pcc -c size.c
pcc -c sqrt.c
pcc -c text.c
rc -c 'cmp -s y.tab.h prevy.tab.h || cp y.tab.h prevy.tab.h'
yacc -d -S eqn.y prevy.tab.h
/sys/src/cmd/eqn/text.c:69[stdin:691] name not declared: QTEXT
/sys/src/cmd/eqn/text.c:79[stdin:701] name not declared: SPACE
/sys/src/cmd/eqn/text.c:81[stdin:703] name not declared: THIN
/sys/src/cmd/eqn/text.c:83[stdin:705] name not declared: TAB

conflicts: 155 shift/reduce
pcc: cpp: 9c 203798: error
mk: pcc -c text.c : exit status=pcc 203796: cpp: 9c 203798: error
mk: for(i in 1a ...  : exit status=rc 201456: mk 203728: error
mk: mk $MKFLAGS yacc.install ...  : exit status=mk 200851: error
mk: date for (i ...  : exit status=rc 195440: mk 200833: error
term% cd /sys/src/cmd/eqn

autolog ON
autolog_colors OFF
autolog_ignore_targets
autolog_level all -crap -clientcrap -ctcps
autolog_only_saved_channels OFF
autolog_path ~/irclogs/$tag/$0.log

test3000

test - ist keine kunst - fuer den markt - kann auch weg,
es gibt im kapitalsmus 2 grosse muellberge: der markt und den verpackungsmuell

test

/proc/509/text:amd64 plan 9 executable
/sys/lib/acid/port
/sys/lib/acid/amd64
acid: abort()+0x0 /sys/src/libc/9sys/abort.c:6
_assert(s=0x40c580)+0x42 /sys/src/libc/port/_assert.c:12
runsweep(id=0x3)+0x8f7 /tmp/gefs/fs.c:2410
	oldhd=0x555b548
	am=0x557cac0
	i=0x40910300000007
	a=0x54f5fe0
	bp=0xffffffffffffffff
	nb=0x4072c0
	b=0x406520
	t=0x5
	off=0x4f8000
	buf=0x100000000000000
	m=0x1fd00409103
launch(f=0x20fab7,text=0x407533,arg=0x0)+0xd0 /tmp/gefs/main.c:212
	id=0x3
main(argc=0x0,argv=0x7fffffffef80)+0x4ab /tmp/gefs/main.c:417
	nann=0x0
	memsz=0x1fa8a000
	_argc=0x66
	_args=0x4074f7
	ann=0x0
	e=0x7fffffffefa7
	s=0x54f2e30
	i=0x2207b400000001
	srvfd=0x100000006
_callmain+0x38 /sys/src/libc/9sys/callmain.c:21
acid:
echo kill > /proc/509/ctl

typedef struct proposition proposition;

#pragma varargck type "P" proposition

struct proposition {
	enum {
		// defined in ascending precedence order
		STATEMENT, AXIOM, VARIABLE,
		NEGATION,
		CONJUNCTION, DISJUNCTION, XOR,
		CONDITIONAL, BICONDITIONAL,
	} type;
	int value;
	union {
		char *statement;
		struct {
			char varletter;
			// the proposition the variable stands for, if known
			proposition *varvalue;
		};
		struct {
			proposition *cond1, *cond2;
		};
		proposition *base;
	};
};

typedef struct {
	int nparams;
	proposition **params;
	// 2^(nparams); here for convenience.
	int nrows;
	int ncolumns;
	proposition **columns;
	// Values are a 2d-array, where each row is listed in order
	// An entry is thus at index row*ncolumns+column
	int *values;
	proposition *p;
} truthtable;

#include <u.h>
#include <libc.h>
#include "logic.h"

// Returns 1 if true, 0 if false, and -1 if unknown
int
propositionvalue(proposition p)
{
	switch(p.type){
	case STATEMENT:
		return -1;
	case AXIOM:
		return p.value;
	case VARIABLE:
		if(p.varvalue)
			return propositionvalue(*p.varvalue);
		return -1;
	case NEGATION:
		return !propositionvalue(*p.base);
	case CONJUNCTION:
		return propositionvalue(*p.cond1) && propositionvalue(*p.cond2);
	case DISJUNCTION:
		return propositionvalue(*p.cond1) || propositionvalue(*p.cond2);
	case XOR:
		return propositionvalue(*p.cond1) != propositionvalue(*p.cond2);
	case CONDITIONAL:
		return !propositionvalue(*p.cond1) || propositionvalue(*p.cond2);
	case BICONDITIONAL:
		return propositionvalue(*p.cond1) == propositionvalue(*p.cond2);
	}
	sysfatal("impossible.");
	return 0;
}

static proposition T = {.type = AXIOM, .value = 1};
static proposition F = {.type = AXIOM, .value = 0};

static proposition*
getprop(void)
{
	// TODO: arena for GC? Refcounting?
	return malloc(sizeof(proposition));
}

proposition*
statement(char *stmt)
{
	proposition *p = getprop();
	p->type = STATEMENT;
	p->statement = stmt;
	return p;
}

proposition*
variable(char c)
{
	proposition *p = getprop();
	p->type = VARIABLE;
	p->varletter = c;
	p->varvalue = nil;
	return p;
}

proposition*
boundvariable(char c, proposition *q)
{
	proposition *p = variable(c);
	p->varvalue = q;
	return p;
}

proposition*
negation(proposition *p)
{
	proposition *notp = getprop();
	notp->type = NEGATION;
	notp->base = p;
	return notp;
}

proposition*
dual(proposition *p, proposition *q, int type)
{
	proposition *dual = getprop();
	dual->type = type;
	dual->cond1 = p;
	dual->cond2 = q;
	return dual;
}

fn xor(proposition* p, proposition* q) proposition* → dual(p, q, XOR);
fn disjunction(proposition* p, proposition* q) proposition* → dual(p, q,
DISJUNCTION);
fn conjunction(proposition* p, proposition* q) proposition* → dual(p, q,
CONJUNCTION);
fn conditional(proposition* p, proposition* q) proposition* → dual(p, q,
CONDITIONAL);
fn biconditional(proposition* p, proposition* q) proposition* → dual(p, q,
BICONDITIONAL);
fn converse(proposition* cond) proposition* → dual(cond->cond2, cond->cond1,
CONDITIONAL);
fn inverse(proposition* cond) proposition* → dual(negation(cond->cond1),
negation(cond->cond2), CONDITIONAL);
fn contrapositive(proposition* cond) proposition* → converse(inverse(cond));

fn opsymbol(int type) char* → {
	switch(type){
	case CONJUNCTION:
		return "∧";
	case DISJUNCTION:
		return "∨";
	case CONDITIONAL:
		return "→";
	case BICONDITIONAL:
		return "←→";
	case NEGATION:
		return "¬";
	case XOR:
		return "⊕";
	}
	abort();
	return nil;
}

static void
snpropprint(proposition *p, char *buf, usize len)
{
	char *tokens[128];
	int ntokens;
	int off;
	char nbuf[128];
	int type;
	proposition *q;
	switch(p->type){
	case STATEMENT:
	case AXIOM:
		snprint(buf, len, "%s", p->statement);
		return;
	case VARIABLE:
		snprint(buf, len, "%c", p->varletter);
		return;
	case NEGATION:
		type = p->base->type;
		q = p;
		while(type == NEGATION){
			type = q->base->type;
			q = q->base;
		}
		switch(p->base->type){
		case NEGATION:
			snprint(buf, len, "¬%P", p->base);
			return;
		case AXIOM:
		case STATEMENT:
			off = snprint(buf, len, "It is not true that %P",
			p->base);
			strncpy(nbuf, buf, 128);
			buf[20] = tolower(buf[20]);
			// If trivial, make it fancier.
			ntokens = tokenize(nbuf, tokens, 128);
			for(int i = 0; i < ntokens-1; i += 1){
				if(strcmp(tokens[i], "is") == 0){
					off = 0;
					for(int j = 0; j <= i && off < len;
					j += 1){
						off += snprint(buf+off, len-off,
						"%s ", tokens[j]);
					}
					if(strcmp(tokens[i+1], "not") == 0){
						// drop the next token, but print
						as is
						i+=1;
					} else {
						// replace this token with "is
						not" and merge
						off += snprint(buf+off, len-off,
						"not ");
					}
					for(int j = i+1; j < ntokens && off
					< len; j += 1){
						off += snprint(buf+off, len-off,
						"%s ", tokens[j]);
					}
					break;
				}
				else if(strcmp(tokens[i], "At") == 0 &&
				strcmp(tokens[i+1], "least") == 0){
					off = 0;
					tokens[i] = "Less";
					tokens[i+1] = "than";
					for(int j = 0; j < ntokens && off <
					len; j += 1){
						off += snprint(buf+off, len-off,
						"%s ", tokens[j]);
					}
					break;
				}
			}
			break;
		case VARIABLE:
		case CONJUNCTION:
		case DISJUNCTION:
		case XOR:
		case CONDITIONAL:
		case BICONDITIONAL:
			// When negating a logical construct, it makes more sense
			to use logical notation.
			// check if logical construct; use ¬ instead of if so.
			type = (type >= VARIABLE);
			snprint(buf, len, "%s%P%s", type ? "¬(" : "It is not true
			that ", p->base, type ? ")" : "");
			break;
		default:
			abort();
		}
		return;
	case CONJUNCTION:
	case DISJUNCTION:
	case XOR:
	case CONDITIONAL:
	case BICONDITIONAL:
		snprint(buf, len, "(%P %s %P)", p->cond1, opsymbol(p->type),
		p->cond2);
		return;
	}
}

static int
Pfmt(Fmt *f)
{
	char buf[1024];
	proposition *p = va_arg(f->args, proposition*);
	snpropprint(p, buf, 1024);
	return fmtprint(f, "%s", buf);
}

static void
ttinsertparam(truthtable *t, proposition *p){
	int missing = 1;
	for(int i = 0; i < t->nparams; i += 1){
		if(t->params[i]->varletter == p->varletter){
			missing = 0;
			break;
		}
	}
	if(missing){
		t->nparams += 1;
		t->params = realloc(t->params, sizeof(proposition*) *
		t->nparams);
		t->params[t->nparams-1] = p;
	}
}

// This checks only that the _structure_ of the propositions are the same.
// This DOES NOT CHECK FOR EQUIVALENCE
int
propositionsequal(proposition *p, proposition *q)
{
	if(p->type != q->type)
		return 0;
	switch(p->type){
	case AXIOM:
		return p->value == q->value;
	case STATEMENT:
		return strcmp(p->statement, q->statement) == 0;
	case VARIABLE:
		return p->varletter == q->varletter;
	case NEGATION:
		return propositionsequal(p->base, q->base);
	case CONJUNCTION:
	case DISJUNCTION:
	case XOR:
	case CONDITIONAL:
	case BICONDITIONAL:
		return propositionsequal(p->cond1, q->cond1) &&
		propositionsequal(p->cond2, q->cond2);
	}
	return 0;
}

void
ttinsertcolumn(truthtable *t, proposition *p)
{
	for(int i = 0; i < t->ncolumns; i += 1)
		if(propositionsequal(p, t->columns[i]))
			return;
	t->ncolumns += 1;
	t->columns = realloc(t->columns, t->ncolumns *
	sizeof(proposition*));
	t->columns[t->ncolumns-1] = p;
}

// Walks down compound proposition `p`, finding parameters to
// insert into truthtable `t`.  Also finds smaller compounds to
// insert as columns.
void
ttrecurse(truthtable *t, proposition *p)
{
	switch(p->type){
	case STATEMENT:
	case AXIOM:
		// TODO maybe reject these?
		break;
	case VARIABLE:
		ttinsertparam(t, p);
		break;
	case NEGATION:
		ttrecurse(t, p->base);
		ttinsertcolumn(t, p);
		break;
	case CONJUNCTION:
	case DISJUNCTION:
	case XOR:
	case CONDITIONAL:
	case BICONDITIONAL:
		ttrecurse(t, p->cond1);
		ttrecurse(t, p->cond2);
		ttinsertcolumn(t, p);
		break;
	}
}

truthtable*
propositiontruthtable(proposition *p)
{
	truthtable *t = malloc(sizeof(truthtable));
	memset(t, 0, sizeof(*t));
	t->p = p;
	// Walk the compound bottom-up, finding premises and partial compounds
	// e.g.  given (p∨¬q)∧(¬q∧p), we have p and q as premises, and a column
	for each of
	// ¬q, p∨¬q, ¬q∧p, and the final column for the full proposition.
	// After finding premises and columns, evaluate the proposition with each
	possible set
	// of variables, and fill in each row with one entry per column.
	ttrecurse(t, p);
	if(t->nparams == 0)
		return nil;
	t->nrows = 2 << (t->nparams - 1);
	t->values = malloc(sizeof(int) * t->nrows * t->ncolumns);
	for(int c = 0; c < t->ncolumns; c += 1){
		for(u32int counter = 0; counter < t->nrows; counter += 1){
			// parameter N is true if counter bit N is set
			for(int i = 0; i < t->nparams; i += 1){
				if((counter >> i) & 0x1)
					t->params[i]->varvalue = &T;
				else
					t->params[i]->varvalue = &F;
			}
			t->values[counter*t->ncolumns+c] =
			propositionvalue(*(t->columns[c]));
		}
	}
	return t;
}

// modified fmtprint to return widths
int
fmtnprint(Fmt *f, char *fmt, ...)
{
	va_list va;
	int n;

	f->flags = 0;
	f->width = 0;
	f->prec = 0;
	va = f->args;
	va_start(f->args, fmt);
	n = dofmt(f, fmt);
	va_end(f->args);
	f->flags = 0;
	f->width = 0;
	f->prec = 0;
	f->args = va;
	return n;
}

static int
Tfmt(Fmt *f)
{
	Rune buf[1024];
	int *widths;
	int n;
	proposition *p = va_arg(f->args, proposition*);
	truthtable *t = propositiontruthtable(p);
	widths = malloc(sizeof(int) * t->ncolumns);
	fmtprint(f, "=============================\n");
	fmtprint(f, "| ");
	// Print out all the column headers; the first is the list of parameters
	for(int i = 0; i < t->nparams; i += 1)
		fmtprint(f, "%c", t->params[i]->varletter);
	fmtprint(f, " |");
	// Then, for each row, print the value of each parameter, and of each
	column
	for(int i = 0; i < t->ncolumns; i += 1){
		widths[i] = runesnprint(buf, 1024, " %P ", t->columns[i]);
		fmtprint(f, "%S|", buf);
	}
	fmtprint(f, "\n");
	for(int counter = 0; counter < t->nrows; counter += 1){
		fmtprint(f, "| ");
		for(int i = 0; i < t->nparams; i += 1)
			fmtprint(f, "%c", ((counter >> i) & 0x1) ? 'T' :
			'F');
		fmtprint(f, " |");
		for(int i = 0; i < t->ncolumns; i += 1){
			n = fmtnprint(f, " %s ",
			t->values[counter*t->ncolumns+i]?"T":"F");
			for(;n < widths[i]; n += 1)
				fmtprint(f, " ");
			fmtnprint(f, "|");
		}
		fmtnprint(f, "\n");
	}
	fmtnprint(f, "=============================\n");
	free(widths);

	return 0;
}

static int
propositionisstatic(proposition *p, int value){
	if(p->type == AXIOM || p->type == STATEMENT || p->type ==
	VARIABLE)
		return p->value == value;
	truthtable *t = propositiontruthtable(p);
	for(int i = 0; i < t->nrows; i += 1){
		if(t->values[i*t->ncolumns+(t->ncolumns-1)] != value)
			return 0;
	}
	return 1;
}

fn propositionistautology(proposition* p) int → propositionisstatic(p, 1);
fn propositioniscontradiction(proposition* p) int → propositionisstatic(p, 0);
fn propositioniscontingency(proposition* p) int → !(propositionistautology(p) ||
propositioniscontradiction(p));
fn propositionsequivalent(proposition* p, proposition* q) int →
	propositionistautology(biconditional(p, q));

static void
init(void)
{
	T.statement = "T";
	F.statement = "F";
	fmtinstall('P', Pfmt);
	fmtinstall('T', Tfmt);
}

void
main(void)
{
	init();
	proposition *p = variable('p');
	proposition *q = variable('q');
	proposition *r = variable('r');
	proposition *s = variable('s');
	print("%T\n", negation(p));
	print("%T\n", conjunction(p, q));
	print("%T\n", disjunction(p, q));
	print("%T\n", xor(p, q));
	print("%T\n", conditional(p, q));
	print("contrapositive equivalence: %s\n",
	propositionsequivalent(conditional(p, q), contrapositive(conditional(p,
	q))) ? "OK" : "FAIL");
	print("biconditional equivalent to conditional and converse: %s\n",
	propositionsequivalent(
		biconditional(p, q),
		conjunction(
			conditional(p, q),
			converse(conditional(p, q))
		)
	) ? "OK" : "FAIL");
	print("%T\n", biconditional(p, q));
	print("%T\n", conditional(
		disjunction(p, negation(q)),
		conjunction(p, q)
	));
	print("%T\n", biconditional(
		biconditional(p, q),
		biconditional(r, s)
	));
	assert(propositionistautology(disjunction(p, negation(p))));
	assert(propositioniscontradiction(conjunction(p, negation(p))));
	assert(propositionsequivalent(
		negation(disjunction(p, q)),
		conjunction(negation(p), negation(q))
	));
	assert(propositionsequivalent(
		conditional(p, q),
		disjunction(negation(p), q)
	));
	// p ∨ (q ∧ r) ≡ (p ∨ q) ∧ (p ∨ r)
	assert(propositionsequivalent(
		disjunction(p, conjunction(q, r)),
		conjunction(disjunction(p, q), disjunction(p, r))
	));
	exits(nil);
}

// TODO: keep track of known equivalences, use to build further instead of always
relying on truth tables
// Next step: math parsing.  Need to be able to evaluate mathematical propositions
before we can introduce predicates.

Zdravo, htio sam znati vašu cijenu.

diff 8ddb649e641ce9373a9e73bf4ba1b7532bff44d4 uncommitted
--- a/sys/src/cmd/jl/asm.c
+++ b/sys/src/cmd/jl/asm.c
@@ -83,10 +83,13 @@
	case 2:
	case 3:
	case 5:
- case 6:
		OFFSET = HEADR+textsize;
		seek(cout, OFFSET, 0);
		break;
+ case 6: /* headerless, padded segments */
+ OFFSET = rnd(HEADR+textsize, INITRND);
+ seek(cout, OFFSET, 0);
+ break;
	}
	for(t = 0; t < datsize; t += sizeof(buf)-100) {
		if(datsize-t > sizeof(buf)-100)
@@ -111,8 +114,11 @@
		case 2:
		case 1:
		case 5:
- case 6:
			OFFSET = HEADR+textsize+datsize;
+ seek(cout, OFFSET, 0);
+ break;
+ case 6: /* headerless, padded segments */
+ OFFSET += rnd(datsize, INITRND);
			seek(cout, OFFSET, 0);
			break;
		}
--- a/sys/src/cmd/jl/obj.c
+++ b/sys/src/cmd/jl/obj.c
@@ -119,6 +119,7 @@
		errorexit();

	case 1: /* headerless */
+ case 6: /* headerless, padded segments */
		HEADR = 0;
		if(INITTEXT == -1)
			INITTEXT = 0;

prev | next