Added TopHandlerE

spectec/src/al/al_util.ml

@@ -78,6 +78,7 @@ let matchE ?(at = no) ~note (e1, e2) = MatchE (e1, e2) |> mk_expr at note
 let hasTypeE ?(at = no) ~note (e, ty) = HasTypeE (e, ty) |> mk_expr at note
 let topLabelE ?(at = no) ~note () = TopLabelE |> mk_expr at note
 let topFrameE ?(at = no) ~note () = TopFrameE |> mk_expr at note
+let topHandlerE ?(at = no) ~note () = TopHandlerE |> mk_expr at note
 let topValueE ?(at = no) ~note e_opt = TopValueE e_opt |> mk_expr at note
 let topValuesE ?(at = no) ~note e = TopValuesE e |> mk_expr at note
 let subE ?(at = no) ~note (id, ty) = SubE (id, ty) |> mk_expr at note

spectec/src/al/ast.ml

@@ -119,6 +119,7 @@ and expr' =
   | HasTypeE of expr * typ                        (* the type of expr is ty *)
   | TopFrameE                                     (* "a frame is now on the top of the stack" *)
   | TopLabelE                                     (* "a label is now on the top of the stack" *)
+  | TopHandlerE                                   (* "a handler is now on the top of the stack" *)
   (* Conditions used in assertions *)
   | TopValueE of expr option                      (* "a value (of type expr)? is now on the top of the stack" *)
   | TopValuesE of expr                            (* "at least expr number of values on the top of the stack" *)

spectec/src/al/eq.ml

@@ -54,7 +54,8 @@ let rec eq_expr e1 e2 =
   | MatchE (e11, e12), MatchE (e21, e22) -> eq_expr e11 e21 && eq_expr e12 e22
   | HasTypeE (e1, t1), HasTypeE (e2, t2) -> eq_expr e1 e2 && Il.Eq.eq_typ t1 t2
   | TopLabelE, TopLabelE
-  | TopFrameE, TopFrameE -> true
+  | TopFrameE, TopFrameE
+  | TopHandlerE, TopHandlerE -> true
   | TopValueE eo1, TopValueE eo2 -> eq_expr_opt eo1 eo2
   | TopValuesE e1, TopValuesE e2 -> eq_expr e1 e2
   | SubE (i1, t1), SubE (i2, t2) -> i1 = i2 && Il.Eq.eq_typ t1 t2

spectec/src/al/free.ml

@@ -56,6 +56,7 @@ let rec free_expr expr =
   | MatchE (e1, e2) -> free_expr e1 @ free_expr e2
   | TopLabelE
   | TopFrameE
+  | TopHandlerE
   | TopValueE None -> IdSet.empty
   | IsDefinedE e
   | IsCaseOfE (e, _)

spectec/src/al/print.ml

@@ -206,6 +206,8 @@ and string_of_expr expr =
     (* TODO: "type(top()) == label"*)
   | TopFrameE -> "top_frame()"
     (* TODO: "type(top()) == frame"*)
+  | TopHandlerE -> "top_handler()"
+    (* TODO: "type(top()) == handler"*)
   | TopValueE (Some e) -> sprintf "top_value(%s)" (string_of_expr e)
   | TopValueE None -> "top_value()"
   | TopValuesE e -> sprintf "top_values(%s)" (string_of_expr e)
@@ -534,6 +536,7 @@ and structured_string_of_expr expr =
   | IsValidE e -> "IsValidE (" ^ structured_string_of_expr e ^ ")"
   | TopLabelE -> "TopLabelE"
   | TopFrameE -> "TopFrameE"
+  | TopHandlerE -> "TopHandlerE"
   | TopValueE None -> "TopValueE"
   | TopValueE (Some e) -> "TopValueE (" ^ structured_string_of_expr e ^ ")"
   | TopValuesE e -> "TopValuesE (" ^ structured_string_of_expr e ^ ")"

spectec/src/al/valid.ml

@@ -468,7 +468,7 @@ and valid_expr env (expr: expr) : unit =
   | VarE id ->
     if not (Env.mem id env) then error expr.at ("free identifier " ^ id)
   | NumE _ -> check_num source expr.note;
-  | BoolE _ | TopFrameE | TopLabelE | ContextKindE _ -> check_bool source expr.note
+  | BoolE _ | TopFrameE | TopLabelE | TopHandlerE | ContextKindE _ -> check_bool source expr.note
   | UnE (NotOp, expr') ->
     valid_expr env expr';
     check_bool source expr.note;

spectec/src/al/walk.ml

@@ -35,7 +35,7 @@ let walk_expr (walker: unit_walker) (expr: expr) : unit =
   match expr.it with
   | VarE _ | SubE _ | NumE _ | BoolE _ | GetCurStateE | GetCurLabelE
   | GetCurContextE | GetCurFrameE | YetE _ | TopLabelE | TopFrameE
-  | TopValueE None | ContextKindE _ -> ()
+  | TopHandlerE | TopValueE None | ContextKindE _ -> ()
 
   | UnE (_, e) | LenE e | ArityE e | ContE e
   | IsDefinedE e | IsCaseOfE (e, _) | HasTypeE (e, _) | IsValidE e
@@ -133,7 +133,8 @@ let walk_expr (walker: walker) (expr: expr) : expr =
   let it =
     match expr.it with
     | NumE _ | BoolE _ | VarE _ | SubE _ | GetCurStateE | GetCurFrameE
-    | GetCurLabelE | GetCurContextE | ContextKindE _ | TopLabelE | TopFrameE | YetE _ -> expr.it
+    | GetCurLabelE | GetCurContextE | ContextKindE _ | TopLabelE | TopFrameE
+    | TopHandlerE | YetE _ -> expr.it
     | UnE (op, e) -> UnE (op, walk_expr e)
     | BinE (op, e1, e2) -> BinE (op, walk_expr e1, walk_expr e2)
     | CallE (id, al) -> CallE (id, List.map walk_arg al)
@@ -286,6 +287,7 @@ let rec walk_expr f e =
       | IsValidE e -> IsValidE (new_ e)
       | TopLabelE -> e.it
       | TopFrameE -> e.it
+      | TopHandlerE -> e.it
       | TopValueE (Some e) -> TopValueE (Some (new_ e))
       | TopValueE _ -> e.it
       | TopValuesE e -> TopValuesE (new_ e)

spectec/src/backend-prose/print.ml

@@ -178,6 +178,7 @@ and string_of_expr expr =
   | IsValidE e -> sprintf "%s is valid" (string_of_expr e)
   | TopLabelE -> "a label is now on the top of the stack"
   | TopFrameE -> "a frame is now on the top of the stack"
+  | TopHandlerE -> "a handler is now on the top of the stack"
   | TopValueE (Some e) -> sprintf "a value of value type %s is on the top of the stack" (string_of_expr e)
   | TopValueE None -> "a value is on the top of the stack"
   | TopValuesE e -> sprintf "there are at least %s values on the top of the stack" (string_of_expr e)

spectec/src/backend-prose/render.ml

@@ -453,6 +453,7 @@ and render_expr' env expr =
     sprintf "%s is valid" se
   | Al.Ast.TopLabelE -> "a label is now on the top of the stack"
   | Al.Ast.TopFrameE -> "a frame is now on the top of the stack"
+  | Al.Ast.TopHandlerE -> "a handler is now on the top of the stack"
   | Al.Ast.TopValueE (Some e) ->
     let se = render_expr env e in
     sprintf "a value of value type %s is on the top of the stack" se

spectec/src/il2al/translate.ml

@@ -359,7 +359,7 @@ let insert_assert exp =
   | Il.CaseE ([{it = Il.Atom "LABEL_"; _}]::_, { it = Il.TupE [ _n; _instrs; _vals ]; _ }) ->
     assertI (topLabelE () ~at:at ~note:boolT) ~at:at
   | Il.CaseE ([{it = Il.Atom "HANDLER_"; _}]::_, _) ->
-    assertI (yetE "a handler is now on the top of the stack" ~at:at ~note:boolT) ~at:at
+    assertI (topHandlerE () ~at:at ~note:boolT) ~at:at
   | Il.CaseE ([{it = Il.Atom "CONST"; _}]::_, { it = Il.TupE (ty' :: _); _ }) ->
     assertI (topValueE (Some (translate_exp ty')) ~note:boolT) ~at:at
   | _ ->