Implement membership operator

spectec/doc/Language.md

@@ -138,6 +138,7 @@ exp ::=
   exp "." atom                         record access
   exp "," exp                          record extension
   exp "++" exp                         list and record composition
+  exp "<-" exp                         list membership
   "|" exp "|"                          list length
   "||" gramid "||"                     expansion length
   "(" list(exp, ",") ")"               parentheses or tupling

spectec/spec/wasm-3.0/6-typing.watsup

@@ -741,7 +741,7 @@ rule Instr_ok/ref.null:
 rule Instr_ok/ref.func:
   C |- REF.FUNC x : eps -> (REF dt)
   -- if C.FUNCS[x] = dt
-  -- if C.REFS = x_1* x x_2*  ;; TODO(2, rossberg): use elementof
+  -- if x <- C.REFS
 
 rule Instr_ok/ref.i31:
   C |- REF.I31 : I32 -> (REF I31)
@@ -1153,19 +1153,10 @@ rule Instr_const/global.get:
   C |- (GLOBAL.GET x) CONST
   -- if C.GLOBALS[x] = t
 
-;; TODO(2, rossberg): built in elemof
-def $in_numtype(numtype, numtype*) : bool    hint(show % <- %)
-def $in_numtype(nt, eps) = false
-def $in_numtype(nt, nt_1 nt'*) = nt = nt_1 \/ $in_numtype(nt, nt'*)
-
-def $in_binop(numtype, binop_(numtype), binop_(numtype)*) : bool  hint(show %2 <- %3)
-def $in_binop(nt, binop, eps) = false
-def $in_binop(nt, binop, (ibinop_1) ibinop'*) = binop = ibinop_1 \/ $in_binop(nt, binop, ibinop'*)
-
 rule Instr_const/binop:
   C |- (BINOP Inn binop) CONST
-  -- if $in_numtype(Inn, I32 I64)
-  -- if $in_binop(Inn, binop, ADD SUB MUL)
+  -- if Inn <- I32 I64
+  -- if binop <- ADD SUB MUL
 
 
 rule Expr_const: C |- instr* CONST

spectec/src/al/al_util.ml

@@ -47,6 +47,7 @@ let updE ?(at = no) (e1, pl, e2) = UpdE (e1, pl, e2) |> mk_expr at
 let extE ?(at = no) (e1, pl, e2, dir) = ExtE (e1, pl, e2, dir) |> mk_expr at
 let strE ?(at = no) r = StrE r |> mk_expr at
 let catE ?(at = no) (e1, e2) = CatE (e1, e2) |> mk_expr at
+let memE ?(at = no) (e1, e2) = MemE (e1, e2) |> mk_expr at
 let lenE ?(at = no) e = LenE e |> mk_expr at
 let tupE ?(at = no) el = TupE el |> mk_expr at
 let caseE ?(at = no) (a, el) = CaseE (a, el) |> mk_expr at

spectec/src/al/ast.ml

@@ -85,6 +85,7 @@ and expr' =
   | ExtE of expr * path list * expr * extend_dir (* expr `[` path* `]` `:+` expr *)
   | StrE of (atom, expr) record         (* `{` (atom `->` expr)* `}` *)
   | CatE of expr * expr                 (* expr `++` expr *)
+  | MemE of expr * expr                 (* expr `<-` expr *)
   | LenE of expr                        (* `|` expr `|` *)
   | TupE of expr list                   (* `(` (expr `,`)* `)` *)
   | CaseE of atom * expr list           (* atom `(` expr* `)` -- MixE/CaseE *)

spectec/src/al/eq.ml

@@ -30,6 +30,9 @@ let rec eq_expr e1 e2 =
   | CatE (e11, e12), CatE (e21, e22) ->
       eq_expr e11 e21 &&
       eq_expr e12 e22
+  | MemE (e11, e12), MemE (e21, e22) ->
+      eq_expr e11 e21 &&
+      eq_expr e12 e22
   | LenE e1, LenE e2 -> eq_expr e1 e2
   | TupE el1, TupE el2 -> eq_exprs el1 el2
   | CaseE (a1, el1), CaseE (a2, el2) ->

spectec/src/al/free.ml

@@ -28,6 +28,7 @@ let rec free_expr expr =
   | ContE e -> free_expr e
   | BinE (_, e1, e2)
   | CatE (e1, e2)
+  | MemE (e1, e2)
   | InfixE (e1, _, e2)
   | LabelE (e1, e2) -> free_expr e1 @ free_expr e2
   | FrameE (e_opt, e) -> free_opt free_expr e_opt @ free_expr e

spectec/src/al/print.ml

@@ -145,6 +145,8 @@ and string_of_expr expr =
   | CallE (id, el) -> sprintf "$%s(%s)" id (string_of_exprs ", " el)
   | CatE (e1, e2) ->
     sprintf "%s ++ %s" (string_of_expr e1) (string_of_expr e2)
+  | MemE (e1, e2) ->
+    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"
@@ -426,6 +428,12 @@ and structured_string_of_expr expr =
     ^ ", "
     ^ structured_string_of_expr e2
     ^ ")"
+  | MemE (e1, e2) ->
+    "MemE ("
+    ^ structured_string_of_expr e1
+    ^ ", "
+    ^ structured_string_of_expr e2
+    ^ ")"
   | LenE e -> "LenE (" ^ structured_string_of_expr e ^ ")"
   | ArityE e -> "ArityE (" ^ structured_string_of_expr e ^ ")"
   | GetCurStateE -> "GetCurStateE"

spectec/src/al/walk.ml

@@ -44,6 +44,7 @@ let rec walk_expr f e =
       (* TODO: Implement walker for iter *)
       | ListE el -> ListE (List.map new_ el)
       | CatE (e1, e2) -> CatE (new_ e1, new_ e2)
+      | MemE (e1, e2) -> MemE (new_ e1, new_ e2)
       | LenE e' -> LenE (new_ e')
       | StrE r -> StrE (Record.map id new_ r)
       | AccE (e, p) -> AccE (new_ e, walk_path f p)

spectec/src/backend-interpreter/interpreter.ml

@@ -150,6 +150,10 @@ and eval_expr env expr =
     | GeOp, v1, v2 -> boolV (v1 >= v2)
     | _ -> fail_expr expr "type mismatch for binary operation"
     )
+  (* Set Operation *)
+  | MemE (e1, e2) ->
+    let v1 = eval_expr env e1 in
+    eval_expr env e2 |> unwrap_listv_to_array |> Array.exists ((=) v1) |> boolV
   (* Function Call *)
   | CallE (fname, el) ->
     let args = List.map (eval_expr env) el in

spectec/src/backend-latex/render.ml

@@ -535,6 +535,10 @@ and expand_exp env ctxt e =
     let e1' = expand_exp env ctxt e1 in
     let e2' = expand_exp env ctxt e2 in
     CompE (e1', e2')
+  | MemE (e1, e2) ->
+    let e1' = expand_exp env ctxt e1 in
+    let e2' = expand_exp env ctxt e2 in
+    MemE (e1', e2')
   | LenE e1 ->
     let e1' = expand_exp env ctxt e1 in
     LenE e1'
@@ -1052,6 +1056,7 @@ Printf.eprintf "[render %s:X @ %s] try expansion\n%!" (Source.string_of_region e
   | DotE (e1, atom) -> render_exp env e1 ^ "{.}" ^ render_fieldname env atom
   | CommaE (e1, e2) -> render_exp env e1 ^ ", " ^ render_exp env e2
   | CompE (e1, e2) -> render_exp env e1 ^ " \\oplus " ^ render_exp env e2
+  | 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, _)

spectec/src/backend-prose/gen.ml

@@ -56,6 +56,8 @@ let rec if_expr_to_instrs e =
       | _ -> print_yet_exp e "if_expr_to_instrs"; YetI (Il.Print.string_of_exp e) ]
   | Ast.BinE (Ast.EquivOp, e1, e2) ->
       [ EquivI (exp_to_expr e1, exp_to_expr e2) ]
+  | Ast.MemE (e1, e2) ->
+      [ MemI (exp_to_expr e1, exp_to_expr e2) ]
   | _ -> print_yet_exp e "if_expr_to_instrs"; [ YetI (Il.Print.string_of_exp e) ]
 
 let rec prem_to_instrs prem = match prem.it with

spectec/src/backend-prose/print.ml

@@ -41,6 +41,10 @@ let rec string_of_instr = function
         (string_of_expr e1)
         (string_of_cmpop cmpop)
         (string_of_expr e2)
+  | MemI (e1, e2) ->
+      sprintf "%s %s must be contained in %s." (indent ())
+        (string_of_expr e1)
+        (string_of_expr e2)
   | MustValidI (e1, e2, eo) ->
       sprintf "%s Under the context %s, %s must be valid%s." (indent ())
         (string_of_expr e1)

spectec/src/backend-prose/prose.ml

@@ -7,6 +7,7 @@ type cmpop = Eq | Ne | Lt | Gt | Le | Ge
 type instr =
 | LetI of Al.Ast.expr * Al.Ast.expr
 | CmpI of Al.Ast.expr * cmpop * Al.Ast.expr
+| MemI of Al.Ast.expr * Al.Ast.expr
 | MustValidI of Al.Ast.expr * Al.Ast.expr * Al.Ast.expr option
 | MustMatchI of Al.Ast.expr * Al.Ast.expr
 | IsValidI of Al.Ast.expr option

spectec/src/backend-prose/render.ml

@@ -417,6 +417,10 @@ let rec render_prose_instr env depth = function
       (String.capitalize_ascii (render_expr env e1))
       (render_prose_cmpop cmpop)
       (render_expr env e2)
+  | MemI (e1, e2) ->
+    sprintf "* %s must be contained in %s."
+      (String.capitalize_ascii (render_expr env e1))
+      (render_expr env e2)
   | MustValidI (e1, e2, e3) ->
     sprintf "* Under the context %s, %s must be valid%s."
       (render_expr env e1)

spectec/src/el/ast.ml

@@ -117,6 +117,7 @@ and exp' =
   | DotE of exp * atom           (* exp `.` atom *)
   | CommaE of exp * exp          (* exp `,` exp *)
   | CompE of exp * exp           (* exp `++` exp *)
+  | MemE of exp * exp            (* exp `<-` exp *)
   | LenE of exp                  (* `|` exp `|` *)
   | SizeE of id                  (* `||` exp `||` *)
   | ParenE of exp * [`Sig | `Insig]  (* `(` exp `)` *)

spectec/src/el/atom.ml

@@ -15,7 +15,7 @@ and atom' =
   | Dot3                         (* `...` *)
   | Semicolon                    (* `;` *)
   | Backslash                    (* `\` *)
-  | In                           (* `<-` *)
+  | Mem                          (* `<-` *)
   | Arrow                        (* `->` *)
   | Arrow2                       (* ``=>` *)
   | ArrowSub                     (* `->_` *)
@@ -71,7 +71,7 @@ let to_string atom =
   | Dot3 -> "..."
   | Semicolon -> ";"
   | Backslash -> "\\"
-  | In -> "in"
+  | Mem -> "<-"
   | Arrow -> "->"
   | Arrow2 -> "=>"
   | ArrowSub -> "->_"
@@ -120,7 +120,7 @@ let name atom =
   | Dot3 -> "dots"                (* Latex: \ldots *)
   | Semicolon -> "semicolon"      (* Latex: ; *)
   | Backslash -> "setminus"
-  | In -> "in"
+  | Mem -> "in"
   | Arrow -> "arrow"              (* Latex: \rightarrow *)
   | Arrow2 -> "darrow"            (* Latex: \Rightarrow *)
   | ArrowSub -> "arrowsub"        (* Latex: \rightarrow with subscript *)

spectec/src/el/eq.ml

@@ -91,6 +91,7 @@ and eq_exp e1 e2 =
   | IdxE (e11, e12), IdxE (e21, e22)
   | CommaE (e11, e12), CommaE (e21, e22)
   | CompE (e11, e12), CompE (e21, e22)
+  | MemE (e11, e12), MemE (e21, e22)
   | FuseE (e11, e12), FuseE (e21, e22) -> eq_exp e11 e21 && eq_exp e12 e22
   | SliceE (e11, e12, e13), SliceE (e21, e22, e23) ->
     eq_exp e11 e21 && eq_exp e12 e22 && eq_exp e13 e23

spectec/src/el/free.ml

@@ -130,7 +130,7 @@ and free_exp e =
   | ParenE (e1, _) | BrackE (_, e1, _) | ArithE e1 | UnparenE e1 -> free_exp e1
   | SizeE id -> free_gramid id
   | BinE (e1, _, e2) | CmpE (e1, _, e2)
-  | IdxE (e1, e2) | CommaE (e1, e2) | CompE (e1, e2)
+  | IdxE (e1, e2) | CommaE (e1, e2) | CompE (e1, e2) | MemE (e1, e2)
   | InfixE (e1, _, e2) | FuseE (e1, e2) -> free_exp e1 + free_exp e2
   | SliceE (e1, e2, e3) -> free_exp e1 + free_exp e2 + free_exp e3
   | SeqE es | TupE es -> free_list free_exp es
@@ -172,7 +172,7 @@ and det_exp e =
   | TypE (e1, _) -> det_exp e1
   | AtomE _ | BoolE _ | NatE _ | TextE _ | EpsE -> empty
   | UnE _ | BinE _ | CmpE _
-  | IdxE _ | SliceE _ | UpdE _ | ExtE _ | CommaE _ | CompE _
+  | IdxE _ | SliceE _ | UpdE _ | ExtE _ | CommaE _ | CompE _ | MemE _
   | DotE _ | LenE _ | SizeE _ -> idx_exp e
   | HoleE _ | FuseE _ | UnparenE _ | LatexE _ -> assert false
 

spectec/src/el/iter.ml

@@ -131,7 +131,7 @@ and exp e =
   | SizeE x -> gramid x
   | BinE (e1, op, e2) -> exp e1; binop op; exp e2
   | CmpE (e1, op, e2) -> exp e1; cmpop op; exp e2
-  | IdxE (e1, e2) | CommaE (e1, e2) | CompE (e1, e2)
+  | IdxE (e1, e2) | CommaE (e1, e2) | CompE (e1, e2) | MemE (e1, e2)
   | FuseE (e1, e2) -> exp e1; exp e2
   | SliceE (e1, e2, e3) -> exp e1; exp e2; exp e3
   | SeqE es | TupE es -> list exp es
@@ -282,6 +282,7 @@ and clone_exp e =
   | DotE (e1, atom) -> DotE (clone_exp e1, clone_atom atom)
   | CommaE (e1, e2) -> CommaE (clone_exp e1, clone_exp e2)
   | CompE (e1, e2) -> CompE (clone_exp e1, clone_exp e2)
+  | MemE (e1, e2) -> MemE (clone_exp e1, clone_exp e2)
   | LenE e1 -> LenE (clone_exp e1)
   | ParenE (e1, b) -> ParenE (clone_exp e1, b)
   | TupE es -> TupE (List.map clone_exp es)

spectec/src/el/print.ml

@@ -155,6 +155,7 @@ and string_of_exp e =
   | DotE (e1, atom) -> string_of_exp e1 ^ "." ^ string_of_atom atom
   | CommaE (e1, e2) -> string_of_exp e1 ^ ", " ^ string_of_exp e2
   | CompE (e1, e2) -> string_of_exp e1 ^ " ++ " ^ string_of_exp e2
+  | MemE (e1, e2) -> string_of_exp e1 ^ " <- " ^ string_of_exp e2
   | LenE e1 -> "|" ^ string_of_exp e1 ^ "|"
   | SizeE id -> "||" ^ string_of_gramid id ^ "||"
   | ParenE (e, signif) ->

spectec/src/el/subst.ml

@@ -138,6 +138,7 @@ and subst_exp s e =
   | DotE (e1, atom) -> DotE (subst_exp s e1, atom)
   | CommaE (e1, e2) -> CommaE (subst_exp s e1, subst_exp s e2)
   | CompE (e1, e2) -> CompE (subst_exp s e1, subst_exp s e2)
+  | MemE (e1, e2) -> MemE (subst_exp s e1, subst_exp s e2)
   | LenE e1 -> LenE (subst_exp s e1)
   | SizeE id -> SizeE (subst_gramid s id)
   | ParenE (e1, b) -> ParenE (subst_exp s e1, b)

spectec/src/frontend/dim.ml

@@ -145,6 +145,7 @@ and check_exp env ctx e =
   | IdxE (e1, e2)
   | CommaE (e1, e2)
   | CompE (e1, e2)
+  | MemE (e1, e2)
   | InfixE (e1, _, e2) ->
     check_exp env ctx e1;
     check_exp env ctx e2
@@ -404,6 +405,10 @@ and annot_exp env e : Il.Ast.exp * occur =
     | ListE es ->
       let es', occurs = List.split (List.map (annot_exp env) es) in
       ListE es', List.fold_left union Env.empty occurs
+    | MemE (e1, e2) ->
+      let e1', occur1 = annot_exp env e1 in
+      let e2', occur2 = annot_exp env e2 in
+      MemE (e1', e2'), union occur1 occur2
     | CatE (e1, e2) ->
       let e1', occur1 = annot_exp env e1 in
       let e2', occur2 = annot_exp env e2 in

spectec/src/frontend/elab.ml

@@ -985,6 +985,10 @@ and infer_exp' env e : Il.exp' * typ =
     let _ = as_comp_typ "expression" env Infer t1 e.at in
     let e2' = elab_exp env e2 t1 in
     Il.CompE (e1', e2'), t1
+  | MemE (e1, e2) ->
+    let e1', t1 = infer_exp env e1 in
+    let e2' = elab_exp env e2 (IterT (t1, List) $ e2.at) in
+    Il.MemE (e1', e2'), BoolT $ e.at
   | LenE e1 ->
     let e1', t1 = infer_exp env e1 in
     let _t11 = as_list_typ "expression" env Infer t1 e1.at in
@@ -1122,6 +1126,9 @@ and elab_exp' env e t : Il.exp' =
     let e1' = elab_exp env e1 t in
     let e2' = elab_exp env e2 t in
     Il.CompE (e1', e2')
+  | MemE _ ->
+    let e', t' = infer_exp env e in
+    cast_exp' "element operator" env e' t' t
   | LenE _ ->
     let e', t' = infer_exp env e in
     cast_exp' "list length" env e' t' t

spectec/src/frontend/eval.ml

@@ -282,6 +282,20 @@ and reduce_exp env e : exp =
       in StrE (merge efs1 efs2)
     | _ -> CompE (e1', e2')
     ) $ e.at
+  | MemE (e1, e2) ->
+    let e1' = reduce_exp env e1 in
+    let e2' = reduce_exp env e2 in
+    (match e2'.it with
+    | SeqE [] -> BoolE false $ e.at
+    | SeqE (e21'::es2') ->
+      reduce_exp env (BinE (
+        CmpE (e1', EqOp, e21') $ e.at,
+        OrOp,
+        MemE (e1', SeqE es2' $ e2.at) $ e.at
+      ) $ e.at)
+    | _ when is_normal_exp e2' -> reduce_exp env (CmpE (e1', EqOp, e2') $ e.at)
+    | _ -> MemE (e1', e2') $ e.at
+    )
   | LenE e1 ->
     let e1' = reduce_exp env e1 in
     (match e1'.it with

spectec/src/frontend/lexer.mll

@@ -184,7 +184,7 @@ and token = parse
   | "+-" { PLUSMINUS }
   | "-+" { MINUSPLUS }
 
-  | "<-" { IN }
+  | "<-" { MEM }
   | "->" { ARROW }
   | "=>" { ARROW2 }
   | "->_" { ARROWSUB }

spectec/src/frontend/parser.mly

@@ -69,7 +69,7 @@ let rec prec_of_exp = function  (* as far as iteration is concerned *)
   | ParenE _ | TupE _ | BrackE _ | CallE _ | HoleE _ -> Prim
   | AtomE _ | IdxE _ | SliceE _ | UpdE _ | ExtE _ | DotE _ | IterE _ -> Post
   | SeqE _ -> Seq
-  | UnE _ | BinE _ | CmpE _ | InfixE _ | LenE _ | SizeE _
+  | UnE _ | BinE _ | CmpE _ | MemE _ | InfixE _ | LenE _ | SizeE _
   | CommaE _ | CompE _ | TypE _ | FuseE _ | UnparenE _ | LatexE _ -> Op
   | ArithE e -> prec_of_exp e.it
 
@@ -123,7 +123,7 @@ let rec is_typcon t =
 %token NOT AND OR
 %token QUEST PLUS MINUS STAR SLASH BACKSLASH UP COMPOSE PLUSMINUS MINUSPLUS
 %token ARROW ARROW2 ARROWSUB ARROW2SUB DARROW2 SQARROW SQARROWSTAR
-%token IN PREC SUCC TURNSTILE TILESTURN
+%token MEM PREC SUCC TURNSTILE TILESTURN
 %token DOLLAR TICK
 %token BOT TOP
 %token HOLE MULTIHOLE NOTHING FUSE FUSEFUSE LATEX
@@ -146,7 +146,7 @@ let rec is_typcon t =
 %right SQARROW SQARROWSTAR PREC SUCC BIGCOMP BIGAND BIGOR
 %left COLON SUB SUP ASSIGN EQUIV APPROX
 %left COMMA COMMA_NL
-%right EQ NE LT GT LE GE IN
+%right EQ NE LT GT LE GE MEM
 %right ARROW ARROWSUB
 %left SEMICOLON
 %left DOT DOTDOT DOTDOTDOT
@@ -252,6 +252,7 @@ atom_ :
   | atom_escape { $1 }
 atom_escape :
   | TICK EQ { Atom.Equal }
+  | TICK MEM { Atom.Mem }
   | TICK QUEST { Atom.Quest }
   | TICK PLUS { Atom.Plus }
   | TICK STAR { Atom.Star }
@@ -343,7 +344,6 @@ check_atom :
   | SUCC { Atom.Succ }
   | TILESTURN { Atom.Tilesturn }
   | TURNSTILE { Atom.Turnstile }
-  | IN { Atom.In }
 
 
 (* Iteration *)
@@ -583,6 +583,7 @@ exp_bin_ :
   | exp_bin COMPOSE exp_bin { CompE ($1, $3) }
   | exp_bin infixop exp_bin { InfixE ($1, $2, $3) }
   | exp_bin cmpop exp_bin { CmpE ($1, $2, $3) }
+  | exp_bin MEM exp_bin { MemE ($1, $3) }
   | exp_bin boolop exp_bin { BinE ($1, $2, $3) }
 
 exp_rel : exp_rel_ { $1 $ $sloc }
@@ -647,6 +648,7 @@ arith_bin_ :
   | arith_un_ { $1 }
   | arith_bin binop arith_bin { BinE ($1, $2, $3) }
   | arith_bin cmpop arith_bin { CmpE ($1, $2, $3) }
+  | arith_bin MEM arith_bin { MemE ($1, $3) }
   | arith_bin boolop arith_bin { BinE ($1, $2, $3) }
 
 arith : arith_bin { $1 }