From fc57f94e8ae0a04fedb026530929754c7f205b62 Mon Sep 17 00:00:00 2001 From: "John J. Camilleri" Date: Wed, 13 Oct 2021 16:59:11 +0200 Subject: [PATCH] Finish unmarshalling of types. Add mkType et al. Add showType tests, but implementation is just stub. --- src/runtime/javascript/expr.ts | 33 +++++++- src/runtime/javascript/ffi.ts | 66 +++++++++++----- src/runtime/javascript/index.ts | 18 ++++- src/runtime/javascript/tests/basic.test.ts | 91 ++++++++++++++++++++-- 4 files changed, 177 insertions(+), 31 deletions(-) diff --git a/src/runtime/javascript/expr.ts b/src/runtime/javascript/expr.ts index e598b55c5..a3f5bc881 100644 --- a/src/runtime/javascript/expr.ts +++ b/src/runtime/javascript/expr.ts @@ -10,10 +10,37 @@ export class Type { } } +export function mkType (hypos: Hypo[], name: string, exprs: Expr[]): Type { + return new Type(hypos, name, exprs) +} + +export enum BindType { + Explicit, + Implicit +} + export class Hypo { - bind_type!: boolean - var!: string - type!: Type + bind_type: BindType + var: string + type: Type + + constructor (bt: BindType, v: string, t: Type) { + this.bind_type = bt + this.var = v + this.type = t + } +} + +export function mkHypo (type: Type): Hypo { + return new Hypo(BindType.Explicit, '_', type) +} + +export function mkDepHypo (vr: string, type: Type): Hypo { + return new Hypo(BindType.Explicit, vr, type) +} + +export function mkImplHypo (vr: string, type: Type): Hypo { + return new Hypo(BindType.Implicit, vr, type) } export class Expr { diff --git a/src/runtime/javascript/ffi.ts b/src/runtime/javascript/ffi.ts index 4dd78a416..d83e3b6af 100644 --- a/src/runtime/javascript/ffi.ts +++ b/src/runtime/javascript/ffi.ts @@ -48,15 +48,22 @@ export const PgfTextPtr = ref.refType(PgfText) export const PgfItorPtr = ref.refType(ref.types.void) -const PgfType = ref.refType(ref.types.Object) // TODO -// const PgfTypePtr = ref.refType(PgfType) +const PgfType = ref.refType(ref.types.Object) -const PgfTypeHypo = ref.types.void // TODO -const PgfTypeHypoPtr = ref.refType(PgfTypeHypo) +const PgfTypeHypo = Struct({ + bind_type: ref.types.int, + cid: PgfTextPtr, + type: PgfType +}) export const PgfExpr = ref.refType(ref.types.Object) export const PgfLiteral = ref.refType(ref.types.Object) +// export const PgfTypePtr = ref.refType(PgfType) +export const PgfTypeHypoPtr = ref.refType(PgfTypeHypo) +export const PgfExprPtr = ref.refType(PgfExpr) +// export const PgfLiteralPtr = ref.refType(PgfLiteral) + const PgfMetaId = ref.types.int const PgfPrintContext = ref.types.void // TODO @@ -158,7 +165,7 @@ export function PgfText_FromString (str: string): Pointer { // ---------------------------------------------------------------------------- // Un/marshalling -const eabs = ffi.Callback(PgfExpr, [PgfUnmarshaller, ref.types.bool, PgfTextPtr, PgfExpr], +const eabs = ffi.Callback(PgfExpr, [PgfUnmarshallerPtr, ref.types.bool, PgfTextPtr, PgfExpr], function (self, btype: boolean, name: Pointer, body: Pointer): Pointer { const jsname = PgfText_AsString(name) const obj = new ExprAbs(btype, jsname, body.deref()) @@ -167,7 +174,7 @@ const eabs = ffi.Callback(PgfExpr, [PgfUnmarshaller, ref.types.bool, PgfTextPtr, return buf }) -const eapp = ffi.Callback(PgfExpr, [PgfUnmarshaller, PgfExpr, PgfExpr], +const eapp = ffi.Callback(PgfExpr, [PgfUnmarshallerPtr, PgfExpr, PgfExpr], function (self, fun: Pointer, arg: Pointer): Pointer { const obj = new ExprApp(fun.deref(), arg.deref()) const buf = ref.alloc(ref.types.Object) as Pointer @@ -175,7 +182,7 @@ const eapp = ffi.Callback(PgfExpr, [PgfUnmarshaller, PgfExpr, PgfExpr], return buf }) -const elit = ffi.Callback(PgfExpr, [PgfUnmarshaller, PgfLiteral], +const elit = ffi.Callback(PgfExpr, [PgfUnmarshallerPtr, PgfLiteral], function (self, lit: Pointer): Pointer { const litObj = lit.deref() const obj = new ExprLit(litObj) @@ -184,7 +191,7 @@ const elit = ffi.Callback(PgfExpr, [PgfUnmarshaller, PgfLiteral], return buf }) -const emeta = ffi.Callback(PgfExpr, [PgfUnmarshaller, PgfMetaId], +const emeta = ffi.Callback(PgfExpr, [PgfUnmarshallerPtr, PgfMetaId], function (self, meta: number): Pointer { const obj = new ExprMeta(meta) const buf = ref.alloc(ref.types.Object) as Pointer @@ -192,7 +199,7 @@ const emeta = ffi.Callback(PgfExpr, [PgfUnmarshaller, PgfMetaId], return buf }) -const efun = ffi.Callback(PgfExpr, [PgfUnmarshaller, PgfTextPtr], +const efun = ffi.Callback(PgfExpr, [PgfUnmarshallerPtr, PgfTextPtr], function (self, name: Pointer): Pointer { const jsname = PgfText_AsString(name) const obj = new ExprFun(jsname) @@ -201,7 +208,7 @@ const efun = ffi.Callback(PgfExpr, [PgfUnmarshaller, PgfTextPtr], return buf }) -const evar = ffi.Callback(PgfExpr, [PgfUnmarshaller, ref.types.int], +const evar = ffi.Callback(PgfExpr, [PgfUnmarshallerPtr, ref.types.int], function (self, index: number): Pointer { const obj = new ExprVar(index) const buf = ref.alloc(ref.types.Object) as Pointer @@ -209,7 +216,7 @@ const evar = ffi.Callback(PgfExpr, [PgfUnmarshaller, ref.types.int], return buf }) -const etyped = ffi.Callback(PgfExpr, [PgfUnmarshaller, PgfExpr, PgfType], +const etyped = ffi.Callback(PgfExpr, [PgfUnmarshallerPtr, PgfExpr, PgfType], function (self, expr: Pointer, type: Pointer): Pointer { const obj = new ExprTyped(expr.deref(), type.deref()) const buf = ref.alloc(ref.types.Object) as Pointer @@ -217,7 +224,7 @@ const etyped = ffi.Callback(PgfExpr, [PgfUnmarshaller, PgfExpr, PgfType], return buf }) -const eimplarg = ffi.Callback(PgfExpr, [PgfUnmarshaller, PgfExpr], +const eimplarg = ffi.Callback(PgfExpr, [PgfUnmarshallerPtr, PgfExpr], function (self, expr: Pointer): Pointer { const obj = new ExprImplArg(expr.deref()) const buf = ref.alloc(ref.types.Object) as Pointer @@ -225,7 +232,7 @@ const eimplarg = ffi.Callback(PgfExpr, [PgfUnmarshaller, PgfExpr], return buf }) -const lint = ffi.Callback(PgfLiteral, [PgfUnmarshaller, ref.types.size_t, ref.refType(ref.types.int)], +const lint = ffi.Callback(PgfLiteral, [PgfUnmarshallerPtr, ref.types.size_t, ref.refType(ref.types.int)], function (self, size: number, val: Pointer): Pointer { let jsval: number | bigint = 0 if (size === 1) { @@ -263,7 +270,7 @@ const lint = ffi.Callback(PgfLiteral, [PgfUnmarshaller, ref.types.size_t, ref.re return buf }) -const lflt = ffi.Callback(PgfLiteral, [PgfUnmarshaller, ref.types.double], +const lflt = ffi.Callback(PgfLiteral, [PgfUnmarshallerPtr, ref.types.double], function (self, val: number): Pointer { const obj = new Literal(val) const buf = ref.alloc(ref.types.Object) as Pointer @@ -271,7 +278,7 @@ const lflt = ffi.Callback(PgfLiteral, [PgfUnmarshaller, ref.types.double], return buf }) -const lstr = ffi.Callback(PgfLiteral, [PgfUnmarshaller, PgfTextPtr], +const lstr = ffi.Callback(PgfLiteral, [PgfUnmarshallerPtr, PgfTextPtr], function (self, val: Pointer): Pointer { const jsval = PgfText_AsString(val) const obj = new Literal(jsval) @@ -280,19 +287,36 @@ const lstr = ffi.Callback(PgfLiteral, [PgfUnmarshaller, PgfTextPtr], return buf }) -const dtyp = ffi.Callback(PgfType, [PgfUnmarshaller, ref.types.int, PgfTypeHypoPtr, PgfTextPtr, ref.types.int, ref.refType(PgfExpr)], +const dtyp = ffi.Callback(PgfType, [PgfUnmarshallerPtr, ref.types.int, PgfTypeHypoPtr, PgfTextPtr, ref.types.int, PgfExprPtr], function (self, n_hypos: number, hypos: Pointer, cat: Pointer, n_exprs: number, exprs: Pointer): Pointer { - // TODO const jshypos: Hypo[] = [] + if (n_hypos > 0) { + const hyposArr = hypos.reinterpret(PgfTypeHypo.size * n_hypos, 0) + for (let i = 0; i < n_hypos; i++) { + const hypo = ref.get(hyposArr, PgfTypeHypo.size * i, PgfTypeHypo) + const h = new Hypo(hypo.bind_type, PgfText_AsString(hypo.cid), hypo.type.deref() as Type) + jshypos.push(h) + } + } + const jsname = PgfText_AsString(cat) + const jsexprs: Expr[] = [] + if (n_exprs > 0) { + const exprsArr = exprs.reinterpret(PgfExpr.size * n_exprs, 0) + for (let i = 0; i < n_exprs; i++) { + const expr = ref.get(exprsArr, PgfExpr.size * i, PgfExpr) + jsexprs.push(expr.deref() as Expr) + } + } + const obj = new Type(jshypos, jsname, jsexprs) const buf = ref.alloc(ref.types.Object) as Pointer ref.writeObject(buf, 0, obj) return buf }) -const free_ref = ffi.Callback(ref.types.void, [PgfUnmarshaller, ref.refType(ref.types.Object)], +const free_ref = ffi.Callback(ref.types.void, [PgfUnmarshallerPtr, ref.refType(ref.types.Object)], function (self, x: Pointer): void { }) @@ -314,17 +338,17 @@ const un_vtbl = new PgfUnmarshallerVtbl({ export const unmarshaller = new PgfUnmarshaller({ vtbl: un_vtbl.ref() }) -const match_lit = ffi.Callback(ref.types.Object, [PgfMarshaller, PgfUnmarshaller, PgfLiteral], +const match_lit = ffi.Callback(ref.types.Object, [PgfMarshallerPtr, PgfUnmarshallerPtr, PgfLiteral], function (self, u: any, lit: any): Pointer { return 0 as any }) -const match_expr = ffi.Callback(ref.types.Object, [PgfMarshaller, PgfUnmarshaller, PgfExpr], +const match_expr = ffi.Callback(ref.types.Object, [PgfMarshallerPtr, PgfUnmarshallerPtr, PgfExpr], function (self, u: any, expr: any): Pointer { return 0 as any }) -const match_type = ffi.Callback(ref.types.Object, [PgfMarshaller, PgfUnmarshaller, PgfType], +const match_type = ffi.Callback(ref.types.Object, [PgfMarshallerPtr, PgfUnmarshallerPtr, PgfType], function (self, u: any, type: any): Pointer { return 0 as any }) diff --git a/src/runtime/javascript/index.ts b/src/runtime/javascript/index.ts index 753484eeb..6c78db85d 100644 --- a/src/runtime/javascript/index.ts +++ b/src/runtime/javascript/index.ts @@ -2,8 +2,8 @@ import errno from './errno' import { - Type, - Hypo, + Type, mkType, + Hypo, mkHypo, mkDepHypo, mkImplHypo, Expr, ExprAbs, ExprApp, @@ -229,6 +229,10 @@ function readExpr (str: string): Expr { return ref.readObject(expr) as Expr } +function showType (context: string[], type: Type): string { + return 'TODO' +} + // ---------------------------------------------------------------------------- // Exposed library API @@ -242,9 +246,14 @@ export { readType, readExpr, + showType, Type, + mkType, Hypo, + mkHypo, + mkDepHypo, + mkImplHypo, Expr, ExprAbs, ExprApp, @@ -266,9 +275,14 @@ export default { readType, readExpr, + showType, Type, + mkType, Hypo, + mkHypo, + mkDepHypo, + mkImplHypo, Expr, ExprAbs, ExprApp, diff --git a/src/runtime/javascript/tests/basic.test.ts b/src/runtime/javascript/tests/basic.test.ts index a01046fe2..f8164f347 100644 --- a/src/runtime/javascript/tests/basic.test.ts +++ b/src/runtime/javascript/tests/basic.test.ts @@ -2,14 +2,18 @@ import PGF, { PGFError, PGFGrammar, // Type, + mkType, // Hypo, + mkHypo, + mkDepHypo, + mkImplHypo, // Expr, // ExprAbs, ExprApp, ExprLit, ExprMeta, ExprFun, - // ExprVar, + ExprVar, // ExprTyped, ExprImplArg // Literal @@ -225,10 +229,87 @@ describe('abstract syntax', () => { // ---------------------------------------------------------------------------- describe('types', () => { - test('invalid', () => { - expect(() => { - PGF.readType('->') - }).toThrow(PGFError) + describe('read', () => { + test('invalid', () => { + expect(() => { + PGF.readType('->') + }).toThrow(PGFError) + }) + + test('1', () => { + const t1 = PGF.readType('A') + const t2 = PGF.readType('A') + const t3 = PGF.readType('B') + expect(t1).toEqual(t2) + expect(t1).not.toEqual(t3) + }) + + test('2', () => { + const t1 = PGF.readType('A -> B') + const t2 = PGF.readType('A->B') + const t3 = PGF.readType('B->B') + expect(t1).toEqual(t2) + expect(t1).not.toEqual(t3) + }) + + test('3', () => { + const t1 = PGF.readType('A -> B -> C') + const t2 = PGF.readType('A->B -> C') + expect(t1).toEqual(t2) + }) + + test('4', () => { + const t1 = PGF.readType('(x : N) -> P x') + const t2 = mkType([mkDepHypo('x', mkType([], 'N', []))], 'P', [new ExprFun('x')]) + expect(t1).toEqual(t2) + }) + }) + + describe.skip('show', () => { + test('1', () => { + const type = mkType([], 'N', []) + expect(PGF.showType([], type)).toEqual('N') + }) + + test('2', () => { + const type = mkType([mkHypo(mkType([], 'N', []))], 'N', []) + expect(PGF.showType([], type)).toEqual('N -> N') + }) + + test('3', () => { + const type = mkType([mkHypo(mkType([mkHypo(mkType([], 'N', []))], 'N', []))], 'N', []) + expect(PGF.showType([], type)).toEqual('(N -> N) -> N') + }) + + test('4', () => { + const type = mkType([mkDepHypo('x', mkType([], 'N', []))], 'P', [new ExprVar(0)]) + expect(PGF.showType([], type)).toEqual('(x : N) -> P x') + }) + + test('5', () => { + const type = mkType([mkDepHypo('f', mkType([mkHypo(mkType([], 'N', []))], 'N', []))], 'P', [new ExprApp(new ExprVar(0), new ExprFun('z'))]) + expect(PGF.showType([], type)).toEqual('(f : N -> N) -> P (f z)') + }) + + test('6', () => { + const type = mkType([mkDepHypo('f', mkType([mkHypo(mkType([], 'N', []))], 'N', []))], 'P', [new ExprApp(new ExprVar(0), new ExprVar(1))]) + expect(PGF.showType(['n'], type)).toEqual('(f : N -> N) -> P (f n)') + }) + + test('7', () => { + const type = mkType([mkImplHypo('f', mkType([mkHypo(mkType([], 'N', []))], 'N', []))], 'P', [new ExprApp(new ExprVar(0), new ExprVar(1))]) + expect(PGF.showType(['n'], type)).toEqual('({f} : N -> N) -> P (f n)') + }) + + test('8', () => { + const type = mkType([mkDepHypo('x', mkType([], 'N', [])), mkHypo(mkType([], 'P', [new ExprVar(0)]))], 'S', []) + expect(PGF.showType(['n'], type)).toEqual('(x : N) -> P x -> S') + }) + + test('9', () => { + const type = mkType([mkDepHypo('x', mkType([], 'N', [])), mkDepHypo('y', mkType([], 'P', [new ExprVar(0)]))], 'S', []) + expect(PGF.showType(['n'], type)).toEqual('(x : N) -> (y : P x) -> S') + }) }) })