Merge pull request #89 from Wasm-DSL/prose-with-state

�Rule prose with state variable z

spectec/src/al/al_util.ml

@@ -58,6 +58,7 @@ let infixE ?(at = no) (e1, infix, e2) = InfixE (e1, infix, e2) |> mk_expr at
 let arityE ?(at = no) e = ArityE e |> mk_expr at
 let frameE ?(at = no) (e_opt, e) = FrameE (e_opt, e) |> mk_expr at
 let labelE ?(at = no) (e1, e2) = LabelE (e1, e2) |> mk_expr at
+let getCurStateE ?(at = no) () = GetCurStateE |> mk_expr at
 let getCurFrameE ?(at = no) () = GetCurFrameE |> mk_expr at
 let getCurLabelE ?(at = no) () = GetCurLabelE |> mk_expr at
 let getCurContextE ?(at = no) () = GetCurContextE |> mk_expr at

spectec/src/al/ast.ml

@@ -95,6 +95,7 @@ and expr' =
   | ArityE of expr                      (* "the arity of expr" *)
   | FrameE of expr option * expr        (* "the activation of expr (with arity expr)?" *)
   | LabelE of expr * expr               (* "the label whose arity is expr and whose continuation is expr" *)
+  | GetCurStateE                        (* "the current state" *)
   | GetCurFrameE                        (* "the current frame" *)
   | GetCurLabelE                        (* "the current lbael" *)
   | GetCurContextE                      (* "the current context" *)

spectec/src/al/eq.ml

@@ -55,6 +55,7 @@ let rec eq_expr e1 e2 =
   | LabelE (e11, e12), LabelE (e21, e22) ->
       eq_expr e11 e21 &&
       eq_expr e12 e22
+  | GetCurStateE, GetCurStateE
   | GetCurFrameE, GetCurFrameE
   | GetCurLabelE, GetCurLabelE
   | GetCurContextE, GetCurContextE -> true

spectec/src/al/free.ml

@@ -15,6 +15,7 @@ let rec free_expr expr =
   match expr.it with
   | NumE _
   | BoolE _
+  | GetCurStateE
   | GetCurLabelE
   | GetCurContextE
   | GetCurFrameE

spectec/src/al/print.ml

@@ -143,6 +143,7 @@ and string_of_expr expr =
     sprintf "%s ++ %s" (string_of_expr e1) (string_of_expr e2)
   | LenE e -> sprintf "|%s|" (string_of_expr e)
   | ArityE e -> sprintf "the arity of %s" (string_of_expr e)
+  | GetCurStateE -> "the current state"
   | GetCurLabelE -> "the current label"
   | GetCurFrameE -> "the current frame"
   | GetCurContextE -> "the current context"
@@ -418,6 +419,7 @@ and structured_string_of_expr expr =
     ^ ")"
   | LenE e -> "LenE (" ^ structured_string_of_expr e ^ ")"
   | ArityE e -> "ArityE (" ^ structured_string_of_expr e ^ ")"
+  | GetCurStateE -> "GetCurStateE"
   | GetCurLabelE -> "GetCurLabelE"
   | GetCurFrameE -> "GetCurFrameE"
   | GetCurContextE -> "GetCurContextE"

spectec/src/al/walk.ml

@@ -34,6 +34,7 @@ let rec walk_expr f e =
       match e.it with
       | NumE _
       | BoolE _
+      | GetCurStateE
       | GetCurFrameE
       | GetCurLabelE
       | GetCurContextE -> e.it

spectec/src/backend-interpreter/ds.ml

@@ -331,6 +331,8 @@ end
 (* Initialization *)
 
 let init algos =
+  let algos = List.map Il2al.Transpile.remove_state algos in
+
   (* Initialize info_map *)
   let init_info algo =
     let algo_name = name_of_algo algo in

spectec/src/backend-interpreter/dune

@@ -1,6 +1,6 @@
 (library
   (name backend_interpreter)
-  (libraries reference_interpreter util il el str middlend al)
+  (libraries reference_interpreter util str el il middlend il2al al)
   (modules
     interpreter
     numerics

spectec/src/backend-interpreter/manual.ml

@@ -1,235 +1,6 @@
 open Al
 open Ast
 open Al_util
-open Util
-
-type config = expr * expr * instr list
-
-let atom_of_name name typ = Il.Atom.Atom name, typ
-
-let eval_expr =
-  let instrs = iterE (varE "instr", ["instr"], List) in
-  let result = varE "val" in
-
-  FuncA (
-    "eval_expr",
-    [instrs],
-    [
-      executeseqI instrs;
-      popI result;
-      returnI (Some (listE [ result ]))
-    ]
-  )
-
-(*
-execution_of_CALL_REF ?(x)
-1. Assert: Due to validation, a value is on the top of the stack.
-2. Pop u_0 from the stack.
-3. If u_0 is of the case REF.NULL, then:
-  a. Trap.
-4. Assert: u_0 is of the case REF.FUNC_ADDR;
-4. Let (REF.FUNC_ADDR a) be u_0.
-5. If a < |$funcinst()|, then:
-  a. Let fi be $funcinst()[a].
-  b. Assert: fi.CODE is of the case FUNC;
-  1) Let (FUNC x' y_1 instr* ) be fi.CODE.
-  2) Let (LOCAL t)* be y_1.
-  3) Assert: $expanddt(fi.TYPE) is of the case FUNC;
-  a) Let (FUNC y_0) be $expanddt(fi.TYPE).
-  b) Let [t_1^n]->[t_2^m] be y_0.
-  c) Assert: Due to validation, there are at least n values on the top of the stack.
-  d) Pop val^n from the stack.
-  e) Let f be { LOCAL: ?(val)^n ++ $default_(t)*; MODULE: fi.MODULE; }.
-  f) Let F be the activation of f with arity m.
-  g) Enter F with label [FRAME_]:
-    1. Let L be the label_m{[]}.
-    2. Enter L with label instr* ++ [LABEL_]:
-
-*)
-
-let call_ref =
-  (* names *)
-  let x = varE "x" in
-  let ref = varE "ref" in
-  let a = varE "a" in
-  let fi = varE "fi" in
-  let y0 = varE "y_0" in
-  let y1 = varE "y_1" in
-  let t = varE "t" in
-  let t1 = varE "t_1" in
-  let t2 = varE "t_2" in
-  let n = varE "n" in
-  let m = varE "m" in
-  let v = varE "val" in
-  let f = varE "f" in
-  let ff = varE "F" in
-  let ll = varE "L" in
-  let instr = varE "instr" in
-
-  RuleA (
-    atom_of_name "CALL_REF" "admininstr",
-    [ x ],
-    [
-      assertI (topValueE None);
-      popI ref;
-      ifI (
-        isCaseOfE (ref, atom_of_name "REF.NULL" "admininstr"),
-        [ trapI () ],
-        []
-      );
-      assertI (isCaseOfE (ref, atom_of_name "REF.FUNC_ADDR" "admininstr"));
-      letI (caseE (atom_of_name "REF.FUNC_ADDR" "admininstr", [a]), ref);
-      ifI (
-        binE (LtOp, a, lenE (callE ("funcinst", []))),
-        [ letI (fi, accE (callE ("funcinst", []), idxP a));
-          assertI (isCaseOfE (accE (fi, dotP (atom_of_name "CODE" "code")), atom_of_name "FUNC" "func"));
-          letI (caseE (atom_of_name "FUNC" "func", [y0 ; y1 ; iterE (instr, ["instr"], List)]), accE (fi, dotP (atom_of_name "CODE" "code")));
-          letI (iterE (caseE (atom_of_name "LOCAL" "local", [t]), ["t"], List), y1);
-          assertI (isCaseOfE (callE ("expanddt", [ accE (fi, dotP (atom_of_name "TYPE" "type")) ]), atom_of_name "FUNC" "comptype"));
-          letI (caseE (atom_of_name "FUNC" "comptype", [y0]), callE ("expanddt", [ accE (fi, dotP (atom_of_name "TYPE" "type")) ]));
-          letI (infixE (iterE (t1, ["t_1"], ListN (n, None)), (Il.Atom.Arrow, ""), iterE (t2, ["t_2"], ListN (m, None))), y0);
-          assertI (topValuesE n);
-          popI (iterE (v, ["val"], ListN(n, None)));
-          letI (f, strE (Record.empty
-            |> Record.add
-              (atom_of_name "LOCALS" "frame")
-              (catE (iterE (optE (Some v), ["val"], ListN (n, None)), iterE (callE("default_", [t]), ["t"], List)))
-            |> Record.add
-              (atom_of_name "MODULE" "frame")
-              (accE (fi, dotP (atom_of_name "MODULE" "module")))
-          ));
-          letI (ff, frameE (Some m, f));
-          enterI (ff, listE ([caseE (atom_of_name "FRAME_" "admininstr", [])]),
-            [
-            letI (ll, labelE (m, listE []));
-            enterI (ll, catE (iterE (instr, ["instr"], List), listE ([caseE (atom_of_name "LABEL_" "admininstr", [])])), []);
-            ]
-          );
-        ], []);
-      ]
-    )
-
-(* Helper for the manual array_new.data algorithm *)
-
-let group_bytes_by =
-  let n = varE "n" in
-  let n' = varE "n'" in
-
-  let bytes_ = iterE (varE "byte", ["byte"], List) in
-  let bytes_left = listE [accE (bytes_, sliceP (numE Z.zero, n))] in
-  let bytes_right = callE
-    (
-      "group_bytes_by",
-      [ n; accE (bytes_, sliceP (n, binE (SubOp, n', n))) ]
-    )
-  in
-
-  FuncA (
-    "group_bytes_by",
-    [n; bytes_],
-    [
-      letI (n', lenE bytes_);
-      ifI (
-        binE (GeOp, n', n),
-        [ returnI (Some (catE (bytes_left, bytes_right))) ],
-        []
-      );
-      returnI (Some (listE []));
-    ]
-  )
-
-let array_new_data =
-  let i32 = caseE (atom_of_name "I32" "numtype", []) in
-
-  let x = varE "x" in
-  let y = varE "y" in
-
-  let n = varE "n" in
-  let i = varE "i" in
-
-  let y_0 = varE "y_0" in
-  let mut = varE "mut" in
-  let zt = varE "zt" in
-
-  let cnn = varE "cnn" in
-
-  let c = varE "c" in
-
-  let bstar = iterE (varE "b", ["b"], List) in
-  let gb = varE "gb" in
-  let gbstar = iterE (gb, ["gb"], List) in
-  let cn = iterE (c, ["c"], ListN (n, None)) in
-
-  let expanddt_with_type = callE ("expanddt", [callE ("type", [x])]) in
-  let zsize = callE ("zsize", [zt]) in
-  let cunpack = callE ("cunpack", [zt]) in
-  (* include z or not ??? *)
-  let data = callE ("data", [y]) in
-  let group_bytes_by = callE ("group_bytes_by", [binE (DivOp, zsize, numE (Z.of_int 8)); bstar]) in
-  let inverse_of_bytes_ = iterE (callE ("inverse_of_ibytes", [zsize; gb]), ["gb"], List) in
-
-  RuleA (
-    atom_of_name "ARRAY.NEW_DATA" "admininstr",
-    [x; y],
-    [
-      assertI (topValueE (Some i32));
-      popI (caseE (atom_of_name "CONST" "admininstr", [i32; n]));
-      assertI (topValueE (Some i32));
-      popI (caseE (atom_of_name "CONST" "admininstr", [i32; i]));
-      ifI (
-        isCaseOfE (expanddt_with_type, atom_of_name "ARRAY" "comptype"),
-        [
-          letI (caseE (atom_of_name "ARRAY" "comptype", [y_0]), expanddt_with_type);
-          letI (tupE [ mut; zt ], y_0);
-          ifI (
-            binE (
-              GtOp,
-              binE (AddOp, i, binE (DivOp, binE (MulOp, n, zsize), numE (Z.of_int 8))),
-              lenE (accE (callE ("data", [y]), dotP (atom_of_name "BYTES" "datainst")))
-            ),
-            [ trapI () ],
-            []
-          );
-          letI (cnn, cunpack);
-          letI (
-            bstar,
-            accE (
-              accE (data, dotP (atom_of_name "BYTES" "datainst")),
-              sliceP (i, binE (DivOp, binE (MulOp, n, zsize), numE (Z.of_int 8)))
-            )
-          );
-          letI (gbstar, group_bytes_by);
-          letI (cn, inverse_of_bytes_);
-          pushI (iterE (caseE (atom_of_name "CONST" "admininstr", [cnn; c]), ["c"], ListN (n, None)));
-          executeI (caseE (atom_of_name "ARRAY.NEW_FIXED" "admininstr", [x; n]));
-        ],
-        []
-      );
-    ]
-  )
-
-let manual_algos = [eval_expr; call_ref; group_bytes_by; array_new_data;]
-
-let return_instrs_of_instantiate config =
-  let store, frame, rhs = config in
-  [
-    enterI (
-      frameE (Some (numE Z.zero), frame),
-      listE ([ caseE (atom_of_name "FRAME_" "admininstr", []) ]), rhs
-    );
-    returnI (Some (tupE [ store; varE "mm" ]))
-  ]
-let return_instrs_of_invoke config =
-  let _, frame, rhs = config in
-  [
-    letI (varE "k", lenE (iterE (varE "t_2", ["t_2"], List)));
-    enterI (
-      frameE (Some (varE "k"), frame),
-      listE ([caseE (atom_of_name "FRAME_" "admininstr", [])]), rhs
-    );
-    popI (iterE (varE "val", ["val"], ListN (varE "k", None)));
-    returnI (Some (iterE (varE "val", ["val"], ListN (varE "k", None))))
-  ]
 
 let ref_type_of =
   (* TODO: some / none *)

spectec/src/backend-interpreter/manual.mli

@@ -1,8 +1,3 @@
 open Al.Ast
 
-type config = expr * expr * instr list
-
-val manual_algos : algorithm list
-val return_instrs_of_instantiate : config -> instr list
-val return_instrs_of_invoke : config -> instr list
 val ref_type_of : value list -> value

spectec/src/backend-prose/dune

@@ -1,6 +1,6 @@
 (library
   (name backend_prose)
-  (libraries util el il backend_interpreter backend_latex il2al)
+  (libraries util el il il2al backend_latex backend_interpreter)
   (modules
     config
     prose

spectec/src/backend-prose/gen.ml

@@ -141,7 +141,14 @@ let gen_validation_prose il =
   |> List.map vrule_group_to_prose
 
 (** Entry for generating execution prose **)
-let gen_execution_prose = List.map (fun algo -> Prose.Algo algo)
+let gen_execution_prose =
+  List.map
+    (fun algo ->
+      let algo = match algo with
+      | Al.Ast.RuleA _ -> Il2al.Transpile.insert_state_binding algo
+      | Al.Ast.FuncA _ -> Il2al.Transpile.remove_state algo
+      in
+      Prose.Algo algo)
 
 (** Main entry for generating prose **)
 let gen_prose il al =

spectec/src/backend-prose/render.ml

@@ -163,7 +163,9 @@ and al_to_el_expr expr =
       let ela = al_to_el_atom a in
       let ela = (El.Ast.AtomE ela) $ no_region in
       let* elel = al_to_el_exprs el in
-      Some (El.Ast.SeqE ([ ela ] @ elel))
+      let ele = El.Ast.SeqE ([ ela ] @ elel) in
+      if List.length elel = 0 then Some ele
+      else Some (El.Ast.ParenE (ele $ no_region, false))
     | Al.Ast.OptE (Some e) ->
       let* ele = al_to_el_expr e in
       Some (ele.it)
@@ -270,13 +272,15 @@ let render_atom env a =
 
 (* Category 1 is translated to EL then rendered by the Latex backend *)
 
+let render_el_exp env exp =
+  (* embedded math blocks cannot have line-breaks *)
+  let newline = Str.regexp "\n" in
+  let sexp = Backend_latex.Render.render_exp env.render_latex exp in
+  let sexp = Str.global_replace newline "" sexp in
+  render_math sexp
+
 let rec render_expr env expr = match al_to_el_expr expr with
-  | Some exp ->
-    (* embedded math blocks cannot have line-breaks *)
-    let newline = Str.regexp "\n" in
-    let sexp = Backend_latex.Render.render_exp env.render_latex exp in
-    let sexp = Str.global_replace newline "" sexp in
-    render_math sexp
+  | Some exp -> render_el_exp env exp
   | None -> render_expr' env expr
 
 (* Categories 2 and 3 are rendered by the prose backend,
@@ -329,6 +333,7 @@ and render_expr' env expr =
   | Al.Ast.ArityE e ->
     let se = render_expr env e in
     sprintf "the arity of %s" se
+  | Al.Ast.GetCurStateE -> "the current state"
   | Al.Ast.GetCurLabelE -> "the current label"
   | Al.Ast.GetCurFrameE -> "the current frame"
   | Al.Ast.GetCurContextE -> "the current context"
@@ -567,7 +572,11 @@ let render_atom_title env name params =
     | _ -> name'
   in
   let name = (name', typ) in
-  render_expr env (Al.Ast.CaseE (name, params) $ no_region)
+  let expr = Al.Ast.CaseE (name, params) $ no_region in
+  match al_to_el_expr expr with
+  | Some ({ it = El.Ast.ParenE (exp, _); _ }) -> render_el_exp env exp
+  | Some exp -> render_el_exp env exp
+  | None -> render_expr' env expr
 
 let render_funcname_title env fname params =
   render_expr env (Al.Ast.CallE (fname, params) $ no_region)