refactoring in the AST to isolate basic statements

src/ast.ml

@@ -140,10 +140,13 @@ and pp_bexpr_ lvl fmt (e : bexpr) = pp_bexpr0_ lvl fmt e.data
 
 let pp_bexpr fmt = pp_bexpr_ 0 fmt
 
-type stmt0 =
+type basic_stmt =
   | Assign of var * expr
   | Print of expr
   | Call of var located list * fname located * expr list
+
+type stmt0 =
+  | Basic of basic_stmt
   | Skip
   | Seq of stmt * stmt
   | While of bexpr * stmt
@@ -152,23 +155,21 @@ type stmt0 =
 and stmt = stmt0 located
 
 let assoc_stmt = function
-  | Assign _ | Skip | Print _ | Call _ | While (_, _) | IfThenElse (_, _, _) ->
-      NonAssoc
+  | Basic _ | Skip | While (_, _) | IfThenElse (_, _, _) -> NonAssoc
   | Seq (_, _) -> Right
 
 let prec_stmt = function
-  | Assign _ | Skip | Print _ | Call _ -> -1
+  | Basic _ | Skip -> -1
   | Seq _ | IfThenElse (_, _, None) -> 0
   | While _ -> 1
   | IfThenElse _ -> 2
 
 let is_seq s = match s.data with Seq _ -> true | _ -> false
 
-let rec pp_stmt0_ lvl fmt =
+let pp_basic_stmt fmt =
   let open Format in
   function
   | Assign (x, e) -> fprintf fmt "@[<hv 2>%a :=@ @[%a@]@]" pp_var x pp_expr e
-  | Skip -> pp_print_string fmt "skip"
   | Print e -> fprintf fmt "@[<hv 2>print@ @[%a@]@]" pp_expr e
   | Call ([], f, args) ->
       fprintf fmt "@[<hv 2>%s@[(%a)@]@]" f.data (pp_list pp_expr) args
@@ -176,6 +177,12 @@ let rec pp_stmt0_ lvl fmt =
       fprintf fmt "@[<hv 2>%a :=@ %s@[(%a)@]@]" (pp_list pp_var)
         (List.map (fun x -> x.data) dsts)
         f.data (pp_list pp_expr) args
+
+let rec pp_stmt0_ lvl fmt =
+  let open Format in
+  function
+  | Basic b_stmt -> pp_basic_stmt fmt b_stmt
+  | Skip -> pp_print_string fmt "skip"
   | Seq (s1, s2) as s ->
       let n = prec_stmt s in
       if n < lvl then fprintf fmt "@[@[<v 2>{ %a@];@ }@]" (pp_stmt0_ n) s

src/ast.mli

@@ -63,14 +63,18 @@ and bexpr = bexpr0 located
 
 val pp_bexpr : Format.formatter -> bexpr -> unit
 
-(** Statements *)
-type stmt0 =
+(** Basic statements *)
+type basic_stmt =
   | Assign of var * expr  (** assignment [Assign(x,e)] denotes "x := e" *)
   | Print of expr
       (** prints the value of an expression on the standard output *)
   | Call of var located list * fname located * expr list
       (** function call: [Call([x1;...;xk],f,[e1;...;en])] denotes "(x1,...,xk)
           := f(e1,...,en)" *)
+
+(** Statements *)
+type stmt0 =
+  | Basic of basic_stmt  (** basic statement *)
   | Skip  (** skip (no-op) *)
   | Seq of stmt * stmt  (** sequence of statements *)
   | While of bexpr * stmt  (** while loop *)

src/check.ml

@@ -58,9 +58,8 @@ let check_unique_ids error f l =
       else xs := StringSet.add x.data !xs)
     l
 
-let rec check_stmt fnames s =
-  match s.data with
-  | Skip | Assign _ | Print _ -> ()
+let check_basic_stmt fnames = function
+  | Assign _ | Print _ -> ()
   | Call (xs, f, es) ->
       let expected_ins, expected_outs =
         try StringMap.find f.data fnames
@@ -73,6 +72,11 @@ let rec check_stmt fnames s =
       if expected_outs <> actual_outs then
         raise (WfError (BadNumberOfOutputs (f, expected_outs, actual_outs)));
       check_unique_ids (fun x -> NonUniqueOutputVar x) Fun.id xs
+
+let rec check_stmt fnames s =
+  match s.data with
+  | Basic s -> check_basic_stmt fnames s
+  | Skip -> ()
   | Seq (s1, s2) | IfThenElse (_, s1, Some s2) ->
       check_stmt fnames s1;
       check_stmt fnames s2

src/parser.mly

@@ -122,9 +122,7 @@ args:
 | x = located(VAR) COMMA xs = separated_nonempty_list(COMMA, located(VAR))
 { x :: xs }
 
-stmt0:
-| SKIP
-{ Skip }
+basic_stmt:
 | x = VAR COLONEQ e = expr
 { Assign (x, e) }
 | PRINT e = expr
@@ -133,6 +131,12 @@ stmt0:
 { Call ([], f, es) }
 | xs = dsts COLONEQ f = located(VAR) es = delimited(LPAR, args, RPAR)
 { Call (xs, f, es) }
+
+stmt0:
+| s = basic_stmt
+{ Basic s }
+| SKIP
+{ Skip }
 | LBRACE s = stmts RBRACE
 { s.data }
 | WHILE b = bexpr s = stmt