Merge branch 'main' into exn

spectec/src/al/al_util.ml

@@ -52,14 +52,12 @@ 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
 let tupE ?(at = no) ~note el = TupE el |> mk_expr at note
-let caseE ?(at = no) ~note (a, el) = CaseE (a, el) |> mk_expr at note
-let caseE2 ?(at = no) ~note (op, el) = CaseE2 (op, el) |> mk_expr at note
+let caseE ?(at = no) ~note (op, el) = CaseE (op, el) |> mk_expr at note
 let callE ?(at = no) ~note (id, el) = CallE (id, el) |> mk_expr at note
 let invCallE ?(at = no) ~note (id, il, el) = InvCallE (id, il, el) |> mk_expr at note
 let iterE ?(at = no) ~note (e, idl, it) = IterE (e, idl, it) |> mk_expr at note
 let optE ?(at = no) ~note e_opt = OptE e_opt |> mk_expr at note
 let listE ?(at = no) ~note el = ListE el |> mk_expr at note
-let infixE ?(at = no) ~note (e1, infix, e2) = InfixE (e1, infix, e2) |> mk_expr at note
 let arityE ?(at = no) ~note e = ArityE e |> mk_expr at note
 let frameE ?(at = no) ~note (e_opt, e) = FrameE (e_opt, e) |> mk_expr at note
 let labelE ?(at = no) ~note (e1, e2) = LabelE (e1, e2) |> mk_expr at note
@@ -242,6 +240,15 @@ let unwrap_framev: value -> value = function
   | v -> fail_value "unwrap_framev" v
 
 
+(* Mixop *)
+
+let get_atom op =
+  match List.find_opt (fun al -> List.length al <> 0) op with
+  | Some al -> Some(List.hd al)
+  | None -> None
+
+let name_of_mixop = Il.Mixop.name
+
 (* Il Types *)
 
 (* name for tuple type *)

spectec/src/al/ast.ml

@@ -92,14 +92,12 @@ and 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 *)
-  | CaseE2 of mixop * expr list                   (* mixop `(` expr* `)` -- CaseE *) (* TODO: Migrate CaseE to CaseE2*)
+  | CaseE of mixop * expr list                   (* mixop `(` expr* `)` -- CaseE *)
   | CallE of id * arg list                        (* id `(` expr* `)` *)
   | InvCallE of id * int option list * arg list   (* id`_`int*`^-1(` expr* `)` *)
   | IterE of expr * id list * iter                (* expr (`{` id* `}`)* *)
   | OptE of expr option                           (* expr?  *)
   | ListE of expr list                            (* `[` expr* `]` *)
-  | InfixE of expr * atom * expr                  (* "expr infix expr" *) (* TODO: Remove InfixE using hint *)
   | 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" *)
@@ -116,15 +114,15 @@ and expr' =
   | IsDefinedE of expr                            (* expr is defined *)
   | MatchE of expr * expr                         (* expr matches expr *)
   (* TODO: use typ *)
-  | HasTypeE of expr * string                     (* the type of expr is ty *)
+  | 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" *)
   (* 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" *)
   (* Administrative Instructions *)
   (* TODO: use typ *)
-  | SubE of id * string                           (* varid, with specific type *)
+  | SubE of id * typ                           (* varid, with specific type *)
   | YetE of string                                (* for future not yet implemented feature *)
 
 and path = path' phrase

spectec/src/al/eq.ml

@@ -23,17 +23,14 @@ let rec eq_expr e1 e2 =
   | 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) -> El.Atom.eq a1 a2 && eq_exprs el1 el2
-  | CaseE2 (op1, el1), CaseE2 (op2, el2) -> Il.Mixop.eq op1 op2 && eq_exprs el1 el2
+  | CaseE (op1, el1), CaseE (op2, el2) -> Il.Mixop.eq op1 op2 && eq_exprs el1 el2
   | CallE (i1, al1), CallE (i2, al2) -> i1 = i2 && eq_args al1 al2
   | InvCallE (i1, nl1, al1), InvCallE (i2, nl2, al2) ->
     i1 = i2 && List.for_all2 (=) nl1 nl2 && eq_args al1 al2
   | IterE (e1, il1, it1), IterE (e2, il2, it2) ->
     eq_expr e1 e2 && il1 = il2 && it1 = it2
   | OptE eo1, OptE eo2 -> eq_expr_opt eo1 eo2
   | ListE el1, ListE el2 -> eq_exprs el1 el2
-  | InfixE (e11, a1, e12), InfixE (e21, a2, e22) ->
-    eq_expr e11 e21 && El.Atom.eq a1 a2 && eq_expr e12 e22
   | ArityE e1, ArityE e2 -> eq_expr e1 e2
   | FrameE (eo1, e1), FrameE (eo2, e2) ->
     eq_expr_opt eo1 eo2 && eq_expr e1 e2
@@ -50,12 +47,12 @@ let rec eq_expr e1 e2 =
   | ContextKindE a1, ContextKindE a2 -> El.Atom.eq a1 a2
   | IsDefinedE e1, IsDefinedE e2 -> 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 && t1 = t2
+  | HasTypeE (e1, t1), HasTypeE (e2, t2) -> eq_expr e1 e2 && Il.Eq.eq_typ t1 t2
   | TopLabelE, TopLabelE
   | TopFrameE, TopFrameE -> 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 && t1 = t2
+  | SubE (i1, t1), SubE (i2, t2) -> i1 = i2 && Il.Eq.eq_typ t1 t2
   | YetE s1, YetE s2 -> s1 = s2
   | _ -> false
 

spectec/src/al/free.ml

@@ -31,15 +31,13 @@ let rec free_expr expr =
   | 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
   | CallE (_, al)
   | InvCallE (_, _, al) ->  free_list free_arg al
   | TupE el
   | ListE el
   | CaseE (_, el) -> free_list free_expr el
-  | CaseE2 (_, el) -> free_list free_expr el
   | StrE r -> free_list (fun (_, e) -> free_expr !e) r
   | AccE (e, p) -> free_expr e @ free_path p
   | ExtE (e1, ps, e2, _)

spectec/src/al/print.ml

@@ -175,18 +175,29 @@ and string_of_expr expr =
   | VarE id -> id
   | SubE (id, _) -> id
   | IterE (e, _, iter) -> string_of_expr e ^ string_of_iter iter
-  | InfixE (e1, a, e2) -> "(" ^ string_of_expr e1 ^ " " ^ string_of_atom a ^ " " ^ string_of_expr e2 ^ ")"
-  | CaseE ({ it=Atom.Atom ("CONST" | "VCONST"); _ }, hd::tl) ->
+  | CaseE ([{ it=Atom.Atom ("CONST" | "VCONST"); _ }]::_tl, hd::tl) ->
     "(" ^ string_of_expr hd ^ ".CONST " ^ string_of_exprs " " tl ^ ")"
-  | CaseE (a, []) -> string_of_atom a
-  | CaseE (a, el) -> "(" ^ string_of_atom a ^ " " ^ string_of_exprs " " el ^ ")"
-  | CaseE2 (op, el) -> "(" ^ string_of_mixop op ^ "_" ^ string_of_exprs " " el ^ ")"
+  | CaseE ([[ atom ]], []) -> string_of_atom atom
+  | CaseE (op, el) ->
+    let op' = List.map (fun al -> String.concat "" (List.map string_of_atom al)) op in
+    (match op' with
+    | [] -> "()"
+    | hd::tl ->
+      let res =
+        List.fold_left2 (
+          fun acc a e ->
+            let a' = if a = "" then "" else " " ^ a in
+            let acc' = if acc = "" then "" else acc ^ " " in
+            acc' ^ string_of_expr e ^ a'
+        ) hd tl el in
+      "(" ^ res ^ ")"
+    )
   | OptE (Some e) -> "?(" ^ string_of_expr e ^ ")"
   | OptE None -> "?()"
   | ContextKindE a -> sprintf "context_kind(%s)" (string_of_atom a)
   | IsDefinedE e -> sprintf "%s != None" (string_of_expr e)
   | IsCaseOfE (e, a) -> sprintf "case(%s) == %s" (string_of_expr e) (string_of_atom a)
-  | HasTypeE (e, t) -> sprintf "type(%s) == %s" (string_of_expr e) t
+  | HasTypeE (e, t) -> sprintf "type(%s) == %s" (string_of_expr e) (string_of_typ t)
   | IsValidE e -> sprintf "valid(%s)" (string_of_expr e)
   | TopLabelE -> "top_label()"
     (* TODO: "type(top()) == label"*)
@@ -286,7 +297,7 @@ let rec string_of_instr' depth instr =
       (string_of_instrs' (depth + 1) il2)
       (repeat indent depth)
   | OtherwiseI il ->
-    sprintf " Otherwise:%s" 
+    sprintf " Otherwise:%s"
       (string_of_instrs' (depth + 1) il)
   | EitherI (il1, il2) ->
     sprintf " Either {%s\n%s }\n%s Or {%s\n %s}"
@@ -308,12 +319,12 @@ let rec string_of_instr' depth instr =
   | LetI (e1, e2) ->
     sprintf " Let %s = %s" (string_of_expr e1)
       (string_of_expr e2)
-  | TrapI -> sprintf " Trap" 
-  | NopI -> sprintf " Nop" 
-  | ReturnI None -> sprintf " Return" 
+  | TrapI -> sprintf " Trap"
+  | NopI -> sprintf " Nop"
+  | ReturnI None -> sprintf " Return"
   | ReturnI (Some e) -> sprintf " Return %s" (string_of_expr e)
   | EnterI (e1, e2, il) ->
-    sprintf " Enter (%s, %s) {%s \n%s }" 
+    sprintf " Enter (%s, %s) {%s \n%s }"
       (string_of_expr e1) (string_of_expr e2) (string_of_instrs' (depth + 1) il) (repeat indent depth)
   | ExecuteI e ->
     sprintf " Execute %s" (string_of_expr e)
@@ -327,7 +338,7 @@ let rec string_of_instr' depth instr =
     sprintf " %s%s := %s"
       (string_of_expr e1) (string_of_path p) (string_of_expr e2)
   | AppendI (e1, e2) ->
-    sprintf " %s :+ %s" 
+    sprintf " %s :+ %s"
       (string_of_expr e2) (string_of_expr e1)
   | YetI s -> sprintf " YetI: %s." s
 
@@ -483,7 +494,7 @@ and structured_string_of_expr expr =
     ^ structured_string_of_expr e2
     ^ ")"
   | VarE id -> "VarE (" ^ id ^ ")"
-  | SubE (id, t) -> "SubE (" ^ id ^ "," ^ t ^ ")"
+  | SubE (id, t) -> sprintf "SubE (%s, %s)" id (string_of_typ t)
   | IterE (e, ids, iter) ->
     "IterE ("
     ^ structured_string_of_expr e
@@ -492,26 +503,16 @@ and structured_string_of_expr expr =
     ^ ", "
     ^ string_of_iter iter
     ^ ")"
-  | InfixE (e1, a, e2) ->
-    "InfixE ("
-    ^ structured_string_of_expr e1
-    ^ ", "
-    ^ string_of_atom a
-    ^ ", "
-    ^ structured_string_of_expr e2
-    ^ ")"
-  | CaseE (a, el) ->
-    "CaseE (" ^ string_of_atom a
-    ^ ", [" ^ structured_string_of_exprs el ^ "])"
-  | CaseE2 (op, el) ->
-    "CaseE2 (" ^ string_of_mixop op
+  | CaseE (op, el) ->
+    "CaseE (" ^ string_of_mixop op
     ^ ", [" ^ structured_string_of_exprs el ^ "])"
   | OptE None -> "OptE"
   | OptE (Some e) -> "OptE (" ^ structured_string_of_expr e ^ ")"
   | ContextKindE a -> sprintf "ContextKindE (%s)" (string_of_atom a)
   | IsDefinedE e -> "DefinedE (" ^ structured_string_of_expr e ^ ")"
   | IsCaseOfE (e, a) -> "CaseOfE (" ^ structured_string_of_expr e ^ ", " ^ string_of_atom a ^ ")"
-  | HasTypeE (e, t) -> "HasTypeE (" ^ structured_string_of_expr e ^ ", " ^ t ^ ")"
+  | HasTypeE (e, t) ->
+    sprintf "HasTypeE (%s, %s)" (structured_string_of_expr e) (string_of_typ t)
   | IsValidE e -> "IsValidE (" ^ structured_string_of_expr e ^ ")"
   | TopLabelE -> "TopLabelE"
   | TopFrameE -> "TopFrameE"

spectec/src/al/print.mli

@@ -1,11 +1,13 @@
 open Ast
 
 val string_of_list : ('a -> string) -> string -> 'a list -> string
-val string_of_atom : atom -> string 
+val string_of_atom : atom -> string
+val string_of_mixop : mixop -> id
 val string_of_value : value -> string
 val string_of_values : string -> value list -> string
 val string_of_iter : iter -> string
 val string_of_iters : iter list -> string
+val string_of_typ : typ -> string
 val string_of_expr : expr -> string
 val string_of_path : path -> string
 val string_of_arg : arg -> string