Rework elaboration (#136)

spectec/doc/Language.md

@@ -133,6 +133,7 @@ exp ::=
   "eps"                                empty sequence
   exp exp                              sequencing
   exp iter                             iteration
+  "[" exp* "]"                         list
   exp "[" arith "]"                    list indexing
   exp "[" arith ":" arith "]"          list slicing
   exp "[" path "=" exp "]"             list update

spectec/spec/wasm-2.0/8-reduction.watsup

@@ -307,7 +307,7 @@ rule Step_pure/vswizzle:
 rule Step_pure/vshuffle:
   (VCONST V128 c_1) (VCONST V128 c_2) (VSHUFFLE (Pnn X N) i*) ~> (VCONST V128 c)
   -- var c' : iN($lsize(Pnn))
-  -- if c'* = $lanes_(Pnn X N, c_1) $lanes_(Pnn X N, c_2)
+  -- if c'* = $lanes_(Pnn X N, c_1) ++ $lanes_(Pnn X N, c_2)
   -- if c = $invlanes_(Pnn X N, c'*[$(i*[k])]^(k<N))
 
 
@@ -365,7 +365,7 @@ rule Step_pure/vcvtop-half:
 rule Step_pure/vcvtop-zero:
   (VCONST V128 c_1) (VCVTOP (nt_2 X M_2) (nt_1 X M_1) vcvtop eps zero) ~> (VCONST V128 c)
   -- if ci* = $lanes_(nt_1 X M_1, c_1)
-  -- if cj** = $setproduct_(lane_(nt_2), ($vcvtop__(nt_1 X M_1, nt_2 X M_2, vcvtop, ci)* ++ $zero(nt_2)^M_1))
+  -- if cj** = $setproduct_(lane_(nt_2), ($vcvtop__(nt_1 X M_1, nt_2 X M_2, vcvtop, ci)* ++ [$zero(nt_2)]^M_1))
   -- if c <- $invlanes_(nt_2 X M_2, cj*)*
 
 

spectec/spec/wasm-3.0/0-aux.watsup

@@ -32,11 +32,6 @@ def $opt_(syntax X, X*) : X?  hint(show %2)
 def $opt_(syntax X, eps) = eps
 def $opt_(syntax X, w) = w
 
-;; TODO(3, rossberg): this function should not be needed
-def $list_(syntax X, X?) : X*  hint(show %2)
-def $list_(syntax X, eps) = eps
-def $list_(syntax X, w) = w
-
 def $concat_(syntax X, (X*)*) : X*  hint(show (++) %2)
 def $concat_(syntax X, eps) = eps
 def $concat_(syntax X, (w*) (w'*)*) = w* ++ $concat_(X, (w'*)*)

spectec/spec/wasm-3.0/4-numerics.watsup

@@ -324,8 +324,8 @@ def $unop_(Fnn, NEAREST, f) = $fnearest_($sizenn(Fnn), f)
 def $binop_(Inn, ADD, i_1, i_2) = $iadd_($sizenn(Inn), i_1, i_2)
 def $binop_(Inn, SUB, i_1, i_2) = $isub_($sizenn(Inn), i_1, i_2)
 def $binop_(Inn, MUL, i_1, i_2) = $imul_($sizenn(Inn), i_1, i_2)
-def $binop_(Inn, DIV sx, i_1, i_2) = $list_(num_(Inn), $idiv_($sizenn(Inn), sx, i_1, i_2))
-def $binop_(Inn, REM sx, i_1, i_2) = $list_(num_(Inn), $irem_($sizenn(Inn), sx, i_1, i_2))
+def $binop_(Inn, DIV sx, i_1, i_2) = $idiv_($sizenn(Inn), sx, i_1, i_2)
+def $binop_(Inn, REM sx, i_1, i_2) = $irem_($sizenn(Inn), sx, i_1, i_2)
 def $binop_(Inn, AND, i_1, i_2) = $iand_($sizenn(Inn), i_1, i_2)
 def $binop_(Inn, OR, i_1, i_2) = $ior_($sizenn(Inn), i_1, i_2)
 def $binop_(Inn, XOR, i_1, i_2) = $ixor_($sizenn(Inn), i_1, i_2)
@@ -363,9 +363,9 @@ def $cvtop__(Inn_1, Inn_2, EXTEND sx, i_1) =
 def $cvtop__(Inn_1, Inn_2, WRAP, i_1) =
   $wrap__($sizenn1(Inn_1), $sizenn2(Inn_2), i_1)
 def $cvtop__(Fnn_1, Inn_2, TRUNC sx, f_1) =
-  $list_(num_(Inn_2), $trunc__($sizenn1(Fnn_1), $sizenn2(Inn_2), sx, f_1))
+  $trunc__($sizenn1(Fnn_1), $sizenn2(Inn_2), sx, f_1)
 def $cvtop__(Fnn_1, Inn_2, TRUNC_SAT sx, f_1) =
-  $list_(num_(Inn_2), $trunc_sat__($sizenn1(Fnn_1), $sizenn2(Inn_2), sx, f_1))
+  $trunc_sat__($sizenn1(Fnn_1), $sizenn2(Inn_2), sx, f_1)
 def $cvtop__(Inn_1, Fnn_2, CONVERT sx, i_1) =
   $convert__($sizenn1(Inn_1), $sizenn2(Fnn_2), sx, i_1)
 def $cvtop__(Fnn_1, Fnn_2, PROMOTE, f_1) =
@@ -655,9 +655,9 @@ def $lcvtop__(Jnn_1 X M_1, Jnn_2 X M_2, EXTEND sx, c_1) = c
     -- if c = $extend__($lsizenn1(Jnn_1), $lsizenn2(Jnn_2), sx, c_1)
 def $lcvtop__(Jnn_1 X M_1, Fnn_2 X M_2, CONVERT sx, c_1) = c
     -- if c = $convert__($lsizenn1(Jnn_1), $lsizenn2(Fnn_2), sx, c_1)
-def $lcvtop__(Fnn_1 X M_1, Inn_2 X M_2, TRUNC_SAT sx, c_1) = $list_(lane_(Inn_2), c?)
+def $lcvtop__(Fnn_1 X M_1, Inn_2 X M_2, TRUNC_SAT sx, c_1) = c?
     -- if c? = $trunc_sat__($lsizenn1(Fnn_1), $lsizenn2(Inn_2), sx, c_1)
-def $lcvtop__(Fnn_1 X M_1, Inn_2 X M_2, RELAXED_TRUNC sx, c_1) = $list_(lane_(Inn_2), c?)
+def $lcvtop__(Fnn_1 X M_1, Inn_2 X M_2, RELAXED_TRUNC sx, c_1) = c?
     -- if c? = $relaxed_trunc__($lsizenn1(Fnn_1), $lsizenn2(Inn_2), sx, c_1)
 def $lcvtop__(Fnn_1 X M_1, Fnn_2 X M_2, DEMOTE, c_1) = c*
     -- if c* = $demote__($lsizenn1(Fnn_1), $lsizenn2(Fnn_2), c_1)
@@ -674,7 +674,7 @@ def $vcvtop__(Lnn_1 X M_1, Lnn_2 X M_2, vcvtop, half, eps, v_1) = v
   -- if v <- $invlanes_(Lnn_2 X M_2, c*)*
 def $vcvtop__(Lnn_1 X M_1, Lnn_2 X M_2, vcvtop, eps, zero, v_1) = v
   -- if c_1* = $lanes_(Lnn_1 X M_1, v_1)
-  -- if c** = $setproduct_(lane_(Lnn_2), ($lcvtop__(Lnn_1 X M_1, Lnn_2 X M_2, vcvtop, c_1)* ++ $zero(Lnn_2)^M_1))
+  -- if c** = $setproduct_(lane_(Lnn_2), ($lcvtop__(Lnn_1 X M_1, Lnn_2 X M_2, vcvtop, c_1)* ++ [$zero(Lnn_2)]^M_1))
   -- if v <- $invlanes_(Lnn_2 X M_2, c*)*
 
 def $vnarrowop__(Jnn_1 X M_1, Jnn_2 X M_2, sx, v_1, v_2) = v

spectec/spec/wasm-3.0/5-runtime.watsup

@@ -122,6 +122,7 @@ var hi : taginst
 var ei : eleminst
 var di : datainst
 var xi : exportinst
+var exn : exninst
 
 var si : structinst
 var ai : arrayinst

spectec/spec/wasm-3.0/6-runtime-aux.watsup

@@ -180,7 +180,6 @@ def $add_exninst(state, exninst*) : state        hint(show %[.EXNS =++ %])    hi
 
 def $add_structinst((s; f), si*) = s[.STRUCTS =++ si*]; f
 def $add_arrayinst((s; f), ai*) = s[.ARRAYS =++ ai*]; f
-;; TODO: variable name for exninst? (ei and xi are both taken)
 def $add_exninst((s; f), exn*) = s[.EXNS =++ exn*]; f
 
 

spectec/spec/wasm-3.0/8-reduction.watsup

@@ -225,7 +225,6 @@ rule Step_pure/return-handler:
 ;; Exceptions
 
 rule Step/throw:
-  ;; TODO(2, rossberg): Appropriate variable name for exception instance `exn`
   z; val^n (THROW x)  ~>  $add_exninst(z, exn); (REF.EXN_ADDR a) THROW_REF
   -- Expand: $tag(z, x).TYPE ~~ FUNC (t^n -> eps)
   -- if a = |$exninst(z)|

spectec/src/al/al_util.ml

@@ -55,6 +55,7 @@ let updE ?(at = no) ~note (e1, pl, e2) = UpdE (e1, pl, e2) |> mk_expr at note
 let extE ?(at = no) ~note (e1, pl, e2, dir) = ExtE (e1, pl, e2, dir) |> mk_expr at note
 let strE ?(at = no) ~note r = StrE r |> mk_expr at note
 let compE ?(at = no) ~note (e1, e2) = CompE (e1, e2) |> mk_expr at note
+let liftE ?(at = no) ~note e = LiftE e |> mk_expr at note
 let catE ?(at = no) ~note (e1, e2) = CatE (e1, e2) |> mk_expr at note
 let memE ?(at = no) ~note (e1, e2) = MemE (e1, e2) |> mk_expr at note
 let lenE ?(at = no) ~note e = LenE e |> mk_expr at note
@@ -111,8 +112,8 @@ let iter_var ?(at = no) x iter t =
     ~at:at ~note:iter_note
 
 
-    let some x = caseV (x, [optV (Some (tupV []))])
-let none x = caseV (x, [optV None])
+let some x = optV (Some (caseV (x, [])))
+let none _x = optV None
 
 
 (* Failures *)

spectec/src/al/ast.ml

@@ -82,6 +82,7 @@ and expr' =
   | IterE of expr * iterexp                       (* expr (`{` id* `}`)* *)
   | OptE of expr option                           (* expr?  *)
   | ListE of expr list                            (* `[` expr* `]` *)
+  | LiftE of expr                                 (* convert option to list *)
   | GetCurStateE                                  (* "the current state" *)
   | GetCurContextE of atom option                 (* "the current context of certain (Some) or any (None) type" *)
   | ChooseE of expr                               (* "an element of" expr *)

spectec/src/al/eq.ml

@@ -38,6 +38,7 @@ let rec eq_expr e1 e2 =
     eq_expr e1 e2 && eq_iterexp ie1 ie2
   | OptE eo1, OptE eo2 -> eq_expr_opt eo1 eo2
   | ListE el1, ListE el2 -> eq_exprs el1 el2
+  | LiftE e1, LiftE e2 -> eq_expr e1 e2
   | GetCurStateE, GetCurStateE -> true
   | GetCurContextE i1, GetCurContextE i2 -> Option.equal (=) i1 i2
   | ChooseE e1, ChooseE e2 -> eq_expr e1 e2

spectec/src/al/eval.ml

@@ -216,6 +216,13 @@ let rec reduce_exp s e : expr =
     | ListE es2' when is_normal_exp e1' && List.for_all is_normal_exp es2' -> BoolE false
     | _ -> MemE (e1', e2')
     ) $> e
+  | LiftE e1 ->
+    let e1' = reduce_exp s e1 in
+    (match e1'.it with
+    | OptE None -> ListE []
+    | OptE (Some e11) -> ListE [e11]
+    | _ -> LiftE e1'
+    ) $> e
   | LenE e1 ->
     let e1' = reduce_exp s e1 in
     (match e1'.it with

spectec/src/al/free.ml

@@ -26,6 +26,7 @@ let rec free_expr expr =
   | SubE (id, _) -> free_id id
   | CvtE (e, _, _)
   | UnE (_, e)
+  | LiftE e
   | LenE e
   | ChooseE e -> free_expr e
   | BinE (_, e1, e2)

spectec/src/al/print.ml

@@ -140,6 +140,7 @@ and string_of_expr expr =
   | GetCurContextE None -> "current_context()"
   | GetCurContextE (Some a) -> sprintf "current_context(%s)" (string_of_atom a)
   | ListE el -> "[" ^ string_of_exprs ", " el ^ "]"
+  | LiftE e -> "lift(" ^ string_of_expr e ^ ")"
   | AccE (e, p) -> sprintf "%s%s" (string_of_expr e) (string_of_path p)
   | ExtE (e1, ps, e2, dir) -> (
     match dir with
@@ -449,6 +450,7 @@ and structured_string_of_expr expr =
   | GetCurContextE None -> "GetCurContextE"
   | GetCurContextE (Some a) -> sprintf "GetCurContextE (%s)" (string_of_atom a)
   | ListE el -> "ListE ([" ^ structured_string_of_exprs el ^ "])"
+  | LiftE e -> "LiftE (" ^ structured_string_of_expr e ^ ")"
   | AccE (e, p) ->
     "AccE ("
     ^ structured_string_of_expr e

spectec/src/al/valid.ml

@@ -598,6 +598,13 @@ and valid_expr env (expr: expr) : unit =
     l
     |> List.map note
     |> List.iter (check_match source elem_typ)
+  | LiftE expr1 ->
+    valid_expr env expr;
+    check_list source expr.note;
+    check_opt source expr1.note;
+    let elem_typ = unwrap_iter_typ expr.note in
+    let elem1_typ = unwrap_iter_typ expr1.note in
+    check_match source elem1_typ elem_typ
   | GetCurStateE ->
     check_evalctx source expr.note
   | GetCurContextE _ ->

spectec/src/al/walk.ml

@@ -37,7 +37,7 @@ let walk_expr (walker: unit_walker) (expr: expr) : unit =
   | GetCurContextE _ | YetE _
   | TopValueE None | ContextKindE _ -> ()
 
-  | CvtE (e, _, _) | UnE (_, e) | LenE e
+  | CvtE (e, _, _) | UnE (_, e) | LiftE e | LenE e
   | IsDefinedE e | IsCaseOfE (e, _) | HasTypeE (e, _) | IsValidE e
   | TopValueE (Some e) | TopValuesE e | ChooseE e -> walker.walk_expr walker e
 
@@ -141,6 +141,7 @@ let walk_expr (walker: walker) (expr: expr) : expr =
     | CompE (e1, e2) -> CompE (walk_expr e1, walk_expr e2)
     | CatE (e1, e2) -> CatE (walk_expr e1, walk_expr e2)
     | MemE (e1, e2) -> MemE (walk_expr e1, walk_expr e2)
+    | LiftE e -> LiftE (walk_expr e)
     | LenE e -> LenE (walk_expr e)
     | StrE r -> StrE (Record.map (fun x -> x) walk_expr r)
     | AccE (e, p) -> AccE (walk_expr e, walk_path p)

spectec/src/backend-interpreter/construct.ml

@@ -94,18 +94,18 @@ let al_to_bool = unwrap_boolv
 (* Destruct type *)
 
 let al_to_null: value -> null = function
-  | CaseV ("NULL", [ OptV None ]) -> NoNull
-  | CaseV ("NULL", [ OptV _ ]) -> Null
+  | OptV None -> NoNull
+  | OptV _ -> Null
   | v -> error_value "null" v
 
 let al_to_final: value -> final = function
-  | CaseV ("FINAL", [ OptV None ]) -> NoFinal
-  | CaseV ("FINAL", [ OptV _ ]) -> Final
+  | OptV None -> NoFinal
+  | OptV _ -> Final
   | v -> error_value "final" v
 
 let al_to_mut: value -> mut = function
-  | CaseV ("MUT", [ OptV None ]) -> Cons
-  | CaseV ("MUT", [ OptV _ ]) -> Var
+  | OptV None -> Cons
+  | OptV _ -> Var
   | v -> error_value "mut" v
 
 let rec al_to_storage_type: value -> storage_type = function

spectec/src/backend-interpreter/interpreter.ml

@@ -278,6 +278,8 @@ and eval_expr env expr =
     in
     (id, Array.append !arr1 !arr2 |> listV |> ref)
     ) s1 |> strV
+  | LiftE e1 ->
+    eval_expr env e1 |> unwrap_optv |> Option.to_list |> listV_of_list
   | CatE (e1, e2) ->
     let a1 = eval_expr env e1 |> unwrap_seq_to_array in
     let a2 = eval_expr env e2 |> unwrap_seq_to_array in

spectec/src/backend-latex/render.ml

@@ -70,13 +70,13 @@ let as_arith_exp e =
 
 let as_paren_exp e =
   match e.it with
-  | ParenE (e1, _) -> e1
+  | ParenE e1 -> e1
   | _ -> e
 
 let as_tup_exp e =
   match e.it with
   | TupE es -> es
-  | ParenE (e1, _) -> [e1]
+  | ParenE e1 -> [e1]
   | _ -> [e]
 
 let as_seq_exp e =
@@ -86,7 +86,7 @@ let as_seq_exp e =
 
 let rec fuse_exp e deep =
   match e.it with
-  | ParenE (e1, b) when deep -> ParenE (fuse_exp e1 false, b) $ e.at
+  | ParenE e1 when deep -> ParenE (fuse_exp e1 false) $ e.at
   | IterE (e1, iter) -> IterE (fuse_exp e1 deep, iter) $ e.at
   | SeqE (e1::es) -> List.fold_left (fun e1 e2 -> FuseE (e1, e2) $ e.at) e1 es
   | _ -> e
@@ -638,6 +638,7 @@ let rec expand_iter env ctxt iter =
   | ListN (e, id_opt) -> ListN (expand_exp env ctxt e, id_opt)
 
 and expand_exp env ctxt e =
+  (* Involves side effects, be careful to order recursive calls! *)
   (match e.it with
   | AtomE atom ->
     let atom' = expand_atom env ctxt atom in
@@ -665,6 +666,9 @@ and expand_exp env ctxt e =
   | SeqE es ->
     let es' = List.map (expand_exp env ctxt) es in
     SeqE es'
+  | ListE es ->
+    let es' = List.map (expand_exp env ctxt) es in
+    ListE es'
   | IdxE (e1, e2) ->
     let e1' = expand_exp env ctxt e1 in
     let e2' = expand_exp env ctxt e2 in
@@ -708,9 +712,9 @@ and expand_exp env ctxt e =
     LenE e1'
   | SizeE id ->
     SizeE id
-  | ParenE (e1, b) ->
+  | ParenE e1 ->
     let e1' = expand_exp env ctxt e1 in
-    ParenE (e1', b)
+    ParenE e1'
   | TupE es ->
     let es' = List.map (expand_exp env ctxt) es in
     TupE es'
@@ -1102,7 +1106,7 @@ let rec render_iter env = function
   | Opt -> "^?"
   | List -> "^\\ast"
   | List1 -> "^{+}"
-  | ListN ({it = ParenE (e, _); _}, None) | ListN (e, None) ->
+  | ListN ({it = ParenE e; _}, None) | ListN (e, None) ->
     "^{" ^ render_exp env e ^ "}"
   | ListN (e, Some id) ->
     "^{" ^ render_varid env id ^ "<" ^ render_exp env e ^ "}"
@@ -1222,7 +1226,7 @@ and render_exp env e =
   | TextE t -> "\\mbox{\\texttt{`" ^ t ^ "'}}"
   | CvtE (e1, _) -> render_exp env e1
   | UnE (op, e2) -> "{" ^ render_unop op ^ render_exp env e2 ^ "}"
-  | BinE (e1, `PowOp, ({it = ParenE (e2, _); _ } | e2)) ->
+  | BinE (e1, `PowOp, ({it = ParenE e2; _ } | e2)) ->
     "{" ^ render_exp env e1 ^ "^{" ^ render_exp env e2 ^ "}}"
   | BinE (({it = NumE (`DecOp, `Nat _); _} as e1), `MulOp,
       ({it = VarE _ | CallE (_, []) | ParenE _; _ } as e2)) ->
@@ -1252,6 +1256,7 @@ Printf.eprintf "[render %s:X @ %s] try expansion\n%!" (Source.string_of_region e
       )
     | _ -> render_exp_seq env es
     )
+  | ListE es -> "{}[" ^ render_exp_seq env es ^ "]"
   | IdxE (e1, e2) -> render_exp env e1 ^ "{}[" ^ render_exp env e2 ^ "]"
   | SliceE (e1, e2, e3) ->
     render_exp env e1 ^
@@ -1273,10 +1278,10 @@ Printf.eprintf "[render %s:X @ %s] try expansion\n%!" (Source.string_of_region e
   | MemE (e1, e2) -> render_exp env e1 ^ " \\in " ^ render_exp env e2
   | LenE e1 -> "{|" ^ render_exp env e1 ^ "|}"
   | SizeE id -> "||" ^ render_gramid env id ^ "||"
-  | ParenE ({it = SeqE [{it = AtomE atom; _}; _]; _} as e1, _)
+  | ParenE ({it = SeqE [{it = AtomE atom; _}; _]; _} as e1)
     when render_atom env atom = "" ->
     render_exp env e1
-  | ParenE (e1, _) -> "(" ^ render_exp env e1 ^ ")"
+  | ParenE e1 -> "(" ^ render_exp env e1 ^ ")"
   | TupE es -> "(" ^ render_exps ", " env es ^ ")"
   | InfixE (e1, atom, e2) ->
     let id = typed_id atom in
@@ -1323,7 +1328,7 @@ Printf.eprintf "[render %s:X @ %s] try expansion\n%!" (Source.string_of_region e
     let es = e2' :: flatten_fuse_exp_rev e1 in
     String.concat "" (List.map (fun e -> "{" ^ render_exp env e ^ "}") (List.rev es))
   | UnparenE {it = ArithE e1; _} -> render_exp env (UnparenE e1 $ e.at)
-  | UnparenE ({it = ParenE (e1, _); _} | e1) -> render_exp env e1
+  | UnparenE ({it = ParenE e1; _} | e1) -> render_exp env e1
   | HoleE `None -> ""
   | HoleE _ -> error e.at "misplaced hole"
   | LatexE s -> s
@@ -1497,7 +1502,7 @@ and render_sym_seq env = function
 and render_prod env prod : row list =
   let (g, e, prems) = prod.it in
   match e.it, prems with
-  | (TupE [] | ParenE ({it = SeqE []; _}, _)), [] ->
+  | (TupE [] | ParenE {it = SeqE []; _}), [] ->
     [Row [Col (render_sym env g)]]
   | _ when not env.config.display ->
     prefix_rows_hd

spectec/src/backend-prose/print.ml

@@ -106,6 +106,7 @@ and string_of_expr expr =
   | GetCurContextE None -> "the current context"
   | GetCurContextE (Some a) -> sprintf "the current %s context" (string_of_atom a)
   | ListE el -> "[" ^ string_of_exprs ", " el ^ "]"
+  | LiftE e -> string_of_expr e
   | AccE (e, p) -> sprintf "%s%s" (string_of_expr e) (string_of_path p)
   | ExtE (e1, ps, e2, dir) -> (
     match dir with