Merge pull request #138 from Wasm-DSL/splice-modulesem

Resolved minor issues of prose spec diffs

spectec/src/al/print.ml

@@ -392,7 +392,7 @@ let rec structured_string_of_iter = function
 
 and structured_string_of_record_expr r =
   Record.fold
-    (fun a v acc -> acc ^ string_of_atom a ^ ": " ^ string_of_expr v ^ "; ")
+    (fun a v acc -> acc ^ string_of_atom a ^ ": " ^ structured_string_of_expr v ^ "; ")
     r "{ "
   ^ "}"
 

spectec/src/backend-interpreter/construct.ml

@@ -114,7 +114,7 @@ let rec al_to_storage_type: value -> storage_type = function
   | v -> ValStorageT (al_to_val_type v)
 
 and al_to_field_type: value -> field_type = function
-  | TupV [ mut; st ] -> FieldT (al_to_mut mut, al_to_storage_type st)
+  | CaseV (_, [ mut; st ]) -> FieldT (al_to_mut mut, al_to_storage_type st)
   | v -> error_value "field type" v
 
 and al_to_result_type: value -> result_type = function
@@ -210,11 +210,11 @@ let al_to_limits (default: int64): value -> limits = function
 
 
 let al_to_global_type: value -> global_type = function
-  | TupV [ mut; vt ] -> GlobalT (al_to_mut mut, al_to_val_type vt)
+  | TupV [ mut; vt ] | CaseV (_, [ mut; vt ]) -> GlobalT (al_to_mut mut, al_to_val_type vt)
   | v -> error_value "global type" v
 
 let al_to_table_type: value -> table_type = function
-  | TupV [ at; limits; rt ] -> TableT (al_to_addr_type at, al_to_limits default_table_max limits, al_to_ref_type rt)
+  | TupV [ at; limits; rt ] | CaseV (_, [ at; limits; rt ]) -> TableT (al_to_addr_type at, al_to_limits default_table_max limits, al_to_ref_type rt)
   | v -> error_value "table type" v
 
 let al_to_memory_type: value -> memory_type = function
@@ -1249,7 +1249,7 @@ let rec al_of_storage_type = function
   | PackStorageT _ as st -> nullary (string_of_storage_type st)
 
 and al_of_field_type = function
-  | FieldT (mut, st) -> tupV [ al_of_mut mut; al_of_storage_type st ]
+  | FieldT (mut, st) -> CaseV ("", [ al_of_mut mut; al_of_storage_type st ])
 
 and al_of_result_type rt = al_of_list al_of_val_type rt
 
@@ -1318,13 +1318,13 @@ let al_of_limits default limits =
   CaseV ("[", [ al_of_nat64 limits.min; max ]) (* TODO: Something better tan this is needed *)
 
 let al_of_global_type = function
-  | GlobalT (mut, vt) -> tupV [ al_of_mut mut; al_of_val_type vt ]
+  | GlobalT (mut, vt) -> CaseV ("", [ al_of_mut mut; al_of_val_type vt ])
 
 let al_of_table_type = function
   | TableT (at, limits, rt) ->
     match !version with
-    | 3 -> tupV [ al_of_addr_type at; al_of_limits default_table_max limits; al_of_ref_type rt ]
-    | _ -> tupV [                     al_of_limits default_table_max limits; al_of_ref_type rt ]
+    | 3 -> CaseV ("", [ al_of_addr_type at; al_of_limits default_table_max limits; al_of_ref_type rt ])
+    | _ -> CaseV ("", [                     al_of_limits default_table_max limits; al_of_ref_type rt ])
 
 let al_of_memory_type = function
   | MemoryT (at, limits) ->
@@ -2104,7 +2104,7 @@ let al_of_global global =
 
 let al_of_table table =
   match !version with
-  | 1 -> CaseV ("TABLE", [ al_of_table_type table.it.ttype |> arg_of_tup 0 ])
+  | 1 -> CaseV ("TABLE", [ al_of_table_type table.it.ttype |> arg_of_case "" 0 ])
   | 2 -> CaseV ("TABLE", [ al_of_table_type table.it.ttype ])
   | 3 -> CaseV ("TABLE", [ al_of_table_type table.it.ttype; al_of_const table.it.tinit ])
   | _ -> failwith "Unsupported version"

spectec/src/backend-prose/gen.ml

@@ -555,34 +555,6 @@ let postprocess_prose defs =
 let gen_validation_prose () =
   !Langs.validation_il |> prose_of_rels
 
-let get_state_arg_opt f =
-  let id = f $ no_region in
-  match Il.Env.find_opt_def (Il.Env.env_of_script !Langs.il) id with
-  | Some (params, _, _) ->
-    List.find_map (
-      fun param ->
-        match param.it with
-        | Il.Ast.ExpP (id, ({ it = VarT ({ it = "state"; _ }, _); _ } as typ)) ->
-          Some (Al.Ast.ExpA ((Al.Ast.VarE "z") $$ id.at % typ) $ no_region)
-        | _ -> None
-    ) params
-  | None -> 
-    None
-
-let get_store_arg_opt f =
-  let id = f $ no_region in
-  match Il.Env.find_opt_def (Il.Env.env_of_script !Langs.il) id with
-  | Some (params, _, _) ->
-    List.find_map (
-      fun param ->
-        match param.it with
-        | Il.Ast.ExpP (id, ({ it = VarT ({ it = "store"; _ }, _); _ } as typ)) ->
-          Some (Al.Ast.ExpA ((Al.Ast.VarE "s") $$ id.at % typ) $ no_region)
-        | _ -> None
-    ) params
-  | None -> 
-    None
-
 let insert_state_binding algo =
   let open Al.Ast in
   let z_binding = ref 0 in
@@ -625,71 +597,12 @@ let insert_state_binding algo =
   )
   else algo
 
-
-let recover_state algo =
-
-  let get_state_and_store_args name =
-    let args = [] in
-    let args = 
-      match get_state_arg_opt name with
-      | Some arg -> arg :: args
-      | _ -> args
-    in
-    let args = 
-      match get_store_arg_opt name with
-      | Some arg -> arg :: args
-      | _ -> args
-    in
-    args
-  in
-
-  let algo =
-    match algo.it with
-    | Al.Ast.RuleA _ -> algo
-    | Al.Ast.FuncA (name, args, instrs) ->
-      let args = get_state_and_store_args name @ args in
-      {algo with it = Al.Ast.FuncA (name, args, instrs)}
-  in
-
-  let recover_state_expr expr =
-    match expr.it with
-    | Al.Ast.CallE (f, args) ->
-      let args = get_state_and_store_args f @ args in
-      {expr with it = Al.Ast.CallE (f, args)}
-    | _ -> expr
-  in
-
-  let recover_state_instr instr =
-    match instr.it with
-    | Al.Ast.PerformI (f, args) ->
-      let args = get_state_and_store_args f @ args in
-      [{instr with it = Al.Ast.PerformI (f, args)}]
-    | _ -> [instr]
-  in
-
-  let walk_expr walker expr =
-    let expr1 = recover_state_expr expr in
-    Al.Walk.base_walker.walk_expr walker expr1
-  in
-  let walk_instr walker instr =
-    let instr1 = recover_state_instr instr in
-    List.concat_map (Al.Walk.base_walker.walk_instr walker) instr1
-  in
-  let walker = { Al.Walk.base_walker with
-    walk_expr = walk_expr;
-    walk_instr = walk_instr;
-  }
-  in
-  let algo' = walker.walk_algo walker algo in
-  algo'
-
 (** Entry for generating execution prose **)
 let gen_execution_prose () =
   List.map
     (fun algo ->
       let algo =
         algo
-        |> recover_state
         |> insert_state_binding
         |> Il2al.Transpile.remove_exit
         |> Il2al.Transpile.remove_enter

spectec/src/backend-prose/print.ml

@@ -234,13 +234,7 @@ let make_index depth =
   | _ -> assert false
 
 (* Prefix for stack push/pop operations *)
-let string_of_stack_prefix expr =
-  match expr.it with
-  | GetCurContextE _
-  | VarE ("F" | "L") -> ""
-  | _ when Il.Eq.eq_typ expr.note Al.Al_util.evalctxT -> "the evaluation context "
-  | IterE _ -> "the values "
-  | _ -> "the value "
+let string_of_stack_prefix = Prose_util.string_of_stack_prefix
 
 let rec string_of_instr' depth instr =
 

spectec/src/backend-prose/prose_util.ml

@@ -63,3 +63,17 @@ let apply_prose_hint hint args =
   let holes, template = split_prose_hint hint in
   let args = List.map (fun hole -> List.nth args (hole_to_int hole - 1)) holes in
   alternate template args |> String.concat ""
+
+let string_of_stack_prefix expr =
+  let open Al.Ast in
+  match expr.it with
+  | GetCurContextE _
+  | VarE ("F" | "L") -> ""
+  | _ when Il.Eq.eq_typ expr.note Al.Al_util.frameT -> "the :ref:`frame <syntax-frame>` "
+  | CaseE (mixop, _) when Il.Eq.eq_typ expr.note Al.Al_util.evalctxT ->
+    let evalctx_name = Xl.Mixop.name (List.nth mixop 0)
+    |> fun s -> String.sub s 0 (String.length s - 1)
+    |> String.lowercase_ascii in
+    Printf.sprintf "the :ref:`%s <syntax-%s>` " evalctx_name evalctx_name
+  | IterE _ -> "the values "
+  | _ -> "the value "

spectec/src/backend-prose/prose_util.mli

@@ -2,3 +2,4 @@ val find_relation : string -> El.Ast.def option
 val extract_desc : Il.Ast.typ -> string
 val alternate : 'a list -> 'a list -> 'a list
 val apply_prose_hint : string -> string list -> string
+val string_of_stack_prefix : Al.Ast.expr -> string