{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Wasm Spec Kernel\n",
    "\n",
    "This is an example notebook demonstrating some of the features in the Wasm Spec Kernel. The kernel is barebones, it's a simple wrapper around the REPL provided by the Wasm reference interpreter. All commands are run directly in that REPL, as though they were typed in to it directly.\n",
    "\n",
    "### Hanging Execution\n",
    "\n",
    "Incomplete code will cause the REPL to hang, such as `(module $incomplete` (notice the lack of a closing parenthesis). You can kill hanging executions by hitting stop or interrupt, which will cause the entire REPL process to be rebooted.\n",
    "\n",
    "### Example Module\n",
    "\n",
    "This notebook includes a simple Wasm module, `$lib_math`, implementing a recursive fibonacci algorithm, which is exported as `$fibonacci_rec`. It then triggers this exported function to calculate the 10th number in the fibonacci sequence.\n",
    "\n",
    "### Example Errors\n",
    "\n",
    "Finally, invalid Wasm code is provided to showcase what an error looks like. Notice that the line numbers (e.g. `stdin:8.19-8.35`) do not correspond to the line numbers in the code sample. Instead, they correspond to the cumulative line numbers received by the REPL. The kernel does not attempt to translate these values and instead passes information directly to and from the REPL, as provided."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "module $lib_math :\r\n",
      "  export func \"fibonacci_rec\" : [i32] -> [i32]"
     ]
    }
   ],
   "source": [
    "(module $lib_math\n",
    "    (func $fib_rec (export \"fibonacci_rec\") (param $n i32) (result i32)\n",
    "        (if (result i32) (i32.lt_s (local.get $n) (i32.const 2))\n",
    "            (then (local.get $n))\n",
    "            (else (i32.add (call $fib_rec (i32.sub (local.get $n) (i32.const 1)))\n",
    "                           (call $fib_rec (i32.sub (local.get $n) (i32.const 2))))))))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "55 : i32"
     ]
    }
   ],
   "source": [
    "(invoke $lib_math \"fibonacci_rec\" (i32.const 10))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "ename": "syntax error",
     "evalue": "unknown operator",
     "output_type": "error",
     "traceback": [
      "stdin:8.19-8.35: syntax error: unknown operator"
     ]
    }
   ],
   "source": [
    "(module $invalid (not_an_operation))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Appendix\n",
    "\n",
    "### Sample: Wasm + Abstract Types\n",
    "\n",
    "[@awendland](https://github.com/awendland) originally created this kernel to share code samples leveraging an extension of the WebAssembly language that included abstract types (see [awendland/webassembly-spec-abstypes](https://github.com/awendland/webassembly-spec-abstypes). This kernel supports any build of the [WebAssembly reference interpreter](https://github.com/WebAssembly/spec/tree/master/interpreter), but this particular notebook environment has been configured to use a build with the abstypes extension.\n",
    "\n",
    "Here's an example with abstypes. First, pseudo-source OCaml that theoretically could have produced the following Wasm:\n",
    "\n",
    "```ocaml\n",
    "(* lib.ml *)\n",
    "module Date = sig\n",
    "  type date (* public, abstract type *)\n",
    "end =\n",
    "struct\n",
    "  type date = {day : int;  month : int;  year : int} (* private, concrete type *)\n",
    "  val create : ?days:int -> ?months:int -> ?years:int -> unit -> date\n",
    "  val yearsBetweenDates : date -> date -> int\n",
    "  val month : date -> int\n",
    "  ...\n",
    "end\n",
    "\n",
    "(* consumer.ml *)\n",
    "let kjohnson_bday : Date.date = Date.create 8 26 1918 () in\n",
    "let mercury_launch : Date.date = Date.create 2 20 1962 () in\n",
    "let kj_age_at_launch = Date.yearsBetweenDates kjohnson_bday mercury_launch in ...\n",
    "(* kjognson_bday.day <- this access is invalid *)\n",
    "```\n",
    "\n",
    "Next, a WebAssembly implementation that leverages abstract types to enforce the same invariants:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "module $lib_date :\r\n",
      "  export func \"createDate\" : [i32 i32 i32] -> [abs{0}]\r\n",
      "  export func \"yearsBetweenDates\" : [abs{0} abs{0}] -> [i32]\r\n",
      "  export abstype \"Date\" : abs{0}\n",
      "module $main :\r\n",
      "  import abstype \"lib_date\" \"Date\" : abs{'Date','lib_date'}\r\n",
      "  import func \"lib_date\" \"createDate\" : [i32 i32 i32] -> [abs{'Date','lib_date'}]\r\n",
      "  import func \"lib_date\" \"yearsBetweenDates\" : [abs{'Date','lib_date'} abs{'Date','lib_date'}] -> [i32]\r\n",
      "  export func \"main\" : [] -> [i32]\n",
      "43 : i32"
     ]
    }
   ],
   "source": [
    ";; ======\n",
    ";; Demo 2.2 - example date library\n",
    ";;\n",
    ";; Reference: Section 3.2 in the thesis (and also Section 3.4)\n",
    ";; Dependencies: Core WebAssembly + abstract types (https://github.com/awendland/webassembly-spec-abstypes)\n",
    ";;\n",
    ";; NOTE: This sample is a poor implementation for a date library because it incorrectly assumes that 1 year is always 31,557,600,000 milliseconds. Do not use it.\n",
    ";; ======\n",
    "\n",
    "(module $lib_date\n",
    "  (abstype_new $Date i32)\n",
    "  (func (export \"createDate\")\n",
    "    (param $day i32) (param $month i32) (param $year i32)\n",
    "    (result (abstype_new_ref $Date))\n",
    "    (i32.add ;; Day, Mon, Year -> Unix milliseconds\n",
    "      (i32.mul (local.get $day) (i32.const 86400))\n",
    "      (i32.add\n",
    "        (i32.mul (local.get $month) (i32.const 2592000))\n",
    "        (i32.mul (i32.const 31557600)\n",
    "          (i32.sub (local.get $year) (i32.const 1970)))))\n",
    "  )\n",
    "  (func (export \"yearsBetweenDates\") (param (abstype_new_ref $Date))\n",
    "    (param (abstype_new_ref $Date)) (result i32)\n",
    "    (i32.sub (local.get 0) (local.get 1))\n",
    "    (i32.div_s (i32.const 31557600))\n",
    "  )\n",
    "  (export \"Date\" (abstype_new_ref $Date))\n",
    ")\n",
    "(register \"lib_date\" $lib_date)\n",
    "\n",
    "(module $main\n",
    "  (import \"lib_date\" \"Date\" (abstype_sealed $Date))\n",
    "  (import \"lib_date\" \"createDate\" (func $createDate\n",
    "    (param i32) (param i32) (param i32)\n",
    "    (result (abstype_sealed_ref $Date))))\n",
    "  (import \"lib_date\" \"yearsBetweenDates\" (func $yearsBetweenDates\n",
    "    (param (abstype_sealed_ref $Date))\n",
    "    (param (abstype_sealed_ref $Date)) (result i32)))\n",
    "  (func (export \"main\") (result i32)\n",
    "    (call $createDate\n",
    "      (i32.const 2) (i32.const 20) (i32.const 1962))\n",
    "    (call $createDate\n",
    "      (i32.const 8) (i32.const 26) (i32.const 1918))\n",
    "    (call $yearsBetweenDates)\n",
    "  )\n",
    ")\n",
    "(invoke $main \"main\")"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "WebAssembly Reference Interpreter",
   "language": "wat",
   "name": "wasm_spec"
  },
  "language_info": {
   "codemirror_mode": "commonlisp",
   "file_extension": ".wat",
   "mimetype": "text/x-common-lisp",
   "name": "wasm_spec"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}