Implement exact rational numbers
This commit is contained in:
parent
c447eb7397
commit
d3fa70bea8
1 changed files with 37 additions and 14 deletions
51
js/mpl.js
51
js/mpl.js
|
|
@ -1,6 +1,18 @@
|
|||
'use strict';
|
||||
/* ================= MPL M0 interpreter (10 tests in js/test/) ================= */
|
||||
/* ============ MPL M0 interpreter (ratified semantics: conformance/JUDGMENT_CALLS.md) ============ */
|
||||
const BOT=Symbol('⊥'),NOMATCH=Symbol('nomatch');
|
||||
/* Numbers are exact rationals (ruling 4): BigInt numerator/denominator,
|
||||
gcd-reduced, denominator > 0, constructed once at creation. */
|
||||
const gcd=(a,b)=>{a=a<0n?-a:a;b=b<0n?-b:b;while(b){const t=a%b;a=b;b=t}return a};
|
||||
const rat=(n,d=1n)=>{if(d<0n){n=-n;d=-d}const g=gcd(n,d)||1n;return{q:true,n:n/g,d:d/g}};
|
||||
const isRat=v=>!!v&&typeof v==='object'&&v.q===true;
|
||||
const R={add:(a,b)=>rat(a.n*b.d+b.n*a.d,a.d*b.d),sub:(a,b)=>rat(a.n*b.d-b.n*a.d,a.d*b.d),
|
||||
mul:(a,b)=>rat(a.n*b.n,a.d*b.d),neg:a=>rat(-a.n,a.d),
|
||||
cmp:(a,b)=>{const l=a.n*b.d,r=b.n*a.d;return l<r?-1:l>r?1:0},eq:(a,b)=>a.n===b.n&&a.d===b.d};
|
||||
/* String ordering is Unicode code-point order (ruling 8). No locale, ever. */
|
||||
const cmpStr=(a,b)=>{const A=[...a],B=[...b],m=Math.min(A.length,B.length);
|
||||
for(let i=0;i<m;i++){const x=A[i].codePointAt(0),y=B[i].codePointAt(0);if(x!==y)return x<y?-1:1}
|
||||
return A.length===B.length?0:A.length<B.length?-1:1};
|
||||
const ESCAPES={lambda:'λ',forall:'∀',in:'∈',coloneq:'≜',leftarrow:'←',implies:'⟹',and:'∧',or:'∨',neq:'≠',leq:'≤',geq:'≥',times:'×',div:'÷',trace:'✎',bot:'⊥',parallel:'‖',circ:'∘',ast:'∗'};
|
||||
function lex(src){const toks=[];let i=0,line=1,col=1;const push=(t,v,l,c)=>toks.push({t,v,line:l,col:c});const err=(key,l,c)=>{const e=new Error(key);e.key=key;e.line=l;e.col=c;throw e};
|
||||
while(i<src.length){const ch=src[i],l=line,c=col;const adv=n=>{for(let k=0;k<n;k++){if(src[i]==='\n'){line++;col=1}else col++;i++}};
|
||||
|
|
@ -9,11 +21,11 @@ if(ch==='-'&&src[i+1]==='-'){while(i<src.length&&src[i]!=='\n')adv(1);continue}
|
|||
if(ch==='{'&&src[i+1]==='-'){let d=0;while(i<src.length){if(src[i]==='{'&&src[i+1]==='-'){d++;adv(2)}else if(src[i]==='-'&&src[i+1]==='}'){d--;adv(2);if(!d)break}else adv(1)}if(d)err('err_comment',l,c);continue}
|
||||
if(ch==='"'){adv(1);let s='';while(i<src.length&&src[i]!=='"'){if(src[i]==='\\'){adv(1);const e=src[i];s+=e==='n'?'\n':e==='t'?'\t':e;adv(1)}else{s+=src[i];adv(1)}}if(src[i]!=='"')err('err_string',l,c);adv(1);push('str',s,l,c);continue}
|
||||
if(ch==='\\'){adv(1);let w='';while(i<src.length&&/[a-zA-Z]/.test(src[i])){w+=src[i];adv(1)}const g=ESCAPES[w];if(!g)err('err_escape',l,c);push(...tokFor(g,l,c));continue}
|
||||
if(/[0-9]/.test(ch)){let n='';while(i<src.length&&/[0-9]/.test(src[i])){n+=src[i];adv(1)}if(src[i]==='.'&&/[0-9]/.test(src[i+1])){n+='.';adv(1);while(i<src.length&&/[0-9]/.test(src[i])){n+=src[i];adv(1)}}push('num',parseFloat(n),l,c);continue}
|
||||
if(/[0-9]/.test(ch)){let n='';while(i<src.length&&/[0-9]/.test(src[i])){n+=src[i];adv(1)}let f='';if(src[i]==='.'&&/[0-9]/.test(src[i+1])){adv(1);while(i<src.length&&/[0-9]/.test(src[i])){f+=src[i];adv(1)}}push('num',rat(BigInt(n+f),10n**BigInt(f.length)),l,c);continue}
|
||||
if(/[a-zA-Z]/.test(ch)){let w='';while(i<src.length&&/[a-zA-Z0-9_]/.test(src[i])){w+=src[i];adv(1)}if(w==='true')push('bool',true,l,c);else if(w==='false')push('bool',false,l,c);else push('id',w,l,c);continue}
|
||||
/* Type symbols lex as identifiers so ∈-constraints (λn∈ℕ:) parse; the
|
||||
parser discards the constraint unevaluated — see §5 “Open problems”:
|
||||
parsed today, not yet enforced. 𝔹 is supplementary-plane (2 units). */
|
||||
parser discards the constraint unevaluated — ruling 17. 𝔹 is
|
||||
supplementary-plane (2 units). */
|
||||
const glyph=String.fromCodePoint(src.codePointAt(i));
|
||||
if('ℕℤℚℝℂ𝔹'.includes(glyph)){adv(glyph.length);push('id',glyph,l,c);continue}
|
||||
const single='✎λ∀∈≜←⟹∧∨≠≤≥×÷∗∘‖⊥+-/=<>|;:,()[]{}';
|
||||
|
|
@ -31,10 +43,10 @@ function parallel(){let l=def();while(at('par')){p++;l={k:'seq',es:[l,def()]}}re
|
|||
function def(){const l=assign();if(at('def')){const tk=toks[p++];if(l.k!=='id')err('err_def_target',tk);return{k:'def',name:l.v,e:def(),line:tk.line,col:tk.col}}return l}
|
||||
function assign(){const l=cond();if(at('assign')){const tk=toks[p++];if(l.k!=='id')err('err_assign_target',tk);return{k:'set',name:l.v,e:assign(),line:tk.line,col:tk.col}}return l}
|
||||
function cond(){let l=implies();while(at('bar')){p++;l={k:'alt',l,r:implies()}}return l}
|
||||
function implies(){const l=lor();if(at('implies')){p++;return{k:'imp',c:l,e:implies()}}return l}
|
||||
function lor(){let l=land();while(at('or')){p++;l={k:'or',l,r:land()}}return l}
|
||||
function land(){let l=compare();while(at('and')){p++;l={k:'and',l,r:compare()}}return l}
|
||||
function compare(){const l=add();const ops={eq:1,neq:1,lt:1,gt:1,leq:1,geq:1};if(ops[peek().t]){const o=toks[p++].t;return{k:'cmp',o,l,r:add()}}return l}
|
||||
function implies(){const l=lor();if(at('implies')){const tk=toks[p++];return{k:'imp',c:l,e:implies(),line:tk.line,col:tk.col}}return l}
|
||||
function lor(){let l=land();while(at('or')){const tk=toks[p++];l={k:'or',l,r:land(),line:tk.line,col:tk.col}}return l}
|
||||
function land(){let l=compare();while(at('and')){const tk=toks[p++];l={k:'and',l,r:compare(),line:tk.line,col:tk.col}}return l}
|
||||
function compare(){const l=add();const ops={eq:1,neq:1,lt:1,gt:1,leq:1,geq:1};if(ops[peek().t]){const tk=toks[p++];return{k:'cmp',o:tk.t,l,r:add(),line:tk.line,col:tk.col}}return l}
|
||||
function add(){let l=mul();while(at('plus')||at('minus')){const o=toks[p++].t;l={k:'bin',o,l,r:mul(),line:toks[p-1].line,col:toks[p-1].col}}return l}
|
||||
function mul(){let l=unary();while(at('mul')||at('divi')){const o=toks[p++].t;l={k:'bin',o,l,r:unary(),line:toks[p-1].line,col:toks[p-1].col}}return l}
|
||||
function unary(){if(at('trace')){const tk=toks[p++];return{k:'trace',e:unary(),line:tk.line,col:tk.col}}if(at('minus')){const tk=toks[p++];return{k:'neg',e:unary(),line:tk.line,col:tk.col}}return postfix()}
|
||||
|
|
@ -54,9 +66,13 @@ return program()}
|
|||
function runMPL(src,print){const ast=parse(lex(src));const global={vars:new Map(),parent:null};
|
||||
const lookup=(sc,n)=>{for(let s=sc;s;s=s.parent)if(s.vars.has(n))return s;return null};
|
||||
const rte=(key,node)=>{const e=new Error(key);e.key=key;e.line=node.line;e.col=node.col;throw e};
|
||||
const num=(v,node)=>{if(typeof v!=='number')rte('err_num',node);return v};
|
||||
const show=v=>v===BOT?'⊥':typeof v==='string'?v:Array.isArray(v)?'['+v.map(showQ).join(', ')+']':typeof v==='object'&&v&&v.closure?'λ':typeof v==='boolean'?(v?'true':'false'):String(v);
|
||||
const num=(v,node)=>{if(!isRat(v))rte('err_num',node);return v};
|
||||
const show=v=>v===BOT?'⊥':typeof v==='string'?v:Array.isArray(v)?'['+v.map(showQ).join(', ')+']':isRat(v)?(v.d===1n?String(v.n):v.n+'/'+v.d):typeof v==='object'&&v&&v.closure?'λ':typeof v==='boolean'?(v?'true':'false'):String(v);
|
||||
const showQ=v=>typeof v==='string'?'"'+v+'"':show(v);
|
||||
/* Equality is structural on data; any function involved raises err_fn_eq
|
||||
(ruling 7). */
|
||||
const fnIn=v=>!!v&&typeof v==='object'&&(v.closure?true:Array.isArray(v)?v.some(fnIn):false);
|
||||
const dEq=(a,b)=>isRat(a)&&isRat(b)?R.eq(a,b):Array.isArray(a)&&Array.isArray(b)?a.length===b.length&&a.every((x,ix)=>dEq(x,b[ix])):a===b;
|
||||
let steps=0;const strip=v=>v===NOMATCH?BOT:v;
|
||||
function ev(n,sc){if(++steps>500000){const e=new Error('err_steps');e.key='err_steps';e.line=n.line||1;e.col=n.col||1;throw e}
|
||||
switch(n.k){
|
||||
|
|
@ -66,12 +82,19 @@ case 'seq':{let v=BOT;for(const e of n.es){v=ev(e,sc);if(v===NOMATCH)v=BOT}retur
|
|||
case 'def':{const v=strip(ev(n.e,sc));sc.vars.set(n.name,v);return v}
|
||||
case 'set':{const v=strip(ev(n.e,sc));const s=lookup(sc,n.name)||sc;s.vars.set(n.name,v);return v}
|
||||
case 'alt':{const l=ev(n.l,sc);return l===NOMATCH?ev(n.r,sc):l}
|
||||
case 'imp':{const c=strip(ev(n.c,sc));return c===true||(typeof c==='number'&&c!==0)?ev(n.e,sc):NOMATCH}
|
||||
case 'imp':{const c=strip(ev(n.c,sc));return c===true||(isRat(c)&&c.n!==0n)?ev(n.e,sc):NOMATCH}
|
||||
case 'or':{const l=strip(ev(n.l,sc));return l===true?true:strip(ev(n.r,sc))===true}
|
||||
case 'and':{const l=strip(ev(n.l,sc));return l===true?strip(ev(n.r,sc))===true:false}
|
||||
case 'cmp':{const a=strip(ev(n.l,sc)),b=strip(ev(n.r,sc));const eq=JSON.stringify(a)===JSON.stringify(b);switch(n.o){case 'eq':return eq;case 'neq':return!eq;case 'lt':return a<b;case 'gt':return a>b;case 'leq':return a<=b;case 'geq':return a>=b}}
|
||||
case 'bin':{const a=strip(ev(n.l,sc)),b=strip(ev(n.r,sc));switch(n.o){case 'plus':return(typeof a==='string'||typeof b==='string')?show(a)+show(b):num(a,n)+num(b,n);case 'minus':return num(a,n)-num(b,n);case 'mul':return num(a,n)*num(b,n);case 'divi':{const d=num(b,n);if(d===0)rte('err_div0',n);return num(a,n)/d}}}
|
||||
case 'neg':return -num(strip(ev(n.e,sc)),n);
|
||||
case 'cmp':{const a=strip(ev(n.l,sc)),b=strip(ev(n.r,sc));
|
||||
if(n.o==='eq'||n.o==='neq'){if(fnIn(a)||fnIn(b))rte('err_fn_eq',n);const eq=dEq(a,b);return n.o==='eq'?eq:!eq}
|
||||
let d;if(isRat(a)&&isRat(b))d=R.cmp(a,b);else if(typeof a==='string'&&typeof b==='string')d=cmpStr(a,b);else rte('err_compare',n);
|
||||
switch(n.o){case 'lt':return d<0;case 'gt':return d>0;case 'leq':return d<=0;case 'geq':return d>=0}}
|
||||
case 'bin':{const a=strip(ev(n.l,sc)),b=strip(ev(n.r,sc));switch(n.o){
|
||||
case 'plus':return(typeof a==='string'||typeof b==='string')?show(a)+show(b):R.add(num(a,n),num(b,n));
|
||||
case 'minus':return R.sub(num(a,n),num(b,n));
|
||||
case 'mul':return R.mul(num(a,n),num(b,n));
|
||||
case 'divi':{const bb=num(b,n);if(bb.n===0n)rte('err_div0',n);const aa=num(a,n);return rat(aa.n*bb.d,aa.d*bb.n)}}}
|
||||
case 'neg':return R.neg(num(strip(ev(n.e,sc)),n));
|
||||
case 'trace':{const v=strip(ev(n.e,sc));print(show(v));return v}
|
||||
case 'lam':return{closure:true,ps:n.ps,body:n.body,sc};
|
||||
case 'call':{const f=strip(ev(n.f,sc));if(!f||!f.closure)rte('err_notfn',n);if(f.ps.length!==n.args.length)rte('err_arity',n);const inner={vars:new Map(),parent:f.sc};f.ps.forEach((pn,ix)=>inner.vars.set(pn,strip(ev(n.args[ix],sc))));return strip(ev(f.body,inner))}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue