diff --git a/runtimes/assemblyscript/assembly/index.ts b/runtimes/assemblyscript/assembly/index.ts index fb265246..3ed47a92 100644 --- a/runtimes/assemblyscript/assembly/index.ts +++ b/runtimes/assemblyscript/assembly/index.ts @@ -561,24 +561,65 @@ export function runtimeEqual(a: EjValue, b: EjValue): EjBool { return c_false; } -function compare(a: T, b: T): EjNumber { - if (a < b) { return c_1; } - if (a > b) { return c_neg1; } - return c_0; -} - -export function runtimeCompare(a: EjValue, b: EjValue): EjNumber { +// This is actually a compare negative. +// We call it compare to be compatible with the coq-extracted code +// https://github.com/querycert/qcert/issues/144 +function compare_base(a: T, b: T): i32 { + if (a < b) { return 1 ; } + if (a > b) { return -1 ; } + return 0; +} + +function type_id(a: EjValue): u32 { + if( a instanceof EjNull ) { return idof(); } + if( a instanceof EjBool ) { return idof(); } + if( a instanceof EjNumber ) { return idof(); } + if( a instanceof EjBigInt ) { return idof(); } + if( a instanceof EjString ) { return idof(); } + if( a instanceof EjArray ) { return idof(); } + if( a instanceof EjObject ) { return idof(); } + throw new Error('type_id: unknown type'); +} + +// This is actually a compare negative. +// We call it compare to be compatible with the coq-extracted code +// https://github.com/querycert/qcert/issues/144 +function compare(a: EjValue, b: EjValue): i32 { + if (a instanceof EjNull && b instanceof EjNull) { + return 0; + } + if (a instanceof EjBool && b instanceof EjBool) { + let aa : EjBool = changetype(a) ; + let bb : EjBool = changetype(b) ; + return compare_base(aa.value, bb.value); + } if (a instanceof EjNumber && b instanceof EjNumber) { let aa : EjNumber = changetype(a) ; let bb : EjNumber = changetype(b) ; - return compare(aa.value, bb.value); + return compare_base(aa.value, bb.value); } if (a instanceof EjBigInt && b instanceof EjBigInt) { let aa : EjBigInt = changetype(a) ; let bb : EjBigInt = changetype(b) ; - return compare(aa.value, bb.value); + return compare_base(aa.value, bb.value); + } + if (a instanceof EjString && b instanceof EjString) { + throw new Error("compare: does not support String"); } - throw new Error('runtimeCompare: invalid arguments'); + if (a instanceof EjArray && b instanceof EjArray) { + throw new Error("compare: does not support Array"); + } + if (a instanceof EjObject && b instanceof EjObject) { + throw new Error("compare: does not support Object"); + } + return compare_base(type_id(a), type_id(b)); +} + +export function runtimeCompare(a: EjValue, b: EjValue): EjNumber { + let c = compare(a, b); + if (c < 0) { return c_neg1; } + if (c > 0) { return c_1; } + return c_0; } function ejValueToString(a: EjValue): string { @@ -873,6 +914,7 @@ export function runtimeFlatten(a: EjArray) : EjArray { return new EjArray(result); } +// List concatenation / SQL Union export function runtimeUnion(a: EjArray, b: EjArray) : EjArray { return new EjArray(a.values.concat(b.values)); } @@ -898,12 +940,49 @@ export function runtimeMinus(a: EjArray, b: EjArray) : EjArray { return new EjArray(result); } +// set intersection export function runtimeMin(a: EjArray, b: EjArray) : EjArray { - throw new Error('runtimeMin: not implemented'); + let av = a.values.slice(); + let bv = b.values.slice(); + av.sort(compare); + bv.sort(compare); + let ai = 0; + let bi = 0; + let result = new Array(); + while (ai < av.length && bi < bv.length) { + let c = compare(av[ai], bv[bi]); + if (c > 0) { bi++; } + else if (c < 0) { ai++; } + else { + result.push(av[ai++]); + } + } + return new EjArray(result); } +// set union export function runtimeMax(a: EjArray, b: EjArray) : EjArray { - throw new Error('runtimeMax: not implemented'); + let av = a.values.slice(); + let bv = b.values.slice(); + av.sort(compare); + bv.sort(compare); + let ai = 0; + let bi = 0; + let result = new Array(); + while (ai < av.length && bi < bv.length) { + let c = compare(av[ai], bv[bi]); + if (c > 0) { + result.push(bv[bi++]); + } else if (c < 0) { + result.push(av[ai++]); + } else { + result.push(av[ai++]); + bi++; + } + } + while (ai < av.length) { result.push(av[ai++]); } + while (bi < bv.length) { result.push(bv[bi++]); } + return new EjArray(result); } export function runtimeNth(a: EjArray, b: EjBigInt) : EjObject { diff --git a/runtimes/assemblyscript/runtime.wasm b/runtimes/assemblyscript/runtime.wasm index 270fdaba..703f1234 100644 Binary files a/runtimes/assemblyscript/runtime.wasm and b/runtimes/assemblyscript/runtime.wasm differ diff --git a/tests/operators/main.ml b/tests/operators/main.ml index e629d817..86343efd 100644 --- a/tests/operators/main.ml +++ b/tests/operators/main.ml @@ -50,7 +50,7 @@ let ejson_eq = let failed = ref false -let test_fn ?(verbose=false) info env fn = +let test_fn ?(fixup=fun x -> x) ?(verbose=false) info env fn = let imp_ejson : _ imp_ejson = [['f'], fn] in let fail message = print_endline ""; @@ -63,7 +63,7 @@ let test_fn ?(verbose=false) info env fn = | None, _ -> fail "imp eval failed" | Some _, None -> fail "wasm eval failed" | Some imp, Some wasm -> - if (not (ejson_eq wasm imp)) then ( + if (not (ejson_eq (fixup wasm) (fixup imp))) then ( fail "wasm and imp differ"; print_string ("imp: "); print_endline (ejson_to_string imp); @@ -76,7 +76,7 @@ let test_fn ?(verbose=false) info env fn = print_endline (ejson_to_string imp) ) -let test_expr_1 ?verbose info expr op args = +let test_expr_1 ?fixup ?verbose info expr op args = let varname i = Util.char_list_of_string ("arg" ^ (string_of_int i)) and info () = info (); @@ -97,10 +97,10 @@ let test_expr_1 ?verbose info expr op args = let stmt = ImpStmtAssign(return, expr op args) in - test_fn ?verbose info env (ImpFun (['x'], stmt, return)) + test_fn ?fixup ?verbose info env (ImpFun (['x'], stmt, return)) -let test_expr ?verbose info expr op args = - List.iter (fun args -> test_expr_1 ?verbose info expr op args) args +let test_expr ?fixup ?verbose info expr op args = + List.iter (fun args -> test_expr_1 ?fixup ?verbose info expr op args) args let test_op ?verbose op = test_expr ?verbose @@ -111,8 +111,8 @@ let test_op ?verbose op = (fun op args -> ImpExprOp (op, args)) op -let test_rtop ?verbose op = - test_expr ?verbose +let test_rtop ?fixup ?verbose op = + test_expr ?fixup ?verbose (fun () -> print_string "operator: "; print_endline (Wasm_backend.string_of_runtime_operator op); @@ -383,14 +383,14 @@ let _ = ; [ arr [] ] ]; test_rtop - EJsonRuntimeUnion + EJsonRuntimeUnion (* Array Concatenation *) [ [ arr [null]; arr [null; bool true] ] ; [ arr []; arr [null] ] ; [ arr [null]; arr [] ] ; [ arr []; arr [] ] ]; test_rtop - EJsonRuntimeMinus + EJsonRuntimeMinus (* Set Minus *) [ [ arr [null]; arr [null; bool true] ] ; [ arr [bool true; bool false]; arr [bool true; bool false] ] ; [ arr [bool true; bool false]; arr [bool true] ] @@ -400,6 +400,36 @@ let _ = ; [ arr [null]; arr [] ] ; [ arr []; arr [] ] ]; + let sort_array (x : _ ejson) = + match x with + | Coq_ejarray z -> Coq_ejarray (List.sort compare z) + | z -> z + in + (* ImpEJson eval does not sort the arrays. + * JS runtime and WASM runtime do sort the arrays. *) + test_rtop ~fixup:sort_array + EJsonRuntimeMin (* Set Intersection *) + [ [arr []; arr []] + ; [arr [bool true]; arr [bool true]] + ; [arr [bool true]; arr [bool false]] + ; [arr [bool false]; arr [bool true]] + ; [arr [bool true]; arr [bool true; bool false]] + ; [arr [bool true; bool false]; arr [bool true; null]] + ; [arr [int 1; int 2]; arr [int 1; int 2]] + ]; + (* ImpEJson eval does not sort the arrays. + * JS runtime and WASM runtime do sort the arrays. *) + test_rtop ~fixup:sort_array + EJsonRuntimeMax (* Set Union *) + [ [arr []; arr []] + ; [arr [bool true]; arr [bool true]] + ; [arr [bool true]; arr [bool false]] + ; [arr [bool false]; arr [bool true]] + ; [arr [bool true]; arr [bool true; bool false]] + ; [arr [bool true; bool false]; arr [bool true]] + ; [arr [bool true; bool false]; arr [bool true; null]] + ; [arr [int 3; int 2; int 1]; arr [int 6; int 2; int 1; int 0]] + ]; test_rtop EJsonRuntimeNth [ [ arr [bool true]; int 0 ]